splitting base out into separate .u file, which is now parsed by tests

This commit is contained in:
Paul Chiusano 2016-08-18 17:24:03 -04:00
parent eb3318f66e
commit 31f6072231
15 changed files with 169 additions and 112 deletions

View File

@ -221,6 +221,7 @@ freshNamed' used n = fresh' used (v' n)
-- | `subst v e body` substitutes `e` for `v` in `body`, avoiding capture by
-- renaming abstractions in `body`
-- TODO: avoid traversing subtrees that cannot contain the free variable
subst :: (Foldable f, Functor f, Var v) => v -> Term f v a -> Term f v a -> Term f v a
subst v = replace match where
match (Var' v') = v == v'
@ -229,7 +230,7 @@ subst v = replace match where
-- | `substs [(t1,v1), (t2,v2), ...] body` performs multiple simultaneous
-- substitutions, avoiding capture
substs :: (Foldable f, Functor f, Var v) => [(v, Term f v a)] -> Term f v a -> Term f v a
substs replacements body = foldr f body replacements where
substs replacements body = foldr f body (reverse replacements) where
f (v, t) body = subst v t body
-- | `replace f t body` substitutes `t` for all maximal (outermost)

View File

@ -31,9 +31,13 @@ synthetic t = Metadata t (Names []) Nothing
syntheticTerm :: Metadata v h
syntheticTerm = synthetic Term
data Names v = Names [v] deriving (Eq,Ord,Show,Generic)
newtype Names v = Names [v] deriving (Eq,Ord,Show,Generic)
data Query = Query Text
firstName :: Names v -> Maybe v
firstName (Names (h:_)) = Just h
firstName _ = Nothing
newtype Query = Query Text
instance Show Query where
show (Query q) = show q

View File

@ -1,9 +1,11 @@
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE OverloadedStrings #-}
module Unison.Node where
-- import Data.Bytes.Serial (Serial)
import Control.Monad
import Data.Foldable
import Data.Aeson.TH
import Data.List
import Data.Map (Map)
@ -12,7 +14,7 @@ import Data.Set (Set)
import Unison.Eval as Eval
import Unison.Metadata (Metadata)
import Unison.Node.Store (Store)
import Unison.Note (Noted)
import Unison.Note (Noted(..),Note(..))
import Unison.Paths (Path)
import Unison.Reference (Reference)
import Unison.Term (Term)
@ -23,11 +25,17 @@ import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Unison.Metadata as Metadata
import qualified Unison.Node.Store as Store
import qualified Unison.Parsers as Parsers
import qualified Unison.Parser as Parser
import qualified Unison.Paths as Paths
import qualified Unison.Reference as Reference
import qualified Unison.Term as Term
import qualified Unison.TermEdit as TermEdit
import qualified Unison.TermParser as TermParser
import qualified Unison.Typechecker as Typechecker
import qualified Unison.Typechecker.Components as Components
import qualified Unison.Var as Var
-- import Debug.Trace
-- | The results of a search.
-- On client, only need to repeat the query if we modify a character
@ -230,3 +238,38 @@ node eval hash store =
types
typeAt
updateMetadata
-- | Declare a group of bindings and add them to the Node.
-- Bindings may be in any order and may refer to each other.
-- They are broken into strongly connected components before
-- being added, and any free variables are resolved using the
-- existing metadata store of the Node.
declare :: (Monad m, Var v) => (h -> Term v) -> [(v, Term v)] -> Node m v h (Type v) (Term v) -> Noted m ()
declare ref bindings node = do
termBuiltins <- do
-- grab all definitions in the node
results <- search node Term.blank [] 1000000 (Metadata.Query "") Nothing
pure [ (v, ref h) | (h, md) <- references results
, v <- toList $ Metadata.firstName (Metadata.names md) ]
let groups = Components.components bindings
-- watch msg a = trace (msg ++ show (map (Var.name . fst) a)) a
bindings' = groups >>= \c -> case c of
[(v,b)] -> [(v,b)]
_ -> [ (v, Term.letRec c b) | (v,b) <- c ]
metadata v = Metadata.Metadata Metadata.Term (Metadata.Names [v]) Nothing
tb0 = Parsers.termBuiltins
step termBuiltins (v, b) = do
let md = metadata v
h <- createTerm node (Parsers.bindBuiltins (tb0 ++ termBuiltins) Parsers.typeBuiltins b) md
updateMetadata node h md
pure ((v, ref h) : termBuiltins)
foldM_ step termBuiltins bindings'
-- | Like `declare`, but takes a `String`
declare' :: (Monad m, Var v) => (h -> Term v) -> String -> Node m v h (Type v) (Term v) -> Noted m ()
declare' ref bindings node = do
bs <- case Parser.run TermParser.moduleBindings bindings of
Parser.Fail err _ -> Noted (pure $ Left (Note err))
Parser.Succeed bs _ _ -> pure bs
declare ref bs node

View File

@ -231,7 +231,7 @@ makeBuiltins whnf =
Term.App' (Term.Builtin' tag) a | tag == "Optional.Some" -> whnf (f `Term.app` a)
_ -> error "Optional.fold unpossible"
op _ = error "Optional.fold unpossible"
in (r, Just (I.Primop 3 op), unsafeParseType "forall a r . r -> (a -> r) -> Optional a -> r", prefix "fold")
in (r, Just (I.Primop 3 op), unsafeParseType "forall a r . r -> (a -> r) -> Optional a -> r", prefix "Optional.fold")
-- Vector
, let r = R.Builtin "Vector.append"

