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

import Data.Map (Map)
import Data.Map qualified as Map
import Data.Text (Text)
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
  | PosRecordLiteral
      -- | record root
      v
      -- | a variable and type per matched field
      (Map Text (v, Type vt loc))
  | -- | 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]
  PosRecordLiteral v
root Map Text (v, Type vt loc)
fields ->
    let fieldStrs :: [Pretty ColorText]
fieldStrs = ((Text, (v, Type vt loc)) -> Pretty ColorText)
-> [(Text, (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 (\(Text
k, (v
v, Type vt loc
_t)) -> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Text -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pany Text
k, Pretty ColorText
":", v -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
prettyVar v
v]) (Map Text (v, Type vt loc) -> [(Text, (v, Type vt loc))]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map Text (v, Type vt loc)
fields)
     in Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
" " [Pretty ColorText
"{" Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
sep Pretty ColorText
", " [Pretty ColorText]
fieldStrs Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
"}", Pretty ColorText
"<-", Pretty ColorText
"record", 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