all shared tests now passing

This commit is contained in:
Paul Chiusano 2016-12-11 22:36:44 -05:00
parent 1e73a1a4be
commit 52840857cf
11 changed files with 175 additions and 145 deletions

View File

@ -1,6 +1,6 @@
{-# Language BangPatterns #-} {-# Language BangPatterns #-}
-- Copyright (c) 2013, Edward Kmett, Luke Palmer -- Copyright (c) 2013, Edward Kmett, Luke Palmer, Paul Chiusano
-- --
-- All rights reserved. -- All rights reserved.
-- --
@ -52,11 +52,12 @@ module Text.Parsec.Layout
, HasLayoutEnv(..) , HasLayoutEnv(..)
, maybeFollowedBy , maybeFollowedBy
, virtual_rbrace , virtual_rbrace
, withoutLayout
) where ) where
import Data.Functor import Data.Functor
import Control.Applicative ((<$>)) import Control.Applicative ((<$>))
import Control.Monad (guard) import Control.Monad
import Data.Char (isSpace) import Data.Char (isSpace)
@ -133,6 +134,10 @@ pushCurrentContext = do
maybeFollowedBy :: Stream s m c => ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m a maybeFollowedBy :: Stream s m c => ParsecT s u m a -> ParsecT s u m b -> ParsecT s u m a
t `maybeFollowedBy` x = do t' <- t; optional x; return t' t `maybeFollowedBy` x = do t' <- t; optional x; return t'
withoutLayout :: (HasLayoutEnv u, Stream s m c) => String -> ParsecT s u m a -> ParsecT s u m a
withoutLayout endMsg p =
pushContext NoLayout *> (p <* popContext endMsg)
-- | @(\``maybeFollowedBy`\` space)@ -- | @(\``maybeFollowedBy`\` space)@
spaced :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m a -> ParsecT s u m a spaced :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m a -> ParsecT s u m a
spaced t = t `maybeFollowedBy` space spaced t = t `maybeFollowedBy` space
@ -200,11 +205,31 @@ layout = try $ do
layoutSatisfies :: (HasLayoutEnv u, Stream s m Char) => (Layout -> Bool) -> ParsecT s u m () layoutSatisfies :: (HasLayoutEnv u, Stream s m Char) => (Layout -> Bool) -> ParsecT s u m ()
layoutSatisfies p = guard . p =<< layout layoutSatisfies p = guard . p =<< layout
inLayout :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m Bool
inLayout = do
env <- getEnv
pure $ case envLayout env of
[] -> True
(NoLayout:_) -> False
(Layout _:_) -> True
pushIncrementedContext :: (HasLayoutEnv u, Stream s m c) => ParsecT s u m ()
pushIncrementedContext = do
env <- getEnv
case envLayout env of
[] -> pushContext (Layout 1)
(Layout n : _) -> pushContext (Layout (n + 1))
(NoLayout : _) -> pure ()
virtual_lbrace :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m () virtual_lbrace :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m ()
virtual_lbrace = pushCurrentContext virtual_lbrace = do
allow <- inLayout
when allow pushCurrentContext
virtual_rbrace :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m () virtual_rbrace :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m ()
virtual_rbrace = eof <|> try (layoutSatisfies (VBrace ==) <?> "outdent") virtual_rbrace = do
allow <- inLayout
when allow $ eof <|> try (layoutSatisfies (VBrace ==) <?> "outdent")
-- | Consumes one or more spaces, comments, and onside newlines in a layout rule. -- | Consumes one or more spaces, comments, and onside newlines in a layout rule.
space :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m String space :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m String
@ -237,10 +262,14 @@ rbrace = do
return "}" return "}"
block :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m a -> ParsecT s u m a block :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m a -> ParsecT s u m a
block p = try (braced p) <|> try (vbraced p) <|> p where block p = braced p <|> vbraced p where
braced s = between (spaced lbrace) (spaced rbrace) s braced s = between (try (spaced lbrace)) (spaced rbrace) s
vbraced s = between (spaced virtual_lbrace) (spaced virtual_rbrace) s vbraced s = between (spaced virtual_lbrace) (spaced virtual_rbrace) s
-- block p = p <* lookAhead (spaced (virtual_lbrace <|> void semi)) -- NB: virtual_lbrace here doesn't use current column for offside calc, instead
-- uses 1 column greater than whatever column is at top of layout stack
virtual_lbrace = do
allow <- inLayout
when allow pushIncrementedContext
-- | Repeat a parser in layout, separated by (virtual) semicolons. -- | Repeat a parser in layout, separated by (virtual) semicolons.
laidout :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m a -> ParsecT s u m [a] laidout :: (HasLayoutEnv u, Stream s m Char) => ParsecT s u m a -> ParsecT s u m [a]

View File

@ -53,6 +53,7 @@ unvar (Free v) = v
unvar (Bound v) = v unvar (Bound v) = v
instance Var v => Var (V v) where instance Var v => Var (V v) where
rename n2 = fmap (Var.rename n2)
named txt = Bound (Var.named txt) named txt = Bound (Var.named txt)
name v = Var.name (unvar v) name v = Var.name (unvar v)
qualifiedName v = Var.qualifiedName (unvar v) qualifiedName v = Var.qualifiedName (unvar v)

View File

@ -1,6 +1,7 @@
{-# Language DeriveFunctor #-} {-# Language DeriveFunctor #-}
{-# Language DeriveTraversable #-} {-# Language DeriveTraversable #-}
{-# Language DeriveFoldable #-} {-# Language DeriveFoldable #-}
{-# Language BangPatterns #-}
module Unison.Parser where module Unison.Parser where
@ -107,9 +108,9 @@ wordyId :: [String] -> Parser s String
wordyId keywords = label "wordyId" . token $ do wordyId keywords = label "wordyId" . token $ do
op <- (False <$ symbolyId keywords) <|> pure True op <- (False <$ symbolyId keywords) <|> pure True
guard op guard op
f <$> sepBy1 dot id f <$> sepBy1 dot id -- todo: this screws up ∀ a. without a space following 'a'
where where
dot = char '.' dot = attempt (char '.')
id = identifier "alphanumeric identifier" id = identifier "alphanumeric identifier"
[any (not . Char.isDigit), any Char.isAlphaNum, (`notElem` keywords)] [any (not . Char.isDigit), any Char.isAlphaNum, (`notElem` keywords)]
f segs = intercalate "." segs f segs = intercalate "." segs
@ -129,8 +130,8 @@ token p = attempt (L.spaced p)
parenthesized :: Parser s a -> Parser s a parenthesized :: Parser s a -> Parser s a
parenthesized p = lp *> body <* rp parenthesized p = lp *> body <* rp
where where
lp = token (char '(') lp = char '(' <* L.withoutLayout "space" (optional L.space)
body = p body = L.withoutLayout "parentheses" p
rp = token (char ')') rp = token (char ')')
takeWhile :: String -> (Char -> Bool) -> Parser s String takeWhile :: String -> (Char -> Bool) -> Parser s String

View File

@ -18,7 +18,10 @@ type TermV = Term V
parse' :: P.Parser (PS.S V) a -> String -> Either String a parse' :: P.Parser (PS.S V) a -> String -> Either String a
parse' p input = P.run p input PS.s0 parse' p input = P.run p input PS.s0
parse :: P.Parser (PS.S V) TermV -> String -> Either String TermV -- parse :: P.Parser (PS.S V) TermV -> String -> Either String TermV
-- parse p input = P.run p input PS.s0
parse :: P.Parser (PS.S V) [(V,TermV)] -> String -> Either String [(V, TermV)]
parse p input = P.run p input PS.s0 parse p input = P.run p input PS.s0
input' = unlines input' = unlines
@ -28,17 +31,14 @@ input' = unlines
, " x = 2" , " x = 2"
, " x + 1" ] , " x + 1" ]
input = "let { x = 1 ; x }" -- input = "let { x = 1 ; x }"
input = "(do Remote { pure 42 } )"
-- input = "let\n x = 1\n x" -- input = "let\n x = 1\n x"
main :: IO () main :: IO ()
main = main = do
let p = E.term input <- readFile "unison-src/base.u"
-- p2 = parser let p = E.moduleBindings
--in case parse' p2 "let { a; a; a }" of case parse p input of
-- Left err -> putStrLn err
-- Right a -> putStrLn (show a)
-- in case parse p "let { x=1; x }" of
in case parse p "let { a = 2 ; 1 }" of
Left err -> putStrLn err Left err -> putStrLn err
Right a -> putStrLn (show a) Right a -> putStrLn (show a)

View File

@ -57,11 +57,11 @@ term :: Var v => Parser (S v) (Term v)
term = term2 term = term2
term2 :: Var v => Parser (S v) (Term v) term2 :: Var v => Parser (S v) (Term v)
term2 = let_ <|> lam term2 <|> term3 term2 = lam term2 <|> effectBlock <|> term3
term3 :: Var v => Parser (S v) (Term v) term3 :: Var v => Parser (S v) (Term v)
term3 = do term3 = do
t <- ifthen <|> infixApp t <- let_ <|> ifthen <|> infixApp
ot <- optional (token (char ':') *> TypeParser.type_) ot <- optional (token (char ':') *> TypeParser.type_)
pure $ case ot of pure $ case ot of
Nothing -> t Nothing -> t
@ -80,7 +80,7 @@ term4 = f <$> some term5
f [] = error "'some' shouldn't produce an empty list" f [] = error "'some' shouldn't produce an empty list"
term5 :: Var v => Parser (S v) (Term v) term5 :: Var v => Parser (S v) (Term v)
term5 = label "effect block" effectBlock <|> termLeaf term5 = termLeaf
termLeaf :: Var v => Parser (S v) (Term v) termLeaf :: Var v => Parser (S v) (Term v)
termLeaf = termLeaf =
@ -89,9 +89,9 @@ termLeaf =
ifthen :: Var v => Parser (S v) (Term v) ifthen :: Var v => Parser (S v) (Term v)
ifthen = do ifthen = do
_ <- token (string "if") _ <- token (string "if")
cond <- term cond <- L.withoutLayout "then" term
_ <- token (string "then") _ <- token (string "then")
iftrue <- term iftrue <- L.withoutLayout "else" term
_ <- token (string "else") _ <- token (string "else")
iffalse <- L.block term iffalse <- L.block term
pure (Term.apps (Term.lit Term.If) [cond, iftrue, iffalse]) pure (Term.apps (Term.lit Term.If) [cond, iftrue, iffalse])

View File

@ -15,7 +15,7 @@ tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
[ t "1 + 1" "2" [ t "1 + 1" "2"
, t "1 + 1 + 1" "3" , t "1 + 1 + 1" "3"
, t "(x -> x) 42" "42" , t "(x -> x) 42" "42"
, t "let x = 2; y = 3 ; x + y;;" "5" , t "let { x = 2; y = 3 ; x + y }" "5"
, t "if False then 0 else 1" "1" , t "if False then 0 else 1" "1"
, t "if True then 12 else 13" "12" , t "if True then 12 else 13" "12"
, t "1 >_Number 0" "True" , t "1 >_Number 0" "True"
@ -41,12 +41,12 @@ tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
, t "False `and` False" "False" , t "False `and` False" "False"
, t "not False" "True" , t "not False" "True"
, t "not True" "False" , 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 { 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;;" , t "let rec { ping n = if n >=_Number 10 then n else pong (n + 1); pong n = ping (n + 1); ping 0}"
"10" "10"
, t "let id x = x; g = id 42; p = id \"hi\" ; g;;" "42" , 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 : 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 "(let { id x = x; id } : forall a . a -> a) 42" "42"
, t "Optional.map ((+) 1) (Some 1)" "Some 2" , t "Optional.map ((+) 1) (Some 1)" "Some 2"
, t "Optional.map ((+) 1) ((Some: ∀ a . a -> Optional a) 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) (Left 1)" "2"

View File

@ -115,11 +115,11 @@ pingpong1 :: TTerm
pingpong1 = pingpong1 =
unsafeParseTerm $ unsafeParseTerm $
unlines [ "let rec " unlines [ "let rec "
, " ping x = pong (x + 1);" , " ping x = pong (x + 1)"
, " pong y = ping (y - 1);" , " pong y = ping (y - 1)"
, " ping 1;;" , " ping 1"
] ]
pingpong2 :: TTerm pingpong2 :: TTerm
pingpong2 = pingpong2 =
unsafeParseTerm $ "let rec pong1 p = ping1 (p - 1); ping1 q = pong1 (q + 1); ping1 1;;" unsafeParseTerm $ "let rec { pong1 p = ping1 (p - 1); ping1 q = pong1 (q + 1); ping1 1 }"

View File

@ -48,7 +48,7 @@ tests = testGroup "TermParser" $ (parse <$> shouldPass)
, ("#V-f/XHD3-N0E", "invalid base64url") , ("#V-f/XHD3-N0E", "invalid base64url")
] ]
shouldParse = shouldParse =
[ "do Remote n1 := Remote.spawn; n2 := Remote.spawn; let rec { x = 10; Remote.pure 42 }" ] [ "do Remote { n1 := Remote.spawn; n2 := Remote.spawn; let rec { x = 10; Remote.pure 42 }}" ]
shouldPass = shouldPass =
[ ("1", one) [ ("1", one)
, ("[1,1]", vectorForced [one, one]) , ("[1,1]", vectorForced [one, one])
@ -83,18 +83,18 @@ tests = testGroup "TermParser" $ (parse <$> shouldPass)
, ("a b -> a + b : Int", lam' ["a", "b"] (ann (apps numberplus [a, b]) int)) , ("a b -> a + b : Int", lam' ["a", "b"] (ann (apps numberplus [a, b]) int))
, ("a -> a", lam' ["a"] a) , ("a -> a", lam' ["a"] a)
, ("(a -> a) : forall a . a -> a", ann (lam' ["a"] a) (T.forall' ["a"] (T.arrow 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 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 { 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 { 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\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 (+) : 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]])) , ("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 -- from Unison.Test.Term
, ("a -> a", lam' ["a"] $ var' "a") -- id , ("a -> a", lam' ["a"] $ var' "a") -- id
, ("x y -> x", lam' ["x", "y"] $ var' "x") -- const , ("x y -> x", lam' ["x", "y"] $ var' "x") -- const
, ("let rec fix = f -> f (fix f); fix", fix) -- fix , ("let rec { fix = f -> f (fix f); fix }", fix) -- fix
, ("let rec\n fix f = f (fix f)\n 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 + 3", num 1 `plus'` num 2 `plus'` num 3)
, ("[1, 2, 1 + 1]", vectorForced [num 1, num 2, num 1 `plus'` num 1]) , ("[1, 2, 1 + 1]", vectorForced [num 1, num 2, num 1 `plus'` num 1])
@ -105,13 +105,13 @@ tests = testGroup "TermParser" $ (parse <$> shouldPass)
, ("#" ++ Text.unpack sampleHash64, derived' sampleHash64) , ("#" ++ Text.unpack sampleHash64, derived' sampleHash64)
, ("#" ++ Text.unpack sampleHash512, derived' sampleHash512) , ("#" ++ Text.unpack sampleHash512, derived' sampleHash512)
, ("(do Remote { pure 42 } )", builtin "Remote.pure" `app` num 42) , ("(do Remote { pure 42 } )", builtin "Remote.pure" `app` num 42)
, ("do Remote x = 42; pure (x + 1) ", , ("do Remote { x = 42; pure (x + 1) } ",
builtin "Remote.bind" `apps` [ builtin "Remote.bind" `apps` [
lam' ["q"] (builtin "Remote.pure" `app` (var' "q" `plus'` num 1)), lam' ["q"] (builtin "Remote.pure" `app` (var' "q" `plus'` num 1)),
builtin "Remote.pure" `app` num 42 builtin "Remote.pure" `app` num 42
] ]
) )
, ("do Remote x := pure 42; pure (x + 1) ", , ("do Remote { x := pure 42; pure (x + 1) } ",
builtin "Remote.bind" `apps` [ builtin "Remote.bind" `apps` [
lam' ["q"] (builtin "Remote.pure" `app` (var' "q" `plus'` num 1)), lam' ["q"] (builtin "Remote.pure" `app` (var' "q" `plus'` num 1)),
builtin "Remote.pure" `app` num 42 builtin "Remote.pure" `app` num 42

View File

@ -99,40 +99,40 @@ tests :: TestTree
tests = withResource Common.codebase (\_ -> pure ()) $ \node -> testGroup "Typechecker" tests = withResource Common.codebase (\_ -> pure ()) $ \node -> testGroup "Typechecker"
[ [
testCase "alpha equivalence (type)" $ assertEqual "const" testCase "alpha equivalence (type)" $ assertEqual "const"
(unsafeParseType "forall a b. a -> b -> a") (unsafeParseType "forall a b . a -> b -> a")
(unsafeParseType "forall x y. x -> y -> x") (unsafeParseType "forall x y . x -> y -> x")
, testCase "subtype (1)" $ checkSubtype , testCase "subtype (1)" $ checkSubtype
(unsafeParseType "Number") (unsafeParseType "Number")
(unsafeParseType "Number") (unsafeParseType "Number")
, testCase "subtype (2)" $ checkSubtype , testCase "subtype (2)" $ checkSubtype
(unsafeParseType "forall a. a") (unsafeParseType "forall a . a")
(unsafeParseType "Number") (unsafeParseType "Number")
, testCase "subtype (3)" $ checkSubtype , testCase "subtype (3)" $ checkSubtype
(unsafeParseType "forall a. a") (unsafeParseType "forall a . a")
(unsafeParseType "forall a. a") (unsafeParseType "forall a . a")
, testCase "strong equivalence (type)" $ assertEqual "types were not equal" , testCase "strong equivalence (type)" $ assertEqual "types were not equal"
(StrongEq (unsafeParseType "forall a b. a -> b -> a")) (StrongEq (unsafeParseType "forall a b . a -> b -> a"))
(StrongEq (unsafeParseType "forall y x. x -> y -> x")) (StrongEq (unsafeParseType "forall y x . x -> y -> x"))
, testTerm "42" $ \tms -> testCase ("synthesize/check" ++ tms) $ synthesizesAndChecks node , testTerm "42" $ \tms -> testCase ("synthesize/check" ++ tms) $ synthesizesAndChecks node
(unsafeParseTerm tms) (unsafeParseTerm tms)
(unsafeParseType "Number") (unsafeParseType "Number")
, testCase "synthesize/check Term.id" $ synthesizesAndChecks node , testCase "synthesize/check Term.id" $ synthesizesAndChecks node
(unsafeParseTerm "a -> a") (unsafeParseTerm "a -> a")
(unsafeParseType "forall b. b -> b") (unsafeParseType "forall b . b -> b")
, testCase "synthesize/check Term.const" $ synthesizesAndChecks node , testCase "synthesize/check Term.const" $ synthesizesAndChecks node
(unsafeParseTerm "x y -> x") (unsafeParseTerm "x y -> x")
(unsafeParseType "forall a b. a -> b -> a") (unsafeParseType "forall a b . a -> b -> a")
, testCase "synthesize/check (x y -> y)" $ synthesizesAndChecks node , testCase "synthesize/check (x y -> y)" $ synthesizesAndChecks node
(unsafeParseTerm "x y -> y") (unsafeParseTerm "x y -> y")
(unsafeParseType "forall a b. a -> b -> b") (unsafeParseType "forall a b . a -> b -> b")
, testCase "synthesize/check (let f = (+); f 1;;)" $ synthesizesAndChecks node , testCase "synthesize/check (let f = (+); f 1;;)" $ synthesizesAndChecks node
(unsafeParseTerm "let f = (+); f 1;;") (unsafeParseTerm "let { f = (+); f 1 }")
(T.lit T.Number --> T.lit T.Number) (T.lit T.Number --> T.lit T.Number)
, testCase "synthesize/check (let blank x = _; blank 1;;)" $ synthesizesAndChecks node , testCase "synthesize/check (let { blank x = _; blank 1 })" $ synthesizesAndChecks node
(unsafeParseTerm "let blank x = _; blank 1;;") (unsafeParseTerm "let { blank x = _; blank 1 }")
(forall' ["a"] $ T.v' "a") (forall' ["a"] $ T.v' "a")
, testCase "synthesize/check Term.fix" $ synthesizesAndChecks node , testCase "synthesize/check Term.fix" $ synthesizesAndChecks node
(unsafeParseTerm "let rec fix f = f (fix f); fix;;") (unsafeParseTerm "let rec { fix f = f (fix f); fix }")
(forall' ["a"] $ (T.v' "a" --> T.v' "a") --> T.v' "a") (forall' ["a"] $ (T.v' "a" --> T.v' "a") --> T.v' "a")
, testCase "synthesize/check Term.pingpong1" $ synthesizesAndChecks node , testCase "synthesize/check Term.pingpong1" $ synthesizesAndChecks node
Term.pingpong1 Term.pingpong1
@ -143,23 +143,23 @@ tests = withResource Common.codebase (\_ -> pure ()) $ \node -> testGroup "Typec
, testTerm "[1, 2, 1 + 1]" $ \tms -> , testTerm "[1, 2, 1 + 1]" $ \tms ->
testCase ("synthesize/checkAt "++tms++"@[Paths.Arg, Index 2]") $ synthesizesAndChecksAt node testCase ("synthesize/checkAt "++tms++"@[Paths.Arg, Index 2]") $ synthesizesAndChecksAt node
[Paths.Arg, Paths.Index 2] (unsafeParseTerm tms) (T.lit T.Number) [Paths.Arg, Paths.Index 2] (unsafeParseTerm tms) (T.lit T.Number)
, testTerm "let x = _; _;;" $ \tms -> , testTerm "let { x = _; _}" $ \tms ->
testCase ("synthesize/checkAt ("++tms++")@[Binding 0,Body]") $ synthesizesAndChecksAt node testCase ("synthesize/checkAt ("++tms++")@[Binding 0,Body]") $ synthesizesAndChecksAt node
[Paths.Binding 0, Paths.Body] (unsafeParseTerm tms) unconstrained [Paths.Binding 0, Paths.Body] (unsafeParseTerm tms) unconstrained
-- fails -- fails
, testTerm "f -> let x = (let saved = f; 42;;); 1;;" $ \tms -> , testTerm "f -> let { x = let { saved = f; 42 }; 1 }" $ \tms ->
testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks node testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks node
(unsafeParseTerm tms) (unsafeParseTerm tms)
(unsafeParseType "forall x. x -> Number") (unsafeParseType "forall x . x -> Number")
, testTerm "f -> let x = (b a -> b) 42 f; 1;;" $ \tms -> , testTerm "f -> let { x = (b a -> b) 42 f; 1 }" $ \tms ->
testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks node testCase ("synthesize/check ("++tms++")") $ synthesizesAndChecks node
(unsafeParseTerm tms) (unsafeParseType "forall x. x -> Number") (unsafeParseTerm tms) (unsafeParseType "forall x . x -> Number")
, testTerm "f x y -> (x y -> y) f _ + _" $ \tms -> , testTerm "f x y -> (x y -> y) f _ + _" $ \tms ->
testCase ("synthesize/check ("++tms++")") $ do testCase ("synthesize/check ("++tms++")") $ do
synthesizesAndChecks node synthesizesAndChecks node
(unsafeParseTerm tms) (unsafeParseTerm tms)
(unsafeParseType "forall a b c. a -> b -> c -> Number") (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 -> , testTerm "(id -> let { x = id 42; y = id \"hi\"; 43 }) : (forall a . a -> a) -> Number" $ \tms ->
testCase ("higher rank checking: " ++ tms) $ testCase ("higher rank checking: " ++ tms) $
let let
t = unsafeParseType "(forall a . a -> a) -> Number" t = unsafeParseType "(forall a . a -> a) -> Number"
@ -180,19 +180,19 @@ tests = withResource Common.codebase (\_ -> pure ()) $ \node -> testGroup "Typec
[(_,xt), (_,yt)] <- localsAt node [Paths.Body, Paths.Body, Paths.Fn, Paths.Arg] tm [(_,xt), (_,yt)] <- localsAt node [Paths.Body, Paths.Body, Paths.Fn, Paths.Arg] tm
assertEqual "xt unconstrainted" unconstrained (T.generalize xt) assertEqual "xt unconstrainted" unconstrained (T.generalize xt)
assertEqual "yt unconstrainted" unconstrained (T.generalize yt) assertEqual "yt unconstrainted" unconstrained (T.generalize yt)
, testTerm "let x = _; _;;" $ \tms -> , testTerm "let { x = _; _ }" $ \tms ->
testCase ("locals ("++tms++")") $ do testCase ("locals ("++tms++")") $ do
let tm = unsafeParseTerm tms let tm = unsafeParseTerm tms
[(_,xt)] <- localsAt node [Paths.Body] tm [(_,xt)] <- localsAt node [Paths.Body] tm
[] <- localsAt node [Paths.Binding 0, Paths.Body] tm [] <- localsAt node [Paths.Binding 0, Paths.Body] tm
assertEqual "xt unconstrainted" unconstrained (T.generalize xt) assertEqual "xt unconstrainted" unconstrained (T.generalize xt)
, testTerm "let x = _; y = _; _;;" $ \tms -> , testTerm "let { x = _; y = _; _ }" $ \tms ->
testCase ("locals ("++tms++")@[Body,Body]") $ do testCase ("locals ("++tms++")@[Body,Body]") $ do
let tm = unsafeParseTerm tms let tm = unsafeParseTerm tms
[(_,xt), (_,yt)] <- localsAt node [Paths.Body, Paths.Body] tm [(_,xt), (_,yt)] <- localsAt node [Paths.Body, Paths.Body] tm
assertEqual "xt unconstrained" unconstrained (T.generalize xt) assertEqual "xt unconstrained" unconstrained (T.generalize xt)
assertEqual "yt unconstrained" unconstrained (T.generalize yt) assertEqual "yt unconstrained" unconstrained (T.generalize yt)
, testTerm "let x = _; y = _; _;;" $ \tms -> , testTerm "let { x = _; y = _; _ }" $ \tms ->
-- testTerm "let x = 42; y = _; _" $ \tms -> -- testTerm "let x = 42; y = _; _" $ \tms ->
-- testTerm "let x = 42; y = 43; _" $ \tms -> -- testTerm "let x = 42; y = 43; _" $ \tms ->
-- testTerm "let x = 42; y = 43; 4224" $ \tms -> -- testTerm "let x = 42; y = 43; 4224" $ \tms ->
@ -203,7 +203,7 @@ tests = withResource Common.codebase (\_ -> pure ()) $ \node -> testGroup "Typec
] ]
unconstrained :: TType unconstrained :: TType
unconstrained = unsafeParseType "forall a. a" unconstrained = unsafeParseType "forall a . a"
main :: IO () main :: IO ()
main = defaultMain tests main = defaultMain tests

View File

@ -15,21 +15,21 @@ tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
tests = tests =
[ [
-- simple case, no minimization done -- simple case, no minimization done
t "let id x = x; g = id 42; y = id id g; y;;" 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;;" "let { id x = x; g = id 42; y = id id g; y }"
-- check that we get let generalization -- check that we get let generalization
, t "let rec id x = x; g = id 42; y = id id g; y;;" , 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;;" "let { id x = x; g = id 42; y = id id g; y }"
-- check that we preserve order of components as much as possible -- check that we preserve order of components as much as possible
, t "let rec id2 x = x; id1 x = x; id3 x = x; id3;;" , t "let rec { id2 x = x; id1 x = x; id3 x = x; id3 }"
"let 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 -- check that we reorder according to dependencies
, t "let rec g = id 42; y = id id g; id x = x; y;;" , 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;;" "let { id x = x; g = id 42; y = id id g; y }"
-- insane example, checks for: generalization, reordering, -- insane example, checks for: generalization, reordering,
-- preservation of order when possible -- 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;;" , 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;;);;" "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 t before after = testCase (before ++ "" ++ after) $ do
(codebase, _, _, _) <- codebase (codebase, _, _, _) <- codebase

View File

@ -72,6 +72,34 @@ Vector.fold-balanced plus zero vs = let rec
go plus zero (1st p) `plus` go plus zero (2nd p) go plus zero (1st p) `plus` go plus zero (2nd p)
go plus zero vs go plus zero vs
Optional.map : ∀ a b . (a -> b) -> Optional a -> Optional b
Optional.map f = Optional.fold None (f `and-then` Some)
Optional.bind : ∀ a b . (a -> Optional b) -> Optional a -> Optional b
Optional.bind f a = Optional.fold None f a
Optional.pure : ∀ a . a -> Optional a
Optional.pure = Some
Optional.get-or : ∀ a . a -> Optional a -> a
Optional.get-or a = Optional.fold a identity
Optional.somes : ∀ a . Vector (Optional a) -> Vector a
Optional.somes = Vector.bind (Optional.fold Vector.empty Vector.single)
Optional.map2 : ∀ a b c . (a -> b -> c) -> Optional a -> Optional b -> Optional c
Optional.map2 f a b = do Optional
a := a
b := b
pure (f a b)
Optional.lift-or : ∀ a . (a -> a -> a) -> Optional a -> Optional a -> Optional a
Optional.lift-or f = a1 a2 ->
a1 |> Optional.fold a2 (a1 -> Optional.fold None (a2 -> Some (f a1 a2)) a2)
Optional.fold' : ∀ a b . (Unit -> b) -> (a -> b) -> Optional a -> Unit -> b
Optional.fold' thunk f = Optional.fold thunk (a u -> f a)
Vector.fold-balanced1 : ∀ a . (a -> a -> a) -> Vector a -> Optional a Vector.fold-balanced1 : ∀ a . (a -> a -> a) -> Vector a -> Optional a
Vector.fold-balanced1 f v = Vector.fold-balanced (Optional.lift-or f) None (Vector.map Some v) Vector.fold-balanced1 f v = Vector.fold-balanced (Optional.lift-or f) None (Vector.map Some v)
@ -97,6 +125,12 @@ Vector.last v = Vector.at (Vector.size v - 1) v
Vector.1st : ∀ a . Vector a -> Optional a Vector.1st : ∀ a . Vector a -> Optional a
Vector.1st = Vector.at 0 Vector.1st = Vector.at 0
Vector.drop-right : ∀ a . Number -> Vector a -> Vector a
Vector.drop-right n v = Vector.take (Vector.size v - n) v
Vector.take-right : ∀ a . Number -> Vector a -> Vector a
Vector.take-right n v = Vector.drop (Vector.size v - n) v
Vector.dedup-adjacent : ∀ a . (a -> a -> Boolean) -> Vector a -> Vector a Vector.dedup-adjacent : ∀ a . (a -> a -> Boolean) -> Vector a -> Vector a
Vector.dedup-adjacent eq v = Vector.dedup-adjacent eq v =
Vector.fold-balanced Vector.fold-balanced
@ -107,12 +141,6 @@ Vector.dedup-adjacent eq v =
[] []
(Vector.map Vector.pure v) (Vector.map Vector.pure v)
Vector.drop-right : ∀ a . Number -> Vector a -> Vector a
Vector.drop-right n v = Vector.take (Vector.size v - n) v
Vector.take-right : ∀ a . Number -> Vector a -> Vector a
Vector.take-right n v = Vector.drop (Vector.size v - n) v
Vector.histogram : ∀ a . Order a -> Vector a -> Vector (a, Number) Vector.histogram : ∀ a . Order a -> Vector a -> Vector (a, Number)
Vector.histogram o v = let Vector.histogram o v = let
merge-bin b1 b2 = (1st b1, 2nd b1 + 2nd b2) merge-bin b1 b2 = (1st b1, 2nd b1 + 2nd b2)
@ -151,33 +179,40 @@ Remote.map2' f a b = Remote.map2 f a b |> Remote.join
Remote.join : ∀ a . Remote (Remote a) -> Remote a Remote.join : ∀ a . Remote (Remote a) -> Remote a
Remote.join = Remote.bind identity Remote.join = Remote.bind identity
Remote.replicate : ∀ a . Number -> Remote a -> Remote (Vector a)
Remote.replicate n r = Remote.sequence (Vector.replicate n r)
Remote.replicate! : ∀ a . Number -> Remote a -> Remote Unit
Remote.replicate! n a = let rec
go n =
if n <=_Number 0 then Remote.pure Unit
else Remote.bind (a -> go (n - 1)) a
go n
Remote.unfold : ∀ s a . s -> (s -> Remote (Optional (a, s))) -> Remote (Vector a) Remote.unfold : ∀ s a . s -> (s -> Remote (Optional (a, s))) -> Remote (Vector a)
Remote.unfold s f = let rec Remote.unfold s f = let rec
go s acc = do Remote { go s acc = do Remote
ht := f s; ht := f s
ht |> Optional.fold ht |> Optional.fold
(pure acc) (pure acc)
(ht -> go (2nd ht) (Vector.append (1st ht) acc)) (ht -> go (2nd ht) (Vector.append (1st ht) acc))
}
go s Vector.empty go s Vector.empty
Remote.at' : ∀ a . Node -> Remote a -> Remote a
Remote.at' node r = do Remote { Remote.transfer node; r }
Remote.transfer : Node -> Remote Unit
Remote.transfer node = Remote.at node unit
Remote.replicate : ∀ a . Number -> Remote a -> Remote (Vector a)
Remote.replicate n r = Remote.sequence (Vector.replicate n r)
Remote.start : ∀ a . Duration -> Remote a -> Remote (Remote a)
Remote.start timeout r = do Remote
here := Remote.here
c := Remote.channel
result := Remote.receive-async c timeout
Remote.fork (Remote.at' here (r |> Remote.bind (Remote.send c)))
pure result
Remote.race : ∀ a . Duration -> Vector (Remote a) -> Remote a Remote.race : ∀ a . Duration -> Vector (Remote a) -> Remote a
Remote.race timeout rs = do Remote Remote.race timeout rs = do Remote
here := Remote.here here := Remote.here
c := Remote.channel c := Remote.channel
result := Remote.receive-async c timeout result := Remote.receive-async c timeout
Remote.traverse Remote.traverse
(r -> Remote.fork <| do Remote { a := r Remote.transfer here; Remote.send c a }) (r -> Remote.fork <| (do Remote { a := r; Remote.transfer here; Remote.send c a }))
rs rs
result result
@ -187,16 +222,15 @@ Remote.timeout : ∀ a . Duration -> Remote a -> Remote (Optional a)
Remote.timeout timeout r = Remote.timeout timeout r =
Remote.race (Duration.seconds 501) [ Remote.race (Duration.seconds 501) [
Remote.map Some r, Remote.map Some r,
do Remote Remote.sleep timeout pure None do Remote { Remote.sleep timeout; pure None }
] ]
Remote.start : ∀ a . Duration -> Remote a -> Remote (Remote a) Remote.replicate! : ∀ a . Number -> Remote a -> Remote Unit
Remote.start timeout r = do Remote Remote.replicate! n a = let rec
here := Remote.here go n =
c := Remote.channel if n <=_Number 0 then Remote.pure Unit
result := Remote.receive-async c timeout else Remote.bind (a -> go (n - 1)) a
Remote.fork (Remote.at' here (r |> Remote.bind (Remote.send c))) go n
pure result
Remote.traverse : ∀ a b . (a -> Remote b) -> Vector a -> Remote (Vector b) Remote.traverse : ∀ a b . (a -> Remote b) -> Vector a -> Remote (Vector b)
Remote.traverse f vs = Remote.traverse f vs =
@ -220,35 +254,6 @@ Remote.parallel-traverse timeout f vs = do Remote
Remote.quorum : ∀ a b . Duration -> Number -> (a -> Remote b) -> Vector a -> Remote b Remote.quorum : ∀ a b . Duration -> Number -> (a -> Remote b) -> Vector a -> Remote b
Remote.quorum timeout n = _ -- todo Remote.quorum timeout n = _ -- todo
Optional.map : ∀ a b . (a -> b) -> Optional a -> Optional b
Optional.map f = Optional.fold None (f `and-then` Some)
Optional.bind : ∀ a b . (a -> Optional b) -> Optional a -> Optional b
Optional.bind f = Optional.fold None f
Optional.pure : ∀ a . a -> Optional a
Optional.pure = Some
Optional.get-or : ∀ a . a -> Optional a -> a
Optional.get-or a = Optional.fold a identity
Optional.somes : ∀ a . Vector (Optional a) -> Vector a
Optional.somes = Vector.bind (Optional.fold Vector.empty Vector.single)
Optional.map2 : ∀ a b c . (a -> b -> c) -> Optional a -> Optional b -> Optional c
Optional.map2 f a b = do Optional
a := a
b := b
pure (f a b)
Optional.lift-or : ∀ a . (a -> a -> a) -> Optional a -> Optional a -> Optional a
Optional.lift-or f = a1 a2 ->
a1 |> Optional.fold a2 (a1 -> Optional.fold None (a2 -> Some (f a1 a2)) a2)
Optional.fold' : ∀ a b . (Unit -> b) -> (a -> b) -> Optional a -> Unit -> b
Optional.fold' thunk f = Optional.fold thunk (a u -> f a)
Either.map : ∀ a b c . (b -> c) -> Either a b -> Either a c Either.map : ∀ a b c . (b -> c) -> Either a b -> Either a c
Either.map f = Either.fold Left (f `and-then` Right) Either.map f = Either.fold Left (f `and-then` Right)
@ -270,9 +275,3 @@ Text.take-right n t = Text.drop (Text.length t - n) t
Text.ends-with : Text -> Text -> Boolean Text.ends-with : Text -> Text -> Boolean
Text.ends-with suffix overall = Text.ends-with suffix overall =
Text.take-right (Text.length suffix) overall ==_Text suffix Text.take-right (Text.length suffix) overall ==_Text suffix
Remote.at' : ∀ a . Node -> Remote a -> Remote a
Remote.at' node r = do Remote { Remote.transfer node; r }
Remote.transfer : Node -> Remote Unit
Remote.transfer node = Remote.at node unit