src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 49112 4de4635d8f93
child 49119 1f605c36869c
equal deleted inserted replaced
49111:9d511132394e 49112:4de4635d8f93
       
     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;