exception Value_not_found of string
+(** {2 Types} *)
+
type value =
| TermValue of CicNotationPt.term
| StringValue of string
type declaration = string * value_type
type binding = string * (value_type * value)
-type env_type = binding list
+type t = binding list
+
+val declaration_of_var: CicNotationPt.pattern_variable -> declaration
+val value_of_term: CicNotationPt.term -> value
+val term_of_value: value -> CicNotationPt.term
+val well_typed: value_type -> value -> bool
+
+val declarations_of_env: t -> declaration list
- (** fills a term pattern instantiating variable magics *)
-val instantiate: env:env_type -> CicNotationPt.term -> CicNotationPt.term
+(** {2 Environment lookup} *)
+
+val lookup_value: t -> string -> value
+val lookup_num: t -> string -> string
+val lookup_string: t -> string -> string
+val lookup_term: t -> string -> CicNotationPt.term
+
+val remove: t -> string -> t
(** {2 Bindings mangling} *)
val opt_declaration: declaration -> declaration (* t -> OptType t *)
val list_declaration: declaration -> declaration (* t -> ListType t *)
-(** {2 Debugging} *)
-
-val set_pp_term: (CicNotationPt.term -> string) -> unit
+(** given a list of environments bindings a set of names n_1, ..., n_k, returns
+ * a single environment where n_i is bound to the list of values bound in the
+ * starting environments *)
+val coalesce_env: declaration list -> t list -> t