mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-17 13:27:30 +03:00
rename Node -> Codebase, split out evaluation functions, tests passing in shared
This commit is contained in:
parent
dde18ec595
commit
4459246024
@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module Unison.Node.Builtin where
|
||||
module Unison.Builtin where
|
||||
|
||||
import Data.List
|
||||
import Data.Text (Text)
|
||||
@ -10,11 +10,12 @@ import Unison.Term (Term)
|
||||
import Unison.Type (Type)
|
||||
import Unison.Typechecker.Context (remoteSignatureOf)
|
||||
import Unison.Util.Logger (Logger)
|
||||
import Unison.Var (Var)
|
||||
import qualified Data.Char as Char
|
||||
import qualified Data.Vector as Vector
|
||||
import qualified Data.Text as Text
|
||||
import qualified Unison.ABT as ABT
|
||||
import qualified Unison.Eval.Interpreter as I
|
||||
import qualified Unison.Interpreter as I
|
||||
import qualified Unison.Metadata as Metadata
|
||||
import qualified Unison.Note as N
|
||||
import qualified Unison.Reference as R
|
||||
@ -28,13 +29,12 @@ import qualified Unison.Util.Logger as L
|
||||
|
||||
type DFO = View.DFO
|
||||
type V = Symbol DFO
|
||||
type WHNFEval = Term V -> N.Noted IO (ABT.Term (Term.F V) V ())
|
||||
|
||||
data Builtin = Builtin
|
||||
{ reference :: R.Reference
|
||||
, op :: Maybe (I.Primop (N.Noted IO) V)
|
||||
, bType :: Type V
|
||||
, metadata :: Metadata V R.Reference
|
||||
data Builtin v =
|
||||
Builtin { reference :: R.Reference
|
||||
, op :: Maybe (I.Primop (N.Noted IO) v)
|
||||
, bType :: Type v
|
||||
, metadata :: Metadata v R.Reference
|
||||
}
|
||||
|
||||
unitRef :: Ord v => Term v
|
||||
@ -47,34 +47,28 @@ 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 :: Logger -> WHNFEval -> [Builtin]
|
||||
makeBuiltins logger whnf =
|
||||
makeBuiltins :: (Show v, Var v) => Logger -> [Builtin v]
|
||||
makeBuiltins logger =
|
||||
let
|
||||
numeric2 :: Term V -> (Double -> Double -> Double) -> I.Primop (N.Noted IO) V
|
||||
numeric2 sym f = I.Primop 2 $ \xs -> case xs of
|
||||
[x,y] -> g <$> whnf x <*> whnf y
|
||||
where g (Term.Number' x) (Term.Number' y) = Term.lit (Term.Number (f x y))
|
||||
g x y = sym `Term.app` x `Term.app` y
|
||||
numeric2 :: Var v => (Double -> Double -> Double) -> I.Primop (N.Noted IO) v
|
||||
numeric2 f = I.Primop 2 $ \xs -> case xs of
|
||||
[Term.Number' x, Term.Number' y] -> pure (Term.num $ f x y)
|
||||
_ -> error "unpossible"
|
||||
numericCompare :: Term V -> (Double -> Double -> Bool) -> I.Primop (N.Noted IO) V
|
||||
numericCompare sym f = I.Primop 2 $ \xs -> case xs of
|
||||
[x,y] -> g <$> whnf x <*> whnf y
|
||||
where g (Term.Number' x) (Term.Number' y) = case f x y of
|
||||
False -> false
|
||||
True -> true
|
||||
g x y = sym `Term.app` x `Term.app` y
|
||||
numericCompare :: Var v => (Double -> Double -> Bool) -> I.Primop (N.Noted IO) v
|
||||
numericCompare f = I.Primop 2 $ \xs -> case xs of
|
||||
[Term.Number' x, Term.Number' y] -> case f x y of
|
||||
False -> pure false
|
||||
True -> pure true
|
||||
_ -> error "unpossible"
|
||||
string2 :: Term V -> (Text -> Text -> Text) -> I.Primop (N.Noted IO) V
|
||||
string2 sym f = I.Primop 2 $ \xs -> case xs of
|
||||
[x,y] -> g <$> whnf x <*> whnf y
|
||||
where g (Term.Text' x) (Term.Text' y) = Term.lit (Term.Text (f x y))
|
||||
g x y = sym `Term.app` x `Term.app` y
|
||||
string2 :: Var v => (Text -> Text -> Text) -> I.Primop (N.Noted IO) v
|
||||
string2 f = I.Primop 2 $ \xs -> case xs of
|
||||
[Term.Text' x, Term.Text' y] -> pure (Term.text $ f x y)
|
||||
_ -> error "unpossible"
|
||||
string2' :: Term V -> (Text -> Text -> Bool) -> I.Primop (N.Noted IO) V
|
||||
string2' sym f = I.Primop 2 $ \xs -> case xs of
|
||||
[x,y] -> g <$> whnf x <*> whnf y
|
||||
where g (Term.Text' x) (Term.Text' y) = if f x y then true else false
|
||||
g x y = sym `Term.app` x `Term.app` y
|
||||
string2' :: Var v => (Text -> Text -> Bool) -> I.Primop (N.Noted IO) v
|
||||
string2' f = I.Primop 2 $ \xs -> case xs of
|
||||
[Term.Text' x, Term.Text' y] -> case f x y of
|
||||
False -> pure false
|
||||
True -> pure true
|
||||
_ -> error "unpossible"
|
||||
in map (\(r, o, t, m) -> Builtin r o t m)
|
||||
[ -- Unit type
|
||||
@ -85,19 +79,15 @@ makeBuiltins logger whnf =
|
||||
|
||||
-- debugging printlns
|
||||
, let r = R.Builtin "Debug.log";
|
||||
op [msg,logged,a] = do
|
||||
Term.Text' msg <- whnf msg
|
||||
logged <- whnf logged
|
||||
op [Term.Text' msg,logged,a] = do
|
||||
N.lift $ L.error logger (Text.unpack msg ++ ": " ++ show logged)
|
||||
whnf a
|
||||
pure a
|
||||
op _ = error "unpossible"
|
||||
typ = "∀ a b . Text -> a -> b -> b"
|
||||
in (r, Just (I.Primop 3 op), unsafeParseType typ, prefix "Debug.log")
|
||||
|
||||
, let r = R.Builtin "Debug.watch";
|
||||
op [msg,a] = do
|
||||
Term.Text' msg <- whnf msg
|
||||
a <- whnf a
|
||||
op [Term.Text' msg, a] = do
|
||||
N.lift $ L.error logger (Text.unpack msg ++ ": " ++ show a)
|
||||
pure a
|
||||
op _ = error "unpossible"
|
||||
@ -110,9 +100,7 @@ makeBuiltins logger whnf =
|
||||
, let r = R.Builtin "False";
|
||||
in (r, Nothing, Type.builtin "Boolean", prefix "False")
|
||||
, let r = R.Builtin "Boolean.and";
|
||||
op [b1,b2] = do
|
||||
Term.Builtin' b1 <- whnf b1
|
||||
Term.Builtin' b2 <- whnf b2
|
||||
op [Term.Builtin' b1, Term.Builtin' b2] =
|
||||
pure $ case (b1,b2) of
|
||||
_ | Text.head b1 /= Text.head b2 -> false
|
||||
| otherwise -> if Text.head b1 == 'T' then true else false
|
||||
@ -120,9 +108,7 @@ makeBuiltins logger whnf =
|
||||
typ = "Boolean -> Boolean -> Boolean"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "and")
|
||||
, let r = R.Builtin "Boolean.or";
|
||||
op [b1,b2] = do
|
||||
Term.Builtin' b1 <- whnf b1
|
||||
Term.Builtin' b2 <- whnf b2
|
||||
op [Term.Builtin' b1,Term.Builtin' b2] =
|
||||
pure $ case (b1,b2) of
|
||||
_ | Text.head b1 /= Text.head b2 -> true
|
||||
| otherwise -> if Text.head b1 == 'F' then false else true
|
||||
@ -130,8 +116,7 @@ makeBuiltins logger whnf =
|
||||
typ = "Boolean -> Boolean -> Boolean"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "or")
|
||||
, let r = R.Builtin "Boolean.not";
|
||||
op [b1] = do
|
||||
Term.Builtin' b1 <- whnf b1
|
||||
op [Term.Builtin' b1] =
|
||||
pure $ if Text.head b1 == 'T' then false else true
|
||||
op _ = error "unpossible"
|
||||
typ = "Boolean -> Boolean"
|
||||
@ -139,50 +124,46 @@ makeBuiltins logger whnf =
|
||||
|
||||
-- Number
|
||||
, let r = R.Builtin "Number.+"
|
||||
in (r, Just (numeric2 (Term.ref r) (+)), numOpTyp, assoc 4 "+")
|
||||
in (r, Just (numeric2 (+)), unsafeParseType "Number -> Number -> Number", prefix "+")
|
||||
, let r = R.Builtin "Number.-"
|
||||
in (r, Just (numeric2 (Term.ref r) (-)), numOpTyp, opl 4 "-")
|
||||
in (r, Just (numeric2 (-)), unsafeParseType "Number -> Number -> Number", prefix "-")
|
||||
, let r = R.Builtin "Number.*"
|
||||
in (r, Just (numeric2 (Term.ref r) (*)), numOpTyp, assoc 5 "*")
|
||||
in (r, Just (numeric2 (*)), unsafeParseType "Number -> Number -> Number", prefix "*")
|
||||
, let r = R.Builtin "Number./"
|
||||
in (r, Just (numeric2 (Term.ref r) (/)), numOpTyp, opl 5 "/")
|
||||
in (r, Just (numeric2 (/)), unsafeParseType "Number -> Number -> Number", prefix "/")
|
||||
, let r = R.Builtin "Number.>"
|
||||
in (r, Just (numericCompare (Term.ref r) (>)), numCompareTyp, opl 3 "Number.>")
|
||||
in (r, Just (numericCompare (>)), unsafeParseType "Number -> Number -> Boolean", prefix "Number.>")
|
||||
, let r = R.Builtin "Number.<"
|
||||
in (r, Just (numericCompare (Term.ref r) (<)), numCompareTyp, opl 3 "Number.<")
|
||||
in (r, Just (numericCompare (<)), unsafeParseType "Number -> Number -> Boolean", prefix "Number.<")
|
||||
, let r = R.Builtin "Number.>="
|
||||
in (r, Just (numericCompare (Term.ref r) (>=)), numCompareTyp, opl 3 "Number.>=")
|
||||
in (r, Just (numericCompare (>=)), unsafeParseType "Number -> Number -> Boolean", prefix "Number.>=")
|
||||
, let r = R.Builtin "Number.<="
|
||||
in (r, Just (numericCompare (Term.ref r) (<=)), numCompareTyp, opl 3 "Number.<=")
|
||||
in (r, Just (numericCompare (<=)), unsafeParseType "Number -> Number -> Boolean", prefix "Number.<=")
|
||||
, let r = R.Builtin "Number.=="
|
||||
in (r, Just (numericCompare (Term.ref r) (==)), numCompareTyp, opl 3 "Number.==")
|
||||
in (r, Just (numericCompare (==)), unsafeParseType "Number -> Number -> Boolean", prefix "Number.==")
|
||||
, let r = R.Builtin "Number.Order"
|
||||
in (r, Nothing, unsafeParseType "Order Number", prefix "Number.Order")
|
||||
|
||||
-- Duration
|
||||
, let r = R.Builtin "Duration.seconds"
|
||||
op [n] = do
|
||||
Term.Number' n <- whnf n
|
||||
pure $ Term.num n
|
||||
op [Term.Number' n] = pure $ Term.num n
|
||||
op _ = fail "Duration.seconds unpossible"
|
||||
in (r, Just (I.Primop 1 op), unsafeParseType "Number -> Duration", prefix "Duration.seconds")
|
||||
|
||||
-- Remote
|
||||
, let r = R.Builtin "Remote.sleep"
|
||||
op [seconds] = do
|
||||
Term.Number' seconds <- whnf seconds
|
||||
op [Term.Number' seconds] =
|
||||
let s = Remote.Seconds seconds
|
||||
pure $ Term.remote (Remote.Step (Remote.Local (Remote.Sleep s)))
|
||||
in pure $ Term.remote (Remote.Step (Remote.Local (Remote.Sleep s)))
|
||||
op _ = fail "Remote.sleep unpossible"
|
||||
in (r, Just (I.Primop 1 op), unsafeParseType "Duration -> Remote Unit", prefix "Remote.sleep")
|
||||
, let r = R.Builtin "Remote.at"
|
||||
op [node,term] = do
|
||||
Term.Distributed' (Term.Node node) <- whnf node
|
||||
op [Term.Distributed' (Term.Node node), term] =
|
||||
pure $ Term.remote (Remote.Step (Remote.At node term))
|
||||
op _ = fail "Remote.at unpossible"
|
||||
in (r, Just (I.Primop 2 op), remoteSignatureOf "Remote.at", prefix "Remote.at")
|
||||
, let r = R.Builtin "Remote.here"
|
||||
op [] = pure $ Term.remote (Remote.Step (Remote.Local (Remote.Here)))
|
||||
op [] = pure $ Term.remote (Remote.Step (Remote.Local Remote.Here))
|
||||
op _ = fail "Remote.here unpossible"
|
||||
in (r, Just (I.Primop 0 op), remoteSignatureOf "Remote.here", prefix "Remote.here")
|
||||
, let r = R.Builtin "Remote.spawn"
|
||||
@ -190,8 +171,7 @@ makeBuiltins logger whnf =
|
||||
op _ = fail "Remote.spawn unpossible"
|
||||
in (r, Just (I.Primop 0 op), remoteSignatureOf "Remote.spawn", prefix "Remote.spawn")
|
||||
, let r = R.Builtin "Remote.send"
|
||||
op [c, v] = do
|
||||
Term.Distributed' (Term.Channel c) <- whnf c
|
||||
op [Term.Distributed' (Term.Channel c), v] =
|
||||
pure $ Term.remote (Remote.Step (Remote.Local (Remote.Send c v)))
|
||||
op _ = fail "Remote.send unpossible"
|
||||
in (r, Just (I.Primop 2 op), remoteSignatureOf "Remote.send", prefix "Remote.send")
|
||||
@ -201,7 +181,6 @@ makeBuiltins logger whnf =
|
||||
in (r, Just (I.Primop 0 op), remoteSignatureOf "Remote.channel", prefix "Remote.channel")
|
||||
, let r = R.Builtin "Remote.bind"
|
||||
op [g, r] = do
|
||||
r <- whnf r
|
||||
-- right associate the binds so that there is always a Step on the outside
|
||||
let kcomp f g = Term.lam' ["x"] $ Term.builtin "Remote.bind" `Term.apps` [g, f `Term.app` Term.var' "x"]
|
||||
case r of
|
||||
@ -224,38 +203,34 @@ makeBuiltins logger whnf =
|
||||
op _ = fail "unpossible"
|
||||
in (r, Just (I.Primop 2 op), remoteSignatureOf "Remote.map", prefix "Remote.map")
|
||||
, let r = R.Builtin "Remote.receive-async"
|
||||
op [chan, timeout] = do
|
||||
Term.Number' seconds <- whnf timeout
|
||||
Term.Distributed' (Term.Channel chan) <- whnf chan
|
||||
op [Term.Distributed' (Term.Channel chan), Term.Number' seconds] =
|
||||
pure $ Term.remote (Remote.Step (Remote.Local (Remote.ReceiveAsync chan (Remote.Seconds seconds))))
|
||||
op _ = fail "unpossible"
|
||||
in (r, Just (I.Primop 2 op), remoteSignatureOf "Remote.receive-async", prefix "Remote.receive-async")
|
||||
, let r = R.Builtin "Remote.receive"
|
||||
op [chan] = do
|
||||
Term.Distributed' (Term.Channel chan) <- whnf chan
|
||||
op [Term.Distributed' (Term.Channel chan)] =
|
||||
pure $ Term.remote (Remote.Step (Remote.Local (Remote.Receive chan)))
|
||||
op _ = fail "unpossible"
|
||||
in (r, Just (I.Primop 1 op), remoteSignatureOf "Remote.receive", prefix "Remote.receive")
|
||||
, let r = R.Builtin "Remote.fork"
|
||||
op [r] = do
|
||||
Term.Distributed' (Term.Remote r) <- whnf r
|
||||
op [Term.Distributed' (Term.Remote r)] =
|
||||
pure $ Term.remote (Remote.Step (Remote.Local (Remote.Fork r)))
|
||||
op _ = fail "unpossible"
|
||||
in (r, Just (I.Primop 1 op), remoteSignatureOf "Remote.fork", prefix "Remote.fork")
|
||||
|
||||
-- Text
|
||||
, let r = R.Builtin "Text.concatenate"
|
||||
in (r, Just (string2 (Term.ref r) mappend), strOpTyp, prefix "Text.concatenate")
|
||||
in (r, Just (string2 mappend), unsafeParseType "Text -> Text -> Text", prefix "Text.concatenate")
|
||||
, let r = R.Builtin "Text.=="
|
||||
in (r, Just (string2' (Term.ref r) (==)), textCompareTyp, prefix "Text.==")
|
||||
in (r, Just (string2' (==)), unsafeParseType "Text -> Text -> Boolean", prefix "Text.==")
|
||||
, let r = R.Builtin "Text.<"
|
||||
in (r, Just (string2' (Term.ref r) (<)), textCompareTyp, prefix "Text.<")
|
||||
in (r, Just (string2' (<)), unsafeParseType "Text -> Text -> Boolean", prefix "Text.<")
|
||||
, let r = R.Builtin "Text.<="
|
||||
in (r, Just (string2' (Term.ref r) (<=)), textCompareTyp, prefix "Text.<=")
|
||||
in (r, Just (string2' (<=)), unsafeParseType "Text -> Text -> Boolean", prefix "Text.<=")
|
||||
, let r = R.Builtin "Text.>"
|
||||
in (r, Just (string2' (Term.ref r) (>)), textCompareTyp, prefix "Text.>")
|
||||
in (r, Just (string2' (>)), unsafeParseType "Text -> Text -> Boolean", prefix "Text.>")
|
||||
, let r = R.Builtin "Text.>="
|
||||
in (r, Just (string2' (Term.ref r) (>=)), textCompareTyp, prefix "Text.>=")
|
||||
in (r, Just (string2' (>=)), unsafeParseType "Text -> Text -> Boolean", prefix "Text.>=")
|
||||
, let r = R.Builtin "Text.Order"
|
||||
in (r, Nothing, unsafeParseType "Order Text", prefix "Text.Order")
|
||||
, let r = R.Builtin "Text.lowercase"
|
||||
@ -292,11 +267,7 @@ makeBuiltins logger whnf =
|
||||
, let r = R.Builtin "Pair"
|
||||
in (r, Nothing, unsafeParseType "forall a b . a -> b -> Pair a b", prefix "Pair")
|
||||
, let r = R.Builtin "Pair.fold"
|
||||
op [f,p] = do
|
||||
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 [f,Term.Apps' (Term.Builtin' "Pair") [a,b]] = pure $ f `Term.apps` [a,b]
|
||||
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 "Pair.fold")
|
||||
, let r = R.Builtin "Pair.Order"
|
||||
@ -309,10 +280,10 @@ makeBuiltins logger whnf =
|
||||
in (r, Nothing, unsafeParseType "forall a b . b -> Either a b", prefix "Right")
|
||||
, let r = R.Builtin "Either.fold"
|
||||
op [fa,fb,e] = do
|
||||
Term.App' (Term.Builtin' tag) aOrB <- whnf e
|
||||
let Term.App' (Term.Builtin' tag) aOrB = e
|
||||
case tag of
|
||||
_ | tag == "Either.Left" -> whnf (fa `Term.app` aOrB)
|
||||
| tag == "Either.Right" -> whnf (fb `Term.app` aOrB)
|
||||
_ | tag == "Either.Left" -> pure $ fa `Term.app` aOrB
|
||||
| tag == "Either.Right" -> pure $ fb `Term.app` aOrB
|
||||
| otherwise -> error "type errror"
|
||||
op _ = error "Either.fold unpossible"
|
||||
in (r, Just (I.Primop 3 op), unsafeParseType "forall a b r . (a -> r) -> (b -> r) -> Either a b -> r", prefix "Either.fold")
|
||||
@ -323,29 +294,21 @@ makeBuiltins logger whnf =
|
||||
, let r = R.Builtin "Optional.Some"
|
||||
in (r, Nothing, unsafeParseType "forall a . a -> Optional a", prefix "Some")
|
||||
, let r = R.Builtin "Optional.fold"
|
||||
op [fz,f,o] = whnf o >>= \o -> case o of
|
||||
Term.Builtin' tag | tag == "Optional.None" -> whnf fz
|
||||
Term.App' (Term.Builtin' tag) a | tag == "Optional.Some" -> whnf (f `Term.app` a)
|
||||
op [fz,f,o] = case o of
|
||||
Term.Builtin' tag | tag == "Optional.None" -> pure fz
|
||||
Term.App' (Term.Builtin' tag) a | tag == "Optional.Some" -> pure (f `Term.app` a)
|
||||
_ -> error $ "Optional.fold unpossible: " ++ show o
|
||||
op _ = error "Optional.fold unpossible"
|
||||
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"
|
||||
op [last,init] = do
|
||||
initr <- whnf init
|
||||
pure $ case initr of
|
||||
Term.Vector' init -> Term.vector' (Vector.snoc init last)
|
||||
init -> Term.ref r `Term.app` last `Term.app` init
|
||||
op [last,Term.Vector' init] = do
|
||||
pure $ Term.vector' (Vector.snoc init last)
|
||||
op _ = fail "Vector.append unpossible"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType "forall a . a -> Vector a -> Vector a", prefix "Vector.append")
|
||||
, let r = R.Builtin "Vector.concatenate"
|
||||
op [a,b] = do
|
||||
ar <- whnf a
|
||||
br <- whnf b
|
||||
pure $ case (ar,br) of
|
||||
(Term.Vector' a, Term.Vector' b) -> Term.vector' (a `mappend` b)
|
||||
(a,b) -> Term.ref r `Term.app` a `Term.app` b
|
||||
op [Term.Vector' a, Term.Vector' b] = pure $ Term.vector' (a `mappend` b)
|
||||
op _ = fail "Vector.concatenate unpossible"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType "forall a . Vector a -> Vector a -> Vector a", prefix "Vector.concatenate")
|
||||
, let r = R.Builtin "Vector.empty"
|
||||
@ -353,56 +316,48 @@ makeBuiltins logger whnf =
|
||||
op _ = fail "Vector.empty unpossible"
|
||||
in (r, Just (I.Primop 0 op), unsafeParseType "forall a . Vector a", prefix "Vector.empty")
|
||||
, let r = R.Builtin "Vector.range"
|
||||
op [start,stop] = do
|
||||
Term.Number' start <- whnf start
|
||||
Term.Number' stop <- whnf stop
|
||||
op [Term.Number' start, Term.Number' stop] =
|
||||
let num = Term.num . fromIntegral
|
||||
ns = [floor start .. floor stop - (1 :: Int)]
|
||||
pure $ Term.vector' (Vector.fromList . map num $ ns)
|
||||
in pure $ Term.vector' (Vector.fromList . map num $ ns)
|
||||
op _ = fail "Vector.range unpossible"
|
||||
typ = unsafeParseType "Number -> Number -> Vector Number"
|
||||
in (r, Just (I.Primop 2 op), typ, prefix "Vector.range")
|
||||
, let r = R.Builtin "Vector.empty?"
|
||||
op [v] = do
|
||||
Term.Vector' vs <- whnf v
|
||||
pure $ if Vector.null vs then true else false
|
||||
op [Term.Vector' vs] = 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.zip"
|
||||
op [v,v2] = do
|
||||
Term.Vector' vs <- whnf v
|
||||
Term.Vector' vs2 <- whnf v2
|
||||
op [Term.Vector' vs, Term.Vector' vs2] =
|
||||
pure $ Term.vector' (Vector.zipWith pair' vs vs2)
|
||||
op _ = fail "Vector.zip unpossible"
|
||||
typ = "∀ a b . Vector a -> Vector b -> Vector (a,b)"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "Vector.zip")
|
||||
, let r = R.Builtin "Vector.sort-keyed"
|
||||
op [f,v] = do
|
||||
Term.Vector' vs <- whnf v
|
||||
ks <- traverse (whnf . Term.app f) vs
|
||||
ks <- pure $ fmap extractKey ks
|
||||
let sortableVs = Vector.zip ks vs
|
||||
op [Term.Vector' vs0] =
|
||||
let extract1 (Term.Apps' _ [hd, _]) = extractKey hd
|
||||
extract1 _ = error "extract1 failure"
|
||||
extract2 (Term.Apps' _ [_, Term.Apps' _ [hd,_]]) = hd
|
||||
extract2 _ = error "extract2 failure"
|
||||
ks = fmap extract1 vs0
|
||||
vs = fmap extract2 vs0
|
||||
sortableVs = Vector.zip ks vs
|
||||
f' (a, _) (b, _) = a `compare` b
|
||||
pure . Term.vector . fmap snd $ sortBy f' (Vector.toList sortableVs)
|
||||
sorted = sortBy f' (Vector.toList sortableVs)
|
||||
in pure . Term.vector . fmap snd $ sorted
|
||||
op _ = fail "Vector.sort-keyed unpossible"
|
||||
typ = "∀ a k . (a -> Order.Key k) -> Vector a -> Vector a"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "Vector.sort-keyed")
|
||||
typ = "∀ a k . Vector (Order.Key k, a) -> Vector a"
|
||||
in (r, Just (I.Primop 1 op), unsafeParseType typ, prefix "Vector.sort-keyed")
|
||||
, let r = R.Builtin "Vector.size"
|
||||
op [v] = do
|
||||
Term.Vector' vs <- whnf v
|
||||
pure $ Term.num (fromIntegral $ Vector.length vs)
|
||||
op [Term.Vector' vs] = 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 [Term.Vector' vs] = 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.halve"
|
||||
op [v] = do
|
||||
Term.Vector' vs <- whnf v
|
||||
pure $ case Vector.null vs of
|
||||
op [Term.Vector' vs] = pure $ case Vector.null vs of
|
||||
True -> pair' (Term.vector []) (Term.vector [])
|
||||
False -> case Vector.splitAt (Vector.length vs `div` 2) vs of
|
||||
(x,y) -> pair' (Term.vector' x) (Term.vector' y)
|
||||
@ -410,9 +365,7 @@ makeBuiltins logger whnf =
|
||||
typ = "forall a . Vector a -> (Vector a, Vector a)"
|
||||
in (r, Just (I.Primop 1 op), unsafeParseType typ, prefix "Vector.halve")
|
||||
, let r = R.Builtin "Vector.at"
|
||||
op [n,vec] = do
|
||||
Term.Number' n <- whnf n
|
||||
Term.Vector' vs <- whnf vec
|
||||
op [Term.Number' n, Term.Vector' vs] =
|
||||
pure $ case vs Vector.!? (floor n) of
|
||||
Nothing -> none
|
||||
Just t -> some t
|
||||
@ -420,42 +373,29 @@ makeBuiltins logger whnf =
|
||||
typ = "forall a . Number -> Vector a -> Optional a"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "Vector.at")
|
||||
, let r = R.Builtin "Vector.take"
|
||||
op [n,vec] = do
|
||||
Term.Number' n <- whnf n
|
||||
Term.Vector' vs <- whnf vec
|
||||
pure $ Term.vector' (Vector.take (floor n) vs)
|
||||
op [Term.Number' n, Term.Vector' vs] = pure $ Term.vector' (Vector.take (floor n) vs)
|
||||
op _ = fail "Vector.take unpossible"
|
||||
typ = "forall a . Number -> Vector a -> Vector a"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "Vector.take")
|
||||
, let r = R.Builtin "Vector.drop"
|
||||
op [n,vec] = do
|
||||
Term.Number' n <- whnf n
|
||||
Term.Vector' vs <- whnf vec
|
||||
op [Term.Number' n, Term.Vector' vs] =
|
||||
pure $ Term.vector' (Vector.drop (floor n) vs)
|
||||
op _ = fail "Vector.drop unpossible"
|
||||
typ = "forall a . Number -> Vector a -> Vector a"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType typ, prefix "Vector.drop")
|
||||
-- I AM HERE
|
||||
, 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
|
||||
_ -> pure $ Term.ref r `Term.app` vec
|
||||
op [f,z,Term.Vector' vs] = pure $
|
||||
Vector.foldl' (\acc a -> f `Term.apps` [acc, a]) z vs
|
||||
op _ = fail "Vector.fold-left unpossible"
|
||||
typ = "forall a b . (b -> a -> b) -> b -> Vector a -> b"
|
||||
in (r, Just (I.Primop 3 op), unsafeParseType typ, prefix "Vector.fold-left")
|
||||
, let r = R.Builtin "Vector.map"
|
||||
op [f,vec] = do
|
||||
vecr <- whnf vec
|
||||
pure $ case vecr of
|
||||
Term.Vector' vs -> Term.vector' (fmap (Term.app f) vs)
|
||||
_ -> Term.ref r `Term.app` vecr
|
||||
op [f,Term.Vector' vs] = pure $ Term.vector' (fmap (Term.app f) vs)
|
||||
op _ = fail "Vector.map unpossible"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType "forall a b . (a -> b) -> Vector a -> Vector b", prefix "Vector.map")
|
||||
, let r = R.Builtin "Vector.prepend"
|
||||
op [hd,tl] = do
|
||||
tlr <- whnf tl
|
||||
pure $ case tlr of
|
||||
Term.Vector' tl -> Term.vector' (Vector.cons hd tl)
|
||||
tl -> Term.ref r `Term.app` hd `Term.app` tl
|
||||
op [hd, Term.Vector' tl] = pure $ Term.vector' (Vector.cons hd tl)
|
||||
op _ = fail "Vector.prepend unpossible"
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType "forall a . a -> Vector a -> Vector a", prefix "Vector.prepend")
|
||||
, let r = R.Builtin "Vector.single"
|
||||
@ -475,20 +415,16 @@ makeBuiltins logger whnf =
|
||||
, let r = R.Builtin "Equal"
|
||||
in (r, Nothing, unsafeParseType "Comparison", prefix "Equal")
|
||||
, let r = R.Builtin "Comparison.fold"
|
||||
op [lt,eq,gt,c] = do
|
||||
Term.Builtin' c <- whnf c
|
||||
case Text.head c of
|
||||
'L' -> whnf lt
|
||||
'E' -> whnf eq
|
||||
'G' -> whnf gt
|
||||
op [lt,eq,gt, Term.Builtin' c] = case Text.head c of
|
||||
'L' -> pure lt
|
||||
'E' -> pure eq
|
||||
'G' -> pure gt
|
||||
_ -> fail $ "Comparison.fold not one of {Less,Equal,Greater}" ++ show c
|
||||
op _ = error "Comparison.fold unpossible"
|
||||
in (r, Just (I.Primop 4 op), unsafeParseType "∀ r . r -> r -> r -> Comparison -> r", prefix "Comparison.fold")
|
||||
|
||||
, let r = R.Builtin "Order.Key.compare"
|
||||
op [a,b] = do
|
||||
a <- whnf a
|
||||
b <- whnf b
|
||||
op [a,b] =
|
||||
pure $ case compareKeys a b of
|
||||
LT -> Term.builtin "Less"
|
||||
EQ -> Term.builtin "Equal"
|
||||
@ -503,21 +439,19 @@ makeBuiltins logger whnf =
|
||||
neg (Term.Number' n) = Term.num (negate n)
|
||||
neg t@(Term.Builtin' _) = t
|
||||
neg t = error $ "don't know how to negate " ++ show t
|
||||
op' ord a = do
|
||||
ord <- whnf ord
|
||||
case ord of
|
||||
op' ord a = case ord of
|
||||
Term.App' (Term.Builtin' invert) ord
|
||||
| invert == "Order.invert" -> flip <$> op' ord a
|
||||
Term.Builtin' b
|
||||
| b == "Text.Order" -> do a <- whnf a; pure (a:)
|
||||
| b == "Number.Order" -> do a <- whnf a; pure (a:)
|
||||
| b == "Hash.Order" -> do Term.App' _ a <- whnf a; pure (a:)
|
||||
| b == "Unit.Order" -> do a <- whnf a; pure (a:)
|
||||
| b == "Text.Order" -> pure (a:)
|
||||
| b == "Number.Order" -> pure (a:)
|
||||
| b == "Hash.Order" -> do Term.App' _ a <- pure a; pure (a:)
|
||||
| b == "Unit.Order" -> pure (a:)
|
||||
| b == "Order.ignore" -> pure id
|
||||
| otherwise -> fail $ "unrecognized order type: " ++ Text.unpack b
|
||||
Term.Apps' (Term.Builtin' pair) [ord1, ord2]
|
||||
| pair == "Pair.Order" -> do
|
||||
Term.Apps' _ [a,b] <- whnf a
|
||||
Term.Apps' _ [a,b] <- pure a
|
||||
(.) <$> op' ord1 a <*> op' ord2 b
|
||||
| otherwise -> fail $ "unrecognized order type: " ++ Text.unpack pair
|
||||
op [ord,a] = Term.app (Term.builtin "Order.Key")
|
||||
@ -528,7 +462,7 @@ makeBuiltins logger whnf =
|
||||
in (r, Just (I.Primop 2 op), unsafeParseType "forall a . Order a -> a -> Order.Key a", prefix "Order.key")
|
||||
]
|
||||
|
||||
extractKey :: Term V -> [Either Double Text]
|
||||
extractKey :: Var v => Term v -> [Either Double Text]
|
||||
extractKey (Term.App' _ t1) = go t1 where
|
||||
go (Term.Builtin' _) = []
|
||||
go (Term.App' (Term.Text' t) tl) = Right t : go tl
|
||||
@ -537,7 +471,7 @@ extractKey (Term.App' _ t1) = go t1 where
|
||||
go _ = error $ "don't know what to do with this in extractKey: " ++ show t1
|
||||
extractKey t = error $ "not a key: " ++ show t
|
||||
|
||||
compareKeys :: Term V -> Term V -> Ordering
|
||||
compareKeys :: Term v -> Term v -> Ordering
|
||||
compareKeys (Term.App' _ t1) (Term.App' _ t2) = go t1 t2 where
|
||||
go (Term.Builtin' u) (Term.Builtin' u2) = u `compare` u2
|
||||
go (Term.App' h1 t1) (Term.App' h2 t2) =
|
||||
@ -555,16 +489,6 @@ compareKeys (Term.App' _ t1) (Term.App' _ t2) = go t1 t2 where
|
||||
compareKeys _ _ = error "not a key"
|
||||
|
||||
-- type helpers
|
||||
alignmentT :: Ord v => Type v
|
||||
alignmentT = Type.ref (R.Builtin "Alignment")
|
||||
numOpTyp :: Type V
|
||||
numOpTyp = unsafeParseType "Number -> Number -> Number"
|
||||
numCompareTyp :: Type V
|
||||
numCompareTyp = unsafeParseType "Number -> Number -> Boolean"
|
||||
textCompareTyp :: Type V
|
||||
textCompareTyp = unsafeParseType "Text -> Text -> Boolean"
|
||||
strOpTyp :: Type V
|
||||
strOpTyp = unsafeParseType "Text -> Text -> Text"
|
||||
unitT :: Ord v => Type v
|
||||
unitT = Type.ref (R.Builtin "Unit")
|
||||
|
||||
@ -573,16 +497,15 @@ infixr 7 -->
|
||||
(-->) = Type.arrow
|
||||
|
||||
-- term helpers
|
||||
none :: Term V
|
||||
none :: Var v => Term v
|
||||
none = Term.ref $ R.Builtin "Optional.None"
|
||||
some :: Term V -> Term V
|
||||
some :: Var v => Term v -> Term v
|
||||
some t = Term.ref (R.Builtin "Optional.Some") `Term.app` t
|
||||
left :: Term V -> Term V
|
||||
left :: Var v => Term v -> Term v
|
||||
left t = Term.ref (R.Builtin "Either.Left") `Term.app` t
|
||||
right :: Term V -> Term V
|
||||
right :: Var v => Term v -> Term v
|
||||
right t = Term.ref (R.Builtin "Either.Right") `Term.app` t
|
||||
|
||||
|
||||
-- metadata helpers
|
||||
opl :: Int -> Text -> Metadata V h
|
||||
opl p s =
|
||||
@ -602,10 +525,10 @@ assoc p s =
|
||||
in
|
||||
Metadata Metadata.Term (Metadata.Names [s']) Nothing
|
||||
|
||||
prefix :: Text -> Metadata V h
|
||||
prefix :: Var v => Text -> Metadata v h
|
||||
prefix s = prefixes [s]
|
||||
|
||||
prefixes :: [Text] -> Metadata V h
|
||||
prefixes :: Var v => [Text] -> Metadata v h
|
||||
prefixes s = Metadata Metadata.Term
|
||||
(Metadata.Names (map Var.named s))
|
||||
Nothing
|
@ -1,7 +1,7 @@
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Unison.Node where
|
||||
module Unison.Codebase where
|
||||
|
||||
-- import Data.Bytes.Serial (Serial)
|
||||
import Control.Monad
|
||||
@ -11,9 +11,9 @@ import Data.List
|
||||
import Data.Map (Map)
|
||||
import Data.Ord
|
||||
import Data.Set (Set)
|
||||
import Unison.Eval as Eval
|
||||
import Unison.Builtin (Builtin(..))
|
||||
import Unison.Codebase.Store (Store)
|
||||
import Unison.Metadata (Metadata)
|
||||
import Unison.Node.Store (Store)
|
||||
import Unison.Note (Noted(..),Note(..))
|
||||
import Unison.Paths (Path)
|
||||
import Unison.Reference (Reference)
|
||||
@ -23,10 +23,12 @@ import Unison.Type (Type)
|
||||
import Unison.Var (Var)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Unison.Codebase.Store as Store
|
||||
import qualified Unison.Interpreter as Interpreter
|
||||
import qualified Unison.Metadata as Metadata
|
||||
import qualified Unison.Node.Store as Store
|
||||
import qualified Unison.Parsers as Parsers
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Parser as Parser
|
||||
import qualified Unison.Parsers as Parsers
|
||||
import qualified Unison.Paths as Paths
|
||||
import qualified Unison.Reference as Reference
|
||||
import qualified Unison.Term as Term
|
||||
@ -69,7 +71,7 @@ deriveJSON defaultOptions ''LocalInfo
|
||||
-- * `h` is the type of hashes
|
||||
-- * `t` is for type
|
||||
-- * `e` is for term (mnemonic "expression")
|
||||
data Node m v h t e = Node {
|
||||
data Codebase m v h t e = Codebase {
|
||||
-- | Obtain the type of the given subterm, assuming the path is valid
|
||||
admissibleTypeAt :: e -> Path -> Noted m t,
|
||||
-- | Create a new term and provide its metadata
|
||||
@ -84,8 +86,6 @@ data Node m v h t e = Node {
|
||||
-- Second argument is path relative to the root.
|
||||
-- Returns (root path, original e, edited e, new cursor position)
|
||||
editTerm :: Path -> Path -> Action v -> e -> Noted m (Maybe (Path,e,e,Path)),
|
||||
-- Evaluate all terms, returning a list of (path, original e, evaluated e)
|
||||
evaluateTerms :: [(Path, e)] -> Noted m [(Path,e,e)],
|
||||
-- | Return information about local types and and variables in scope
|
||||
localInfo :: e -> Path -> Noted m (LocalInfo e t),
|
||||
-- | Access the metadata for the term and/or types identified by @k@
|
||||
@ -106,12 +106,21 @@ data Node m v h t e = Node {
|
||||
updateMetadata :: h -> Metadata v h -> Noted m ()
|
||||
}
|
||||
|
||||
node :: (Show v, Monad f, Var v)
|
||||
=> Eval (Noted f) v
|
||||
-> (Term v -> Reference)
|
||||
addBuiltins :: Monad f
|
||||
=> [Builtin v]
|
||||
-> Store f v
|
||||
-> Node f v Reference.Reference (Type v) (Term v)
|
||||
node eval hash store =
|
||||
-> Codebase f v Reference.Reference (Type v) (Term v)
|
||||
-> f ()
|
||||
addBuiltins builtins store code = Note.run $
|
||||
forM_ builtins $ \(Builtin r _ t md) -> do
|
||||
updateMetadata code r md
|
||||
Store.annotateTerm store r t
|
||||
|
||||
make :: (Show v, Monad f, Var v)
|
||||
=> (Term v -> Reference)
|
||||
-> Store f v
|
||||
-> Codebase f v Reference.Reference (Type v) (Term v)
|
||||
make hash store =
|
||||
let
|
||||
readTypeOf = Store.typeOfTerm store
|
||||
|
||||
@ -145,14 +154,10 @@ node eval hash store =
|
||||
(Set.toList hs)
|
||||
pure $ Set.fromList [x | (x,deps) <- hs', Set.member h deps]
|
||||
|
||||
edit rootPath path action e = case Paths.atTerm rootPath e of
|
||||
Nothing -> pure Nothing
|
||||
Just e -> f <$> TermEdit.interpret eval (Store.readTerm store) path action e
|
||||
where f Nothing = Nothing
|
||||
f (Just (newPath,e')) = Just (rootPath,e,e',newPath)
|
||||
|
||||
evaluateTerms es = traverse go es
|
||||
where go (path,e) = (\e' -> (path,e,e')) <$> Eval.whnf eval (Store.readTerm store) e
|
||||
edit rootPath path action e = pure $ do
|
||||
e <- Paths.atTerm rootPath e
|
||||
(newPath, e') <- TermEdit.interpret path action e
|
||||
pure (rootPath, e, e', newPath)
|
||||
|
||||
metadatas hs =
|
||||
Map.fromList <$> sequence (map (\h -> (,) h <$> Store.readMetadata store h) hs)
|
||||
@ -224,14 +229,13 @@ node eval hash store =
|
||||
Typechecker.typeAt readTypeOf loc ctx
|
||||
|
||||
updateMetadata = Store.writeMetadata store
|
||||
in Node
|
||||
in Codebase
|
||||
admissibleTypeAt
|
||||
createTerm
|
||||
createType
|
||||
dependencies
|
||||
dependents
|
||||
edit
|
||||
evaluateTerms
|
||||
localInfo
|
||||
metadatas
|
||||
search
|
||||
@ -242,13 +246,12 @@ node eval hash store =
|
||||
typeAt
|
||||
updateMetadata
|
||||
|
||||
|
||||
-- | Declare a group of bindings and add them to the Node.
|
||||
-- | Declare a group of bindings and add them to the codebase.
|
||||
-- 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 ()
|
||||
-- existing metadata store of the codebase.
|
||||
declare :: (Monad m, Var v) => (h -> Term v) -> [(v, Term v)] -> Codebase m v h (Type v) (Term v) -> Noted m ()
|
||||
declare ref bindings node = do
|
||||
termBuiltins <- allTermsByVarName ref node
|
||||
let groups = Components.components bindings
|
||||
@ -266,21 +269,30 @@ declare ref bindings node = do
|
||||
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' :: (Monad m, Var v) => (h -> Term v) -> String -> Codebase m v h (Type v) (Term v) -> Noted m ()
|
||||
declare' ref bindings node = do
|
||||
bs <- case Parser.run TermParser.moduleBindings bindings TypeParser.s0 of
|
||||
Parser.Fail err _ -> Noted (pure $ Left (Note err))
|
||||
Parser.Succeed bs _ _ -> pure bs
|
||||
declare ref bs node
|
||||
|
||||
allTermsByVarName :: (Monad m, Var v) => (h -> Term v) -> Node m v h (Type v) (Term v) -> Noted m [(v, Term v)]
|
||||
allTermsByVarName :: (Monad m, Var v) => (h -> Term v) -> Codebase m v h (Type v) (Term v) -> Noted m [(v, Term v)]
|
||||
allTermsByVarName ref node = 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 <- Metadata.allNames (Metadata.names md) ]
|
||||
|
||||
allTerms :: (Monad m, Var v) => Node m v h (Type v) (Term v) -> Noted m [(h, Term v)]
|
||||
allTerms :: (Monad m, Var v) => Codebase m v h (Type v) (Term v) -> Noted m [(h, Term v)]
|
||||
allTerms node = do
|
||||
hs <- map fst . references <$> search node Term.blank [] 100000 (Metadata.Query "") Nothing
|
||||
Map.toList <$> terms node hs
|
||||
|
||||
interpreter :: Var v
|
||||
=> [Builtin v] -> Codebase IO v Reference (Type v) (Term v)
|
||||
-> Term v -> Noted IO (Term v)
|
||||
interpreter builtins codebase =
|
||||
let env = Map.fromList [(ref, op) | Builtin ref (Just op) _ _ <- builtins ]
|
||||
resolveHash h = snd . head . Map.toList <$> terms codebase [Reference.Derived h]
|
||||
in Interpreter.make env resolveHash
|
||||
|
@ -1,11 +1,12 @@
|
||||
{-# OPTIONS_GHC -fno-warn-orphans #-}
|
||||
|
||||
module Unison.Node.MemNode where
|
||||
module Unison.Codebase.MemCodebase where
|
||||
|
||||
import Data.List
|
||||
import Unison.Codebase (Codebase)
|
||||
import Unison.Codebase.Store (Store)
|
||||
import Unison.Note (Noted)
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Node (Node)
|
||||
import Unison.Node.Store (Store)
|
||||
import Unison.Reference (Reference(Derived))
|
||||
import Unison.Term (Term)
|
||||
import Unison.Type (Type)
|
||||
@ -17,11 +18,11 @@ import qualified Data.Digest.Murmur64 as Murmur
|
||||
import qualified Data.Text as Text
|
||||
import qualified Data.Text.Encoding as Encoding
|
||||
import qualified Unison.ABT as ABT
|
||||
import qualified Unison.Builtin as Builtin
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Codebase.MemStore as MemStore
|
||||
import qualified Unison.Hash as Hash
|
||||
import qualified Unison.Hashable as Hashable
|
||||
import qualified Unison.Node.BasicNode as BasicNode
|
||||
import qualified Unison.Node.Builtin as Builtin
|
||||
import qualified Unison.Node.MemStore as MemStore
|
||||
import qualified Unison.Symbol as Symbol
|
||||
import qualified Unison.Term as Term
|
||||
import qualified Unison.View as View
|
||||
@ -45,7 +46,11 @@ instance Hashable.Accumulate Hash where
|
||||
|
||||
type V = Symbol.Symbol View.DFO
|
||||
|
||||
make :: Logger -> IO (Node IO V Reference (Type V) (Term V))
|
||||
make :: (Show v, Var v) => Logger
|
||||
-> IO (Codebase IO v Reference (Type v) (Term v), Term v -> Noted IO (Term v))
|
||||
make logger = do
|
||||
store <- MemStore.make :: IO (Store IO V)
|
||||
BasicNode.make hash store (Builtin.makeBuiltins logger)
|
||||
store <- MemStore.make :: IO (Store IO v)
|
||||
code <- pure $ Codebase.make hash store
|
||||
let builtins = Builtin.makeBuiltins logger
|
||||
Codebase.addBuiltins builtins store code
|
||||
pure (code, Codebase.interpreter builtins code)
|
@ -1,11 +1,11 @@
|
||||
module Unison.Node.MemStore (make) where
|
||||
module Unison.Codebase.MemStore (make) where
|
||||
|
||||
import Data.Functor
|
||||
import Data.Map (Map)
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Metadata (Metadata)
|
||||
import Unison.Note (Noted)
|
||||
import Unison.Node.Store (Store(Store))
|
||||
import Unison.Codebase.Store (Store(Store))
|
||||
import Unison.Reference (Reference)
|
||||
import Unison.Term (Term)
|
||||
import Unison.Type (Type)
|
@ -1,4 +1,4 @@
|
||||
module Unison.Node.Store where
|
||||
module Unison.Codebase.Store where
|
||||
|
||||
import Data.Set (Set)
|
||||
import Unison.Metadata (Metadata)
|
@ -1,9 +0,0 @@
|
||||
module Unison.Eval where
|
||||
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Term (Term)
|
||||
|
||||
data Eval m v = Eval {
|
||||
whnf :: (Hash -> m (Term v)) -> Term v -> m (Term v), -- ^ Simplify to weak head normal form
|
||||
step :: (Hash -> m (Term v)) -> Term v -> m (Term v) -- ^ Perform one beta reduction
|
||||
}
|
@ -3,12 +3,12 @@
|
||||
{-# LANGUAGE BangPatterns #-}
|
||||
|
||||
-- | Very simple and inefficient interpreter of Unison terms
|
||||
module Unison.Eval.Interpreter where
|
||||
module Unison.Interpreter where
|
||||
|
||||
import Data.Map (Map)
|
||||
import Data.List
|
||||
import Data.Map (Map)
|
||||
import Debug.Trace
|
||||
import Unison.Eval
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Term (Term)
|
||||
import Unison.Var (Var)
|
||||
import qualified Data.Map as M
|
||||
@ -25,23 +25,25 @@ watch :: Show a => String -> a -> a
|
||||
watch msg a = trace (msg ++ ": " ++ show a) a
|
||||
|
||||
-- | Produce an evaluator from a environment of 'Primop' values
|
||||
eval :: forall f v . (Monad f, Var v) => Map R.Reference (Primop f v) -> Eval f v
|
||||
eval env = Eval whnf step
|
||||
make :: forall f v . (Monad f, Var v) => Map R.Reference (Primop f v)
|
||||
-> (Hash -> f (Term v))
|
||||
-> Term v -> f (Term v)
|
||||
make env = nf
|
||||
where
|
||||
-- reduce x args | trace ("reduce:" ++ show (x:args)) False = undefined
|
||||
reduce resolveRef (E.Ann' e _) args = reduce resolveRef e args
|
||||
reduce resolveRef (E.App' f x) args = do
|
||||
x <- whnf resolveRef x
|
||||
x <- nf resolveRef x
|
||||
reduce resolveRef f (x:args)
|
||||
reduce resolveRef (E.Let1' binding body) xs = do
|
||||
binding <- whnf resolveRef binding
|
||||
binding <- nf resolveRef binding
|
||||
reduce resolveRef (ABT.bind body binding) xs
|
||||
reduce resolveRef f args = do
|
||||
f <- whnf resolveRef f
|
||||
f <- nf resolveRef f
|
||||
case f of
|
||||
E.If' -> case take 3 args of
|
||||
[cond,t,f] -> do
|
||||
cond <- whnf resolveRef cond
|
||||
cond <- nf resolveRef cond
|
||||
case cond of
|
||||
E.Builtin' c | Text.head c == 'F' -> pure . Just $ foldl E.app f (drop 3 args)
|
||||
| otherwise -> pure . Just $ foldl E.app t (drop 3 args)
|
||||
@ -51,9 +53,9 @@ eval env = Eval whnf step
|
||||
Nothing -> case h of
|
||||
R.Derived h -> do
|
||||
r <- resolveRef h
|
||||
r <- whnf resolveRef r
|
||||
r <- nf resolveRef r
|
||||
reduce resolveRef r args
|
||||
R.Builtin b -> pure Nothing
|
||||
R.Builtin _ -> pure Nothing
|
||||
Just op | length args >= arity op ->
|
||||
call op (take (arity op) args) >>= \e ->
|
||||
pure . Just $ foldl E.app e (drop (arity op) args)
|
||||
@ -64,49 +66,33 @@ eval env = Eval whnf step
|
||||
| otherwise -> pure Nothing
|
||||
_ -> pure Nothing
|
||||
|
||||
step resolveRef e = case e of
|
||||
E.Ann' e _ -> step resolveRef e
|
||||
E.Ref' h -> case M.lookup h env of
|
||||
Just op | arity op == 0 -> call op []
|
||||
_ -> pure e
|
||||
E.Apps' f xs -> do
|
||||
e' <- reduce resolveRef f xs
|
||||
maybe (pure e) pure e'
|
||||
E.Let1' binding body -> step resolveRef (ABT.bind body binding)
|
||||
E.LetRecNamed' bs body -> step resolveRef (ABT.substs substs body) where
|
||||
expandBinding v (E.LamNamed' name body) = E.lam name (expandBinding v body)
|
||||
expandBinding v body = ABT.substs substs' body
|
||||
where substs' = [ (v', ABT.subst v (E.letRec bs (E.var v)) b) | (v',b) <- bs ]
|
||||
substs = [ (v, expandBinding v b) | (v,b) <- bs ]
|
||||
_ -> pure e
|
||||
|
||||
whnf resolveRef e = case e of
|
||||
nf resolveRef e = case e of
|
||||
E.Ref' h -> case M.lookup h env of
|
||||
Just op | arity op == 0 -> call op []
|
||||
| otherwise -> pure e
|
||||
Nothing -> case h of
|
||||
R.Derived h -> do
|
||||
r <- resolveRef h
|
||||
whnf resolveRef r
|
||||
R.Builtin b -> pure e
|
||||
E.Ann' e _ -> whnf resolveRef e
|
||||
nf resolveRef r
|
||||
R.Builtin _ -> pure e
|
||||
E.Ann' e _ -> nf resolveRef e
|
||||
E.Apps' E.If' (cond:t:f:tl) -> do
|
||||
cond <- whnf resolveRef cond
|
||||
cond <- nf resolveRef cond
|
||||
case cond of
|
||||
E.Builtin' b | Text.head b == 'F' -> whnf resolveRef f >>= \f -> (`E.apps` tl) <$> whnf resolveRef f
|
||||
| otherwise -> whnf resolveRef t >>= \t -> (`E.apps` tl) <$> whnf resolveRef t
|
||||
E.Builtin' b | Text.head b == 'F' -> nf resolveRef f >>= \f -> (`E.apps` tl) <$> nf resolveRef f
|
||||
| otherwise -> nf resolveRef t >>= \t -> (`E.apps` tl) <$> nf resolveRef t
|
||||
_ -> pure e
|
||||
E.Apps' f xs -> do
|
||||
xs <- traverse (whnf resolveRef) xs
|
||||
f <- whnf resolveRef f
|
||||
xs <- traverse (nf resolveRef) xs
|
||||
f <- nf resolveRef f
|
||||
e' <- reduce resolveRef f xs
|
||||
maybe (pure $ f `E.apps` xs) (whnf resolveRef) e'
|
||||
maybe (pure $ f `E.apps` xs) (nf resolveRef) e'
|
||||
E.Let1' binding body -> do
|
||||
binding <- whnf resolveRef binding
|
||||
whnf resolveRef (ABT.bind body binding)
|
||||
E.LetRecNamed' bs body -> whnf resolveRef (ABT.substs bs' body) where
|
||||
binding <- nf resolveRef binding
|
||||
nf resolveRef (ABT.bind body binding)
|
||||
E.LetRecNamed' bs body -> nf resolveRef (ABT.substs bs' body) where
|
||||
bs' = [ (v, expandBinding v b) | (v,b) <- bs ]
|
||||
expandBinding v (E.LamNamed' name body) = E.lam name (expandBinding v body)
|
||||
expandBinding v body = E.letRec bs body
|
||||
E.Vector' es -> E.vector' <$> traverse (whnf resolveRef) es
|
||||
E.Vector' es -> E.vector' <$> traverse (nf resolveRef) es
|
||||
_ -> pure e
|
@ -1,42 +0,0 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module Unison.Node.BasicNode where
|
||||
|
||||
import Unison.Node (Node)
|
||||
import Unison.Node.Store (Store)
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Term (Term)
|
||||
import Unison.Type (Type)
|
||||
import qualified Data.Map as M
|
||||
import qualified Unison.Eval as Eval
|
||||
import qualified Unison.Eval.Interpreter as I
|
||||
import qualified Unison.Node as Node
|
||||
import qualified Unison.Node.Builtin as B
|
||||
import qualified Unison.Node.Store as Store
|
||||
import qualified Unison.Note as N
|
||||
import qualified Unison.Reference as R
|
||||
import qualified Unison.Type as Type
|
||||
import qualified Unison.View as View
|
||||
|
||||
infixr 7 -->
|
||||
(-->) :: Ord v => Type v -> Type v -> Type v
|
||||
(-->) = Type.arrow
|
||||
|
||||
type DFO = View.DFO
|
||||
type V = Symbol DFO
|
||||
|
||||
make :: (Term V -> R.Reference)
|
||||
-> Store IO V
|
||||
-> (B.WHNFEval -> [B.Builtin])
|
||||
-> IO (Node IO V R.Reference (Type V) (Term V))
|
||||
make hash store getBuiltins =
|
||||
let
|
||||
builtins = getBuiltins whnf
|
||||
eval = I.eval (M.fromList [ (k,v) | (B.Builtin k (Just v) _ _) <- builtins ])
|
||||
readTerm h = Store.readTerm store h
|
||||
whnf = Eval.whnf eval readTerm
|
||||
node = Node.node eval hash store
|
||||
in N.run $ do
|
||||
mapM_ (\(B.Builtin r _ t md) -> Node.updateMetadata node r md *> Store.annotateTerm store r t)
|
||||
builtins
|
||||
pure node
|
@ -4,12 +4,10 @@ module Unison.Parsers where
|
||||
|
||||
import Control.Arrow ((***))
|
||||
import Data.Text (Text)
|
||||
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
|
||||
import qualified Unison.ABT as ABT
|
||||
@ -20,19 +18,18 @@ import qualified Unison.Type as Type
|
||||
import qualified Unison.Reference as R
|
||||
import qualified Unison.Var as Var
|
||||
|
||||
type V = Symbol DFO
|
||||
type S = TypeParser.S V
|
||||
type S v = TypeParser.S v
|
||||
|
||||
s0 :: S
|
||||
s0 :: S v
|
||||
s0 = TypeParser.s0
|
||||
|
||||
parseTerm :: String -> Result S (Term V)
|
||||
parseTerm :: Var v => String -> Result (S v) (Term v)
|
||||
parseTerm = parseTerm' termBuiltins typeBuiltins
|
||||
|
||||
parseType :: String -> Result S (Type V)
|
||||
parseType :: Var v => String -> Result (S v) (Type v)
|
||||
parseType = parseType' typeBuiltins
|
||||
|
||||
parseTerm' :: [(V, Term V)] -> [(V, Type V)] -> String -> Result S (Term V)
|
||||
parseTerm' :: Var v => [(v, Term v)] -> [(v, Type v)] -> String -> Result (S v) (Term v)
|
||||
parseTerm' termBuiltins typeBuiltins s =
|
||||
bindBuiltins termBuiltins typeBuiltins <$> run (Parser.root TermParser.term) s s0
|
||||
|
||||
@ -40,20 +37,20 @@ 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 S (Type V)
|
||||
parseType' :: Var v => [(v, Type v)] -> String -> Result (S v) (Type v)
|
||||
parseType' typeBuiltins s =
|
||||
ABT.substs typeBuiltins <$> run (Parser.root TypeParser.type_) s s0
|
||||
|
||||
unsafeParseTerm :: String -> Term V
|
||||
unsafeParseTerm :: Var v => String -> Term v
|
||||
unsafeParseTerm = unsafeGetSucceed . parseTerm
|
||||
|
||||
unsafeParseType :: String -> Type V
|
||||
unsafeParseType :: Var v => String -> Type v
|
||||
unsafeParseType = unsafeGetSucceed . parseType
|
||||
|
||||
unsafeParseTerm' :: [(V, Term V)] -> [(V, Type V)] -> String -> Term V
|
||||
unsafeParseTerm' :: Var v => [(v, Term v)] -> [(v, Type v)] -> String -> Term v
|
||||
unsafeParseTerm' er tr = unsafeGetSucceed . parseTerm' er tr
|
||||
|
||||
unsafeParseType' :: [(V, Type V)] -> String -> Type V
|
||||
unsafeParseType' :: Var v => [(v, Type v)] -> String -> Type v
|
||||
unsafeParseType' tr = unsafeGetSucceed . parseType' tr
|
||||
|
||||
-- Alias <alias> <fully-qualified-name>
|
||||
|
@ -7,16 +7,12 @@ module Unison.TermEdit where
|
||||
|
||||
import Data.Aeson.TH
|
||||
import GHC.Generics
|
||||
import Unison.Eval (Eval)
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Term (Term)
|
||||
import Unison.Type (Type)
|
||||
import Unison.Note (Noted)
|
||||
import Unison.Var (Var)
|
||||
import Unison.Paths (Path)
|
||||
-- import qualified Data.Set as Set
|
||||
-- import qualified Unison.ABT as ABT
|
||||
-- import qualified Unison.Eval as Eval
|
||||
import qualified Unison.Term as Term
|
||||
import qualified Unison.Type as Type
|
||||
|
||||
@ -30,20 +26,16 @@ data Action v
|
||||
| MergeLet -- Merge a let block into its parent let block
|
||||
| Noop -- Do nothing to the target
|
||||
| Rename v -- Rename the target var
|
||||
| Step -- Link + beta reduce the target
|
||||
| BetaReduce -- beta reduce the target
|
||||
| SwapDown -- Swap the target let binding with the subsequent binding
|
||||
| SwapUp -- Swap the target let binding with the previous binding
|
||||
| WHNF -- Simplify target to weak head normal form
|
||||
deriving Generic
|
||||
|
||||
-- | Interpret the given 'Action', returning the new path and the replacement
|
||||
-- term at that path (the new path may not be equal to the path passed in, though
|
||||
-- it will be related to it in some way that depends on the action).
|
||||
interpret :: (Applicative f, Monad f, Var v)
|
||||
=> Eval (Noted f) v
|
||||
-> (Hash -> Noted f (Term v))
|
||||
-> Path -> Action v -> Term v -> Noted f (Maybe (Path, Term v))
|
||||
interpret _ _ _ _ _ =
|
||||
interpret :: Var v => Path -> Action v -> Term v -> Maybe (Path, Term v)
|
||||
interpret _ _ _ =
|
||||
error "todo - interpret"
|
||||
-- interpret eval link path action t =
|
||||
--case action of
|
||||
|
@ -6,46 +6,51 @@ import Control.Monad.IO.Class
|
||||
import Data.Foldable
|
||||
import Data.Text.Encoding (decodeUtf8)
|
||||
import System.IO (FilePath)
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Node (Node)
|
||||
import Unison.Codebase (Codebase)
|
||||
import Unison.Note (Noted)
|
||||
import Unison.Reference (Reference)
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Term (Term)
|
||||
import Unison.Type (Type)
|
||||
import Unison.Views (defaultSymbol)
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Text.IO as Text.IO
|
||||
import qualified Data.Text as Text
|
||||
import qualified Data.Text.IO as Text.IO
|
||||
import qualified System.FilePath as FP
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Codebase.MemCodebase as MemCodebase
|
||||
import qualified Unison.Metadata as Metadata
|
||||
import qualified Unison.Node as Node
|
||||
import qualified Unison.Node.MemNode as MemNode
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Term as Term
|
||||
import qualified Unison.View as View
|
||||
import qualified Unison.Util.Logger as L
|
||||
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, [(V, Term V)])
|
||||
-- A codebase for testing
|
||||
type TCodebase =
|
||||
( Codebase IO V Reference (Type V) (Term V) -- the codebase
|
||||
, Reference -> V -- resolve references to symbols
|
||||
, [(V, Term V)] -- all symbol bindings
|
||||
, Term V -> Noted IO (Term V)) -- evaluator
|
||||
|
||||
loadDeclarations :: FilePath -> Node IO V Reference (Type V) (Term V) -> IO ()
|
||||
loadDeclarations path node = do
|
||||
loadDeclarations :: FilePath -> Codebase IO V Reference (Type V) (Term V) -> IO ()
|
||||
loadDeclarations path codebase = do
|
||||
-- note - when run from repl current directory is root, but when run via stack test, current
|
||||
-- directory is the shared subdir - so we check both locations
|
||||
txt <- decodeUtf8 <$> (B.readFile path <|> B.readFile (".." `FP.combine` path))
|
||||
let str = Text.unpack txt
|
||||
_ <- Note.run $ Node.declare' Term.ref str node
|
||||
_ <- Note.run $ Codebase.declare' Term.ref str codebase
|
||||
putStrLn $ "loaded file: " ++ path
|
||||
|
||||
node :: IO TNode
|
||||
node = do
|
||||
codebase :: IO TCodebase
|
||||
codebase = do
|
||||
logger <- L.atomic (L.atInfo L.toStandardOut)
|
||||
node <- MemNode.make logger
|
||||
loadDeclarations "unison-src/base.u" node
|
||||
(codebase, eval) <- MemCodebase.make logger
|
||||
loadDeclarations "unison-src/base.u" codebase
|
||||
symbols <- liftIO . Note.run $
|
||||
Map.fromList . Node.references <$> Node.search node Term.blank [] 1000 (Metadata.Query "") Nothing
|
||||
base <- Note.run $ Node.allTermsByVarName Term.ref node
|
||||
Map.fromList . Codebase.references <$> Codebase.search codebase Term.blank [] 1000 (Metadata.Query "") Nothing
|
||||
base <- Note.run $ Codebase.allTermsByVarName Term.ref codebase
|
||||
let firstName (Metadata.Names (n:_)) = n
|
||||
let lookupSymbol ref = maybe (defaultSymbol ref) (firstName . Metadata.names) (Map.lookup ref symbols)
|
||||
pure (node, lookupSymbol, base)
|
||||
pure (codebase, lookupSymbol, base, eval)
|
||||
|
@ -3,12 +3,13 @@ module Unison.Test.Interpreter where
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import qualified Unison.Parsers as P
|
||||
import qualified Unison.Node as Node
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Interpreter as I
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.node (\_ -> pure ()) $ \node ->
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
|
||||
let
|
||||
tests =
|
||||
[ t "1 + 1" "2"
|
||||
@ -91,11 +92,11 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
|
||||
, t "Vector.drop 2 [1,2,3]" "[3]"
|
||||
]
|
||||
t uneval eval = testCase (uneval ++ " ⟹ " ++ eval) $ do
|
||||
(node, _, builtins) <- node
|
||||
(codebase, _, builtins, evaluate) <- codebase
|
||||
-- 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)]
|
||||
_ <- Note.run $ Codebase.typeAt codebase term []
|
||||
result <- Note.run $ evaluate term
|
||||
assertEqual "comparing results" (P.unsafeParseTerm eval) result
|
||||
in testGroup "Interpreter" tests
|
||||
|
||||
|
@ -6,7 +6,7 @@ module Unison.Test.Term where
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Unison.Hash (Hash)
|
||||
import Unison.Node.MemNode ()
|
||||
import Unison.Codebase.MemCodebase ()
|
||||
import Unison.Parsers (unsafeParseTerm)
|
||||
import Unison.Reference as R
|
||||
import Unison.Symbol (Symbol)
|
||||
@ -31,8 +31,8 @@ type TTerm = Term (Symbol DFO)
|
||||
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 :: Bool -> Common.TCodebase -> [(Int,Int)] -> TTerm -> [(Paths.Path, Region)]
|
||||
atPts print (_,symbol,_,_) pts t = map go pts where
|
||||
go (x,y) = let p = path x y in (p, Doc.region bounds p)
|
||||
doc = Views.term symbol t
|
||||
layout = Doc.layout Doc.textWidth (Width 80) doc
|
||||
@ -43,40 +43,43 @@ atPts print (_,symbol,_) pts t = map go pts where
|
||||
main :: IO ()
|
||||
main = defaultMain tests
|
||||
|
||||
unsafeParseTerm' :: String -> TTerm
|
||||
unsafeParseTerm' = unsafeParseTerm
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Term"
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \codebase -> testGroup "Term"
|
||||
[ testCase "alpha equivalence (term)" $ assertEqual "identity"
|
||||
(unsafeParseTerm "a -> a")
|
||||
(unsafeParseTerm "x -> x")
|
||||
(unsafeParseTerm' "a -> a")
|
||||
(unsafeParseTerm' "x -> x")
|
||||
, testCase "hash cycles" $ assertEqual "pingpong"
|
||||
(hash pingpong1)
|
||||
(hash pingpong2)
|
||||
-- , testCase "infix-rendering (1)" $ node >>= \(_,symbol,_) ->
|
||||
-- , testCase "infix-rendering (1)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus 1 1"
|
||||
-- in assertEqual "+"
|
||||
-- "1 + 1"
|
||||
-- (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (unsaturated)" $ node >>= \(_,symbol,_) ->
|
||||
-- , testCase "infix-rendering (unsaturated)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus _"
|
||||
-- in assertEqual "+"
|
||||
-- "(+) _"
|
||||
-- (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (totally unsaturated)" $ node >>= \(_,symbol,_) ->
|
||||
-- , testCase "infix-rendering (totally unsaturated)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- let t = unsafeParseTerm "Number.plus"
|
||||
-- in assertEqual "+" "(+)" (Doc.formatText (Width 80) (Views.term symbol t))
|
||||
-- , testCase "infix-rendering (2)" $ node >>= \(_,symbol,_) ->
|
||||
-- , testCase "infix-rendering (2)" $ codebase >>= \(_,symbol,_) ->
|
||||
-- do
|
||||
-- t <- pure $ unsafeParseTerm "Number.plus 1 1"
|
||||
-- let d = Views.term symbol t
|
||||
-- assertEqual "path sanity check"
|
||||
-- [Paths.Fn,Paths.Arg]
|
||||
-- (head $ Doc.leafPaths d)
|
||||
-- , testCase "let-rendering (1)" $ node >>= \node ->
|
||||
-- , testCase "let-rendering (1)" $ codebase >>= \codebase ->
|
||||
-- do
|
||||
-- -- let xy = 4223 in 42
|
||||
-- t <- pure $ unsafeParseTerm "let xy = 4223 in 42"
|
||||
-- [(p1,r1), (p2,_), (p3,r3), (p4,_), (p5,r5), (p6,r6)] <- pure $
|
||||
-- atPts False node [(0,0), (1,0), (10,0), (11,0), (5,0), (8,0)] t
|
||||
-- atPts False codebase [(0,0), (1,0), (10,0), (11,0), (5,0), (8,0)] t
|
||||
-- assertEqual "p1" [] p1
|
||||
-- assertEqual "p2" [] p2
|
||||
-- assertEqual "r1" (rect 0 0 19 1) r1
|
||||
@ -87,17 +90,17 @@ tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Term"
|
||||
-- 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 ->
|
||||
-- , testCase "map lambda rendering" $ codebase >>= \codebase ->
|
||||
-- do
|
||||
-- -- map (x -> _) [1,2,3]
|
||||
-- t <- pure $ builtin "Vector.map" `app` lam' ["x"] blank `app` vector (map num [1,2,3])
|
||||
-- [(p1,r1)] <- pure $ atPts False node [(5,0)] t
|
||||
-- [(p1,r1)] <- pure $ atPts False codebase [(5,0)] t
|
||||
-- assertEqual "p1" [Paths.Fn, Paths.Arg] p1
|
||||
-- assertEqual "r1" (rect 4 0 8 1) r1
|
||||
-- , testCase "operator chain rendering" $ node >>= \node ->
|
||||
-- , testCase "operator chain rendering" $ codebase >>= \codebase ->
|
||||
-- do
|
||||
-- t <- pure $ unsafeParseTerm "1 + 2 + 3"
|
||||
-- [(p1,r1),(p2,_)] <- pure $ atPts False node [(1,0), (2,0)] t
|
||||
-- [(p1,r1),(p2,_)] <- pure $ atPts False codebase [(1,0), (2,0)] t
|
||||
-- assertEqual "p1" [Paths.Fn, Paths.Arg, Paths.Fn, Paths.Arg] p1
|
||||
-- assertEqual "r1" (rect 0 0 1 1) r1
|
||||
-- assertEqual "p2" [] p2
|
||||
|
@ -1,4 +1,6 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE PartialTypeSignatures #-}
|
||||
|
||||
module Unison.Test.TermParser where
|
||||
|
||||
import Data.List
|
||||
@ -18,7 +20,7 @@ import qualified Unison.Type as T
|
||||
|
||||
parse' :: String -> TestTree
|
||||
parse' s = testCase ("`" ++ s ++ "`") $
|
||||
case parseTerm s of
|
||||
case parseTerm s :: Result _ (Term (Symbol DFO)) of
|
||||
Fail e _ -> assertFailure $ "parse failure " ++ intercalate "\n" e
|
||||
Succeed a _ _ -> pure ()
|
||||
|
||||
@ -32,7 +34,7 @@ parse (s, expected) =
|
||||
parseFail :: (String,String) -> TestTree
|
||||
parseFail (s, reason) =
|
||||
testCase ("`" ++ s ++ "` shouldn't parse: " ++ reason) $ assertBool "should not have parsed" $
|
||||
case parseTerm s of
|
||||
case parseTerm s :: Result _ (Term (Symbol DFO)) of
|
||||
Fail {} -> True;
|
||||
Succeed _ _ n -> n == length s;
|
||||
|
||||
|
@ -5,16 +5,16 @@ module Unison.Test.Typechecker where
|
||||
import Data.Functor
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Unison.Node.MemNode ()
|
||||
import Unison.Codebase.MemCodebase ()
|
||||
import Unison.Symbol (Symbol)
|
||||
import Unison.Term as E
|
||||
import Unison.Parsers (unsafeParseTerm, unsafeParseType)
|
||||
import Unison.Paths (Path)
|
||||
import Unison.Type as T
|
||||
import Unison.Typechecker as Typechecker
|
||||
import Unison.View (DFO)
|
||||
import Unison.Paths (Path)
|
||||
import qualified Unison.Node as Node
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Parsers as Parsers
|
||||
import qualified Unison.Paths as Paths
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Test.Term as Term
|
||||
@ -23,7 +23,7 @@ type V = Symbol DFO
|
||||
type TTerm = Term.TTerm
|
||||
type TType = Type V
|
||||
type TEnv f = T.Env f V
|
||||
type TNode = IO Common.TNode
|
||||
type TCodebase = IO Common.TCodebase
|
||||
|
||||
infixr 1 -->
|
||||
(-->) :: TType -> TType -> TType
|
||||
@ -33,40 +33,40 @@ data StrongEq = StrongEq TType
|
||||
instance Eq StrongEq where StrongEq t1 == StrongEq t2 = Typechecker.equals t1 t2
|
||||
instance Show StrongEq where show (StrongEq t) = show t
|
||||
|
||||
env :: TNode -> TEnv IO
|
||||
env node r = do
|
||||
(node, _, _) <- Note.lift node
|
||||
Node.typeAt node (E.ref r) mempty
|
||||
env :: TCodebase -> TEnv IO
|
||||
env codebase r = do
|
||||
(codebase, _, _, _) <- Note.lift codebase
|
||||
Codebase.typeAt codebase (E.ref r) mempty
|
||||
|
||||
localsAt :: TNode -> Path -> TTerm -> IO [(V, Type V)]
|
||||
localsAt node path e = Note.run $ do
|
||||
t2 <- Typechecker.locals (env node) path e
|
||||
localsAt :: TCodebase -> Path -> TTerm -> IO [(V, Type V)]
|
||||
localsAt codebase path e = Note.run $ do
|
||||
t2 <- Typechecker.locals (env codebase) path e
|
||||
pure t2
|
||||
|
||||
synthesizesAt :: TNode -> Path -> TTerm -> TType -> Assertion
|
||||
synthesizesAt node path e t = Note.run $ do
|
||||
(node, _, _) <- Note.lift node
|
||||
t2 <- Node.typeAt node e path
|
||||
synthesizesAt :: TCodebase -> Path -> TTerm -> TType -> Assertion
|
||||
synthesizesAt codebase path e t = Note.run $ do
|
||||
(codebase, _, _, _) <- Note.lift codebase
|
||||
t2 <- Codebase.typeAt codebase e path
|
||||
_ <- Note.fromEither (Typechecker.subtype t2 t)
|
||||
_ <- Note.fromEither (Typechecker.subtype t t2)
|
||||
pure ()
|
||||
|
||||
checksAt :: TNode -> Path -> TTerm -> TType -> Assertion
|
||||
checksAt :: TCodebase -> Path -> TTerm -> TType -> Assertion
|
||||
checksAt node path e t = Note.run . void $
|
||||
Typechecker.synthesize (env node) (Paths.modifyTerm' (\e -> E.wrapV (E.ann e t)) path e)
|
||||
|
||||
synthesizesAndChecksAt :: TNode -> Path -> TTerm -> TType -> Assertion
|
||||
synthesizesAndChecksAt :: TCodebase -> Path -> TTerm -> TType -> Assertion
|
||||
synthesizesAndChecksAt node path e t =
|
||||
synthesizesAt node path e t >> checksAt node path e t
|
||||
|
||||
synthesizes :: TNode -> TTerm -> TType -> Assertion
|
||||
synthesizes :: TCodebase -> TTerm -> TType -> Assertion
|
||||
synthesizes node e t = Note.run $ do
|
||||
t2 <- Typechecker.synthesize (env node) e
|
||||
_ <- Note.fromEither (Typechecker.subtype t2 t)
|
||||
_ <- Note.fromEither (Typechecker.subtype t t2)
|
||||
pure ()
|
||||
|
||||
checks :: TNode -> TTerm -> TType -> Assertion
|
||||
checks :: TCodebase -> TTerm -> TType -> Assertion
|
||||
checks node e t = void $ Note.run (Typechecker.check (env node) e t)
|
||||
|
||||
checkSubtype :: TType -> TType -> Assertion
|
||||
@ -74,7 +74,7 @@ checkSubtype t1 t2 = case Typechecker.subtype t1 t2 of
|
||||
Left err -> assertFailure ("subtype failure:\n" ++ show err)
|
||||
Right _ -> pure ()
|
||||
|
||||
synthesizesAndChecks :: TNode -> TTerm -> TType -> Assertion
|
||||
synthesizesAndChecks :: TCodebase -> TTerm -> TType -> Assertion
|
||||
synthesizesAndChecks node e t =
|
||||
synthesizes node e t >> checks node e t
|
||||
|
||||
@ -89,8 +89,14 @@ synthesizesAndChecks node e t =
|
||||
testTerm :: String -> (String -> TestTree) -> TestTree
|
||||
testTerm termString f = f termString
|
||||
|
||||
unsafeParseTerm :: String -> TTerm
|
||||
unsafeParseTerm = Parsers.unsafeParseTerm
|
||||
|
||||
unsafeParseType :: String -> TType
|
||||
unsafeParseType = Parsers.unsafeParseType
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.node (\_ -> pure ()) $ \node -> testGroup "Typechecker"
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \node -> testGroup "Typechecker"
|
||||
[
|
||||
testCase "alpha equivalence (type)" $ assertEqual "const"
|
||||
(unsafeParseType "forall a b. a -> b -> a")
|
||||
|
@ -3,14 +3,14 @@ module Unison.Test.Typechecker.Components where
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit
|
||||
import Unison.Parsers (unsafeParseTerm)
|
||||
import qualified Unison.Node as Node
|
||||
import qualified Unison.Codebase as Codebase
|
||||
import qualified Unison.Note as Note
|
||||
import qualified Unison.Term as Term
|
||||
import qualified Unison.Test.Common as Common
|
||||
import qualified Unison.Typechecker.Components as Components
|
||||
|
||||
tests :: TestTree
|
||||
tests = withResource Common.node (\_ -> pure ()) $ \node ->
|
||||
tests = withResource Common.codebase (\_ -> pure ()) $ \codebase ->
|
||||
let
|
||||
tests =
|
||||
[
|
||||
@ -32,10 +32,10 @@ tests = withResource Common.node (\_ -> pure ()) $ \node ->
|
||||
"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
|
||||
(codebase, _, _, _) <- codebase
|
||||
let term = unsafeParseTerm before
|
||||
let after' = Components.minimize' term
|
||||
_ <- Note.run $ Node.typeAt node after' []
|
||||
_ <- Note.run $ Codebase.typeAt codebase after' []
|
||||
assertEqual "comparing results" (unsafeParseTerm after) after'
|
||||
in testGroup "Typechecker.Components" tests
|
||||
|
||||
|
@ -35,24 +35,22 @@ library
|
||||
|
||||
exposed-modules:
|
||||
Unison.ABT
|
||||
Unison.Builtin
|
||||
Unison.BlockStore
|
||||
Unison.Cryptography
|
||||
Unison.Dimensions
|
||||
Unison.Distance
|
||||
Unison.Doc
|
||||
Unison.Eval
|
||||
Unison.Eval.Interpreter
|
||||
Unison.Hash
|
||||
Unison.Hashable
|
||||
Unison.Interpreter
|
||||
Unison.JSON
|
||||
Unison.Kind
|
||||
Unison.Metadata
|
||||
Unison.Node
|
||||
Unison.Node.BasicNode
|
||||
Unison.Node.Builtin
|
||||
Unison.Node.MemNode
|
||||
Unison.Node.MemStore
|
||||
Unison.Node.Store
|
||||
Unison.Codebase
|
||||
Unison.Codebase.MemCodebase
|
||||
Unison.Codebase.MemStore
|
||||
Unison.Codebase.Store
|
||||
Unison.Note
|
||||
Unison.Parser
|
||||
Unison.Parsers
|
||||
|
@ -87,7 +87,8 @@ Vector.all? : ∀ a . (a -> Boolean) -> Vector a -> Boolean;
|
||||
Vector.all? f vs = Vector.fold-balanced and True (Vector.map f vs);
|
||||
|
||||
Vector.sort-by : ∀ k a . Order k -> (a -> k) -> Vector a -> Vector a;
|
||||
Vector.sort-by ok f v = Vector.sort-keyed (f `and-then` Order.key ok) v;
|
||||
Vector.sort-by ok f v =
|
||||
Vector.sort-keyed <| Vector.map (a -> (Order.key ok (f a), a)) v;
|
||||
|
||||
Vector.sort : ∀ a . Order a -> Vector a -> Vector a;
|
||||
Vector.sort o = Vector.sort-by o identity;
|
||||
|
Loading…
Reference in New Issue
Block a user