--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Mar 22 08:30:13 2010 +0100
@@ -20,14 +20,15 @@
| comb_option f (SOME x1, NONE) = SOME x1
| comb_option f (NONE, NONE) = NONE
-fun map2_optional f (x :: xs) (y :: ys) = (f x (SOME y)) :: (map2_optional f xs ys)
+fun map2_optional f (x :: xs) (y :: ys) = f x (SOME y) :: (map2_optional f xs ys)
| map2_optional f (x :: xs) [] = (f x NONE) :: (map2_optional f xs [])
| map2_optional f [] [] = []
fun find_indices f xs =
map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
-fun assert check = if check then () else error "Assertion failed!"
+fun assert check = if check then () else raise Fail "Assertion failed!"
+
(* mode *)
datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
@@ -48,7 +49,7 @@
(* name: binder_modes? *)
fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
| strip_fun_mode Bool = []
- | strip_fun_mode _ = error "Bad mode for strip_fun_mode"
+ | strip_fun_mode _ = raise Fail "Bad mode for strip_fun_mode"
fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode'
| dest_fun_mode mode = [mode]
@@ -67,51 +68,36 @@
else
[Input, Output]
end
- | all_modes_of_typ' (Type ("*", [T1, T2])) =
+ | all_modes_of_typ' (Type (@{type_name "*"}, [T1, T2])) =
map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
| all_modes_of_typ' _ = [Input, Output]
fun all_modes_of_typ (T as Type ("fun", _)) =
- let
- val (S, U) = strip_type T
- in
- if U = HOLogic.boolT then
- fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
- (map all_modes_of_typ' S) [Bool]
- else
- [Input, Output]
- end
- | all_modes_of_typ (Type ("bool", [])) = [Bool]
+ let
+ val (S, U) = strip_type T
+ in
+ if U = @{typ bool} then
+ fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
+ (map all_modes_of_typ' S) [Bool]
+ else
+ [Input, Output]
+ end
+ | all_modes_of_typ @{typ bool} = [Bool]
| all_modes_of_typ T = all_modes_of_typ' T
fun all_smodes_of_typ (T as Type ("fun", _)) =
let
val (S, U) = strip_type T
- fun all_smodes (Type ("*", [T1, T2])) =
+ fun all_smodes (Type (@{type_name "*"}, [T1, T2])) =
map_product (curry Pair) (all_smodes T1) (all_smodes T2)
| all_smodes _ = [Input, Output]
in
if U = HOLogic.boolT then
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool]
else
- error "all_smodes_of_typ: invalid type for predicate"
+ raise Fail "all_smodes_of_typ: invalid type for predicate"
end
-(*
-fun extract_params arg =
- case fastype_of arg of
- (T as Type ("fun", _)) =>
- (if (body_type T = HOLogic.boolT) then
- (case arg of
- Free _ => [arg] | _ => error "extract_params: Unexpected term")
- else [])
- | (Type ("*", [T1, T2])) =>
- let
- val (t1, t2) = HOLogic.dest_prod arg
- in
- extract_params t1 @ extract_params t2
- end
- | _ => []
-*)
+
fun ho_arg_modes_of mode =
let
fun ho_arg_mode (m as Fun _) = [m]
@@ -125,7 +111,7 @@
let
fun ho_arg (Fun _) (SOME t) = [t]
| ho_arg (Fun _) NONE = error "ho_arg_of"
- | ho_arg (Pair (m1, m2)) (SOME (Const ("Pair", _) $ t1 $ t2)) =
+ | ho_arg (Pair (m1, m2)) (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2)
| ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE
| ho_arg _ _ = []
@@ -146,13 +132,13 @@
end
| replace (_, t) hoargs = (t, hoargs)
in
- fst (fold_map replace ((strip_fun_mode mode) ~~ ts) hoargs)
+ fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs)
end
fun ho_argsT_of mode Ts =
let
fun ho_arg (Fun _) T = [T]
- | ho_arg (Pair (m1, m2)) (Type ("*", [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
+ | ho_arg (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
| ho_arg _ _ = []
in
flat (map2 ho_arg (strip_fun_mode mode) Ts)
@@ -172,7 +158,7 @@
| split_arg_mode' m t =
if eq_mode (m, Input) then (SOME t, NONE)
else if eq_mode (m, Output) then (NONE, SOME t)
- else error "split_map_mode: mode and term do not match"
+ else raise Fail "split_map_mode: mode and term do not match"
in
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
end
@@ -181,7 +167,7 @@
fun split_map_modeT f mode Ts =
let
fun split_arg_mode' (m as Fun _) T = f m T
- | split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) =
+ | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
let
val (i1, o1) = split_arg_mode' m1 T1
val (i2, o2) = split_arg_mode' m2 T2
@@ -190,14 +176,14 @@
end
| split_arg_mode' Input T = (SOME T, NONE)
| split_arg_mode' Output T = (NONE, SOME T)
- | split_arg_mode' _ _ = error "split_modeT': mode and type do not match"
+ | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
in
(pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
end
fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
-fun fold_map_aterms_prodT comb f (Type ("*", [T1, T2])) s =
+fun fold_map_aterms_prodT comb f (Type (@{type_name "*"}, [T1, T2])) s =
let
val (x1, s') = fold_map_aterms_prodT comb f T1 s
val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
@@ -215,7 +201,7 @@
fun split_modeT' mode Ts =
let
fun split_arg_mode' (Fun _) T = ([], [])
- | split_arg_mode' (Pair (m1, m2)) (Type ("*", [T1, T2])) =
+ | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name "*"}, [T1, T2])) =
let
val (i1, o1) = split_arg_mode' m1 T1
val (i2, o2) = split_arg_mode' m2 T2
@@ -224,7 +210,7 @@
end
| split_arg_mode' Input T = ([T], [])
| split_arg_mode' Output T = ([], [T])
- | split_arg_mode' _ _ = error "split_modeT': mode and type do not match"
+ | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
in
(pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
end
@@ -296,7 +282,7 @@
val T = (Sign.the_const_type thy constname)
in body_type T = @{typ "bool"} end;
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
+fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
| is_predT _ = false
(*** check if a term contains only constructor functions ***)
@@ -366,7 +352,7 @@
let
val (literals, head) = Logic.strip_horn intro
fun appl t = (case t of
- (@{term "Not"} $ t') => HOLogic.mk_not (f t')
+ (@{term Not} $ t') => HOLogic.mk_not (f t')
| _ => f t)
in
Logic.list_implies
@@ -377,7 +363,7 @@
let
val (literals, head) = Logic.strip_horn intro
fun appl t s = (case t of
- (@{term "Not"} $ t') => f t' s
+ (@{term Not} $ t') => f t' s
| _ => f t s)
in fold appl (map HOLogic.dest_Trueprop literals) s end
@@ -385,7 +371,7 @@
let
val (literals, head) = Logic.strip_horn intro
fun appl t s = (case t of
- (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
+ (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s)
| _ => f t s)
val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
in
@@ -489,7 +475,8 @@
fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
| compilation_for_polarity _ c = c
-fun string_of_compilation c = case c of
+fun string_of_compilation c =
+ case c of
Pred => ""
| Random => "random"
| Depth_Limited => "depth limited"
@@ -589,9 +576,9 @@
(case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
let
- fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
+ fun rewrite_arg' (Const (@{const_name "Pair"}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
- | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
+ | rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
let
val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100
@@ -79,12 +79,12 @@
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
-fun assert b = if not b then error "Assertion failed" else warning "Assertion holds"
+fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
datatype assertion = Max_number_of_subgoals of int
fun assert_tac (Max_number_of_subgoals i) st =
if (nprems_of st <= i) then Seq.single st
- else error ("assert_tac: Numbers of subgoals mismatch at goal state :"
+ else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
^ "\n" ^ Pretty.string_of (Pretty.chunks
(Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
@@ -153,8 +153,8 @@
| mode_of (Term m) = m
| mode_of (Mode_App (d1, d2)) =
(case mode_of d1 of Fun (m, m') =>
- (if eq_mode (m, mode_of d2) then m' else error "mode_of")
- | _ => error "mode_of2")
+ (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of")
+ | _ => raise Fail "mode_of2")
| mode_of (Mode_Pair (d1, d2)) =
Pair (mode_of d1, mode_of d2)
@@ -220,8 +220,8 @@
| eq_option eq _ = false
fun eq_pred_data (PredData d1, PredData d2) =
- eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
- eq_option (Thm.eq_thm) (#elim d1, #elim d2)
+ eq_list Thm.eq_thm (#intros d1, #intros d2) andalso
+ eq_option Thm.eq_thm (#elim d1, #elim d2)
structure PredData = Theory_Data
(
@@ -318,7 +318,7 @@
(Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)"
| string_of_prem thy (Sidecond t) =
(Syntax.string_of_term_global thy t) ^ "(sidecondition)"
- | string_of_prem thy _ = error "string_of_prem: unexpected input"
+ | string_of_prem thy _ = raise Fail "string_of_prem: unexpected input"
fun string_of_clause thy pred (ts, prems) =
(space_implode " --> "
@@ -449,7 +449,7 @@
let
val (pred', _) = strip_intro_concl th
val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
- error "Trying to instantiate another predicate" else ()
+ raise Fail "Trying to instantiate another predicate" else ()
in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
fun instantiate_ho_args th =
let
@@ -569,7 +569,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
- | _ => error "Trueprop_conv"
+ | _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
Conv.fconv_rule
@@ -767,7 +767,9 @@
fun mk_if cond = Const (@{const_name Predicate.if_pred},
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
-fun mk_not t = let val T = mk_predT HOLogic.unitT
+fun mk_not t =
+ let
+ val T = mk_predT HOLogic.unitT
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
fun mk_Enum f =
@@ -825,7 +827,9 @@
fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
-fun mk_not t = let val T = mk_randompredT HOLogic.unitT
+fun mk_not t =
+ let
+ val T = mk_randompredT HOLogic.unitT
in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
@@ -841,33 +845,33 @@
struct
fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])])
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [T])])])])) = T
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
| dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
-fun mk_bot T = Const ("DSequence.empty", mk_dseqT T);
+fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
fun mk_single t =
let val T = fastype_of t
- in Const("DSequence.single", T --> mk_dseqT T) $ t end;
+ in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
fun mk_bind (x, f) =
let val T as Type ("fun", [_, U]) = fastype_of f
in
- Const ("DSequence.bind", fastype_of x --> T --> U) $ x $ f
+ Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
end;
-val mk_sup = HOLogic.mk_binop "DSequence.union";
+val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
-fun mk_if cond = Const ("DSequence.if_seq",
+fun mk_if cond = Const (@{const_name DSequence.if_seq},
HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
fun mk_not t = let val T = mk_dseqT HOLogic.unitT
- in Const ("DSequence.not_seq", T --> T) $ t end
+ in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
-fun mk_map T1 T2 tf tp = Const ("DSequence.map",
+fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
(T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
@@ -888,28 +892,31 @@
Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
| dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
-fun mk_bot T = Const ("Random_Sequence.empty", mk_random_dseqT T);
+fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
fun mk_single t =
- let val T = fastype_of t
- in Const("Random_Sequence.single", T --> mk_random_dseqT T) $ t end;
+ let
+ val T = fastype_of t
+ in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
- Const ("Random_Sequence.bind", fastype_of x --> T --> U) $ x $ f
+ Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
end;
-val mk_sup = HOLogic.mk_binop "Random_Sequence.union";
+val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
-fun mk_if cond = Const ("Random_Sequence.if_random_dseq",
+fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
-fun mk_not t = let val T = mk_random_dseqT HOLogic.unitT
- in Const ("Random_Sequence.not_random_dseq", T --> T) $ t end
+fun mk_not t =
+ let
+ val T = mk_random_dseqT HOLogic.unitT
+ in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
-fun mk_map T1 T2 tf tp = Const ("Random_Sequence.map",
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
(T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
@@ -982,8 +989,8 @@
else ()
fun error_of p (pol, m) is =
- (" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m)
+ " Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
+ p ^ " violates mode " ^ string_of_mode m
fun is_all_input mode =
let
@@ -1004,7 +1011,7 @@
if U = HOLogic.boolT then
fold_rev (curry Fun) (map input_of Ts) Bool
else
- error "all_input_of: not a predicate"
+ raise Fail "all_input_of: not a predicate"
end
fun partial_hd [] = NONE
@@ -1146,11 +1153,11 @@
case mode_of d1 of
Fun (m', _) => map (fn (d2, mvars2) =>
(Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m')
- | _ => error "Something went wrong") derivs1
+ | _ => raise Fail "Something went wrong") derivs1
end
| all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
| all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
- | all_derivations_of _ modes vs _ = error "all_derivations_of"
+ | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of"
fun rev_option_ord ord (NONE, NONE) = EQUAL
| rev_option_ord ord (NONE, SOME _) = GREATER
@@ -1223,7 +1230,7 @@
| choose_mode_of_prem (Negprem t) = partial_hd
(sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
(all_derivations_of thy neg_modes vs t)))
- | choose_mode_of_prem p = error ("choose_mode_of_prem: " ^ string_of_prem thy p)
+ | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
in
if #reorder_premises mode_analysis_options then
partial_hd (sort (premise_ord thy modes) (ps ~~ map choose_mode_of_prem ps))
@@ -1252,7 +1259,7 @@
Prem t => union (op =) vs (term_vs t)
| Sidecond t => union (op =) vs (term_vs t)
| Negprem t => union (op =) vs (term_vs t)
- | _ => error "I do not know")
+ | _ => raise Fail "I do not know")
fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
| check_mode_prems acc_ps rnd vs ps =
(case