src/Symantic/Parser.hs

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