Node now has openEdit function

node/src/Unison/Edit/Term.hs

@@ -1,7 +1,8 @@
 module Unison.Edit.Term (
-  admissibleTypeOf, abstract, step, eta, interpret, letFloat, locals, typeOf) where
+  admissibleTypeOf, abstract, applications, step, eta, interpret, letFloat, locals, typeOf) where
 
 import Control.Applicative
+import Data.Traversable
 import qualified Data.Set as S
 import Unison.Edit.Term.Action as A
 import qualified Unison.Edit.Term.Path as P
@@ -112,12 +113,43 @@ letFloat loc ctx = case P.at loc ctx of
         loc' <- pure $ P.extend P.Arg trimmedPath
         pure (ctx', loc')
 
--- | Return the type of all local variables introduced by the
--- given lambda, assuming that lambda has the annotated type
-locals :: E.Term -> T.Type -> [(V.Var, T.Type)]
-locals (E.Lam n body) (T.Arrow i o) = (n, i) : locals body o
-locals ctx (T.Forall _ t) = locals ctx t
-locals _ _ = []
+-- | Return the type of all local variables in scope at the given location
+locals :: Applicative f => T.Env f -> P.Path -> E.Term -> Noted f [(V.Var, T.Type)]
+locals synthLit path ctx | E.isClosed ctx = pushDown <$> lambdaTypes
+  where
+    pointsToLambda path = case P.at path ctx of
+      Just (E.Lam _ _) -> True
+      _ -> False
+
+    lambdas :: [P.Path]
+    lambdas = filter pointsToLambda (P.prefixes path)
+
+    notedAt path expr = maybe (N.failure "invalid path") pure (P.at path expr)
+
+    lambdaTypes = traverse t lambdas
+      where t path = liftA2 extract (notedAt path ctx) (typeOf synthLit path ctx)
+
+    -- not sure about this impl, or if it matters
+    -- we prefer type information obtained higher in the syntax tree
+    pushDown :: [[(V.Var, T.Type)]] -> [(V.Var, T.Type)]
+    pushDown [] = []
+    pushDown (env0 : tl) = env0 ++ pushDown (drop (length env0) tl)
+
+    extract :: E.Term -> T.Type -> [(V.Var, T.Type)]
+    extract (E.Lam n body) (T.Arrow i o) = (n, i) : extract body o
+    extract ctx (T.Forall _ t) = extract ctx t
+    extract _ _ = []
+locals _ _ ctx =
+  N.failure $ "Term.locals: term contains free variables - " ++ show (E.freeVars ctx)
+
+-- | Produce `e`, `e _`, `e _ _`, `e _ _ _` and so on,
+-- until the result is no longer a function type
+applications :: E.Term -> T.Type -> [E.Term]
+applications e t = e : go e t
+  where
+    go e (T.Forall _ t) = go e t
+    go e (T.Arrow _ t) = let e' = E.App e E.Blank in go e' t
+    go _ _ = []
 
 -- | Compute the type of the given subterm, unconstrained as much
 -- as possible by any local usages of that subterm. For example, in

node/src/Unison/Edit/Term/Path.hs

