Changed Action to preserve typeability

editor/src/Unison/Action.elm

@@ -9,17 +9,15 @@ import Unison.Term as E
 
 type Action
   = Abstract -- Turn target into function parameter
-  | Beta -- Beta reduce the target
+  | Step -- Beta reduce the target
   | 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
-  | Apply Term -- Replace the target, `e`, with `f e`
 
 encode : Encoder Action
 encode a = case a of
   Abstract -> Encoder.tag' "Abstract" Encoder.product0 ()
-  Beta -> Encoder.tag' "Beta" Encoder.product0 ()
+  Step -> Encoder.tag' "Step" Encoder.product0 ()
   Eta -> Encoder.tag' "Eta" Encoder.product0 ()
   LetFloat -> Encoder.tag' "LetFloat" Encoder.product0 ()
   WHNF -> Encoder.tag' "WHNF" Encoder.product0 ()
-  Apply f -> Encoder.tag' "Apply" E.encodeTerm f

editor/src/Unison/Editor.elm

@@ -40,7 +40,7 @@ import Window
 type alias Model =
   { term : Term
   , scope : Scope.Model
-  , goalType : Type
+  , admissibleType : Type
   , currentType : Type
   , availableWidth : Maybe Int
   , dependents : Trie Path.E (List Path)
@@ -55,6 +55,12 @@ type alias Model =
 
 type alias Request = { term : Term, path : Path, query : Maybe String }
 
+type Req
+  = Edit Term Path
+  | Accept Term Path Term
+  | Search Type String
+  | Act
+
 type alias Action = Model -> (Maybe Request, Model)
 
 combine : Action -> Action -> Action
@@ -72,7 +78,7 @@ model0 : Model
 model0 =
   { term = Term.Blank
   , scope = Nothing
-  , goalType = Type.all
+  , admissibleType = Type.all
   , currentType = Type.all
   , availableWidth = Nothing
   , dependents = Trie.empty
@@ -238,7 +244,7 @@ refreshExplorer searchbox model =
           , overrides x = Nothing }
         in List.map show model.explorerValues
 
-      aboveMsg = "Allowed: " ++ toString model.goalType ++ "\n" ++
+      aboveMsg = "Allowed: " ++ toString model.admissibleType ++ "\n" ++
                  "Current: " ++ toString model.currentType
       explorer' : Explorer.Model
       explorer' = model.explorer |> Maybe.map (\e ->
@@ -352,17 +358,17 @@ host = Signal.constant "http://localhost:8080"
 search2 : Sink Field.Content -> Signal Request -> Signal Action
 search2 searchbox reqs =
   let req r = (r.term, r.path)
-      goal resp model = norequest << refreshExplorer searchbox <| case resp of
-        Http.Success t -> { model | goalType <- t }
+      admissible resp model = norequest << refreshExplorer searchbox <| case resp of
+        Http.Success t -> { model | admissibleType <- t }
         Http.Waiting -> model
         Http.Failure code msg -> pushError msg model
       current resp model = norequest << refreshExplorer searchbox <| case resp of
         Http.Success t -> { model | currentType <- t }
         Http.Waiting -> model
         Http.Failure code msg -> pushError msg model
-      goalTypes = Node.admissibleTypeOf host (Signal.map req reqs) |> Signal.map goal
+      admissibleTypes = Node.admissibleTypeOf host (Signal.map req reqs) |> Signal.map admissible
       currentTypes = Node.typeOf host (Signal.map req reqs) |> Signal.map current
-  in Signal.merge goalTypes currentTypes
+  in Signal.merge admissibleTypes currentTypes
 
 -- need to hook into the Signal Field.Content associated with the model
 

node/src/Unison/Edit/Term.hs

@@ -1,5 +1,5 @@
 module Unison.Edit.Term (
-  admissibleTypeOf, abstract, beta, eta, interpret, letFloat, locals, typeOf) where
+  admissibleTypeOf, abstract, step, eta, interpret, letFloat, locals, typeOf) where
 
 import Control.Applicative
 import qualified Data.Set as S
