added function for case certificates
authorhaftmann
Mon Jul 16 09:29:04 2007 +0200 (2007-07-16)
changeset 23811b18557301bf9
parent 23810 f5e6932d0500
child 23812 f935b85fbb4c
added function for case certificates
src/HOL/Tools/datatype_codegen.ML
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Codegenerator_Rat.thy
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Jul 16 09:29:03 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Jul 16 09:29:04 2007 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val get_eq_datatype: theory -> string -> thm list
     1.5    val dest_case_expr: theory -> term
     1.6      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
     1.7 +  val get_case_cert: theory -> string -> thm
     1.8  
     1.9    type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    1.10      -> theory -> theory
    1.11 @@ -406,6 +407,36 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +fun get_case_cert thy tyco =
    1.16 +  let
    1.17 +    val raw_thms =
    1.18 +      (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
    1.19 +    val thms as hd_thm :: _ = raw_thms
    1.20 +      |> Conjunction.intr_balanced
    1.21 +      |> Drule.unvarify
    1.22 +      |> Conjunction.elim_balanced (length raw_thms)
    1.23 +      |> map Simpdata.mk_meta_eq
    1.24 +      |> map Drule.zero_var_indexes
    1.25 +    val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
    1.26 +      | _ => I) (Thm.prop_of hd_thm) [];
    1.27 +    val rhs = hd_thm
    1.28 +      |> Thm.prop_of
    1.29 +      |> Logic.dest_equals
    1.30 +      |> fst
    1.31 +      |> Term.strip_comb
    1.32 +      |> apsnd (fst o split_last)
    1.33 +      |> list_comb;
    1.34 +    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
    1.35 +    val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
    1.36 +  in
    1.37 +    thms
    1.38 +    |> Conjunction.intr_balanced
    1.39 +    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
    1.40 +    |> Thm.implies_intr asm
    1.41 +    |> Thm.generalize ([], params) 0
    1.42 +    |> Thm.varifyT
    1.43 +  end;
    1.44 +
    1.45  
    1.46  
    1.47  (** codetypes for code 2nd generation **)
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Jul 16 09:29:03 2007 +0200
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Jul 16 09:29:04 2007 +0200
     2.3 @@ -8,7 +8,11 @@
     2.4  imports ExecutableContent
     2.5  begin
     2.6  
     2.7 -code_gen "*" in SML in OCaml file - in OCaml file -
     2.8 -code_gen in SML in OCaml file - in OCaml file -
     2.9 +code_gen "*" in SML to CodegenTest
    2.10 +  in OCaml file -
    2.11 +  in Haskell file -
    2.12 +code_gen in SML to CodegenTest
    2.13 +  in OCaml file -
    2.14 +  in Haskell file -
    2.15  
    2.16  end
     3.1 --- a/src/HOL/ex/Codegenerator_Rat.thy	Mon Jul 16 09:29:03 2007 +0200
     3.2 +++ b/src/HOL/ex/Codegenerator_Rat.thy	Mon Jul 16 09:29:04 2007 +0200
     3.3 @@ -29,8 +29,10 @@
     3.4  definition
     3.5    "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
     3.6  
     3.7 -code_gen foobar in SML in OCaml file - in Haskell file -
     3.8 -ML {* ROOT.Codegenerator_Rat.foobar *}
     3.9 +code_gen foobar in SML to Foo
    3.10 +  in OCaml file -
    3.11 +  in Haskell file -
    3.12 +ML {* Foo.foobar *}
    3.13  
    3.14  code_module Foo
    3.15    contains foobar