{-# LANGUAGE DataKinds #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Unison.PatternMatchCoverage.Solve
  ( uncoverAnnotate,
    classify,
    expandSolution,
    generateInhabitants,
  )
where

import Control.Monad.State
import Control.Monad.Trans.Compose
import Control.Monad.Trans.Maybe
import Data.Foldable
import Data.Function
import Data.Functor
import Data.Functor.Compose
import Data.Map qualified as Map
import Data.Sequence qualified as Seq
import Data.Set qualified as Set
import Unison.Builtin.Decls (unitRef)
import Unison.ConstructorReference (ConstructorReference, reference_)
import Unison.Debug (DebugFlag (PatternCoverageConstraintSolver), shouldDebug)
import Unison.Pattern (Pattern)
import Unison.Pattern qualified as Pattern
import Unison.PatternMatchCoverage.Class
import Unison.PatternMatchCoverage.Constraint (Constraint)
import Unison.PatternMatchCoverage.Constraint qualified as C
import Unison.PatternMatchCoverage.EffectHandler
import Unison.PatternMatchCoverage.GrdTree
import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
import Unison.PatternMatchCoverage.IntervalSet qualified as IntervalSet
import Unison.PatternMatchCoverage.Literal
import Unison.PatternMatchCoverage.NormalizedConstraints
import Unison.PatternMatchCoverage.PmGrd
import Unison.PatternMatchCoverage.PmLit (PmLit)
import Unison.PatternMatchCoverage.PmLit qualified as PmLit
import Unison.PatternMatchCoverage.UFMap qualified as UFMap
import Unison.Prelude
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Util.Pretty qualified as P
import Unison.Util.Recursion
import Unison.Var (Var)

-- | top-down traversal of the 'GrdTree' that produces:
--
-- * a refinement type describing values that do not match the 'GrdTree'
--   (the "uncovered" set)
-- * a new 'GrdTree' annotated with refinement types at the nodes describing
--   values that cause an effect to be performed and values that match
--   the case at the leaves.
--
-- If the former is inhabited then its inhabitants are unmatched
-- values. If the leaves of the latter are inhabited then the case is
-- redundant.
uncoverAnnotate ::
  forall vt v loc m l.
  (Pmc vt v loc m) =>
  Set (NormalizedConstraints vt v loc) ->
  GrdTree (PmGrd vt v loc) l ->
  ( m
      ( Set (NormalizedConstraints vt v loc),
        GrdTree (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l)
      )
  )
uncoverAnnotate :: forall vt v loc (m :: * -> *) l.
Pmc vt v loc m =>
Set (NormalizedConstraints vt v loc)
-> GrdTree (PmGrd vt v loc) l
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
uncoverAnnotate Set (NormalizedConstraints vt v loc)
z GrdTree (PmGrd vt v loc) l
grdtree0 = Algebra
  (GrdTreeF (PmGrd vt v loc) l)
  (Set (NormalizedConstraints vt v loc)
   -> m (Set (NormalizedConstraints vt v loc),
         GrdTree
           (Set (NormalizedConstraints vt v loc))
           (Set (NormalizedConstraints vt v loc), l)))
-> GrdTree (PmGrd vt v loc) l
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
forall a.
Algebra (GrdTreeF (PmGrd vt v loc) l) a
-> GrdTree (PmGrd vt v loc) l -> a
forall t (f :: * -> *) a. Recursive t f => Algebra f a -> t -> a
cata Algebra
  (GrdTreeF (PmGrd vt v loc) l)
  (Set (NormalizedConstraints vt v loc)
   -> m (Set (NormalizedConstraints vt v loc),
         GrdTree
           (Set (NormalizedConstraints vt v loc))
           (Set (NormalizedConstraints vt v loc), l)))
phi GrdTree (PmGrd vt v loc) l
grdtree0 Set (NormalizedConstraints vt v loc)
z
  where
    phi :: Algebra
  (GrdTreeF (PmGrd vt v loc) l)
  (Set (NormalizedConstraints vt v loc)
   -> m (Set (NormalizedConstraints vt v loc),
         GrdTree
           (Set (NormalizedConstraints vt v loc))
           (Set (NormalizedConstraints vt v loc), l)))
phi = \case
      -- There is no way to fail matching a leaf, return the empty set
      -- to represent false.
      LeafF l
l -> \Set (NormalizedConstraints vt v loc)
nc -> do
        Set (NormalizedConstraints vt v loc)
nc' <- Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc))
ensureInhabited' Set (NormalizedConstraints vt v loc)
nc
        pure (Set (NormalizedConstraints vt v loc)
forall a. Set a
Set.empty, (Set (NormalizedConstraints vt v loc), l)
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
forall l n. l -> GrdTree n l
Leaf (Set (NormalizedConstraints vt v loc)
nc', l
l))
      ForkF [Set (NormalizedConstraints vt v loc)
 -> m (Set (NormalizedConstraints vt v loc),
       GrdTree
         (Set (NormalizedConstraints vt v loc))
         (Set (NormalizedConstraints vt v loc), l))]
ks -> \Set (NormalizedConstraints vt v loc)
nc0 -> do
        -- depth-first fold in match-case order to acculate the
        -- constraints for a match failure at every case.
        (Set (NormalizedConstraints vt v loc)
ncfinal, [GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l)]
ts) <- ((Set (NormalizedConstraints vt v loc),
  [GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)])
 -> (Set (NormalizedConstraints vt v loc)
     -> m (Set (NormalizedConstraints vt v loc),
           GrdTree
             (Set (NormalizedConstraints vt v loc))
             (Set (NormalizedConstraints vt v loc), l)))
 -> m (Set (NormalizedConstraints vt v loc),
       [GrdTree
          (Set (NormalizedConstraints vt v loc))
          (Set (NormalizedConstraints vt v loc), l)]))
-> (Set (NormalizedConstraints vt v loc),
    [GrdTree
       (Set (NormalizedConstraints vt v loc))
       (Set (NormalizedConstraints vt v loc), l)])
-> [Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l))]
-> m (Set (NormalizedConstraints vt v loc),
      [GrdTree
         (Set (NormalizedConstraints vt v loc))
         (Set (NormalizedConstraints vt v loc), l)])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\(Set (NormalizedConstraints vt v loc)
nc, [GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l)]
ts) Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
a -> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
a Set (NormalizedConstraints vt v loc)
nc m (Set (NormalizedConstraints vt v loc),
   GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l))
-> ((Set (NormalizedConstraints vt v loc),
     GrdTree
       (Set (NormalizedConstraints vt v loc))
       (Set (NormalizedConstraints vt v loc), l))
    -> m (Set (NormalizedConstraints vt v loc),
          [GrdTree
             (Set (NormalizedConstraints vt v loc))
             (Set (NormalizedConstraints vt v loc), l)]))
-> m (Set (NormalizedConstraints vt v loc),
      [GrdTree
         (Set (NormalizedConstraints vt v loc))
         (Set (NormalizedConstraints vt v loc), l)])
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Set (NormalizedConstraints vt v loc)
nc', GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t) -> (Set (NormalizedConstraints vt v loc),
 [GrdTree
    (Set (NormalizedConstraints vt v loc))
    (Set (NormalizedConstraints vt v loc), l)])
-> m (Set (NormalizedConstraints vt v loc),
      [GrdTree
         (Set (NormalizedConstraints vt v loc))
         (Set (NormalizedConstraints vt v loc), l)])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (NormalizedConstraints vt v loc)
nc', GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
-> [GrdTree
      (Set (NormalizedConstraints vt v loc))
      (Set (NormalizedConstraints vt v loc), l)]
-> [GrdTree
      (Set (NormalizedConstraints vt v loc))
      (Set (NormalizedConstraints vt v loc), l)]
forall a. a -> [a] -> [a]
: [GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l)]
ts)) (Set (NormalizedConstraints vt v loc)
nc0, []) [Set (NormalizedConstraints vt v loc)
 -> m (Set (NormalizedConstraints vt v loc),
       GrdTree
         (Set (NormalizedConstraints vt v loc))
         (Set (NormalizedConstraints vt v loc), l))]
ks
        (Set (NormalizedConstraints vt v loc),
 GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l))
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (NormalizedConstraints vt v loc)
ncfinal, [GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l)]
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
forall n l. [GrdTree n l] -> GrdTree n l
Fork ([GrdTree
    (Set (NormalizedConstraints vt v loc))
    (Set (NormalizedConstraints vt v loc), l)]
 -> GrdTree
      (Set (NormalizedConstraints vt v loc))
      (Set (NormalizedConstraints vt v loc), l))
-> [GrdTree
      (Set (NormalizedConstraints vt v loc))
      (Set (NormalizedConstraints vt v loc), l)]
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
forall a b. (a -> b) -> a -> b
$ [GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l)]
-> [GrdTree
      (Set (NormalizedConstraints vt v loc))
      (Set (NormalizedConstraints vt v loc), l)]
forall a. [a] -> [a]
reverse [GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l)]
ts)
      GrdF PmGrd vt v loc
grd Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k -> \Set (NormalizedConstraints vt v loc)
nc0 -> case PmGrd vt v loc
grd of
        PmEffect v
var ConstructorReference
con [(v, Type vt loc)]
convars -> Literal vt v loc
-> Literal vt v loc
-> (Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l)))
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
handleGrd (v -> EffectHandler -> [(v, Type vt loc)] -> Literal vt v loc
forall vt v loc.
v -> EffectHandler -> [(v, Type vt loc)] -> Literal vt v loc
PosEffect v
var (ConstructorReference -> EffectHandler
Effect ConstructorReference
con) [(v, Type vt loc)]
convars) (v -> EffectHandler -> Literal vt v loc
forall vt v loc. v -> EffectHandler -> Literal vt v loc
NegEffect v
var (ConstructorReference -> EffectHandler
Effect ConstructorReference
con)) Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0
        PmEffectPure v
var (v, Type vt loc)
resume -> Literal vt v loc
-> Literal vt v loc
-> (Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l)))
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
handleGrd (v -> EffectHandler -> [(v, Type vt loc)] -> Literal vt v loc
forall vt v loc.
v -> EffectHandler -> [(v, Type vt loc)] -> Literal vt v loc
PosEffect v
var EffectHandler
NoEffect [(v, Type vt loc)
resume]) (v -> EffectHandler -> Literal vt v loc
forall vt v loc. v -> EffectHandler -> Literal vt v loc
NegEffect v
var EffectHandler
NoEffect) Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0
        PmCon v
var ConstructorReference
con [(v, Type vt loc)]
convars -> do
          Literal vt v loc
-> Literal vt v loc
-> (Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l)))
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
handleGrd (v -> ConstructorReference -> [(v, Type vt loc)] -> Literal vt v loc
forall vt v loc.
v -> ConstructorReference -> [(v, Type vt loc)] -> Literal vt v loc
PosCon v
var ConstructorReference
con [(v, Type vt loc)]
convars) (v -> ConstructorReference -> Literal vt v loc
forall vt v loc. v -> ConstructorReference -> Literal vt v loc
NegCon v
var ConstructorReference
con) Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0
        PmLit v
var PmLit
lit -> do
          Literal vt v loc
-> Literal vt v loc
-> (Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l)))
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
handleGrd (v -> PmLit -> Literal vt v loc
forall vt v loc. v -> PmLit -> Literal vt v loc
PosLit v
var PmLit
lit) (v -> PmLit -> Literal vt v loc
forall vt v loc. v -> PmLit -> Literal vt v loc
NegLit v
var PmLit
lit) Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0
        PmListHead v
listVar Int
n v
el Type vt loc
elt -> do
          Set (NormalizedConstraints vt v loc)
nc <- Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
nc0 (v -> Int -> v -> Type vt loc -> Literal vt v loc
forall vt v loc. v -> Int -> v -> Type vt loc -> Literal vt v loc
PosListHead v
listVar Int
n v
el Type vt loc
elt)
          Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc
        PmListTail v
listVar Int
n v
el Type vt loc
elt -> do
          Set (NormalizedConstraints vt v loc)
nc <- Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
nc0 (v -> Int -> v -> Type vt loc -> Literal vt v loc
forall vt v loc. v -> Int -> v -> Type vt loc -> Literal vt v loc
PosListTail v
listVar Int
n v
el Type vt loc
elt)
          Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc
        PmListInterval v
listVar Int
lb Int
ub -> do
          let iset :: IntervalSet
iset = (Int, Int) -> IntervalSet
IntervalSet.singleton (Int
lb, Int
ub)
          Literal vt v loc
-> Literal vt v loc
-> (Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l)))
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
handleGrd (v -> IntervalSet -> Literal vt v loc
forall vt v loc. v -> IntervalSet -> Literal vt v loc
NegListInterval v
listVar (IntervalSet -> IntervalSet
IntervalSet.complement IntervalSet
iset)) (v -> IntervalSet -> Literal vt v loc
forall vt v loc. v -> IntervalSet -> Literal vt v loc
NegListInterval v
listVar IntervalSet
iset) Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0
        PmBang v
var -> do
          (Set (NormalizedConstraints vt v loc)
ncCont, GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t) <- Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0
          Set (NormalizedConstraints vt v loc)
ncEff <- Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
nc0 (v -> Literal vt v loc
forall vt v loc. v -> Literal vt v loc
Effectful v
var)
          let t' :: GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t' = Set (NormalizedConstraints vt v loc)
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
forall n l. n -> GrdTree n l -> GrdTree n l
Grd Set (NormalizedConstraints vt v loc)
ncEff GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t
          (Set (NormalizedConstraints vt v loc),
 GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l))
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (NormalizedConstraints vt v loc)
ncCont, GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t')
        PmLet v
var Term' vt v loc
expr Type vt loc
typ -> do
          Set (NormalizedConstraints vt v loc)
nc <- Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
nc0 (v -> Term' vt v loc -> Type vt loc -> Literal vt v loc
forall vt v loc.
v -> Term' vt v loc -> Type vt loc -> Literal vt v loc
Let v
var Term' vt v loc
expr Type vt loc
typ)
          Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc

    -- Constructors and literals are handled uniformly except that
    -- they pass different positive and negative literals.
    handleGrd :: Literal vt v loc
-> Literal vt v loc
-> (Set (NormalizedConstraints vt v loc)
    -> m (Set (NormalizedConstraints vt v loc),
          GrdTree
            (Set (NormalizedConstraints vt v loc))
            (Set (NormalizedConstraints vt v loc), l)))
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
handleGrd Literal vt v loc
pos Literal vt v loc
neg Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
nc0 = do
      Set (NormalizedConstraints vt v loc)
ncNoMatch <- Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
nc0 Literal vt v loc
neg
      Set (NormalizedConstraints vt v loc)
ncMatch <- Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
nc0 Literal vt v loc
pos
      (Set (NormalizedConstraints vt v loc)
ncMatch, GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t) <- Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
k Set (NormalizedConstraints vt v loc)
ncMatch
      -- A match can fail bacause it fails to match the immediate
      -- pattern or it can match the immediate pattern but fail to
      -- match some pattern or guard defined later in this same case.
      --
      -- This split can lead to an exponential number of terms, so we
      -- limit this growth to a constant, conservatively
      -- approximating. This is known as "throttling" in the paper and
      -- described in section 5.2.
      let ncFinalCandidate :: Set (NormalizedConstraints vt v loc)
ncFinalCandidate = Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (NormalizedConstraints vt v loc)
ncMatch Set (NormalizedConstraints vt v loc)
ncNoMatch
          ncFinal :: Set (NormalizedConstraints vt v loc)
ncFinal = case Set (NormalizedConstraints vt v loc) -> Int
forall a. Set a -> Int
Set.size Set (NormalizedConstraints vt v loc)
ncFinalCandidate Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
30 of
            Bool
True -> Set (NormalizedConstraints vt v loc)
nc0
            Bool
False -> Set (NormalizedConstraints vt v loc)
ncFinalCandidate
      (Set (NormalizedConstraints vt v loc),
 GrdTree
   (Set (NormalizedConstraints vt v loc))
   (Set (NormalizedConstraints vt v loc), l))
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (NormalizedConstraints vt v loc)
ncFinal, GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
t)

    ensureInhabited' ::
      Set (NormalizedConstraints vt v loc) ->
      m (Set (NormalizedConstraints vt v loc))
    ensureInhabited' :: Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc))
ensureInhabited' Set (NormalizedConstraints vt v loc)
ncs0 = (Set (NormalizedConstraints vt v loc)
 -> NormalizedConstraints vt v loc
 -> m (Set (NormalizedConstraints vt v loc)))
-> Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Set (NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
forall {f :: * -> *} {vt} {v} {loc}.
Pmc vt v loc f =>
Set (NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
phi Set (NormalizedConstraints vt v loc)
forall a. Set a
Set.empty Set (NormalizedConstraints vt v loc)
ncs0
      where
        phi :: Set (NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
phi Set (NormalizedConstraints vt v loc)
ncs NormalizedConstraints vt v loc
nc =
          Fuel
-> NormalizedConstraints vt v loc
-> f (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
ensureInhabited Fuel
initFuel NormalizedConstraints vt v loc
nc f (Maybe (NormalizedConstraints vt v loc))
-> (Maybe (NormalizedConstraints vt v loc)
    -> Set (NormalizedConstraints vt v loc))
-> f (Set (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            Maybe (NormalizedConstraints vt v loc)
Nothing -> Set (NormalizedConstraints vt v loc)
ncs
            Just NormalizedConstraints vt v loc
nc -> NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
forall a. Ord a => a -> Set a -> Set a
Set.insert NormalizedConstraints vt v loc
nc Set (NormalizedConstraints vt v loc)
ncs

    -- Add a literal to each term in our DNF, dropping terms that
    -- become contradictory
    addLiteral' ::
      Set (NormalizedConstraints vt v loc) ->
      Literal vt v loc ->
      m (Set (NormalizedConstraints vt v loc))
    addLiteral' :: Set (NormalizedConstraints vt v loc)
-> Literal vt v loc -> m (Set (NormalizedConstraints vt v loc))
addLiteral' Set (NormalizedConstraints vt v loc)
ncs0 Literal vt v loc
lit = (Set (NormalizedConstraints vt v loc)
 -> NormalizedConstraints vt v loc
 -> m (Set (NormalizedConstraints vt v loc)))
-> Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
-> m (Set (NormalizedConstraints vt v loc))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Set (NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
phi Set (NormalizedConstraints vt v loc)
forall a. Set a
Set.empty Set (NormalizedConstraints vt v loc)
ncs0
      where
        phi :: Set (NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
phi Set (NormalizedConstraints vt v loc)
ncs NormalizedConstraints vt v loc
nc =
          Literal vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Literal vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addLiteral Literal vt v loc
lit NormalizedConstraints vt v loc
nc m (Maybe (NormalizedConstraints vt v loc))
-> (Maybe (NormalizedConstraints vt v loc)
    -> Set (NormalizedConstraints vt v loc))
-> m (Set (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            Maybe (NormalizedConstraints vt v loc)
Nothing -> Set (NormalizedConstraints vt v loc)
ncs
            Just NormalizedConstraints vt v loc
nc -> NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
forall a. Ord a => a -> Set a -> Set a
Set.insert NormalizedConstraints vt v loc
nc Set (NormalizedConstraints vt v loc)
ncs

-- | Collect accessible, inaccessible, and redundant GRHSs
classify ::
  forall vt v loc l.
  GrdTree (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l) ->
  ([l], [l], [l])
classify :: forall vt v loc l.
GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
-> ([l], [l], [l])
classify = Algebra
  (GrdTreeF
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l))
  ([l], [l], [l])
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
-> ([l], [l], [l])
forall a.
Algebra
  (GrdTreeF
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l))
  a
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l)
-> a
forall t (f :: * -> *) a. Recursive t f => Algebra f a -> t -> a
cata Algebra
  (GrdTreeF
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), l))
  ([l], [l], [l])
forall vt v loc l.
GrdTreeF
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
  ([l], [l], [l])
-> ([l], [l], [l])
classifyAlg

classifyAlg ::
  forall vt v loc l.
  GrdTreeF (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l) ([l], [l], [l]) ->
  ([l], [l], [l])
classifyAlg :: forall vt v loc l.
GrdTreeF
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
  ([l], [l], [l])
-> ([l], [l], [l])
classifyAlg = \case
  LeafF (Set (NormalizedConstraints vt v loc)
rt, l
l) ->
    case Set (NormalizedConstraints vt v loc) -> Bool
forall {a}. Set a -> Bool
inh Set (NormalizedConstraints vt v loc)
rt of
      Bool
True -> ([l
l], [], [])
      Bool
False -> ([], [], [l
l])
  GrdF Set (NormalizedConstraints vt v loc)
rt ([l], [l], [l])
rest ->
    -- The presence of a 'GrdF' node indicates that an effect was
    -- performed (see 'uncoverAnnotate').
    case Set (NormalizedConstraints vt v loc) -> Bool
forall {a}. Set a -> Bool
inh Set (NormalizedConstraints vt v loc)
rt of
      Bool
True ->
        -- The rest of the subtree is redundant, but an effect is
        -- performed. Classify this as "Inaccessible".
        case ([l], [l], [l])
rest of
          ([], [], l
x : [l]
xs) -> ([], [l
x], [l]
xs)
          ([l], [l], [l])
_ -> ([l], [l], [l])
rest
      Bool
False -> ([l], [l], [l])
rest
  ForkF [([l], [l], [l])]
xs -> (([l], [l], [l]) -> ([l], [l], [l]) -> ([l], [l], [l]))
-> ([l], [l], [l]) -> [([l], [l], [l])] -> ([l], [l], [l])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\([l]
a, [l]
b, [l]
c) ~([l]
acc, [l]
inacc, [l]
redun) -> ([l]
a [l] -> [l] -> [l]
forall a. [a] -> [a] -> [a]
++ [l]
acc, [l]
b [l] -> [l] -> [l]
forall a. [a] -> [a] -> [a]
++ [l]
inacc, [l]
c [l] -> [l] -> [l]
forall a. [a] -> [a] -> [a]
++ [l]
redun)) ([], [], []) [([l], [l], [l])]
xs
  where
    -- inhabitation check
    inh :: Set a -> Bool
inh = Bool -> Bool
not (Bool -> Bool) -> (Set a -> Bool) -> Set a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> Bool
forall {a}. Set a -> Bool
Set.null

-- | Expand a full DNF term (i.e. each term identifies exactly one
-- solution) into an inhabiting pattern.
generateInhabitants ::
  forall vt v loc.
  (Var v) =>
  v ->
  NormalizedConstraints vt v loc ->
  Pattern ()
generateInhabitants :: forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
x NormalizedConstraints vt v loc
nc =
  let (v
_xcanon, VarInfo vt v loc
xvi, NormalizedConstraints vt v loc
nc') = v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
x NormalizedConstraints vt v loc
nc
   in 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
xvi of
        Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
_neg -> case Maybe (ConstructorReference, [(v, Type vt loc)])
pos of
          Maybe (ConstructorReference, [(v, Type vt loc)])
Nothing -> () -> Pattern ()
forall loc. loc -> Pattern loc
Pattern.Unbound ()
          Just (ConstructorReference
dc, [(v, Type vt loc)]
convars) ->
            () -> ConstructorReference -> [Pattern ()] -> Pattern ()
forall loc.
loc -> ConstructorReference -> [Pattern loc] -> Pattern loc
Pattern.Constructor () ConstructorReference
dc (((v, Type vt loc) -> Pattern ())
-> [(v, Type vt loc)] -> [Pattern ()]
forall a b. (a -> b) -> [a] -> [b]
map (\(v
v, Type vt loc
_) -> v -> NormalizedConstraints vt v loc -> Pattern ()
forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
v NormalizedConstraints vt v loc
nc') [(v, Type vt loc)]
convars)
        Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
_neg -> case Maybe (EffectHandler, [(v, Type vt loc)])
pos of
          Maybe (EffectHandler, [(v, Type vt loc)])
Nothing -> () -> Pattern ()
forall loc. loc -> Pattern loc
Pattern.Unbound ()
          Just (EffectHandler
effHandler, [(v, Type vt loc)]
convars) -> case EffectHandler
effHandler of
            EffectHandler
NoEffect -> () -> Pattern () -> Pattern ()
forall loc. loc -> Pattern loc -> Pattern loc
Pattern.EffectPure () case [(v, Type vt loc)]
convars of
              [(v
v, Type vt loc
_)] -> v -> NormalizedConstraints vt v loc -> Pattern ()
forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
v NormalizedConstraints vt v loc
nc'
              [(v, Type vt loc)]
_ -> [Char] -> Pattern ()
forall a. HasCallStack => [Char] -> a
error [Char]
"NoEffect has the incorrect number of convars"
            Effect ConstructorReference
cr -> ()
-> ConstructorReference -> [Pattern ()] -> Pattern () -> Pattern ()
forall loc.
loc
-> ConstructorReference
-> [Pattern loc]
-> Pattern loc
-> Pattern loc
Pattern.EffectBind () ConstructorReference
cr (((v, Type vt loc) -> Pattern ())
-> [(v, Type vt loc)] -> [Pattern ()]
forall a b. (a -> b) -> [a] -> [b]
map (\(v
v, Type vt loc
_) -> v -> NormalizedConstraints vt v loc -> Pattern ()
forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
v NormalizedConstraints vt v loc
nc') [(v, Type vt loc)]
convars) (() -> Pattern ()
forall loc. loc -> Pattern loc
Pattern.Unbound ())
        Vc'Boolean Maybe Bool
pos Set Bool
_neg -> case Maybe Bool
pos of
          Maybe Bool
Nothing -> () -> Pattern ()
forall loc. loc -> Pattern loc
Pattern.Unbound ()
          Just Bool
b -> () -> Bool -> Pattern ()
forall loc. loc -> Bool -> Pattern loc
Pattern.Boolean () Bool
b
        Vc'ListRoot Type vt loc
_typ Seq v
consPos Seq v
snocPos IntervalSet
intset ->
          let matchedLength :: Int
matchedLength = (Int -> Int -> Int) -> (Seq v -> Int) -> Seq v -> Seq v -> Int
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
consPos Seq v
snocPos
              mmaxLength :: Maybe Int
mmaxLength = IntervalSet -> Maybe Int
IntervalSet.lookupMax IntervalSet
intset
              matchIsIncomplete :: Bool
matchIsIncomplete = case Maybe Int
mmaxLength of
                Maybe Int
Nothing -> Bool
True
                Just Int
maxLength -> Int
matchedLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxLength
              rootPat :: Pattern ()
rootPat = case Bool
matchIsIncomplete of
                Bool
True -> () -> Pattern ()
forall loc. loc -> Pattern loc
Pattern.Unbound ()
                Bool
False -> () -> [Pattern ()] -> Pattern ()
forall loc. loc -> [Pattern loc] -> Pattern loc
Pattern.SequenceLiteral () []
              snoced :: Pattern ()
snoced = (v -> Pattern () -> Pattern ())
-> Pattern () -> Seq v -> Pattern ()
forall a b. (a -> b -> b) -> b -> Seq a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\v
a Pattern ()
b -> () -> Pattern () -> SeqOp -> Pattern () -> Pattern ()
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
Pattern.SequenceOp () Pattern ()
b SeqOp
Pattern.Snoc (v -> NormalizedConstraints vt v loc -> Pattern ()
forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
a NormalizedConstraints vt v loc
nc')) Pattern ()
rootPat Seq v
snocPos
              consed :: Pattern ()
consed = (v -> Pattern () -> Pattern ())
-> Pattern () -> Seq v -> Pattern ()
forall a b. (a -> b -> b) -> b -> Seq a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\v
a Pattern ()
b -> () -> Pattern () -> SeqOp -> Pattern () -> Pattern ()
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
Pattern.SequenceOp () (v -> NormalizedConstraints vt v loc -> Pattern ()
forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
a NormalizedConstraints vt v loc
nc') SeqOp
Pattern.Cons Pattern ()
b) Pattern ()
snoced Seq v
consPos
           in Pattern ()
consed
        VarConstraints vt v loc
_ -> () -> Pattern ()
forall loc. loc -> Pattern loc
Pattern.Unbound ()

-- | Instantiate a variable to a given constructor.
instantiate ::
  forall vt v loc x m.
  (Pmc vt v loc m) =>
  Fuel ->
  NormalizedConstraints vt v loc ->
  v ->
  -- | constructor
  x ->
  -- | type of datacon's args
  [Type vt loc] ->
  -- | produce positive constraint
  (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]) ->
  m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
instantiate :: forall vt v loc x (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> v
-> x
-> [Type vt loc]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
instantiate Fuel
fuel NormalizedConstraints vt v loc
nc v
x x
c [Type vt loc]
argTyps v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]
posConstraint = do
  -- todo: centralize this declVar logic. Currently in 'addLiteral' and here.
  [(v, Type vt loc)]
newVars :: [(var, typ)] <- (Type vt loc -> m (v, Type vt loc))
-> [Type vt loc] -> m [(v, Type vt loc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\Type vt loc
t -> (,Type vt loc
t) (v -> (v, Type vt loc)) -> m v -> m (v, Type vt loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m v
forall vt v loc (m :: * -> *). Pmc vt v loc m => m v
fresh) [Type vt loc]
argTyps
  let nc' :: NormalizedConstraints vt v loc
nc' = ((v, Type vt loc)
 -> NormalizedConstraints vt v loc
 -> NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> [(v, Type vt loc)]
-> NormalizedConstraints vt v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(v
v, Type vt loc
t) NormalizedConstraints vt v loc
b -> v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
forall a. a -> a
id NormalizedConstraints vt v loc
b) NormalizedConstraints vt v loc
nc [(v, Type vt loc)]
newVars
      cons :: [Constraint vt v loc]
cons = v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]
posConstraint v
x x
c [(v, Type vt loc)]
newVars
  Maybe (NormalizedConstraints vt v loc)
mnc <- MaybeT m (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
    NormalizedConstraints vt v loc
nc <- m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT ([Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraints [Constraint vt v loc]
cons NormalizedConstraints vt v loc
nc')
    -- mark all new fields as dirty as we need to ensure they are
    -- inhabited
    let nc' :: NormalizedConstraints vt v loc
nc' =
          -- HACK ALERT: Even if an ability handler constructor is
          -- uninhabited, the type system requires at least one
          -- constructor of the ability to be matched on to determine
          -- that it should dischange the ability. So, we don't do the
          -- inhabitation check if it is for an ability type that we
          -- haven't handled in a prior case.
          let (v
_xcanon, VarInfo vt v loc
xvi, NormalizedConstraints vt v loc
_) = v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
x NormalizedConstraints vt v loc
nc
              missingEffectBind :: TypeReference -> t EffectHandler -> Bool
missingEffectBind TypeReference
r t EffectHandler
neg =
                (EffectHandler -> Bool -> Bool) -> Bool -> t EffectHandler -> Bool
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
                  ( \EffectHandler
a Bool
b -> case EffectHandler
a of
                      Effect ConstructorReference
cr | Getting TypeReference ConstructorReference TypeReference
-> ConstructorReference -> TypeReference
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting TypeReference ConstructorReference TypeReference
forall r s (f :: * -> *).
Functor f =>
(r -> f s)
-> GConstructorReference r -> f (GConstructorReference s)
reference_ ConstructorReference
cr TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
r -> Bool
False
                      EffectHandler
_ -> Bool
b
                  )
                  Bool
True
                  t EffectHandler
neg
           in 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
xvi of
                Vc'Effect (Just (Effect ConstructorReference
cr, [(v, Type vt loc)]
_)) Set EffectHandler
neg | TypeReference -> Set EffectHandler -> Bool
forall {t :: * -> *}.
Foldable t =>
TypeReference -> t EffectHandler -> Bool
missingEffectBind (Getting TypeReference ConstructorReference TypeReference
-> ConstructorReference -> TypeReference
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting TypeReference ConstructorReference TypeReference
forall r s (f :: * -> *).
Functor f =>
(r -> f s)
-> GConstructorReference r -> f (GConstructorReference s)
reference_ ConstructorReference
cr) Set EffectHandler
neg -> NormalizedConstraints vt v loc
nc
                VarConstraints vt v loc
_ -> ((v, Type vt loc)
 -> NormalizedConstraints vt v loc
 -> NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> [(v, Type vt loc)]
-> NormalizedConstraints vt v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(v
v, Type vt loc
_) NormalizedConstraints vt v loc
b -> 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 NormalizedConstraints vt v loc
b) NormalizedConstraints vt v loc
nc [(v, Type vt loc)]
newVars
    -- branching factor
    let newFuel :: Fuel
newFuel = case [(v, Type vt loc)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(v, Type vt loc)]
newVars Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 of
          Bool
True -> Fuel -> Fuel -> Fuel
forall a. Ord a => a -> a -> a
min Fuel
fuel Fuel
3
          Bool
False -> Fuel
fuel
    -- we must ensure that all strict fields are inhabited
    m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Fuel
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
ensureInhabited Fuel
newFuel NormalizedConstraints vt v loc
nc')
  pure ((\NormalizedConstraints vt v loc
x -> (NormalizedConstraints vt v loc
x, [(v, Type vt loc)]
newVars)) (NormalizedConstraints vt v loc
 -> (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
-> Maybe (NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (NormalizedConstraints vt v loc)
mnc)

-- | Given a variable and a term in DNF, expand it to an identical DNF
-- expression with enough positive info to print pattern suggestions.
expandSolution ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  v ->
  NormalizedConstraints vt v loc ->
  m (Set (NormalizedConstraints vt v loc))
expandSolution :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
expandSolution v
x NormalizedConstraints vt v loc
nc =
  let go :: a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go a
fuel v
x NormalizedConstraints vt v loc
nc
        -- If we run out of fuel conservatively assume the term is
        -- inhabited.
        | a
fuel a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
forall a. a -> Set a
Set.singleton NormalizedConstraints vt v loc
nc)
        | Bool
otherwise =
            let (v
_xcanon, VarInfo vt v loc
xvi, NormalizedConstraints vt v loc
nc') = v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
x NormalizedConstraints vt v loc
nc
             in f (Set (NormalizedConstraints vt v loc))
-> VarInfo vt v loc
-> (forall x.
    [(x, [Type vt loc])]
    -> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
    -> (v -> x -> Constraint vt v loc)
    -> f (Set (NormalizedConstraints vt v loc)))
-> f (Set (NormalizedConstraints vt v loc))
forall vt v loc r (m :: * -> *).
Pmc vt v loc m =>
m r
-> VarInfo vt v loc
-> (forall x.
    [(x, [Type vt loc])]
    -> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
    -> (v -> x -> Constraint vt v loc)
    -> m r)
-> m r
withConstructors (Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
forall a. a -> Set a
Set.singleton NormalizedConstraints vt v loc
nc')) VarInfo vt v loc
xvi \[(x, [Type vt loc])]
cs v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]
posConstraint v -> x -> Constraint vt v loc
_negConstraint ->
                  -- We have some constructors to attempt
                  -- instantiation with. Instantiate each one, if
                  -- doesn't lead to a contradiction then add it to
                  -- the set of valid solutions.
                  let phi :: (x, [Type vt loc]) -> f (Set (NormalizedConstraints vt v loc))
phi (x
cref, [Type vt loc]
cvt) = do
                        Fuel
-> NormalizedConstraints vt v loc
-> v
-> x
-> [Type vt loc]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> f (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
forall vt v loc x (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> v
-> x
-> [Type vt loc]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
instantiate Fuel
initFuel NormalizedConstraints vt v loc
nc' v
x x
cref [Type vt loc]
cvt v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]
posConstraint f (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
-> (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)])
    -> f (Set (NormalizedConstraints vt v loc)))
-> f (Set (NormalizedConstraints vt v loc))
forall a b. f a -> (a -> f b) -> f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                          Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)])
Nothing -> Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set (NormalizedConstraints vt v loc)
forall a. Set a
Set.empty -- contradiction
                          Just (NormalizedConstraints vt v loc
nc'', [(v, Type vt loc)]
newVars) -> case [(v, Type vt loc)]
newVars of
                            [] -> Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
forall a. a -> Set a
Set.singleton NormalizedConstraints vt v loc
nc'')
                            [(v, Type vt loc)]
_ ->
                              -- If we have the match expression:
                              -- @
                              -- match blerg : Maybe (Maybe ()) with
                              --   Nothing -> ()
                              --   Just Nothing -> ()
                              -- @
                              --
                              -- Then we would like to suggest @Just (Just _)@ rather than @Just _@.
                              -- To accomplish this, we recurse and expand variables for which we have
                              -- positive or negative information.

                              -- branching factor
                              let newFuel :: a
newFuel = case [(v, Type vt loc)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(v, Type vt loc)]
newVars Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 of
                                    Bool
True -> a -> a -> a
forall a. Ord a => a -> a -> a
min a
fuel a
3
                                    Bool
False -> a
fuel
                               in [NormalizedConstraints vt v loc]
-> Set (NormalizedConstraints vt v loc)
forall a. Ord a => [a] -> Set a
Set.fromList
                                    ([NormalizedConstraints vt v loc]
 -> Set (NormalizedConstraints vt v loc))
-> f [NormalizedConstraints vt v loc]
-> f (Set (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([NormalizedConstraints vt v loc]
 -> (v, Type vt loc) -> f [NormalizedConstraints vt v loc])
-> [NormalizedConstraints vt v loc]
-> [(v, Type vt loc)]
-> f [NormalizedConstraints vt v loc]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
                                      ( \[NormalizedConstraints vt v loc]
b (v
v, Type vt loc
_t) ->
                                          Set (NormalizedConstraints vt v loc)
-> [NormalizedConstraints vt v loc]
forall a. Set a -> [a]
Set.toList (Set (NormalizedConstraints vt v loc)
 -> [NormalizedConstraints vt v loc])
-> ([Set (NormalizedConstraints vt v loc)]
    -> Set (NormalizedConstraints vt v loc))
-> [Set (NormalizedConstraints vt v loc)]
-> [NormalizedConstraints vt v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set (NormalizedConstraints vt v loc)]
-> Set (NormalizedConstraints vt v loc)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                                            ([Set (NormalizedConstraints vt v loc)]
 -> [NormalizedConstraints vt v loc])
-> f [Set (NormalizedConstraints vt v loc)]
-> f [NormalizedConstraints vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NormalizedConstraints vt v loc
 -> f (Set (NormalizedConstraints vt v loc)))
-> [NormalizedConstraints vt v loc]
-> f [Set (NormalizedConstraints vt v loc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
                                              ( \NormalizedConstraints vt v loc
nc ->
                                                  case v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
v NormalizedConstraints vt v loc
nc of
                                                    (v
_vc, VarInfo vt v loc
vi, NormalizedConstraints vt v loc
nc') -> 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
                                                        -- always instantiate unit, this ensures we print tuple patterns correctly
                                                        | Type.Ref' TypeReference
x <- 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, TypeReference
x TypeReference -> TypeReference -> Bool
forall a. Eq a => a -> a -> Bool
== TypeReference
unitRef -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go a
newFuel v
v NormalizedConstraints vt v loc
nc'
                                                        | Just (ConstructorReference, [(v, Type vt loc)])
_ <- Maybe (ConstructorReference, [(v, Type vt loc)])
pos -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go a
newFuel v
v NormalizedConstraints vt v loc
nc'
                                                        | Bool -> Bool
not (Set ConstructorReference -> Bool
forall {a}. Set a -> Bool
Set.null Set ConstructorReference
neg) -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go (a
newFuel a -> a -> a
forall a. Num a => a -> a -> a
- a
1) v
v NormalizedConstraints vt v loc
nc'
                                                      Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg
                                                        | Just (EffectHandler, [(v, Type vt loc)])
_ <- Maybe (EffectHandler, [(v, Type vt loc)])
pos -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go a
newFuel v
v NormalizedConstraints vt v loc
nc'
                                                        | Bool -> Bool
not (Set EffectHandler -> Bool
forall {a}. Set a -> Bool
Set.null Set EffectHandler
neg) -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go (a
newFuel a -> a -> a
forall a. Num a => a -> a -> a
- a
1) v
v NormalizedConstraints vt v loc
nc'
                                                      Vc'Boolean Maybe Bool
_pos Set Bool
neg
                                                        | Bool -> Bool
not (Set Bool -> Bool
forall {a}. Set a -> Bool
Set.null Set Bool
neg) -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go (a
newFuel a -> a -> a
forall a. Num a => a -> a -> a
- a
1) v
v NormalizedConstraints vt v loc
nc'
                                                      Vc'ListRoot Type vt loc
_typ Seq v
_posCons Seq v
_posSnoc IntervalSet
neg
                                                        | Bool -> Bool
not ((Int, Int) -> IntervalSet
IntervalSet.singleton (Int
0, Int
forall a. Bounded a => a
maxBound) IntervalSet -> IntervalSet -> Bool
forall a. Eq a => a -> a -> Bool
== IntervalSet
neg) -> a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go (a
newFuel a -> a -> a
forall a. Num a => a -> a -> a
- a
1) v
v NormalizedConstraints vt v loc
nc'
                                                      VarConstraints vt v loc
_ -> Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
forall a. a -> Set a
Set.singleton NormalizedConstraints vt v loc
nc')
                                              )
                                              [NormalizedConstraints vt v loc]
b
                                      )
                                      [NormalizedConstraints vt v loc
nc'']
                                      [(v, Type vt loc)]
newVars
                   in ((x, [Type vt loc])
 -> (Set (NormalizedConstraints vt v loc)
     -> f (Set (NormalizedConstraints vt v loc)))
 -> Set (NormalizedConstraints vt v loc)
 -> f (Set (NormalizedConstraints vt v loc)))
-> (Set (NormalizedConstraints vt v loc)
    -> f (Set (NormalizedConstraints vt v loc)))
-> [(x, [Type vt loc])]
-> Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(x, [Type vt loc])
a Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
b Set (NormalizedConstraints vt v loc)
s -> (x, [Type vt loc]) -> f (Set (NormalizedConstraints vt v loc))
phi (x, [Type vt loc])
a f (Set (NormalizedConstraints vt v loc))
-> (Set (NormalizedConstraints vt v loc)
    -> f (Set (NormalizedConstraints vt v loc)))
-> f (Set (NormalizedConstraints vt v loc))
forall a b. f a -> (a -> f b) -> f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Set (NormalizedConstraints vt v loc)
a' -> Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
b (Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
-> Set (NormalizedConstraints vt v loc)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (NormalizedConstraints vt v loc)
a' Set (NormalizedConstraints vt v loc)
s)) Set (NormalizedConstraints vt v loc)
-> f (Set (NormalizedConstraints vt v loc))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(x, [Type vt loc])]
cs Set (NormalizedConstraints vt v loc)
forall a. Set a
Set.empty
   in Fuel
-> v
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
forall {f :: * -> *} {vt} {v} {loc} {a}.
(Pmc vt v loc f, Num a, Ord a) =>
a
-> v
-> NormalizedConstraints vt v loc
-> f (Set (NormalizedConstraints vt v loc))
go Fuel
initFuel v
x NormalizedConstraints vt v loc
nc

withConstructors ::
  forall vt v loc r m.
  (Pmc vt v loc m) =>
  m r ->
  VarInfo vt v loc ->
  ( forall x.
    [(x, [Type vt loc])] ->
    (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]) ->
    (v -> x -> Constraint vt v loc) ->
    m r
  ) ->
  m r
withConstructors :: forall vt v loc r (m :: * -> *).
Pmc vt v loc m =>
m r
-> VarInfo vt v loc
-> (forall x.
    [(x, [Type vt loc])]
    -> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
    -> (v -> x -> Constraint vt v loc)
    -> m r)
-> m r
withConstructors m r
nil VarInfo vt v loc
vinfo forall x.
[(x, [Type vt loc])]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> x -> Constraint vt v loc)
-> m r
k = do
  Type vt loc -> m (EnumeratedConstructors vt v loc)
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Type vt loc -> m (EnumeratedConstructors vt v loc)
getConstructors Type vt loc
typ m (EnumeratedConstructors vt v loc)
-> (EnumeratedConstructors vt v loc -> m r) -> m r
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    AbilityType Type vt loc
resultType Map ConstructorReference (v, Type vt loc)
cs -> do
      [(EffectHandler, [Type vt loc])]
arg <- [(ConstructorReference, (v, Type vt loc))]
-> ((ConstructorReference, (v, Type vt loc))
    -> m (EffectHandler, [Type vt loc]))
-> m [(EffectHandler, [Type vt loc])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (Map ConstructorReference (v, Type vt loc)
-> [(ConstructorReference, (v, Type vt loc))]
forall k a. Map k a -> [(k, a)]
Map.toList Map ConstructorReference (v, Type vt loc)
cs) \(ConstructorReference
cref, (v, Type vt loc)
_) -> do
        [Type vt loc]
cvts <- Type vt loc -> ConstructorReference -> m [Type vt loc]
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Type vt loc -> ConstructorReference -> m [Type vt loc]
getConstructorVarTypes Type vt loc
typ ConstructorReference
cref
        pure (ConstructorReference -> EffectHandler
Effect ConstructorReference
cref, [Type vt loc]
cvts)
      [(EffectHandler, [Type vt loc])]
-> (v
    -> EffectHandler -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> EffectHandler -> Constraint vt v loc)
-> m r
forall x.
[(x, [Type vt loc])]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> x -> Constraint vt v loc)
-> m r
k ((EffectHandler
NoEffect, [Type vt loc
resultType]) (EffectHandler, [Type vt loc])
-> [(EffectHandler, [Type vt loc])]
-> [(EffectHandler, [Type vt loc])]
forall a. a -> [a] -> [a]
: [(EffectHandler, [Type vt loc])]
arg) (\v
v EffectHandler
cref [(v, Type vt loc)]
args -> [v -> EffectHandler -> [(v, Type vt loc)] -> Constraint vt v loc
forall vt v loc.
v -> EffectHandler -> [(v, Type vt loc)] -> Constraint vt v loc
C.PosEffect v
v EffectHandler
cref [(v, Type vt loc)]
args]) (\v
v EffectHandler
cref -> v -> EffectHandler -> Constraint vt v loc
forall vt v loc. v -> EffectHandler -> Constraint vt v loc
C.NegEffect v
v EffectHandler
cref)
    ConstructorType [(v, ConstructorReference, Type vt loc)]
cs -> do
      [(ConstructorReference, [Type vt loc])]
arg <- [(v, ConstructorReference, Type vt loc)]
-> ((v, ConstructorReference, Type vt loc)
    -> m (ConstructorReference, [Type vt loc]))
-> m [(ConstructorReference, [Type vt loc])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(v, ConstructorReference, Type vt loc)]
cs \(v
_, ConstructorReference
cref, Type vt loc
_) -> do
        [Type vt loc]
cvts <- Type vt loc -> ConstructorReference -> m [Type vt loc]
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Type vt loc -> ConstructorReference -> m [Type vt loc]
getConstructorVarTypes Type vt loc
typ ConstructorReference
cref
        pure (ConstructorReference
cref, [Type vt loc]
cvts)
      [(ConstructorReference, [Type vt loc])]
-> (v
    -> ConstructorReference
    -> [(v, Type vt loc)]
    -> [Constraint vt v loc])
-> (v -> ConstructorReference -> Constraint vt v loc)
-> m r
forall x.
[(x, [Type vt loc])]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> x -> Constraint vt v loc)
-> m r
k [(ConstructorReference, [Type vt loc])]
arg (\v
v ConstructorReference
cref [(v, Type vt loc)]
args -> [v
-> ConstructorReference
-> [(v, Type vt loc)]
-> Constraint vt v loc
forall vt v loc.
v
-> ConstructorReference
-> [(v, Type vt loc)]
-> Constraint vt v loc
C.PosCon v
v ConstructorReference
cref [(v, Type vt loc)]
args]) (\v
v ConstructorReference
cref -> v -> ConstructorReference -> Constraint vt v loc
forall vt v loc. v -> ConstructorReference -> Constraint vt v loc
C.NegCon v
v ConstructorReference
cref)
    SequenceType [(ListPat, [Type vt loc])]
_cs ->
      let Vc'ListRoot Type vt loc
elemType Seq v
consPos Seq v
snocPos IntervalSet
iset = 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
vinfo of
            Vc'ListRoot {} -> 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
vinfo
            VarConstraints vt v loc
_ -> [Char] -> VarConstraints vt v loc
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: constraint for sequence type not a list root"
          varCount :: Int
varCount = Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
consPos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
snocPos
          minLen :: Int
minLen = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ IntervalSet -> Maybe Int
IntervalSet.lookupMin IntervalSet
iset

          mkPosCons :: (Int -> [v] -> [Constraint vt v loc]) -> Int -> [v] -> [Constraint vt v loc]
          mkPosCons :: (Int -> [v] -> [Constraint vt v loc])
-> Int -> [v] -> [Constraint vt v loc]
mkPosCons Int -> [v] -> [Constraint vt v loc]
z Int
elvs0 = (v
 -> (Int -> [v] -> [Constraint vt v loc])
 -> Int
 -> [v]
 -> [Constraint vt v loc])
-> (Int -> [v] -> [Constraint vt v loc])
-> Seq v
-> Int
-> [v]
-> [Constraint vt v loc]
forall a b. (a -> b -> b) -> b -> Seq a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\v
_ Int -> [v] -> [Constraint vt v loc]
b Int
n (v
elv : [v]
elvs) -> v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListHead v
v Int
n v
elv Constraint vt v loc
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. a -> [a] -> [a]
: Int -> [v] -> [Constraint vt v loc]
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [v]
elvs) Int -> [v] -> [Constraint vt v loc]
z Seq v
consPos Int
elvs0

          mkPosSnoc :: (Int -> [v] -> [Constraint vt v loc]) -> Int -> [v] -> [Constraint vt v loc]
          mkPosSnoc :: (Int -> [v] -> [Constraint vt v loc])
-> Int -> [v] -> [Constraint vt v loc]
mkPosSnoc Int -> [v] -> [Constraint vt v loc]
z Int
elvs0 = (v
 -> (Int -> [v] -> [Constraint vt v loc])
 -> Int
 -> [v]
 -> [Constraint vt v loc])
-> (Int -> [v] -> [Constraint vt v loc])
-> Seq v
-> Int
-> [v]
-> [Constraint vt v loc]
forall a b. (a -> b -> b) -> b -> Seq a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\v
_ Int -> [v] -> [Constraint vt v loc]
b Int
n (v
elv : [v]
elvs) -> v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListTail v
v Int
n v
elv Constraint vt v loc
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. a -> [a] -> [a]
: Int -> [v] -> [Constraint vt v loc]
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [v]
elvs) Int -> [v] -> [Constraint vt v loc]
z Seq v
snocPos Int
elvs0

          constraints :: [(([(v, Type vt loc)] -> [Constraint vt v loc], Constraint vt v loc), [Type vt loc])]
          constraints :: [(([(v, Type vt loc)] -> [Constraint vt v loc],
   Constraint vt v loc),
  [Type vt loc])]
constraints =
            let mk :: ([v] -> [Constraint vt v loc])
-> [(v, Type vt loc)] -> [Constraint vt v loc]
mk [v] -> [Constraint vt v loc]
f [(v, Type vt loc)]
elvs = (Int -> [v] -> [Constraint vt v loc])
-> Int -> [v] -> [Constraint vt v loc]
mkPosCons (\Int
_ [v]
elvs -> (Int -> [v] -> [Constraint vt v loc])
-> Int -> [v] -> [Constraint vt v loc]
mkPosSnoc (\Int
_ [v]
elvs -> [v] -> [Constraint vt v loc]
f [v]
elvs) Int
0 [v]
elvs) Int
0 (((v, Type vt loc) -> v) -> [(v, Type vt loc)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map (v, Type vt loc) -> v
forall a b. (a, b) -> a
fst [(v, Type vt loc)]
elvs)
             in [ ((([v] -> [Constraint vt v loc])
-> [(v, Type vt loc)] -> [Constraint vt v loc]
mk \[] -> [], v -> IntervalSet -> Constraint vt v loc
forall vt v loc. v -> IntervalSet -> Constraint vt v loc
C.NegListInterval v
v ((Int, Int) -> IntervalSet
IntervalSet.singleton (Int
minLen, Int
forall a. Bounded a => a
maxBound))), Int -> Type vt loc -> [Type vt loc]
forall a. Int -> a -> [a]
replicate Int
varCount Type vt loc
elemType)
                ]

          mkPos :: p -> (t -> t, b) -> t -> t
mkPos p
_v (t -> t
pos, b
_neg) t
args =
            t -> t
pos t
args
          mkNeg :: p -> (a, b) -> b
mkNeg p
_v (a
_pos, b
neg) =
            b
neg
       in [(([(v, Type vt loc)] -> [Constraint vt v loc],
   Constraint vt v loc),
  [Type vt loc])]
-> (v
    -> ([(v, Type vt loc)] -> [Constraint vt v loc],
        Constraint vt v loc)
    -> [(v, Type vt loc)]
    -> [Constraint vt v loc])
-> (v
    -> ([(v, Type vt loc)] -> [Constraint vt v loc],
        Constraint vt v loc)
    -> Constraint vt v loc)
-> m r
forall x.
[(x, [Type vt loc])]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> x -> Constraint vt v loc)
-> m r
k [(([(v, Type vt loc)] -> [Constraint vt v loc],
   Constraint vt v loc),
  [Type vt loc])]
constraints v
-> ([(v, Type vt loc)] -> [Constraint vt v loc],
    Constraint vt v loc)
-> [(v, Type vt loc)]
-> [Constraint vt v loc]
forall {p} {t} {t} {b}. p -> (t -> t, b) -> t -> t
mkPos v
-> ([(v, Type vt loc)] -> [Constraint vt v loc],
    Constraint vt v loc)
-> Constraint vt v loc
forall {p} {a} {b}. p -> (a, b) -> b
mkNeg
    EnumeratedConstructors vt v loc
BooleanType -> do
      [(Bool, [Type vt loc])]
-> (v -> Bool -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> Bool -> Constraint vt v loc)
-> m r
forall x.
[(x, [Type vt loc])]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> (v -> x -> Constraint vt v loc)
-> m r
k [(Bool
True, []), (Bool
False, [])] (\v
v Bool
b [(v, Type vt loc)]
_ -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
C.PosLit v
v (Bool -> PmLit
PmLit.Boolean Bool
b)]) (\v
v Bool
b -> v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
C.NegLit v
v (Bool -> PmLit
PmLit.Boolean Bool
b))
    EnumeratedConstructors vt v loc
OtherType -> m r
nil
  where
    typ :: Type vt loc
typ = VarInfo vt v loc -> Type vt loc
forall vt v loc. VarInfo vt v loc -> Type vt loc
vi_typ VarInfo vt v loc
vinfo
    v :: v
v = VarInfo vt v loc -> v
forall vt v loc. VarInfo vt v loc -> v
vi_id VarInfo vt v loc
vinfo

-- | Test that the given variable is inhabited. This test is
-- undecidable in general so we adopt a fuel based approach as
-- described in section 3.7.
inhabited ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  Fuel ->
  v ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
inhabited :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> v
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
inhabited Fuel
fuel v
x NormalizedConstraints vt v loc
nc0 =
  let (v
_xcanon, VarInfo vt v loc
xvi, NormalizedConstraints vt v loc
nc') = v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
x NormalizedConstraints vt v loc
nc0
      -- more ability handler hack stuff
      --
      -- We don't want to add a negative effect constraint as we want
      -- to ensure there is at least one constructor given per
      -- ability.
      shouldAddNegative :: Bool
      shouldAddNegative :: Bool
shouldAddNegative = 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
xvi of
        Vc'Effect {} -> Bool
False
        VarConstraints vt v loc
_ -> Bool
True
   in m (Maybe (NormalizedConstraints vt v loc))
-> VarInfo vt v loc
-> (forall x.
    [(x, [Type vt loc])]
    -> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
    -> (v -> x -> Constraint vt v loc)
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc r (m :: * -> *).
Pmc vt v loc m =>
m r
-> VarInfo vt v loc
-> (forall x.
    [(x, [Type vt loc])]
    -> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
    -> (v -> x -> Constraint vt v loc)
    -> m r)
-> m r
withConstructors (Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a. a -> Maybe a
Just NormalizedConstraints vt v loc
nc')) VarInfo vt v loc
xvi \[(x, [Type vt loc])]
cs v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]
posConstraint v -> x -> Constraint vt v loc
negConstraint ->
        -- one of the constructors must be inhabited, Return the
        -- first non-contradictory instantiation.
        let phi :: (x, [Type vt loc])
-> (NormalizedConstraints vt v loc
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
phi (x
cref, [Type vt loc]
cvt) NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
b NormalizedConstraints vt v loc
nc = do
              Fuel
-> NormalizedConstraints vt v loc
-> v
-> x
-> [Type vt loc]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
forall vt v loc x (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> v
-> x
-> [Type vt loc]
-> (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc])
-> m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
instantiate Fuel
fuel NormalizedConstraints vt v loc
nc v
x x
cref [Type vt loc]
cvt v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]
posConstraint m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)]))
-> (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)])
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> m (Maybe (NormalizedConstraints vt v loc))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)])
Nothing -> do
                  case Bool
