commit 7f339c58c6d34e9ecb44725e74b78bdb1ea8110c
parent aea61ae5b29bb37149845ffc56a23d84ec56ff21
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 29 Aug 2024 20:54:17 -0700
Add add/mul to surface syntax, and clean up parser
Diffstat:
| M | Main.hs | | | 16 | +++++++++++++--- |
| M | Parser.hs | | | 164 | +++++++++++++++++++++++++++++++++++++++++-------------------------------------- |
| M | Surface.hs | | | 3 | ++- |
3 files changed, 101 insertions(+), 82 deletions(-)
diff --git a/Main.hs b/Main.hs
@@ -112,6 +112,16 @@ inferType = \case
S.TypeQ q -> pure (C.TypeQ q, KindQ)
+ S.TypeQAdd q r -> do
+ q' <- checkType q KindQ
+ r' <- checkType r KindQ
+ pure (C.TypeQAdd q' r', KindQ)
+
+ S.TypeQMul q r -> do
+ q' <- checkType q KindQ
+ r' <- checkType r KindQ
+ pure (C.TypeQMul q' r', KindQ)
+
S.TypeQTPair q a -> do
q' <- checkType q KindQ
a' <- checkType a KindT
@@ -268,19 +278,19 @@ data Prog = Prog {
parseKind :: ByteString -> IO Kind
parseKind k =
- case P.runP P.pTopKind pQ k of
+ case P.runP (P.pTop P.pKind) pQ k of
Ok k _ _ -> pure k
result -> print result *> exitFailure
parseType :: ByteString -> IO (S.Type Q)
parseType a =
- case P.runP P.pTopType pQ a of
+ case P.runP (P.pTop P.pType) pQ a of
Ok a _ _ -> pure a
result -> print result *> exitFailure
parseTerm :: ByteString -> IO (S.Term Q)
parseTerm t =
- case P.runP P.pTopTerm pQ t of
+ case P.runP (P.pTop P.pTerm) pQ t of
Ok t _ _ -> pure t
result -> print result *> exitFailure
diff --git a/Parser.hs b/Parser.hs
@@ -5,6 +5,7 @@ import Control.Monad.Identity
import Control.Monad.Reader
import Data.Char
import Data.ByteString (ByteString)
+import Data.Function ((&))
import Sparsec
import Qul (Qul)
@@ -81,25 +82,26 @@ pAnyIdent = do
pDelim :: Monad m => String -> ParseT Err m a -> String -> ParseT Err m a
pDelim l p r = pSym l *> (p <* pSym r) `cut` Err
+pTop :: Monad m => ParseT Err m a -> ParseT Err m a
+pTop p = pWs *> p <* eof `cut` Err
+
--------------------------------------------------------------------------------
-- Kinds
+pKind :: P q Kind
+pKind = match pKind_atom [pKindArrow, pure]
+
+pKind_atom :: P q Kind
+pKind_atom =
+ choice [
+ pSym "$%" *> pure KindQT,
+ pSym "$" *> pure KindQ,
+ pSym "%" *> pure KindT,
+ pDelim "(" pKind ")"
+ ]
+
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"
-
-pTopKind :: P q Kind
-pTopKind = pWs *> pKind 0 <* eof
+pKindArrow dom = pSym "->" *> (KindArrow dom <$> pKind) `cut` Err
--------------------------------------------------------------------------------
-- Types
@@ -107,54 +109,62 @@ pTopKind = pWs *> pKind 0 <* eof
pTypeName :: P q TypeName
pTypeName = TypeName <$> pAnyIdent
+pType :: P q (Type q)
+pType = match pType_abs [pTypeAnnot, pure]
+
+pType_abs :: P q (Type q)
+pType_abs = pTypeArrowAbs <|> pType_arrow
+
+pType_arrow :: P q (Type q)
+pType_arrow = pTypeTForall <|> match pType_pair [pTypeTArrow, pure]
+
+pType_pair :: P q (Type q)
+pType_pair = match pType_add [pTypeQTPair, pure]
+
+pType_add :: P q (Type q)
+pType_add = chainl TypeQAdd pType_mul (pSym "+" *> pType_mul `cut` Err)
+
+pType_mul :: P q (Type q)
+pType_mul = chainl TypeQMul pType_app (pSym "*" *> pType_app `cut` Err)
+
+pType_app :: P q (Type q)
+pType_app = chainl TypeArrowApp pType_proj pType_proj
+
+pType_proj :: P q (Type q)
+pType_proj = chainl (&) pType_atom (pSym ".$" *> pure TypeQTFst
+ <|> pSym ".%" *> pure TypeQTSnd)
+
+pType_atom :: P q (Type q)
+pType_atom = TypeVar <$> pTypeName <|> pTypeQ <|> pDelim "(" pType ")"
+
pTypeAnnot :: Type q -> P q (Type q)
-pTypeAnnot a = pSym ":" *> (TypeAnnot a <$> pKind 0) `cut` Err
+pTypeAnnot a = pSym ":" *> (TypeAnnot a <$> pKind) `cut` Err
+
+pTypeArrowAbs :: P q (Type q)
+pTypeArrowAbs = do
+ pSym "\\"
+ binders <- some (TypeArrowAbs <$> pTypeName) `cut` Err
+ pSym "=>" `cut` Err
+ body <- pType_abs `cut` Err
+ pure $ foldr1 (.) binders body
pTypeTArrow :: Type q -> P q (Type q)
-pTypeTArrow dom = pSym "->" *> (TypeTArrow dom <$> pType 2) `cut` Err
+pTypeTArrow dom = pSym "->" *> (TypeTArrow dom <$> pType_arrow) `cut` Err
pTypeTForall :: P q (Type q)
pTypeTForall = do
pSym "@"
x <- pTypeName `cut` Err
- k <- branch (pSym ":") (pKind 1 `cut` Err) (pure KindQT)
+ k <- branch (pSym ":") (pKind_atom `cut` Err) (pure KindQT)
pSym "->" `cut` Err
- body <- pType 2 `cut` Err
+ body <- pType_arrow `cut` Err
pure $ TypeTForall x k body
-pTypeQTPair :: Type q -> P q (Type q)
-pTypeQTPair q = pSym "!" *> (TypeQTPair q <$> pType 4) `cut` Err
+pTypeQ :: P q (Type q)
+pTypeQ = mapParseT (pure . runIdentity) . fmap TypeQ =<< ask
-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"
-
-pTopType :: P q (Type q)
-pTopType = pWs *> pType 0 <* eof
+pTypeQTPair :: Type q -> P q (Type q)
+pTypeQTPair q = pSym "!" *> (TypeQTPair q <$> pType_add) `cut` Err
--------------------------------------------------------------------------------
-- Terms
@@ -162,41 +172,39 @@ pTopType = pWs *> pType 0 <* eof
pTermName :: P q TermName
pTermName = TermName <$> pAnyIdent
-pTermAnnot :: Term q -> P q (Term q)
-pTermAnnot t = pSym ":" *> (TermAnnot t <$> pType 0) `cut` Err
+pTerm :: P q (Term q)
+pTerm = pTermLet <|> match pTerm_abs [pTermAnnot, pure]
-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_abs :: P q (Term q)
+pTerm_abs = pTermAbs <|> pTerm_app
+
+pTerm_app :: P q (Term q)
+pTerm_app = chainl (&) pTerm_atom (flip TermArrowApp <$> pTerm_atom
+ <|> flip TermForallApp <$> pDelim "[" pType "]")
+
+pTerm_atom :: P q (Term q)
+pTerm_atom = TermVar <$> pTermName <|> pDelim "(" pTerm ")"
+
+pTermAnnot :: Term q -> P q (Term q)
+pTermAnnot t = pSym ":" *> (TermAnnot t <$> pType) `cut` Err
pTermLet :: P q (Term q)
pTermLet = do
pWord "let"
x <- pTermName `cut` Err
pSym ":" `cut` Err
- qa <- pType 0 `cut` Err
+ qa <- pType `cut` Err
pSym "=" `cut` Err
- arg <- pTerm 1 `cut` Err
+ arg <- pTerm `cut` Err
pSym ";" `cut` Err
- body <- pTerm 0 `cut` Err
+ body <- pTerm `cut` Err
pure $ TermLet x arg qa body
-pTerm :: Int -> P q (Term q)
-pTerm = \case
- 0 -> pTermLet <|> 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"
-
-pTopTerm :: P q (Term q)
-pTopTerm = pWs *> pTerm 0 <* eof
+pTermAbs :: P q (Term q)
+pTermAbs = do
+ pSym "\\"
+ binders <- some (TermArrowAbs <$> pTermName
+ <|> TermForallAbs <$> pDelim "[" pTypeName "]") `cut` Err
+ pSym "=>" `cut` Err
+ body <- pTerm_abs `cut` Err
+ pure $ foldr1 (.) binders body
diff --git a/Surface.hs b/Surface.hs
@@ -16,7 +16,8 @@ data Type q
| TypeTForall TypeName Kind (Type q)
| TypeQ q
- -- TODO: Internal Mul and Add operations
+ | TypeQAdd (Type q) (Type q)
+ | TypeQMul (Type q) (Type q)
| TypeQTPair (Type q) (Type q)
| TypeQTFst (Type q)
