-- |
-- Module      :  Disco.Exhaustiveness.TypeInfo
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Utilities for converting Disco types into 'Constructors'
-- that the exhaustiveness checker understands, and utilities
-- for working with 'TypedVar's and their names.
module Disco.Exhaustiveness.TypeInfo where

import Control.Monad (replicateM)
import Data.Function (on)
import Data.List ((\\))
import qualified Data.Map as M
import Disco.AST.Typed (ATerm)
import Disco.Effects.Fresh (Fresh, fresh)
import qualified Disco.Types as Ty
import Polysemy
import Unbound.Generics.LocallyNameless (Name, s2n)

newtype TypedVar = TypedVar (Name ATerm, Ty.Type)
  deriving (Int -> TypedVar -> ShowS
[TypedVar] -> ShowS
TypedVar -> String
(Int -> TypedVar -> ShowS)
-> (TypedVar -> String) -> ([TypedVar] -> ShowS) -> Show TypedVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypedVar -> ShowS
showsPrec :: Int -> TypedVar -> ShowS
$cshow :: TypedVar -> String
show :: TypedVar -> String
$cshowList :: [TypedVar] -> ShowS
showList :: [TypedVar] -> ShowS
Show, Eq TypedVar
Eq TypedVar =>
(TypedVar -> TypedVar -> Ordering)
-> (TypedVar -> TypedVar -> Bool)
-> (TypedVar -> TypedVar -> Bool)
-> (TypedVar -> TypedVar -> Bool)
-> (TypedVar -> TypedVar -> Bool)
-> (TypedVar -> TypedVar -> TypedVar)
-> (TypedVar -> TypedVar -> TypedVar)
-> Ord TypedVar
TypedVar -> TypedVar -> Bool
TypedVar -> TypedVar -> Ordering
TypedVar -> TypedVar -> TypedVar
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
$ccompare :: TypedVar -> TypedVar -> Ordering
compare :: TypedVar -> TypedVar -> Ordering
$c< :: TypedVar -> TypedVar -> Bool
< :: TypedVar -> TypedVar -> Bool
$c<= :: TypedVar -> TypedVar -> Bool
<= :: TypedVar -> TypedVar -> Bool
$c> :: TypedVar -> TypedVar -> Bool
> :: TypedVar -> TypedVar -> Bool
$c>= :: TypedVar -> TypedVar -> Bool
>= :: TypedVar -> TypedVar -> Bool
$cmax :: TypedVar -> TypedVar -> TypedVar
max :: TypedVar -> TypedVar -> TypedVar
$cmin :: TypedVar -> TypedVar -> TypedVar
min :: TypedVar -> TypedVar -> TypedVar
Ord)

instance Eq TypedVar where
  TypedVar (Name ATerm
n1, Type
_) == :: TypedVar -> TypedVar -> Bool
== TypedVar (Name ATerm
n2, Type
_) = Name ATerm
n1 Name ATerm -> Name ATerm -> Bool
forall a. Eq a => a -> a -> Bool
== Name ATerm
n2

getType :: TypedVar -> Ty.Type
getType :: TypedVar -> Type
getType (TypedVar (Name ATerm
_, Type
t)) = Type
t

