module Unison.KindInference.Constraint.Unsolved
  ( Constraint (..),
    typeProv,
    prov,
    loc,
  )
where

import Control.Lens (Lens, Lens', Traversal)
import Unison.KindInference.Constraint.Provenance (Provenance)
import Unison.KindInference.Constraint.Provenance qualified as Provenance

-- | Unsolved constraints
--
-- These are produced during constraint generation and given as input
-- to the constraint solver.
data Constraint uv v loc typeProv
  = -- | An IsType constraint may arise from generation or from the
    -- solver. During generation the provenance is always a real
    -- source code location, but the solver defaults unconstrained
    -- kind vars to Star.
    IsType uv (typeProv v loc)
  | IsArr uv (Provenance v loc) uv uv
  | IsAbility uv (Provenance v loc)
  | Unify (Provenance v loc) uv uv
  deriving stock (Int -> Constraint uv v loc typeProv -> ShowS
[Constraint uv v loc typeProv] -> ShowS
Constraint uv v loc typeProv -> String
(Int -> Constraint uv v loc typeProv -> ShowS)
-> (Constraint uv v loc typeProv -> String)
-> ([Constraint uv v loc typeProv] -> ShowS)
-> Show (Constraint uv v loc typeProv)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Int -> Constraint uv v loc typeProv -> ShowS
forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
[Constraint uv v loc typeProv] -> ShowS
forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Constraint uv v loc typeProv -> String
$cshowsPrec :: forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Int -> Constraint uv v loc typeProv -> ShowS
showsPrec :: Int -> Constraint uv v loc typeProv -> ShowS
$cshow :: forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Constraint uv v loc typeProv -> String
show :: Constraint uv v loc typeProv -> String
$cshowList :: forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
[Constraint uv v loc typeProv] -> ShowS
showList :: [Constraint uv v loc typeProv] -> ShowS
Show, Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
(Constraint uv v loc typeProv
 -> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Bool)
-> Eq (Constraint uv v loc typeProv)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Eq loc, Eq uv, Eq (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c== :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Eq loc, Eq uv, Eq (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
== :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c/= :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Eq loc, Eq uv, Eq (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
/= :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
Eq, Eq (Constraint uv v loc typeProv)
Eq (Constraint uv v loc typeProv) =>
(Constraint uv v loc typeProv
 -> Constraint uv v loc typeProv -> Ordering)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Constraint uv v loc typeProv)
-> (Constraint uv v loc typeProv
    -> Constraint uv v loc typeProv -> Constraint uv v loc typeProv)
-> Ord (Constraint uv v loc typeProv)
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Eq (Constraint uv v loc typeProv)
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
$ccompare :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
compare :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
$c< :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
< :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c<= :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
<= :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c> :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
> :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c>= :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
>= :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$cmax :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
max :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
$cmin :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
min :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
Ord)

typeProv ::
  Traversal
    (Constraint uv v loc prov)
    (Constraint uv v loc prov')
    (prov v loc)
    (prov' v loc)
typeProv :: forall uv v loc (prov :: * -> * -> *) (prov' :: * -> * -> *)
       (f :: * -> *).
Applicative f =>
(prov v loc -> f (prov' v loc))
-> Constraint uv v loc prov -> f (Constraint uv v loc prov')
typeProv prov v loc -> f (prov' v loc)
f = \case
  IsType uv
x prov v loc
l -> uv -> prov' v loc -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType uv
x (prov' v loc -> Constraint uv v loc prov')
-> f (prov' v loc) -> f (Constraint uv v loc prov')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> prov v loc -> f (prov' v loc)
f prov v loc
l
  IsAbility uv
x Provenance v loc
l -> Constraint uv v loc prov' -> f (Constraint uv v loc prov')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (uv -> Provenance v loc -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility uv
x Provenance v loc
l)
  IsArr uv
s Provenance v loc
l uv
a uv
b -> Constraint uv v loc prov' -> f (Constraint uv v loc prov')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr uv
s Provenance v loc
l uv
a uv
b)
  Unify Provenance v loc
l uv
a uv
b -> Constraint uv v loc prov' -> f (Constraint uv v loc prov')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Provenance v loc -> uv -> uv -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify Provenance v loc
l uv
a uv
b)
{-# INLINE typeProv #-}

prov ::
  Lens
    (Constraint uv v loc Provenance)
    (Constraint uv v loc' Provenance)
    (Provenance v loc)
    (Provenance v loc')
prov :: forall uv v loc loc' (f :: * -> *).
Functor f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc' Provenance)
prov Provenance v loc -> f (Provenance v loc')
f = \case
  IsType uv
x Provenance v loc
l -> uv -> Provenance v loc' -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType uv
x (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
  IsAbility uv
x Provenance v loc
l -> uv -> Provenance v loc' -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility uv
x (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
  IsArr uv
s Provenance v loc
l uv
a uv
b -> (\Provenance v loc'
x -> uv
-> Provenance v loc' -> uv -> uv -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr uv
s Provenance v loc'
x uv
a uv
b) (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
  Unify Provenance v loc
l uv
a uv
b -> (\Provenance v loc'
x -> Provenance v loc' -> uv -> uv -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify Provenance v loc'
x uv
a uv
b) (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
{-# INLINE prov #-}

loc :: Lens' (Constraint uv v loc Provenance) loc
loc :: forall uv v loc (f :: * -> *).
Functor f =>
(loc -> f loc)
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
loc = (Provenance v loc -> f (Provenance v loc))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
forall uv v loc loc' (f :: * -> *).
Functor f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc' Provenance)
prov ((Provenance v loc -> f (Provenance v loc))
 -> Constraint uv v loc Provenance
 -> f (Constraint uv v loc Provenance))
-> ((loc -> f loc) -> Provenance v loc -> f (Provenance v loc))
-> (loc -> f loc)
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (loc -> f loc) -> Provenance v loc -> f (Provenance v loc)
forall v loc (f :: * -> *).
Functor f =>
(loc -> f loc) -> Provenance v loc -> f (Provenance v loc)
Provenance.loc
{-# INLINE loc #-}