finished Action interpreter

src/Unison/Edit/Term.hs

@@ -5,7 +5,8 @@ import Control.Applicative
 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.Edit.Term.Eval as Eval
+import Unison.Edit.Term.Eval (Eval)
 import qualified Unison.Syntax.Hash as H
 import qualified Unison.Syntax.Var as V
 import qualified Unison.Note as N
@@ -22,7 +23,10 @@ interpret eval loc f ctx = go f where
   go Eta = eta loc ctx
   go Beta = beta eval loc ctx
   go LetFloat = fst <$> letFloat loc ctx
-  go _ = error "todo: Apply, WHNF, HNF, Apply will have to invoke typechecker"
+  go WHNF = whnf eval loc ctx
+  go (Apply e) = case P.modify loc (E.App e) ctx of
+    Nothing -> N.failure $ invalid loc ctx
+    Just e -> const e <$> synthesize (Eval.typ eval) e
 
 invalid :: (Show a1, Show a) => a -> a1 -> String
 invalid loc ctx = "invalid path " ++ show loc ++ " in:\n" ++ show ctx
@@ -33,49 +37,6 @@ 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
-
--- | 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 _ _ = []
-
--- | 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]@.
-typeOf :: Applicative f
-       => (H.Hash -> Noted f T.Type)
-       -> P.Path
-       -> E.Term
-       -> Noted f T.Type
-typeOf synthLit (P.Path []) ctx = synthesize synthLit ctx
-typeOf 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
-        -- copy the subtree so type is unconstrained by local usage
-        ksub f = E.lam2 (\x _ -> x) `E.App` sub `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)
-        go _ = error "impossible, f had better be a function"
-    in go <$> synthesize synthLit ctx
-
 -- | 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
@@ -104,6 +65,20 @@ admissibleTypeOf synthLit loc ctx = case P.at' loc ctx of
         go _ = error "impossible, f had better be a function"
     in go <$> synthesize synthLit 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 <$> Eval.step eval sub
+
+-- | 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
+
+
 -- | 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:
@@ -134,3 +109,41 @@ letFloat loc ctx = case P.at loc ctx of
         ctx' <- P.set trimmedPath (body `E.App` sub) ctx
         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 _ _ = []
+
+-- | 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]@.
+typeOf :: Applicative f
+       => (H.Hash -> Noted f T.Type)
+       -> P.Path
+       -> E.Term
+       -> Noted f T.Type
+typeOf synthLit (P.Path []) ctx = synthesize synthLit ctx
+typeOf 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
+        -- copy the subtree so type is unconstrained by local usage
+        ksub f = E.lam2 (\x _ -> x) `E.App` sub `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)
+        go _ = error "impossible, f had better be a function"
+    in go <$> synthesize synthLit ctx
+
+-- | Evaluate the given location to weak head normal form.
+-- If the location contains any free variables, this noops.
+whnf :: Applicative f => Eval f -> P.Path -> E.Term -> Noted f E.Term
+whnf eval loc ctx = case P.at' loc ctx of
+  Nothing -> N.failure $ invalid loc ctx
+  Just (sub,replace) | S.null (E.freeVars sub) -> replace <$> Eval.whnf eval sub
+  Just _             | otherwise               -> pure ctx

src/Unison/Edit/Term/Action.hs

@@ -9,7 +9,6 @@ data Action e
   | Eta -- Eta reduce the target
   | LetFloat -- Float the target out to a let binding, as far as possible
   | WHNF -- Simplify target to weak head normal form
-  | HNF -- Simplify target to head normal form
   | Apply e -- Replace the target, `e`, with `f e`
 
 deriveJSON defaultOptions ''Action

src/Unison/Edit/Term/Eval.hs

@@ -1,10 +1,13 @@
 module Unison.Edit.Term.Eval where
 
 import Unison.Note (Noted)
-import Unison.Syntax.Term
+import Unison.Syntax.Hash (Hash)
+import Unison.Syntax.Term (Term)
+import Unison.Syntax.Type (Type)
 
 data Eval m = Eval {
-  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
+  whnf :: Term -> Noted m Term,  -- ^ Simplify to weak head normal form
+  step :: Term -> Noted m Term,  -- ^ Perform one beta reduction
+  term :: Hash -> Noted m Term,  -- ^ Lookup the source of a given term
+  typ :: Hash -> Noted m Type    -- ^ Lookup the source of a given type
 }

src/Unison/Syntax/Term.hs

@@ -6,6 +6,7 @@
 
 module Unison.Syntax.Term where
 
+import Control.Applicative
 import Control.Monad
 import Data.Aeson.TH
 import qualified Data.Aeson.Encode as JE
@@ -68,6 +69,15 @@ lam2 f = lam1 $ \x -> lam1 $ \y -> f x y
 lam3 :: (Term -> Term -> Term -> Term) -> Term
 lam3 f = lam1 $ \x -> lam1 $ \y -> lam1 $ \z -> f x y z
 
+-- | Convert all 'Ref' constructors to the corresponding term
+link :: Applicative f => (H.Hash -> f Term) -> Term -> f Term
+link env e = case e of
+  Ref h -> env h
+  App fn arg -> App <$> link env fn <*> link env arg
+  Lam n body -> go <$> link env body
+    where go body = lam1 $ \x -> betaReduce (Lam n body `App` x)
+  _ -> pure e
+
 dependencies :: Term -> S.Set H.Hash
 dependencies e = case e of
   Ref h -> S.singleton h