-
Notifications
You must be signed in to change notification settings - Fork 5
/
abbot_user.sml
252 lines (235 loc) · 8.25 KB
/
abbot_user.sml
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
(* Abbot: emitting user interface (___.abt.sig) *)
structure AbbotUser =
struct
open Analysis
open SmlSyntax
open AbbotCore
fun create_mutual_type_decls ana abt_or_sort =
List.map
(fn {aliases, datatypes} =>
TypeDecls
{datatypes = datatypes,
aliases =
List.map
(fn (name, args, _) =>
(name, args, NONE))
aliases})
(op@ (create_mutual_types ana abt_or_sort))
fun create_abt_structure_decl ana (abt, (args, opers)) =
StructureDecl
(Big (abt_to_string abt),
SigBody
(concatWith [BlankDecl]
[create_mutual_type_decls ana (Abt abt),
[TypeDecls
{datatypes=[abt_datatype ana (abt, (args, opers))],
aliases=[]}],
[TypeDecls
{aliases=[("t", args, SOME (TypeVar (abt_to_string abt)))],
datatypes=[]}],
[ValDecl
("aequiv",
List.foldr
(fn (arg, acc) =>
ArrowType
(ArrowType
(ProdType
[TypeVar ("'" ^ arg ^ "1"),
TypeVar ("'" ^ arg ^ "2")],
TypeVar "bool"),
acc))
(ArrowType
(ProdType
[AppType
(List.map (fn arg => TypeVar ("'" ^ arg ^ "1")) args,
TypeVar "t"),
AppType
(List.map (fn arg => TypeVar ("'" ^ arg ^ "2")) args,
TypeVar "t")],
TypeVar "bool"))
args)],
[ValDecl
("toString",
List.foldr
(fn (arg, acc) =>
ArrowType
(ArrowType (TypeVar ("'" ^ arg), TypeVar "string"),
acc))
(ArrowType
(AppType
(List.map (fn arg => TypeVar ("'" ^ arg)) args,
TypeVar "t"),
TypeVar "string"))
args)]]))
fun create_view_datatype_decl ana (srt, opers) =
let
val oper_branches =
List.map
(fn (oper, arity_opt) =>
(oper,
(case arity_opt of
NONE => NONE
| SOME arity =>
SOME (sort_arity_to_type ana false srt arity))))
opers
val body =
if #hasvar ana srt
then ("Var", SOME (TypeVar (sort_to_var_type srt))) :: oper_branches
else oper_branches
in
TypeDecls {datatypes = [("view", [], body)], aliases = []}
end
fun create_sort_structure_decl (ana : ana) (sort, opers) =
let
val var_structure_decl =
if #hasvar ana sort
then
[StructureDecl
("Var",
WhereType
(SigVar "TEMP",
TypeVar "t",
TypeVar (sort_to_var_type sort)))]
else []
val convenient_contructors =
let
val oper_constructors =
List.map
(fn (oper, arity_opt) =>
ValDecl
(oper ^ "'",
case arity_opt of
NONE => sort_to_type sort
| SOME arity =>
ArrowType
(sort_arity_to_type ana false sort arity,
sort_to_type sort)))
opers
in
if #hasvar ana sort
then
ValDecl
("Var'",
ArrowType
(TypeVar (sort_to_var_type sort),
sort_to_type sort))
:: oper_constructors
else
oper_constructors
end
val substitutions =
List.map
(fn sort' =>
ValDecl
(if sort = sort'
then "subst"
else "subst" ^ Big (sort_to_string sort'),
ArrowType
((if #mutualwith ana (Sort sort) (Sort sort')
then sort_to_type sort'
else TypeVar (Big (sort_to_string sort') ^ ".t")),
ArrowType
((if #mutualwith ana (Sort sort) (Sort sort')
then TypeVar (sort_to_var_type sort')
else TypeVar (Big (sort_to_string sort') ^ ".Var.t")),
ArrowType (sort_to_type sort, sort_to_type sort)))))
(List.filter (#hasvar ana) (#2 (#dependencies ana (Sort sort))))
val all_decls =
List.concat
[create_mutual_type_decls ana (Sort sort),
[TypeDecls
{datatypes = [],
aliases = [(sort_to_string sort, [], NONE)]},
TypeDecls
{datatypes = [],
aliases = [("t", [], SOME (sort_to_type sort))]},
BlankDecl],
var_structure_decl,
[BlankDecl,
create_view_datatype_decl ana (sort, opers),
BlankDecl],
convenient_contructors,
[BlankDecl,
ValDecl
("into", ArrowType (TypeVar "view", sort_to_type sort)),
ValDecl
("out", ArrowType (sort_to_type sort, TypeVar "view")),
ValDecl
("aequiv",
ArrowType
(ProdType [sort_to_type sort, sort_to_type sort],
TypeVar "bool")),
ValDecl
("toString", ArrowType (sort_to_type sort, TypeVar "string"))],
(case substitutions of [] => [] | _ => BlankDecl :: substitutions)]
in
StructureDecl (Big (sort_to_string sort), SigBody all_decls)
end
fun create_sharing_decls mods field =
case mods of
[x] => []
| x::y::mods' =>
SharingDecl
(ModProjType (StructVar (Big x), field),
ModProjType (StructVar (Big y), field))
:: create_sharing_decls (y::mods') field
fun create_mutual_abt_and_sort_structure_decls ana abts_and_sorts =
let
val abt_and_sort_structures =
List.map
(fn Sum2.In1 abt => create_abt_structure_decl ana abt
| Sum2.In2 sort => create_sort_structure_decl ana sort)
abts_and_sorts
val abt_and_sort_strings =
List.map
(fn Sum2.In1 (abt, _) => abt_to_string abt
| Sum2.In2 (sort, _) => sort_to_string sort)
abts_and_sorts
fun remove_data abt_or_sort =
case abt_or_sort of
Sum2.In1 (abt, _) => Abt abt
| Sum2.In2 (sort, _) => Sort sort
in
case abts_and_sorts of
([] | [_]) => abt_and_sort_structures
| abt_or_sort :: _ =>
abt_and_sort_structures
@ List.concat
(List.map
(create_sharing_decls abt_and_sort_strings)
(abt_and_sort_strings
@ List.map
(fn sort => sort_to_string sort ^ "Var")
(List.filter (#hasvar ana) (#2 (#mutual ana (remove_data abt_or_sort))))))
end
fun doit_user sig_name (ana : ana) =
let
val symbols =
List.map
(fn sym =>
StructureDecl
(Big (sym_to_string sym),
SigVar "TEMP"))
(#symbols ana)
val exts =
List.map
(fn (ext, args) =>
StructureDecl
(Big (ext_to_string ext),
create_ext_signature args))
(#externals ana)
val abts_and_sorts =
List.concat
(List.map
(create_mutual_abt_and_sort_structure_decls ana)
(#abts_and_sorts ana))
in
Emit.emit
[TLSignature
(sig_name,
SigBody
(symbols
@ [BlankDecl]
@ interleave BlankDecl (exts @ abts_and_sorts)))]
end
end