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
type t =
Pident of Ident.t
| Pdot of t * string
| Papply of t * t
let rec same_aux ident_cmp p1 p2 =
let same_aux p1 p2 = same_aux ident_cmp p1 p2 in
p1 == p2
|| match (p1, p2) with
(Pident id1, Pident id2) -> ident_cmp id1 id2
| (Pdot(p1, s1), Pdot(p2, s2)) ->
s1 = s2 && same_aux p1 p2
| (Papply(fun1, arg1), Papply(fun2, arg2)) ->
same_aux fun1 fun2 && same_aux arg1 arg2
| (Pextra_ty (p1, t1), Pextra_ty (p2, t2)) ->
let = match t1, t2 with
| (Pcstr_ty s1, Pcstr_ty s2) -> s1 = s2
| (Pext_ty, Pext_ty) -> true
| ((Pcstr_ty _ | Pext_ty), _) -> false
in same_extra && same_aux p1 p2
| (_, _) -> false
let same p1 p2 = same_aux Ident.same p1 p2
let equiv id_pairs p1 p2 = same_aux (Ident.equiv id_pairs) p1 p2
let rec compare p1 p2 =
if p1 == p2 then 0
else match (p1, p2) with
(Pident id1, Pident id2) -> Ident.compare id1 id2
| (Pdot(p1, s1), Pdot(p2, s2)) ->
let h = compare p1 p2 in
if h <> 0 then h else String.compare s1 s2
| (Papply(fun1, arg1), Papply(fun2, arg2)) ->
let h = compare fun1 fun2 in
if h <> 0 then h else compare arg1 arg2
| (Pextra_ty (p1, t1), Pextra_ty (p2, t2)) ->
let h = compare_extra t1 t2 in
if h <> 0 then h else compare p1 p2
| (Pident _, (Pdot _ | Papply _ | Pextra_ty _))
| (Pdot _, (Papply _ | Pextra_ty _))
| (Papply _, Pextra_ty _)
-> -1
| ((Pextra_ty _ | Papply _ | Pdot _), Pident _)
| ((Pextra_ty _ | Papply _) , Pdot _)
| (Pextra_ty _, Papply _)
-> 1
and t1 t2 =
match (t1, t2) with
Pcstr_ty s1, Pcstr_ty s2 -> String.compare s1 s2
| (Pext_ty, Pext_ty)
-> 0
| (Pcstr_ty _, Pext_ty)
-> -1
| (Pext_ty, Pcstr_ty _)
-> 1
let rec find_free_opt ids = function
Pident id -> List.find_opt (Ident.same id) ids
| Pdot(p, _) | Pextra_ty (p, _) -> find_free_opt ids p
| Papply(p1, p2) -> begin
match find_free_opt ids p1 with
| None -> find_free_opt ids p2
| Some _ as res -> res
end
let exists_free ids p =
match find_free_opt ids p with
| None -> false
| _ -> true
let rec scope = function
Pident id -> Ident.scope id
| Pdot(p, _) | Pextra_ty (p, _) -> scope p
| Papply(p1, p2) -> Int.max (scope p1) (scope p2)
let subst id_map p =
if id_map = [] then
p
else
let changed = ref false in
let rec aux = function
| Pident id ->
begin match List.find (fun (i, _) -> Ident.same i id) id_map with
| (_, p) -> changed := true; p
| exception Not_found -> Pident id
end
| Pdot(p, s) -> Pdot(aux p, s)
| Pextra_ty(p, e) -> Pextra_ty(aux p, e)
| Papply(p1, p2) -> Papply(aux p1, aux p2)
in
let p' = aux p in
if !changed then p' else p
let check_for_unbound_unscoped_idents idl p =
let exception Escape of Ident.Unscoped.t in
let rec aux = function
Pident id ->
begin match Ident.find_unscoped id with
| None -> ()
| Some us ->
if Ident.Unscoped.Set.exists (Ident.Unscoped.same us) idl
then ()
else raise (Escape us)
end
| Pdot (p, _) | Pextra_ty (p, _) -> aux p
| Papply (p1, p2) -> aux p1; aux p2
in match aux p with
| () -> None
| exception Escape id -> Some id
let kfalse _ = false
let maybe_escape s =
if Lexer.is_keyword s then "\\#" ^ s else s
let rec name ?(paren=kfalse) = function
Pident id -> maybe_escape (Ident.name id)
| Pdot(p, s) | Pextra_ty (p, Pcstr_ty s) ->
let s = maybe_escape s in
name ~paren p ^ if paren s then ".( " ^ s ^ " )" else "." ^ s
| Papply(p1, p2) -> name ~paren p1 ^ "(" ^ name ~paren p2 ^ ")"
| Pextra_ty (p, Pext_ty) -> name ~paren p
let rec print ppf = function
| Pident id -> Ident.print_with_scope ppf id
| Pdot(p, s) | Pextra_ty (p, Pcstr_ty s) ->
Format_doc.fprintf ppf "%a.%s" print p s
| Papply(p1, p2) -> Format_doc.fprintf ppf "%a(%a)" print p1 print p2
| Pextra_ty (p, Pext_ty) -> print ppf p
let rec head = function
Pident id -> id
| Pdot(p, _) | Pextra_ty (p, _) -> head p
| Papply _ -> assert false
let flatten =
let rec flatten acc = function
| Pident id -> `Ok (id, acc)
| Pdot (p, s) | Pextra_ty (p, Pcstr_ty s) -> flatten (s :: acc) p
| Papply _ -> `Contains_apply
| Pextra_ty (p, Pext_ty) -> flatten acc p
in
fun t -> flatten [] t
let rec = function
| Pextra_ty (t, _) -> scrape_extra_ty t
| t -> t
let heads p =
let rec heads p acc = match p with
| Pident id -> id :: acc
| Pdot (p, _) | Pextra_ty (p, _) -> heads p acc
| Papply(p1, p2) ->
heads p1 (heads p2 acc)
in heads p []
let rec last = function
| Pident id -> Ident.name id
| Pdot(_, s) | Pextra_ty (_, Pcstr_ty s) -> s
| Papply(_, p) | Pextra_ty (p, Pext_ty) -> last p
let is_constructor_typath p =
match p with
| Pident _ | Pdot _ | Papply _ -> false
| Pextra_ty _ -> true
module T = struct
type nonrec t = t
let compare = compare
end
module Set = Set.Make(T)
module Map = Map.Make(T)