-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- TODO [#712]: Remove this next major release
{-# OPTIONS_GHC -Wno-deprecations #-}

-- TODO [#712]: Remove this next major release
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Parsing of Michelson types.

module Morley.Michelson.Parser.Type
  ( type_
  , field
  ) where

import Prelude hiding (note, some, try)

import Data.Default (Default, def)
import Data.Map qualified as Map
import Data.Type.Equality ((:~:)(Refl))
import Fmt (pretty)
import Text.Megaparsec (choice, customFailure, label, sepBy)
import Text.Megaparsec.Char.Lexer qualified as L

import Morley.Michelson.Let (LetType(..))
import Morley.Michelson.Parser.Annotations
import Morley.Michelson.Parser.Error
import Morley.Michelson.Parser.Helpers
import Morley.Michelson.Parser.Lexer
import Morley.Michelson.Parser.Types (LetEnv, Parser, Parser', assertLetEnv, isLetEnv, letTypes)
import Morley.Michelson.Untyped
import Morley.Util.Generic

-- | This parses arbitrary type expressions.
--
-- Note that this includes parenthesized ones for efficiency, see 't_operator'.
-- That is to say, @int@, @(int)@, @((int))@, etc will match with this parser and produce @TInt@.
type_ :: Parser le Ty
type_ :: Parser' le Ty
type_ = (FieldAnn, Ty) -> Ty
forall a b. (a, b) -> b
snd ((FieldAnn, Ty) -> Ty)
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
-> Parser' le Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le FieldAnn -> Parser le (FieldAnn, Ty)
forall le. Parser le FieldAnn -> Parser le (FieldAnn, Ty)
typeInner (FieldAnn -> ReaderT le (Parsec CustomParserException Text) FieldAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure FieldAnn
forall k (a :: k). Annotation a
noAnn)

field :: Parser le (FieldAnn, Ty)
field :: Parser' le (FieldAnn, Ty)
field = Parser le FieldAnn -> Parser le (FieldAnn, Ty)
forall le. Parser le FieldAnn -> Parser le (FieldAnn, Ty)
typeInner Parser le FieldAnn
forall tag le. KnownAnnTag tag => Parser le (Annotation tag)
note

-- | 't_operator' parses tuples @(a, b, c)@, variants @(a | b | c)@, and also type expressions in
-- parentheses @(a)@ and unit @()@. This is done this way for performance considerations.
--
-- Consequently, 't_unit' doesn't bother with parsing @()@.
t_operator :: Parser' le FieldAnn -> Parser le (FieldAnn, Ty)
t_operator :: Parser' le FieldAnn -> Parser le (FieldAnn, Ty)
t_operator Parser' le FieldAnn
fp = do
  Maybe ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)]))
whole <- Parser le (Maybe ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)])))
-> Parser
     le (Maybe ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)])))
forall le a. Parser le a -> Parser le a
parens do
    ReaderT
  le
  (Parsec CustomParserException Text)
  ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)]))
-> Parser'
     le (Maybe ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)])))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional do
      (FieldAnn, Ty)
ty   <- Parser' le (FieldAnn, Ty)
forall le. Parser le (FieldAnn, Ty)
field
      Maybe (Bool, [(FieldAnn, Ty)])
rest <- ReaderT
  le (Parsec CustomParserException Text) (Bool, [(FieldAnn, Ty)])
-> ReaderT
     le
     (Parsec CustomParserException Text)
     (Maybe (Bool, [(FieldAnn, Ty)]))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional do
        Bool
