--- a/src/HOL/Extraction/Pigeonhole.thy Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy Fri Mar 23 09:40:50 2007 +0100
@@ -282,50 +282,55 @@
we generate ML code from them.
*}
-consts_code
- arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-
-code_module PH
-contains
- test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
- test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m - 1)"
- sel = "op !"
-
-ML "timeit (fn () => PH.test 10)"
-ML "timeit (fn () => PH.test' 10)"
-ML "timeit (fn () => PH.test 20)"
-ML "timeit (fn () => PH.test' 20)"
-ML "timeit (fn () => PH.test 25)"
-ML "timeit (fn () => PH.test' 25)"
-ML "timeit (fn () => PH.test 500)"
-
-ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
-
-definition
- arbitrary_nat :: "nat \<times> nat" where
- [symmetric, code inline]: "arbitrary_nat = arbitrary"
-definition
- arbitrary_nat_subst :: "nat \<times> nat" where
- "arbitrary_nat_subst = (0, 0)"
-
-code_axioms
- arbitrary_nat \<equiv> arbitrary_nat_subst
-
definition
"test n = pigeonhole n (\<lambda>m. m - 1)"
definition
"test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
+definition
+ "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
-code_gen test test' "op !" (SML #)
+
+consts_code
+ arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
+
+definition
+ arbitrary_nat_pair :: "nat \<times> nat" where
+ [symmetric, code inline]: "arbitrary_nat_pair = arbitrary"
+
+code_const arbitrary_nat_pair (SML "(~1, ~1)")
+ (* this is justified since for valid inputs this "arbitrary" will be dropped
+ in the next recursion step in pigeonhole_def *)
+code_module PH
+contains
+ test = test
+ test' = test'
+ test'' = test''
+
+code_gen test test' test'' (SML #)
+
+ML "timeit (fn () => PH.test 10)"
ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
+
+ML "timeit (fn () => PH.test' 10)"
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
+
+ML "timeit (fn () => PH.test 20)"
ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
+
+ML "timeit (fn () => PH.test' 20)"
ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
+
+ML "timeit (fn () => PH.test 25)"
ML "timeit (fn () => ROOT.Pigeonhole.test 25)"
+
+ML "timeit (fn () => PH.test' 25)"
ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"
+
+ML "timeit (fn () => PH.test 500)"
ML "timeit (fn () => ROOT.Pigeonhole.test 500)"
-ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])"
+ML "timeit PH.test''"
+ML "timeit ROOT.Pigeonhole.test''"
end
--- a/src/HOL/Library/EfficientNat.thy Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy Fri Mar 23 09:40:50 2007 +0100
@@ -148,6 +148,8 @@
@{typ nat} is no longer a datatype but embedded into the integers.
*}
+code_datatype nat_of_int
+
code_const "0::nat"
(SML "!(0 : IntInf.int)")
(OCaml "Big'_int.big'_int'_of'_int/ 0")
@@ -158,10 +160,6 @@
(OCaml "Big_int.succ'_big'_int")
(Haskell "!((_) + 1)")
-setup {*
- CodegenData.add_datatype ("nat", ([], []))
-*}
-
types_code
nat ("int")
attach (term_of) {*
--- a/src/HOL/ex/Codegenerator_Rat.thy Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/ex/Codegenerator_Rat.thy Fri Mar 23 09:40:50 2007 +0100
@@ -6,7 +6,7 @@
header {* Simple example for executable rational numbers *}
theory Codegenerator_Rat
-imports ExecutableRat EfficientNat
+imports EfficientNat ExecutableRat
begin
definition
--- a/src/Pure/Tools/class_package.ML Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Mar 23 09:40:50 2007 +0100
@@ -112,13 +112,13 @@
val (_, t) = read_def thy (raw_name, raw_t);
val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
val atts = map (prep_att thy) raw_atts;
- val insts = (Consts.typargs (Sign.consts_of thy) (c, ty))
+ val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
val name = case raw_name
of "" => NONE
| _ => SOME raw_name;
in (c, (insts, ((name, t), atts))) end;
-fun read_def_cmd thy = gen_read_def thy Attrib.intern_src read_axm;
+fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
fun read_def thy = gen_read_def thy (K I) (K I);
fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
@@ -153,13 +153,13 @@
val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
val ((tyco, class), ty') = case AList.lookup (op =) cs c
- of NONE => error ("superfluous definition for constant " ^ quote c)
+ of NONE => error ("illegal definition for constant " ^ quote c)
| SOME class_ty => class_ty;
val name = case name_opt
of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
| SOME name => name;
val t' = case mk_typnorm thy_read (ty', ty)
- of NONE => error ("superfluous definition for constant " ^
+ of NONE => error ("illegal definition for constant " ^
quote c ^ "::" ^ Sign.string_of_typ thy_read ty)
| SOME norm => map_types norm t
in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
--- a/src/Pure/Tools/codegen_data.ML Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML Fri Mar 23 09:40:50 2007 +0100
@@ -14,20 +14,23 @@
val add_func: bool -> thm -> theory -> theory
val del_func: thm -> theory -> theory
val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
- val add_datatype: string * ((string * sort) list * (string * typ list) list)
- -> theory -> theory
val add_inline: thm -> theory -> theory
val del_inline: thm -> theory -> theory
val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
val del_inline_proc: string -> theory -> theory
val add_preproc: string * (theory -> thm list -> thm list) -> theory -> theory
val del_preproc: string -> theory -> theory
+ val add_datatype: string * ((string * sort) list * (string * typ list) list)
+ -> theory -> theory
+ val add_datatype_consts: CodegenConsts.const list -> theory -> theory
+
val coregular_algebra: theory -> Sorts.algebra
val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
val these_funcs: theory -> CodegenConsts.const -> thm list
val tap_typ: theory -> CodegenConsts.const -> typ option
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
+ val get_constr_typ: theory -> CodegenConsts.const -> typ option
val preprocess_cterm: cterm -> thm
@@ -190,38 +193,37 @@
in (SOME consts, thms) end;
val eq_string = op = : string * string -> bool;
+val eq_co = eq_pair eq_string (eq_list (is_equal o Term.typ_ord));
fun eq_dtyp ((vs1, cs1), (vs2, cs2)) =
gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
- andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2);
+ andalso gen_eq_set eq_co (cs1, cs2);
fun merge_dtyps (tabs as (tab1, tab2)) =
let
val tycos1 = Symtab.keys tab1;
val tycos2 = Symtab.keys tab2;
val tycos' = filter (member eq_string tycos2) tycos1;
- val touched = not (gen_eq_set (op =) (tycos1, tycos2) andalso
- gen_eq_set (eq_pair (op =) (eq_dtyp))
+ val new_types = not (gen_eq_set (op =) (tycos1, tycos2));
+ val diff_types = not (gen_eq_set (eq_pair (op =) eq_dtyp)
(AList.make (the o Symtab.lookup tab1) tycos',
AList.make (the o Symtab.lookup tab2) tycos'));
- in (touched, Symtab.merge (K true) tabs) end;
+ in ((new_types, diff_types), Symtab.merge (K true) tabs) end;
datatype spec = Spec of {
funcs: sdthms Consttab.table,
- dconstrs: string Consttab.table,
dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
};
-fun mk_spec ((funcs, dconstrs), dtyps) =
- Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps };
-fun map_spec f (Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps }) =
- mk_spec (f ((funcs, dconstrs), dtyps));
-fun merge_spec (Spec { funcs = funcs1, dconstrs = dconstrs1, dtyps = dtyps1 },
- Spec { funcs = funcs2, dconstrs = dconstrs2, dtyps = dtyps2 }) =
+fun mk_spec (funcs, dtyps) =
+ Spec { funcs = funcs, dtyps = dtyps };
+fun map_spec f (Spec { funcs = funcs, dtyps = dtyps }) =
+ mk_spec (f (funcs, dtyps));
+fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1 },
+ Spec { funcs = funcs2, dtyps = dtyps2 }) =
let
val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
- val dconstrs = Consttab.merge (K true) (dconstrs1, dconstrs2);
- val (touched', dtyps) = merge_dtyps (dtyps1, dtyps2);
- val touched = if touched' then NONE else touched_cs;
- in (touched, mk_spec ((funcs, dconstrs), dtyps)) end;
+ val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
+ val touched = if new_types orelse diff_types then NONE else touched_cs;
+ in (touched, mk_spec (funcs, dtyps)) end;
datatype exec = Exec of {
preproc: preproc,
@@ -240,16 +242,14 @@
val touched = if touched' then NONE else touched_cs;
in (touched, mk_exec (preproc, spec)) end;
val empty_exec = mk_exec (mk_preproc (([], []), []),
- mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty));
+ mk_spec (Consttab.empty, Symtab.empty));
fun the_preproc (Exec { preproc = Preproc x, ...}) = x;
fun the_spec (Exec { spec = Spec x, ...}) = x;
val the_funcs = #funcs o the_spec;
-val the_dcontrs = #dconstrs o the_spec;
val the_dtyps = #dtyps o the_spec;
val map_preproc = map_exec o apfst o map_preproc;
-val map_funcs = map_exec o apsnd o map_spec o apfst o apfst;
-val map_dconstrs = map_exec o apsnd o map_spec o apfst o apsnd;
+val map_funcs = map_exec o apsnd o map_spec o apfst;
val map_dtyps = map_exec o apsnd o map_spec o apsnd;
@@ -491,7 +491,6 @@
val ty_inst = Type (tyco, map TFree sort_args);
in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
-(*FIXME: make distinct step: building algebra from code theorems*)
fun retrieve_algebra thy operational =
Sorts.subalgebra (Sign.pp thy) operational
(weakest_constraints thy)
@@ -611,80 +610,29 @@
local
-fun consts_of_cos thy tyco vs cos =
- let
- val dty = Type (tyco, map TFree vs);
- fun mk_co (co, tys) = CodegenConsts.norm_of_typ thy (co, tys ---> dty);
- in map mk_co cos end;
-
-fun co_of_const thy (c, ty) =
- let
- fun err () = error
- ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
- val (tys, ty') = strip_type ty;
- val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
- handle TYPE _ => err ();
- val sorts = if has_duplicates (eq_fst op =) vs then err ()
- else map snd vs;
- val vs_names = Name.invent_list [] "'a" (length vs);
- val vs_map = map fst vs ~~ vs_names;
- val vs' = vs_names ~~ sorts;
- val tys' = (map o map_type_tfree) (fn (v, sort) =>
- (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
- handle Option => err ();
- in (tyco, (vs', (c, tys'))) end;
-
fun del_datatype tyco thy =
case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
of SOME (vs, cos) => let
- val consts = consts_of_cos thy tyco vs cos;
- val del =
- map_dtyps (Symtab.delete tyco)
- #> map_dconstrs (fold Consttab.delete consts)
- in map_exec_purge (SOME consts) del thy end
+ val consts = CodegenConsts.consts_of_cos thy tyco vs cos;
+ in map_exec_purge (SOME consts) (map_dtyps (Symtab.delete tyco)) thy end
| NONE => thy;
-(*FIXME integrate this auxiliary properly*)
-
in
fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
let
- val consts = consts_of_cos thy tyco vs cos;
- val add =
- map_dtyps (Symtab.update_new (tyco, vs_cos))
- #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
+ val consts = CodegenConsts.consts_of_cos thy tyco vs cos;
in
thy
|> del_datatype tyco
- |> map_exec_purge (SOME consts) add
+ |> map_exec_purge (SOME consts) (map_dtyps (Symtab.update_new (tyco, vs_cos)))
end;
-fun add_datatype_consts cs thy =
- let
- val raw_cos = map (co_of_const thy) cs;
- val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
- then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
- map ((apfst o map) snd o snd) raw_cos))
- else error ("Term constructors not referring to the same type: "
- ^ commas (map (CodegenConsts.string_of_const_typ thy) cs));
- val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
- (map fst sorts_cos);
- val cos = map snd sorts_cos;
- val vs = vs_names ~~ sorts;
- in
- thy
- |> add_datatype (tyco, (vs, cos))
- end;
+fun add_datatype_consts consts thy =
+ add_datatype (CodegenConsts.cos_of_consts thy consts) thy;
fun add_datatype_consts_cmd raw_cs thy =
- let
- val cs = map (apsnd Logic.unvarifyT o CodegenConsts.typ_of_inst thy
- o CodegenConsts.read_const thy) raw_cs
- in
- thy
- |> add_datatype_consts cs
- end;
+ add_datatype_consts (map (CodegenConsts.read_const thy) raw_cs) thy
end; (*local*)
@@ -712,6 +660,10 @@
fun del_preproc name =
(map_exec_purge NONE o map_preproc o apsnd) (delete_force "preprocessor" name);
+
+
+(** retrieval **)
+
local
fun gen_apply_inline_proc prep post thy f x =
@@ -764,25 +716,6 @@
end; (*local*)
-fun get_datatype thy tyco =
- case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
- of SOME spec => spec
- | NONE => Sign.arity_number thy tyco
- |> Name.invents Name.context "'a"
- |> map (rpair [])
- |> rpair [];
-
-fun get_datatype_of_constr thy =
- Consttab.lookup ((the_dcontrs o get_exec) thy);
-
-fun get_datatype_constr thy const =
- case Consttab.lookup ((the_dcontrs o get_exec) thy) const
- of SOME tyco => let
- val (vs, cs) = get_datatype thy tyco;
- (*FIXME continue here*)
- in NONE end
- | NONE => NONE;
-
local
fun get_funcs thy const =
@@ -821,6 +754,33 @@
end; (*local*)
+fun get_datatype thy tyco =
+ case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+ of SOME spec => spec
+ | NONE => Sign.arity_number thy tyco
+ |> Name.invents Name.context "'a"
+ |> map (rpair [])
+ |> rpair [];
+
+fun get_datatype_of_constr thy const =
+ case CodegenConsts.co_of_const' thy const
+ of SOME (tyco, (_, co)) => if member eq_co
+ (Symtab.lookup (((the_dtyps o get_exec) thy)) tyco
+ |> Option.map snd
+ |> the_default []) co then SOME tyco else NONE
+ | NONE => NONE;
+
+fun get_constr_typ thy const =
+ case get_datatype_of_constr thy const
+ of SOME tyco => let
+ val (vs, cos) = get_datatype thy tyco;
+ val (_, (_, (co, tys))) = CodegenConsts.co_of_const thy const
+ in (tys ---> Type (tyco, map TFree vs))
+ |> map_atyps (fn TFree (v, _) => TFree (v, AList.lookup (op =) vs v |> the))
+ |> Logic.varifyT
+ |> SOME end
+ | NONE => NONE;
+
(** code attributes **)
--- a/src/Pure/Tools/codegen_funcgr.ML Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML Fri Mar 23 09:40:50 2007 +0100
@@ -15,6 +15,7 @@
val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
val all: T -> CodegenConsts.const list
val pretty: theory -> T -> Pretty.T
+ structure Constgraph : GRAPH
end
signature CODEGEN_FUNCGR_RETRIEVAL =
@@ -257,11 +258,13 @@
|> Logic.varifyT
| _ => TVar (("'a", 0), [class]);
in Term.map_type_tvar (K inst) ty end;
- fun default_typ (const as (c, tys)) = case CodegenData.tap_typ thy const
- of SOME ty => ty
- | NONE => (case AxClass.class_of_param thy c
+ fun default_typ (const as (c, tys)) = case AxClass.class_of_param thy c
of SOME class => classop_typ const class
- | NONE => Sign.the_const_type thy c)
+ | NONE => (case CodegenData.tap_typ thy const
+ of SOME ty => ty
+ | NONE => (case CodegenData.get_constr_typ thy const
+ of SOME ty => ty
+ | NONE => Sign.the_const_type thy c))
fun typ_func (const as (c, tys)) thms thm =
let
val ty = CodegenFunc.typ_func thm;
--- a/src/Pure/Tools/codegen_package.ML Fri Mar 23 09:40:49 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Mar 23 09:40:50 2007 +0100
@@ -74,6 +74,19 @@
fun print_codethms thy =
Pretty.writeln o CodegenFuncgr.pretty thy o Funcgr.make thy;
+fun code_deps thy consts =
+ let
+ val gr = Funcgr.make thy consts;
+ fun mk_entry (const, (_, (_, parents))) =
+ let
+ val name = CodegenConsts.string_of_const thy const;
+ val nameparents = map (CodegenConsts.string_of_const thy) parents;
+ in { name = name, ID = name, dir = "", unfold = true,
+ path = "", parents = nameparents }
+ end;
+ val prgr = CodegenFuncgr.Constgraph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
+ in Present.display_graph prgr end;
+
structure Code = CodeDataFun
(struct
val name = "Pure/codegen_package_code";
@@ -574,8 +587,8 @@
fun raw_eval_term thy (ref_spec, t) args =
let
- val _ = (Term.fold_types o Term.fold_atyps) (fn _ =>
- error ("Term" ^ Sign.string_of_term thy t ^ "is polymorphic"))
+ val _ = (Term.map_types o Term.map_atyps) (fn _ =>
+ error ("Term " ^ Sign.string_of_term thy t ^ " contains polymorphic type"))
t;
val t' = codegen_term thy t;
in
@@ -650,9 +663,11 @@
(map (serialize' cs code) (map_filter snd seris'); ())
end;
-fun print_codethms_e thy =
+fun print_codethms_cmd thy =
print_codethms thy o map (CodegenConsts.read_const thy);
+fun code_deps_cmd thy =
+ code_deps thy o map (CodegenConsts.read_const thy);
val code_exprP = (
(Scan.repeat P.term
@@ -662,8 +677,8 @@
>> (fn (raw_cs, seris) => code raw_cs seris)
);
-val (codeK, code_abstypeK, code_axiomsK, code_thmsK) =
- ("code_gen", "code_abstype", "code_axioms", "code_thms");
+val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
+ ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps");
in
@@ -693,9 +708,15 @@
OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag
(Scan.repeat P.term
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep ((fn thy => print_codethms_e thy cs) o Toplevel.theory_of)));
+ o Toplevel.keep ((fn thy => print_codethms_cmd thy cs) o Toplevel.theory_of)));
-val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP];
+val code_depsP =
+ OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations" OuterKeyword.diag
+ (Scan.repeat P.term
+ >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+ o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+
+val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP, code_depsP];
end; (* local *)