From cc5755c3a91055b3d9fb01f0281440945cb63e13 Mon Sep 17 00:00:00 2001 From: Martin Fredin Date: Mon, 3 Apr 2023 09:24:13 +0200 Subject: [PATCH] Add layout grammar --- Grammar.cf | 10 +- Makefile | 6 +- language.cabal | 3 + src/Main.hs | 76 +++++------ tests/TestTypeCheckerBidir.hs | 236 ++++++++++++++++------------------ 5 files changed, 155 insertions(+), 176 deletions(-) diff --git a/Grammar.cf b/Grammar.cf index 55763f4..586140c 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -37,7 +37,6 @@ internal MkTEVar. TEVar ::= LIdent; Data. Data ::= "data" Type "where" "{" [Inj] "}" ; Inj. Inj ::= UIdent ":" Type ; -separator nonempty Inj " " ; ------------------------------------------------------------------------------- -- * Expressions @@ -76,8 +75,13 @@ PInj. Pattern ::= UIdent [Pattern1]; -- * AUX ------------------------------------------------------------------------------- -terminator Def ";"; -terminator Branch ";" ; +layout "of", "where", "let"; +layout stop "in"; +layout toplevel; + +separator Def ";"; +separator Branch ";" ; +separator Inj ";"; separator LIdent ""; separator Type " "; diff --git a/Makefile b/Makefile index d5c908c..bba98b0 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ language : src/Grammar/Test cabal install --installdir=. --overwrite-policy=always -src/Grammar/Test.hs src/Grammar/Lex.x src/Grammar/Par.y : Grammar.cf +src/Grammar/Test.hs src/Grammar/Lex.x src/Grammar/Par.y src/Grammar/Layout : Grammar.cf bnfc -o src -d $< src/Grammar/Par.hs : src/Grammar/Par.y @@ -15,8 +15,8 @@ src/Grammar/Lex.hs : src/Grammar/Lex.x src/Grammar/%.y : Grammar.cf bnfc -o src -d $< -src/Grammar/Test : src/Grammar/Test.hs src/Grammar/Par.hs src/Grammar/Lex.hs - ghc src/Grammar/Test.hs src/Grammar/Par.hs src/Grammar/Lex.hs src/Grammar/Abs.hs src/Grammar/Skel.hs src/Grammar/Print.hs -o src/Grammar/test +src/Grammar/Test : src/Grammar/Test.hs src/Grammar/Par.hs src/Grammar/Lex.hs src/Grammar/Layout + ghc src/Grammar/Test.hs src/Grammar/Par.hs src/Grammar/Lex.hs src/Grammar/Abs.hs src/Grammar/Skel.hs src/Grammar/Print.hs src/Grammar/Layout -o src/Grammar/test clean : rm -r src/Grammar diff --git a/language.cabal b/language.cabal index 1c54e3f..82e1492 100644 --- a/language.cabal +++ b/language.cabal @@ -30,6 +30,8 @@ executable language Grammar.Print Grammar.Skel Grammar.ErrM + Grammar.ErrM + Grammar.Layout Auxiliary Renamer.Renamer TypeChecker.TypeChecker @@ -82,6 +84,7 @@ Test-suite language-testsuite Grammar.Print Grammar.Skel Grammar.ErrM + Grammar.Layout Auxiliary Monomorphizer.Monomorphizer Monomorphizer.MonomorphizerIr diff --git a/src/Main.hs b/src/Main.hs index a6337bf..3e21803 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -2,44 +2,36 @@ module Main where -import Codegen.Codegen (generateCode) -import Compiler (compile) -import Control.Monad (when) -import Data.Bool (bool) -import Data.List.Extra (isSuffixOf) -import Data.Maybe (fromJust, isNothing) -import Desugar.Desugar (desugar) -import GHC.IO.Handle.Text (hPutStrLn) -import Grammar.ErrM (Err) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import LambdaLifter (lambdaLift) -import Monomorphizer.Monomorphizer (monomorphize) -import Renamer.Renamer (rename) -import System.Console.GetOpt ( - ArgDescr (NoArg, ReqArg), - ArgOrder (RequireOrder), - OptDescr (Option), - getOpt, - usageInfo, - ) -import System.Directory ( - createDirectory, - doesPathExist, - getDirectoryContents, - removeDirectoryRecursive, - setCurrentDirectory, - ) -import System.Environment (getArgs) -import System.Exit ( - ExitCode (ExitFailure), - exitFailure, - exitSuccess, - exitWith, - ) -import System.IO (stderr) -import System.Process (spawnCommand, waitForProcess) -import TypeChecker.TypeChecker (TypeChecker (Bi, Hm), typecheck) +import Codegen.Codegen (generateCode) +import Compiler (compile) +import Control.Monad (when) +import Data.Bool (bool) +import Data.List.Extra (isSuffixOf) +import Data.Maybe (fromJust, isNothing) +import Desugar.Desugar (desugar) +import GHC.IO.Handle.Text (hPutStrLn) +import Grammar.ErrM (Err) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import LambdaLifter (lambdaLift) +import Monomorphizer.Monomorphizer (monomorphize) +import Renamer.Renamer (rename) +import System.Console.GetOpt (ArgDescr (NoArg, ReqArg), + ArgOrder (RequireOrder), + OptDescr (Option), getOpt, + usageInfo) +import System.Directory (createDirectory, doesPathExist, + getDirectoryContents, + removeDirectoryRecursive, + setCurrentDirectory) +import System.Environment (getArgs) +import System.Exit (ExitCode (ExitFailure), + exitFailure, exitSuccess, + exitWith) +import System.IO (stderr) +import System.Process (spawnCommand, waitForProcess) +import TypeChecker.TypeChecker (TypeChecker (Bi, Hm), typecheck) main :: IO () main = getArgs >>= parseArgs >>= uncurry main' @@ -86,11 +78,11 @@ chooseTypechecker s options = options{typechecker = tc} tc = case s of "hm" -> pure Hm "bi" -> pure Bi - _ -> Nothing + _ -> Nothing data Options = Options - { help :: Bool - , debug :: Bool + { help :: Bool + , debug :: Bool , typechecker :: Maybe TypeChecker } @@ -99,7 +91,7 @@ main' opts s = do file <- readFile s printToErr "-- Parse Tree -- " - parsed <- fromSyntaxErr . pProgram $ myLexer file + parsed <- fromSyntaxErr . pProgram . resolveLayout True $ myLexer file bool (printToErr $ printTree parsed) (printToErr $ show parsed) opts.debug printToErr "-- Desugar --" diff --git a/tests/TestTypeCheckerBidir.hs b/tests/TestTypeCheckerBidir.hs index 5e1d5b1..33d7575 100644 --- a/tests/TestTypeCheckerBidir.hs +++ b/tests/TestTypeCheckerBidir.hs @@ -10,6 +10,7 @@ import Test.Hspec import Control.Monad ((<=<)) import Grammar.ErrM (Err, pattern Bad, pattern Ok) +import Grammar.Layout (resolveLayout) import Grammar.Par (myLexer, pProgram) import Renamer.Renamer (rename) import TypeChecker.RemoveTEVar (RemoveTEVar (rmTEVar)) @@ -38,52 +39,52 @@ testTypeCheckerBidir = describe "Bidirectional type checker test" $ do tc_id = specify "Basic identity function polymorphism" $ run - [ "id : forall a. a -> a;" - , "id x = x;" - , "main = id 4;" + [ "id : forall a. a -> a" + , "id x = x" + , "main = id 4" ] `shouldSatisfy` ok tc_double = specify "Addition inference" $ run - ["double x = x + x;"] + ["double x = x + x"] `shouldSatisfy` ok tc_add_lam = specify "Addition lambda inference" $ run - ["four = (\\x. x + x) 2;"] + ["four = (\\x. x + x) 2"] `shouldSatisfy` ok tc_const = specify "Basic polymorphism with multiple type variables" $ run - [ "const : forall a. forall b. a -> b -> a;" - , "const x y = x;" - , "main = const 'a' 65;" + [ "const : forall a. forall b. a -> b -> a" + , "const x y = x" + , "main = const 'a' 65" ] `shouldSatisfy` ok tc_simple_rank2 = specify "Simple rank two polymorphism" $ run - [ "id : forall a. a -> a;" - , "id x = x;" - , "f : forall a. a -> (forall b. b -> b) -> a;" - , "f x g = g x;" - , "main = f 4 id;" + [ "id : forall a. a -> a" + , "id x = x" + , "f : forall a. a -> (forall b. b -> b) -> a" + , "f x g = g x" + , "main = f 4 id" ] `shouldSatisfy` ok tc_rank2 = specify "Rank two polymorphism is ok" $ run - [ "const : forall a. forall b. a -> b -> a;" - , "const x y = x;" - , "rank2 : forall a. forall b. a -> (forall c. c -> Int) -> b -> Int;" - , "rank2 x f y = f x + f y;" - , "main = rank2 3 (\\x. const 5 x : forall a. a -> Int) 'h';" + [ "const : forall a. forall b. a -> b -> a" + , "const x y = x" + , "rank2 : forall a. forall b. a -> (forall c. c -> Int) -> b -> Int" + , "rank2 x f y = f x + f y" + , "main = rank2 3 (\\x. const 5 x : forall a. a -> Int) 'h'" ] `shouldSatisfy` ok @@ -92,20 +93,20 @@ tc_identity = describe "(∀b. b → b) should only accept the identity function specify "identity is accepted" $ run (fs ++ id) `shouldSatisfy` ok where fs = - [ "f : forall a. a -> (forall b. b -> b) -> a;" - , "f x g = g x;" - , "id : forall a. a -> a;" - , "id x = x;" - , "id_int : Int -> Int;" - , "id_int x = x;" + [ "f : forall a. a -> (forall b. b -> b) -> a" + , "f x g = g x" + , "id : forall a. a -> a" + , "id x = x" + , "id_int : Int -> Int" + , "id_int x = x" ] id = - [ "main : Int;" - , "main = f 4 id;" + [ "main : Int" + , "main = f 4 id" ] id_int = - [ "main : Int;" - , "main = f 4 id_int;" + [ "main : Int" + , "main = f 4 id_int" ] tc_pair = describe "Pair. Type variables in Pair a b typechecked" $ do @@ -113,26 +114,24 @@ tc_pair = describe "Pair. Type variables in Pair a b typechecked" $ do specify "Correct arguments are accepted" $ run (fs ++ correct) `shouldSatisfy` ok where fs = - [ "data forall a. forall b. Pair (a b) where {" + [ "data forall a. forall b. Pair (a b) where" , " Pair : a -> b -> Pair (a b)" - , "};" - , "main : Pair (Int Char);" + , "main : Pair (Int Char)" ] - wrong = ["main = Pair 'a' 65;"] - correct = ["main = Pair 65 'a';"] + wrong = ["main = Pair 'a' 65"] + correct = ["main = Pair 65 'a'"] tc_tree = describe "Tree. Recursive data type" $ do specify "Wrong tree is rejected" $ run (fs ++ wrong) `shouldNotSatisfy` ok specify "Correct tree is accepted" $ run (fs ++ correct) `shouldSatisfy` ok where fs = - [ "data forall a. Tree (a) where {" + [ "data forall a. Tree (a) where" , " Node : a -> Tree (a) -> Tree (a) -> Tree (a)" , " Leaf : a -> Tree (a)" - , "};" ] - wrong = ["tree = Node 1 (Node 2 (Node 4) (Leaf 5)) (Leaf 3);"] - correct = ["tree = Node 1 (Node 2 (Leaf 4) (Leaf 5)) (Leaf 3);"] + wrong = ["tree = Node 1 (Node 2 (Node 4) (Leaf 5)) (Leaf 3)"] + correct = ["tree = Node 1 (Node 2 (Leaf 4) (Leaf 5)) (Leaf 3)"] tc_mono_case = describe "Monomorphic pattern matching" $ do specify "First wrong case expression rejected" $ @@ -147,39 +146,34 @@ tc_mono_case = describe "Monomorphic pattern matching" $ do run correct2 `shouldSatisfy` ok where wrong1 = - [ "simple : Int -> Int;" - , "simple c = case c of {" - , " 'F' => 0;" - , " 'T' => 1;" - , "};" + [ "simple : Int -> Int" + , "simple c = case c of" + , " 'F' => 0" + , " 'T' => 1" ] wrong2 = - [ "simple : Char -> Int;" - , "simple c = case c of {" - , " 'F' => 0;" - , " 1 => 1;" - , "};" + [ "simple : Char -> Int" + , "simple c = case c of" + , " 'F' => 0" + , " 1 => 1" ] wrong3 = - [ "simple : Char -> Int;" - , "simple c = case c of {" - , " 'F' => 0;" - , " 'T' => '1';" - , "};" + [ "simple : Char -> Int" + , "simple c = case c of" + , " 'F' => 0" + , " 'T' => '1'" ] correct1 = - [ "simple : Char -> Int;" - , "simple c = case c of {" - , " 'F' => 0;" - , " 'T' => 1;" - , "};" + [ "simple : Char -> Int" + , "simple c = case c of" + , " 'F' => 0" + , " 'T' => 1" ] correct2 = - [ "simple : Char -> Int;" - , "simple c = case c of {" - , " 'F' => 0;" - , " _ => 1;" - , "};" + [ "simple : Char -> Int" + , "simple c = case c of" + , " 'F' => 0" + , " _ => 1" ] tc_pol_case = describe "Polymophic and recursive pattern matching" $ do @@ -201,72 +195,63 @@ tc_pol_case = describe "Polymophic and recursive pattern matching" $ do run (fs ++ correct4) `shouldSatisfy` ok where fs = - [ "data forall a. List (a) where {" + [ "data forall a. List (a) where" , " Nil : List (a)" , " Cons : a -> List (a) -> List (a)" - , "};" ] wrong1 = - [ "length : forall c. List (c) -> Int;" - , "length = \\list. case list of {" - , " Nil => 0;" - , " Cons 6 xs => 1 + length xs;" - , "};" + [ "length : forall c. List (c) -> Int" + , "length = \\list. case list of" + , " Nil => 0" + , " Cons 6 xs => 1 + length xs" ] wrong2 = - [ "length : forall c. List (c) -> Int;" - , "length = \\list. case list of {" - , " Cons => 0;" - , " Cons x xs => 1 + length xs;" - , "};" + [ "length : forall c. List (c) -> Int" + , "length = \\list. case list of" + , " Cons => 0" + , " Cons x xs => 1 + length xs" ] wrong3 = - [ "length : forall c. List (c) -> Int;" - , "length = \\list. case list of {" - , " 0 => 0;" - , " Cons x xs => 1 + length xs;" - , "};" + [ "length : forall c. List (c) -> Int" + , "length = \\list. case list of" + , " 0 => 0" + , " Cons x xs => 1 + length xs" ] wrong4 = - [ "elems : forall c. List (List(c)) -> Int;" - , "elems = \\list. case list of {" - , " Nil => 0;" - , " Cons Nil Nil => 0;" - , " Cons Nil xs => elems xs;" - , " Cons (Cons Nil ys) xs => 1 + elems (Cons ys xs);" - , "};" + [ "elems : forall c. List (List(c)) -> Int" + , "elems = \\list. case list of" + , " Nil => 0" + , " Cons Nil Nil => 0" + , " Cons Nil xs => elems xs" + , " Cons (Cons Nil ys) xs => 1 + elems (Cons ys xs)" ] correct1 = - [ "length : forall c. List (c) -> Int;" - , "length = \\list. case list of {" - , " Nil => 0;" - , " Cons x xs => 1 + length xs;" - , " Cons x (Cons y Nil) => 2;" - , "};" + [ "length : forall c. List (c) -> Int" + , "length = \\list. case list of" + , " Nil => 0" + , " Cons x xs => 1 + length xs" + , " Cons x (Cons y Nil) => 2" ] correct2 = - [ "length : forall c. List (c) -> Int;" - , "length = \\list. case list of {" - , " Nil => 0;" - , " non_empty => 1;" - , "};" + [ "length : forall c. List (c) -> Int" + , "length = \\list. case list of" + , " Nil => 0" + , " non_empty => 1" ] correct3 = - [ "length : List (Int) -> Int;" - , "length = \\list. case list of {" - , " Nil => 0;" - , " Cons 1 Nil => 1;" - , " Cons x (Cons 2 xs) => 2 + length xs;" - , "};" + [ "length : List (Int) -> Int" + , "length = \\list. case list of" + , " Nil => 0" + , " Cons 1 Nil => 1" + , " Cons x (Cons 2 xs) => 2 + length xs" ] correct4 = - [ "elems : forall c. List (List(c)) -> Int;" - , "elems = \\list. case list of {" - , " Nil => 0;" - , " Cons Nil Nil => 0;" - , " Cons Nil xs => elems xs;" - , " Cons (Cons _ ys) xs => 1 + elems (Cons ys xs);" - , "};" + [ "elems : forall c. List (List(c)) -> Int" + , "elems = \\list. case list of" + , " Nil => 0" + , " Cons Nil Nil => 0" + , " Cons Nil xs => elems xs" + , " Cons (Cons _ ys) xs => 1 + elems (Cons ys xs)" ] @@ -277,44 +262,39 @@ tc_infer_case = describe "Infer case expression" $ do run (fs ++ correct) `shouldSatisfy` ok where fs = - [ "data Bool () where {" + [ "data Bool () where" , " True : Bool ()" , " False : Bool ()" - , "};" ] correct = - [ "toBool = case 0 of {" - , " 0 => False;" - , " _ => True;" - , "};" + [ "toBool = case 0 of" + , " 0 => False" + , " _ => True" ] wrong = - [ "toBool = case 0 of {" - , " 0 => False;" - , " _ => 1;" - , "};" + [ "toBool = case 0 of" + , " 0 => False" + , " _ => 1" ] tc_rec1 = specify "Infer simple recursive definition" $ - run ["test x = 1 + test (x + 1);"] `shouldSatisfy` ok + run ["test x = 1 + test (x + 1)"] `shouldSatisfy` ok tc_rec2 = specify "Infer recursive definition with pattern matching" $ run - [ "data Bool () where {" + [ "data Bool () where" , " False : Bool ()" , " True : Bool ()" - , "};" - , "test = \\x. case x of {" - , " 10 => True;" - , " _ => test (x+1);" - , "};" + , "test = \\x. case x of" + , " 10 => True" + , " _ => test (x+1)" ] `shouldSatisfy` ok run :: [String] -> Err T.Program -run = rmTEVar <=< typecheck <=< pProgram . myLexer . unlines +run = rmTEVar <=< typecheck <=< pProgram . resolveLayout True . myLexer . unlines ok = \case Ok _ -> True