* 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 *)
+type loc = Lexing.position * Lexing.position
+val noloc : loc
+val print_loc : out_channel -> loc -> unit
+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") *)
- | PTactic of id * substs list
- (** match named variable, which must be a string or list *)
- | PVar of id
+ | PPred of loc * id * substs list
+ (** match predicate such as is-file ("filename") *)
and expr =
- (** goal (params) = patterns : exprs = code *)
- | EGoal of goal
- (** goalname (params), tactic (params) etc. *)
- | ECall of id * expr list
- (** variable *)
- | EVar of id
+ | EGoalDefn of loc * goal
+ (** goal (params) = patterns : exprs code *)
+ | EFuncDefn of loc * func
+ (** function (params) = code *)
+ | EPredDefn of loc * pred
+ (** predicate (params) = code *)
+ | ECall of loc * id * expr list
+ (** call goal (params) or function (params) *)
+ | EPredCtor of loc * id * expr list
+ (** constructor is-predicate (params) *)
+ | EVar of loc * id
+ (** variable, or goal call with no parameters *)
+ | EList of loc * expr list
(** list *)
- | EList of expr list
+ | ESubsts of loc * substs
(** string with %-substitutions *)
- | ESubsts of substs
+ | EConstant of loc * constant
(** constant expression, such as a plain string, int, boolean, etc. *)
- | EConstant of 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 func = param_decl list * returning * bool * code
+and pred = param_decl list * code
+and param_decl = id (** goal/func/pred parameter. *)
and id = string
-and code = substs
+and code = substs * bool (** code + quiet flag *)
+and returning = RetExpr | RetStrings | RetString
and substs = subst list
and subst =
- (** String literal part. *)
| SString of string
- (** %-substitution. *)
+ (** String literal part. *)
| SVar of id
+ (** %-substitution. *)
+
+val getvar : env -> loc -> id -> expr
+(** Look up a variable in the environment. Raise [Failure _]
+ if not found. *)
+
+val getgoal : env -> loc -> id -> goal
+(** Look up a goal in the environment. Raise [Failure _] if not
+ found or if the named variable is not a goal. *)
+
+val getfunc : env -> loc -> id -> func
+(** Look up a function in the environment. Raise [Failure _] if not
+ found or if the named variable is not a function. *)
+
+val getpred : env -> loc -> id -> pred
+(** Look up a predicate in the environment. Raise [Failure _] if not
+ found or if the named variable is not a predicate. *)
(** This is used for incrementally building Ast.substs in the parser. *)
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