--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 26 14:13:03 2019 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 26 14:23:18 2019 +0100
@@ -1354,7 +1354,7 @@
fun all_nondefs_of ctxt subst =
ctxt |> Spec_Rules.get
- |> filter (curry (op =) Spec_Rules.Unknown o fst)
+ |> filter (Spec_Rules.is_unknown o fst)
|> maps (snd o snd)
|> filter_out (is_built_in_theory o Thm.theory_id)
|> map (subst_atomic subst o Thm.prop_of)
@@ -1948,8 +1948,8 @@
def_table_for
(maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of)
o snd o snd)
- (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
- cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst
+ (filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o #1)
+ (Spec_Rules.get ctxt))) subst
end
fun ground_theorem_table thy =
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Mar 26 14:13:03 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Mar 26 14:23:18 2019 +0100
@@ -471,13 +471,6 @@
card_of []
end;
-fun int_of_classif Spec_Rules.Equational = 1
- | int_of_classif Spec_Rules.Inductive = 2
- | int_of_classif Spec_Rules.Co_Inductive = 3
- | int_of_classif Spec_Rules.Unknown = 4;
-
-val classif_ord = int_ord o apply2 int_of_classif;
-
fun spec_rules_of ctxt (x as (s, T)) =
let
val thy = Proof_Context.theory_of ctxt;
@@ -503,7 +496,7 @@
fun spec_rules () =
Spec_Rules.retrieve ctxt (Const x)
- |> sort (classif_ord o apply2 fst);
+ |> sort (Spec_Rules.rough_classification_ord o apply2 fst);
val specs =
if s = \<^const_name>\<open>The\<close> then
@@ -544,7 +537,7 @@
val orphan_axioms_of =
Spec_Rules.get
- #> filter (curry (op =) Spec_Rules.Unknown o fst)
+ #> filter (Spec_Rules.is_unknown o fst)
#> map snd
#> filter (null o fst)
#> maps snd
@@ -959,7 +952,7 @@
val (props', cmds) =
if null props then
([], map IVal consts)
- else if classif = Spec_Rules.Equational then
+ else if Spec_Rules.is_equational classif then
(case partition_props consts props of
SOME propss =>
(props,
@@ -968,15 +961,15 @@
pat_complete = is_apparently_pat_complete ctxt props})
consts propss)])
| NONE => def_or_spec ())
- else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive]
- classif then
+ else if (Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) classif
+ then
if is_inductive_set_intro (hd props) then
def_or_spec ()
else
(case partition_props consts props of
SOME propss =>
(props,
- [ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP
+ [ICoPred (if Spec_Rules.is_inductive classif then BNF_Util.Least_FP
else BNF_Util.Greatest_FP,
length consts = 1 andalso
is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Mar 26 14:13:03 2019 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Mar 26 14:23:18 2019 +0100
@@ -317,11 +317,11 @@
*)
val specs = Spec_Rules.get ctxt
val (rec_defs, nonrec_defs) = specs
- |> filter (curry (op =) Spec_Rules.Equational o fst)
+ |> filter (Spec_Rules.is_equational o fst)
|> maps (snd o snd)
|> List.partition (is_rec_def o Thm.prop_of)
val spec_intros = specs
- |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
+ |> filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o fst)
|> maps (snd o snd)
in
Termtab.empty
--- a/src/Pure/Isar/spec_rules.ML Tue Mar 26 14:13:03 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML Tue Mar 26 14:23:18 2019 +0100
@@ -8,7 +8,12 @@
signature SPEC_RULES =
sig
- datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
+ datatype rough_classification = Equational | Inductive | Co_Inductive | Unknown
+ val rough_classification_ord: rough_classification * rough_classification -> order
+ val is_equational: rough_classification -> bool
+ val is_inductive: rough_classification -> bool
+ val is_co_inductive: rough_classification -> bool
+ val is_unknown: rough_classification -> bool
type spec = rough_classification * (term list * thm list)
val get: Proof.context -> spec list
val get_global: theory -> spec list
@@ -21,9 +26,21 @@
structure Spec_Rules: SPEC_RULES =
struct
+(* rough classification *)
+
+datatype rough_classification = Equational | Inductive | Co_Inductive | Unknown;
+
+val rough_classification_ord =
+ int_ord o apply2 (fn Equational => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3);
+
+val is_equational = fn Equational => true | _ => false;
+val is_inductive = fn Inductive => true | _ => false;
+val is_co_inductive = fn Co_Inductive => true | _ => false;
+val is_unknown = fn Unknown => true | _ => false;
+
+
(* rules *)
-datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
type spec = rough_classification * (term list * thm list);
structure Rules = Generic_Data
@@ -32,7 +49,7 @@
val empty : T =
Item_Net.init
(fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
- class1 = class2 andalso
+ rough_classification_ord (class1, class2) = EQUAL andalso
eq_list (op aconv) (ts1, ts2) andalso
eq_list Thm.eq_thm_prop (ths1, ths2))
(#1 o #2);