isOr <- (Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' Text
"|" Parser' le ()
-> ReaderT le (Parsec CustomParserException Text) Bool
-> ReaderT le (Parsec CustomParserException Text) Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ReaderT le (Parsec CustomParserException Text) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
            ReaderT le (Parsec CustomParserException Text) Bool
-> ReaderT le (Parsec CustomParserException Text) Bool
-> ReaderT le (Parsec CustomParserException Text) Bool
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' Text
"," Parser' le ()
-> ReaderT le (Parsec CustomParserException Text) Bool
-> ReaderT le (Parsec CustomParserException Text) Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ReaderT le (Parsec CustomParserException Text) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
        [(FieldAnn, Ty)]
others <- Parser' le (FieldAnn, Ty)
forall le. Parser le (FieldAnn, Ty)
field Parser' le (FieldAnn, Ty)
-> Parser' le ()
-> ReaderT le (Parsec CustomParserException Text) [(FieldAnn, Ty)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' if Bool
isOr then Text
"|" else Text
","
        return (Bool
isOr, [(FieldAnn, Ty)]
others)
      return ((FieldAnn, Ty)
ty, Maybe (Bool, [(FieldAnn, Ty)])
rest)

  (FieldAnn
f, TypeAnn
t) <- Parser le FieldAnn -> Parser le (FieldAnn, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le FieldAnn
Parser le FieldAnn
fp
  case Maybe ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)]))
whole of
    Just ((FieldAnn, Ty)
ty, Just (Bool
isOr, [(FieldAnn, Ty)]
tys)) -> do
      Parser' le (le :~: LetEnv)
forall le. Parser le (le :~: LetEnv)
assertLetEnv
      let (FieldAnn
f', Ty T
ty' TypeAnn
_) = (Natural -> (FieldAnn, Ty) -> (FieldAnn, Ty) -> (FieldAnn, Ty))
-> NonEmpty (FieldAnn, Ty) -> (FieldAnn, Ty)
forall a. (Natural -> a -> a -> a) -> NonEmpty a -> a
mkGenericTree (Bool
-> Natural -> (FieldAnn, Ty) -> (FieldAnn, Ty) -> (FieldAnn, Ty)
forall k p (a :: k).
Bool -> p -> (FieldAnn, Ty) -> (FieldAnn, Ty) -> (Annotation a, Ty)
mergeTwo Bool
isOr) ((FieldAnn, Ty)
ty (FieldAnn, Ty) -> [(FieldAnn, Ty)] -> NonEmpty (FieldAnn, Ty)
forall a. a -> [a] -> NonEmpty a
:| [(FieldAnn, Ty)]
tys)
      FieldAnn
f'' <- FieldAnn -> FieldAnn -> Parser' le FieldAnn
forall a (m :: * -> *) s.
(Default a, MonadParsec CustomParserException s m, Eq a) =>
a -> a -> m a
mergeAnnots FieldAnn
f FieldAnn
f'
      return (FieldAnn
f'', T -> TypeAnn -> Ty
Ty T
ty' TypeAnn
t)
    Just ((FieldAnn, Ty)
res, Maybe (Bool, [(FieldAnn, Ty)])
_) -> do
      (FieldAnn, Ty) -> Parser' le (FieldAnn, Ty)
forall (m :: * -> *) a. Monad m => a -> m a
return (FieldAnn, Ty)
res
    Maybe ((FieldAnn, Ty), Maybe (Bool, [(FieldAnn, Ty)]))
Nothing -> do
      Parser' le (le :~: LetEnv)
forall le. Parser le (le :~: LetEnv)
assertLetEnv
      return (FieldAnn
f, T -> TypeAnn -> Ty
Ty T
TUnit TypeAnn
t)
  where
    mergeTwo :: Bool -> p -> (FieldAnn, Ty) -> (FieldAnn, Ty) -> (Annotation a, Ty)
mergeTwo Bool
isOr p
_ (FieldAnn
l, Ty
a) (FieldAnn
r, Ty
b) =
      (Annotation a
forall k (a :: k). Annotation a
noAnn, T -> TypeAnn -> Ty
Ty ((if Bool
isOr then FieldAnn -> FieldAnn -> Ty -> Ty -> T
TOr FieldAnn
l FieldAnn
r else FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
TPair FieldAnn
l FieldAnn
r VarAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn) Ty
a Ty
b) TypeAnn
forall k (a :: k). Annotation a
noAnn)

    mergeAnnots :: a -> a -> m a
mergeAnnots a
l a
r
      | a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Default a => a
def  = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
      | a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Default a => a
def  = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
l
      | Bool
otherwise = CustomParserException -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure CustomParserException
ExcessFieldAnnotation

typeInner
  :: Parser le FieldAnn -> Parser le (FieldAnn, Ty)
