50 |
50 |
51 type nun_model = |
51 type nun_model = |
52 {type_model: ty_entry list, |
52 {type_model: ty_entry list, |
53 const_model: tm_entry list, |
53 const_model: tm_entry list, |
54 skolem_model: tm_entry list}; |
54 skolem_model: tm_entry list}; |
|
55 |
|
56 fun base_of_id id = hd (space_explode "/" id); |
55 |
57 |
56 val nun_SAT = str_of_ident "SAT"; |
58 val nun_SAT = str_of_ident "SAT"; |
57 |
59 |
58 fun str_of_ty_entry (ty, tms) = |
60 fun str_of_ty_entry (ty, tms) = |
59 "type " ^ str_of_ty ty ^ " := {" ^ commas (map str_of_tm tms) ^ "}."; |
61 "type " ^ str_of_ty ty ^ " := {" ^ commas (map str_of_tm tms) ^ "}."; |
229 and parse_comb toks = |
231 and parse_comb toks = |
230 (parse_arg -- Scan.repeat (Scan.unless parse_confusing_id parse_arg) >> napps) toks |
232 (parse_arg -- Scan.repeat (Scan.unless parse_confusing_id parse_arg) >> napps) toks |
231 and parse_arg toks = |
233 and parse_arg toks = |
232 (parse_choice_or_unique |
234 (parse_choice_or_unique |
233 || parse_ident >> (fn id => NConst (id, [], dummy_ty)) |
235 || parse_ident >> (fn id => NConst (id, [], dummy_ty)) |
234 || parse_sym nun_irrelevant |
236 || parse_sym nun_irrelevant |-- parse_ident |
235 |-- Scan.option (parse_sym nun_lparen |-- parse_tm --| parse_sym nun_rparen) (* FIXME *) |
237 >> (fn num => NConst (nun_irrelevant ^ num, [], dummy_ty)) |
236 >> (fn _ => NConst (nun_irrelevant, [], dummy_ty)) |
|
237 || parse_sym nun_unparsable |-- parse_ty >> (fn ty => NConst (nun_unparsable, [], ty)) |
238 || parse_sym nun_unparsable |-- parse_ty >> (fn ty => NConst (nun_unparsable, [], ty)) |
238 || parse_sym nun_lparen |-- parse_tm -- Scan.option (parse_sym nun_colon |-- parse_ty) |
239 || parse_sym nun_lparen |-- parse_tm -- Scan.option (parse_sym nun_colon |-- parse_ty) |
239 --| parse_sym nun_rparen |
240 --| parse_sym nun_rparen |
240 >> (fn (NConst (id, [], _), SOME ty) => NConst (id, [], ty) |
241 >> (fn (NConst (id, [], _), SOME ty) => NConst (id, [], ty) |
241 | (tm, _) => tm) |
242 | (tm, _) => tm) |
242 || parse_atom >> (fn (id, j) => NAtom (j, NType (id, [])))) toks; |
243 || parse_atom >> (fn (id, j) => NAtom (j, NType (id, [])))) toks; |
243 |
244 |
244 val parse_witness_name = |
245 val parse_witness_name = |
245 parse_ident >> (fn id => NConst (hd (space_explode "/" id), [], dummy_ty)); |
246 parse_ident >> (fn id => NConst (base_of_id id, [], dummy_ty)); |
246 |
247 |
247 val parse_witness = |
248 val parse_witness = |
248 parse_id nun__witness_of |-- parse_sym nun_lparen |-- (parse_id nun_forall || parse_id nun_exists) |
249 parse_id nun__witness_of |-- parse_sym nun_lparen |-- (parse_id nun_forall || parse_id nun_exists) |
249 |-- Scan.option (parse_sym nun_lparen) |-- parse_witness_name |
250 |-- Scan.option (parse_sym nun_lparen) |-- parse_witness_name |
250 --| Scan.repeat (Scan.one (curry (op <>) (Symbol nun_assign))); |
251 --| Scan.repeat (Scan.one (curry (op <>) (Symbol nun_assign))); |