author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 66646 | 383d8e388d1b |
permissions | -rw-r--r-- |
66646 | 1 |
(* Title: HOL/Tools/Nunchaku/nunchaku_model.ML |
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
64389
diff
changeset
|
2 |
Author: Jasmin Blanchette, VU Amsterdam |
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
64389
diff
changeset
|
3 |
Copyright 2015, 2016, 2017 |
64389 | 4 |
|
5 |
Abstract syntax tree for Nunchaku models. |
|
6 |
*) |
|
7 |
||
8 |
signature NUNCHAKU_MODEL = |
|
9 |
sig |
|
10 |
type ident = Nunchaku_Problem.ident |
|
11 |
type ty = Nunchaku_Problem.ty |
|
12 |
type tm = Nunchaku_Problem.tm |
|
13 |
type name_pool = Nunchaku_Problem.name_pool |
|
14 |
||
15 |
type ty_entry = ty * tm list |
|
16 |
type tm_entry = tm * tm |
|
17 |
||
18 |
type nun_model = |
|
19 |
{type_model: ty_entry list, |
|
20 |
const_model: tm_entry list, |
|
66623 | 21 |
skolem_model: tm_entry list, |
22 |
auxiliary_model: tm_entry list} |
|
64389 | 23 |
|
24 |
val str_of_nun_model: nun_model -> string |
|
25 |
||
26 |
val allocate_ugly: name_pool -> string * string -> string * name_pool |
|
27 |
||
28 |
val ugly_nun_model: name_pool -> nun_model -> nun_model |
|
29 |
||
30 |
datatype token = |
|
31 |
Ident of ident |
|
32 |
| Symbol of ident |
|
33 |
| Atom of ident * int |
|
34 |
| End_of_Stream |
|
35 |
||
36 |
val parse_tok: ''a -> ''a list -> ''a * ''a list |
|
37 |
val parse_ident: token list -> ident * token list |
|
38 |
val parse_id: ident -> token list -> token * token list |
|
39 |
val parse_sym: ident -> token list -> token * token list |
|
40 |
val parse_atom: token list -> (ident * int) * token list |
|
41 |
val nun_model_of_str: string -> nun_model |
|
42 |
end; |
|
43 |
||
44 |
structure Nunchaku_Model : NUNCHAKU_MODEL = |
|
45 |
struct |
|
46 |
||
47 |
open Nunchaku_Problem; |
|
48 |
||
49 |
type ty_entry = ty * tm list; |
|
50 |
type tm_entry = tm * tm; |
|
51 |
||
52 |
type nun_model = |
|
53 |
{type_model: ty_entry list, |
|
54 |
const_model: tm_entry list, |
|
66623 | 55 |
skolem_model: tm_entry list, |
56 |
auxiliary_model: tm_entry list}; |
|
64389 | 57 |
|
66616 | 58 |
fun base_of_id id = hd (space_explode "/" id); |
59 |
||
64389 | 60 |
val nun_SAT = str_of_ident "SAT"; |
61 |
||
62 |
fun str_of_ty_entry (ty, tms) = |
|
63 |
"type " ^ str_of_ty ty ^ " := {" ^ commas (map str_of_tm tms) ^ "}."; |
|
64 |
||
65 |
fun str_of_tm_entry (tm, value) = |
|
66 |
"val " ^ str_of_tm tm ^ " := " ^ str_of_tm value ^ "."; |
|
67 |
||
66623 | 68 |
fun str_of_nun_model {type_model, const_model, skolem_model, auxiliary_model} = |
64389 | 69 |
map str_of_ty_entry type_model @ "" :: map str_of_tm_entry const_model @ "" :: |
66623 | 70 |
map str_of_tm_entry skolem_model @ "" :: map str_of_tm_entry auxiliary_model |
64389 | 71 |
|> cat_lines; |
72 |
||
73 |
fun fold_map_ty_entry_idents f (ty, atoms) = |
|
74 |
fold_map_ty_idents f ty |
|
75 |
##>> fold_map (fold_map_tm_idents f) atoms; |
|
76 |
||
77 |
fun fold_map_tm_entry_idents f (tm, value) = |
|
78 |
fold_map_tm_idents f tm |
|
79 |
##>> fold_map_tm_idents f value; |
|
80 |
||
66623 | 81 |
fun fold_map_nun_model_idents f {type_model, const_model, skolem_model, auxiliary_model} = |
64389 | 82 |
fold_map (fold_map_ty_entry_idents f) type_model |
83 |
##>> fold_map (fold_map_tm_entry_idents f) const_model |
|
84 |
##>> fold_map (fold_map_tm_entry_idents f) skolem_model |
|
66623 | 85 |
##>> fold_map (fold_map_tm_entry_idents f) auxiliary_model |
86 |
#>> (fn (((type_model, const_model), skolem_model), auxiliary_model) => |
|
87 |
{type_model = type_model, const_model = const_model, skolem_model = skolem_model, |
|
88 |
auxiliary_model = auxiliary_model}); |
|
64389 | 89 |
|
90 |
fun swap_name_pool ({nice_of_ugly, ugly_of_nice} : name_pool) = |
|
91 |
{nice_of_ugly = ugly_of_nice, ugly_of_nice = nice_of_ugly}; |
|
92 |
||
93 |
fun allocate_ugly pool (nice, ugly_sugg) = |
|
94 |
allocate_nice (swap_name_pool pool) (nice, ugly_sugg) ||> swap_name_pool; |
|
95 |
||
96 |
fun ugly_ident nice (pool as {ugly_of_nice, ...}) = |
|
97 |
(case Symtab.lookup ugly_of_nice nice of |
|
98 |
NONE => allocate_ugly pool (nice, nice) |
|
99 |
| SOME ugly => (ugly, pool)); |
|
100 |
||
101 |
fun ugly_nun_model pool model = |
|
102 |
fst (fold_map_nun_model_idents ugly_ident model pool); |
|
103 |
||
104 |
datatype token = |
|
105 |
Ident of ident |
|
106 |
| Symbol of ident |
|
107 |
| Atom of ident * int |
|
108 |
| End_of_Stream; |
|
109 |
||
110 |
val rev_str = String.implode o rev o String.explode; |
|
111 |
||
112 |
fun atom_of_str s = |
|
113 |
(case first_field "_" (rev_str s) of |
|
114 |
SOME (rev_suf, rev_pre) => |
|
115 |
let |
|
116 |
val pre = rev_str rev_pre; |
|
117 |
val suf = rev_str rev_suf; |
|
118 |
in |
|
119 |
(case Int.fromString suf of |
|
120 |
SOME j => Atom (ident_of_str pre, j) |
|
66623 | 121 |
| NONE => raise Fail ("ill-formed atom: " ^ s)) |
64389 | 122 |
end |
66623 | 123 |
| NONE => raise Fail ("ill-formed atom: " ^ s)); |
64389 | 124 |
|
125 |
fun is_alnum_etc_char c = Char.isAlphaNum c orelse c = #"_" orelse c = #"/"; |
|
126 |
||
66623 | 127 |
fun is_dollar_alnum_etc_char c = c = #"$" orelse is_alnum_etc_char c; |
128 |
||
64389 | 129 |
val multi_ids = |
130 |
[nun_arrow, nun_assign, nun_conj, nun_disj, nun_implies, nun_unparsable, nun_irrelevant]; |
|
131 |
||
66623 | 132 |
val nun_dollar_anon_fun_prefix_exploded = String.explode nun_dollar_anon_fun_prefix; |
64389 | 133 |
val [nun_dollar_char] = String.explode nun_dollar; |
134 |
||
135 |
fun next_token [] = (End_of_Stream, []) |
|
136 |
| next_token (c :: cs) = |
|
137 |
if Char.isSpace c then |
|
138 |
next_token cs |
|
139 |
else if c = nun_dollar_char then |
|
66623 | 140 |
let val n = find_index (not o is_dollar_alnum_etc_char) cs in |
64389 | 141 |
(if n = ~1 then (cs, []) else chop n cs) |
142 |
|>> (String.implode |
|
66623 | 143 |
#> (if is_prefix (op =) nun_dollar_anon_fun_prefix_exploded cs then ident_of_str #> Ident |
64389 | 144 |
else atom_of_str)) |
145 |
end |
|
146 |
else if is_alnum_etc_char c then |
|
147 |
let val n = find_index (not o is_alnum_etc_char) cs in |
|
148 |
(if n = ~1 then (cs, []) else chop n cs) |
|
149 |
|>> (cons c #> String.implode #> ident_of_str #> Ident) |
|
150 |
end |
|
151 |
else |
|
152 |
let |
|
153 |
fun next_multi id = |
|
154 |
let |
|
155 |
val s = str_of_ident id; |
|
156 |
val n = String.size s - 1; |
|
157 |
in |
|
158 |
if c = String.sub (s, 0) andalso |
|
159 |
is_prefix (op =) (String.explode (String.substring (s, 1, n))) cs then |
|
160 |
SOME (Symbol id, drop n cs) |
|
161 |
else |
|
162 |
NONE |
|
163 |
end; |
|
164 |
in |
|
165 |
(case get_first next_multi multi_ids of |
|
166 |
SOME res => res |
|
167 |
| NONE => (Symbol (ident_of_str (String.str c)), cs)) |
|
168 |
end; |
|
169 |
||
170 |
val tokenize = |
|
171 |
let |
|
172 |
fun toks cs = |
|
173 |
(case next_token cs of |
|
174 |
(End_of_Stream, []) => [] |
|
175 |
| (tok, cs') => tok :: toks cs'); |
|
176 |
in |
|
177 |
toks o String.explode |
|
178 |
end; |
|
179 |
||
66628 | 180 |
fun parse_enum sep scan = |
181 |
Scan.optional (scan ::: Scan.repeat (sep |-- scan)) []; |
|
64389 | 182 |
|
66628 | 183 |
fun parse_tok tok = |
184 |
Scan.one (curry (op =) tok); |
|
64389 | 185 |
|
186 |
val parse_ident = Scan.some (try (fn Ident id => id)); |
|
187 |
val parse_id = parse_tok o Ident; |
|
188 |
val parse_sym = parse_tok o Symbol; |
|
189 |
val parse_atom = Scan.some (try (fn Atom id_j => id_j)); |
|
190 |
||
191 |
val confusing_ids = [nun_else, nun_then, nun_with]; |
|
192 |
||
193 |
val parse_confusing_id = Scan.one (fn Ident id => member (op =) confusing_ids id | _ => false); |
|
194 |
||
195 |
fun parse_ty toks = |
|
196 |
(parse_ty_arg -- Scan.option (parse_sym nun_arrow -- parse_ty) |
|
197 |
>> (fn (ty, NONE) => ty |
|
198 |
| (lhs, SOME (Symbol id, rhs)) => NType (id, [lhs, rhs]))) toks |
|
199 |
and parse_ty_arg toks = |
|
200 |
(parse_ident >> (rpair [] #> NType) |
|
201 |
|| parse_sym nun_lparen |-- parse_ty --| parse_sym nun_rparen) toks; |
|
202 |
||
203 |
val parse_choice_or_unique = |
|
204 |
(parse_tok (Ident nun_choice) || parse_tok (Ident nun_unique) |
|
205 |
|| parse_tok (Ident nun_unique_unsafe)) |
|
206 |
-- parse_ty_arg |
|
207 |
>> (fn (Ident id, ty) => NConst (id, [ty], mk_arrows_ty ([ty, prop_ty], ty))); |
|
208 |
||
209 |
fun parse_tm toks = |
|
210 |
(parse_id nun_lambda |-- Scan.repeat parse_arg --| parse_sym nun_dot -- parse_tm >> nabss |
|
211 |
|| parse_id nun_mu |-- parse_arg --| parse_sym nun_dot -- parse_tm |
|
212 |
>> (fn (var, body) => |
|
213 |
let val ty = safe_ty_of body in |
|
214 |
NApp (NConst (nun_mu, [ty], mk_arrow_ty (mk_arrow_ty (ty, ty), ty)), NAbs (var, body)) |
|
215 |
end) |
|
216 |
|| parse_id nun_if |-- parse_tm --| parse_id nun_then -- parse_tm --| parse_id nun_else |
|
217 |
-- parse_tm |
|
218 |
>> (fn ((cond, th), el) => |
|
219 |
let val ty = safe_ty_of th in |
|
220 |
napps (NConst (nun_if, [ty], mk_arrows_ty ([prop_ty, ty, ty], ty)), [cond, th, el]) |
|
221 |
end) |
|
222 |
|| parse_implies) toks |
|
223 |
and parse_implies toks = |
|
224 |
(parse_disj -- Scan.option (parse_sym nun_implies -- parse_implies) |
|
225 |
>> (fn (tm, NONE) => tm |
|
226 |
| (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks |
|
227 |
and parse_disj toks = |
|
228 |
(parse_conj -- Scan.option (parse_sym nun_disj -- parse_disj) |
|
229 |
>> (fn (tm, NONE) => tm |
|
230 |
| (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks |
|
231 |
and parse_conj toks = |
|
66623 | 232 |
(parse_not -- Scan.option (parse_sym nun_conj -- parse_conj) |
64389 | 233 |
>> (fn (tm, NONE) => tm |
234 |
| (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks |
|
66623 | 235 |
and parse_not toks = |
236 |
(Scan.option (parse_sym nun_not) -- parse_equals |
|
237 |
>> (fn (NONE, tm) => tm |
|
238 |
| (SOME _, tm) => napps (NConst (nun_not, [], dummy_ty), [tm]))) toks |
|
64389 | 239 |
and parse_equals toks = |
240 |
(parse_comb -- Scan.option (parse_sym nun_equals -- parse_comb) |
|
241 |
>> (fn (tm, NONE) => tm |
|
242 |
| (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks |
|
243 |
and parse_comb toks = |
|
244 |
(parse_arg -- Scan.repeat (Scan.unless parse_confusing_id parse_arg) >> napps) toks |
|
245 |
and parse_arg toks = |
|
246 |
(parse_choice_or_unique |
|
247 |
|| parse_ident >> (fn id => NConst (id, [], dummy_ty)) |
|
66616 | 248 |
|| parse_sym nun_irrelevant |-- parse_ident |
249 |
>> (fn num => NConst (nun_irrelevant ^ num, [], dummy_ty)) |
|
64389 | 250 |
|| parse_sym nun_unparsable |-- parse_ty >> (fn ty => NConst (nun_unparsable, [], ty)) |
251 |
|| parse_sym nun_lparen |-- parse_tm -- Scan.option (parse_sym nun_colon |-- parse_ty) |
|
252 |
--| parse_sym nun_rparen |
|
253 |
>> (fn (NConst (id, [], _), SOME ty) => NConst (id, [], ty) |
|
254 |
| (tm, _) => tm) |
|
255 |
|| parse_atom >> (fn (id, j) => NAtom (j, NType (id, [])))) toks; |
|
256 |
||
257 |
val parse_witness_name = |
|
66616 | 258 |
parse_ident >> (fn id => NConst (base_of_id id, [], dummy_ty)); |
64389 | 259 |
|
260 |
val parse_witness = |
|
261 |
parse_id nun__witness_of |-- parse_sym nun_lparen |-- (parse_id nun_forall || parse_id nun_exists) |
|
262 |
|-- Scan.option (parse_sym nun_lparen) |-- parse_witness_name |
|
263 |
--| Scan.repeat (Scan.one (curry (op <>) (Symbol nun_assign))); |
|
264 |
||
66623 | 265 |
val parse_anon_fun_name = |
266 |
Scan.one (fn Ident id => String.isPrefix nun_dollar_anon_fun_prefix id | _ => false); |
|
267 |
||
268 |
val parse_anon_fun = |
|
269 |
parse_anon_fun_name >> (fn Ident id => NConst (id, [], dummy_ty)); |
|
270 |
||
64389 | 271 |
datatype entry = |
272 |
Type_Entry of ty_entry |
|
66623 | 273 |
| Const_Entry of tm_entry |
64389 | 274 |
| Skolem_Entry of tm_entry |
66623 | 275 |
| Auxiliary_Entry of tm_entry; |
64389 | 276 |
|
277 |
val parse_entry = |
|
278 |
(parse_id nun_type |-- parse_ty --| parse_sym nun_assign --| parse_sym nun_lbrace -- |
|
279 |
parse_enum (parse_sym nun_comma) parse_tm --| parse_sym nun_rbrace |
|
280 |
>> Type_Entry |
|
66623 | 281 |
|| parse_id nun_val |-- parse_anon_fun --| parse_sym nun_assign -- parse_tm >> Auxiliary_Entry |
64389 | 282 |
|| parse_id nun_val |-- parse_witness --| parse_sym nun_assign -- parse_tm >> Skolem_Entry |
283 |
|| parse_id nun_val |-- parse_tm --| parse_sym nun_assign -- parse_tm >> Const_Entry) |
|
284 |
--| parse_sym nun_dot; |
|
285 |
||
286 |
val parse_model = |
|
287 |
parse_id nun_SAT |-- parse_sym nun_colon |-- parse_sym nun_lbrace |-- Scan.repeat parse_entry |
|
288 |
--| parse_sym nun_rbrace; |
|
289 |
||
66623 | 290 |
fun add_entry entry ({type_model, const_model, skolem_model, auxiliary_model} : nun_model) = |
64389 | 291 |
(case entry of |
292 |
Type_Entry e => |
|
66623 | 293 |
{type_model = e :: type_model, const_model = const_model, skolem_model = skolem_model, |
294 |
auxiliary_model = auxiliary_model} |
|
295 |
| Const_Entry e => |
|
296 |
{type_model = type_model, const_model = e :: const_model, skolem_model = skolem_model, |
|
297 |
auxiliary_model = auxiliary_model} |
|
64389 | 298 |
| Skolem_Entry e => |
66623 | 299 |
{type_model = type_model, const_model = const_model, skolem_model = e :: skolem_model, |
300 |
auxiliary_model = auxiliary_model} |
|
301 |
| Auxiliary_Entry e => |
|
302 |
{type_model = type_model, const_model = const_model, skolem_model = skolem_model, |
|
303 |
auxiliary_model = e :: auxiliary_model}); |
|
64389 | 304 |
|
305 |
fun nun_model_of_str str = |
|
306 |
let val (entries, _) = parse_model (tokenize str) in |
|
66623 | 307 |
{type_model = [], const_model = [], skolem_model = [], auxiliary_model = []} |
64389 | 308 |
|> fold_rev add_entry entries |
309 |
end; |
|
310 |
||
311 |
end; |