{-# LANGUAGE OverloadedStrings #-}

module Unison.Syntax.TypeParser
  ( computationType,
    valueType,
    valueTypeLeaf,
  )
where

import Control.Monad.Reader (asks)
import Data.Set qualified as Set
import Text.Megaparsec qualified as P
import Unison.ABT qualified as ABT
import Unison.Builtin.Decls qualified as DD
import Unison.HashQualified qualified as HQ
import Unison.NamesWithHistory qualified as Names
import Unison.Parser.Ann (Ann (..))
import Unison.Prelude
import Unison.Syntax.Lexer qualified as L
import Unison.Syntax.Name qualified as Name (toVar)
import Unison.Syntax.Parser
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Var (Var)

-- A parsed type is annotated with its starting and ending position in the
-- source text.
type TypeP v m = P v m (Type v Ann)

-- Value types cannot have effects, unless those effects appear to
-- the right of a function arrow:
--   valueType ::= Int | Text | App valueType valueType | Arrow valueType computationType
valueType :: (Monad m, Var v) => TypeP v m
valueType :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueType = TypeP v m -> TypeP v m
forall v (m :: * -> *). Var v => TypeP v m -> TypeP v m
forAll TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type1 TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type1

-- Computation
-- computationType ::= [{effect*}] valueType
computationType :: (Monad m, Var v) => TypeP v m
computationType :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
computationType = TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effect TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueType

valueTypeLeaf :: (Monad m, Var v) => TypeP v m
valueTypeLeaf :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueTypeLeaf =
  TypeP v m -> TypeP v m
forall v (m :: * -> *). Var v => TypeP v m -> TypeP v m
tupleOrParenthesizedType TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueType TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
typeAtom TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
sequenceTyp

-- Examples: Optional, Optional#abc, woot, #abc
typeAtom :: (Monad m, Var v) => TypeP v m
typeAtom :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
typeAtom =
  P v m (Token (HashQualified Name))
forall v (m :: * -> *). Ord v => P v m (Token (HashQualified Name))
hqPrefixId P v m (Token (HashQualified Name))
-> (Token (HashQualified Name)
    -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann))
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann)
forall a b.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> (a -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) b)
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Token (HashQualified Name)
tok -> case Token (HashQualified Name) -> HashQualified Name
forall a. Token a -> a
L.payload Token (HashQualified Name)
tok of
    HQ.NameOnly Name
n -> Type v Ann
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann)
forall a. a -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v Ann
 -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann))
-> Type v Ann
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> v -> Type v Ann
forall v a. Ord v => a -> v -> Type v a
Type.var (Token (HashQualified Name) -> Ann
forall a. Annotated a => a -> Ann
ann Token (HashQualified Name)
tok) (Name -> v
forall v. Var v => Name -> v
Name.toVar Name
n)
    HashQualified Name
hq -> do
      Names
names <- (ParsingEnv m -> Names)
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) Names
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ParsingEnv m -> Names
forall (m :: * -> *). ParsingEnv m -> Names
names
      let matches :: Set TypeReference
matches = SearchType -> HashQualified Name -> Names -> Set TypeReference
Names.lookupHQType SearchType
Names.IncludeSuffixes HashQualified Name
hq Names
names
      if Set TypeReference -> Int
forall a. Set a -> Int
Set.size Set TypeReference
matches Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1
        then Error v
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann)
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
P.customFailure (Token (HashQualified Name) -> Set TypeReference -> Error v
forall v.
Token (HashQualified Name) -> Set TypeReference -> Error v
UnknownType Token (HashQualified Name)
tok Set TypeReference
matches)
        else Type v Ann
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann)
forall a. a -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v Ann
 -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann))
-> Type v Ann
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Type v Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> TypeReference -> Type v Ann
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref (Token (HashQualified Name) -> Ann
forall a. Annotated a => a -> Ann
ann Token (HashQualified Name)
tok) (Set TypeReference -> TypeReference
forall a. Set a -> a
Set.findMin Set TypeReference
matches)