View File

@ -1,3 +1,7 @@
{-# Language DeriveFunctor #-}
{-# Language DeriveTraversable #-}
{-# Language DeriveFoldable #-}
module Unison.Parser where
import Control.Applicative
@ -156,7 +160,7 @@ toEither (Succeed a _ _) = Right a
data Result a
= Fail [String] Bool
| Succeed a Int Bool
deriving (Show)
deriving (Show,Functor,Foldable,Traversable)
instance Functor Parser where
fmap = liftM

View File

@ -8,6 +8,7 @@ import Unison.Symbol (Symbol)
import Unison.Term (Term)
import Unison.Type (Type)
import Unison.Parser (Result(..), run, unsafeGetSucceed)
import Unison.Var (Var)
import Unison.View (DFO)
import qualified Unison.Parser as Parser
import qualified Data.Text as Text
@ -28,74 +29,15 @@ parseType :: String -> Result (Type V)
parseType = parseType' typeBuiltins
parseTerm' :: [(V, Term V)] -> [(V, Type V)] -> String -> Result (Term V)
parseTerm' termBuiltins typeBuiltins s = case run (Parser.root TermParser.term) s of
Succeed e n b ->
Succeed (Term.typeMap (ABT.substs typeBuiltins) (ABT.substs termBuiltins e)) n b
fail -> fail
parseTerm' termBuiltins typeBuiltins s =
bindBuiltins termBuiltins typeBuiltins <$> run (Parser.root TermParser.term) s
bindBuiltins :: Var v => [(v, Term v)] -> [(v, Type v)] -> Term v -> Term v
bindBuiltins termBuiltins typeBuiltins =
Term.typeMap (ABT.substs typeBuiltins) . ABT.substs termBuiltins
parseType' :: [(V, Type V)] -> String -> Result (Type V)
parseType' typeBuiltins s = case run (Parser.root TypeParser.type_) s of
Succeed t n b -> Succeed (ABT.substs typeBuiltins t) n b
fail -> fail
prelude' :: String -> String
prelude' body = unlines
[ "let"
, " Index.empty : forall k v . Remote (Index k v);"
, " Index.empty = Remote.map Index.unsafeEmpty Remote.here"
, "in", "(", prelude body, ")"]
prelude :: String -> String
prelude body = unlines
[ "let"
, " Remote.transfer : Node -> Remote Unit;"
, " Remote.transfer node = Remote.at node unit;"
, ""
, " then : forall a b c . (a -> b) -> (b -> c) -> a -> c;"
, " then f1 f2 x = f2 (f1 x);"
, ""
, " Optional.map : forall a b . (a -> b) -> Optional a -> Optional b;"
, " Optional.map f = Optional.fold None (f `then` Some);"
, ""
, " Optional.bind : forall a b . (a -> Optional b) -> Optional a -> Optional b;"
, " Optional.bind f = Optional.fold None f;"
, ""
, " Optional.pure : forall a . a -> Optional a;"
, " Optional.pure = Some;"
, ""
, " Either.map : forall a b c . (b -> c) -> Either a b -> Either a c;"
, " Either.map f = Either.fold Left (f `then` Right);"
, ""
, " Either.pure : forall a b . b -> Either a b;"
, " Either.pure = Right;"
, ""
, " Either.bind : forall a b c . (b -> Either a c) -> Either a b -> Either a c;"
, " Either.bind = Either.fold Left;"
, ""
, " Either.swap : forall a b . Either a b -> Either b a;"
, " Either.swap e = Either.fold Right Left e;"
, ""
, " const x y = x;"
, ""
, " first : forall a b . Pair a b -> a;"
, " first p = Pair.fold const p;"
, ""
, " rest : forall 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)))"
, ""
, "in" , "(", body, ")"]
unsafeParseTermWithPrelude' :: String -> Term V
unsafeParseTermWithPrelude' prog = unsafeParseTerm (prelude' prog)
unsafeParseTermWithPrelude :: String -> Term V
unsafeParseTermWithPrelude prog = unsafeParseTerm (prelude prog)
parseType' typeBuiltins s = ABT.substs typeBuiltins <$> run (Parser.root TypeParser.type_) s
unsafeParseTerm :: String -> Term V
unsafeParseTerm = unsafeGetSucceed . parseTerm
@ -120,7 +62,7 @@ data Builtin = Builtin Text -- e.g. Builtin "()"
| AliasFromModule Text [Text] [Text]
-- aka default imports
termBuiltins :: [(V, Term V)]
termBuiltins :: Var v => [(v, Term v)]
termBuiltins = (Var.named *** Term.ref) <$> (
[ Alias "+" "Number.plus"
, Alias "-" "Number.minus"
@ -169,7 +111,7 @@ termBuiltins = (Var.named *** Term.ref) <$> (
aliasFromModule m sym = alias sym (Text.intercalate "." [m, sym])
builtinInModule m sym = builtin (Text.intercalate "." [m, sym])
typeBuiltins :: [(V, Type V)]
typeBuiltins :: Var v => [(v, Type v)]
typeBuiltins = (Var.named *** Type.lit) <$>
[ ("Number", Type.Number)
, builtin "Unit"

View File

@ -31,13 +31,13 @@ operator characters (like empty? or fold-left).
Sections / partial application of infix operators is not implemented.
-}
term :: (Var v, Show v) => Parser (Term v)
term :: Var v => Parser (Term v)
term = possiblyAnnotated term2
term2 :: (Var v, Show v) => Parser (Term v)
term2 :: Var v => Parser (Term v)
term2 = let_ term3 <|> term3
term3 ::(Var v, Show v) => Parser (Term v)
term3 :: Var v => Parser (Term v)
term3 = infixApp term4 <|> term4
infixApp :: Var v => Parser (Term v) -> Parser (Term v)
@ -49,16 +49,16 @@ infixApp p = f <$> arg <*> some ((,) <$> infixVar <*> arg)
g :: Ord v => Term v -> (v, Term v) -> Term v
g lhs (op, rhs) = Term.apps (Term.var op) [lhs,rhs]
term4 :: (Var v, Show v) => Parser (Term v)
term4 :: Var v => Parser (Term v)
term4 = prefixApp term5
term5 :: (Var v, Show v) => Parser (Term v)
term5 :: Var v => Parser (Term v)
term5 = lam term <|> effectBlock <|> termLeaf
termLeaf :: (Var v, Show v) => Parser (Term v)
termLeaf :: Var v => Parser (Term v)
termLeaf = asum [hashLit, prefixTerm, lit, tupleOrParenthesized term, blank, vector term]
tupleOrParenthesized :: (Var v, Show v) => Parser (Term v) -> Parser (Term v)
tupleOrParenthesized :: Var v => Parser (Term v) -> Parser (Term v)
tupleOrParenthesized rec =
parenthesized $ go <$> sepBy1 (token $ string ",") rec where
go [t] = t -- was just a parenthesized term
@ -70,7 +70,7 @@ tupleOrParenthesized rec =
-- Remote { x := pure 23; y := at node2 23; pure 19 }
-- Remote { action1; action2; }
-- Remote { action1; x = 1 + 1; action2; }
effectBlock :: (Var v, Show v) => Parser (Term v)
effectBlock :: Var v => Parser (Term v)
effectBlock = do
name <- wordyId <* token (string "{")
let qualifiedPure = ABT.var' (Text.pack name `mappend` Text.pack ".pure")
@ -147,29 +147,29 @@ ann'' :: Var v => Parser (Type v)
ann'' = token (char ':') *> TypeParser.type_
--let server = _; blah = _ in _
let_ :: (Var v, Show v) => Parser (Term v) -> Parser (Term v)
let_ :: Var v => Parser (Term v) -> Parser (Term v)
let_ p = f <$> (let_ *> optional rec_) <*> bindings' <* in_ <*> body
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'" $ token (string "in")
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, Show v) => Parser (Term v) -> Parser (v, Term v)
infixBinding :: Var v => Parser (Term v) -> Parser (v, Term v)
infixBinding p = ((,,,,) <$> optional (typedecl <* semicolon) <*> prefixVar <*> infixVar <*> prefixVar <*> bindingEqBody p) >>= f
where
f :: (Ord v, Show v) => (Maybe (v, Type v), v, v, v, Term v) -> Parser (v, Term v)
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 opName' ++ " lacks an accompanying binding")
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
@ -180,12 +180,11 @@ mkBinding f args body = (f, Term.lam'' args body)
typedecl :: Var v => Parser (v, Type v)
typedecl = (,) <$> prefixVar <*> ann''
prefixBinding :: (Var v, Show v) => Parser (Term v) -> Parser (v, Term v)
prefixBinding :: Var v => Parser (Term v) -> Parser (v, Term v)
prefixBinding p = ((,,,) <$> optional (typedecl <* semicolon) <*> prefixVar <*> many prefixVar <*> bindingEqBody p) >>= f -- todo
where
f :: (Ord v, Show v) => (Maybe (v, Type v), v, [v], Term v) -> Parser (v, Term v)
f (Just (opName, _), opName', _, _) | opName /= opName' =
failWith ("The type signature for " ++ show opName' ++ " lacks an accompanying binding")
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
@ -240,6 +239,9 @@ prefixApp p = f <$> some p
f (func:args) = Term.apps func args
f [] = error "'some' shouldn't produce an empty list"
bindings :: (Var v, Show v) => Parser (Term v) -> Parser [(v, Term v)]
bindings p = --many (binding term)
sepBy1 (token (char ';' <|> char '\n')) (prefixBinding p <|> infixBinding p)
bindings :: Var v => Parser (Term v) -> Parser [(v, Term v)]
bindings p =
sepBy1 (token (char ';')) (prefixBinding p <|> infixBinding p)
moduleBindings :: Var v => Parser [(v, Term v)]
moduleBindings = root (bindings term3 <* optional (token (char ';')))

View File

@ -2,19 +2,18 @@
module Unison.TypeParser where
import Control.Applicative ((<|>), some)
import Data.Char (isUpper, isLower, isAlpha)
import Data.List (foldl1')
import Data.Foldable (asum)
import qualified Data.Text as Text
import Data.Functor
import Data.List (foldl1')
import Unison.Parser
import Unison.Type (Type)
import Unison.Var (Var)
import qualified Data.Text as Text
import qualified Unison.Type as Type
-- type V = Symbol DFO
type_ :: Var v => Parser (Type v)
type_ = forall type1 <|> type1
@ -49,7 +48,7 @@ arrow rec = foldr1 Type.arrow <$> sepBy1 (token $ string "->") rec
-- "forall a b . List a -> List b -> Maybe Text"
forall :: Var v => Parser (Type v) -> Parser (Type v)
forall rec = do
_ <- token $ string "forall"
(void . token $ string "forall") <|> void (token (char '∀'))
vars <- some $ token varName
_ <- token (char '.')
t <- rec

View File

@ -2,6 +2,8 @@
module Unison.Test.Common where
import Control.Monad.IO.Class
import Data.Foldable
import System.IO (FilePath)
import Unison.Symbol (Symbol)
import Unison.Node (Node)
import Unison.Reference (Reference)
@ -9,6 +11,8 @@ import Unison.Term (Term)
import Unison.Type (Type)
import Unison.Views (defaultSymbol)
import qualified Data.Map as Map
import qualified Data.Text.IO as Text.IO
import qualified Data.Text as Text
import qualified Unison.Metadata as Metadata
import qualified Unison.Node as Node
import qualified Unison.Node.MemNode as MemNode
@ -18,13 +22,27 @@ import qualified Unison.View as View
type V = Symbol View.DFO
-- A Node for testing
type TNode = (Node IO V Reference (Type V) (Term V), Reference -> V)
type TNode = (Node IO V Reference (Type V) (Term V), Reference -> V, [(V, Term V)])
loadDeclarations :: FilePath -> Node IO V Reference (Type V) (Term V) -> IO ()
loadDeclarations path node = do
txt <- Text.IO.readFile path
let str = Text.unpack txt
Note.run $ Node.declare' Term.ref str node
node :: IO TNode
node = do
node <- MemNode.make
loadDeclarations "unison-src/base.u" node
symbols <- liftIO . Note.run $
Map.fromList . Node.references <$> Node.search node Term.blank [] 1000 (Metadata.Query "") Nothing
base <- Note.run $ do
-- grab all definitions in the node
results <- Node.search node Term.blank [] 1000000 (Metadata.Query "") Nothing
let x = [ (v, Term.ref h) | (h, md) <- Node.references results
, v <- toList $ Metadata.firstName (Metadata.names md) ]
Note.lift $ putStrLn (show x)
pure x
let firstName (Metadata.Names (n:_)) = n
let lookupSymbol ref = maybe (defaultSymbol ref) (firstName . Metadata.names) (Map.lookup ref symbols)
pure (node, lookupSymbol)
pure (node, lookupSymbol, base)

View File

@ -38,8 +38,9 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
, t "2nd (1,2 + 1,3,4)" "3"
]
t uneval eval = testCase (uneval ++ "" ++ eval) $ do
(node, _) <- node
let term = P.unsafeParseTermWithPrelude uneval
(node, _, builtins) <- node
-- putStrLn (show $ map fst builtins)
let term = P.bindBuiltins builtins [] $ P.unsafeParseTerm uneval
_ <- Note.run $ Node.typeAt node term []
[(_,_,result)] <- Note.run $ Node.evaluateTerms node [([], term)]
assertEqual "comparing results" (P.unsafeParseTerm eval) result

View File

@ -32,7 +32,7 @@ hash :: TTerm -> Hash
hash = ABT.hash
atPts :: Bool -> Common.TNode -> [(Int,Int)] -> TTerm -> [(Paths.Path, Region)]
atPts print (_,symbol) pts t = map go pts where
atPts print (_,symbol,_) pts t = map go pts where
go (x,y) = let p = path x y in (p, Doc.region bounds p)
doc = Views.term symbol t
layout = Doc.layout Doc.textWidth (Width 80) doc
@ -48,20 +48,20 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Term"
, testCase "hash cycles" $ assertEqual "pingpong"
(hash pingpong1)
(hash pingpong2)
, testCase "infix-rendering (1)" $ node >>= \(_,symbol) ->
, 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) ->
, 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) ->
, 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) ->
, testCase "infix-rendering (2)" $ node >>= \(_,symbol,_) ->
do
t <- pure $ unsafeParseTerm "Number.plus 1 1"
let d = Views.term symbol t

View File

@ -35,7 +35,7 @@ instance Show StrongEq where show (StrongEq t) = show t
env :: TNode -> TEnv IO
env node r = do
(node, _) <- Note.lift node
(node, _, _) <- Note.lift node
Node.typeAt node (E.ref r) mempty
localsAt :: TNode -> Path -> TTerm -> IO [(V, Type V)]
@ -45,7 +45,7 @@ localsAt node path e = Note.run $ do
synthesizesAt :: TNode -> Path -> TTerm -> TType -> Assertion
synthesizesAt node path e t = Note.run $ do
(node, _) <- Note.lift node
(node, _, _) <- Note.lift node
t2 <- Node.typeAt node e path
_ <- Note.fromEither (Typechecker.subtype t2 t)
_ <- Note.fromEither (Typechecker.subtype t t2)

View File

@ -32,7 +32,7 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
"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 before after = testCase (before ++ "" ++ after) $ do
(node, _) <- node
(node, _, _) <- node
let term = unsafeParseTerm before
case term of
Term.LetRecNamed' bs _ ->

40
unison-src/base.u Normal file
View File

@ -0,0 +1,40 @@
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);
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.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.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.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)));

3
unison-src/extra.u Normal file
View File

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