diff --git a/Grammar.cf b/Grammar.cf index 46795f2..da40cbc 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -22,12 +22,14 @@ internal Bind. Bind ::= LIdent [LIdent] "=" Exp; -- * Types ------------------------------------------------------------------------------- - TLit. Type1 ::= UIdent; -- τ - TVar. Type1 ::= TVar; -- α -internal TEVar. Type1 ::= TEVar; -- ά - TData. Type1 ::= UIdent "(" [Type] ")"; -- D () - TFun. Type ::= Type1 "->" Type; -- A → A +internal TLit. Type3 ::= UIdent; -- τ + TIdent. Type3 ::= UIdent; + TVar. Type3 ::= TVar; -- α + TApp. Type2 ::= Type2 Type3 ; + TFun. Type1 ::= Type1 "->" Type; -- A → A TAll. Type ::= "forall" TVar "." Type; -- ∀α. A +internal TEVar. Type1 ::= TEVar; -- ά +internal TData. Type1 ::= UIdent "(" [Type] ")"; -- D () MkTVar. TVar ::= LIdent; internal MkTEVar. TEVar ::= LIdent; @@ -98,7 +100,7 @@ separator nonempty Pattern1 " "; coercions Pattern 1; coercions Exp 4; -coercions Type 1 ; +coercions Type 3 ; token UIdent (upper (letter | digit | '_')*) ; token LIdent (lower (letter | digit | '_')*) ; diff --git a/src/Desugar/Desugar.hs b/src/Desugar/Desugar.hs index 14abef1..02eb4d9 100644 --- a/src/Desugar/Desugar.hs +++ b/src/Desugar/Desugar.hs @@ -1,9 +1,12 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} -module Desugar.Desugar where +module Desugar.Desugar (desugar) where import Data.Function (on) +import Debug.Trace (traceShow) import Grammar.Abs +import Grammar.Print {- @@ -37,7 +40,25 @@ desugarData :: Data -> Data desugarData (Data typ injs) = Data (desugarType typ) (map desugarInj injs) desugarType :: Type -> Type -desugarType t = t +desugarType = \case + TIdent (UIdent "Int") -> TLit "Int" + TIdent (UIdent "Char") -> TLit "Char" + TIdent ident -> TData ident [] + TApp t1 t2 -> + let (name : tvars) = flatten t1 ++ [t2] + in case name of + TIdent ident -> TData ident (map desugarType tvars) + _ -> error "desugarType in Desugar.hs is not implemented correctly" + TLit l -> TLit l + TVar v -> TVar v + (TAll i t) -> TAll i (desugarType t) + TFun t1 t2 -> TFun (desugarType t1) (desugarType t2) + TEVar v -> TEVar v + TData ident typ -> TData ident (map desugarType typ) + where + flatten :: Type -> [Type] + flatten (TApp a b) = flatten a <> flatten b + flatten a = [a] desugarInj :: Inj -> Inj desugarInj (Inj ident typ) = Inj ident (desugarType typ) diff --git a/src/Main.hs b/src/Main.hs index 0e2e5c0..6088a7c 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -2,38 +2,47 @@ module Main where -import AnnForall (annotateForall) -import Codegen.Codegen (generateCode) -import Compiler (compile) -import Control.Monad (when, (<=<)) -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 (Print, printTree) -import LambdaLifter (lambdaLift) -import Monomorphizer.Monomorphizer (monomorphize) -import OrderDefs (orderDefs) -import Renamer.Renamer (rename) -import ReportForall (reportForall) -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 AnnForall (annotateForall) +import Codegen.Codegen (generateCode) +import Compiler (compile) +import Control.Monad (when, (<=<)) +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 (Print, printTree) +import LambdaLifter (lambdaLift) +import Monomorphizer.Monomorphizer (monomorphize) +import OrderDefs (orderDefs) +import Renamer.Renamer (rename) +import ReportForall (reportForall) +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' @@ -85,12 +94,12 @@ 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 - , gc :: Bool + { help :: Bool + , debug :: Bool + , gc :: Bool , typechecker :: Maybe TypeChecker } @@ -169,12 +178,12 @@ prelude :: String prelude = unlines [ "\n" - --, "customHelperFunctionCuzPoorImplementation : Bool () -> Int -> Bool ()" - --, "customHelperFunctionCuzPoorImplementation x y = x" - , "data Bool () where" - , " False : Bool ()" - , " True : Bool ()" - , "lt : Int -> Int -> Bool ()" + , -- , "customHelperFunctionCuzPoorImplementation : Bool () -> Int -> Bool ()" + -- , "customHelperFunctionCuzPoorImplementation x y = x" + "data Bool where" + , " False : Bool" + , " True : Bool" + , "lt : Int -> Int -> Bool" , "lt x y = True" , "\n" ] diff --git a/test_program.crf b/test_program.crf index 435a071..5f35a1d 100644 --- a/test_program.crf +++ b/test_program.crf @@ -1,23 +1,15 @@ -data List (a) where { - Nil : List (a) - Cons : a -> List (a) -> List (a) -}; +data List a where + Cons : a -> List a -> List a + Nil : List a -main = length (Cons 1 (Cons 2 Nil)) ; -id x = x; -const x y = x ; +.++ xs ys = case xs of + Nil => ys + Cons z zs => Cons z (zs ++ ys) -map : (o -> g) -> List (o) -> List (g) ; -map f xs = case xs of { - Nil => Nil ; - Cons x xs => Cons (f x) (map f xs) ; -}; +length xs = case xs of + Cons x xs => 1 + length xs -length : List (Int) -> Int ; -length xs = case xs of { - Nil => 0 ; - Cons _ xs => 1 + length xs ; -}; +main = length (list1 ++ list2) -id_int : a -> b ; -id_int x = (x : a) ; +list1 = Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil))) +list2 = Cons 4 (Cons 5 (Cons 6 (Cons 7 Nil))) diff --git a/tests/TestAnnForall.hs b/tests/TestAnnForall.hs index 98776fe..9280f33 100644 --- a/tests/TestAnnForall.hs +++ b/tests/TestAnnForall.hs @@ -1,97 +1,112 @@ {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QualifiedDo #-} {-# HLINT ignore "Use camelCase" #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# LANGUAGE QualifiedDo #-} module TestAnnForall (testAnnForall, test) where -import AnnForall (annotateForall) -import Control.Monad ((<=<)) -import qualified DoStrings as D -import Grammar.ErrM (Err, pattern Bad, pattern Ok) -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import Renamer.Renamer (rename) -import ReportForall (reportForall) -import Test.Hspec (describe, hspec, shouldBe, - shouldNotSatisfy, shouldSatisfy, - shouldThrow, specify) -import TypeChecker.ReportTEVar (reportTEVar) -import TypeChecker.TypeChecker (TypeChecker (Bi, Hm)) -import TypeChecker.TypeCheckerBidir (typecheck) -import qualified TypeChecker.TypeCheckerIr as T +import AnnForall (annotateForall) +import Control.Monad ((<=<)) +import Desugar.Desugar (desugar) +import DoStrings qualified as D +import Grammar.ErrM (Err, pattern Bad, pattern Ok) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import Renamer.Renamer (rename) +import ReportForall (reportForall) +import Test.Hspec ( + describe, + hspec, + shouldBe, + shouldNotSatisfy, + shouldSatisfy, + shouldThrow, + specify, + ) +import TypeChecker.ReportTEVar (reportTEVar) +import TypeChecker.TypeChecker (TypeChecker (Bi, Hm)) +import TypeChecker.TypeCheckerBidir (typecheck) +import TypeChecker.TypeCheckerIr qualified as T test = hspec testAnnForall testAnnForall = describe "Test AnnForall" $ do - ann_data1 - ann_data2 - ann_bad_data1 - ann_bad_data2 - ann_bad_data3 - ann_sig1 - ann_sig2 - ann_bind + ann_data1 + ann_data2 + ann_bad_data1 + ann_bad_data2 + ann_bad_data3 + ann_sig1 + ann_sig2 + ann_bind -ann_data1 = specify "Annotate data type" $ - D.do "data Either (a b) where" - " Left : a -> Either (a b)" - " Right : b -> Either (a b)" - `shouldBePrg` - D.do "data forall a. forall b. Either (a b) where" - " Left : a -> Either (a b)" - " Right : b -> Either (a b)" +ann_data1 = + specify "Annotate data type" $ + D.do + "data Either a b where" + " Left : a -> Either a b" + " Right : b -> Either a b" + `shouldBePrg` D.do + "data forall a. forall b. Either a b where" + " Left : a -> Either a b" + " Right : b -> Either a b" -ann_data2 = specify "Annotate constructor with additional type variable" $ - D.do "data forall a. forall b. Either (a b) where" - " Left : c -> a -> Either (a b)" - " Right : b -> Either (a b)" - `shouldBePrg` - D.do "data forall a. forall b. Either (a b) where" - " Left : forall c. c -> a -> Either (a b)" - " Right : b -> Either (a b)" +ann_data2 = + specify "Annotate constructor with additional type variable" $ + D.do + "data forall a. forall b. Either a b where" + " Left : c -> a -> Either a b" + " Right : b -> Either a b" + `shouldBePrg` D.do + "data forall a. forall b. Either a b where" + " Left : forall c. c -> a -> Either a b" + " Right : b -> Either a b" -ann_bad_data1 = specify "Bad data type variables" $ - D.do "data Either (Int b) where" - " Left : a -> Either (a b)" - " Right : b -> Either (a b)" - `shouldBeErr` - "Misformed data declaration: Non type variable argument" +ann_bad_data1 = + specify "Bad data type variables" $ + D.do + "data Either Int b where" + " Left : a -> Either a b" + " Right : b -> Either a b" + `shouldBeErr` "Misformed data declaration: Non type variable argument" -ann_bad_data2 = specify "Bad data identifer" $ - D.do "data Int -> Either (a b) where" - " Left : a -> Either (a b)" - " Right : b -> Either (a b)" - `shouldBeErr` - "Misformed data declaration" +ann_bad_data2 = + specify "Bad data identifer" $ + D.do + "data Int -> Either a b where" + " Left : a -> Either a b" + " Right : b -> Either a b" + `shouldBeErr` "Misformed data declaration" -ann_bad_data3 = specify "Constructor forall duplicate" $ - D.do "data Int -> Either (a b) where" - " Left : forall a. a -> Either (a b)" - " Right : b -> Either (a b)" - `shouldBeErr` - "Misformed data declaration" +ann_bad_data3 = + specify "Constructor forall duplicate" $ + D.do + "data Int -> Either a b where" + " Left : forall a. a -> Either a b" + " Right : b -> Either a b" + `shouldBeErr` "Misformed data declaration" +ann_sig1 = + specify "Annotate signature" $ + "f : a -> b -> (forall a. a -> a) -> a" + `shouldBePrg` "f : forall a. forall b. a -> b -> (forall a. a -> a) -> a" -ann_sig1 = specify "Annotate signature" $ - "f : a -> b -> (forall a. a -> a) -> a" - `shouldBePrg` - "f : forall a. forall b. a -> b -> (forall a. a -> a) -> a" +ann_sig2 = + specify "Annotate signature 2" $ + D.do + "const : forall a. forall b. a -> b -> a" + "const x y = x" + "main = const 'a' 65" + `shouldBePrg` D.do + "const : forall a. forall b. a -> b -> a" + "const x y = x" + "main = const 'a' 65" -ann_sig2 = specify "Annotate signature 2" $ - D.do "const : forall a. forall b. a -> b -> a" - "const x y = x" - "main = const 'a' 65" - `shouldBePrg` - D.do "const : forall a. forall b. a -> b -> a" - "const x y = x" - "main = const 'a' 65" - -ann_bind = specify "Annotate bind" $ - "f = (\\x.\\y. x : a -> b -> a) 4" - `shouldBePrg` - "f = (\\x.\\y. x : forall a. forall b. a -> b -> a) 4" +ann_bind = + specify "Annotate bind" $ + "f = (\\x.\\y. x : a -> b -> a) 4" + `shouldBePrg` "f = (\\x.\\y. x : forall a. forall b. a -> b -> a) 4" shouldBeErr s err = run s `shouldBe` Bad err @@ -104,10 +119,10 @@ run' s = do p <- run'' s reportForall Bi p pure p -run'' = pProgram . resolveLayout True . myLexer +run'' = fmap desugar . pProgram . resolveLayout True . myLexer runPrint = (putStrLn . either show printTree . run) $ - D.do "data forall a. forall b. Either (a b) where" - " Left : c -> a -> Either (a b)" - " Right : b -> Either (a b)" - + D.do + "data forall a. forall b. Either a b where" + " Left : c -> a -> Either a b" + " Right : b -> Either a b" diff --git a/tests/TestLambdaLifter.hs b/tests/TestLambdaLifter.hs index d209819..d10e7ee 100644 --- a/tests/TestLambdaLifter.hs +++ b/tests/TestLambdaLifter.hs @@ -1,35 +1,36 @@ -{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QualifiedDo #-} {-# HLINT ignore "Use camelCase" #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE QualifiedDo #-} module TestLambdaLifter where -import Test.Hspec - -import AnnForall (annotateForall) -import Control.Monad ((<=<)) -import Control.Monad.Error.Class (liftEither) -import Control.Monad.Extra (eitherM) -import Grammar.ErrM (Err, pattern Bad, pattern Ok) -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import LambdaLifter -import Renamer.Renamer (rename) -import ReportForall (reportForall) -import TypeChecker.RemoveForall (removeForall) -import TypeChecker.ReportTEVar (reportTEVar) -import TypeChecker.TypeChecker (TypeChecker (Bi)) -import TypeChecker.TypeCheckerBidir (typecheck) -import TypeChecker.TypeCheckerIr +import Test.Hspec +import AnnForall (annotateForall) +import Control.Monad ((<=<)) +import Control.Monad.Error.Class (liftEither) +import Control.Monad.Extra (eitherM) +import Desugar.Desugar (desugar) +import Grammar.ErrM (Err, pattern Bad, pattern Ok) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import LambdaLifter +import Renamer.Renamer (rename) +import ReportForall (reportForall) +import TypeChecker.RemoveForall (removeForall) +import TypeChecker.ReportTEVar (reportTEVar) +import TypeChecker.TypeChecker (TypeChecker (Bi)) +import TypeChecker.TypeCheckerBidir (typecheck) +import TypeChecker.TypeCheckerIr test = hspec testLambdaLifter testLambdaLifter = describe "Test Lambda Lifter" $ do undefined + -- frees_exp1 -- frees_exp1 = specify "Free variables 1" $ @@ -43,67 +44,63 @@ testLambdaLifter = describe "Test Lambda Lifter" $ do -- ),TVar (MkTVar (Ident "a"))) -- } - abs_1 = undefined where - input = unlines [ "data List (a) where" - , " Nil : List (a)" - , " Cons : a -> List (a) -> List (a)" - , "map : (a -> b) -> List (a) -> List (b)" - , "add : Int -> Int -> Int" - - , "f : List (Int)" - , "f = (\\x.\\ys. map (\\y. add y x) ys) 4 (Cons 1 (Cons 2 Nil))" - ] - - + input = + unlines + [ "data List a where" + , " Nil : List a" + , " Cons : a -> List a -> List a" + , "map : (a -> b) -> List a -> List b" + , "add : Int -> Int -> Int" + , "f : List Int" + , "f = (\\x.\\ys. map (\\y. add y x) ys) 4 (Cons 1 (Cons 2 Nil))" + ] runFreeVars = either putStrLn print (runFree s2) runAbstract = either putStrLn (putStrLn . printTree) (runAbs s2) runCollect = either putStrLn (putStrLn . printTree) (run s2) +s1 = + unlines + [ "add : Int -> Int -> Int" + , "f : Int -> Int -> Int" + , "f x y = add x y" + , "f = \\x. (\\y. add x y)" + ] -s1 = unlines [ "add : Int -> Int -> Int" - , "f : Int -> Int -> Int" - , "f x y = add x y" - , "f = \\x. (\\y. add x y)" - ] - -s2 = unlines [ "data List (a) where" - , " Nil : List (a)" - , " Cons : a -> List (a) -> List (a)" - , "add : Int -> Int -> Int" - , "map : (a -> b) -> List (a) -> List (b)" - -- , "map f xs = case xs of" +s2 = + unlines + [ "data List a where" + , " Nil : List (a)" + , " Cons : a -> List a -> List a" + , "add : Int -> Int -> Int" + , "map : (a -> b) -> List a -> List b" + , -- , "map f xs = case xs of" -- , " Nil => Nil" -- , " Cons x xs => Cons (f x) (map f xs)" - , "f : List (Int)" - , "f = (\\x.\\ys. map (\\y. add y x) ys) 4 (Cons 1 (Cons 2 Nil))" - ] + "f : List Int" + , "f = (\\x.\\ys. map (\\y. add y x) ys) 4 (Cons 1 (Cons 2 Nil))" + ] s3 = "main = (\\plussq. (\\f. f (f 0)) (plussq 3)) (\\x. \\y. y + x + x)" - - run = fmap collectScs . runAbs runAbs = fmap abstract . runFree runFree s = do - Program ds <- run' s - pure $ freeVars [b | DBind b <- ds] + Program ds <- run' s + pure $ freeVars [b | DBind b <- ds] -run' = fmap removeForall - . reportTEVar - <=< typecheck - <=< run'' +run' = + fmap removeForall + . reportTEVar + <=< typecheck + <=< run'' run'' s = do - p <- (pProgram . resolveLayout True . myLexer) s + p <- (fmap desugar . pProgram . resolveLayout True . myLexer) s reportForall Bi p (rename <=< annotateForall) p - - - - diff --git a/tests/TestRenamer.hs b/tests/TestRenamer.hs index acdbb87..dc71d38 100644 --- a/tests/TestRenamer.hs +++ b/tests/TestRenamer.hs @@ -1,39 +1,49 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QualifiedDo #-} {-# HLINT ignore "Use camelCase" #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE QualifiedDo #-} module TestRenamer (testRenamer, test, runPrint) where - -import AnnForall (annotateForall) -import Control.Exception (ErrorCall (ErrorCall), - Exception (displayException), - SomeException (SomeException), - evaluate, try) -import Control.Exception.Extra (try_) -import Control.Monad (unless, (<=<)) -import Control.Monad.Except (throwError) -import Data.Either.Extra (fromEither) -import qualified DoStrings as D -import GHC.Generics (Generic, Generic1) -import Grammar.Abs (Program (Program)) -import Grammar.ErrM (Err, pattern Bad, pattern Ok) -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import Renamer.Renamer (rename) -import System.IO.Error (catchIOError, tryIOError) -import Test.Hspec (anyErrorCall, anyException, - describe, hspec, shouldBe, - shouldNotSatisfy, shouldReturn, - shouldSatisfy, shouldThrow, - specify) -import TypeChecker.ReportTEVar (reportTEVar) -import TypeChecker.TypeCheckerBidir (typecheck) -import qualified TypeChecker.TypeCheckerIr as T +import AnnForall (annotateForall) +import Control.Exception ( + ErrorCall (ErrorCall), + Exception (displayException), + SomeException (SomeException), + evaluate, + try, + ) +import Control.Exception.Extra (try_) +import Control.Monad (unless, (<=<)) +import Control.Monad.Except (throwError) +import Data.Either.Extra (fromEither) +import Desugar.Desugar (desugar) +import DoStrings qualified as D +import GHC.Generics (Generic, Generic1) +import Grammar.Abs (Program (Program)) +import Grammar.ErrM (Err, pattern Bad, pattern Ok) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import Renamer.Renamer (rename) +import System.IO.Error (catchIOError, tryIOError) +import Test.Hspec ( + anyErrorCall, + anyException, + describe, + hspec, + shouldBe, + shouldNotSatisfy, + shouldReturn, + shouldSatisfy, + shouldThrow, + specify, + ) +import TypeChecker.ReportTEVar (reportTEVar) +import TypeChecker.TypeCheckerBidir (typecheck) +import TypeChecker.TypeCheckerIr qualified as T -- FIXME tests sucks @@ -47,50 +57,58 @@ testRenamer = describe "Test Renamer" $ do rn_bind2 rn_data1 = specify "Rename data type" . shouldSatisfyOk $ - D.do "data forall a. forall b. Either (a b) where" - " Left : a -> Either (a b)" - " Right : b -> Either (a b)" + D.do + "data forall a. forall b. Either a b where" + " Left : a -> Either a b" + " Right : b -> Either a b" rn_data2 = specify "Rename data type forall in constructor " . shouldSatisfyOk $ - D.do "data forall a. forall b. Either (a b) where" - " Left : forall c. c -> a -> Either (a b)" - " Right : b -> Either (a b)" + D.do + "data forall a. forall b. Either a b where" + " Left : forall c. c -> a -> Either a b" + " Right : b -> Either a b" -rn_sig = specify "Rename signature" $ shouldSatisfyOk - "f : forall a. forall b. a -> b -> (forall a. a -> a) -> a" +rn_sig = + specify "Rename signature" $ + shouldSatisfyOk + "f : forall a. forall b. a -> b -> (forall a. a -> a) -> a" -rn_bind1 = specify "Rename simple bind" $ shouldSatisfyOk - "f x = (\\y. let y2 = y + 1 in y2) (x + 1)" +rn_bind1 = + specify "Rename simple bind" $ + shouldSatisfyOk + "f x = (\\y. let y2 = y + 1 in y2) (x + 1)" rn_bind2 = specify "Rename bind with case" . shouldSatisfyOk $ - D.do "data forall a. List (a) where" - " Nil : List (a) " - " Cons : a -> List (a) -> List (a)" + D.do + "data forall a. List a where" + " Nil : List a " + " Cons : a -> List a -> List a" - "length : forall a. List (a) -> Int" - "length list = case list of" - " Nil => 0" - " Cons x Nil => 1" - " Cons x (Cons y ys) => 2 + length ys" + "length : forall a. List a -> Int" + "length list = case list of" + " Nil => 0" + " Cons x Nil => 1" + " Cons x (Cons y ys) => 2 + length ys" runPrint = putStrLn . either show printTree . run $ - D.do "data forall a. List (a) where" - " Nil : List (a) " - " Cons : a -> List (a) -> List (a)" + D.do + "data forall a. List a where" + " Nil : List a " + " Cons : a -> List a -> List a" - "length : forall a. List (a) -> Int" - "length list = case list of" - " Nil => 0" - " Cons x Nil => 1" - " Cons x (Cons y ys) => 2 + length ys" + "length : forall a. List a -> Int" + "length list = case list of" + " Nil => 0" + " Cons x Nil => 1" + " Cons x (Cons y ys) => 2 + length ys" shouldSatisfyOk s = run s `shouldSatisfy` ok ok = \case - Ok !_ -> True + Ok !_ -> True Bad !_ -> False shouldBeErr s err = run s `shouldBe` Bad err -run = rename <=< run' -run' = pProgram . resolveLayout True . myLexer +run = rename <=< run' +run' = fmap desugar . pProgram . resolveLayout True . myLexer diff --git a/tests/TestReportForall.hs b/tests/TestReportForall.hs index d4e49d7..2d3371d 100644 --- a/tests/TestReportForall.hs +++ b/tests/TestReportForall.hs @@ -4,19 +4,26 @@ module TestReportForall (testReportForall, test) where -import AnnForall (annotateForall) -import Control.Monad ((<=<)) -import qualified DoStrings as D -import Grammar.ErrM (Err, pattern Bad, pattern Ok) -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import Renamer.Renamer (rename) -import ReportForall (reportForall) -import Test.Hspec (describe, hspec, shouldBe, - shouldNotSatisfy, shouldSatisfy, - shouldThrow, specify) -import TypeChecker.TypeChecker (TypeChecker (Bi, Hm)) +import AnnForall (annotateForall) +import Control.Monad ((<=<)) +import Desugar.Desugar (desugar) +import DoStrings qualified as D +import Grammar.ErrM (Err, pattern Bad, pattern Ok) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import Renamer.Renamer (rename) +import ReportForall (reportForall) +import Test.Hspec ( + describe, + hspec, + shouldBe, + shouldNotSatisfy, + shouldSatisfy, + shouldThrow, + specify, + ) +import TypeChecker.TypeChecker (TypeChecker (Bi, Hm)) testReportForall = describe "Test ReportForall" $ do rp_unused1 @@ -25,23 +32,23 @@ testReportForall = describe "Test ReportForall" $ do test = hspec testReportForall -rp_unused1 = specify "Unused forall 1" $ - "g : forall a. forall a. a -> (forall a. a -> a) -> a" - `shouldBeErrBi` - "Unused forall" +rp_unused1 = + specify "Unused forall 1" $ + "g : forall a. forall a. a -> (forall a. a -> a) -> a" + `shouldBeErrBi` "Unused forall" -rp_unused2 = specify "Unused forall 2" $ - "g : forall a. (forall a. a -> a) -> Int" - `shouldBeErrBi` - "Unused forall" +rp_unused2 = + specify "Unused forall 2" $ + "g : forall a. (forall a. a -> a) -> Int" + `shouldBeErrBi` "Unused forall" -rp_forall = specify "Rank2 forall with Hm" $ - "f : a -> b -> (forall a. a -> a) -> a" - `shouldBeErrHm` - "Higher rank forall not allowed" +rp_forall = + specify "Rank2 forall with Hm" $ + "f : a -> b -> (forall a. a -> a) -> a" + `shouldBeErrHm` "Higher rank forall not allowed" shouldBeErrBi = shouldBeErr Bi shouldBeErrHm = shouldBeErr Hm shouldBeErr tc s err = run tc s `shouldBe` Bad err -run tc = reportForall tc <=< pProgram . resolveLayout True . myLexer +run tc = reportForall tc <=< fmap desugar . pProgram . resolveLayout True . myLexer diff --git a/tests/TestTypeCheckerBidir.hs b/tests/TestTypeCheckerBidir.hs index 916b688..15e0c1f 100644 --- a/tests/TestTypeCheckerBidir.hs +++ b/tests/TestTypeCheckerBidir.hs @@ -1,28 +1,28 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PatternSynonyms #-} {-# HLINT ignore "Use camelCase" #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} module TestTypeCheckerBidir (test, testTypeCheckerBidir) where -import Test.Hspec - -import AnnForall (annotateForall) -import Control.Monad ((<=<)) -import Grammar.Abs (Program) -import Grammar.ErrM (Err, pattern Bad, pattern Ok) -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import Renamer.Renamer (rename) -import ReportForall (reportForall) -import TypeChecker.RemoveForall (removeForall) -import TypeChecker.ReportTEVar (reportTEVar) -import TypeChecker.TypeChecker (TypeChecker (Bi)) -import TypeChecker.TypeCheckerBidir (typecheck) -import qualified TypeChecker.TypeCheckerIr as T +import Test.Hspec +import AnnForall (annotateForall) +import Control.Monad ((<=<)) +import Desugar.Desugar (desugar) +import Grammar.Abs (Program) +import Grammar.ErrM (Err, pattern Bad, pattern Ok) +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import Renamer.Renamer (rename) +import ReportForall (reportForall) +import TypeChecker.RemoveForall (removeForall) +import TypeChecker.ReportTEVar (reportTEVar) +import TypeChecker.TypeChecker (TypeChecker (Bi)) +import TypeChecker.TypeCheckerBidir (typecheck) +import TypeChecker.TypeCheckerIr qualified as T test = hspec testTypeCheckerBidir @@ -120,9 +120,9 @@ 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 Pair (a b) where" - , " Pair : a -> b -> Pair (a b)" - , "main : Pair (Int Char)" + [ "data Pair a b where" + , " Pair : a -> b -> Pair a b" + , "main : Pair Int Char" ] wrong = ["main = Pair 'a' 65"] correct = ["main = Pair 65 'a'"] @@ -132,9 +132,9 @@ tc_tree = describe "Tree. Recursive data type" $ do specify "Correct tree is accepted" $ run (fs ++ correct) `shouldSatisfy` ok where fs = - [ "data Tree (a) where" - , " Node : a -> Tree (a) -> Tree (a) -> Tree (a)" - , " Leaf : a -> Tree (a)" + [ "data 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)"] @@ -201,30 +201,30 @@ tc_pol_case = describe "Polymophic and recursive pattern matching" $ do run (fs ++ correct4) `shouldSatisfy` ok where fs = - [ "data List (a) where" - , " Nil : List (a)" - , " Cons : a -> List (a) -> List (a)" + [ "data List a where" + , " Nil : List a" + , " Cons : a -> List a -> List a" ] wrong1 = - [ "length : List (c) -> Int" + [ "length : List c -> Int" , "length = \\list. case list of" , " Nil => 0" , " Cons 6 xs => 1 + length xs" ] wrong2 = - [ "length : List (c) -> Int" + [ "length : List c -> Int" , "length = \\list. case list of" , " Cons => 0" , " Cons x xs => 1 + length xs" ] wrong3 = - [ "length : List (c) -> Int" + [ "length : List c -> Int" , "length = \\list. case list of" , " 0 => 0" , " Cons x xs => 1 + length xs" ] wrong4 = - [ "elems : List (List(c)) -> Int" + [ "elems : List (List c) -> Int" , "elems = \\list. case list of" , " Nil => 0" , " Cons Nil Nil => 0" @@ -232,27 +232,27 @@ tc_pol_case = describe "Polymophic and recursive pattern matching" $ do , " Cons (Cons Nil ys) xs => 1 + elems (Cons ys xs)" ] correct1 = - [ "length : List (c) -> Int" + [ "length : List c -> Int" , "length = \\list. case list of" , " Nil => 0" , " Cons x xs => 1 + length xs" , " Cons x (Cons y Nil) => 2" ] correct2 = - [ "length : List (c) -> Int" + [ "length : List c -> Int" , "length = \\list. case list of" , " Nil => 0" , " non_empty => 1" ] correct3 = - [ "length : List (Int) -> Int" + [ "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 : List (List(c)) -> Int" + [ "elems : List (List c) -> Int" , "elems = \\list. case list of" , " Nil => 0" , " Cons Nil Nil => 0" @@ -261,16 +261,16 @@ tc_pol_case = describe "Polymophic and recursive pattern matching" $ do ] tc_if = specify "Test if else case expression" $ do - run [ "data Bool () where" - , " True : Bool ()" - , " False : Bool ()" - - , "ifThenElse : Bool () -> a -> a -> a" + run + [ "data Bool where" + , " True : Bool" + , " False : Bool" + , "ifThenElse : Bool -> a -> a -> a" , "ifThenElse b if else = case b of" , " True => if" , " False => else" - ] `shouldSatisfy` ok - + ] + `shouldSatisfy` ok tc_infer_case = describe "Infer case expression" $ do specify "Wrong case expression rejected" $ @@ -279,9 +279,9 @@ tc_infer_case = describe "Infer case expression" $ do run (fs ++ correct) `shouldSatisfy` ok where fs = - [ "data Bool () where" - , " True : Bool ()" - , " False : Bool ()" + [ "data Bool where" + , " True : Bool" + , " False : Bool" ] correct = @@ -296,33 +296,38 @@ tc_infer_case = describe "Infer case expression" $ do , " _ => 1" ] -tc_rec1 = specify "Infer simple recursive definition" $ - run ["test x = 1 + test (x + 1)"] `shouldSatisfy` ok +tc_rec1 = + specify "Infer simple recursive definition" $ + run ["test x = 1 + test (x + 1)"] `shouldSatisfy` ok -tc_rec2 = specify "Infer recursive definition with pattern matching" $ run - [ "data Bool () where" - , " False : Bool ()" - , " True : Bool ()" - - , "test = \\x. case x of" - , " 10 => True" - , " _ => test (x+1)" - ] `shouldSatisfy` ok +tc_rec2 = + specify "Infer recursive definition with pattern matching" $ + run + [ "data Bool where" + , " False : Bool" + , " True : Bool" + , "test = \\x. case x of" + , " 10 => True" + , " _ => test (x+1)" + ] + `shouldSatisfy` ok run :: [String] -> Err T.Program -run = fmap removeForall - . reportTEVar - <=< typecheck - <=< run' +run = + fmap removeForall + . reportTEVar + <=< typecheck + <=< run' run' s = do - p <- (pProgram . resolveLayout True . myLexer . unlines) s + p <- (fmap desugar . pProgram . resolveLayout True . myLexer . unlines) s reportForall Bi p (rename <=< annotateForall) p -runPrint = (putStrLn . either show printTree . run') - ["double x = x + x"] +runPrint = + (putStrLn . either show printTree . run') + ["double x = x + x"] ok = \case - Ok _ -> True + Ok _ -> True Bad _ -> False diff --git a/tests/TestTypeCheckerHm.hs b/tests/TestTypeCheckerHm.hs index fd88ab2..8137937 100644 --- a/tests/TestTypeCheckerHm.hs +++ b/tests/TestTypeCheckerHm.hs @@ -2,19 +2,20 @@ module TestTypeCheckerHm where -import Control.Monad (sequence_, (<=<)) -import Test.Hspec +import Control.Monad (sequence_, (<=<)) +import Test.Hspec -import AnnForall (annotateForall) -import qualified DoStrings as D -import Grammar.Layout (resolveLayout) -import Grammar.Par (myLexer, pProgram) -import Grammar.Print (printTree) -import Renamer.Renamer (rename) -import ReportForall (reportForall) -import TypeChecker.TypeChecker (TypeChecker (Hm)) -import TypeChecker.TypeCheckerHm (typecheck) -import TypeChecker.TypeCheckerIr (Program) +import AnnForall (annotateForall) +import Desugar.Desugar (desugar) +import DoStrings qualified as D +import Grammar.Layout (resolveLayout) +import Grammar.Par (myLexer, pProgram) +import Grammar.Print (printTree) +import Renamer.Renamer (rename) +import ReportForall (reportForall) +import TypeChecker.TypeChecker (TypeChecker (Hm)) +import TypeChecker.TypeCheckerHm (typecheck) +import TypeChecker.TypeCheckerIr (Program) testTypeCheckerHm = describe "Hindley-Milner type checker test" $ do sequence_ goods @@ -47,10 +48,10 @@ goods = "Pattern matching on a nested list" ( D.do _List - "main : List (List (a)) -> Int ;" + "main : List (List a) -> Int;" "main xs = case xs of {" - " Cons Nil _ => 1 ;" - " _ => 0 ;" + " Cons Nil _ => 1;" + " _ => 0;" "};" ) ok @@ -78,7 +79,7 @@ bads = ( D.do _Bool _not - "f : a -> Bool () ;" + "f : a -> Bool ;" "f x = not x ;" ) bad @@ -102,7 +103,7 @@ bads = "Pattern matching on literal and _List should not succeed" ( D.do _List - "length : List (c) -> Int;" + "length : List c -> Int;" "length _List = case _List of {" " 0 => 0;" " Cons x xs => 1 + length xs;" @@ -120,29 +121,29 @@ bads = " };" ) bad - -- FIXME FAILING TEST - -- , testSatisfy - -- "id with incorrect signature" - -- ( D.do - -- "id : a -> b;" - -- "id x = x;" - -- ) - -- bad - -- FIXME FAILING TEST - -- , testSatisfy - -- "incorrect signature on const" - -- ( D.do - -- "const : a -> b -> b;" - -- "const x y = x" - -- ) - -- bad - -- FIXME FAILING TEST - -- , testSatisfy - -- "incorrect type signature on id lambda" - -- ( D.do - -- "id = ((\\x. x) : a -> b);" - -- ) - -- bad + -- FIXME FAILING TEST + -- , testSatisfy + -- "id with incorrect signature" + -- ( D.do + -- "id : a -> b;" + -- "id x = x;" + -- ) + -- bad + -- FIXME FAILING TEST + -- , testSatisfy + -- "incorrect signature on const" + -- ( D.do + -- "const : a -> b -> b;" + -- "const x y = x" + -- ) + -- bad + -- FIXME FAILING TEST + -- , testSatisfy + -- "incorrect type signature on id lambda" + -- ( D.do + -- "id = ((\\x. x) : a -> b);" + -- ) + -- bad ] bes = @@ -187,42 +188,33 @@ bes = , testBe "length function on int list infers correct signature" ( D.do - "data List () where {" - " Nil : List ()" - " Cons : Int -> List () -> List ()" - "};" + "data List where " + " Nil : List" + " Cons : Int -> List -> List" - "length xs = case xs of {" - " Nil => 0 ;" - " Cons _ xs => 1 + length xs ;" - "};" + "length xs = case xs of" + " Nil => 0" + " Cons _ xs => 1 + length xs" ) ( D.do - "data List () where {" - " Nil : List ()" - " Cons : Int -> List () -> List ()" - "};" + "data List where" + " Nil : List" + " Cons : Int -> List -> List" - "length : List () -> Int ;" - "length xs = case xs of {" - " Nil => 0 ;" - " Cons _ xs => 1 + length xs ;" - "};" + "length : List -> Int" + "length xs = case xs of" + " Nil => 0" + " Cons _ xs => 1 + length xs" ) ] testSatisfy desc test satisfaction = specify desc $ run test `shouldSatisfy` satisfaction testBe desc test shouldbe = specify desc $ run test `shouldBe` run shouldbe -run = fmap (printTree . fst) . typecheck <=< pProgram . myLexer - -run' s = do - p <- (pProgram . resolveLayout True . myLexer) s - reportForall Hm p - (rename <=< annotateForall) p +run = fmap (printTree . fst) . typecheck <=< fmap desugar . pProgram . myLexer ok (Right _) = True -ok (Left _) = False +ok (Left _) = False bad = not . ok @@ -232,14 +224,13 @@ _const = D.do "const : a -> b -> a ;" "const x y = x ;" _List = D.do - "data List (a) where" - " {" - " Nil : List (a);" - " Cons : a -> List (a) -> List (a)" - " };" + "data List a where {" + " Nil : List a;" + " Cons : a -> List a -> List a;" + "};" _headSig = D.do - "head : List (a) -> a ;" + "head : List a -> a ;" _head = D.do "head xs = " @@ -248,13 +239,13 @@ _head = D.do " };" _Bool = D.do - "data Bool () where {" - " True : Bool ()" - " False : Bool ()" + "data Bool where {" + " True : Bool" + " False : Bool" "};" _not = D.do - "not : Bool () -> Bool () ;" + "not : Bool -> Bool ;" "not x = case x of {" " True => False ;" " False => True ;" @@ -262,9 +253,9 @@ _not = D.do _id = "id x = x ;" _Maybe = D.do - "data Maybe (a) where {" - " Nothing : Maybe (a)" - " Just : a -> Maybe (a)" + "data Maybe a where {" + " Nothing : Maybe a" + " Just : a -> Maybe a" " };" _fmap = D.do