author | blanchet |
Sat, 29 Oct 2016 00:39:32 +0200 | |
changeset 64429 | 582f54f6b29b |
parent 64411 | 0af9926e1303 |
permissions | -rw-r--r-- |
64389 | 1 |
(* Title: HOL/Nunchaku/Tools/nunchaku_problem.ML |
2 |
Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII |
|
3 |
Copyright 2015, 2016 |
|
4 |
||
5 |
Abstract syntax tree for Nunchaku problems. |
|
6 |
*) |
|
7 |
||
8 |
signature NUNCHAKU_PROBLEM = |
|
9 |
sig |
|
10 |
eqtype ident |
|
11 |
||
12 |
datatype ty = |
|
13 |
NType of ident * ty list |
|
14 |
||
15 |
datatype tm = |
|
16 |
NAtom of int * ty |
|
17 |
| NConst of ident * ty list * ty |
|
18 |
| NAbs of tm * tm |
|
19 |
| NMatch of tm * (ident * tm list * tm) list |
|
20 |
| NApp of tm * tm |
|
21 |
||
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
22 |
type nun_copy_spec = |
64389 | 23 |
{abs_ty: ty, |
24 |
rep_ty: ty, |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
25 |
subset: tm option, |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
26 |
quotient: tm option, |
64389 | 27 |
abs: tm, |
28 |
rep: tm} |
|
29 |
||
30 |
type nun_ctr_spec = |
|
31 |
{ctr: tm, |
|
32 |
arg_tys: ty list} |
|
33 |
||
34 |
type nun_co_data_spec = |
|
35 |
{ty: ty, |
|
36 |
ctrs: nun_ctr_spec list} |
|
37 |
||
38 |
type nun_const_spec = |
|
39 |
{const: tm, |
|
40 |
props: tm list} |
|
41 |
||
42 |
type nun_consts_spec = |
|
43 |
{consts: tm list, |
|
44 |
props: tm list} |
|
45 |
||
46 |
datatype nun_command = |
|
47 |
NTVal of ty * (int option * int option) |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
48 |
| NCopy of nun_copy_spec |
64389 | 49 |
| NData of nun_co_data_spec list |
50 |
| NCodata of nun_co_data_spec list |
|
51 |
| NVal of tm * ty |
|
52 |
| NPred of bool * nun_const_spec list |
|
53 |
| NCopred of nun_const_spec list |
|
54 |
| NRec of nun_const_spec list |
|
55 |
| NSpec of nun_consts_spec |
|
56 |
| NAxiom of tm |
|
57 |
| NGoal of tm |
|
58 |
| NEval of tm |
|
59 |
||
60 |
type nun_problem = |
|
61 |
{commandss: nun_command list list, |
|
62 |
sound: bool, |
|
63 |
complete: bool} |
|
64 |
||
65 |
type name_pool = |
|
66 |
{nice_of_ugly: string Symtab.table, |
|
67 |
ugly_of_nice: string Symtab.table} |
|
68 |
||
69 |
val nun_abstract: string |
|
70 |
val nun_and: string |
|
71 |
val nun_anon_fun_prefix: string |
|
72 |
val nun_arrow: string |
|
73 |
val nun_asserting: string |
|
74 |
val nun_assign: string |
|
75 |
val nun_at: string |
|
76 |
val nun_axiom: string |
|
77 |
val nun_bar: string |
|
78 |
val nun_choice: string |
|
79 |
val nun_codata: string |
|
80 |
val nun_colon: string |
|
81 |
val nun_comma: string |
|
82 |
val nun_concrete: string |
|
83 |
val nun_conj: string |
|
84 |
val nun_copred: string |
|
85 |
val nun_copy: string |
|
86 |
val nun_data: string |
|
87 |
val nun_disj: string |
|
88 |
val nun_dollar: string |
|
89 |
val nun_dot: string |
|
90 |
val nun_dummy: string |
|
91 |
val nun_else: string |
|
92 |
val nun_end: string |
|
93 |
val nun_equals: string |
|
94 |
val nun_eval: string |
|
95 |
val nun_exists: string |
|
96 |
val nun_false: string |
|
97 |
val nun_forall: string |
|
98 |
val nun_goal: string |
|
99 |
val nun_hash: string |
|
100 |
val nun_if: string |
|
101 |
val nun_implies: string |
|
102 |
val nun_irrelevant: string |
|
103 |
val nun_lambda: string |
|
104 |
val nun_lbrace: string |
|
105 |
val nun_lbracket: string |
|
106 |
val nun_lparen: string |
|
107 |
val nun_match: string |
|
108 |
val nun_mu: string |
|
109 |
val nun_not: string |
|
64429
582f54f6b29b
adapted Nunchaku integration to keyword renaming
blanchet
parents:
64411
diff
changeset
|
110 |
val nun_partial_quotient: string |
64389 | 111 |
val nun_pred: string |
112 |
val nun_prop: string |
|
113 |
val nun_quotient: string |
|
114 |
val nun_rbrace: string |
|
115 |
val nun_rbracket: string |
|
116 |
val nun_rec: string |
|
117 |
val nun_rparen: string |
|
118 |
val nun_semicolon: string |
|
119 |
val nun_spec: string |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
120 |
val nun_subset: string |
64389 | 121 |
val nun_then: string |
122 |
val nun_true: string |
|
123 |
val nun_type: string |
|
124 |
val nun_unparsable: string |
|
125 |
val nun_unique: string |
|
126 |
val nun_unique_unsafe: string |
|
127 |
val nun_val: string |
|
128 |
val nun_wf: string |
|
129 |
val nun_with: string |
|
130 |
val nun__witness_of: string |
|
131 |
||
132 |
val ident_of_str: string -> ident |
|
133 |
val str_of_ident: ident -> string |
|
134 |
val encode_args: string list -> string |
|
135 |
val nun_const_of_str: string list -> string -> ident |
|
136 |
val nun_tconst_of_str: string list -> string -> ident |
|
137 |
val nun_free_of_str: string -> ident |
|
138 |
val nun_tfree_of_str: string -> ident |
|
139 |
val nun_var_of_str: string -> ident |
|
140 |
val str_of_nun_const: ident -> string list * string |
|
141 |
val str_of_nun_tconst: ident -> string list * string |
|
142 |
val str_of_nun_free: ident -> string |
|
143 |
val str_of_nun_tfree: ident -> string |
|
144 |
val str_of_nun_var: ident -> string |
|
145 |
||
146 |
val dummy_ty: ty |
|
147 |
val prop_ty: ty |
|
148 |
val mk_arrow_ty: ty * ty -> ty |
|
149 |
val mk_arrows_ty: ty list * ty -> ty |
|
150 |
val nabss: tm list * tm -> tm |
|
151 |
val napps: tm * tm list -> tm |
|
152 |
||
153 |
val ty_of: tm -> ty |
|
154 |
val safe_ty_of: tm -> ty |
|
155 |
||
156 |
val fold_map_ty_idents: (string -> 'a -> string * 'a) -> ty -> 'a -> ty * 'a |
|
157 |
val fold_map_tm_idents: (string -> 'a -> string * 'a) -> tm -> 'a -> tm * 'a |
|
158 |
val fold_map_nun_command_idents: (string -> 'a -> string * 'a) -> nun_command -> 'a -> |
|
159 |
nun_command * 'a |
|
160 |
val fold_map_nun_problem_idents: (string -> 'a -> string * 'a) -> nun_problem -> 'a -> |
|
161 |
nun_problem * 'a |
|
162 |
||
163 |
val allocate_nice: name_pool -> string * string -> string * name_pool |
|
164 |
||
165 |
val rcomb_tms: tm list -> tm -> tm |
|
166 |
val abs_tms: tm list -> tm -> tm |
|
167 |
val beta_reduce_tm: tm -> tm |
|
168 |
val eta_expandN_tm: int -> tm -> tm |
|
169 |
val eta_expand_builtin_tm: tm -> tm |
|
170 |
||
171 |
val str_of_ty: ty -> string |
|
172 |
val str_of_tm: tm -> string |
|
173 |
val str_of_tmty: tm -> string |
|
174 |
||
175 |
val nice_nun_problem: nun_problem -> nun_problem * name_pool |
|
176 |
val str_of_nun_problem: nun_problem -> string |
|
177 |
end; |
|
178 |
||
179 |
structure Nunchaku_Problem : NUNCHAKU_PROBLEM = |
|
180 |
struct |
|
181 |
||
182 |
open Nunchaku_Util; |
|
183 |
||
184 |
type ident = string; |
|
185 |
||
186 |
datatype ty = |
|
187 |
NType of ident * ty list; |
|
188 |
||
189 |
datatype tm = |
|
190 |
NAtom of int * ty |
|
191 |
| NConst of ident * ty list * ty |
|
192 |
| NAbs of tm * tm |
|
193 |
| NMatch of tm * (ident * tm list * tm) list |
|
194 |
| NApp of tm * tm; |
|
195 |
||
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
196 |
type nun_copy_spec = |
64389 | 197 |
{abs_ty: ty, |
198 |
rep_ty: ty, |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
199 |
subset: tm option, |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
200 |
quotient: tm option, |
64389 | 201 |
abs: tm, |
202 |
rep: tm}; |
|
203 |
||
204 |
type nun_ctr_spec = |
|
205 |
{ctr: tm, |
|
206 |
arg_tys: ty list}; |
|
207 |
||
208 |
type nun_co_data_spec = |
|
209 |
{ty: ty, |
|
210 |
ctrs: nun_ctr_spec list}; |
|
211 |
||
212 |
type nun_const_spec = |
|
213 |
{const: tm, |
|
214 |
props: tm list}; |
|
215 |
||
216 |
type nun_consts_spec = |
|
217 |
{consts: tm list, |
|
218 |
props: tm list}; |
|
219 |
||
220 |
datatype nun_command = |
|
221 |
NTVal of ty * (int option * int option) |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
222 |
| NCopy of nun_copy_spec |
64389 | 223 |
| NData of nun_co_data_spec list |
224 |
| NCodata of nun_co_data_spec list |
|
225 |
| NVal of tm * ty |
|
226 |
| NPred of bool * nun_const_spec list |
|
227 |
| NCopred of nun_const_spec list |
|
228 |
| NRec of nun_const_spec list |
|
229 |
| NSpec of nun_consts_spec |
|
230 |
| NAxiom of tm |
|
231 |
| NGoal of tm |
|
232 |
| NEval of tm; |
|
233 |
||
234 |
type nun_problem = |
|
235 |
{commandss: nun_command list list, |
|
236 |
sound: bool, |
|
237 |
complete: bool}; |
|
238 |
||
239 |
type name_pool = |
|
240 |
{nice_of_ugly: string Symtab.table, |
|
241 |
ugly_of_nice: string Symtab.table}; |
|
242 |
||
243 |
val nun_abstract = "abstract"; |
|
244 |
val nun_and = "and"; |
|
245 |
val nun_anon_fun_prefix = "anon_fun_"; |
|
246 |
val nun_arrow = "->"; |
|
247 |
val nun_asserting = "asserting"; |
|
248 |
val nun_assign = ":="; |
|
249 |
val nun_at = "@"; |
|
250 |
val nun_axiom = "axiom"; |
|
251 |
val nun_bar = "|"; |
|
252 |
val nun_choice = "choice"; |
|
253 |
val nun_codata = "codata"; |
|
254 |
val nun_colon = ":"; |
|
255 |
val nun_comma = ","; |
|
256 |
val nun_concrete = "concrete"; |
|
257 |
val nun_conj = "&&"; |
|
258 |
val nun_copred = "copred"; |
|
259 |
val nun_copy = "copy"; |
|
260 |
val nun_data = "data"; |
|
261 |
val nun_disj = "||"; |
|
262 |
val nun_dollar = "$"; |
|
263 |
val nun_dot = "."; |
|
264 |
val nun_dummy = "_"; |
|
265 |
val nun_else = "else"; |
|
266 |
val nun_end = "end"; |
|
267 |
val nun_equals = "="; |
|
268 |
val nun_eval = "eval"; |
|
269 |
val nun_exists = "exists"; |
|
270 |
val nun_false = "false"; |
|
271 |
val nun_forall = "forall"; |
|
272 |
val nun_goal = "goal"; |
|
273 |
val nun_hash = "#"; |
|
274 |
val nun_if = "if"; |
|
275 |
val nun_implies = "=>"; |
|
276 |
val nun_irrelevant = "?__"; |
|
277 |
val nun_lambda = "fun"; |
|
278 |
val nun_lbrace = "{"; |
|
279 |
val nun_lbracket = "["; |
|
280 |
val nun_lparen = "("; |
|
281 |
val nun_match = "match"; |
|
282 |
val nun_mu = "mu"; |
|
283 |
val nun_not = "~"; |
|
64429
582f54f6b29b
adapted Nunchaku integration to keyword renaming
blanchet
parents:
64411
diff
changeset
|
284 |
val nun_partial_quotient = "partial_quotient"; |
64389 | 285 |
val nun_pred = "pred"; |
286 |
val nun_prop = "prop"; |
|
287 |
val nun_quotient = "quotient"; |
|
288 |
val nun_rbrace = "}"; |
|
289 |
val nun_rbracket = "]"; |
|
290 |
val nun_rec = "rec"; |
|
291 |
val nun_rparen = ")"; |
|
292 |
val nun_semicolon = ";"; |
|
293 |
val nun_spec = "spec"; |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
294 |
val nun_subset = "subset"; |
64389 | 295 |
val nun_then = "then"; |
296 |
val nun_true = "true"; |
|
297 |
val nun_type = "type"; |
|
298 |
val nun_unique = "unique"; |
|
299 |
val nun_unique_unsafe = "unique_unsafe"; |
|
300 |
val nun_unparsable = "?__unparsable"; |
|
301 |
val nun_val = "val"; |
|
302 |
val nun_wf = "wf"; |
|
303 |
val nun_with = "with"; |
|
304 |
val nun__witness_of = "_witness_of"; |
|
305 |
||
306 |
val nun_parens = enclose nun_lparen nun_rparen; |
|
307 |
||
308 |
fun nun_parens_if_space s = s |> String.isSubstring " " s ? nun_parens; |
|
309 |
||
310 |
fun str_of_nun_arg_list str_of_arg = |
|
311 |
map (prefix " " o nun_parens_if_space o str_of_arg) #> space_implode ""; |
|
312 |
||
313 |
fun str_of_nun_and_list str_of_elem = |
|
314 |
map str_of_elem #> space_implode ("\n" ^ nun_and ^ " "); |
|
315 |
||
316 |
val is_nun_const_quantifier = member (op =) [nun_forall, nun_exists]; |
|
317 |
val is_nun_const_connective = member (op =) [nun_conj, nun_disj, nun_implies]; |
|
318 |
||
319 |
val nun_builtin_arity = |
|
320 |
[(nun_asserting, 2), |
|
321 |
(nun_conj, 2), |
|
322 |
(nun_disj, 2), |
|
323 |
(nun_equals, 2), |
|
324 |
(nun_exists, 1), |
|
325 |
(nun_false, 0), |
|
326 |
(nun_forall, 1), |
|
327 |
(nun_if, 3), |
|
328 |
(nun_implies, 2), |
|
329 |
(nun_not, 1), |
|
330 |
(nun_true, 0)]; |
|
331 |
||
332 |
val arity_of_nun_builtin = AList.lookup (op =) nun_builtin_arity #> the_default 0; |
|
333 |
||
334 |
val nun_const_prefix = "c."; |
|
335 |
val nun_free_prefix = "f."; |
|
336 |
val nun_var_prefix = "v."; |
|
337 |
val nun_tconst_prefix = "C."; |
|
338 |
val nun_tfree_prefix = "F."; |
|
339 |
val nun_custom_id_suffix = "_"; |
|
340 |
||
341 |
val ident_of_str = I : string -> ident; |
|
342 |
val str_of_ident = I : ident -> string; |
|
343 |
||
344 |
val encode_args = enclose "(" ")" o commas; |
|
345 |
||
346 |
fun decode_args s = |
|
347 |
let |
|
348 |
fun delta #"(" = 1 |
|
349 |
| delta #")" = ~1 |
|
350 |
| delta _ = 0; |
|
351 |
||
352 |
fun dec 0 (#"(" :: #")" :: cs) _ = ([], String.implode cs) |
|
353 |
| dec 0 (#"(" :: cs) [] = dec 1 cs [[]] |
|
354 |
| dec 0 cs _ = ([], String.implode cs) |
|
355 |
| dec _ [] _ = raise Fail ("ill-formed arguments in " ^ quote s) |
|
356 |
| dec 1 (#")" :: cs) args = (rev (map (String.implode o rev) args), String.implode cs) |
|
357 |
| dec 1 (#"," :: cs) args = dec 1 cs ([] :: args) |
|
358 |
| dec n (c :: cs) (arg :: args) = dec (n + delta c) cs ((c :: arg) :: args); |
|
359 |
in |
|
360 |
dec 0 (String.explode s) [] |
|
361 |
end; |
|
362 |
||
363 |
fun nun_const_of_str args = |
|
364 |
suffix nun_custom_id_suffix #> prefix nun_const_prefix #> prefix (encode_args args); |
|
365 |
fun nun_tconst_of_str args = |
|
366 |
suffix nun_custom_id_suffix #> prefix nun_tconst_prefix #> prefix (encode_args args); |
|
367 |
||
368 |
val nun_free_of_str = suffix nun_custom_id_suffix #> prefix nun_free_prefix; |
|
369 |
val nun_tfree_of_str = suffix nun_custom_id_suffix #> prefix nun_tfree_prefix; |
|
370 |
val nun_var_of_str = suffix nun_custom_id_suffix #> prefix nun_var_prefix; |
|
371 |
val str_of_nun_const = decode_args ##> unprefix nun_const_prefix ##> unsuffix nun_custom_id_suffix; |
|
372 |
val str_of_nun_tconst = decode_args ##> unprefix nun_tconst_prefix ##> unsuffix nun_custom_id_suffix; |
|
373 |
val str_of_nun_free = unprefix nun_free_prefix #> unsuffix nun_custom_id_suffix; |
|
374 |
val str_of_nun_tfree = unprefix nun_tfree_prefix #> unsuffix nun_custom_id_suffix; |
|
375 |
val str_of_nun_var = unprefix nun_var_prefix #> unsuffix nun_custom_id_suffix; |
|
376 |
||
377 |
fun index_name s 0 = s |
|
378 |
| index_name s j = |
|
379 |
let |
|
380 |
val n = size s; |
|
381 |
val m = n - 1; |
|
382 |
in |
|
383 |
String.substring (s, 0, m) ^ string_of_int j ^ String.substring (s, m, n - m) |
|
384 |
end; |
|
385 |
||
386 |
val dummy_ty = NType (nun_dummy, []); |
|
387 |
val prop_ty = NType (nun_prop, []); |
|
388 |
||
389 |
fun mk_arrow_ty (dom, ran) = NType (nun_arrow, [dom, ran]); |
|
390 |
val mk_arrows_ty = Library.foldr mk_arrow_ty; |
|
391 |
||
392 |
val nabss = Library.foldr NAbs; |
|
393 |
val napps = Library.foldl NApp; |
|
394 |
||
395 |
fun domain_ty (NType (_, [ty, _])) = ty |
|
396 |
| domain_ty ty = ty; |
|
397 |
||
398 |
fun range_ty (NType (_, [_, ty])) = ty |
|
399 |
| range_ty ty = ty; |
|
400 |
||
401 |
fun domain_tys 0 _ = [] |
|
402 |
| domain_tys n ty = domain_ty ty :: domain_tys (n - 1) (range_ty ty); |
|
403 |
||
404 |
fun ty_of (NAtom (_, ty)) = ty |
|
405 |
| ty_of (NConst (_, _, ty)) = ty |
|
406 |
| ty_of (NAbs (var, body)) = mk_arrow_ty (ty_of var, ty_of body) |
|
407 |
| ty_of (NMatch (_, (_, _, body1) :: _)) = ty_of body1 |
|
408 |
| ty_of (NApp (const, _)) = range_ty (ty_of const); |
|
409 |
||
410 |
val safe_ty_of = try ty_of #> the_default dummy_ty; |
|
411 |
||
412 |
fun strip_nun_binders binder (app as NApp (NConst (id, _, _), NAbs (var, body))) = |
|
413 |
if id = binder then |
|
414 |
strip_nun_binders binder body |
|
415 |
|>> cons var |
|
416 |
else |
|
417 |
([], app) |
|
418 |
| strip_nun_binders _ tm = ([], tm); |
|
419 |
||
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
420 |
fun fold_map_option _ NONE = pair NONE |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
421 |
| fold_map_option f (SOME x) = f x #>> SOME; |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
422 |
|
64389 | 423 |
fun fold_map_ty_idents f (NType (id, tys)) = |
424 |
f id |
|
425 |
##>> fold_map (fold_map_ty_idents f) tys |
|
426 |
#>> NType; |
|
427 |
||
428 |
fun fold_map_match_branch_idents f (id, vars, body) = |
|
429 |
f id |
|
430 |
##>> fold_map (fold_map_tm_idents f) vars |
|
431 |
##>> fold_map_tm_idents f body |
|
432 |
#>> Scan.triple1 |
|
433 |
and fold_map_tm_idents f (NAtom (j, ty)) = |
|
434 |
fold_map_ty_idents f ty |
|
435 |
#>> curry NAtom j |
|
436 |
| fold_map_tm_idents f (NConst (id, tys, ty)) = |
|
437 |
f id |
|
438 |
##>> fold_map (fold_map_ty_idents f) tys |
|
439 |
##>> fold_map_ty_idents f ty |
|
440 |
#>> (Scan.triple1 #> NConst) |
|
441 |
| fold_map_tm_idents f (NAbs (var, body)) = |
|
442 |
fold_map_tm_idents f var |
|
443 |
##>> fold_map_tm_idents f body |
|
444 |
#>> NAbs |
|
445 |
| fold_map_tm_idents f (NMatch (obj, branches)) = |
|
446 |
fold_map_tm_idents f obj |
|
447 |
##>> fold_map (fold_map_match_branch_idents f) branches |
|
448 |
#>> NMatch |
|
449 |
| fold_map_tm_idents f (NApp (const, arg)) = |
|
450 |
fold_map_tm_idents f const |
|
451 |
##>> fold_map_tm_idents f arg |
|
452 |
#>> NApp; |
|
453 |
||
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
454 |
fun fold_map_nun_copy_spec_idents f {abs_ty, rep_ty, subset, quotient, abs, rep} = |
64389 | 455 |
fold_map_ty_idents f abs_ty |
456 |
##>> fold_map_ty_idents f rep_ty |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
457 |
##>> fold_map_option (fold_map_tm_idents f) subset |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
458 |
##>> fold_map_option (fold_map_tm_idents f) quotient |
64389 | 459 |
##>> fold_map_tm_idents f abs |
460 |
##>> fold_map_tm_idents f rep |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
461 |
#>> (fn (((((abs_ty, rep_ty), subset), quotient), abs), rep) => |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
462 |
{abs_ty = abs_ty, rep_ty = rep_ty, subset = subset, quotient = quotient, abs = abs, rep = rep}); |
64389 | 463 |
|
464 |
fun fold_map_nun_ctr_spec_idents f {ctr, arg_tys} = |
|
465 |
fold_map_tm_idents f ctr |
|
466 |
##>> fold_map (fold_map_ty_idents f) arg_tys |
|
467 |
#>> (fn (ctr, arg_tys) => {ctr = ctr, arg_tys = arg_tys}); |
|
468 |
||
469 |
fun fold_map_nun_co_data_spec_idents f {ty, ctrs} = |
|
470 |
fold_map_ty_idents f ty |
|
471 |
##>> fold_map (fold_map_nun_ctr_spec_idents f) ctrs |
|
472 |
#>> (fn (ty, ctrs) => {ty = ty, ctrs = ctrs}); |
|
473 |
||
474 |
fun fold_map_nun_const_spec_idents f {const, props} = |
|
475 |
fold_map_tm_idents f const |
|
476 |
##>> fold_map (fold_map_tm_idents f) props |
|
477 |
#>> (fn (const, props) => {const = const, props = props}); |
|
478 |
||
479 |
fun fold_map_nun_consts_spec_idents f {consts, props} = |
|
480 |
fold_map (fold_map_tm_idents f) consts |
|
481 |
##>> fold_map (fold_map_tm_idents f) props |
|
482 |
#>> (fn (consts, props) => {consts = consts, props = props}); |
|
483 |
||
484 |
fun fold_map_nun_command_idents f (NTVal (ty, cards)) = |
|
485 |
fold_map_ty_idents f ty |
|
486 |
#>> (rpair cards #> NTVal) |
|
487 |
| fold_map_nun_command_idents f (NCopy spec) = |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
488 |
fold_map_nun_copy_spec_idents f spec |
64389 | 489 |
#>> NCopy |
490 |
| fold_map_nun_command_idents f (NData specs) = |
|
491 |
fold_map (fold_map_nun_co_data_spec_idents f) specs |
|
492 |
#>> NData |
|
493 |
| fold_map_nun_command_idents f (NCodata specs) = |
|
494 |
fold_map (fold_map_nun_co_data_spec_idents f) specs |
|
495 |
#>> NCodata |
|
496 |
| fold_map_nun_command_idents f (NVal (tm, ty)) = |
|
497 |
fold_map_tm_idents f tm |
|
498 |
##>> fold_map_ty_idents f ty |
|
499 |
#>> NVal |
|
500 |
| fold_map_nun_command_idents f (NPred (wf, specs)) = |
|
501 |
fold_map (fold_map_nun_const_spec_idents f) specs |
|
502 |
#>> curry NPred wf |
|
503 |
| fold_map_nun_command_idents f (NCopred specs) = |
|
504 |
fold_map (fold_map_nun_const_spec_idents f) specs |
|
505 |
#>> NCopred |
|
506 |
| fold_map_nun_command_idents f (NRec specs) = |
|
507 |
fold_map (fold_map_nun_const_spec_idents f) specs |
|
508 |
#>> NRec |
|
509 |
| fold_map_nun_command_idents f (NSpec spec) = |
|
510 |
fold_map_nun_consts_spec_idents f spec |
|
511 |
#>> NSpec |
|
512 |
| fold_map_nun_command_idents f (NAxiom tm) = |
|
513 |
fold_map_tm_idents f tm |
|
514 |
#>> NAxiom |
|
515 |
| fold_map_nun_command_idents f (NGoal tm) = |
|
516 |
fold_map_tm_idents f tm |
|
517 |
#>> NGoal |
|
518 |
| fold_map_nun_command_idents f (NEval tm) = |
|
519 |
fold_map_tm_idents f tm |
|
520 |
#>> NEval; |
|
521 |
||
522 |
fun fold_map_nun_problem_idents f ({commandss, sound, complete} : nun_problem) = |
|
523 |
fold_map (fold_map (fold_map_nun_command_idents f)) commandss |
|
524 |
#>> (fn commandss' => {commandss = commandss', sound = sound, complete = complete}); |
|
525 |
||
526 |
fun dest_rassoc_args oper arg0 rest = |
|
527 |
(case rest of |
|
528 |
NApp (NApp (oper', arg1), rest') => |
|
529 |
if oper' = oper then arg0 :: dest_rassoc_args oper arg1 rest' else [arg0, rest] |
|
530 |
| _ => [arg0, rest]); |
|
531 |
||
532 |
fun replace_tm from to = |
|
533 |
let |
|
534 |
(* This code assumes all enclosing binders bind distinct variables and bound variables are |
|
535 |
distinct from any other variables. *) |
|
536 |
fun repl_br (id, vars, body) = (id, map repl vars, repl body) |
|
537 |
and repl (NApp (const, arg)) = NApp (repl const, repl arg) |
|
538 |
| repl (NAbs (var, body)) = NAbs (var, repl body) |
|
539 |
| repl (NMatch (obj, branches)) = NMatch (repl obj, map repl_br branches) |
|
540 |
| repl tm = if tm = from then to else tm; |
|
541 |
in |
|
542 |
repl |
|
543 |
end; |
|
544 |
||
545 |
val rcomb_tms = fold (fn arg => fn func => NApp (func, arg)); |
|
546 |
val abs_tms = fold_rev (curry NAbs); |
|
547 |
||
548 |
fun fresh_var_names_wrt_tm n tm = |
|
549 |
let |
|
550 |
fun max_var_br (_, vars, body) = fold max_var (body :: vars) |
|
551 |
and max_var (NAtom _) = I |
|
552 |
| max_var (NConst (id, _, _)) = |
|
553 |
(fn max => if String.isPrefix nun_var_prefix id andalso size id > size max then id else max) |
|
554 |
| max_var (NApp (func, arg)) = fold max_var [func, arg] |
|
555 |
| max_var (NAbs (var, body)) = fold max_var [var, body] |
|
556 |
| max_var (NMatch (obj, branches)) = max_var obj #> fold max_var_br branches; |
|
557 |
||
558 |
val dummy_name = nun_var_of_str Name.uu; |
|
559 |
val max_name = max_var tm dummy_name; |
|
560 |
in |
|
561 |
map (index_name max_name) (1 upto n) |
|
562 |
end; |
|
563 |
||
564 |
fun beta_reduce_tm (NApp (NAbs (var, body), arg)) = beta_reduce_tm (replace_tm var arg body) |
|
565 |
| beta_reduce_tm (NApp (const, arg)) = |
|
566 |
(case beta_reduce_tm const of |
|
567 |
const' as NAbs _ => beta_reduce_tm (NApp (const', arg)) |
|
568 |
| const' => NApp (const', beta_reduce_tm arg)) |
|
569 |
| beta_reduce_tm (NAbs (var, body)) = NAbs (var, beta_reduce_tm body) |
|
570 |
| beta_reduce_tm (NMatch (obj, branches)) = |
|
571 |
NMatch (beta_reduce_tm obj, map (@{apply 3(3)} beta_reduce_tm) branches) |
|
572 |
| beta_reduce_tm tm = tm; |
|
573 |
||
574 |
fun eta_expandN_tm 0 tm = tm |
|
575 |
| eta_expandN_tm n tm = |
|
576 |
let |
|
577 |
val var_names = fresh_var_names_wrt_tm n tm; |
|
578 |
val arg_tys = domain_tys n (ty_of tm); |
|
579 |
val vars = map2 (fn id => fn ty => NConst (id, [], ty)) var_names arg_tys; |
|
580 |
in |
|
581 |
abs_tms vars (rcomb_tms vars tm) |
|
582 |
end; |
|
583 |
||
584 |
val eta_expand_builtin_tm = |
|
585 |
let |
|
586 |
fun expand_quant_arg (NAbs (var, body)) = NAbs (var, expand_quant_arg body) |
|
587 |
| expand_quant_arg (NMatch (obj, branches)) = |
|
588 |
NMatch (obj, map (@{apply 3(3)} expand_quant_arg) branches) |
|
589 |
| expand_quant_arg (tm as NApp (_, NAbs _)) = tm |
|
590 |
| expand_quant_arg (NApp (quant, arg)) = NApp (quant, eta_expandN_tm 1 arg) |
|
591 |
| expand_quant_arg tm = tm; |
|
592 |
||
593 |
fun expand args (NApp (func, arg)) = expand (expand [] arg :: args) func |
|
594 |
| expand args (func as NConst (id, _, _)) = |
|
595 |
let val missing = Int.max (0, arity_of_nun_builtin id - length args) in |
|
596 |
rcomb_tms args func |
|
597 |
|> eta_expandN_tm missing |
|
598 |
|> is_nun_const_quantifier id ? expand_quant_arg |
|
599 |
end |
|
600 |
| expand args (func as NAtom _) = rcomb_tms args func |
|
601 |
| expand args (NAbs (var, body)) = rcomb_tms args (NAbs (var, expand [] body)) |
|
602 |
| expand args (NMatch (obj, branches)) = |
|
603 |
rcomb_tms args (NMatch (obj, map (@{apply 3(3)} (expand [])) branches)); |
|
604 |
in |
|
605 |
expand [] |
|
606 |
end; |
|
607 |
||
608 |
val str_of_ty = |
|
609 |
let |
|
610 |
fun str_of maybe_parens (NType (id, tys)) = |
|
611 |
if id = nun_arrow then |
|
612 |
(case tys of |
|
613 |
[ty, ty'] => maybe_parens (str_of nun_parens ty ^ " " ^ nun_arrow ^ " " ^ str_of I ty')) |
|
614 |
else |
|
615 |
id ^ str_of_nun_arg_list (str_of I) tys |
|
616 |
in |
|
617 |
str_of I |
|
618 |
end; |
|
619 |
||
620 |
val (str_of_tmty, str_of_tm) = |
|
621 |
let |
|
622 |
fun is_triv_head (NConst (id, _, _)) = (arity_of_nun_builtin id = 0) |
|
623 |
| is_triv_head (NAtom _) = true |
|
624 |
| is_triv_head (NApp (const, _)) = is_triv_head const |
|
625 |
| is_triv_head (NAbs _) = false |
|
626 |
| is_triv_head (NMatch _) = false; |
|
627 |
||
628 |
fun str_of_at_const id tys = |
|
629 |
nun_at ^ str_of_ident id ^ str_of_nun_arg_list str_of_ty tys; |
|
630 |
||
631 |
fun str_of_app ty_opt const arg = |
|
632 |
let |
|
633 |
val ty_opt' = |
|
634 |
try (Option.map (fn ty => mk_arrow_ty (ty_of arg, ty))) ty_opt |
|
635 |
|> the_default NONE; |
|
636 |
in |
|
637 |
(str_of ty_opt' const |> (case const of NAbs _ => nun_parens | _ => I)) ^ |
|
638 |
str_of_nun_arg_list (str_of NONE) [arg] |
|
639 |
end |
|
640 |
and str_of_br ty_opt (id, vars, body) = |
|
641 |
" " ^ nun_bar ^ " " ^ id ^ space_implode "" (map (prefix " " o str_of NONE) vars) ^ " " ^ |
|
642 |
nun_arrow ^ " " ^ str_of ty_opt body |
|
643 |
and str_of_tmty tm = |
|
644 |
let val ty = ty_of tm in |
|
645 |
str_of (SOME ty) tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty |
|
646 |
end |
|
647 |
and str_of _ (NAtom (j, _)) = nun_dollar ^ string_of_int j |
|
648 |
| str_of _ (NConst (id, [], _)) = str_of_ident id |
|
649 |
| str_of (SOME ty0) (NConst (id, tys, ty)) = |
|
650 |
if ty = ty0 then str_of_ident id else str_of_at_const id tys |
|
651 |
| str_of _ (NConst (id, tys, _)) = str_of_at_const id tys |
|
652 |
| str_of ty_opt (NAbs (var, body)) = |
|
653 |
nun_lambda ^ " " ^ |
|
654 |
(case ty_opt of |
|
655 |
SOME ty => str_of (SOME (domain_ty ty)) |
|
656 |
| NONE => nun_parens o str_of_tmty) var ^ |
|
657 |
nun_dot ^ " " ^ str_of (Option.map range_ty ty_opt) body |
|
658 |
| str_of ty_opt (NMatch (obj, branches)) = |
|
659 |
nun_match ^ " " ^ str_of NONE obj ^ " " ^ nun_with ^ " " ^ |
|
660 |
space_implode "" (map (str_of_br ty_opt) branches) ^ " " ^ nun_end |
|
661 |
| str_of ty_opt (app as NApp (func, argN)) = |
|
662 |
(case (func, argN) of |
|
663 |
(NApp (oper as NConst (id, _, _), arg1), arg2) => |
|
664 |
if id = nun_asserting then |
|
665 |
str_of ty_opt arg1 ^ " " ^ nun_asserting ^ " " ^ str_of (SOME prop_ty) arg2 |
|
666 |
|> nun_parens |
|
667 |
else if id = nun_equals then |
|
668 |
(str_of NONE arg1 |> not (is_triv_head arg1) ? nun_parens) ^ " " ^ id ^ " " ^ |
|
669 |
(str_of (try ty_of arg2) arg2 |> not (is_triv_head arg2) ? nun_parens) |
|
670 |
else if is_nun_const_connective id then |
|
671 |
let val args = dest_rassoc_args oper arg1 arg2 in |
|
672 |
space_implode (" " ^ id ^ " ") |
|
673 |
(map (fn arg => str_of NONE arg |> not (is_triv_head arg) ? nun_parens) args) |
|
674 |
end |
|
675 |
else |
|
676 |
str_of_app ty_opt func argN |
|
677 |
| (NApp (NApp (NConst (id, _, _), arg1), arg2), arg3) => |
|
678 |
if id = nun_if then |
|
679 |
nun_if ^ " " ^ str_of NONE arg1 ^ " " ^ nun_then ^ " " ^ str_of NONE arg2 ^ " " ^ |
|
680 |
nun_else ^ " " ^ str_of NONE arg3 |
|
681 |
|> nun_parens |
|
682 |
else |
|
683 |
str_of_app ty_opt func argN |
|
684 |
| (NConst (id, _, _), NAbs _) => |
|
685 |
if is_nun_const_quantifier id then |
|
686 |
let val (vars, body) = strip_nun_binders id app in |
|
687 |
id ^ " " ^ space_implode " " (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^ |
|
688 |
str_of NONE body |
|
689 |
end |
|
690 |
else |
|
691 |
str_of_app ty_opt func argN |
|
692 |
| _ => str_of_app ty_opt func argN); |
|
693 |
in |
|
694 |
(str_of_tmty, str_of NONE) |
|
695 |
end; |
|
696 |
||
697 |
val empty_name_pool = {nice_of_ugly = Symtab.empty, ugly_of_nice = Symtab.empty}; |
|
698 |
||
699 |
val nice_of_ugly_suggestion = |
|
700 |
unascii_of #> Long_Name.base_name #> ascii_of #> unsuffix nun_custom_id_suffix |
|
701 |
#> (fn s => if s = "" orelse not (Char.isAlpha (String.sub (s, 0))) then "x" ^ s else s); |
|
702 |
||
703 |
fun allocate_nice ({nice_of_ugly, ugly_of_nice} : name_pool) (ugly, nice_sugg0) = |
|
704 |
let |
|
705 |
fun alloc j = |
|
706 |
let val nice_sugg = index_name nice_sugg0 j in |
|
707 |
(case Symtab.lookup ugly_of_nice nice_sugg of |
|
708 |
NONE => |
|
709 |
(nice_sugg, |
|
710 |
{nice_of_ugly = Symtab.update_new (ugly, nice_sugg) nice_of_ugly, |
|
711 |
ugly_of_nice = Symtab.update_new (nice_sugg, ugly) ugly_of_nice}) |
|
712 |
| SOME _ => alloc (j + 1)) |
|
713 |
end; |
|
714 |
in |
|
715 |
alloc 0 |
|
716 |
end; |
|
717 |
||
718 |
fun nice_ident ugly (pool as {nice_of_ugly, ...}) = |
|
719 |
if String.isSuffix nun_custom_id_suffix ugly then |
|
720 |
(case Symtab.lookup nice_of_ugly ugly of |
|
721 |
NONE => allocate_nice pool (ugly, nice_of_ugly_suggestion ugly) |
|
722 |
| SOME nice => (nice, pool)) |
|
723 |
else |
|
724 |
(ugly, pool); |
|
725 |
||
726 |
fun nice_nun_problem problem = |
|
727 |
fold_map_nun_problem_idents nice_ident problem empty_name_pool; |
|
728 |
||
729 |
fun str_of_tval (NType (id, tys)) = |
|
730 |
str_of_ident id ^ " " ^ nun_colon ^ " " ^ |
|
731 |
fold (K (prefix (nun_type ^ " " ^ nun_arrow ^ " "))) tys nun_type; |
|
732 |
||
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
733 |
fun is_triv_subset (NAbs (_, body)) = is_triv_subset body |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
734 |
| is_triv_subset (NConst (id, _, _)) = (id = nun_true) |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
735 |
| is_triv_subset _ = false; |
64389 | 736 |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
737 |
fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} = |
64389 | 738 |
str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^ |
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
739 |
(case subset of |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
740 |
NONE => "" |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
741 |
| SOME s => if is_triv_subset s then "" else "\n " ^ nun_subset ^ " " ^ str_of_tm s) ^ |
64429
582f54f6b29b
adapted Nunchaku integration to keyword renaming
blanchet
parents:
64411
diff
changeset
|
742 |
(* TODO: use nun_quotient when possible *) |
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
743 |
(case quotient of |
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
744 |
NONE => "" |
64429
582f54f6b29b
adapted Nunchaku integration to keyword renaming
blanchet
parents:
64411
diff
changeset
|
745 |
| SOME q => "\n " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^ |
64389 | 746 |
"\n " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n " ^ nun_concrete ^ " " ^ str_of_tm rep; |
747 |
||
748 |
fun str_of_nun_ctr_spec {ctr, arg_tys} = |
|
749 |
str_of_tm ctr ^ str_of_nun_arg_list str_of_ty arg_tys; |
|
750 |
||
751 |
fun str_of_nun_co_data_spec {ty, ctrs} = |
|
752 |
str_of_ty ty ^ " " ^ nun_assign ^ "\n " ^ |
|
753 |
space_implode ("\n" ^ nun_bar ^ " ") (map str_of_nun_ctr_spec ctrs); |
|
754 |
||
755 |
fun str_of_nun_const_spec {const, props} = |
|
756 |
str_of_tmty const ^ " " ^ nun_assign ^ "\n " ^ |
|
757 |
space_implode (nun_semicolon ^ "\n ") (map str_of_tm props); |
|
758 |
||
759 |
fun str_of_nun_consts_spec {consts, props} = |
|
760 |
space_implode (" " ^ nun_and ^ "\n ") (map str_of_tmty consts) ^ " " ^ nun_assign ^ "\n " ^ |
|
761 |
space_implode (nun_semicolon ^ "\n ") (map str_of_tm props); |
|
762 |
||
763 |
fun str_of_nun_cards_suffix (NONE, NONE) = "" |
|
764 |
| str_of_nun_cards_suffix (c1, c2) = |
|
765 |
let |
|
766 |
val s1 = Option.map (prefix "min_card " o signed_string_of_int) c1; |
|
767 |
val s2 = Option.map (prefix "max_card " o signed_string_of_int) c2; |
|
768 |
in |
|
769 |
enclose " [" "]" (space_implode ", " (map_filter I [s1, s2])) |
|
770 |
end; |
|
771 |
||
772 |
fun str_of_nun_command (NTVal (ty, cards)) = |
|
773 |
nun_val ^ " " ^ str_of_tval ty ^ str_of_nun_cards_suffix cards |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
774 |
| str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_copy_spec spec |
64389 | 775 |
| str_of_nun_command (NData specs) = |
776 |
nun_data ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs |
|
777 |
| str_of_nun_command (NCodata specs) = |
|
778 |
nun_codata ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs |
|
779 |
| str_of_nun_command (NVal (tm, ty)) = |
|
780 |
nun_val ^ " " ^ str_of_tm tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty |
|
781 |
| str_of_nun_command (NPred (wf, specs)) = |
|
782 |
nun_pred ^ " " ^ (if wf then nun_lbracket ^ nun_wf ^ nun_rbracket ^ " " else "") ^ |
|
783 |
str_of_nun_and_list str_of_nun_const_spec specs |
|
784 |
| str_of_nun_command (NCopred specs) = |
|
785 |
nun_copred ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs |
|
786 |
| str_of_nun_command (NRec specs) = |
|
787 |
nun_rec ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs |
|
788 |
| str_of_nun_command (NSpec spec) = nun_spec ^ " " ^ str_of_nun_consts_spec spec |
|
789 |
| str_of_nun_command (NAxiom tm) = nun_axiom ^ " " ^ str_of_tm tm |
|
790 |
| str_of_nun_command (NGoal tm) = nun_goal ^ " " ^ str_of_tm tm |
|
791 |
| str_of_nun_command (NEval tm) = nun_hash ^ " " ^ nun_eval ^ " " ^ str_of_tm tm; |
|
792 |
||
793 |
fun str_of_nun_problem {commandss, sound, complete} = |
|
794 |
map (cat_lines o map (suffix nun_dot o str_of_nun_command)) commandss |
|
795 |
|> space_implode "\n\n" |> suffix "\n" |
|
796 |
|> prefix (nun_hash ^ " " ^ (if sound then "sound" else "unsound") ^ "\n") |
|
797 |
|> prefix (nun_hash ^ " " ^ (if complete then "complete" else "incomplete") ^ "\n"); |
|
798 |
||
799 |
end; |