aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml22
-rw-r--r--interp/reserve.ml80
-rw-r--r--interp/reserve.mli2
-rw-r--r--library/libnames.ml14
-rw-r--r--pretyping/evarutil.ml3
-rw-r--r--pretyping/namegen.ml11
-rw-r--r--pretyping/namegen.mli5
-rw-r--r--toplevel/vernacentries.ml2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 18:49:12 +0000