# HG changeset patch # User haftmann # Date 1242151625 -7200 # Node ID d8a6122affd7dc42512bda988e774a40470822fa # Parent fc654c95c29e362b6240af01069a0e46891e76dd# Parent 80218ee73167b1788f9620ddca6c8ae5b8bbc86c merged diff -r fc654c95c29e -r d8a6122affd7 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue May 12 17:32:50 2009 +0100 +++ b/src/HOL/HOL.thy Tue May 12 20:07:05 2009 +0200 @@ -1870,8 +1870,8 @@ subsubsection {* Generic code generator preprocessor *} setup {* - Code.map_pre (K HOL_basic_ss) - #> Code.map_post (K HOL_basic_ss) + Code_Preproc.map_pre (K HOL_basic_ss) + #> Code_Preproc.map_post (K HOL_basic_ss) *} subsubsection {* Generic code generator target languages *} diff -r fc654c95c29e -r d8a6122affd7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue May 12 17:32:50 2009 +0100 +++ b/src/HOL/IsaMakefile Tue May 12 20:07:05 2009 +0200 @@ -92,10 +92,10 @@ $(SRC)/Tools/auto_solve.ML \ $(SRC)/Tools/code/code_haskell.ML \ $(SRC)/Tools/code/code_ml.ML \ + $(SRC)/Tools/code/code_preproc.ML \ $(SRC)/Tools/code/code_printer.ML \ $(SRC)/Tools/code/code_target.ML \ $(SRC)/Tools/code/code_thingol.ML \ - $(SRC)/Tools/code/code_wellsorted.ML \ $(SRC)/Tools/coherent.ML \ $(SRC)/Tools/eqsubst.ML \ $(SRC)/Tools/induct.ML \ diff -r fc654c95c29e -r d8a6122affd7 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Tue May 12 17:32:50 2009 +0100 +++ b/src/HOL/Predicate.thy Tue May 12 20:07:05 2009 +0200 @@ -669,11 +669,26 @@ code_const Seq and Empty and Insert and Join (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") -text {* dummy setup for @{text code_pred} keyword *} +text {* dummy setup for @{text code_pred} and @{text values} keywords *} ML {* -OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" - OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]]))) +local + +structure P = OuterParse; + +val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; + +in + +val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" + OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]]))); + +val _ = OuterSyntax.improper_command "values" "evaluate and print enumerations" + OuterKeyword.diag ((opt_modes -- P.term) + >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep + (K ()))); + +end *} no_notation diff -r fc654c95c29e -r d8a6122affd7 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/HOL/Tools/recfun_codegen.ML Tue May 12 20:07:05 2009 +0200 @@ -54,7 +54,7 @@ let val c' = AxClass.unoverload_const thy (c, T); val opt_name = Symtab.lookup (ModuleData.get thy) c'; - val thms = Code.these_raw_eqns thy c' + val thms = Code.these_eqns thy c' |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |> expand_eta thy |> map_filter (meta_eq_to_obj_eq thy) diff -r fc654c95c29e -r d8a6122affd7 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Tue May 12 17:32:50 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile.thy Tue May 12 20:07:05 2009 +0200 @@ -7,11 +7,6 @@ setup {* Predicate_Compile.setup *} -ML {* - OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" - OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd) -*} - text {* Experimental code *} @@ -59,16 +54,20 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -setup {* pred_compile "even" *} -thm even_codegen +code_pred even + using assms by (rule even.cases) + +thm even.equation inductive append :: "'a list \ 'a list \ 'a list \ bool" where append_Nil: "append [] xs xs" | append_Cons: "append xs ys zs \ append (x # xs) ys (x # zs)" -setup {* pred_compile "append" *} -thm append_codegen +code_pred append + using assms by (rule append.cases) + +thm append.equation inductive partition :: "('a \ bool) \ 'a list \ 'a list \ 'a list \ bool" @@ -77,27 +76,21 @@ | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -setup {* pred_compile "partition" *} -thm partition_codegen +code_pred partition + using assms by (rule partition.cases) + +thm partition.equation + -setup {* pred_compile "tranclp" *} -thm tranclp_codegen +code_pred tranclp + using assms by (rule tranclp.cases) + +thm tranclp.equation + ML_val {* Predicate_Compile.modes_of @{theory} @{const_name partition} *} ML_val {* Predicate_Compile.modes_of @{theory} @{const_name tranclp} *} ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *} -section {* Example for user interface *} - -inductive append2 :: "'a list \ 'a list \ 'a list \ bool" where - append2_Nil: "append2 [] xs xs" - | append2_Cons: "append2 xs ys zs \ append2 (x # xs) ys (x # zs)" - -(*code_pred append2 - using assms by (rule append2.cases) - -thm append2_codegen -thm append2_cases*) - end \ No newline at end of file diff -r fc654c95c29e -r d8a6122affd7 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/HOL/ex/predicate_compile.ML Tue May 12 20:07:05 2009 +0200 @@ -7,25 +7,22 @@ signature PREDICATE_COMPILE = sig type mode = int list option list * int list - val create_def_equation': string -> mode option -> theory -> theory - val create_def_equation: string -> theory -> theory + val prove_equation: string -> mode option -> theory -> theory val intro_rule: theory -> string -> mode -> thm val elim_rule: theory -> string -> mode -> thm - val strip_intro_concl : term -> int -> (term * (term list * term list)) - val code_ind_intros_attrib : attribute - val code_ind_cases_attrib : attribute + val strip_intro_concl: term -> int -> term * (term list * term list) val modename_of: theory -> string -> mode -> string val modes_of: theory -> string -> mode list - val setup : theory -> theory - val code_pred : string -> Proof.context -> Proof.state - val code_pred_cmd : string -> Proof.context -> Proof.state - val print_alternative_rules : theory -> theory + val setup: theory -> theory + val code_pred: string -> Proof.context -> Proof.state + val code_pred_cmd: string -> Proof.context -> Proof.state + val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) val do_proofs: bool ref - val pred_intros : theory -> string -> thm list - val get_nparams : theory -> string -> int + val pred_intros: theory -> string -> thm list + val get_nparams: theory -> string -> int end; -structure Predicate_Compile: PREDICATE_COMPILE = +structure Predicate_Compile : PREDICATE_COMPILE = struct (** auxiliary **) @@ -1224,7 +1221,7 @@ val Ts = binder_types T val names = Name.variant_list [] (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts))) - val vs = map Free (names ~~ Ts) + val vs = map2 (curry Free) names Ts val clausehd = HOLogic.mk_Trueprop (list_comb(Const (predname, T), vs)) val intro_t = Logic.mk_implies (@{prop False}, clausehd) val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)) @@ -1242,9 +1239,9 @@ (* main function *********************************************************************) (*************************************************************************************) -fun create_def_equation' ind_name (mode : mode option) thy = +fun prove_equation ind_name mode thy = let - val _ = tracing ("starting create_def_equation' with " ^ ind_name) + val _ = tracing ("starting prove_equation' with " ^ ind_name) val (prednames, preds) = case (try (InductivePackage.the_inductive (ProofContext.init thy)) ind_name) of SOME info => let val preds = info |> snd |> #preds @@ -1268,7 +1265,7 @@ fun rec_call name thy = (*FIXME use member instead of infix mem*) if not (name mem (Symtab.keys (#modes (IndCodegenData.get thy)))) then - create_def_equation name thy else thy + prove_equation name NONE thy else thy val thy'' = fold rec_call name_of_calls thy' val _ = tracing "returning from recursive calls" val _ = tracing "starting mode inference" @@ -1322,12 +1319,11 @@ val _ = tracing "starting proof" val result_thms = prove_preds thy''' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts)) val (_, thy'''') = yield_singleton PureThy.add_thmss - ((Binding.name (Long_Name.base_name ind_name ^ "_codegen" (*FIXME other suffix*)), result_thms), + ((Binding.qualify true (Long_Name.base_name ind_name) (Binding.name "equation"), result_thms), [Attrib.attribute_i thy''' Code.add_default_eqn_attrib]) thy''' in thy'''' end -and create_def_equation ind_name thy = create_def_equation' ind_name NONE thy fun set_nparams (pred, nparams) thy = map_nparams (Symtab.update (pred, nparams)) thy @@ -1345,22 +1341,12 @@ in () end val _ = map print preds in thy end; - -fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I) -val code_ind_intros_attrib = attrib add_intro_thm - -val code_ind_cases_attrib = attrib add_elim_thm - -val setup = - Attrib.setup @{binding code_ind_intros} (Scan.succeed code_ind_intros_attrib) - "adding alternative introduction rules for code generation of inductive predicates" #> - Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib) - "adding alternative elimination rules for code generation of inductive predicates"; (* generation of case rules from user-given introduction rules *) - fun mk_casesrule introrules nparams ctxt = let +fun mk_casesrule introrules nparams ctxt = + let val intros = map prop_of introrules val (pred, (params, args)) = strip_intro_concl (hd intros) nparams val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt @@ -1368,6 +1354,7 @@ val (argnames, ctxt2) = Variable.variant_fixes (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1 val argvs = map Free (argnames ~~ (map fastype_of args)) + (*FIXME map2*) fun mk_case intro = let val (_, (_, args)) = strip_intro_concl intro nparams val prems = Logic.strip_imp_prems intro @@ -1384,32 +1371,59 @@ ctxt2 in (pred, prop, ctxt3) end; -(* setup for user interface *) + +(** user interface **) + +local + +fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); + +val add_elim_attrib = attrib add_elim_thm; - fun generic_code_pred prep_const raw_const lthy = - let - val thy = (ProofContext.theory_of lthy) - val const = prep_const thy raw_const - val nparams = get_nparams thy const - val intro_rules = pred_intros thy const - val (((tfrees, frees), fact), lthy') = - Variable.import_thms true intro_rules lthy; - val (pred, prop, lthy'') = mk_casesrule fact nparams lthy' - val (predname, _) = dest_Const pred - fun after_qed [[th]] lthy'' = - LocalTheory.note Thm.theoremK - ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *) - [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy'' - |> snd - |> LocalTheory.theory (create_def_equation predname) - in - Proof.theorem_i NONE after_qed [[(prop, [])]] lthy'' - end; +fun generic_code_pred prep_const raw_const lthy = + let + val thy = ProofContext.theory_of lthy + val const = prep_const thy raw_const + val nparams = get_nparams thy const + val intro_rules = pred_intros thy const + val (((tfrees, frees), fact), lthy') = + Variable.import_thms true intro_rules lthy; + val (pred, prop, lthy'') = mk_casesrule fact nparams lthy' + val (predname, _) = dest_Const pred + fun after_qed [[th]] lthy'' = + lthy'' + |> LocalTheory.note Thm.theoremK + ((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th]) + |> snd + |> LocalTheory.theory (prove_equation predname NONE) + in + Proof.theorem_i NONE after_qed [[(prop, [])]] lthy'' + end; + +structure P = OuterParse - val code_pred = generic_code_pred (K I); - val code_pred_cmd = generic_code_pred Code_Unit.read_const +in + +val code_pred = generic_code_pred (K I); +val code_pred_cmd = generic_code_pred Code_Unit.read_const + +val setup = + Attrib.setup @{binding code_ind_intros} (Scan.succeed (attrib add_intro_thm)) + "adding alternative introduction rules for code generation of inductive predicates" #> + Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib) + "adding alternative elimination rules for code generation of inductive predicates"; + (*FIXME name discrepancy in attribs and ML code*) + (*FIXME intros should be better named intro*) + (*FIXME why distinguished atribute for cases?*) + +val _ = OuterSyntax.local_theory_to_proof "code_pred" + "prove equations for predicate specified by intro/elim rules" + OuterKeyword.thy_goal (P.term_group >> code_pred_cmd) + +end + +(*FIXME +- Naming of auxiliary rules necessary? +*) end; - -fun pred_compile name thy = Predicate_Compile.create_def_equation - (Sign.intern_const thy name) thy; diff -r fc654c95c29e -r d8a6122affd7 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/Pure/Isar/code.ML Tue May 12 20:07:05 2009 +0200 @@ -15,13 +15,6 @@ val del_eqn: thm -> theory -> theory val del_eqns: string -> theory -> theory val add_eqnl: string * (thm * bool) list lazy -> theory -> theory - val map_pre: (simpset -> simpset) -> theory -> theory - val map_post: (simpset -> simpset) -> theory -> theory - val add_inline: thm -> theory -> theory - val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory - val del_functrans: string -> theory -> theory - val simple_functrans: (theory -> thm list -> thm list option) - -> theory -> (thm * bool) list -> (thm * bool) list option val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory val type_interpretation: @@ -32,17 +25,14 @@ val purge_data: theory -> theory val these_eqns: theory -> string -> (thm * bool) list - val these_raw_eqns: theory -> string -> (thm * bool) list val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option val get_case_scheme: theory -> string -> (int * (int * string list)) option val is_undefined: theory -> string -> bool val default_typscheme: theory -> string -> (string * sort) list * typ - - val preprocess_conv: theory -> cterm -> thm - val preprocess_term: theory -> term -> term - val postprocess_conv: theory -> cterm -> thm - val postprocess_term: theory -> term -> term + val assert_eqn: theory -> thm * bool -> thm * bool + val assert_eqns_const: theory -> string + -> (thm * bool) list -> (thm * bool) list val add_attribute: string * attribute parser -> theory -> theory @@ -159,6 +149,8 @@ fun mk_spec ((concluded_history, eqns), (dtyps, cases)) = Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases }; +val empty_spec = + mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty))); fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases }) = mk_spec (f ((concluded_history, eqns), (dtyps, cases))); @@ -167,7 +159,8 @@ let fun merge_eqns ((_, history1), (_, history2)) = let - val raw_history = AList.merge (op =) (K true) (history1, history2) + val raw_history = AList.merge (op = : serial * serial -> bool) + (K true) (history1, history2) val filtered_history = filter_out (fst o snd) raw_history val history = if null filtered_history then raw_history else filtered_history; @@ -179,57 +172,16 @@ in mk_spec ((false, eqns), (dtyps, cases)) end; -(* pre- and postprocessor *) - -datatype thmproc = Thmproc of { - pre: simpset, - post: simpset, - functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list -}; - -fun mk_thmproc ((pre, post), functrans) = - Thmproc { pre = pre, post = post, functrans = functrans }; -fun map_thmproc f (Thmproc { pre, post, functrans }) = - mk_thmproc (f ((pre, post), functrans)); -fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 }, - Thmproc { pre = pre2, post = post2, functrans = functrans2 }) = - let - val pre = Simplifier.merge_ss (pre1, pre2); - val post = Simplifier.merge_ss (post1, post2); - val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2); - in mk_thmproc ((pre, post), functrans) end; - -datatype exec = Exec of { - thmproc: thmproc, - spec: spec -}; - - (* code setup data *) -fun mk_exec (thmproc, spec) = - Exec { thmproc = thmproc, spec = spec }; -fun map_exec f (Exec { thmproc = thmproc, spec = spec }) = - mk_exec (f (thmproc, spec)); -fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 }, - Exec { thmproc = thmproc2, spec = spec2 }) = - let - val thmproc = merge_thmproc (thmproc1, thmproc2); - val spec = merge_spec (spec1, spec2); - in mk_exec (thmproc, spec) end; -val empty_exec = mk_exec (mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []), - mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty)))); - -fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x; -fun the_spec (Exec { spec = Spec x, ...}) = x; +fun the_spec (Spec x) = x; val the_eqns = #eqns o the_spec; val the_dtyps = #dtyps o the_spec; val the_cases = #cases o the_spec; -val map_thmproc = map_exec o apfst o map_thmproc; -val map_concluded_history = map_exec o apsnd o map_spec o apfst o apfst; -val map_eqns = map_exec o apsnd o map_spec o apfst o apsnd; -val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst; -val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd; +val map_concluded_history = map_spec o apfst o apfst; +val map_eqns = map_spec o apfst o apsnd; +val map_dtyps = map_spec o apsnd o apfst; +val map_cases = map_spec o apsnd o apsnd; (* data slots dependent on executable content *) @@ -277,17 +229,17 @@ type data = Object.T Datatab.table; val empty_data = Datatab.empty : data; -structure CodeData = TheoryDataFun +structure Code_Data = TheoryDataFun ( - type T = exec * data ref; - val empty = (empty_exec, ref empty_data); - fun copy (exec, data) = (exec, ref (! data)); + type T = spec * data ref; + val empty = (empty_spec, ref empty_data); + fun copy (spec, data) = (spec, ref (! data)); val extend = copy; - fun merge pp ((exec1, data1), (exec2, data2)) = - (merge_exec (exec1, exec2), ref empty_data); + fun merge pp ((spec1, data1), (spec2, data2)) = + (merge_spec (spec1, spec2), ref empty_data); ); -fun thy_data f thy = f ((snd o CodeData.get) thy); +fun thy_data f thy = f ((snd o Code_Data.get) thy); fun get_ensure_init kind data_ref = case Datatab.lookup (! data_ref) kind @@ -299,7 +251,7 @@ (* access to executable content *) -val the_exec = fst o CodeData.get; +val the_exec = fst o Code_Data.get; fun complete_class_params thy cs = fold (fn c => case AxClass.inst_of_param thy c @@ -307,11 +259,11 @@ | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs []; fun map_exec_purge touched f thy = - CodeData.map (fn (exec, data) => (f exec, ref (case touched + Code_Data.map (fn (exec, data) => (f exec, ref (case touched of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data) | NONE => empty_data))) thy; -val purge_data = (CodeData.map o apsnd) (K (ref empty_data)); +val purge_data = (Code_Data.map o apsnd) (K (ref empty_data)); (* tackling equation history *) @@ -323,21 +275,21 @@ fun continue_history thy = if (#concluded_history o the_spec o the_exec) thy then thy - |> (CodeData.map o apfst o map_concluded_history) (K false) + |> (Code_Data.map o apfst o map_concluded_history) (K false) |> SOME else NONE; fun conclude_history thy = if (#concluded_history o the_spec o the_exec) thy then NONE else thy - |> (CodeData.map o apfst) + |> (Code_Data.map o apfst) ((map_eqns o Symtab.map) (fn ((changed, current), history) => ((false, current), if changed then (serial (), current) :: history else history)) #> map_concluded_history (K true)) |> SOME; -val _ = Context.>> (Context.map_theory (CodeData.init +val _ = Context.>> (Context.map_theory (Code_Data.init #> Theory.at_begin continue_history #> Theory.at_end conclude_history)); @@ -366,9 +318,6 @@ end; (*local*) - -(* print executable content *) - fun print_codesetup thy = let val ctxt = ProofContext.init thy; @@ -390,9 +339,6 @@ :: Pretty.str "of" :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos) ); - val pre = (#pre o the_thmproc) exec; - val post = (#post o the_thmproc) exec; - val functrans = (map fst o #functrans o the_thmproc) exec; val eqns = the_eqns exec |> Symtab.dest |> (map o apfst) (Code_Unit.string_of_const thy) @@ -410,21 +356,6 @@ :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_eqn) eqns ), - Pretty.block [ - Pretty.str "preprocessing simpset:", - Pretty.fbrk, - Simplifier.pretty_ss ctxt pre - ], - Pretty.block [ - Pretty.str "postprocessing simpset:", - Pretty.fbrk, - Simplifier.pretty_ss ctxt post - ], - Pretty.block ( - Pretty.str "function transformers:" - :: Pretty.fbrk - :: (Pretty.fbreaks o map Pretty.str) functrans - ), Pretty.block ( Pretty.str "datatypes:" :: Pretty.fbrk @@ -461,10 +392,6 @@ (** interfaces and attributes **) -fun delete_force msg key xs = - if AList.defined (op =) xs key then AList.delete (op =) key xs - else error ("No such " ^ msg ^ ": " ^ quote key); - fun get_datatype thy tyco = case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) of (_, spec) :: _ => spec @@ -568,26 +495,6 @@ fun add_undefined c thy = (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy; -val map_pre = map_exec_purge NONE o map_thmproc o apfst o apfst; -val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd; - -val add_inline = map_pre o MetaSimplifier.add_simp; -val del_inline = map_pre o MetaSimplifier.del_simp; -val add_post = map_post o MetaSimplifier.add_simp; -val del_post = map_post o MetaSimplifier.del_simp; - -fun add_functrans (name, f) = - (map_exec_purge NONE o map_thmproc o apsnd) - (AList.update (op =) (name, (serial (), f))); - -fun del_functrans name = - (map_exec_purge NONE o map_thmproc o apsnd) - (delete_force "function transformer" name); - -fun simple_functrans f thy eqns = case f thy (map fst eqns) - of SOME thms' => SOME (map (rpair (forall snd eqns)) thms') - | NONE => NONE; - val _ = Context.>> (Context.map_theory (let fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); @@ -600,77 +507,12 @@ TypeInterpretation.init #> add_del_attribute ("", (add_eqn, del_eqn)) #> add_simple_attribute ("nbe", add_nbe_eqn) - #> add_del_attribute ("inline", (add_inline, del_inline)) - #> add_del_attribute ("post", (add_post, del_post)) end)); - -(** post- and preprocessing **) - -local - -fun apply_functrans thy c _ [] = [] - | apply_functrans thy c [] eqns = eqns - | apply_functrans thy c functrans eqns = eqns - |> perhaps (perhaps_loop (perhaps_apply functrans)) - |> assert_eqns_const thy c; - -fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); - -fun term_of_conv thy f = - Thm.cterm_of thy - #> f - #> Thm.prop_of - #> Logic.dest_equals - #> snd; - -fun preprocess thy c eqns = - let - val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy; - val functrans = (map (fn (_, (_, f)) => f thy) o #functrans - o the_thmproc o the_exec) thy; - in - eqns - |> apply_functrans thy c functrans - |> (map o apfst) (Code_Unit.rewrite_eqn pre) - |> (map o apfst) (AxClass.unoverload thy) - |> map (assert_eqn thy) - |> burrow_fst (common_typ_eqns thy) - end; - -in - -fun preprocess_conv thy ct = - let - val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy; - in - ct - |> Simplifier.rewrite pre - |> rhs_conv (AxClass.unoverload_conv thy) - end; - -fun preprocess_term thy = term_of_conv thy (preprocess_conv thy); - -fun postprocess_conv thy ct = - let - val post = (Simplifier.theory_context thy o #post o the_thmproc o the_exec) thy; - in - ct - |> AxClass.overload_conv thy - |> rhs_conv (Simplifier.rewrite post) - end; - -fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); - -fun these_raw_eqns thy c = - get_eqns thy c - |> (map o apfst) (Thm.transfer thy) - |> burrow_fst (common_typ_eqns thy); - fun these_eqns thy c = get_eqns thy c |> (map o apfst) (Thm.transfer thy) - |> preprocess thy c; + |> burrow_fst (common_typ_eqns thy); fun default_typscheme thy c = let @@ -685,8 +527,6 @@ of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm | [] => strip_sorts (the_const_typscheme c) end; -end; (*local*) - end; (*struct*) diff -r fc654c95c29e -r d8a6122affd7 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue May 12 20:07:05 2009 +0200 @@ -881,7 +881,7 @@ (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); val _ = - OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag + OuterSyntax.improper_command "print_codesetup" "print code generator setup" K.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); diff -r fc654c95c29e -r d8a6122affd7 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/Pure/codegen.ML Tue May 12 20:07:05 2009 +0200 @@ -1024,8 +1024,6 @@ val setup = add_codegen "default" default_codegen #> add_tycodegen "default" default_tycodegen - #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute - (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I))) #> add_preprocessor unfold_preprocessor; val _ = diff -r fc654c95c29e -r d8a6122affd7 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Tue May 12 17:32:50 2009 +0100 +++ b/src/Tools/Code_Generator.thy Tue May 12 20:07:05 2009 +0200 @@ -9,7 +9,7 @@ uses "~~/src/Tools/value.ML" "~~/src/Tools/quickcheck.ML" - "~~/src/Tools/code/code_wellsorted.ML" + "~~/src/Tools/code/code_preproc.ML" "~~/src/Tools/code/code_thingol.ML" "~~/src/Tools/code/code_printer.ML" "~~/src/Tools/code/code_target.ML" @@ -19,7 +19,8 @@ begin setup {* - Code_ML.setup + Code_Preproc.setup + #> Code_ML.setup #> Code_Haskell.setup #> Nbe.setup *} diff -r fc654c95c29e -r d8a6122affd7 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/Tools/code/code_ml.ML Tue May 12 20:07:05 2009 +0200 @@ -161,20 +161,21 @@ :: map (pr "|") clauses ) end - | pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\""; + | pr_case is_closure thm vars fxy ((_, []), _) = + (concat o map str) ["raise", "Fail", "\"empty case\""]; fun pr_stmt (MLExc (name, n)) = let val exc_str = (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; in - concat ( - str (if n = 0 then "val" else "fun") - :: (str o deresolve) name - :: map str (replicate n "_") - @ str "=" - :: str "raise" - :: str "(Fail" - @@ str (exc_str ^ ")") + (concat o map str) ( + (if n = 0 then "val" else "fun") + :: deresolve name + :: replicate n "_" + @ "=" + :: "raise" + :: "Fail" + @@ exc_str ) end | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) = @@ -458,7 +459,8 @@ :: map (pr "|") clauses ) end - | pr_case is_closure thm vars fxy ((_, []), _) = str "failwith \"empty case\""; + | pr_case is_closure thm vars fxy ((_, []), _) = + (concat o map str) ["failwith", "\"empty case\""]; fun fish_params vars eqs = let fun fish_param _ (w as SOME _) = w @@ -477,13 +479,13 @@ val exc_str = (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; in - concat ( - str "let" - :: (str o deresolve) name - :: map str (replicate n "_") - @ str "=" - :: str "failwith" - @@ str exc_str + (concat o map str) ( + "let" + :: deresolve name + :: replicate n "_" + @ "=" + :: "failwith" + @@ exc_str ) end | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) = diff -r fc654c95c29e -r d8a6122affd7 src/Tools/code/code_preproc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/code/code_preproc.ML Tue May 12 20:07:05 2009 +0200 @@ -0,0 +1,515 @@ +(* Title: Tools/code/code_preproc.ML + Author: Florian Haftmann, TU Muenchen + +Preprocessing code equations into a well-sorted system +in a graph with explicit dependencies. +*) + +signature CODE_PREPROC = +sig + val map_pre: (simpset -> simpset) -> theory -> theory + val map_post: (simpset -> simpset) -> theory -> theory + val add_inline: thm -> theory -> theory + val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory + val del_functrans: string -> theory -> theory + val simple_functrans: (theory -> thm list -> thm list option) + -> theory -> (thm * bool) list -> (thm * bool) list option + val print_codeproc: theory -> unit + + type code_algebra + type code_graph + val eqns: code_graph -> string -> (thm * bool) list + val typ: code_graph -> string -> (string * sort) list * typ + val all: code_graph -> string list + val pretty: theory -> code_graph -> Pretty.T + val obtain: theory -> string list -> term list -> code_algebra * code_graph + val eval_conv: theory -> (sort -> sort) + -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm + val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) + -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a + + val setup: theory -> theory +end + +structure Code_Preproc : CODE_PREPROC = +struct + +(** preprocessor administration **) + +(* theory data *) + +datatype thmproc = Thmproc of { + pre: simpset, + post: simpset, + functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list +}; + +fun mk_thmproc ((pre, post), functrans) = + Thmproc { pre = pre, post = post, functrans = functrans }; +fun map_thmproc f (Thmproc { pre, post, functrans }) = + mk_thmproc (f ((pre, post), functrans)); +fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 }, + Thmproc { pre = pre2, post = post2, functrans = functrans2 }) = + let + val pre = Simplifier.merge_ss (pre1, pre2); + val post = Simplifier.merge_ss (post1, post2); + val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2); + in mk_thmproc ((pre, post), functrans) end; + +structure Code_Preproc_Data = TheoryDataFun +( + type T = thmproc; + val empty = mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []); + fun copy spec = spec; + val extend = copy; + fun merge pp = merge_thmproc; +); + +fun the_thmproc thy = case Code_Preproc_Data.get thy + of Thmproc x => x; + +fun delete_force msg key xs = + if AList.defined (op =) xs key then AList.delete (op =) key xs + else error ("No such " ^ msg ^ ": " ^ quote key); + +fun map_data f thy = + thy + |> Code.purge_data + |> (Code_Preproc_Data.map o map_thmproc) f; + +val map_pre = map_data o apfst o apfst; +val map_post = map_data o apfst o apsnd; + +val add_inline = map_pre o MetaSimplifier.add_simp; +val del_inline = map_pre o MetaSimplifier.del_simp; +val add_post = map_post o MetaSimplifier.add_simp; +val del_post = map_post o MetaSimplifier.del_simp; + +fun add_functrans (name, f) = (map_data o apsnd) + (AList.update (op =) (name, (serial (), f))); + +fun del_functrans name = (map_data o apsnd) + (delete_force "function transformer" name); + + +(* post- and preprocessing *) + +fun apply_functrans thy c _ [] = [] + | apply_functrans thy c [] eqns = eqns + | apply_functrans thy c functrans eqns = eqns + |> perhaps (perhaps_loop (perhaps_apply functrans)) + |> Code.assert_eqns_const thy c; + +fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); + +fun term_of_conv thy f = + Thm.cterm_of thy + #> f + #> Thm.prop_of + #> Logic.dest_equals + #> snd; + +fun preprocess thy c eqns = + let + val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy; + val functrans = (map (fn (_, (_, f)) => f thy) o #functrans + o the_thmproc) thy; + in + eqns + |> apply_functrans thy c functrans + |> (map o apfst) (Code_Unit.rewrite_eqn pre) + |> (map o apfst) (AxClass.unoverload thy) + |> map (Code.assert_eqn thy) + |> burrow_fst (Code_Unit.norm_args thy) + |> burrow_fst (Code_Unit.norm_varnames thy) + end; + +fun preprocess_conv thy ct = + let + val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy; + in + ct + |> Simplifier.rewrite pre + |> rhs_conv (AxClass.unoverload_conv thy) + end; + +fun postprocess_conv thy ct = + let + val post = (Simplifier.theory_context thy o #post o the_thmproc) thy; + in + ct + |> AxClass.overload_conv thy + |> rhs_conv (Simplifier.rewrite post) + end; + +fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); + +fun print_codeproc thy = + let + val ctxt = ProofContext.init thy; + val pre = (#pre o the_thmproc) thy; + val post = (#post o the_thmproc) thy; + val functrans = (map fst o #functrans o the_thmproc) thy; + in + (Pretty.writeln o Pretty.chunks) [ + Pretty.block [ + Pretty.str "preprocessing simpset:", + Pretty.fbrk, + Simplifier.pretty_ss ctxt pre + ], + Pretty.block [ + Pretty.str "postprocessing simpset:", + Pretty.fbrk, + Simplifier.pretty_ss ctxt post + ], + Pretty.block ( + Pretty.str "function transformers:" + :: Pretty.fbrk + :: (Pretty.fbreaks o map Pretty.str) functrans + ) + ] + end; + +fun simple_functrans f thy eqns = case f thy (map fst eqns) + of SOME thms' => SOME (map (rpair (forall snd eqns)) thms') + | NONE => NONE; + + +(** sort algebra and code equation graph types **) + +type code_algebra = (sort -> sort) * Sorts.algebra; +type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T; + +fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr); +fun typ eqngr = fst o Graph.get_node eqngr; +fun all eqngr = Graph.keys eqngr; + +fun pretty thy eqngr = + AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) + |> (map o apfst) (Code_Unit.string_of_const thy) + |> sort (string_ord o pairself fst) + |> map (fn (s, thms) => + (Pretty.block o Pretty.fbreaks) ( + Pretty.str s + :: map (Display.pretty_thm o fst) thms + )) + |> Pretty.chunks; + + +(** the Waisenhaus algorithm **) + +(* auxiliary *) + +fun is_proper_class thy = can (AxClass.get_info thy); + +fun complete_proper_sort thy = + Sign.complete_sort thy #> filter (is_proper_class thy); + +fun inst_params thy tyco = + map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) + o maps (#params o AxClass.get_info thy); + +fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) + (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) + (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); + +fun tyscm_rhss_of thy c eqns = + let + val tyscm = case eqns of [] => Code.default_typscheme thy c + | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm; + val rhss = consts_of thy eqns; + in (tyscm, rhss) end; + + +(* data structures *) + +datatype const = Fun of string | Inst of class * string; + +fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2) + | const_ord (Inst class_tyco1, Inst class_tyco2) = + prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2) + | const_ord (Fun _, Inst _) = LESS + | const_ord (Inst _, Fun _) = GREATER; + +type var = const * int; + +structure Vargraph = + GraphFun(type key = var val ord = prod_ord const_ord int_ord); + +datatype styp = Tyco of string * styp list | Var of var | Free; + +fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys) + | styp_of c_lhs (TFree (v, _)) = case c_lhs + of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs) + | NONE => Free; + +type vardeps_data = ((string * styp list) list * class list) Vargraph.T + * (((string * sort) list * (thm * bool) list) Symtab.table + * (class * string) list); + +val empty_vardeps_data : vardeps_data = + (Vargraph.empty, (Symtab.empty, [])); + + +(* retrieving equations and instances from the background context *) + +fun obtain_eqns thy eqngr c = + case try (Graph.get_node eqngr) c + of SOME ((lhs, _), eqns) => ((lhs, []), []) + | NONE => let + val eqns = Code.these_eqns thy c + |> preprocess thy c; + val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns; + in ((lhs, rhss), eqns) end; + +fun obtain_instance thy arities (inst as (class, tyco)) = + case AList.lookup (op =) arities inst + of SOME classess => (classess, ([], [])) + | NONE => let + val all_classes = complete_proper_sort thy [class]; + val superclasses = remove (op =) class all_classes + val classess = map (complete_proper_sort thy) + (Sign.arity_sorts thy tyco [class]); + val inst_params = inst_params thy tyco all_classes; + in (classess, (superclasses, inst_params)) end; + + +(* computing instantiations *) + +fun add_classes thy arities eqngr c_k new_classes vardeps_data = + let + val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k; + val diff_classes = new_classes |> subtract (op =) old_classes; + in if null diff_classes then vardeps_data + else let + val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k; + in + vardeps_data + |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes) + |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps + |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks + end end +and add_styp thy arities eqngr c_k tyco_styps vardeps_data = + let + val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k; + in if member (op =) old_styps tyco_styps then vardeps_data + else + vardeps_data + |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps) + |> fold (ensure_typmatch_inst thy arities eqngr tyco_styps) classes + end +and add_dep thy arities eqngr c_k c_k' vardeps_data = + let + val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k; + in + vardeps_data + |> add_classes thy arities eqngr c_k' classes + |> apfst (Vargraph.add_edge (c_k, c_k')) + end +and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data = + if can (Sign.arity_sorts thy tyco) [class] + then vardeps_data + |> ensure_inst thy arities eqngr (class, tyco) + |> fold_index (fn (k, styp) => + ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps + else vardeps_data (*permissive!*) +and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) = + if member (op =) insts inst then vardeps_data + else let + val (classess, (superclasses, inst_params)) = + obtain_instance thy arities inst; + in + vardeps_data + |> (apsnd o apsnd) (insert (op =) inst) + |> fold_index (fn (k, _) => + apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess + |> fold (fn superclass => ensure_inst thy arities eqngr (superclass, tyco)) superclasses + |> fold (ensure_fun thy arities eqngr) inst_params + |> fold_index (fn (k, classes) => + add_classes thy arities eqngr (Inst (class, tyco), k) classes + #> fold (fn superclass => + add_dep thy arities eqngr (Inst (superclass, tyco), k) + (Inst (class, tyco), k)) superclasses + #> fold (fn inst_param => + add_dep thy arities eqngr (Fun inst_param, k) + (Inst (class, tyco), k) + ) inst_params + ) classess + end +and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data = + vardeps_data + |> add_styp thy arities eqngr c_k tyco_styps + | ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data = + vardeps_data + |> add_dep thy arities eqngr c_k c_k' + | ensure_typmatch thy arities eqngr Free c_k vardeps_data = + vardeps_data +and ensure_rhs thy arities eqngr (c', styps) vardeps_data = + vardeps_data + |> ensure_fun thy arities eqngr c' + |> fold_index (fn (k, styp) => + ensure_typmatch thy arities eqngr styp (Fun c', k)) styps +and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) = + if Symtab.defined eqntab c then vardeps_data + else let + val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c; + val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss; + in + vardeps_data + |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns))) + |> fold_index (fn (k, _) => + apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs + |> fold_index (fn (k, (_, sort)) => + add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs + |> fold (ensure_rhs thy arities eqngr) rhss' + end; + + +(* applying instantiations *) + +fun dicts_of thy (proj_sort, algebra) (T, sort) = + let + fun class_relation (x, _) _ = x; + fun type_constructor tyco xs class = + inst_params thy tyco (Sorts.complete_sort algebra [class]) + @ (maps o maps) fst xs; + fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort); + in + flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra + { class_relation = class_relation, type_constructor = type_constructor, + type_variable = type_variable } (T, proj_sort sort) + handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) + end; + +fun add_arity thy vardeps (class, tyco) = + AList.default (op =) + ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) + (0 upto Sign.arity_number thy tyco - 1)); + +fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) = + if can (Graph.get_node eqngr) c then (rhss, eqngr) + else let + val lhs = map_index (fn (k, (v, _)) => + (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; + val inst_tab = Vartab.empty |> fold (fn (v, sort) => + Vartab.update ((v, 0), sort)) lhs; + val eqns = proto_eqns + |> (map o apfst) (Code_Unit.inst_thm thy inst_tab); + val (tyscm, rhss') = tyscm_rhss_of thy c eqns; + val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; + in (map (pair c) rhss' @ rhss, eqngr') end; + +fun extend_arities_eqngr thy cs ts (arities, eqngr) = + let + val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) => + insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts []; + val (vardeps, (eqntab, insts)) = empty_vardeps_data + |> fold (ensure_fun thy arities eqngr) cs + |> fold (ensure_rhs thy arities eqngr) cs_rhss; + val arities' = fold (add_arity thy vardeps) insts arities; + val pp = Syntax.pp_global thy; + val algebra = Sorts.subalgebra pp (is_proper_class thy) + (AList.lookup (op =) arities') (Sign.classes_of thy); + val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr); + fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra) + (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c); + val eqngr'' = fold (fn (c, rhs) => fold + (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr'; + in (algebra, (arities', eqngr'')) end; + + +(** store for preprocessed arities and code equations **) + +structure Wellsorted = CodeDataFun +( + type T = ((string * class) * sort list) list * code_graph; + val empty = ([], Graph.empty); + fun purge thy cs (arities, eqngr) = + let + val del_cs = ((Graph.all_preds eqngr + o filter (can (Graph.get_node eqngr))) cs); + val del_arities = del_cs + |> map_filter (AxClass.inst_of_param thy) + |> maps (fn (c, tyco) => + (map (rpair tyco) o Sign.complete_sort thy o the_list + o AxClass.class_of_param thy) c); + val arities' = fold (AList.delete (op =)) del_arities arities; + val eqngr' = Graph.del_nodes del_cs eqngr; + in (arities', eqngr') end; +); + + +(** retrieval and evaluation interfaces **) + +fun obtain thy cs ts = apsnd snd + (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); + +fun prepare_sorts_typ prep_sort + = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort)); + +fun prepare_sorts prep_sort (Const (c, ty)) = + Const (c, prepare_sorts_typ prep_sort ty) + | prepare_sorts prep_sort (t1 $ t2) = + prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2 + | prepare_sorts prep_sort (Abs (v, ty, t)) = + Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t) + | prepare_sorts _ (t as Bound _) = t; + +fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct = + let + val pp = Syntax.pp_global thy; + val ct = cterm_of proto_ct; + val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) + (Thm.term_of ct); + val thm = preprocess_conv thy ct; + val ct' = Thm.rhs_of thm; + val t' = Thm.term_of ct'; + val vs = Term.add_tfrees t' []; + val consts = fold_aterms + (fn Const (c, _) => insert (op =) c | _ => I) t' []; + + val t'' = prepare_sorts prep_sort t'; + val (algebra', eqngr') = obtain thy consts [t'']; + in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end; + +fun simple_evaluator evaluator algebra eqngr vs t ct = + evaluator algebra eqngr vs t; + +fun eval_conv thy = + let + fun conclude_evaluation thm2 thm1 = + let + val thm3 = postprocess_conv thy (Thm.rhs_of thm2); + in + Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => + error ("could not construct evaluation proof:\n" + ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) + end; + in gen_eval thy I conclude_evaluation end; + +fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy) + (K o postproc (postprocess_term thy)) prep_sort (simple_evaluator evaluator); + + +(** setup **) + +val setup = + let + fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); + fun add_del_attribute (name, (add, del)) = + Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) + || Scan.succeed (mk_attribute add)) + in + add_del_attribute ("inline", (add_inline, del_inline)) + #> add_del_attribute ("post", (add_post, del_post)) + #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute + (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I))) + end; + +val _ = + OuterSyntax.improper_command "print_codeproc" "print code preprocessor setup" + OuterKeyword.diag (Scan.succeed + (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep + (print_codeproc o Toplevel.theory_of))); + +end; (*struct*) diff -r fc654c95c29e -r d8a6122affd7 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Tue May 12 17:32:50 2009 +0100 +++ b/src/Tools/code/code_thingol.ML Tue May 12 20:07:05 2009 +0200 @@ -509,7 +509,7 @@ of SOME tyco => stmt_datatypecons tyco | NONE => (case AxClass.class_of_param thy c of SOME class => stmt_classparam class - | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c)) + | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c)) in ensure_stmt lookup_const (declare_const thy) stmt_const c end and ensure_class thy (algbr as (_, algebra)) funcgr class = let @@ -603,7 +603,7 @@ and translate_const thy algbr funcgr thm (c, ty) = let val tys = Sign.const_typargs thy (c, ty); - val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c; + val sorts = (map snd o fst o Code_Preproc.typ funcgr) c; val tys_args = (fst o Term.strip_type) ty; in ensure_const thy algbr funcgr c @@ -748,7 +748,7 @@ fun generate_consts thy algebra funcgr = fold_map (ensure_const thy algebra funcgr); in - invoke_generation thy (Code_Wellsorted.obtain thy cs []) generate_consts cs + invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs |-> project_consts end; @@ -788,8 +788,8 @@ val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; in evaluator naming program ((vs'', (vs', ty')), t') deps end; -fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy; -fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy; +fun eval_conv thy prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy; +fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy; (** diagnostic commands **) @@ -817,7 +817,7 @@ fun code_depgr thy consts = let - val (_, eqngr) = Code_Wellsorted.obtain thy consts []; + val (_, eqngr) = Code_Preproc.obtain thy consts []; val select = Graph.all_succs eqngr consts; in eqngr @@ -825,7 +825,7 @@ |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy)) end; -fun code_thms thy = Pretty.writeln o Code_Wellsorted.pretty thy o code_depgr thy; +fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy; fun code_deps thy consts = let diff -r fc654c95c29e -r d8a6122affd7 src/Tools/code/code_wellsorted.ML --- a/src/Tools/code/code_wellsorted.ML Tue May 12 17:32:50 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,342 +0,0 @@ -(* Title: Tools/code/code_wellsorted.ML - Author: Florian Haftmann, TU Muenchen - -Producing well-sorted systems of code equations in a graph -with explicit dependencies -- the Waisenhaus algorithm. -*) - -signature CODE_WELLSORTED = -sig - type code_algebra - type code_graph - val eqns: code_graph -> string -> (thm * bool) list - val typ: code_graph -> string -> (string * sort) list * typ - val all: code_graph -> string list - val pretty: theory -> code_graph -> Pretty.T - val obtain: theory -> string list -> term list -> code_algebra * code_graph - val eval_conv: theory -> (sort -> sort) - -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm - val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) - -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a -end - -structure Code_Wellsorted : CODE_WELLSORTED = -struct - -(** the algebra and code equation graph types **) - -type code_algebra = (sort -> sort) * Sorts.algebra; -type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T; - -fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr); -fun typ eqngr = fst o Graph.get_node eqngr; -fun all eqngr = Graph.keys eqngr; - -fun pretty thy eqngr = - AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) - |> (map o apfst) (Code_Unit.string_of_const thy) - |> sort (string_ord o pairself fst) - |> map (fn (s, thms) => - (Pretty.block o Pretty.fbreaks) ( - Pretty.str s - :: map (Display.pretty_thm o fst) thms - )) - |> Pretty.chunks; - - -(** the Waisenhaus algorithm **) - -(* auxiliary *) - -fun is_proper_class thy = can (AxClass.get_info thy); - -fun complete_proper_sort thy = - Sign.complete_sort thy #> filter (is_proper_class thy); - -fun inst_params thy tyco = - map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) - o maps (#params o AxClass.get_info thy); - -fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) - (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) - (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); - -fun tyscm_rhss_of thy c eqns = - let - val tyscm = case eqns of [] => Code.default_typscheme thy c - | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm; - val rhss = consts_of thy eqns; - in (tyscm, rhss) end; - - -(* data structures *) - -datatype const = Fun of string | Inst of class * string; - -fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2) - | const_ord (Inst class_tyco1, Inst class_tyco2) = - prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2) - | const_ord (Fun _, Inst _) = LESS - | const_ord (Inst _, Fun _) = GREATER; - -type var = const * int; - -structure Vargraph = - GraphFun(type key = var val ord = prod_ord const_ord int_ord); - -datatype styp = Tyco of string * styp list | Var of var | Free; - -fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys) - | styp_of c_lhs (TFree (v, _)) = case c_lhs - of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs) - | NONE => Free; - -type vardeps_data = ((string * styp list) list * class list) Vargraph.T - * (((string * sort) list * (thm * bool) list) Symtab.table - * (class * string) list); - -val empty_vardeps_data : vardeps_data = - (Vargraph.empty, (Symtab.empty, [])); - - -(* retrieving equations and instances from the background context *) - -fun obtain_eqns thy eqngr c = - case try (Graph.get_node eqngr) c - of SOME ((lhs, _), eqns) => ((lhs, []), []) - | NONE => let - val eqns = Code.these_eqns thy c - |> burrow_fst (Code_Unit.norm_args thy) - |> burrow_fst (Code_Unit.norm_varnames thy); - val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns; - in ((lhs, rhss), eqns) end; - -fun obtain_instance thy arities (inst as (class, tyco)) = - case AList.lookup (op =) arities inst - of SOME classess => (classess, ([], [])) - | NONE => let - val all_classes = complete_proper_sort thy [class]; - val superclasses = remove (op =) class all_classes - val classess = map (complete_proper_sort thy) - (Sign.arity_sorts thy tyco [class]); - val inst_params = inst_params thy tyco all_classes; - in (classess, (superclasses, inst_params)) end; - - -(* computing instantiations *) - -fun add_classes thy arities eqngr c_k new_classes vardeps_data = - let - val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k; - val diff_classes = new_classes |> subtract (op =) old_classes; - in if null diff_classes then vardeps_data - else let - val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k; - in - vardeps_data - |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes) - |> fold (fn styp => fold (assert_typmatch_inst thy arities eqngr styp) new_classes) styps - |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks - end end -and add_styp thy arities eqngr c_k tyco_styps vardeps_data = - let - val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k; - in if member (op =) old_styps tyco_styps then vardeps_data - else - vardeps_data - |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps) - |> fold (assert_typmatch_inst thy arities eqngr tyco_styps) classes - end -and add_dep thy arities eqngr c_k c_k' vardeps_data = - let - val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k; - in - vardeps_data - |> add_classes thy arities eqngr c_k' classes - |> apfst (Vargraph.add_edge (c_k, c_k')) - end -and assert_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data = - if can (Sign.arity_sorts thy tyco) [class] - then vardeps_data - |> assert_inst thy arities eqngr (class, tyco) - |> fold_index (fn (k, styp) => - assert_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps - else vardeps_data (*permissive!*) -and assert_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) = - if member (op =) insts inst then vardeps_data - else let - val (classess, (superclasses, inst_params)) = - obtain_instance thy arities inst; - in - vardeps_data - |> (apsnd o apsnd) (insert (op =) inst) - |> fold_index (fn (k, _) => - apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess - |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses - |> fold (assert_fun thy arities eqngr) inst_params - |> fold_index (fn (k, classes) => - add_classes thy arities eqngr (Inst (class, tyco), k) classes - #> fold (fn superclass => - add_dep thy arities eqngr (Inst (superclass, tyco), k) - (Inst (class, tyco), k)) superclasses - #> fold (fn inst_param => - add_dep thy arities eqngr (Fun inst_param, k) - (Inst (class, tyco), k) - ) inst_params - ) classess - end -and assert_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data = - vardeps_data - |> add_styp thy arities eqngr c_k tyco_styps - | assert_typmatch thy arities eqngr (Var c_k') c_k vardeps_data = - vardeps_data - |> add_dep thy arities eqngr c_k c_k' - | assert_typmatch thy arities eqngr Free c_k vardeps_data = - vardeps_data -and assert_rhs thy arities eqngr (c', styps) vardeps_data = - vardeps_data - |> assert_fun thy arities eqngr c' - |> fold_index (fn (k, styp) => - assert_typmatch thy arities eqngr styp (Fun c', k)) styps -and assert_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) = - if Symtab.defined eqntab c then vardeps_data - else let - val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c; - val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss; - in - vardeps_data - |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns))) - |> fold_index (fn (k, _) => - apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs - |> fold_index (fn (k, (_, sort)) => - add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs - |> fold (assert_rhs thy arities eqngr) rhss' - end; - - -(* applying instantiations *) - -fun dicts_of thy (proj_sort, algebra) (T, sort) = - let - fun class_relation (x, _) _ = x; - fun type_constructor tyco xs class = - inst_params thy tyco (Sorts.complete_sort algebra [class]) - @ (maps o maps) fst xs; - fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort); - in - flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra - { class_relation = class_relation, type_constructor = type_constructor, - type_variable = type_variable } (T, proj_sort sort) - handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) - end; - -fun add_arity thy vardeps (class, tyco) = - AList.default (op =) - ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) - (0 upto Sign.arity_number thy tyco - 1)); - -fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) = - if can (Graph.get_node eqngr) c then (rhss, eqngr) - else let - val lhs = map_index (fn (k, (v, _)) => - (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; - val inst_tab = Vartab.empty |> fold (fn (v, sort) => - Vartab.update ((v, 0), sort)) lhs; - val eqns = proto_eqns - |> (map o apfst) (Code_Unit.inst_thm thy inst_tab); - val (tyscm, rhss') = tyscm_rhss_of thy c eqns; - val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; - in (map (pair c) rhss' @ rhss, eqngr') end; - -fun extend_arities_eqngr thy cs ts (arities, eqngr) = - let - val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) => - insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts []; - val (vardeps, (eqntab, insts)) = empty_vardeps_data - |> fold (assert_fun thy arities eqngr) cs - |> fold (assert_rhs thy arities eqngr) cs_rhss; - val arities' = fold (add_arity thy vardeps) insts arities; - val pp = Syntax.pp_global thy; - val algebra = Sorts.subalgebra pp (is_proper_class thy) - (AList.lookup (op =) arities') (Sign.classes_of thy); - val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr); - fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra) - (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c); - val eqngr'' = fold (fn (c, rhs) => fold - (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr'; - in (algebra, (arities', eqngr'')) end; - - -(** store **) - -structure Wellsorted = CodeDataFun -( - type T = ((string * class) * sort list) list * code_graph; - val empty = ([], Graph.empty); - fun purge thy cs (arities, eqngr) = - let - val del_cs = ((Graph.all_preds eqngr - o filter (can (Graph.get_node eqngr))) cs); - val del_arities = del_cs - |> map_filter (AxClass.inst_of_param thy) - |> maps (fn (c, tyco) => - (map (rpair tyco) o Sign.complete_sort thy o the_list - o AxClass.class_of_param thy) c); - val arities' = fold (AList.delete (op =)) del_arities arities; - val eqngr' = Graph.del_nodes del_cs eqngr; - in (arities', eqngr') end; -); - - -(** retrieval interfaces **) - -fun obtain thy cs ts = apsnd snd - (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); - -fun prepare_sorts_typ prep_sort - = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort)); - -fun prepare_sorts prep_sort (Const (c, ty)) = - Const (c, prepare_sorts_typ prep_sort ty) - | prepare_sorts prep_sort (t1 $ t2) = - prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2 - | prepare_sorts prep_sort (Abs (v, ty, t)) = - Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t) - | prepare_sorts _ (t as Bound _) = t; - -fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct = - let - val pp = Syntax.pp_global thy; - val ct = cterm_of proto_ct; - val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) - (Thm.term_of ct); - val thm = Code.preprocess_conv thy ct; - val ct' = Thm.rhs_of thm; - val t' = Thm.term_of ct'; - val vs = Term.add_tfrees t' []; - val consts = fold_aterms - (fn Const (c, _) => insert (op =) c | _ => I) t' []; - - val t'' = prepare_sorts prep_sort t'; - val (algebra', eqngr') = obtain thy consts [t'']; - in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end; - -fun simple_evaluator evaluator algebra eqngr vs t ct = - evaluator algebra eqngr vs t; - -fun eval_conv thy = - let - fun conclude_evaluation thm2 thm1 = - let - val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2); - in - Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => - error ("could not construct evaluation proof:\n" - ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) - end; - in gen_eval thy I conclude_evaluation end; - -fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy) - (K o postproc (Code.postprocess_term thy)) prep_sort (simple_evaluator evaluator); - -end; (*struct*)