# HG changeset patch # User wenzelm # Date 1553606598 -3600 # Node ID 6b097aeb3650c06f313cbb09371b9067d3b680ee # Parent eb072ce80f82ee4630a6e069560068d375788bb1 clarified signature: avoid direct comparison on type rough_classification; diff -r eb072ce80f82 -r 6b097aeb3650 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 = diff -r eb072ce80f82 -r 6b097aeb3650 src/HOL/Tools/Nunchaku/nunchaku_collect.ML --- 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>\The\ 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 diff -r eb072ce80f82 -r 6b097aeb3650 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r eb072ce80f82 -r 6b097aeb3650 src/Pure/Isar/spec_rules.ML --- 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);