--- a/src/Pure/Isar/code.ML Mon Jun 06 21:28:46 2016 +0200
+++ b/src/Pure/Isar/code.ML Mon Jun 06 22:22:05 2016 +0200
@@ -428,20 +428,24 @@
*)
exception BAD_THM of string;
+
fun bad_thm msg = raise BAD_THM msg;
-fun error_thm f thy (thm, proper) = f (thm, proper)
- handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
-fun error_abs_thm f thy thm = f thm
- handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
-fun warning_thm f thy (thm, proper) = SOME (f (thm, proper))
- handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); NONE)
-fun try_thm f thm_proper = SOME (f thm_proper)
- handle BAD_THM _ => NONE;
+
+datatype strictness = Silent | Liberal | Strict
+
+fun handle_strictness thm_of f strictness thy x = SOME (f x)
+ handle BAD_THM msg => case strictness of
+ Silent => NONE
+ | Liberal => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x)); NONE)
+ | Strict => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x));
fun is_linear thm =
- let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
- in not (has_duplicates (op =) ((fold o fold_aterms)
- (fn Var (v, _) => cons v | _ => I) args [])) end;
+ let
+ val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
+ in
+ not (has_duplicates (op =) ((fold o fold_aterms)
+ (fn Var (v, _) => cons v | _ => I) args []))
+ end;
fun check_decl_ty thy (c, ty) =
let
@@ -507,7 +511,9 @@
| _ => ();
in () end;
-fun assert_eqn' thy check_patterns (thm, proper) =
+local
+
+fun raw_assert_eqn thy check_patterns (thm, proper) =
let
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
handle TERM _ => bad_thm "Not an equation"
@@ -516,7 +522,7 @@
allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
in (thm, proper) end;
-fun assert_abs_eqn' thy some_tyco thm =
+fun raw_assert_abs_eqn thy some_tyco thm =
let
val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
handle TERM _ => bad_thm "Not an equation"
@@ -542,29 +548,19 @@
else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
in (thm, tyco) end;
-fun assert_eqn thy = error_thm (assert_eqn' thy true) thy;
-
-fun assert_abs_eqn thy some_tyco = error_abs_thm (assert_abs_eqn' thy some_tyco) thy;
-
-fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
+in
-fun mk_eqn thy = error_thm (assert_eqn' thy false) thy o
- apfst (meta_rewrite thy);
-
-fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
- o try_thm (assert_eqn' thy false) o rpair false o meta_rewrite thy;
+fun generic_assert_eqn strictness thy check_patterns thm_proper =
+ handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy thm_proper;
-fun mk_eqn_maybe_abs thy raw_thm =
- let
- val thm = meta_rewrite thy raw_thm;
- val some_abs_thm = try_thm (assert_abs_eqn' thy NONE) thm;
- in case some_abs_thm
- of SOME (thm, tyco) => SOME ((thm, true), SOME tyco)
- | NONE => (Option.map (fn (thm, _) => ((thm, is_linear thm), NONE))
- o warning_thm (assert_eqn' thy false) thy) (thm, false)
- end;
+fun generic_assert_abs_eqn strictness thy check_patterns thm =
+ handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm;
-fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn' thy NONE) thy o meta_rewrite thy;
+end;
+
+fun assert_eqn thy = the o generic_assert_eqn Strict thy true;
+
+fun assert_abs_eqn thy some_tyco = the o generic_assert_abs_eqn Strict thy some_tyco;
val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
@@ -589,6 +585,8 @@
(* technical transformations of code equations *)
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
+
fun expand_eta thy k thm =
let
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
@@ -642,7 +640,9 @@
(* abstype certificates *)
-fun check_abstype_cert thy proto_thm =
+local
+
+fun raw_abstype_cert thy proto_thm =
let
val thm = (Axclass.unoverload (Proof_Context.init_global thy) o meta_rewrite thy) proto_thm;
val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
@@ -667,6 +667,13 @@
val (vs', _) = typscheme thy (abs, ty');
in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
+in
+
+fun check_abstype_cert strictness thy proto_thm =
+ handle_strictness I (raw_abstype_cert thy) strictness thy proto_thm;
+
+end;
+
(* code equation certificates *)
@@ -1070,6 +1077,12 @@
processual distinction:
thm * proper for concrete equations
thm for abstract equations
+
+ strictness wrt. shape of theorem propositions:
+ * default attributes: silent
+ * user attributes: warnings (after morphism application!)
+ * Isabelle/ML functions: strict
+ * internal processing after storage: strict
*)
fun gen_add_eqn default (raw_thm, proper) thy =
@@ -1113,31 +1126,49 @@
datatype kind = Equation | Nbe | Abstract;
-fun add_eqn (kind, default) thm thy =
- case (kind, default) of
- (Equation, true) => (case mk_eqn_liberal thy thm of
- SOME eqn => gen_add_eqn true eqn thy
- | NONE => thy)
- | (Equation, false) => gen_add_eqn false (mk_eqn thy (thm, true)) thy
- | (Nbe, _) => gen_add_eqn default (mk_eqn thy (thm, false)) thy
- | (Abstract, _) => gen_add_abs_eqn default (mk_abs_eqn thy thm) thy;
+fun mk_eqn strictness thy = generic_assert_eqn strictness thy false o
+ apfst (meta_rewrite thy);
+
+fun mk_abs_eqn strictness thy = generic_assert_abs_eqn strictness thy NONE o
+ meta_rewrite thy;
+
+fun mk_maybe_abs_eqn thy raw_thm =
+ let
+ val thm = meta_rewrite thy raw_thm;
+ val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm;
+ in case some_abs_thm
+ of SOME (thm, tyco) => SOME ((thm, true), SOME tyco)
+ | NONE => Option.map (fn (thm, _) => ((thm, is_linear thm), NONE))
+ (generic_assert_eqn Liberal thy false (thm, false))
+ end;
+
+fun generic_add_eqn strictness (kind, default) thm thy =
+ case kind of
+ Equation => fold (gen_add_eqn default)
+ (the_list (mk_eqn strictness thy (thm, true))) thy
+ | Nbe => fold (gen_add_eqn default)
+ (the_list (mk_eqn strictness thy (thm, false))) thy
+ | Abstract => fold (gen_add_abs_eqn default)
+ (the_list (mk_abs_eqn strictness thy thm)) thy;
+
+val add_eqn = generic_add_eqn Strict;
fun lift_attribute f = Thm.declaration_attribute
(fn thm => Context.mapping (f thm) I);
fun add_default_eqn_attribute kind =
- lift_attribute (add_eqn (kind, true));
+ lift_attribute (generic_add_eqn Silent (kind, true));
fun add_default_eqn_attrib kind =
Attrib.internal (K (add_default_eqn_attribute kind));
-fun add_eqn_maybe_abs thm thy =
- case mk_eqn_maybe_abs thy thm
+fun add_maybe_abs_eqn_liberal thm thy =
+ case mk_maybe_abs_eqn thy thm
of SOME (eqn, NONE) => gen_add_eqn false eqn thy
| SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy
| NONE => thy;
-fun del_eqn thm thy = case mk_eqn_liberal thy thm
+fun del_eqn thm thy = case mk_eqn Liberal thy (thm, true)
of SOME (thm, _) =>
let
fun del_eqn' (Eqns_Default _) = initial_fun_spec
@@ -1267,20 +1298,18 @@
(fn tyco =>
Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
-fun gen_add_abstype default proto_thm thy =
- let
- val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
- error_abs_thm (check_abstype_cert thy) thy proto_thm;
- in
- thy
- |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
- |> change_fun_spec rep
- (K (Proj ((Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco), default)))
- |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
- end;
+fun generic_add_abstype strictness default proto_thm thy =
+ case check_abstype_cert strictness thy proto_thm of
+ SOME (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =>
+ thy
+ |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
+ |> change_fun_spec rep
+ (K (Proj ((Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco), default)))
+ |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
+ | NONE => thy;
-val add_abstype = gen_add_abstype false;
-val add_abstype_default = gen_add_abstype true;
+val add_abstype = generic_add_abstype Strict false;
+val add_abstype_default = generic_add_abstype Strict true;
(* setup *)
@@ -1290,14 +1319,14 @@
fun lift_const_attribute f cs =
lift_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
val code_attribute_parser =
- Args.$$$ "equation" |-- Scan.succeed (lift_attribute (add_eqn (Equation, false)))
- || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (add_eqn (Nbe, false)))
- || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (add_eqn (Abstract, false)))
- || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute add_abstype)
+ Args.$$$ "equation" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Equation, false)))
+ || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Nbe, false)))
+ || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Abstract, false)))
+ || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute (generic_add_abstype Liberal false))
|| Args.del |-- Scan.succeed (lift_attribute del_eqn)
|| Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_eqns)
|| Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_exception)
- || Scan.succeed (lift_attribute add_eqn_maybe_abs);
+ || Scan.succeed (lift_attribute add_maybe_abs_eqn_liberal);
in
Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
"declare theorems for code generation"