src/HOL/Tools/datatype_codegen.ML
changeset 19346 c4c003abd830
parent 19008 14c1b2f5dda4
child 19458 a70f1b0f09cd
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Apr 06 16:10:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Apr 06 16:10:46 2006 +0200
     1.3 @@ -7,6 +7,11 @@
     1.4  
     1.5  signature DATATYPE_CODEGEN =
     1.6  sig
     1.7 +  val get_datatype_spec_thms: theory -> string
     1.8 +    -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.9 +  val get_case_const_data: theory -> string -> (string * int) list option
    1.10 +  val get_all_datatype_cons: theory -> (string * string) list
    1.11 +  val get_datatype_case_consts: theory -> string list
    1.12    val setup: theory -> theory
    1.13  end;
    1.14  
    1.15 @@ -297,19 +302,58 @@
    1.16    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
    1.17  
    1.18  
    1.19 +(** code 2nd generation **)
    1.20 +
    1.21 +fun datatype_tac thy dtco =
    1.22 +  let
    1.23 +    val ctxt = Context.init_proof thy;
    1.24 +    val inject = (#inject o DatatypePackage.the_datatype thy) dtco;
    1.25 +    val simpset = Simplifier.context ctxt
    1.26 +      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    1.27 +  in
    1.28 +    (TRY o ALLGOALS o resolve_tac) [HOL.eq_reflection]
    1.29 +    THEN (
    1.30 +      (ALLGOALS o resolve_tac) (eqTrueI :: inject)
    1.31 +      ORELSE (ALLGOALS o simp_tac) simpset
    1.32 +    )
    1.33 +    THEN (ALLGOALS o resolve_tac) [HOL.refl, Drule.reflexive_thm]
    1.34 +  end;
    1.35 +
    1.36 +fun get_datatype_spec_thms thy dtco =
    1.37 +  case DatatypePackage.get_datatype_spec thy dtco
    1.38 +   of SOME vs_cos =>
    1.39 +        SOME (vs_cos, datatype_tac thy dtco)
    1.40 +    | NONE => NONE;
    1.41 +
    1.42 +fun get_all_datatype_cons thy =
    1.43 +  Symtab.fold (fn (dtco, _) => fold
    1.44 +    (fn (co, _) => cons (co, dtco))
    1.45 +      ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
    1.46 +        (DatatypePackage.get_datatypes thy) [];
    1.47 +
    1.48 +fun get_case_const_data thy c =
    1.49 +  case find_first (fn (_, {index, descr, case_name, ...}) =>
    1.50 +      case_name = c
    1.51 +    ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
    1.52 +   of NONE => NONE
    1.53 +    | SOME (_, {index, descr, ...}) =>
    1.54 +        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    1.55 +
    1.56 +fun get_datatype_case_consts thy =
    1.57 +  Symtab.fold (fn (_, {case_name, ...}) => cons case_name)
    1.58 +    (DatatypePackage.get_datatypes thy) [];
    1.59 +
    1.60  val setup = 
    1.61    add_codegen "datatype" datatype_codegen #>
    1.62    add_tycodegen "datatype" datatype_tycodegen #>
    1.63 +  CodegenTheorems.add_datatype_extr
    1.64 +    get_datatype_spec_thms #>
    1.65    CodegenPackage.set_get_datatype
    1.66 -    DatatypePackage.get_datatype #>
    1.67 +    DatatypePackage.get_datatype_spec #>
    1.68    CodegenPackage.set_get_all_datatype_cons
    1.69 -    DatatypePackage.get_all_datatype_cons #>
    1.70 -  (fn thy => thy |> CodegenPackage.add_eqextr_default ("equality",
    1.71 -    (CodegenPackage.eqextr_eq
    1.72 -      DatatypePackage.get_eq_equations
    1.73 -      (Sign.read_term thy "False")))) #>
    1.74 +    get_all_datatype_cons #>
    1.75    CodegenPackage.ensure_datatype_case_consts
    1.76 -    DatatypePackage.get_datatype_case_consts
    1.77 -    DatatypePackage.get_case_const_data;
    1.78 +    get_datatype_case_consts
    1.79 +    get_case_const_data;
    1.80  
    1.81  end;