Passage à des contextes de vars et de rels pouvant contenir des déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 72 insertions, 104 deletions

diff --git a/kernel/sign.mli b/kernel/sign.mli
index 763a674716..3add55894c 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,107 +7,75 @@ open Generic
 open Term
 (*i*)
 
-(* Signatures of named variables. *)
-
-type 'a signature
-
-val nil_sign : 'a signature
-val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
-val lookup_sign : identifier -> 'a signature -> (identifier * 'a)
-
-val rev_sign : 'a signature -> 'a signature
-val map_sign_typ : ('a -> 'b) -> 'a signature -> 'b signature
-val isnull_sign : 'a signature -> bool
-val hd_sign : 'a signature -> identifier * 'a
-val tl_sign : 'a signature -> 'a signature
-
-(* [sign_it f sign a] iters [f] on [sign] starting from [a] and
-   peeling [sign] from the oldest declaration *)
-
-val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
-
-(* [it_sign f a sign] iters [f] on [sign] starting from [a] and
-   peeling [sign] from the more recent declaration *)
-
-val it_sign : ('b -> identifier -> 'a -> 'b) -> 'b -> 'a signature -> 'b
-
-val concat_sign : 'a signature -> 'a signature -> 'a signature
-
-val ids_of_sign : 'a signature -> identifier list
-val vals_of_sign : 'a signature -> 'a list
-
-val nth_sign : 'a signature -> int -> (identifier * 'a)
-val map_sign_graph : (identifier -> 'a -> 'b) -> 'a signature -> 'b list
-val list_of_sign : 'a signature -> (identifier * 'a) list
-val make_sign    : (identifier * 'a) list -> 'a signature
-val do_sign : (identifier -> 'a -> unit) -> 'a signature -> unit
-val uncons_sign : 'a signature -> (identifier * 'a) * 'a signature
-val sign_length : 'a signature -> int
-val mem_sign    : 'a signature -> identifier -> bool
-val modify_sign : identifier -> 'a -> 'a signature -> 'a signature
-
-val exists_sign : (identifier -> 'a -> bool) -> 'a signature -> bool
-val sign_prefix : identifier -> 'a signature -> 'a signature
-val add_sign_after : 
-  identifier -> (identifier * 'a) -> 'a signature -> 'a signature
-val add_sign_replacing : 
-  identifier -> (identifier * 'a) -> 'a signature -> 'a signature
-val prepend_sign : 'a signature -> 'a signature -> 'a signature
-
-val dunbind : identifier -> 'a signature -> 'a -> 'b term 
-  -> 'a signature * 'b term
-val dunbindv : identifier -> 'a signature -> 'a -> 'b term 
-  -> 'a signature * 'b term array
-val dbind : 'a signature -> 'b term -> 'a * 'b term
-val dbindv : 'a signature -> 'b term array -> 'a * 'b term
-
-(*s Signatures with named and de Bruijn variables. *)
-
-type 'a db_signature
-type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
-
-val gLOB : 'b signature -> ('b,'a) sign
-
-val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign 
-val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign
-val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
-val lookup_rel : int -> ('b,'a) sign  -> (name * 'a)
-val mem_glob : identifier -> ('b,'a) sign -> bool
-
-val nil_dbsign : 'a db_signature
-val get_globals : ('b,'a) sign -> 'b signature
-val get_rels : ('b,'a) sign -> 'a db_signature
-val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
-val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c
-val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign
-val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
-val isnull_rel_env : ('a,'b) sign -> bool
-val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
-val ids_of_env : ('a, 'b) sign -> identifier list
-val number_of_rels : ('b,'a) sign -> int
-
-(*i This is for Cases i*)
-(* raise [Not_found] if the integer is out of range *)
-val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign
-
-val make_all_name_different : ('a, 'b) sign -> ('a, 'b) sign
-
-type ('b,'a) search_result =
-  | GLOBNAME of identifier  * 'b
-  | RELNAME of int * 'a
-
-val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result
-
-
-type 'b assumptions = (typed_type,'b) sign
-type context = (typed_type,typed_type) sign
-type var_context = typed_type signature
-
-val unitize_env : 'a assumptions -> unit assumptions
-
-
-
-
-
-
-
+(*s Signatures of _ordered_ named variables, intended to be accessed by name *)
+
+type var_context = var_declaration list
+
+val add_var : identifier * constr option * typed_type -> var_context -> var_context
+val add_var_decl : identifier * typed_type -> var_context -> var_context
+val add_var_def : identifier * constr * typed_type -> var_context ->var_context
+val lookup_id : identifier -> var_context -> constr option * typed_type
+val lookup_id_type : identifier -> var_context -> typed_type
+val lookup_id_value : identifier -> var_context -> constr option 
+val pop_var : identifier -> var_context -> var_context
+val empty_var_context : var_context
+val ids_of_var_context : var_context -> identifier list
+val map_var_context : (constr -> constr) -> var_context -> var_context
+val mem_var_context : identifier -> var_context -> bool
+val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a
+val fold_var_context_both_sides :
+  ('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a
+val it_var_context_quantifier :
+  (var_declaration -> constr -> constr) -> constr -> var_context -> constr
+val instantiate_sign : var_context -> constr list -> (identifier * constr) list
+val keep_hyps : Idset.t -> var_context -> var_context
+
+(*s Signatures of ordered optionally named variables, intended to be
+   accessed by de Bruijn indices *)
+
+type rel_context = rel_declaration list
+
+val add_rel : (name * constr option * typed_type) -> rel_context -> rel_context
+val add_rel_decl : (name * typed_type) -> rel_context -> rel_context
+val add_rel_def : (name * constr * typed_type) -> rel_context -> rel_context
+val lookup_rel_type : int -> rel_context -> name * typed_type
+val lookup_rel_value : int -> rel_context -> constr option
+val lookup_rel_id : identifier -> rel_context -> int * typed_type
+val empty_rel_context : rel_context
+val rel_context_length : rel_context -> int
+val lift_rel_context : int -> rel_context -> rel_context
+val concat_rel_context : newer:rel_context -> older:rel_context -> rel_context
+val ids_of_rel_context : rel_context -> identifier list
+val decls_of_rel_context : rel_context -> (name * constr) list
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+
+(*s This is used to translate names into de Bruijn indices and
+   vice-versa without to care about typing information *)
+
+type names_context
+val add_name : name -> names_context -> names_context
+val lookup_name_of_rel : int -> names_context -> name
+val lookup_rel_of_name : identifier -> names_context -> int
+val names_of_rel_context : rel_context -> names_context
+val empty_names_context : names_context
+
+(*s Term destructors *)
+
+(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins
+   into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
+   product nor a let. *)
+val decompose_prod_assum : constr -> rel_context * constr
+
+(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins
+   into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
+   lambda nor a let. *)
+val decompose_lam_assum : constr -> rel_context * constr
+
+(* Given a positive integer n, transforms a product term 
+   $(x_1:T_1)..(x_n:T_n)T$
+   into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
+val decompose_prod_n_assum : int -> constr -> rel_context * constr
+
+(* Given a positive integer $n$, transforms a lambda term 
+   $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
+val decompose_lam_n_assum : int -> constr -> rel_context * constr