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
|
(***********************************************************************)
(* 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 Util
open Names
open Libnames
(*i*)
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
|
