mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-23 16:28:02 +03:00
more progress on implementing editor backend
This commit is contained in:
parent
fad7b9f364
commit
bdf0a738a7
@ -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')
|
||||
|
@ -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
|
||||
}
|
||||
|
@ -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))
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user