--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 11:14:26 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 13:31:41 2014 +0100
@@ -42,11 +42,11 @@
val simp_attrs = @{attributes [simp]};
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
-exception Primcorec_Error of string * term list;
+exception PRIMCOREC of string * term list;
-fun primcorec_error str = raise Primcorec_Error (str, []);
-fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]);
-fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns);
+fun primcorec_error str = raise PRIMCOREC (str, []);
+fun primcorec_error_eqn str eqn = raise PRIMCOREC (str, [eqn]);
+fun primcorec_error_eqns str eqns = raise PRIMCOREC (str, eqns);
datatype primcorec_option = Sequential_Option | Exhaustive_Option;
@@ -83,7 +83,7 @@
nested_map_comps: thm list,
ctr_specs: corec_ctr_spec list};
-exception AINT_NO_MAP of term;
+exception NOT_A_MAP of term;
fun not_codatatype ctxt T =
error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
@@ -259,14 +259,14 @@
in
Term.list_comb (map', fs')
end
- | NONE => raise AINT_NO_MAP t)
- | massage_map _ _ _ t = raise AINT_NO_MAP t
+ | NONE => raise NOT_A_MAP t)
+ | massage_map _ _ _ t = raise NOT_A_MAP t
and massage_map_or_map_arg bound_Ts U T t =
if T = U then
tap check_no_call t
else
massage_map bound_Ts U T t
- handle AINT_NO_MAP _ => massage_mutual_fun bound_Ts U T t
+ handle NOT_A_MAP _ => massage_mutual_fun bound_Ts U T t
and massage_mutual_fun bound_Ts U T t =
(case t of
Const (@{const_name comp}, _) $ t1 $ t2 =>
@@ -307,7 +307,7 @@
massage_mutual_call bound_Ts U T t
else
massage_map bound_Ts U T t1 $ t2
- handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)
+ handle NOT_A_MAP _ => massage_mutual_call bound_Ts U T t)
| Abs (s, T', t') =>
Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
| _ => massage_mutual_call bound_Ts U T t))
@@ -594,14 +594,14 @@
let
val (lhs, rhs) = HOLogic.dest_eq eqn
handle TERM _ =>
- primcorec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
+ primcorec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
val sel = head_of lhs;
val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free
handle TERM _ =>
- primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
+ primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name)
handle Option.Option =>
- primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
+ primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
val {ctr, ...} =
(case of_spec_opt of
SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
@@ -1354,11 +1354,12 @@
add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
handle ERROR str => primcorec_error str
end
- handle Primcorec_Error (str, eqns) =>
- if null eqns
- then error ("primcorec error:\n " ^ str)
- else error ("primcorec error:\n " ^ str ^ "\nin\n " ^
- space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
+ handle PRIMCOREC (str, eqns) =>
+ if null eqns then
+ error ("primcorec error:\n " ^ str)
+ else
+ error ("primcorec error:\n " ^ str ^ "\nin\n " ^
+ space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
lthy
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 11:14:26 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 13:31:41 2014 +0100
@@ -37,11 +37,11 @@
val simp_attrs = @{attributes [simp]};
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
-exception Primrec_Error of string * term list;
+exception PRIMREC of string * term list;
-fun primrec_error str = raise Primrec_Error (str, []);
-fun primrec_error_eqn str eqn = raise Primrec_Error (str, [eqn]);
-fun primrec_error_eqns str eqns = raise Primrec_Error (str, eqns);
+fun primrec_error str = raise PRIMREC (str, []);
+fun primrec_error_eqn str eqn = raise PRIMREC (str, [eqn]);
+fun primrec_error_eqns str eqns = raise PRIMREC (str, eqns);
datatype rec_call =
No_Rec of int * typ |
@@ -60,7 +60,7 @@
nested_map_comps: thm list,
ctr_specs: rec_ctr_spec list};
-exception AINT_NO_MAP of term;
+exception NOT_A_MAP of term;
fun ill_formed_rec_call ctxt t =
error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
@@ -104,20 +104,20 @@
in
Term.list_comb (map', fs')
end
- | NONE => raise AINT_NO_MAP t)
- | massage_map _ _ t = raise AINT_NO_MAP t
+ | NONE => raise NOT_A_MAP t)
+ | massage_map _ _ t = raise NOT_A_MAP t
and massage_map_or_map_arg U T t =
if T = U then
tap check_no_call t
else
massage_map U T t
- handle AINT_NO_MAP _ => massage_mutual_fun U T t;
+ handle NOT_A_MAP _ => massage_mutual_fun U T t;
fun massage_call (t as t1 $ t2) =
if has_call t then
if t2 = y then
massage_map yU yT (elim_y t1) $ y'
- handle AINT_NO_MAP t' => invalid_map ctxt t'
+ handle NOT_A_MAP t' => invalid_map ctxt t'
else
let val (g, xs) = Term.strip_comb t2 in
if g = y then
@@ -238,10 +238,10 @@
let
val eqn = drop_all eqn' |> HOLogic.dest_Trueprop
handle TERM _ =>
- primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
+ primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
val (lhs, rhs) = HOLogic.dest_eq eqn
handle TERM _ =>
- primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
+ primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
val (fun_name, args) = strip_comb lhs
|>> (fn x => if is_Free x then fst (dest_Free x)
else primrec_error_eqn "malformed function equation (does not start with free)" eqn);
@@ -475,8 +475,9 @@
val funs_data = eqns_data
|> partition_eq ((op =) o pairself #fun_name)
|> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
- |> map (fn (x, y) => the_single y handle List.Empty =>
- primrec_error ("missing equations for function " ^ quote x));
+ |> map (fn (x, y) => the_single y
+ handle List.Empty =>
+ primrec_error ("missing equations for function " ^ quote x));
val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
val arg_Ts = map (#rec_type o hd) funs_data;
@@ -542,22 +543,21 @@
lthy' |> Local_Theory.notes (notes @ common_notes) |> snd)
end;
-(* primrec definition *)
-
fun add_primrec_simple fixes ts lthy =
let
- val (((names, defs), prove), lthy) = prepare_primrec fixes ts lthy
+ val (((names, defs), prove), lthy') = prepare_primrec fixes ts lthy
handle ERROR str => primrec_error str;
in
- lthy
+ lthy'
|> fold_map Local_Theory.define defs
|-> (fn defs => `(fn lthy => (names, (map fst defs, prove lthy defs))))
end
- handle Primrec_Error (str, eqns) =>
- if null eqns
- then error ("primrec_new error:\n " ^ str)
- else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^
- space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
+ handle PRIMREC (str, eqns) =>
+ if null eqns then
+ error ("primrec_new error:\n " ^ str)
+ else
+ error ("primrec_new error:\n " ^ str ^ "\nin\n " ^
+ space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
local