203 |
203 |
204 fun witness_aux (classes, arities) log_types hyps sorts = |
204 fun witness_aux (classes, arities) log_types hyps sorts = |
205 let |
205 let |
206 val top_witn = (propT, []); |
206 val top_witn = (propT, []); |
207 fun le S1 S2 = sort_le classes (S1, S2); |
207 fun le S1 S2 = sort_le classes (S1, S2); |
208 fun get_solved S2 (T, S1) = if le S1 S2 then Some (T, S2) else None; |
208 fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE; |
209 fun get_hyp S2 S1 = if le S1 S2 then Some (TFree ("'hyp", S1), S2) else None; |
209 fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE; |
210 fun mg_dom t S = Some (mg_domain (classes, arities) t S) handle DOMAIN _ => None; |
210 fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle DOMAIN _ => NONE; |
211 |
211 |
212 fun witn_sort _ (solved_failed, []) = (solved_failed, Some top_witn) |
212 fun witn_sort _ (solved_failed, []) = (solved_failed, SOME top_witn) |
213 | witn_sort path ((solved, failed), S) = |
213 | witn_sort path ((solved, failed), S) = |
214 if exists (le S) failed then ((solved, failed), None) |
214 if exists (le S) failed then ((solved, failed), NONE) |
215 else |
215 else |
216 (case get_first (get_solved S) solved of |
216 (case get_first (get_solved S) solved of |
217 Some w => ((solved, failed), Some w) |
217 SOME w => ((solved, failed), SOME w) |
218 | None => |
218 | NONE => |
219 (case get_first (get_hyp S) hyps of |
219 (case get_first (get_hyp S) hyps of |
220 Some w => ((w :: solved, failed), Some w) |
220 SOME w => ((w :: solved, failed), SOME w) |
221 | None => witn_types path log_types ((solved, failed), S))) |
221 | NONE => witn_types path log_types ((solved, failed), S))) |
222 |
222 |
223 and witn_sorts path x = foldl_map (witn_sort path) x |
223 and witn_sorts path x = foldl_map (witn_sort path) x |
224 |
224 |
225 and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), None) |
225 and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), NONE) |
226 | witn_types path (t :: ts) (solved_failed, S) = |
226 | witn_types path (t :: ts) (solved_failed, S) = |
227 (case mg_dom t S of |
227 (case mg_dom t S of |
228 Some SS => |
228 SOME SS => |
229 (*do not descend into stronger args (achieving termination)*) |
229 (*do not descend into stronger args (achieving termination)*) |
230 if exists (fn D => le D S orelse exists (le D) path) SS then |
230 if exists (fn D => le D S orelse exists (le D) path) SS then |
231 witn_types path ts (solved_failed, S) |
231 witn_types path ts (solved_failed, S) |
232 else |
232 else |
233 let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in |
233 let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in |
234 if forall is_some ws then |
234 if forall is_some ws then |
235 let val w = (Type (t, map (#1 o the) ws), S) |
235 let val w = (Type (t, map (#1 o the) ws), S) |
236 in ((w :: solved', failed'), Some w) end |
236 in ((w :: solved', failed'), SOME w) end |
237 else witn_types path ts ((solved', failed'), S) |
237 else witn_types path ts ((solved', failed'), S) |
238 end |
238 end |
239 | None => witn_types path ts (solved_failed, S)); |
239 | NONE => witn_types path ts (solved_failed, S)); |
240 |
240 |
241 in witn_sorts [] (([], []), sorts) end; |
241 in witn_sorts [] (([], []), sorts) end; |
242 |
242 |
243 fun str_of_sort [c] = c |
243 fun str_of_sort [c] = c |
244 | str_of_sort cs = enclose "{" "}" (commas cs); |
244 | str_of_sort cs = enclose "{" "}" (commas cs); |
246 in |
246 in |
247 |
247 |
248 fun witness_sorts (classes, arities) log_types hyps sorts = |
248 fun witness_sorts (classes, arities) log_types hyps sorts = |
249 let |
249 let |
250 (*double check result of witness search*) |
250 (*double check result of witness search*) |
251 fun check_result None = None |
251 fun check_result NONE = NONE |
252 | check_result (Some (T, S)) = |
252 | check_result (SOME (T, S)) = |
253 if of_sort (classes, arities) (T, S) then Some (T, S) |
253 if of_sort (classes, arities) (T, S) then SOME (T, S) |
254 else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); |
254 else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); |
255 in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; |
255 in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; |
256 |
256 |
257 end; |
257 end; |
258 |
258 |