reviving the classical depth-limited computation in the predicate compiler
authorbulwahn
Mon Mar 22 08:30:13 2010 +0100 (2010-03-22)
changeset 3587999818df5b8f5
parent 35878 74a74828d682
child 35880 2623b23e41fc
reviving the classical depth-limited computation in the predicate compiler
src/HOL/Predicate_Compile.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Predicate_Compile.thy	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  (*  Title:      HOL/Predicate_Compile.thy
     1.6      Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
     1.7  *)
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
     2.3 @@ -570,7 +570,8 @@
     2.4    "no_topmost_reordering"]
     2.5  
     2.6  val compilation_names = [("pred", Pred),
     2.7 -  (*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*)
     2.8 +  (*("random", Random),*)
     2.9 +  ("depth_limited", Depth_Limited), (*("annotated", Annotated),*)
    2.10    ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
    2.11  
    2.12  fun print_step options s =
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     3.3 @@ -1447,6 +1447,7 @@
     3.4    compilation : compilation,
     3.5    function_name_prefix : string,
     3.6    compfuns : compilation_funs,
     3.7 +  modify_funT : typ -> typ,
     3.8    additional_arguments : string list -> term list,
     3.9    wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
    3.10    transform_additional_arguments : indprem -> term list -> term list
    3.11 @@ -1457,7 +1458,11 @@
    3.12  val compilation = #compilation o dest_comp_modifiers
    3.13  val function_name_prefix = #function_name_prefix o dest_comp_modifiers
    3.14  val compfuns = #compfuns o dest_comp_modifiers
    3.15 -val funT_of = funT_of o compfuns
    3.16 +
    3.17 +val funT_of' = funT_of o compfuns
    3.18 +val modify_funT = #modify_funT o dest_comp_modifiers
    3.19 +fun funT_of comp mode = modify_funT comp o funT_of' comp mode
    3.20 +
    3.21  val additional_arguments = #additional_arguments o dest_comp_modifiers
    3.22  val wrap_compilation = #wrap_compilation o dest_comp_modifiers
    3.23  val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
    3.24 @@ -1544,7 +1549,7 @@
    3.25           | (SOME t, SOME u) => SOME (t $ u)
    3.26           | _ => error "something went wrong here!"))
    3.27    in
    3.28 -    the (expr_of (t, deriv))
    3.29 +    list_comb (the (expr_of (t, deriv)), additional_arguments)
    3.30    end
    3.31  
    3.32  fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments
    3.33 @@ -1624,14 +1629,12 @@
    3.34  
    3.35  fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
    3.36    let
    3.37 -    (* TODO: val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
    3.38 +    val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
    3.39        (all_vs @ param_vs)
    3.40 -    *)
    3.41      val compfuns = Comp_Mod.compfuns compilation_modifiers
    3.42      fun is_param_type (T as Type ("fun",[_ , T'])) =
    3.43        is_some (try (dest_predT compfuns) T) orelse is_param_type T'
    3.44        | is_param_type T = is_some (try (dest_predT compfuns) T)
    3.45 -    val additional_arguments = []
    3.46      val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
    3.47        (binder_types T)
    3.48      val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
    3.49 @@ -2451,11 +2454,12 @@
    3.50  fun add_equations_of steps mode_analysis_options options prednames thy =
    3.51    let
    3.52      fun dest_steps (Steps s) = s
    3.53 +    val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
    3.54      val _ = print_step options
    3.55 -      ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
    3.56 +      ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
    3.57 +        ^ ") for predicates " ^ commas prednames ^ "...")
    3.58        (*val _ = check_intros_elim_match thy prednames*)
    3.59        (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
    3.60 -    val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
    3.61      val _ =
    3.62        if show_intermediate_results options then
    3.63          tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
    3.64 @@ -2533,45 +2537,40 @@
    3.65          else thy)
    3.66        scc thy' |> Theory.checkpoint
    3.67    in thy'' end
    3.68 -(*
    3.69 +
    3.70  val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
    3.71    {
    3.72    compilation = Depth_Limited,
    3.73 -  function_name_of = function_name_of Depth_Limited,
    3.74 -  set_function_name = set_function_name Depth_Limited,
    3.75 -  funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ),
    3.76    function_name_prefix = "depth_limited_",
    3.77 +  compfuns = PredicateCompFuns.compfuns,
    3.78    additional_arguments = fn names =>
    3.79      let
    3.80 -      val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"]
    3.81 -    in [Free (polarity_name, @{typ "bool"}), Free (depth_name, @{typ "code_numeral"})] end,
    3.82 +      val [depth_name] = Name.variant_list names ["depth"]
    3.83 +    in [Free (depth_name, @{typ code_numeral})] end,
    3.84 +  modify_funT = (fn T => let val (Ts, U) = strip_type T
    3.85 +  val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
    3.86    wrap_compilation =
    3.87      fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
    3.88      let
    3.89 -      val [polarity, depth] = additional_arguments
    3.90 -      val (_, Ts2) = chop (length (fst mode)) (binder_types T)
    3.91 -      val (_, Us2) = split_smodeT (snd mode) Ts2
    3.92 -      val T' = mk_predT compfuns (HOLogic.mk_tupleT Us2)
    3.93 +      val [depth] = additional_arguments
    3.94 +      val (_, Ts) = split_modeT' mode (binder_types T)
    3.95 +      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
    3.96        val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    3.97 -      val full_mode = null Us2
    3.98      in
    3.99        if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
   3.100 -        $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T')
   3.101 -          $ (if full_mode then mk_single compfuns HOLogic.unit else
   3.102 -            Const (@{const_name undefined}, T')))
   3.103 +        $ mk_bot compfuns (dest_predT compfuns T')
   3.104          $ compilation
   3.105      end,
   3.106    transform_additional_arguments =
   3.107      fn prem => fn additional_arguments =>
   3.108      let
   3.109 -      val [polarity, depth] = additional_arguments
   3.110 -      val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
   3.111 +      val [depth] = additional_arguments
   3.112        val depth' =
   3.113          Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
   3.114            $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
   3.115 -    in [polarity', depth'] end
   3.116 +    in [depth'] end
   3.117    }
   3.118 -
   3.119 +(*
   3.120  val random_comp_modifiers = Comp_Mod.Comp_Modifiers
   3.121    {
   3.122    compilation = Random,
   3.123 @@ -2592,6 +2591,7 @@
   3.124    compilation = Pred,
   3.125    function_name_prefix = "",
   3.126    compfuns = PredicateCompFuns.compfuns,
   3.127 +    modify_funT = I,
   3.128    additional_arguments = K [],
   3.129    wrap_compilation = K (K (K (K (K I))))
   3.130     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   3.131 @@ -2615,6 +2615,7 @@
   3.132    compilation = Annotated,
   3.133    function_name_prefix = "annotated_",
   3.134    compfuns = PredicateCompFuns.compfuns,
   3.135 +  modify_funT = I,
   3.136    additional_arguments = K [],
   3.137    wrap_compilation =
   3.138      fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   3.139 @@ -2628,6 +2629,7 @@
   3.140    compilation = DSeq,
   3.141    function_name_prefix = "dseq_",
   3.142    compfuns = DSequence_CompFuns.compfuns,
   3.143 +  modify_funT = I,
   3.144    additional_arguments = K [],
   3.145    wrap_compilation = K (K (K (K (K I))))
   3.146     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   3.147 @@ -2639,6 +2641,7 @@
   3.148    compilation = Pos_Random_DSeq,
   3.149    function_name_prefix = "random_dseq_",
   3.150    compfuns = Random_Sequence_CompFuns.compfuns,
   3.151 +  modify_funT = I,
   3.152    additional_arguments = K [],
   3.153    wrap_compilation = K (K (K (K (K I))))
   3.154     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   3.155 @@ -2650,22 +2653,25 @@
   3.156    compilation = Neg_Random_DSeq,
   3.157    function_name_prefix = "random_dseq_neg_",
   3.158    compfuns = Random_Sequence_CompFuns.compfuns,
   3.159 +  modify_funT = I,
   3.160    additional_arguments = K [],
   3.161    wrap_compilation = K (K (K (K (K I))))
   3.162     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   3.163    transform_additional_arguments = K I : (indprem -> term list -> term list)
   3.164    }
   3.165  
   3.166 -(*
   3.167  val add_depth_limited_equations = gen_add_equations
   3.168 -  (Steps {infer_modes = infer_modes,
   3.169 -  define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   3.170 -  compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   3.171 +  (Steps {
   3.172 +  define_functions =
   3.173 +    fn options => fn preds => fn (s, modes) =>
   3.174 +    define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns
   3.175 +    options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   3.176    prove = prove_by_skip,
   3.177    add_code_equations = K (K I),
   3.178 -  defined = defined_functions Depth_Limited,
   3.179 +  comp_modifiers = depth_limited_comp_modifiers,
   3.180 +  use_random = false,
   3.181    qname = "depth_limited_equation"})
   3.182 -*)
   3.183 +
   3.184  val add_annotated_equations = gen_add_equations
   3.185    (Steps {
   3.186    define_functions =
   3.187 @@ -2769,10 +2775,10 @@
   3.188            ((case compilation options of
   3.189               Pred => add_equations
   3.190             | DSeq => add_dseq_equations
   3.191 -           | Random_DSeq => add_random_dseq_equations
   3.192 +           | Pos_Random_DSeq => add_random_dseq_equations
   3.193 +           | Depth_Limited => add_depth_limited_equations
   3.194             | compilation => error ("Compilation not supported")
   3.195             (*| Random => (fn opt => fn cs => add_equations opt cs #> add_quickcheck_equations opt cs)
   3.196 -           | Depth_Limited => add_depth_limited_equations
   3.197             | Annotated => add_annotated_equations*)
   3.198             ) options [const]))
   3.199        end
   3.200 @@ -2854,17 +2860,17 @@
   3.201              Pred => []
   3.202            | Random => [@{term "5 :: code_numeral"}]
   3.203            | Annotated => []
   3.204 -          | Depth_Limited => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
   3.205 +          | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
   3.206            | DSeq => []
   3.207 -          | Random_DSeq => []
   3.208 +          | Pos_Random_DSeq => []
   3.209          val comp_modifiers =
   3.210            case compilation of
   3.211              Pred => predicate_comp_modifiers
   3.212 -          (*| Random => random_comp_modifiers
   3.213 +          | Random => random_comp_modifiers
   3.214            | Depth_Limited => depth_limited_comp_modifiers
   3.215 -          | Annotated => annotated_comp_modifiers*)
   3.216 +          (*| Annotated => annotated_comp_modifiers*)
   3.217            | DSeq => dseq_comp_modifiers
   3.218 -          | Random_DSeq => pos_random_dseq_comp_modifiers
   3.219 +          | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
   3.220          val t_pred = compile_expr comp_modifiers compfuns thy true (body, deriv) additional_arguments;
   3.221          val T_pred = dest_predT compfuns (fastype_of t_pred)
   3.222          val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple