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