diff --git a/editor/src/Unison/Action.elm b/editor/src/Unison/Action.elm index 3f321dfe3..dff6161d9 100644 --- a/editor/src/Unison/Action.elm +++ b/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 diff --git a/editor/src/Unison/Editor.elm b/editor/src/Unison/Editor.elm index 51f1687a4..71453e2a3 100644 --- a/editor/src/Unison/Editor.elm +++ b/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 diff --git a/node/src/Unison/Edit/Term.hs b/node/src/Unison/Edit/Term.hs index dd680762a..21b9b2262 100644 --- a/node/src/Unison/Edit/Term.hs +++ b/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 diff --git a/node/src/Unison/Edit/Term/Action.hs b/node/src/Unison/Edit/Term/Action.hs index 675f5cd56..1f8c65392 100644 --- a/node/src/Unison/Edit/Term/Action.hs +++ b/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 diff --git a/node/src/Unison/Node.hs b/node/src/Unison/Node.hs index 203cd9b85..eb1024139 100644 --- a/node/src/Unison/Node.hs +++ b/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 diff --git a/node/src/Unison/Node/Common.hs b/node/src/Unison/Node/Common.hs index e8a20e370..d0c48efbc 100644 --- a/node/src/Unison/Node/Common.hs +++ b/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"