From bdf0a738a7b89fe9a06bc1bdcf87e4fefe07e74c Mon Sep 17 00:00:00 2001
From: Paul Chiusano <paul.chiusano@gmail.com>
Date: Fri, 27 Jun 2014 18:00:39 -0400
Subject: [PATCH] more progress on implementing editor backend

---
 src/Unison/Edit/Term.hs                   | 117 +++++++++++++++++++---
 src/Unison/Edit/Term/Eval.hs              |   7 +-
 src/Unison/Edit/Term/Path.hs              |  43 +++++++-
 src/Unison/Node/Implementations/Common.hs |   2 +-
 src/Unison/Syntax/Index.hs                |   1 -
 src/Unison/Syntax/Term.hs                 |  11 +-
 src/Unison/Syntax/Type.hs                 |   6 +-
 src/Unison/Type.hs                        |   2 +-
 8 files changed, 163 insertions(+), 26 deletions(-)

diff --git a/src/Unison/Edit/Term.hs b/src/Unison/Edit/Term.hs
index 09c00d7ca..9b0a91088 100644
--- a/src/Unison/Edit/Term.hs
+++ b/src/Unison/Edit/Term.hs
@@ -1,24 +1,111 @@
-module Unison.Edit.Term where
+module Unison.Edit.Term (interpret, abstract, eta, beta, letFloat) where
 
 import Control.Applicative
-import qualified Unison.Edit.Term.Path as P
+import qualified Data.Set as S
 import Unison.Edit.Term.Action as A
+import qualified Unison.Edit.Term.Path as P
 import Unison.Edit.Term.Eval as Eval
+import qualified Unison.Syntax.Hash as H
 import qualified Unison.Note as N
 import Unison.Note (Noted)
+import qualified Unison.Syntax.Var
 import qualified Unison.Syntax.Term as E
+import qualified Unison.Syntax.Type as T
+import Unison.Type (synthesize)
 
-apply :: (Applicative f, Monad f)
+-- | Interpret the given 'Action'
+interpret :: (Applicative f, Monad f)
       => Eval f -> P.Path -> Action E.Term -> E.Term -> Noted f E.Term
