aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile3
-rw-r--r--contrib/correctness/pcic.ml2
-rw-r--r--interp/constrintern.ml6
-rw-r--r--interp/reserve.ml69
-rw-r--r--interp/reserve.mli6
-rw-r--r--interp/topconstr.ml2
-rw-r--r--library/nameops.ml16
-rw-r--r--library/nameops.mli3
-rw-r--r--parsing/g_vernac.ml43
-rw-r--r--parsing/g_vernacnew.ml43
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/rawterm.ml4
-rw-r--r--pretyping/rawterm.mli2
-rw-r--r--toplevel/himsg.ml6
-rw-r--r--toplevel/vernacentries.ml15
-rw-r--r--toplevel/vernacexpr.ml1
16 files changed, 119 insertions, 28 deletions
diff --git a/Makefile b/Makefile
index f3b7abcff..ae4037230 100644
--- a/Makefile
+++ b/Makefile
@@ -116,7 +116,8 @@ PRETYPING=\
INTERP=\
interp/topconstr.cmo interp/ppextend.cmo interp/symbols.cmo \
- interp/genarg.cmo interp/syntax_def.cmo interp/constrintern.cmo \
+ interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \
+ interp/constrintern.cmo \
interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo
PARSING=\
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index e3852504a..66ac7b97e 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -133,7 +133,7 @@ let tuple_ref dep n =
(* Binders. *)
let trad_binder avoid nenv id = function
- | CC_untyped_binder -> RHole (dummy_loc,AbstractionType (Name id))
+ | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
| CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
let rec push_vars avoid nenv = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e7db4afe4..9ab3ddf42 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -335,7 +335,11 @@ let check_capture loc ty = function
()
let locate_if_isevar loc na = function
- | RHole _ -> RHole (loc, AbstractionType na)
+ | RHole _ ->
+ (try match na with
+ | Name id -> Reserve.find_reserved_type id
+ | Anonymous -> raise Not_found
+ with Not_found -> RHole (loc, BinderType na))
| x -> x
(**********************************************************************)
diff --git a/interp/reserve.ml b/interp/reserve.ml
new file mode 100644
index 000000000..deb696733
--- /dev/null
+++ b/interp/reserve.ml
@@ -0,0 +1,69 @@
+(* Reserved names *)
+
+open Util
+open Names
+open Nameops
+open Summary
+open Libobject
+open Lib
+
+let reserve_table = ref Idmap.empty
+
+let cache_reserved_type (_,(id,t)) =
+ reserve_table := Idmap.add id t !reserve_table
+
+let (in_reserved, _) =
+ declare_object {(default_object "RESERVED-TYPE") with
+ cache_function = cache_reserved_type }
+
+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.survive_section = false }
+
+let declare_reserved_type id t =
+ if id <> root_of_id id then
+ error ((string_of_id id)^
+ " is not reservable: it must have no trailing digits, quote, or _");
+ begin try
+ let _ = Idmap.find id !reserve_table in
+ error ((string_of_id id)^" is already bound to a type")
+ with Not_found -> () end;
+ add_anonymous_leaf (in_reserved (id,t))
+
+let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
+
+open Rawterm
+
+let rec unloc = function
+ | RVar (_,id) -> RVar (dummy_loc,id)
+ | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
+ | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
+ | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
+ | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
+ | RCases (_,tyopt,tml,pl) ->
+ RCases (dummy_loc,option_app unloc tyopt,List.map unloc tml,
+ List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
+ | ROrderedCase (_,b,tyopt,tm,bv) ->
+ ROrderedCase
+ (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv)
+ | RRec (_,fk,idl,tyl,bv) ->
+ RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
+ | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
+ | RSort (_,x) -> RSort (dummy_loc,x)
+ | RHole (_,x) -> RHole (dummy_loc,x)
+ | RRef (_,x) -> RRef (dummy_loc,x)
+ | REvar (_,x) -> REvar (dummy_loc,x)
+ | RMeta (_,x) -> RMeta (dummy_loc,x)
+ | RDynamic (_,x) -> RDynamic (dummy_loc,x)
+
+let anonymize_if_reserved na t = match na with
+ | Name id as na ->
+ (try
+ if unloc t = find_reserved_type id
+ then RHole (dummy_loc,BinderType na)
+ else t
+ with Not_found -> t)
+ | Anonymous -> t
diff --git a/interp/reserve.mli b/interp/reserve.mli
new file mode 100644
index 000000000..0c60caf9b
--- /dev/null
+++ b/interp/reserve.mli
@@ -0,0 +1,6 @@
+open Names
+open Rawterm
+
+val declare_reserved_type : identifier -> rawconstr -> unit
+val find_reserved_type : identifier -> rawconstr
+val anonymize_if_reserved : name -> rawconstr -> rawconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 17b324937..7f53f7eb2 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -128,7 +128,7 @@ let rec subst_aconstr subst raw =
let ref' = subst_global subst ref in
if ref' == ref then raw else
AHole (ImplicitArg (ref',i))
- | AHole ( (AbstractionType _ | QuestionMark | CasesType |
+ | AHole ( (BinderType _ | QuestionMark | CasesType |
InternalHole | TomatchTypeParameter _)) -> raw
| ACast (r1,r2) ->
diff --git a/library/nameops.ml b/library/nameops.ml
index 6e5de89ac..ee5bb7477 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -23,27 +23,29 @@ let wildcard = id_of_string "_"
let code_of_0 = Char.code '0'
let code_of_9 = Char.code '9'
-let cut_ident s =
+let cut_ident skip_quote s =
let s = string_of_id s in
let slen = String.length s in
(* [n'] is the position of the first non nullary digit *)
let rec numpart n n' =
if n = 0 then
failwith
- ("The string " ^ s ^ " is not an identifier: it contains only digits")
+ ("The string " ^ s ^ " is not an identifier: it contains only digits or _")
else
let c = Char.code (String.get s (n-1)) in
if c = code_of_0 && n <> slen then
numpart (n-1) n'
else if code_of_0 <= c && c <= code_of_9 then
numpart (n-1) (n-1)
- else
+ else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+ numpart (n-1) (n-1)
+ else
n'
in
numpart slen slen
let repr_ident s =
- let numstart = cut_ident s in
+ let numstart = cut_ident false s in
let s = string_of_id s in
let slen = String.length s in
if numstart = slen then
@@ -61,6 +63,10 @@ let make_ident sa = function
id_of_string s
| None -> id_of_string (String.copy sa)
+let root_of_id id =
+ let suffixstart = cut_ident true id in
+ id_of_string (String.sub (string_of_id id) 0 suffixstart)
+
(* Rem: semantics is a bit different, if an ident starts with toto00 then
after successive renamings it comes to toto09, then it goes on with toto10 *)
let lift_subscript id =
@@ -94,7 +100,7 @@ let has_subscript id =
is_digit (id.[String.length id - 1])
let forget_subscript id =
- let numstart = cut_ident id in
+ let numstart = cut_ident false id in
let newid = String.make (numstart+1) '0' in
String.blit (string_of_id id) 0 newid 0 numstart;
(id_of_string newid)
diff --git a/library/nameops.mli b/library/nameops.mli
index 8e751be09..1ae0c5303 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -17,7 +17,8 @@ val wildcard : identifier
val make_ident : string -> int option -> identifier
val repr_ident : identifier -> string * int option
-val atompart_of_id : identifier -> string
+val atompart_of_id : identifier -> string (* remove trailing digits *)
+val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *)
val add_suffix : identifier -> string -> identifier
val add_prefix : string -> identifier -> identifier
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d60a4db73..cb02b082e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -424,6 +424,9 @@ GEXTEND Gram
VernacDeclareImplicits (qid,Some l)
| IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
+ | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
+ idl = LIST1 ident SEP ","; ":"; c = constr -> VernacReserve (idl,c)
+
(* For compatibility *)
| IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
VernacSetOption
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 883000111..12e95d235 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -423,6 +423,9 @@ GEXTEND Gram
VernacDeclareImplicits (qid,Some l)
| IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
+ | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
+ idl = LIST1 ident; ":"; c = constr -> VernacReserve (idl,c)
+
(* For compatibility *)
| IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
VernacSetOption
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f676717d7..c2578cdd7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -272,18 +272,18 @@ let rec detype tenv avoid env t =
let rec remove_type avoid args c =
match c,args with
| RLambda (loc,na,t,c), _::args ->
- let h = RHole (loc,AbstractionType na) in
+ let h = RHole (loc,BinderType na) in
RLambda (loc,na,h,remove_type avoid args c)
| RLetIn (loc,na,b,c), _::args ->
RLetIn (loc,na,b,remove_type avoid args c)
| c, (na,None,t)::args ->
let id = next_name_away_with_default "x" na avoid in
- let h = RHole (dummy_loc,AbstractionType na) in
+ let h = RHole (dummy_loc,BinderType na) in
let c = remove_type (id::avoid) args
(RApp (dummy_loc,c,[RVar (dummy_loc,id)])) in
RLambda (dummy_loc,Name id,h,c)
| c, (na,Some b,t)::args ->
- let h = RHole (dummy_loc,AbstractionType na) in
+ let h = RHole (dummy_loc,BinderType na) in
let avoid = name_fold (fun x l -> x::l) na avoid in
RLetIn (dummy_loc,na,h,remove_type avoid args c)
| c, [] -> c in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 77afa8041..0075be7d8 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -50,7 +50,7 @@ type 'a with_bindings = 'a * 'a substitution
type hole_kind =
| ImplicitArg of global_reference * int
- | AbstractionType of name
+ | BinderType of name
| QuestionMark
| CasesType
| InternalHole
@@ -235,7 +235,7 @@ let rec subst_raw subst raw =
let ref' = subst_global subst ref in
if ref' == ref then raw else
RHole (loc,ImplicitArg (ref',i))
- | RHole (loc, (AbstractionType _ | QuestionMark | CasesType |
+ | RHole (loc, (BinderType _ | QuestionMark | CasesType |
InternalHole | TomatchTypeParameter _)) -> raw
| RCast (loc,r1,r2) ->
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index b5e408bb5..7ac8a15b7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -48,7 +48,7 @@ type 'a with_bindings = 'a * 'a substitution
type hole_kind =
| ImplicitArg of global_reference * int
- | AbstractionType of name
+ | BinderType of name
| QuestionMark
| CasesType
| InternalHole
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b6dac63a9..55fce41aa 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -310,10 +310,10 @@ let explain_unsolvable_implicit env = function
| QuestionMark -> str "Cannot infer a term for this placeholder"
| CasesType ->
str "Cannot infer the type of this pattern-matching problem"
- | AbstractionType (Name id) ->
+ | BinderType (Name id) ->
str "Cannot infer a type for " ++ Nameops.pr_id id
- | AbstractionType Anonymous ->
- str "Cannot infer a type of this anonymous abstraction"
+ | BinderType Anonymous ->
+ str "Cannot infer a type of this anonymous binder"
| ImplicitArg (c,n) ->
str "Cannot infer the " ++ pr_ord n ++
str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1cf01bf11..cb1f21149 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -470,7 +470,6 @@ let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o =
(* | true, _, _, _ -> *)
(* error "Module definition not allowed in a Module Type" *)
-
let vernac_end_module id =
Declaremods.end_module id;
if_verbose message
@@ -714,6 +713,11 @@ let vernac_declare_implicits locqid = function
| Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps
| None -> Impargs.declare_implicits (Nametab.global locqid)
+let vernac_reserve idl c =
+ let t = Constrintern.interp_type Evd.empty (Global.env()) c in
+ let t = Detyping.detype (Global.env()) [] [] t in
+ List.iter (fun id -> Reserve.declare_reserved_type id t) idl
+
let make_silent_if_not_pcoq b =
if !pcoq <> None then
error "Turning on/off silent flag is not supported in Centaur mode"
@@ -791,14 +795,6 @@ let _ =
optread=Pp_control.get_depth_boxes;
optwrite=Pp_control.set_depth_boxes }
-let _ =
- declare_int_option
- { optsync=true;
- optkey=SecondaryTable("Printing","Width");
- optname="the printing width";
- optread=Pp_control.get_margin;
- optwrite=Pp_control.set_margin}
-
let vernac_set_opacity opaq locqid =
match Nametab.global locqid with
| ConstRef sp ->
@@ -1202,6 +1198,7 @@ let interp c = match c with
| VernacHintDestruct (id,l,p,n,tac) -> Dhyp.add_destructor_hint id l p n tac
| VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n
| VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
+ | VernacReserve (idl,c) -> vernac_reserve idl c
| VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
| VernacSetOption (key,v) -> vernac_set_option key v
| VernacUnsetOption key -> vernac_unset_option key
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 14c9a295e..c332e894a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -228,6 +228,7 @@ type vernac_expr =
identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
| VernacSyntacticDefinition of identifier * constr_expr * int option
| VernacDeclareImplicits of reference * int list option
+ | VernacReserve of identifier list * constr_expr
| VernacSetOpacity of opacity_flag * reference list
| VernacUnsetOption of Goptions.option_name
| VernacSetOption of Goptions.option_name * option_value
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:10:32 +0000