unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-09-11 02:25:39 +03:00
Code Issues Projects Releases Wiki Activity

get rid of hacky layout support, tweak syntax, build up standard library

Browse Source
This commit is contained in:
Paul Chiusano 2016-08-22 15:27:13 -04:00
parent d95b9ce286
commit 1d4e3210d5
15 changed files with 173 additions and 174 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
node/tests/Unison/Test/SerializationAndHashing.hs
View File

@ -26,10 +26,10 @@ lambda :: Assertion
lambda = testTermString "x -> x"
letBinding :: Assertion
letBinding = testTermString "let x = 42; x + 1"
letBinding = testTermString "let x = 42; x + 1;;"
letRec :: Assertion
letRec = testTermString "let rec x = x + 1; x"
letRec = testTermString "let rec x = x + 1; x;;"
vec :: Assertion
vec = testTermString "[\"a\", \"b\", \"c\"]"
@ -43,5 +43,4 @@ tests = testGroup "SerializationAndHashing"
, testCase "letBinding" letBinding
, testCase "letRec" letRec
, testCase "vec" vec
]

1
shared/src/Unison/Node.hs
View File

@ -6,7 +6,6 @@ module Unison.Node where
-- import Data.Bytes.Serial (Serial)
import Control.Monad
import Control.Applicative
import Data.Foldable
import Data.Aeson.TH
import Data.List
import Data.Map (Map)

29
shared/src/Unison/Node/Builtin.hs
View File

@ -40,6 +40,8 @@ true = Term.builtin "True"
false = Term.builtin "False"
pair :: Ord v => Term v
pair = Term.builtin "Pair"
pair' :: Ord v => Term v -> Term v -> Term v
pair' t1 t2 = pair `Term.app` t1 `Term.app` (pair `Term.app` t2 `Term.app` unitRef)
makeBuiltins :: WHNFEval -> [Builtin]
makeBuiltins whnf =
@ -200,8 +202,10 @@ makeBuiltins whnf =
in (r, Nothing, unsafeParseType "forall a b . a -> b -> Pair a b", prefix "Pair")
, let r = R.Builtin "Pair.fold"
op [f,p] = do
Term.Apps' (Term.Builtin' "Pair") [a,b] <- whnf p
whnf (f `Term.apps` [a,b])
p <- whnf p
case p of
Term.Apps' (Term.Builtin' "Pair") [a,b] -> whnf (f `Term.apps` [a,b])
p -> fail $ "expected pair, got: " ++ show p
op _ = error "Pair.fold unpossible"
in (r, Just (I.Primop 2 op), unsafeParseType "forall a b c . (a -> b -> c) -> Pair a b -> c", prefix "fold")
@ -261,15 +265,28 @@ makeBuiltins whnf =
pure $ if Vector.null vs then true else false
op _ = fail "Vector.empty? unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "forall a. Vector a -> Boolean", prefix "empty?")
, let r = R.Builtin "Vector.size"
op [v] = do
Term.Vector' vs <- whnf v
pure $ Term.num (fromIntegral $ Vector.length vs)
op _ = fail "Vector.size unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "forall a. Vector a -> Number", prefix "Vector.size")
, let r = R.Builtin "Vector.reverse"
op [v] = do
Term.Vector' vs <- whnf v
pure $ Term.vector' (Vector.reverse vs)
op _ = fail "Vector.reverse unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "forall a. Vector a -> Vector a", prefix "Vector.reverse")
, let r = R.Builtin "Vector.split"
op [v] = do
Term.Vector' vs <- whnf v
pure $ case Vector.null vs of
True -> pair `Term.apps` [Term.vector [], Term.vector []]
True -> pair' (Term.vector []) (Term.vector [])
False -> case Vector.splitAt (Vector.length vs `div` 2) vs of
(x,y) -> pair `Term.app` (Term.vector' x) `Term.app` (Term.vector' y)
(x,y) -> pair' (Term.vector' x) (Term.vector' y)
op _ = fail "Vector.split unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "forall a. Vector a -> Boolean", prefix "empty?")
typ = "forall a. Vector a -> (Vector a, Vector a)"
in (r, Just (I.Primop 1 op), unsafeParseType typ, prefix "Vector.split")
, let r = R.Builtin "Vector.fold-left"
op [f,z,vec] = whnf vec >>= \vec -> case vec of
Term.Vector' vs -> Vector.foldM (\acc a -> whnf (f `Term.apps` [acc, a])) z vs
@ -295,7 +312,7 @@ makeBuiltins whnf =
, let r = R.Builtin "Vector.single"
op [hd] = pure $ Term.vector (pure hd)
op _ = fail "Vector.single unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "forall a. a -> Vector a", prefix "single")
in (r, Just (I.Primop 1 op), unsafeParseType "forall a. a -> Vector a", prefix "Vector.single")
]
-- type helpers