shouldAddNegative of
                    Bool
True ->
                      -- record failed instantiation attempt so we don't
                      -- attempt to instantiate this constructor again
                      Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> x -> Constraint vt v loc
negConstraint v
x x
cref) NormalizedConstraints vt v loc
nc m (Maybe (NormalizedConstraints vt v loc))
-> (Maybe (NormalizedConstraints vt v loc)
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> m (Maybe (NormalizedConstraints vt v loc))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                        Maybe (NormalizedConstraints vt v loc)
Nothing -> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
b NormalizedConstraints vt v loc
nc
                        Just NormalizedConstraints vt v loc
nc -> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
b NormalizedConstraints vt v loc
nc
                    Bool
False -> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
b NormalizedConstraints vt v loc
nc
                Just (NormalizedConstraints vt v loc, [(v, Type vt loc)])
_ -> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a. a -> Maybe a
Just NormalizedConstraints vt v loc
nc)
         in ((x, [Type vt loc])
 -> (NormalizedConstraints vt v loc
     -> m (Maybe (NormalizedConstraints vt v loc)))
 -> NormalizedConstraints vt v loc
 -> m (Maybe (NormalizedConstraints vt v loc)))
-> (NormalizedConstraints vt v loc
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> [(x, [Type vt loc])]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (x, [Type vt loc])
-> (NormalizedConstraints vt v loc
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
phi (\NormalizedConstraints vt v loc
_ -> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (NormalizedConstraints vt v loc)
forall a. Maybe a
Nothing) [(x, [Type vt loc])]
cs NormalizedConstraints vt v loc
nc'

newtype Fuel = Fuel Int
  deriving newtype (Int -> Fuel -> ShowS
[Fuel] -> ShowS
Fuel -> [Char]
(Int -> Fuel -> ShowS)
-> (Fuel -> [Char]) -> ([Fuel] -> ShowS) -> Show Fuel
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Fuel -> ShowS
showsPrec :: Int -> Fuel -> ShowS
$cshow :: Fuel -> [Char]
show :: Fuel -> [Char]
$cshowList :: [Fuel] -> ShowS
showList :: [Fuel] -> ShowS
Show, Fuel -> Fuel -> Bool
(Fuel -> Fuel -> Bool) -> (Fuel -> Fuel -> Bool) -> Eq Fuel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Fuel -> Fuel -> Bool
== :: Fuel -> Fuel -> Bool
$c/= :: Fuel -> Fuel -> Bool
/= :: Fuel -> Fuel -> Bool
Eq, Eq Fuel
Eq Fuel =>
(Fuel -> Fuel -> Ordering)
-> (Fuel -> Fuel -> Bool)
-> (Fuel -> Fuel -> Bool)
-> (Fuel -> Fuel -> Bool)
-> (Fuel -> Fuel -> Bool)
-> (Fuel -> Fuel -> Fuel)
-> (Fuel -> Fuel -> Fuel)
-> Ord Fuel
Fuel -> Fuel -> Bool
Fuel -> Fuel -> Ordering
Fuel -> Fuel -> Fuel
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 :: Fuel -> Fuel -> Ordering
compare :: Fuel -> Fuel -> Ordering
$c< :: Fuel -> Fuel -> Bool
< :: Fuel -> Fuel -> Bool
$c<= :: Fuel -> Fuel -> Bool
<= :: Fuel -> Fuel -> Bool
$c> :: Fuel -> Fuel -> Bool
> :: Fuel -> Fuel -> Bool
$c>= :: Fuel -> Fuel -> Bool
>= :: Fuel -> Fuel -> Bool
$cmax :: Fuel -> Fuel -> Fuel
max :: Fuel -> Fuel -> Fuel
$cmin :: Fuel -> Fuel -> Fuel
min :: Fuel -> Fuel -> Fuel
Ord, Int -> Fuel
Fuel -> Int
Fuel -> [Fuel]
Fuel -> Fuel
Fuel -> Fuel -> [Fuel]
Fuel -> Fuel -> Fuel -> [Fuel]
(Fuel -> Fuel)
-> (Fuel -> Fuel)
-> (Int -> Fuel)
-> (Fuel -> Int)
-> (Fuel -> [Fuel])
-> (Fuel -> Fuel -> [Fuel])
-> (Fuel -> Fuel -> [Fuel])
-> (Fuel -> Fuel -> Fuel -> [Fuel])
-> Enum Fuel
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Fuel -> Fuel
succ :: Fuel -> Fuel
$cpred :: Fuel -> Fuel
pred :: Fuel -> Fuel
$ctoEnum :: Int -> Fuel
toEnum :: Int -> Fuel
$cfromEnum :: Fuel -> Int
fromEnum :: Fuel -> Int
$cenumFrom :: Fuel -> [Fuel]
enumFrom :: Fuel -> [Fuel]
$cenumFromThen :: Fuel -> Fuel -> [Fuel]
enumFromThen :: Fuel -> Fuel -> [Fuel]
$cenumFromTo :: Fuel -> Fuel -> [Fuel]
enumFromTo :: Fuel -> Fuel -> [Fuel]
$cenumFromThenTo :: Fuel -> Fuel -> Fuel -> [Fuel]
enumFromThenTo :: Fuel -> Fuel -> Fuel -> [Fuel]
Enum, Fuel
Fuel -> Fuel -> Bounded Fuel
forall a. a -> a -> Bounded a
$cminBound :: Fuel
minBound :: Fuel
$cmaxBound :: Fuel
maxBound :: Fuel
Bounded, Integer -> Fuel
Fuel -> Fuel
Fuel -> Fuel -> Fuel
(Fuel -> Fuel -> Fuel)
-> (Fuel -> Fuel -> Fuel)
-> (Fuel -> Fuel -> Fuel)
-> (Fuel -> Fuel)
-> (Fuel -> Fuel)
-> (Fuel -> Fuel)
-> (Integer -> Fuel)
-> Num Fuel
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Fuel -> Fuel -> Fuel
+ :: Fuel -> Fuel -> Fuel
$c- :: Fuel -> Fuel -> Fuel
- :: Fuel -> Fuel -> Fuel
$c* :: Fuel -> Fuel -> Fuel
* :: Fuel -> Fuel -> Fuel
$cnegate :: Fuel -> Fuel
negate :: Fuel -> Fuel
$cabs :: Fuel -> Fuel
abs :: Fuel -> Fuel
$csignum :: Fuel -> Fuel
signum :: Fuel -> Fuel
$cfromInteger :: Integer -> Fuel
fromInteger :: Integer -> Fuel
Num)

initFuel :: Fuel
initFuel :: Fuel
initFuel = Fuel
8

-- | Check that all variables marked dirty are inhabited.
ensureInhabited ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  Fuel ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
ensureInhabited :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
ensureInhabited Fuel
fuel nc0 :: NormalizedConstraints vt v loc
nc0@NormalizedConstraints {Set v
dirtySet :: Set v
$sel:dirtySet:NormalizedConstraints :: forall vt v loc. NormalizedConstraints vt v loc -> Set v
dirtySet}
  | Fuel
fuel Fuel -> Fuel -> Bool
forall a. Eq a => a -> a -> Bool
== Fuel
0 = Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a. a -> Maybe a
Just NormalizedConstraints vt v loc
clean) -- out of fuel, assume inhabited
  | Bool
otherwise = do
      -- all dirty vars must be inhabited or this NormalizedConstraints
      -- is dropped
      let phi :: v
-> (NormalizedConstraints vt v loc
    -> MaybeT m (NormalizedConstraints vt v loc))
-> NormalizedConstraints vt v loc
-> MaybeT m (NormalizedConstraints vt v loc)
phi v
dirtyVar NormalizedConstraints vt v loc
-> MaybeT m (NormalizedConstraints vt v loc)
b NormalizedConstraints vt v loc
nc = do
            NormalizedConstraints vt v loc
nc <- m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Fuel
-> v
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> v
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
inhabited (Fuel
fuel Fuel -> Fuel -> Fuel
forall a. Num a => a -> a -> a
- Fuel
1) v
dirtyVar NormalizedConstraints vt v loc
nc)
            NormalizedConstraints vt v loc
