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

4 files changed, 81 insertions, 2 deletions

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) ->