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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
(*i*)
open Names
open Libnames
(*i*)
type loc = int * int
type t =
| Node of loc * string * t list
| Nmeta of loc * string
| Nvar of loc * identifier
| Slam of loc * identifier option * t
| Smetalam of loc * string * t
| Num of loc * int
| Str of loc * string
| Id of loc * string
| Path of loc * kernel_name
| Dynamic of loc * Dyn.t
type the_coq_ast = t
let subst_meta bl ast =
let rec aux = function
| Node (_,"META", [Num(_, n)]) -> List.assoc n bl
| Node(loc, node_name, args) ->
Node(loc, node_name, List.map aux args)
| Slam(loc, var, arg) -> Slam(loc, var, aux arg)
| Smetalam(loc, var, arg) -> Smetalam(loc, var, aux arg)
| other -> other
in
aux ast
let rec collect_metas = function
| Node (_,"META", [Num(_, n)]) -> [n]
| Node(_, _, args) -> List.concat (List.map collect_metas args)
| Slam(loc, var, arg) -> collect_metas arg
| Smetalam(loc, var, arg) -> collect_metas arg
| _ -> []
(* Hash-consing *)
module Hloc = Hashcons.Make(
struct
type t = loc
type u = unit
let equal (b1,e1) (b2,e2) = b1=b2 & e1=e2
let hash_sub () x = x
let hash = Hashtbl.hash
end)
module Hast = Hashcons.Make(
struct
type t = the_coq_ast
type u =
(the_coq_ast -> the_coq_ast) *
((loc -> loc) * (string -> string)
* (identifier -> identifier) * (kernel_name -> kernel_name))
let hash_sub (hast,(hloc,hstr,hid,hsp)) = function
| Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
| Nmeta(l,s) -> Nmeta(hloc l, hstr s)
| Nvar(l,s) -> Nvar(hloc l, hid s)
| Slam(l,None,t) -> Slam(hloc l, None, hast t)
| Slam(l,Some s,t) -> Slam(hloc l, Some (hid s), hast t)
| Smetalam(l,s,t) -> Smetalam(hloc l, hstr s, hast t)
| Num(l,n) -> Num(hloc l, n)
| Id(l,s) -> Id(hloc l, hstr s)
| Str(l,s) -> Str(hloc l, hstr s)
| Path(l,d) -> Path(hloc l, hsp d)
| Dynamic(l,d) -> Dynamic(hloc l, d)
let equal a1 a2 =
match (a1,a2) with
| (Node(l1,s1,al1), Node(l2,s2,al2)) ->
(l1==l2 & s1==s2 & List.length al1 = List.length al2)
& List.for_all2 (==) al1 al2
| (Nmeta(l1,s1), Nmeta(l2,s2)) -> l1==l2 & s1==s2
| (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
| (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
| (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) ->l1==l2 & s1==s2 & t1==t2
| (Smetalam(l1,s1,t1), Smetalam(l2,s2,t2)) -> l1==l2 & s1==s2 & t1==t2
| (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
| (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
| (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
| (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2)
| _ -> false
let hash = Hashtbl.hash
end)
let hcons_ast (hstr,hid,hpath) =
let hloc = Hashcons.simple_hcons Hloc.f () in
let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in
(hast,hloc)
let rec subst_ast subst ast = match ast with
| Node (l,s,astl) ->
let astl' = Util.list_smartmap (subst_ast subst) astl in
if astl' == astl then ast else
Node (l,s,astl')
| Slam (l,ido,ast1) ->
let ast1' = subst_ast subst ast1 in
if ast1' == ast1 then ast else
Slam (l,ido,ast1')
| Smetalam (l,s,ast1) ->
let ast1' = subst_ast subst ast1 in
if ast1' == ast1 then ast else
Smetalam (l,s,ast1')
| Path (loc,kn) ->
let kn' = Names.subst_kn subst kn in
if kn' == kn then ast else
Path(loc,kn')
| Nmeta _
| Nvar _ -> ast
| Num _
| Str _
| Id _
| Dynamic _ -> ast
open Util
open Rawterm
open Term
type scope_name = string
type reference_expr =
| RQualid of qualid located
| RIdent of identifier located
type explicitation = int
type cases_pattern =
| CPatAlias of loc * cases_pattern * identifier
| CPatCstr of loc * reference_expr * cases_pattern list
| CPatAtom of loc * reference_expr option
| CPatNumeral of loc * Bignat.bigint
| CPatDelimiters of loc * scope_name * cases_pattern
type ordered_case_style = CIf | CLet | CMatch | CCase
type constr_ast =
| CRef of reference_expr
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_ast * constr_ast
| CProdN of loc * (name located list * constr_ast) list * constr_ast
| CLambdaN of loc * (name located list * constr_ast) list * constr_ast
| CLetIn of loc * identifier located * constr_ast * constr_ast
| CAppExpl of loc * reference_expr * constr_ast list
| CApp of loc * constr_ast * (constr_ast * explicitation option) list
| CCases of loc * case_style * constr_ast option * constr_ast list *
(loc * cases_pattern list * constr_ast) list
| COrderedCase of loc * ordered_case_style * constr_ast option * constr_ast * constr_ast list
| CHole of loc
| CMeta of loc * int
| CSort of loc * rawsort
| CCast of loc * constr_ast * constr_ast
| CNotation of loc * string * constr_ast list
| CNumeral of loc * Bignat.bigint
| CDelimiters of loc * scope_name * constr_ast
| CDynamic of loc * Dyn.t
and local_binder = name located list * constr_ast
and fixpoint_expr = identifier * local_binder list * constr_ast * constr_ast
and cofixpoint_expr = identifier * constr_ast * constr_ast
let constr_loc = function
| CRef (RIdent (loc,_)) -> loc
| CRef (RQualid (loc,_)) -> loc
| CFix (loc,_,_) -> loc
| CCoFix (loc,_,_) -> loc
| CArrow (loc,_,_) -> loc
| CProdN (loc,_,_) -> loc
| CLambdaN (loc,_,_) -> loc
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
| CCases (loc,_,_,_,_) -> loc
| COrderedCase (loc,_,_,_,_) -> loc
| CHole loc -> loc
| CMeta (loc,_) -> loc
| CSort (loc,_) -> loc
| CCast (loc,_,_) -> loc
| CNotation (loc,_,_) -> loc
| CNumeral (loc,_) -> loc
| CDelimiters (loc,_,_) -> loc
| CDynamic _ -> dummy_loc
let cases_pattern_loc = function
| CPatAlias (loc,_,_) -> loc
| CPatCstr (loc,_,_) -> loc
| CPatAtom (loc,_) -> loc
| CPatNumeral (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
let replace_vars_constr_ast l t =
if l = [] then t else failwith "replace_constr_ast: TODO"
let occur_var_constr_ast id t = Pp.warning "occur_var_constr_ast:TODO"; true
|
