module FactInference: sig .. end
This module analyzes data type declarations to synthesize facts about
data types.
val assume : TypeCore.env -> TypeCore.mode_constraint -> TypeCore.env
assume env c produces a new environment where the mode constraint
c is assumed (i.e., it is added to the environment as a new
hypothesis).
val analyze_data_types : TypeCore.env -> TypeCore.var list -> TypeCore.env
analyze_data_types env vars assumes that vars forms a group of
mutually recursive algebraic data type definitions. It assumes that
the members of vars which are *abstract* data types have already
received a fact in env. It synthesizes a fact for the members of
vars which are *concrete* data types, and adds these facts to the
environment, producing a new environment.
val has_mode : Mode.mode -> TypeCore.env -> TypeCore.typ -> bool
has_mode mode env ty tells whether the predicate mode ty is
satisfied, using the information stored in env about the ambient
type definitions and mode assumptions.
val is_duplicable : TypeCore.env -> TypeCore.typ -> bool
A specialized version of has_mode.
val is_exclusive : TypeCore.env -> TypeCore.typ -> bool
A specialized version of has_mode.