data DataCon = DataCon
  { DataCon -> Ident
dcIdent :: Ident
  , DataCon -> [Type]
dcTypes :: [Ty.Type]
  }
  deriving (Eq DataCon
Eq DataCon =>
(DataCon -> DataCon -> Ordering)
-> (DataCon -> DataCon -> Bool)
-> (DataCon -> DataCon -> Bool)
-> (DataCon -> DataCon -> Bool)
-> (DataCon -> DataCon -> Bool)
-> (DataCon -> DataCon -> DataCon)
-> (DataCon -> DataCon -> DataCon)
-> Ord DataCon
DataCon -> DataCon -> Bool
DataCon -> DataCon -> Ordering
DataCon -> DataCon -> DataCon
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
$ccompare :: DataCon -> DataCon -> Ordering
compare :: DataCon -> DataCon -> Ordering
$c< :: DataCon -> DataCon -> Bool
< :: DataCon -> DataCon -> Bool
$c<= :: DataCon -> DataCon -> Bool
<= :: DataCon -> DataCon -> Bool
$c> :: DataCon -> DataCon -> Bool
> :: DataCon -> DataCon -> Bool
$c>= :: DataCon -> DataCon -> Bool
>= :: DataCon -> DataCon -> Bool
$cmax :: DataCon -> DataCon -> DataCon
max :: DataCon -> DataCon -> DataCon
$cmin :: DataCon -> DataCon -> DataCon
min :: DataCon -> DataCon -> DataCon
Ord, Int -> DataCon -> ShowS
[DataCon] -> ShowS
DataCon -> String
(Int -> DataCon -> ShowS)
-> (DataCon -> String) -> ([DataCon] -> ShowS) -> Show DataCon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataCon -> ShowS
showsPrec :: Int -> DataCon -> ShowS
$cshow :: DataCon -> String
show :: DataCon -> String
$cshowList :: [DataCon] -> ShowS
showList :: [DataCon] -> ShowS
Show)

