1.1 --- a/src/HOL/Integ/IntDef.thy Tue Nov 22 12:42:59 2005 +0100
1.2 +++ b/src/HOL/Integ/IntDef.thy Tue Nov 22 12:59:25 2005 +0100
1.3 @@ -897,6 +897,10 @@
1.4 "neg" ("(_ < 0)")
1.5
1.6 ML {*
1.7 +fun mk_int_to_nat bin =
1.8 + Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
1.9 + $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
1.10 +
1.11 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
1.12 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
1.13 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
1.14 @@ -909,7 +913,11 @@
1.15 | number_of_codegen _ _ _ _ _ _ _ = NONE;
1.16 *}
1.17
1.18 -setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
1.19 +setup {*[
1.20 + Codegen.add_codegen "number_of_codegen" number_of_codegen,
1.21 + CodegenPackage.add_codegen_expr
1.22 + ("number", CodegenPackage.codegen_number_of HOLogic.dest_binum mk_int_to_nat)
1.23 +]*}
1.24
1.25 quickcheck_params [default_type = int]
1.26
2.1 --- a/src/HOL/Product_Type.thy Tue Nov 22 12:42:59 2005 +0100
2.2 +++ b/src/HOL/Product_Type.thy Tue Nov 22 12:59:25 2005 +0100
2.3 @@ -865,9 +865,14 @@
2.4
2.5 in
2.6
2.7 -val prod_codegen_setup =
2.8 - [Codegen.add_codegen "let_codegen" let_codegen,
2.9 - Codegen.add_codegen "split_codegen" split_codegen];
2.10 +val prod_codegen_setup = [
2.11 + Codegen.add_codegen "let_codegen" let_codegen,
2.12 + Codegen.add_codegen "split_codegen" split_codegen,
2.13 + CodegenPackage.add_codegen_expr
2.14 + ("let", CodegenPackage.codegen_let strip_abs),
2.15 + CodegenPackage.add_codegen_expr
2.16 + ("split", CodegenPackage.codegen_split strip_abs)
2.17 +];
2.18
2.19 end;
2.20 *}
3.1 --- a/src/HOL/Tools/datatype_codegen.ML Tue Nov 22 12:42:59 2005 +0100
3.2 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Nov 22 12:59:25 2005 +0100
3.3 @@ -7,6 +7,9 @@
3.4
3.5 signature DATATYPE_CODEGEN =
3.6 sig
3.7 + val is_datatype: theory -> string -> bool
3.8 + val get_datatype: theory -> string -> (string list * string list) option
3.9 + val get_datacons: theory -> string * string -> typ list option
3.10 val setup: (theory -> theory) list
3.11 end;
3.12
3.13 @@ -296,9 +299,58 @@
3.14 end)
3.15 | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
3.16
3.17 +fun is_datatype thy dtyco =
3.18 + Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco
3.19 + |> is_some;
3.20
3.21 -val setup =
3.22 - [add_codegen "datatype" datatype_codegen,
3.23 - add_tycodegen "datatype" datatype_tycodegen];
3.24 +fun get_datatype thy dtname =
3.25 + case CodegenPackage.tname_of_idf thy dtname
3.26 + of SOME dtname =>
3.27 + dtname
3.28 + |> Symtab.lookup (DatatypePackage.get_datatypes thy)
3.29 + |> Option.map #descr
3.30 + |> these
3.31 + |> get_first (fn (_, (dtname', vs, cs)) =>
3.32 + if dtname = dtname'
3.33 + then SOME (vs, map fst cs)
3.34 + else NONE)
3.35 + |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)))
3.36 + | _ => NONE;
3.37 +
3.38 +fun get_datacons thy (c, dtname) =
3.39 + let
3.40 + val descr =
3.41 + dtname
3.42 + |> Symtab.lookup (DatatypePackage.get_datatypes thy)
3.43 + |> Option.map #descr
3.44 + |> these
3.45 + val one_descr =
3.46 + descr
3.47 + |> get_first (fn (_, (dtname', vs, cs)) =>
3.48 + if dtname = dtname'
3.49 + then SOME (vs, cs)
3.50 + else NONE);
3.51 + in
3.52 + if is_some one_descr
3.53 + then
3.54 + the one_descr
3.55 + |> (fn (vs, cs) =>
3.56 + c
3.57 + |> AList.lookup (op =) cs
3.58 + |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
3.59 + (map DatatypeAux.dest_DtTFree vs)))))
3.60 + else NONE
3.61 + end;
3.62 +
3.63 +val setup = [
3.64 + add_codegen "datatype" datatype_codegen,
3.65 + add_tycodegen "datatype" datatype_tycodegen,
3.66 + CodegenPackage.set_is_datatype
3.67 + is_datatype,
3.68 + CodegenPackage.add_defgen
3.69 + ("datatype", CodegenPackage.defgen_datatype get_datatype),
3.70 + CodegenPackage.add_defgen
3.71 + ("datacons", CodegenPackage.defgen_datacons get_datacons)
3.72 +];
3.73
3.74 end;
4.1 --- a/src/HOL/Tools/recfun_codegen.ML Tue Nov 22 12:42:59 2005 +0100
4.2 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Nov 22 12:59:25 2005 +0100
4.3 @@ -9,6 +9,7 @@
4.4 sig
4.5 val add: string option -> theory attribute
4.6 val del: theory attribute
4.7 + val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
4.8 val setup: (theory -> theory) list
4.9 end;
4.10
4.11 @@ -79,6 +80,19 @@
4.12 | SOME thyname => thyname)
4.13 end);
4.14
4.15 +fun get_rec_equations thy (s, T) =
4.16 + Symtab.lookup (CodegenData.get thy) s
4.17 + |> Option.map (fn thms =>
4.18 + List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms
4.19 + |> del_redundant thy [])
4.20 + |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
4.21 + |> Option.map (fn thms =>
4.22 + (preprocess thy (map fst thms),
4.23 + (snd o const_of o prop_of o fst o hd) thms))
4.24 + |> the_default ([], dummyT)
4.25 + |> apfst (map prop_of)
4.26 + |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
4.27 +
4.28 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
4.29 SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
4.30
4.31 @@ -165,11 +179,14 @@
4.32 | _ => NONE);
4.33
4.34
4.35 -val setup =
4.36 - [CodegenData.init,
4.37 - add_codegen "recfun" recfun_codegen,
4.38 - add_attribute ""
4.39 - ( Args.del |-- Scan.succeed del
4.40 - || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
4.41 +val setup = [
4.42 + CodegenData.init,
4.43 + add_codegen "recfun" recfun_codegen,
4.44 + add_attribute ""
4.45 + ( Args.del |-- Scan.succeed del
4.46 + || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
4.47 + CodegenPackage.add_defgen
4.48 + ("rec", CodegenPackage.defgen_recfun get_rec_equations)
4.49 +];
4.50
4.51 end;