equal
deleted
inserted
replaced
|
1 (* Title: HOL/Codatatype/Tools/bnf_fp_sugar.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Sugar for constructing LFPs and GFPs. |
|
6 *) |
|
7 |
|
8 signature BNF_FP_SUGAR = |
|
9 sig |
|
10 end; |
|
11 |
|
12 structure BNF_FP_Sugar : BNF_FP_SUGAR = |
|
13 struct |
|
14 |
|
15 fun data_cmd gfp specs lthy = |
|
16 let |
|
17 in |
|
18 lthy |
|
19 end; |
|
20 |
|
21 val parse_ctr_arg = |
|
22 Parse.$$$ "(" |-- Scan.option Parse.binding --| Parse.$$$ ":" -- Parse.typ --| Parse.$$$ ")" || |
|
23 (Parse.typ >> pair NONE); |
|
24 |
|
25 val parse_single_spec = |
|
26 Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- |
|
27 (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat parse_ctr_arg -- |
|
28 Parse.opt_mixfix)) |
|
29 >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons)); |
|
30 |
|
31 val _ = |
|
32 Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes" |
|
33 (Parse.and_list1 parse_single_spec >> data_cmd false); |
|
34 |
|
35 val _ = |
|
36 Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes" |
|
37 (Parse.and_list1 parse_single_spec >> data_cmd true); |
|
38 |
|
39 end; |