type1 :: (Monad m, Var v) => TypeP v m
type1 :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type1 = TypeP v m -> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m -> TypeP v m
arrow TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type2a

type2a :: (Monad m, Var v) => TypeP v m
type2a :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type2a = TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
delayed TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type2

delayed :: (Monad m, Var v) => TypeP v m
delayed :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
delayed = do
  Token String
q <- String -> P v m (Token String)
forall v (m :: * -> *). Ord v => String -> P v m (Token String)
reserved String
"'"
  Type v Ann
t <- TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effect TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Type v Ann -> Type v Ann
forall {v}. Ord v => Term F v Ann -> Term F v Ann
pt (Type v Ann -> Type v Ann) -> TypeP v m -> TypeP v m
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type2a)
  pure $
    Ann -> Type v Ann -> Type v Ann -> Type v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.arrow
      (Pos -> Pos -> Ann
Ann (Token String -> Pos
forall a. Token a -> Pos
L.start Token String
q) (Ann -> Pos
end (Ann -> Pos) -> Ann -> Pos
forall a b. (a -> b) -> a -> b
$ Type v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Type v Ann
t))
      (Ann -> Type v Ann
forall v a. Ord v => a -> Type v a
DD.thunkArgType (Token String -> Ann
forall a. Annotated a => a -> Ann
ann Token String
q))
      Type v Ann
t
  where
    -- if no abilities listed on 't, assume '{} t
    pt :: Term F v Ann -> Term F v Ann
pt Term F v Ann
t = Ann -> [Term F v Ann] -> Term F v Ann -> Term F v Ann
forall v a. Ord v => a -> [Type v a] -> Type v a -> Type v a
Type.effect (Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
t) [] Term F v Ann
t

type2 :: (Monad m, Var v) => TypeP v m
type2 :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type2 = do
  Type v Ann
hd <- TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueTypeLeaf
  [Type v Ann]
tl <- TypeP v m
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [Type v Ann]
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effectList TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueTypeLeaf)
  pure $ (Type v Ann -> Type v Ann -> Type v Ann)
-> Type v Ann -> [Type v Ann] -> Type v Ann
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Type v Ann
a Type v Ann
b -> Ann -> Type v Ann -> Type v Ann -> Type v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app (Type v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Type v Ann
a Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Type v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Type v Ann
b) Type v Ann
a Type v Ann
b) Type v Ann
hd [Type v Ann]
tl

-- ex : {State Text, IO} (List Int)
effect :: (Monad m, Var v) => TypeP v m
effect :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effect = do
  Type v Ann
es <- TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effectList
  Type v Ann
t <- TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
type2
  pure (Ann -> Type v Ann -> Type v Ann -> Type v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.effect1 (Type v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Type v Ann
es Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Type v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Type v Ann
t) Type v Ann
es Type v Ann
t)

effectList :: (Monad m, Var v) => TypeP v m
effectList :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effectList = do
  Token ()
open <- String -> P v m (Token ())
forall v (m :: * -> *). Ord v => String -> P v m (Token ())
openBlockWith String
"{"
  [Type v Ann]
es <- P v m (Token String) -> TypeP v m -> P v m [Type v Ann]
forall v (m :: * -> *) a b.
Ord v =>
P v m a -> P v m b -> P v m [b]
sepBy (String -> P v m (Token String)
forall v (m :: * -> *). Ord v => String -> P v m (Token String)
reserved String
",") TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueType
  Token ()
close <- P v m (Token ())
forall v (m :: * -> *). Ord v => P v m (Token ())
closeBlock
  pure $ Ann -> [Type v Ann] -> Type v Ann
forall v a. Ord v => a -> [Type v a] -> Type v a
Type.effects (Token () -> Ann
forall a. Annotated a => a -> Ann
ann Token ()
open Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Token () -> Ann
forall a. Annotated a => a -> Ann
ann Token ()
close) [Type v Ann]
es

