mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
added layout blocks, using for do blocks and let bindings, altered syntax of let bindings to closer match do blocks
This commit is contained in:
parent
6e198724d6
commit
78c3cddef0
@ -26,10 +26,10 @@ lambda :: Assertion
|
||||
lambda = testTermString "x -> x"
|
||||
|
||||
letBinding :: Assertion
|
||||
letBinding = testTermString "let x = 42 in x + 1"
|
||||
letBinding = testTermString "let x = 42; x + 1"
|
||||
|
||||
letRec :: Assertion
|
||||
letRec = testTermString "let rec x = x + 1 in x"
|
||||
letRec = testTermString "let rec x = x + 1; x"
|
||||
|
||||
vec :: Assertion
|
||||
vec = testTermString "[\"a\", \"b\", \"c\"]"
|
||||
|
@ -12,22 +12,32 @@ import Data.Maybe
|
||||
import Prelude hiding (takeWhile)
|
||||
import qualified Data.Char as Char
|
||||
import qualified Prelude
|
||||
import Debug.Trace
|
||||
|
||||
newtype Parser a = Parser { run :: String -> Result a }
|
||||
type InLayout = Bool
|
||||
newtype Parser a = Parser { run' :: (String,InLayout) -> Result a }
|
||||
|
||||
root :: Parser a -> Parser a
|
||||
root p = many (whitespace1 <|> haskellLineComment) *> (p <* eof)
|
||||
root p = ignored *> (p <* (optional semicolon <* eof))
|
||||
|
||||
semicolon :: Parser ()
|
||||
semicolon = void $ token (char ';')
|
||||
|
||||
eof :: Parser ()
|
||||
eof = Parser $ \s -> case s of
|
||||
eof = Parser $ \(s,_) -> case s of
|
||||
[] -> Succeed () 0 False
|
||||
_ -> Fail [Prelude.takeWhile (/= '\n') s, "expected eof, got"] False
|
||||
|
||||
attempt :: Parser a -> Parser a
|
||||
attempt p = Parser $ \s -> case run p s of
|
||||
attempt p = Parser $ \s -> case run' p s of
|
||||
Fail stack _ -> Fail stack False
|
||||
Succeed a n _ -> Succeed a n False
|
||||
|
||||
run :: Parser a -> String -> Result a
|
||||
-- run p s = run' p (watch "layoutized" $ layoutize s, False)
|
||||
run p s = run' p (layoutize s, False)
|
||||
where watch msg a = trace (msg ++ ":\n" ++ a) a
|
||||
|
||||
unsafeRun :: Parser a -> String -> a
|
||||
unsafeRun p s = case toEither $ run p s of
|
||||
Right a -> a
|
||||
@ -39,7 +49,7 @@ unsafeGetSucceed r = case r of
|
||||
Fail e _ -> error (unlines ("Parse error:":e))
|
||||
|
||||
string :: String -> Parser String
|
||||
string s = Parser $ \input ->
|
||||
string s = Parser $ \(input,_) ->
|
||||
if s `isPrefixOf` input then Succeed s (length s) False
|
||||
else Fail ["expected '" ++ s ++ "', got " ++ takeLine input] False
|
||||
|
||||
@ -47,12 +57,12 @@ takeLine :: String -> String
|
||||
takeLine = Prelude.takeWhile (/= '\n')
|
||||
|
||||
char :: Char -> Parser Char
|
||||
char c = Parser $ \input ->
|
||||
char c = Parser $ \(input,_) ->
|
||||
if listToMaybe input == Just c then Succeed c 1 False
|
||||
else Fail [] False
|
||||
else Fail ["expected " ++ show c ++ " near " ++ takeLine input] False
|
||||
|
||||
one :: (Char -> Bool) -> Parser Char
|
||||
one f = Parser $ \s -> case s of
|
||||
one f = Parser $ \(s,_) -> case s of
|
||||
(h:_) | f h -> Succeed h 1 False
|
||||
_ -> Fail [] False
|
||||
|
||||
@ -83,31 +93,31 @@ identifier' charTests stringTests = do
|
||||
pure i
|
||||
|
||||
token :: Parser a -> Parser a
|
||||
token p = p <* many (whitespace1 <|> haskellLineComment)
|
||||
token p = p <* ignored
|
||||
|
||||
haskellLineComment :: Parser ()
|
||||
haskellLineComment = void $ string "--" *> takeWhile "-- comment" (/= '\n')
|
||||
|
||||
lineErrorUnless :: String -> Parser a -> Parser a
|
||||
lineErrorUnless s p = commitFail $ Parser $ \input -> case run p input of
|
||||
lineErrorUnless s p = commitFail $ Parser $ \input -> case run' p input of
|
||||
Fail e b -> Fail (s:m:e) b
|
||||
where m = "near \'" ++ Prelude.takeWhile (/= '\n') input ++ "\'"
|
||||
where m = "near \'" ++ Prelude.takeWhile (/= '\n') (fst input) ++ "\'"
|
||||
ok -> ok
|
||||
|
||||
parenthesized :: Parser a -> Parser a
|
||||
parenthesized p = lp *> body <* rp
|
||||
where
|
||||
lp = token (char '(')
|
||||
body = p
|
||||
lp = char '(' *> withoutLayout ignored
|
||||
body = withoutLayout p
|
||||
rp = lineErrorUnless "missing )" $ token (char ')')
|
||||
|
||||
takeWhile :: String -> (Char -> Bool) -> Parser String
|
||||
takeWhile msg f = scope msg . Parser $ \s ->
|
||||
takeWhile msg f = scope msg . Parser $ \(s,_) ->
|
||||
let hd = Prelude.takeWhile f s
|
||||
in Succeed hd (length hd) False
|
||||
|
||||
takeWhile1 :: String -> (Char -> Bool) -> Parser String
|
||||
takeWhile1 msg f = scope msg . Parser $ \s ->
|
||||
takeWhile1 msg f = scope msg . Parser $ \(s,_) ->
|
||||
let hd = Prelude.takeWhile f s
|
||||
in if null hd then Fail ["takeWhile1 empty: " ++ take 20 s] False
|
||||
else Succeed hd (length hd) False
|
||||
@ -119,22 +129,22 @@ whitespace1 :: Parser ()
|
||||
whitespace1 = void $ takeWhile1 "whitespace1" Char.isSpace
|
||||
|
||||
nonempty :: Parser a -> Parser a
|
||||
nonempty p = Parser $ \s -> case run p s of
|
||||
nonempty p = Parser $ \s -> case run' p s of
|
||||
Succeed _ 0 b -> Fail [] b
|
||||
ok -> ok
|
||||
|
||||
scope :: String -> Parser a -> Parser a
|
||||
scope s p = Parser $ \input -> case run p input of
|
||||
scope s p = Parser $ \input -> case run' p input of
|
||||
Fail e b -> Fail (s:e) b
|
||||
ok -> ok
|
||||
|
||||
commitSuccess :: Parser a -> Parser a
|
||||
commitSuccess p = Parser $ \input -> case run p input of
|
||||
commitSuccess p = Parser $ \input -> case run' p input of
|
||||
Fail e b -> Fail e b
|
||||
Succeed a n _ -> Succeed a n True
|
||||
|
||||
commitFail :: Parser a -> Parser a
|
||||
commitFail p = Parser $ \input -> case run p input of
|
||||
commitFail p = Parser $ \input -> case run' p input of
|
||||
Fail e _ -> Fail e True
|
||||
Succeed a n b -> Succeed a n b
|
||||
|
||||
@ -153,6 +163,53 @@ 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) '}'
|
||||
|
||||
toEither :: Result a -> Either String a
|
||||
toEither (Fail e _) = Left (intercalate "\n" e)
|
||||
toEither (Succeed a _ _) = Right a
|
||||
@ -176,13 +233,13 @@ instance Alternative Parser where
|
||||
instance Monad Parser where
|
||||
return a = Parser $ \_ -> Succeed a 0 False
|
||||
Parser p >>= f = Parser $ \s -> case p s of
|
||||
Succeed a n committed -> case run (f a) (drop n s) of
|
||||
Succeed a n committed -> case run' (f a) (drop n (fst s), snd s) of
|
||||
Succeed b m c2 -> Succeed b (n+m) (committed || c2)
|
||||
Fail e b -> Fail e (committed || b)
|
||||
Fail e b -> Fail e b
|
||||
|
||||
instance MonadPlus Parser where
|
||||
mzero = Parser $ \_ -> Fail [] False
|
||||
mplus p1 p2 = Parser $ \s -> case run p1 s of
|
||||
Fail _ False -> run p2 s
|
||||
mplus p1 p2 = Parser $ \s -> case run' p1 s of
|
||||
Fail _ False -> run' p2 s
|
||||
ok -> ok
|
||||
|
@ -7,7 +7,7 @@ import Prelude hiding (takeWhile)
|
||||
import Control.Applicative
|
||||
import Data.Char (isDigit, isAlphaNum, isSpace, isSymbol, isPunctuation)
|
||||
import Data.Foldable (asum)
|
||||
import Data.Functor (($>), void)
|
||||
import Data.Functor
|
||||
import Data.List (foldl')
|
||||
import Data.Set (Set)
|
||||
import Unison.Parser
|
||||
@ -67,32 +67,36 @@ tupleOrParenthesized rec =
|
||||
unit = Term.builtin "()"
|
||||
|
||||
-- |
|
||||
-- Remote { x := pure 23; y := at node2 23; pure 19 }
|
||||
-- Remote { action1; action2; }
|
||||
-- Remote { action1; x = 1 + 1; action2; }
|
||||
-- do Remote { x := pure 23; y := at node2 23; pure 19 }
|
||||
-- do Remote { action1; action2; }
|
||||
-- do Remote { action1; x = 1 + 1; action2; }
|
||||
-- do Remote
|
||||
-- x := pure 23
|
||||
-- y = 11
|
||||
-- pure (f x)
|
||||
effectBlock :: Var v => Parser (Term v)
|
||||
effectBlock = do
|
||||
name <- wordyId <* token (string "{")
|
||||
let qualifiedPure = ABT.var' (Text.pack name `mappend` Text.pack ".pure")
|
||||
qualifiedBind = ABT.var' (Text.pack name `mappend` Text.pack ".bind")
|
||||
bindings <- some $ asum [Right <$> binding qualifiedPure, Left <$> action qualifiedPure]
|
||||
Just result <- pure $ foldr (bind qualifiedBind) Nothing bindings
|
||||
result <$ lineErrorUnless "missing }" (token (string "}"))
|
||||
where
|
||||
bind qb = go where
|
||||
go (Right (lhs,rhs)) (Just acc) = Just $ qb `Term.apps` [Term.lam lhs acc, rhs]
|
||||
go (Right (_,_)) Nothing = Nothing
|
||||
go (Left action) (Just acc) = Just $ qb `Term.apps` [Term.lam (ABT.v' "_") acc, action]
|
||||
go (Left action) _ = Just action
|
||||
interpretPure qp = ABT.subst (ABT.v' "pure") qp
|
||||
binding qp = scope "binding" $ do
|
||||
lhs <- ABT.v' . Text.pack <$> token wordyId
|
||||
eff <- token $ (True <$ string ":=") <|> (False <$ string "=")
|
||||
rhs <- term <* token (string ";")
|
||||
let rhs' = if eff then interpretPure qp rhs
|
||||
else qp `Term.app` rhs
|
||||
pure (lhs, rhs')
|
||||
action qp = attempt . scope "action" $ (interpretPure qp <$> term) <* token (string ";")
|
||||
effectBlock = (token (string "do") *> withLayout wordyId) >>= go where
|
||||
go name = layout $ do
|
||||
bindings <- sepBy1 semicolon $ asum [Right <$> binding, Left <$> action]
|
||||
Just result <- pure $ foldr bind Nothing bindings
|
||||
pure result
|
||||
where
|
||||
qualifiedPure = ABT.var' (Text.pack name `mappend` Text.pack ".pure")
|
||||
qualifiedBind = ABT.var' (Text.pack name `mappend` Text.pack ".bind")
|
||||
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 = ABT.subst (ABT.v' "pure") qualifiedPure
|
||||
binding = scope "binding" $ do
|
||||
lhs <- ABT.v' . Text.pack <$> token wordyId
|
||||
eff <- token $ (True <$ string ":=") <|> (False <$ string "=")
|
||||
rhs <- term
|
||||
let rhs' = if eff then interpretPure rhs
|
||||
else qualifiedPure `Term.app` rhs
|
||||
pure (lhs, rhs')
|
||||
action = attempt . scope "action" $ (interpretPure <$> term)
|
||||
|
||||
text' :: Parser Literal
|
||||
text' =
|
||||
@ -148,48 +152,24 @@ ann'' = token (char ':') *> TypeParser.type_
|
||||
|
||||
--let server = _; blah = _ in _
|
||||
let_ :: Var v => Parser (Term v) -> Parser (Term v)
|
||||
let_ p = f <$> (let_ *> optional rec_) <*> bindings' <* in_ <*> body
|
||||
let_ p = f <$> withLayout (let_ *> optional rec_) <*> (layout bindings' <|> bindings')
|
||||
where
|
||||
let_ = token (string "let")
|
||||
rec_ = token (string "rec") $> ()
|
||||
bindings' = lineErrorUnless "error parsing let bindings" (bindings p)
|
||||
in_ = lineErrorUnless "missing 'in' after bindings in let-expression'" $
|
||||
(optional (token (string ";")) *> token (string "in"))
|
||||
body = lineErrorUnless "parse error in body of let-expression" p
|
||||
-- f = maybe Term.let1'
|
||||
f :: Ord v => Maybe () -> [(v, Term v)] -> Term v -> Term v
|
||||
f Nothing bindings body = Term.let1 bindings body
|
||||
f (Just _) bindings body = Term.letRec bindings body
|
||||
|
||||
semicolon :: Parser ()
|
||||
semicolon = void $ token (char ';')
|
||||
|
||||
infixBinding :: Var v => Parser (Term v) -> Parser (v, Term v)
|
||||
infixBinding p = ((,,,,) <$> optional (typedecl <* semicolon) <*> prefixVar <*> infixVar <*> prefixVar <*> bindingEqBody p) >>= f
|
||||
where
|
||||
f :: Var v => (Maybe (v, Type v), v, v, v, Term v) -> Parser (v, Term v)
|
||||
f (Just (opName', _), _, opName, _, _) | opName /= opName' =
|
||||
failWith ("The type signature for ‘" ++ show (Var.name opName') ++ "’ lacks an accompanying binding")
|
||||
f (Nothing, arg1, opName, arg2, body) = pure (mkBinding opName [arg1,arg2] body)
|
||||
f (Just (_, type'), arg1, opName, arg2, body) = pure $ (`Term.ann` type') <$> mkBinding opName [arg1,arg2] body
|
||||
|
||||
mkBinding :: Ord v => v -> [v] -> Term v -> (v, Term v)
|
||||
mkBinding f [] body = (f, body)
|
||||
mkBinding f args body = (f, Term.lam'' args body)
|
||||
bindings' = withLayout $ do
|
||||
bs <- lineErrorUnless "error parsing let bindings" (bindings p)
|
||||
semicolon
|
||||
body <- lineErrorUnless "parse error in body of let-expression" p
|
||||
pure (bs, body)
|
||||
f :: Ord v => Maybe () -> ([(v, Term v)], Term v) -> Term v
|
||||
f Nothing (bindings, body) = Term.let1 bindings body
|
||||
f (Just _) (bindings, body) = Term.letRec bindings body
|
||||
|
||||
typedecl :: Var v => Parser (v, Type v)
|
||||
typedecl = (,) <$> prefixVar <*> ann''
|
||||
|
||||
prefixBinding :: Var v => Parser (Term v) -> Parser (v, Term v)
|
||||
prefixBinding p = ((,,,) <$> optional (typedecl <* semicolon) <*> prefixVar <*> many prefixVar <*> bindingEqBody p) >>= f -- todo
|
||||
where
|
||||
f (Just (opName, _), opName', _, _) | opName /= opName' =
|
||||
failWith ("The type signature for ‘" ++ show (Var.name opName') ++ "’ lacks an accompanying binding")
|
||||
f (Nothing, name, args, body) = pure $ mkBinding name args body
|
||||
f (Just (_, t), name, args, body) = pure $ (`Term.ann` t) <$> mkBinding name args body
|
||||
|
||||
bindingEqBody :: Parser (Term v) -> Parser (Term v)
|
||||
bindingEqBody p = eq *> body
|
||||
bindingEqBody p = eq *> (layout body <|> body)
|
||||
where
|
||||
eq = token (char '=')
|
||||
body = lineErrorUnless "parse error in body of binding" p
|
||||
@ -213,7 +193,6 @@ infixVar = (Var.named . Text.pack) <$> (backticked <|> symbolyId)
|
||||
where
|
||||
backticked = char '`' *> wordyId <* token (char '`')
|
||||
|
||||
|
||||
prefixVar :: Var v => Parser v
|
||||
prefixVar = (Var.named . Text.pack) <$> prefixOp
|
||||
where
|
||||
@ -224,7 +203,7 @@ prefixTerm :: Var v => Parser (Term v)
|
||||
prefixTerm = Term.var <$> prefixVar
|
||||
|
||||
keywords :: Set String
|
||||
keywords = Set.fromList ["let", "rec", "in", "->", ":", "=", "where"]
|
||||
keywords = Set.fromList ["do", "let", "rec", "in", "->", ":", "=", "where"]
|
||||
|
||||
lam :: Var v => Parser (Term v) -> Parser (Term v)
|
||||
lam p = Term.lam'' <$> vars <* arrow <*> body
|
||||
@ -240,8 +219,20 @@ 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 =
|
||||
sepBy1 (token (char ';')) (prefixBinding p <|> infixBinding p)
|
||||
bindings p = withLayout (sepBy1 semicolon binding) where
|
||||
binding = do
|
||||
typ <- optional (typedecl <* semicolon)
|
||||
(name, args) <- ((\arg1 op arg2 -> (op,[arg1,arg2])) <$> prefixVar <*> infixVar <*> prefixVar)
|
||||
<|> ((,) <$> prefixVar <*> many prefixVar)
|
||||
body <- bindingEqBody p
|
||||
case typ of
|
||||
Nothing -> pure $ mkBinding name args body
|
||||
Just (nameT, typ)
|
||||
| name == nameT -> case mkBinding name args body of (v,body) -> pure (v, Term.ann body typ)
|
||||
| otherwise -> failWith ("The type signature for ‘" ++ show (Var.name nameT) ++ "’ lacks an accompanying binding")
|
||||
|
||||
mkBinding f [] body = (f, body)
|
||||
mkBinding f args body = (f, Term.lam'' args body)
|
||||
|
||||
moduleBindings :: Var v => Parser [(v, Term v)]
|
||||
moduleBindings = root (bindings term3 <* optional (token (char ';')))
|
||||
moduleBindings = root (bindings term3)
|
||||
|
@ -32,7 +32,8 @@ loadDeclarations path node = do
|
||||
-- directory is the shared subdir - so we check both locations
|
||||
txt <- Text.IO.readFile path <|> Text.IO.readFile (".." `FP.combine` path)
|
||||
let str = Text.unpack txt
|
||||
Note.run $ Node.declare' Term.ref str node
|
||||
_ <- Note.run $ Node.declare' Term.ref str node
|
||||
putStrLn $ "loaded file: " ++ path
|
||||
|
||||
node :: IO TNode
|
||||
node = do
|
||||
|
@ -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 in 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)) in fac 5" "120"
|
||||
, t "let rec ping n = if (n >= 10) n (pong (n + 1)); pong n = ping (n + 1) in 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\" in g" "42"
|
||||
, t "let id : forall a . a -> a; id x = x; g = id 42; p = id \"hi\" in g" "42"
|
||||
, t "((let id x = x in 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"
|
||||
|
@ -40,6 +40,9 @@ atPts print (_,symbol,_) pts t = map go pts where
|
||||
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
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Term"
|
||||
[ testCase "alpha equivalence (term)" $ assertEqual "identity"
|
||||
@ -48,56 +51,56 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Term"
|
||||
, testCase "hash cycles" $ assertEqual "pingpong"
|
||||
(hash pingpong1)
|
||||
(hash pingpong2)
|
||||
, testCase "infix-rendering (1)" $ node >>= \(_,symbol,_) ->
|
||||
let t = unsafeParseTerm "Number.plus 1 1"
|
||||
in assertEqual "+"
|
||||
"1 + 1"
|
||||
(Doc.formatText (Width 80) (Views.term symbol t))
|
||||
, testCase "infix-rendering (unsaturated)" $ node >>= \(_,symbol,_) ->
|
||||
let t = unsafeParseTerm "Number.plus _"
|
||||
in assertEqual "+"
|
||||
"(+) _"
|
||||
(Doc.formatText (Width 80) (Views.term symbol t))
|
||||
, testCase "infix-rendering (totally unsaturated)" $ node >>= \(_,symbol,_) ->
|
||||
let t = unsafeParseTerm "Number.plus"
|
||||
in assertEqual "+" "(+)" (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
, testCase "infix-rendering (2)" $ node >>= \(_,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)" $ node >>= \node ->
|
||||
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 node [(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" $ node >>= \node ->
|
||||
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 node [(5,0)] t
|
||||
assertEqual "p1" [Paths.Fn, Paths.Arg] p1
|
||||
assertEqual "r1" (rect 4 0 8 1) r1
|
||||
, testCase "operator chain rendering" $ node >>= \node ->
|
||||
do
|
||||
t <- pure $ unsafeParseTerm "1 + 2 + 3"
|
||||
[(p1,r1),(p2,_)] <- pure $ atPts False node [(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
|
||||
-- , testCase "infix-rendering (1)" $ node >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus 1 1"
|
||||
-- in assertEqual "+"
|
||||
-- "1 + 1"
|
||||
-- (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (unsaturated)" $ node >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus _"
|
||||
-- in assertEqual "+"
|
||||
-- "(+) _"
|
||||
-- (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (totally unsaturated)" $ node >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus"
|
||||
-- in assertEqual "+" "(+)" (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (2)" $ node >>= \(_,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)" $ node >>= \node ->
|
||||
-- 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 node [(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" $ node >>= \node ->
|
||||
-- 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 node [(5,0)] t
|
||||
-- assertEqual "p1" [Paths.Fn, Paths.Arg] p1
|
||||
-- assertEqual "r1" (rect 4 0 8 1) r1
|
||||
-- , testCase "operator chain rendering" $ node >>= \node ->
|
||||
-- do
|
||||
-- t <- pure $ unsafeParseTerm "1 + 2 + 3"
|
||||
-- [(p1,r1),(p2,_)] <- pure $ atPts False node [(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)
|
||||
@ -108,15 +111,12 @@ rect x y w h =
|
||||
pingpong1 :: TTerm
|
||||
pingpong1 =
|
||||
unsafeParseTerm $
|
||||
unlines [ "let rec ping = x -> pong (x + 1)"
|
||||
, " ; pong = y -> ping (y - 1)"
|
||||
, " in ping 1"
|
||||
unlines [ "let rec "
|
||||
, " ping x = pong (x + 1)"
|
||||
, " pong y = ping (y - 1)"
|
||||
, " ping 1"
|
||||
]
|
||||
|
||||
pingpong2 :: TTerm
|
||||
pingpong2 =
|
||||
unsafeParseTerm $
|
||||
unlines [ "let rec pong1 = p -> ping1 (p - 1)"
|
||||
, " ; ping1 = q -> pong1 (q + 1)"
|
||||
, " in ping1 1"
|
||||
]
|
||||
unsafeParseTerm $ "let rec pong1 p = ping1 (p - 1); ping1 q = pong1 (q + 1); ping1 1"
|
||||
|
@ -1,6 +1,7 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module Unison.Test.TermParser where
|
||||
|
||||
import Data.List
|
||||
import Data.Text (Text)
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
@ -19,7 +20,7 @@ parse :: (String, Term (Symbol DFO)) -> TestTree
|
||||
parse (s, expected) =
|
||||
testCase ("`" ++ s ++ "`") $
|
||||
case parseTerm s of
|
||||
Fail _ _ -> assertFailure "parse failure"
|
||||
Fail e _ -> assertFailure $ "parse failure " ++ intercalate "\n" e
|
||||
Succeed a _ _ -> assertEqual "mismatch" expected a
|
||||
|
||||
parseFail :: (String,String) -> TestTree
|
||||
@ -62,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 in a + 1", let1' [("a", one)] (apps numberplus [a, one]))
|
||||
, ("let a : Int; a = 1 in a + 1", let_a_int1_in_aplus1)
|
||||
, ("let a: Int; a = 1 in a + 1", let_a_int1_in_aplus1)
|
||||
, ("let a :Int; a = 1 in a + 1", let_a_int1_in_aplus1)
|
||||
, ("let a:Int; a = 1 in 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 in f 1 1", f_eq_lamab_in_f11)
|
||||
, ("let f a b = a + b in f 1 1", f_eq_lamab_in_f11)
|
||||
, ("let f (+) b = 1 + b in f g 1", let1' [("f", lam' ["+", "b"] (apps plus [one, b]))] (apps f [g,one]))
|
||||
, ("let a + b = f a b in 1 + 1", let1' [("+", lam' ["a", "b"] fab)] one_plus_one)
|
||||
, ("let (+) : Int -> Int -> Int; a + b = f a b in 1 + 1", plusintintint_fab_in_1plus1)
|
||||
, ("let (+) : Int -> Int -> Int; (+) a b = f a b in 1 + 1", plusintintint_fab_in_1plus1)
|
||||
, ("let (+) : Int -> Int -> Int; (+) a b = f a b in (+) 1 1", plusintintint_fab_in_1plus1)
|
||||
, ("let f b = b + 1; a = 1 in (+) 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) in fix", fix) -- fix
|
||||
, ("let rec fix f = f (fix f) in 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\" in 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)
|
||||
, ("(Remote { pure 42; })", builtin "Remote.pure" `app` num 42)
|
||||
, ("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
|
||||
]
|
||||
)
|
||||
, ("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
|
||||
]
|
||||
)
|
||||
, ("Remote { x := pure 42; y := pure 18; 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")),
|
||||
|
@ -80,7 +80,7 @@ synthesizesAndChecks node e t =
|
||||
|
||||
--singleTest = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typechecker"
|
||||
-- [
|
||||
-- testTerm "f -> let x = (let saved = f in 42) in 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")
|
||||
@ -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 = (+) in f 1)" $ synthesizesAndChecks node
|
||||
(unsafeParseTerm "let f = (+) in 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 = _ in blank 1)" $ synthesizesAndChecks node
|
||||
(unsafeParseTerm "let blank x = _ in 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) in 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 = _ in _" $ \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 in 42) in 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 in 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,14 +153,14 @@ 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\" in 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"
|
||||
tm = unsafeParseTerm tms
|
||||
in synthesizesAndChecks node tm t
|
||||
-- Let generalization not implemented yet; this test fails
|
||||
--, testCase "let generalization: let id a = a; x = id 42; y = id 'hi' in 23" $
|
||||
--, 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")),
|
||||
@ -174,22 +174,22 @@ 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 = _ in _" $ \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 = _ in _" $ \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 = _ in _" $ \tms ->
|
||||
-- testTerm "let x = 42; y = _ in _" $ \tms ->
|
||||
-- testTerm "let x = 42; y = 43 in _" $ \tms ->
|
||||
-- testTerm "let x = 42; y = 43 in 4224" $ \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 ->
|
||||
testCase ("locals ("++tms++")@[Body,Binding 0,Body]") $ do
|
||||
let tm = unsafeParseTerm tms
|
||||
[(_,xt)] <- localsAt node [Paths.Body, Paths.Binding 0, Paths.Body] tm
|
||||
|
@ -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 in y"
|
||||
"let id x = x; g = id 42; y = id id g in 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 in y"
|
||||
"let id x = x; g = id 42; y = id id g in 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 in id3"
|
||||
"let id2 x = x; id1 x = x; id3 x = x in 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 in y"
|
||||
"let id x = x; g = id 42; y = id id g in 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 in y"
|
||||
"let id x = x; g = id 42; y = id id g in (let rec ping x = pong x; pong x = id (ping x) in 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
|
||||
|
@ -1,46 +1,48 @@
|
||||
identity : ∀ a . a -> a;
|
||||
identity a = a;
|
||||
identity : ∀ a . a -> a
|
||||
identity a = a
|
||||
|
||||
Remote.transfer : Node -> Remote Unit;
|
||||
Remote.transfer node = Remote.at node unit;
|
||||
then : ∀ a b c . (a -> b) -> (b -> c) -> a -> c
|
||||
then f1 f2 x = f2 (f1 x)
|
||||
|
||||
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
|
||||
|
||||
then : ∀ a b c . (a -> b) -> (b -> c) -> a -> c;
|
||||
then f1 f2 x = f2 (f1 x);
|
||||
-- Apply a function to a `Remote`
|
||||
Remote.map : ∀ a b . (a -> b) -> Remote a -> Remote b
|
||||
Remote.map f =
|
||||
Remote.bind (f `then` Remote.pure)
|
||||
|
||||
Optional.map : ∀ a b . (a -> b) -> Optional a -> Optional b;
|
||||
Optional.map f = Optional.fold None (f `then` Some);
|
||||
Optional.map : ∀ a b . (a -> b) -> Optional a -> Optional b
|
||||
Optional.map f = Optional.fold None (f `then` Some)
|
||||
|
||||
Optional.bind : ∀ a b . (a -> Optional b) -> Optional a -> Optional b;
|
||||
Optional.bind f = Optional.fold None f;
|
||||
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.pure : ∀ a . a -> Optional a
|
||||
Optional.pure = Some
|
||||
|
||||
Either.map : ∀ a b c . (b -> c) -> Either a b -> Either a c;
|
||||
Either.map f = Either.fold Left (f `then` Right);
|
||||
Either.map : ∀ a b c . (b -> c) -> Either a b -> Either a c
|
||||
Either.map f = Either.fold Left (f `then` Right)
|
||||
|
||||
Either.pure : ∀ a b . b -> Either a b;
|
||||
Either.pure = Right;
|
||||
Either.pure : ∀ a b . b -> Either a b
|
||||
Either.pure = Right
|
||||
|
||||
Either.bind : ∀ a b c . (b -> Either a c) -> Either a b -> Either a c;
|
||||
Either.bind = Either.fold Left;
|
||||
Either.bind : ∀ a b c . (b -> Either a c) -> Either a b -> Either a c
|
||||
Either.bind = Either.fold Left
|
||||
|
||||
Either.swap : ∀ a b . Either a b -> Either b a;
|
||||
Either.swap e = Either.fold Right Left e;
|
||||
Either.swap : ∀ a b . Either a b -> Either b a
|
||||
Either.swap e = Either.fold Right Left e
|
||||
|
||||
const x y = x;
|
||||
const x y = x
|
||||
|
||||
first : ∀ a b . Pair a b -> a;
|
||||
first p = Pair.fold const p;
|
||||
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;
|
||||
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)));
|
||||
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)))
|
||||
|
@ -1,3 +1,4 @@
|
||||
|
||||
Index.empty : ∀ k v . Remote (Index k v);
|
||||
Index.empty = Remote.map Index.unsafeEmpty Remote.here
|
||||
Index.empty : ∀ k v . Remote (Index k v)
|
||||
Index.empty =
|
||||
Remote.map Index.unsafeEmpty Remote.here
|
||||
|
Loading…
Reference in New Issue
Block a user