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