@@ -12,7 +12,6 @@ import qualified Unison.Note as N
 import Unison.Note (Noted)
 import qualified Unison.Syntax.Term as E
 import qualified Unison.Syntax.Hash as H
-import qualified Unison.Syntax.Reference as R
 import qualified Unison.Syntax.Type as T
 import Unison.Type (synthesize)
 
@@ -20,23 +19,23 @@ import Unison.Type (synthesize)
 interpret :: (Applicative f, Monad f)
           => Eval (Noted f)
           -> (H.Hash -> Noted f E.Term)
-          -> T.Env f
-          -> P.Path -> Action E.Term -> E.Term -> Noted f E.Term
-interpret eval readTerm readType loc f ctx = go f where
+          -> P.Path -> Action -> E.Term -> Noted f E.Term
+interpret eval readTerm loc f ctx = go f where
   go Abstract = abstract loc ctx
   go Eta = eta loc ctx
-  go Beta = beta eval readTerm loc ctx
+  go Step = step eval readTerm loc ctx
   go LetFloat = fst <$> letFloat loc ctx
   go WHNF = whnf eval readTerm 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 readType e
 
 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 f [[42]] => (\x -> f x) 42
+-- abstract (\f x -> [[g x + 1]] * 42) => (\gx1 -> (\f x -> gx x * 42)) (\x -> g x + 1)
+-- todo: if the location references any free variables, make these
+-- function parameters of the
 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
@@ -65,13 +64,13 @@ admissibleTypeOf synthLit loc ctx = case P.at' loc ctx of
 
 -- | Beta-reduce the target, @(\x -> x+1) p@ becomes @p+1@.
 -- This noops if target is not beta-reducible.
-beta :: Applicative f
+step :: Applicative f
      => Eval (Noted f)
      -> (H.Hash -> Noted f E.Term)
      -> P.Path
      -> E.Term
      -> Noted f E.Term
-beta eval readTerm loc ctx = case P.at' loc ctx of
+step eval readTerm loc ctx = case P.at' loc ctx of
   Nothing -> N.failure $ invalid loc ctx
   Just (sub,replace) -> replace <$> Eval.step eval readTerm sub
 

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

@@ -3,13 +3,12 @@
 module Unison.Edit.Term.Action where
 import Data.Aeson.TH
 
-data Action e
+data Action
   = Abstract -- Turn target into function parameter
-  | Beta -- Beta reduce the target
+  | Step -- Beta reduce the target
   | 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
-  | Apply e -- Replace the target, `e`, with `f e`
 
 deriveJSON defaultOptions ''Action
 -- combine fst snd

node/src/Unison/Node.hs

@@ -20,9 +20,9 @@ data Node m k t e = Node {
   -- | Lookup the set of terms/types depending directly on the given @k@, optionally limited to the given set
   dependents :: Maybe (S.Set k) -> k -> Noted m (S.Set k),
   -- | Modify the given subterm, which may fail
-  editTerm :: P.Path -> A.Action e -> e -> Noted m e,
+  editTerm :: P.Path -> A.Action -> e -> Noted m e,
   -- | Modify the given type, which may fail
-  editType :: P.Path -> A.Action t -> t -> Noted m t,
+  editType :: P.Path -> A.Action -> t -> Noted m t,
   -- | Access the metadata for the term and/or types identified by @k@
   metadatas :: [k] -> Noted m (Map k (MD.Metadata k)),
   -- | Search for a term, optionally constrained to be of the given type

node/src/Unison/Node/Common.hs

@@ -62,7 +62,7 @@ node eval store =
       pure $ S.fromList [x | (x,deps) <- hs', S.member h deps]
 
     edit path action e = do
-      TE.interpret eval (readTerm store) readTypeOf path action e
+      TE.interpret eval (readTerm store) path action e
 
     editType = error "Common.editType.todo"