@@ -1,4 +1,3 @@
-{-# OPTIONS_GHC -ddump-splices #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE OverloadedStrings #-}
 
@@ -25,6 +24,11 @@ newtype Path = Path [E] deriving (Eq,Ord,Show)
 elements :: Path -> [E]
 elements (Path e) = e
 
+prefixes :: Path -> [Path]
+prefixes (Path p) = map Path (go p)
+  where go :: [a] -> [[a]]
+        go as = map reverse (scanl (flip (:)) [] as)
+
 -- | Add an element onto the end of this 'Path'
 extend :: E -> Path -> Path
 extend e (Path p) = Path (p ++ [e])
@@ -41,6 +45,18 @@ at (Path (h:t)) e = go h e where
   go Body (E.Lam _ body) = at (Path t) body
   go _ _ = Nothing
 
+along :: Path -> E.Term -> [E.Term]
+along (Path path) e = go path e
+  where go [] e = [e]
+        go (Fn:path) e@(E.App f _) = e : go path f
+        go (Arg:path) e@(E.App _ arg) = e : go path arg
+        go (Body:path) e@(E.Lam _ body) = e : go path body
+        go (Index i:path) e@(E.Vector xs) = e : maybe [] (go path) (xs !? i)
+        go _ _ = []
+
+valid :: Path -> E.Term -> Bool
+valid p e = maybe False (const True) (at p e)
+
 -- | 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

node/src/Unison/Node.hs

@@ -26,12 +26,14 @@ data Node m k t e = Node {
   -- | Access the metadata for the term and/or types identified by @k@
   metadatas :: [k] -> Noted m (Map k (MD.Metadata k)),
   -- | Open the given location for editing;
-  -- returns the current type, admissible type, local vars, matching local expressions
-  open :: e -> P.Path -> Noted m (t, t, [e], [e]),
+  -- returns ( current type
+  --         , admissible type
+  --         , local vars
+  --         , matching local applications
+  --         , matching local expressions )
+  openEdit :: e -> P.Path -> Noted m (t, t, [e], [Int], [e]),
   -- | Search for a term, optionally constrained to be of the given type
   search :: Maybe t -> Query -> Noted m [e],
-  -- | Search for a term of the given type in local scope
-  searchLocal :: k -> P.Path -> Maybe t -> Noted m [e],
   -- | Lookup the source of the term identified by @k@
   terms :: [k] -> Noted m (Map k e),
   -- | Lookup the dependencies of @k@, optionally limited to those that intersect the given set

node/src/Unison/Node/Common.hs

@@ -4,10 +4,12 @@ module Unison.Node.Common (node) where
 import Control.Applicative
 import Control.Monad
 import Unison.Edit.Term.Eval as Eval
+import Unison.Edit.Term.Path as Path
 import Unison.Node as N
 import Unison.Node.Metadata as MD
 import Unison.Node.Store
 import Unison.Note (Noted)
+import qualified Unison.Note as Note
 import Unison.Syntax.Term (Term)
 import Unison.Syntax.Type (Type)
 import qualified Data.Map as M
@@ -69,8 +71,17 @@ node eval store =
     metadatas hs =
       M.fromList <$> sequence (map (\h -> (,) h <$> readMetadata store h) hs)
 
-    open e path =
-      error "Common.open.todo"
+    openEdit e loc = do
+      current <- TE.typeOf readTypeOf loc e
+      admissible <- TE.admissibleTypeOf readTypeOf loc e
+      locals <- TE.locals readTypeOf loc e
+      annotatedLocals <- pure $ map (\(v,t) -> E.Var v `E.Ann` t) locals
+      let f e = (const True <$> Type.check readTypeOf e admissible) `Note.orElse` pure False
+      let fi (e,_) = f e
+      let currentApplies = maybe [] (\e -> TE.applications e admissible) (Path.at loc e) `zip` [0..]
+      matchingCurrentApplies <- map snd <$> filterM fi currentApplies
+      matchingLocals <- filterM f (locals >>= (\(v,t) -> TE.applications (E.Var v) t))
+      pure (current, admissible, annotatedLocals, matchingCurrentApplies, matchingLocals)
 
     search t query = do
       hs <- hashes store Nothing
@@ -80,8 +91,6 @@ node eval store =
       mds <- mapM (\h -> (,) h <$> readMetadata store h) hs'
       pure . map (\(h,_) -> E.Ref h) . filter (\(_,md) -> MD.matches query md) $ mds
 
-    searchLocal h path t = pure [] -- todo: implement
-
     readTermRef (R.Derived h) = readTerm store h
     readTermRef r = pure (E.Ref r)
 
@@ -110,9 +119,8 @@ node eval store =
        edit
        editType
        metadatas
-       open
+       openEdit
        search
-       searchLocal
        terms
        transitiveDependencies
        transitiveDependents

node/src/Unison/Node/Server.hs

@@ -93,18 +93,14 @@ server port node = S.scotty port $ do
     hs <- S.jsonData
     md <- runN $ N.metadatas node hs
     S.json md
-  S.post "/open" . route $ do
+  S.post "/open-edit" . route $ do
     (e, path) <- S.jsonData
-    t <- runN $ N.open node e path
+    t <- runN $ N.openEdit node e path
     S.json t
   S.get "/search" $ do
     (t,q) <- S.jsonData
     es <- runN $ N.search node t q
     S.json es
-  S.get "/search-local" $ do
-    (h,p,t) <- S.jsonData
-    es <- runN $ N.searchLocal node h p t
-    S.json es
   S.get "/terms" $ do
     hs <- S.jsonData
     r <- runN $ N.terms node hs

node/src/Unison/Syntax/Term.hs

@@ -9,6 +9,7 @@ module Unison.Syntax.Term where
 import qualified Data.Foldable as Foldable
 import Data.Traversable
 import Control.Applicative
+import Control.Lens.TH
 import Control.Monad
 import Control.Monad.Writer
 import Data.Aeson.TH
@@ -219,3 +220,5 @@ hashes _ = error "todo: Term.hashes"
 
 deriveJSON defaultOptions ''Literal
 deriveJSON defaultOptions ''Term
+
+makePrisms ''Term

node/src/Unison/Type.hs

@@ -34,16 +34,19 @@ check' :: E.Term -> T.Type -> Either Note T.Type
 check' term typ = join . N.unnote $ check missing term typ
   where missing h = N.failure $ "unexpected ref: " ++ show h
 
--- | @subtype a b@ is @Right b@ iff any @b -> t@ is well-typed when
--- given a value of type @a@, and is @Left note@ with information
+-- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
+-- @x : a@ and @f : b -> t@. That is, if a value of type `a`
+-- can be passed to a function expecting a `b`, then `subtype a b`
+-- returns `Right b`. This function returns @Left note@ with information
 -- about the reason for subtyping failure otherwise.
--- Example: the identity function, of type @forall a. a -> a@,
--- is a subtype of @Int -> Int@.
+--
+-- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
 subtype :: T.Type -> T.Type -> Either Note T.Type
 subtype t1 t2 = case C.subtype (C.context []) t1 t2 of
   Left e -> Left e
   Right _ -> Right t2
 
+-- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
 isSubtype :: T.Type -> T.Type -> Bool
 isSubtype t1 t2 = case C.subtype (C.context []) t1 t2 of
   Left _ -> False

node/src/Unison/Type/Context.hs

@@ -285,6 +285,7 @@ check ctx e t | wellformedType ctx t = scope (show e ++ " : " ++ show t) $ go e
         ctx' = extend (E.Ann x' i) ctx
         body' = Term.betaReduce (fn `Term.App` v)
     in check ctx' body' o >>= retract (E.Ann x' i)
+  -- go Term.Blank _ = Right ctx -- possible hack to workaround lack of impredicative instantiation
   go _ _ = do -- Sub
     (a, ctx') <- synthesize ctx e
     subtype ctx' (apply ctx' a) (apply ctx' t)

node/unison.cabal

@@ -86,7 +86,7 @@ library
     directory                 ,
     filepath                  ,
     http-types                ,
-    lens                      >= 4.2, 
+    lens                      >= 4.7,
     mtl                       >= 2.1.1,
     prelude-extras            >= 0.3,
     scotty                    == 0.9.1,