src/Symantic/Parser.hs

   1 {-# LANGUAGE RankNTypes #-}
   2 {-# OPTIONS_GHC -Wno-partial-fields #-}
   3
   4 module Symantic.Parser where
   5
   6 import Data.Either (Either (..))
   7 import Data.Eq (Eq (..))
   8 import Data.Function (($))
   9 import Data.Semigroup (Semigroup (..))
  10 import Data.String (String)
  11 import Data.Void (Void)
  12 import GHC.Types
  13 import Text.Read (Read (..), reads)
  14 import Text.Show (Show (..))
  15
  16 import Symantic.Compiler
  17 import Symantic.Semantics (PerSyntax)
  18 import Symantic.Typer
  19
  20 -- * Type 'Parser'
  21 data Parser syns meta = Parser
  22   { unParser ::
  23       ( -- MT.State (TokenTerm meta a)
  24         forall vs.
  25         CtxTy meta vs Void ->
  26         Either (PerSyntax syns (ErrorParser meta)) (TermVT syns meta vs)
  27       )
  28   }
  29 type ErrMsg = String
  30
  31 -- * Data family 'ErrorParser'
  32 data family ErrorParser meta (syn :: Syntax)
  33
  34 ---- * Type 'SomeParsingError'
  35 -- data SomeParsingError
  36 --  = forall syn.
  37 --    (
  38 --    -- Derivable (SomeParsingError syn sem),
  39 --    Typeable syn
  40 --    ) =>
  41 --    SomeParsingError (SomeParsingError syn)
  42 --
  43 ----type instance Derived (SomeParsingError sem) = sem
  44 ----instance Derivable (SomeParsingError sem) where
  45 ----  derive (SomeParsingError x) = derive x
  46 --
  47 ---- ** Type 'SomeParsingError'
  48 --
  49 ---- TODO: neither data families nor data instances
  50 ---- can have phantom roles with GHC-9's RoleAnnotations,
  51 ---- hence 'SomeParsingError.Coerce.coerce' cannot be used on them for now.
  52 ---- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
  53 ---- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
  54 -- data family SomeParsingError (syn :: Syntax) :: Semantic -> Semantic
  55 ----type instance Derived (SomeParsingError syn sem) = sem
  56 --
  57 ---- | Convenient utility to pattern-match a 'SomeParsingError'.
  58 ----pattern SomeParsingError :: Typeable syn => SomeParsingError syn sem a -> SomeParsingError sem a
  59 ----pattern SomeParsingError x <- (unSomeParsingError -> Maybe.Just x)
  60 --
  61 ---- | @(unSomeParsingError sd :: 'Maybe' ('SomeParsingError' syn sem a))@
  62 ---- extract the data-constructor from the given 'SomeParsingError' @(sd)@
  63 ---- iif. it belongs to the @('SomeParsingError' syn sem a)@ data-instance.
  64 -- unSomeParsingError ::
  65 --  forall syn sem a.
  66 --  Typeable syn =>
  67 --  SomeParsingError sem a ->
  68 --  Maybe (SomeParsingError syn sem a)
  69 -- unSomeParsingError (SomeParsingError (constr :: SomeParsingError actualSyn sem a)) =
  70 --  case typeRep @syn `eqTypeRep` typeRep @actualSyn of
  71 --    Maybe.Just HRefl -> Maybe.Just constr
  72 --    Maybe.Nothing -> Maybe.Nothing
  73
  74 data TermVT syns meta vs = forall a vs'.
  75   TermVT
  76   { termVTType :: Ty meta vs' a
  77   , unTermVT :: OpenTerm syns vs a
  78   }
  79
  80 -- * Type 'BinTree'
  81
  82 -- | /Binary Tree/.
  83 data BinTree a
  84   = BinTree0 a
  85   | BinTree2 (BinTree a) (BinTree a)
  86   deriving (Eq, Show)
  87
  88 type TermAST meta = BinTree (TokenTerm meta)
  89 data TokenTerm meta
  90   = TokenTermAbst String (TyT meta '[]) (TermAST meta)
  91   | TokenTermVar Name
  92   | TokenTermAtom String
  93   deriving (Show)
  94
  95 safeRead :: Read a => String -> Either ErrMsg a
  96 safeRead s = case reads s of
  97   [(x, "")] -> Right x
  98   _ -> Left $ "Read error: " <> s
  99
 100 {-
 101 instance ( forall sem. syns sem => Functor sem
 102          ) => Functor (Parser syns) where
 103   fmap f (Parser esa) = Parser $
 104     case esa of
 105       Left e -> Left e
 106       Right (Sem sem) -> Right (Sem (f <$> sem))
 107   a <$ Parser esa = Parser $
 108     case esa of
 109       Left e -> Left e
 110       Right (Sem sem) -> Right (Sem (a <$ sem))
 111 instance ( forall sem. syns sem => Applicative sem
 112          , Applicative (Sem syns)
 113          , forall err. syns (Either err)
 114          , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
 115          ) => Applicative (Parser syns) where
 116   pure a = Parser (Right (Sem (pure a)))
 117   liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
 118   (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
 119   (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
 120   (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
 121 instance ( forall sem. syns sem => Monad sem
 122          , forall err. syns (Either err)
 123          , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
 124          ) => Monad (Parser syns) where
 125   (>>=) (Parser efsa) f = Parser (efsa >>= \(Sem sa) -> sa >>= unParser . f)
 126 -}
 127
 128 -- * Type 'CtxTy'
 129
 130 -- | /Typing context/
 131 -- accumulating at each /lambda abstraction/
 132 -- the 'Type' of the introduced variable.
 133 -- It is built top-down from the closest
 134 -- including /lambda abstraction/ to the farest.
 135 -- It determines the 'Type's of 'CtxTe'.
 136 data CtxTy meta (as :: [Type]) void where
 137   CtxTyZ :: CtxTy meta '[] Void
 138   CtxTyS :: NameTe -> Ty meta '[] a -> CtxTy meta as Void -> CtxTy meta (a ': as) Void
 139
 140 infixr 5 `CtxTyS`
 141
 142 instance LenVar CtxTy where
 143   lenVar CtxTyZ = LenZ
 144   lenVar (CtxTyS _n _ty x) = LenS (lenVar x)
 145
 146 type NameTe = String