-- | The basic syntax and operations on types.
module Glam.Type where

import Control.Monad
import Data.List
import Data.String
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Map (Map)
import Data.Map qualified as Map
import Text.Megaparsec
import Control.Monad.Combinators.Expr

import Glam.Utils

-- | Type variables
type TVar = String

-- | Type substitutions
type TSubst = Map TVar Type

-- | Whether a type, or term, is constant. Note that 'False' means "we don't know".
type Constancy = Bool

-- | A fixed point variable can only be used when it is /guarded/ by a @▸@ modality.
data Guardedness = Unguarded -- ^ Can't use it yet
                 | Guarded -- ^ OK, under @▸@
                 | Forbidden -- ^ No way, we're under @■@
                 deriving Guardedness -> Guardedness -> Bool
(Guardedness -> Guardedness -> Bool)
-> (Guardedness -> Guardedness -> Bool) -> Eq Guardedness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Guardedness -> Guardedness -> Bool
== :: Guardedness -> Guardedness -> Bool
$c/= :: Guardedness -> Guardedness -> Bool
/= :: Guardedness -> Guardedness -> Bool
Eq

infixr 7 :*:
infixr 6 :+:
infixr 5 :->:

-- | Monomorphic types of the guarded λ-calculus
data Type = TVar TVar -- ^ Variables
          | TInt -- ^ Integers
          | TApp Type Type -- ^ Applications
          | One | Type :*: Type -- ^ Products
          | Zero | Type :+: Type -- ^ Sums
          | Type :->: Type -- ^ Functions
          | Later Type -- ^ @▸@ modality
          | Constant Type -- ^ @■@ modality
          | TFix TVar Type -- ^ Fixed points
          deriving Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
/= :: Type -> Type -> Bool
Eq

-- | Polymorphic type schemes
data Polytype = Forall [(TVar, Constancy)] Type
              deriving Polytype -> Polytype -> Bool
(Polytype -> Polytype -> Bool)
-> (Polytype -> Polytype -> Bool) -> Eq Polytype
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Polytype -> Polytype -> Bool
== :: Polytype -> Polytype -> Bool
$c/= :: Polytype -> Polytype -> Bool
/= :: Polytype -> Polytype -> Bool
Eq

pattern $mMonotype :: forall {r}. Polytype -> (Type -> r) -> ((# #) -> r) -> r
$bMonotype :: Type -> Polytype
Monotype ty = Forall [] ty

instance IsString Type where
    fromString :: [Char] -> Type
fromString = [Char] -> Type
TVar

-- * Variables and substitution

class HasTVars t where
    freeTVars :: t -> Set TVar
    allTVars :: t -> Set TVar

instance HasTVars Type where
    freeTVars :: Type -> Set [Char]
freeTVars (TVar [Char]
x)     = [Char] -> Set [Char]
forall a. a -> Set a
Set.singleton [Char]
x
    freeTVars (Type
t1 :*: Type
t2)  = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t1 Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t2
    freeTVars (Type
t1 :+: Type
t2)  = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t1 Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t2
    freeTVars (Type
t1 :->: Type
t2) = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t1 Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t2
    freeTVars (Later Type
t)    = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t
    freeTVars (Constant Type
t) = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t
    freeTVars (TFix [Char]
x Type
t)   = [Char] -> Set [Char] -> Set [Char]
forall a. Ord a => a -> Set a -> Set a
Set.delete [Char]
x (Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
t)
    freeTVars Type
_            = Set [Char]
forall a. Monoid a => a
mempty
    allTVars :: Type -> Set [Char]
allTVars (TVar [Char]
x)     = [Char] -> Set [Char]
forall a. a -> Set a
Set.singleton [Char]
x
    allTVars (Type
t1 :*: Type
t2)  = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t1 Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t2
    allTVars (Type
t1 :+: Type
t2)  = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t1 Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t2
    allTVars (Type
t1 :->: Type
t2) = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t1 Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t2
    allTVars (Later Type
t)    = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t
    allTVars (Constant Type
t) = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t
    allTVars (TFix [Char]
x Type
t)   = [Char] -> Set [Char] -> Set [Char]
forall a. Ord a => a -> Set a -> Set a
Set.insert [Char]
x (Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
t)
    allTVars Type
_            = Set [Char]
forall a. Monoid a => a
mempty

instance HasTVars Polytype where
    freeTVars :: Polytype -> Set [Char]
freeTVars (Forall ((([Char], Bool) -> [Char]) -> [([Char], Bool)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], Bool) -> [Char]
forall a b. (a, b) -> a
fst -> [[Char]]
xs) Type
ty) = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
ty Set [Char] -> Set [Char] -> Set [Char]
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ [[Char]] -> Set [Char]
forall a. Ord a => [a] -> Set a
Set.fromList [[Char]]
xs
    allTVars :: Polytype -> Set [Char]
allTVars (Forall ((([Char], Bool) -> [Char]) -> [([Char], Bool)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], Bool) -> [Char]
forall a b. (a, b) -> a
fst -> [[Char]]
xs) Type
ty) = Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
allTVars Type
ty Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> [[Char]] -> Set [Char]
forall a. Ord a => [a] -> Set a
Set.fromList [[Char]]
xs

