From 8c376b71eb6ebc72ec44fd980dc282b8796299c7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Mar 2011 16:42:46 +0000 Subject: Added a table for using reserved names for binding names to types (in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/notation.ml | 22 ++++--------- interp/reserve.ml | 80 ++++++++++++++++++++++++++--------------------- interp/reserve.mli | 2 +- library/libnames.ml | 14 +++------ pretyping/evarutil.ml | 3 +- pretyping/namegen.ml | 11 +++++++ pretyping/namegen.mli | 5 +++ toplevel/vernacentries.ml | 2 +- 8 files changed, 75 insertions(+), 64 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 0628e7229..771e85692 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -187,30 +187,20 @@ type key = let notations_key_table = ref Gmapl.empty let prim_token_key_table = Hashtbl.create 7 - -let make_gr = function - | ConstRef con -> - ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> - IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> - ConstructRef((mind_of_kn(canonical_mind kn),i),j) - | VarRef id -> VarRef id - let glob_constr_key = function - | GApp (_,GRef (_,ref),_) -> RefKey (make_gr ref) - | GRef (_,ref) -> RefKey (make_gr ref) + | GApp (_,GRef (_,ref),_) -> RefKey (canonical_gr ref) + | GRef (_,ref) -> RefKey (canonical_gr ref) | _ -> Oth let cases_pattern_key = function - | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref)) + | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) | _ -> Oth let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) - | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args) + | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) | AList (_,_,AApp (ARef ref,args),_,_) - | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args) - | ARef ref -> RefKey(make_gr ref), None + | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | ARef ref -> RefKey(canonical_gr ref), None | _ -> Oth, None (**********************************************************************) diff --git a/interp/reserve.ml b/interp/reserve.ml index c143b5710..16d64edfc 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -16,23 +16,43 @@ open Summary open Libobject open Lib open Topconstr +open Libnames + +type key = + | RefKey of global_reference + | Oth let reserve_table = ref Idmap.empty +let reserve_revtable = ref Gmapl.empty + +let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) + | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) + | AList (_,_,AApp (ARef ref,args),_,_) + | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | ARef ref -> RefKey(canonical_gr ref), None + | _ -> Oth, None let cache_reserved_type (_,(id,t)) = - reserve_table := Idmap.add id t !reserve_table + let key = fst (aconstr_key t) in + reserve_table := Idmap.add id t !reserve_table; + reserve_revtable := Gmapl.add key (t,id) !reserve_revtable let in_reserved = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } +let freeze_reserved () = (!reserve_table,!reserve_revtable) +let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr +let init_reserved () = + reserve_table := Idmap.empty; reserve_revtable := Gmapl.empty + let _ = Summary.declare_summary "reserved-type" - { Summary.freeze_function = (fun () -> !reserve_table); - Summary.unfreeze_function = (fun r -> reserve_table := r); - Summary.init_function = (fun () -> reserve_table := Idmap.empty) } + { Summary.freeze_function = freeze_reserved; + Summary.unfreeze_function = unfreeze_reserved; + Summary.init_function = init_reserved } -let declare_reserved_type (loc,id) t = +let declare_reserved_type_binding (loc,id) t = if id <> root_of_id id then user_err_loc(loc,"declare_reserved_type", (pr_id id ++ str @@ -44,40 +64,28 @@ let declare_reserved_type (loc,id) t = with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) +let declare_reserved_type idl t = + List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl) + let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table -open Glob_term +let constr_key c = + try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c)))) + with Not_found -> Oth + +let revert_reserved_type t = + try + let l = Gmapl.find (constr_key t) !reserve_revtable in + let t = Detyping.detype false [] [] t in + list_try_find + (fun (pat,id) -> + try let _ = match_aconstr t ([],pat) in Name id + with No_match -> failwith "") l + with Not_found | Failure _ -> Anonymous -let rec unloc = function - | GVar (_,id) -> GVar (dummy_loc,id) - | GApp (_,g,args) -> GApp (dummy_loc,unloc g, List.map unloc args) - | GLambda (_,na,bk,ty,c) -> GLambda (dummy_loc,na,bk,unloc ty,unloc c) - | GProd (_,na,bk,ty,c) -> GProd (dummy_loc,na,bk,unloc ty,unloc c) - | GLetIn (_,na,b,c) -> GLetIn (dummy_loc,na,unloc b,unloc c) - | GCases (_,sty,rtntypopt,tml,pl) -> - GCases (dummy_loc,sty, - (Option.map unloc rtntypopt), - List.map (fun (tm,x) -> (unloc tm,x)) tml, - List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | GLetTuple (_,nal,(na,po),b,c) -> - GLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) - | GIf (_,c,(na,po),b1,b2) -> - GIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) - | GRec (_,fk,idl,bl,tyl,bv) -> - GRec (dummy_loc,fk,idl, - Array.map (List.map - (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty))) - bl, - Array.map unloc tyl, - Array.map unloc bv) - | GCast (_,c, CastConv (k,t)) -> GCast (dummy_loc,unloc c, CastConv (k,unloc t)) - | GCast (_,c, CastCoerce) -> GCast (dummy_loc,unloc c, CastCoerce) - | GSort (_,x) -> GSort (dummy_loc,x) - | GHole (_,x) -> GHole (dummy_loc,x) - | GRef (_,x) -> GRef (dummy_loc,x) - | GEvar (_,x,l) -> GEvar (dummy_loc,x,l) - | GPatVar (_,x) -> GPatVar (dummy_loc,x) - | GDynamic (_,x) -> GDynamic (dummy_loc,x) +let _ = Namegen.set_reserved_typed_name revert_reserved_type + +open Glob_term let anonymize_if_reserved na t = match na with | Name id as na -> diff --git a/interp/reserve.mli b/interp/reserve.mli index 0e43e5283..97b22d2b2 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -11,6 +11,6 @@ open Names open Glob_term open Topconstr -val declare_reserved_type : identifier located -> aconstr -> unit +val declare_reserved_type : identifier located list -> aconstr -> unit val find_reserved_type : identifier -> aconstr val anonymize_if_reserved : name -> glob_constr -> glob_constr diff --git a/library/libnames.ml b/library/libnames.ml index e47ce86ca..733c45af2 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -27,8 +27,7 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false let eq_gr gr1 gr2 = match gr1,gr2 with - ConstRef con1, ConstRef con2 -> - eq_constant con1 con2 + | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2 | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2 | _,_ -> gr1=gr2 @@ -56,13 +55,10 @@ let subst_global subst ref = match ref with if c'==c then ref,t else ConstructRef c', t let canonical_gr = function - | ConstRef con -> - ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> - IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> - ConstructRef((mind_of_kn(canonical_mind kn),i),j) - | VarRef id -> VarRef id + | ConstRef con -> ConstRef(constant_of_kn(canonical_con con)) + | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i) + | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j) + | VarRef id -> VarRef id let global_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0f71e47fb..774180c67 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1537,7 +1537,8 @@ let define_pure_evar_as_lambda env evd evk = | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ | _ -> error_not_product_loc dummy_loc env evd typ in let avoid = ids_of_named_context (evar_context evi) in - let id = next_name_away_with_default "x" na avoid in + let id = + next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in let newenv = push_named (id, None, dom) evenv in let filter = true::evar_filter evi in let src = evar_source evk evd1 in diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index c3c6b205d..2ad2f3515 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -205,6 +205,17 @@ let next_name_away_with_default default na avoid = let id = match na with Name id -> id | Anonymous -> id_of_string default in next_ident_away id avoid +let reserved_type_name = ref (fun t -> Anonymous) +let set_reserved_typed_name f = reserved_type_name := f + +let next_name_away_with_default_using_types default na avoid t = + let id = match na with + | Name id -> id + | Anonymous -> match !reserved_type_name t with + | Name id -> id + | Anonymous -> id_of_string default in + next_ident_away id avoid + let next_name_away = next_name_away_with_default "H" let make_all_name_different env = diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 0c9fc4f6b..637cbf64d 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -59,6 +59,11 @@ val next_name_away : name -> identifier list -> identifier (** default is "H" * val next_name_away_with_default : string -> name -> identifier list -> identifier +val next_name_away_with_default_using_types : string -> name -> + identifier list -> types -> identifier + +val set_reserved_typed_name : (types -> name) -> unit + (********************************************************************* Making name distinct for displaying *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e3d3d2032..ddd97dda5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -804,7 +804,7 @@ let vernac_reserve bl = let t = Constrintern.interp_type Evd.empty (Global.env()) c in let t = Detyping.detype false [] [] t in let t = aconstr_of_glob_constr [] [] t in - List.iter (fun id -> Reserve.declare_reserved_type id t) idl) + Reserve.declare_reserved_type idl t) in List.iter sb_decl bl let vernac_generalizable = Implicit_quantifiers.declare_generalizable -- cgit v1.2.3