proper exception for internal program failure, not user-error;
authorwenzelm
Fri Dec 19 12:56:06 2014 +0100 (2014-12-19)
changeset 59151a012574b78e7
parent 59150 71b416020f42
child 59152 66e6c539a36d
proper exception for internal program failure, not user-error;
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/Tools/Code/code_runtime.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 19 12:36:50 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 19 12:56:06 2014 +0100
     1.3 @@ -1687,56 +1687,49 @@
     1.4  structure Pred_Result = Proof_Data
     1.5  (
     1.6    type T = unit -> term Predicate.pred
     1.7 -  (* FIXME avoid user error with non-user text *)
     1.8 -  fun init _ () = error "Pred_Result"
     1.9 +  fun init _ () = raise Fail "Pred_Result"
    1.10  );
    1.11  val put_pred_result = Pred_Result.put;
    1.12  
    1.13  structure Pred_Random_Result = Proof_Data
    1.14  (
    1.15    type T = unit -> seed -> term Predicate.pred * seed
    1.16 -  (* FIXME avoid user error with non-user text *)
    1.17 -  fun init _ () = error "Pred_Random_Result"
    1.18 +  fun init _ () = raise Fail "Pred_Random_Result"
    1.19  );
    1.20  val put_pred_random_result = Pred_Random_Result.put;
    1.21  
    1.22  structure Dseq_Result = Proof_Data
    1.23  (
    1.24    type T = unit -> term Limited_Sequence.dseq
    1.25 -  (* FIXME avoid user error with non-user text *)
    1.26 -  fun init _ () = error "Dseq_Result"
    1.27 +  fun init _ () = raise Fail "Dseq_Result"
    1.28  );
    1.29  val put_dseq_result = Dseq_Result.put;
    1.30  
    1.31  structure Dseq_Random_Result = Proof_Data
    1.32  (
    1.33    type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term Limited_Sequence.dseq * seed
    1.34 -  (* FIXME avoid user error with non-user text *)
    1.35 -  fun init _ () = error "Dseq_Random_Result"
    1.36 +  fun init _ () = raise Fail "Dseq_Random_Result"
    1.37  );
    1.38  val put_dseq_random_result = Dseq_Random_Result.put;
    1.39  
    1.40  structure New_Dseq_Result = Proof_Data
    1.41  (
    1.42    type T = unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
    1.43 -  (* FIXME avoid user error with non-user text *)
    1.44 -  fun init _ () = error "New_Dseq_Random_Result"
    1.45 +  fun init _ () = raise Fail "New_Dseq_Random_Result"
    1.46  );
    1.47  val put_new_dseq_result = New_Dseq_Result.put;
    1.48  
    1.49  structure Lseq_Random_Result = Proof_Data
    1.50  (
    1.51    type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
    1.52 -  (* FIXME avoid user error with non-user text *)
    1.53 -  fun init _ () = error "Lseq_Random_Result"
    1.54 +  fun init _ () = raise Fail "Lseq_Random_Result"
    1.55  );
    1.56  val put_lseq_random_result = Lseq_Random_Result.put;
    1.57  
    1.58  structure Lseq_Random_Stats_Result = Proof_Data
    1.59  (
    1.60    type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence
    1.61 -  (* FIXME avoid user error with non-user text *)
    1.62 -  fun init _ () = error "Lseq_Random_Stats_Result"
    1.63 +  fun init _ () = raise Fail "Lseq_Random_Stats_Result"
    1.64  );
    1.65  val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
    1.66  
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 19 12:36:50 2014 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 19 12:56:06 2014 +0100
     2.3 @@ -44,41 +44,39 @@
     2.4  
     2.5  structure Pred_Result = Proof_Data
     2.6  (
     2.7 -  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
     2.8 -  (* FIXME avoid user error with non-user text *)
     2.9 -  fun init _ () = error "Pred_Result"
    2.10 +  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
    2.11 +    Code_Numeral.natural -> seed -> term list Predicate.pred
    2.12 +  fun init _ () = raise Fail "Pred_Result"
    2.13  )
    2.14  val put_pred_result = Pred_Result.put
    2.15  
    2.16  structure Dseq_Result = Proof_Data
    2.17  (
    2.18 -  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
    2.19 -  (* FIXME avoid user error with non-user text *)
    2.20 -  fun init _ () = error "Dseq_Result"
    2.21 +  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
    2.22 +    seed -> term list Limited_Sequence.dseq * seed
    2.23 +  fun init _ () = raise Fail "Dseq_Result"
    2.24  )
    2.25  val put_dseq_result = Dseq_Result.put
    2.26  
    2.27  structure Lseq_Result = Proof_Data
    2.28  (
    2.29 -  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    2.30 -  (* FIXME avoid user error with non-user text *)
    2.31 -  fun init _ () = error "Lseq_Result"
    2.32 +  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
    2.33 +    seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    2.34 +  fun init _ () = raise Fail "Lseq_Result"
    2.35  )
    2.36  val put_lseq_result = Lseq_Result.put
    2.37  
    2.38  structure New_Dseq_Result = Proof_Data
    2.39  (
    2.40    type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    2.41 -  (* FIXME avoid user error with non-user text *)
    2.42 -  fun init _ () = error "New_Dseq_Random_Result"
    2.43 +  fun init _ () = raise Fail "New_Dseq_Random_Result"
    2.44  )
    2.45  val put_new_dseq_result = New_Dseq_Result.put
    2.46  
    2.47  structure CPS_Result = Proof_Data
    2.48  (
    2.49    type T = unit -> Code_Numeral.natural -> (bool * term list) option
    2.50 -  (* FIXME avoid user error with non-user text *)
    2.51 -  fun init _ () = error "CPS_Result"
    2.52 +  fun init _ () = raise Fail "CPS_Result"
    2.53  )
    2.54  val put_cps_result = CPS_Result.put
    2.55  
     3.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Dec 19 12:36:50 2014 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Dec 19 12:56:06 2014 +0100
     3.3 @@ -446,25 +446,23 @@
     3.4  
     3.5  structure Counterexample = Proof_Data
     3.6  (
     3.7 -  type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option
     3.8 -  (* FIXME avoid user error with non-user text *)
     3.9 -  fun init _ () = error "Counterexample"
    3.10 +  type T = unit -> Code_Numeral.natural -> bool ->
    3.11 +    Code_Numeral.natural -> (bool * term list) option
    3.12 +  fun init _ () = raise Fail "Counterexample"
    3.13  );
    3.14  val put_counterexample = Counterexample.put;
    3.15  
    3.16  structure Counterexample_Batch = Proof_Data
    3.17  (
    3.18    type T = unit -> (Code_Numeral.natural -> term list option) list
    3.19 -  (* FIXME avoid user error with non-user text *)
    3.20 -  fun init _ () = error "Counterexample"
    3.21 +  fun init _ () = raise Fail "Counterexample"
    3.22  );
    3.23  val put_counterexample_batch = Counterexample_Batch.put;
    3.24  
    3.25  structure Validator_Batch = Proof_Data
    3.26  (
    3.27    type T = unit -> (Code_Numeral.natural -> bool) list
    3.28 -  (* FIXME avoid user error with non-user text *)
    3.29 -  fun init _ () = error "Counterexample"
    3.30 +  fun init _ () = raise Fail "Counterexample"
    3.31  );
    3.32  val put_validator_batch = Validator_Batch.put;
    3.33  
     4.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Dec 19 12:36:50 2014 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Dec 19 12:56:06 2014 +0100
     4.3 @@ -315,7 +315,7 @@
     4.4  structure Counterexample = Proof_Data
     4.5  (
     4.6    type T = unit -> (bool * term list) option
     4.7 -  fun init _ () = error "Counterexample"
     4.8 +  fun init _ () = raise Fail "Counterexample"
     4.9  )
    4.10  
    4.11  datatype counterexample = Universal_Counterexample of (term * counterexample)
    4.12 @@ -332,7 +332,7 @@
    4.13  structure Existential_Counterexample = Proof_Data
    4.14  (
    4.15    type T = unit -> counterexample option
    4.16 -  fun init _ () = error "Counterexample"
    4.17 +  fun init _ () = raise Fail "Counterexample"
    4.18  )
    4.19  
    4.20  val put_existential_counterexample = Existential_Counterexample.put
     5.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 19 12:36:50 2014 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 19 12:56:06 2014 +0100
     5.3 @@ -273,16 +273,14 @@
     5.4  structure Counterexample = Proof_Data
     5.5  (
     5.6    type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed
     5.7 -  (* FIXME avoid user error with non-user text *)
     5.8 -  fun init _ () = error "Counterexample"
     5.9 +  fun init _ () = raise Fail "Counterexample"
    5.10  );
    5.11  val put_counterexample = Counterexample.put;
    5.12  
    5.13  structure Counterexample_Report = Proof_Data
    5.14  (
    5.15    type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed
    5.16 -  (* FIXME avoid user error with non-user text *)
    5.17 -  fun init _ () = error "Counterexample_Report"
    5.18 +  fun init _ () = raise Fail "Counterexample_Report"
    5.19  );
    5.20  val put_counterexample_report = Counterexample_Report.put;
    5.21  
     6.1 --- a/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 12:36:50 2014 +0100
     6.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 12:56:06 2014 +0100
     6.3 @@ -174,8 +174,7 @@
     6.4  structure Evaluation = Proof_Data
     6.5  (
     6.6    type T = unit -> term
     6.7 -  (* FIXME avoid user error with non-user text *)
     6.8 -  fun init _ () = error "Evaluation"
     6.9 +  fun init _ () = raise Fail "Evaluation"
    6.10  );
    6.11  val put_term = Evaluation.put;
    6.12  val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
     7.1 --- a/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:36:50 2014 +0100
     7.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:56:06 2014 +0100
     7.3 @@ -160,8 +160,7 @@
     7.4  structure Truth_Result = Proof_Data
     7.5  (
     7.6    type T = unit -> truth
     7.7 -  (* FIXME avoid user error with non-user text *)
     7.8 -  fun init _ () = error "Truth_Result"
     7.9 +  fun init _ () = raise Fail "Truth_Result"
    7.10  );
    7.11  val put_truth = Truth_Result.put;
    7.12  val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
     8.1 --- a/src/Tools/nbe.ML	Fri Dec 19 12:36:50 2014 +0100
     8.2 +++ b/src/Tools/nbe.ML	Fri Dec 19 12:56:06 2014 +0100
     8.3 @@ -234,18 +234,17 @@
     8.4  structure Univs = Proof_Data
     8.5  (
     8.6    type T = unit -> Univ list -> Univ list
     8.7 -  (* FIXME avoid user error with non-user text *)
     8.8 -  fun init _ () = error "Univs"
     8.9 +  fun init _ () = raise Fail "Univs"
    8.10  );
    8.11  val put_result = Univs.put;
    8.12  
    8.13  local
    8.14 -  val prefix =     "Nbe.";
    8.15 -  val name_put =   prefix ^ "put_result";
    8.16 +  val prefix = "Nbe.";
    8.17 +  val name_put = prefix ^ "put_result";
    8.18    val name_const = prefix ^ "Const";
    8.19 -  val name_abss =  prefix ^ "abss";
    8.20 -  val name_apps =  prefix ^ "apps";
    8.21 -  val name_same =  prefix ^ "same";
    8.22 +  val name_abss = prefix ^ "abss";
    8.23 +  val name_apps = prefix ^ "apps";
    8.24 +  val name_same = prefix ^ "same";
    8.25  in
    8.26  
    8.27  val univs_cookie = (Univs.get, put_result, name_put);