diff --git a/src/Main.hs b/src/Main.hs index 9cd992d..ba73720 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,5 +1,14 @@ module Main where +import qualified Data.ByteString.Lazy as Bsl +import Data.Foldable + +import Presyntax.Parser +import Presyntax.Tokens +import Presyntax.Lexer + main :: IO () main = do - putStrLn "hello world" + t <- Bsl.readFile "test.tt" + let Right tks = runAlex t parseProg + traverse_ print tks \ No newline at end of file diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x index e7c54cd..42ded0c 100644 --- a/src/Presyntax/Lexer.x +++ b/src/Presyntax/Lexer.x @@ -7,31 +7,44 @@ import qualified Data.Text.Encoding as T import Presyntax.Tokens } -%wrapper "monad-bytestring" +%wrapper "monadUserState-bytestring" $alpha = [a-zA-Z] $digit = [0-9] +$white_nol = $white # \n tokens :- - $white+ ; - $alpha [$alpha $digit \_ \']* { yield TokVar } + $white_nol+ ; - \= { always TokEqual } - \: { always TokColon } - \, { always TokComma } - \* { always TokStar } +-- zero state: normal lexing +<0> $alpha [$alpha $digit \_ \']* { yield TokVar } - ".1" { always TokPi1 } - ".2" { always TokPi2 } - - \\ { always TokLambda } - "->" { always TokArrow } +<0> \= { always TokEqual } +<0> \: { always TokColon } +<0> \, { always TokComma } +<0> \* { always TokStar } + +<0> ".1" { always TokPi1 } +<0> ".2" { always TokPi2 } + +<0> \\ { always TokLambda } +<0> "->" { always TokArrow } + +<0> \( { always TokOParen } +<0> \{ { always TokOBrace } - \( { always TokOParen } - \{ { always TokOBrace } +<0> \) { always TokCParen } +<0> \} { always TokCBrace } +<0> \; { always TokSemi } + +<0> \n { begin newline } + +-- newline: emit a semicolon when de-denting + { + \n ; + () { offsideRule } +} - \) { always TokCParen } - \} { always TokCBrace } { alexEOF :: Alex Token @@ -41,4 +54,43 @@ alexEOF = do yield k (AlexPn _ l c, _, s, _) i = pure (Token (k $! (T.decodeUtf8 (Lbs.toStrict (Lbs.take i s)))) l c) always k x i = yield (const k) x i + +data AlexUserState = AlexUserState { layoutColumns :: [Int], startCodes :: [Int] } +alexInitUserState = AlexUserState [1] [] + +just :: Alex a -> AlexAction Token +just k _ _ = k *> alexMonadScan + +getUserState :: Alex AlexUserState +getUserState = Alex $ \s -> Right (s, alex_ust s) + +mapUserState :: (AlexUserState -> AlexUserState) -> Alex () +mapUserState k = Alex $ \s -> Right (s { alex_ust = k $! alex_ust s }, ()) + +pushStartCode :: Int -> Alex () +pushStartCode c = do + sc <- alexGetStartCode + mapUserState $ \s -> s { startCodes = sc:startCodes s } + alexSetStartCode c + +popStartCode :: Alex () +popStartCode = do + sc <- startCodes <$> getUserState + case sc of + [] -> alexSetStartCode 0 + (x:xs) -> do + mapUserState $ \s -> s { startCodes = xs } + alexSetStartCode x + +offsideRule :: AlexInput -> Int64 -> Alex Token +offsideRule i@(AlexPn p line col, _, s, _) l = do + ~(col':_) <- layoutColumns <$> getUserState + case col `compare` col' of + EQ -> do + popStartCode + pure (Token TokSemi line col) + GT -> do + popStartCode + alexMonadScan + LT -> alexError "wrong ass indentation" } \ No newline at end of file diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index ab90586..90c1e1e 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -10,7 +10,9 @@ import Presyntax.Lexer } -%name parseExp Exp +%name parseExp Exp +%name parseStmt Statement +%name parseProg Program %tokentype { Token } @@ -32,6 +34,7 @@ import Presyntax.Lexer '->' { Token TokArrow _ _ } ':' { Token TokColon _ _ } + ';' { Token TokSemi _ _ } '=' { Token TokEqual _ _ } ',' { Token TokComma _ _ } '*' { Token TokStar _ _ } @@ -43,12 +46,12 @@ import Presyntax.Lexer Exp :: { Expr } Exp - : ExpProj Exp { App Ex $1 $2 } - | ExpProj '{' Exp '}' { App Im $1 $3 } + : Exp ExpProj { App Ex $1 $2 } + | Exp '{' Exp '}' { App Im $1 $3 } | '\\' LambdaList '->' Exp { makeLams $2 $4 } - | '(' VarList ':' Exp ')' '->' Exp { makePis Ex $2 $4 $7 } - | '{' VarList ':' Exp '}' '->' Exp { makePis Im $2 $4 $7 } + | '(' VarList ':' Exp ')' ProdTail { makePis Ex $2 $4 $6 } + | '{' VarList ':' Exp '}' ProdTail { makePis Im $2 $4 $6 } | ExpProj '->' Exp { Pi Ex (T.singleton '_') $1 $3 } | '(' VarList ':' Exp ')' '*' Exp { makeSigmas $2 $4 $7 } @@ -56,6 +59,11 @@ Exp | ExpProj { $1 } +ProdTail :: { Expr } + : '(' VarList ':' Exp ')' ProdTail { makePis Ex $2 $4 $6 } + | '{' VarList ':' Exp '}' ProdTail { makePis Im $2 $4 $6 } + | '->' Exp { $2 } + LambdaList :: { [(Plicity, Text)] } : var { [(Ex, $1)] } | var LambdaList { (Ex, $1):$2 } @@ -80,6 +88,14 @@ Tuple :: { Expr } : Exp { $1 } | Exp ',' Tuple { Pair $1 $3 } +Statement :: { Statement } + : var ':' Exp { Decl $1 $3 } + | var '=' Exp { Defn $1 $3 } + +Program :: { [Statement] } + : Statement { [$1] } + | Statement ';' Program { $1:$3 } + { lexer cont = alexMonadScan >>= cont diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs index 46c4f23..93c5fd9 100644 --- a/src/Presyntax/Tokens.hs +++ b/src/Presyntax/Tokens.hs @@ -21,6 +21,8 @@ data TokenClass | TokPi1 | TokPi2 + + | TokSemi deriving (Eq, Show, Ord) data Token