adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
authorbulwahn
Thu Oct 21 19:13:11 2010 +0200 (2010-10-21)
changeset 40054cd7b1fa20bce
parent 40053 3fa49ea76cbb
child 40055 1f7cc5357d96
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Oct 21 19:13:10 2010 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Oct 21 19:13:11 2010 +0200
     1.3 @@ -96,8 +96,8 @@
     1.4    val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
     1.5    val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
     1.6    val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
     1.7 -  val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio
     1.8 -  val minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio
     1.9 +  val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
    1.10 +  val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
    1.11    fun subtract_nat compfuns (_ : typ) =
    1.12      let
    1.13        val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
    1.14 @@ -128,21 +128,21 @@
    1.15              (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
    1.16      end
    1.17  in
    1.18 -  Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_nat}
    1.19 +  Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
    1.20      [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
    1.21       (ooi, (enumerate_addups_nat, false))]
    1.22    #> Predicate_Compile_Fun.add_function_predicate_translation
    1.23         (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
    1.24 -  #> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_nat}
    1.25 +  #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
    1.26         [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
    1.27    #> Predicate_Compile_Fun.add_function_predicate_translation
    1.28        (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
    1.29 -  #> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_eq_int}
    1.30 +  #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
    1.31      [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
    1.32       (oii, (@{const_name subtract}, false))]
    1.33    #> Predicate_Compile_Fun.add_function_predicate_translation
    1.34         (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
    1.35 -  #> Predicate_Compile_Core.force_modes_and_functions @{const_name minus_eq_int}
    1.36 +  #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
    1.37      [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
    1.38       (ioi, (@{const_name minus}, false))]
    1.39    #> Predicate_Compile_Fun.add_function_predicate_translation
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu Oct 21 19:13:10 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu Oct 21 19:13:11 2010 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
     2.5  
     2.6  code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
     2.7 -ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_nth_el'P} *}
     2.8 +ML {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
     2.9  
    2.10  thm greater_than_index.equation
    2.11  
    2.12 @@ -42,7 +42,7 @@
    2.13  
    2.14  thm max_of_my_SucP.equation
    2.15  
    2.16 -ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_max_natP} *}
    2.17 +ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
    2.18  
    2.19  values "{x. max_of_my_SucP x 6}"
    2.20  
     3.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Oct 21 19:13:10 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Oct 21 19:13:11 2010 +0200
     3.3 @@ -386,9 +386,9 @@
     3.4             (fn s => member (op =) (the (AList.lookup (op =) random s))))
     3.5          val (preds, all_vs, param_vs, all_modes, clauses) =
     3.6            Predicate_Compile_Core.prepare_intrs options ctxt prednames
     3.7 -            (maps (Predicate_Compile_Core.intros_of ctxt) prednames)
     3.8 +            (maps (Core_Data.intros_of ctxt) prednames)
     3.9          val ((moded_clauses, random'), _) =
    3.10 -          Predicate_Compile_Core.infer_modes mode_analysis_options options 
    3.11 +          Mode_Inference.infer_modes mode_analysis_options options 
    3.12              (lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses
    3.13          val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
    3.14          val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes
    3.15 @@ -474,7 +474,7 @@
    3.16    let 
    3.17      fun strong_conn_of gr keys =
    3.18        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
    3.19 -    val gr = Predicate_Compile_Core.intros_graph_of ctxt
    3.20 +    val gr = Core_Data.intros_graph_of ctxt
    3.21      val gr' = add_edges depending_preds_of const gr
    3.22      val scc = strong_conn_of gr' [const]
    3.23      val initial_constant_table = 
    3.24 @@ -917,6 +917,7 @@
    3.25    no_higher_order_predicate = [],
    3.26    inductify = false,
    3.27    detect_switches = true,
    3.28 +  smart_depth_limiting = true,
    3.29    compilation = Predicate_Compile_Aux.Pred
    3.30  }
    3.31  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:10 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:11 2010 +0200
     4.3 @@ -676,7 +676,8 @@
     4.4    ("depth_limited", Depth_Limited),
     4.5    ("depth_limited_random", Depth_Limited_Random),
     4.6    (*("annotated", Annotated),*)
     4.7 -  ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
     4.8 +  ("dseq", DSeq),
     4.9 +  ("random_dseq", Pos_Random_DSeq),
    4.10    ("new_random_dseq", New_Pos_Random_DSeq),
    4.11    ("generator_dseq", Pos_Generator_DSeq)]
    4.12  
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Oct 21 19:13:10 2010 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Oct 21 19:13:11 2010 +0200
     5.3 @@ -85,6 +85,7 @@
     5.4    function_flattening = true,
     5.5    fail_safe_function_flattening = false,
     5.6    no_higher_order_predicate = [],
     5.7 +  smart_depth_limiting = true,
     5.8    no_topmost_reordering = false
     5.9  }
    5.10  
    5.11 @@ -108,6 +109,7 @@
    5.12    function_flattening = true,
    5.13    fail_safe_function_flattening = false,
    5.14    no_higher_order_predicate = [],
    5.15 +  smart_depth_limiting = true,
    5.16    no_topmost_reordering = true
    5.17  }
    5.18  
    5.19 @@ -119,14 +121,14 @@
    5.20      show_invalid_clauses = s_ic, skip_proof = s_p,
    5.21      compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
    5.22      fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
    5.23 -    no_topmost_reordering = re}) =
    5.24 +    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
    5.25    (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    5.26      show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    5.27      show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    5.28      show_invalid_clauses = s_ic, skip_proof = s_p,
    5.29      compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
    5.30      fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
    5.31 -    no_topmost_reordering = re})
    5.32 +    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
    5.33  
    5.34  fun set_fail_safe_function_flattening b
    5.35    (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    5.36 @@ -135,14 +137,14 @@
    5.37      show_invalid_clauses = s_ic, skip_proof = s_p,
    5.38      compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
    5.39      fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
    5.40 -    no_topmost_reordering = re}) =
    5.41 +    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
    5.42    (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    5.43      show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    5.44      show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    5.45      show_invalid_clauses = s_ic, skip_proof = s_p,
    5.46      compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
    5.47      fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
    5.48 -    no_topmost_reordering = re})
    5.49 +    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
    5.50  
    5.51  fun set_no_higher_order_predicate ss
    5.52    (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    5.53 @@ -151,13 +153,14 @@
    5.54      show_invalid_clauses = s_ic, skip_proof = s_p,
    5.55      compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
    5.56      fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
    5.57 -    no_topmost_reordering = re}) =
    5.58 +    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
    5.59    (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
    5.60      show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
    5.61      show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
    5.62      show_invalid_clauses = s_ic, skip_proof = s_p,
    5.63      compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
    5.64 -    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
    5.65 +    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss,
    5.66 +    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
    5.67  
    5.68  
    5.69  fun get_options () = 
    5.70 @@ -173,9 +176,12 @@
    5.71  val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
    5.72  val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
    5.73  
    5.74 -val mk_new_randompredT = Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.compfuns
    5.75 -val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
    5.76 -val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
    5.77 +val mk_new_randompredT =
    5.78 +  Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
    5.79 +val mk_new_return =
    5.80 +  Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
    5.81 +val mk_new_bind =
    5.82 +  Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
    5.83  
    5.84  val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
    5.85  
    5.86 @@ -207,13 +213,12 @@
    5.87      val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
    5.88      val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
    5.89      val ctxt4 = ProofContext.init_global thy4
    5.90 -    val modes = Predicate_Compile_Core.modes_of compilation ctxt4 full_constname
    5.91 +    val modes = Core_Data.modes_of compilation ctxt4 full_constname
    5.92      val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
    5.93      val prog =
    5.94        if member eq_mode modes output_mode then
    5.95          let
    5.96 -          val name = Predicate_Compile_Core.function_name_of compilation ctxt4
    5.97 -            full_constname output_mode
    5.98 +          val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
    5.99            val T = 
   5.100              case compilation of
   5.101                Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))