--- 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