Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in

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

5 files changed, 48 insertions, 31 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7507be838a..0ef449ff42 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -33,7 +33,7 @@ type env = {
   env_universes : universes }
 
 let empty_env = { 
-  env_context = ENVIRON (([],[]),[]);
+  env_context = ENVIRON (nil_sign,nil_dbsign);
   env_globals = {
     env_constants = Spmap.empty;
     env_inductives = Spmap.empty;
@@ -61,12 +61,8 @@ let change_hyps f env =
  * if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
  * then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
  *)
-let change_name_rel env j id =
-  let ENVIRON(sign,db) = context env in
-  (match list_chop (j-1) db with
-       db1,((_,ty)::db2) ->
-	 {env with env_context = ENVIRON(sign,db1@(Name id,ty)::db2)}
-     | _ -> assert false)
+let change_name_rel env j id = 
+  { env with env_context = change_name_env (context env) j id }
 (****)
 
 let push_rel idrel env =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b2c5df74f6..be489e047a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -439,11 +439,11 @@ let pop_vars idl env =
     if n = 0 then
       sign
     else
-      match sign with
-	| (id::ids,_::tys) ->
+      if isnull_sign sign then anomaly "pop_vars"
+      else
+	let (id,_) = hd_sign sign in 
 	    if not (List.mem id idl) then anomaly "pop_vars";
-	    remove (pred n) (ids,tys) 
-	| _ -> anomaly "pop_vars"
+	    remove (pred n) (tl_sign sign)
   in
   change_hyps (remove (List.length idl)) env
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 0b34c7edf3..00a160ffd6 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -53,6 +53,7 @@ let list_of_sign (ids,tys) =
   try List.combine ids tys
   with _ -> anomaly "Corrupted signature"
 
+
 let make_sign = List.split
 let do_sign f (ids,tys) = List.iter2 f ids tys
 
@@ -163,6 +164,9 @@ let dbindv sign cl =
   and sign' = tl_sign sign in
   (ty,DLAMV(Name id,Array.map (subst_var id) cl))
 
+(* de Bruijn environments *)
+
+let nil_dbsign = []
 
 (* Signatures + de Bruijn environments *)
 
@@ -220,6 +224,13 @@ let map_var_env f (ENVIRON((dom,rang),r)) =
 	     (fun na x (doml,rangl) -> (na::doml,(f x)::rangl))
       	     dom rang ([],[]),r)
 
+let number_of_rels (ENVIRON(_,db)) = List.length db
+
+let change_name_env (ENVIRON(sign,db)) j id =
+  match list_chop (j-1) db with
+    | db1,((_,ty)::db2) -> ENVIRON(sign,db1@(Name id,ty)::db2)
+    | _ -> raise Not_found
+
 let unitize_env env = map_rel_env (fun _ -> ()) env
 
 type ('b,'a) search_result =
diff --git a/kernel/sign.mli b/kernel/sign.mli
index e2ef7d4a1e..1970285895 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
 
 (* Signatures of named variables. *)
 
-type 'a signature = identifier list * 'a list
+type 'a signature
 
 val nil_sign : 'a signature
 val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
@@ -23,6 +23,7 @@ val tl_sign : 'a signature -> 'a signature
 val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
 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
 
@@ -64,6 +65,7 @@ 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
@@ -73,6 +75,11 @@ 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
 
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
@@ -87,3 +94,9 @@ type var_context = typed_type signature
 
 val unitize_env : 'a assumptions -> unit assumptions
 
+
+
+
+
+
+
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4b20f3b0a9..1feb20e82c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -51,25 +51,22 @@ let relative env n =
 
 (* Checks if a context of variable is included in another one. *)
 
-let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) =
-  let rec aux = function
-    | ([], [], _, _) -> true
-    | (_, _, [], []) -> false
-    | ((id1::idl1), (ty1::tyl1), idl2, tyl2) ->
-        let rec search = function
-          | ([], []) -> false
-          | ((id2::idl2), (ty2::tyl2)) ->
-              if id1 = id2 then
-		(is_conv env sigma (body_of_type ty1) (body_of_type ty2))
-		& aux (idl1,tyl1,idl2,tyl2)
-              else 
-		search (idl2,tyl2)
-          | (_, _) -> invalid_arg "hyps_inclusion"
-        in 
-	search (idl2,tyl2)
-    | (_, _, _, _) -> invalid_arg "hyps_inclusion"
-  in
-  aux (idl1,tyl1,idl2,tyl2) 
+let rec hyps_inclusion env sigma sign1 sign2 =
+  if isnull_sign sign1 then true
+  else
+    let (id1,ty1) = hd_sign sign1 in
+    let rec search sign2 =
+      if isnull_sign sign2 then false
+      else
+	let (id2,ty2) = hd_sign sign2 in
+        if id1 = id2 then
+	  (is_conv env sigma (body_of_type ty1) (body_of_type ty2))
+	  &
+	  hyps_inclusion env sigma (tl_sign sign1) (tl_sign sign2)
+        else 
+	  search (tl_sign sign2)
+    in 
+    search sign2
 
 (* Checks if the given context of variables [hyps] is included in the
    current context of [env]. *)