1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
(* 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_module = false;
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,rtntypopt),tml,pl) ->
RCases (dummy_loc,
(option_app unloc tyopt,ref (option_app unloc !rtntypopt)),
List.map (fun (tm,x) -> (unloc tm,x)) tml,
List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
| ROrderedCase (_,b,tyopt,tm,bv,x) ->
ROrderedCase
(dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x)
| RLetTuple (_,nal,(na,po),b,c) ->
RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
| 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)
| RPatVar (_,x) -> RPatVar (dummy_loc,x)
| RDynamic (_,x) -> RDynamic (dummy_loc,x)
let anonymize_if_reserved na t = match na with
| Name id as na ->
if !Options.v7 & id = id_of_string "_" then t else
(try
if unloc t = find_reserved_type id
then RHole (dummy_loc,BinderType na)
else t
with Not_found -> t)
| Anonymous -> t
|
