# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID 7b39120a1494fae5ba6792de387ab4da43c31d36
# Parent  362bfc2ca0ee855fccb49bc2f333f77eeb4e9979
some improvements thanks to Makarius source code review

diff -r 362bfc2ca0ee -r 7b39120a1494 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- 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)))
diff -r 362bfc2ca0ee -r 7b39120a1494 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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