src/HOL/Tools/datatype_codegen.ML
changeset 20105 454f4be984b7
parent 20071 8f3e1ddb50e6
child 20177 0af885e3dabf
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 00:34:54 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 17:00:22 2006 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/datatype_codegen.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Stefan Berghofer, TU Muenchen
     1.7 +    Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
     1.8  
     1.9  Code generator for inductive datatypes.
    1.10  *)
    1.11 @@ -10,6 +10,8 @@
    1.12    val get_datatype_spec_thms: theory -> string
    1.13      -> (((string * sort) list * (string * typ list) list) * tactic) option
    1.14    val get_all_datatype_cons: theory -> (string * string) list
    1.15 +  val dest_case_expr: theory -> term
    1.16 +    -> ((string * typ) list * ((term * typ) * (term * term) list)) option;
    1.17    val add_datatype_case_const: string -> theory -> theory
    1.18    val add_datatype_case_defs: string -> theory -> theory
    1.19    val setup: theory -> theory
    1.20 @@ -304,6 +306,34 @@
    1.21  
    1.22  (** code 2nd generation **)
    1.23  
    1.24 +fun dtyp_of_case_const thy c =
    1.25 +  get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
    1.26 +    ((Symtab.dest o DatatypePackage.get_datatypes) thy);
    1.27 +
    1.28 +fun dest_case_app cs ts tys =
    1.29 +  let
    1.30 +    val abs = CodegenThingol.give_names [] (Library.drop (length ts, tys));
    1.31 +    val (ts', t) = split_last (ts @ map Free abs);
    1.32 +    val (tys', sty) = split_last tys;
    1.33 +    fun freenames_of t = fold_aterms
    1.34 +      (fn Free (v, _) => insert (op =) v | _ => I) t [];
    1.35 +    fun dest_case ((c, tys_decl), ty) t =
    1.36 +      let
    1.37 +        val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
    1.38 +        val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
    1.39 +      in (c', t') end;
    1.40 +  in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts')) end;
    1.41 +
    1.42 +fun dest_case_expr thy t =
    1.43 +  case strip_comb t
    1.44 +   of (Const (c, ty), ts) =>
    1.45 +        (case dtyp_of_case_const thy c
    1.46 +         of SOME dtco =>
    1.47 +              let val (vs, cs) = (the o DatatypePackage.get_datatype_spec thy) dtco;
    1.48 +              in SOME (dest_case_app cs ts (Library.take (length cs + 1, (fst o strip_type) ty))) end
    1.49 +          | _ => NONE)
    1.50 +    | _ => NONE;
    1.51 +
    1.52  fun datatype_tac thy dtco =
    1.53    let
    1.54      val ctxt = Context.init_proof thy;
    1.55 @@ -333,10 +363,9 @@
    1.56  
    1.57  fun add_datatype_case_const dtco thy =
    1.58    let
    1.59 -    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
    1.60 +    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
    1.61    in
    1.62 -    CodegenPackage.add_case_const case_name
    1.63 -      ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
    1.64 +    CodegenPackage.add_appconst_i (case_name, CodegenPackage.appgen_case dest_case_expr) thy
    1.65    end;
    1.66  
    1.67  fun add_datatype_case_defs dtco thy =
    1.68 @@ -351,8 +380,6 @@
    1.69    add_tycodegen "datatype" datatype_tycodegen #>
    1.70    CodegenTheorems.add_datatype_extr
    1.71      get_datatype_spec_thms #>
    1.72 -  CodegenPackage.set_get_datatype
    1.73 -    DatatypePackage.get_datatype_spec #>
    1.74    CodegenPackage.set_get_all_datatype_cons
    1.75      get_all_datatype_cons #>
    1.76    DatatypeHooks.add add_datatype_case_const #>