| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Unison.PatternMatchCoverage.NormalizedConstraints
Synopsis
- data NormalizedConstraints vt v loc = NormalizedConstraints {
- constraintMap :: UFMap v (VarInfo vt v loc)
- dirtySet :: Set v
- data VarInfo vt v loc = VarInfo {
- vi_id :: v
- vi_typ :: Type vt loc
- vi_con :: VarConstraints vt v loc
- vi_eff :: EffectInfo
- data VarConstraints vt v loc
- = Vc'Constructor (Maybe (ConstructorReference, [(v, Type vt loc)])) (Set ConstructorReference)
- | Vc'Effect (Maybe (EffectHandler, [(v, Type vt loc)])) (Set EffectHandler)
- | Vc'Boolean (Maybe Bool) (Set Bool)
- | Vc'Int (Maybe Int64) (Set Int64)
- | Vc'Nat (Maybe Word64) (Set Word64)
- | Vc'Float (Maybe Double) (Set Double)
- | Vc'Text (Maybe Text) (Set Text)
- | Vc'Char (Maybe Char) (Set Char)
- | Vc'ListRoot (Type vt loc) (Seq v) (Seq v) IntervalSet
- data EffectInfo
- markDirty :: Ord v => v -> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
- emptyNormalizedConstraints :: Ord v => NormalizedConstraints vt v loc
- updateF :: forall vt v loc f. (Var v, Functor f) => v -> (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) -> NormalizedConstraints vt v loc -> f (NormalizedConstraints vt v loc)
- data ConstraintUpdate a
- expectCanon :: forall vt v loc. Var v => v -> NormalizedConstraints vt v loc -> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
- declVar :: forall vt v loc. Var v => v -> Type vt loc -> (VarInfo vt v loc -> VarInfo vt v loc) -> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
- prettyNormalizedConstraints :: forall vt v loc. (Var v, Var vt) => PrettyPrintEnv -> NormalizedConstraints vt v loc -> Pretty ColorText
- prettyDnf :: (Var v, Var vt) => PrettyPrintEnv -> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
Documentation
data NormalizedConstraints vt v loc Source #
Normalized refinement types (fig 6)
Each variable may be associated with a number of constraints
represented by VarInfo. A NormalizedConstraints is conceptually
the conjunction of all constraints in the map. Disjunction is
represented by passing a Set of NormalizedConstraints. So, the
constraints are normalized into disjunctive normal form and each
NormalizedConstraints is a DNF term.
Additionally, the following invariants are enforced (Section 3.4)
- Mutual compatibility: No two constraints should conflict with each other.
- Inhabitation: There must be at least one value that inhabits each
refinement type. (N.B. We don't truly know if a type is inhabited,
see
inhabitedin Unison.PatternMatchCoverage.Solve for details. However, the refinement type is inhabited as far as our inhabitation checker is concerned.)
These invariants ensure that each term in our DNF has at least one solution, and it is easy to expand and print these solutions.
Constructors
| NormalizedConstraints | |
Instances
data VarInfo vt v loc Source #
Normalized constraints on a specific variable
Constructors
| VarInfo | |
Fields
| |
Instances
data VarConstraints vt v loc Source #
The constraints are different for different types, although most of them take the form of an optional positive constraint and a set of negative constraints.
Constructors
| Vc'Constructor (Maybe (ConstructorReference, [(v, Type vt loc)])) (Set ConstructorReference) | |
| Vc'Effect (Maybe (EffectHandler, [(v, Type vt loc)])) (Set EffectHandler) | |
| Vc'Boolean (Maybe Bool) (Set Bool) | |
| Vc'Int (Maybe Int64) (Set Int64) | |
| Vc'Nat (Maybe Word64) (Set Word64) | |
| Vc'Float (Maybe Double) (Set Double) | |
| Vc'Text (Maybe Text) (Set Text) | |
| Vc'Char (Maybe Char) (Set Char) | |
| Vc'ListRoot | |
Fields
| |
Instances
data EffectInfo Source #
Constructors
| IsEffectful | |
| IsNotEffectful |
Instances
| Show EffectInfo Source # | |
Defined in Unison.PatternMatchCoverage.NormalizedConstraints Methods showsPrec :: Int -> EffectInfo -> ShowS # show :: EffectInfo -> String # showList :: [EffectInfo] -> ShowS # | |
| Eq EffectInfo Source # | |
| Ord EffectInfo Source # | |
Defined in Unison.PatternMatchCoverage.NormalizedConstraints Methods compare :: EffectInfo -> EffectInfo -> Ordering # (<) :: EffectInfo -> EffectInfo -> Bool # (<=) :: EffectInfo -> EffectInfo -> Bool # (>) :: EffectInfo -> EffectInfo -> Bool # (>=) :: EffectInfo -> EffectInfo -> Bool # max :: EffectInfo -> EffectInfo -> EffectInfo # min :: EffectInfo -> EffectInfo -> EffectInfo # | |
markDirty :: Ord v => v -> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc Source #
Mark a variable as requiring a new test for inhabitation.
emptyNormalizedConstraints :: Ord v => NormalizedConstraints vt v loc Source #
Arguments
| :: forall vt v loc f. (Var v, Functor f) | |
| => v | variable to lookup |
| -> (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) | update function |
| -> NormalizedConstraints vt v loc | constraint map |
| -> f (NormalizedConstraints vt v loc) |
Generic function to lookup or alter constraints in the constraint map. Throws an error if the variable is not in the map.
data ConstraintUpdate a Source #
Instances
| Functor ConstraintUpdate Source # | |
Defined in Unison.PatternMatchCoverage.NormalizedConstraints Methods fmap :: (a -> b) -> ConstraintUpdate a -> ConstraintUpdate b # (<$) :: a -> ConstraintUpdate b -> ConstraintUpdate a # | |
expectCanon :: forall vt v loc. Var v => v -> NormalizedConstraints vt v loc -> (v, VarInfo vt v loc, NormalizedConstraints vt v loc) Source #
Lookup the canonical value of v from the constraint map. Throws
an error if the variable is not in the map.
Arguments
| :: forall vt v loc. Var v | |
| => v | new variable to install |
| -> Type vt loc | type of variable |
| -> (VarInfo vt v loc -> VarInfo vt v loc) | modifier for the default var info of the given type |
| -> NormalizedConstraints vt v loc | Normalized constraints to install the variable into |
| -> NormalizedConstraints vt v loc |
Install a new variable into the constraint map. Throws an error if the variable already exists in the map.
prettyNormalizedConstraints :: forall vt v loc. (Var v, Var vt) => PrettyPrintEnv -> NormalizedConstraints vt v loc -> Pretty ColorText Source #
prettyDnf :: (Var v, Var vt) => PrettyPrintEnv -> Set (NormalizedConstraints vt v loc) -> Pretty ColorText Source #