From a7d9ac4c0b9b6f313a8a588c58b6e2694fce5645 Mon Sep 17 00:00:00 2001 From: depsterr Date: Sat, 23 Jul 2022 03:38:15 +0200 Subject: [PATCH] added parser --- pi.ipkg | 17 +- src/{ => Core}/Check.idr | 12 +- src/{ => Core}/Convert.idr | 10 +- src/{ => Core}/Misc.idr | 2 +- src/{ => Core}/Normalize.idr | 8 +- src/{ => Core}/Term.idr | 4 +- src/{ => Core}/Tests.idr | 14 +- src/{ => Core}/Value.idr | 6 +- src/Main.idr | 10 +- src/Parser/Parse.idr | 366 +++++++++++++++++++++++++++++++++++ 10 files changed, 412 insertions(+), 37 deletions(-) rename src/{ => Core}/Check.idr (97%) rename src/{ => Core}/Convert.idr (96%) rename src/{ => Core}/Misc.idr (98%) rename src/{ => Core}/Normalize.idr (96%) rename src/{ => Core}/Term.idr (99%) rename src/{ => Core}/Tests.idr (97%) rename src/{ => Core}/Value.idr (94%) create mode 100644 src/Parser/Parse.idr diff --git a/pi.ipkg b/pi.ipkg index 2502d42..10a86ec 100644 --- a/pi.ipkg +++ b/pi.ipkg @@ -1,16 +1,17 @@ package pi -modules = Term - , Value - , Normalize - , Convert - , Check - , Misc - , Tests +modules = Core.Check + , Core.Convert + , Core.Misc + , Core.Normalize + , Core.Term + , Core.Tests + , Core.Value + , Parser.Parse options = "-p contrib --warnpartial" main = Main sourcedir = "src" -executable = "addict" +executable = "pi" diff --git a/src/Check.idr b/src/Core/Check.idr similarity index 97% rename from src/Check.idr rename to src/Core/Check.idr index bf32bdf..68954df 100644 --- a/src/Check.idr +++ b/src/Core/Check.idr @@ -1,4 +1,4 @@ -module Check +module Core.Check import Control.Monad.RWS import Control.Monad.Either @@ -6,11 +6,11 @@ import Control.Monad.Identity import Data.Vect import Data.Fin -import Term -import Value -import Normalize -import Misc -import Convert +import Core.Term +import Core.Value +import Core.Normalize +import Core.Misc +import Core.Convert %default total diff --git a/src/Convert.idr b/src/Core/Convert.idr similarity index 96% rename from src/Convert.idr rename to src/Core/Convert.idr index cbe3013..fb06399 100644 --- a/src/Convert.idr +++ b/src/Core/Convert.idr @@ -1,9 +1,9 @@ -module Convert +module Core.Convert -import Term -import Value -import Misc -import Normalize +import Core.Term +import Core.Value +import Core.Misc +import Core.Normalize import Control.Monad.RWS import Control.Monad.Identity diff --git a/src/Misc.idr b/src/Core/Misc.idr similarity index 98% rename from src/Misc.idr rename to src/Core/Misc.idr index 1d2e4af..dfdac45 100644 --- a/src/Misc.idr +++ b/src/Core/Misc.idr @@ -1,4 +1,4 @@ -module Misc +module Core.Misc import Control.Monad.RWS import Control.Monad.Identity diff --git a/src/Normalize.idr b/src/Core/Normalize.idr similarity index 96% rename from src/Normalize.idr rename to src/Core/Normalize.idr index f4c3cf4..de9d31a 100644 --- a/src/Normalize.idr +++ b/src/Core/Normalize.idr @@ -1,8 +1,8 @@ -module Normalize +module Core.Normalize -import Term -import Value -import Misc +import Core.Term +import Core.Value +import Core.Misc import Control.Monad.RWS import Control.Monad.Identity diff --git a/src/Term.idr b/src/Core/Term.idr similarity index 99% rename from src/Term.idr rename to src/Core/Term.idr index 18e665c..e74ee01 100644 --- a/src/Term.idr +++ b/src/Core/Term.idr @@ -1,8 +1,8 @@ -module Term +module Core.Term import Data.Fin -import Misc +import Core.Misc %default total diff --git a/src/Tests.idr b/src/Core/Tests.idr similarity index 97% rename from src/Tests.idr rename to src/Core/Tests.idr index 8b415d3..1ff9b3b 100644 --- a/src/Tests.idr +++ b/src/Core/Tests.idr @@ -1,11 +1,11 @@ -module Tests +module Core.Tests -import Term -import Check -import Convert -import Misc -import Normalize -import Value +import Core.Term +import Core.Check +import Core.Convert +import Core.Misc +import Core.Normalize +import Core.Value import Control.Monad.RWS import Control.Monad.Identity diff --git a/src/Value.idr b/src/Core/Value.idr similarity index 94% rename from src/Value.idr rename to src/Core/Value.idr index 43b3541..28f426d 100644 --- a/src/Value.idr +++ b/src/Core/Value.idr @@ -1,7 +1,7 @@ -module Value +module Core.Value -import Term -import Misc +import Core.Term +import Core.Misc import Data.Vect diff --git a/src/Main.idr b/src/Main.idr index 09b50ac..7b329d5 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -1,4 +1,12 @@ module Main +import Core.Check +import Core.Term +import Parser.Parse + main : IO () -main = pure () +main = do + str <- getLine + case parse0 str of + Left e => putStrLn e + Right t => print t diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr new file mode 100644 index 0000000..60f3260 --- /dev/null +++ b/src/Parser/Parse.idr @@ -0,0 +1,366 @@ +module Parser.Parse + +import Text.Lexer +import Text.Parser + +import Data.Vect +import Data.List +import Data.List1 +import Data.Maybe + +-- eventually start using elaborator representation here, or just a parser +-- exclusive one +import Core.Term +import Core.Misc + +%default total + +data PiTokenKind + = PTLambda + | PTIdentifier + | PTDot + | PTArrow + | PTPi + | PTSigma + | PTComma + | PTLParen + | PTRParen + | PTColon + | PTLet + | PTDefEq + | PTIn + | PTIgnore + | PTType + | PTTop + | PTStar + | PTTopInd + | PTBot + | PTBotInd + | PTNat + | PTZero + | PTSuc + | PTNatInd + | PTSigInd + +Eq PiTokenKind where + (==) PTLambda PTLambda = True + (==) PTIdentifier PTIdentifier = True + (==) PTDot PTDot = True + (==) PTArrow PTArrow = True + (==) PTPi PTPi = True + (==) PTSigma PTSigma = True + (==) PTComma PTComma = True + (==) PTLParen PTLParen = True + (==) PTRParen PTRParen = True + (==) PTColon PTColon = True + (==) PTLet PTLet = True + (==) PTDefEq PTDefEq = True + (==) PTIn PTIn = True + (==) PTIgnore PTIgnore = True + (==) PTType PTType = True + (==) PTTop PTTop = True + (==) PTStar PTStar = True + (==) PTTopInd PTTopInd = True + (==) PTBot PTBot = True + (==) PTBotInd PTBotInd = True + (==) PTNat PTNat = True + (==) PTZero PTZero = True + (==) PTSuc PTSuc = True + (==) PTNatInd PTNatInd = True + (==) PTSigInd PTSigInd = True + (==) _ _ = False + +Show PiTokenKind where + show PTLambda = "PTLambda" + show PTIdentifier = "PTIdentifier" + show PTDot = "PTDot" + show PTArrow = "PTArrow" + show PTPi = "PTPi" + show PTSigma = "PTSigma" + show PTComma = "PTComma" + show PTLParen = "PTLParen" + show PTRParen = "PTRParen" + show PTColon = "PTColon" + show PTLet = "PTLet" + show PTDefEq = "PTDefEq" + show PTIn = "PTIn" + show PTIgnore = "PTIgnore" + show PTType = "PTType" + show PTTop = "PTTop" + show PTStar = "PTSTar" + show PTTopInd = "PTTopInd" + show PTBot = "PTBot" + show PTBotInd = "PTBotInd" + show PTNat = "PTNat" + show PTZero = "PTZero" + show PTSuc = "PTSuc" + show PTNatInd = "PTNatInd" + show PTSigInd = "PTSigInd" + +PiToken : Type +PiToken = Token PiTokenKind + +Show PiToken where + show (Tok kind text) = "Tok kind: " ++ show kind ++ " text: " ++ text + +TokenKind PiTokenKind where + TokType PTIdentifier = String + TokType _ = () + + tokValue PTLambda _ = () + tokValue PTIdentifier s = s + tokValue PTDot _ = () + tokValue PTArrow _ = () + tokValue PTPi _ = () + tokValue PTSigma _ = () + tokValue PTComma _ = () + tokValue PTLParen _ = () + tokValue PTRParen _ = () + tokValue PTColon _ = () + tokValue PTLet _ = () + tokValue PTDefEq _ = () + tokValue PTIn _ = () + tokValue PTIgnore _ = () + tokValue PTType _ = () + tokValue PTTop _ = () + tokValue PTStar _ = () + tokValue PTTopInd _ = () + tokValue PTBot _ = () + tokValue PTBotInd _ = () + tokValue PTNat _ = () + tokValue PTZero _ = () + tokValue PTSuc _ = () + tokValue PTNatInd _ = () + tokValue PTSigInd _ = () + +ignored : WithBounds PiToken -> Bool +ignored (MkBounded (Tok PTIgnore _) _ _) = True +ignored _ = False + +identifier : Lexer +identifier = some (alphaNum <|> symbol) + +keywords : List (String, PiTokenKind) +keywords = [ + ("in", PTIn), + ("let", PTLet), + ("Type", PTType), + ("⊤-ind", PTTopInd), + ("⊥-ind", PTBotInd), + ("ℕ-ind", PTNatInd), + ("Σ-ind", PTSigInd), + ("λ", PTLambda), + (".", PTDot), + ("→", PTArrow), + ("Π", PTPi), + ("Σ", PTSigma), + (",", PTComma), + ("(", PTLParen), + (")", PTRParen), + (":", PTColon), + ("≔", PTDefEq), + ("⊤", PTTop), + ("⊥", PTBot), + ("ℕ", PTNat), + ("★", PTStar) +] + +piTokenMap : TokenMap PiToken +piTokenMap = (spaces, Tok PTIgnore) :: + [(identifier, \s => + case lookup s keywords of + (Just kind) => Tok kind s + Nothing => Tok PTIdentifier s + ) + ] + +lexPi : String -> Maybe (List (WithBounds PiToken)) +lexPi str = + case lex piTokenMap str of + (tokens, _, _, "") => Just tokens + _ => Nothing + +{- Basic idea, parsing has a list of the identifiers to convert to -} +{- de bruijn indecies, and a Nat to keep track of context size -} +mutual + expr : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + expr n env = ttopind n env + <|> tbotind n env + <|> tsuc n env + <|> tnatind n env + <|> tsigind n env + <|> (do + t <- term n env + tapp n env t <|> pure t) + + term : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + term n env = ttype + <|> ttop + <|> tstar + <|> tbot + <|> tnat + <|> tzero + <|> tsigma n env + <|> tpair n env + <|> tlet n env + <|> tlam n env + <|> tpi n env + <|> tvar n env + <|> paren n env + + ttype : Grammar state PiToken True (Term n) + ttype = match PTType >> pure TType + + ttop : Grammar state PiToken True (Term n) + ttop = match PTTop >> pure TTop + + tstar : Grammar state PiToken True (Term n) + tstar = match PTStar >> pure TStar + + ttopind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + ttopind n env = do + match PTTopInd + commit + c <- term n env + st <- term n env + pure (TTopInd c st) + + tbot : Grammar state PiToken True (Term n) + tbot = match PTBot >> pure TBot + + tbotind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tbotind n env = do + match PTBotInd + commit + c <- term n env + pure (TBotInd c) + + tnat : Grammar state PiToken True (Term n) + tnat = match PTNat >> pure TNat + + tzero : Grammar state PiToken True (Term n) + tzero = match PTZero >> pure TZero + + tsuc : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tsuc n env = do + match PTSuc + commit + m <- term n env + pure (TSuc m) + + tnatind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tnatind n env = do + match PTNatInd + commit + c <- term n env + z <- term n env + s <- term n env + pure (TNatInd c z s) + + tsigma : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tsigma n env = do + match PTSigma + commit + match PTLParen + arg <- match PTIdentifier + match PTColon + a <- term n env + match PTRParen + b <- term (S n) (arg :: env) + pure (TSigma a (TLam b)) + + tpair : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tpair n env = do + match PTLParen + commit + x <- expr n env + match PTComma + y <- expr n env + match PTRParen + pure (TPair x y) + + tsigind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tsigind n env = do + match PTSigInd + commit + a <- term n env + b <- term n env + c <- term n env + f <- term n env + pure (TSigInd a b c f) + + tlet : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tlet n env = do + match PTLet + commit + arg <- match PTIdentifier + match PTColon + ty <- expr n env + match PTDefEq + tr <- expr n env + match PTIn + tri <- expr (S n) (arg :: env) + pure (TLet ty tr tri) + + tlam : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tlam n env = do + match PTLambda + commit + arg <- match PTIdentifier + match PTDot + e <- term (S n) (arg :: env) + pure (TLam e) + + tpi : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tpi n env = do + match PTPi + commit + match PTLParen + arg <- match PTIdentifier + match PTColon + a <- term n env + match PTRParen + b <- term (S n) (arg :: env) + pure (TPi a b) + + tapp : (n : Nat) -> Vect n String -> Term n -> Grammar state PiToken True (Term n) + tapp n env e1 = do + e2 <- term n env + tapp1 n env (TApp e1 e2) + + tapp1 : (n : Nat) -> Vect n String -> Term n -> Grammar state PiToken False (Term n) + tapp1 n env e = tapp n env e <|> pure e + + tvar : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tvar n env = do + str <- match PTIdentifier + fromMaybe (fail ("'" ++ str ++ "' not in env")) (pure . TVar <$> findIndex (== str) env) + + paren : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + paren n env = do + match PTLParen + e <- expr n env + match PTRParen + pure e + +parsePi : (n : Nat) -> Vect n String -> List (WithBounds PiToken) -> Either String (Term n) +parsePi n env toks = + case parse (expr n env) $ filter (not . ignored) toks of + Right (l, []) => Right l + Right e => Left "contains tokens that were not consumed" + Left e => (Left . show . map getErr) e + where + getErr : ParsingError tok -> String + getErr (Error s _) = s + + +public export +parse : (n : Nat) -> Vect n String -> String -> Either String (Term n) +parse n env x = + case lexPi x of + Just toks => parsePi n env toks + Nothing => Left "Failed to lex." + +public export +parse0 : String -> Either String (Term 0) +parse0 = parse 0 []