src/Symantic/Parser.hs

   1 {-# LANGUAGE RankNTypes #-}
   2
   3 module Symantic.Parser where
   4
   5 import Control.Applicative (Applicative (..))
   6 import Control.Monad (Monad (..))
   7 import Control.Monad.Trans.Except qualified as MT
   8 import Control.Monad.Trans.Reader qualified as MT
   9 import Control.Monad.Trans.State qualified as MT
  10 import Data.Bool (otherwise)
  11 import Data.Either (Either (..))
  12 import Data.Eq (Eq (..))
  13 import Data.Function (id, ($), (.))
  14 import Data.Functor (Functor (..), (<$>))
  15 import Data.Functor.Constant (Constant (..))
  16 import Data.Int (Int)
  17 import Data.Kind (Constraint, Type)
  18 import Data.Maybe (Maybe (..), isJust)
  19 import Data.Proxy (Proxy (..))
  20 import Data.Semigroup (Semigroup (..))
  21 import Data.String (String)
  22 import Data.Void (Void)
  23 import GHC.Types
  24 import Text.Read (Read (..), reads)
  25 import Text.Show (Show (..))
  26 import Unsafe.Coerce (unsafeCoerce)
  27 import Prelude (error)
  28 import Prelude qualified
  29
  30 import Symantic.Compiler
  31 import Symantic.Typer
  32
  33 -- * Type 'Parser'
  34 data Parser syn meta = Parser
  35   { unParser ::
  36       ( -- MT.State (TokenTerm meta a)
  37         forall vs.
  38         CtxTy meta vs Void ->
  39         Either ErrMsg (TermVT syn meta vs)
  40       )
  41   }
  42 type ErrMsg = String
  43
  44 data TermVT syn meta vs = forall a vs'.
  45   TermVT
  46   { termVTType :: Ty meta vs' a
  47   , unTermVT :: OTerm syn vs a
  48   }
  49
  50 -- * Type 'BinTree'
  51
  52 -- | /Binary Tree/.
  53 data BinTree a
  54   = BinTree0 a
  55   | BinTree2 (BinTree a) (BinTree a)
  56   deriving (Eq, Show)
  57
  58 type TermAST meta = BinTree (TokenTerm meta)
  59 data TokenTerm meta
  60   = TokenTermAtom String
  61   | TokenTermVar Name
  62   | TokenTermAbst String (TyT meta '[]) (TermAST meta)
  63   deriving (Show)
  64
  65 safeRead :: Read a => String -> Either ErrMsg a
  66 safeRead s = case reads s of
  67   [(x, "")] -> Right x
  68   _ -> Left $ "Read error: " <> s
  69
  70 {-
  71 instance ( forall sem. syn sem => Functor sem
  72          ) => Functor (Parser syn) where
  73   fmap f (Parser esa) = Parser $
  74     case esa of
  75       Left e -> Left e
  76       Right (Semantics sem) -> Right (Semantics (f <$> sem))
  77   a <$ Parser esa = Parser $
  78     case esa of
  79       Left e -> Left e
  80       Right (Semantics sem) -> Right (Semantics (a <$ sem))
  81 instance ( forall sem. syn sem => Applicative sem
  82          , Applicative (Semantics syn)
  83          , forall err. syn (Either err)
  84          , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
  85          ) => Applicative (Parser syn) where
  86   pure a = Parser (Right (Semantics (pure a)))
  87   liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
  88   (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
  89   (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
  90   (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
  91 instance ( forall sem. syn sem => Monad sem
  92          , forall err. syn (Either err)
  93          , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
  94          ) => Monad (Parser syn) where
  95   (>>=) (Parser efsa) f = Parser (efsa >>= \(Semantics sa) -> sa >>= unParser . f)
  96 -}
  97
  98 -- * Type 'CtxTy'
  99
 100 -- | /Typing context/
 101 -- accumulating at each /lambda abstraction/
 102 -- the 'Type' of the introduced variable.
 103 -- It is built top-down from the closest
 104 -- including /lambda abstraction/ to the farest.
 105 -- It determines the 'Type's of 'CtxTe'.
 106 data CtxTy meta (as :: [Type]) void where
 107   CtxTyZ :: CtxTy meta '[] Void
 108   CtxTyS :: NameTe -> Ty meta '[] a -> CtxTy meta as Void -> CtxTy meta (a ': as) Void
 109
 110 infixr 5 `CtxTyS`
 111
 112 instance LenVar CtxTy where
 113   lenVar CtxTyZ = LenZ
 114   lenVar (CtxTyS _n _ty x) = LenS (lenVar x)
 115
 116 type NameTe = String