Merge pull request #247 from unisonweb/topic/haskell-runtime

Merge WIP on a Haskell-based Unison runtime

parser-typechecker/src/Unison/ABT.hs

@@ -104,6 +104,23 @@ bound' t = case out t of
   Tm f -> Foldable.toList f >>= bound'
   _ -> []
 
+annotateBound' :: (Ord v, Functor f, Foldable f) => Term f v a0 -> Term f v [v]
+annotateBound' t = go [] t where
+  go env t = case out t of
+    Abs v body -> abs' env v (go (v : env) body)
+    Cycle body -> cycle' env (go env body)
+    Tm f -> tm' env (go env <$> f)
+    Var v -> annotatedVar env v
+
+-- Annotate the tree with the set of bound variables at each node.
+annotateBound :: (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v)
+annotateBound t = go Set.empty t where
+  go bound t = let a = (annotation t, bound) in case out t of
+    Var v -> annotatedVar a v
+    Cycle body -> cycle' a (go bound body)
+    Abs x body -> abs' a x (go (Set.insert x bound) body)
+    Tm body -> tm' a (go bound <$> body)
+
 -- | Return the list of all variables bound by this ABT
 bound :: (Ord v, Foldable f) => Term f v a -> Set v
 bound t = Set.fromList (bound' t)
@@ -323,15 +340,6 @@ rebuildUp' f (Term _ ann body) = case body of
   Abs x e -> f $ abs' ann x (rebuildUp' f e)
   Tm body -> f $ tm' ann (fmap (rebuildUp' f) body)
 
--- Annotate the tree with the set of bound variables at each node.
-annotateBound :: (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v)
-annotateBound t = go Set.empty t where
-  go bound t = let a = (annotation t, bound) in case out t of
-    Var v -> annotatedVar a v
-    Cycle body -> cycle' a (go bound body)
-    Abs x body -> abs' a x (go (Set.insert x bound) body)
-    Tm body -> tm' a (go bound <$> body)
-
 freeVarAnnotations :: (Traversable f, Ord v) => Term f v a -> [(v, a)]
 freeVarAnnotations t =
   join . runIdentity $ foreachSubterm f (annotateBound t) where