typeInner :: Parser le FieldAnn -> Parser le (FieldAnn, Ty)
typeInner Parser le FieldAnn
fp = String
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type" (ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
 -> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty))
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a b. (a -> b) -> a -> b
$ [ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)]
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)]
 -> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty))
-> [ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)]
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a b. (a -> b) -> a -> b
$ (\Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
x -> Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
x Parser' le FieldAnn
Parser le FieldAnn
fp) ((Parser' le FieldAnn
  -> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty))
 -> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty))
-> [Parser' le FieldAnn
    -> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)]
-> [ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  [ Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall le. Parser' le FieldAnn -> Parser le (FieldAnn, Ty)
t_operator
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_int, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_nat, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_string, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_bytes, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_mutez, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_bool
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_keyhash, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_timestamp, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_address
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_key, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_unit, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_never, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_signature, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_chain_id
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_bls12381fr, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_bls12381g1, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_bls12381g2
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_option, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_list, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_set
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_operation, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_contract, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_ticket, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_pair, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_or
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_lambda, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_map, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_big_map, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_view
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_void, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall le fp. Default fp => Parser' le fp -> Parser le (fp, Ty)
t_letType'
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_chestKey, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_chest
  , Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_saplingState, Parser' le FieldAnn
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall a le. Default a => Parser' le a -> Parser le (a, Ty)
t_saplingTransaction
  ]
  where
    t_letType' :: forall le fp. Default fp => Parser' le fp -> Parser le (fp, Ty)
    t_letType' :: Parser' le fp -> Parser le (fp, Ty)
t_letType' = case HasLetEnv le => Maybe (le :~: LetEnv)
forall a. HasLetEnv a => Maybe (a :~: LetEnv)
isLetEnv @le of
      Just le :~: LetEnv
Refl -> Parser' le fp -> Parser' le (fp, Ty)
forall fp.
Default fp =>
Parser' LetEnv fp -> Parser' LetEnv (fp, Ty)
t_letType
      Maybe (le :~: LetEnv)
Nothing -> Parser' le (fp, Ty) -> Parser' le fp -> Parser' le (fp, Ty)
forall a b. a -> b -> a
const Parser' le (fp, Ty)
forall (m :: * -> *) a. MonadPlus m => m a
mzero

----------------------------------------------------------------------------
-- Non-comparable types
----------------------------------------------------------------------------

mkType :: T -> (a, TypeAnn) -> (a, Ty)
mkType :: T -> (a, TypeAnn) -> (a, Ty)
mkType T
t (a
a, TypeAnn
ta) = (a
a, T -> TypeAnn -> Ty
Ty T
t TypeAnn
ta)


t_int :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_int :: Parser' le a -> Parser le (a, Ty)
t_int Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Int" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TInt) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_nat :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_nat :: Parser' le a -> Parser le (a, Ty)
t_nat Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Nat" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TNat) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_string :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_string :: Parser' le a -> Parser le (a, Ty)
t_string Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"String" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TString) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_bytes :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_bytes :: Parser' le a -> Parser le (a, Ty)
t_bytes Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Bytes" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TBytes) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_mutez :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_mutez :: Parser' le a -> Parser le (a, Ty)
t_mutez Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Mutez" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TMutez) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_bool :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_bool :: Parser' le a -> Parser le (a, Ty)
t_bool Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Bool" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TBool) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_keyhash :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_keyhash :: Parser' le a -> Parser le (a, Ty)
t_keyhash Parser' le a
fp = ((Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"KeyHash" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TKeyHash)) Parser' le ((a, TypeAnn) -> (a, Ty))
-> Parser' le ((a, TypeAnn) -> (a, Ty))
-> Parser' le ((a, TypeAnn) -> (a, Ty))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word Tokens Text
"key_hash" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TKeyHash))) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_timestamp :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_timestamp :: Parser' le a -> Parser le (a, Ty)
t_timestamp Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Timestamp" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TTimestamp) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_address :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_address :: Parser' le a -> Parser le (a, Ty)
t_address Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Address" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TAddress) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_key :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_key :: Parser' le a -> Parser le (a, Ty)
t_key Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Key" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TKey) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_signature :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_signature :: Parser' le a -> Parser le (a, Ty)
t_signature Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Signature" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TSignature) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_bls12381fr :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_bls12381fr :: Parser' le a -> Parser le (a, Ty)
t_bls12381fr Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"bls12_381_fr" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Bls12381Fr"
  T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TBls12381Fr ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> Parser' le (a, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_bls12381g1 :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_bls12381g1 :: Parser' le a -> Parser le (a, Ty)
