Implement -include (optional include) command.

[goals.git] / src / ast.mli

diff --git a/src/ast.mli b/src/ast.mli
index 9bb2c9a..831878d 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 *)
@@ -40,16 +43,15 @@ type env = expr Env.t
 and pattern =
   (** match tactic such as *file ("filename") *)
   | PTactic of loc * id * substs list
-  (** match named variable, which must be a string, ETactic or
-      a list of those *)
-  | PVar of loc * id
 and expr =
-  (** goal (params) = patterns : exprs = code *)
+  (** goal (params) = patterns : exprs code *)
   | EGoal of loc * goal
-  (** goalname (params) etc. *)
-  | ECall of loc * id * expr list
-  (** *tactic (params) etc. *)
-  | ETactic of loc * id * expr list
+  (** tactic (params) = code *)
+  | ETactic of loc * tactic
+  (** call goalname (params) etc. *)
+  | ECallGoal of loc * id * expr list
+  (** call *tactic (params) etc. *)
+  | ECallTactic of loc * id * expr list
   (** variable, or goal call with no parameters *)
   | EVar of loc * id
   (** list *)
@@ -61,7 +63,8 @@ and expr =
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option
-  (** Goal parameter is the parameter name and an optional default value. *)
+and tactic = param_decl list * code
+  (** Goal/tactic parameter. *)
 and param_decl = id
 and id = string
 and code = substs
@@ -80,6 +83,10 @@ 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 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 _]. *)