module Unison.PatternMatchCoverage.NormalizedConstraints
  ( NormalizedConstraints (..),
    VarInfo (..),
    VarConstraints (..),
    EffectInfo (..),
    markDirty,
    emptyNormalizedConstraints,
    updateF,
    ConstraintUpdate (..),
    expectCanon,
    declVar,
    prettyNormalizedConstraints,
    prettyDnf,
  )
where

import Data.Functor.Compose
import Data.Sequence (pattern Empty)
import Data.Set qualified as Set
import Unison.ConstructorReference (ConstructorReference)
import Unison.PatternMatchCoverage.Constraint
import Unison.PatternMatchCoverage.EffectHandler
import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
import Unison.PatternMatchCoverage.IntervalSet qualified as IntervalSet
import Unison.PatternMatchCoverage.PmLit qualified as PmLit
import Unison.PatternMatchCoverage.Pretty
import Unison.PatternMatchCoverage.UFMap (UFMap)
import Unison.PatternMatchCoverage.UFMap qualified as UFMap
import Unison.Prelude
import Unison.PrettyPrintEnv qualified as PPE
import Unison.Syntax.TypePrinter qualified as TypePrinter
import Unison.Type (Type, booleanRef, charRef, effectRef, floatRef, intRef, listRef, natRef, textRef, pattern App', pattern Apps', pattern Ref')
import Unison.Util.Pretty
import Unison.Var (Var)

-- | 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 'inhabited' in "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.
data NormalizedConstraints vt v loc = NormalizedConstraints
  { -- | Constraints keyed by the variable they constrain. Equality
    -- constraints are handled by 'UFMap'.
    forall vt v loc.
NormalizedConstraints vt v loc -> UFMap v (VarInfo vt v loc)
constraintMap :: UFMap v (VarInfo vt v loc),
    -- | dirty variables are ones that must be checked for inhabitance
    forall vt v loc. NormalizedConstraints vt v loc -> Set v
dirtySet :: Set v
  }
  deriving stock (NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
(NormalizedConstraints vt v loc
 -> NormalizedConstraints vt v loc -> Bool)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc -> Bool)
-> Eq (NormalizedConstraints vt v loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall vt v loc.
(Var vt, Eq v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
$c== :: forall vt v loc.
(Var vt, Eq v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
== :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
$c/= :: forall vt v loc.
(Var vt, Eq v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
/= :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
Eq, Eq (NormalizedConstraints vt v loc)
Eq (NormalizedConstraints vt v loc) =>
(NormalizedConstraints vt v loc
 -> NormalizedConstraints vt v loc -> Ordering)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc -> Bool)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc -> Bool)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc -> Bool)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc -> Bool)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc)
-> (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc)
-> Ord (NormalizedConstraints vt v loc)
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Ordering
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall vt v loc.
(Var vt, Ord v) =>
Eq (NormalizedConstraints vt v loc)
forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Ordering
forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
$ccompare :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Ordering
compare :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Ordering
$c< :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
< :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
$c<= :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
<= :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
$c> :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
> :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
$c>= :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
>= :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> Bool
$cmax :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
max :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
$cmin :: forall vt v loc.
(Var vt, Ord v) =>
NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
min :: NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
Ord, Int -> NormalizedConstraints vt v loc -> ShowS
[NormalizedConstraints vt v loc] -> ShowS
NormalizedConstraints vt v loc -> String
(Int -> NormalizedConstraints vt v loc -> ShowS)
-> (NormalizedConstraints vt v loc -> String)
-> ([NormalizedConstraints vt v loc] -> ShowS)
-> Show (NormalizedConstraints vt v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall vt v loc.
(Show v, Show vt) =>
Int -> NormalizedConstraints vt v loc -> ShowS
forall vt v loc.
(Show v, Show vt) =>
[NormalizedConstraints vt v loc] -> ShowS
forall vt v loc.
(Show v, Show vt) =>
NormalizedConstraints vt v loc -> String
$cshowsPrec :: forall vt v loc.
(Show v, Show vt) =>
Int -> NormalizedConstraints vt v loc -> ShowS
showsPrec :: Int -> NormalizedConstraints vt v loc -> ShowS
$cshow :: forall vt v loc.
(Show v, Show vt) =>
NormalizedConstraints vt v loc -> String
show :: NormalizedConstraints vt v loc -> String
$cshowList :: forall vt v loc.
(Show v, Show vt) =>
[NormalizedConstraints vt v loc] -> ShowS
showList :: [NormalizedConstraints vt v loc] -> ShowS
Show)

-- | Mark a variable as requiring a new test for inhabitation.
markDirty ::
  (Ord v) =>
  v ->
  NormalizedConstraints vt v loc ->
  NormalizedConstraints vt v loc
markDirty :: forall v vt loc.
Ord v =>
v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
markDirty v
k nc :: NormalizedConstraints vt v loc
nc@NormalizedConstraints {Set v
$sel:dirtySet:NormalizedConstraints :: forall vt v loc. NormalizedConstraints vt v loc -> Set v
dirtySet :: Set v
dirtySet} =
  NormalizedConstraints vt v loc
nc {dirtySet = Set.insert k dirtySet}

emptyNormalizedConstraints :: (Ord v) => NormalizedConstraints vt v loc
emptyNormalizedConstraints :: forall v vt loc. Ord v => NormalizedConstraints vt v loc
emptyNormalizedConstraints =
  NormalizedConstraints
    { $sel:constraintMap:NormalizedConstraints :: UFMap v (VarInfo vt v loc)
constraintMap = UFMap v (VarInfo vt v loc)
forall k v. UFMap k v
UFMap.empty,
      $sel:dirtySet:NormalizedConstraints :: Set v
dirtySet = Set v
forall a. Monoid a => a
mempty
    }

