From 8e85d97b7f1252f8993e074595f4bd5d1cdb2736 Mon Sep 17 00:00:00 2001 From: depsterr Date: Tue, 26 Jul 2022 01:11:44 +0200 Subject: [PATCH] parser is now useable for tests n stuff --- makefile | 6 +++- src/Main.idr | 48 +++++++++++++++++++--------- src/Parser/Parse.idr | 74 ++++++++++++++++++++++++-------------------- tests/projections.pi | 5 +++ 4 files changed, 84 insertions(+), 49 deletions(-) create mode 100644 tests/projections.pi diff --git a/makefile b/makefile index 28d688b..41a516b 100644 --- a/makefile +++ b/makefile @@ -1,3 +1,7 @@ -.PHONY: all +.PHONY: all run all: idris2 --build pi.ipkg +run: + ./build/exec/pi +test: + for file in ./tests/*; do ./build/exec/pi $$file; done diff --git a/src/Main.idr b/src/Main.idr index 9bd92c3..4cd4f12 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -4,24 +4,42 @@ import Core.Check import Core.Term import Parser.Parse +import Data.Vect +import Data.String import System import System.File -ioStr : IO String -ioStr = getArgs >>= \case - [] => getLine - (x :: _) => do - r <- readFile x - case r of - Left e => do - print e - exitFailure - Right s => pure s +unwrap : {a : Type} -> Show a => Either a b -> IO b +unwrap {a = a} = \case + Left e => do + case a of + String => putStrLn e + _ => printLn e + exitFailure + Right s => pure s +replRead : IO String +replRead = do + line <- getLine + if null (trim line) + then replRead + else case line of + ":exit" => exitSuccess + _ => pure line + +repl : (n : Nat) -> Vect n String -> IO () +repl n env = do + line <- replRead + printLn =<< unwrap (parseEnv n env line) + repl n env main : IO () -main = do - str <- ioStr - case parse0 str of - Left e => putStrLn e - Right t => print t +main = getArgs >>= \case + (_ :: x :: _) => do + res <- readFile x >>= unwrap >>= unwrap . parsetoplevel + >>= unwrap . (`typecheck` TTop) + putStr (x ++ ": ") + if fst res + then putStrLn ("Success !") + else unwrap (Left res) + _ => repl 0 [] diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr index 5903d7c..8e30466 100644 --- a/src/Parser/Parse.idr +++ b/src/Parser/Parse.idr @@ -192,13 +192,13 @@ lexPi str = {- 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 : Nat) -> Vect n String -> Grammar () PiToken True (Term n) expr n env = tpi n env <|> tsigma n env <|> tarr n env <|> expr1 n env - expr1 : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + expr1 : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) expr1 n env = ttopind n env <|> tbotind n env <|> tsuc n env @@ -208,7 +208,7 @@ mutual t <- term n env tapp n env t <|> pure t) - term : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + term : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) term n env = ttype <|> ttop <|> tstar @@ -221,16 +221,16 @@ mutual <|> tvar n env <|> paren n env - ttype : Grammar state PiToken True (Term n) + ttype : Grammar () PiToken True (Term n) ttype = match PTType >> pure TType - ttop : Grammar state PiToken True (Term n) + ttop : Grammar () PiToken True (Term n) ttop = match PTTop >> pure TTop - tstar : Grammar state PiToken True (Term n) + tstar : Grammar () PiToken True (Term n) tstar = match PTStar >> pure TStar - ttopind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + ttopind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) ttopind n env = do match PTTopInd commit @@ -238,30 +238,30 @@ mutual st <- term n env pure (TTopInd c st) - tbot : Grammar state PiToken True (Term n) + tbot : Grammar () PiToken True (Term n) tbot = match PTBot >> pure TBot - tbotind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tbotind : (n : Nat) -> Vect n String -> Grammar () 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 : Grammar () PiToken True (Term n) tnat = match PTNat >> pure TNat - tzero : Grammar state PiToken True (Term n) + tzero : Grammar () PiToken True (Term n) tzero = match PTZero >> pure TZero - tsuc : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tsuc : (n : Nat) -> Vect n String -> Grammar () 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 : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tnatind n env = do match PTNatInd commit @@ -270,7 +270,7 @@ mutual s <- term n env pure (TNatInd c z s) - tsigma : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tsigma : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tsigma n env = do match PTSigma commit @@ -282,7 +282,7 @@ mutual b <- expr (S n) (arg :: env) pure (TSigma a (TLam b)) - tpair : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tpair : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tpair n env = do match PTLParen x <- expr n env @@ -292,7 +292,7 @@ mutual match PTRParen pure (TPair x y) - tsigind : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tsigind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tsigind n env = do match PTSigInd commit @@ -302,7 +302,7 @@ mutual f <- term n env pure (TSigInd a b c f) - tlet : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tlet : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tlet n env = do match PTLet commit @@ -315,7 +315,7 @@ mutual 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 : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tlam n env = do match PTLambda commit @@ -324,7 +324,7 @@ mutual e <- expr (S n) (arg :: env) pure (TLam e) - tpi : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tpi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tpi n env = do match PTPi commit @@ -336,7 +336,7 @@ mutual b <- expr (S n) (arg :: env) pure (TPi a b) - tarr : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tarr : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) tarr n env = do l <- expr1 n env match PTArrow @@ -344,20 +344,20 @@ mutual r <- expr (S n) ("" :: env) pure (TPi l r) - tapp : (n : Nat) -> Vect n String -> Term n -> Grammar state PiToken True (Term n) + tapp : (n : Nat) -> Vect n String -> Term n -> Grammar () 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 : Nat) -> Vect n String -> Term n -> Grammar () 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 : Nat) -> Vect n String -> Grammar () 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 : Nat) -> Vect n String -> Grammar () PiToken True (Term n) paren n env = do match PTLParen commit @@ -365,7 +365,7 @@ mutual match PTRParen pure e -definitions : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) +definitions : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) definitions n env = do match PTLet commit @@ -377,12 +377,12 @@ definitions n env = do next <- definitions (S n) (arg :: env) <|> pure TStar pure (TLet ty tr next) -toplevel : Grammar state PiToken True (Term 0) +toplevel : Grammar () PiToken True (Term 0) toplevel = definitions 0 [] -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 +parsePi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> List (WithBounds PiToken) -> Either String (Term n) +parsePi n env parseEntry toks = + case parse parseEntry $ 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 @@ -392,12 +392,20 @@ parsePi n env toks = public export -parse : (n : Nat) -> Vect n String -> String -> Either String (Term n) -parse n env x = +parse : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> String -> Either String (Term n) +parse n env parseEntry x = case lexPi x of - Just toks => parsePi n env toks + Just toks => parsePi n env parseEntry toks Nothing => Left "Failed to lex." public export parse0 : String -> Either String (Term 0) -parse0 = parse 0 [] +parse0 = parse 0 [] (expr 0 []) + +public export +parseEnv : (n : Nat) -> Vect n String -> String -> Either String (Term n) +parseEnv n env = parse n env (expr n env) + +public export +parsetoplevel : String -> Either String (Term 0) +parsetoplevel = parse 0 [] (toplevel) diff --git a/tests/projections.pi b/tests/projections.pi new file mode 100644 index 0000000..e8e21c6 --- /dev/null +++ b/tests/projections.pi @@ -0,0 +1,5 @@ +let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A + ≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a) + +let pr2 : Π (A : Type) Π (B : A → Type) Π (s : Σ (a : A) B a) B (pr1 A B s) + ≔ λA.λB. Σ-ind A B (λs. B (pr1 A B s)) (λa.λBa. Ba)