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