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