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 prov = Parser
  22   { unParser ::
  23       ( -- MT.State (TokenTerm prov a)
  24         forall vs.
  25         CtxTy prov vs Void ->
  26         Either (PerSyntax syns (ErrorParser prov)) (TermVT syns prov vs)
  27       )
  28   }
  29 type ErrMsg = String
  30
  31 -- * Data family 'ErrorParser'
  32 data family ErrorParser prov (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 prov vs = forall a vs'.
  75   TermVT
  76   { termVTType :: Ty prov 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'
  89 type TermAST prov = BinTree (TokenTerm prov)
  90
  91 -- * Type 'TokenTerm'
  92 data TokenTerm prov
  93   = TokenTermAbst String (TyT prov '[]) (TermAST prov)
  94   | TokenTermVar Name
  95   | TokenTermAtom String
  96   deriving (Show)
  97
  98 safeRead :: Read a => String -> Either ErrMsg a
  99 safeRead s = case reads s of
 100   [(x, "")] -> Right x
 101   _ -> Left $ "Read error: " <> s
 102
 103 {-
 104 instance ( forall sem. syns sem => Functor sem
 105          ) => Functor (Parser syns) where
 106   fmap f (Parser esa) = Parser $
 107     case esa of
 108       Left e -> Left e
 109       Right (Sem sem) -> Right (Sem (f <$> sem))
 110   a <$ Parser esa = Parser $
 111     case esa of
 112       Left e -> Left e
 113       Right (Sem sem) -> Right (Sem (a <$ sem))
 114 instance ( forall sem. syns sem => Applicative sem
 115          , Applicative (Sem syns)
 116          , forall err. syns (Either err)
 117          , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
 118          ) => Applicative (Parser syns) where
 119   pure a = Parser (Right (Sem (pure a)))
 120   liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
 121   (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
 122   (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
 123   (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
 124 instance ( forall sem. syns sem => Monad sem
 125          , forall err. syns (Either err)
 126          , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
 127          ) => Monad (Parser syns) where
 128   (>>=) (Parser efsa) f = Parser (efsa >>= \(Sem sa) -> sa >>= unParser . f)
 129 -}
 130
 131 -- * Type 'CtxTy'
 132
 133 -- | /Typing context/
 134 -- accumulating at each /lambda abstraction/
 135 -- the 'Type' of the introduced variable.
 136 -- It is built top-down from the closest
 137 -- including /lambda abstraction/ to the farest.
 138 -- It determines the 'Type's of 'CtxTe'.
 139 data CtxTy prov (as :: [Type]) void where
 140   CtxTyZ :: CtxTy prov '[] Void
 141   CtxTyS :: NameTe -> Ty prov '[] a -> CtxTy prov as Void -> CtxTy prov (a ': as) Void
 142
 143 infixr 5 `CtxTyS`
 144
 145 instance LenVar CtxTy where
 146   lenVar CtxTyZ = LenZ
 147   lenVar (CtxTyS _n _ty x) = LenS (lenVar x)
 148
 149 type NameTe = String