# HG changeset patch # User blanchet # Date 1392640301 -3600 # Node ID 171d73e39d6d15203ad17e442b794fa1205d2410 # Parent 39708e59f4b010e1be111856a54e7979d81b0adc tuning diff -r 39708e59f4b0 -r 171d73e39d6d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 diff -r 39708e59f4b0 -r 171d73e39d6d src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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