-> MaybeT m (NormalizedConstraints vt v loc)
b NormalizedConstraints vt v loc
nc
       in MaybeT m (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT ((v
 -> (NormalizedConstraints vt v loc
     -> MaybeT m (NormalizedConstraints vt v loc))
 -> NormalizedConstraints vt v loc
 -> MaybeT m (NormalizedConstraints vt v loc))
-> (NormalizedConstraints vt v loc
    -> MaybeT m (NormalizedConstraints vt v loc))
-> Set v
-> NormalizedConstraints vt v loc
-> MaybeT m (NormalizedConstraints 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 v
-> (NormalizedConstraints vt v loc
    -> MaybeT m (NormalizedConstraints vt v loc))
-> NormalizedConstraints vt v loc
-> MaybeT m (NormalizedConstraints vt v loc)
phi NormalizedConstraints vt v loc
-> MaybeT m (NormalizedConstraints vt v loc)
forall a. a -> MaybeT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set v
dirtySet NormalizedConstraints vt v loc
clean)
  where
    clean :: NormalizedConstraints vt v loc
clean = NormalizedConstraints vt v loc
nc0 {dirtySet = mempty}

-- | Add a formula literal to our normalized constraint set. This
-- corresponds to fig 7.
addLiteral ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  Literal vt v loc ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
addLiteral :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Literal vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addLiteral Literal vt v loc
lit0 NormalizedConstraints vt v loc
nabla0 = MaybeT m (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
  NormalizedConstraints vt v loc
nc <- m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (NormalizedConstraints vt v loc))
 -> MaybeT m (NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall a b. (a -> b) -> a -> b
$ case Literal vt v loc
lit0 of
    Literal vt v loc
F -> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (NormalizedConstraints vt v loc)
forall a. Maybe a
Nothing
    Literal vt v loc
T -> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a. a -> Maybe a
Just NormalizedConstraints vt v loc
nabla0)
    PosCon v
var ConstructorReference
datacon [(v, Type vt loc)]
convars ->
      let ctx :: NormalizedConstraints vt v loc
ctx = ((v, Type vt loc)
 -> NormalizedConstraints vt v loc
 -> NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> [(v, Type vt loc)]
-> NormalizedConstraints vt v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(v
trm, Type vt loc
typ) NormalizedConstraints vt v loc
b -> v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
trm Type vt loc
typ VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id NormalizedConstraints vt v loc
b) NormalizedConstraints vt v loc
nabla0 [(v, Type vt loc)]
convars
          c :: Constraint vt v loc
c = v
-> ConstructorReference
-> [(v, Type vt loc)]
-> Constraint vt v loc
forall vt v loc.
v
-> ConstructorReference
-> [(v, Type vt loc)]
-> Constraint vt v loc
C.PosCon v
var ConstructorReference
datacon [(v, Type vt loc)]
convars
       in Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint Constraint vt v loc
c NormalizedConstraints vt v loc
ctx
    NegCon v
var ConstructorReference
datacon -> Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> ConstructorReference -> Constraint vt v loc
forall vt v loc. v -> ConstructorReference -> Constraint vt v loc
C.NegCon v
var ConstructorReference
datacon) NormalizedConstraints vt v loc
nabla0
    PosEffect v
var EffectHandler
datacon [(v, Type vt loc)]
convars ->
      let ctx :: NormalizedConstraints vt v loc
ctx = ((v, Type vt loc)
 -> NormalizedConstraints vt v loc
 -> NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
-> [(v, Type vt loc)]
-> NormalizedConstraints vt v loc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(v
trm, Type vt loc
typ) NormalizedConstraints vt v loc
b -> v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
trm Type vt loc
typ VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id NormalizedConstraints vt v loc
b) NormalizedConstraints vt v loc
nabla0 [(v, Type vt loc)]
convars
          c :: Constraint vt v loc
c = v -> EffectHandler -> [(v, Type vt loc)] -> Constraint vt v loc
forall vt v loc.
v -> EffectHandler -> [(v, Type vt loc)] -> Constraint vt v loc
C.PosEffect v
var EffectHandler
datacon [(v, Type vt loc)]
convars
       in Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint Constraint vt v loc
c NormalizedConstraints vt v loc
ctx
    NegEffect v
var EffectHandler
datacon -> Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> EffectHandler -> Constraint vt v loc
forall vt v loc. v -> EffectHandler -> Constraint vt v loc
C.NegEffect v
var EffectHandler
datacon) NormalizedConstraints vt v loc
nabla0
    PosLit v