55
shared/src/Unison/Parser.hs
View File

@ -23,6 +23,9 @@ root p = ignored *> (p <* (optional semicolon <* eof))
semicolon :: Parser ()
semicolon = void $ token (char ';')
semicolon2 :: Parser ()
semicolon2 = semicolon *> semicolon
eof :: Parser ()
eof = Parser $ \(s,_) -> case s of
[] -> Succeed () 0 False
@ -35,7 +38,7 @@ attempt p = Parser $ \s -> case run' p s of
run :: Parser a -> String -> Result a
-- run p s = run' p (watch "layoutized" $ layoutize s, False)
run p s = run' p (layoutize s, False)
run p s = run' p (s, False)
where watch msg a = trace (msg ++ ":\n" ++ a) a
unsafeRun :: Parser a -> String -> a
@ -107,8 +110,8 @@ lineErrorUnless s p = commitFail $ Parser $ \input -> case run' p input of
parenthesized :: Parser a -> Parser a
parenthesized p = lp *> body <* rp
where
lp = char '(' *> withoutLayout ignored
body = withoutLayout p
lp = token (char '(')
body = p
rp = lineErrorUnless "missing )" $ token (char ')')
takeWhile :: String -> (Char -> Bool) -> Parser String
@ -163,52 +166,8 @@ sepBy sep pb = f <$> optional (sepBy1 sep pb)
sepBy1 :: Parser a -> Parser b -> Parser [b]
sepBy1 sep pb = (:) <$> pb <*> many (sep *> pb)
inLayout :: Parser Bool
inLayout = Parser $ \(_,inLayout) -> Succeed inLayout 0 False
layoutChar :: Parser ()
layoutChar = void $ one (\c -> c == ';' || c == '{' || c == '}')
ignored :: Parser ()
ignored = void $ do
inLayout <- inLayout
case inLayout of
True -> many (whitespace1 <|> haskellLineComment)
False -> many (whitespace1 <|> haskellLineComment <|> layoutChar)
withLayout :: Parser a -> Parser a
withLayout p = Parser $ \(s,_) -> run' p (s,True)
withoutLayout :: Parser a -> Parser a
withoutLayout p = Parser $ \(s,_) -> run' p (s,False)
layout :: Parser a -> Parser a
layout p = withLayout $ token (char '{') *> p <* token (char '}')
layoutize :: String -> String
layoutize s = tweak $ go s [] where
close s = '}' : s
onlysemis line = all (\c -> Char.isSpace c || c == ';') line
tweak [] = []
tweak s = case span (/= '\n') s of
([],[]) -> []
([],nl:s) -> nl : tweak s
(line,rem) ->
if onlysemis line then (filter (/= ';') line) ++ tweak rem
else line ++ tweak rem
go s stack = case s of
'\n' : tl -> handle tl stack where
indent = length $ Prelude.takeWhile (\c -> c == ' ' || c == '\t') tl
handle :: String -> [Int] -> String
handle tl [] | indent == 0 = ';' : '\n' : go tl stack
| otherwise = '\n' : '{' : go tl (indent : stack)
handle tl stack@(level:levels) =
if indent == level then ';' : '\n' : go tl stack
else if indent > level then '{' : '\n' : go tl (indent:stack)
else close $ go ('\n' : tl) levels
'\r' : tl -> go tl stack
hd : tl -> hd : go tl stack
[] -> replicate (length stack) '}'
ignored = void $ many (whitespace1 <|> haskellLineComment)
toEither :: Result a -> Either String a
toEither (Fail e _) = Left (intercalate "\n" e)

2
shared/src/Unison/Parsers.hs
View File

