--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sat Dec 30 21:22:31 2023 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sat Dec 30 21:35:00 2023 +0100
@@ -297,7 +297,7 @@
| HASKELL => ProgHaskell (AM_GHC.compile rules)
| SML => ProgSML (AM_SML.compile rules)
- fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
+ fun has_witness s = not (null (#1 (Sign.witness_sorts thy [] [s])))
val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
@@ -345,7 +345,7 @@
val shyptab = add_shyps shyps Sorttab.empty
fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
- fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
+ fun has_witness s = not (null (#1 (Sign.witness_sorts thy [] [s])))
val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
val _ =
--- a/src/Pure/sign.ML Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/sign.ML Sat Dec 30 21:35:00 2023 +0100
@@ -23,7 +23,8 @@
val subsort: theory -> sort * sort -> bool
val of_sort: theory -> typ * sort -> bool
val inter_sort: theory -> sort * sort -> sort
- val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
+ val witness_sorts: theory -> (typ * sort) list -> sort Ord_List.T ->
+ (typ * sort) list * sort Ord_List.T
val logical_types: theory -> string list
val typ_instance: theory -> typ * typ -> bool
val typ_equiv: theory -> typ * typ -> bool
--- a/src/Pure/sorts.ML Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/sorts.ML Sat Dec 30 21:35:00 2023 +0100
@@ -64,7 +64,8 @@
typ * sort -> 'a list (*exception CLASS_ERROR*)
val classrel_derivation: algebra ->
('a * class -> class -> 'a) -> 'a * class -> class -> 'a (*exception CLASS_ERROR*)
- val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
+ val witness_sorts: algebra -> string list -> (typ * sort) list -> sort Ord_List.T ->
+ (typ * sort) list * sort Ord_List.T
end;
structure Sorts: SORTS =
@@ -489,6 +490,8 @@
end
| NONE => witn_types path ts S solved_failed);
- in map_filter I (#1 (witn_sorts [] sorts ([], []))) end;
+ val witnessed = map_filter I (#1 (witn_sorts [] sorts ([], [])));
+ val non_witnessed = fold (remove_sort o #2) witnessed sorts;
+ in (witnessed, non_witnessed) end;
end;
--- a/src/Pure/thm.ML Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/thm.ML Sat Dec 30 21:35:00 2023 +0100
@@ -1058,9 +1058,7 @@
val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
val thy = theory_of_thm thm;
-
val algebra = Sign.classes_of thy;
- val minimize = Sorts.minimize_sort algebra;
val le = Sorts.sort_le algebra;
fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
@@ -1070,8 +1068,8 @@
val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
val extra = fold (Sorts.remove_sort o #2) present shyps;
- val witnessed = Sign.witness_sorts thy present extra;
- val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
+ val (witnessed, non_witnessed) =
+ Sign.witness_sorts thy present extra ||> map (`(Sorts.minimize_sort algebra));
val extra' =
non_witnessed |> map_filter (fn (S, _) =>
--- a/src/Pure/type.ML Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/type.ML Sat Dec 30 21:35:00 2023 +0100
@@ -38,7 +38,8 @@
val cert_class: tsig -> class -> class
val cert_sort: tsig -> sort -> sort
val minimize_sort: tsig -> sort -> sort
- val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list
+ val witness_sorts: tsig -> (typ * sort) list -> sort Ord_List.T ->
+ (typ * sort) list * sort Ord_List.T
type mode
val mode_default: mode
val mode_syntax: mode