-apply eval loc f ctx = go f where
-  go Abstract = N.liftMaybe invalid $ E.lam1 <$> P.set' loc ctx
-  go Eta = case P.at loc ctx of
-    Nothing -> N.failure invalid
-    Just sub -> N.liftMaybe invalid $ P.set loc (E.etaReduce sub) ctx
-  go Beta = case P.at loc ctx of
-    Nothing -> N.failure invalid
-    Just sub -> do
-      sub <- N.lift $ step eval sub
-      N.liftMaybe invalid $ P.set loc sub ctx
-  go _ = undefined
-  invalid = "invalid path " ++ show loc ++ " in:\n" ++ show ctx
+interpret eval loc f ctx = go f where
+  go Abstract = abstract loc ctx
+  go Eta = eta loc ctx
+  go Beta = beta eval loc ctx
+  go _ = error "todo: Apply, WHNF, HNF, Apply will have to invoke typechecker"
+
+invalid :: (Show a1, Show a) => a -> a1 -> String
+invalid loc ctx = "invalid path " ++ show loc ++ " in:\n" ++ show ctx
+
+-- | Pull the given path location in the term out into the outermost
+-- function parameter
+abstract :: Applicative f => P.Path -> E.Term -> Noted f E.Term
+abstract loc ctx =
+  N.liftMaybe (invalid loc ctx) $ E.lam1 <$> P.set' loc ctx
+
+-- | Eta-reduce the target; @\x -> f x@ becomes @f@.
+-- This noops if target is not eta-reducible.
+eta :: Applicative f => P.Path -> E.Term -> Noted f E.Term
+eta loc ctx =
+  N.liftMaybe (invalid loc ctx) $ P.modify loc E.etaReduce ctx
+
+-- | Beta-reduce the target, @(\x -> x+1) p@ becomes @p+1@.
+-- This noops if target is not beta-reducible.
+beta :: Applicative f => Eval f -> P.Path -> E.Term -> Noted f E.Term
+beta eval loc ctx = case P.at' loc ctx of
+  Nothing -> N.failure $ invalid loc ctx
+  Just (sub,replace) -> replace <$> step eval sub
+
+-- | Compute the allowed type of a replacement for a given subterm.
+-- Example, in @\g -> map g [1,2,3]@, @g@ has an admissible type of
+-- @forall r . Int -> r@, which means that an @Int -> Bool@, an
+-- @Int -> String@, etc could all be substituted for @g@.
+--
+-- Algorithm works by replacing the subterm, @e@ with
+-- @const e (f e)@, where @f@ is a fresh function parameter. We then
+-- read off the type of @e@ from the inferred type of @f@.
+admissibleTypeAt :: Applicative f
+                 => (H.Hash -> Noted f T.Type)
+                 -> P.Path
+                 -> E.Term
+                 -> Noted f T.Type
+admissibleTypeAt synthLit (P.Path []) ctx = synthesize synthLit ctx
+admissibleTypeAt synthLit loc ctx = case P.at' loc ctx of
+  Nothing -> N.failure $ invalid loc ctx
+  Just (sub,replace) ->
+    let ctx = E.lam1 $ \f -> replace (ksub f)
+        -- we annotate `f` as returning `Number` so as not to introduce
+        -- any new quantified variables in the inferred type
+        ksub f = E.lam2 (\x y -> x) `E.App` (f `E.App` sub `E.Ann` T.Unit T.Number)
+        go (T.Arrow (T.Arrow tsub _) _) = tsub
+        go (T.Forall n t) = T.Forall n (go t)
+    in go <$> synthesize synthLit ctx
+
+-- | Compute the type of the given subterm, unconstrained as much
+-- as possible by any local usages of that subterm. For example, in
+-- @\g -> map g [1,2,3]@, @g@ will have a type of @forall r . Int -> r@,
+-- and @map@ will have a type of @forall a b . (a -> b) -> [a] -> [b]@.
+typeAt :: (Monad f, Applicative f)
+       => (H.Hash -> Noted f T.Type)
+       -> P.Path
+       -> E.Term
+       -> Noted f T.Type
+typeAt synthLit (P.Path []) ctx = synthesize synthLit ctx
+typeAt synthLit loc ctx = case P.at loc ctx of
+  Nothing -> N.failure $ invalid loc ctx
+  Just sub -> letFloat loc ctx >>= \(ctx,loc) ->
+    admissibleTypeAt synthLit loc ctx
+
+-- | Extract the given subterm into a let (implemented with a lambda)
+-- floated out as far as possible while ensuring access to all the
+-- variables used by the subterm. Examples:
+--
+-- * @\x -> f x 42@, 'letFloat' targeting @42@ (which has no free variables)
+--   will float this all the way to the outside, yielding @\y -> (\x -> f x y) 42@.
+-- * Targeting @f x@ in the same expression will float the let out to the
+--   @\x -> ..@ lambda (since @f x@ references the variable bound by that lambda),
+--   yielding @\x -> (\y -> y 42) (f x)@
+--
+-- This function returns a path to the floated subexpression (@42@ and @f x@ in
+-- the above examples.)
+letFloat :: Applicative f => P.Path -> E.Term -> Noted f (E.Term, P.Path)
+letFloat loc ctx = case P.at loc ctx of
+  Nothing  -> N.failure $ invalid loc ctx
+  Just sub ->
+    let
+      free = E.freeVars sub
+      minVar = if S.null free then Nothing else Just (S.findMin free)
+      trimmedPath = P.trimToV minVar loc
+    in
+      N.liftMaybe (invalid loc ctx) $ do
+        ctx' <- P.modify trimmedPath (\body -> E.lam1 (\x -> body) `E.App` sub) ctx
+        loc' <- pure $ P.extend P.Arg trimmedPath
+        pure (ctx', loc')
diff --git a/src/Unison/Edit/Term/Eval.hs b/src/Unison/Edit/Term/Eval.hs
index e92f7b463..1aa3ecb06 100644
--- a/src/Unison/Edit/Term/Eval.hs
+++ b/src/Unison/Edit/Term/Eval.hs
@@ -1,9 +1,10 @@
 module Unison.Edit.Term.Eval where
 