sequenceTyp :: (Monad m, Var v) => TypeP v m
sequenceTyp :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
sequenceTyp = do
  Token ()
open <- String -> P v m (Token ())
forall v (m :: * -> *). Ord v => String -> P v m (Token ())
openBlockWith String
"["
  Type v Ann
t <- TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
valueType
  Token ()
close <- P v m (Token ())
forall v (m :: * -> *). Ord v => P v m (Token ())
closeBlock
  let a :: Ann
a = Token () -> Ann
forall a. Annotated a => a -> Ann
ann Token ()
open Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Token () -> Ann
forall a. Annotated a => a -> Ann
ann Token ()
close
  Type v Ann -> TypeP v m
forall a. a -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v Ann -> TypeP v m) -> Type v Ann -> TypeP v m
forall a b. (a -> b) -> a -> b
$ Ann -> Type v Ann -> Type v Ann -> Type v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app Ann
a (Ann -> Type v Ann
forall v a. Ord v => a -> Type v a
Type.list Ann
a) Type v Ann
t

tupleOrParenthesizedType :: (Var v) => TypeP v m -> TypeP v m
tupleOrParenthesizedType :: forall v (m :: * -> *). Var v => TypeP v m -> TypeP v m
tupleOrParenthesizedType TypeP v m
rec = do
  (Ann
spanAnn, Type v Ann
ty) <- TypeP v m
-> (Ann -> Type v Ann)
-> (Type v Ann -> Type v Ann -> Type v Ann)
-> P v m (Ann, Type v Ann)
forall v (m :: * -> *) a.
Ord v =>
P v m a -> (Ann -> a) -> (a -> a -> a) -> P v m (Ann, a)
tupleOrParenthesized TypeP v m
rec Ann -> Type v Ann
forall v a. Ord v => a -> Type v a
DD.unitType Type v Ann -> Type v Ann -> Type v Ann
forall {v}. Ord v => Term F v Ann -> Term F v Ann -> Term F v Ann
pair
  Type v Ann -> TypeP v m
forall a. a -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v Ann
ty {ABT.annotation = ABT.annotation ty <> spanAnn})
  where
    pair :: Term F v Ann -> Term F v Ann -> Term F v Ann
pair Term F v Ann
t1 Term F v Ann
t2 =
      let a :: Ann
a = Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
t1 Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
t2
       in Ann -> Term F v Ann -> Term F v Ann -> Term F v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app Ann
a (Ann -> Term F v Ann -> Term F v Ann -> Term F v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app (Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
t1) (Ann -> Term F v Ann
forall v a. Ord v => a -> Type v a
DD.pairType Ann
a) Term F v Ann
t1) Term F v Ann
t2

--  valueType ::= ... | Arrow valueType computationType
arrow :: (Monad m, Var v) => TypeP v m -> TypeP v m
arrow :: forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m -> TypeP v m
arrow TypeP v m
rec =
  let eff :: ParsecT
  (Error v)
  Input
  (ReaderT (ParsingEnv m) m)
  (Term F v Ann -> Term F v Ann -> Term F v Ann)
eff = Maybe (Term F v Ann)
-> Term F v Ann -> Term F v Ann -> Term F v Ann
forall {v}.
Ord v =>
Maybe (Term F v Ann)
-> Term F v Ann -> Term F v Ann -> Term F v Ann
mkArr (Maybe (Term F v Ann)
 -> Term F v Ann -> Term F v Ann -> Term F v Ann)
-> ParsecT
     (Error v) Input (ReaderT (ParsingEnv m) m) (Maybe (Term F v Ann))
