* 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
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 *)
(** 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 *)
| 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
(** %-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
val add_var : t -> string -> unit
end
+(** Print all definitions in an environment. *)
val print_env : out_channel -> env -> unit
+(** %a formatters. *)
val string_pattern : unit -> pattern -> string
+val string_expr : unit -> expr -> string