{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Parsing types in the Swarm language.
module Swarm.Language.Parser.Type (
  parsePolytype,
  parseType,
  parseTypeMolecule,
  parseTypeAtom,
  parseTyCon,
) where

import Control.Lens (view)
import Control.Monad (join)
import Control.Monad.Combinators (many)
import Control.Monad.Combinators.Expr (Operator (..), makeExprParser)
import Data.Fix (Fix (..), foldFix)
import Data.List.Extra (enumerate)
import Data.Maybe (fromMaybe)
import Data.Set qualified as S
import Swarm.Language.Parser.Core (LanguageVersion (..), Parser, languageVersion)
import Swarm.Language.Parser.Lex (
  braces,
  brackets,
  parens,
  reserved,
  reservedCS,
  symbol,
  tyName,
  tyVar,
 )
import Swarm.Language.Parser.Record (parseRecord)
import Swarm.Language.Types
import Text.Megaparsec (choice, optional, some, (<|>))
import Witch (from)

-- | Parse a Swarm language polytype, which starts with an optional
--   quanitifation (@forall@ followed by one or more variables and a
--   period) followed by a type.  Note that anything accepted by
--   'parseType' is also accepted by 'parsePolytype'.
parsePolytype :: Parser Polytype
parsePolytype :: Parser Polytype
parsePolytype =
  ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  (Parser Polytype)
-> Parser Polytype
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ReaderT
   ParserConfig
   (StateT CommentState (Parsec Void Var))
   (Parser Polytype)
 -> Parser Polytype)
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     (Parser Polytype)
-> Parser Polytype
forall a b. (a -> b) -> a -> b
$
    ( [Var] -> Type -> Parser Polytype
quantify ([Var] -> Type -> Parser Polytype)
-> (Maybe [Var] -> [Var]) -> Maybe [Var] -> Type -> Parser Polytype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> Maybe [Var] -> [Var]
forall a. a -> Maybe a -> a
fromMaybe []
        (Maybe [Var] -> Type -> Parser Polytype)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) (Maybe [Var])
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     (Type -> Parser Polytype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) [Var]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) (Maybe [Var])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional ((Var -> Parser ()
reserved Var
"forall" Parser () -> Parser () -> Parser ()
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> Parser ()
reserved Var
"∀") Parser ()
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Var]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Var]
forall a b.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Var]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
tyVar ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) [Var]
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Var]
forall a b.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
symbol Var
".")
    )
      ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  (Type -> Parser Polytype)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     (Parser Polytype)
forall a b.
ReaderT
  ParserConfig (StateT CommentState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseType
 where
  quantify :: [Var] -> Type -> Parser Polytype
  quantify :: [Var] -> Type -> Parser Polytype
quantify [Var]
xs Type
ty
    -- Iplicitly quantify over free type variables if the user didn't write a forall
    | [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
xs = Polytype -> Parser Polytype
forall a.
a -> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Polytype -> Parser Polytype) -> Polytype -> Parser Polytype
forall a b. (a -> b) -> a -> b
$ [Var] -> Type -> Polytype
forall t. [Var] -> t -> Poly t
Forall (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
free) Type
ty
    -- Otherwise, require all variables to be explicitly quantified
    | Set Var -> Bool
forall a. Set a -> Bool
S.null Set Var
free = Polytype -> Parser Polytype
forall a.
a -> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Polytype -> Parser Polytype) -> Polytype -> Parser Polytype
forall a b. (a -> b) -> a -> b
$ [Var] -> Type -> Polytype
forall t. [Var] -> t -> Poly t
Forall [Var]
xs Type
ty
    | Bool
otherwise =
        [Char] -> Parser Polytype
forall a.
[Char]
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser Polytype) -> [Char] -> Parser Polytype
forall a b. (a -> b) -> a -> b
$
          [[Char]] -> [Char]
unlines
            [ [Char]
"  Type contains free variable(s): " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ((Var -> [Char]) -> [Var] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Var -> [Char]
forall source target. From source target => source -> target
from (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
free))
            , [Char]
"  Try adding them to the 'forall'."
            ]
   where
    free :: Set Var
