adjusted to improved code generator interface
authorhaftmann
Fri Dec 02 16:05:12 2005 +0100 (2005-12-02)
changeset 18334a41ce9c10b73
parent 18333 b356f7837921
child 18335 99baddf6b0d0
adjusted to improved code generator interface
src/HOL/Integ/IntDef.thy
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Integ/IntDef.thy	Fri Dec 02 16:04:48 2005 +0100
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Dec 02 16:05:12 2005 +0100
     1.3 @@ -915,8 +915,8 @@
     1.4  
     1.5  setup {*[
     1.6    Codegen.add_codegen "number_of_codegen" number_of_codegen,
     1.7 -  CodegenPackage.add_codegen_expr
     1.8 -    ("number", CodegenPackage.codegen_number_of HOLogic.dest_binum mk_int_to_nat)
     1.9 +  CodegenPackage.add_appgen
    1.10 +    ("number", CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat)
    1.11  ]*}
    1.12  
    1.13  quickcheck_params [default_type = int]
     2.1 --- a/src/HOL/Product_Type.thy	Fri Dec 02 16:04:48 2005 +0100
     2.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 02 16:05:12 2005 +0100
     2.3 @@ -868,10 +868,10 @@
     2.4  val prod_codegen_setup = [
     2.5    Codegen.add_codegen "let_codegen" let_codegen,
     2.6    Codegen.add_codegen "split_codegen" split_codegen,
     2.7 -  CodegenPackage.add_codegen_expr
     2.8 -    ("let", CodegenPackage.codegen_let strip_abs),
     2.9 -  CodegenPackage.add_codegen_expr
    2.10 -    ("split", CodegenPackage.codegen_split strip_abs)
    2.11 +  CodegenPackage.add_appgen
    2.12 +    ("let", CodegenPackage.appgen_let strip_abs),
    2.13 +  CodegenPackage.add_appgen
    2.14 +    ("split", CodegenPackage.appgen_split strip_abs)
    2.15  ];
    2.16  
    2.17  end;
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 02 16:04:48 2005 +0100
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 02 16:05:12 2005 +0100
     3.3 @@ -305,19 +305,16 @@
     3.4    |> is_some;
     3.5  
     3.6  fun get_datatype thy dtname =
     3.7 -  case CodegenPackage.tname_of_idf thy dtname
     3.8 -   of SOME dtname =>
     3.9 -        dtname
    3.10 -        |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    3.11 -        |> Option.map #descr
    3.12 -        |> these
    3.13 -        |> get_first (fn (_, (dtname', vs, cs)) =>
    3.14 -             if dtname = dtname'
    3.15 -             then SOME (vs, map fst cs)
    3.16 -             else NONE)
    3.17 -        |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)))
    3.18 -    | _ => NONE;
    3.19 -
    3.20 +  dtname
    3.21 +  |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    3.22 +  |> Option.map #descr
    3.23 +  |> these
    3.24 +  |> get_first (fn (_, (dtname', vs, cs)) =>
    3.25 +       if dtname = dtname'
    3.26 +       then SOME (vs, map fst cs)
    3.27 +       else NONE)
    3.28 +  |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)));
    3.29 +  
    3.30  fun get_datacons thy (c, dtname) =
    3.31    let
    3.32      val descr =
    3.33 @@ -358,11 +355,13 @@
    3.34    CodegenPackage.set_is_datatype
    3.35      is_datatype,
    3.36    CodegenPackage.add_defgen
    3.37 -    ("datatype", CodegenPackage.defgen_datatype get_datatype),
    3.38 +    ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons),
    3.39    CodegenPackage.add_defgen
    3.40      ("datacons", CodegenPackage.defgen_datacons get_datacons),
    3.41 -  CodegenPackage.add_codegen_expr
    3.42 -    ("case", CodegenPackage.codegen_case get_case_const_data)
    3.43 +  CodegenPackage.add_defgen
    3.44 +    ("dataeq", CodegenPackage.defgen_datatype_eqinst get_datatype),
    3.45 +  CodegenPackage.add_appgen
    3.46 +    ("case", CodegenPackage.appgen_case get_case_const_data)
    3.47  ];
    3.48  
    3.49  end;