ancien names decoupe en names + sign

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

2 files changed, 277 insertions, 0 deletions

diff --git a/kernel/sign.ml b/kernel/sign.ml
new file mode 100644
index 0000000000..7aa3f75e9a
--- /dev/null
+++ b/kernel/sign.ml
@@ -0,0 +1,209 @@
+
+(* $Id$ *)
+
+open Names
+open Util
+
+(* Signatures *)
+
+type 'a signature = identifier list * 'a list
+type 'a db_signature = (name * 'a) list
+type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
+
+let gLOB hyps = ENVIRON (hyps,[])
+
+let ids_of_sign (idl,_) = idl
+let vals_of_sign (_,vals) = vals
+let add_sign (id,ty) (idl,tyl) = (id::idl,ty::tyl)
+let sign_it f (idl,tyl) e = List.fold_right2 f idl tyl e
+let it_sign f e (idl,tyl) = List.fold_left2 f e idl tyl
+let nil_sign = ([],[])
+let rev_sign (idl,tyl) = (List.rev idl, List.rev tyl)
+let map_sign_typ f (idl,tyl) = (idl, List.map f tyl)
+let concat_sign (idl1,tyl1) (idl2,tyl2) = (idl1@idl2, tyl1@tyl2)
+let diff_sign (idl1,tyl1) (idl2,tyl2) = 
+  (subtract idl1 idl2, subtract tyl1 tyl2)
+let nth_sign (idl,tyl) n = (List.nth idl (n-1), List.nth tyl (n-1))
+let map_sign_graph f (ids,tys) = List.map2 f ids tys
+
+let isnull_sign = function 
+  | ([],[])     -> true
+  | (_::_,_::_) -> false
+  | _           -> invalid_arg "isnull_sign"
+
+let hd_sign = function
+  | (id::_,ty::_) -> (id,ty)
+  | _             -> failwith "hd_sign"
+
+let tl_sign = function
+  | (_::idl,_::tyl) -> (idl,tyl)
+  | _               -> failwith "tl_sign"
+
+let lookup_sign id (dom,rang) = 
+  let rec aux = function
+    | ([],          [])        -> raise Not_found
+    | ((id'::id'l), (ty::tyl)) -> if id' = id then (id',ty) else aux (id'l,tyl)
+    | _                        -> anomaly "Names: lookup_sign"
+  in 
+  aux (dom,rang)
+
+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
+
+let uncons_sign = function
+  | (id::idl,ty::tyl) -> ((id,ty),(idl,tyl))
+  | _ -> anomaly "signatures are being manipulated in a non-abstract way"
+
+let sign_length (idl,tyl) =
+  let lenid = List.length idl
+  and lenty = List.length tyl in
+  if lenid = lenty then 
+    lenid
+  else 
+    invalid_arg "lookup_sign"
+
+let mem_sign sign id = List.mem id (ids_of_sign sign)
+
+let modify_sign id ty = 
+  let rec modrec = function
+    | [],[] -> invalid_arg "modify_sign"
+    | sign  -> 
+	let (id',ty') = hd_sign sign in
+	if id = id' then
+      	  add_sign (id,ty) (tl_sign sign)
+	else
+      	  add_sign (id',ty') (modrec (tl_sign sign))
+  in 
+  modrec
+
+let exists_sign f = 
+  let rec exrec sign =
+    if isnull_sign sign then 
+      false
+    else 
+      let ((id,t),tl) = uncons_sign sign in
+      f id t or exrec tl
+  in 
+  exrec
+
+(* [sign_prefix id sign] returns the signature up to and including id,
+   with all later assumptions stripped off.  It is an error to call it
+   with a signature not containing id, and that error is generated
+   with error. *)
+
+let sign_prefix id sign = 
+  let rec prefrec sign =
+    if isnull_sign sign then
+      error "sign_prefix"
+    else
+      let ((id',t),sign') = uncons_sign sign in
+      if id' = id then sign else prefrec sign'
+  in 
+  prefrec sign
+
+let add_sign_after whereid (id,t) sign = 
+  let rec addrec sign =
+    if isnull_sign sign then
+      error "add_sign_after"
+    else
+      let ((id',t'),sign') = uncons_sign sign in
+      if id' = whereid then add_sign (id,t) sign
+      else add_sign (id',t') (addrec sign')
+  in 
+  addrec sign
+
+let add_sign_replacing whereid (id,t) sign = 
+  let rec addrec sign =
+    if isnull_sign sign then
+      error "add_replacing_after"
+    else
+      let ((id',t'),sign') = uncons_sign sign in
+      if id' = whereid then add_sign (id,t) sign'
+      else add_sign (id',t') (addrec sign')
+  in 
+  addrec sign
+  
+(* [prepend_sign Gamma1 Gamma2]
+   prepends Gamma1 to the front of Gamma2, given that their namespaces
+   are distinct. *)
+
+let prepend_sign gamma1 gamma2 =
+  if [] = intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then
+    let (ids1,vals1) = gamma1
+    and (ids2,vals2) = gamma2 in
+    (ids1@ids2, vals1@vals2)
+  else
+    invalid_arg "prepend_sign"
+
+
+(* Signatures + de Bruijn environments *)
+
+let dbenv_it f (ENVIRON(_,dbs)) init =
+  List.fold_right (fun (na,t) v -> f na t v) dbs init
+
+let it_dbenv f init (ENVIRON(_,dbs)) =
+  List.fold_left (fun v (na,t) -> f v na t) init dbs
+
+let isnull_rel_env (ENVIRON(_,dbs)) = (dbs = [])
+let uncons_rel_env (ENVIRON(sign,dbs)) = List.hd dbs,ENVIRON(sign,List.tl dbs)
+
+let ids_of_env (ENVIRON(sign,dbenv)) =
+  let filter (n,_) l = match n with (Name id) -> id::l | Anonymous -> l in
+  (ids_of_sign sign) @ (List.fold_right filter dbenv [])
+
+let get_globals (ENVIRON(g,_)) = g
+let get_rels (ENVIRON(_,r)) = r
+
+let add_rel (n,x) (ENVIRON(g,r)) = (ENVIRON(g,(n,x)::r))
+
+let add_glob (id,x) (ENVIRON((dom,rang),r)) = (ENVIRON((id::dom,x::rang),r))
+
+let lookup_glob id (ENVIRON((dom,rang),_)) = 
+  let rec aux = function
+    | ([],          [])        -> raise Not_found
+    | ((id'::id'l), (ty::tyl)) -> if id' = id then (id',ty) else aux (id'l,tyl)
+    | _                        -> anomaly "Names: lookup_glob"
+  in 
+  aux (dom,rang)
+
+let mem_glob id (ENVIRON((dom,_),_)) = List.mem id dom
+
+let lookup_rel n (ENVIRON(_,r)) = 
+  let rec lookrec n l = match (n,l) with
+    | (1, ((na,x)::l)) -> (na,x)
+    | (n, (_::l))      -> lookrec (n-1) l
+    | (_, [])          -> raise Not_found
+  in 
+  lookrec n r
+
+let rec lookup_rel_id id (ENVIRON(_,r)) = 
+  let rec lookrec = function
+    | (n, ((Anonymous,x)::l)) -> lookrec (n+1,l)
+    | (n, ((Name id',x)::l))  -> if id' = id then (n,x) else lookrec (n+1,l)
+    | (_, [])                 -> raise Not_found
+  in 
+  lookrec (1,r)
+
+let map_rel_env f (ENVIRON(g,r)) =
+  ENVIRON (g,List.map (fun (na,x) -> (na,f x)) r)
+
+let map_var_env f (ENVIRON((dom,rang),r)) =
+  ENVIRON (List.fold_right2 
+	     (fun na x (doml,rangl) -> (na::doml,(f x)::rangl))
+      	     dom rang ([],[]),r)
+
+
+type ('b,'a) search_result =
+  | GLOBNAME of identifier  * 'b
+  | RELNAME of int * 'a
+
+let lookup_id id env =
+  try 
+    let (x,y) = lookup_rel_id id env in RELNAME(x,y)
+  with 
+    | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
+
diff --git a/kernel/sign.mli b/kernel/sign.mli
new file mode 100644
index 0000000000..2cbab3672d
--- /dev/null
+++ b/kernel/sign.mli
@@ -0,0 +1,68 @@
+
+(* $Id$ *)
+
+open Names
+
+type 'a signature = identifier list * 'a list
+type 'a db_signature = (name * 'a) list
+type ('a,'b) env = ENVIRON of 'a signature * 'b db_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
+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
+
+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 gLOB : 'b signature -> ('b,'a) env
+
+val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env 
+val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env
+val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b)
+val lookup_rel : int -> ('b,'a) env  -> (name * 'a)
+val mem_glob : identifier -> ('b,'a) env -> bool
+
+val get_globals : ('b,'a) env -> 'b signature
+val get_rels : ('b,'a) env -> 'a db_signature
+val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c
+val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c
+val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env
+val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env
+val isnull_rel_env : ('a,'b) env -> bool
+val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env
+val ids_of_env : ('a, 'b) env -> identifier list
+
+type ('b,'a) search_result =
+  | GLOBNAME of identifier  * 'b
+  | RELNAME of int * 'a
+
+val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
+
+