# HG changeset patch # User haftmann # Date 1174639250 -3600 # Node ID 3572bc633d9a212f6ef9767622b1410beaddb6d1 # Parent c78f1d924bfea2c9ba68cacd3e9776a9cd8bb102 tuned diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/Extraction/Pigeonhole.thy --- 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 \ nat" ("{* (0::nat, 0::nat) *}") - -code_module PH -contains - test = "\n. pigeonhole n (\m. m - 1)" - test' = "\n. pigeonhole_slow n (\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 \ nat" where - [symmetric, code inline]: "arbitrary_nat = arbitrary" -definition - arbitrary_nat_subst :: "nat \ nat" where - "arbitrary_nat_subst = (0, 0)" - -code_axioms - arbitrary_nat \ arbitrary_nat_subst - definition "test n = pigeonhole n (\m. m - 1)" definition "test' n = pigeonhole_slow n (\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 \ nat" ("{* (0::nat, 0::nat) *}") + +definition + arbitrary_nat_pair :: "nat \ 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 diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/Library/EfficientNat.thy --- 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) {* diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/ex/Codegenerator_Rat.thy --- 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 diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/class_package.ML --- 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; diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/codegen_data.ML --- 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 **) diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/codegen_funcgr.ML --- 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; diff -r c78f1d924bfe -r 3572bc633d9a src/Pure/Tools/codegen_package.ML --- 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 *)