X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.mli;h=d4f87097e2fa2c50d86a56b6b55d985e2a72032c;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a5267b04463b8493bcdf28c72989551611feb182;hpb=b19ee5bd8a25151b78eb1c78f98e6ab1f4b325ff;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli
index a5267b044..d4f87097e 100644
--- a/helm/ocaml/cic_notation/cicNotationEnv.mli
+++ b/helm/ocaml/cic_notation/cicNotationEnv.mli
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception Value_not_found of string
+(** {2 Types} *)
 
 type value =
   | TermValue of CicNotationPt.term
@@ -39,12 +39,40 @@ type value_type =
   | 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 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
+val declarations_of_term: CicNotationPt.term -> declaration list
+val combine: declaration list -> value list -> t  (** @raise Invalid_argument *)
 
-  (** 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  (** @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} *)
 
@@ -57,7 +85,8 @@ val list_binding_of_name: declaration -> binding  (* [] binding *)
 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