-- This is very important, as we have (sometimes recursive) type aliases
-- Equality of dcTypes doesn't measure equality of dataconstructors,
-- because we could have two different aliases for the same type
-- (And we can't just resolve all aliases up front, because they can be recursive)
instance Eq DataCon where
  == :: DataCon -> DataCon -> Bool
(==) = Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Ident -> Ident -> Bool)
-> (DataCon -> Ident) -> DataCon -> DataCon -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` DataCon -> Ident
dcIdent

-- The Show instance of 'Ident' should never be used
-- for displaying results to the user.
-- Instead, convert to a proper pattern and use the
-- pretty printer, like in Exhaustiveness.hs
data Ident where
  KUnit :: Ident
  KBool :: Bool -> Ident
  KNat :: Integer -> Ident
  KInt :: Integer -> Ident
  KPair :: Ident
  KCons :: Ident
  KNil :: Ident
  KChar :: Char -> Ident
  KLeft :: Ident
  KRight :: Ident
  KUnknown :: Ident
  deriving (Int -> Ident -> ShowS
[Ident] -> ShowS
Ident -> String
(Int -> Ident -> ShowS)
-> (Ident -> String) -> ([Ident] -> ShowS) -> Show Ident
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Ident -> ShowS
showsPrec :: Int -> Ident -> ShowS
$cshow :: Ident -> String
show :: Ident -> String
$cshowList :: [Ident] -> ShowS
showList :: [Ident] -> ShowS
Show, Ident -> Ident -> Bool
(Ident -> Ident -> Bool) -> (Ident -> Ident -> Bool) -> Eq Ident
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ident -> Ident -> Bool
== :: Ident -> Ident -> Bool
$c/= :: Ident -> Ident -> Bool
/= :: Ident -> Ident -> Bool
Eq, Eq Ident
Eq Ident =>
(Ident -> Ident -> Ordering)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Ident)
-> (Ident -> Ident -> Ident)
-> Ord Ident
Ident -> Ident -> Bool
Ident -> Ident -> Ordering
Ident -> Ident -> Ident
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
$ccompare :: Ident -> Ident -> Ordering
compare :: Ident -> Ident -> Ordering
$c< :: Ident -> Ident -> Bool
< :: Ident -> Ident -> Bool
$c<= :: Ident -> Ident -> Bool
<= :: Ident -> Ident -> Bool
$c> :: Ident -> Ident -> Bool
> :: Ident -> Ident -> Bool
$c>= :: Ident -> Ident -> Bool
>= :: Ident -> Ident -> Bool
$cmax :: Ident -> Ident -> Ident
max :: Ident -> Ident -> Ident
$cmin :: Ident -> Ident -> Ident
min :: Ident -> Ident -> Ident
Ord)

-- | 'Finite' constructors are used in the LYG checker
--   'Infinite' constructors are used when reporting
--   examples of uncovered patterns, we only pick out a few of them
data Constructors where
  Finite :: [DataCon] -> Constructors
  Infinite :: [DataCon] -> Constructors

unknown :: DataCon
unknown :: DataCon
unknown = DataCon {dcIdent :: Ident
dcIdent = Ident
KUnknown, dcTypes :: [Type]
dcTypes = []}

unit :: DataCon
unit :: DataCon
unit = DataCon {dcIdent :: Ident
dcIdent = Ident
KUnit, dcTypes :: [Type]
dcTypes = []}

bool :: Bool -> DataCon
bool :: Bool -> DataCon
bool Bool
b = DataCon {dcIdent :: Ident
dcIdent = Bool -> Ident
KBool Bool
b, dcTypes :: [Type]
dcTypes = []}

natural :: Integer -> DataCon
natural :: Integer -> DataCon
natural Integer
n = DataCon {dcIdent :: Ident
dcIdent = Integer -> Ident
KNat Integer
n, dcTypes :: [Type]
dcTypes = []}

integer :: Integer -> DataCon
integer :: Integer -> DataCon
integer Integer
z = DataCon {dcIdent :: Ident
dcIdent = Integer -> Ident
KInt Integer
z, dcTypes :: [Type]
dcTypes = []}

char :: Char -> DataCon
char :: Char -> DataCon
char Char
c = DataCon {dcIdent :: Ident
dcIdent = Char -> Ident
KChar Char
c, dcTypes :: [Type]
dcTypes = []}

cons :: Ty.Type -> Ty.Type -> DataCon
cons :: Type -> Type -> DataCon
cons Type
tHead Type
tTail = DataCon {dcIdent :: Ident
dcIdent = Ident
KCons, dcTypes :: [Type]
dcTypes = [Type
tHead, Type
tTail]}

nil :: DataCon
nil :: DataCon
nil = DataCon {dcIdent :: Ident
dcIdent = Ident
KNil, dcTypes :: [Type]
dcTypes = []}

pair :: Ty.Type -> Ty.Type -> DataCon
pair :: Type -> Type -> DataCon
pair Type
a Type
b = DataCon {dcIdent :: Ident
dcIdent = Ident
KPair, dcTypes :: [Type]
dcTypes = [Type
a, Type
b]}

left :: Ty.Type -> DataCon
left :: Type -> DataCon
left Type
tl = DataCon {dcIdent :: Ident
dcIdent = Ident
KLeft, dcTypes :: [Type]
dcTypes = [Type
tl]}

right :: Ty.Type -> DataCon
right :: Type -> DataCon
right Type
tr = DataCon {dcIdent :: Ident
dcIdent = Ident
KRight, dcTypes :: [Type]
dcTypes = [Type
tr]}

tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors
tyDataCons :: Type -> TyDefCtx -> Constructors
tyDataCons Type
ty TyDefCtx
ctx = Type -> Constructors
tyDataConsHelper (Type -> Constructors) -> Type -> Constructors
forall a b. (a -> b) -> a -> b
$ Type -> TyDefCtx -> Type
resolveAlias Type
ty TyDefCtx
ctx

-- Type aliases that would cause infinite recursion here are
-- not possible to construct, so we don't have to worry about that.
-- (aka cyclic type definitions are not allowed in Disco)
resolveAlias :: Ty.Type -> Ty.TyDefCtx -> Ty.Type
resolveAlias :: Type -> TyDefCtx -> Type
resolveAlias (Ty.TyUser String
name [Type]
args) TyDefCtx
ctx = case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name TyDefCtx
ctx of
  Maybe TyDefBody
Nothing -> String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ TyDefCtx -> String
forall a. Show a => a -> String
show TyDefCtx
ctx String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nType definition not found for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
name
  Just (Ty.TyDefBody [String]
_argNames [Type] -> Type
typeCon) -> Type -> TyDefCtx -> Type
resolveAlias ([Type] -> Type
typeCon [Type]
args) TyDefCtx
ctx
resolveAlias Type
t TyDefCtx
_ = Type
t

-- | Assuming type aliases have been resolved, this
--   function converts Disco types into lists of DataCons
--   that are compatible with the LYG checker.
--
--   A list of constructors is 'Infinite' if the only way to fully
--   match against the type is with a wildcard or variable pattern.
--   Otherwise, it is 'Finite'.
--
--   The LYG checker only reads the list of constructors if
--   a type is 'Finite'. From the point of view of the checker,
--   'Infinite' is a synonym for opaque, and the constructors are discarded.
--   The dataconstructors in an `Infinite` list are only
--   used when generating the 3 positive examples of what
--   you haven't matched against.
--   This will probably need to change a bit when bringing
--   exhaustiveness checking to the new arithmetic patterns.
--
--   Notice the last case of this function, which a wildcard handling the types:
--   (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _)
--   (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _)
--
--   I believe all of these are impossible to pattern match against
--   with anything other than a wildcard (or variable pattern) in Disco, so they should always
--   be fully covered. But if they are in a pair, for example, Set(Int)*Int,
--   we still need to generate 3 examples of the pair if that Int part isn't covered.
--   So how do we fill the concrete part of Set(Int), (or a generic type "a", or a function, etc.)?
--   I'm calling that 'unknown', and printing an underscore.
--   (Also, I'm using 'Infinite' for reasons metioned above).
tyDataConsHelper :: Ty.Type -> Constructors
tyDataConsHelper :: Type -> Constructors
tyDataConsHelper (Type
a Ty.:*: Type
b) = [DataCon] -> Constructors
Finite [Type -> Type -> DataCon
pair Type
a Type
b]
tyDataConsHelper (Type
l Ty.:+: Type
r) = [DataCon] -> Constructors
Finite [Type -> DataCon
left Type
l, Type -> DataCon
right Type
r]
tyDataConsHelper t :: Type
t@(Ty.TyList Type
a) = [DataCon] -> Constructors
Finite [DataCon
nil, Type -> Type -> DataCon
cons Type
a Type
t]
tyDataConsHelper Type
Ty.TyVoid = [DataCon] -> Constructors
Finite []
tyDataConsHelper Type
Ty.TyUnit = [DataCon] -> Constructors
Finite [DataCon
unit]
tyDataConsHelper Type
Ty.TyBool = [DataCon] -> Constructors
Finite [Bool -> DataCon
bool Bool
True, Bool -> DataCon
bool Bool
False]
tyDataConsHelper Type
Ty.TyN = [DataCon] -> Constructors
Infinite ([DataCon] -> Constructors) -> [DataCon] -> Constructors
forall a b. (a -> b) -> a -> b
$ (Integer -> DataCon) -> [Integer] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> DataCon
natural [Integer
0, Integer
1 ..]
-- Many thanks to this answer and its comment for a convenient way to list the integers
-- https://stackoverflow.com/a/9749957
tyDataConsHelper Type
Ty.TyZ = [DataCon] -> Constructors
Infinite ([DataCon] -> Constructors) -> [DataCon] -> Constructors
forall a b. (a -> b) -> a -> b
$ (Integer -> DataCon) -> [Integer] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> DataCon
integer ([Integer] -> [DataCon]) -> [Integer] -> [DataCon]
forall a b. (a -> b) -> a -> b
$ Integer
0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer
y | Integer
x <- [Integer
1 ..], Integer
y <- [Integer
x, -Integer
x]]
tyDataConsHelper Type
Ty.TyF = [DataCon] -> Constructors
Infinite []
tyDataConsHelper Type
Ty.TyQ = [DataCon] -> Constructors
Infinite []
-- The Char constructors are all unicode characters, but
-- given in a very particular order that I think will
-- make the most sense for students.
-- Many thanks to Dr. Yorgey for mentioning [minBound .. maxBound] and \\
tyDataConsHelper Type
Ty.TyC =
  [DataCon] -> Constructors
Infinite ([DataCon] -> Constructors) -> [DataCon] -> Constructors
forall a b. (a -> b) -> a -> b
$
    (Char -> DataCon) -> String -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map Char -> DataCon
char (String -> [DataCon]) -> String -> [DataCon]
forall a b. (a -> b) -> a -> b
$
      String
alphanum String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String
allUnicodeNicelyOrdered String -> ShowS
forall a. Eq a => [a] -> [a] -> [a]
\\ String
alphanum)
 where
  allUnicodeNicelyOrdered :: String
allUnicodeNicelyOrdered = [(Int -> Char
forall a. Enum a => Int -> a
toEnum Int
32) .. (Int -> Char
forall a. Enum a => Int -> a
toEnum Int
126)] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Int -> Char
forall a. Enum a => Int -> a
toEnum Int
161) .. Char
forall a. Bounded a => a
maxBound] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
forall a. Bounded a => a
minBound .. (Int -> Char
forall a. Enum a => Int -> a
toEnum Int
31)] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Int -> Char
forall a. Enum a => Int -> a
toEnum Int
127) .. (Int -> Char
forall a. Enum a => Int -> a
toEnum Int
160)]
  alphanum :: String
alphanum = [Char
'a' .. Char
'z'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
'A' .. Char
'Z'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
'0' .. Char
'9']
tyDataConsHelper Type
_ = [DataCon] -> Constructors
Infinite [DataCon
unknown]

newName :: (Member Fresh r) => Sem r (Name ATerm)
newName :: forall (r :: EffectRow). Member Fresh r => Sem r (Name ATerm)
newName = Name ATerm -> Sem r (Name ATerm)
forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (Name ATerm -> Sem r (Name ATerm))
-> Name ATerm -> Sem r (Name ATerm)
forall a b. (a -> b) -> a -> b
$ String -> Name ATerm
forall a. String -> Name a
s2n String
""

newVar :: (Member Fresh r) => Ty.Type -> Sem r TypedVar
newVar :: forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
newVar Type
types = do
  Name ATerm
names <- Sem r (Name ATerm)
forall (r :: EffectRow). Member Fresh r => Sem r (Name ATerm)
newName
  TypedVar -> Sem r TypedVar
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypedVar -> Sem r TypedVar) -> TypedVar -> Sem r TypedVar
forall a b. (a -> b) -> a -> b
$ (Name ATerm, Type) -> TypedVar
TypedVar (Name ATerm
names, Type
types)

newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm]
newNames :: forall (r :: EffectRow).
Member Fresh r =>
Int -> Sem r [Name ATerm]
newNames Int
i = Int -> Sem r (Name ATerm) -> Sem r [Name ATerm]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
i Sem r (Name ATerm)
forall (r :: EffectRow). Member Fresh r => Sem r (Name ATerm)
newName

newVars :: (Member Fresh r) => [Ty.Type] -> Sem r [TypedVar]
newVars :: forall (r :: EffectRow).
Member Fresh r =>
[Type] -> Sem r [TypedVar]
newVars [Type]
types = do
  [Name ATerm]
names <- Int -> Sem r [Name ATerm]
forall (r :: EffectRow).
Member Fresh r =>
Int -> Sem r [Name ATerm]
newNames ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
types)
  [TypedVar] -> Sem r [TypedVar]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypedVar] -> Sem r [TypedVar]) -> [TypedVar] -> Sem r [TypedVar]
forall a b. (a -> b) -> a -> b
$ (Name ATerm -> Type -> TypedVar)
-> [Name ATerm] -> [Type] -> [TypedVar]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Name ATerm, Type) -> TypedVar) -> Name ATerm -> Type -> TypedVar
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Name ATerm, Type) -> TypedVar
TypedVar) [Name ATerm]
names [Type]
types