TypeInfo.hs

-- |
-- 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 (Show, Ord)

instance Eq TypedVar where
  TypedVar (n1, _) == TypedVar (n2, _) = n1 == n2

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

data DataCon = DataCon
  { dcIdent :: Ident
  , dcTypes :: [Ty.Type]
  }
  deriving (Ord, 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
  (==) = (==) `on` 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 (Show, Eq, 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 {dcIdent = KUnknown, dcTypes = []}

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

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

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

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

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

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

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

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

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

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

tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors
tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty 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 (Ty.TyUser name args) ctx = case M.lookup name ctx of
  Nothing -> error $ show ctx ++ "\nType definition not found for: " ++ show name
  Just (Ty.TyDefBody _argNames typeCon) -> resolveAlias (typeCon args) ctx
resolveAlias t _ = 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 (a Ty.:*: b) = Finite [pair a b]
tyDataConsHelper (l Ty.:+: r) = Finite [left l, right r]
tyDataConsHelper t@(Ty.TyList a) = Finite [nil, cons a t]
tyDataConsHelper Ty.TyVoid = Finite []
tyDataConsHelper Ty.TyUnit = Finite [unit]
tyDataConsHelper Ty.TyBool = Finite [bool True, bool False]
tyDataConsHelper Ty.TyN = Infinite $ map natural [0, 1 ..]
-- Many thanks to this answer and its comment for a convenient way to list the integers
-- https://stackoverflow.com/a/9749957
tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x, -x]]
tyDataConsHelper Ty.TyF = Infinite []
tyDataConsHelper Ty.TyQ = 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 Ty.TyC =
  Infinite $
    map char $
      alphanum ++ (allUnicodeNicelyOrdered \\ alphanum)
 where
  allUnicodeNicelyOrdered = [(toEnum 32) .. (toEnum 126)] ++ [(toEnum 161) .. maxBound] ++ [minBound .. (toEnum 31)] ++ [(toEnum 127) .. (toEnum 160)]
  alphanum = ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9']
tyDataConsHelper _ = Infinite [unknown]

newName :: (Member Fresh r) => Sem r (Name ATerm)
newName = fresh $ s2n ""

newVar :: (Member Fresh r) => Ty.Type -> Sem r TypedVar
newVar types = do
  names <- newName
  return $ TypedVar (names, types)

newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm]
newNames i = replicateM i newName

newVars :: (Member Fresh r) => [Ty.Type] -> Sem r [TypedVar]
newVars types = do
  names <- newNames (length types)
  return $ zipWith (curry TypedVar) names types