Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)

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

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