+import Unison.Note (Noted)
 import Unison.Syntax.Term
 
 data Eval m = Eval {
-  whnf :: Term -> m Term, -- ^ Simplify to weak head normal form
-  hnf :: Term -> m Term,  -- ^ Simplify to head normal form
-  step :: Term -> m Term  -- ^ Perform one beta reduction
+  whnf :: Term -> Noted m Term, -- ^ Simplify to weak head normal form
+  hnf :: Term -> Noted m Term,  -- ^ Simplify to head normal form
+  step :: Term -> Noted m Term  -- ^ Perform one beta reduction
 }
diff --git a/src/Unison/Edit/Term/Path.hs b/src/Unison/Edit/Term/Path.hs
index 74d3e7e04..5928ebbcb 100644
--- a/src/Unison/Edit/Term/Path.hs
+++ b/src/Unison/Edit/Term/Path.hs
@@ -1,6 +1,7 @@
 module Unison.Edit.Term.Path where
 
 import Control.Applicative
+import Control.Lens (Traversal')
 import Data.Maybe (fromJust)
 import qualified Unison.Syntax.Term as E
 import qualified Unison.Syntax.Var as V
@@ -13,6 +14,10 @@ data E
 
 newtype Path = Path [E] deriving (Eq,Ord,Show)
 
+-- | Add an element onto the end of this 'Path'
+extend :: E -> Path -> Path
+extend e (Path p) = Path (p ++ [e])
+
 at :: Path -> E.Term -> Maybe E.Term
 at (Path [])    e = Just e
 at (Path (h:t)) e = go h e where
@@ -24,6 +29,25 @@ at (Path (h:t)) e = go h e where
   go Body (E.Lam _ body) = at (Path t) body
   go _ _ = Nothing
 
+-- | If the given @Path@ points to a valid subterm, we replace
+-- that subterm @e@ with @v e@ and sequence the @Applicative@ effects
+-- visit :: Path -> Traversal' E.Term E.Term
+visit :: Applicative f => Path -> (E.Term -> f E.Term) -> E.Term -> f E.Term
+visit (Path []) v e = v e
+visit (Path (h:t)) v e = go h e where
+  go Fn (E.App f arg) = E.App <$> visit (Path t) v f <*> pure arg
+  go Arg (E.App f arg) = E.App <$> pure f <*> visit (Path t) v arg
+  go _ (E.Ann e' typ) = E.Ann <$> visit (Path (h:t)) v e' <*> pure typ
+  go Body (E.Lam n body) = fn <$> visit (Path t) v body
+    where fn body = E.lam1 $ \x -> E.betaReduce (E.Lam n body `E.App` x)
+  go _ e = pure e
+
+-- | Like 'at', but returns a function which may be used to modify the focus
+at' :: Path -> E.Term -> Maybe (E.Term, E.Term -> E.Term)
+at' loc ctx = case at loc ctx of
+  Nothing -> Nothing
+  Just focus -> Just (focus, \focus -> fromJust (set loc focus ctx)) -- safe since `at` proves `loc` valid
+
 set :: Path -> E.Term -> E.Term -> Maybe E.Term
 set path focus ctx = impl path ctx where
   maxVar = E.maxV focus
@@ -39,11 +63,24 @@ set path focus ctx = impl path ctx where
 
 -- | Like 'set', but accepts the new focus within the returned @Maybe@.
 set' :: Path -> E.Term -> Maybe (E.Term -> E.Term)
-set' loc ctx = case at loc ctx of
-  Nothing -> Nothing
-  Just _ -> Just $ \focus -> fromJust (set loc focus ctx) -- safe since `at` proves `loc` valid
+set' loc ctx = snd <$> at' loc ctx
 
 modify :: Path -> (E.Term -> E.Term) -> E.Term -> Maybe E.Term
 modify loc f ctx = do
   x <- at loc ctx
   set loc (f x) ctx
+
+-- | Drop from the right of this 'Path' until reaching the given element
+trimToR :: E -> Path -> Path
+trimToR e (Path p) = Path . reverse . dropWhile (/= e) . reverse $ p
+
+-- | Drop the rightmost element of this 'Path', if it exists
+drop1R :: Path -> Path
+drop1R (Path p) = Path . reverse . drop 1 . reverse $ p
+
+-- | Assuming Axelsson-Claessen naming, drop from the right of this
+-- path until reaching the shortest path which still binds that name
+trimToV :: Maybe (V.Var) -> Path -> Path
+trimToV Nothing p = p
+trimToV (Just minv) p | minv == V.bound1 = trimToR Body p
+                      | otherwise        = trimToV (Just $ V.decr minv) (drop1R (trimToR Body p))
diff --git a/src/Unison/Node/Implementations/Common.hs b/src/Unison/Node/Implementations/Common.hs
index f29c05c2b..05bcccf9c 100644
--- a/src/Unison/Node/Implementations/Common.hs
+++ b/src/Unison/Node/Implementations/Common.hs
@@ -67,7 +67,7 @@ node eval store =
 
     edit k path action = do
       e <- readTerm store k
-      e' <- TE.apply eval path action e
+      e' <- TE.interpret eval path action e
       pure $ (E.finalizeHash e', e')
 
     editType = error "todo later"
diff --git a/src/Unison/Syntax/Index.hs b/src/Unison/Syntax/Index.hs
index da705aa39..d7d658960 100644
--- a/src/Unison/Syntax/Index.hs
+++ b/src/Unison/Syntax/Index.hs
@@ -1,6 +1,5 @@
 module Unison.Syntax.Index where
 
--- how many scopes out to go to reach the lambda where this is bound
 newtype Index = I Int deriving (Eq,Ord)
 
 instance Show Index where
diff --git a/src/Unison/Syntax/Term.hs b/src/Unison/Syntax/Term.hs
index 1941fdb13..5b68676bf 100644
--- a/src/Unison/Syntax/Term.hs
+++ b/src/Unison/Syntax/Term.hs
@@ -91,6 +91,14 @@ dependencies e = case e of
   Ann e _ -> dependencies e
   Lam _ body -> dependencies body
 
+freeVars :: Term -> S.Set V.Var
+freeVars e = case e of
+  Var v -> S.singleton v
+  App fn arg -> freeVars fn `S.union` freeVars arg
+  Ann e _ -> freeVars e
+  Lam n body -> S.delete n (freeVars body)
+  _ -> S.empty
+
 {-
 vars :: Term -> [V.Var]
 vars e = getConst $ collect (\v -> Const [v]) e
@@ -113,7 +121,8 @@ betaReduce (App (Lam var f) arg) = go f where
   go body = case body of
     App f x -> App (go f) (go x)
     Ann body t -> Ann (go body) t
-    Lam n body -> Lam n (go body)
+    Lam n body | n == var  -> Lam n body -- this lambda shadows var; avoid substituting
+               | otherwise -> Lam n (go body)
     Var v | v == var -> arg
     _ -> body
 betaReduce e = e
diff --git a/src/Unison/Syntax/Type.hs b/src/Unison/Syntax/Type.hs
index 8a07c832d..0c313afaf 100644
--- a/src/Unison/Syntax/Type.hs
+++ b/src/Unison/Syntax/Type.hs
@@ -5,11 +5,12 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TemplateHaskell #-}
 
 module Unison.Syntax.Type where
 
 import Control.Applicative
+import Control.Lens
 import qualified Data.List as L
 import qualified Data.Set as S
 import qualified Unison.Syntax.Hash as H
@@ -136,3 +137,6 @@ finalizeHash = H.finalize . hash
 
 hashes :: [Type] -> H.Hash
 hashes _ = error "todo: Type.hashes"
+
+makePrisms ''Literal
+makePrisms ''Type
diff --git a/src/Unison/Type.hs b/src/Unison/Type.hs
index 32c9332ad..f44f0afb7 100644
--- a/src/Unison/Type.hs
+++ b/src/Unison/Type.hs
@@ -47,5 +47,5 @@ subtype t1 t2 = case C.subtype (C.context []) t1 t2 of
 
 isSubtype :: T.Type -> T.Type -> Bool
 isSubtype t1 t2 = case C.subtype (C.context []) t1 t2 of
-  Left e -> False
+  Left _ -> False
   Right _ -> True