# HG changeset patch # User bulwahn # Date 1282894446 -7200 # Node ID 970508a5119f666d9d6046d6edf8d0cef9357dbe # Parent 4a4be1be0faebcf31591b4a05ff2cc11dc0c6c51 added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory diff -r 4a4be1be0fae -r 970508a5119f src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- 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 \ B \ 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}" diff -r 4a4be1be0fae -r 970508a5119f src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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)