@@ -385,6 +393,16 @@ visitPure :: (Traversable f, Ord v)
       => (Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
 visitPure f = runIdentity . visit (fmap pure . f)
 
+rewriteDown :: (Traversable f, Ord v)
+            => (Term f v a -> Term f v a)
+            -> Term f v a
+            -> Term f v a
+rewriteDown f t = let t' = f t in case out t' of
+  Var _ -> t'
+  Cycle body -> cycle' (annotation t) (rewriteDown f body)
+  Abs x e -> abs' (annotation t) x (rewriteDown f e)
+  Tm body -> tm' (annotation t) (rewriteDown f `fmap` body)
+
 data Subst f v a =
   Subst { freshen :: forall m v' . Monad m => (v -> m v') -> m v'
         , bind :: Term f v a -> Term f v a

parser-typechecker/src/Unison/Runtime/Rt0.hs

@@ -0,0 +1,231 @@
+{-# Language OverloadedStrings #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language StrictData #-}
+{-# Language TupleSections #-}
+{-# Language UnicodeSyntax #-}
+
+module Unison.Runtime.Rt0 where
+
+import Data.Functor
+import Data.Foldable
+import Data.Int (Int64)
+import Data.Text (Text)
+import Data.Word (Word64)
+import Data.List
+import Unison.Symbol (Symbol)
+import Unison.Term (AnnotatedTerm)
+import qualified Unison.Builtin as B
+import qualified Unison.ABT as ABT
+import qualified Unison.Reference as R
+import qualified Unison.Term as Term
+
+type Arity = Int
+type ConstructorId = Int
+type Pos = Int
+type ArgCount = Int
+
+type Term v = AnnotatedTerm v ()
+
+data V
+  = I Int64 | F Double | U Word64 | B Bool | T Text
+  | Lam Arity (Either R.Reference (Term Symbol)) IR
+  | Data R.Reference ConstructorId [V]
+  | Requested Req
+  deriving (Eq,Show)
+--
+-- Contains the effect ref and ctor id, the args, and the continuation
+-- which expects the result at the top of the stack
+data Req = Req R.Reference ConstructorId [V] IR
+  deriving (Eq,Show)
+
+data IR
+  = Var Pos
+  | AddI Pos Pos | SubI Pos Pos | MultI Pos Pos | DivI Pos Pos
+  | AddU Pos Pos | SubU Pos Pos | MultU Pos Pos | DivU Pos Pos
+  | AddF Pos Pos | SubF Pos Pos | MultF Pos Pos | DivF Pos Pos
+  | Let IR IR
+  | LetRec [IR] IR
+  | V V
+  -- | Apply IR [Pos] -- fully saturated function call
+  | DynamicApply Pos [Pos] -- call to unknown function
+  | Construct R.Reference Int [Pos]
+  | Request R.Reference Int [Pos]
+  | Handle Pos IR
+  | If Pos IR IR
+  | And Pos IR
+  | Or Pos IR
+  deriving (Eq,Show)
+
+type Machine = [V] -- a stack of values
+
+push :: V -> Machine -> Machine
+push = (:)
+
+pushes :: [V] -> Machine -> Machine
+pushes s m = reverse s <> m
+
+at :: Int -> Machine -> V
+at i m = m !! i
+
+ati :: Int -> Machine -> Int64
+ati i m = case at i m of
+  I i -> i
+  _ -> error "type error"
+
+atu :: Int -> Machine -> Word64
+atu i m = case at i m of
+  U i -> i
+  _ -> error "type error"
+
+atf :: Int -> Machine -> Double
+atf i m = case at i m of
+  F i -> i
+  _ -> error "type error"
+
+atb :: Int -> Machine -> Bool
+atb i m = case at i m of
+  B b -> b
+  _ -> error "type error"
+
+att :: Int -> Machine -> Text
+att i m = case at i m of
+  T t -> t
+  _ -> error "type error"
+
+appendCont :: Req -> IR -> Req
+appendCont (Req r cid args k) k2 = Req r cid args (Let k k2)
+
+data Result = RRequest Req | RMatchFail | RDone V deriving (Show)
+
+done :: V -> Result
+done = RDone
+
+run :: (R.Reference -> V) -> IR -> Machine -> Result
+run env = go where
+  go ir m = case ir of
+    If c t f -> if atb c m then go t m else go f m
+    And i j -> case at i m of
+      b@(B False) -> done b
+      _ -> go j m
+    Or i j -> case at i m of
+      b@(B True) -> done b
+      _ -> go j m
+    Let b body -> case go b m of
+      RRequest req -> RRequest (req `appendCont` body)
+      RDone v -> go body (v : m)
+      e -> error $ show e
+    LetRec bs body ->
+      let m' = pushes bs' m
+          g (RDone a) = a
+          g e = error ("bindings in a let rec must not have effects " ++ show e)
+          bs' = map (\ir -> g $ go ir m') bs
+      in go body m'
+    -- Apply body args -> go body (map (`at` m) args `pushes` m)
+    DynamicApply fnPos args -> call (at fnPos m) args m
+    Request r cid args -> RRequest (Req r cid ((`at` m) <$> args) (Var 0))
+    Handle handler body -> case go body m of
+      RRequest req -> call (at handler m) [0] (Requested req `push` m)
+      r -> r
+    ir -> done $ case ir of
+      Var i -> at i m
+      V v -> v
+      Construct r cid args -> Data r cid ((`at` m) <$> args)
+      AddI i j -> I (ati i m + ati j m)
+      SubI i j -> I (ati i m - ati j m)
+      MultI i j -> I (ati i m * ati j m)
+      DivI i j -> I (ati i m `div` ati j m)
+      AddF i j -> F (atf i m + atf j m)
+      SubF i j -> F (atf i m - atf j m)
+      MultF i j -> F (atf i m * atf j m)
+      DivF i j -> F (atf i m / atf j m)
+      AddU i j -> U (atu i m + atu j m)
+      SubU i j -> U (atu i m - atu j m)
+      MultU i j -> U (atu i m * atu j m)
+      DivU i j -> U (atu i m `div` atu j m)
+      _ -> error "should be caught by above cases"
+
+  call :: V -> [Pos] -> Machine -> Result
+  call (Lam arity term body) args m = let nargs = length args in
+    case nargs of
+      _ | nargs == arity -> go body (map (`at` m) args `pushes` m)
+      _ | nargs > arity ->
+        case go body (map (`at` m) (take arity args) `pushes` m) of
+          RRequest req -> RRequest $ req `appendCont` error "todo"
+          RDone fn' -> call fn' (drop arity args) m
+          e -> error $ "type error, tried to apply: " ++ show e
+      -- nargs < arity
+      _ -> case term of
+        Right (Term.LamsNamed' vs body) -> done $ Lam (arity - nargs) (Right lam) (compile env lam)
+          where
+          lam = Term.lam'() (drop nargs vs) $
+            ABT.substs (vs `zip` (map decompile . reverse . take nargs $ m)) body
+        Left _builtin -> error "todo - handle partial application of builtins by forming closure"
+        _ -> error "type error"
+  call _ _ _ = error "type error"
+
+decompile :: V -> Term Symbol
+decompile v = case v of
+  I n -> Term.int64 () n
+  U n -> Term.uint64 () n
+  F n -> Term.float () n
+  B b -> Term.boolean () b
+  T t -> Term.text () t
+  Lam _ f _ -> case f of Left r -> Term.ref() r; Right f -> f
+  Data r cid args -> Term.apps' (Term.constructor() r cid) (toList $ fmap decompile args)
+  Requested (Req r cid args _) ->
+    let req = Term.apps (Term.request() r cid) (((),) . decompile <$> args)
+    in req
+
+compile :: (R.Reference -> V) -> Term Symbol -> IR
+compile env = compile0 env []
+
+compile0 :: (R.Reference -> V) -> [Symbol] -> Term Symbol -> IR
+compile0 env bound t = go ((++ bound) <$> ABT.annotateBound' (Term.anf t)) where
+  go t = case t of
+    Term.LamsNamed' vs body
+      | ABT.isClosed t -> V (Lam (length vs) (Right $ void t) (go body))
+      | otherwise -> let
+        fvs = toList $ ABT.freeVars t
+        lifted = Term.lam'() (fvs ++ vs) (void body)
+        in compile0 env (ABT.annotation t) (Term.apps' lifted (Term.var() <$> fvs))
+    Term.And' x y -> And (ind t x) (go y)
+    Term.Or' x y -> Or (ind t x) (go y)
+    Term.If' cond ifT ifF -> If (ind t cond) (go ifT) (go ifF)
+    Term.Int64' n -> V (I n)
+    Term.UInt64' n -> V (U n)
+    Term.Float' n -> V (F n)
+    Term.Boolean' b -> V (B b)
+    Term.Text' t -> V (T t)
+    Term.Ref' r -> V (env r)
+    Term.Var' v -> maybe (unknown v) Var $ elemIndex v (ABT.annotation t)
+    Term.Let1Named' _ b body -> Let (go b) (go body)
+    Term.LetRecNamed' bs body -> LetRec (go . snd <$> bs) (go body)
+    Term.Constructor' r cid -> V (Data r cid mempty)
+    Term.Apps' f args -> case f of
+      Term.Ref' r -> Let (V (env r)) (DynamicApply 0 ((+1) . ind t <$> args))
+      Term.Request' r cid -> Request r cid (ind t <$> args)
+      Term.Constructor' r cid -> Construct r cid (ind t <$> args)
+      _ -> DynamicApply (ind t f) (map (ind t) args) where
+    Term.Handle' h body -> Handle (ind t h) (go body)
+    Term.Ann' e _ -> go e
+    _ -> error $ "TODO - don't know how to compile " ++ show t
+    where
+      unknown v = error $ "free variable during compilation: " ++ show v
+      ind t (Term.Var' v) = case elemIndex v (ABT.annotation t) of
+        Nothing -> error $ "free variable during compilation: " ++ show v
+        Just i -> i
+      ind _ e = error $ "ANF should eliminate any non-var arguments to apply " ++ show e
+
+normalize :: (R.Reference -> V) -> AnnotatedTerm Symbol a -> Term Symbol
+normalize env t =
+  let v = case run env (compile env $ Term.unannotate t) [] of
+        RRequest e -> Requested e
+        RDone a -> a
+        e -> error $ show e
+  in decompile v
+
+parseAndNormalize :: (R.Reference -> V) -> String -> Term Symbol
+parseAndNormalize env s = normalize env (Term.unannotate $ B.tm s)
+
+parseANF :: String -> Term Symbol
+parseANF s = Term.anf . Term.unannotate $ B.tm s

parser-typechecker/src/Unison/Term.hs

@@ -6,12 +6,15 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Unison.Term where
 
+import Prelude hiding (and,or)
 import qualified Control.Monad.Writer.Strict as Writer
+import Data.Functor (void)
 import           Data.Foldable (traverse_, toList)
 import           Data.Int (Int64)
 import           Data.List (foldl')
@@ -139,6 +142,21 @@ typeMap f t = go t where
     -- otherwise we'd have to manually match on every non-`Ann` ctor
     ABT.Tm ts -> unsafeCoerce $ ABT.Tm (fmap go ts)
 
+unannotate :: ∀ vt at ap v a . Ord v => AnnotatedTerm2 vt at ap v a -> Term' vt v
+unannotate t = go t where
+  go :: AnnotatedTerm2 vt at ap v a -> Term' vt v
+  go (ABT.out -> ABT.Abs v body) = ABT.abs v (go body)
+  go (ABT.out -> ABT.Cycle body) = ABT.cycle (go body)
+  go (ABT.Var' v) = ABT.var v
+  go (ABT.Tm' f) =
+    case go <$> f of
+      Ann e t -> ABT.tm (Ann e (void t))
+      Match scrutinee branches ->
+        let unann (MatchCase pat guard body) = MatchCase (void pat) guard body
+        in ABT.tm (Match scrutinee (unann <$> branches))
+      f' -> ABT.tm (unsafeCoerce f')
+  go _ = error "unpossible"
+
 wrapV :: Ord v => AnnotatedTerm v a -> AnnotatedTerm (ABT.V v) a
 wrapV = vmap ABT.Bound
 
@@ -279,6 +297,10 @@ vector' a es = ABT.tm' a (Vector es)
 apps :: Ord v => AnnotatedTerm2 vt at ap v a -> [(a, AnnotatedTerm2 vt at ap v a)] -> AnnotatedTerm2 vt at ap v a
 apps f = foldl' (\f (a,t) -> app a f t) f
 
+apps' :: (Ord v, Semigroup a)
+      => AnnotatedTerm2 vt at ap v a -> [AnnotatedTerm2 vt at ap v a] -> AnnotatedTerm2 vt at ap v a
+apps' f = foldl' (\f t -> app (ABT.annotation f <> ABT.annotation t) f t) f
+
 iff :: Ord v => a -> AnnotatedTerm2 vt at ap v a -> AnnotatedTerm2 vt at ap v a -> AnnotatedTerm2 vt at ap v a -> AnnotatedTerm2 vt at ap v a
 iff a cond t f = ABT.tm' a (If cond t f)
 
@@ -342,6 +364,16 @@ let1 bindings e = foldr f e bindings
   where
     f ((ann,v),b) body = ABT.tm' ann (Let b (ABT.abs' ann v body))
 
+let1' :: (Semigroup a, Ord v)
+      => [(v, AnnotatedTerm2 vt at ap v a)]
+      -> AnnotatedTerm2 vt at ap v a
+      -> AnnotatedTerm2 vt at ap v a
+let1' bindings e = foldr f e bindings
+  where
+    ann = ABT.annotation
+    f (v,b) body = ABT.tm' a (Let b (ABT.abs' a v body)) where
+      a = ann b <> ann body
+
 -- let1' :: Var v => [(Text, Term' vt v)] -> Term' vt v -> Term' vt v
 -- let1' bs e = let1 [(ABT.v' name, b) | (name,b) <- bs ] e
 
@@ -359,22 +391,22 @@ unLet t = fixup (go t) where
   fixup bst = Just bst
 
 -- | Satisfies `unLetRec (letRec bs e) == Just (bs, e)`
-unLetRecNamed :: AnnotatedTerm' vt v a -> Maybe ([(v, AnnotatedTerm' vt v a)], AnnotatedTerm' vt v a)
+unLetRecNamed :: AnnotatedTerm2 vt at ap v a -> Maybe ([(v, AnnotatedTerm2 vt at ap v a)], AnnotatedTerm2 vt at ap v a)
 unLetRecNamed (ABT.Cycle' vs (ABT.Tm' (LetRec bs e)))
   | length vs == length vs = Just (zip vs bs, e)
 unLetRecNamed _ = Nothing
 
 unLetRec :: (Monad m, Var v)
