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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: reserve.ml 9976 2007-07-12 11:58:30Z msozeau $ i*)
(* Reserved names *)
open Util
open Pp
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 (loc,id) t =
if id <> root_of_id id then
user_err_loc(loc,"declare_reserved_type",
(pr_id id ++ str
" is not reservable: it must have no trailing digits, quote, or _"));
begin try
let _ = Idmap.find id !reserve_table in
user_err_loc(loc,"declare_reserved_type",
(pr_id id++str" 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 (_,rtntypopt,tml,pl) ->
RCases (dummy_loc,
(option_map unloc rtntypopt),
List.map (fun (tm,x) -> (unloc tm,x)) tml,
List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
| RLetTuple (_,nal,(na,po),b,c) ->
RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
| RRec (_,fk,idl,bl,tyl,bv) ->
RRec (dummy_loc,fk,idl,
Array.map (List.map
(fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
Array.map unloc bv)
| RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t))
| RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce)
| RSort (_,x) -> RSort (dummy_loc,x)
| RHole (_,x) -> RHole (dummy_loc,x)
| RRef (_,x) -> RRef (dummy_loc,x)
| REvar (_,x,l) -> REvar (dummy_loc,x,l)
| 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 ->
(try
if unloc t = find_reserved_type id
then RHole (dummy_loc,Evd.BinderType na)
else t
with Not_found -> t)
| Anonymous -> t
|
