387 (* the major type of All and Ex quantifiers *) |
387 (* the major type of All and Ex quantifiers *) |
388 fun qnt_typ ty = domain_type (domain_type ty) |
388 fun qnt_typ ty = domain_type (domain_type ty) |
389 |
389 |
390 (* Checks that two types match, for example: |
390 (* Checks that two types match, for example: |
391 rty -> rty matches qty -> qty *) |
391 rty -> rty matches qty -> qty *) |
392 fun matches_typ thy T T' = |
392 fun matches_typ thy rT qT = |
393 case (T, T') of |
393 if rT = qT then true else |
394 (TFree _, TFree _) => true |
394 case (rT, qT) of |
395 | (TVar _, TVar _) => true |
395 (Type (rs, rtys), Type (qs, qtys)) => |
396 | (Type (s, tys), Type (s', tys')) => ( |
396 if rs = qs then |
397 if T = T' then true else |
397 if length rtys <> length qtys then false else |
398 let |
398 forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) |
399 val rty = #rtyp (Quotient_Info.quotdata_lookup thy s') |
399 else |
400 in |
400 (case Quotient_Info.quotdata_lookup_raw thy qs of |
401 if Sign.typ_instance thy (T, rty) then true else false |
401 SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
402 end |
402 | NONE => false) |
403 handle Not_found => |
|
404 if length tys <> length tys' then false else |
|
405 (* 'andalso' is buildin syntax so it needs to be expanded *) |
|
406 fold (fn x => fn y => x andalso y) (map2 (matches_typ thy) tys tys') (s = s') |
|
407 ) |
|
408 | _ => false |
403 | _ => false |
409 |
404 |
410 |
405 |
411 (* produces a regularized version of rtrm |
406 (* produces a regularized version of rtrm |
412 |
407 |