--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 10:56:46 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 10:57:32 2010 +0200
@@ -6,7 +6,9 @@
signature CODE_PROLOG =
sig
- type code_options = {ensure_groundness : bool}
+ datatype prolog_system = SWI_PROLOG | YAP
+ type code_options =
+ {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
val options : code_options ref
datatype arith_op = Plus | Minus
@@ -21,10 +23,10 @@
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
type constant_table = (string * string) list
-
- val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
+
+ val generate : bool -> Proof.context -> string -> (logic_program * constant_table)
val write_program : logic_program -> string
- val run : logic_program -> string -> string list -> int option -> prol_term list list
+ val run : prolog_system -> logic_program -> string -> string list -> int option -> prol_term list list
val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
@@ -42,9 +44,13 @@
(* code generation options *)
-type code_options = {ensure_groundness : bool}
+datatype prolog_system = SWI_PROLOG | YAP
-val options = Unsynchronized.ref {ensure_groundness = false};
+type code_options =
+ {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
+
+val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
+ prolog_system = SWI_PROLOG};
(* general string functions *)
@@ -190,10 +196,10 @@
fun mk_groundness_prems t = map Ground (Term.add_frees t [])
-fun translate_prem options ctxt constant_table t =
+fun translate_prem ensure_groundness ctxt constant_table t =
case try HOLogic.dest_not t of
SOME t =>
- if #ensure_groundness options then
+ if ensure_groundness then
Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
else
NegRel_of (translate_literal ctxt constant_table t)
@@ -215,7 +221,7 @@
(Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
(Thm.transfer thy rule)
-fun translate_intros options ctxt gr const constant_table =
+fun translate_intros ensure_groundness ctxt gr const constant_table =
let
val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
@@ -225,33 +231,11 @@
let
val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
- val prems' = Conj (map (translate_prem options ctxt' constant_table') prems)
+ val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
in (map translate_intro intros', constant_table') end
-val preprocess_options = Predicate_Compile_Aux.Options {
- expected_modes = NONE,
- proposed_modes = NONE,
- proposed_names = [],
- show_steps = false,
- show_intermediate_results = false,
- show_proof_trace = false,
- show_modes = false,
- show_mode_inference = false,
- show_compilation = false,
- show_caught_failures = false,
- skip_proof = true,
- no_topmost_reordering = false,
- function_flattening = true,
- specialise = false,
- fail_safe_function_flattening = false,
- no_higher_order_predicate = [],
- inductify = false,
- detect_switches = true,
- compilation = Predicate_Compile_Aux.Pred
-}
-
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -272,7 +256,7 @@
fst (extend' key (G, []))
end
-fun generate options ctxt const =
+fun generate ensure_groundness ctxt const =
let
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -281,10 +265,11 @@
val scc = strong_conn_of gr' [const]
val constant_table = mk_constant_table (flat scc)
in
- apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
+ apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
end
-(* add implementation for ground predicates *)
+(* implementation for fully enumerating predicates and
+ for size-limited predicates for enumerating the values of a datatype upto a specific size *)
fun add_ground_typ (Conj prems) = fold add_ground_typ prems
| add_ground_typ (Ground (_, T)) = insert (op =) T
@@ -294,34 +279,58 @@
first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
| mk_relname _ = raise Fail "unexpected type"
+fun mk_lim_relname T = "lim_" ^ mk_relname T
+
(* This is copied from "pat_completeness.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
map (fn (Cn,CT) =>
Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
(the (Datatype.get_constrs thy name))
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
+
+fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
-fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) =
+fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
if member (op =) seen T then ([], (seen, constant_table))
else
let
- val rel_name = mk_relname T
- fun mk_impl (Const (constr_name, T)) (seen, constant_table) =
+ val (limited, size) = case AList.lookup (op =) limited_types T of
+ SOME s => (true, s)
+ | NONE => (false, 0)
+ val rel_name = (if limited then mk_lim_relname else mk_relname) T
+ fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) =
let
val constant_table' = declare_consts [constr_name] constant_table
+ val Ts = binder_types cT
val (rec_clauses, (seen', constant_table'')) =
- fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table')
- val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T)))
- fun mk_prem v T = Rel (mk_relname T, [v])
+ fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table')
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts))
+ val lim_var =
+ if limited then
+ if recursive then [AppF ("suc", [Var "Lim"])]
+ else [Var "Lim"]
+ else []
+ fun mk_prem v T' =
+ if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v])
+ else Rel (mk_relname T', [v])
val clause =
- ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
- Conj (map2 mk_prem vars (binder_types T)))
+ ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
+ Conj (map2 mk_prem vars Ts))
in
(clause :: flat rec_clauses, (seen', constant_table''))
end
val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
- in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end
- | mk_ground_impl ctxt T (seen, constant_table) =
+ val constrs' = (constrs ~~ map (is_recursive_constr T) constrs)
+ |> (fn cs => filter_out snd cs @ filter snd cs)
+ val (clauses, constant_table') =
+ apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table))
+ val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero")
+ in
+ ((if limited then
+ cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"]))
+ else I) clauses, constant_table')
+ end
+ | mk_ground_impl ctxt _ T (seen, constant_table) =
raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T)
fun replace_ground (Conj prems) = Conj (map replace_ground prems)
@@ -329,15 +338,16 @@
Rel (mk_relname T, [Var x])
| replace_ground p = p
-fun add_ground_predicates ctxt (p, constant_table) =
+fun add_ground_predicates ctxt limited_types (p, constant_table) =
let
val ground_typs = fold (add_ground_typ o snd) p []
- val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table)
+ val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
val p' = map (apsnd replace_ground) p
in
((flat grs) @ p', constant_table')
end
-
+
+
(* rename variables to prolog-friendly names *)
fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
@@ -396,14 +406,16 @@
fun write_program p =
cat_lines (map write_clause p)
-(** query templates **)
+(* query templates *)
-fun query_first rel vnames =
+(** query and prelude for swi-prolog **)
+
+fun swi_prolog_query_first rel vnames =
"eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
"\\n', [" ^ space_implode ", " vnames ^ "]).\n"
-fun query_firstn n rel vnames =
+fun swi_prolog_query_firstn n rel vnames =
"eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
"writelist([]).\n" ^
@@ -411,7 +423,7 @@
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
"\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
-val prelude =
+val swi_prolog_prelude =
"#!/usr/bin/swipl -q -t main -f\n\n" ^
":- use_module(library('dialect/ciao/aggregates')).\n" ^
":- style_check(-singleton).\n" ^
@@ -420,7 +432,38 @@
"main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
"main :- halt(1).\n"
+(** query and prelude for yap **)
+
+fun yap_query_first rel vnames =
+ "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
+ "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^
+ "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
+
+val yap_prelude =
+ "#!/usr/bin/yap -L\n\n" ^
+ ":- initialization(eval).\n"
+
+(* system-dependent query, prelude and invocation *)
+
+fun query system nsols =
+ case system of
+ SWI_PROLOG =>
+ (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n)
+ | YAP =>
+ case nsols of NONE => yap_query_first | SOME n =>
+ error "No support for querying multiple solutions in the prolog system yap"
+
+fun prelude system =
+ case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
+
+fun invoke system file_name =
+ let
+ val cmd =
+ case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
+ in bash_output (cmd ^ file_name) end
+
(* parsing prolog solution *)
+
val scan_number =
Scan.many1 Symbol.is_ascii_digit
@@ -471,26 +514,25 @@
(* calling external interpreter and getting results *)
-fun run p query_rel vnames nsols =
+fun run system p query_rel vnames nsols =
let
val cmd = Path.named_root
- val query = case nsols of NONE => query_first | SOME n => query_firstn n
val p' = rename_vars_program p
val _ = tracing "Renaming variable names..."
val renaming = fold mk_renaming vnames []
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
- val prog = prelude ^ query query_rel vnames' ^ write_program p'
+ val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
val _ = tracing ("Generated prolog program:\n" ^ prog)
val prolog_file = File.tmp_path (Path.basic "prolog_file")
val _ = File.write prolog_file prog
- val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
+ val (solution, _) = invoke system (File.shell_path prolog_file)
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
tss
end
-(* values command *)
+(* restoring types in terms *)
fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
| restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
@@ -509,6 +551,30 @@
map (restore_term ctxt constant_table) (args ~~ argsT'))
end
+(* values command *)
+
+val preprocess_options = Predicate_Compile_Aux.Options {
+ expected_modes = NONE,
+ proposed_modes = NONE,
+ proposed_names = [],
+ show_steps = false,
+ show_intermediate_results = false,
+ show_proof_trace = false,
+ show_modes = false,
+ show_mode_inference = false,
+ show_compilation = false,
+ show_caught_failures = false,
+ skip_proof = true,
+ no_topmost_reordering = false,
+ function_flattening = true,
+ specialise = false,
+ fail_safe_function_flattening = false,
+ no_higher_order_predicate = [],
+ inductify = false,
+ detect_switches = true,
+ compilation = Predicate_Compile_Aux.Pred
+}
+
fun values ctxt soln t_compr =
let
val options = !options
@@ -534,10 +600,13 @@
val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
val ctxt'' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
- val (p, constant_table) = generate options ctxt'' name
- |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I)
+ val (p, constant_table) = generate (#ensure_groundness options) ctxt'' name
+ |> (if #ensure_groundness options then
+ add_ground_predicates ctxt'' (#limited_types options)
+ else I)
val _ = tracing "Running prolog program..."
- val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
+ val tss = run (#prolog_system options)
+ p (translate_const constant_table name) (map first_upper vnames) soln
val _ = tracing "Restoring terms..."
val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
fun mk_insert x S =
@@ -626,11 +695,11 @@
val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
val ctxt'' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
- val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname
- |> add_ground_predicates ctxt''
+ val (p, constant_table) = generate true ctxt'' full_constname
+ |> add_ground_predicates ctxt'' (#limited_types (!options))
val _ = tracing "Running prolog program..."
- val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
- (SOME 1)
+ val [ts] = run (#prolog_system (!options))
+ p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
val empty_report = ([], false)