module Unison.KindInference.Constraint.Solved
  ( Constraint (..),
    prov,
    loc,
  )
where

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

-- | Solved constraints
--
-- These constraints are associated with unification variables during
-- kind inference.
data Constraint uv v loc
  = IsType (TypeProvenance v loc)
  | IsAbility (Provenance v loc)
  | IsArr (Provenance v loc) uv uv
  deriving stock (Int -> Constraint uv v loc -> ShowS
[Constraint uv v loc] -> ShowS
Constraint uv v loc -> String
(Int -> Constraint uv v loc -> ShowS)
-> (Constraint uv v loc -> String)
-> ([Constraint uv v loc] -> ShowS)
-> Show (Constraint uv v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall uv v loc.
(Show v, Show loc, Show uv) =>
Int -> Constraint uv v loc -> ShowS
forall uv v loc.
(Show v, Show loc, Show uv) =>
[Constraint uv v loc] -> ShowS
forall uv v loc.
(Show v, Show loc, Show uv) =>
Constraint uv v loc -> String
$cshowsPrec :: forall uv v loc.
(Show v, Show loc, Show uv) =>
Int -> Constraint uv v loc -> ShowS
showsPrec :: Int -> Constraint uv v loc -> ShowS
$cshow :: forall uv v loc.
(Show v, Show loc, Show uv) =>
Constraint uv v loc -> String
show :: Constraint uv v loc -> String
$cshowList :: forall uv v loc.
(Show v, Show loc, Show uv) =>
[Constraint uv v loc] -> ShowS
showList :: [Constraint uv v loc] -> ShowS
Show, Constraint uv v loc -> Constraint uv v loc -> Bool
(Constraint uv v loc -> Constraint uv v loc -> Bool)
-> (Constraint uv v loc -> Constraint uv v loc -> Bool)
-> Eq (Constraint uv v loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall uv v loc.
(Var v, Eq loc, Eq uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
$c== :: forall uv v loc.
(Var v, Eq loc, Eq uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
== :: Constraint uv v loc -> Constraint uv v loc -> Bool
$c/= :: forall uv v loc.
(Var v, Eq loc, Eq uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
/= :: Constraint uv v loc -> Constraint uv v loc -> Bool
Eq, Eq (Constraint uv v loc)
Eq (Constraint uv v loc) =>
(Constraint uv v loc -> Constraint uv v loc -> Ordering)
-> (Constraint uv v loc -> Constraint uv v loc -> Bool)
-> (Constraint uv v loc -> Constraint uv v loc -> Bool)
-> (Constraint uv v loc -> Constraint uv v loc -> Bool)
-> (Constraint uv v loc -> Constraint uv v loc -> Bool)
-> (Constraint uv v loc
    -> Constraint uv v loc -> Constraint uv v loc)
-> (Constraint uv v loc
    -> Constraint uv v loc -> Constraint uv v loc)
-> Ord (Constraint uv v loc)
Constraint uv v loc -> Constraint uv v loc -> Bool
Constraint uv v loc -> Constraint uv v loc -> Ordering
Constraint uv v loc -> Constraint uv v loc -> Constraint uv v loc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Eq (Constraint uv v loc)
forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Ordering
forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Constraint uv v loc
$ccompare :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Ordering
compare :: Constraint uv v loc -> Constraint uv v loc -> Ordering
$c< :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
< :: Constraint uv v loc -> Constraint uv v loc -> Bool
$c<= :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
<= :: Constraint uv v loc -> Constraint uv v loc -> Bool
$c> :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
> :: Constraint uv v loc -> Constraint uv v loc -> Bool
$c>= :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Bool
>= :: Constraint uv v loc -> Constraint uv v loc -> Bool
$cmax :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Constraint uv v loc
max :: Constraint uv v loc -> Constraint uv v loc -> Constraint uv v loc
$cmin :: forall uv v loc.
(Var v, Ord loc, Ord uv) =>
Constraint uv v loc -> Constraint uv v loc -> Constraint uv v loc
min :: Constraint uv v loc -> Constraint uv v loc -> Constraint uv v loc
Ord)

prov ::
  Traversal
    (Constraint uv v loc)
    (Constraint uv v loc')
    (Provenance v loc)
    (Provenance v loc')
prov :: forall uv v loc loc' (f :: * -> *).
Applicative f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc -> f (Constraint uv v loc')
prov Provenance v loc -> f (Provenance v loc')
f = \case
  IsType TypeProvenance v loc
x -> TypeProvenance v loc' -> Constraint uv v loc'
forall uv v loc. TypeProvenance v loc -> Constraint uv v loc
IsType (TypeProvenance v loc' -> Constraint uv v loc')
-> f (TypeProvenance v loc') -> f (Constraint uv v loc')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Provenance v loc -> f (Provenance v loc'))
-> TypeProvenance v loc -> f (TypeProvenance v loc')
forall v loc loc' (f :: * -> *).
Applicative f =>
(Provenance v loc -> f (Provenance v loc'))
-> TypeProvenance v loc -> f (TypeProvenance v loc')
TP.prov Provenance v loc -> f (Provenance v loc')
f TypeProvenance v loc
x
  IsAbility Provenance v loc
x -> Provenance v loc' -> Constraint uv v loc'
forall uv v loc. Provenance v loc -> Constraint uv v loc
IsAbility (Provenance v loc' -> Constraint uv v loc')
-> f (Provenance v loc') -> f (Constraint uv v loc')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
x
  IsArr Provenance v loc
l uv
a uv
b -> (\Provenance v loc'
x -> Provenance v loc' -> uv -> uv -> Constraint uv v loc'
forall uv v loc.
Provenance v loc -> uv -> uv -> Constraint uv v loc
IsArr Provenance v loc'
x uv
a uv
b) (Provenance v loc' -> Constraint uv v loc')
-> f (Provenance v loc') -> f (Constraint uv v loc')
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 :: Traversal' (Constraint uv v loc) loc
loc :: forall uv v loc (f :: * -> *).
Applicative f =>
(loc -> f loc) -> Constraint uv v loc -> f (Constraint uv v loc)
loc = (Provenance v loc -> f (Provenance v loc))
-> Constraint uv v loc -> f (Constraint uv v loc)
forall uv v loc loc' (f :: * -> *).
Applicative f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc -> f (Constraint uv v loc')
prov ((Provenance v loc -> f (Provenance v loc))
 -> Constraint uv v loc -> f (Constraint uv v loc))
-> ((loc -> f loc) -> Provenance v loc -> f (Provenance v loc))
-> (loc -> f loc)
-> Constraint uv v loc
-> f (Constraint uv v loc)
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 #-}