commit 9587a979940d30637452a3eb845512fe40ecb5a5
parent 19d87c54f3f72712a7802ba0da12ff17cc3f3aae
Author: Robert Russell <robert@rr3.xyz>
Date: Tue, 27 Aug 2024 14:25:43 -0700
Extend surface syntax
Diffstat:
| M | example/Main.hs | | | 159 | +++++++++++++++++++++++++++++++++++++++++++++++++++---------------------------- |
1 file changed, 103 insertions(+), 56 deletions(-)
diff --git a/example/Main.hs b/example/Main.hs
@@ -9,45 +9,48 @@ import Debug.Trace -- TODO
import Sparsec
--------------------------------------------------------------------------------
+-- Surface syntax
-newtype Label = Label ByteString deriving Show
-newtype Name = Name ByteString deriving Show
+newtype XtorName = XtorName ByteString deriving (Show, Eq, Ord)
+newtype VarName = VarName ByteString deriving (Show, Eq, Ord)
+newtype CmdName = CmdName ByteString deriving (Show, Eq, Ord)
data PosNeg = Pos | Neg deriving Show
data PrdCns = Prd | Cns deriving Show
-data DeclField
- = DeclFieldType Name
- | DeclFieldTerm PrdCns Type
- deriving Show
-data DeclXtor = DeclXtor Label [DeclField] deriving Show
-data DeclParam = DeclParam Name Kind deriving Show
-data Decl = Decl PosNeg Name [DeclParam] [DeclXtor] deriving Show
+data DeclParam = DeclParam VarName Kind deriving Show
+data DeclField = DeclField PrdCns Type deriving Show
+data DeclXtor = DeclXtor XtorName [DeclParam] [DeclField] deriving Show
+data Decl = Decl PosNeg VarName [DeclParam] [DeclXtor] deriving Show
data Kind
- = KindType
+ = KindType PosNeg
| KindArrow Kind Kind
deriving Show
data Type
- = TypeVar Name
- | TypeLam Name Kind Type
+ = TypeVar VarName
+ | TypeLam VarName (Maybe Kind) Type
| TypeApp Type Type
deriving Show
-data Case = Case Label [Name] Stmt deriving Show
+data Case = Case XtorName [VarName] Stmt deriving Show
data Term
- = TermVar Name
- | TermMu Name Stmt
- | TermXtor Label [Term]
+ = TermVar VarName
+ | TermMu VarName (Maybe Type) Stmt
+ | TermXtor XtorName [Type] [Term]
| TermMatch [Case]
deriving Show
-data Stmt = StmtCut Term Type Term deriving Show
+data Stmt
+ = StmtCut Term Type Term -- TODO: Should Cut be a special case of Cmd?
+ | StmtCmd CmdName [Type] [Term]
+ deriving Show
data Prog = Prog [Decl] Stmt deriving Show
--------------------------------------------------------------------------------
+-- Parser
data Err = ErrUtf8 Loc | Err deriving Show -- TODO
@@ -60,7 +63,7 @@ isLetterOrDigit c = isLetter c || isDigit c
isWordStart c = isLetter c || c == '_'
isWordCont c = isLetterOrDigit c || c == '_' || c == '\''
-isKw s = s == "pos" || s == "neg" || s == "prd" || s == "cns"
+isKw s = s == "data" || s == "prd" || s == "cns"
pWs = charWhile isSpace
pToken p = p <* pWs
@@ -73,56 +76,60 @@ pDelim l p r = pSym l *> (p <* pSym r) `cut` Err
pManySepByWithTrailer p sep = p `someSepBy` sep <* opt sep <|> pure []
pList p = p `pManySepByWithTrailer` pSym ","
-pLabel = Label <$> pToken (char '#' *> pWord `cut` Err)
-pName = do
+pXtorName = XtorName <$> pToken (char '#' *> pWord `cut` Err)
+
+pVarName = do
x <- pToken pWord
guard $ not $ isKw x
- pure $ Name x
+ pure $ VarName x
+
+pCmdName = CmdName <$> pToken (char '@' *> pWord `cut` Err)
-pPosNeg = pKw "pos" *> pure Pos <|> pKw "neg" *> pure Neg
+pPosNeg = pSym "+" *> pure Pos <|> pSym "-" *> pure Neg
pPrdCns = pKw "prd" *> pure Prd <|> pKw "cns" *> pure Cns
+pDeclParam :: Int -> P DeclParam
+pDeclParam = \case
+ 0 -> DeclParam <$> pVarName <*> branch (pSym ":") (pKind 0 `cut` Err) (pure $ KindType Pos)
+ 1 -> DeclParam <$> pVarName <*> pure (KindType Pos) <|> pDelim "(" (pDeclParam 0) ")"
+
pDeclField :: Int -> P DeclField
pDeclField = \case
- 0 -> DeclFieldTerm <$> (pPrdCns <|> pure Prd) <*> pType 0 <|> pDeclField 1
- 1 -> pSym "$" *> (DeclFieldType <$> pName) `cut` Err
- <|> pDelim "(" (pDeclField 0) ")"
- <|> DeclFieldTerm Prd <$> pTypeAtom
+ 0 -> DeclField <$> (pPrdCns <|> pure Prd) <*> pType 0
+ 1 -> DeclField Prd <$> pTypeAtom <|> pDelim "(" (pDeclField 0) ")"
-pDeclXtor = DeclXtor <$> pLabel <*> many (pDeclField 1)
-
-pDeclParam :: Int -> P DeclParam
-pDeclParam = \case
- 0 -> do
- x <- pName
- k <- pSym ":" *> pKind 0 `cut` Err <|> pure KindType
- pure $ DeclParam x k
- 1 -> DeclParam <$> pName <*> pure KindType <|> pDelim "(" (pDeclParam 0) ")"
+pDeclXtor = do
+ x <- pXtorName
+ params <- pDelim "[" (many (pDeclParam 1)) "]" <|> pure []
+ fields <- many (pDeclField 1)
+ pure $ DeclXtor x params fields
pDecl = do
- posneg <- pPosNeg
- x <- pName
+ pKw "data"
+ x <- pVarName
params <- many (pDeclParam 1)
+ posneg <- branch (pSym ":") (pPosNeg `cut` Err) (pure Pos)
xtors <- pDelim "{" (pList pDeclXtor) "}"
pure $ Decl posneg x params xtors
+pKindArrow dom = pSym "->" *> (KindArrow dom <$> pKind 0) `cut` Err
+
pKind :: Int -> P Kind
pKind = \case
0 -> do
k <- pKind 1
- (pSym "->" *> (KindArrow k <$> pKind 0) `cut` Err) <|> pure k
- 1 -> pSym "*" *> pure KindType <|> pDelim "(" (pKind 0) ")"
+ pKindArrow k <|> pure k
+ 1 -> KindType <$> pPosNeg <|> pDelim "(" (pKind 0) ")"
pTypeLam = do
pSym "\\"
- x <- pName `cut` Err
- pSym ":" `cut` Err
- k <- pKind 0 `cut` Err
+ x <- pVarName `cut` Err
+ mk <- opt (pSym ":" *> pKind 0 `cut` Err)
pSym "=>" `cut` Err
body <- pType 0 `cut` Err
- pure $ TypeLam x k body
+ pure $ TypeLam x mk body
-pTypeAtom = TypeVar <$> pName
+pTypeAtom = TypeVar <$> pVarName
pType :: Int -> P Type
pType = \case
@@ -131,48 +138,88 @@ pType = \case
2 -> pTypeAtom <|> pDelim "(" (pType 0) ")"
pCase = do
- l <- pLabel
- vars <- many pName
+ x <- pXtorName
+ vars <- many pVarName
pSym "=>" `cut` Err
body <- pStmt `cut` Err
- pure $ Case l vars body
+ pure $ Case x vars body
pTermMu = do
pSym "\\"
- x <- pName `cut` Err
+ x <- pVarName `cut` Err
+ ma <- opt (pSym ":" *> pType 1 `cut` Err)
pSym "=>" `cut` Err
body <- pStmt `cut` Err
- pure $ TermMu x body
+ pure $ TermMu x ma body
+
+pTermArg = pTerm 2 <|> TermXtor <$> pXtorName <*> pure [] <*> pure []
+
+args = do
+ tyArgs <- pDelim "[" (many (pType 2)) "]" <|> pure []
+ tmArgs <- many pTermArg
+ pure (tyArgs, tmArgs)
+
+pTermXtor = do
+ x <- pXtorName
+ (tyArgs, tmArgs) <- args
+ pure $ TermXtor x tyArgs tmArgs
pTerm :: Int -> P Term
pTerm = \case
0 -> pTermMu <|> pTerm 1
- 1 -> TermXtor <$> pLabel <*> many (pTerm 2) <|> pTerm 2
- 2 -> TermVar <$> pName
- <|> TermXtor <$> pLabel <*> pure []
+ 1 -> pTermXtor <|> pTerm 2
+ 2 -> TermVar <$> pVarName
<|> TermMatch <$> pDelim "{" (pList pCase) "}"
<|> pDelim "(" (pTerm 0) ")"
-pStmt = do
- pSym "["
+pStmtCmd = do
+ x <- pCmdName
+ (tyArgs, tmArgs) <- args
+ pure $ StmtCmd x tyArgs tmArgs
+
+pStmtCut = do
prd <- pTerm 0
pSym ":" `cut` Err
typ <- pType 0 `cut` Err
pSym ":" `cut` Err
cns <- pTerm 0 `cut` Err
- pSym "]" `cut` Err
pure $ StmtCut prd typ cns
+pStmt = pStmtCmd <|> pStmtCut
+
pProg :: P Prog
pProg = Prog <$> many pDecl <*> pStmt
pSrc :: P Prog
pSrc = pWs *> pProg <* eof
+
+--------------------------------------------------------------------------------
+-- Core syntax
--------------------------------------------------------------------------------
+-- Context
+
+data Ctx = Ctx {
+}
+
+--------------------------------------------------------------------------------
+-- Elaboration monad
+
+--------------------------------------------------------------------------------
+-- Elaboration
+
+{-
+elabDecl :: Decl -> Elab
+elabDecl (Decl posneg x params xtors) =
+
+elabProg :: Prog -> Elab
+elabProg (Prog decls stmt) =
+-}
+
+--------------------------------------------------------------------------------
ex :: ByteString
-ex = "pos Bool { #true, #false } pos Any { #any $A A, } [#true :Bool: #false]"
+ex = "data Bool { #true, #false } data Any { #any [A] A, } #true :Bool: \\x=>@print"
main :: IO ()
main = print $ runParse pSrc ex locZero