var PmLit
lit -> Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
C.PosLit v
var PmLit
lit) NormalizedConstraints vt v loc
nabla0
    NegLit v
var PmLit
lit -> Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
C.NegLit v
var PmLit
lit) NormalizedConstraints vt v loc
nabla0
    PosListHead v
listRoot Int
n v
listElem Type vt loc
listElemType -> do
      let nabla1 :: NormalizedConstraints vt v loc
nabla1 = v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
listElem Type vt loc
listElemType VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id NormalizedConstraints vt v loc
nabla0
          c :: Constraint vt v loc
c = v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListHead v
listRoot Int
n v
listElem
      Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint Constraint vt v loc
c NormalizedConstraints vt v loc
nabla1
    PosListTail v
listRoot Int
n v
listElem Type vt loc
listElemType -> do
      let nabla1 :: NormalizedConstraints vt v loc
nabla1 = v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
listElem Type vt loc
listElemType VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id NormalizedConstraints vt v loc
nabla0
          c :: Constraint vt v loc
c = v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListTail v
listRoot Int
n v
listElem
      Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint Constraint vt v loc
c NormalizedConstraints vt v loc
nabla1
    NegListInterval v
listVar IntervalSet
iset -> Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> IntervalSet -> Constraint vt v loc
forall vt v loc. v -> IntervalSet -> Constraint vt v loc
C.NegListInterval v
listVar IntervalSet
iset) NormalizedConstraints vt v loc
nabla0
    Effectful v
var -> Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint (v -> Constraint vt v loc
forall vt v loc. v -> Constraint vt v loc
C.Effectful v
var) NormalizedConstraints vt v loc
nabla0
    Let v
var Term' vt v loc
_expr Type vt loc
typ -> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a. a -> Maybe a
Just (v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
var Type vt loc
typ VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id NormalizedConstraints vt v loc
nabla0))
  m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Fuel
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Fuel
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
ensureInhabited Fuel
initFuel NormalizedConstraints vt v loc
nc)

insertVarInfo ::
  forall vt v loc.
  (Ord v) =>
  v ->
  VarInfo vt v loc ->
  NormalizedConstraints vt v loc ->
  NormalizedConstraints vt v loc
insertVarInfo :: forall vt v loc.
Ord v =>
v
-> VarInfo vt v loc
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
insertVarInfo v
k VarInfo vt v loc
v nc :: NormalizedConstraints vt v loc
nc@NormalizedConstraints {UFMap v (VarInfo vt v loc)
constraintMap :: UFMap v (VarInfo vt v loc)
$sel:constraintMap:NormalizedConstraints :: forall vt v loc.
NormalizedConstraints vt v loc -> UFMap v (VarInfo vt v loc)
constraintMap} =
  NormalizedConstraints vt v loc
nc {constraintMap = UFMap.insert k v constraintMap}

-- | Add a constraint to our normalized constraint set. This
-- corresponds to fig 7.
addConstraint ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  Constraint vt v loc ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
addConstraint :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint Constraint vt v loc
con0 NormalizedConstraints vt v loc
nc = do
  PrettyPrintEnv
ppe <- m PrettyPrintEnv
forall vt v loc (m :: * -> *). Pmc vt v loc m => m PrettyPrintEnv
getPrettyPrintEnv
  PrettyPrintEnv
-> Maybe (NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
debugConstraint PrettyPrintEnv
ppe (Maybe (NormalizedConstraints vt v loc)
 -> Maybe (NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Constraint vt v loc
con0 of
    C.PosLit v
var PmLit
pmlit ->
      let updateLiteral :: Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
updateLiteral Maybe a
pos Set a
neg a
lit
            | Just a
lit1 <- Maybe a
pos,
              a
lit1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
lit =
                -- we already have this positive constraint
                (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), ConstraintUpdate (Maybe a, Set a)
forall a. ConstraintUpdate a
Ignore)
            | a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
lit Set a
neg = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate (Maybe a, Set a)
forall a. ConstraintUpdate a
Ignore)
            | Bool
otherwise = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Maybe a, Set a) -> ConstraintUpdate (Maybe a, Set a)
forall a. a -> ConstraintUpdate a
Update (a -> Maybe a
forall a. a -> Maybe a
Just a
lit, Set a
neg))
       in v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a
    -> Set a
    -> a
    -> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a
    -> Set a
    -> a
    -> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyLiteralC v
var PmLit
pmlit Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
forall a.
Ord a =>
Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
forall {a} {m :: * -> *} {vt} {v} {loc}.
(Monad m, Ord a) =>
Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
updateLiteral NormalizedConstraints vt v loc
nc
    C.NegLit v
var PmLit
pmlit ->
      let updateLiteral :: Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
updateLiteral Maybe a
pos Set a
neg a
lit
            -- the constraint contradicts positive info
            | Just a
lit1 <- Maybe a
pos, a
lit1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
lit = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate (Maybe a, Set a)
forall a. ConstraintUpdate a
Ignore)
            -- we already have this negative constraint
            | a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
lit Set a
neg = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), ConstraintUpdate (Maybe a, Set a)
forall a. ConstraintUpdate a
Ignore)
            | Bool
otherwise = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Maybe a, Set a) -> ConstraintUpdate (Maybe a, Set a)
forall a. a -> ConstraintUpdate a
Update (Maybe a
pos, a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
lit Set a
neg))
       in v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a
    -> Set a
    -> a
    -> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a
    -> Set a
    -> a
    -> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyLiteralC v
var PmLit
pmlit Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
forall a.
Ord a =>
Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
forall {a} {m :: * -> *} {vt} {v} {loc}.
(Ord a, Monad m) =>
Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
updateLiteral NormalizedConstraints vt v loc
nc
    C.NegListInterval v
var IntervalSet
negMatchInterval ->
      let updateList :: Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
updateList Type vt loc
_typ Seq v
pCons Seq v
pSnoc IntervalSet
posMatchInterval
            -- No lengths are accepted
            | IntervalSet -> Bool
IntervalSet.null IntervalSet
newMatchInterval = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. ConstraintUpdate a
Ignore)
            -- This length constraint forces equating some cons and snoc matches
            | let unconflictedLen :: Int
unconflictedLen = Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
pCons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
pSnoc,
              Just Int
maxLen <- IntervalSet -> Maybe Int
IntervalSet.lookupMax IntervalSet
newMatchInterval,
              Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
unconflictedLen =
                let varsToEquate :: Int
varsToEquate = Int
unconflictedLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
maxLen
                    (Seq v
newPSnoc, [(v, v)]
vars) =
                      let (Seq v
_as, Seq v
bs) = Int -> Seq v -> (Seq v, Seq v)
forall a. Int -> Seq a -> (Seq a, Seq a)
Seq.splitAt (Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
pCons Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
varsToEquate) Seq v
pCons
                          (Seq v
cs, Seq v
ds) = Int -> Seq v -> (Seq v, Seq v)
forall a. Int -> Seq a -> (Seq a, Seq a)
Seq.splitAt (Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
pSnoc Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
varsToEquate) Seq v
pSnoc
                       in (Seq v
cs, [v] -> [v] -> [(v, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Seq v -> [v]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
bs) (Seq v -> [v]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
ds))
                 in ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v, v)]
vars, (Seq v, Seq v, IntervalSet)
-> ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. a -> ConstraintUpdate a
Update (Seq v
pCons, Seq v
newPSnoc, IntervalSet
newMatchInterval))
            | Bool
otherwise =
                (v -> Seq v -> IntervalSet -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v -> Seq v -> IntervalSet -> C vt v loc m ()
populateCons v
var Seq v
pCons IntervalSet
newMatchInterval, (Seq v, Seq v, IntervalSet)
-> ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. a -> ConstraintUpdate a
Update (Seq v
pCons, Seq v
pSnoc, IntervalSet
newMatchInterval))
            where
              newMatchInterval :: IntervalSet
newMatchInterval = IntervalSet -> IntervalSet -> IntervalSet
IntervalSet.difference IntervalSet
posMatchInterval IntervalSet
negMatchInterval
       in v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyListC v
var Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
updateList NormalizedConstraints vt v loc
nc
    C.PosListHead v
r Int
n v
e ->
      let updateList :: Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
updateList Type vt loc
_elmType Seq v
posCons Seq v
posSnocs IntervalSet
iset
            -- there is an existing positive constraint on this element
            | Just v
existingElemVar <- Int -> Seq v -> Maybe v
forall a. Int -> Seq a -> Maybe a
Seq.lookup Int
n Seq v
posCons = ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v
e, v
existingElemVar)], ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. ConstraintUpdate a
Ignore)
            -- a list of this length is proscribed
            | let minPatLen :: Int
minPatLen = Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posCons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
              Just Int
maxLen <- IntervalSet -> Maybe Int
IntervalSet.lookupMax IntervalSet
iset,
              Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minPatLen =
                (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. ConstraintUpdate a
Ignore)
            -- the length constraint forces us to equate some cons and snoc patterns
            | let unconflictedLen :: Int
unconflictedLen = Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posCons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posSnocs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
              Just Int
maxLen <- IntervalSet -> Maybe Int
IntervalSet.lookupMax IntervalSet
iset,
              Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
unconflictedLen =
                let posCons' :: Seq v
posCons' = Seq v
posCons Seq v -> v -> Seq v
forall a. Seq a -> a -> Seq a
Seq.|> v
e
                    e' :: v
e' = Seq v -> Int -> v
forall a. Seq a -> Int -> a
Seq.index Seq v
posSnocs (Int
maxLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posCons')
                 in ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v
e, v
e')], (Seq v, Seq v, IntervalSet)
-> ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. a -> ConstraintUpdate a
Update (Seq v
posCons', Seq v
posSnocs, IntervalSet
iset))
            | Bool
otherwise =
                let posCons' :: Seq v
posCons' = Seq v
posCons Seq v -> v -> Seq v
forall a. Seq a -> a -> Seq a
Seq.|> v
e
                    iset' :: IntervalSet
iset' = (Int, Int) -> IntervalSet -> IntervalSet
IntervalSet.delete (Int
0, Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posCons' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) IntervalSet
iset
                 in (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Seq v, Seq v, IntervalSet)
-> ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. a -> ConstraintUpdate a
Update (Seq v
posCons', Seq v
posSnocs, IntervalSet
iset'))
       in v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyListC v
r Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
updateList NormalizedConstraints vt v loc
nc
    C.PosListTail v
r Int
n v
e ->
      let updateList :: Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
updateList Type vt loc
_elmType Seq v
posCons Seq v
posSnoc IntervalSet
iset
            -- there is an existing positive constraint on this element
            | Just v
existingElemVar <- Int -> Seq v -> Maybe v
forall a. Int -> Seq a -> Maybe a
Seq.lookup Int
n Seq v
posSnoc = ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v
e, v
existingElemVar)], ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. ConstraintUpdate a
Ignore)
            -- a list of this length is proscribed
            | let minPatLen :: Int
minPatLen = Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posSnoc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
              Just Int
maxLen <- IntervalSet -> Maybe Int
IntervalSet.lookupMax IntervalSet
iset,
              Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minPatLen =
                (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. ConstraintUpdate a
Ignore)
            -- the length constraint forces us to equate some cons and snoc patterns
            | let unconflictedLen :: Int
unconflictedLen = Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posCons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posSnoc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
              Just Int
maxLen <- IntervalSet -> Maybe Int
IntervalSet.lookupMax IntervalSet
iset,
              Int
maxLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
unconflictedLen =
                let posSnoc' :: Seq v
posSnoc' = Seq v
posSnoc Seq v -> v -> Seq v
forall a. Seq a -> a -> Seq a
Seq.|> v
e
                    e' :: v
e' = Seq v -> Int -> v
forall a. Seq a -> Int -> a
Seq.index Seq v
posCons (Int
maxLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posSnoc')
                 in ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v
e, v
e')], (Seq v, Seq v, IntervalSet)
-> ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. a -> ConstraintUpdate a
Update (Seq v
posCons, Seq v
posSnoc', IntervalSet
iset))
            | Bool
otherwise =
                let posSnoc' :: Seq v
posSnoc' = Seq v
posSnoc Seq v -> v -> Seq v
forall a. Seq a -> a -> Seq a
Seq.|> v
e
                    iset' :: IntervalSet
iset' = (Int, Int) -> IntervalSet -> IntervalSet
IntervalSet.delete (Int
0, Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
posSnoc' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) IntervalSet
iset
                 in (v -> Seq v -> IntervalSet -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v -> Seq v -> IntervalSet -> C vt v loc m ()
populateCons v
r Seq v
posCons IntervalSet
iset', (Seq v, Seq v, IntervalSet)
-> ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall a. a -> ConstraintUpdate a
Update (Seq v
posCons, Seq v
posSnoc', IntervalSet
iset'))
       in v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyListC v
r Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
updateList NormalizedConstraints vt v loc
nc
    C.PosCon v
var ConstructorReference
datacon [(v, Type vt loc)]
convars ->
      let updateConstructor :: Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
updateConstructor Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg
            | Just (ConstructorReference
datacon1, [(v, Type vt loc)]
convars1) <- Maybe (ConstructorReference, [(v, Type vt loc)])
pos = case ConstructorReference
datacon ConstructorReference -> ConstructorReference -> Bool
forall a. Eq a => a -> a -> Bool
== ConstructorReference
datacon1 of
                Bool
True -> do
                  -- we already have an assertion, so equate convars
                  let varsToEquate :: [(v, v)]
varsToEquate = ((v, Type vt loc) -> (v, Type vt loc) -> (v, v))
-> [(v, Type vt loc)] -> [(v, Type vt loc)] -> [(v, v)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(v
y, Type vt loc
_) (v
z, Type vt loc
_) -> (v
y, v
z)) [(v, Type vt loc)]
convars [(v, Type vt loc)]
convars1
                  ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v, v)]
varsToEquate, ConstraintUpdate
  (Maybe (ConstructorReference, [(v, Type vt loc)]),
   Set ConstructorReference)
forall a. ConstraintUpdate a
Ignore)
                Bool
False -> (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate
  (Maybe (ConstructorReference, [(v, Type vt loc)]),
   Set ConstructorReference)
forall a. ConstraintUpdate a
Ignore)
            -- contradicts negative info
            | Bool
True <- ConstructorReference -> Set ConstructorReference -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ConstructorReference
datacon Set ConstructorReference
neg = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate
  (Maybe (ConstructorReference, [(v, Type vt loc)]),
   Set ConstructorReference)
forall a. ConstraintUpdate a
Ignore)
            | Bool
otherwise =
                -- no conflicting info, add constraint
                (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Maybe (ConstructorReference, [(v, Type vt loc)]),
 Set ConstructorReference)
-> ConstraintUpdate
     (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference)
forall a. a -> ConstraintUpdate a
Update ((ConstructorReference, [(v, Type vt loc)])
-> Maybe (ConstructorReference, [(v, Type vt loc)])
forall a. a -> Maybe a
Just (ConstructorReference
datacon, [(v, Type vt loc)]
convars), Set ConstructorReference
neg))
       in v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (ConstructorReference, [(v, Type vt loc)]),
           Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (ConstructorReference, [(v, Type vt loc)]),
           Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyConstructorC v
var Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
updateConstructor NormalizedConstraints vt v loc
nc
    C.NegCon v
var ConstructorReference
datacon ->
      let updateConstructor :: Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
updateConstructor Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg
            -- contradicts positive info
            | Just (ConstructorReference
datacon1, [(v, Type vt loc)]
_) <- Maybe (ConstructorReference, [(v, Type vt loc)])
pos, ConstructorReference
datacon1 ConstructorReference -> ConstructorReference -> Bool
forall a. Eq a => a -> a -> Bool
== ConstructorReference
datacon = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate
  (Maybe (ConstructorReference, [(v, Type vt loc)]),
   Set ConstructorReference)
forall a. ConstraintUpdate a
Ignore)
            -- we already have this negative constraint
            | ConstructorReference -> Set ConstructorReference -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ConstructorReference
datacon Set ConstructorReference
neg = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), ConstraintUpdate
  (Maybe (ConstructorReference, [(v, Type vt loc)]),
   Set ConstructorReference)
forall a. ConstraintUpdate a
Ignore)
            | Bool
otherwise = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Maybe (ConstructorReference, [(v, Type vt loc)]),
 Set ConstructorReference)
-> ConstraintUpdate
     (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference)
forall a. a -> ConstraintUpdate a
Update (Maybe (ConstructorReference, [(v, Type vt loc)])
pos, ConstructorReference
-> Set ConstructorReference -> Set ConstructorReference
forall a. Ord a => a -> Set a -> Set a
Set.insert ConstructorReference
datacon Set ConstructorReference
neg))
       in v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (ConstructorReference, [(v, Type vt loc)]),
           Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (ConstructorReference, [(v, Type vt loc)]),
           Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyConstructorC v
var Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
updateConstructor NormalizedConstraints vt v loc
nc
    C.PosEffect v
var EffectHandler
datacon [(v, Type vt loc)]
convars ->
      let updateConstructor :: Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
updateConstructor Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg
            | Just (EffectHandler
datacon1, [(v, Type vt loc)]
convars1) <- Maybe (EffectHandler, [(v, Type vt loc)])
pos = case EffectHandler
datacon EffectHandler -> EffectHandler -> Bool
forall a. Eq a => a -> a -> Bool
== EffectHandler
datacon1 of
                Bool
