module Unison.PatternMatchCoverage.Constraint
  ( Constraint (..),
    prettyConstraint,
  )
where

import Unison.ConstructorReference (ConstructorReference)
import Unison.PatternMatchCoverage.EffectHandler
import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
import Unison.PatternMatchCoverage.PmLit
import Unison.PatternMatchCoverage.Pretty
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import Unison.Syntax.TypePrinter qualified as TypePrinter
import Unison.Type (Type)
import Unison.Util.Pretty
import Unison.Var (Var)

-- | A constraint to add to a [normalized constraint
-- set]("Unison.PatternMatchCoverage.NormalizedConstraints") (fig 6)
-- See 'Unison.PatternMatchCoverage.Solve.addConstraint'
data Constraint vt v loc
  = -- | Positive constraint regarding data type. States that the
    -- given variable must be the given constructor, and it also binds
    -- variables corresponding to constructor arguments.
    PosCon v ConstructorReference [(v, Type vt loc)]
  | -- | Negative constraint concerning data type. States that the
    -- given variable must not be the given constructor.
    NegCon v ConstructorReference
  | -- | Positive constraint regarding data type. States that the
    -- given variable must be the given constructor, and it also binds
    -- variables corresponding to constructor arguments.
    PosEffect v EffectHandler [(v, Type vt loc)]
  | -- | Negative constraint concerning data type. States that the
    -- given variable must not be the given constructor.
    NegEffect v EffectHandler
  | -- | Positive constraint regarding literal
    PosLit v PmLit
  | -- | Negative constraint regarding literal
    NegLit v PmLit
  | -- | Positive constraint on list element with position relative to head of list
    PosListHead
      -- | list root
      v
      -- | cons position (0 is head)
      Int
      -- | element variable
      v
  | -- | Positive constraint on list element with position relative to end of list
    PosListTail
      -- | list root
      v
      -- | snoc position (0 is last)
      Int
      -- | element variable
      v
  | -- | Negative constraint on length of the list (/i.e./ the list
    -- may not be an element of the interval set)
    NegListInterval v IntervalSet
  | -- | An effect is performed
    Effectful v
  | -- | Equality constraint
    Eq v v
  deriving stock (Constraint vt v loc -> Constraint vt v loc -> Bool
(Constraint vt v loc -> Constraint vt v loc -> Bool)
-> (Constraint vt v loc -> Constraint vt v loc -> Bool)
-> Eq (Constraint vt v loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall vt v loc.
(Var vt, Eq v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
$c== :: forall vt v loc.
(Var vt, Eq v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
== :: Constraint vt v loc -> Constraint vt v loc -> Bool
$c/= :: forall vt v loc.
(Var vt, Eq v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
/= :: Constraint vt v loc -> Constraint vt v loc -> Bool
Eq, Eq (Constraint vt v loc)
Eq (Constraint vt v loc) =>
(Constraint vt v loc -> Constraint vt v loc -> Ordering)
-> (Constraint vt v loc -> Constraint vt v loc -> Bool)
-> (Constraint vt v loc -> Constraint vt v loc -> Bool)
-> (Constraint vt v loc -> Constraint vt v loc -> Bool)
-> (Constraint vt v loc -> Constraint vt v loc -> Bool)
-> (Constraint vt v loc
    -> Constraint vt v loc -> Constraint vt v loc)
-> (Constraint vt v loc
    -> Constraint vt v loc -> Constraint vt v loc)
-> Ord (Constraint vt v loc)
Constraint vt v loc -> Constraint vt v loc -> Bool
Constraint vt v loc -> Constraint vt v loc -> Ordering
Constraint vt v loc -> Constraint vt v loc -> Constraint vt v loc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall vt v loc. (Var vt, Ord v) => Eq (Constraint vt v loc)
forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Ordering
forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Constraint vt v loc
$ccompare :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Ordering
compare :: Constraint vt v loc -> Constraint vt v loc -> Ordering
$c< :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
< :: Constraint vt v loc -> Constraint vt v loc -> Bool
$c<= :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
<= :: Constraint vt v loc -> Constraint vt v loc -> Bool
$c> :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
> :: Constraint vt v loc -> Constraint vt v loc -> Bool
$c>= :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Bool
>= :: Constraint vt v loc -> Constraint vt v loc -> Bool
$cmax :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Constraint vt v loc
max :: Constraint vt v loc -> Constraint vt v loc -> Constraint vt v loc
$cmin :: forall vt v loc.
(Var vt, Ord v) =>
Constraint vt v loc -> Constraint vt v loc -> Constraint vt v loc
min :: Constraint vt v loc -> Constraint vt v loc -> Constraint vt v loc
Ord)

prettyConstraint :: forall vt v loc. (Var vt, Var v) => PrettyPrintEnv -> Constraint vt v loc -> Pretty ColorText
prettyConstraint :: forall vt v loc.
(Var vt, Var v) =>
PrettyPrintEnv -> Constraint vt v loc -> Pretty ColorText
prettyConstraint PrettyPrintEnv
ppe = \case
  PosCon v
var ConstructorReference
con [(v, Type vt loc)]
convars ->
    let xs :: [Pretty ColorText]
xs = ConstructorReference -> Pretty ColorText
pc ConstructorReference
con Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: ((v, Type vt loc) -> Pretty ColorText)
-> [(v, Type vt loc)] -> [Pretty ColorText]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(v
trm, Type vt loc
typ) -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Pretty ColorText
"(" Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
trm, Pretty ColorText
":", PrettyPrintEnv -> Type vt loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TypePrinter.pretty PrettyPrintEnv
ppe Type vt loc
typ Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
")"]) [(v, Type vt loc)]
convars [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ [Pretty ColorText
"<-", v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var]
     in Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Pretty ColorText]
xs
  NegCon v
var ConstructorReference
con -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var, Pretty ColorText
"≠", ConstructorReference -> Pretty ColorText
pc ConstructorReference
con]
  PosEffect v
var EffectHandler
eff [(v, Type vt loc)]
effvars ->
    let xs :: [Pretty ColorText]
xs = EffectHandler -> Pretty ColorText
pe EffectHandler
eff Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: ((v, Type vt loc) -> Pretty ColorText)
-> [(v, Type vt loc)] -> [Pretty ColorText]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(v
trm, Type vt loc
typ) -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Pretty ColorText
"(" Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
trm, Pretty ColorText
":", PrettyPrintEnv -> Type vt loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TypePrinter.pretty PrettyPrintEnv
ppe Type vt loc
typ Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
")"]) [(v, Type vt loc)]
effvars [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ [Pretty ColorText
"<-", v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var]
     in Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Pretty ColorText]
