--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 06 17:52:57 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 06 19:02:36 2009 +0100
@@ -6,9 +6,11 @@
signature PREDICATE_COMPILE_CORE =
sig
- val setup: theory -> theory
- val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
- val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+ val setup : theory -> theory
+ val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+ val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+ val values_cmd : string list -> Predicate_Compile_Aux.smode option list option
+ -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
val register_predicate : (string * thm list * thm * int) -> theory -> theory
val register_intros : string * thm list -> theory -> theory
val is_registered : theory -> string -> bool
@@ -19,20 +21,21 @@
val modes_of: theory -> string -> Predicate_Compile_Aux.mode list
val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
- val generator_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
- val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
+ val random_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
+ val random_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
- val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
- val intros_of: theory -> string -> thm list
- val nparams_of: theory -> string -> int
- val add_intro: thm -> theory -> theory
- val set_elim: thm -> theory -> theory
+ val all_random_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
+ val intros_of : theory -> string -> thm list
+ val nparams_of : theory -> string -> int
+ val add_intro : thm -> theory -> theory
+ val set_elim : thm -> theory -> theory
val set_nparams : string -> int -> theory -> theory
- val print_stored_rules: theory -> unit
- val print_all_modes: theory -> unit
+ val print_stored_rules : theory -> unit
+ val print_all_modes : theory -> unit
val mk_casesrule : Proof.context -> term -> int -> thm list -> term
val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
- val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref
+ val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
+ option Unsynchronized.ref
val code_pred_intros_attrib : attribute
(* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
@@ -51,7 +54,9 @@
val randompred_compfuns : compilation_funs
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 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 +121,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 *)
@@ -197,17 +206,22 @@
intros : thm list,
elim : thm option,
nparams : int,
- functions : (mode * predfun_data) list,
- generators : (mode * function_data) list,
- depth_limited_functions : (mode * function_data) list
+ functions : bool * (mode * predfun_data) list,
+ random_functions : bool * (mode * function_data) list,
+ depth_limited_functions : bool * (mode * function_data) list,
+ annotated_functions : bool * (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, random_functions, 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, random_functions = random_functions,
+ depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions}
+fun map_pred_data f (PredData {intros, elim, nparams,
+ functions, random_functions, depth_limited_functions, annotated_functions}) =
+ mk_pred_data (f ((intros, elim, nparams), (functions, random_functions,
+ depth_limited_functions, annotated_functions)))
fun eq_option eq (NONE, NONE) = true
| eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -250,22 +264,19 @@
val nparams_of = #nparams oo the_pred_data
-val modes_of = (map fst) o #functions oo the_pred_data
+val modes_of = (map fst) o snd o #functions oo the_pred_data
-val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data
-
-val random_modes_of = (map fst) o #generators oo the_pred_data
-
fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy)
-val is_compiled = not o null o #functions oo the_pred_data
+val defined_functions = fst o #functions oo the_pred_data
fun lookup_predfun_data thy name mode =
- Option.map rep_predfun_data (AList.lookup (op =)
- (#functions (the_pred_data thy name)) mode)
+ Option.map rep_predfun_data
+ (AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode)
fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
- of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
+ of NONE => error ("No function defined for mode " ^ string_of_mode mode ^
+ " of predicate " ^ name)
| SOME data => data;
val predfun_name_of = #name ooo the_predfun_data
@@ -276,31 +287,54 @@
val predfun_elim_of = #elim ooo the_predfun_data
-fun lookup_generator_data thy name mode =
- Option.map rep_function_data (AList.lookup (op =)
- (#generators (the_pred_data thy name)) mode)
+fun lookup_random_function_data thy name mode =
+ Option.map rep_function_data
+ (AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode)
-fun the_generator_data thy name mode = case lookup_generator_data thy name mode
- of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
+fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of
+ NONE => error ("No random function defined for mode " ^ string_of_mode mode ^
+ " of predicate " ^ name)
| SOME data => data
-val generator_name_of = #name ooo the_generator_data
+val random_function_name_of = #name ooo the_random_function_data
+
+val random_modes_of = (map fst) o snd o #random_functions oo the_pred_data
-val generator_modes_of = (map fst) o #generators oo the_pred_data
+val defined_random_functions = fst o #random_functions oo the_pred_data
-fun all_generator_modes_of thy =
- map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy)
+fun all_random_modes_of thy =
+ map (fn name => (name, random_modes_of thy name)) (all_preds_of thy)
fun lookup_depth_limited_function_data thy name mode =
- Option.map rep_function_data (AList.lookup (op =)
- (#depth_limited_functions (the_pred_data thy name)) mode)
+ Option.map rep_function_data
+ (AList.lookup (op =) (snd (#depth_limited_functions (the_pred_data thy name))) mode)
+
+fun the_depth_limited_function_data thy name mode =
+ case lookup_depth_limited_function_data thy name mode of
+ NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode
+ ^ " of predicate " ^ name)
+ | SOME data => data
+
+val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
-fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode
- of NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode
+val depth_limited_modes_of = (map fst) o snd o #depth_limited_functions oo the_pred_data
+
+val defined_depth_limited_functions = fst o #depth_limited_functions oo the_pred_data
+
+fun lookup_annotated_function_data thy name mode =
+ Option.map rep_function_data
+ (AList.lookup (op =) (snd (#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 depth_limited_function_name_of = #name ooo the_depth_limited_function_data
+val annotated_function_name_of = #name ooo the_annotated_function_data
+
+val annotated_modes_of = (map fst) o snd o #annotated_functions oo the_pred_data
+
+val defined_annotated_functions = fst o #annotated_functions oo the_pred_data
(* diagnostic display functions *)
@@ -555,6 +589,16 @@
fun expand_tuples_elim th = th
+(* updaters *)
+
+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 appair f g (x, y) = (f x, g x)
+
+val no_compilation = ((false, []), (false, []), (false, []), (false, []))
+
fun fetch_pred_data thy name =
case try (Inductive.the_inductive (ProofContext.init thy)) name of
SOME (info as (_, result)) =>
@@ -576,19 +620,13 @@
(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), ([], [], []))
- end
+ mk_pred_data ((intros, SOME elim, nparams), no_compilation)
+ 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 add_predfun name mode data =
let
- val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data)
+ val add = (apsnd o apfst4) (fn (x, y) => (true, cons (mode, mk_predfun_data data) y))
in PredData.map (Graph.map_node name (map_pred_data add)) end
fun is_inductive_predicate thy name =
@@ -599,7 +637,8 @@
val intros = (#intros o rep_pred_data) value
in
fold Term.add_const_names (map Thm.prop_of intros) []
- |> filter (fn c => (not (c = key)) andalso (is_inductive_predicate thy c orelse is_registered thy c))
+ |> filter (fn c => (not (c = key)) andalso
+ (is_inductive_predicate thy c orelse is_registered thy c))
end;
@@ -637,8 +676,9 @@
(apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr
| 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;
+ 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), no_compilation)) gr end;
in PredData.map cons_intro thy end
fun set_elim thm = let
@@ -659,7 +699,8 @@
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), no_compilation))) thy
else thy
end
@@ -679,16 +720,24 @@
(mk_casesrule (ProofContext.init thy) pred nparams pre_intros)
in register_predicate (constname, pre_intros, pre_elim, nparams) thy end
-fun set_generator_name pred mode name =
+fun set_random_function_name pred mode name =
let
- val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
+ val set = (apsnd o apsnd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
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) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
+ 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)
+ (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
in
PredData.map (Graph.map_node pred (map_pred_data set))
end
@@ -715,19 +764,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
@@ -815,9 +851,9 @@
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
(T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
-val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot,
- mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- mk_map = mk_map};
+val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_not = mk_not, mk_map = mk_map};
end;
(* for external use with interactive mode *)
@@ -829,25 +865,41 @@
val T = dest_randomT (fastype_of random)
in
Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} -->
- HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
RandomPredCompFuns.mk_randompredT T) $ random
end;
+(* function types and names of different compilations *)
+
+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 depth_limited_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 SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs
+ val paramTs' =
+ map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs
in
(paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}])
---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
- end;
+ end;
-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)
-
-fun mk_generator_of compfuns thy (name, T) mode =
- Const (generator_name_of thy name mode, depth_limited_funT_of compfuns mode T)
+fun random_function_funT_of (iss, is) T =
+ let
+ val Ts = binder_types T
+ val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
+ val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs
+ in
+ (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
+ (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
+ end
(* Mode analysis *)
@@ -860,7 +912,8 @@
fun check t = (case strip_comb t of
(Free _, []) => true
| (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
- (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
+ (SOME (i, Tname), Type (Tname', _)) =>
+ length ts = i andalso Tname = Tname' andalso forall check ts
| _ => false)
| _ => false)
in check end;
@@ -993,11 +1046,14 @@
(filter_out (equal p) ps)
| _ =>
let
- val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) |> sort (int_ord o (pairself length))
+ val all_generator_vs = all_subsets (subtract (op =) vs prem_vs)
+ |> sort (int_ord o (pairself length))
in
case (find_first (fn generator_vs => is_some
- (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of
- SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
+ (select_mode_prem thy modes' (union (op =) vs generator_vs) ps))
+ all_generator_vs) of
+ SOME generator_vs => check_mode_prems
+ ((map (generator vTs) generator_vs) @ acc_ps)
(union (op =) vs generator_vs) ps
| NONE => NONE
end)
@@ -1073,14 +1129,14 @@
let
val prednames = map fst clauses
val extra_modes' = all_modes_of thy
- val gen_modes = all_generator_modes_of thy
+ val gen_modes = all_random_modes_of thy
|> filter_out (fn (name, _) => member (op =) prednames name)
val starting_modes = remove_from extra_modes' all_modes
fun eq_mode (m1, m2) = (m1 = m2)
val modes =
fixp (fn modes =>
- map (check_modes_pred options true thy param_vs clauses extra_modes' (gen_modes @ modes)) modes)
- starting_modes
+ map (check_modes_pred options true thy param_vs clauses extra_modes'
+ (gen_modes @ modes)) modes) starting_modes
in
AList.join (op =)
(fn _ => fn ((mps1, mps2)) =>
@@ -1169,7 +1225,9 @@
datatype comp_modifiers = Comp_Modifiers of
{
- const_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string,
+ function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string,
+ set_function_name : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory,
+ function_name_prefix : string,
funT_of : compilation_funs -> mode -> typ -> typ,
additional_arguments : string list -> term list,
wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
@@ -1178,7 +1236,9 @@
fun dest_comp_modifiers (Comp_Modifiers c) = c
-val const_name_of = #const_name_of o dest_comp_modifiers
+val function_name_of = #function_name_of o dest_comp_modifiers
+val set_function_name = #set_function_name o dest_comp_modifiers
+val function_name_prefix = #function_name_prefix o dest_comp_modifiers
val funT_of = #funT_of o dest_comp_modifiers
val additional_arguments = #additional_arguments o dest_comp_modifiers
val wrap_compilation = #wrap_compilation o dest_comp_modifiers
@@ -1200,7 +1260,8 @@
| map_params t = t
in map_aterms map_params arg end
-fun compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy eqs eqs' out_ts success_t =
+fun compile_match compilation_modifiers compfuns additional_arguments
+ param_vs iss thy eqs eqs' out_ts success_t =
let
val eqs'' = maps mk_eq eqs @ eqs'
val eqs'' =
@@ -1243,7 +1304,7 @@
val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
val f' =
case f of
- Const (name, T) => Const (Comp_Mod.const_name_of compilation_modifiers thy name mode,
+ Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode,
Comp_Mod.funT_of compilation_modifiers compfuns mode T)
| Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T)
| _ => error ("PredicateCompiler: illegal parameter term")
@@ -1251,23 +1312,26 @@
list_comb (f', params' @ args')
end
-fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments =
+fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t)
+ inargs additional_arguments =
case strip_comb t of
(Const (name, T), params) =>
let
val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
- (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*)
- val name' = Comp_Mod.const_name_of compilation_modifiers thy name mode
+ val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode
val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T
in
(list_comb (Const (name', T'), params' @ inargs @ additional_arguments))
end
| (Free (name, T), params) =>
- list_comb (Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments)
+ list_comb (Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T),
+ params @ inargs @ additional_arguments)
-fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments (iss, is) inp (ts, moded_ps) =
+fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments
+ (iss, is) inp (ts, moded_ps) =
let
- val compile_match = compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy
+ val compile_match = compile_match compilation_modifiers compfuns
+ additional_arguments param_vs iss thy
fun check_constrt t (names, eqs) =
if is_constrt thy t then (t, (names, eqs)) else
let
@@ -1302,10 +1366,11 @@
Prem (us, t) =>
let
val (in_ts, out_ts''') = split_smode is us;
- val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
- thy param_vs iss) in_ts
+ val in_ts = map (compile_arg compilation_modifiers compfuns
+ additional_arguments thy param_vs iss) in_ts
val u =
- compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments'
+ compile_expr compilation_modifiers compfuns thy
+ (mode, t) in_ts additional_arguments'
val rest = compile_prems out_ts''' vs' names'' ps
in
(u, rest)
@@ -1313,10 +1378,11 @@
| Negprem (us, t) =>
let
val (in_ts, out_ts''') = split_smode is us
- val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
- thy param_vs iss) in_ts
+ val in_ts = map (compile_arg compilation_modifiers compfuns
+ additional_arguments thy param_vs iss) in_ts
val u = mk_not compfuns
- (compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments')
+ (compile_expr compilation_modifiers compfuns thy
+ (mode, t) in_ts additional_arguments')
val rest = compile_prems out_ts''' vs' names'' ps
in
(u, rest)
@@ -1351,12 +1417,14 @@
val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
val (Us1, Us2) = split_smodeT (snd mode) Ts2
val Ts1' =
- map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1
+ map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is))
+ (fst mode) Ts1
fun mk_input_term (i, NONE) =
[Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
| mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
[] => error "strange unit input"
- | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
+ | [T] => [Free (Name.variant (all_vs @ param_vs)
+ ("x" ^ string_of_int i), nth Ts2 (i - 1))]
| Ts => let
val vnames = Name.variant_list (all_vs @ param_vs)
(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
@@ -1365,16 +1433,18 @@
else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
val in_ts = maps mk_input_term (snd mode)
val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
- val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs)
+ val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
+ (all_vs @ param_vs)
val cl_ts =
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
+ 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)
val fun_const =
- Const (Comp_Mod.const_name_of compilation_modifiers thy s mode,
+ Const (Comp_Mod.function_name_of compilation_modifiers thy s mode,
Comp_Mod.funT_of compilation_modifiers compfuns mode T)
in
HOLogic.mk_Trueprop
@@ -1399,7 +1469,8 @@
val Ts = binder_types (fastype_of pred)
val funtrm = Const (mode_id, funT)
val (Ts1, Ts2) = chop (length iss) Ts;
- val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
+ val Ts1' =
+ map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
val param_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
val params = map Free (param_names ~~ Ts1')
@@ -1440,14 +1511,12 @@
val simprules = [defthm, @{thm eval_pred},
@{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
- val introthm =
- Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm
- (fn _ => unfolddef_tac)
+ val introthm = Goal.prove (ProofContext.init thy)
+ (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
- val elimthm =
- Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm
- (fn _ => unfolddef_tac)
+ val elimthm = Goal.prove (ProofContext.init thy)
+ (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
in
(introthm, elimthm)
end;
@@ -1455,7 +1524,8 @@
fun create_constname_of_mode thy prefix name mode =
let
fun string_of_mode mode = if null mode then "0"
- else space_implode "_" (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
+ else space_implode "_"
+ (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
^ space_implode "p" (map string_of_int pis)) mode)
val HOmode = space_implode "_and_"
(fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
@@ -1529,7 +1599,9 @@
val xin = Free (name_in, HOLogic.mk_tupleT Tins)
val xout = Free (name_out, HOLogic.mk_tupleT Touts)
val xarg = mk_arg xin xout pis T
- in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
+ in
+ (((if null Tins then [] else [xin],
+ if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
end
val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
val (xinout, xargs) = split_list xinoutargs
@@ -1563,46 +1635,22 @@
fold create_definition modes thy
end;
-fun create_definitions_of_depth_limited_functions preds (name, modes) thy =
+fun define_functions comp_modifiers compfuns 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 "depth_limited_" name mode
- val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T
+ val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
+ val mode_cname = create_constname_of_mode thy function_name_prefix name mode
+ val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T
in
thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
- |> set_depth_limited_function_name name mode mode_cname
+ |> Comp_Mod.set_function_name comp_modifiers name mode mode_cname
end;
in
fold create_definition modes thy
end;
-fun generator_funT_of (iss, is) T =
- let
- val Ts = binder_types T
- val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
- val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs
- in
- (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
- (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
- end
-
-fun random_create_definitions 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 "gen_" name mode
- val funT = generator_funT_of mode T
- in
- thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
- |> set_generator_name name mode mode_cname
- end;
- in
- fold create_definition modes thy
- end;
-
(* Proving equivalence of term *)
fun is_Type (Type _) = true
@@ -1752,7 +1800,8 @@
in
rtac @{thm bindI} 1
THEN (if (is_some name) then
- simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1
+ simp_tac (HOL_basic_ss addsimps
+ [predfun_definition_of thy (the name) (iss, is)]) 1
THEN rtac @{thm not_predI} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
THEN (REPEAT_DETERM (atac 1))
@@ -1823,14 +1872,16 @@
THEN (print_tac "after splitting with split_asm rules")
(* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
- THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
+ THEN (REPEAT_DETERM_N (num_of_constrs - 1)
+ (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
THEN (assert_tac (Max_number_of_subgoals 2))
THEN (EVERY (map split_term_tac ts))
end
else all_tac
in
split_term_tac (HOLogic.mk_tuple out_ts)
- THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
+ THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
+ THEN (etac @{thm botE} 2))))
end
(* VERY LARGE SIMILIRATIY to function prove_param
@@ -1910,7 +1961,8 @@
THEN (print_tac "state before assumption matching")
THEN (REPEAT (atac 1 ORELSE
(CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
- [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
+ [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
+ @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
THEN print_tac "state after simp_tac:"))))
| prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
let
@@ -1932,7 +1984,8 @@
print_tac "before neg prem 2"
THEN etac @{thm bindE} 1
THEN (if is_some name then
- full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1
+ full_simp_tac (HOL_basic_ss addsimps
+ [predfun_definition_of thy (the name) (iss, is)]) 1
THEN etac @{thm not_predE} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params)))
@@ -2027,9 +2080,10 @@
fun dest_prem thy params t =
(case strip_comb t of
(v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
- | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of
+ | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of
Prem (ts, t) => Negprem (ts, t)
- | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t)))
+ | Negprem _ => error ("Double negation not allowed in premise: " ^
+ Syntax.string_of_term_global thy (c $ t))
| Sidecond t => Sidecond (c $ t))
| (c as Const (s, _), ts) =>
if is_registered thy s then
@@ -2044,14 +2098,17 @@
val nparams = nparams_of thy (hd prednames)
val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
val (preds, intrs) = unify_consts thy preds intrs
- val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy)
+ val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
+ (ProofContext.init thy)
val preds = map dest_Const preds
- val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
+ val extra_modes = all_modes_of thy
+ |> filter_out (fn (name, _) => member (op =) prednames name)
val params = case intrs of
[] =>
let
val (paramTs, _) = chop nparams (binder_types (snd (hd preds)))
- val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) (1 upto length paramTs))
+ val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
+ (1 upto length paramTs))
in map Free (param_names ~~ paramTs) end
| intr :: _ => fst (chop nparams
(snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)))))
@@ -2087,12 +2144,13 @@
[] => [(i + 1, NONE)]
| [U] => [(i + 1, NONE)]
| Us => (i + 1, NONE) ::
- (map (pair (i + 1) o SOME) (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us)))))
+ (map (pair (i + 1) o SOME)
+ (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us)))))
Ts)
in
cprod (cprods (map (fn T => case strip_type T of
- (Rs as _ :: _, Type ("bool", [])) => map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts),
- all_smodes_of_typs Us)
+ (Rs as _ :: _, Type ("bool", [])) =>
+ map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us)
end
val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds
in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
@@ -2180,7 +2238,7 @@
{
compile_preds : theory -> string list -> string list -> (string * typ) list
-> (moded_clause list) pred_mode_table -> term pred_mode_table,
- create_definitions: (string * typ) list -> string * mode list -> theory -> theory,
+ define_functions : (string * typ) list -> string * mode list -> theory -> theory,
infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
-> string list -> (string * (term list * indprem list) list) list
-> moded_clause list pred_mode_table,
@@ -2189,7 +2247,7 @@
-> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
add_code_equations : theory -> int -> (string * typ) list
-> (string * thm list) list -> (string * thm list) list,
- are_not_defined : theory -> string list -> bool,
+ defined : theory -> string -> bool,
qname : bstring
}
@@ -2197,19 +2255,21 @@
fun add_equations_of steps options prednames thy =
let
fun dest_steps (Steps s) = s
- val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+ val _ = print_step options
+ ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
(*val _ = check_intros_elim_match thy prednames*)
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
prepare_intrs thy prednames (maps (intros_of thy) prednames)
val _ = print_step options "Infering modes..."
- val moded_clauses = #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
+ val moded_clauses =
+ #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = check_expected_modes options modes
val _ = print_modes options modes
(*val _ = print_moded_clauses thy moded_clauses*)
val _ = print_step options "Defining executable functions..."
- val thy' = fold (#create_definitions (dest_steps steps) preds) modes thy
+ val thy' = fold (#define_functions (dest_steps steps) preds) modes thy
|> Theory.checkpoint
val _ = print_step options "Compiling equations..."
val compiled_terms =
@@ -2236,7 +2296,8 @@
val (G', v) = case try (Graph.get_node G) key of
SOME v => (G, v)
| NONE => (Graph.new_node (key, value_of key) G, value_of key)
- val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v)))
+ val (G'', visited') = fold (extend' value_of edges_of)
+ (subtract (op =) visited (edges_of (key, v)))
(G', key :: visited)
in
(fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
@@ -2247,22 +2308,26 @@
fun gen_add_equations steps options names thy =
let
fun dest_steps (Steps s) = s
- val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
+ val thy' = thy
+ |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names)
|> Theory.checkpoint;
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
val scc = strong_conn_of (PredData.get thy') names
val thy'' = fold_rev
(fn preds => fn thy =>
- if #are_not_defined (dest_steps steps) thy preds then
- add_equations_of steps options preds thy else thy)
+ if not (forall (#defined (dest_steps steps) thy) preds) then
+ add_equations_of steps options preds thy
+ else thy)
scc thy' |> Theory.checkpoint
in thy'' end
(* different instantiantions of the predicate compiler *)
val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
- {const_name_of = predfun_name_of : (theory -> string -> mode -> string),
+ {function_name_of = predfun_name_of : (theory -> string -> mode -> string),
+ set_function_name = (fn _ => fn _ => fn _ => I),
+ function_name_prefix = "",
funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = K [],
wrap_compilation = K (K (K (K (K I))))
@@ -2271,8 +2336,10 @@
}
val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
- {const_name_of = depth_limited_function_name_of,
+ {function_name_of = depth_limited_function_name_of,
+ set_function_name = set_depth_limited_function_name,
funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ),
+ function_name_prefix = "depth_limited_",
additional_arguments = fn names =>
let
val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"]
@@ -2289,7 +2356,8 @@
in
if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
$ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T')
- $ (if full_mode then mk_single compfuns HOLogic.unit else Const (@{const_name undefined}, T')))
+ $ (if full_mode then mk_single compfuns HOLogic.unit else
+ Const (@{const_name undefined}, T')))
$ compilation
end,
transform_additional_arguments =
@@ -2304,39 +2372,62 @@
}
val random_comp_modifiers = Comp_Mod.Comp_Modifiers
- {const_name_of = generator_name_of,
- funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ),
+ {function_name_of = random_function_name_of,
+ set_function_name = set_random_function_name,
+ function_name_prefix = "random",
+ funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
+val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {function_name_of = annotated_function_name_of,
+ set_function_name = set_annotated_function_name,
+ function_name_prefix = "annotated",
+ 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,
+ define_functions = create_definitions,
compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns,
prove = prove,
add_code_equations = add_code_equations,
- are_not_defined = fn thy => forall (null o modes_of thy),
+ defined = defined_functions,
qname = "equation"})
val add_depth_limited_equations = gen_add_equations
(Steps {infer_modes = infer_modes,
- create_definitions = create_definitions_of_depth_limited_functions,
+ define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns,
compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
prove = prove_by_skip,
add_code_equations = K (K (K I)),
- are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
+ defined = defined_depth_limited_functions,
qname = "depth_limited_equation"})
+val add_annotated_equations = gen_add_equations
+ (Steps {infer_modes = infer_modes,
+ define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns,
+ compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns,
+ prove = prove_by_skip,
+ add_code_equations = K (K (K I)),
+ defined = defined_annotated_functions,
+ qname = "annotated_equation"})
+
val add_quickcheck_equations = gen_add_equations
(Steps {infer_modes = infer_modes_with_generator,
- create_definitions = random_create_definitions,
+ define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns,
compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
prove = prove_by_skip,
add_code_equations = K (K (K I)),
- are_not_defined = fn thy => forall (null o random_modes_of thy),
+ defined = defined_random_functions,
qname = "random_equation"})
(** user interface **)
@@ -2396,6 +2487,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,11 +2502,12 @@
(* transformation for code generation *)
val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
-val random_eval_ref = Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
+val random_eval_ref =
+ Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
-(* TODO: *)
-fun analyze_compr thy compfuns (depth_limit, random) t_compr =
+(* TODO: make analyze_compr generic with respect to the compilation modifiers*)
+fun analyze_compr thy compfuns param_user_modes (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);
@@ -2424,9 +2518,17 @@
(fn (i, t) => case t of Bound j => if j < length Ts then NONE
else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
val user_mode' = map (rpair NONE) user_mode
- val all_modes_of = if random then all_generator_modes_of else all_modes_of
- (*val compile_expr = if random then compile_gen_expr else compile_expr*)
- val modes = filter (fn Mode (_, is, _) => is = user_mode')
+ val all_modes_of = if random then all_random_modes_of else all_modes_of
+ fun fits_to is NONE = true
+ | fits_to is (SOME pm) = (is = pm)
+ fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) =
+ fits_to is pm andalso valid (ms @ ms') pms
+ | valid (NONE :: ms') pms = valid ms' pms
+ | valid [] [] = true
+ | valid [] _ = error "Too many mode annotations"
+ | valid (SOME _ :: _) [] = error "Not enough mode annotations"
+ val modes = filter (fn Mode (_, is, ms) => is = user_mode'
+ andalso (the_default true (Option.map (valid ms) param_user_modes)))
(modes_of_term (all_modes_of thy) (list_comb (pred, params)));
val m = case modes
of [] => error ("No mode possible for comprehension "
@@ -2440,10 +2542,11 @@
NONE => (if random then [@{term "5 :: code_numeral"}] else [])
| 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 (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of
+ case depth_limit of
+ NONE =>
+ (if random then random_comp_modifiers else
+ if annotated then annotated_comp_modifiers else predicate_comp_modifiers)
+ | SOME _ => depth_limited_comp_modifiers
val t_pred = compile_expr comp_modifiers compfuns thy
(m, list_comb (pred, params)) inargs additional_arguments;
val t_eval = if null outargs then t_pred else
@@ -2461,10 +2564,10 @@
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 param_user_modes (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;
+ val t = analyze_compr thy compfuns param_user_modes options t_compr;
val T = dest_predT compfuns (fastype_of t);
val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
val eval =
@@ -2476,15 +2579,16 @@
Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
in (T, eval) end;
-fun values ctxt options k t_compr =
+fun values ctxt param_user_modes options k t_compr =
let
val thy = ProofContext.theory_of ctxt;
- val (T, ts) = eval thy options t_compr;
+ val (T, ts) = eval thy param_user_modes options t_compr;
val (ts, _) = Predicate.yieldn k ts;
val setT = HOLogic.mk_setT T;
val elemsT = HOLogic.mk_set T ts;
+ val cont = Free ("...", setT)
in if k = ~1 orelse length ts < k then elemsT
- else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+ else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont
end;
(*
fun random_values ctxt k t =
@@ -2494,35 +2598,16 @@
in
end;
*)
-fun values_cmd modes options k raw_t state =
+fun values_cmd print_modes param_user_modes options k raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
- val t' = values ctxt options k t;
+ val t' = values ctxt param_user_modes options k t;
val ty' = Term.type_of t';
val ctxt' = Variable.auto_fixes t' ctxt;
- val p = PrintMode.with_modes modes (fn () =>
+ val p = PrintMode.with_modes print_modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
-local structure P = OuterParse in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val options =
- let
- val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
- val random = Scan.optional (Args.$$$ "random" >> K true) false
- in
- Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false)
- end
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
- (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term
- >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
- (values_cmd modes options k t)));
-
end;
-
-end;