True -> do
                  -- we already have an assertion, so equate convars
                  let varsToEquate :: [(v, v)]
varsToEquate = ((v, Type vt loc) -> (v, Type vt loc) -> (v, v))
-> [(v, Type vt loc)] -> [(v, Type vt loc)] -> [(v, v)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(v
y, Type vt loc
_) (v
z, Type vt loc
_) -> (v
y, v
z)) [(v, Type vt loc)]
convars [(v, Type vt loc)]
convars1
                  ([(v, v)] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v, v)]
varsToEquate, ConstraintUpdate
  (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. ConstraintUpdate a
Ignore)
                Bool
False -> (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate
  (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. ConstraintUpdate a
Ignore)
            -- contradicts negative info
            | Bool
True <- EffectHandler -> Set EffectHandler -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EffectHandler
datacon Set EffectHandler
neg = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate
  (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. ConstraintUpdate a
Ignore)
            | Bool
otherwise =
                -- no conflicting info, add constraint
                (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
-> ConstraintUpdate
     (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. a -> ConstraintUpdate a
Update ((EffectHandler, [(v, Type vt loc)])
-> Maybe (EffectHandler, [(v, Type vt loc)])
forall a. a -> Maybe a
Just (EffectHandler
datacon, [(v, Type vt loc)]
convars), Set EffectHandler
neg))
       in v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyEffectC v
var Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
updateConstructor NormalizedConstraints vt v loc
nc
    C.NegEffect v
var EffectHandler
datacon ->
      let updateConstructor :: Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
updateConstructor Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg
            -- contradicts positive info
            | Just (EffectHandler
datacon1, [(v, Type vt loc)]
_) <- Maybe (EffectHandler, [(v, Type vt loc)])
pos, EffectHandler
datacon1 EffectHandler -> EffectHandler -> Bool
forall a. Eq a => a -> a -> Bool
== EffectHandler
datacon = (C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction, ConstraintUpdate
  (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. ConstraintUpdate a
Ignore)
            -- we already have this negative constraint
            | EffectHandler -> Set EffectHandler -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EffectHandler
datacon Set EffectHandler
neg = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), ConstraintUpdate
  (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. ConstraintUpdate a
Ignore)
            | Bool
otherwise = (() -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
-> ConstraintUpdate
     (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall a. a -> ConstraintUpdate a
Update (Maybe (EffectHandler, [(v, Type vt loc)])
pos, EffectHandler -> Set EffectHandler -> Set EffectHandler
forall a. Ord a => a -> Set a -> Set a
Set.insert EffectHandler
datacon Set EffectHandler
neg))
       in v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyEffectC v
var Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
updateConstructor NormalizedConstraints vt v loc
nc
    C.Effectful v
var ->
      case v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
var NormalizedConstraints vt v loc
nc of
        (v
var, VarInfo vt v loc
vi, NormalizedConstraints vt v loc
nc)
          | Bool
otherwise -> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (NormalizedConstraints vt v loc)
 -> m (Maybe (NormalizedConstraints vt v loc)))
-> Maybe (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a b. (a -> b) -> a -> b
$ NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a. a -> Maybe a
Just (NormalizedConstraints vt v loc
 -> Maybe (NormalizedConstraints vt v loc))
-> NormalizedConstraints vt v loc
-> Maybe (NormalizedConstraints vt v loc)
forall a b. (a -> b) -> a -> b
$ v
-> VarInfo vt v loc
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
forall vt v loc.
Ord v =>
v
-> VarInfo vt v loc
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
insertVarInfo v
var VarInfo vt v loc
vi {vi_eff = IsEffectful} NormalizedConstraints vt v loc
nc
    C.Eq v
x v
y -> v
-> v
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> v
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
union v
x v
y NormalizedConstraints vt v loc
nc
  where
    debugConstraint :: PrettyPrintEnv
-> Maybe (NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
debugConstraint PrettyPrintEnv
ppe Maybe (NormalizedConstraints vt v loc)
x =
      let debugOutput :: Pretty ColorText
debugOutput =
            Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
P.sep
              Pretty ColorText
"\n"
              [ Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
P.red Pretty ColorText
"input constraints: ") (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
nc),
                Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
P.yellow Pretty ColorText
"additional constraint: ") (PrettyPrintEnv -> Constraint vt v loc -> Pretty ColorText
forall vt v loc.
(Var vt, Var v) =>
PrettyPrintEnv -> Constraint vt v loc -> Pretty ColorText
C.prettyConstraint PrettyPrintEnv
ppe Constraint vt v loc
con0),
                Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
P.green Pretty ColorText
"resulting constraint: ") (Pretty ColorText
-> (NormalizedConstraints vt v loc -> Pretty ColorText)
-> Maybe (NormalizedConstraints vt v loc)
-> Pretty ColorText
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pretty ColorText
"contradiction" (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) Maybe (NormalizedConstraints vt v loc)
x),
                Pretty ColorText
""
              ]
       in if DebugFlag -> Bool
shouldDebug DebugFlag
PatternCoverageConstraintSolver then [Char]
-> Maybe (NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
forall a. [Char] -> a -> a
trace (Pretty ColorText -> [Char]
P.toAnsiUnbroken Pretty ColorText
debugOutput) Maybe (NormalizedConstraints vt v loc)
x else Maybe (NormalizedConstraints vt v loc)
x

-- | Like 'addConstraint', but for a list of constraints
addConstraints ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  [Constraint vt v loc] ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
addConstraints :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraints [Constraint vt v loc]
cs NormalizedConstraints vt v loc
nc0 = MaybeT m (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (NormalizedConstraints vt v loc)
 -> m (Maybe (NormalizedConstraints vt v loc)))
-> MaybeT m (NormalizedConstraints vt v loc)
-> m (Maybe (NormalizedConstraints vt v loc))
forall a b. (a -> b) -> a -> b
$ (NormalizedConstraints vt v loc
 -> Constraint vt v loc
 -> MaybeT m (NormalizedConstraints vt v loc))
-> NormalizedConstraints vt v loc
-> [Constraint vt v loc]
-> MaybeT m (NormalizedConstraints vt v loc)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\NormalizedConstraints vt v loc
b Constraint vt v loc
a -> m (Maybe (NormalizedConstraints vt v loc))
-> MaybeT m (NormalizedConstraints vt v loc)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Constraint vt v loc
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraint Constraint vt v loc
a NormalizedConstraints vt v loc
b)) NormalizedConstraints vt v loc
nc0 [Constraint vt v loc]
cs

-- | Equate two variables
union ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  v ->
  v ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
union :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> v
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
union v
v0 v
v1 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} =
  v
-> v
-> UFMap v (VarInfo vt v loc)
-> (UFMap v (VarInfo vt v loc)
    -> m (NormalizedConstraints vt v loc))
-> (v
    -> VarInfo vt v loc
    -> UFMap v (VarInfo vt v loc)
    -> m (Maybe (NormalizedConstraints vt v loc)))
-> m (Maybe (NormalizedConstraints vt v loc))
forall (m :: * -> *) k v r.
(MonadFix m, Ord k) =>
k
-> k
-> UFMap k v
-> (UFMap k v -> m r)
-> (k -> v -> UFMap k v -> m (Maybe r))
-> m (Maybe r)
UFMap.union v
v0 v
v1 UFMap v (VarInfo vt v loc)
constraintMap UFMap v (VarInfo vt v loc) -> m (NormalizedConstraints vt v loc)
noMerge \v
chosenCanon VarInfo vt v loc
nonCanonValue UFMap v (VarInfo vt v loc)
m ->
    -- In this block we want to collect the constraints from the
    -- non-canonical value and add them to the canonical value.

    -- literals are handled uniformly
    let handleLit :: forall x. (x -> PmLit) -> Maybe x -> Set x -> ([Constraint vt v loc], [Constraint vt v loc])
        handleLit :: forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit x -> PmLit
toPmLit Maybe x
pos Set x
neg =
          let posC :: [Constraint vt v loc]
posC = case Maybe x
pos of
                Maybe x
Nothing -> []
                Just x
lit -> [v -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
C.PosLit v
chosenCanon (x -> PmLit
toPmLit x
lit)]
              negC :: [Constraint vt v loc]
