Implement functions.

[goals.git] / src / ast.mli

diff --git a/src/ast.mli b/src/ast.mli
index 56bfa7b..f8b88f0 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -26,6 +26,9 @@ module Env : sig
   val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val filter: (key -> 'a -> bool) -> 'a t -> 'a t
   val bindings: 'a t -> (key * 'a) list
+
+  (* This is not the normal Map.merge function. *)
+  val merge : 'a t -> 'a t -> 'a t
 end
 
 (** Location where we parsed from $loc = $startpos, $endpos *)
@@ -42,13 +45,15 @@ and pattern =
   | PTactic of loc * id * substs list
 and expr =
   (** goal (params) = patterns : exprs code *)
-  | EGoal of loc * goal
+  | EGoalDefn of loc * goal
+  (** function (params) = code *)
+  | EFuncDefn of loc * func
   (** tactic (params) = code *)
-  | ETactic of loc * tactic
-  (** call goalname (params) etc. *)
-  | ECallGoal of loc * id * expr list
+  | ETacticDefn of loc * tactic
+  (** call goal (params) or function (params) *)
+  | ECall of loc * id * expr list
   (** call *tactic (params) etc. *)
-  | ECallTactic of loc * id * expr list
+  | ETacticCtor of loc * id * expr list
   (** variable, or goal call with no parameters *)
   | EVar of loc * id
   (** list *)
@@ -60,8 +65,9 @@ and expr =
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option
+and func = param_decl list * code
 and tactic = param_decl list * code
-  (** Goal/tactic parameter. *)
+  (** Goal/func/tactic parameter. *)
 and param_decl = id
 and id = string
 and code = substs
@@ -80,26 +86,14 @@ val getvar : env -> loc -> id -> expr
     found or if the named variable is not a goal. *)
 val getgoal : env -> loc -> id -> goal
 
+(** Look up a function in the environment.  Raise [Failure _] if not
+    found or if the named variable is not a function. *)
+val getfunc : env -> loc -> id -> func
+
 (** Look up a tactic in the environment.  Raise [Failure _] if not
     found or if the named variable is not a tactic. *)
 val gettactic : env -> loc -> id -> tactic
 
-(** Take any expression and simplify it down to a constant.
-    If the expression cannot be simplified then this raises
-    [Failure _]. *)
-val to_constant : env -> expr -> constant
-
-(** Take a substitution list and try to turn it into a simple
-    string by evaluating every variable.  If not possible this
-    raises [Failure _]. *)
-val substitute : env -> loc -> substs -> string
-
-(** Similar to {!substitute} except this is used where we will
-    pass the result immediately to the shell to execute.  Variables
-    are substituted with shell quoted strings.  Raises [Failure _]
-    on error. *)
-val to_shell_script : env -> loc -> substs -> string
-
 (** This is used for incrementally building Ast.substs in the parser. *)
 module Substs : sig
   type t
@@ -110,9 +104,8 @@ module Substs : sig
   val add_var : t -> string -> unit
 end
 
-(** Print all definitions in an environment. *)
-val print_env : out_channel -> env -> unit
-
 (** %a formatters. *)
+val print_env : out_channel -> env -> unit
 val string_pattern : unit -> pattern -> string
 val string_expr : unit -> expr -> string
+val print_expr : out_channel -> expr -> unit