t_bls12381g1 Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"bls12_381_g1" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Bls12381G1"
  T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TBls12381G1 ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> Parser' le (a, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_bls12381g2 :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_bls12381g2 :: Parser' le a -> Parser le (a, Ty)
t_bls12381g2 Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"bls12_381_g2" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Bls12381G2"
  T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TBls12381G2 ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> Parser' le (a, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_chestKey :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_chestKey :: Parser' le a -> Parser le (a, Ty)
t_chestKey Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' Text
"ChestKey" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' Text
"chest_key"
  T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TChestKey ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> Parser' le (a, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_chest :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_chest :: Parser' le a -> Parser le (a, Ty)
t_chest Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Chest" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TChest) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_chain_id :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_chain_id :: Parser' le a -> Parser le (a, Ty)
t_chain_id Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"ChainId" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"chain_id"
  T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TChainId ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> Parser' le (a, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_operation :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_operation :: Parser' le a -> Parser le (a, Ty)
t_operation Parser' le a
fp = Tokens Text
-> ((a, TypeAnn) -> (a, Ty)) -> Parser le ((a, TypeAnn) -> (a, Ty))
forall a le. Tokens Text -> a -> Parser le a
word' Tokens Text
"Operation" (T -> (a, TypeAnn) -> (a, Ty)
forall a. T -> (a, TypeAnn) -> (a, Ty)
mkType T
TOperation) Parser' le ((a, TypeAnn) -> (a, Ty))
-> ReaderT le (Parsec CustomParserException Text) (a, TypeAnn)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp

t_contract :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_contract :: Parser' le a -> Parser le (a, Ty)
t_contract Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Contract"
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
  return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TContract Ty
a) TypeAnn
t)

t_ticket :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_ticket :: Parser' le a -> Parser le (a, Ty)
t_ticket Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Ticket"
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
  return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TTicket Ty
a) TypeAnn
t)