negC = (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 -> PmLit -> Constraint vt v loc
forall vt v loc. v -> PmLit -> Constraint vt v loc
C.NegLit v
chosenCanon (x -> PmLit
toPmLit 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
neg
           in ([Constraint vt v loc]
posC, [Constraint vt v loc]
negC)
        constraints :: [Constraint vt v loc]
constraints = [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]
effCon
        ([Constraint vt v loc]
posCon, [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
nonCanonValue of
          Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg ->
            let posC :: [Constraint vt v loc]
posC = case Maybe (ConstructorReference, [(v, Type vt loc)])
pos of
                  Maybe (ConstructorReference, [(v, Type vt loc)])
Nothing -> []
                  Just (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
C.PosCon v
chosenCanon ConstructorReference
datacon [(v, Type vt loc)]
convars]
                negC :: [Constraint vt v loc]
negC = (ConstructorReference
 -> [Constraint vt v loc] -> [Constraint vt v loc])
-> [Constraint vt v loc]
-> Set ConstructorReference
-> [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 (\ConstructorReference
a [Constraint vt v loc]
b -> v -> ConstructorReference -> Constraint vt v loc
forall vt v loc. v -> ConstructorReference -> Constraint vt v loc
C.NegCon v
chosenCanon ConstructorReference
a Constraint vt v loc
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. a -> [a] -> [a]
: [Constraint vt v loc]
b) [] Set ConstructorReference
neg
             in ([Constraint vt v loc]
posC, [Constraint vt v loc]
negC)
          Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg ->
            let posC :: [Constraint vt v loc]
posC = case Maybe (EffectHandler, [(v, Type vt loc)])
pos of
                  Maybe (EffectHandler, [(v, Type vt loc)])
Nothing -> []
                  Just (EffectHandler
datacon, [(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
C.PosEffect v
chosenCanon EffectHandler
datacon [(v, Type vt loc)]
convars]
                negC :: [Constraint vt v loc]
negC = (EffectHandler -> [Constraint vt v loc] -> [Constraint vt v loc])
-> [Constraint vt v loc]
-> Set EffectHandler
-> [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 (\EffectHandler
a [Constraint vt v loc]
b -> v -> EffectHandler -> Constraint vt v loc
forall vt v loc. v -> EffectHandler -> Constraint vt v loc
C.NegEffect v
chosenCanon EffectHandler
a Constraint vt v loc
-> [Constraint vt v loc] -> [Constraint vt v loc]
forall a. a -> [a] -> [a]
: [Constraint vt v loc]
b) [] Set EffectHandler
neg
             in ([Constraint vt v loc]
posC, [Constraint vt v loc]
negC)
          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]
map (\(Int
i, v
x) -> v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListHead v
chosenCanon 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]
map (\(Int
i, v
x) -> v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListTail v
chosenCanon 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))
                neg :: [Constraint vt v loc]
neg = [v -> IntervalSet -> Constraint vt v loc
forall vt v loc. v -> IntervalSet -> Constraint vt v loc
C.NegListInterval v
chosenCanon (IntervalSet -> IntervalSet
IntervalSet.complement IntervalSet
iset)]
             in ([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, [Constraint vt v loc]
neg)
          Vc'Boolean Maybe Bool
pos Set Bool
neg -> (Bool -> PmLit)
-> Maybe Bool
-> Set Bool
-> ([Constraint vt v loc], [Constraint vt v loc])
forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit Bool -> PmLit
PmLit.Boolean Maybe Bool
pos Set Bool
neg
          Vc'Int Maybe Int64
pos Set Int64
neg -> (Int64 -> PmLit)
-> Maybe Int64
-> Set Int64
-> ([Constraint vt v loc], [Constraint vt v loc])
forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit Int64 -> PmLit
PmLit.Int Maybe Int64
pos Set Int64
neg
          Vc'Nat Maybe Word64
pos Set Word64
neg -> (Word64 -> PmLit)
-> Maybe Word64
-> Set Word64
-> ([Constraint vt v loc], [Constraint vt v loc])
forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit Word64 -> PmLit
PmLit.Nat Maybe Word64
pos Set Word64
neg
          Vc'Float Maybe Double
pos Set Double
neg -> (Double -> PmLit)
-> Maybe Double
-> Set Double
-> ([Constraint vt v loc], [Constraint vt v loc])
forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit Double -> PmLit
PmLit.Float Maybe Double
pos Set Double
neg
          Vc'Text Maybe Text
pos Set Text
neg -> (Text -> PmLit)
-> Maybe Text
-> Set Text
-> ([Constraint vt v loc], [Constraint vt v loc])
forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit Text -> PmLit
PmLit.Text Maybe Text
pos Set Text
neg
          Vc'Char Maybe Char
pos Set Char
neg -> (Char -> PmLit)
-> Maybe Char
-> Set Char
-> ([Constraint vt v loc], [Constraint vt v loc])
forall x.
(x -> PmLit)
-> Maybe x
-> Set x
-> ([Constraint vt v loc], [Constraint vt v loc])
handleLit Char -> PmLit
PmLit.Char Maybe Char
pos Set Char
neg
        effCon :: [Constraint vt v loc]
effCon = case VarInfo vt v loc -> EffectInfo
forall vt v loc. VarInfo vt v loc -> EffectInfo
vi_eff VarInfo vt v loc
nonCanonValue of
          EffectInfo
IsNotEffectful -> []
          EffectInfo
IsEffectful -> [v -> Constraint vt v loc
forall vt v loc. v -> Constraint vt v loc
C.Effectful v
chosenCanon]
     in [Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraints [Constraint vt v loc]
constraints NormalizedConstraints vt v loc
nc {constraintMap = m}
  where
    noMerge :: UFMap v (VarInfo vt v loc) -> m (NormalizedConstraints vt v loc)
noMerge UFMap v (VarInfo vt v loc)
m = NormalizedConstraints vt v loc
-> m (NormalizedConstraints vt v loc)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NormalizedConstraints vt v loc
nc {constraintMap = m}

modifyListC ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  v ->
  ( Type vt loc ->
    Seq v ->
    Seq v ->
    IntervalSet ->
    (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
  ) ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
modifyListC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyListC v
v Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
f NormalizedConstraints vt v loc
nc0 =
  let (C vt v loc m ()
ccomp, NormalizedConstraints vt v loc
nc1) = v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> (C vt v loc m (), NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> f (ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyListF v
v Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet))
f NormalizedConstraints vt v loc
nc0
   in (((), NormalizedConstraints vt v loc)
 -> NormalizedConstraints vt v loc)
-> Maybe ((), NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
forall a b. (a, b) -> b
snd (Maybe ((), NormalizedConstraints vt v loc)
 -> Maybe (NormalizedConstraints vt v loc))
-> m (Maybe ((), NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NormalizedConstraints vt v loc
-> C vt v loc m ()
-> m (Maybe ((), NormalizedConstraints vt v loc))
forall (m :: * -> *) vt v loc a.
Applicative m =>
NormalizedConstraints vt v loc
-> C vt v loc m a -> m (Maybe (a, NormalizedConstraints vt v loc))
runC NormalizedConstraints vt v loc
nc1 C vt v loc m ()
ccomp

modifyListF ::
  forall vt v loc f.
  (Var v, Functor f) =>
  v ->
  ( Type vt loc ->
    Seq v ->
    Seq v ->
    IntervalSet ->
    f (ConstraintUpdate (Seq v, Seq v, IntervalSet))
  ) ->
  NormalizedConstraints vt v loc ->
  f (NormalizedConstraints vt v loc)
modifyListF :: forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (Type vt loc
    -> Seq v
    -> Seq v
    -> IntervalSet
    -> f (ConstraintUpdate (Seq v, Seq v, IntervalSet)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyListF v
v Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> f (ConstraintUpdate (Seq v, Seq v, IntervalSet))
f NormalizedConstraints vt v loc
nc =
  let g :: VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g VarConstraints vt v loc
vc = Compose f ConstraintUpdate (VarConstraints vt v loc)
-> f (ConstraintUpdate (VarConstraints vt v loc))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose ((Type vt loc
 -> Seq v
 -> Seq v
 -> IntervalSet
 -> Compose f ConstraintUpdate (Seq v, Seq v, IntervalSet))
-> VarConstraints vt v loc
-> Compose f ConstraintUpdate (VarConstraints vt v loc)
forall (f :: * -> *) vt v loc.
Functor f =>
(Type vt loc
 -> Seq v -> Seq v -> IntervalSet -> f (Seq v, Seq v, IntervalSet))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegList (\Type vt loc
typ Seq v
pcons Seq v
psnoc IntervalSet
iset -> f (ConstraintUpdate (Seq v, Seq v, IntervalSet))
-> Compose f ConstraintUpdate (Seq v, Seq v, IntervalSet)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Type vt loc
-> Seq v
-> Seq v
-> IntervalSet
-> f (ConstraintUpdate (Seq v, Seq v, IntervalSet))
f Type vt loc
typ Seq v
pcons Seq v
psnoc IntervalSet
iset)) VarConstraints vt v loc
vc)
   in v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyVarConstraints v
v VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g NormalizedConstraints vt v loc
nc

modifyConstructorC ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  v ->
  ( (Maybe (ConstructorReference, [(v, Type vt loc)])) ->
    Set ConstructorReference ->
    (C vt v loc m (), ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference))
  ) ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
modifyConstructorC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (ConstructorReference, [(v, Type vt loc)]),
           Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyConstructorC v
v Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
f NormalizedConstraints vt v loc
nc0 =
  let (C vt v loc m ()
ccomp, NormalizedConstraints vt v loc
nc1) = v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (ConstructorReference, [(v, Type vt loc)]),
           Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> (C vt v loc m (), NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> f (ConstraintUpdate
            (Maybe (ConstructorReference, [(v, Type vt loc)]),
             Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyConstructorF v
v Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
f NormalizedConstraints vt v loc
nc0
   in (((), NormalizedConstraints vt v loc)
 -> NormalizedConstraints vt v loc)
-> Maybe ((), NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
forall a b. (a, b) -> b
snd (Maybe ((), NormalizedConstraints vt v loc)
 -> Maybe (NormalizedConstraints vt v loc))
-> m (Maybe ((), NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NormalizedConstraints vt v loc
-> C vt v loc m ()
-> m (Maybe ((), NormalizedConstraints vt v loc))
forall (m :: * -> *) vt v loc a.
Applicative m =>
NormalizedConstraints vt v loc
-> C vt v loc m a -> m (Maybe (a, NormalizedConstraints vt v loc))
runC NormalizedConstraints vt v loc
nc1 C vt v loc m ()
ccomp

modifyConstructorF ::
  forall vt v loc f.
  (Var v, Functor f) =>
  v ->
  ( (Maybe (ConstructorReference, [(v, Type vt loc)])) ->
    Set ConstructorReference ->
    f (ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference))
  ) ->
  NormalizedConstraints vt v loc ->
  f (NormalizedConstraints vt v loc)
modifyConstructorF :: forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (Maybe (ConstructorReference, [(v, Type vt loc)])
    -> Set ConstructorReference
    -> f (ConstraintUpdate
            (Maybe (ConstructorReference, [(v, Type vt loc)]),
             Set ConstructorReference)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyConstructorF v
v Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> f (ConstraintUpdate
        (Maybe (ConstructorReference, [(v, Type vt loc)]),
         Set ConstructorReference))
f NormalizedConstraints vt v loc
nc =
  let g :: VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g VarConstraints vt v loc
vc = Compose f ConstraintUpdate (VarConstraints vt v loc)
-> f (ConstraintUpdate (VarConstraints vt v loc))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose ((Maybe (ConstructorReference, [(v, Type vt loc)])
 -> Set ConstructorReference
 -> Compose
      f
      ConstraintUpdate
      (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
-> VarConstraints vt v loc
-> Compose f ConstraintUpdate (VarConstraints vt v loc)
forall (f :: * -> *) vt v loc.
Functor f =>
(Maybe (ConstructorReference, [(v, Type vt loc)])
 -> Set ConstructorReference
 -> f (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegConstructor (\Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg -> f (ConstraintUpdate
     (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference))
-> Compose
     f
     ConstraintUpdate
     (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> f (ConstraintUpdate
        (Maybe (ConstructorReference, [(v, Type vt loc)]),
         Set ConstructorReference))
f Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg)) VarConstraints vt v loc
vc)
   in v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyVarConstraints v
v VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g NormalizedConstraints vt v loc
nc

modifyEffectC ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  v ->
  ( (Maybe (EffectHandler, [(v, Type vt loc)])) ->
    Set EffectHandler ->
    (C vt v loc m (), ConstraintUpdate (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
  ) ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
modifyEffectC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyEffectC v
v Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
f NormalizedConstraints vt v loc
nc0 =
  let (C vt v loc m ()
ccomp, NormalizedConstraints vt v loc
nc1) = v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> (C vt v loc m (),
        ConstraintUpdate
          (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> (C vt v loc m (), NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> f (ConstraintUpdate
            (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyEffectF v
v Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> (C vt v loc m (),
    ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
f NormalizedConstraints vt v loc
nc0
   in (((), NormalizedConstraints vt v loc)
 -> NormalizedConstraints vt v loc)
-> Maybe ((), NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
forall a b. (a, b) -> b
snd (Maybe ((), NormalizedConstraints vt v loc)
 -> Maybe (NormalizedConstraints vt v loc))
-> m (Maybe ((), NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NormalizedConstraints vt v loc
-> C vt v loc m ()
-> m (Maybe ((), NormalizedConstraints vt v loc))
forall (m :: * -> *) vt v loc a.
Applicative m =>
NormalizedConstraints vt v loc
-> C vt v loc m a -> m (Maybe (a, NormalizedConstraints vt v loc))
runC NormalizedConstraints vt v loc
nc1 C vt v loc m ()
ccomp

modifyEffectF ::
  forall vt v loc f.
  (Var v, Functor f) =>
  v ->
  ( (Maybe (EffectHandler, [(v, Type vt loc)])) ->
    Set EffectHandler ->
    f (ConstraintUpdate (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
  ) ->
  NormalizedConstraints vt v loc ->
  f (NormalizedConstraints vt v loc)
modifyEffectF :: forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (Maybe (EffectHandler, [(v, Type vt loc)])
    -> Set EffectHandler
    -> f (ConstraintUpdate
            (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyEffectF v
v Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> f (ConstraintUpdate
        (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
f NormalizedConstraints vt v loc
nc =
  let g :: VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g VarConstraints vt v loc
vc = Compose f ConstraintUpdate (VarConstraints vt v loc)
-> f (ConstraintUpdate (VarConstraints vt v loc))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose ((Maybe (EffectHandler, [(v, Type vt loc)])
 -> Set EffectHandler
 -> Compose
      f
      ConstraintUpdate
      (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
-> VarConstraints vt v loc
-> Compose f ConstraintUpdate (VarConstraints vt v loc)
forall (f :: * -> *) vt v loc.
Functor f =>
(Maybe (EffectHandler, [(v, Type vt loc)])
 -> Set EffectHandler
 -> f (Maybe (EffectHandler, [(v, Type vt loc)]),
       Set EffectHandler))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegEffect (\Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg -> f (ConstraintUpdate
     (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
-> Compose
     f
     ConstraintUpdate
     (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> f (ConstraintUpdate
        (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler))
f Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg)) VarConstraints vt v loc
vc)
   in v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyVarConstraints v
v VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g NormalizedConstraints vt v loc
nc

modifyLiteralC ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  v ->
  PmLit ->
  ( forall a.
    (Ord a) =>
    -- positive info
    Maybe a ->
    -- negative info
    Set a ->
    -- the passed in PmLit, unpacked
    a ->
    (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
  ) ->
  NormalizedConstraints vt v loc ->
  m (Maybe (NormalizedConstraints vt v loc))
modifyLiteralC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a
    -> Set a
    -> a
    -> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
modifyLiteralC v
v PmLit
lit forall a.
Ord a =>
Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
f NormalizedConstraints vt v loc
nc0 =
  let (C vt v loc m ()
ccomp, NormalizedConstraints vt v loc
nc1) = v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a
    -> Set a
    -> a
    -> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> (C vt v loc m (), NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a -> Set a -> a -> f (ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyLiteralF v
v PmLit
lit Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
forall a.
Ord a =>
Maybe a
-> Set a
-> a
-> (C vt v loc m (), ConstraintUpdate (Maybe a, Set a))
f NormalizedConstraints vt v loc
nc0
   in (((), NormalizedConstraints vt v loc)
 -> NormalizedConstraints vt v loc)
-> Maybe ((), NormalizedConstraints vt v loc)
-> Maybe (NormalizedConstraints vt v loc)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc
forall a b. (a, b) -> b
snd (Maybe ((), NormalizedConstraints vt v loc)
 -> Maybe (NormalizedConstraints vt v loc))
-> m (Maybe ((), NormalizedConstraints vt v loc))
-> m (Maybe (NormalizedConstraints vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NormalizedConstraints vt v loc
-> C vt v loc m ()
-> m (Maybe ((), NormalizedConstraints vt v loc))
forall (m :: * -> *) vt v loc a.
Applicative m =>
NormalizedConstraints vt v loc
-> C vt v loc m a -> m (Maybe (a, NormalizedConstraints vt v loc))
runC NormalizedConstraints vt v loc
nc1 C vt v loc m ()
ccomp

-- | Update constraints on some literal by only depending on their Ord
-- instance.
modifyLiteralF ::
  forall vt v loc f.
  (Var v, Functor f) =>
  v ->
  PmLit ->
  ( forall a.
    (Ord a) =>
    -- positive info
    Maybe a ->
    -- negative info
    Set a ->
    -- the passed in PmLit, unpacked
    a ->
    f (ConstraintUpdate (Maybe a, Set a))
  ) ->
  NormalizedConstraints vt v loc ->
  f (NormalizedConstraints vt v loc)
modifyLiteralF :: forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> PmLit
-> (forall a.
    Ord a =>
    Maybe a -> Set a -> a -> f (ConstraintUpdate (Maybe a, Set a)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyLiteralF v
v PmLit
lit forall a.
Ord a =>
Maybe a -> Set a -> a -> f (ConstraintUpdate (Maybe a, Set a))
f NormalizedConstraints vt v loc
nc =
  let g :: VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g VarConstraints vt v loc
vc = Compose f ConstraintUpdate (VarConstraints vt v loc)
-> f (ConstraintUpdate (VarConstraints vt v loc))
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose ((forall a.
 Ord a =>
 Maybe a
 -> Set a -> a -> Compose f ConstraintUpdate (Maybe a, Set a))
-> PmLit
-> VarConstraints vt v loc
-> Compose f ConstraintUpdate (VarConstraints vt v loc)
forall (f :: * -> *) vt v loc.
Functor f =>
(forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a))
-> PmLit -> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegLiteral (\Maybe a
pos Set a
neg a
candidate -> f (ConstraintUpdate (Maybe a, Set a))
-> Compose f ConstraintUpdate (Maybe a, Set a)
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Maybe a -> Set a -> a -> f (ConstraintUpdate (Maybe a, Set a))
forall a.
Ord a =>
Maybe a -> Set a -> a -> f (ConstraintUpdate (Maybe a, Set a))
f Maybe a
pos Set a
neg a
candidate)) PmLit
lit VarConstraints vt v loc
vc)
   in v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyVarConstraints v
v VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
g NormalizedConstraints vt v loc
nc

modifyVarConstraints ::
  forall vt v loc f.
  (Var v, Functor f) =>
  v ->
  ( VarConstraints vt v loc ->
    f (ConstraintUpdate (VarConstraints vt v loc))
  ) ->
  NormalizedConstraints vt v loc ->
  -- | applied to 'Vc'Constructor'
  f (NormalizedConstraints vt v loc)
modifyVarConstraints :: forall vt v loc (f :: * -> *).
(Var v, Functor f) =>
v
-> (VarConstraints vt v loc
    -> f (ConstraintUpdate (VarConstraints vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
modifyVarConstraints v
v VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
updateVarConstraint NormalizedConstraints vt v loc
nc0 = do
  v
-> (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
-> (v
    -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc)))
-> NormalizedConstraints vt v loc
-> f (NormalizedConstraints vt v loc)
updateF v
v (\v
_v VarInfo vt v loc
vi -> (VarConstraints vt v loc -> VarInfo vt v loc)
-> ConstraintUpdate (VarConstraints vt v loc)
-> ConstraintUpdate (VarInfo vt v loc)
forall a b. (a -> b) -> ConstraintUpdate a -> ConstraintUpdate b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\VarConstraints vt v loc
vc -> VarInfo vt v loc
vi {vi_con = vc}) (ConstraintUpdate (VarConstraints vt v loc)
 -> ConstraintUpdate (VarInfo vt v loc))
-> f (ConstraintUpdate (VarConstraints vt v loc))
-> f (ConstraintUpdate (VarInfo vt v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarConstraints vt v loc
-> f (ConstraintUpdate (VarConstraints vt v loc))
updateVarConstraint (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)) NormalizedConstraints vt v loc
nc0
{-# INLINE modifyVarConstraints #-}

-- | Modify the positive and negative constraints of a constructor.
posAndNegConstructor ::
  forall f vt v loc.
  (Functor f) =>
  ( (Maybe (ConstructorReference, [(v, Type vt loc)])) ->
    Set ConstructorReference ->
    f (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference)
  ) ->
  VarConstraints vt v loc ->
  f (VarConstraints vt v loc)
posAndNegConstructor :: forall (f :: * -> *) vt v loc.
Functor f =>
(Maybe (ConstructorReference, [(v, Type vt loc)])
 -> Set ConstructorReference
 -> f (Maybe (ConstructorReference, [(v, Type vt loc)]),
       Set ConstructorReference))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegConstructor Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> f (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference)
f = \case
  Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg -> (Maybe (ConstructorReference, [(v, Type vt loc)])
 -> Set ConstructorReference -> VarConstraints vt v loc)
-> (Maybe (ConstructorReference, [(v, Type vt loc)]),
    Set ConstructorReference)
-> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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)]),
  Set ConstructorReference)
 -> VarConstraints vt v loc)
-> f (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference)
-> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConstructorReference, [(v, Type vt loc)])
-> Set ConstructorReference
-> f (Maybe (ConstructorReference, [(v, Type vt loc)]),
      Set ConstructorReference)
f Maybe (ConstructorReference, [(v, Type vt loc)])
pos Set ConstructorReference
neg
  VarConstraints vt v loc
_ -> [Char] -> f (VarConstraints vt v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: posAndNegConstructor called on something other than Vc'Constructor"
{-# INLINE posAndNegConstructor #-}

-- | Modify the positive and negative constraints of an effect.
posAndNegEffect ::
  forall f vt v loc.
  (Functor f) =>
  ( (Maybe (EffectHandler, [(v, Type vt loc)])) ->
    Set EffectHandler ->
    f (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
  ) ->
  VarConstraints vt v loc ->
  f (VarConstraints vt v loc)
posAndNegEffect :: forall (f :: * -> *) vt v loc.
Functor f =>
(Maybe (EffectHandler, [(v, Type vt loc)])
 -> Set EffectHandler
 -> f (Maybe (EffectHandler, [(v, Type vt loc)]),
       Set EffectHandler))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegEffect Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> f (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
f = \case
  Vc'Effect Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg -> (Maybe (EffectHandler, [(v, Type vt loc)])
 -> Set EffectHandler -> VarConstraints vt v loc)
-> (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
-> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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)]), Set EffectHandler)
 -> VarConstraints vt v loc)
-> f (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
-> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (EffectHandler, [(v, Type vt loc)])
-> Set EffectHandler
-> f (Maybe (EffectHandler, [(v, Type vt loc)]), Set EffectHandler)
f Maybe (EffectHandler, [(v, Type vt loc)])
pos Set EffectHandler
neg
  VarConstraints vt v loc
_ -> [Char] -> f (VarConstraints vt v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: posAndNegEffect called on something other than Vc'Effect"
{-# INLINE posAndNegEffect #-}

-- | Modify the positive and negative constraints in a way that
-- doesn't rely upon the particular literal type, but only on it being
-- an instance of Ord.
posAndNegLiteral ::
  forall f vt v loc.
  (Functor f) =>
  ( forall a.
    (Ord a) =>
    Maybe a ->
    Set a ->
    a ->
    f (Maybe a, Set a)
  ) ->
  PmLit ->
  VarConstraints vt v loc ->
  f (VarConstraints vt v loc)
posAndNegLiteral :: forall (f :: * -> *) vt v loc.
Functor f =>
(forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a))
-> PmLit -> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegLiteral forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f PmLit
lit = \case
  Vc'Boolean Maybe Bool
pos Set Bool
neg
    | PmLit.Boolean Bool
b <- PmLit
lit -> (Maybe Bool -> Set Bool -> VarConstraints vt v loc)
-> (Maybe Bool, Set Bool) -> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Bool -> Set Bool -> VarConstraints vt v loc
forall vt v loc. Maybe Bool -> Set Bool -> VarConstraints vt v loc
Vc'Boolean ((Maybe Bool, Set Bool) -> VarConstraints vt v loc)
-> f (Maybe Bool, Set Bool) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool -> Set Bool -> Bool -> f (Maybe Bool, Set Bool)
forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f Maybe Bool
pos Set Bool
neg Bool
b
  Vc'Int Maybe Int64
pos Set Int64
neg
    | PmLit.Int Int64
b <- PmLit
lit -> (Maybe Int64 -> Set Int64 -> VarConstraints vt v loc)
-> (Maybe Int64, Set Int64) -> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Int64 -> Set Int64 -> VarConstraints vt v loc
forall vt v loc.
Maybe Int64 -> Set Int64 -> VarConstraints vt v loc
Vc'Int ((Maybe Int64, Set Int64) -> VarConstraints vt v loc)
-> f (Maybe Int64, Set Int64) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int64 -> Set Int64 -> Int64 -> f (Maybe Int64, Set Int64)
forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f Maybe Int64
pos Set Int64
neg Int64
b
  Vc'Nat Maybe Word64
pos Set Word64
neg
    | PmLit.Nat Word64
b <- PmLit
lit -> (Maybe Word64 -> Set Word64 -> VarConstraints vt v loc)
-> (Maybe Word64, Set Word64) -> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Word64 -> Set Word64 -> VarConstraints vt v loc
forall vt v loc.
Maybe Word64 -> Set Word64 -> VarConstraints vt v loc
Vc'Nat ((Maybe Word64, Set Word64) -> VarConstraints vt v loc)
-> f (Maybe Word64, Set Word64) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Word64
-> Set Word64 -> Word64 -> f (Maybe Word64, Set Word64)
forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f Maybe Word64
pos Set Word64
neg Word64
b
  Vc'Float Maybe Double
pos Set Double
neg
    | PmLit.Float Double
b <- PmLit
lit -> (Maybe Double -> Set Double -> VarConstraints vt v loc)
-> (Maybe Double, Set Double) -> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Double -> Set Double -> VarConstraints vt v loc
forall vt v loc.
Maybe Double -> Set Double -> VarConstraints vt v loc
Vc'Float ((Maybe Double, Set Double) -> VarConstraints vt v loc)
-> f (Maybe Double, Set Double) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Double
-> Set Double -> Double -> f (Maybe Double, Set Double)
forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f Maybe Double
pos Set Double
neg Double
b
  Vc'Text Maybe Text
pos Set Text
neg
    | PmLit.Text Text
b <- PmLit
lit -> (Maybe Text -> Set Text -> VarConstraints vt v loc)
-> (Maybe Text, Set Text) -> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Text -> Set Text -> VarConstraints vt v loc
forall vt v loc. Maybe Text -> Set Text -> VarConstraints vt v loc
Vc'Text ((Maybe Text, Set Text) -> VarConstraints vt v loc)
-> f (Maybe Text, Set Text) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text -> Set Text -> Text -> f (Maybe Text, Set Text)
forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f Maybe Text
pos Set Text
neg Text
b
  Vc'Char Maybe Char
pos Set Char
neg
    | PmLit.Char Char
b <- PmLit
lit -> (Maybe Char -> Set Char -> VarConstraints vt v loc)
-> (Maybe Char, Set Char) -> VarConstraints vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe Char -> Set Char -> VarConstraints vt v loc
forall vt v loc. Maybe Char -> Set Char -> VarConstraints vt v loc
Vc'Char ((Maybe Char, Set Char) -> VarConstraints vt v loc)
-> f (Maybe Char, Set Char) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Char -> Set Char -> Char -> f (Maybe Char, Set Char)
forall a. Ord a => Maybe a -> Set a -> a -> f (Maybe a, Set a)
f Maybe Char
pos Set Char
neg Char
b
  Vc'Constructor Maybe (ConstructorReference, [(v, Type vt loc)])
_ Set ConstructorReference
_ -> [Char] -> f (VarConstraints vt v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: posAndNegLiteral called on constructor"
  VarConstraints vt v loc
_ -> [Char] -> f (VarConstraints vt v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: incompatible PmLit and VarConstraints types"
{-# INLINE posAndNegLiteral #-}

posAndNegList ::
  forall f vt v loc.
  (Functor f) =>
  ( Type vt loc ->
    Seq v ->
    Seq v ->
    IntervalSet ->
    f (Seq v, Seq v, IntervalSet)
  ) ->
  VarConstraints vt v loc ->
  f (VarConstraints vt v loc)
posAndNegList :: forall (f :: * -> *) vt v loc.
Functor f =>
(Type vt loc
 -> Seq v -> Seq v -> IntervalSet -> f (Seq v, Seq v, IntervalSet))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegList Type vt loc
-> Seq v -> Seq v -> IntervalSet -> f (Seq v, Seq v, IntervalSet)
f = \case
  Vc'ListRoot Type vt loc
typ Seq v
posCons Seq v
posSnocs IntervalSet
iset -> (\(Seq v
posCons, Seq v
posSnocs, IntervalSet
iset) -> 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
typ Seq v
posCons Seq v
posSnocs IntervalSet
iset) ((Seq v, Seq v, IntervalSet) -> VarConstraints vt v loc)
-> f (Seq v, Seq v, IntervalSet) -> f (VarConstraints vt v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type vt loc
-> Seq v -> Seq v -> IntervalSet -> f (Seq v, Seq v, IntervalSet)
f Type vt loc
typ Seq v
posCons Seq v
posSnocs IntervalSet
iset
  VarConstraints vt v loc
_ -> [Char] -> f (VarConstraints vt v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: posAndNegList called on a something that isn't a list"
{-# INLINE posAndNegList #-}

newtype C vt v loc m a = C
  { forall vt v loc (m :: * -> *) a.
C vt v loc m a
-> NormalizedConstraints vt v loc
-> m (Maybe (a, NormalizedConstraints vt v loc))
unC ::
      NormalizedConstraints vt v loc ->
      m (Maybe (a, NormalizedConstraints vt v loc))
  }
  deriving
    ((forall a b. (a -> b) -> C vt v loc m a -> C vt v loc m b)
-> (forall a b. a -> C vt v loc m b -> C vt v loc m a)
-> Functor (C vt v loc m)
forall a b. a -> C vt v loc m b -> C vt v loc m a
forall a b. (a -> b) -> C vt v loc m a -> C vt v loc m b
forall vt v loc (m :: * -> *) a b.
Functor m =>
a -> C vt v loc m b -> C vt v loc m a
forall vt v loc (m :: * -> *) a b.
Functor m =>
(a -> b) -> C vt v loc m a -> C vt v loc m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall vt v loc (m :: * -> *) a b.
Functor m =>
(a -> b) -> C vt v loc m a -> C vt v loc m b
fmap :: forall a b. (a -> b) -> C vt v loc m a -> C vt v loc m b
$c<$ :: forall vt v loc (m :: * -> *) a b.
Functor m =>
a -> C vt v loc m b -> C vt v loc m a
<$ :: forall a b. a -> C vt v loc m b -> C vt v loc m a
Functor, Functor (C vt v loc m)
Functor (C vt v loc m) =>
(forall a. a -> C vt v loc m a)
-> (forall a b.
    C vt v loc m (a -> b) -> C vt v loc m a -> C vt v loc m b)
-> (forall a b c.
    (a -> b -> c)
    -> C vt v loc m a -> C vt v loc m b -> C vt v loc m c)
-> (forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m b)
-> (forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m a)
-> Applicative (C vt v loc m)
forall a. a -> C vt v loc m a
forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m a
forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m b
forall a b.
C vt v loc m (a -> b) -> C vt v loc m a -> C vt v loc m b
forall a b c.
(a -> b -> c) -> C vt v loc m a -> C vt v loc m b -> C vt v loc m c
forall vt v loc (m :: * -> *). Monad m => Functor (C vt v loc m)
forall vt v loc (m :: * -> *) a. Monad m => a -> C vt v loc m a
forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> C vt v loc m b -> C vt v loc m a
forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> C vt v loc m b -> C vt v loc m b
forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m (a -> b) -> C vt v loc m a -> C vt v loc m b
forall vt v loc (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> C vt v loc m a -> C vt v loc m b -> C vt v loc m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall vt v loc (m :: * -> *) a. Monad m => a -> C vt v loc m a
pure :: forall a. a -> C vt v loc m a
$c<*> :: forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m (a -> b) -> C vt v loc m a -> C vt v loc m b
<*> :: forall a b.
C vt v loc m (a -> b) -> C vt v loc m a -> C vt v loc m b
$cliftA2 :: forall vt v loc (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> C vt v loc m a -> C vt v loc m b -> C vt v loc m c
liftA2 :: forall a b c.
(a -> b -> c) -> C vt v loc m a -> C vt v loc m b -> C vt v loc m c
$c*> :: forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> C vt v loc m b -> C vt v loc m b
*> :: forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m b
$c<* :: forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> C vt v loc m b -> C vt v loc m a
<* :: forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m a
Applicative, Applicative (C vt v loc m)
Applicative (C vt v loc m) =>
(forall a b.
 C vt v loc m a -> (a -> C vt v loc m b) -> C vt v loc m b)
-> (forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m b)
-> (forall a. a -> C vt v loc m a)
-> Monad (C vt v loc m)
forall a. a -> C vt v loc m a
forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m b
forall a b.
C vt v loc m a -> (a -> C vt v loc m b) -> C vt v loc m b
forall vt v loc (m :: * -> *).
Monad m =>
Applicative (C vt v loc m)
forall vt v loc (m :: * -> *) a. Monad m => a -> C vt v loc m a
forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> C vt v loc m b -> C vt v loc m b
forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> (a -> C vt v loc m b) -> C vt v loc m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> (a -> C vt v loc m b) -> C vt v loc m b
>>= :: forall a b.
C vt v loc m a -> (a -> C vt v loc m b) -> C vt v loc m b
$c>> :: forall vt v loc (m :: * -> *) a b.
Monad m =>
C vt v loc m a -> C vt v loc m b -> C vt v loc m b
>> :: forall a b. C vt v loc m a -> C vt v loc m b -> C vt v loc m b
$creturn :: forall vt v loc (m :: * -> *) a. Monad m => a -> C vt v loc m a
return :: forall a. a -> C vt v loc m a
Monad, MonadState (NormalizedConstraints vt v loc))
    via StateT (NormalizedConstraints vt v loc) (MaybeT m)
  deriving ((forall (m :: * -> *). Monad m => Monad (C vt v loc m)) =>
(forall (m :: * -> *) a. Monad m => m a -> C vt v loc m a)
-> MonadTrans (C vt v loc)
forall vt v loc (m :: * -> *). Monad m => Monad (C vt v loc m)
forall vt v loc (m :: * -> *) a. Monad m => m a -> C vt v loc m a
forall (m :: * -> *). Monad m => Monad (C vt v loc m)
forall (m :: * -> *) a. Monad m => m a -> C vt v loc m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall vt v loc (m :: * -> *) a. Monad m => m a -> C vt v loc m a
lift :: forall (m :: * -> *) a. Monad m => m a -> C vt v loc m a
MonadTrans) via ComposeT (StateT (NormalizedConstraints vt v loc)) MaybeT

contradiction :: (Applicative m) => C vt v loc m a
contradiction :: forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction = (NormalizedConstraints vt v loc
 -> m (Maybe (a, NormalizedConstraints vt v loc)))
-> C vt v loc m a
forall vt v loc (m :: * -> *) a.
(NormalizedConstraints vt v loc
 -> m (Maybe (a, NormalizedConstraints vt v loc)))
-> C vt v loc m a
C \NormalizedConstraints vt v loc
_ -> Maybe (a, NormalizedConstraints vt v loc)
-> m (Maybe (a, NormalizedConstraints vt v loc))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, NormalizedConstraints vt v loc)
forall a. Maybe a
Nothing

equate :: (Pmc vt v loc m) => [(v, v)] -> C vt v loc m ()
equate :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[(v, v)] -> C vt v loc m ()
equate [(v, v)]
vs = [Constraint vt v loc] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc] -> C vt v loc m ()
addConstraintsC (((v, v) -> Constraint vt v loc)
-> [(v, v)] -> [Constraint vt v loc]
forall a b. (a -> b) -> [a] -> [b]
map ((v -> v -> Constraint vt v loc) -> (v, v) -> Constraint vt v loc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> v -> Constraint vt v loc
forall vt v loc. v -> v -> Constraint vt v loc
C.Eq) [(v, v)]
vs)

lookupListElemTypeC :: (Pmc vt v loc m) => v -> C vt v loc m (Type vt loc)
lookupListElemTypeC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v -> C vt v loc m (Type vt loc)
lookupListElemTypeC v
listVar = do
  NormalizedConstraints vt v loc
nc0 <- C vt v loc m (NormalizedConstraints vt v loc)
forall s (m :: * -> *). MonadState s m => m s
get
  let (v
_var, VarInfo vt v loc
vi, NormalizedConstraints vt v loc
nc1) = v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
forall vt v loc.
Var v =>
v
-> NormalizedConstraints vt v loc
-> (v, VarInfo vt v loc, NormalizedConstraints vt v loc)
expectCanon v
listVar NormalizedConstraints vt v loc
nc0
  NormalizedConstraints vt v loc -> C vt v loc m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put NormalizedConstraints vt v loc
nc1
  pure $ Const (Type vt loc) (VarConstraints vt v loc) -> Type vt loc
forall {k} a (b :: k). Const a b -> a
getConst ((Type vt loc
 -> Seq v
 -> Seq v
 -> IntervalSet
 -> Const (Type vt loc) (Seq v, Seq v, IntervalSet))
-> VarConstraints vt v loc
-> Const (Type vt loc) (VarConstraints vt v loc)
forall (f :: * -> *) vt v loc.
Functor f =>
(Type vt loc
 -> Seq v -> Seq v -> IntervalSet -> f (Seq v, Seq v, IntervalSet))
-> VarConstraints vt v loc -> f (VarConstraints vt v loc)
posAndNegList (\Type vt loc
elemTyp Seq v
_ Seq v
_ IntervalSet
_ -> Type vt loc -> Const (Type vt loc) (Seq v, Seq v, IntervalSet)
forall {k} a (b :: k). a -> Const a b
Const Type vt loc
elemTyp) (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))

addConstraintsC :: (Pmc vt v loc m) => [Constraint vt v loc] -> C vt v loc m ()
addConstraintsC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc] -> C vt v loc m ()
addConstraintsC [Constraint vt v loc]
cs = do
  NormalizedConstraints vt v loc
nc <- C vt v loc m (NormalizedConstraints vt v loc)
forall s (m :: * -> *). MonadState s m => m s
get
  m (Maybe (NormalizedConstraints vt v loc))
-> C vt v loc m (Maybe (NormalizedConstraints vt v loc))
forall (m :: * -> *) a. Monad m => m a -> C vt v loc m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ([Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc]
-> NormalizedConstraints vt v loc
-> m (Maybe (NormalizedConstraints vt v loc))
addConstraints [Constraint vt v loc]
cs NormalizedConstraints vt v loc
nc) C vt v loc m (Maybe (NormalizedConstraints vt v loc))
-> (Maybe (NormalizedConstraints vt v loc) -> C vt v loc m ())
-> C vt v loc m ()
forall a b.
C vt v loc m a -> (a -> C vt v loc m b) -> C vt v loc m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (NormalizedConstraints vt v loc)
Nothing -> C vt v loc m ()
forall (m :: * -> *) vt v loc a. Applicative m => C vt v loc m a
contradiction
    Just NormalizedConstraints vt v loc
nc -> NormalizedConstraints vt v loc -> C vt v loc m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put NormalizedConstraints vt v loc
nc

declVarC ::
  (Pmc vt v loc m) =>
  v ->
  Type vt loc ->
  (VarInfo vt v loc -> VarInfo vt v loc) ->
  C vt v loc m ()
declVarC :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> C vt v loc m ()
declVarC v
v Type vt loc
vt VarInfo vt v loc -> VarInfo vt v loc
vimod = do
  NormalizedConstraints vt v loc
nc0 <- C vt v loc m (NormalizedConstraints vt v loc)
forall s (m :: * -> *). MonadState s m => m s
get
  let nc1 :: NormalizedConstraints vt v loc
nc1 = v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
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
vt VarInfo vt v loc -> VarInfo vt v loc
vimod NormalizedConstraints vt v loc
nc0
  NormalizedConstraints vt v loc -> C vt v loc m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put NormalizedConstraints vt v loc
nc1

freshC ::
  (Pmc vt v loc m) =>
  C vt v loc m v
freshC :: forall vt v loc (m :: * -> *). Pmc vt v loc m => C vt v loc m v
freshC = m v -> C vt v loc m v
forall (m :: * -> *) a. Monad m => m a -> C vt v loc m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m v
forall vt v loc (m :: * -> *). Pmc vt v loc m => m v
fresh

populateCons :: (Pmc vt v loc m) => v -> Seq v -> IntervalSet -> C vt v loc m ()
populateCons :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v -> Seq v -> IntervalSet -> C vt v loc m ()
populateCons v
listVar Seq v
pCons IntervalSet
iset = do
  case IntervalSet -> Maybe Int
IntervalSet.lookupMin IntervalSet
iset of
    Just Int
minLen
      | Int
minLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0,
        let targets :: [Int]
targets = [Seq v -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq v
pCons .. Int
minLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1],
        Bool -> Bool
not ([Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
targets) -> do
          Type vt loc
elemTyp <- v -> C vt v loc m (Type vt loc)
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v -> C vt v loc m (Type vt loc)
lookupListElemTypeC v
listVar
          [Int] -> (Int -> C vt v loc m ()) -> C vt v loc m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Int]
targets \Int
idx -> do
            v
elv <- C vt v loc m v
forall vt v loc (m :: * -> *). Pmc vt v loc m => C vt v loc m v
freshC
            v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> C vt v loc m ()
declVarC v
elv Type vt loc
elemTyp VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id
            [Constraint vt v loc] -> C vt v loc m ()
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
[Constraint vt v loc] -> C vt v loc m ()
addConstraintsC [v -> Int -> v -> Constraint vt v loc
forall vt v loc. v -> Int -> v -> Constraint vt v loc
C.PosListHead v
listVar Int
idx v
elv]
    Maybe Int
_ -> () -> C vt v loc m ()
forall a. a -> C vt v loc m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

runC ::
  (Applicative m) =>
  NormalizedConstraints vt v loc ->
  C vt v loc m a ->
  m (Maybe (a, NormalizedConstraints vt v loc))
runC :: forall (m :: * -> *) vt v loc a.
Applicative m =>
NormalizedConstraints vt v loc
-> C vt v loc m a -> m (Maybe (a, NormalizedConstraints vt v loc))
runC NormalizedConstraints vt v loc
nc0 C vt v loc m a
ca = C vt v loc m a
-> NormalizedConstraints vt v loc
-> m (Maybe (a, NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *) a.
C vt v loc m a
-> NormalizedConstraints vt v loc
-> m (Maybe (a, NormalizedConstraints vt v loc))
unC C vt v loc m a
ca NormalizedConstraints vt v loc
nc0