--- a/src/Pure/defs.ML Sun Oct 20 22:26:44 2019 +0200
+++ b/src/Pure/defs.ML Mon Oct 21 16:32:10 2019 +0200
@@ -31,6 +31,7 @@
val dest: T ->
{restricts: (entry * string) list,
reducts: (entry * entry list) list}
+ val dest_constdefs: T list -> T -> (string * string) list
val empty: T
val merge: context -> T * T -> T
val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T
@@ -140,6 +141,19 @@
fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
in {restricts = restricts, reducts = reducts} end;
+fun dest_constdefs prevs (Defs defs) =
+ let
+ fun prev_spec c i = prevs |> exists (fn Defs prev_defs =>
+ (case Itemtab.lookup prev_defs c of
+ NONE => false
+ | SOME {specs, ...} => Inttab.defined specs i));
+ in
+ (defs, []) |-> Itemtab.fold (fn (c, {specs, ...}) =>
+ specs |> Inttab.fold (fn (i, spec) =>
+ if #1 c = Const andalso is_some (#def spec) andalso not (prev_spec c i)
+ then cons (#2 c, the (#def spec)) else I))
+ end;
+
val empty = Defs Itemtab.empty;