-- | Parses a @unit@ type. Unit type admits two variants of syntax, @unit@ and @()@. This parser
-- handles only the former, the latter is handled in 't_operator'
t_unit :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_unit :: Parser' le a -> Parser le (a, Ty)
t_unit Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Unit"
  (a
f,TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  return (a
f, T -> TypeAnn -> Ty
Ty T
TUnit TypeAnn
t)

t_never :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_never :: Parser' le a -> Parser le (a, Ty)
t_never Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Never" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"⊥"
  (a
f,TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  return (a
f, T -> TypeAnn -> Ty
Ty T
TNever TypeAnn
t)

t_pair :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_pair :: Parser' le a -> Parser le (a, Ty)
t_pair Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Pair"
  (a
fieldAnn, TypeAnn
typeAnn) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  [(FieldAnn, Ty)]
fields <- ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
-> ReaderT le (Parsec CustomParserException Text) [(FieldAnn, Ty)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
forall le. Parser le (FieldAnn, Ty)
field
  T
tPair <- [(FieldAnn, Ty)] -> Parser le T
forall le. [(FieldAnn, Ty)] -> Parser le T
go [(FieldAnn, Ty)]
fields
  pure $ (a
fieldAnn, T -> TypeAnn -> Ty
Ty T
tPair TypeAnn
typeAnn)
  where
    go :: [(FieldAnn, Ty)] -> Parser le T
    go :: [(FieldAnn, Ty)] -> Parser le T
go = \case
      [] -> String -> Parser' le T
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The 'pair' type expects at least 2 type arguments, but 0 were given."
      [(FieldAnn
_, Ty
t)] -> String -> Parser' le T
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser' le T) -> String -> Parser' le T
forall a b. (a -> b) -> a -> b
$ String
"The 'pair' type expects at least 2 type arguments, but only 1 was given: '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Ty -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty Ty
t String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'."
      [(FieldAnn
fieldAnnL, Ty
typeL), (FieldAnn
fieldAnnR, Ty
typeR)] ->
        T -> Parser' le T
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> Parser' le T) -> T -> Parser' le T
forall a b. (a -> b) -> a -> b
$ FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
TPair FieldAnn
fieldAnnL FieldAnn
fieldAnnR VarAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn Ty
typeL Ty
typeR
      (FieldAnn
fieldAnnL, Ty
typeL) : [(FieldAnn, Ty)]
fields -> do
        T
rightCombedT <- [(FieldAnn, Ty)] -> Parser le T
forall le. [(FieldAnn, Ty)] -> Parser le T
go [(FieldAnn, Ty)]
fields
        pure $ FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
TPair FieldAnn
fieldAnnL FieldAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn Ty
typeL (T -> TypeAnn -> Ty
Ty T
rightCombedT TypeAnn
forall k (a :: k). Annotation a
noAnn)

t_or :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_or :: Parser' le a -> Parser le (a, Ty)
t_or Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Or"
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  (FieldAnn
l, Ty
a) <- Parser' le (FieldAnn, Ty)
forall le. Parser le (FieldAnn, Ty)
field
  (FieldAnn
r, Ty
b) <- Parser' le (FieldAnn, Ty)
forall le. Parser le (FieldAnn, Ty)
field
  return (a
f, T -> TypeAnn -> Ty
Ty (FieldAnn -> FieldAnn -> Ty -> Ty -> T
TOr FieldAnn
l FieldAnn
r Ty
a Ty
b) TypeAnn
t)

t_option :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_option :: Parser' le a -> Parser le (a, Ty)
t_option Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Option"
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  Ty
a <- (FieldAnn, Ty) -> Ty
forall a b. (a, b) -> b
snd ((FieldAnn, Ty) -> Ty)
-> ReaderT le (Parsec CustomParserException Text) (FieldAnn, Ty)
-> ReaderT le (Parsec CustomParserException Text) Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser le FieldAnn -> Parser le (FieldAnn, Ty)
forall le. Parser le FieldAnn -> Parser le (FieldAnn, Ty)
typeInner (FieldAnn -> ReaderT le (Parsec CustomParserException Text) FieldAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure FieldAnn
forall k (a :: k). Annotation a
noAnn)
  return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TOption Ty
a) TypeAnn
t)

t_saplingState :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_saplingState :: Parser' le a -> Parser le (a, Ty)
t_saplingState Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Sapling_state"
  (a
f,TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  Natural
n <- Parser le Natural -> Parser le Natural
forall le a. Parser le a -> Parser le a
lexeme Parser le Natural
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal
  return (a
f, T -> TypeAnn -> Ty
Ty (Natural -> T
TSaplingState Natural
n) TypeAnn
t)

t_saplingTransaction :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_saplingTransaction :: Parser' le a -> Parser le (a, Ty)
t_saplingTransaction Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Sapling_transaction"
  (a
f,TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  Natural
n <- Parser le Natural -> Parser le Natural
forall le a. Parser le a -> Parser le a
lexeme Parser le Natural
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal
  return (a
f, T -> TypeAnn -> Ty
Ty (Natural -> T
TSaplingTransaction Natural
n) TypeAnn
t)

t_lambda :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_lambda :: Parser' le a -> Parser le (a, Ty)
t_lambda Parser' le a
fp = ReaderT le (Parsec CustomParserException Text) (a, Ty)
core ReaderT le (Parsec CustomParserException Text) (a, Ty)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT le (Parsec CustomParserException Text) (a, Ty)
slashLambda
  where
    core :: ReaderT le (Parsec CustomParserException Text) (a, Ty)
core = do
      Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Lambda"
      (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
      Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
      Ty
b <- Parser' le Ty
forall le. Parser le Ty
type_
      return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> Ty -> T
TLambda Ty
a Ty
b) TypeAnn
t)
    slashLambda :: ReaderT le (Parsec CustomParserException Text) (a, Ty)
slashLambda = do
      Tokens Text -> Parser le ()
forall le. Tokens Text -> Parser le ()
symbol Tokens Text
"\\"
      (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
      Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
      Tokens Text -> Parser le ()
forall le. Tokens Text -> Parser le ()
symbol Tokens Text
"->"
      Parser' le (le :~: LetEnv)
forall le. Parser le (le :~: LetEnv)
assertLetEnv
      Ty
b <- Parser' le Ty
forall le. Parser le Ty
type_
      return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> Ty -> T
TLambda Ty
a Ty
b) TypeAnn
t)

-- Container types
t_list :: forall a le. (Default a) => Parser' le a -> Parser le (a, Ty)
t_list :: Parser' le a -> Parser le (a, Ty)
t_list Parser' le a
fp = ReaderT le (Parsec CustomParserException Text) (a, Ty)
core ReaderT le (Parsec CustomParserException Text) (a, Ty)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT le (Parsec CustomParserException Text) (a, Ty)
Parser le (a, Ty)
bracketList
  where
    core :: ReaderT le (Parsec CustomParserException Text) (a, Ty)
core = do
      Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"List"
      (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
      Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
      return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TList Ty
a) TypeAnn
t)
    bracketList :: Parser le (a, Ty)
    bracketList :: ReaderT le (Parsec CustomParserException Text) (a, Ty)
