1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 30 10:48:09 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 30 10:48:11 2010 +0200
1.3 @@ -9,6 +9,7 @@
1.4 datatype prolog_system = SWI_PROLOG | YAP
1.5 type code_options =
1.6 {ensure_groundness : bool,
1.7 + limit_globally : int option,
1.8 limited_types : (typ * int) list,
1.9 limited_predicates : (string list * int) list,
1.10 replacing : ((string * string) * string) list,
1.11 @@ -58,38 +59,45 @@
1.12
1.13 type code_options =
1.14 {ensure_groundness : bool,
1.15 + limit_globally : int option,
1.16 limited_types : (typ * int) list,
1.17 limited_predicates : (string list * int) list,
1.18 replacing : ((string * string) * string) list,
1.19 manual_reorder : ((string * int) * int list) list}
1.20
1.21
1.22 -fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates,
1.23 +fun set_ensure_groundness {ensure_groundness, limit_globally, limited_types, limited_predicates,
1.24 replacing, manual_reorder} =
1.25 - {ensure_groundness = true, limited_types = limited_types,
1.26 + {ensure_groundness = true, limit_globally = limit_globally, limited_types = limited_types,
1.27 limited_predicates = limited_predicates, replacing = replacing,
1.28 manual_reorder = manual_reorder}
1.29
1.30 -fun map_limit_predicates f {ensure_groundness, limited_types, limited_predicates,
1.31 +fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates,
1.32 replacing, manual_reorder} =
1.33 - {ensure_groundness = ensure_groundness, limited_types = limited_types,
1.34 + {ensure_groundness = ensure_groundness, limit_globally = limit_globally, limited_types = limited_types,
1.35 limited_predicates = f limited_predicates, replacing = replacing,
1.36 manual_reorder = manual_reorder}
1.37 -
1.38 +
1.39 +fun merge_global_limit (NONE, NONE) = NONE
1.40 + | merge_global_limit (NONE, SOME n) = SOME n
1.41 + | merge_global_limit (SOME n, NONE) = SOME n
1.42 + | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
1.43 +
1.44 structure Options = Theory_Data
1.45 (
1.46 type T = code_options
1.47 - val empty = {ensure_groundness = false,
1.48 + val empty = {ensure_groundness = false, limit_globally = NONE,
1.49 limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []}
1.50 val extend = I;
1.51 fun merge
1.52 - ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
1.53 - limited_predicates = limited_predicates1, replacing = replacing1,
1.54 - manual_reorder = manual_reorder1},
1.55 - {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
1.56 - limited_predicates = limited_predicates2, replacing = replacing2,
1.57 - manual_reorder = manual_reorder2}) =
1.58 + ({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1,
1.59 + limited_types = limited_types1, limited_predicates = limited_predicates1,
1.60 + replacing = replacing1, manual_reorder = manual_reorder1},
1.61 + {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
1.62 + limited_types = limited_types2, limited_predicates = limited_predicates2,
1.63 + replacing = replacing2, manual_reorder = manual_reorder2}) =
1.64 {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
1.65 + limit_globally = merge_global_limit (limit_globally1, limit_globally2),
1.66 limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
1.67 limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
1.68 manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
1.69 @@ -188,7 +196,7 @@
1.70 type clause = ((string * prol_term list) * prem);
1.71
1.72 type logic_program = clause list;
1.73 -
1.74 +
1.75 (* translation from introduction rules to internal representation *)
1.76
1.77 fun mk_conform f empty avoid name =
1.78 @@ -591,13 +599,14 @@
1.79 ((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
1.80 end
1.81
1.82 -fun add_limited_predicates limited_predicates =
1.83 +fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
1.84 +
1.85 +fun add_limited_predicates limited_predicates (p, constant_table) =
1.86 let
1.87 - fun add (rel_names, limit) (p, constant_table) =
1.88 + fun add (rel_names, limit) p =
1.89 let
1.90 val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
1.91 val clauses' = map (mk_depth_limited rel_names) clauses
1.92 - fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
1.93 fun mk_entry_clause rel_name =
1.94 let
1.95 val nargs = length (snd (fst
1.96 @@ -606,9 +615,9 @@
1.97 in
1.98 (("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
1.99 end
1.100 - in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
1.101 + in (p @ (map mk_entry_clause rel_names) @ clauses') end
1.102 in
1.103 - fold add limited_predicates
1.104 + (fold add limited_predicates p, constant_table)
1.105 end
1.106
1.107
1.108 @@ -663,10 +672,29 @@
1.109
1.110 val rename_vars_program = map rename_vars_clause
1.111
1.112 +(* limit computation globally by some threshold *)
1.113 +
1.114 +fun limit_globally ctxt limit const_name (p, constant_table) =
1.115 + let
1.116 + val rel_names = fold (fn ((r, _), _) => insert (op =) r) p []
1.117 + val p' = map (mk_depth_limited rel_names) p
1.118 + val rel_name = translate_const constant_table const_name
1.119 + val nargs = length (snd (fst
1.120 + (the (find_first (fn ((rel, _), _) => rel = rel_name) p))))
1.121 + val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
1.122 + val entry_clause = ((rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
1.123 + val p'' = filter_out (fn ((rel, _), _) => rel = rel_name) p
1.124 + in
1.125 + (entry_clause :: p' @ p'', constant_table)
1.126 + end
1.127 +
1.128 (* post processing of generated prolog program *)
1.129
1.130 -fun post_process ctxt options (p, constant_table) =
1.131 +fun post_process ctxt options const_name (p, constant_table) =
1.132 (p, constant_table)
1.133 + |> (case #limit_globally options of
1.134 + SOME limit => limit_globally ctxt limit const_name
1.135 + | NONE => I)
1.136 |> (if #ensure_groundness options then
1.137 add_ground_predicates ctxt (#limited_types options)
1.138 else I)
1.139 @@ -915,7 +943,7 @@
1.140 val ctxt' = ProofContext.init_global thy'
1.141 val _ = tracing "Generating prolog program..."
1.142 val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
1.143 - |> post_process ctxt' options
1.144 + |> post_process ctxt' options name
1.145 val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
1.146 val args' = map (translate_term ctxt constant_table') all_args
1.147 val _ = tracing "Running prolog program..."
1.148 @@ -991,7 +1019,7 @@
1.149 val ctxt' = ProofContext.init_global thy3
1.150 val _ = tracing "Generating prolog program..."
1.151 val (p, constant_table) = generate (NONE, true) ctxt' full_constname
1.152 - |> post_process ctxt' (set_ensure_groundness options)
1.153 + |> post_process ctxt' (set_ensure_groundness options) full_constname
1.154 val _ = tracing "Running prolog program..."
1.155 val system_config = System_Config.get (Context.Proof ctxt)
1.156 val tss = run (#timeout system_config, #prolog_system system_config)