free = Type -> Set Var
tyVars Type
ty Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs

-- | Parse a Swarm language (mono)type.
parseType :: Parser Type
parseType :: ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseType = ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> [[Operator
       (ReaderT ParserConfig (StateT CommentState (Parsec Void Var)))
       Type]]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseTypeMolecule [[Operator
    (ReaderT ParserConfig (StateT CommentState (Parsec Void Var)))
    Type]]
table
 where
  table :: [[Operator
    (ReaderT ParserConfig (StateT CommentState (Parsec Void Var)))
    Type]]
table =
    [ [ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  (Type -> Type -> Type)
-> Operator
     (ReaderT ParserConfig (StateT CommentState (Parsec Void Var))) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (Type -> Type -> Type
(:*:) (Type -> Type -> Type)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     (Type -> Type -> Type)
forall a b.
a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
symbol Var
"*")]
    , [ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  (Type -> Type -> Type)
-> Operator
     (ReaderT ParserConfig (StateT CommentState (Parsec Void Var))) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (Type -> Type -> Type
(:+:) (Type -> Type -> Type)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     (Type -> Type -> Type)
forall a b.
a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
symbol Var
"+")]
    , [ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  (Type -> Type -> Type)
-> Operator
     (ReaderT ParserConfig (StateT CommentState (Parsec Void Var))) Type
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (Type -> Type -> Type
(:->:) (Type -> Type -> Type)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     (Type -> Type -> Type)
forall a b.
a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
symbol Var
"->")]
    ]

-- | A "type molecule" consists of either a type constructor applied
--   to a chain of type atoms, or just a type atom by itself.  We have
--   to separate this out from parseTypeAtom to deal with the left
--   recursion.
parseTypeMolecule :: Parser Type
parseTypeMolecule :: ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseTypeMolecule =
  TyCon -> [Type] -> Type
TyConApp (TyCon -> [Type] -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
parseTyCon ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  ([Type] -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Type]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a b.
ReaderT
  ParserConfig (StateT CommentState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Type]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseTypeAtom
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseTypeAtom

-- | A "type atom" consists of some atomic type snytax --- type
--   variables, things in brackets of some kind, or a lone type
--   constructor.
parseTypeAtom :: Parser Type
parseTypeAtom :: ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseTypeAtom =
  Var -> Type
TyVar (Var -> Type)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
tyVar
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon -> [Type] -> Type
TyConApp (TyCon -> [Type] -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
parseTyCon ReaderT
  ParserConfig
  (StateT CommentState (Parsec Void Var))
  ([Type] -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Type]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a b.
ReaderT
  ParserConfig (StateT CommentState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) [Type]
forall a.
a -> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type -> Type
TyDelay (Type -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a. Parser a -> Parser a
braces ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseType
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Map Var Type -> Type
TyRcd (Map Var Type -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) (Map Var Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  ParserConfig (StateT CommentState (Parsec Void Var)) (Map Var Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) (Map Var Type)
forall a. Parser a -> Parser a
brackets (ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) (Map Var Type)
forall a. Parser a -> Parser (Map Var a)
parseRecord (Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
symbol Var
":" ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseType))
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> Type -> Type
tyRec (Var -> Type -> Type)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> Parser ()
reserved Var
"rec" Parser ()
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
forall a b.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
tyVar) ReaderT
  ParserConfig (StateT CommentState (Parsec Void Var)) (Type -> Type)
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a b.
ReaderT
  ParserConfig (StateT CommentState (Parsec Void Var)) (a -> b)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Var
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
symbol Var
"." ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a b.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseType)
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) Type
forall a. Parser a -> Parser a
parens ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Type
parseType

-- | A type constructor.
parseTyCon :: Parser TyCon
parseTyCon :: ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
parseTyCon = do
  LanguageVersion
ver <- Getting LanguageVersion ParserConfig LanguageVersion
-> ReaderT
     ParserConfig
     (StateT CommentState (Parsec Void Var))
     LanguageVersion
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting LanguageVersion ParserConfig LanguageVersion
Lens' ParserConfig LanguageVersion
languageVersion
  let reservedCase :: Var -> Parser ()