bracketList = do
      Ty
a <- Parser le Ty -> Parser le Ty
forall le a. Parser le a -> Parser le a
brackets Parser le Ty
forall le. Parser le Ty
type_
      Parser' le (le :~: LetEnv)
forall le. Parser le (le :~: LetEnv)
assertLetEnv
      (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
      return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TList Ty
a) TypeAnn
t)

t_set :: forall a le. (Default a) => Parser' le a -> Parser le (a, Ty)
t_set :: Parser' le a -> Parser le (a, Ty)
t_set Parser' le a
fp = ReaderT le (Parsec CustomParserException Text) (a, Ty)
core ReaderT le (Parsec CustomParserException Text) (a, Ty)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
-> ReaderT le (Parsec CustomParserException Text) (a, Ty)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT le (Parsec CustomParserException Text) (a, Ty)
Parser le (a, Ty)
braceSet
  where
    core :: ReaderT le (Parsec CustomParserException Text) (a, Ty)
core = do
      Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Set"
      (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
      Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
      return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TSet Ty
a) TypeAnn
t)
    braceSet :: Parser le (a, Ty)
    braceSet :: ReaderT le (Parsec CustomParserException Text) (a, Ty)
braceSet = do
      Ty
a <- Parser le Ty -> Parser le Ty
forall le a. Parser le a -> Parser le a
braces Parser le Ty
forall le. Parser le Ty
type_
      Parser' le (le :~: LetEnv)
forall le. Parser le (le :~: LetEnv)
assertLetEnv
      (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
      return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> T
TSet Ty
a) TypeAnn
t)

t_map_like
  :: (Default a)
  => Parser' le a -> Parser le (Ty, Ty, a, TypeAnn)
t_map_like :: Parser' le a -> Parser le (Ty, Ty, a, TypeAnn)
t_map_like Parser' le a
fp = do
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
  Ty
b <- Parser' le Ty
forall le. Parser le Ty
type_
  return (Ty
a, Ty
b, a
f, TypeAnn
t)

t_map :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_map :: Parser' le a -> Parser le (a, Ty)
t_map Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"Map"
  (Ty
a, Ty
b, a
f, TypeAnn
t) <- Parser' le a -> Parser le (Ty, Ty, a, TypeAnn)
forall a le.
Default a =>
Parser' le a -> Parser le (Ty, Ty, a, TypeAnn)
t_map_like Parser' le a
fp
  return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> Ty -> T
TMap Ty
a Ty
b) TypeAnn
t)

t_big_map :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_big_map :: Parser' le a -> Parser le (a, Ty)
t_big_map Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol1' Text
"BigMap" Parser' le () -> Parser' le () -> Parser' le ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> Parser le ()
forall le. Tokens Text -> Parser le ()
symbol1 Tokens Text
"big_map"
  (Ty
a, Ty
b, a
f, TypeAnn
t) <- Parser' le a -> Parser le (Ty, Ty, a, TypeAnn)
forall a le.
Default a =>
Parser' le a -> Parser le (Ty, Ty, a, TypeAnn)
t_map_like Parser' le a
fp
  return (a
f, T -> TypeAnn -> Ty
Ty (Ty -> Ty -> T
TBigMap Ty
a Ty
b) TypeAnn
t)

