* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-type file = stmt list
-and stmt =
- (* let id = expr *)
- | Let of id * expr
- (* goal id (params) = patterns : exprs = code *)
- | Goal of id * id list * pattern list * expr list * code option
+module StringMap : sig
+ type key = string
+ type 'a t
+ val empty: 'a t
+ val add: key -> 'a -> 'a t -> 'a t
+ val find: key -> 'a t -> 'a
+ 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
+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
and pattern =
- (* match tactic such as file ("filename") *)
- | PTactic of id * substs list
- (* match named variable, which must be a string or list *)
- | PVarSubst of id
+ (** 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 =
- (* goalname (params), tactic (params) etc. *)
- | ECall of id * expr list
- (* variable *)
- | EVar of id
- (* string with %-substitutions *)
- | EString of substs
- (* list *)
- | EList of expr list
+ (** 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
+ (** variable, or goal call with no parameters *)
+ | EVar of loc * id
+ (** list *)
+ | EList of loc * expr list
+ (** string with %-substitutions *)
+ | ESubsts of loc * substs
+ (** constant expression, such as a plain string, int, boolean, etc. *)
+ | EConstant of loc * constant
+and constant =
+ | CString of string
+and goal = id list * pattern list * expr list * code option
and id = string
and code = substs
and substs = subst list
and subst =
- (* String literal part. *)
+ (** String literal part. *)
| SString of string
- (* %-substitution. *)
+ (** %-substitution. *)
| SVar of id
-(* This is used for incrementally building Ast.substs in the parser. *)
+(** This is used for incrementally building Ast.substs in the parser. *)
module Substs : sig
type t
val create : unit -> t
val add_var : t -> string -> unit
end
-val print_file : out_channel -> file -> unit
+val print_env : out_channel -> env -> unit