[Char]
x freeInType :: [Char] -> t -> Bool
`freeInType` t
t = [Char]
x [Char] -> Set [Char] -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` t -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars t
t

freshTVarsFor :: Set TVar -> [TVar]
freshTVarsFor :: Set [Char] -> [[Char]]
freshTVarsFor Set [Char]
xs = [[Char]
x | Int
n <- [Int
1..]
                      , [Char]
x <- Int -> [Char] -> [[Char]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n [Char
'a'..Char
'z']
                      , [Char]
x [Char] -> Set [Char] -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set [Char]
xs]

avoidCaptureType :: Set [Char] -> ([Char], Type) -> ([Char], Type)
avoidCaptureType Set [Char]
vs ([Char]
x, Type
ty)
    | [Char]
x [Char] -> Set [Char] -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set [Char]
vs = ([Char]
y, [Char] -> Type -> Type -> Type
substituteType1 [Char]
x ([Char] -> Type
TVar [Char]
y) Type
ty)
    | Bool
otherwise = ([Char]
x, Type
ty)
    where [Char]
y:[[Char]]
_ = Set [Char] -> [[Char]]
freshTVarsFor (Set [Char]
vs Set [Char] -> Set [Char] -> Set [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> Set [Char] -> Set [Char]
forall a. Ord a => a -> Set a -> Set a
Set.delete [Char]
x (Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Type
ty))

substituteType :: TSubst -> Type -> Type
substituteType :: TSubst -> Type -> Type
substituteType TSubst
s (TVar [Char]
x) = Type -> [Char] -> TSubst -> Type
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Type
TVar [Char]
x) [Char]
x TSubst
s
substituteType TSubst
s (Type
t1 :*: Type
t2) = TSubst -> Type -> Type
substituteType TSubst
s Type
t1 Type -> Type -> Type
:*: TSubst -> Type -> Type
substituteType TSubst
s Type
t2
substituteType TSubst
s (Type
t1 :+: Type
t2) = TSubst -> Type -> Type
substituteType TSubst
s Type
t1 Type -> Type -> Type
:+: TSubst -> Type -> Type
substituteType TSubst
s Type
t2
substituteType TSubst
s (Type
t1 :->: Type
t2) = TSubst -> Type -> Type
substituteType TSubst
s Type
t1 Type -> Type -> Type
:->: TSubst -> Type -> Type
substituteType TSubst
s Type
t2
substituteType TSubst
s (Later Type
t1) = Type -> Type
Later (TSubst -> Type -> Type
substituteType TSubst
s Type
t1)
substituteType TSubst
s (Constant Type
t1) = Type -> Type
Constant (TSubst -> Type -> Type
substituteType TSubst
s Type
t1)
substituteType TSubst
s (TFix [Char]
x Type
tf) = [Char] -> Type -> Type
TFix [Char]
x' (TSubst -> Type -> Type
substituteType ([Char] -> TSubst -> TSubst
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete [Char]
x' TSubst
s) Type
tf')
    where ([Char]
x', Type
tf') = Set [Char] -> ([Char], Type) -> ([Char], Type)
avoidCaptureType ((Type -> Set [Char]) -> TSubst -> Set [Char]
forall m a. Monoid m => (a -> m) -> Map [Char] a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars TSubst
s) ([Char]
x, Type
tf)
substituteType TSubst
_ Type
ty = Type
ty

substituteType1 :: [Char] -> Type -> Type -> Type
substituteType1 [Char]
x Type
s = TSubst -> Type -> Type
substituteType ([Char] -> Type -> TSubst
forall k a. k -> a -> Map k a
Map.singleton [Char]
x Type
s)

alphaNormalise :: Polytype -> Polytype
alphaNormalise :: Polytype -> Polytype
alphaNormalise pty :: Polytype
pty@(Forall [([Char], Bool)]
as Type
ty) = [([Char], Bool)] -> Type -> Polytype
Forall [([Char]
b, Bool
c) | (([Char]
_, Bool
c), [Char]
b) <- [(([Char], Bool), [Char])]
s] Type
ty' where
    s :: [(([Char], Bool), [Char])]
s = [([Char], Bool)] -> [[Char]] -> [(([Char], Bool), [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip [([Char], Bool)]
as (Set [Char] -> [[Char]]
freshTVarsFor (Polytype -> Set [Char]
forall t. HasTVars t => t -> Set [Char]
freeTVars Polytype
pty))
    ty' :: Type
ty' = TSubst -> Type -> Type
substituteType ([([Char], Type)] -> TSubst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [([Char]
a, [Char] -> Type
TVar [Char]
b) | (([Char]
a, Bool
_), [Char]
b) <- [(([Char], Bool), [Char])]
s]) Type
ty

-- * Printing

prodPrec :: a
prodPrec = a
6
sumPrec :: a
sumPrec = a
4
funPrec :: a
funPrec = a
0
modPrec :: a
modPrec = a
8
appPrec :: a
appPrec = a
10

instance Show Type where
    showsPrec :: Int -> Type -> ShowS
showsPrec Int
_ (TVar [Char]
x)     = [Char] -> ShowS
showString [Char]
x
    showsPrec Int
_ Type
TInt         = [Char] -> ShowS
showString [Char]
"Int"
    showsPrec Int
d (TApp Type
t1 Type
t2) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
forall {a}. Num a => a
appPrec Type
t1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
t2
    showsPrec Int
_ Type
One          = [Char] -> ShowS
showString [Char]
"1"
    showsPrec Int
d (Type
t1 :*: Type
t2)  = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
prodPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
forall {a}. Num a => a
prodPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
t1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" * " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
forall {a}. Num a => a
prodPrec Type
t2
    showsPrec Int
_ Type
Zero         = [Char] -> ShowS
showString [Char]
"0"
    showsPrec Int
d (Type
t1 :+: Type
t2)  = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
sumPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
forall {a}. Num a => a
sumPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
t1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" + " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
forall {a}. Num a => a
sumPrec Type
t2
    showsPrec Int
d (Type
t1 :->: Type
t2) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
funPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
forall {a}. Num a => a
funPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
t1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
" -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
forall {a}. Num a => a
funPrec Type
t2
    showsPrec Int
d (Later Type
ty)    = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
modPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        [Char] -> ShowS
showString [Char]
">" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
forall {a}. Num a => a
modPrec Type
ty
    showsPrec Int
d (Constant Type
ty) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
modPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        [Char] -> ShowS
showString [Char]
"#" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
forall {a}. Num a => a
modPrec Type
ty
    showsPrec Int
_ (TFix [Char]
x Type
tf)   = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        [Char] -> ShowS
showString [Char]
"Fix " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
". " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ShowS
forall a. Show a => a -> ShowS
shows Type
tf

instance Show Polytype where
    showsPrec :: Int -> Polytype -> ShowS
showsPrec Int
_ (Forall [] Type
ty) = Type -> ShowS
forall a. Show a => a -> ShowS
shows Type
ty
    showsPrec Int
_ (Forall [([Char], Bool)]
xs Type
ty) = [Char] -> ShowS
showString [Char]
"forall " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " [(if Bool
c then [Char]
"#" else [Char]
"") [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
x | ([Char]
x, Bool
c) <- [([Char], Bool)]
xs]) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ShowS
showString [Char]
". " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ShowS
forall a. Show a => a -> ShowS
shows Type
ty

-- * Parsing

tVar :: Parser TVar
tVar :: ReaderT IndentRef (Parsec Void [Char]) [Char]
tVar = [[Char]] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
mkIdentifier [[Char]
"type", [Char]
"Fix", [Char]
"μ", [Char]
"Int", [Char]
"ℤ", [Char]
"forall"]

tConstant :: ReaderT IndentRef (Parsec Void [Char]) [Char]
tConstant = [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"#" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"■"

type_ :: Parser Type
type_ :: Parser Type
type_ = Parser Type
tfix Parser Type -> Parser Type -> Parser Type
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Type
-> [[Operator (ReaderT IndentRef (Parsec Void [Char])) Type]]
-> Parser Type
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser Parser Type
base [[Operator (ReaderT IndentRef (Parsec Void [Char])) Type]]
ops Parser Type -> [Char] -> Parser Type
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"type"
    where
    tfix :: Parser Type
tfix = [Char] -> Type -> Type
TFix ([Char] -> Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) ([Char] -> Type -> Type)
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (ReaderT IndentRef (Parsec Void [Char]) [Char]
"Fix" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT IndentRef (Parsec Void [Char]) [Char]
"μ") ReaderT IndentRef (Parsec Void [Char]) ([Char] -> Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
forall a b.
ReaderT IndentRef (Parsec Void [Char]) (a -> b)
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void [Char]) [Char]
tVar ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
forall a b.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReaderT IndentRef (Parsec Void [Char]) [Char]
dot ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
-> Parser Type -> Parser Type
forall a b.
ReaderT IndentRef (Parsec Void [Char]) (a -> b)
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Type
type_
    base :: Parser Type
base =  Type
TInt Type
-> ReaderT IndentRef (Parsec Void [Char]) [Char] -> Parser Type
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (ReaderT IndentRef (Parsec Void [Char]) [Char]
"Int" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT IndentRef (Parsec Void [Char]) [Char]
"ℤ")
        Parser Type -> Parser Type -> Parser Type
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Type
TVar ([Char] -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Char] -> Parser Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT IndentRef (Parsec Void [Char]) [Char]
tVar
        Parser Type -> Parser Type -> Parser Type
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
One Type
-> ReaderT IndentRef (Parsec Void [Char]) [Char] -> Parser Type
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"1" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"⊤")
        Parser Type -> Parser Type -> Parser Type
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
Zero Type
-> ReaderT IndentRef (Parsec Void [Char]) [Char] -> Parser Type
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"0" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"⊥")
        Parser Type -> Parser Type -> Parser Type
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Type -> Parser Type
forall a. Parser a -> Parser a
parens Parser Type
type_
    modality :: ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
modality =  Type -> Type
Later (Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
">" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"▸")
            ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type -> Type
Constant (Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReaderT IndentRef (Parsec Void [Char]) [Char]
tConstant
    ops :: [[Operator (ReaderT IndentRef (Parsec Void [Char])) Type]]
ops = [ [ReaderT IndentRef (Parsec Void [Char]) (Type -> Type -> Type)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL ((Type -> Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type -> Type)
forall a. a -> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type -> Type -> Type
TApp)]
          , [ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) Type
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (((Type -> Type) -> (Type -> Type) -> Type -> Type)
-> [Type -> Type] -> Type -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ([Type -> Type] -> Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Type -> Type]
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
-> ReaderT IndentRef (Parsec Void [Char]) [Type -> Type]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some ReaderT IndentRef (Parsec Void [Char]) (Type -> Type)
modality)]
          , [[[Char]]
-> (Type -> Type -> Type)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) Type
forall {a}.
[[Char]]
-> (a -> a -> a)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) a
binary [[Char]
"*", [Char]
"×"] Type -> Type -> Type
(:*:)]
          , [[[Char]]
-> (Type -> Type -> Type)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) Type
forall {a}.
[[Char]]
-> (a -> a -> a)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) a
binary [[Char]
"+"] Type -> Type -> Type
(:+:)]
          , [[[Char]]
-> (Type -> Type -> Type)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) Type
forall {a}.
[[Char]]
-> (a -> a -> a)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) a
binary [[Char]
"->", [Char]
"→"] Type -> Type -> Type
(:->:)] ]
    binary :: [[Char]]
-> (a -> a -> a)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) a
binary [[Char]]
s a -> a -> a
f = ReaderT IndentRef (Parsec Void [Char]) (a -> a -> a)
-> Operator (ReaderT IndentRef (Parsec Void [Char])) a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (a -> a -> a
f (a -> a -> a)
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) (a -> a -> a)
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [ReaderT IndentRef (Parsec Void [Char]) [Char]]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice (([Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char])
-> [[Char]] -> [ReaderT IndentRef (Parsec Void [Char]) [Char]]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [[Char]]
s))

quantifiedTVar :: Parser (TVar, Constancy)
quantifiedTVar :: Parser ([Char], Bool)
quantifiedTVar = ([Char] -> Bool -> ([Char], Bool))
-> Bool -> [Char] -> ([Char], Bool)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) (Bool -> [Char] -> ([Char], Bool))
-> ReaderT IndentRef (Parsec Void [Char]) Bool
-> ReaderT
     IndentRef (Parsec Void [Char]) ([Char] -> ([Char], Bool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> ReaderT IndentRef (Parsec Void [Char]) Bool
-> ReaderT IndentRef (Parsec Void [Char]) Bool
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
option Bool
False (Bool
True Bool
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) Bool
forall a b.
a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReaderT IndentRef (Parsec Void [Char]) [Char]
tConstant) ReaderT IndentRef (Parsec Void [Char]) ([Char] -> ([Char], Bool))
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> Parser ([Char], Bool)
forall a b.
ReaderT IndentRef (Parsec Void [Char]) (a -> b)
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void [Char]) [Char]
tVar

polytype :: Parser Polytype
polytype :: Parser Polytype
polytype = [([Char], Bool)] -> Type -> Polytype
Forall ([([Char], Bool)] -> Type -> Polytype)
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
-> ReaderT IndentRef (Parsec Void [Char]) (Type -> Polytype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Char], Bool)]
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
option [] ((ReaderT IndentRef (Parsec Void [Char]) [Char]
"forall" ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
forall a.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> ReaderT IndentRef (Parsec Void [Char]) [Char]
symbol [Char]
"∀") ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
forall a b.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ([Char], Bool)
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser ([Char], Bool)
quantifiedTVar ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
-> ReaderT IndentRef (Parsec Void [Char]) [Char]
-> ReaderT IndentRef (Parsec Void [Char]) [([Char], Bool)]
forall a b.
ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
-> ReaderT IndentRef (Parsec Void [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReaderT IndentRef (Parsec Void [Char]) [Char]
dot) ReaderT IndentRef (Parsec Void [Char]) (Type -> Polytype)
-> Parser Type -> Parser Polytype
forall a b.
ReaderT IndentRef (Parsec Void [Char]) (a -> b)
-> ReaderT IndentRef (Parsec Void [Char]) a
-> ReaderT IndentRef (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Type
type_