# HG changeset patch # User bulwahn # Date 1283257839 -7200 # Node ID 363bfb2459179b624c029b5e6fc2944cc6e3fb2e # Parent 706ab66e3464f736b12ee35890a67f616e1b18ab adding manual reordering of premises to prolog generation diff -r 706ab66e3464 -r 363bfb245917 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 12:15:50 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 14:30:39 2010 +0200 @@ -12,6 +12,7 @@ limited_types : (typ * int) list, limited_predicates : (string list * int) list, replacing : ((string * string) * string) list, + manual_reorder : ((string * int) * int list) list, prolog_system : prolog_system} val code_options_of : theory -> code_options val map_code_options : (code_options -> code_options) -> theory -> theory @@ -58,23 +59,27 @@ limited_types : (typ * int) list, limited_predicates : (string list * int) list, replacing : ((string * string) * string) list, + manual_reorder : ((string * int) * int list) list, prolog_system : prolog_system} structure Options = Theory_Data ( type T = code_options val empty = {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], + limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [], prolog_system = SWI_PROLOG} val extend = I; fun merge ({ensure_groundness = ensure_groundness1, limited_types = limited_types1, - limited_predicates = limited_predicates1, replacing = replacing1, prolog_system = prolog_system1}, + limited_predicates = limited_predicates1, replacing = replacing1, + manual_reorder = manual_reorder1, prolog_system = prolog_system1}, {ensure_groundness = ensure_groundness2, limited_types = limited_types2, - limited_predicates = limited_predicates2, replacing = replacing2, prolog_system = prolog_system2}) = + limited_predicates = limited_predicates2, replacing = replacing2, + manual_reorder = manual_reorder2, prolog_system = prolog_system2}) = {ensure_groundness = ensure_groundness1 orelse ensure_groundness2, limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2), limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2), + manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2), replacing = Library.merge (op =) (replacing1, replacing2), prolog_system = prolog_system1}; ); @@ -449,7 +454,23 @@ map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p end + +(* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *) +fun reorder_manually reorder p = + let + fun reorder' (clause as ((rel, args), prem)) seen = + let + val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen + val i = the (AList.lookup (op =) seen' rel) + val perm = AList.lookup (op =) reorder (rel, i) + val prem' = (case perm of + SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem) + | NONE => prem) + in (((rel, args), prem'), seen') end + in + fst (fold_map reorder' p []) + end (* rename variables to prolog-friendly names *) fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) @@ -697,6 +718,7 @@ else I) |> add_limited_predicates (#limited_predicates options) |> apfst (fold replace (#replacing options)) + |> apfst (reorder_manually (#manual_reorder options)) val _ = tracing "Running prolog program..." val tss = run (#prolog_system options) p (translate_const constant_table name) (map first_upper vnames) soln @@ -791,7 +813,8 @@ val (p, constant_table) = generate true ctxt' full_constname |> add_ground_predicates ctxt' (#limited_types options) |> add_limited_predicates (#limited_predicates options) - |> apfst (fold replace (#replacing options)) + |> apfst (fold replace (#replacing options)) + |> apfst (reorder_manually (#manual_reorder options)) val _ = tracing "Running prolog program..." val [ts] = run (#prolog_system options) p (translate_const constant_table full_constname) (map fst vs') (SOME 1)