# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 3b275a0bf18c23edb7a799404417399f3e2c598f
# Parent  181fae134b434afb9d9854132e7b705052582e43
adding tracing function for evaluated code; annotated compilation in the predicate compiler

diff -r 181fae134b43 -r 3b275a0bf18c src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -243,6 +243,26 @@
 hide const dummy_term App valapp
 hide (open) const Const termify valtermify term_of term_of_num
 
+subsection {* Tracing of generated and evaluated code *}
+
+definition tracing :: "String.literal => 'a => 'a"
+where
+  [code del]: "tracing s x = x"
+
+ML {*
+structure Code_Evaluation =
+struct
+
+fun tracing s x = (Output.tracing s; x)
+
+end
+*}
+
+code_const "tracing :: String.literal => 'a => 'a"
+  (Eval "Code'_Evaluation.tracing")
+
+hide (open) const tracing
+code_reserved Eval Code_Evaluation
 
 subsection {* Evaluation setup *}
 
diff -r 181fae134b43 -r 3b275a0bf18c src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -121,7 +121,8 @@
       skip_proof = chk "skip_proof",
       inductify = chk "inductify",
       random = chk "random",
-      depth_limited = chk "depth_limited"
+      depth_limited = chk "depth_limited",
+      annotated = chk "annotated"
     }
   end
 
@@ -149,7 +150,8 @@
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
-  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"]
+  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
+  "annotated"]
 
 local structure P = OuterParse
 in
diff -r 181fae134b43 -r 3b275a0bf18c src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -170,7 +170,8 @@
 
   inductify : bool,
   random : bool,
-  depth_limited : bool
+  depth_limited : bool,
+  annotated : bool
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
@@ -185,6 +186,7 @@
 fun is_inductify (Options opt) = #inductify opt
 fun is_random (Options opt) = #random opt
 fun is_depth_limited (Options opt) = #depth_limited opt
+fun is_annotated (Options opt) = #annotated opt
 
 val default_options = Options {
   expected_modes = NONE,
@@ -198,7 +200,8 @@
   
   inductify = false,
   random = false,
-  depth_limited = false
+  depth_limited = false,
+  annotated = false
 }
 
 
diff -r 181fae134b43 -r 3b275a0bf18c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -52,6 +52,7 @@
   val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val mk_tracing : string -> term -> term
 end;
 
 structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
@@ -116,6 +117,10 @@
   Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
 
+fun mk_tracing s t =
+  Const(@{const_name Code_Evaluation.tracing},
+    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
+
 (* destruction of intro rules *)
 
 (* FIXME: look for other place where this functionality was used before *)
@@ -198,16 +203,21 @@
   elim : thm option,
   nparams : int,
   functions : (mode * predfun_data) list,
-  generators : (mode * function_data) list,
-  depth_limited_functions : (mode * function_data) list 
+  generators : (mode * function_data) list, (*TODO: maybe rename to random_functions *)
+  depth_limited_functions : (mode * function_data) list,
+  annotated_functions : (mode * function_data) list
 };
 
 fun rep_pred_data (PredData data) = data;
-fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) =
+fun mk_pred_data ((intros, elim, nparams),
+  (functions, generators, depth_limited_functions, annotated_functions)) =
   PredData {intros = intros, elim = elim, nparams = nparams,
-    functions = functions, generators = generators, depth_limited_functions = depth_limited_functions}
-fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) =
-  mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions)))
+    functions = functions, generators = generators,
+    depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions}
+fun map_pred_data f (PredData {intros, elim, nparams,
+  functions, generators, depth_limited_functions, annotated_functions}) =
+  mk_pred_data (f ((intros, elim, nparams), (functions, generators,
+    depth_limited_functions, annotated_functions)))
 
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -302,6 +312,19 @@
 
 val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
 
