src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 39461 0ed0f015d140
parent 39383 ddfafa97da2f
child 39462 3a86194d1534
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 08:18:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:04 2010 +0200
     1.3 @@ -12,12 +12,13 @@
     1.4       limited_types : (typ * int) list,
     1.5       limited_predicates : (string list * int) list,
     1.6       replacing : ((string * string) * string) list,
     1.7 -     manual_reorder : ((string * int) * int list) list,
     1.8 -     timeout : Time.time,
     1.9 -     prolog_system : prolog_system}
    1.10 +     manual_reorder : ((string * int) * int list) list}
    1.11 +  val set_ensure_groundness : code_options -> code_options
    1.12 +  val map_limit_predicates : ((string list * int) list -> (string list * int) list)
    1.13 +    -> code_options -> code_options
    1.14    val code_options_of : theory -> code_options 
    1.15    val map_code_options : (code_options -> code_options) -> theory -> theory
    1.16 -
    1.17 +  
    1.18    datatype arith_op = Plus | Minus
    1.19    datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
    1.20      | Number of int | ArithOp of arith_op * prol_term list;
    1.21 @@ -30,12 +31,13 @@
    1.22    type clause = ((string * prol_term list) * prem);
    1.23    type logic_program = clause list;
    1.24    type constant_table = (string * string) list
    1.25 -
    1.26 -  val generate : bool -> Proof.context -> string -> (logic_program * constant_table)
    1.27 +  
    1.28 +  val generate : Predicate_Compile_Aux.mode option * bool ->
    1.29 +    Proof.context -> string -> (logic_program * constant_table)
    1.30    val write_program : logic_program -> string
    1.31    val run : (Time.time * prolog_system) -> logic_program -> string -> string list -> int option -> prol_term list list
    1.32 -
    1.33 -  val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
    1.34 +  
    1.35 +  val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool)
    1.36  
    1.37    val trace : bool Unsynchronized.ref
    1.38    
    1.39 @@ -53,44 +55,67 @@
    1.40  
    1.41  (* code generation options *)
    1.42  
    1.43 -datatype prolog_system = SWI_PROLOG | YAP
    1.44  
    1.45  type code_options =
    1.46    {ensure_groundness : bool,
    1.47     limited_types : (typ * int) list,
    1.48     limited_predicates : (string list * int) list,
    1.49     replacing : ((string * string) * string) list,
    1.50 -   manual_reorder : ((string * int) * int list) list,
    1.51 -   timeout : Time.time,
    1.52 -   prolog_system : prolog_system}
    1.53 +   manual_reorder : ((string * int) * int list) list}
    1.54 +
    1.55  
    1.56 +fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates,
    1.57 +  replacing, manual_reorder} =
    1.58 +  {ensure_groundness = true, limited_types = limited_types,
    1.59 +   limited_predicates = limited_predicates, replacing = replacing,
    1.60 +   manual_reorder = manual_reorder}
    1.61 +
    1.62 +fun map_limit_predicates f {ensure_groundness, limited_types, limited_predicates,
    1.63 +  replacing, manual_reorder} =
    1.64 +  {ensure_groundness = ensure_groundness, limited_types = limited_types,
    1.65 +   limited_predicates = f limited_predicates, replacing = replacing,
    1.66 +   manual_reorder = manual_reorder}
    1.67 +  
    1.68  structure Options = Theory_Data
    1.69  (
    1.70    type T = code_options
    1.71    val empty = {ensure_groundness = false,
    1.72 -    limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [],
    1.73 -    timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
    1.74 +    limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []}
    1.75    val extend = I;
    1.76    fun merge
    1.77      ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
    1.78        limited_predicates = limited_predicates1, replacing = replacing1,
    1.79 -      manual_reorder = manual_reorder1, timeout = timeout1, prolog_system = prolog_system1},
    1.80 +      manual_reorder = manual_reorder1},
    1.81       {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
    1.82        limited_predicates = limited_predicates2, replacing = replacing2,
    1.83 -      manual_reorder = manual_reorder2, timeout = timeout2, prolog_system = prolog_system2}) =
    1.84 +      manual_reorder = manual_reorder2}) =
    1.85      {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
    1.86       limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
    1.87       limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
    1.88       manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
    1.89 -     replacing = Library.merge (op =) (replacing1, replacing2),
    1.90 -     timeout = timeout1,
    1.91 -     prolog_system = prolog_system1};
    1.92 +     replacing = Library.merge (op =) (replacing1, replacing2)};
    1.93  );
    1.94  
    1.95  val code_options_of = Options.get
    1.96  
    1.97  val map_code_options = Options.map
    1.98  
    1.99 +(* system configuration *)
   1.100 +
   1.101 +datatype prolog_system = SWI_PROLOG | YAP
   1.102 +
   1.103 +type system_configuration = {timeout : Time.time, prolog_system : prolog_system}
   1.104 +
   1.105 +structure System_Config = Generic_Data
   1.106 +(
   1.107 +  type T = system_configuration
   1.108 +  val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
   1.109 +  val extend = I;
   1.110 +  fun merge ({timeout = timeout1, prolog_system = prolog_system1},
   1.111 +        {timeout = timeout2, prolog_system = prolog_system2}) =
   1.112 +    {timeout = timeout1, prolog_system = prolog_system1}
   1.113 +)
   1.114 +
   1.115  (* general string functions *)
   1.116  
   1.117  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
   1.118 @@ -176,7 +201,6 @@
   1.119  
   1.120  type constant_table = (string * string) list
   1.121  
   1.122 -(* assuming no clashing *)
   1.123  fun declare_consts consts constant_table =
   1.124    let
   1.125      fun update' c table =
   1.126 @@ -281,7 +305,6 @@
   1.127      val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
   1.128      val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
   1.129      val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
   1.130 -      |> declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}]
   1.131      fun translate_intro intro =
   1.132        let
   1.133          val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
   1.134 @@ -316,18 +339,153 @@
   1.135    tracing (cat_lines (map (fn const =>
   1.136      "Constant " ^ const ^ "has intros:\n" ^
   1.137      cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
   1.138 -    
   1.139 -fun generate ensure_groundness ctxt const =
   1.140 +
   1.141 +(* translation of moded predicates *)
   1.142 +
   1.143 +(** generating graph of moded predicates **)
   1.144 +
   1.145 +(* could be moved to Predicate_Compile_Core *)
   1.146 +fun requires_modes polarity cls =
   1.147 +  let
   1.148 +    fun req_mode_of pol (t, derivation) =
   1.149 +      (case fst (strip_comb t) of
   1.150 +        Const (c, _) => SOME (c, (pol, Predicate_Compile_Core.head_mode_of derivation))
   1.151 +      | _ => NONE)
   1.152 +    fun req (Predicate_Compile_Aux.Prem t, derivation) = req_mode_of polarity (t, derivation)
   1.153 +      | req (Predicate_Compile_Aux.Negprem t, derivation) = req_mode_of (not polarity) (t, derivation)
   1.154 +      | req _ = NONE
   1.155 +  in      
   1.156 +    maps (fn (_, prems) => map_filter req prems) cls
   1.157 +  end
   1.158 + 
   1.159 +structure Mode_Graph = Graph(type key = string * (bool * Predicate_Compile_Aux.mode)
   1.160 +  val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord));
   1.161 +
   1.162 +fun mk_moded_clauses_graph ctxt scc gr =
   1.163 +  let
   1.164 +    val options = Predicate_Compile_Aux.default_options
   1.165 +    val mode_analysis_options =
   1.166 +      {use_random = true, reorder_premises = true, infer_pos_and_neg_modes = true}
   1.167 +    fun infer prednames (gr, (pos_modes, neg_modes, random)) =
   1.168 +      let
   1.169 +        val (lookup_modes, lookup_neg_modes, needs_random) =
   1.170 +          ((fn s => the (AList.lookup (op =) pos_modes s)),
   1.171 +           (fn s => the (AList.lookup (op =) neg_modes s)),
   1.172 +           (fn s => member (op =) (the (AList.lookup (op =) random s))))
   1.173 +        val (preds, all_vs, param_vs, all_modes, clauses) =
   1.174 +          Predicate_Compile_Core.prepare_intrs options ctxt prednames
   1.175 +            (maps (Predicate_Compile_Core.intros_of ctxt) prednames)
   1.176 +        val ((moded_clauses, random'), _) =
   1.177 +          Predicate_Compile_Core.infer_modes mode_analysis_options options 
   1.178 +            (lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses
   1.179 +        val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
   1.180 +        val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes
   1.181 +        val neg_modes' = map (apsnd (map_filter (fn (false, m) => SOME m | _ => NONE))) modes
   1.182 +        val _ = tracing ("Inferred modes:\n" ^
   1.183 +          cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
   1.184 +            (fn (p, m) => Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
   1.185 +        val gr' = gr
   1.186 +          |> fold (fn (p, mps) => fold (fn (mode, cls) =>
   1.187 +                Mode_Graph.new_node ((p, mode), cls)) mps)
   1.188 +            moded_clauses
   1.189 +          |> fold (fn (p, mps) => fold (fn (mode, cls) => fold (fn req =>
   1.190 +              Mode_Graph.add_edge ((p, mode), req)) (requires_modes (fst mode) cls)) mps)
   1.191 +            moded_clauses
   1.192 +      in
   1.193 +        (gr', (AList.merge (op =) (op =) (pos_modes, pos_modes'),
   1.194 +          AList.merge (op =) (op =) (neg_modes, neg_modes'),
   1.195 +          AList.merge (op =) (op =) (random, random')))
   1.196 +      end
   1.197 +  in  
   1.198 +    fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], []))) 
   1.199 +  end
   1.200 +
   1.201 +fun declare_moded_predicate moded_preds table =
   1.202 +  let
   1.203 +    fun update' (p as (pred, (pol, mode))) table =
   1.204 +      if AList.defined (op =) table p then table else
   1.205 +        let
   1.206 +          val name = Long_Name.base_name pred ^ (if pol then "p" else "n")
   1.207 +            ^ Predicate_Compile_Aux.ascii_string_of_mode mode
   1.208 +          val p' = mk_conform first_lower "pred" (map snd table) name
   1.209 +        in
   1.210 +          AList.update (op =) (p, p') table
   1.211 +        end
   1.212 +  in
   1.213 +    fold update' moded_preds table
   1.214 +  end
   1.215 +
   1.216 +fun mk_program ctxt moded_gr moded_preds (prog, (moded_pred_table, constant_table)) =
   1.217 +  let
   1.218 +    val moded_pred_table' = declare_moded_predicate moded_preds moded_pred_table
   1.219 +    fun mk_literal pol derivation constant_table' t =
   1.220 +      let
   1.221 +        val (p, args) = strip_comb t
   1.222 +        val mode = Predicate_Compile_Core.head_mode_of derivation 
   1.223 +        val name = fst (dest_Const p)
   1.224 +        
   1.225 +        val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode)))
   1.226 +        val args' = map (translate_term ctxt constant_table') args
   1.227 +      in
   1.228 +        Rel (p', args')
   1.229 +      end
   1.230 +    fun mk_prem pol (indprem, derivation) constant_table =
   1.231 +      case indprem of
   1.232 +        Predicate_Compile_Aux.Generator (s, T) => (Ground (s, T), constant_table)
   1.233 +      | _ =>
   1.234 +        declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) []) constant_table
   1.235 +        |> (fn constant_table' =>
   1.236 +          (case indprem of Predicate_Compile_Aux.Negprem t =>
   1.237 +            NegRel_of (mk_literal (not pol) derivation constant_table' t)
   1.238 +          | _ =>
   1.239 +            mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem), constant_table'))
   1.240 +    fun mk_clause pred_name pol (ts, prems) (prog, constant_table) =
   1.241 +    let
   1.242 +      val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table
   1.243 +      val args = map (translate_term ctxt constant_table') ts
   1.244 +      val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table'
   1.245 +    in
   1.246 +      (((pred_name, args), Conj prems') :: prog, constant_table'')
   1.247 +    end
   1.248 +    fun mk_clauses (pred, mode as (pol, _)) =
   1.249 +      let
   1.250 +        val clauses = Mode_Graph.get_node moded_gr (pred, mode)
   1.251 +        val pred_name = the (AList.lookup (op =) moded_pred_table' (pred, mode))
   1.252 +      in
   1.253 +        fold (mk_clause pred_name pol) clauses
   1.254 +      end
   1.255 +  in
   1.256 +    apsnd (pair moded_pred_table') (fold mk_clauses moded_preds (prog, constant_table))
   1.257 +  end
   1.258 +
   1.259 +fun generate (use_modes, ensure_groundness) ctxt const =
   1.260    let 
   1.261      fun strong_conn_of gr keys =
   1.262        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
   1.263      val gr = Predicate_Compile_Core.intros_graph_of ctxt
   1.264      val gr' = add_edges depending_preds_of const gr
   1.265      val scc = strong_conn_of gr' [const]
   1.266 -    val _ = print_intros ctxt gr (flat scc)
   1.267 -    val constant_table = declare_consts (flat scc) []
   1.268 +    val initial_constant_table = 
   1.269 +      declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] []
   1.270    in
   1.271 -    apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
   1.272 +    case use_modes of
   1.273 +      SOME mode =>
   1.274 +        let
   1.275 +          val moded_gr = mk_moded_clauses_graph ctxt scc gr
   1.276 +          val moded_gr' = Mode_Graph.subgraph
   1.277 +            (member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr
   1.278 +          val scc = Mode_Graph.strong_conn moded_gr' 
   1.279 +        in
   1.280 +          apfst rev (apsnd snd
   1.281 +            (fold (mk_program ctxt moded_gr') (rev scc) ([], ([], initial_constant_table))))
   1.282 +        end
   1.283 +      | NONE =>
   1.284 +        let 
   1.285 +          val _ = print_intros ctxt gr (flat scc)
   1.286 +          val constant_table = declare_consts (flat scc) initial_constant_table
   1.287 +        in
   1.288 +          apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
   1.289 +        end
   1.290    end
   1.291    
   1.292  (* implementation for fully enumerating predicates and
   1.293 @@ -521,6 +679,7 @@
   1.294    | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
   1.295    | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r
   1.296    | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r
   1.297 +  | write_prem _ = raise Fail "Not a valid prolog premise"
   1.298  
   1.299  fun write_clause (head, prem) =
   1.300    write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
   1.301 @@ -723,7 +882,7 @@
   1.302        |> Predicate_Compile.preprocess preprocess_options t
   1.303      val ctxt' = ProofContext.init_global thy'
   1.304      val _ = tracing "Generating prolog program..."
   1.305 -    val (p, constant_table) = generate (#ensure_groundness options) ctxt' name
   1.306 +    val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
   1.307        |> (if #ensure_groundness options then
   1.308            add_ground_predicates ctxt' (#limited_types options)
   1.309          else I)
   1.310 @@ -731,7 +890,8 @@
   1.311        |> apfst (fold replace (#replacing options))
   1.312        |> apfst (reorder_manually (#manual_reorder options))
   1.313      val _ = tracing "Running prolog program..."
   1.314 -    val tss = run (#timeout options, #prolog_system options)
   1.315 +    val system_config = System_Config.get (Context.Proof ctxt)
   1.316 +    val tss = run (#timeout system_config, #prolog_system system_config)
   1.317        p (translate_const constant_table name) (map first_upper vnames) soln
   1.318      val _ = tracing "Restoring terms..."
   1.319      val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
   1.320 @@ -798,7 +958,7 @@
   1.321  
   1.322  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   1.323  
   1.324 -fun quickcheck ctxt report t size =
   1.325 +fun quickcheck ctxt t size =
   1.326    let
   1.327      val options = code_options_of (ProofContext.theory_of ctxt)
   1.328      val thy = Theory.copy (ProofContext.theory_of ctxt)
   1.329 @@ -821,13 +981,14 @@
   1.330      val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
   1.331      val ctxt' = ProofContext.init_global thy3
   1.332      val _ = tracing "Generating prolog program..."
   1.333 -    val (p, constant_table) = generate true ctxt' full_constname
   1.334 +    val (p, constant_table) = generate (NONE, true) ctxt' full_constname
   1.335        |> add_ground_predicates ctxt' (#limited_types options)
   1.336        |> add_limited_predicates (#limited_predicates options)
   1.337        |> apfst (fold replace (#replacing options))
   1.338        |> apfst (reorder_manually (#manual_reorder options))
   1.339      val _ = tracing "Running prolog program..."
   1.340 -    val tss = run (#timeout options, #prolog_system options)
   1.341 +    val system_config = System_Config.get (Context.Proof ctxt)
   1.342 +    val tss = run (#timeout system_config, #prolog_system system_config)
   1.343        p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
   1.344      val _ = tracing "Restoring terms..."
   1.345      val res =