X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.mli;h=406a8293bf8710f83cdf353d9b508c194f34818f;hb=ef2b2a9ce0c7ba6f05754e3da1e5e9fbbdf88d15;hp=c7e3be4797645d6ce1412f48682eefbf2778b52b;hpb=b14ff66c953e6a73e9ac2fe8d42dd68e92e58f53;p=goals.git

diff --git a/src/ast.mli b/src/ast.mli
index c7e3be4..406a829 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -17,7 +17,7 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-module StringMap : sig
+module Env : sig
   type key = string
   type 'a t
   val empty: 'a t
@@ -26,6 +26,9 @@ module StringMap : 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 *)
@@ -36,19 +39,19 @@ val string_loc : unit -> loc -> string
 
 (** An environment is a set of variable and goal definitions, mapping
     variable or goal name -> expression. *)
-type env = expr StringMap.t
+type env = expr Env.t
 and pattern =
-  (** match tactic such as file ("filename") *)
+  (** match tactic such as *file ("filename") *)
   | PTactic of loc * id * substs list
-  (** match named variable, which must be a string or list *)
-  | PVar of loc * id
 and expr =
-  (** 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
+  (** goal (params) = patterns : exprs code *)
+  | EGoalDefn of loc * goal
+  (** tactic (params) = code *)
+  | ETacticDefn of loc * tactic
+  (** call goalname (params) etc. *)
+  | ECallGoal of loc * id * expr list
+  (** call *tactic (params) etc. *)
+  | ETacticConstructor of loc * id * expr list
   (** variable, or goal call with no parameters *)
   | EVar of loc * id
   (** list *)
@@ -59,7 +62,10 @@ and expr =
   | EConstant of loc * constant
 and constant =
   | CString of string
-and goal = id list * pattern list * expr list * code option
+and goal = param_decl list * pattern list * expr list * code option
+and tactic = param_decl list * code
+  (** Goal/tactic parameter. *)
+and param_decl = id
 and id = string
 and code = substs
 and substs = subst list
@@ -69,6 +75,34 @@ and subst =
   (** %-substitution. *)
   | SVar of id
 
+(** Look up a variable in the environment.  Raise [Failure _]
+    if not found. *)
+val getvar : env -> loc -> id -> expr
+
+(** Look up a goal in the environment.  Raise [Failure _] if not
+    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 _]. *)
+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
@@ -79,4 +113,8 @@ module Substs : sig
   val add_var : t -> string -> unit
 end
 
+(** %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