-         => AnnotatedTerm' vt v a
+         => AnnotatedTerm2 vt at ap v a
          -> Maybe ((v -> m v) ->
-                   m ([(v, AnnotatedTerm' vt v a)], AnnotatedTerm' vt v a))
+                   m ([(v, AnnotatedTerm2 vt at ap v a)], AnnotatedTerm2 vt at ap v a))
 unLetRec (unLetRecNamed -> Just (bs, e)) = Just $ \freshen -> do
   vs <- sequence [ freshen v | (v,_) <- bs ]
   let sub = ABT.substsInheritAnnotation (map fst bs `zip` map ABT.var vs)
   pure (vs `zip` [ sub b | (_,b) <- bs ], sub e)
 unLetRec _ = Nothing
 
-unApps :: AnnotatedTerm' vt v a -> Maybe (AnnotatedTerm' vt v a, [AnnotatedTerm' vt v a])
+unApps :: AnnotatedTerm2 vt at ap v a -> Maybe (AnnotatedTerm2 vt at ap v a, [AnnotatedTerm2 vt at ap v a])
 unApps t = case go t [] of [] -> Nothing; f:args -> Just (f,args)
   where
   go (App' i o) acc = go i (o:acc)
@@ -383,7 +415,7 @@ unApps t = case go t [] of [] -> Nothing; f:args -> Just (f,args)
 
 pattern LamsNamed' vs body <- (unLams' -> Just (vs, body))
 
-unLams' :: AnnotatedTerm' vt v a -> Maybe ([v], AnnotatedTerm' vt v a)
+unLams' :: AnnotatedTerm2 vt at ap v a -> Maybe ([v], AnnotatedTerm2 vt at ap v a)
 unLams' (LamNamed' v body) = case unLams' body of
   Nothing -> Just ([v], body)
   Just (vs, body) -> Just (v:vs, body)
@@ -444,6 +476,60 @@ betaReduce :: Var v => Term v -> Term v
 betaReduce (App' (Lam' f) arg) = ABT.bind f arg
 betaReduce e = e
 
+anf :: ∀ vt at v a . (Semigroup a, Var v)
+    => AnnotatedTerm2 vt at a v a -> AnnotatedTerm2 vt at a v a
+anf t = go t where
+  ann = ABT.annotation
+  isVar (Var' _) = True
+  isVar _ = False
+  isClosedLam t@(LamNamed' _ _) | Set.null (ABT.freeVars t) = True
+  isClosedLam _ = False
+  fixAp t f args =
+    let
+      args' = Map.fromList $ toVar =<< (args `zip` [0..])
+      toVar (b, i) | isVar b   = []
+                   | otherwise = [(i, ABT.fresh t (Var.named . Text.pack $ "arg" ++ show i))]
+      argsANF = map toANF (args `zip` [0..])
+      toANF (b,i) = maybe b (var (ann b)) $ Map.lookup i args'
+      addLet (b,i) body = maybe body (\v -> let1' [(v,go b)] body) (Map.lookup i args')
+    in foldr addLet (apps' f argsANF) (args `zip` [(0::Int)..])
+  go :: AnnotatedTerm2 vt at a v a -> AnnotatedTerm2 vt at a v a
+  go (Apps' f@(LamsNamed' vs body) args) | isClosedLam f = ap vs body args where
+    ap vs body [] = lam' (ann f) vs body
+    ap (v:vs) body (arg:args) = let1' [(v,arg)] $ ap vs body args
+    ap [] _body _args = error "type error"
+  go t@(Apps' f args)
+    | isVar f = fixAp t f args
+    | otherwise = let fv' = ABT.fresh t (Var.named "f")
+                  in let1' [(fv', anf f)] (fixAp t (var (ann f) fv') args)
+  go e@(Handle' h body)
+    | isVar h = handle (ann e) h (go body)
+    | otherwise = let h' = ABT.fresh e (Var.named "handler")
+                  in let1' [(h', go h)] (handle (ann e) (var (ann h) h') (go body))
+  go e@(If' cond t f)
+    | isVar cond = iff (ann e) cond (go t) (go f)
+    | otherwise = let cond' = ABT.fresh e (Var.named "cond")
+                  in let1' [(cond', anf cond)] (iff (ann e) (var (ann cond) cond') t f)
+  go e@(Match' scrutinee cases)
+    | isVar scrutinee = match (ann e) scrutinee (fmap go <$> cases)
+    | otherwise = let scrutinee' = ABT.fresh e (Var.named "scrutinee")
+                  in let1' [(scrutinee', go scrutinee)] (match (ann e) (var (ann scrutinee) scrutinee') cases)
+  go e@(And' x y)
+    | isVar x = and (ann e) x (go y)
+    | otherwise =
+        let x' = ABT.fresh e (Var.named "argX")
+        in let1' [(x', anf x)] (and (ann e) (var (ann x) x') (go y))
+  go e@(Or' x y)
+    | isVar x = or (ann e) x (go y)
+    | otherwise =
+        let x' = ABT.fresh e (Var.named "argX")
+        in let1' [(x', go x)] (or (ann e) (var (ann x) x') (go y))
+  go e@(ABT.Tm' f) = ABT.tm' (ann e) (go <$> f)
+  go e@(ABT.Var' _) = e
+  go e@(ABT.out -> ABT.Cycle body) = ABT.cycle' (ann e) (go body)
+  go e@(ABT.out -> ABT.Abs v body) = ABT.abs' (ann e) v (go body)
+  go e = e
+
 instance Var v => Hashable1 (F v a p) where
   hash1 hashCycle hash e =
     let

parser-typechecker/unison-parser-typechecker.cabal

@@ -53,6 +53,7 @@ library
     Unison.PatternP
     Unison.PrintError
     Unison.Reference
+    Unison.Runtime.Rt0
     Unison.Result
     Unison.Symbol
     Unison.Term