src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 38731 2c8a595af43e
parent 38729 9c9d14827380
child 38732 3371dbc806ae
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:50 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    type logic_program = clause list;
     1.5    type constant_table = (string * string) list
     1.6      
     1.7 -  val generate : code_options -> Proof.context -> string list -> (logic_program * constant_table)
     1.8 +  val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
     1.9    val write_program : logic_program -> string
    1.10    val run : logic_program -> string -> string list -> int option -> prol_term list list
    1.11  
    1.12 @@ -190,15 +190,63 @@
    1.13        in clause end
    1.14    in (map translate_intro intros', constant_table') end
    1.15  
    1.16 +val preprocess_options = Predicate_Compile_Aux.Options {
    1.17 +  expected_modes = NONE,
    1.18 +  proposed_modes = NONE,
    1.19 +  proposed_names = [],
    1.20 +  show_steps = false,
    1.21 +  show_intermediate_results = false,
    1.22 +  show_proof_trace = false,
    1.23 +  show_modes = false,
    1.24 +  show_mode_inference = false,
    1.25 +  show_compilation = false,
    1.26 +  show_caught_failures = false,
    1.27 +  skip_proof = true,
    1.28 +  no_topmost_reordering = false,
    1.29 +  function_flattening = true,
    1.30 +  specialise = false,
    1.31 +  fail_safe_function_flattening = false,
    1.32 +  no_higher_order_predicate = [],
    1.33 +  inductify = false,
    1.34 +  detect_switches = true,
    1.35 +  compilation = Predicate_Compile_Aux.Pred
    1.36 +}
    1.37 +
    1.38 +fun depending_preds_of (key, intros) =
    1.39 +  fold Term.add_const_names (map Thm.prop_of intros) []
    1.40 +
    1.41 +fun add_edges edges_of key G =
    1.42 +  let
    1.43 +    fun extend' key (G, visited) = 
    1.44 +      case try (Graph.get_node G) key of
    1.45 +          SOME v =>
    1.46 +            let
    1.47 +              val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
    1.48 +              val (G', visited') = fold extend'
    1.49 +                (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
    1.50 +            in
    1.51 +              (fold (Graph.add_edge o (pair key)) new_edges G', visited')
    1.52 +            end
    1.53 +        | NONE => (G, visited)
    1.54 +  in
    1.55 +    fst (extend' key (G, []))
    1.56 +  end
    1.57 +
    1.58  fun generate options ctxt const =
    1.59    let 
    1.60 -     fun strong_conn_of gr keys =
    1.61 +    val T = Sign.the_const_type (ProofContext.theory_of ctxt) const
    1.62 +    val t = Const (const, T)
    1.63 +    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
    1.64 +    val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
    1.65 +    val ctxt'' = ProofContext.init_global thy'
    1.66 +    fun strong_conn_of gr keys =
    1.67        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
    1.68 -    val gr = Predicate_Compile_Core.intros_graph_of ctxt
    1.69 -    val scc = strong_conn_of gr const
    1.70 +    val gr = Predicate_Compile_Core.intros_graph_of ctxt''
    1.71 +    val gr' = add_edges depending_preds_of const gr
    1.72 +    val scc = strong_conn_of gr' [const]
    1.73      val constant_table = mk_constant_table (flat scc)
    1.74    in
    1.75 -    apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
    1.76 +    apfst flat (fold_map (translate_intros options ctxt'' gr) (flat scc) constant_table)
    1.77    end
    1.78    
    1.79  (* add implementation for ground predicates *)
    1.80 @@ -411,7 +459,7 @@
    1.81          SOME vs => vs
    1.82        | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
    1.83      val _ = tracing "Generating prolog program..."
    1.84 -    val (p, constant_table) = generate options ctxt [name]
    1.85 +    val (p, constant_table) = generate options ctxt name
    1.86        |> (if #ensure_groundness options then add_ground_predicates ctxt else I)
    1.87      val _ = tracing "Running prolog program..."
    1.88      val tss = run p (translate_const constant_table name) (map first_upper vnames) soln