started work on datatype sugar
authorblanchet
Thu Aug 30 09:47:46 2012 +0200 (2012-08-30)
changeset 4901766fc7fc2d49b
parent 49016 640ce226a973
child 49018 b2884253b421
started work on datatype sugar
src/HOL/Codatatype/Codatatype.thy
src/HOL/Codatatype/Tools/bnf_sugar.ML
     1.1 --- a/src/HOL/Codatatype/Codatatype.thy	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Codatatype.thy	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (*  Title:      HOL/Codatatype/Codatatype.thy
     1.5      Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8      Copyright   2012
     1.9  
    1.10  The (co)datatype package.
    1.11 @@ -9,6 +11,10 @@
    1.12  
    1.13  theory Codatatype
    1.14  imports BNF_LFP BNF_GFP
    1.15 +keywords
    1.16 +  "bnf_sugar" :: thy_goal
    1.17 +uses
    1.18 +  "Tools/bnf_sugar.ML"
    1.19  begin
    1.20  
    1.21  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 09:47:46 2012 +0200
     2.3 @@ -0,0 +1,54 @@
     2.4 +(*  Title:      HOL/Codatatype/Tools/bnf_sugar.ML
     2.5 +    Author:     Jasmin Blanchette, TU Muenchen
     2.6 +    Copyright   2012
     2.7 +
     2.8 +Sugar on top of a BNF.
     2.9 +*)
    2.10 +
    2.11 +signature BNF_SUGAR =
    2.12 +sig
    2.13 +  val prepare_sugar : (Proof.context -> 'b -> term) ->
    2.14 +    (((typ * 'b list) * binding list) * binding list list) * 'b -> local_theory ->
    2.15 +    term list * local_theory
    2.16 +end;
    2.17 +
    2.18 +structure BNF_Sugar : BNF_SUGAR =
    2.19 +struct
    2.20 +
    2.21 +open BNF_Util
    2.22 +
    2.23 +fun prepare_sugar prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur) lthy =
    2.24 +  let
    2.25 +    val ctors = map (prep_term lthy) raw_ctors;
    2.26 +
    2.27 +    (* TODO: sanity checks on arguments *)
    2.28 +    val ctor_Tss = map (binder_types o fastype_of) ctors;
    2.29 +    val (ctor_argss, _) = lthy |>
    2.30 +      mk_Freess "x" ctor_Tss;
    2.31 +
    2.32 +    val goal_distincts =
    2.33 +      let
    2.34 +        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)))
    2.35 +        fun mk_goals [] = []
    2.36 +          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts)
    2.37 +      in
    2.38 +        mk_goals (map2 (curry Term.list_comb) ctors ctor_argss)
    2.39 +      end;
    2.40 +
    2.41 +    val goals = goal_distincts;
    2.42 +  in
    2.43 +    (goals, lthy)
    2.44 +  end;
    2.45 +
    2.46 +val parse_binding_list = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
    2.47 +
    2.48 +val bnf_sugar_cmd = (fn (goals, lthy) =>
    2.49 +  Proof.theorem NONE (K I) (map (single o rpair []) goals) lthy) oo prepare_sugar Syntax.read_term;
    2.50 +
    2.51 +val _ =
    2.52 +  Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
    2.53 +    ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
    2.54 +      parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") --
    2.55 +      Parse.term) >> bnf_sugar_cmd);
    2.56 +
    2.57 +end;