--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Aug 26 14:48:48 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Aug 27 09:34:06 2010 +0200
@@ -4,13 +4,24 @@
section {* Example append *}
+
inductive append
where
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+
+values "{(x, y, z). append x y z}"
+
values 3 "{(x, y, z). append x y z}"
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
+
+values "{(x, y, z). append x y z}"
+
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+
section {* Example queens *}
@@ -172,7 +183,7 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = []} *}
+ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
values 2 "{y. notB y}"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 14:48:48 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 09:34:06 2010 +0200
@@ -6,7 +6,9 @@
signature CODE_PROLOG =
sig
- type code_options = {ensure_groundness : bool, limited_types : (typ * int) list}
+ 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, limited_types : (typ * int) list}
+datatype prolog_system = SWI_PROLOG | YAP
-val options = Unsynchronized.ref {ensure_groundness = false, limited_types = []};
+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,7 +231,7 @@
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
@@ -250,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)
@@ -259,7 +265,7 @@
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
(* implementation for fully enumerating predicates and
@@ -402,12 +408,14 @@
(* 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" ^
@@ -415,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" ^
@@ -424,6 +432,36 @@
"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 =
@@ -476,19 +514,18 @@
(* 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
@@ -563,12 +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
+ 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 =
@@ -657,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, limited_types = []} ctxt'' full_constname
+ 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)