reservedCase = case LanguageVersion
ver of
        -- Version 0.5 of the language accepted type names in any case
        LanguageVersion
SwarmLang0_5 -> Var -> Parser ()
reserved
        -- The latest version requires them to be uppercase
        LanguageVersion
SwarmLangLatest -> Var -> Parser ()
reservedCS
  [ReaderT
   ParserConfig (StateT CommentState (Parsec Void Var)) TyCon]
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((BaseTy
 -> ReaderT
      ParserConfig (StateT CommentState (Parsec Void Var)) TyCon)
-> [BaseTy]
-> [ReaderT
      ParserConfig (StateT CommentState (Parsec Void Var)) TyCon]
forall a b. (a -> b) -> [a] -> [b]
map (\BaseTy
b -> BaseTy -> TyCon
TCBase BaseTy
b TyCon
-> Parser ()
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
forall a b.
a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser ()
reservedCase (BaseTy -> Var
baseTyName BaseTy
b)) [BaseTy]
forall a. (Enum a, Bounded a) => [a]
enumerate)
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon
TCCmd TyCon
-> Parser ()
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
forall a b.
a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) b
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser ()
reservedCase Var
"Cmd"
    ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
forall a.
ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> TyCon
TCUser (Var -> TyCon)
-> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
-> ReaderT
     ParserConfig (StateT CommentState (Parsec Void Var)) TyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT ParserConfig (StateT CommentState (Parsec Void Var)) Var
tyName

-- | Close over a recursive type, replacing any bound occurrences
--   of its variable in the body with de Bruijn indices.  Note that
--   (1) we don't have to worry about conflicts with type variables
--   bound by a top-level @forall@; since @forall@ must always be at
--   the top level, any @rec@ will necessarily be lexically within the
--   scope of any @forall@ and hence variables bound by @rec@ will
--   shadow any variables bound by a @forall@.  For example, @forall
--   a. a -> (rec a. unit + a)@ is a function from an arbitrary type
--   to a recursive natural number. (2) Any @rec@ contained inside
--   this one will have already been closed over when it was parsed,
--   and its bound variables thus replaced by de Bruijn indices, so
--   neither do we have to worry about being shadowed --- any
--   remaining free occurrences of the variable name in question are
--   indeed references to this @rec@ binder.
tyRec :: Var -> Type -> Type
tyRec :: Var -> Type -> Type
tyRec Var
x = Var -> Type -> Type
TyRec Var
x (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Nat -> Type) -> Nat -> Type
forall a b. (a -> b) -> a -> b
$ Nat
NZ) ((Nat -> Type) -> Type) -> (Type -> Nat -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeF (Nat -> Type) -> Nat -> Type) -> Type -> Nat -> Type
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix TypeF (Nat -> Type) -> Nat -> Type
s
 where
  s :: TypeF (Nat -> Type) -> Nat -> Type
  s :: TypeF (Nat -> Type) -> Nat -> Type
s = \case
    TyRecF Var
y Nat -> Type
ty -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF Type -> Type) -> (Nat -> TypeF Type) -> Nat -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type -> TypeF Type
forall t. Var -> t -> TypeF t
TyRecF Var
y (Type -> TypeF Type) -> (Nat -> Type) -> Nat -> TypeF Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Type
ty (Nat -> Type) -> (Nat -> Nat) -> Nat -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Nat
NS
    TyVarF Var
y
      | Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF Type -> Type) -> (Nat -> TypeF Type) -> Nat -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> TypeF Type
forall t. Nat -> TypeF t
TyRecVarF
      | Bool
otherwise -> Type -> Nat -> Type
forall a b. a -> b -> a
const (TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Var -> TypeF Type
forall t. Var -> TypeF t
TyVarF Var
y))
    TypeF (Nat -> Type)
fty -> \Nat
i -> TypeF Type -> Type
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (((Nat -> Type) -> Type) -> TypeF (Nat -> Type) -> TypeF Type
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Nat -> Type) -> Nat -> Type
forall a b. (a -> b) -> a -> b
$ Nat
i) TypeF (Nat -> Type)
fty)