mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-21 23:37:23 +03:00
converted unison-shared tests over to EasyTest, went fabulously
This commit is contained in:
Paul Chiusano
parent
2a307b0d4a
commit
d5f686eb22
@ -18,7 +18,7 @@ import qualified Prelude
|
||||
import qualified Text.Parsec as Parsec
|
||||
import qualified Text.Parsec.Layout as L
|
||||
|
||||
import Debug.Trace
|
||||
-- import Debug.Trace
|
||||
|
||||
type Parser s a = Parsec.Parsec Text (Env s) a
|
||||
|
||||
|
||||
@ -1,19 +1,20 @@
|
||||
module Main where
|
||||
|
||||
import EasyTest
|
||||
import System.IO
|
||||
import Test.Tasty
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Test.Doc as Doc
|
||||
import qualified Unison.Test.Typechecker as Typechecker
|
||||
import qualified Unison.Test.Term as Term
|
||||
import qualified Unison.Test.TermParser as TermParser
|
||||
import qualified Unison.Test.TypeParser as TypeParser
|
||||
import qualified Unison.Test.Interpreter as Interpreter
|
||||
import qualified Unison.Test.Typechecker.Components as Components
|
||||
|
||||
tests :: TestTree
|
||||
tests = testGroup "unison" [Doc.tests, Typechecker.tests, Term.tests, TermParser.tests, TypeParser.tests, Interpreter.tests, Components.tests]
|
||||
test :: Test ()
|
||||
test = scope "unison-shared" $ do
|
||||
(codebase, resolveSymbol, allBindings, evaluate) <- io Common.codebase
|
||||
tests [ Doc.test
|
||||
, Interpreter.test codebase allBindings evaluate
|
||||
, Components.test codebase ]
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
mapM_ (`hSetEncoding` utf8) [stdout, stdin, stderr]
|
||||
defaultMain tests
|
||||
run test
|
||||
|
||||
@ -28,9 +28,13 @@ import qualified Unison.Util.Logger as L
|
||||
import qualified Unison.View as View
|
||||
|
||||
type V = Symbol View.DFO
|
||||
type TermV = Term V
|
||||
|
||||
type CodebaseIOV = Codebase IO V
|
||||
|
||||
-- A codebase for testing
|
||||
type TCodebase =
|
||||
( Codebase IO V -- the codebase
|
||||
( CodebaseIOV -- the codebase
|
||||
, Reference -> V -- resolve references to symbols
|
||||
, [(V, Term V)] -- all symbol bindings
|
||||
, Term V -> Noted IO (Term V)) -- evaluator
|
||||
|
||||
@ -1,48 +1,34 @@
|
||||
module Unison.Test.Doc where
|
||||
|
||||
import EasyTest
|
||||
import Unison.Doc
|
||||
import Test.Tasty
|
||||
import Unison.Dimensions
|
||||
-- import Test.Tasty.SmallCheck as SC
|
||||
-- import Test.Tasty.QuickCheck as QC
|
||||
import Test.Tasty.HUnit
|
||||
import qualified Unison.Test.Common as Common
|
||||
|
||||
fmt :: Word -> Doc String [Int] -> String
|
||||
fmt w d = formatString (Width $ fromIntegral w) d
|
||||
|
||||
tests :: TestTree
|
||||
tests = testGroup "Doc"
|
||||
[ testCase "ex (1)" $ assertEqual "should fit on one line"
|
||||
"a b c"
|
||||
(fmt 10 (sep' " " ["a", "b", "c"]))
|
||||
, testCase "ex (1a)" $ assertEqual "should break onto 3 lines"
|
||||
"a\nb\nc"
|
||||
(fmt 4 (sep' " " ["a", "b", "c"]))
|
||||
, testCase "ex (2)" $ assertEqual "should fit on one line"
|
||||
"a b c d e"
|
||||
(fmt 9 (sep " " [embed "a", sep' " " ["b", "c", "d"], embed "e"]))
|
||||
, testCase "ex (2a)" $ assertEqual "should break onto 3 lines"
|
||||
"a\nb c d\ne"
|
||||
(fmt 8 (sep " " [embed "a", sep' " " ["b", "c", "d"], embed "e"]))
|
||||
, testCase "ex (3)" $ assertEqual "should break onto 3 lines with indent"
|
||||
"a\n b c d\ne"
|
||||
(fmt 8 (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"], embed "e"]))
|
||||
, testCase "ex (3a)" $ assertEqual "should fit on one line"
|
||||
"a b c d e"
|
||||
(fmt 9 (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"], embed "e"]))
|
||||
, testCase "parenthesize (1)" $ assertEqual "should fit on one line"
|
||||
"(a b c d)"
|
||||
(fmt 9 $ parenthesize True (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"]]))
|
||||
, testCase "parenthesize (2)" $ assertEqual "should break onto two lines with indent and no parens"
|
||||
"a\n b"
|
||||
(fmt 3 $ parenthesize True (docs [embed "a", breakable " ", nest " " $ embed "b"]))
|
||||
, testCase "parenthesize (3)" $ assertEqual "should break onto two lines with indent and no parens"
|
||||
test :: Test ()
|
||||
test = scope "Doc" $ tests
|
||||
[ scope "ex (1)" $ expect ("a b c" == fmt 10 (sep' " " ["a", "b", "c"]))
|
||||
, scope "ex (1a)" $ expect ("a\nb\nc" == fmt 4 (sep' " " ["a", "b", "c"]))
|
||||
, scope "ex (2)" $ expect ("a b c d e" == fmt 9 (sep " " [embed "a", sep' " " ["b", "c", "d"], embed "e"]))
|
||||
, scope "ex (2a)" $ expect ("a\nb c d\ne" == fmt 8 (sep " " [embed "a", sep' " " ["b", "c", "d"], embed "e"]))
|
||||
, scope "ex (3)" . expect $
|
||||
"a\n b c d\ne" == fmt 8 (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"], embed "e"])
|
||||
, scope "ex (3a)" . expect $
|
||||
"a b c d e" == fmt 9 (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"], embed "e"])
|
||||
, scope "parenthesize (1)" . expect $
|
||||
"(a b c d)" == fmt 9 (parenthesize True (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"]]))
|
||||
, scope "parenthesize (2)" . expect $
|
||||
"a\n b" == fmt 3 (parenthesize True (docs [embed "a", breakable " ", nest " " $ embed "b"]))
|
||||
, scope "parenthesize (3)" . expect $
|
||||
"a\n b c d"
|
||||
(fmt 7 $ parenthesize True (docs [embed "a", breakable " ", nest " " $ sep' " " ["b", "c", "d"]]))
|
||||
, testCase "parenthesize (4)" $ assertEqual "should break onto two lines with indent and no parens"
|
||||
==
|
||||
fmt 7 (parenthesize True (docs [embed "a", breakable " ", nest " " $ sep' " " ["b", "c", "d"]]))
|
||||
, scope "parenthesize (4)" . expect $
|
||||
"a\n b c d"
|
||||
(fmt 8 $ parenthesize True (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"]]))
|
||||
==
|
||||
fmt 8 (parenthesize True (sep " " [embed "a", nest " " $ sep' " " ["b", "c", "d"]]))
|
||||
]
|
||||
|
||||
main = defaultMain tests
|
||||
main = run test
|
||||
|
||||
@ -1,105 +1,102 @@
|
||||
module Unison.Test.Interpreter where
|
||||
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import EasyTest
|
||||
import qualified Unison.Parsers as P
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Interpreter as I
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
|
||||
let
|
||||
tests =
|
||||
[ t "1 + 1" "2"
|
||||
, t "1 + 1 + 1" "3"
|
||||
, t "(x -> x) 42" "42"
|
||||
, t "let { x = 2; y = 3 ; x + y }" "5"
|
||||
, t "if False then 0 else 1" "1"
|
||||
, t "if True then 12 else 13" "12"
|
||||
, t "1 >_Number 0" "True"
|
||||
, t "1 ==_Number 1" "True"
|
||||
, t "2 ==_Number 0" "False"
|
||||
, t "1 <_Number 2" "True"
|
||||
, t "1 <=_Number 1" "True"
|
||||
, t "1 >=_Number 1" "True"
|
||||
, t "Comparison.fold 1 0 0 Less" "1"
|
||||
, t "Comparison.fold 0 1 0 Equal" "1"
|
||||
, t "Comparison.fold 0 0 1 Greater" "1"
|
||||
, t "Order.compare (Order.invert <| Order.tuple2 Number.Order Number.Order) (1,2) (1,3)" "Greater"
|
||||
, t "Order.compare (Order.invert <| Order.tuple2 Number.Order Number.Order) (2,1) (1,3)" "Less"
|
||||
, t "Order.compare (Order.tuple2 Number.Order Order.ignore) (1,2) (1,3)" "Equal"
|
||||
, t "Order.compare (Order.tuple2 Order.ignore Number.Order ) (2,2) (1,3)" "Less"
|
||||
, t "True `or` False" "True"
|
||||
, t "False `or` True" "True"
|
||||
, t "True `or` True" "True"
|
||||
, t "False `or` False" "False"
|
||||
, t "True `and` True" "True"
|
||||
, t "True `and` False" "False"
|
||||
, t "False `and` True" "False"
|
||||
, t "False `and` False" "False"
|
||||
, t "not False" "True"
|
||||
, t "not True" "False"
|
||||
, t "let rec { fac n = if n ==_Number 0 then 1 else n * fac (n - 1); fac 5 }" "120"
|
||||
, t "let rec { ping n = if n >=_Number 10 then n else pong (n + 1); pong n = ping (n + 1); ping 0}"
|
||||
"10"
|
||||
, t "let\n id x = x\n g = id 42\n p = id \"hi\"\n g" "42"
|
||||
, t "let { id : forall a . a -> a; id x = x; g = id 42; p = id \"hi\" ; g }" "42"
|
||||
, t "(let { id x = x; id } : forall a . a -> a) 42" "42"
|
||||
, t "Optional.map ((+) 1) (Some 1)" "Some 2"
|
||||
, t "Optional.map ((+) 1) ((Some: ∀ a . a -> Optional a) 1)" "Some 2"
|
||||
, t "Either.fold ((+) 1) ((+) 2) (Left 1)" "2"
|
||||
, t "Either.fold ((+) 1) ((+) 2) (Right 1)" "3"
|
||||
, t "Either.swap (Left 1)" "Either.Right 1"
|
||||
, t "Pair.fold (x y -> x) (1, 2)" "1"
|
||||
, t "const 41 0" "41"
|
||||
, t "1st (1,2,3,4)" "1"
|
||||
, t "2nd (1,2 + 1,3,4)" "3"
|
||||
, t "identity <| (1 + 1)" "2"
|
||||
, t "(1 + 1) |> identity" "2"
|
||||
, t "if \"hi\" ==_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hi\" <_Text \"hiya\" then 1 else 2" "1"
|
||||
, t "if \"hi\" <=_Text \"hiya\" then 1 else 2" "1"
|
||||
, t "if \"hiya\" >_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hiya\" >=_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hi\" >=_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hi\" <=_Text \"hi\" then 1 else 2" "1"
|
||||
, t "Vector.reverse [1,2,3]" "[3,2,1]"
|
||||
, t "Vector.reverse Vector.empty" "[]"
|
||||
, t "Vector.fold-right Vector.prepend Vector.empty [1,2,3]" "[1,2,3]"
|
||||
, t "Vector.fold-balanced Vector.concatenate Vector.empty (Vector.map Vector.single [1,2,3,4,5])"
|
||||
"[1,2,3,4,5]"
|
||||
, t "Vector.fold-balanced Vector.concatenate Vector.empty [[1],[2],[3,4],[5]]"
|
||||
"[1,2,3,4,5]"
|
||||
, t "Vector.fold-balanced (+) 0 [1,2,3]" "6"
|
||||
, t "Vector.dedup-adjacent (==_Number) [1,1,2,2,3,4,4,4,4,5]" "[1,2,3,4,5]"
|
||||
, t "Vector.dedup Number.Order [1,2,1,5,4,2,4,4,3,5]" "[1,2,3,4,5]"
|
||||
, t "Vector.histogram Number.Order [1,2,1,5,4,2,4,4,3,5]" "[(1,2),(2,2),(3,1),(4,3),(5,2)]"
|
||||
, t "Vector.ranked-histogram Number.Order [1,2,1,5,4,2,4,4,3,5]"
|
||||
"[(4,3),(1,2),(2,2),(5,2),(3,1)]"
|
||||
, t "Vector.range 0 10" "[0,1,2,3,4,5,6,7,8,9]"
|
||||
, t "Vector.range 0 0" "[]"
|
||||
, t "Vector.fold-left (+) 0 (Vector.replicate 5 1)" "5"
|
||||
, t "Vector.sort-by Number.Order identity [5,2,1,3,4]" "[1,2,3,4,5]"
|
||||
, t "Vector.sort-by (Order.invert Number.Order) identity [5,2,1,3,4]" "[5,4,3,2,1]"
|
||||
, t "Vector.bind 2nd (Vector.zip [1,2,3] [[1],[2],[3]])" "[1,2,3]"
|
||||
, t "Vector.all? identity [True,True,True,True]" "True"
|
||||
, t "Vector.all? identity [True,False,True,True]" "False"
|
||||
, t "Optional.get-or 96 (Vector.at 1 [0,1,2,3,4])" "1"
|
||||
, t "Vector.take 0 [1,2,3]" "[]"
|
||||
, t "Vector.take 2 [1,2,3]" "[1,2]"
|
||||
, t "Vector.drop 2 [1,2,3]" "[3]"
|
||||
, t "Text.join [\"a\", \"b\", \"c\"]" "\"abc\""
|
||||
]
|
||||
t uneval eval = testCase (uneval ++ " ⟹ " ++ eval) $ do
|
||||
(codebase, _, builtins, evaluate) <- codebase
|
||||
-- putStrLn (show $ map fst builtins)
|
||||
let term = P.bindBuiltins builtins [] $ P.unsafeParseTerm uneval
|
||||
_ <- Note.run $ Codebase.typeAt codebase term []
|
||||
actual <- Note.run $ evaluate term
|
||||
expected <- Note.run $ evaluate (P.unsafeParseTerm eval)
|
||||
assertEqual "comparing results" expected actual
|
||||
in testGroup "Interpreter" tests
|
||||
|
||||
main = defaultMain tests
|
||||
test :: Common.CodebaseIOV
|
||||
-> [(Common.V, Common.TermV)]
|
||||
-> (Common.TermV -> Note.Noted IO Common.TermV)
|
||||
-> Test ()
|
||||
test codebase builtins evaluate = scope "Interpreter" . tests $
|
||||
[ t "1 + 1" "2"
|
||||
, t "1 + 1 + 1" "3"
|
||||
, t "(x -> x) 42" "42"
|
||||
, t "let { x = 2; y = 3 ; x + y }" "5"
|
||||
, t "if False then 0 else 1" "1"
|
||||
, t "if True then 12 else 13" "12"
|
||||
, t "1 >_Number 0" "True"
|
||||
, t "1 ==_Number 1" "True"
|
||||
, t "2 ==_Number 0" "False"
|
||||
, t "1 <_Number 2" "True"
|
||||
, t "1 <=_Number 1" "True"
|
||||
, t "1 >=_Number 1" "True"
|
||||
, t "Comparison.fold 1 0 0 Less" "1"
|
||||
, t "Comparison.fold 0 1 0 Equal" "1"
|
||||
, t "Comparison.fold 0 0 1 Greater" "1"
|
||||
, t "Order.compare (Order.invert <| Order.tuple2 Number.Order Number.Order) (1,2) (1,3)" "Greater"
|
||||
, t "Order.compare (Order.invert <| Order.tuple2 Number.Order Number.Order) (2,1) (1,3)" "Less"
|
||||
, t "Order.compare (Order.tuple2 Number.Order Order.ignore) (1,2) (1,3)" "Equal"
|
||||
, t "Order.compare (Order.tuple2 Order.ignore Number.Order ) (2,2) (1,3)" "Less"
|
||||
, t "True `or` False" "True"
|
||||
, t "False `or` True" "True"
|
||||
, t "True `or` True" "True"
|
||||
, t "False `or` False" "False"
|
||||
, t "True `and` True" "True"
|
||||
, t "True `and` False" "False"
|
||||
, t "False `and` True" "False"
|
||||
, t "False `and` False" "False"
|
||||
, t "not False" "True"
|
||||
, t "not True" "False"
|
||||
, t "let rec { fac n = if n ==_Number 0 then 1 else n * fac (n - 1); fac 5 }" "120"
|
||||
, t "let rec { ping n = if n >=_Number 10 then n else pong (n + 1); pong n = ping (n + 1); ping 0}"
|
||||
"10"
|
||||
, t "let\n id x = x\n g = id 42\n p = id \"hi\"\n g" "42"
|
||||
, t "let { id : forall a . a -> a; id x = x; g = id 42; p = id \"hi\" ; g }" "42"
|
||||
, t "(let { id x = x; id } : forall a . a -> a) 42" "42"
|
||||
, t "Optional.map ((+) 1) (Some 1)" "Some 2"
|
||||
, t "Optional.map ((+) 1) ((Some: ∀ a . a -> Optional a) 1)" "Some 2"
|
||||
, t "Either.fold ((+) 1) ((+) 2) (Left 1)" "2"
|
||||
, t "Either.fold ((+) 1) ((+) 2) (Right 1)" "3"
|
||||
, t "Either.swap (Left 1)" "Either.Right 1"
|
||||
, t "Pair.fold (x y -> x) (1, 2)" "1"
|
||||
, t "const 41 0" "41"
|
||||
, t "1st (1,2,3,4)" "1"
|
||||
, t "2nd (1,2 + 1,3,4)" "3"
|
||||
, t "identity <| (1 + 1)" "2"
|
||||
, t "(1 + 1) |> identity" "2"
|
||||
, t "if \"hi\" ==_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hi\" <_Text \"hiya\" then 1 else 2" "1"
|
||||
, t "if \"hi\" <=_Text \"hiya\" then 1 else 2" "1"
|
||||
, t "if \"hiya\" >_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hiya\" >=_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hi\" >=_Text \"hi\" then 1 else 2" "1"
|
||||
, t "if \"hi\" <=_Text \"hi\" then 1 else 2" "1"
|
||||
, t "Vector.reverse [1,2,3]" "[3,2,1]"
|
||||
, t "Vector.reverse Vector.empty" "[]"
|
||||
, t "Vector.fold-right Vector.prepend Vector.empty [1,2,3]" "[1,2,3]"
|
||||
, t "Vector.fold-balanced Vector.concatenate Vector.empty (Vector.map Vector.single [1,2,3,4,5])"
|
||||
"[1,2,3,4,5]"
|
||||
, t "Vector.fold-balanced Vector.concatenate Vector.empty [[1],[2],[3,4],[5]]"
|
||||
"[1,2,3,4,5]"
|
||||
, t "Vector.fold-balanced (+) 0 [1,2,3]" "6"
|
||||
, t "Vector.dedup-adjacent (==_Number) [1,1,2,2,3,4,4,4,4,5]" "[1,2,3,4,5]"
|
||||
, t "Vector.dedup Number.Order [1,2,1,5,4,2,4,4,3,5]" "[1,2,3,4,5]"
|
||||
, t "Vector.histogram Number.Order [1,2,1,5,4,2,4,4,3,5]" "[(1,2),(2,2),(3,1),(4,3),(5,2)]"
|
||||
, t "Vector.ranked-histogram Number.Order [1,2,1,5,4,2,4,4,3,5]"
|
||||
"[(4,3),(1,2),(2,2),(5,2),(3,1)]"
|
||||
, t "Vector.range 0 10" "[0,1,2,3,4,5,6,7,8,9]"
|
||||
, t "Vector.range 0 0" "[]"
|
||||
, t "Vector.fold-left (+) 0 (Vector.replicate 5 1)" "5"
|
||||
, t "Vector.sort-by Number.Order identity [5,2,1,3,4]" "[1,2,3,4,5]"
|
||||
, t "Vector.sort-by (Order.invert Number.Order) identity [5,2,1,3,4]" "[5,4,3,2,1]"
|
||||
, t "Vector.bind 2nd (Vector.zip [1,2,3] [[1],[2],[3]])" "[1,2,3]"
|
||||
, t "Vector.all? identity [True,True,True,True]" "True"
|
||||
, t "Vector.all? identity [True,False,True,True]" "False"
|
||||
, t "Optional.get-or 96 (Vector.at 1 [0,1,2,3,4])" "1"
|
||||
, t "Vector.take 0 [1,2,3]" "[]"
|
||||
, t "Vector.take 2 [1,2,3]" "[1,2]"
|
||||
, t "Vector.drop 2 [1,2,3]" "[3]"
|
||||
, t "Text.join [\"a\", \"b\", \"c\"]" "\"abc\""
|
||||
]
|
||||
where
|
||||
t uneval eval = scope (uneval ++ " ⟹ " ++ eval) $ do
|
||||
-- putStrLn (show $ map fst builtins)
|
||||
let term = P.bindBuiltins builtins [] $ P.unsafeParseTerm uneval
|
||||
_ <- io . Note.run $ Codebase.typeAt codebase term []
|
||||
actual <- io . Note.run $ evaluate term
|
||||
expected <- io . Note.run $ evaluate (P.unsafeParseTerm eval)
|
||||
expect (expected == actual)
|
||||
|
||||
@ -1,125 +0,0 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module Unison.Test.Term where
|
||||
|
||||
-- import Test.Tasty.QuickCheck as QC
|
||||
-- import Test.Tasty.SmallCheck as SC
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Codebase.MemCodebase ()
|
||||
import Unison.Parsers (unsafeParseTerm)
|
||||
import Unison.Reference as R
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Term
|
||||
import Unison.View (DFO)
|
||||
import Unison.Dimensions (Width(..),Height(..),Region,X(..),Y(..))
|
||||
import Data.Text (Text)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import qualified Unison.ABT as ABT
|
||||
import qualified Unison.Doc as Doc
|
||||
import qualified Unison.Paths as Paths
|
||||
import qualified Unison.Parser as Parser
|
||||
import qualified Unison.TermParser as TermParser
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Var as Var
|
||||
import qualified Unison.Views as Views
|
||||
import Debug.Trace
|
||||
|
||||
-- term for testing
|
||||
type TTerm = Term (Symbol DFO)
|
||||
|
||||
hash :: TTerm -> Hash
|
||||
hash = ABT.hash
|
||||
|
||||
atPts :: Bool -> Common.TCodebase -> [(Int,Int)] -> TTerm -> [(Paths.Path, Region)]
|
||||
atPts print (_,symbol,_,_) pts t = map go pts where
|
||||
go (x,y) = let p = path x y in (p, Doc.region bounds p)
|
||||
doc = Views.term symbol t
|
||||
layout = Doc.layout Doc.textWidth (Width 80) doc
|
||||
bounds = debug $ Doc.bounds (\t -> (Doc.textWidth t, Height 1)) (Doc.box layout)
|
||||
path x y = Doc.at bounds (X (fromIntegral x), Y (fromIntegral y))
|
||||
debug b = if print then trace ("\n" ++ Doc.debugDoc doc ++ "\n\n" ++ Doc.debugBox b ++ "\n\n" ++ Doc.debugBoxp b) b else b
|
||||
|
||||
main :: IO ()
|
||||
main = defaultMain tests
|
||||
|
||||
unsafeParseTerm' :: String -> TTerm
|
||||
unsafeParseTerm' = unsafeParseTerm
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \codebase -> testGroup "Term"
|
||||
[ testCase "alpha equivalence (term)" $ assertEqual "identity"
|
||||
(unsafeParseTerm' "a -> a")
|
||||
(unsafeParseTerm' "x -> x")
|
||||
, testCase "hash cycles" $ assertEqual "pingpong"
|
||||
(hash pingpong1)
|
||||
(hash pingpong2)
|
||||
-- , testCase "infix-rendering (1)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus 1 1"
|
||||
-- in assertEqual "+"
|
||||
-- "1 + 1"
|
||||
-- (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (unsaturated)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus _"
|
||||
-- in assertEqual "+"
|
||||
-- "(+) _"
|
||||
-- (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (totally unsaturated)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus"
|
||||
-- in assertEqual "+" "(+)" (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (2)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- do
|
||||
-- t <- pure $ unsafeParseTerm "Number.plus 1 1"
|
||||
-- let d = Views.term symbol t
|
||||
-- assertEqual "path sanity check"
|
||||
-- [Paths.Fn,Paths.Arg]
|
||||
-- (head $ Doc.leafPaths d)
|
||||
-- , testCase "let-rendering (1)" $ codebase >>= \codebase ->
|
||||
-- do
|
||||
-- -- let xy = 4223 in 42
|
||||
-- t <- pure $ unsafeParseTerm "let xy = 4223 in 42"
|
||||
-- [(p1,r1), (p2,_), (p3,r3), (p4,_), (p5,r5), (p6,r6)] <- pure $
|
||||
-- atPts False codebase [(0,0), (1,0), (10,0), (11,0), (5,0), (8,0)] t
|
||||
-- assertEqual "p1" [] p1
|
||||
-- assertEqual "p2" [] p2
|
||||
-- assertEqual "r1" (rect 0 0 19 1) r1
|
||||
-- assertEqual "p3" [Paths.Binding 0, Paths.Body] p3
|
||||
-- assertEqual "r3" (rect 9 0 4 1) r3
|
||||
-- assertEqual "p3 == p4" p3 p4
|
||||
-- assertEqual "p5" [Paths.Binding 0, Paths.Bound] p5
|
||||
-- assertEqual "r5" (rect 4 0 2 1) r5
|
||||
-- assertEqual "p6" [Paths.Binding 0] p6
|
||||
-- assertEqual "r6" (rect 4 0 9 1) r6
|
||||
-- , testCase "map lambda rendering" $ codebase >>= \codebase ->
|
||||
-- do
|
||||
-- -- map (x -> _) [1,2,3]
|
||||
-- t <- pure $ builtin "Vector.map" `app` lam' ["x"] blank `app` vector (map num [1,2,3])
|
||||
-- [(p1,r1)] <- pure $ atPts False codebase [(5,0)] t
|
||||
-- assertEqual "p1" [Paths.Fn, Paths.Arg] p1
|
||||
-- assertEqual "r1" (rect 4 0 8 1) r1
|
||||
-- , testCase "operator chain rendering" $ codebase >>= \codebase ->
|
||||
-- do
|
||||
-- t <- pure $ unsafeParseTerm "1 + 2 + 3"
|
||||
-- [(p1,r1),(p2,_)] <- pure $ atPts False codebase [(1,0), (2,0)] t
|
||||
-- assertEqual "p1" [Paths.Fn, Paths.Arg, Paths.Fn, Paths.Arg] p1
|
||||
-- assertEqual "r1" (rect 0 0 1 1) r1
|
||||
-- assertEqual "p2" [] p2
|
||||
]
|
||||
|
||||
rect :: Int -> Int -> Int -> Int -> (X,Y,Width,Height)
|
||||
rect x y w h =
|
||||
(X (fromIntegral x), Y (fromIntegral y), Width (fromIntegral w), Height (fromIntegral h))
|
||||
|
||||
-- various unison terms, useful for testing
|
||||
pingpong1 :: TTerm
|
||||
pingpong1 =
|
||||
unsafeParseTerm $
|
||||
unlines [ "let rec "
|
||||
, " ping x = pong (x + 1)"
|
||||
, " pong y = ping (y - 1)"
|
||||
, " ping 1"
|
||||
]
|
||||
|
||||
pingpong2 :: TTerm
|
||||
pingpong2 =
|
||||
unsafeParseTerm $ "let rec { pong1 p = ping1 (p - 1); ping1 q = pong1 (q + 1); ping1 1 }"
|
||||
@ -1,154 +0,0 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE PartialTypeSignatures #-}
|
||||
|
||||
module Unison.Test.TermParser where
|
||||
|
||||
import Data.List
|
||||
import Data.Text (Text)
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Unison.Literal (Literal)
|
||||
import Unison.Parsers (parseTerm)
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Term
|
||||
import Unison.Type (Type)
|
||||
import Unison.View (DFO)
|
||||
import qualified Data.Text as Text
|
||||
import qualified Unison.Literal as Literal
|
||||
import qualified Unison.Type as T
|
||||
-- import Test.Tasty.SmallCheck as SC
|
||||
-- import Test.Tasty.QuickCheck as QC
|
||||
|
||||
parse' :: String -> TestTree
|
||||
parse' s = testCase ("`" ++ s ++ "`") $
|
||||
case parseTerm s :: Either _ (Term (Symbol DFO)) of
|
||||
Left e -> assertFailure $ "parse failure \n" ++ e
|
||||
Right a -> pure ()
|
||||
|
||||
parse :: (String, Term (Symbol DFO)) -> TestTree
|
||||
parse (s, expected) =
|
||||
testCase ("`" ++ s ++ "`") $
|
||||
case parseTerm s of
|
||||
Left e -> assertFailure $ "parse failure \n" ++ e
|
||||
Right a -> assertEqual "mismatch" expected a
|
||||
|
||||
parseFail :: (String,String) -> TestTree
|
||||
parseFail (s, reason) =
|
||||
testCase ("`" ++ s ++ "` shouldn't parse: " ++ reason) $ assertBool "should not have parsed" $
|
||||
case parseTerm s :: Either _ (Term (Symbol DFO)) of
|
||||
Left _ -> True
|
||||
Right _ -> False
|
||||
|
||||
tests :: TestTree
|
||||
tests = testGroup "TermParser" $ (parse <$> shouldPass)
|
||||
++ (parse' <$> shouldParse)
|
||||
++ (parseFail <$> shouldFail)
|
||||
where
|
||||
shouldFail =
|
||||
[ ("+", "operator needs to be enclosed in parens or between arguments") ]
|
||||
shouldParse =
|
||||
[ "do Remote { n1 := Remote.spawn; n2 := Remote.spawn; let rec { x = 10; Remote.pure 42 }}" ]
|
||||
shouldPass =
|
||||
[ ("1", one)
|
||||
, ("[1,1]", vectorForced [one, one])
|
||||
, ("[1,1] : Vector Number", ann (vectorForced [one, one]) (T.vectorOf number))
|
||||
, ("(+)", numberplus)
|
||||
, ("(++)", var' "++")
|
||||
, ("(++)", var' "++")
|
||||
, ("((++))", var' "++")
|
||||
, ("1+", var' "1+")
|
||||
, ("(1+)", var' "1+")
|
||||
, ("((1+))", var' "1+")
|
||||
, ("1+1", onenone)
|
||||
, ("1+1", onenone)
|
||||
, ("1+ 1", app (var' "1+") one)
|
||||
-- todo: failing
|
||||
-- , ("1 +1", app one (var' "+1"))
|
||||
, ("[1+1]", vectorForced [onenone])
|
||||
, ("\"hello\"", hello)
|
||||
, ("_", blank)
|
||||
, ("a", a)
|
||||
, ("(+_Number)", numberplus)
|
||||
, ("Number.Other.plus", var' "Number.Other.plus")
|
||||
, ("1:Int", ann one int)
|
||||
, ("(1:Int)", ann one int)
|
||||
, ("(1:Int) : Int", ann (ann one int) int)
|
||||
, ("let { a = 1; a + 1 }", let1' [("a", one)] (apps numberplus [a, one]))
|
||||
, ("let\n a : Int\n a = 1\n a + 1", let_a_int1_in_aplus1)
|
||||
, ("let\n a : Int\n a = 1\n a + 1", let_a_int1_in_aplus1)
|
||||
, ("a b -> a + b", lam_ab_aplusb)
|
||||
, ("(a b -> a + b) : Int -> Int -> Int", ann lam_ab_aplusb intintint)
|
||||
, ("a b -> a + b : Int", lam' ["a", "b"] (ann (apps numberplus [a, b]) int))
|
||||
, ("a -> a", lam' ["a"] a)
|
||||
, ("(a -> a) : forall a . a -> a", ann (lam' ["a"] a) (T.forall' ["a"] (T.arrow a' a')))
|
||||
, ("let { f = a b -> a + b; f 1 1 }", f_eq_lamab_in_f11)
|
||||
, ("let { f a b = a + b; f 1 1 }", f_eq_lamab_in_f11)
|
||||
, ("let { f (+) b = 1 + b; f g 1 }", let1' [("f", lam' ["+", "b"] (apps plus [one, b]))] (apps f [g,one]))
|
||||
, ("let { a + b = f a b; 1 + 1 }", let1' [("+", lam' ["a", "b"] fab)] one_plus_one)
|
||||
, ("let\n (+) : Int -> Int -> Int\n a + b = f a b\n 1 + 1", plusintintint_fab_in_1plus1)
|
||||
, ("let { (+) : Int -> Int -> Int; (+) a b = f a b; 1 + 1 }", plusintintint_fab_in_1plus1)
|
||||
, ("let { (+) : Int -> Int -> Int; (+) a b = f a b; (+) 1 1 }", plusintintint_fab_in_1plus1)
|
||||
, ("let { f b = b + 1; a = 1; (+) a (f 1) }", let1' [("f", lam_b_bplus1), ("a", one)] (apps numberplus [a, apps f [one]]))
|
||||
-- from Unison.Test.Term
|
||||
, ("a -> a", lam' ["a"] $ var' "a") -- id
|
||||
, ("x y -> x", lam' ["x", "y"] $ var' "x") -- const
|
||||
, ("let rec { fix = f -> f (fix f); fix }", fix) -- fix
|
||||
, ("let rec\n fix f = f (fix f)\n fix", fix) -- fix
|
||||
, ("1 + 2 + 3", num 1 `plus'` num 2 `plus'` num 3)
|
||||
, ("[1, 2, 1 + 1]", vectorForced [num 1, num 2, num 1 `plus'` num 1])
|
||||
, ("(id -> let { x = id 42; y = id \"hi\"; 43 }) : (forall a . a) -> Number", lam' ["id"] (let1'
|
||||
[ ("x", var' "id" `app` num 42),
|
||||
("y", var' "id" `app` text "hi")
|
||||
] (num 43)) `ann` (T.forall' ["a"] (T.v' "a") `T.arrow` T.lit T.Number))
|
||||
, ("(do Remote { pure 42 } )", builtin "Remote.pure" `app` num 42)
|
||||
, ("do Remote { x = 42; pure (x + 1) } ",
|
||||
builtin "Remote.bind" `apps` [
|
||||
lam' ["q"] (builtin "Remote.pure" `app` (var' "q" `plus'` num 1)),
|
||||
builtin "Remote.pure" `app` num 42
|
||||
]
|
||||
)
|
||||
, ("do Remote { x := pure 42; pure (x + 1) } ",
|
||||
builtin "Remote.bind" `apps` [
|
||||
lam' ["q"] (builtin "Remote.pure" `app` (var' "q" `plus'` num 1)),
|
||||
builtin "Remote.pure" `app` num 42
|
||||
]
|
||||
)
|
||||
, ("do Remote\n x := pure 42\n y := pure 18\n pure (x + y)",
|
||||
builtin "Remote.bind" `apps` [
|
||||
lam' ["x"] (builtin "Remote.bind" `apps` [
|
||||
lam' ["y"] (builtin "Remote.pure" `app` (var' "x" `plus'` var' "y")),
|
||||
builtin "Remote.pure" `app` num 18
|
||||
]),
|
||||
builtin "Remote.pure" `app` num 42
|
||||
]
|
||||
)
|
||||
]
|
||||
one = (lit . Literal.Number) 1
|
||||
hello = text "hello"
|
||||
number :: Ord v => Type v
|
||||
number = T.lit T.Number
|
||||
int = T.v' "Int"
|
||||
intintint = T.arrow int (T.arrow int int)
|
||||
a = var' "a"
|
||||
a' = T.v' "a"
|
||||
b = var' "b"
|
||||
f = var' "f"
|
||||
g = var' "g"
|
||||
plus = var' "+"
|
||||
plus' x y = builtin "Number.+" `app` x `app` y
|
||||
numberplus = builtin "Number.+"
|
||||
onenone = var' "1+1"
|
||||
one_plus_one = apps plus [one,one]
|
||||
lam_ab_aplusb = lam' ["a", "b"] (apps numberplus [a, b])
|
||||
lam_b_bplus1 = lam' ["b"] (apps numberplus [b, one])
|
||||
lam_ab_fab = lam' ["a", "b"] fab
|
||||
fab = apps f [a, b]
|
||||
f_eq_lamab_in_f11 = let1' [("f", lam_ab_aplusb)] (apps f [one,one])
|
||||
let_a_int1_in_aplus1 = let1' [("a", ann one int)] (apps numberplus [a,one])
|
||||
plusintintint_fab_in_1plus1 = let1' [("+", ann lam_ab_fab intintint)] one_plus_one
|
||||
fix = letRec'
|
||||
[ ("fix", lam' ["f"] $ var' "f" `app` (var' "fix" `app` var' "f")) ]
|
||||
(var' "fix")
|
||||
|
||||
main :: IO ()
|
||||
main = defaultMain tests
|
||||
@ -1,46 +0,0 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module Unison.Test.TypeParser where
|
||||
|
||||
import Test.Tasty
|
||||
import Unison.Parser
|
||||
import Unison.Parsers (parseType)
|
||||
import Unison.Type (Type)
|
||||
import qualified Unison.Type as T
|
||||
-- import Test.Tasty.SmallCheck as SC
|
||||
-- import Test.Tasty.QuickCheck as QC
|
||||
import Test.Tasty.HUnit
|
||||
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.View (DFO)
|
||||
|
||||
parseV :: (String, Type (Symbol DFO)) -> TestTree
|
||||
parseV (s,expected) =
|
||||
testCase ("`" ++ s ++ "`") $ case parseType s of
|
||||
Left e -> assertFailure $ "parse failure\n" ++ e
|
||||
Right a -> assertEqual "mismatch" expected a
|
||||
|
||||
tests :: TestTree
|
||||
tests = testGroup "TypeParser" $ fmap parseV strings
|
||||
where
|
||||
strings :: [(String, Type (Symbol DFO))]
|
||||
strings =
|
||||
[ ("Number", T.lit T.Number)
|
||||
, ("Text", T.lit T.Text)
|
||||
, ("Vector", T.lit T.Vector)
|
||||
, ("Remote", T.builtin "Remote")
|
||||
, ("Foo", foo)
|
||||
, ("Foo -> Foo", T.arrow foo foo)
|
||||
, ("a -> a", T.arrow a a)
|
||||
, ("Foo -> Foo -> Foo", T.arrow foo (T.arrow foo foo))
|
||||
, ("Foo -> (Foo -> Foo)", T.arrow foo (T.arrow foo foo))
|
||||
, ("(Foo -> Foo) -> Foo", T.arrow (T.arrow foo foo) foo)
|
||||
, ("Vector Foo", T.vectorOf foo)
|
||||
, ("forall a . a -> a", forall_aa)
|
||||
, ("(forall a . a) -> Number", T.forall' ["a"] (T.v' "a") `T.arrow` T.lit T.Number)
|
||||
]
|
||||
a = T.v' "a"
|
||||
foo = T.v' "Foo"
|
||||
forall_aa = T.forall' ["a"] (T.arrow a a)
|
||||
|
||||
main :: IO ()
|
||||
main = defaultMain tests
|
||||
@ -1,215 +0,0 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Unison.Test.Typechecker where
|
||||
|
||||
import Data.Functor
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Unison.Codebase.MemCodebase ()
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Term as E
|
||||
import Unison.Paths (Path)
|
||||
import Unison.Type as T
|
||||
import Unison.Typechecker as Typechecker
|
||||
import Unison.View (DFO)
|
||||
import Unison.Reference (Reference)
|
||||
import Unison.DataDeclaration (DataDeclaration)
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Parsers as Parsers
|
||||
import qualified Unison.Paths as Paths
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Test.Term as Term
|
||||
|
||||
type V = Symbol DFO
|
||||
type TTerm = Term.TTerm
|
||||
type TType = Type V
|
||||
type TEnv f = T.Env f V
|
||||
type TCodebase = IO Common.TCodebase
|
||||
|
||||
infixr 1 -->
|
||||
(-->) :: TType -> TType -> TType
|
||||
(-->) = T.arrow
|
||||
|
||||
data StrongEq = StrongEq TType
|
||||
instance Eq StrongEq where StrongEq t1 == StrongEq t2 = Typechecker.equals t1 t2
|
||||
instance Show StrongEq where show (StrongEq t) = show t
|
||||
|
||||
env :: TCodebase -> TEnv IO
|
||||
env codebase r = do
|
||||
(codebase, _, _, _) <- Note.lift codebase
|
||||
Codebase.typeAt codebase (E.ref r) mempty
|
||||
|
||||
decls :: TCodebase -> Reference -> Note.Noted IO (DataDeclaration V)
|
||||
decls code r = do
|
||||
(code, _, _, _) <- Note.lift code
|
||||
Codebase.dataDeclaration code r
|
||||
|
||||
localsAt :: TCodebase -> Path -> TTerm -> IO [(V, Type V)]
|
||||
localsAt codebase path e = Note.run $ Typechecker.locals (env codebase) (decls codebase) path e
|
||||
|
||||
synthesizesAt :: TCodebase -> Path -> TTerm -> TType -> Assertion
|
||||
synthesizesAt codebase path e t = Note.run $ do
|
||||
(codebase, _, _, _) <- Note.lift codebase
|
||||
t2 <- Codebase.typeAt codebase e path
|
||||
_ <- Note.fromEither (Typechecker.subtype t2 t)
|
||||
_ <- Note.fromEither (Typechecker.subtype t t2)
|
||||
pure ()
|
||||
|
||||
checksAt :: TCodebase -> Path -> TTerm -> TType -> Assertion
|
||||
checksAt code path e t = Note.run . void $
|
||||
Typechecker.synthesize (env code) (decls code) (Paths.modifyTerm' (\e -> E.wrapV (E.ann e t)) path e)
|
||||
|
||||
synthesizesAndChecksAt :: TCodebase -> Path -> TTerm -> TType -> Assertion
|
||||
synthesizesAndChecksAt code path e t =
|
||||
synthesizesAt code path e t >> checksAt code path e t
|
||||
|
||||
synthesizes :: TCodebase -> TTerm -> TType -> Assertion
|
||||
synthesizes code e t = Note.run $ do
|
||||
t2 <- Typechecker.synthesize (env code) (decls code) e
|
||||
_ <- Note.fromEither (Typechecker.subtype t2 t)
|
||||
_ <- Note.fromEither (Typechecker.subtype t t2)
|
||||
pure ()
|
||||
|
||||
checks :: TCodebase -> TTerm -> TType -> Assertion
|
||||
checks code e t = void $ Note.run (Typechecker.check (env code) (decls code) e t)
|
||||
|
||||
checkSubtype :: TType -> TType -> Assertion
|
||||
checkSubtype t1 t2 = case Typechecker.subtype t1 t2 of
|
||||
Left err -> assertFailure ("subtype failure:\n" ++ show err)
|
||||
Right _ -> pure ()
|
||||
|
||||
synthesizesAndChecks :: TCodebase -> TTerm -> TType -> Assertion
|
||||
synthesizesAndChecks code e t =
|
||||
synthesizes code e t >> checks code e t
|
||||
|
||||
--singleTest = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typechecker"
|
||||
-- [
|
||||
-- testTerm "f -> let x = (let saved = f; 42); 1" $ \tms ->
|
||||
-- testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks node
|
||||
-- (unsafeParseTerm tms)
|
||||
-- (unsafeParseType "forall x. x -> Number")
|
||||
-- ]
|
||||
|
||||
testTerm :: String -> (String -> TestTree) -> TestTree
|
||||
testTerm termString f = f termString
|
||||
|
||||
unsafeParseTerm :: String -> TTerm
|
||||
unsafeParseTerm = Parsers.unsafeParseTerm
|
||||
|
||||
unsafeParseType :: String -> TType
|
||||
unsafeParseType = Parsers.unsafeParseType
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \code -> testGroup "Typechecker"
|
||||
[
|
||||
testCase "alpha equivalence (type)" $ assertEqual "const"
|
||||
(unsafeParseType "forall a b . a -> b -> a")
|
||||
(unsafeParseType "forall x y . x -> y -> x")
|
||||
, testCase "subtype (1)" $ checkSubtype
|
||||
(unsafeParseType "Number")
|
||||
(unsafeParseType "Number")
|
||||
, testCase "subtype (2)" $ checkSubtype
|
||||
(unsafeParseType "forall a . a")
|
||||
(unsafeParseType "Number")
|
||||
, testCase "subtype (3)" $ checkSubtype
|
||||
(unsafeParseType "forall a . a")
|
||||
(unsafeParseType "forall a . a")
|
||||
, testCase "strong equivalence (type)" $ assertEqual "types were not equal"
|
||||
(StrongEq (unsafeParseType "forall a b . a -> b -> a"))
|
||||
(StrongEq (unsafeParseType "forall y x . x -> y -> x"))
|
||||
, testTerm "42" $ \tms -> testCase ("synthesize/check" ++ tms) $ synthesizesAndChecks code
|
||||
(unsafeParseTerm tms)
|
||||
(unsafeParseType "Number")
|
||||
, testCase "synthesize/check Term.id" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "a -> a")
|
||||
(unsafeParseType "forall b . b -> b")
|
||||
, testCase "synthesize/check Term.const" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "x y -> x")
|
||||
(unsafeParseType "forall a b . a -> b -> a")
|
||||
, testCase "synthesize/check (x y -> y)" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "x y -> y")
|
||||
(unsafeParseType "forall a b . a -> b -> b")
|
||||
, testCase "synthesize/check (let f = (+); f 1;;)" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "let { f = (+); f 1 }")
|
||||
(T.lit T.Number --> T.lit T.Number)
|
||||
, testCase "synthesize/check (let { blank x = _; blank 1 })" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "let { blank x = _; blank 1 }")
|
||||
(forall' ["a"] $ T.v' "a")
|
||||
, testCase "synthesize/check Term.fix" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "let rec { fix f = f (fix f); fix }")
|
||||
(forall' ["a"] $ (T.v' "a" --> T.v' "a") --> T.v' "a")
|
||||
, testCase "synthesize/check Term.pingpong1" $ synthesizesAndChecks code
|
||||
Term.pingpong1
|
||||
(forall' ["a"] $ T.v' "a")
|
||||
, testCase "synthesize/check [1,2,1+1]" $ synthesizesAndChecks code
|
||||
(unsafeParseTerm "[1, 2, 1 + 1]")
|
||||
(T.lit T.Vector `T.app` T.lit T.Number)
|
||||
, testTerm "[1, 2, 1 + 1]" $ \tms ->
|
||||
testCase ("synthesize/checkAt "++tms++"@[Paths.Arg, Index 2]") $ synthesizesAndChecksAt code
|
||||
[Paths.Arg, Paths.Index 2] (unsafeParseTerm tms) (T.lit T.Number)
|
||||
, testTerm "let { x = _; _}" $ \tms ->
|
||||
testCase ("synthesize/checkAt ("++tms++")@[Binding 0,Body]") $ synthesizesAndChecksAt code
|
||||
[Paths.Binding 0, Paths.Body] (unsafeParseTerm tms) unconstrained
|
||||
-- fails
|
||||
, testTerm "f -> let { x = let { saved = f; 42 }; 1 }" $ \tms ->
|
||||
testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks code
|
||||
(unsafeParseTerm tms)
|
||||
(unsafeParseType "forall x . x -> Number")
|
||||
, testTerm "f -> let { x = (b a -> b) 42 f; 1 }" $ \tms ->
|
||||
testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks code
|
||||
(unsafeParseTerm tms) (unsafeParseType "forall x . x -> Number")
|
||||
, testTerm "f x y -> (x y -> y) f _ + _" $ \tms ->
|
||||
testCase ("synthesize/check ("++tms++")") $ do
|
||||
synthesizesAndChecks code
|
||||
(unsafeParseTerm tms)
|
||||
(unsafeParseType "forall a b c . a -> b -> c -> Number")
|
||||
, testTerm "(id -> let { x = id 42; y = id \"hi\"; 43 }) : (forall a . a -> a) -> Number" $ \tms ->
|
||||
testCase ("higher rank checking: " ++ tms) $
|
||||
let
|
||||
t = unsafeParseType "(forall a . a -> a) -> Number"
|
||||
tm = unsafeParseTerm tms
|
||||
in synthesizesAndChecks code tm t
|
||||
-- Let generalization not implemented yet; this test fails
|
||||
--, testCase "let generalization: let id a = a; x = id 42; y = id 'hi'; 23" $
|
||||
-- let
|
||||
-- tm = E.let1'
|
||||
-- [ ("id", E.lam' ["a"] (E.var' "a") `E.ann` T.forall' ["a"] (T.v' "a")),
|
||||
-- ("id@Number", E.var' "id" `E.app` E.num 42),
|
||||
-- ("id@Text", E.var' "id" `E.app` E.text "hi")
|
||||
-- ] (E.num 43)
|
||||
-- in synthesizesAndChecks code tm $ T.lit T.Number
|
||||
, testTerm "x y -> _ + _" $ \tms ->
|
||||
testCase ("locals ("++tms++")@[Body,Body,Fn,Arg]") $ do
|
||||
let tm = unsafeParseTerm tms
|
||||
[(_,xt), (_,yt)] <- localsAt code [Paths.Body, Paths.Body, Paths.Fn, Paths.Arg] tm
|
||||
assertEqual "xt unconstrainted" unconstrained (T.generalize xt)
|
||||
assertEqual "yt unconstrainted" unconstrained (T.generalize yt)
|
||||
, testTerm "let { x = _; _ }" $ \tms ->
|
||||
testCase ("locals ("++tms++")") $ do
|
||||
let tm = unsafeParseTerm tms
|
||||
[(_,xt)] <- localsAt code [Paths.Body] tm
|
||||
[] <- localsAt code [Paths.Binding 0, Paths.Body] tm
|
||||
assertEqual "xt unconstrainted" unconstrained (T.generalize xt)
|
||||
, testTerm "let { x = _; y = _; _ }" $ \tms ->
|
||||
testCase ("locals ("++tms++")@[Body,Body]") $ do
|
||||
let tm = unsafeParseTerm tms
|
||||
[(_,xt), (_,yt)] <- localsAt code [Paths.Body, Paths.Body] tm
|
||||
assertEqual "xt unconstrained" unconstrained (T.generalize xt)
|
||||
assertEqual "yt unconstrained" unconstrained (T.generalize yt)
|
||||
, testTerm "let { x = _; y = _; _ }" $ \tms ->
|
||||
-- testTerm "let x = 42; y = _; _" $ \tms ->
|
||||
-- testTerm "let x = 42; y = 43; _" $ \tms ->
|
||||
-- testTerm "let x = 42; y = 43; 4224" $ \tms ->
|
||||
testCase ("locals ("++tms++")@[Body,Binding 0,Body]") $ do
|
||||
let tm = unsafeParseTerm tms
|
||||
[(_,xt)] <- localsAt code [Paths.Body, Paths.Binding 0, Paths.Body] tm
|
||||
assertEqual "xt unconstrainted" unconstrained (T.generalize xt)
|
||||
]
|
||||
|
||||
unconstrained :: TType
|
||||
unconstrained = unsafeParseType "forall a . a"
|
||||
|
||||
main :: IO ()
|
||||
main = defaultMain tests
|
||||
-- main = defaultMain singleTest
|
||||
@ -1,42 +1,35 @@
|
||||
module Unison.Test.Typechecker.Components where
|
||||
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import EasyTest
|
||||
import Unison.Parsers (unsafeParseTerm)
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Term as Term
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Typechecker.Components as Components
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
|
||||
let
|
||||
tests =
|
||||
[
|
||||
-- simple case, no minimization done
|
||||
t "let { id x = x; g = id 42; y = id id g; y }"
|
||||
"let { id x = x; g = id 42; y = id id g; y }"
|
||||
-- check that we get let generalization
|
||||
, t "let rec { id x = x; g = id 42; y = id id g; y }"
|
||||
"let { id x = x; g = id 42; y = id id g; y }"
|
||||
-- check that we preserve order of components as much as possible
|
||||
, t "let rec { id2 x = x; id1 x = x; id3 x = x; id3 }"
|
||||
"let { id2 x = x; id1 x = x; id3 x = x; id3 }"
|
||||
-- check that we reorder according to dependencies
|
||||
, t "let rec { g = id 42; y = id id g; id x = x; y }"
|
||||
"let { id x = x; g = id 42; y = id id g; y }"
|
||||
-- insane example, checks for: generalization, reordering,
|
||||
-- preservation of order when possible
|
||||
, t "let rec { g = id 42; y = id id g; ping x = pong x; pong x = id (ping x); id x = x; y }"
|
||||
"let { id x = x; g = id 42; y = id id g ; (let rec { ping x = pong x; pong x = id (ping x) ; y })}"
|
||||
]
|
||||
t before after = testCase (before ++ " ⟹ " ++ after) $ do
|
||||
(codebase, _, _, _) <- codebase
|
||||
let term = unsafeParseTerm before
|
||||
let after' = Components.minimize' term
|
||||
_ <- Note.run $ Codebase.typeAt codebase after' []
|
||||
assertEqual "comparing results" (unsafeParseTerm after) after'
|
||||
in testGroup "Typechecker.Components" tests
|
||||
|
||||
main = defaultMain tests
|
||||
test :: Common.CodebaseIOV -> Test ()
|
||||
test codebase = scope "Typechecker.Components" $ tests
|
||||
[
|
||||
-- simple case, no minimization done
|
||||
t "let { id x = x; g = id 42; y = id id g; y }"
|
||||
"let { id x = x; g = id 42; y = id id g; y }"
|
||||
-- check that we get let generalization
|
||||
, t "let rec { id x = x; g = id 42; y = id id g; y }"
|
||||
"let { id x = x; g = id 42; y = id id g; y }"
|
||||
-- check that we preserve order of components as much as possible
|
||||
, t "let rec { id2 x = x; id1 x = x; id3 x = x; id3 }"
|
||||
"let { id2 x = x; id1 x = x; id3 x = x; id3 }"
|
||||
-- check that we reorder according to dependencies
|
||||
, t "let rec { g = id 42; y = id id g; id x = x; y }"
|
||||
"let { id x = x; g = id 42; y = id id g; y }"
|
||||
-- insane example, checks for: generalization, reordering,
|
||||
-- preservation of order when possible
|
||||
, t "let rec { g = id 42; y = id id g; ping x = pong x; pong x = id (ping x); id x = x; y }"
|
||||
"let { id x = x; g = id 42; y = id id g ; (let rec { ping x = pong x; pong x = id (ping x) ; y })}"
|
||||
]
|
||||
where
|
||||
t before after = scope (before ++ " ⟹ " ++ after) $ do
|
||||
let term = unsafeParseTerm before
|
||||
let after' = Components.minimize' term
|
||||
_ <- io . Note.run $ Codebase.typeAt codebase after' []
|
||||
expect (unsafeParseTerm after == after')
|
||||
|
||||
@ -118,11 +118,8 @@ test-suite tests
|
||||
base,
|
||||
bytestring,
|
||||
containers,
|
||||
easytest,
|
||||
filepath,
|
||||
tasty,
|
||||
tasty-hunit,
|
||||
tasty-smallcheck,
|
||||
tasty-quickcheck,
|
||||
text,
|
||||
transformers,
|
||||
unison-shared
|
||||
|
||||
@ -39,6 +39,9 @@ data Env =
|
||||
|
||||
newtype Test a = Test (ReaderT Env IO (Maybe a))
|
||||
|
||||
io :: IO a -> Test a
|
||||
io = liftIO
|
||||
|
||||
atomicLogger :: IO (String -> IO ())
|
||||
atomicLogger = do
|
||||
lock <- newMVar ()
|
||||
@ -90,7 +93,7 @@ run' seed note allow (Test t) = do
|
||||
e <- try (runReaderT (void t) (Env rngVar [] resultsQ note allow)) :: IO (Either SomeException ())
|
||||
case e of
|
||||
Left e -> note $ "Exception while running tests: " ++ show e
|
||||
Right () -> note $ "Waiting for any asynchronously spawned tests to complete ..."
|
||||
Right () -> pure ()
|
||||
atomically $ writeTQueue resultsQ Nothing
|
||||
_ <- A.waitCatch rs
|
||||
resultsMap <- readTVarIO results
|
||||
@ -134,14 +137,16 @@ parseMessages s = reverse (go s) where
|
||||
(hd, tl) -> hd : go (drop 1 tl)
|
||||
|
||||
scope :: String -> Test a -> Test a
|
||||
scope msg (Test t) = Test $ do
|
||||
env <- ask
|
||||
let messages' = msg : messages env
|
||||
dropRight1 [] = []
|
||||
dropRight1 xs = init xs
|
||||
case (null (allow env) || [msg] `isSuffixOf` allow env) of
|
||||
False -> putResult Skipped >> pure Nothing
|
||||
True -> liftIO $ runReaderT t (env { messages = messages', allow = dropRight1 (allow env) })
|
||||
scope msg t = foldr go t (parseMessages msg) where
|
||||
go :: String -> Test a -> Test a
|
||||
go msg (Test t) = Test $ do
|
||||
env <- ask
|
||||
let messages' = msg : messages env
|
||||
dropRight1 [] = []
|
||||
dropRight1 xs = init xs
|
||||
case (null (allow env) || [msg] `isSuffixOf` allow env) of
|
||||
False -> putResult Skipped >> pure Nothing
|
||||
True -> liftIO $ runReaderT t (env { messages = messages', allow = dropRight1 (allow env) })
|
||||
|
||||
note :: String -> Test ()
|
||||
note msg = do
|
||||
|
||||
Loading…
Reference in New Issue
Block a user