-- | Lookup the canonical value of @v@ from the constraint map. Throws
-- an error if the variable is not in the map.
expectCanon ::
  forall vt v loc.
  (Var v) =>
  v ->
  NormalizedConstraints vt v loc ->
  (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon :: forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
k NormalizedConstraints vt v loc
nc =
  let ((v
v, VarInfo vt v loc
vi), NormalizedConstraints vt v loc
nc') = v
-> (v
    -> VarInfo vt v loc
    -> ((v, VarInfo vt v loc), ConstraintUpdate (VarInfo vt v loc)))
-> NormalizedConstraints vt v loc
-> ((v, VarInfo vt v loc), NormalizedConstraints vt v loc)
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)
updateF v
k (\v
v VarInfo vt v loc
vi -> ((v
v, VarInfo vt v loc
vi), ConstraintUpdate (VarInfo vt v loc)
forall a. ConstraintUpdate a
Ignore)) NormalizedConstraints vt v loc
nc
   in (v
v, VarInfo vt v loc
vi, NormalizedConstraints vt v loc
nc')

-- | Alter a constraint, marks var as dirty if updated
alterF ::
  forall vt v loc f.
  (Var v, Functor f) =>
  v ->
  f (ConstraintUpdate (VarInfo vt v loc)) ->
  (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) ->
  NormalizedConstraints vt v loc ->
  f (NormalizedConstraints vt v loc)
alterF :: forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> f (ConstraintUpdate (VarInfo vt v loc))
-> (v
    -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
alterF v
v f (ConstraintUpdate (VarInfo vt v loc))
nothing v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))
just NormalizedConstraints vt v loc
nc =
  (\(NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
f, UFMap v (VarInfo vt v loc)
x) -> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
f NormalizedConstraints vt v loc
nc {constraintMap = x})
    ((NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc,
  UFMap v (VarInfo vt v loc))
 -> NormalizedConstraints vt v loc)
-> f (NormalizedConstraints vt v loc
      -> NormalizedConstraints vt v loc,
      UFMap v (VarInfo vt v loc))
-> f (NormalizedConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Compose
  f
  ((,)
     (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
  (UFMap v (VarInfo vt v loc))
-> f (NormalizedConstraints vt v loc
      -> NormalizedConstraints vt v loc,
      UFMap v (VarInfo vt v loc))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
      ( v
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (Maybe (VarInfo vt v loc))
-> (v
    -> Int
    -> VarInfo vt v loc
    -> Compose
         f
         ((,)
            (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
         (UFValue v (VarInfo vt v loc)))
-> UFMap v (VarInfo vt v loc)
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (UFMap v (VarInfo vt v loc))
forall (f :: * -> *) k v.
(Functor f, Ord k) =>
k
-> f (Maybe v)
-> (k -> Int -> v -> f (UFValue k v))
-> UFMap k v
-> f (UFMap k v)
UFMap.alterF
          v
v
          Compose
  f
  ((,)
     (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
  (Maybe (VarInfo vt v loc))
nothing'
          v
-> Int
-> VarInfo vt v loc
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (UFValue v (VarInfo vt v loc))
just'
          (NormalizedConstraints vt v loc -> UFMap v (VarInfo vt v loc)
forall vt v loc.
NormalizedConstraints vt v loc -> UFMap v (VarInfo vt v loc)
constraintMap NormalizedConstraints vt v loc
nc)
      )
  where
    just' :: v
-> Int
-> VarInfo vt v loc
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (UFValue v (VarInfo vt v loc))
just' v
canonK Int
eqClassSize VarInfo vt v loc
vi =
      (VarInfo vt v loc -> UFValue v (VarInfo vt v loc))
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (VarInfo vt v loc)
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (UFValue v (VarInfo vt v loc))
forall a b.
(a -> b)
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     a
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> VarInfo vt v loc -> UFValue v (VarInfo vt v loc)
forall k v. Int -> v -> UFValue k v
UFMap.Canonical Int
eqClassSize) (Compose
   f
   ((,)
      (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
   (VarInfo vt v loc)
 -> Compose
      f
      ((,)
         (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
      (UFValue v (VarInfo vt v loc)))
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (VarInfo vt v loc)
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (UFValue v (VarInfo vt v loc))
forall a b. (a -> b) -> a -> b
$
        f (NormalizedConstraints vt v loc
   -> NormalizedConstraints vt v loc,
   VarInfo vt v loc)
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (VarInfo vt v loc)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc,
    VarInfo vt v loc)
 -> Compose
      f
      ((,)
         (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
      (VarInfo vt v loc))
-> f (NormalizedConstraints vt v loc
      -> NormalizedConstraints vt v loc,
      VarInfo vt v loc)
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (VarInfo vt v loc)
forall a b. (a -> b) -> a -> b
$
          v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))
just v
canonK VarInfo vt v loc
vi f (ConstraintUpdate (VarInfo vt v loc))
-> (ConstraintUpdate (VarInfo vt v loc)
    -> (NormalizedConstraints vt v loc
        -> NormalizedConstraints vt v loc,
        VarInfo vt v loc))
-> f (NormalizedConstraints vt v loc
      -> NormalizedConstraints vt v loc,
      VarInfo vt v loc)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            ConstraintUpdate (VarInfo vt v loc)
Ignore -> (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall a. a -> a
id, VarInfo vt v loc
vi)
            Update VarInfo vt v loc
vi -> (v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall v vt loc.
Ord v =>
v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
markDirty v
canonK, VarInfo vt v loc
vi)
    nothing' :: Compose
  f
  ((,)
     (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
  (Maybe (VarInfo vt v loc))
nothing' =
      f (NormalizedConstraints vt v loc
   -> NormalizedConstraints vt v loc,
   Maybe (VarInfo vt v loc))
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (Maybe (VarInfo vt v loc))
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (NormalizedConstraints vt v loc
    -> NormalizedConstraints vt v loc,
    Maybe (VarInfo vt v loc))
 -> Compose
      f
      ((,)
         (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
      (Maybe (VarInfo vt v loc)))
-> f (NormalizedConstraints vt v loc
      -> NormalizedConstraints vt v loc,
      Maybe (VarInfo vt v loc))
-> Compose
     f
     ((,)
        (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc))
     (Maybe (VarInfo vt v loc))
forall a b. (a -> b) -> a -> b
$
        f (ConstraintUpdate (VarInfo vt v loc))
nothing f (ConstraintUpdate (VarInfo vt v loc))
-> (ConstraintUpdate (VarInfo vt v loc)
    -> (NormalizedConstraints vt v loc
        -> NormalizedConstraints vt v loc,
        Maybe (VarInfo vt v loc)))
-> f (NormalizedConstraints vt v loc
      -> NormalizedConstraints vt v loc,
      Maybe (VarInfo vt v loc))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
          ConstraintUpdate (VarInfo vt v loc)
Ignore -> (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall a. a -> a
id, Maybe (VarInfo vt v loc)
forall a. Maybe a
Nothing)
          Update VarInfo vt v loc
x -> (v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall v vt loc.
Ord v =>
v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
markDirty v
v, VarInfo vt v loc -> Maybe (VarInfo vt v loc)
forall a. a -> Maybe a
Just VarInfo vt v loc
x)
{-# INLINE alterF #-}

-- | Generic function to lookup or alter constraints in the constraint
-- map. Throws an error if the variable is not in the map.
updateF ::
  forall vt v loc f.
  (Var v, Functor f) =>
  -- | variable to lookup
  v ->
  -- | update function
  (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) ->
  -- | constraint map
  NormalizedConstraints vt v loc ->
  f (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)
updateF v
v v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))
just NormalizedConstraints vt v loc
nc =
  v
-> f (ConstraintUpdate (VarInfo vt v loc))
-> (v
    -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> f (ConstraintUpdate (VarInfo vt v loc))
-> (v
    -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
alterF v
v f (ConstraintUpdate (VarInfo vt v loc))
nothing v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))
just NormalizedConstraints vt v loc
nc
  where
    nothing :: f (ConstraintUpdate (VarInfo vt v loc))
nothing = String -> f (ConstraintUpdate (VarInfo vt v loc))
forall a. HasCallStack => String -> a
error (String
"expected " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" to be in UFMap")

data ConstraintUpdate a
  = Update a
  | Ignore
  deriving stock ((forall a b. (a -> b) -> ConstraintUpdate a -> ConstraintUpdate b)
-> (forall a b. a -> ConstraintUpdate b -> ConstraintUpdate a)
-> Functor ConstraintUpdate
forall a b. a -> ConstraintUpdate b -> ConstraintUpdate a
forall a b. (a -> b) -> ConstraintUpdate a -> ConstraintUpdate b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ConstraintUpdate a -> ConstraintUpdate b
fmap :: forall a b. (a -> b) -> ConstraintUpdate a -> ConstraintUpdate b
$c<$ :: forall a b. a -> ConstraintUpdate b -> ConstraintUpdate a
<$ :: forall a b. a -> ConstraintUpdate b -> ConstraintUpdate a
Functor)

-- | Install a new variable into the constraint map. Throws an error
-- if the variable already exists in the map.
declVar ::
  forall vt v loc.
  (Var v) =>
  -- | new variable to install
  v ->
  -- | type of variable
  Type vt loc ->
  -- | modifier for the default var info of the given type
  (VarInfo vt v loc -> VarInfo vt v loc) ->
  -- | Normalized constraints to install the variable into
  NormalizedConstraints 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
declVar v
v Type vt loc
t VarInfo vt v loc -> VarInfo vt v loc
f nc :: NormalizedConstraints vt v loc
nc@NormalizedConstraints {UFMap v (VarInfo vt v loc)
$sel:constraintMap:NormalizedConstraints :: forall vt v loc.
NormalizedConstraints vt v loc -> UFMap v (VarInfo vt v loc)
constraintMap :: UFMap v (VarInfo vt v loc)
constraintMap} =
  NormalizedConstraints vt v loc
nc {constraintMap = UFMap.alter v nothing just constraintMap}
  where
    nothing :: Maybe (VarInfo vt v loc)
nothing =
      let !vi :: VarInfo vt v loc
vi = VarInfo vt v loc -> VarInfo vt v loc
f (v -> Type vt loc -> VarInfo vt v loc
forall vt v loc. v -> Type vt loc -> VarInfo vt v loc
mkVarInfo v
v Type vt loc
t)
       in VarInfo vt v loc -> Maybe (VarInfo vt v loc)
forall a. a -> Maybe a
Just VarInfo vt v loc
vi
    just :: v -> Int -> VarInfo vt v loc -> UFValue v (VarInfo vt v loc)
just v
_ Int
_ VarInfo vt v loc
_ = String -> UFValue v (VarInfo vt v loc)
forall a. HasCallStack => String -> a
error (String
"attempted to declare: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" but it already exists")

mkVarInfo :: forall vt v loc. v -> Type vt loc -> VarInfo vt v loc
mkVarInfo :: forall vt v loc. v -> Type vt loc -> VarInfo vt v loc
mkVarInfo v
v Type vt loc
t =
  VarInfo
    { $sel:vi_id:VarInfo :: v
vi_id = v
v,
      $sel:vi_typ:VarInfo :: Type vt loc
vi_typ = Type vt loc
t,
      $sel:vi_con:VarInfo :: VarConstraints vt v loc
vi_con = case Type vt loc
t of
        Apps' (Ref' TypeReference
r) [Type vt loc]
_ | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
effectRef -> Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler -> VarConstraints vt v loc
forall vt v loc.
Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler -> VarConstraints vt v loc
Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
forall a. Maybe a
Nothing Set EffectHandler
forall a. Monoid a => a
mempty
        App' (Ref' TypeReference
r) Type vt loc
t
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
listRef -> Type vt loc
-> Seq v -> Seq v -> IntervalSet -> VarConstraints vt v loc
forall vt v loc.
Type vt loc
-> Seq v -> Seq v -> IntervalSet -> VarConstraints vt v loc
Vc'ListRoot Type vt loc
t Seq v
forall a. Seq a
Empty Seq v
forall a. Seq a
Empty ((Int, Int) -> IntervalSet
IntervalSet.singleton (Int
0, Int
forall a. Bounded a => a
maxBound))
        Ref' TypeReference
r
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
booleanRef -> Maybe Bool -> Set Bool -> VarConstraints vt v loc
forall vt v loc. Maybe Bool -> Set Bool -> VarConstraints vt v loc
Vc'Boolean Maybe Bool
forall a. Maybe a
Nothing Set Bool
forall a. Monoid a => a
mempty
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
intRef -> Maybe Int64 -> Set Int64 -> VarConstraints vt v loc
forall vt v loc.
Maybe Int64 -> Set Int64 -> VarConstraints vt v loc
Vc'Int Maybe Int64
forall a. Maybe a
Nothing Set Int64
forall a. Monoid a => a
mempty
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
natRef -> Maybe Word64 -> Set Word64 -> VarConstraints vt v loc
forall vt v loc.
Maybe Word64 -> Set Word64 -> VarConstraints vt v loc
Vc'Nat Maybe Word64
forall a. Maybe a
Nothing Set Word64
forall a. Monoid a => a
mempty
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
floatRef -> Maybe Double -> Set Double -> VarConstraints vt v loc
forall vt v loc.
Maybe Double -> Set Double -> VarConstraints vt v loc
Vc'Float Maybe Double
forall a. Maybe a
Nothing Set Double
forall a. Monoid a => a
mempty
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
textRef -> Maybe Text -> Set Text -> VarConstraints vt v loc
forall vt v loc. Maybe Text -> Set Text -> VarConstraints vt v loc
Vc'Text Maybe Text
forall a. Maybe a
Nothing Set Text
forall a. Monoid a => a
mempty
          | TypeReference
r TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
charRef -> Maybe Char -> Set Char -> VarConstraints vt v loc
forall vt v loc. Maybe Char -> Set Char -> VarConstraints vt v loc
Vc'Char Maybe Char
forall a. Maybe a
Nothing Set Char
forall a. Monoid a => a
mempty
        -- this may not be a constructor, but we won't be producing
        -- any constraints for it in that case anyway
        Type vt loc
_ -> Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference -> VarConstraints vt v loc
forall vt v loc.
Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference -> VarConstraints vt v loc
Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
forall a. Maybe a
Nothing Set ConstructorReference
forall a. Monoid a => a
mempty,
      $sel:vi_eff:VarInfo :: EffectInfo
vi_eff = EffectInfo
IsNotEffectful
    }

-- | Normalized constraints on a specific variable
data VarInfo vt v loc = VarInfo
  { forall vt v loc. VarInfo vt v loc -> v
vi_id :: v,
    forall vt v loc. VarInfo vt v loc -> Type vt loc
vi_typ :: Type vt loc,
    forall vt v loc. VarInfo vt v loc -> VarConstraints vt v loc
vi_con :: VarConstraints vt v loc,
    forall vt v loc. VarInfo vt v loc -> EffectInfo
vi_eff :: EffectInfo
  }
  deriving stock (Int -> VarInfo vt v loc -> ShowS
[VarInfo vt v loc] -> ShowS
VarInfo vt v loc -> String
(Int -> VarInfo vt v loc -> ShowS)
-> (VarInfo vt v loc -> String)
-> ([VarInfo vt v loc] -> ShowS)
-> Show (VarInfo vt v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall vt v loc.
(Show v, Show vt) =>
Int -> VarInfo vt v loc -> ShowS
forall vt v loc. (Show v, Show vt) => [VarInfo vt v loc] -> ShowS
forall vt v loc. (Show v, Show vt) => VarInfo vt v loc -> String
$cshowsPrec :: forall vt v loc.
(Show v, Show vt) =>
Int -> VarInfo vt v loc -> ShowS
showsPrec :: Int -> VarInfo vt v loc -> ShowS
$cshow :: forall vt v loc. (Show v, Show vt) => VarInfo vt v loc -> String
show :: VarInfo vt v loc -> String
$cshowList :: forall vt v loc. (Show v, Show vt) => [VarInfo vt v loc] -> ShowS
showList :: [VarInfo vt v loc] -> ShowS
Show, VarInfo vt v loc -> VarInfo vt v loc -> Bool
(VarInfo vt v loc -> VarInfo vt v loc -> Bool)
-> (VarInfo vt v loc -> VarInfo vt v loc -> Bool)
-> Eq (VarInfo vt v loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall vt v loc.
(Var vt, Eq v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
$c== :: forall vt v loc.
(Var vt, Eq v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
== :: VarInfo vt v loc -> VarInfo vt v loc -> Bool
$c/= :: forall vt v loc.
(Var vt, Eq v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
/= :: VarInfo vt v loc -> VarInfo vt v loc -> Bool
Eq, Eq (VarInfo vt v loc)
Eq (VarInfo vt v loc) =>
(VarInfo vt v loc -> VarInfo vt v loc -> Ordering)
-> (VarInfo vt v loc -> VarInfo vt v loc -> Bool)
-> (VarInfo vt v loc -> VarInfo vt v loc -> Bool)
-> (VarInfo vt v loc -> VarInfo vt v loc -> Bool)
-> (VarInfo vt v loc -> VarInfo vt v loc -> Bool)
-> (VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc)
-> (VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc)
-> Ord (VarInfo vt v loc)
VarInfo vt v loc -> VarInfo vt v loc -> Bool
VarInfo vt v loc -> VarInfo vt v loc -> Ordering
VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall vt v loc. (Var vt, Ord v) => Eq (VarInfo vt v loc)
forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Ordering
forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc
$ccompare :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Ordering
compare :: VarInfo vt v loc -> VarInfo vt v loc -> Ordering
$c< :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
< :: VarInfo vt v loc -> VarInfo vt v loc -> Bool
$c<= :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
<= :: VarInfo vt v loc -> VarInfo vt v loc -> Bool
$c> :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
> :: VarInfo vt v loc -> VarInfo vt v loc -> Bool
$c>= :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> Bool
>= :: VarInfo vt v loc -> VarInfo vt v loc -> Bool
$cmax :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc
max :: VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc
$cmin :: forall vt v loc.
(Var vt, Ord v) =>
VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc
min :: VarInfo vt v loc -> VarInfo vt v loc -> VarInfo vt v loc
Ord, (forall x. VarInfo vt v loc -> Rep (VarInfo vt v loc) x)
-> (forall x. Rep (VarInfo vt v loc) x -> VarInfo vt v loc)
-> Generic (VarInfo vt v loc)
forall x. Rep (VarInfo vt v loc) x -> VarInfo vt v loc
forall x. VarInfo vt v loc -> Rep (VarInfo vt v loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall vt v loc x. Rep (VarInfo vt v loc) x -> VarInfo vt v loc
forall vt v loc x. VarInfo vt v loc -> Rep (VarInfo vt v loc) x
$cfrom :: forall vt v loc x. VarInfo vt v loc -> Rep (VarInfo vt v loc) x
from :: forall x. VarInfo vt v loc -> Rep (VarInfo vt v loc) x
$cto :: forall vt v loc x. Rep (VarInfo vt v loc) x -> VarInfo vt v loc
to :: forall x. Rep (VarInfo vt v loc) x -> VarInfo vt v loc
Generic)

-- | 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.
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 of list elems
      (Type vt loc)
      -- | Positive constraint on cons elements
      (Seq v)
      -- | Positive constraint on snoc elements
      (Seq v)
      -- | positive constraint on input list size
      IntervalSet
  deriving stock (Int -> VarConstraints vt v loc -> ShowS
[VarConstraints vt v loc] -> ShowS
VarConstraints vt v loc -> String
(Int -> VarConstraints vt v loc -> ShowS)
-> (VarConstraints vt v loc -> String)
-> ([VarConstraints vt v loc] -> ShowS)
-> Show (VarConstraints vt v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall vt v loc.
(Show v, Show vt) =>
Int -> VarConstraints vt v loc -> ShowS
forall vt v loc.
(Show v, Show vt) =>
[VarConstraints vt v loc] -> ShowS
forall vt v loc.
(Show v, Show vt) =>
VarConstraints vt v loc -> String
$cshowsPrec :: forall vt v loc.
(Show v, Show vt) =>
Int -> VarConstraints vt v loc -> ShowS
showsPrec :: Int -> VarConstraints vt v loc -> ShowS
$cshow :: forall vt v loc.
(Show v, Show vt) =>
VarConstraints vt v loc -> String
show :: VarConstraints vt v loc -> String
$cshowList :: forall vt v loc.
(Show v, Show vt) =>
[VarConstraints vt v loc] -> ShowS
showList :: [VarConstraints vt v loc] -> ShowS
Show, VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
(VarConstraints vt v loc -> VarConstraints vt v loc -> Bool)
-> (VarConstraints vt v loc -> VarConstraints vt v loc -> Bool)
-> Eq (VarConstraints vt v loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall vt v loc.
(Var vt, Eq v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
$c== :: forall vt v loc.
(Var vt, Eq v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
== :: VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
$c/= :: forall vt v loc.
(Var vt, Eq v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
/= :: VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
Eq, Eq (VarConstraints vt v loc)
Eq (VarConstraints vt v loc) =>
(VarConstraints vt v loc -> VarConstraints vt v loc -> Ordering)
-> (VarConstraints vt v loc -> VarConstraints vt v loc -> Bool)
-> (VarConstraints vt v loc -> VarConstraints vt v loc -> Bool)
-> (VarConstraints vt v loc -> VarConstraints vt v loc -> Bool)
-> (VarConstraints vt v loc -> VarConstraints vt v loc -> Bool)
-> (VarConstraints vt v loc
    -> VarConstraints vt v loc -> VarConstraints vt v loc)
-> (VarConstraints vt v loc
    -> VarConstraints vt v loc -> VarConstraints vt v loc)
-> Ord (VarConstraints vt v loc)
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
VarConstraints vt v loc -> VarConstraints vt v loc -> Ordering
VarConstraints vt v loc
-> VarConstraints vt v loc -> VarConstraints vt v loc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall vt v loc. (Var vt, Ord v) => Eq (VarConstraints vt v loc)
forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Ordering
forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc
-> VarConstraints vt v loc -> VarConstraints vt v loc
$ccompare :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Ordering
compare :: VarConstraints vt v loc -> VarConstraints vt v loc -> Ordering
$c< :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
< :: VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
$c<= :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
<= :: VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
$c> :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
> :: VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
$c>= :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
>= :: VarConstraints vt v loc -> VarConstraints vt v loc -> Bool
$cmax :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc
-> VarConstraints vt v loc -> VarConstraints vt v loc
max :: VarConstraints vt v loc
-> VarConstraints vt v loc -> VarConstraints vt v loc
$cmin :: forall vt v loc.
(Var vt, Ord v) =>
VarConstraints vt v loc
-> VarConstraints vt v loc -> VarConstraints vt v loc
min :: VarConstraints vt v loc
-> VarConstraints vt v loc -> VarConstraints vt v loc
Ord, (forall x.
 VarConstraints vt v loc -> Rep (VarConstraints vt v loc) x)
-> (forall x.
    Rep (VarConstraints vt v loc) x -> VarConstraints vt v loc)
-> Generic (VarConstraints vt v loc)
forall x.
Rep (VarConstraints vt v loc) x -> VarConstraints vt v loc
forall x.
VarConstraints vt v loc -> Rep (VarConstraints vt v loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall vt v loc x.
Rep (VarConstraints vt v loc) x -> VarConstraints vt v loc
forall vt v loc x.
VarConstraints vt v loc -> Rep (VarConstraints vt v loc) x
$cfrom :: forall vt v loc x.
VarConstraints vt v loc -> Rep (VarConstraints vt v loc) x
from :: forall x.
VarConstraints vt v loc -> Rep (VarConstraints vt v loc) x
$cto :: forall vt v loc x.
Rep (VarConstraints vt v loc) x -> VarConstraints vt v loc
to :: forall x.
Rep (VarConstraints vt v loc) x -> VarConstraints vt v loc
Generic)

data EffectInfo
  = IsEffectful
  | IsNotEffectful
  deriving stock (Int -> EffectInfo -> ShowS
[EffectInfo] -> ShowS
EffectInfo -> String
(Int -> EffectInfo -> ShowS)
-> (EffectInfo -> String)
-> ([EffectInfo] -> ShowS)
-> Show EffectInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EffectInfo -> ShowS
showsPrec :: Int -> EffectInfo -> ShowS
$cshow :: EffectInfo -> String
show :: EffectInfo -> String
$cshowList :: [EffectInfo] -> ShowS
showList :: [EffectInfo] -> ShowS
Show, EffectInfo -> EffectInfo -> Bool
(EffectInfo -> EffectInfo -> Bool)
-> (EffectInfo -> EffectInfo -> Bool) -> Eq EffectInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EffectInfo -> EffectInfo -> Bool
== :: EffectInfo -> EffectInfo -> Bool
$c/= :: EffectInfo -> EffectInfo -> Bool
/= :: EffectInfo -> EffectInfo -> Bool
Eq, Eq EffectInfo
Eq EffectInfo =>
(EffectInfo -> EffectInfo -> Ordering)
-> (EffectInfo -> EffectInfo -> Bool)
-> (EffectInfo -> EffectInfo -> Bool)
-> (EffectInfo -> EffectInfo -> Bool)
-> (EffectInfo -> EffectInfo -> Bool)
-> (EffectInfo -> EffectInfo -> EffectInfo)
-> (EffectInfo -> EffectInfo -> EffectInfo)
-> Ord EffectInfo
EffectInfo -> EffectInfo -> Bool
EffectInfo -> EffectInfo -> Ordering
EffectInfo -> EffectInfo -> EffectInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: EffectInfo -> EffectInfo -> Ordering
compare :: EffectInfo -> EffectInfo -> Ordering
$c< :: EffectInfo -> EffectInfo -> Bool
< :: EffectInfo -> EffectInfo -> Bool
$c<= :: EffectInfo -> EffectInfo -> Bool
<= :: EffectInfo -> EffectInfo -> Bool
$c> :: EffectInfo -> EffectInfo -> Bool
> :: EffectInfo -> EffectInfo -> Bool
$c>= :: EffectInfo -> EffectInfo -> Bool
>= :: EffectInfo -> EffectInfo -> Bool
$cmax :: EffectInfo -> EffectInfo -> EffectInfo
max :: EffectInfo -> EffectInfo -> EffectInfo
$cmin :: EffectInfo -> EffectInfo -> EffectInfo
min :: EffectInfo -> EffectInfo -> EffectInfo
Ord)

prettyNormalizedConstraints :: forall vt v loc. (Var v, Var vt) => PPE.PrettyPrintEnv -> NormalizedConstraints vt v loc -> Pretty ColorText
prettyNormalizedConstraints :: forall vt v loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> NormalizedConstraints vt v loc -> Pretty ColorText
prettyNormalizedConstraints PrettyPrintEnv
ppe (NormalizedConstraints {UFMap v (VarInfo vt v loc)
$sel:constraintMap:NormalizedConstraints :: forall vt v loc.
NormalizedConstraints vt v loc -> UFMap v (VarInfo vt v loc)
constraintMap :: UFMap v (VarInfo vt v loc)
constraintMap}) = Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Pretty ColorText
"⟨", Pretty ColorText
pconstraints, Pretty ColorText
"⟩"]
  where
    cls :: [(v, Set v, VarInfo vt v loc)]
cls = UFMap v (VarInfo vt v loc) -> [(v, Set v, VarInfo vt v loc)]
forall k v. Ord k => UFMap k v -> [(k, Set k, v)]
UFMap.toClasses UFMap v (VarInfo vt v loc)
constraintMap

    pconstraints :: Pretty ColorText
pconstraints = Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
", " ((v, Set v, VarInfo vt v loc) -> Pretty ColorText
prettyCon ((v, Set v, VarInfo vt v loc) -> Pretty ColorText)
-> [(v, Set v, VarInfo vt v loc)] -> [Pretty ColorText]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, Set v, VarInfo vt v loc)]
cls)
    prettyCon :: (v, Set v, VarInfo vt v loc) -> Pretty ColorText
prettyCon (v
kcanon, Set v
ks, VarInfo vt v loc
vi) =
      let posCon :: [Constraint vt v loc]
posCon = [Constraint vt v loc]
-> Maybe [Constraint vt v loc] -> [Constraint vt v loc]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [Constraint vt v loc] -> [Constraint vt v loc])
-> Maybe [Constraint vt v loc] -> [Constraint vt v loc]
forall a b. (a -> b) -> a -> b
$ case VarInfo vt v loc -> VarConstraints vt v loc
forall vt v loc. VarInfo vt v loc -> VarConstraints vt v loc
vi_con VarInfo vt v loc
vi of
            Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
_neg ->
              (\(ConstructorReference
datacon, [(v, Type vt loc)]
convars) -> [v
-> ConstructorReference
-> [(v, Type vt loc)]
-> Constraint vt v loc
forall vt v loc.
v
-> ConstructorReference
-> [(v, Type vt loc)]
-> Constraint vt v loc
PosCon v
kcanon ConstructorReference
datacon [(v, Type vt loc)]
convars]) ((ConstructorReference, [(v, Type vt loc)])
 -> [Constraint vt v loc])
-> Maybe (ConstructorReference, [(v, Type vt loc)])
-> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConstructorReference, [(v, Type vt loc)])
pos
            Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
_neg ->
              (\(EffectHandler
effectHandler, [(v, Type vt loc)]
convars) -> [v -> EffectHandler -> [(v, Type vt loc)] -> Constraint vt v loc
forall vt v loc.
v -> EffectHandler -> [(v, Type vt loc)] -> Constraint vt v loc
PosEffect v
kcanon EffectHandler
effectHandler [(v, Type vt loc)]
convars]) ((EffectHandler, [(v, Type vt loc)]) -> [Constraint vt v loc])
-> Maybe (EffectHandler, [(v, Type vt loc)])
-> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (EffectHandler, [(v, Type vt loc)])
pos
            Vc'Boolean Maybe Bool
pos Set Bool
_neg ->
              (\Bool
x -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
PosLit v
kcanon (Bool -> PmLit
PmLit.Boolean Bool
x)]) (Bool -> [Constraint vt v loc])
-> Maybe Bool -> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool
pos
            Vc'Int Maybe Int64
pos Set Int64
_neg ->
              (\Int64
x -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
PosLit v
kcanon (Int64 -> PmLit
PmLit.Int Int64
x)]) (Int64 -> [Constraint vt v loc])
-> Maybe Int64 -> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int64
pos
            Vc'Nat Maybe Word64
pos Set Word64
_neg ->
              (\Word64
x -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
PosLit v
kcanon (Word64 -> PmLit
PmLit.Nat Word64
x)]) (Word64 -> [Constraint vt v loc])
-> Maybe Word64 -> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Word64
pos
            Vc'Float Maybe Double
pos Set Double
_neg ->
              (\Double
x -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
PosLit v
kcanon (Double -> PmLit
PmLit.Float Double
x)]) (Double -> [Constraint vt v loc])
-> Maybe Double -> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Double
pos
            Vc'Text Maybe Text
pos Set Text
_neg ->
              (\Text
x -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
PosLit v
kcanon (Text -> PmLit
PmLit.Text Text
x)]) (Text -> [Constraint vt v loc])
-> Maybe Text -> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
pos
            Vc'Char Maybe Char
pos Set Char
_neg ->
              (\Char
x -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
PosLit v
kcanon (Char -> PmLit
PmLit.Char Char
x)]) (Char -> [Constraint vt v loc])
-> Maybe Char -> Maybe [Constraint vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Char
pos
            Vc'ListRoot Type vt loc
_typ Seq v
posCons Seq v
posSnoc IntervalSet
_iset ->
              let consConstraints :: [Constraint vt v loc]
consConstraints = ((Int, v) -> Constraint vt v loc)
-> [(Int, v)] -> [Constraint vt v loc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
i, v
x) -> v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
PosListHead v
kcanon Int
i v
x) ([Int] -> [v] -> [(Int, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] (Seq v -> [v]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
posCons))
                  snocConstraints :: [Constraint vt v loc]
snocConstraints = ((Int, v) -> Constraint vt v loc)
-> [(Int, v)] -> [Constraint vt v loc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
i, v
x) -> v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
PosListTail v
kcanon Int
i v
x) ([Int] -> [v] -> [(Int, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] (Seq v -> [v]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
posSnoc))
               in [Constraint vt v loc] -> Maybe [Constraint vt v loc]
forall a. a -> Maybe a
Just ([Constraint vt v loc]
consConstraints [Constraint vt v loc]
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. [a] -> [a] -> [a]
++ [Constraint vt v loc]
snocConstraints)
          negConK :: forall x. Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
          negConK :: forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set x
s v -> x -> Constraint vt v loc
f = (x -> [Constraint vt v loc] -> [Constraint vt v loc])
-> [Constraint vt v loc] -> Set x -> [Constraint vt v loc]
forall a b. (a -> b -> b) -> b -> Set a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\x
a [Constraint vt v loc]
b -> v -> x -> Constraint vt v loc
f v
kcanon x
a Constraint vt v loc
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. a -> [a] -> [a]
: [Constraint vt v loc]
b) [] Set x
s
          negCon :: [Constraint vt v loc]
negCon = case VarInfo vt v loc -> VarConstraints vt v loc
forall vt v loc. VarInfo vt v loc -> VarConstraints vt v loc
vi_con VarInfo vt v loc
vi of
            Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
_pos Set ConstructorReference
neg -> Set ConstructorReference
-> (v -> ConstructorReference -> Constraint vt v loc)
-> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set ConstructorReference
neg v -> ConstructorReference -> Constraint vt v loc
forall vt v loc. v -> ConstructorReference -> Constraint vt v loc
NegCon
            Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
_pos Set EffectHandler
neg -> Set EffectHandler
-> (v -> EffectHandler -> Constraint vt v loc)
-> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set EffectHandler
neg v -> EffectHandler -> Constraint vt v loc
forall vt v loc. v -> EffectHandler -> Constraint vt v loc
NegEffect
            Vc'Boolean Maybe Bool
_pos Set Bool
neg -> Set Bool
-> (v -> Bool -> Constraint vt v loc) -> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set Bool
neg (\v
v Bool
a -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
NegLit v
v (Bool -> PmLit
PmLit.Boolean Bool
a))
            Vc'Int Maybe Int64
_pos Set Int64
neg -> Set Int64
-> (v -> Int64 -> Constraint vt v loc) -> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set Int64
neg (\v
v Int64
a -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
NegLit v
v (Int64 -> PmLit
PmLit.Int Int64
a))
            Vc'Nat Maybe Word64
_pos Set Word64
neg -> Set Word64
-> (v -> Word64 -> Constraint vt v loc) -> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set Word64
neg (\v
v Word64
a -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
NegLit v
v (Word64 -> PmLit
PmLit.Nat Word64
a))
            Vc'Float Maybe Double
_pos Set Double
neg -> Set Double
-> (v -> Double -> Constraint vt v loc) -> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set Double
neg (\v
v Double
a -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
NegLit v
v (Double -> PmLit
PmLit.Float Double
a))
            Vc'Text Maybe Text
_pos Set Text
neg -> Set Text
-> (v -> Text -> Constraint vt v loc) -> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set Text
neg (\v
v Text
a -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
NegLit v
v (Text -> PmLit
PmLit.Text Text
a))
            Vc'Char Maybe Char
_pos Set Char
neg -> Set Char
-> (v -> Char -> Constraint vt v loc) -> [Constraint vt v loc]
forall x.
Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc]
negConK Set Char
neg (\v
v Char
a -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
NegLit v
v (Char -> PmLit
PmLit.Char Char
a))
            Vc'ListRoot Type vt loc
_typ Seq v
_posCons Seq v
_posSnoc IntervalSet
iset -> [v -> IntervalSet -> Constraint vt v loc
forall vt v loc. v -> IntervalSet -> Constraint vt v loc
NegListInterval v
kcanon (IntervalSet -> IntervalSet
IntervalSet.complement IntervalSet
iset)]
          botCon :: [Constraint vt v loc]
botCon = case VarInfo vt v loc -> EffectInfo
forall vt v loc. VarInfo vt v loc -> EffectInfo
vi_eff VarInfo vt v loc
vi of
            EffectInfo
IsNotEffectful -> []
            EffectInfo
IsEffectful -> [v -> Constraint vt v loc
forall vt v loc. v -> Constraint vt v loc
Effectful v
kcanon]
       in Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " ([Pretty ColorText] -> Pretty ColorText)
-> [Pretty ColorText] -> Pretty ColorText
forall a b. (a -> b) -> a -> b
$
            v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
kcanon
              Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: (v -> Pretty ColorText) -> [v] -> [Pretty ColorText]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar (Set v -> [v]
forall a. Set a -> [a]
Set.toList (Set v -> [v]) -> Set v -> [v]
forall a b. (a -> b) -> a -> b
$ v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
Set.delete v
kcanon Set v
ks)
              [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ [Pretty ColorText
":", PrettyPrintEnv -> Type vt loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TypePrinter.pretty PrettyPrintEnv
ppe (VarInfo vt v loc -> Type vt loc
forall vt v loc. VarInfo vt v loc -> Type vt loc
vi_typ VarInfo vt v loc
vi)]
              [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ [Pretty ColorText
"|"]
              [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ case [Constraint vt v loc]
posCon [Constraint vt v loc]
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. [a] -> [a] -> [a]
++ [Constraint vt v loc]
negCon [Constraint vt v loc]
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. [a] -> [a] -> [a]
++ [Constraint vt v loc]
botCon of
                [] -> [Pretty ColorText
"∅"]
                [Constraint vt v loc]
_ -> [Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
", " ([Pretty ColorText] -> Pretty ColorText)
-> [Pretty ColorText] -> Pretty ColorText
forall a b. (a -> b) -> a -> b
$ (Constraint vt v loc -> Pretty ColorText)
-> [Constraint vt v loc] -> [Pretty ColorText]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrettyPrintEnv -> Constraint vt v loc -> Pretty ColorText
forall vt v loc.
(Var vt, Var v) =>
PrettyPrintEnv -> Constraint vt v loc -> Pretty ColorText
prettyConstraint PrettyPrintEnv
ppe) ([Constraint vt v loc]
posCon [Constraint vt v loc]
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. [a] -> [a] -> [a]
++ [Constraint vt v loc]
negCon [Constraint vt v loc]
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. [a] -> [a] -> [a]
++ [Constraint vt v loc]
botCon)]

prettyDnf :: (Var v, Var vt) => PPE.PrettyPrintEnv -> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
prettyDnf :: forall v vt loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
prettyDnf PrettyPrintEnv
ppe Set (NormalizedConstraints vt v loc)
xs = Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " (Pretty ColorText
"{" Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
", " (PrettyPrintEnv
-> NormalizedConstraints vt v loc -> Pretty ColorText
forall vt v loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> NormalizedConstraints vt v loc -> Pretty ColorText
prettyNormalizedConstraints PrettyPrintEnv
ppe (NormalizedConstraints vt v loc -> Pretty ColorText)
-> [NormalizedConstraints vt v loc] -> [Pretty ColorText]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (NormalizedConstraints vt v loc)
-> [NormalizedConstraints vt v loc]
forall a. Set a -> [a]
Set.toList Set (NormalizedConstraints vt v loc)
xs) Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: [Pretty ColorText
"}"])