xs
  NegEffect v
var EffectHandler
eff -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var, Pretty ColorText
"≠", EffectHandler -> Pretty ColorText
pe EffectHandler
eff]
  PosLit v
var PmLit
lit -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [PmLit -> Pretty ColorText
forall s. IsString s => PmLit -> Pretty s
prettyPmLit PmLit
lit, Pretty ColorText
"<-", v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var]
  NegLit v
var PmLit
lit -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var, Pretty ColorText
"≠", PmLit -> Pretty ColorText
forall s. IsString s => PmLit -> Pretty s
prettyPmLit PmLit
lit]
  PosListHead v
root Int
n v
el -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
el, Pretty ColorText
"<-", Pretty ColorText
"head", Int -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pany Int
n, v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
root]
  PosListTail v
root Int
n v
el -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
el, Pretty ColorText
"<-", Pretty ColorText
"tail", Int -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pany Int
n, v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
root]
  NegListInterval v
var IntervalSet
x -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var, Pretty ColorText
"≠", String -> Pretty ColorText
forall s. IsString s => String -> Pretty s
string (IntervalSet -> String
forall a. Show a => a -> String
show IntervalSet
x)]
  Effectful v
var -> Pretty ColorText
"!" Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
var
  Eq v
v0 v
v1 -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
v0, Pretty ColorText
"=", v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
v1]
  where
    pany :: (Show a) => a -> Pretty ColorText
    pany :: forall a. Show a => a -> Pretty ColorText
pany = String -> Pretty ColorText
forall s. IsString s => String -> Pretty s
string (String -> Pretty ColorText)
-> (a -> String) -> a -> Pretty ColorText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show

    pc :: ConstructorReference -> Pretty ColorText
pc = PrettyPrintEnv -> ConstructorReference -> Pretty ColorText
prettyConstructorReference PrettyPrintEnv
ppe
    pe :: EffectHandler -> Pretty ColorText
pe = PrettyPrintEnv -> EffectHandler -> Pretty ColorText
prettyEffectHandler PrettyPrintEnv
ppe