+fun lookup_annotated_function_data thy name mode =
+  Option.map rep_function_data (AList.lookup (op =)
+  (#annotated_functions (the_pred_data thy name)) mode)
+
+fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode
+  of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode
+    ^ " of predicate " ^ name)
+   | SOME data => data
+
+val annotated_modes_of = (map fst) o #annotated_functions oo the_pred_data
+
+val annotated_function_name_of = #name ooo the_annotated_function_data
+
 (* diagnostic display functions *)
 
 fun print_modes options modes =
@@ -576,19 +599,20 @@
           (mk_casesrule (ProofContext.init thy) pred nparams intros)
         val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)
       in
-        mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
+        mk_pred_data ((intros, SOME elim, nparams), ([], [], [], []))
       end                                                                    
   | NONE => error ("No such predicate: " ^ quote name)
 
 (* updaters *)
 
-fun apfst3 f (x, y, z) =  (f x, y, z)
-fun apsnd3 f (x, y, z) =  (x, f y, z)
-fun aptrd3 f (x, y, z) =  (x, y, f z)
+fun apfst4 f (x1, x2, x3, x4) = (f x1, x2, x3, x4)
+fun apsnd4 f (x1, x2, x3, x4) = (x1, f x2, x3, x4)
+fun aptrd4 f (x1, x2, x3, x4) = (x1, x2, f x3, x4)
+fun apfourth4 f (x1, x2, x3, x4) = (x1, x2, x3, f x4)
 
 fun add_predfun name mode data =
   let
-    val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data)
+    val add = (apsnd o apfst4 o cons) (mode, mk_predfun_data data)
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate thy name =
@@ -638,7 +662,7 @@
      | NONE =>
        let
          val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
-       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end;
+       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], [], []))) gr end;
   in PredData.map cons_intro thy end
 
 fun set_elim thm = let
@@ -659,7 +683,7 @@
   in
     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
       PredData.map
-        (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
+        (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [], [])))) thy
     else thy
   end
 
@@ -681,14 +705,21 @@
 
 fun set_generator_name pred mode name = 
   let
-    val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
+    val set = (apsnd o apsnd4 o cons) (mode, mk_function_data (name, NONE))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
 
 fun set_depth_limited_function_name pred mode name = 
   let
-    val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
+    val set = (apsnd o aptrd4 o cons) (mode, mk_function_data (name, NONE))
+  in
+    PredData.map (Graph.map_node pred (map_pred_data set))
+  end
+
+fun set_annotated_function_name pred mode name =
+  let
+    val set = (apsnd o apfourth4 o cons) (mode, mk_function_data (name, NONE))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
@@ -715,19 +746,6 @@
 fun mk_not (CompilationFuns funs) = #mk_not funs
 fun mk_map (CompilationFuns funs) = #mk_map funs
 
-fun funT_of compfuns (iss, is) T =
-  let
-    val Ts = binder_types T
-    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
-  in
-    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
-  end;
-
-fun mk_fun_of compfuns thy (name, T) mode = 
-  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
-
-
 structure PredicateCompFuns =
 struct
 
@@ -833,6 +851,8 @@
       RandomPredCompFuns.mk_randompredT T) $ random
   end;
 
+(* function types and names of different compilations *)
+
 fun depth_limited_funT_of compfuns (iss, is) T =
   let
     val Ts = binder_types T
@@ -841,7 +861,22 @@
   in
     (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}])
       ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
-  end;  
+  end;
+
+fun funT_of compfuns (iss, is) T =
+  let
+    val Ts = binder_types T
+    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
+    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
+  in
+    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
+  end;
+
+fun mk_fun_of compfuns thy (name, T) mode = 
+  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
+
+fun mk_annotated_fun_of compfuns thy (name, T) mode =
+  Const (annotated_function_name_of thy name mode, funT_of compfuns mode T)
 
 fun mk_depth_limited_fun_of compfuns thy (name, T) mode =
   Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)
