{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

-- |
-- Module      :  Disco.Types.Qualifiers
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- Type qualifiers and sorts.
module Disco.Types.Qualifiers where

import GHC.Generics
import Unbound.Generics.LocallyNameless

import Data.Set (Set)
import qualified Data.Set as S

import Disco.Pretty
import Disco.Syntax.Operators

------------------------------------------------------------
-- Qualifiers
------------------------------------------------------------

-- | A "qualifier" is kind of like a type class in Haskell; but unlike
--   Haskell, disco users cannot define their own.  Rather, there is a
--   finite fixed list of qualifiers supported by disco.  For example,
--   @QSub@ denotes types which support a subtraction operation.  Each
--   qualifier corresponds to a set of types which satisfy it (see
--   'hasQual' and 'qualRules').
--
--   These qualifiers generally arise from uses of various operations.
--   For example, the expression @\\x y. x - y@ would be inferred to
--   have a type @a -> a -> a [subtractive a]@, that is, a function of
--   type @a -> a -> a@ where @a@ is any type that supports
--   subtraction.
--
--   These qualifiers can appear in a 'CQual' constraint; see
--   "Disco.Typecheck.Constraint".
data Qualifier
  = -- | Numeric, i.e. a semiring supporting + and *
    QNum
  | -- | Subtractive, i.e. supports -
    QSub
  | -- | Divisive, i.e. supports /
    QDiv
  | -- | Comparable, i.e. supports decidable ordering/comparison (see Note [QCmp])
    QCmp
  | -- | Enumerable, i.e. supports ellipsis notation [x .. y]
    QEnum
  | -- | Boolean, i.e. supports and, or, not (Bool or Prop)
    QBool
  | -- | Things that do not involve Prop.
    QBasic
  | -- | Things for which we can derive a *Haskell* Ord instance
    QSimple
  deriving (Int -> Qualifier -> ShowS
[Qualifier] -> ShowS
Qualifier -> String
(Int -> Qualifier -> ShowS)
-> (Qualifier -> String)
-> ([Qualifier] -> ShowS)
-> Show Qualifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Qualifier -> ShowS
showsPrec :: Int -> Qualifier -> ShowS
$cshow :: Qualifier -> String
show :: Qualifier -> String
$cshowList :: [Qualifier] -> ShowS
showList :: [Qualifier] -> ShowS
Show, Qualifier -> Qualifier -> Bool
(Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool) -> Eq Qualifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Qualifier -> Qualifier -> Bool
== :: Qualifier -> Qualifier -> Bool
$c/= :: Qualifier -> Qualifier -> Bool
/= :: Qualifier -> Qualifier -> Bool
Eq, Eq Qualifier
Eq Qualifier =>
(Qualifier -> Qualifier -> Ordering)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Bool)
-> (Qualifier -> Qualifier -> Qualifier)
-> (Qualifier -> Qualifier -> Qualifier)
-> Ord Qualifier
Qualifier -> Qualifier -> Bool
Qualifier -> Qualifier -> Ordering
Qualifier -> Qualifier -> Qualifier
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 :: Qualifier -> Qualifier -> Ordering
compare :: Qualifier -> Qualifier -> Ordering
$c< :: Qualifier -> Qualifier -> Bool
< :: Qualifier -> Qualifier -> Bool
$c<= :: Qualifier -> Qualifier -> Bool
<= :: Qualifier -> Qualifier -> Bool
$c> :: Qualifier -> Qualifier -> Bool
> :: Qualifier -> Qualifier -> Bool
$c>= :: Qualifier -> Qualifier -> Bool
>= :: Qualifier -> Qualifier -> Bool
$cmax :: Qualifier -> Qualifier -> Qualifier
max :: Qualifier -> Qualifier -> Qualifier
$cmin :: Qualifier -> Qualifier -> Qualifier
min :: Qualifier -> Qualifier -> Qualifier
Ord, (forall x. Qualifier -> Rep Qualifier x)
-> (forall x. Rep Qualifier x -> Qualifier) -> Generic Qualifier
forall x. Rep Qualifier x -> Qualifier
forall x. Qualifier -> Rep Qualifier x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Qualifier -> Rep Qualifier x
from :: forall x. Qualifier -> Rep Qualifier x
$cto :: forall x. Rep Qualifier x -> Qualifier
to :: forall x. Rep Qualifier x -> Qualifier
Generic, Show Qualifier
Show Qualifier =>
(AlphaCtx -> Qualifier -> Qualifier -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Qualifier -> f Qualifier)
-> (AlphaCtx -> NamePatFind -> Qualifier -> Qualifier)
-> (AlphaCtx -> NthPatFind -> Qualifier -> Qualifier)
-> (Qualifier -> DisjointSet AnyName)
-> (Qualifier -> All)
-> (Qualifier -> Bool)
-> (Qualifier -> NthPatFind)
-> (Qualifier -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Qualifier -> Qualifier)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Qualifier -> (Qualifier -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Qualifier -> m (Qualifier, Perm AnyName))
-> (AlphaCtx -> Qualifier -> Qualifier -> Ordering)
-> Alpha Qualifier
AlphaCtx -> Perm AnyName -> Qualifier -> Qualifier
AlphaCtx -> NamePatFind -> Qualifier -> Qualifier
AlphaCtx -> NthPatFind -> Qualifier -> Qualifier
AlphaCtx -> Qualifier -> Qualifier -> Bool
AlphaCtx -> Qualifier -> Qualifier -> Ordering
Qualifier -> Bool
Qualifier -> All
Qualifier -> NamePatFind
Qualifier -> NthPatFind
Qualifier -> DisjointSet AnyName
forall a.
Show a =>
(AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Qualifier -> f Qualifier
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Qualifier -> m (Qualifier, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Qualifier -> (Qualifier -> Perm AnyName -> m b) -> m b
$caeq' :: AlphaCtx -> Qualifier -> Qualifier -> Bool
aeq' :: AlphaCtx -> Qualifier -> Qualifier -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Qualifier -> f Qualifier
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Qualifier -> f Qualifier
$cclose :: AlphaCtx -> NamePatFind -> Qualifier -> Qualifier
close :: AlphaCtx -> NamePatFind -> Qualifier -> Qualifier
$copen :: AlphaCtx -> NthPatFind -> Qualifier -> Qualifier
open :: AlphaCtx -> NthPatFind -> Qualifier -> Qualifier
$cisPat :: Qualifier -> DisjointSet AnyName
isPat :: Qualifier -> DisjointSet AnyName
$cisTerm :: Qualifier -> All
isTerm :: Qualifier -> All
$cisEmbed :: Qualifier -> Bool
isEmbed :: Qualifier -> Bool
$cnthPatFind :: Qualifier -> NthPatFind
nthPatFind :: Qualifier -> NthPatFind
$cnamePatFind :: Qualifier -> NamePatFind
namePatFind :: Qualifier -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Qualifier -> Qualifier
swaps' :: AlphaCtx -> Perm AnyName -> Qualifier -> Qualifier
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Qualifier -> (Qualifier -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Qualifier -> (Qualifier -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Qualifier -> m (Qualifier, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Qualifier -> m (Qualifier, Perm AnyName)
$cacompare' :: AlphaCtx -> Qualifier -> Qualifier -> Ordering
acompare' :: AlphaCtx -> Qualifier -> Qualifier -> Ordering
Alpha)

instance Pretty Qualifier where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Qualifier -> Sem r (Doc ann)
pretty = \case
    Qualifier
QNum -> Sem r (Doc ann)
"num"
    Qualifier
QSub -> Sem r (Doc ann)
"sub"
    Qualifier
QDiv -> Sem r (Doc ann)
"div"
    Qualifier
QCmp -> Sem r (Doc ann)
"cmp"
    Qualifier
QEnum -> Sem r (Doc ann)
"enum"
    Qualifier
QBool -> Sem r (Doc ann)
"bool"
    Qualifier
QBasic -> Sem r (Doc ann)
"basic"
    Qualifier
QSimple -> Sem r (Doc ann)
"simple"

-- ~~~~ Note [QCmp]
--
-- XXX edit this!  I don't think we actually need type info for
-- comparisons at runtime any more, if we disallow functions from
-- being QCmp.  With the switch to eager semantics + disallowing
-- function comparison, it's now the case that QCmp should mean

-- * decidable* (terminating) comparison.

--
-- It used to be the case that every type in disco supported
-- (semi-decidable) linear ordering, so in one sense the QCmp
-- constraint was unnecessary.  However, in order to do a comparison we
-- need to know the type at runtime.  Currently, we use QCmp to track
-- which types have comparisons done on them, and reject any type
-- variables with a QCmp constraint (just as we reject any other type
-- variables with remaining constraints).  Every type with comparisons
-- done on it must be statically known at compile time.
--
-- However, there's now another reason: the Prop type does not support
-- comparisons at all.
--
-- Eventually, one could imagine compiling to something like System F
-- with explicit type lambdas and applications; then the QCmp
-- constraints would tell us which type applications need to be kept
-- and which can be erased.

-- | A helper function that returns the appropriate qualifier for a
--   binary arithmetic operation.
bopQual :: BOp -> Qualifier
bopQual :: BOp -> Qualifier
bopQual BOp
Add = Qualifier
QNum
bopQual BOp
Mul = Qualifier
QNum
bopQual BOp
Div = Qualifier
QDiv
bopQual BOp
Sub = Qualifier
QSub
bopQual BOp
SSub = Qualifier
QNum
bopQual BOp
And = Qualifier
QBool
bopQual BOp
Or = Qualifier
QBool
bopQual BOp
Impl = Qualifier
QBool
bopQual BOp
Iff = Qualifier
QBool
bopQual BOp
_ = String -> Qualifier
forall a. HasCallStack => String -> a
error String
"No qualifier for binary operation"

------------------------------------------------------------
-- Sorts
------------------------------------------------------------

-- | A 'Sort' represents a set of qualifiers, and also represents a
--   set of types (in general, the intersection of the sets
--   corresponding to the qualifiers).
type Sort = Set Qualifier

-- | The special sort \(\top\) which includes all types.
topSort :: Sort
topSort :: Sort
topSort = Sort
forall a. Set a
S.empty