|
1 (* Title: HOL/Codatatype/Tools/bnf_sugar.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Sugar on top of a BNF. |
|
6 *) |
|
7 |
|
8 signature BNF_SUGAR = |
|
9 sig |
|
10 val prepare_sugar : (Proof.context -> 'b -> term) -> |
|
11 (((typ * 'b list) * binding list) * binding list list) * 'b -> local_theory -> |
|
12 term list * local_theory |
|
13 end; |
|
14 |
|
15 structure BNF_Sugar : BNF_SUGAR = |
|
16 struct |
|
17 |
|
18 open BNF_Util |
|
19 |
|
20 fun prepare_sugar prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur) lthy = |
|
21 let |
|
22 val ctors = map (prep_term lthy) raw_ctors; |
|
23 |
|
24 (* TODO: sanity checks on arguments *) |
|
25 val ctor_Tss = map (binder_types o fastype_of) ctors; |
|
26 val (ctor_argss, _) = lthy |> |
|
27 mk_Freess "x" ctor_Tss; |
|
28 |
|
29 val goal_distincts = |
|
30 let |
|
31 fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u))) |
|
32 fun mk_goals [] = [] |
|
33 | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts) |
|
34 in |
|
35 mk_goals (map2 (curry Term.list_comb) ctors ctor_argss) |
|
36 end; |
|
37 |
|
38 val goals = goal_distincts; |
|
39 in |
|
40 (goals, lthy) |
|
41 end; |
|
42 |
|
43 val parse_binding_list = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
|
44 |
|
45 val bnf_sugar_cmd = (fn (goals, lthy) => |
|
46 Proof.theorem NONE (K I) (map (single o rpair []) goals) lthy) oo prepare_sugar Syntax.read_term; |
|
47 |
|
48 val _ = |
|
49 Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" |
|
50 ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- |
|
51 parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") -- |
|
52 Parse.term) >> bnf_sugar_cmd); |
|
53 |
|
54 end; |