adding tracing function for evaluated code; annotated compilation in the predicate compiler
authorbulwahn
Fri Nov 06 08:11:58 2009 +0100 (2009-11-06)
changeset 334733b275a0bf18c
parent 33440 181fae134b43
child 33474 767cfb37833e
adding tracing function for evaluated code; annotated compilation in the predicate compiler
src/HOL/Code_Evaluation.thy
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Nov 05 14:47:27 2009 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Nov 06 08:11:58 2009 +0100
     1.3 @@ -243,6 +243,26 @@
     1.4  hide const dummy_term App valapp
     1.5  hide (open) const Const termify valtermify term_of term_of_num
     1.6  
     1.7 +subsection {* Tracing of generated and evaluated code *}
     1.8 +
     1.9 +definition tracing :: "String.literal => 'a => 'a"
    1.10 +where
    1.11 +  [code del]: "tracing s x = x"
    1.12 +
    1.13 +ML {*
    1.14 +structure Code_Evaluation =
    1.15 +struct
    1.16 +
    1.17 +fun tracing s x = (Output.tracing s; x)
    1.18 +
    1.19 +end
    1.20 +*}
    1.21 +
    1.22 +code_const "tracing :: String.literal => 'a => 'a"
    1.23 +  (Eval "Code'_Evaluation.tracing")
    1.24 +
    1.25 +hide (open) const tracing
    1.26 +code_reserved Eval Code_Evaluation
    1.27  
    1.28  subsection {* Evaluation setup *}
    1.29  
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 05 14:47:27 2009 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
     2.3 @@ -121,7 +121,8 @@
     2.4        skip_proof = chk "skip_proof",
     2.5        inductify = chk "inductify",
     2.6        random = chk "random",
     2.7 -      depth_limited = chk "depth_limited"
     2.8 +      depth_limited = chk "depth_limited",
     2.9 +      annotated = chk "annotated"
    2.10      }
    2.11    end
    2.12  
    2.13 @@ -149,7 +150,8 @@
    2.14  val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
    2.15  
    2.16  val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
    2.17 -  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"]
    2.18 +  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
    2.19 +  "annotated"]
    2.20  
    2.21  local structure P = OuterParse
    2.22  in
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 05 14:47:27 2009 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 06 08:11:58 2009 +0100
     3.3 @@ -170,7 +170,8 @@
     3.4  
     3.5    inductify : bool,
     3.6    random : bool,
     3.7 -  depth_limited : bool
     3.8 +  depth_limited : bool,
     3.9 +  annotated : bool
    3.10  };
    3.11  
    3.12  fun expected_modes (Options opt) = #expected_modes opt
    3.13 @@ -185,6 +186,7 @@
    3.14  fun is_inductify (Options opt) = #inductify opt
    3.15  fun is_random (Options opt) = #random opt
    3.16  fun is_depth_limited (Options opt) = #depth_limited opt
    3.17 +fun is_annotated (Options opt) = #annotated opt
    3.18  
    3.19  val default_options = Options {
    3.20    expected_modes = NONE,
    3.21 @@ -198,7 +200,8 @@
    3.22    
    3.23    inductify = false,
    3.24    random = false,
    3.25 -  depth_limited = false
    3.26 +  depth_limited = false,
    3.27 +  annotated = false
    3.28  }
    3.29  
    3.30  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 05 14:47:27 2009 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
     4.3 @@ -52,6 +52,7 @@
     4.4    val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
     4.5    val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
     4.6    val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
     4.7 +  val mk_tracing : string -> term -> term
     4.8  end;
     4.9  
    4.10  structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
    4.11 @@ -116,6 +117,10 @@
    4.12    Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    4.13    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
    4.14  
    4.15 +fun mk_tracing s t =
    4.16 +  Const(@{const_name Code_Evaluation.tracing},
    4.17 +    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
    4.18 +
    4.19  (* destruction of intro rules *)
    4.20  
    4.21  (* FIXME: look for other place where this functionality was used before *)
    4.22 @@ -198,16 +203,21 @@
    4.23    elim : thm option,
    4.24    nparams : int,
    4.25    functions : (mode * predfun_data) list,
    4.26 -  generators : (mode * function_data) list,
    4.27 -  depth_limited_functions : (mode * function_data) list 
    4.28 +  generators : (mode * function_data) list, (*TODO: maybe rename to random_functions *)
    4.29 +  depth_limited_functions : (mode * function_data) list,
    4.30 +  annotated_functions : (mode * function_data) list
    4.31  };
    4.32  
    4.33  fun rep_pred_data (PredData data) = data;
    4.34 -fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) =
    4.35 +fun mk_pred_data ((intros, elim, nparams),
    4.36 +  (functions, generators, depth_limited_functions, annotated_functions)) =
    4.37    PredData {intros = intros, elim = elim, nparams = nparams,
    4.38 -    functions = functions, generators = generators, depth_limited_functions = depth_limited_functions}
    4.39 -fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) =
    4.40 -  mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions)))
    4.41 +    functions = functions, generators = generators,
    4.42 +    depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions}
    4.43 +fun map_pred_data f (PredData {intros, elim, nparams,
    4.44 +  functions, generators, depth_limited_functions, annotated_functions}) =
    4.45 +  mk_pred_data (f ((intros, elim, nparams), (functions, generators,
    4.46 +    depth_limited_functions, annotated_functions)))
    4.47  
    4.48  fun eq_option eq (NONE, NONE) = true
    4.49    | eq_option eq (SOME x, SOME y) = eq (x, y)
    4.50 @@ -302,6 +312,19 @@
    4.51  
    4.52  val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
    4.53  
    4.54 +fun lookup_annotated_function_data thy name mode =
    4.55 +  Option.map rep_function_data (AList.lookup (op =)
    4.56 +  (#annotated_functions (the_pred_data thy name)) mode)
    4.57 +
    4.58 +fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode
    4.59 +  of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode
    4.60 +    ^ " of predicate " ^ name)
    4.61 +   | SOME data => data
    4.62 +
    4.63 +val annotated_modes_of = (map fst) o #annotated_functions oo the_pred_data
    4.64 +
    4.65 +val annotated_function_name_of = #name ooo the_annotated_function_data
    4.66 +
    4.67  (* diagnostic display functions *)
    4.68  
    4.69  fun print_modes options modes =
    4.70 @@ -576,19 +599,20 @@
    4.71            (mk_casesrule (ProofContext.init thy) pred nparams intros)
    4.72          val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)
    4.73        in
    4.74 -        mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
    4.75 +        mk_pred_data ((intros, SOME elim, nparams), ([], [], [], []))
    4.76        end                                                                    
    4.77    | NONE => error ("No such predicate: " ^ quote name)
    4.78  
    4.79  (* updaters *)
    4.80  
    4.81 -fun apfst3 f (x, y, z) =  (f x, y, z)
    4.82 -fun apsnd3 f (x, y, z) =  (x, f y, z)
    4.83 -fun aptrd3 f (x, y, z) =  (x, y, f z)
    4.84 +fun apfst4 f (x1, x2, x3, x4) = (f x1, x2, x3, x4)
    4.85 +fun apsnd4 f (x1, x2, x3, x4) = (x1, f x2, x3, x4)
    4.86 +fun aptrd4 f (x1, x2, x3, x4) = (x1, x2, f x3, x4)
    4.87 +fun apfourth4 f (x1, x2, x3, x4) = (x1, x2, x3, f x4)
    4.88  
    4.89  fun add_predfun name mode data =
    4.90    let
    4.91 -    val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data)
    4.92 +    val add = (apsnd o apfst4 o cons) (mode, mk_predfun_data data)
    4.93    in PredData.map (Graph.map_node name (map_pred_data add)) end
    4.94  
    4.95  fun is_inductive_predicate thy name =
    4.96 @@ -638,7 +662,7 @@
    4.97       | NONE =>
    4.98         let
    4.99           val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
   4.100 -       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end;
   4.101 +       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], [], []))) gr end;
   4.102    in PredData.map cons_intro thy end
   4.103  
   4.104  fun set_elim thm = let
   4.105 @@ -659,7 +683,7 @@
   4.106    in
   4.107      if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
   4.108        PredData.map
   4.109 -        (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
   4.110 +        (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [], [])))) thy
   4.111      else thy
   4.112    end
   4.113  
   4.114 @@ -681,14 +705,21 @@
   4.115  
   4.116  fun set_generator_name pred mode name = 
   4.117    let
   4.118 -    val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
   4.119 +    val set = (apsnd o apsnd4 o cons) (mode, mk_function_data (name, NONE))
   4.120    in
   4.121      PredData.map (Graph.map_node pred (map_pred_data set))
   4.122    end
   4.123  
   4.124  fun set_depth_limited_function_name pred mode name = 
   4.125    let
   4.126 -    val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
   4.127 +    val set = (apsnd o aptrd4 o cons) (mode, mk_function_data (name, NONE))
   4.128 +  in
   4.129 +    PredData.map (Graph.map_node pred (map_pred_data set))
   4.130 +  end
   4.131 +
   4.132 +fun set_annotated_function_name pred mode name =
   4.133 +  let
   4.134 +    val set = (apsnd o apfourth4 o cons) (mode, mk_function_data (name, NONE))
   4.135    in
   4.136      PredData.map (Graph.map_node pred (map_pred_data set))
   4.137    end
   4.138 @@ -715,19 +746,6 @@
   4.139  fun mk_not (CompilationFuns funs) = #mk_not funs
   4.140  fun mk_map (CompilationFuns funs) = #mk_map funs
   4.141  
   4.142 -fun funT_of compfuns (iss, is) T =
   4.143 -  let
   4.144 -    val Ts = binder_types T
   4.145 -    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
   4.146 -    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
   4.147 -  in
   4.148 -    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
   4.149 -  end;
   4.150 -
   4.151 -fun mk_fun_of compfuns thy (name, T) mode = 
   4.152 -  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
   4.153 -
   4.154 -
   4.155  structure PredicateCompFuns =
   4.156  struct
   4.157  
   4.158 @@ -833,6 +851,8 @@
   4.159        RandomPredCompFuns.mk_randompredT T) $ random
   4.160    end;
   4.161  
   4.162 +(* function types and names of different compilations *)
   4.163 +
   4.164  fun depth_limited_funT_of compfuns (iss, is) T =
   4.165    let
   4.166      val Ts = binder_types T
   4.167 @@ -841,7 +861,22 @@
   4.168    in
   4.169      (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}])
   4.170        ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
   4.171 -  end;  
   4.172 +  end;
   4.173 +
   4.174 +fun funT_of compfuns (iss, is) T =
   4.175 +  let
   4.176 +    val Ts = binder_types T
   4.177 +    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
   4.178 +    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
   4.179 +  in
   4.180 +    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
   4.181 +  end;
   4.182 +
   4.183 +fun mk_fun_of compfuns thy (name, T) mode = 
   4.184 +  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
   4.185 +
   4.186 +fun mk_annotated_fun_of compfuns thy (name, T) mode =
   4.187 +  Const (annotated_function_name_of thy name mode, funT_of compfuns mode T)
   4.188  
   4.189  fun mk_depth_limited_fun_of compfuns thy (name, T) mode =
   4.190    Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)
   4.191 @@ -1370,9 +1405,7 @@
   4.192        map (compile_clause compilation_modifiers compfuns
   4.193          thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls;
   4.194      val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
   4.195 -      (if null cl_ts then
   4.196 -        mk_bot compfuns (HOLogic.mk_tupleT Us2)
   4.197 -      else foldr1 (mk_sup compfuns) cl_ts)
   4.198 +      (if null cl_ts then mk_bot compfuns (HOLogic.mk_tupleT Us2) else foldr1 (mk_sup compfuns) cl_ts)
   4.199      val fun_const =
   4.200        Const (Comp_Mod.const_name_of compilation_modifiers thy s mode,
   4.201          Comp_Mod.funT_of compilation_modifiers compfuns mode T)
   4.202 @@ -1598,7 +1631,23 @@
   4.203    in
   4.204      fold create_definition modes thy
   4.205    end;
   4.206 -  
   4.207 +
   4.208 +fun create_definitions_of_annotated_functions preds (name, modes) thy =
   4.209 +  let
   4.210 +    val T = AList.lookup (op =) preds name |> the
   4.211 +    fun create_definition mode thy =
   4.212 +      let
   4.213 +        val mode_cname = create_constname_of_mode thy "annotated_" name mode
   4.214 +        val funT = funT_of PredicateCompFuns.compfuns mode T
   4.215 +      in
   4.216 +        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
   4.217 +        |> set_annotated_function_name name mode mode_cname 
   4.218 +      end;
   4.219 +  in
   4.220 +    fold create_definition modes thy
   4.221 +  end;
   4.222 +
   4.223 +
   4.224  (* Proving equivalence of term *)
   4.225  
   4.226  fun is_Type (Type _) = true
   4.227 @@ -2308,6 +2357,16 @@
   4.228    transform_additional_arguments = K I : (indprem -> term list -> term list)
   4.229    }
   4.230  
   4.231 +val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
   4.232 +  {const_name_of = annotated_function_name_of,
   4.233 +  funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
   4.234 +  additional_arguments = K [],
   4.235 +  wrap_compilation =
   4.236 +    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   4.237 +      mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation,
   4.238 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   4.239 +  }
   4.240 +
   4.241  val add_equations = gen_add_equations
   4.242    (Steps {infer_modes = infer_modes,
   4.243    create_definitions = create_definitions,
   4.244 @@ -2326,6 +2385,15 @@
   4.245    are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
   4.246    qname = "depth_limited_equation"})
   4.247  
   4.248 +val add_annotated_equations = gen_add_equations
   4.249 +  (Steps {infer_modes = infer_modes,
   4.250 +  create_definitions = create_definitions_of_annotated_functions,
   4.251 +  compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns,
   4.252 +  prove = prove_by_skip,
   4.253 +  add_code_equations = K (K (K I)),
   4.254 +  are_not_defined = fn thy => forall (null o annotated_modes_of thy),
   4.255 +  qname = "annotated_equation"})
   4.256 +
   4.257  val add_quickcheck_equations = gen_add_equations
   4.258    (Steps {infer_modes = infer_modes_with_generator,
   4.259    create_definitions = random_create_definitions,
   4.260 @@ -2392,6 +2460,8 @@
   4.261              add_quickcheck_equations options [const])
   4.262             else if is_depth_limited options then
   4.263               add_depth_limited_equations options [const]
   4.264 +           else if is_annotated options then
   4.265 +             add_annotated_equations options [const]
   4.266             else
   4.267               add_equations options [const]))
   4.268        end
   4.269 @@ -2409,7 +2479,7 @@
   4.270  
   4.271  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
   4.272  (* TODO: *)
   4.273 -fun analyze_compr thy compfuns (depth_limit, random) t_compr =
   4.274 +fun analyze_compr thy compfuns (depth_limit, (random, annotated)) t_compr =
   4.275    let
   4.276      val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
   4.277        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
   4.278 @@ -2437,8 +2507,11 @@
   4.279        | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d]
   4.280      val comp_modifiers =
   4.281        case depth_limit of NONE => 
   4.282 -      (if random then random_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
   4.283 -    val mk_fun_of = if random then mk_generator_of else
   4.284 +      (if random then random_comp_modifiers else
   4.285 +       if annotated then annotated_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
   4.286 +    val mk_fun_of =
   4.287 +      if random then mk_generator_of else
   4.288 +      if annotated then mk_annotated_fun_of else
   4.289        if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of
   4.290      val t_pred = compile_expr comp_modifiers compfuns thy
   4.291        (m, list_comb (pred, params)) inargs additional_arguments;
   4.292 @@ -2457,7 +2530,7 @@
   4.293        in mk_map compfuns T_pred T_compr arrange t_pred end
   4.294    in t_eval end;
   4.295  
   4.296 -fun eval thy (options as (depth_limit, random)) t_compr =
   4.297 +fun eval thy (options as (depth_limit, (random, annotated))) t_compr =
   4.298    let
   4.299      val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns
   4.300      val t = analyze_compr thy compfuns options t_compr;
   4.301 @@ -2510,8 +2583,10 @@
   4.302    let
   4.303      val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
   4.304      val random = Scan.optional (Args.$$$ "random" >> K true) false
   4.305 +    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
   4.306    in
   4.307 -    Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false)
   4.308 +    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
   4.309 +      (NONE, (false, false))
   4.310    end
   4.311  
   4.312  val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
     5.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 05 14:47:27 2009 +0100
     5.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
     5.3 @@ -247,13 +247,15 @@
     5.4      "append [] xs xs"
     5.5    | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
     5.6  
     5.7 -code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
     5.8 +(*code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .*)
     5.9  code_pred [depth_limited] append .
    5.10 -code_pred [random] append .
    5.11 +(*code_pred [random] append .*)
    5.12 +code_pred [annotated] append .
    5.13  
    5.14 -thm append.equation
    5.15 +(*thm append.equation
    5.16  thm append.depth_limited_equation
    5.17 -thm append.random_equation
    5.18 +thm append.random_equation*)
    5.19 +thm append.annotated_equation
    5.20  
    5.21  values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
    5.22  values "{zs. append [0, Suc 0, 2] [17, 8] zs}"