-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 Env : 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
+
+ (* 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 Env.t