-> ParsecT
     (Error v)
     Input
     (ReaderT (ParsingEnv m) m)
     (Term F v Ann -> Term F v Ann -> Term F v Ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeP v m
-> ParsecT
     (Error v) Input (ReaderT (ParsingEnv m) m) (Maybe (Term F v Ann))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effectList
      mkArr :: Maybe (Term F v Ann)
-> Term F v Ann -> Term F v Ann -> Term F v Ann
mkArr Maybe (Term F v Ann)
Nothing Term F v Ann
a Term F v Ann
b = Ann -> Term F v Ann -> Term F v Ann -> Term F v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.arrow (Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
a Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
b) Term F v Ann
a Term F v Ann
b
      mkArr (Just Term F v Ann
es) Term F v Ann
a Term F v Ann
b = Ann -> Term F v Ann -> Term F v Ann -> Term F v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.arrow (Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
a Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
b) Term F v Ann
a (Ann -> Term F v Ann -> Term F v Ann -> Term F v Ann
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.effect1 (Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
es Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Term F v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Term F v Ann
b) Term F v Ann
es Term F v Ann
b)
   in TypeP v m
-> ParsecT
     (Error v)
     Input
     (ReaderT (ParsingEnv m) m)
     (Term F v Ann -> Term F v Ann -> Term F v Ann)
-> TypeP v m
forall v (m :: * -> *) a.
Ord v =>
P v m a -> P v m (a -> a -> a) -> P v m a
chainr1 (TypeP v m
forall (m :: * -> *) v. (Monad m, Var v) => TypeP v m
effect TypeP v m -> TypeP v m -> TypeP v m
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeP v m
rec) (String -> P v m (Token String)
forall v (m :: * -> *). Ord v => String -> P v m (Token String)
reserved String
"->" P v m (Token String)
-> ParsecT
     (Error v)
     Input
     (ReaderT (ParsingEnv m) m)
     (Term F v Ann -> Term F v Ann -> Term F v Ann)
-> ParsecT
     (Error v)
     Input
     (ReaderT (ParsingEnv m) m)
     (Term F v Ann -> Term F v Ann -> Term F v Ann)
forall a b.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) b
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  (Error v)
  Input
  (ReaderT (ParsingEnv m) m)
  (Term F v Ann -> Term F v Ann -> Term F v Ann)
eff)

-- "forall a b . List a -> List b -> Maybe Text"
forAll :: (Var v) => TypeP v m -> TypeP v m
forAll :: forall v (m :: * -> *). Var v => TypeP v m -> TypeP v m
forAll TypeP v m
rec = do
  Token String
kw <- String -> P v m (Token String)
forall v (m :: * -> *). Ord v => String -> P v m (Token String)
reserved String
"forall" P v m (Token String)
-> P v m (Token String) -> P v m (Token String)
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> P v m (Token String)
forall v (m :: * -> *). Ord v => String -> P v m (Token String)
reserved String
"∀"
  [v]
vars <- ([Token v] -> [v])
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [Token v]
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [v]
forall a b.
(a -> b)
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Token v -> v) -> [Token v] -> [v]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token v -> v
forall a. Token a -> a
L.payload) (ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [Token v]
 -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [v])
-> (ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Token v)
    -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [Token v])
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Token v)
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Token v)
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [Token v]
forall a.
ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) a
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Token v)
 -> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [v])
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Token v)
-> ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) [v]
forall a b. (a -> b) -> a -> b
$ ParsecT (Error v) Input (ReaderT (ParsingEnv m) m) (Token v)
forall v (m :: * -> *). Var v => P v m (Token v)
prefixDefinitionName
  Token String
_ <- String -> P v m (Token String)
forall v (m :: * -> *). Ord v => String -> P v m (Token String)
reserved String
"."
  Type v Ann
t <- TypeP v m
rec
  pure $ Ann -> [v] -> Type v Ann -> Type v Ann
forall v a. Ord v => a -> [v] -> Type v a -> Type v a
Type.foralls (Token String -> Ann
forall a. Annotated a => a -> Ann
ann Token String
kw Ann -> Ann -> Ann
forall a. Semigroup a => a -> a -> a
<> Type v Ann -> Ann
forall a. Annotated a => a -> Ann
ann Type v Ann
t) [v]
vars Type v Ann
t