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

1 files changed, 69 insertions, 0 deletions

diff --git a/interp/reserve.ml b/interp/reserve.ml
new file mode 100644
index 0000000000..deb6967339
--- /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