@@ -1370,9 +1405,7 @@
       map (compile_clause compilation_modifiers compfuns
         thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls;
     val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
-      (if null cl_ts then
-        mk_bot compfuns (HOLogic.mk_tupleT Us2)
-      else foldr1 (mk_sup compfuns) cl_ts)
+      (if null cl_ts then mk_bot compfuns (HOLogic.mk_tupleT Us2) else foldr1 (mk_sup compfuns) cl_ts)
     val fun_const =
       Const (Comp_Mod.const_name_of compilation_modifiers thy s mode,
         Comp_Mod.funT_of compilation_modifiers compfuns mode T)
@@ -1598,7 +1631,23 @@
   in
     fold create_definition modes thy
   end;
-  
+
+fun create_definitions_of_annotated_functions preds (name, modes) thy =
+  let
+    val T = AList.lookup (op =) preds name |> the
+    fun create_definition mode thy =
+      let
+        val mode_cname = create_constname_of_mode thy "annotated_" name mode
+        val funT = funT_of PredicateCompFuns.compfuns mode T
+      in
+        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
+        |> set_annotated_function_name name mode mode_cname 
+      end;
+  in
+    fold create_definition modes thy
+  end;
+
+
 (* Proving equivalence of term *)
 
 fun is_Type (Type _) = true
@@ -2308,6 +2357,16 @@
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
 
+val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {const_name_of = annotated_function_name_of,
+  funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
+  additional_arguments = K [],
+  wrap_compilation =
+    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+      mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation,
+  transform_additional_arguments = K I : (indprem -> term list -> term list)
+  }
+
 val add_equations = gen_add_equations
   (Steps {infer_modes = infer_modes,
   create_definitions = create_definitions,
@@ -2326,6 +2385,15 @@
   are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
   qname = "depth_limited_equation"})
 
+val add_annotated_equations = gen_add_equations
+  (Steps {infer_modes = infer_modes,
+  create_definitions = create_definitions_of_annotated_functions,
+  compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns,
+  prove = prove_by_skip,
+  add_code_equations = K (K (K I)),
+  are_not_defined = fn thy => forall (null o annotated_modes_of thy),
+  qname = "annotated_equation"})
+
 val add_quickcheck_equations = gen_add_equations
   (Steps {infer_modes = infer_modes_with_generator,
   create_definitions = random_create_definitions,
@@ -2392,6 +2460,8 @@
             add_quickcheck_equations options [const])
            else if is_depth_limited options then
              add_depth_limited_equations options [const]
+           else if is_annotated options then
+             add_annotated_equations options [const]
            else
              add_equations options [const]))
       end
@@ -2409,7 +2479,7 @@
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 (* TODO: *)
-fun analyze_compr thy compfuns (depth_limit, random) t_compr =
+fun analyze_compr thy compfuns (depth_limit, (random, annotated)) t_compr =
   let
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
@@ -2437,8 +2507,11 @@
       | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d]
     val comp_modifiers =
       case depth_limit of NONE => 
-      (if random then random_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
-    val mk_fun_of = if random then mk_generator_of else
+      (if random then random_comp_modifiers else
+       if annotated then annotated_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
+    val mk_fun_of =
+      if random then mk_generator_of else
+      if annotated then mk_annotated_fun_of else
       if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of
     val t_pred = compile_expr comp_modifiers compfuns thy
       (m, list_comb (pred, params)) inargs additional_arguments;
@@ -2457,7 +2530,7 @@
       in mk_map compfuns T_pred T_compr arrange t_pred end
   in t_eval end;
 
-fun eval thy (options as (depth_limit, random)) t_compr =
+fun eval thy (options as (depth_limit, (random, annotated))) t_compr =
   let
     val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns
     val t = analyze_compr thy compfuns options t_compr;
@@ -2510,8 +2583,10 @@
   let
     val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
     val random = Scan.optional (Args.$$$ "random" >> K true) false
+    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
   in
-    Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false)
+    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
+      (NONE, (false, false))
   end
 
 val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
diff -r 181fae134b43 -r 3b275a0bf18c src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -247,13 +247,15 @@
     "append [] xs xs"
   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+(*code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .*)
 code_pred [depth_limited] append .
-code_pred [random] append .
+(*code_pred [random] append .*)
+code_pred [annotated] append .
 
-thm append.equation
+(*thm append.equation
 thm append.depth_limited_equation
-thm append.random_equation
+thm append.random_equation*)
+thm append.annotated_equation
 
 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"