* http://helm.cs.unibo.it/
*)
-exception Value_not_found of string
-
(** {2 Types} *)
type value =
| OptType of value_type
| ListType of value_type
+ (** looked up value not found in environment *)
+exception Value_not_found of string
+
+ (** looked up value has the wrong type
+ * parameters are value name and value type in environment *)
+exception Type_mismatch of string * value_type
+
type declaration = string * value_type
type binding = string * (value_type * value)
type t = binding list
val term_of_value: value -> CicNotationPt.term
val well_typed: value_type -> value -> bool
+val declarations_of_env: t -> declaration list
+val declarations_of_term: CicNotationPt.term -> declaration list
+val combine: declaration list -> value list -> t (** @raise Invalid_argument *)
+
(** {2 Environment lookup} *)
-val lookup_value: t -> string -> value
-val lookup_num: t -> string -> string
-val lookup_string: t -> string -> string
+val lookup_value: t -> string -> value (** @raise Value_not_found *)
+
+(** lookup_* functions below may raise Value_not_found and Type_mismatch *)
+
val lookup_term: t -> string -> CicNotationPt.term
+val lookup_string: t -> string -> string
+val lookup_num: t -> string -> string
+val lookup_opt: t -> string -> value option
+val lookup_list: t -> string -> value list
+
+val remove_name: t -> string -> t
+val remove_names: t -> string list -> t
(** {2 Bindings mangling} *)
val opt_declaration: declaration -> declaration (* t -> OptType t *)
val list_declaration: declaration -> declaration (* t -> ListType t *)
+(** 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
+