# HG changeset patch # User haftmann # Date 1282899452 -7200 # Node ID c421cfe2eadae8c2731cddd33d753fe06f26d007 # Parent eba0175d4cd1735762abe0ad4f2cca9abddb9f84# Parent 848be46708dc2e5a0f519f8f6801c57bbf6a0838 merged diff -r 848be46708dc -r c421cfe2eada src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Aug 27 10:56:46 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Aug 27 10:57:32 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} *} +ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *} values 2 "{y. notB y}" @@ -187,7 +198,7 @@ inductive equals :: "abc => abc => bool" where "equals y' y'" -ML {* set Code_Prolog.trace *} + values 1 "{(y, z). equals y z}" end diff -r 848be46708dc -r c421cfe2eada src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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)