invocation of values for prolog execution does not require invocation of code_pred anymore
authorbulwahn
Wed Aug 25 16:59:50 2010 +0200 (2010-08-25)
changeset 387312c8a595af43e
parent 38730 5bbdd9a9df62
child 38732 3371dbc806ae
invocation of values for prolog execution does not require invocation of code_pred anymore
src/HOL/Library/Code_Prolog.thy
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
     1.1 --- a/src/HOL/Library/Code_Prolog.thy	Wed Aug 25 16:59:49 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Prolog.thy	Wed Aug 25 16:59:50 2010 +0200
     1.3 @@ -9,5 +9,10 @@
     1.4  uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
     1.5  begin
     1.6  
     1.7 +section {* Setup for Numerals *}
     1.8 +
     1.9 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
    1.10 +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
    1.11 +
    1.12  end
    1.13  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:49 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:50 2010 +0200
     2.3 @@ -9,8 +9,6 @@
     2.4    "append [] ys ys"
     2.5  | "append xs ys zs ==> append (x # xs) ys (x # zs)"
     2.6  
     2.7 -code_pred append .
     2.8 -
     2.9  values 3 "{(x, y, z). append x y z}"
    2.10  
    2.11  
    2.12 @@ -71,9 +69,7 @@
    2.13  where
    2.14    "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
    2.15  
    2.16 -code_pred queen_9 .
    2.17 -
    2.18 -values 150 "{ys. queen_9 ys}"
    2.19 +values 10 "{ys. queen_9 ys}"
    2.20  
    2.21  
    2.22  section {* Example symbolic derivation *}
    2.23 @@ -163,11 +159,6 @@
    2.24  where
    2.25    "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
    2.26  
    2.27 -code_pred ops8 .
    2.28 -code_pred divide10 .
    2.29 -code_pred log10 .
    2.30 -code_pred times10 .
    2.31 -
    2.32  values "{e. ops8 e}"
    2.33  values "{e. divide10 e}"
    2.34  values "{e. log10 e}"
    2.35 @@ -181,8 +172,6 @@
    2.36  where
    2.37    "y \<noteq> B \<Longrightarrow> notB y"
    2.38  
    2.39 -code_pred notB .
    2.40 -
    2.41  ML {* Code_Prolog.options := {ensure_groundness = true} *}
    2.42  
    2.43  values 2 "{y. notB y}"
    2.44 @@ -191,8 +180,6 @@
    2.45  where
    2.46    "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
    2.47  
    2.48 -code_pred notAB .
    2.49 -
    2.50  values 5 "{y. notAB y}"
    2.51  
    2.52  end
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:49 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:50 2010 +0200
     3.3 @@ -84,10 +84,10 @@
     3.4  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
     3.5  by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
     3.6  
     3.7 -code_pred [new_random_dseq inductify, skip_proof] hotel .
     3.8 -
     3.9  ML {* Code_Prolog.options := {ensure_groundness = true} *}
    3.10  
    3.11  values 10 "{s. hotel s}"
    3.12  
    3.13 +
    3.14 +
    3.15  end
    3.16 \ No newline at end of file
     4.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:49 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:50 2010 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    type logic_program = clause list;
     4.5    type constant_table = (string * string) list
     4.6      
     4.7 -  val generate : code_options -> Proof.context -> string list -> (logic_program * constant_table)
     4.8 +  val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
     4.9    val write_program : logic_program -> string
    4.10    val run : logic_program -> string -> string list -> int option -> prol_term list list
    4.11  
    4.12 @@ -190,15 +190,63 @@
    4.13        in clause end
    4.14    in (map translate_intro intros', constant_table') end
    4.15  
    4.16 +val preprocess_options = Predicate_Compile_Aux.Options {
    4.17 +  expected_modes = NONE,
    4.18 +  proposed_modes = NONE,
    4.19 +  proposed_names = [],
    4.20 +  show_steps = false,
    4.21 +  show_intermediate_results = false,
    4.22 +  show_proof_trace = false,
    4.23 +  show_modes = false,
    4.24 +  show_mode_inference = false,
    4.25 +  show_compilation = false,
    4.26 +  show_caught_failures = false,
    4.27 +  skip_proof = true,
    4.28 +  no_topmost_reordering = false,
    4.29 +  function_flattening = true,
    4.30 +  specialise = false,
    4.31 +  fail_safe_function_flattening = false,
    4.32 +  no_higher_order_predicate = [],
    4.33 +  inductify = false,
    4.34 +  detect_switches = true,
    4.35 +  compilation = Predicate_Compile_Aux.Pred
    4.36 +}
    4.37 +
    4.38 +fun depending_preds_of (key, intros) =
    4.39 +  fold Term.add_const_names (map Thm.prop_of intros) []
    4.40 +
    4.41 +fun add_edges edges_of key G =
    4.42 +  let
    4.43 +    fun extend' key (G, visited) = 
    4.44 +      case try (Graph.get_node G) key of
    4.45 +          SOME v =>
    4.46 +            let
    4.47 +              val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
    4.48 +              val (G', visited') = fold extend'
    4.49 +                (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
    4.50 +            in
    4.51 +              (fold (Graph.add_edge o (pair key)) new_edges G', visited')
    4.52 +            end
    4.53 +        | NONE => (G, visited)
    4.54 +  in
    4.55 +    fst (extend' key (G, []))
    4.56 +  end
    4.57 +
    4.58  fun generate options ctxt const =
    4.59    let 
    4.60 -     fun strong_conn_of gr keys =
    4.61 +    val T = Sign.the_const_type (ProofContext.theory_of ctxt) const
    4.62 +    val t = Const (const, T)
    4.63 +    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
    4.64 +    val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
    4.65 +    val ctxt'' = ProofContext.init_global thy'
    4.66 +    fun strong_conn_of gr keys =
    4.67        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
    4.68 -    val gr = Predicate_Compile_Core.intros_graph_of ctxt
    4.69 -    val scc = strong_conn_of gr const
    4.70 +    val gr = Predicate_Compile_Core.intros_graph_of ctxt''
    4.71 +    val gr' = add_edges depending_preds_of const gr
    4.72 +    val scc = strong_conn_of gr' [const]
    4.73      val constant_table = mk_constant_table (flat scc)
    4.74    in
    4.75 -    apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
    4.76 +    apfst flat (fold_map (translate_intros options ctxt'' gr) (flat scc) constant_table)
    4.77    end
    4.78    
    4.79  (* add implementation for ground predicates *)
    4.80 @@ -411,7 +459,7 @@
    4.81          SOME vs => vs
    4.82        | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
    4.83      val _ = tracing "Generating prolog program..."
    4.84 -    val (p, constant_table) = generate options ctxt [name]
    4.85 +    val (p, constant_table) = generate options ctxt name
    4.86        |> (if #ensure_groundness options then add_ground_predicates ctxt else I)
    4.87      val _ = tracing "Running prolog program..."
    4.88      val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Aug 25 16:59:49 2010 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Aug 25 16:59:50 2010 +0200
     5.3 @@ -275,7 +275,6 @@
     5.4        else
     5.5          let
     5.6            val specs = get_specification options thy t
     5.7 -            (*|> Predicate_Compile_Set.unfold_set_notation*)
     5.8            (*val _ = print_specification options thy constname specs*)
     5.9            val us = defiants_of specs
    5.10          in