commit 1816e42deb15b5e96fa68e235f2acdbb9d70b32a
parent 909a7e64900d98cceb0f591e721cc2c1a09a1261
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 28 Aug 2024 23:02:54 -0700
Add Parser, and get it all working on Church nat example
Diffstat:
| M | Main.hs | | | 84 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++------------------ |
| A | Parser.hs | | | 172 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
2 files changed, 237 insertions(+), 19 deletions(-)
diff --git a/Main.hs b/Main.hs
@@ -2,16 +2,20 @@ module Main where
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
+import Data.ByteString (ByteString)
+import Sparsec
import Algebra
import Ledger (Ledger)
import qualified Ledger as L
import Common
+import qualified Environment as Env
import Context (Ctx)
import qualified Context as Ctx
import qualified Surface as S
import qualified Core as C
import qualified Value as V
+import qualified Parser as P
--------------------------------------------------------------------------------
-- Util
@@ -32,9 +36,31 @@ data BothCtx q = BothCtx {
termCtx :: TermCtx q
}
-data Err = Err -- TODO
-
-type Elab q a = ReaderT (BothCtx q) (Except Err) a
+bothCtxEmpty :: BothCtx q
+bothCtxEmpty = BothCtx Ctx.empty Ctx.empty
+
+data Err
+ = ErrTypeInferCheckMismatch
+ | ErrTypeVarUnbound
+ | ErrTypeArrowAbsNotInferable
+ | ErrTypeArrowAppNotArrow
+ | ErrTermInferCheckMismatch
+ | ErrTermVarUnbound
+ | ErrTermArrowAbsNotInferable
+ | ErrTermArrowAbsQuantityMismatch
+ | ErrTermArrowAbsNotArrow
+ | ErrTermArrowAppQuantityMismatch
+ | ErrTermArrowAppNotArrow
+ | ErrTermForallAbsNotInferable
+ | ErrTermForallAbsNotForall
+ | ErrTermForallAppQuantityMismatch
+ | ErrTermForallAppNotForall
+ deriving Show
+
+type Elab q a = ReaderT (BothCtx q) (Either Err) a
+
+runElab :: Elab q a -> BothCtx q -> Either Err a
+runElab = runReaderT
--------------------------------------------------------------------------------
-- Type-level elaboration
@@ -59,7 +85,7 @@ bindAndAssignType x k f = do
local (const $ ctx { typeCtx = typeCtx' }) (f lvl)
lookupType :: QuantityAlgebra q => S.TypeName -> Elab q (V.Type q, Kind)
-lookupType x = (Ctx.lookup x 0 <$> asks (.typeCtx)) >>= (`orThrowError` Err) -- TODO
+lookupType x = (Ctx.lookup x 0 <$> asks (.typeCtx)) >>= (`orThrowError` ErrTypeVarUnbound)
inferType :: QuantityAlgebra q => S.Type q -> Elab q (C.Type q, Kind)
inferType = \case
@@ -67,33 +93,42 @@ inferType = \case
(va, k) <- lookupType x
a <- quoteType va
pure (a, k)
+
S.TypeAnnot a k -> (, k) <$> checkType a k
+
S.TypeTArrow dom cod -> do
dom' <- checkType dom KindQT
cod' <- checkType cod KindQT
pure (C.TypeTArrow dom' cod', KindT)
+
S.TypeTForall x k a -> do
a' <- bindAndAssignType x k \_ -> checkType a KindQT
pure (C.TypeTForall k a', KindT)
+
S.TypeQ q -> pure (C.TypeQ q, KindQ)
+
S.TypeQTPair q a -> do
q' <- checkType q KindQ
a' <- checkType a KindT
pure (C.TypeQTPair q' a', KindQT)
+
S.TypeQTFst qa -> do
qa' <- checkType qa KindQT
pure (C.TypeQTFst qa', KindQ)
+
S.TypeQTSnd qa -> do
qa' <- checkType qa KindQT
pure (C.TypeQTSnd qa', KindT)
- S.TypeArrowAbs _ _ -> throwError Err -- TODO
+
+ S.TypeArrowAbs _ _ -> throwError ErrTypeArrowAbsNotInferable
+
S.TypeArrowApp fun arg -> do
(fun', k) <- inferType fun
case k of
KindArrow dom cod -> do
arg' <- checkType arg dom
pure (C.TypeArrowApp fun' arg', cod)
- _ -> throwError Err -- TODO
+ _ -> throwError ErrTypeArrowAppNotArrow
checkType :: QuantityAlgebra q => S.Type q -> Kind -> Elab q (C.Type q)
checkType a k = case (a, k) of
@@ -101,7 +136,7 @@ checkType a k = case (a, k) of
bindAndAssignType x dom \_ -> checkType body cod
(a, k) -> do
(a', k') <- inferType a
- unless (k' == k) $ throwError Err -- TODO
+ unless (k' == k) $ throwError ErrTypeInferCheckMismatch
pure a'
--------------------------------------------------------------------------------
@@ -122,7 +157,7 @@ bindAndAssignTerm x a f = do
lookupTerm :: QuantityAlgebra q => S.TermName -> Elab q (V.TermLvl, V.Type q)
lookupTerm x = do
m <- Ctx.lookup x 0 <$> asks (.termCtx)
- (V.TermGeneric lvl, a) <- m `orThrowError` Err -- TODO
+ (V.TermGeneric lvl, a) <- m `orThrowError` ErrTermVarUnbound
pure (lvl, a)
termLvlToIdx :: QuantityAlgebra q => V.TermLvl -> Elab q C.TermIdx
@@ -144,18 +179,18 @@ inferTerm t q = case t of
(t', tLedger) <- checkTerm t q a''
pure (t', a'', tLedger)
- S.TermArrowAbs _ _ -> throwError Err -- TODO
+ S.TermArrowAbs _ _ -> throwError ErrTermArrowAbsNotInferable
S.TermArrowApp fun arg -> do
(fun', funType, funLedger) <- inferTerm fun one
case funType of
V.TypeTArrow dom cod -> do
(arg', argLedger) <- checkTerm arg (V.qtFst dom) (V.qtSnd dom)
- unless (V.qtFst cod `V.qGeq` q) $ throwError Err -- TODO
+ unless (V.qtFst cod `V.qGeq` q) $ throwError ErrTermArrowAppQuantityMismatch
pure (C.TermArrowApp fun' arg', V.qtSnd cod, funLedger <+> argLedger)
- _ -> throwError Err -- TODO
+ _ -> throwError ErrTermArrowAppNotArrow
- S.TermForallAbs _ _ -> throwError Err -- TODO
+ S.TermForallAbs _ _ -> throwError ErrTermForallAbsNotInferable
S.TermForallApp fun arg -> do
(fun', funType, funLedger) <- inferTerm fun one
@@ -164,9 +199,9 @@ inferTerm t q = case t of
arg' <- checkType arg k
arg'' <- evalType arg'
let qa = V.applyClosure clo arg''
- unless (V.qtFst qa `V.qGeq` q) $ throwError Err -- TODO
+ unless (V.qtFst qa `V.qGeq` q) $ throwError ErrTermForallAppQuantityMismatch
pure (C.TermForallApp fun' arg', V.qtSnd qa, funLedger)
- _ -> throwError Err -- TODO
+ _ -> throwError ErrTermForallAppNotForall
checkTerm :: QuantityAlgebra q
=> S.Term q
@@ -178,10 +213,10 @@ checkTerm t q a = case (t, a) of
bindAndAssignTerm x (V.qtSnd dom) \lvl -> do
(body', bodyLedger) <- checkTerm body (V.qtFst cod) (V.qtSnd cod)
let (domDemand, absLedger) = L.split lvl bodyLedger
- unless (V.qtFst dom `V.qGeq` domDemand) $ throwError Err -- TODO
+ unless (V.qtFst dom `V.qGeq` domDemand) $ throwError ErrTermArrowAbsQuantityMismatch
pure (C.TermArrowAbs body', q <⋅> absLedger)
- (S.TermArrowAbs _ _, _) -> throwError Err -- TODO
+ (S.TermArrowAbs _ _, _) -> throwError ErrTermArrowAbsNotArrow
(S.TermForallAbs x body, V.TypeTForall k clo) ->
bindAndAssignType x k \lvl -> do
@@ -189,15 +224,26 @@ checkTerm t q a = case (t, a) of
(body', bodyLedger) <- checkTerm body (V.qtFst qa) (V.qtSnd qa)
pure (C.TermForallAbs body', q <⋅> bodyLedger)
- (S.TermForallAbs _ _, _) -> throwError Err -- TODO
+ (S.TermForallAbs _ _, _) -> throwError ErrTermForallAbsNotForall
(t, a) -> do
(t', a', tLedger) <- inferTerm t q
equal <- convType a' a
- unless equal $ throwError Err -- TODO
+ unless equal $ throwError ErrTermInferCheckMismatch
pure (t', tLedger)
--------------------------------------------------------------------------------
+input :: ByteString
+input = "\\[M] z s => z : @M : * -> top ! (top ! M -> top ! (top ! (top ! M -> top ! M) -> top ! M))"
+
main :: IO ()
-main = putStrLn "whoa"
+main =
+ case P.runP P.pSrc P.pQul input of
+ Ok t _ _ ->
+ case inferTerm t one `runElab` bothCtxEmpty of
+ Left e -> print e
+ Right (t, a, _) -> do
+ print t
+ print $ V.quoteType Env.empty a
+ result -> print result
diff --git a/Parser.hs b/Parser.hs
@@ -0,0 +1,172 @@
+module Parser where
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Identity
+import Control.Monad.Reader
+import Data.Char
+import Data.ByteString (ByteString)
+import Sparsec
+
+import Qul (Qul)
+import qualified Qul
+import Qular (Qular)
+import qualified Qular
+import Common
+import Surface
+
+data Err = ErrUtf8 Loc | Err deriving Show -- TODO
+
+instance Utf8Error Err where
+ utf8Error = ErrUtf8
+
+type P q a = ParseT Err (Reader (Parse Err q)) a
+
+runP :: P q a -> Parse Err q -> ByteString -> Result Err a
+runP p pq input = runParseT p input locZero `runReader` pq
+
+pQul :: Parse Err Qul
+pQul = pWord "bot" *> pure Qul.Alpha
+ <|> pWord "0" *> pure Qul.Zero
+ <|> pWord "1" *> pure Qul.One
+ <|> pWord "top" *> pure Qul.Omega
+
+pQular :: Parse Err Qular
+pQular = pWord "bot" *> pure Qular.Alpha
+ <|> pWord "0" *> pure Qular.Zero
+ <|> pWord "1" *> pure Qular.One
+ <|> pWord "top" *> pure Qular.Omega
+ -- TODO: syntax for Aff and Rel
+
+isWordStart :: Char -> Bool
+isWordStart c = isLetter c || isDigit c || c == '_'
+
+isWordCont :: Char -> Bool
+isWordCont c = isLetter c || isDigit c || c == '_' || c == '\''
+
+isIdentStart :: Char -> Bool
+isIdentStart c = isLetter c || c == '_'
+
+isIdentCont :: Char -> Bool
+isIdentCont = isWordCont
+
+isReservedIdent :: ByteString -> Bool
+isReservedIdent s = s == "bot" || s == "top"
+
+pWs :: Monad m => ParseT Err m ByteString
+pWs = charWhile isSpace
+
+pToken :: Monad m => ParseT Err m a -> ParseT Err m a
+pToken p = p <* pWs
+
+pSym :: Monad m => String -> ParseT Err m ()
+pSym s = pToken (string s) *> pure ()
+
+pAnyWord :: Monad m => ParseT Err m ByteString
+pAnyWord = snd <$> pToken (bytesOf $ charIf isWordStart *> charWhile isWordCont)
+
+pWord :: Monad m => ByteString -> ParseT Err m ()
+pWord w = do
+ w' <- pAnyWord
+ guard (w' == w)
+
+pAnyIdent :: Monad m => ParseT Err m ByteString
+pAnyIdent = do
+ x <- snd <$> pToken (bytesOf $ charIf isIdentStart *> charWhile isIdentCont)
+ guard $ not $ isReservedIdent x
+ pure x
+
+pDelim :: Monad m => String -> ParseT Err m a -> String -> ParseT Err m a
+pDelim l p r = pSym l *> (p <* pSym r) `cut` Err
+
+pTypeName :: P q TypeName
+pTypeName = TypeName <$> pAnyIdent
+
+pTermName :: P q TermName
+pTermName = TermName <$> pAnyIdent
+
+pKindArrow :: Kind -> P q Kind
+pKindArrow dom = pSym "->" *> (KindArrow dom <$> pKind 0) `cut` Err
+
+pKind :: Int -> P q Kind
+pKind = \case
+ 0 -> do
+ k <- pKind 1
+ pKindArrow k <|> pure k
+ 1 -> pSym "$*" *> pure KindQT
+ <|> pSym "$" *> pure KindQ
+ <|> pSym "*" *> pure KindT
+ <|> pDelim "(" (pKind 0) ")"
+ _ -> error "pKind: invalid precedence"
+
+pTypeAnnot :: Type q -> P q (Type q)
+pTypeAnnot a = pSym ":" *> (TypeAnnot a <$> pKind 0) `cut` Err
+
+pTypeTArrow :: Type q -> P q (Type q)
+pTypeTArrow dom = pSym "->" *> (TypeTArrow dom <$> pType 2) `cut` Err
+
+pTypeTForall :: P q (Type q)
+pTypeTForall = do
+ pSym "@"
+ x <- pTypeName `cut` Err
+ k <- branch (pSym ":") (pKind 1 `cut` Err) (pure KindQT)
+ pSym "->" `cut` Err
+ body <- pType 2 `cut` Err
+ pure $ TypeTForall x k body
+
+pTypeQTPair :: Type q -> P q (Type q)
+pTypeQTPair q = pSym "!" *> (TypeQTPair q <$> pType 4) `cut` Err
+
+pTypeArrowAbs :: P q (Type q)
+pTypeArrowAbs = do
+ pSym "\\"
+ binders <- some (TypeArrowAbs <$> pTypeName) `cut` Err
+ pSym "=>" `cut` Err
+ body <- pType 1 `cut` Err
+ pure $ foldr1 (.) binders body
+
+pType :: Int -> P q (Type q)
+pType = \case
+ 0 -> do
+ a <- pType 1
+ pTypeAnnot a <|> pure a
+ 1 -> pTypeArrowAbs <|> pType 2
+ 2 -> pTypeTForall <|> do
+ a <- pType 3
+ pTypeTArrow a <|> pure a
+ 3 -> do
+ a <- pType 4
+ pTypeQTPair a <|> pure a
+ 4 -> pType 5 >>= iter \a -> TypeArrowApp a <$> pType 4
+ 5 -> pType 6 >>= iter \a -> pure (TypeQTFst a) <* pSym ".$"
+ <|> pure (TypeQTSnd a) <* pSym ".*"
+ 6 -> TypeVar <$> pTypeName
+ <|> (mapParseT (pure . runIdentity) . fmap TypeQ =<< ask)
+ <|> pDelim "(" (pType 0) ")"
+ _ -> error "pType: invalid precedence"
+
+pTermAnnot :: Term q -> P q (Term q)
+pTermAnnot t = pSym ":" *> (TermAnnot t <$> pType 0) `cut` Err
+
+pTermAbs :: P q (Term q)
+pTermAbs = do
+ pSym "\\"
+ binders <- some (TermArrowAbs <$> pTermName
+ <|> TermForallAbs <$> (pDelim "[" pTypeName "]")) `cut` Err
+ pSym "=>" `cut` Err
+ body <- pTerm 1 `cut` Err
+ pure $ foldr1 (.) binders body
+
+pTerm :: Int -> P q (Term q)
+pTerm = \case
+ 0 -> do
+ t <- pTerm 1
+ pTermAnnot t <|> pure t
+ 1 -> pTermAbs <|> pTerm 2
+ 2 -> pTerm 3 >>= iter \t -> TermArrowApp t <$> pTerm 3
+ <|> TermForallApp t <$> pDelim "[" (pType 0) "]"
+ 3 -> TermVar <$> pTermName
+ <|> pDelim "(" (pTerm 0) ")"
+ _ -> error "pTerm: invalid precedence"
+
+pSrc :: P q (Term q)
+pSrc = pWs *> pTerm 0 <* eof
