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