Module IR.Subtype
val subtypes_cast : t
denotes the current type and any subtypes
val subtypes_instof : t
val join : t -> t -> t
val case_analysis : Tenv.t -> (Typ.Name.t * t) -> (Typ.Name.t * t) -> t option * t option
case_analysis tenv (c1, st1) (c2, st2)
performs case analysis onc1 <: c2
according tost1
andst2
.case_analysis
returns a pair:- whether
st1
andst2
admitc1 <: c2
, and in case returns the updated subtypest1
- whether
st1
andst2
admitnot(c1 <: c2)
, and in case returns the updated subtypest1
- whether
val is_known_subtype : Tenv.t -> Typ.Name.t -> Typ.Name.t -> bool
is_known_subtype tenv c1 c2
returns true if there is enough information intenv
to prove thatc1
is a subtype ofc2
. Note thatnot (is_known_subtype tenv c1 c2) == true
does not imply thatis_known_not_subtype tenv c1 c2 == true