@ -87,7 +87,7 @@ termBuiltins = (Var.named *** Term.ref) <$> (
, Builtin "Pair.fold"
, Builtin "Pair"
, AliasFromModule "Vector"
["single", "prepend", "map", "fold-left", "concatenate", "append"] ["empty"]
["single", "prepend", "map", "fold-left", "concatenate", "append", "empty"] []
, AliasFromModule "Text"
["concatenate", "left", "right", "center", "justify"] []
, AliasFromModule "Remote"

33
shared/src/Unison/TermParser.hs
View File

@ -1,4 +1,5 @@
{-# Language OverloadedStrings #-}
{-# Language ScopedTypeVariables #-}
module Unison.TermParser where
@ -74,21 +75,26 @@ tupleOrParenthesized rec =
-- x := pure 23
-- y = 11
-- pure (f x)
effectBlock :: Var v => Parser (Term v)
effectBlock = (token (string "do") *> withLayout wordyId) >>= go where
go name = layout $ do
bindings <- sepBy1 semicolon $ asum [Right <$> binding, Left <$> action]
effectBlock :: forall v . Var v => Parser (Term v)
effectBlock = (token (string "do") *> wordyId) >>= go where
go name = do
bindings <- some $ asum [Right <$> binding, Left <$> action] <* semicolon
semicolon
Just result <- pure $ foldr bind Nothing bindings
pure result
where
qualifiedPure, qualifiedBind :: Term v
qualifiedPure = ABT.var' (Text.pack name `mappend` Text.pack ".pure")
qualifiedBind = ABT.var' (Text.pack name `mappend` Text.pack ".bind")
bind :: (Either (Term v) (v, Term v)) -> Maybe (Term v) -> Maybe (Term v)
bind = go where
go (Right (lhs,rhs)) (Just acc) = Just $ qualifiedBind `Term.apps` [Term.lam lhs acc, rhs]
go (Right (_,_)) Nothing = Nothing
go (Left action) (Just acc) = Just $ qualifiedBind `Term.apps` [Term.lam (ABT.v' "_") acc, action]
go (Left action) _ = Just action
interpretPure :: Term v -> Term v
interpretPure = ABT.subst (ABT.v' "pure") qualifiedPure
binding :: Parser (v, Term v)
binding = scope "binding" $ do
lhs <- ABT.v' . Text.pack <$> token wordyId
eff <- token $ (True <$ string ":=") <|> (False <$ string "=")
@ -96,7 +102,8 @@ effectBlock = (token (string "do") *> withLayout wordyId) >>= go where
let rhs' = if eff then interpretPure rhs
else qualifiedPure `Term.app` rhs
pure (lhs, rhs')
action = attempt . scope "action" $ (interpretPure <$> term)
action :: Parser (Term v)
action = scope "action" $ (interpretPure <$> term)
text' :: Parser Literal
text' =
@ -148,18 +155,18 @@ possiblyAnnotated p = f <$> p <*> optional ann''
f t Nothing = t
ann'' :: Var v => Parser (Type v)
ann'' = withoutLayout $ token (char ':') *> TypeParser.type_
ann'' = token (char ':') *> TypeParser.type_
--let server = _; blah = _ in _
let_ :: Var v => Parser (Term v) -> Parser (Term v)
let_ p = f <$> withLayout (let_ *> optional rec_) <*> (layout bindings' <|> bindings')
let_ p = f <$> (let_ *> optional rec_) <*> bindings'
where
let_ = token (string "let")
rec_ = token (string "rec") $> ()
bindings' = withLayout $ do
bindings' = do
bs <- lineErrorUnless "error parsing let bindings" (bindings p)
semicolon
body <- lineErrorUnless "parse error in body of let-expression" p
body <- lineErrorUnless "parse error in body of let-expression" term
semicolon2
pure (bs, body)
f :: Ord v => Maybe () -> ([(v, Term v)], Term v) -> Term v
f Nothing (bindings, body) = Term.let1 bindings body
@ -169,7 +176,7 @@ typedecl :: Var v => Parser (v, Type v)
typedecl = (,) <$> prefixVar <*> ann''
bindingEqBody :: Parser (Term v) -> Parser (Term v)
bindingEqBody p = eq *> (layout body <|> body)
bindingEqBody p = eq *> body
where
eq = token (char '=')
body = lineErrorUnless "parse error in body of binding" p
@ -219,12 +226,12 @@ prefixApp p = f <$> some p
f [] = error "'some' shouldn't produce an empty list"
bindings :: Var v => Parser (Term v) -> Parser [(v, Term v)]
bindings p = withLayout (sepBy1 semicolon binding) where
bindings p = some (binding <* semicolon) where
binding = do
typ <- optional (typedecl <* semicolon)
(name, args) <- ((\arg1 op arg2 -> (op,[arg1,arg2])) <$> prefixVar <*> infixVar <*> prefixVar)
<|> ((,) <$> prefixVar <*> many prefixVar)
body <- bindingEqBody p
body <- bindingEqBody term
case typ of
Nothing -> pure $ mkBinding name args body
Just (nameT, typ)

9
shared/src/Unison/TypeParser.hs
View File

@ -8,7 +8,7 @@ import Data.Char (isUpper, isLower, isAlpha)
import Data.Foldable (asum)
import Data.Functor
import Data.List (foldl1')
import Unison.Parser hiding (ignored, token)
import Unison.Parser
import Unison.Type (Type)
import Unison.Var (Var)
import qualified Data.Text as Text
@ -17,13 +17,6 @@ import qualified Unison.Type as Type
type_ :: Var v => Parser (Type v)
type_ = forall type1 <|> type1
-- we ignore indentation markers { and }, but not semicolon
ignored :: Parser ()
ignored = void $ many (whitespace1 <|> haskellLineComment <|> (void $ one (\c -> c == '{' || c == '}')))
token :: Parser a -> Parser a
token p = (p <* ignored)
typeLeaf :: Var v => Parser (Type v)
typeLeaf =
asum [ literal

19
shared/tests/Unison/Test/Interpreter.hs
View File

@ -14,7 +14,7 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
[ t "1 + 1" "2"
, t "1 + 1 + 1" "3"
, 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 0 1" "1"
, t "if True 12 13" "12"
, t "1 > 0" "True"
@ -23,12 +23,12 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
, t "1 < 2" "True"
, t "1 <= 1" "True"
, t "1 >= 1" "True"
, t "let rec fac n = if (n == 0) 1 (n * fac (n - 1)); fac 5" "120"
, t "let rec ping n = if (n >= 10) n (pong (n + 1)); pong n = ping (n + 1); ping 0"
, t "let rec fac n = if (n == 0) 1 (n * fac (n - 1)); fac 5;;" "120"
, t "let rec ping n = if (n >= 10) n (pong (n + 1)); pong n = ping (n + 1); ping 0;;"
"10"
, t "let 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; 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 "Optional.map ((+) 1) (Some 1)" "Optional.Some (1 + 1)"
, t "Either.fold ((+) 1) ((+) 2) (Either.Left 1)" "2"
, t "Either.fold ((+) 1) ((+) 2) (Either.Right 1)" "3"
@ -37,6 +37,13 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
, t "const 41 0" "41"
, t "1st (1,2,3,4)" "1"
, t "2nd (1,2 + 1,3,4)" "3"
, 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 uneval eval = testCase (uneval ++ " ⟹ " ++ eval) $ do
(node, _, builtins) <- node

8
shared/tests/Unison/Test/Term.hs
View File

@ -112,11 +112,11 @@ pingpong1 :: TTerm
pingpong1 =
unsafeParseTerm $
unlines [ "let rec "
, " ping x = pong (x + 1)"
, " pong y = ping (y - 1)"
, " ping 1"
, " 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"
unsafeParseTerm $ "let rec pong1 p = ping1 (p - 1); ping1 q = pong1 (q + 1); ping1 1;;"

40
shared/tests/Unison/Test/TermParser.hs
View File

@ -63,51 +63,51 @@ tests = testGroup "TermParser" $ (parse <$> shouldPass) ++ (parseFail <$> should
, ("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 a : Int; a = 1; a + 1", let_a_int1_in_aplus1)
, ("let a: Int; a = 1; a + 1", let_a_int1_in_aplus1)
, ("let a :Int; a = 1; a + 1", let_a_int1_in_aplus1)
, ("let a:Int; a = 1; a + 1", let_a_int1_in_aplus1)
, ("let a = 1; a + 1;;", let1' [("a", one)] (apps numberplus [a, one]))
, ("let a : Int; a = 1; a + 1;;", let_a_int1_in_aplus1)
, ("let a: Int; a = 1; a + 1;;", let_a_int1_in_aplus1)
, ("let a :Int; a = 1; a + 1;;", let_a_int1_in_aplus1)
, ("let a:Int; a = 1; 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 (+) : 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 = 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 (+) : 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]]))
-- 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 fix f = f (fix f); fix", fix) -- fix
, ("let rec fix = f -> f (fix f); fix;;", fix) -- fix
, ("let rec fix f = f (fix f); fix;;", fix) -- fix
, ("1 + 2 + 3", num 1 `plus'` num 2 `plus'` num 3)
, ("[1, 2, 1 + 1]", vector [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'
, ("(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))
, ("#" ++ Text.unpack sampleHash64, derived' sampleHash64)
, ("#" ++ Text.unpack sampleHash512, derived' sampleHash512)
, ("(do Remote { pure 42 })", builtin "Remote.pure" `app` num 42)
, ("do Remote { x = 42; pure (x + 1) }",
, ("(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) }",
, ("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)",
, ("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")),

24
shared/tests/Unison/Test/Typechecker.hs
View File

@ -119,14 +119,14 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typecheck
, testCase "synthesize/check (x y -> y)" $ synthesizesAndChecks node
(unsafeParseTerm "x y -> y")
(unsafeParseType "forall a b. a -> b -> b")
, testCase "synthesize/check (let f = (+); f 1)" $ synthesizesAndChecks node
(unsafeParseTerm "let f = (+); f 1")
, testCase "synthesize/check (let f = (+); f 1;;)" $ synthesizesAndChecks node
(unsafeParseTerm "let f = (+); f 1;;")
(T.lit T.Number --> T.lit T.Number)
, testCase "synthesize/check (let blank x = _; blank 1)" $ synthesizesAndChecks node
(unsafeParseTerm "let blank x = _; blank 1")
, testCase "synthesize/check (let blank x = _; blank 1;;)" $ synthesizesAndChecks node
(unsafeParseTerm "let blank x = _; blank 1;;")
(forall' ["a"] $ T.v' "a")
, 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")
, testCase "synthesize/check Term.pingpong1" $ synthesizesAndChecks node
Term.pingpong1
@ -137,15 +137,15 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typecheck
, testTerm "[1, 2, 1 + 1]" $ \tms ->
testCase ("synthesize/checkAt "++tms++"@[Index 2]") $ synthesizesAndChecksAt node
[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
[Paths.Binding 0, Paths.Body] (unsafeParseTerm tms) unconstrained
-- 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
(unsafeParseTerm tms)
(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
(unsafeParseTerm tms) (unsafeParseType "forall x. x -> Number")
, testTerm "f x y -> (x y -> y) f _ + _" $ \tms ->
@ -153,7 +153,7 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typecheck
synthesizesAndChecks node
(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 ->
, 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"
@ -174,19 +174,19 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typecheck
[(_,xt), (_,yt)] <- localsAt node [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 ->
, testTerm "let x = _; _;;" $ \tms ->
testCase ("locals ("++tms++")") $ do
let tm = unsafeParseTerm tms
[(_,xt)] <- localsAt node [Paths.Body] tm
[] <- localsAt node [Paths.Binding 0, Paths.Body] tm
assertEqual "xt unconstrainted" unconstrained (T.generalize xt)
, testTerm "let x = _; y = _; _" $ \tms ->
, testTerm "let x = _; y = _; _;;" $ \tms ->
testCase ("locals ("++tms++")@[Body,Body]") $ do
let tm = unsafeParseTerm tms
[(_,xt), (_,yt)] <- localsAt node [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 = _; y = _; _;;" $ \tms ->
-- testTerm "let x = 42; y = _; _" $ \tms ->
-- testTerm "let x = 42; y = 43; _" $ \tms ->
-- testTerm "let x = 42; y = 43; 4224" $ \tms ->

20
shared/tests/Unison/Test/Typechecker/Components.hs
View File

@ -15,21 +15,21 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
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"
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"
, 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"
, 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"
, 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 "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
(node, _, _) <- node

88
unison-src/base.u
View File

@ -1,48 +1,68 @@
identity : ∀ a . a -> a
identity a = a
identity : ∀ a . a -> a;
identity a = a;
then : ∀ a b c . (a -> b) -> (b -> c) -> a -> c
then f1 f2 x = f2 (f1 x)
then : ∀ a b c . (a -> b) -> (b -> c) -> a -> c;
then f1 f2 x = f2 (f1 x);
Remote.transfer : Node -> Remote Unit
Remote.transfer node = Remote.at node unit
flip : ∀ a b c . (a -> b -> c) -> b -> a -> c;
flip f b a = f a b;
Remote.map :
∀ a b . (a -> b) -> Remote a -> Remote b
Remote.map f =
Remote.bind (f `then` Remote.pure)
Remote.transfer : Node -> Remote Unit;
Remote.transfer node = Remote.at node unit;
Optional.map : ∀ a b . (a -> b) -> Optional a -> Optional b
Optional.map f = Optional.fold None (f `then` Some)
Remote.map : ∀ a b . (a -> b) -> Remote a -> Remote b;
Remote.map f = Remote.bind (f `then` Remote.pure);
Optional.bind : ∀ a b . (a -> Optional b) -> Optional a -> Optional b
Optional.bind f = Optional.fold None f
Remote =
( Remote.pure : ∀ a . a -> Remote a
, Remote.bind : ∀ a b . (a -> Remote b) -> Remote a -> Remote b);
Optional.pure : ∀ a . a -> Optional a
Optional.pure = Some
Vector.fold-right : ∀ a b . (a -> b -> b) -> b -> Vector a -> b;
Vector.fold-right f z vs = Vector.fold-left (flip f) z (Vector.reverse vs);
Either.map : ∀ a b c . (b -> c) -> Either a b -> Either a c
Either.map f = Either.fold Left (f `then` Right)
-- todo: figure out why typechecker bombs when try to annotate this
-- Vector.fold-balanced : ∀ a . a -> (a -> a -> a) -> Vector a -> a;
Vector.fold-balanced zero plus vs =
let rec
go zero plus vs =
if (Vector.size vs <= 2)
(Vector.fold-left zero plus vs)
(let p = Vector.split vs;
go zero plus (1st p) `Vector.concatenate` go zero plus (2nd p);;);
go zero plus vs;;
;
Either.pure : ∀ a b . b -> Either a b
Either.pure = Right
Optional.map : ∀ a b . (a -> b) -> Optional a -> Optional b;
Optional.map f = Optional.fold None (f `then` Some);
Either.bind : ∀ a b c . (b -> Either a c) -> Either a b -> Either a c
Either.bind = Either.fold Left
Optional.bind : ∀ a b . (a -> Optional b) -> Optional a -> Optional b;
Optional.bind f = Optional.fold None f;
Either.swap : ∀ a b . Either a b -> Either b a
Either.swap e = Either.fold Right Left e
Optional.pure : ∀ a . a -> Optional a;
Optional.pure = Some;
const x y = x
Either.map : ∀ a b c . (b -> c) -> Either a b -> Either a c;
Either.map f = Either.fold Left (f `then` Right);
first : ∀ a b . Pair a b -> a
first p = Pair.fold const p
Either.pure : ∀ a b . b -> Either a b;
Either.pure = Right;
rest : ∀ a b . Pair a b -> b
rest p = Pair.fold (x y -> y) p
Either.bind : ∀ a b c . (b -> Either a c) -> Either a b -> Either a c;
Either.bind = Either.fold Left;
1st = first
2nd = rest `then` first
3rd = rest `then` (rest `then` first)
4th = rest `then` (rest `then` (rest `then` first))
5th = rest `then` (rest `then` (rest `then` (rest `then` first)))
Either.swap : ∀ a b . Either a b -> Either b a;
Either.swap e = Either.fold Right Left e;
const x y = x;
first : ∀ a b . Pair a b -> a;
first p = Pair.fold const p;
rest : ∀ a b . Pair a b -> b;
rest p = Pair.fold (x y -> y) p;
1st = first;
2nd = rest `then` first;
3rd = rest `then` (rest `then` first);
4th = rest `then` (rest `then` (rest `then` first));
5th = rest `then` (rest `then` (rest `then` (rest `then` first)));

4
unison-src/extra.u
View File

@ -1,4 +1,4 @@
Index.empty : ∀ k v . Remote (Index k v)
Index.empty : ∀ k v . Remote (Index k v);
Index.empty =
Remote.map Index.unsafeEmpty Remote.here
Remote.map Index.unsafeEmpty Remote.here;

10
unison-src/index.u
View File

@ -1,15 +1,13 @@
-- run from unison root directory
-- curl -H "Content-Type: text/plain; charset=UTF-8" --data-binary @node/tests/index.u http://localhost:8081/compute/dummynode909
Remote {
do Remote
n1 := Remote.spawn;
n2 := Remote.spawn;
ind := Remote {
ind := do Remote
Remote.transfer n1;
ind := Index.empty;
Index.insert "Unison" "Rulez!!!1" ind;
pure ind;
};
pure ind;;
Remote.transfer n2;
Index.lookup "Unison" ind;
}
Index.lookup "Unison" ind;;