equal
deleted
inserted
replaced
115 |
115 |
116 fun exceeded limit = (limit <= 0) |
116 fun exceeded limit = (limit <= 0) |
117 fun exceeded_limit (limit, _, _) = exceeded limit |
117 fun exceeded_limit (limit, _, _) = exceeded limit |
118 |
118 |
119 |
119 |
|
120 fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => |
|
121 Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false) |
|
122 |
|
123 fun eq_subst (subst1, subst2) = |
|
124 derived_subst subst1 subst2 andalso derived_subst subst2 subst1 |
|
125 |
|
126 |
120 fun with_all_grounds cx grounds f = |
127 fun with_all_grounds cx grounds f = |
121 if exceeded_limit cx then I else Symtab.fold f grounds |
128 if exceeded_limit cx then I else Symtab.fold f grounds |
122 |
129 |
123 fun with_all_type_combinations cx schematics f (n, Ts) = |
130 fun with_all_type_combinations cx schematics f (n, Ts) = |
124 if exceeded_limit cx then I |
131 if exceeded_limit cx then I |
127 fun derive_new_substs thy cx new_grounds schematics subst = |
134 fun derive_new_substs thy cx new_grounds schematics subst = |
128 with_all_grounds cx new_grounds |
135 with_all_grounds cx new_grounds |
129 (with_all_type_combinations cx schematics (fn T => fn U => |
136 (with_all_type_combinations cx schematics (fn T => fn U => |
130 (case try (Sign.typ_match thy (T, U)) subst of |
137 (case try (Sign.typ_match thy (T, U)) subst of |
131 NONE => I |
138 NONE => I |
132 | SOME subst' => cons subst'))) [] |
139 | SOME subst' => insert eq_subst subst'))) [] |
133 |
140 |
134 |
141 |
135 fun same_subst subst' (_, subst) = subst' |> Vartab.forall (fn (n, (_, T)) => |
142 fun known_subst sub subs1 subs2 subst' = |
136 Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false) |
143 let fun derived (_, subst) = derived_subst subst' subst |
137 |
144 in derived sub orelse exists derived subs1 orelse exists derived subs2 end |
138 fun known_subst sub subs1 subs2 subst = |
|
139 same_subst subst sub orelse exists (same_subst subst) subs1 orelse |
|
140 exists (same_subst subst) subs2 |
|
141 |
145 |
142 fun within_limit f cx = if exceeded_limit cx then cx else f cx |
146 fun within_limit f cx = if exceeded_limit cx then cx else f cx |
143 |
147 |
144 fun fold_partial_substs derive add = within_limit ( |
148 fun fold_partial_substs derive add = within_limit ( |
145 let |
149 let |