bulwahn@38073: (* Title: HOL/Tools/Predicate_Compile/code_prolog.ML bulwahn@38073: Author: Lukas Bulwahn, TU Muenchen bulwahn@38073: bulwahn@38073: Prototype of an code generator for logic programming languages (a.k.a. Prolog) bulwahn@38073: *) bulwahn@38073: bulwahn@38073: signature CODE_PROLOG = bulwahn@38073: sig bulwahn@38792: datatype prolog_system = SWI_PROLOG | YAP bulwahn@38792: type code_options = bulwahn@38947: {ensure_groundness : bool, bulwahn@38947: limited_types : (typ * int) list, bulwahn@38959: limited_predicates : (string list * int) list, bulwahn@38947: replacing : ((string * string) * string) list, bulwahn@39461: manual_reorder : ((string * int) * int list) list} bulwahn@39461: val set_ensure_groundness : code_options -> code_options bulwahn@39461: val map_limit_predicates : ((string list * int) list -> (string list * int) list) bulwahn@39461: -> code_options -> code_options bulwahn@38950: val code_options_of : theory -> code_options bulwahn@38950: val map_code_options : (code_options -> code_options) -> theory -> theory bulwahn@39461: bulwahn@38113: datatype arith_op = Plus | Minus bulwahn@38112: datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list bulwahn@38113: | Number of int | ArithOp of arith_op * prol_term list; bulwahn@38113: datatype prem = Conj of prem list bulwahn@38113: | Rel of string * prol_term list | NotRel of string * prol_term list bulwahn@38113: | Eq of prol_term * prol_term | NotEq of prol_term * prol_term bulwahn@38727: | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term bulwahn@38727: | Ground of string * typ; bulwahn@38727: bulwahn@38079: type clause = ((string * prol_term list) * prem); bulwahn@38073: type logic_program = clause list; bulwahn@38079: type constant_table = (string * string) list bulwahn@39461: bulwahn@39461: val generate : Predicate_Compile_Aux.mode option * bool -> bulwahn@39461: Proof.context -> string -> (logic_program * constant_table) bulwahn@38079: val write_program : logic_program -> string bulwahn@39187: val run : (Time.time * prolog_system) -> logic_program -> string -> string list -> int option -> prol_term list list bulwahn@39461: bulwahn@39461: val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool) bulwahn@38733: bulwahn@38079: val trace : bool Unsynchronized.ref bulwahn@38947: bulwahn@38947: val replace : ((string * string) * string) -> logic_program -> logic_program bulwahn@38073: end; bulwahn@38073: bulwahn@38073: structure Code_Prolog : CODE_PROLOG = bulwahn@38073: struct bulwahn@38073: bulwahn@38079: (* diagnostic tracing *) bulwahn@38079: bulwahn@38079: val trace = Unsynchronized.ref false bulwahn@38079: bulwahn@38079: fun tracing s = if !trace then Output.tracing s else () bulwahn@38727: bulwahn@38727: (* code generation options *) bulwahn@38727: bulwahn@38727: bulwahn@38792: type code_options = bulwahn@38947: {ensure_groundness : bool, bulwahn@38947: limited_types : (typ * int) list, bulwahn@38959: limited_predicates : (string list * int) list, bulwahn@38947: replacing : ((string * string) * string) list, bulwahn@39461: manual_reorder : ((string * int) * int list) list} bulwahn@39461: bulwahn@38792: bulwahn@39461: fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates, bulwahn@39461: replacing, manual_reorder} = bulwahn@39461: {ensure_groundness = true, limited_types = limited_types, bulwahn@39461: limited_predicates = limited_predicates, replacing = replacing, bulwahn@39461: manual_reorder = manual_reorder} bulwahn@39461: bulwahn@39461: fun map_limit_predicates f {ensure_groundness, limited_types, limited_predicates, bulwahn@39461: replacing, manual_reorder} = bulwahn@39461: {ensure_groundness = ensure_groundness, limited_types = limited_types, bulwahn@39461: limited_predicates = f limited_predicates, replacing = replacing, bulwahn@39461: manual_reorder = manual_reorder} bulwahn@39461: bulwahn@38950: structure Options = Theory_Data bulwahn@38950: ( bulwahn@38950: type T = code_options bulwahn@38950: val empty = {ensure_groundness = false, bulwahn@39461: limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []} bulwahn@38950: val extend = I; bulwahn@38950: fun merge bulwahn@38950: ({ensure_groundness = ensure_groundness1, limited_types = limited_types1, bulwahn@38960: limited_predicates = limited_predicates1, replacing = replacing1, bulwahn@39461: manual_reorder = manual_reorder1}, bulwahn@38950: {ensure_groundness = ensure_groundness2, limited_types = limited_types2, bulwahn@38960: limited_predicates = limited_predicates2, replacing = replacing2, bulwahn@39461: manual_reorder = manual_reorder2}) = bulwahn@38950: {ensure_groundness = ensure_groundness1 orelse ensure_groundness2, bulwahn@38950: limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2), bulwahn@38950: limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2), bulwahn@38960: manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2), bulwahn@39461: replacing = Library.merge (op =) (replacing1, replacing2)}; bulwahn@38950: ); bulwahn@38950: bulwahn@38950: val code_options_of = Options.get bulwahn@38950: bulwahn@38950: val map_code_options = Options.map bulwahn@38727: bulwahn@39461: (* system configuration *) bulwahn@39461: bulwahn@39461: datatype prolog_system = SWI_PROLOG | YAP bulwahn@39461: bulwahn@39462: fun string_of_system SWI_PROLOG = "swiprolog" bulwahn@39462: | string_of_system YAP = "yap" bulwahn@39462: bulwahn@39461: type system_configuration = {timeout : Time.time, prolog_system : prolog_system} bulwahn@39462: bulwahn@39461: structure System_Config = Generic_Data bulwahn@39461: ( bulwahn@39461: type T = system_configuration bulwahn@39461: val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG} bulwahn@39461: val extend = I; bulwahn@39461: fun merge ({timeout = timeout1, prolog_system = prolog_system1}, bulwahn@39461: {timeout = timeout2, prolog_system = prolog_system2}) = bulwahn@39461: {timeout = timeout1, prolog_system = prolog_system1} bulwahn@39461: ) bulwahn@39461: bulwahn@38073: (* general string functions *) bulwahn@38073: bulwahn@38073: val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; bulwahn@38073: val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; bulwahn@38073: bulwahn@38073: (* internal program representation *) bulwahn@38073: bulwahn@38113: datatype arith_op = Plus | Minus bulwahn@38113: bulwahn@38112: datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list bulwahn@38113: | Number of int | ArithOp of arith_op * prol_term list; bulwahn@38113: bulwahn@38735: fun dest_Var (Var v) = v bulwahn@38735: bulwahn@38735: fun add_vars (Var v) = insert (op =) v bulwahn@38735: | add_vars (ArithOp (_, ts)) = fold add_vars ts bulwahn@38735: | add_vars (AppF (_, ts)) = fold add_vars ts bulwahn@38735: | add_vars _ = I bulwahn@38735: bulwahn@38735: fun map_vars f (Var v) = Var (f v) bulwahn@38735: | map_vars f (ArithOp (opr, ts)) = ArithOp (opr, map (map_vars f) ts) bulwahn@38735: | map_vars f (AppF (fs, ts)) = AppF (fs, map (map_vars f) ts) bulwahn@38735: | map_vars f t = t bulwahn@38735: bulwahn@38728: fun maybe_AppF (c, []) = Cons c bulwahn@38728: | maybe_AppF (c, xs) = AppF (c, xs) bulwahn@38728: bulwahn@38113: fun is_Var (Var _) = true bulwahn@38113: | is_Var _ = false bulwahn@38113: bulwahn@38113: fun is_arith_term (Var _) = true bulwahn@38113: | is_arith_term (Number _) = true bulwahn@38113: | is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands bulwahn@38113: | is_arith_term _ = false bulwahn@38073: bulwahn@38081: fun string_of_prol_term (Var s) = "Var " ^ s bulwahn@38075: | string_of_prol_term (Cons s) = "Cons " ^ s bulwahn@38075: | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" bulwahn@38112: | string_of_prol_term (Number n) = "Number " ^ string_of_int n bulwahn@38075: bulwahn@38113: datatype prem = Conj of prem list bulwahn@38113: | Rel of string * prol_term list | NotRel of string * prol_term list bulwahn@38113: | Eq of prol_term * prol_term | NotEq of prol_term * prol_term bulwahn@38727: | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term bulwahn@38727: | Ground of string * typ; bulwahn@38735: bulwahn@38073: fun dest_Rel (Rel (c, ts)) = (c, ts) bulwahn@38735: bulwahn@38735: fun map_term_prem f (Conj prems) = Conj (map (map_term_prem f) prems) bulwahn@38735: | map_term_prem f (Rel (r, ts)) = Rel (r, map f ts) bulwahn@38735: | map_term_prem f (NotRel (r, ts)) = NotRel (r, map f ts) bulwahn@38735: | map_term_prem f (Eq (l, r)) = Eq (f l, f r) bulwahn@38735: | map_term_prem f (NotEq (l, r)) = NotEq (f l, f r) bulwahn@38735: | map_term_prem f (ArithEq (l, r)) = ArithEq (f l, f r) bulwahn@38735: | map_term_prem f (NotArithEq (l, r)) = NotArithEq (f l, f r) bulwahn@38735: | map_term_prem f (Ground (v, T)) = Ground (dest_Var (f (Var v)), T) bulwahn@38735: bulwahn@38735: fun fold_prem_terms f (Conj prems) = fold (fold_prem_terms f) prems bulwahn@38735: | fold_prem_terms f (Rel (_, ts)) = fold f ts bulwahn@38735: | fold_prem_terms f (NotRel (_, ts)) = fold f ts bulwahn@38735: | fold_prem_terms f (Eq (l, r)) = f l #> f r bulwahn@38735: | fold_prem_terms f (NotEq (l, r)) = f l #> f r bulwahn@38735: | fold_prem_terms f (ArithEq (l, r)) = f l #> f r bulwahn@38735: | fold_prem_terms f (NotArithEq (l, r)) = f l #> f r bulwahn@38735: | fold_prem_terms f (Ground (v, T)) = f (Var v) bulwahn@38735: bulwahn@38079: type clause = ((string * prol_term list) * prem); bulwahn@38073: bulwahn@38073: type logic_program = clause list; bulwahn@38073: bulwahn@38073: (* translation from introduction rules to internal representation *) bulwahn@38073: bulwahn@38958: fun mk_conform f empty avoid name = bulwahn@38956: let bulwahn@38956: fun dest_Char (Symbol.Char c) = c bulwahn@38956: val name' = space_implode "" (map (dest_Char o Symbol.decode) bulwahn@38956: (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) bulwahn@38956: (Symbol.explode name))) bulwahn@38958: val name'' = f (if name' = "" then empty else name') bulwahn@38958: in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end bulwahn@38956: bulwahn@38079: (** constant table **) bulwahn@38079: bulwahn@38079: type constant_table = (string * string) list bulwahn@38079: bulwahn@38079: fun declare_consts consts constant_table = bulwahn@38956: let bulwahn@38956: fun update' c table = bulwahn@38956: if AList.defined (op =) table c then table else bulwahn@38956: let bulwahn@38958: val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c) bulwahn@38956: in bulwahn@38956: AList.update (op =) (c, c') table bulwahn@38956: end bulwahn@38956: in bulwahn@38956: fold update' consts constant_table bulwahn@38956: end bulwahn@38079: bulwahn@38079: fun translate_const constant_table c = bulwahn@38079: case AList.lookup (op =) constant_table c of bulwahn@38079: SOME c' => c' bulwahn@38079: | NONE => error ("No such constant: " ^ c) bulwahn@38073: bulwahn@38079: fun inv_lookup _ [] _ = NONE bulwahn@38079: | inv_lookup eq ((key, value)::xs) value' = bulwahn@38079: if eq (value', value) then SOME key bulwahn@38079: else inv_lookup eq xs value'; bulwahn@38079: bulwahn@38079: fun restore_const constant_table c = bulwahn@38079: case inv_lookup (op =) constant_table c of bulwahn@38079: SOME c' => c' bulwahn@38079: | NONE => error ("No constant corresponding to " ^ c) bulwahn@38727: bulwahn@38079: (** translation of terms, literals, premises, and clauses **) bulwahn@38079: bulwahn@38113: fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus bulwahn@38113: | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus bulwahn@38113: | translate_arith_const _ = NONE bulwahn@38113: bulwahn@38734: fun mk_nat_term constant_table n = bulwahn@38734: let bulwahn@38734: val zero = translate_const constant_table @{const_name "Groups.zero_class.zero"} bulwahn@38734: val Suc = translate_const constant_table @{const_name "Suc"} bulwahn@38734: in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end bulwahn@38734: bulwahn@38079: fun translate_term ctxt constant_table t = bulwahn@38112: case try HOLogic.dest_number t of bulwahn@38112: SOME (@{typ "int"}, n) => Number n bulwahn@38734: | SOME (@{typ "nat"}, n) => mk_nat_term constant_table n bulwahn@38112: | NONE => bulwahn@38112: (case strip_comb t of bulwahn@38112: (Free (v, T), []) => Var v bulwahn@38112: | (Const (c, _), []) => Cons (translate_const constant_table c) bulwahn@38112: | (Const (c, _), args) => bulwahn@38113: (case translate_arith_const c of bulwahn@38113: SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args) bulwahn@38113: | NONE => bulwahn@38113: AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)) bulwahn@38112: | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)) bulwahn@38073: bulwahn@38079: fun translate_literal ctxt constant_table t = bulwahn@38073: case strip_comb t of haftmann@38864: (Const (@{const_name HOL.eq}, _), [l, r]) => bulwahn@38113: let bulwahn@38113: val l' = translate_term ctxt constant_table l bulwahn@38113: val r' = translate_term ctxt constant_table r bulwahn@38113: in bulwahn@38728: (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r') bulwahn@38113: end bulwahn@38079: | (Const (c, _), args) => bulwahn@38079: Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args) bulwahn@38073: | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t) bulwahn@38073: bulwahn@38073: fun NegRel_of (Rel lit) = NotRel lit bulwahn@38073: | NegRel_of (Eq eq) = NotEq eq bulwahn@38113: | NegRel_of (ArithEq eq) = NotArithEq eq bulwahn@38113: bulwahn@38727: fun mk_groundness_prems t = map Ground (Term.add_frees t []) bulwahn@38727: bulwahn@38792: fun translate_prem ensure_groundness ctxt constant_table t = bulwahn@38073: case try HOLogic.dest_not t of bulwahn@38727: SOME t => bulwahn@38792: if ensure_groundness then bulwahn@38727: Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)]) bulwahn@38727: else bulwahn@38727: NegRel_of (translate_literal ctxt constant_table t) bulwahn@38079: | NONE => translate_literal ctxt constant_table t bulwahn@38114: bulwahn@38114: fun imp_prems_conv cv ct = bulwahn@38114: case Thm.term_of ct of bulwahn@38114: Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct bulwahn@38114: | _ => Conv.all_conv ct bulwahn@38114: bulwahn@38114: fun Trueprop_conv cv ct = bulwahn@38114: case Thm.term_of ct of haftmann@38558: Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct bulwahn@38114: | _ => raise Fail "Trueprop_conv" bulwahn@38114: bulwahn@38114: fun preprocess_intro thy rule = bulwahn@38114: Conv.fconv_rule bulwahn@38114: (imp_prems_conv bulwahn@38114: (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq})))) bulwahn@38114: (Thm.transfer thy rule) bulwahn@38114: bulwahn@38792: fun translate_intros ensure_groundness ctxt gr const constant_table = bulwahn@38073: let bulwahn@38114: val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const) bulwahn@38073: val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt bulwahn@38079: val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table bulwahn@38073: fun translate_intro intro = bulwahn@38073: let bulwahn@38073: val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro) bulwahn@38727: val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro) bulwahn@38792: val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems) bulwahn@38079: val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems') bulwahn@38073: in clause end bulwahn@38958: val res = (map translate_intro intros', constant_table') bulwahn@38958: in res end bulwahn@38073: bulwahn@38731: fun depending_preds_of (key, intros) = bulwahn@38731: fold Term.add_const_names (map Thm.prop_of intros) [] bulwahn@38731: bulwahn@38731: fun add_edges edges_of key G = bulwahn@38731: let bulwahn@38731: fun extend' key (G, visited) = bulwahn@38731: case try (Graph.get_node G) key of bulwahn@38731: SOME v => bulwahn@38731: let bulwahn@38731: val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v)) bulwahn@38731: val (G', visited') = fold extend' bulwahn@38731: (subtract (op =) (key :: visited) new_edges) (G, key :: visited) bulwahn@38731: in bulwahn@38731: (fold (Graph.add_edge o (pair key)) new_edges G', visited') bulwahn@38731: end bulwahn@38731: | NONE => (G, visited) bulwahn@38731: in bulwahn@38731: fst (extend' key (G, [])) bulwahn@38731: end bulwahn@38731: bulwahn@39183: fun print_intros ctxt gr consts = bulwahn@39183: tracing (cat_lines (map (fn const => bulwahn@39183: "Constant " ^ const ^ "has intros:\n" ^ bulwahn@39183: cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts)) bulwahn@39461: bulwahn@39461: (* translation of moded predicates *) bulwahn@39461: bulwahn@39461: (** generating graph of moded predicates **) bulwahn@39461: bulwahn@39461: (* could be moved to Predicate_Compile_Core *) bulwahn@39461: fun requires_modes polarity cls = bulwahn@39461: let bulwahn@39461: fun req_mode_of pol (t, derivation) = bulwahn@39461: (case fst (strip_comb t) of bulwahn@39461: Const (c, _) => SOME (c, (pol, Predicate_Compile_Core.head_mode_of derivation)) bulwahn@39461: | _ => NONE) bulwahn@39461: fun req (Predicate_Compile_Aux.Prem t, derivation) = req_mode_of polarity (t, derivation) bulwahn@39461: | req (Predicate_Compile_Aux.Negprem t, derivation) = req_mode_of (not polarity) (t, derivation) bulwahn@39461: | req _ = NONE bulwahn@39461: in bulwahn@39461: maps (fn (_, prems) => map_filter req prems) cls bulwahn@39461: end bulwahn@39461: bulwahn@39461: structure Mode_Graph = Graph(type key = string * (bool * Predicate_Compile_Aux.mode) bulwahn@39461: val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord)); bulwahn@39461: bulwahn@39461: fun mk_moded_clauses_graph ctxt scc gr = bulwahn@39461: let bulwahn@39461: val options = Predicate_Compile_Aux.default_options bulwahn@39461: val mode_analysis_options = bulwahn@39461: {use_random = true, reorder_premises = true, infer_pos_and_neg_modes = true} bulwahn@39461: fun infer prednames (gr, (pos_modes, neg_modes, random)) = bulwahn@39461: let bulwahn@39461: val (lookup_modes, lookup_neg_modes, needs_random) = bulwahn@39461: ((fn s => the (AList.lookup (op =) pos_modes s)), bulwahn@39461: (fn s => the (AList.lookup (op =) neg_modes s)), bulwahn@39461: (fn s => member (op =) (the (AList.lookup (op =) random s)))) bulwahn@39461: val (preds, all_vs, param_vs, all_modes, clauses) = bulwahn@39461: Predicate_Compile_Core.prepare_intrs options ctxt prednames bulwahn@39461: (maps (Predicate_Compile_Core.intros_of ctxt) prednames) bulwahn@39461: val ((moded_clauses, random'), _) = bulwahn@39461: Predicate_Compile_Core.infer_modes mode_analysis_options options bulwahn@39461: (lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses bulwahn@39461: val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses bulwahn@39461: val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes bulwahn@39461: val neg_modes' = map (apsnd (map_filter (fn (false, m) => SOME m | _ => NONE))) modes bulwahn@39461: val _ = tracing ("Inferred modes:\n" ^ bulwahn@39461: cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map bulwahn@39461: (fn (p, m) => Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes)) bulwahn@39461: val gr' = gr bulwahn@39461: |> fold (fn (p, mps) => fold (fn (mode, cls) => bulwahn@39461: Mode_Graph.new_node ((p, mode), cls)) mps) bulwahn@39461: moded_clauses bulwahn@39461: |> fold (fn (p, mps) => fold (fn (mode, cls) => fold (fn req => bulwahn@39461: Mode_Graph.add_edge ((p, mode), req)) (requires_modes (fst mode) cls)) mps) bulwahn@39461: moded_clauses bulwahn@39461: in bulwahn@39461: (gr', (AList.merge (op =) (op =) (pos_modes, pos_modes'), bulwahn@39461: AList.merge (op =) (op =) (neg_modes, neg_modes'), bulwahn@39461: AList.merge (op =) (op =) (random, random'))) bulwahn@39461: end bulwahn@39461: in bulwahn@39461: fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], []))) bulwahn@39461: end bulwahn@39461: bulwahn@39461: fun declare_moded_predicate moded_preds table = bulwahn@39461: let bulwahn@39461: fun update' (p as (pred, (pol, mode))) table = bulwahn@39461: if AList.defined (op =) table p then table else bulwahn@39461: let bulwahn@39461: val name = Long_Name.base_name pred ^ (if pol then "p" else "n") bulwahn@39461: ^ Predicate_Compile_Aux.ascii_string_of_mode mode bulwahn@39461: val p' = mk_conform first_lower "pred" (map snd table) name bulwahn@39461: in bulwahn@39461: AList.update (op =) (p, p') table bulwahn@39461: end bulwahn@39461: in bulwahn@39461: fold update' moded_preds table bulwahn@39461: end bulwahn@39461: bulwahn@39461: fun mk_program ctxt moded_gr moded_preds (prog, (moded_pred_table, constant_table)) = bulwahn@39461: let bulwahn@39461: val moded_pred_table' = declare_moded_predicate moded_preds moded_pred_table bulwahn@39461: fun mk_literal pol derivation constant_table' t = bulwahn@39461: let bulwahn@39461: val (p, args) = strip_comb t bulwahn@39461: val mode = Predicate_Compile_Core.head_mode_of derivation bulwahn@39461: val name = fst (dest_Const p) bulwahn@39461: bulwahn@39461: val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode))) bulwahn@39461: val args' = map (translate_term ctxt constant_table') args bulwahn@39461: in bulwahn@39461: Rel (p', args') bulwahn@39461: end bulwahn@39461: fun mk_prem pol (indprem, derivation) constant_table = bulwahn@39461: case indprem of bulwahn@39461: Predicate_Compile_Aux.Generator (s, T) => (Ground (s, T), constant_table) bulwahn@39461: | _ => bulwahn@39461: declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) []) constant_table bulwahn@39461: |> (fn constant_table' => bulwahn@39461: (case indprem of Predicate_Compile_Aux.Negprem t => bulwahn@39461: NegRel_of (mk_literal (not pol) derivation constant_table' t) bulwahn@39461: | _ => bulwahn@39461: mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem), constant_table')) bulwahn@39461: fun mk_clause pred_name pol (ts, prems) (prog, constant_table) = bulwahn@39461: let bulwahn@39461: val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table bulwahn@39461: val args = map (translate_term ctxt constant_table') ts bulwahn@39461: val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table' bulwahn@39461: in bulwahn@39461: (((pred_name, args), Conj prems') :: prog, constant_table'') bulwahn@39461: end bulwahn@39461: fun mk_clauses (pred, mode as (pol, _)) = bulwahn@39461: let bulwahn@39461: val clauses = Mode_Graph.get_node moded_gr (pred, mode) bulwahn@39461: val pred_name = the (AList.lookup (op =) moded_pred_table' (pred, mode)) bulwahn@39461: in bulwahn@39461: fold (mk_clause pred_name pol) clauses bulwahn@39461: end bulwahn@39461: in bulwahn@39461: apsnd (pair moded_pred_table') (fold mk_clauses moded_preds (prog, constant_table)) bulwahn@39461: end bulwahn@39461: bulwahn@39461: fun generate (use_modes, ensure_groundness) ctxt const = bulwahn@38073: let bulwahn@38731: fun strong_conn_of gr keys = bulwahn@38073: Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) bulwahn@38732: val gr = Predicate_Compile_Core.intros_graph_of ctxt bulwahn@38731: val gr' = add_edges depending_preds_of const gr bulwahn@38731: val scc = strong_conn_of gr' [const] bulwahn@39461: val initial_constant_table = bulwahn@39461: declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] [] bulwahn@38073: in bulwahn@39461: case use_modes of bulwahn@39461: SOME mode => bulwahn@39461: let bulwahn@39461: val moded_gr = mk_moded_clauses_graph ctxt scc gr bulwahn@39461: val moded_gr' = Mode_Graph.subgraph bulwahn@39461: (member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr bulwahn@39461: val scc = Mode_Graph.strong_conn moded_gr' bulwahn@39461: in bulwahn@39461: apfst rev (apsnd snd bulwahn@39461: (fold (mk_program ctxt moded_gr') (rev scc) ([], ([], initial_constant_table)))) bulwahn@39461: end bulwahn@39461: | NONE => bulwahn@39461: let bulwahn@39461: val _ = print_intros ctxt gr (flat scc) bulwahn@39461: val constant_table = declare_consts (flat scc) initial_constant_table bulwahn@39461: in bulwahn@39461: apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table) bulwahn@39461: end bulwahn@38073: end bulwahn@38727: bulwahn@38789: (* implementation for fully enumerating predicates and bulwahn@38789: for size-limited predicates for enumerating the values of a datatype upto a specific size *) bulwahn@38073: bulwahn@38727: fun add_ground_typ (Conj prems) = fold add_ground_typ prems bulwahn@38727: | add_ground_typ (Ground (_, T)) = insert (op =) T bulwahn@38727: | add_ground_typ _ = I bulwahn@38073: bulwahn@38728: fun mk_relname (Type (Tcon, Targs)) = bulwahn@38728: first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs) bulwahn@38728: | mk_relname _ = raise Fail "unexpected type" bulwahn@38728: bulwahn@38789: fun mk_lim_relname T = "lim_" ^ mk_relname T bulwahn@38789: bulwahn@38728: (* This is copied from "pat_completeness.ML" *) bulwahn@38728: fun inst_constrs_of thy (T as Type (name, _)) = bulwahn@38728: map (fn (Cn,CT) => bulwahn@38728: Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) bulwahn@38728: (the (Datatype.get_constrs thy name)) bulwahn@38728: | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) bulwahn@38789: bulwahn@38789: fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T bulwahn@38728: bulwahn@38789: fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) = bulwahn@38728: if member (op =) seen T then ([], (seen, constant_table)) bulwahn@38728: else bulwahn@38728: let bulwahn@38789: val (limited, size) = case AList.lookup (op =) limited_types T of bulwahn@38789: SOME s => (true, s) bulwahn@38789: | NONE => (false, 0) bulwahn@38789: val rel_name = (if limited then mk_lim_relname else mk_relname) T bulwahn@38789: fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) = bulwahn@38727: let bulwahn@38727: val constant_table' = declare_consts [constr_name] constant_table bulwahn@38789: val Ts = binder_types cT bulwahn@38728: val (rec_clauses, (seen', constant_table'')) = bulwahn@38789: fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table') bulwahn@38789: val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts)) bulwahn@38789: val lim_var = bulwahn@38789: if limited then bulwahn@38789: if recursive then [AppF ("suc", [Var "Lim"])] bulwahn@38789: else [Var "Lim"] bulwahn@38789: else [] bulwahn@38789: fun mk_prem v T' = bulwahn@38789: if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v]) bulwahn@38789: else Rel (mk_relname T', [v]) bulwahn@38728: val clause = bulwahn@38789: ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]), bulwahn@38789: Conj (map2 mk_prem vars Ts)) bulwahn@38727: in bulwahn@38728: (clause :: flat rec_clauses, (seen', constant_table'')) bulwahn@38727: end bulwahn@38728: val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T bulwahn@38789: val constrs' = (constrs ~~ map (is_recursive_constr T) constrs) bulwahn@38789: |> (fn cs => filter_out snd cs @ filter snd cs) bulwahn@38789: val (clauses, constant_table') = bulwahn@38789: apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table)) bulwahn@38789: val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero") bulwahn@38789: in bulwahn@38789: ((if limited then bulwahn@38789: cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"])) bulwahn@38789: else I) clauses, constant_table') bulwahn@38789: end bulwahn@38789: | mk_ground_impl ctxt _ T (seen, constant_table) = bulwahn@38728: raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T) bulwahn@38728: bulwahn@38727: fun replace_ground (Conj prems) = Conj (map replace_ground prems) bulwahn@38728: | replace_ground (Ground (x, T)) = bulwahn@38728: Rel (mk_relname T, [Var x]) bulwahn@38727: | replace_ground p = p bulwahn@38727: bulwahn@38789: fun add_ground_predicates ctxt limited_types (p, constant_table) = bulwahn@38727: let bulwahn@38727: val ground_typs = fold (add_ground_typ o snd) p [] bulwahn@38789: val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table) bulwahn@38727: val p' = map (apsnd replace_ground) p bulwahn@38073: in bulwahn@38727: ((flat grs) @ p', constant_table') bulwahn@38073: end bulwahn@38789: bulwahn@38947: (* make depth-limited version of predicate *) bulwahn@38947: bulwahn@38947: fun mk_lim_rel_name rel_name = "lim_" ^ rel_name bulwahn@38947: bulwahn@38959: fun mk_depth_limited rel_names ((rel_name, ts), prem) = bulwahn@38947: let bulwahn@38947: fun has_positive_recursive_prems (Conj prems) = exists has_positive_recursive_prems prems bulwahn@38959: | has_positive_recursive_prems (Rel (rel, ts)) = member (op =) rel_names rel bulwahn@38947: | has_positive_recursive_prems _ = false bulwahn@38947: fun mk_lim_prem (Conj prems) = Conj (map mk_lim_prem prems) bulwahn@38947: | mk_lim_prem (p as Rel (rel, ts)) = bulwahn@38959: if member (op =) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p bulwahn@38947: | mk_lim_prem p = p bulwahn@38947: in bulwahn@38947: if has_positive_recursive_prems prem then bulwahn@38947: ((mk_lim_rel_name rel_name, (AppF ("suc", [Var "Lim"])) :: ts), mk_lim_prem prem) bulwahn@38947: else bulwahn@38947: ((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem) bulwahn@38947: end bulwahn@38947: bulwahn@38947: fun add_limited_predicates limited_predicates = bulwahn@38956: let bulwahn@38959: fun add (rel_names, limit) (p, constant_table) = bulwahn@38947: let bulwahn@38959: val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p bulwahn@38959: val clauses' = map (mk_depth_limited rel_names) clauses bulwahn@38947: fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero") bulwahn@38959: fun mk_entry_clause rel_name = bulwahn@38959: let bulwahn@38959: val nargs = length (snd (fst bulwahn@38959: (the (find_first (fn ((rel, _), _) => rel = rel_name) clauses)))) bulwahn@38959: val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs) bulwahn@38959: in bulwahn@38959: (("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars)) bulwahn@38959: end bulwahn@38959: in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end bulwahn@38947: in bulwahn@38947: fold add limited_predicates bulwahn@38947: end bulwahn@38947: bulwahn@38947: bulwahn@38947: (* replace predicates in clauses *) bulwahn@38947: bulwahn@38947: (* replace (A, B, C) p = replace A by B in clauses of C *) bulwahn@38947: fun replace ((from, to), location) p = bulwahn@38947: let bulwahn@38947: fun replace_prem (Conj prems) = Conj (map replace_prem prems) bulwahn@38947: | replace_prem (r as Rel (rel, ts)) = bulwahn@38947: if rel = from then Rel (to, ts) else r bulwahn@38947: | replace_prem r = r bulwahn@38947: in bulwahn@38947: map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p bulwahn@38947: end bulwahn@38947: bulwahn@38960: bulwahn@38960: (* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *) bulwahn@38947: bulwahn@38960: fun reorder_manually reorder p = bulwahn@38960: let bulwahn@38960: fun reorder' (clause as ((rel, args), prem)) seen = bulwahn@38960: let bulwahn@38960: val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen bulwahn@38960: val i = the (AList.lookup (op =) seen' rel) bulwahn@38960: val perm = AList.lookup (op =) reorder (rel, i) bulwahn@38960: val prem' = (case perm of bulwahn@38960: SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem) bulwahn@38960: | NONE => prem) bulwahn@38960: in (((rel, args), prem'), seen') end bulwahn@38960: in bulwahn@38960: fst (fold_map reorder' p []) bulwahn@38960: end bulwahn@39462: bulwahn@38735: (* rename variables to prolog-friendly names *) bulwahn@38735: bulwahn@38735: fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) bulwahn@38735: bulwahn@38735: fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming) bulwahn@38735: bulwahn@38735: fun is_prolog_conform v = bulwahn@38735: forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v) bulwahn@38735: bulwahn@38735: fun mk_renaming v renaming = bulwahn@38958: (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming bulwahn@38735: bulwahn@38735: fun rename_vars_clause ((rel, args), prem) = bulwahn@38735: let bulwahn@38735: val vars = fold_prem_terms add_vars prem (fold add_vars args []) bulwahn@38735: val renaming = fold mk_renaming vars [] bulwahn@38735: in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end bulwahn@38735: bulwahn@38735: val rename_vars_program = map rename_vars_clause bulwahn@38956: bulwahn@38073: (* code printer *) bulwahn@38073: bulwahn@38113: fun write_arith_op Plus = "+" bulwahn@38113: | write_arith_op Minus = "-" bulwahn@38113: bulwahn@38735: fun write_term (Var v) = v bulwahn@38079: | write_term (Cons c) = c bulwahn@38113: | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" bulwahn@38113: | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2 bulwahn@38112: | write_term (Number n) = string_of_int n bulwahn@38073: bulwahn@38073: fun write_rel (pred, args) = bulwahn@38073: pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" bulwahn@38073: bulwahn@38073: fun write_prem (Conj prems) = space_implode ", " (map write_prem prems) bulwahn@38073: | write_prem (Rel p) = write_rel p bulwahn@38073: | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")" bulwahn@38073: | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r bulwahn@38073: | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r bulwahn@38113: | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r bulwahn@38113: | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r bulwahn@39461: | write_prem _ = raise Fail "Not a valid prolog premise" bulwahn@38073: bulwahn@38073: fun write_clause (head, prem) = bulwahn@38073: write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".") bulwahn@38073: bulwahn@38073: fun write_program p = bulwahn@38073: cat_lines (map write_clause p) bulwahn@38073: bulwahn@38790: (* query templates *) bulwahn@38078: bulwahn@38792: (** query and prelude for swi-prolog **) bulwahn@38792: bulwahn@38792: fun swi_prolog_query_first rel vnames = bulwahn@38073: "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^ bulwahn@38082: "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ bulwahn@38082: "\\n', [" ^ space_implode ", " vnames ^ "]).\n" bulwahn@38077: bulwahn@38792: fun swi_prolog_query_firstn n rel vnames = bulwahn@38077: "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^ bulwahn@38077: rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^ bulwahn@38077: "writelist([]).\n" ^ bulwahn@38077: "writelist([(" ^ space_implode ", " vnames ^ ")|T]) :- " ^ bulwahn@38079: "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ bulwahn@38079: "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n" bulwahn@38077: bulwahn@38792: val swi_prolog_prelude = bulwahn@38073: "#!/usr/bin/swipl -q -t main -f\n\n" ^ bulwahn@38077: ":- use_module(library('dialect/ciao/aggregates')).\n" ^ bulwahn@38729: ":- style_check(-singleton).\n" ^ bulwahn@38729: ":- style_check(-discontiguous).\n" ^ bulwahn@38729: ":- style_check(-atom).\n\n" ^ bulwahn@38073: "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^ bulwahn@38073: "main :- halt(1).\n" bulwahn@38075: bulwahn@38792: (** query and prelude for yap **) bulwahn@38792: bulwahn@38792: fun yap_query_first rel vnames = bulwahn@38792: "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^ bulwahn@38792: "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^ bulwahn@38792: "\\n', [" ^ space_implode ", " vnames ^ "]).\n" bulwahn@38792: bulwahn@38792: val yap_prelude = bulwahn@38792: "#!/usr/bin/yap -L\n\n" ^ bulwahn@38792: ":- initialization(eval).\n" bulwahn@38792: bulwahn@38792: (* system-dependent query, prelude and invocation *) bulwahn@38792: bulwahn@38792: fun query system nsols = bulwahn@38792: case system of bulwahn@38792: SWI_PROLOG => bulwahn@38792: (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n) bulwahn@38792: | YAP => bulwahn@38792: case nsols of NONE => yap_query_first | SOME n => bulwahn@38792: error "No support for querying multiple solutions in the prolog system yap" bulwahn@38792: bulwahn@38792: fun prelude system = bulwahn@38792: case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude bulwahn@38792: bulwahn@38792: fun invoke system file_name = bulwahn@38792: let bulwahn@39462: val env_var = bulwahn@39462: (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP") bulwahn@39462: val prog = getenv env_var bulwahn@38792: val cmd = bulwahn@39462: case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L " bulwahn@39462: in bulwahn@39462: if prog = "" then bulwahn@39462: (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "") bulwahn@39462: else fst (bash_output (cmd ^ file_name)) bulwahn@39462: end bulwahn@38792: bulwahn@38075: (* parsing prolog solution *) bulwahn@38790: bulwahn@38115: val scan_number = bulwahn@38115: Scan.many1 Symbol.is_ascii_digit bulwahn@38075: bulwahn@38075: val scan_atom = bulwahn@38728: Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) bulwahn@38075: bulwahn@38075: val scan_var = bulwahn@38078: Scan.many1 bulwahn@38078: (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) bulwahn@38075: bulwahn@38076: val scan_ident = bulwahn@38076: Scan.repeat (Scan.one bulwahn@38076: (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)) bulwahn@38076: bulwahn@38075: fun dest_Char (Symbol.Char s) = s bulwahn@38075: bulwahn@38075: val string_of = concat o map (dest_Char o Symbol.decode) bulwahn@38075: bulwahn@38076: val is_atom_ident = forall Symbol.is_ascii_lower bulwahn@38076: bulwahn@38076: val is_var_ident = bulwahn@38076: forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) bulwahn@38078: bulwahn@38115: fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0 bulwahn@38115: bulwahn@38078: fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms) bulwahn@38078: || (scan_term >> single)) xs bulwahn@38078: and scan_term xs = bulwahn@38115: ((scan_number >> (Number o int_of_symbol_list)) bulwahn@38115: || (scan_var >> (Var o string_of)) bulwahn@38078: || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")")) bulwahn@38079: >> (fn (f, ts) => AppF (string_of f, ts))) bulwahn@38078: || (scan_atom >> (Cons o string_of))) xs bulwahn@38079: bulwahn@38075: val parse_term = fst o Scan.finite Symbol.stopper bulwahn@38077: (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term) bulwahn@38075: o explode bulwahn@38075: bulwahn@38079: fun parse_solutions sol = bulwahn@38075: let bulwahn@38077: fun dest_eq s = case space_explode "=" s of bulwahn@38075: (l :: r :: []) => parse_term (unprefix " " r) bulwahn@38078: | _ => raise Fail "unexpected equation in prolog output" bulwahn@38079: fun parse_solution s = map dest_eq (space_explode ";" s) bulwahn@38961: val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s) bulwahn@38075: in bulwahn@38961: map parse_solution sols bulwahn@38075: end bulwahn@38073: bulwahn@38073: (* calling external interpreter and getting results *) bulwahn@38073: bulwahn@39187: fun run (timeout, system) p query_rel vnames nsols = bulwahn@38073: let bulwahn@38735: val p' = rename_vars_program p bulwahn@38735: val _ = tracing "Renaming variable names..." bulwahn@38735: val renaming = fold mk_renaming vnames [] bulwahn@38735: val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames bulwahn@38792: val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p' bulwahn@38079: val _ = tracing ("Generated prolog program:\n" ^ prog) bulwahn@39187: val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file => bulwahn@39187: (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog bulwahn@38079: val _ = tracing ("Prolog returned solution(s):\n" ^ solution) bulwahn@38079: val tss = parse_solutions solution bulwahn@38073: in bulwahn@38079: tss bulwahn@38073: end bulwahn@38073: bulwahn@38790: (* restoring types in terms *) bulwahn@38075: bulwahn@38081: fun restore_term ctxt constant_table (Var s, T) = Free (s, T) bulwahn@38115: | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n bulwahn@38115: | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number") bulwahn@38079: | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T) bulwahn@38079: | restore_term ctxt constant_table (AppF (f, args), T) = bulwahn@38079: let bulwahn@38079: val thy = ProofContext.theory_of ctxt bulwahn@38079: val c = restore_const constant_table f bulwahn@38079: val cT = Sign.the_const_type thy c bulwahn@38079: val (argsT, resT) = strip_type cT bulwahn@38079: val subst = Sign.typ_match thy (resT, T) Vartab.empty bulwahn@38079: val argsT' = map (Envir.subst_type subst) argsT bulwahn@38079: in bulwahn@38079: list_comb (Const (c, Envir.subst_type subst cT), bulwahn@38079: map (restore_term ctxt constant_table) (args ~~ argsT')) bulwahn@38079: end bulwahn@38079: bulwahn@38790: (* values command *) bulwahn@38790: bulwahn@38790: val preprocess_options = Predicate_Compile_Aux.Options { bulwahn@38790: expected_modes = NONE, bulwahn@39383: proposed_modes = [], bulwahn@38790: proposed_names = [], bulwahn@38790: show_steps = false, bulwahn@38790: show_intermediate_results = false, bulwahn@38790: show_proof_trace = false, bulwahn@38790: show_modes = false, bulwahn@38790: show_mode_inference = false, bulwahn@38790: show_compilation = false, bulwahn@38790: show_caught_failures = false, bulwahn@39383: show_invalid_clauses = false, bulwahn@38790: skip_proof = true, bulwahn@38790: no_topmost_reordering = false, bulwahn@38790: function_flattening = true, bulwahn@38790: specialise = false, bulwahn@38790: fail_safe_function_flattening = false, bulwahn@38790: no_higher_order_predicate = [], bulwahn@38790: inductify = false, bulwahn@38790: detect_switches = true, bulwahn@38790: compilation = Predicate_Compile_Aux.Pred bulwahn@38790: } bulwahn@38790: bulwahn@38075: fun values ctxt soln t_compr = bulwahn@38075: let bulwahn@38950: val options = code_options_of (ProofContext.theory_of ctxt) bulwahn@38075: val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t bulwahn@38075: | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); bulwahn@38075: val (body, Ts, fp) = HOLogic.strip_psplits split; bulwahn@38075: val output_names = Name.variant_list (Term.add_free_names body []) bulwahn@38075: (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) bulwahn@38080: val output_frees = rev (map2 (curry Free) output_names Ts) bulwahn@38075: val body = subst_bounds (output_frees, body) bulwahn@38075: val (pred as Const (name, T), all_args) = bulwahn@38075: case strip_comb body of bulwahn@38075: (Const (name, T), all_args) => (Const (name, T), all_args) bulwahn@38075: | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) bulwahn@38075: val vnames = bulwahn@38075: case try (map (fst o dest_Free)) all_args of bulwahn@38075: SOME vs => vs bulwahn@38075: | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args)) bulwahn@38732: val _ = tracing "Preprocessing specification..." bulwahn@38732: val T = Sign.the_const_type (ProofContext.theory_of ctxt) name bulwahn@38732: val t = Const (name, T) wenzelm@38755: val thy' = wenzelm@38755: Theory.copy (ProofContext.theory_of ctxt) wenzelm@38755: |> Predicate_Compile.preprocess preprocess_options t wenzelm@38755: val ctxt' = ProofContext.init_global thy' bulwahn@38079: val _ = tracing "Generating prolog program..." bulwahn@39461: val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *) bulwahn@38789: |> (if #ensure_groundness options then wenzelm@38797: add_ground_predicates ctxt' (#limited_types options) bulwahn@38789: else I) bulwahn@38947: |> add_limited_predicates (#limited_predicates options) bulwahn@38947: |> apfst (fold replace (#replacing options)) bulwahn@38960: |> apfst (reorder_manually (#manual_reorder options)) bulwahn@38079: val _ = tracing "Running prolog program..." bulwahn@39461: val system_config = System_Config.get (Context.Proof ctxt) bulwahn@39461: val tss = run (#timeout system_config, #prolog_system system_config) bulwahn@38792: p (translate_const constant_table name) (map first_upper vnames) soln bulwahn@38079: val _ = tracing "Restoring terms..." bulwahn@38115: val empty = Const("Orderings.bot_class.bot", fastype_of t_compr) bulwahn@38115: fun mk_insert x S = bulwahn@38115: Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S bulwahn@38115: fun mk_set_compr in_insert [] xs = bulwahn@38115: rev ((Free ("...", fastype_of t_compr)) :: bulwahn@38115: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)) bulwahn@38115: | mk_set_compr in_insert (t :: ts) xs = bulwahn@38115: let bulwahn@38115: val frees = Term.add_frees t [] bulwahn@38115: in bulwahn@38115: if null frees then bulwahn@38115: mk_set_compr (t :: in_insert) ts xs bulwahn@38115: else bulwahn@38115: let wenzelm@38755: val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t) bulwahn@38115: val set_compr = bulwahn@38115: HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) bulwahn@38115: frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) bulwahn@38115: in bulwahn@38729: mk_set_compr [] ts bulwahn@38729: (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)) bulwahn@38115: end bulwahn@38115: end bulwahn@38075: in bulwahn@38115: foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr [] wenzelm@38755: (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) []) bulwahn@38075: end bulwahn@38075: bulwahn@38075: fun values_cmd print_modes soln raw_t state = bulwahn@38075: let bulwahn@38075: val ctxt = Toplevel.context_of state bulwahn@38075: val t = Syntax.read_term ctxt raw_t bulwahn@38075: val t' = values ctxt soln t bulwahn@38075: val ty' = Term.type_of t' bulwahn@38075: val ctxt' = Variable.auto_fixes t' ctxt bulwahn@38115: val _ = tracing "Printing terms..." bulwahn@38075: val p = Print_Mode.with_modes print_modes (fn () => bulwahn@38075: Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, bulwahn@38075: Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); bulwahn@38075: in Pretty.writeln p end; bulwahn@38075: bulwahn@38075: bulwahn@38075: (* renewing the values command for Prolog queries *) bulwahn@38075: bulwahn@38075: val opt_print_modes = bulwahn@38075: Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) []; bulwahn@38075: bulwahn@38075: val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag bulwahn@38077: (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term bulwahn@38075: >> (fn ((print_modes, soln), t) => Toplevel.keep haftmann@38504: (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*) bulwahn@38075: bulwahn@38733: (* quickcheck generator *) bulwahn@38733: bulwahn@38733: (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *) bulwahn@38733: haftmann@38786: fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B bulwahn@38733: | strip_imp_prems _ = []; bulwahn@38733: haftmann@38786: fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B bulwahn@38733: | strip_imp_concl A = A : term; bulwahn@38733: bulwahn@38733: fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); bulwahn@38733: bulwahn@39461: fun quickcheck ctxt t size = bulwahn@38733: let bulwahn@38950: val options = code_options_of (ProofContext.theory_of ctxt) wenzelm@38755: val thy = Theory.copy (ProofContext.theory_of ctxt) bulwahn@38733: val (vs, t') = strip_abs t wenzelm@38755: val vs' = Variable.variant_frees ctxt [] vs bulwahn@38733: val Ts = map snd vs' bulwahn@38733: val t'' = subst_bounds (map Free (rev vs'), t') bulwahn@38733: val (prems, concl) = strip_horn t'' bulwahn@38733: val constname = "quickcheck" bulwahn@38733: val full_constname = Sign.full_bname thy constname bulwahn@38733: val constT = Ts ---> @{typ bool} bulwahn@38733: val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy bulwahn@38733: val const = Const (full_constname, constT) bulwahn@38733: val t = Logic.list_implies bulwahn@38733: (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), bulwahn@38733: HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) bulwahn@38733: val tac = fn _ => Skip_Proof.cheat_tac thy1 bulwahn@38733: val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac bulwahn@38733: val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 bulwahn@38733: val thy3 = Predicate_Compile.preprocess preprocess_options const thy2 wenzelm@38755: val ctxt' = ProofContext.init_global thy3 bulwahn@38733: val _ = tracing "Generating prolog program..." bulwahn@39461: val (p, constant_table) = generate (NONE, true) ctxt' full_constname bulwahn@38950: |> add_ground_predicates ctxt' (#limited_types options) bulwahn@38950: |> add_limited_predicates (#limited_predicates options) bulwahn@38960: |> apfst (fold replace (#replacing options)) bulwahn@38960: |> apfst (reorder_manually (#manual_reorder options)) bulwahn@38733: val _ = tracing "Running prolog program..." bulwahn@39461: val system_config = System_Config.get (Context.Proof ctxt) bulwahn@39461: val tss = run (#timeout system_config, #prolog_system system_config) bulwahn@38792: p (translate_const constant_table full_constname) (map fst vs') (SOME 1) bulwahn@38733: val _ = tracing "Restoring terms..." bulwahn@38961: val res = bulwahn@38961: case tss of bulwahn@38961: [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts)) bulwahn@38961: | _ => NONE bulwahn@38733: val empty_report = ([], false) bulwahn@38733: in bulwahn@38733: (res, empty_report) bulwahn@38733: end; bulwahn@38732: bulwahn@38073: end;