module Unison.PatternMatchCoverage.Literal
  ( Literal (..),
    prettyLiteral,
  )
where

import Unison.ConstructorReference (ConstructorReference)
import Unison.PatternMatchCoverage.EffectHandler
import Unison.PatternMatchCoverage.IntervalSet (IntervalSet)
import Unison.PatternMatchCoverage.PmLit (PmLit, prettyPmLit)
import Unison.PrettyPrintEnv qualified as PPE
import Unison.Syntax.TermPrinter qualified as TermPrinter
import Unison.Syntax.TypePrinter qualified as TypePrinter
import Unison.Term (Term')
import Unison.Type (Type)
import Unison.Typechecker.TypeVar (TypeVar, lowerTerm)
import Unison.Util.Pretty
import Unison.Var (Var)

-- | Refinement type literals (fig 3)
data Literal vt v loc
  = -- | True
    T
  | -- | False
    F
  | -- | 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
      (Type vt loc)
  | -- | 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
      (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
  | -- | Introduce a binding for a term
    Let v (Term' vt v loc) (Type vt loc)
  deriving stock (Int -> Literal vt v loc -> ShowS
[Literal vt v loc] -> ShowS
Literal vt v loc -> String
(Int -> Literal vt v loc -> ShowS)
-> (Literal vt v loc -> String)
-> ([Literal vt v loc] -> ShowS)
-> Show (Literal vt v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall vt v loc.
(Show v, Show vt) =>
Int -> Literal vt v loc -> ShowS
forall vt v loc. (Show v, Show vt) => [Literal vt v loc] -> ShowS
forall vt v loc. (Show v, Show vt) => Literal vt v loc -> String
$cshowsPrec :: forall vt v loc.
(Show v, Show vt) =>
Int -> Literal vt v loc -> ShowS
showsPrec :: Int -> Literal vt v loc -> ShowS
$cshow :: forall vt v loc. (Show v, Show vt) => Literal vt v loc -> String
show :: Literal vt v loc -> String
$cshowList :: forall vt v loc. (Show v, Show vt) => [Literal vt v loc] -> ShowS
showList :: [Literal vt v loc] -> ShowS
Show)

prettyLiteral :: (Var v) => Literal (TypeVar b v) v loc -> Pretty ColorText
prettyLiteral :: forall v b loc.
Var v =>
Literal (TypeVar b v) v loc -> Pretty ColorText
prettyLiteral = \case
  Literal (TypeVar b v) v loc
T -> Pretty ColorText
"✓"
  Literal (TypeVar b v) v loc
F -> Pretty ColorText
"⨉"
  PosCon v
var ConstructorReference
con [(v, Type (TypeVar b v) loc)]
convars ->
    let xs :: [Pretty ColorText]
xs = ConstructorReference -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pc ConstructorReference
con Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: ((v, Type (TypeVar b v) loc) -> Pretty ColorText)
-> [(v, Type (TypeVar b v) 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 (TypeVar b v) 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
" " [v -> Pretty ColorText
pv v
trm, Pretty ColorText
":", PrettyPrintEnv -> Type (TypeVar b v) loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TypePrinter.pretty PrettyPrintEnv
PPE.empty Type (TypeVar b v) loc
typ]) [(v, Type (TypeVar b v) loc)]
convars [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ [Pretty ColorText
"<-", v -> Pretty ColorText
pv 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
pv v
var, Pretty ColorText
"≠", ConstructorReference -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pc ConstructorReference
con]
  PosEffect v
var EffectHandler
con [(v, Type (TypeVar b v) loc)]
convars ->
    let xs :: [Pretty ColorText]
xs = EffectHandler -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pc EffectHandler
con Pretty ColorText -> [Pretty ColorText] -> [Pretty ColorText]
forall a. a -> [a] -> [a]
: ((v, Type (TypeVar b v) loc) -> Pretty ColorText)
-> [(v, Type (TypeVar b v) 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 (TypeVar b v) 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
" " [v -> Pretty ColorText
pv v
trm, Pretty ColorText
":", PrettyPrintEnv -> Type (TypeVar b v) loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TypePrinter.pretty PrettyPrintEnv
PPE.empty Type (TypeVar b v) loc
typ]) [(v, Type (TypeVar b v) loc)]
convars [Pretty ColorText] -> [Pretty ColorText] -> [Pretty ColorText]
forall a. [a] -> [a] -> [a]
++ [Pretty ColorText
"<-", v -> Pretty ColorText
pv 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
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
pv v
var, Pretty ColorText
"≠", EffectHandler -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pc EffectHandler
con]
  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
pv 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
pv v
var, Pretty ColorText
"≠", PmLit -> Pretty ColorText
forall s. IsString s => PmLit -> Pretty s
prettyPmLit PmLit
lit]
  PosListHead v
root Int
n v
el Type (TypeVar b v) loc
_ -> 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
pv v
el, Pretty ColorText
"<-", Pretty ColorText
"head", Int -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pc Int
n, v -> Pretty ColorText
pv v
root]
  PosListTail v
root Int
n v
el Type (TypeVar b v) loc
_ -> 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
pv v
el, Pretty ColorText
"<-", Pretty ColorText
"tail", Int -> Pretty ColorText
forall a. Show a => a -> Pretty ColorText
pc Int
n, v -> Pretty ColorText
pv 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
pv 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
pv v
var
  Let v
var Term' (TypeVar b v) v loc
expr Type (TypeVar b v) 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
"let", v -> Pretty ColorText
pv v
var, Pretty ColorText
"=", PrettyPrintEnv -> Term v loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Term v a -> Pretty ColorText
TermPrinter.pretty PrettyPrintEnv
PPE.empty (Term' (TypeVar b v) v loc -> Term v loc
forall v b a. Ord v => Term' (TypeVar b v) v a -> Term v a
lowerTerm Term' (TypeVar b v) v loc
expr), Pretty ColorText
":", PrettyPrintEnv -> Type (TypeVar b v) loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TypePrinter.pretty PrettyPrintEnv
PPE.empty Type (TypeVar b v) loc
typ]
  where
    pv :: v -> Pretty ColorText
pv = String -> Pretty ColorText
forall s. IsString s => String -> Pretty s
string (String -> Pretty ColorText)
-> (v -> String) -> v -> Pretty ColorText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> String
forall a. Show a => a -> String
show
    pc :: forall a. (Show a) => a -> Pretty ColorText
    pc :: forall a. Show a => a -> Pretty ColorText
pc = 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