----------------------------------------------------------------------------
-- Non-standard types (Morley extensions)
----------------------------------------------------------------------------

t_view :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_view :: Parser' le a -> Parser le (a, Ty)
t_view Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' Text
"View"
  Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
  Ty
r <- Parser' le Ty
forall le. Parser le Ty
type_
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  let c' :: Ty
c' = T -> TypeAnn -> Ty
Ty (Ty -> T
TContract Ty
r) TypeAnn
forall k (a :: k). Annotation a
noAnn
  return (a
f, T -> TypeAnn -> Ty
Ty (FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
TPair FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn Ty
a Ty
c') TypeAnn
t)

t_void :: (Default a) => Parser' le a -> Parser le (a, Ty)
t_void :: Parser' le a -> Parser le (a, Ty)
t_void Parser' le a
fp = do
  Text -> Parser le ()
forall le. Text -> Parser le ()
symbol' Text
"Void"
  Ty
a <- Parser' le Ty
forall le. Parser le Ty
type_
  Ty
b <- Parser' le Ty
forall le. Parser le Ty
type_
  (a
f, TypeAnn
t) <- Parser le a -> Parser le (a, TypeAnn)
forall a le. Default a => Parser le a -> Parser le (a, TypeAnn)
fieldType Parser' le a
Parser le a
fp
  let c :: Ty
c = T -> TypeAnn -> Ty
Ty (Ty -> Ty -> T
TLambda Ty
b Ty
b) TypeAnn
forall k (a :: k). Annotation a
noAnn
  return (a
f, T -> TypeAnn -> Ty
Ty (FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
TPair FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn VarAnn
forall k (a :: k). Annotation a
noAnn Ty
a Ty
c) TypeAnn
t)

t_letType :: (Default fp) => Parser' LetEnv fp -> Parser' LetEnv (fp, Ty)
t_letType :: Parser' LetEnv fp -> Parser' LetEnv (fp, Ty)
t_letType Parser' LetEnv fp
fp = do
  Map Text LetType
lts <- (LetEnv -> Map Text LetType)
-> ReaderT
     LetEnv (Parsec CustomParserException Text) (Map Text LetType)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks LetEnv -> Map Text LetType
letTypes
  Ty
lt <- LetType -> Ty
ltSig (LetType -> Ty)
-> ReaderT LetEnv (Parsec CustomParserException Text) LetType
-> ReaderT LetEnv (Parsec CustomParserException Text) Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map Text LetType -> Parser LetEnv LetType
forall le. Map Text LetType -> Parser le LetType
mkLetType Map Text LetType
lts)
  fp
f <- Parser LetEnv fp -> Parser LetEnv fp
forall a le. Default a => Parser le a -> Parser le a
parseDef Parser' LetEnv fp
Parser LetEnv fp
fp
  return (fp
f, Ty
lt)

mkLetType :: Map Text LetType -> Parser le LetType
mkLetType :: Map Text LetType -> Parser le LetType
mkLetType Map Text LetType
lts = [ReaderT le (Parsec CustomParserException Text) LetType]
-> ReaderT le (Parsec CustomParserException Text) LetType
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([ReaderT le (Parsec CustomParserException Text) LetType]
 -> ReaderT le (Parsec CustomParserException Text) LetType)
-> [ReaderT le (Parsec CustomParserException Text) LetType]
-> ReaderT le (Parsec CustomParserException Text) LetType
forall a b. (a -> b) -> a -> b
$ (LetType -> Text) -> LetType -> Parser le LetType
forall a le. (a -> Text) -> a -> Parser le a
mkParser LetType -> Text
ltName (LetType -> ReaderT le (Parsec CustomParserException Text) LetType)
-> [LetType]
-> [ReaderT le (Parsec CustomParserException Text) LetType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map Text LetType -> [LetType]
forall k a. Map k a -> [a]
Map.elems Map Text LetType
lts)