sparsec

commit 0e629ebca0cb1e808dde1800064e4c83d8bb1f2a
parent a3a2975db4b55a0fc472a1be5f13ca00c16dc4df
Author: Robert Russell <robert@rr3.xyz>
Date:   Tue, 27 Aug 2024 02:39:31 -0700

Start work on example

The example is basically System CD of Downen and Ariola, "Compiling
with Classical Connectives".

Diffstat:
A
example/Main.hs
 | 
166
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
M
package.yaml
 | 
6
+++++-

2 files changed, 171 insertions(+), 1 deletion(-)
diff --git a/example/Main.hs b/example/Main.hs
@@ -0,0 +1,166 @@
+module Main where
+import Control.Applicative
+import Control.Monad
+import Data.ByteString (ByteString)
+import Data.Char
+
+import Sparsec
+
+--------------------------------------------------------------------------------
+
+newtype Label = Label ByteString
+newtype Name = Name ByteString
+
+data PosNeg = Pos | Neg
+data PrdCns = Prd | Cns
+
+data DeclField
+    = DeclFieldType Name
+    | DeclFieldTerm PrdCns Type
+data DeclXtor = DeclXtor Label [DeclField]
+data DeclParam = DeclParam Name Kind
+data Decl = Decl PosNeg Name [DeclParam] [DeclXtor]
+
+data Kind
+    = KindType
+    | KindArrow Kind Kind
+
+data Type
+    = TypeVar Name
+    | TypeLam Name Kind Type
+    | TypeApp Type Type
+
+data Case = Case Label [Name] Stmt
+data Term
+    = TermVar Name
+    | TermMu Name Stmt
+    | TermXtor Label [Term]
+    | TermMatch [Case]
+
+data Stmt = StmtCut Term Type Term
+
+data Prog = Prog [Decl] Stmt
+
+--------------------------------------------------------------------------------
+
+data Err = ErrUtf8 Loc | Err
+
+instance Utf8Error Err where
+    utf8Error = ErrUtf8
+
+type P a = Parse Err a
+
+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"
+
+pWs = charWhile isSpace
+pToken p = p <* pWs
+pSym = pToken . string
+pBreak = notp $ charIf isWordCont
+pKw s = pSym s <* pBreak
+pWord = bytesOf $ charIf isWordStart *> charWhile isWordCont
+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
+    x <- pToken pWord
+    guard $ not $ isKw x
+    pure $ Name x
+
+pPosNeg = pKw "pos" *> pure Pos <|> pKw "neg" *> pure Neg
+pPrdCns = pKw "prd" *> pure Prd <|> pKw "cns" *> pure Cns
+
+pDeclField :: Int -> P DeclField
+pDeclField = \case
+    0 -> DeclFieldTerm <$> (pPrdCns <|> pure Prd) <*> pType 1
+    1 -> DeclFieldTerm Prd <$> pType 2
+        <|> pSym "$" *> (DeclFieldType <$> pName) `cut` Err
+        <|> 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) ")"
+
+pDecl = do
+    posneg <- pPosNeg
+    x <- pName
+    params <- many (pDeclParam 1)
+    xtors <- pDelim "{" (pList pDeclXtor) "}"
+    pure $ Decl posneg x params xtors
+
+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) ")"
+
+pTypeLam = do
+    pSym "\\"
+    x <- pName `cut` Err
+    pSym ":" `cut` Err
+    k <- pKind 0 `cut` Err
+    pSym "=>" `cut` Err
+    body <- pType 0 `cut` Err
+    pure $ TypeLam x k body
+
+pType :: Int -> P Type
+pType = \case
+    0 -> pTypeLam <|> pType 1
+    1 -> pType 2 >>= iter \a -> TypeApp a <$> pType 2
+    2 -> TypeVar <$> pName <|> pDelim "(" (pType 0) ")"
+
+pCase = do
+    l <- pLabel
+    vars <- many pName
+    pSym "=>" `cut` Err
+    body <- pStmt `cut` Err
+    pure $ Case l vars body
+
+pTermMu = do
+    pSym "\\"
+    x <- pName `cut` Err
+    pSym "=>" `cut` Err
+    body <- pStmt `cut` Err
+    pure $ TermMu x body
+
+pTerm :: Int -> P Term
+pTerm = \case
+    0 -> pTermMu <|> pTerm 1
+    1 -> TermXtor <$> pLabel <*> many (pTerm 2) <|> pTerm 2
+    2 -> TermVar <$> pName
+        <|> TermXtor <$> pLabel <*> pure []
+        <|> TermMatch <$> pDelim "{" (pList pCase) "}"
+        <|> pDelim "(" (pTerm 0) ")"
+
+pStmt = do
+    pSym "["
+    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
+
+pProg :: P Prog
+pProg = Prog <$> many pDecl <*> pStmt
+
+pSrc :: P Prog
+pSrc = pWs *> pProg <* eof
+    
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main = putStrLn "whoa"
diff --git a/package.yaml b/package.yaml
@@ -16,6 +16,8 @@ default-extensions:
   - LambdaCase
   - MultiWayIf
 
+  - OverloadedStrings
+
   - ScopedTypeVariables
 
   - FlexibleInstances
@@ -24,15 +26,17 @@ default-extensions:
 
 dependencies:
   - base >= 4.18 && < 5
+  - bytestring
 
 library:
   source-dirs: .
   dependencies:
     - mtl
-    - bytestring
     - utf8-string
 
 executables:
   example:
     source-dirs: example
     main: Main.hs
+    dependencies:
+      - sparsec