1
1
mirror of https://github.com/github/semantic.git synced 2025-01-01 11:46:14 +03:00

Bump higher-order-effects for interposition.

This commit is contained in:
Rob Rix 2018-10-25 09:27:40 -04:00
parent 05c4f76663
commit 775bc6ef80
4 changed files with 21 additions and 38 deletions

View File

@ -7,7 +7,7 @@ import Control.Abstract.Heap (Allocator, Deref, deref)
import Control.Abstract.Value
import Control.Effect.Carrier
import Control.Effect.Sum
import Data.Abstract.Evaluatable
import Data.Abstract.Evaluatable hiding (InterposeC)
import Data.Abstract.Name (name)
import Data.Abstract.Path (stripQuotes)
import Data.Abstract.Value.Concrete (Value (..), ValueError (..))

View File

@ -30,6 +30,7 @@ import Control.Abstract.Modules as X (Modules, ModuleResult, ResolutionError(..)
import Control.Abstract.Value as X hiding (Boolean(..), Function(..), While(..))
import Control.Abstract.ScopeGraph
import Control.Effect.Eavesdrop
import Control.Effect.Interpose
import Data.Abstract.Declarations as X
import Data.Abstract.Environment as X
import Data.Abstract.BaseError as X
@ -86,15 +87,16 @@ class (Show1 constr, Foldable constr) => Evaluatable constr where
type ModuleC address value m
= EavesdropC (Modules address) (Eff
( ErrorC (LoopControl address) (Eff
( ErrorC (Return address) (Eff
( EnvC address (Eff
( ScopeEnvC address (Eff
( DerefC address value (Eff
( AllocatorC address (Eff
( ReaderC ModuleInfo (Eff
m)))))))))))))))
= EavesdropC (Modules address) (Eff
( InterposeC (Resumable (BaseError (UnspecializedError value))) (Eff
( ErrorC (LoopControl address) (Eff
( ErrorC (Return address) (Eff
( EnvC address (Eff
( ScopeEnvC address (Eff
( DerefC address value (Eff
( AllocatorC address (Eff
( ReaderC ModuleInfo (Eff
m)))))))))))))))))
type ValueC term address value m
= FunctionC term address value (Eff
@ -110,7 +112,7 @@ evaluate :: ( AbstractValue term address value valueC
, booleanC ~ BooleanC value (Eff moduleC)
, Carrier (Boolean value :+: moduleSig) booleanC
, whileC ~ WhileC value (Eff booleanC)
, moduleSig ~ (Eavesdrop (Modules address) :+: Error (LoopControl address) :+: Error (Return address) :+: Env address :+: ScopeEnv address :+: Deref value :+: Allocator address :+: Reader ModuleInfo :+: sig)
, moduleSig ~ (Eavesdrop (Modules address) :+: Interpose (Resumable (BaseError (UnspecializedError value))) :+: Error (LoopControl address) :+: Error (Return address) :+: Env address :+: ScopeEnv address :+: Deref value :+: Allocator address :+: Reader ModuleInfo :+: sig)
, Carrier (While value :+: Boolean value :+: moduleSig) whileC
, Carrier (Function term address value :+: While value :+: Boolean value :+: moduleSig) valueC
, Declarations term
@ -170,6 +172,7 @@ evaluate lang analyzeModule analyzeTerm modules = do
. runEnv (EvalContext Nothing (X.push (newEnv preludeBinds)))
. runReturn
. runLoopControl
. raiseHandler runInterpose
. raiseHandler runEavesdrop

View File

@ -10,7 +10,7 @@ module Data.Abstract.Value.Concrete
import qualified Control.Abstract as Abstract
import Control.Abstract hiding (Boolean(..), Function(..), While(..))
import Control.Effect.Carrier
import Control.Effect.Internal
import Control.Effect.Interpose
import Control.Effect.Sum
import Data.Abstract.BaseError
import Data.Abstract.Evaluatable (UnspecializedError(..))
@ -129,10 +129,10 @@ instance ( Carrier sig m
, Member (Deref (Value term address)) sig
, Member (Abstract.Boolean (Value term address)) sig
, Member (Error (LoopControl address)) sig
, Member (Interpose (Resumable (BaseError (UnspecializedError (Value term address))))) sig
, Member (Reader ModuleInfo) sig
, Member (Reader Span) sig
, Member (Resumable (BaseError (AddressError address (Value term address)))) sig
, Member (Resumable (BaseError (UnspecializedError (Value term address)))) sig
, Member (State (Heap address (Value term address))) sig
, Ord address
, Show address
@ -142,15 +142,16 @@ instance ( Carrier sig m
ret = WhileC . ret
eff = WhileC . (alg \/ eff . handleCoercible)
where alg = \case
Abstract.While cond body k -> interpose @(Resumable (BaseError (UnspecializedError (Value term address))))
(\(Resumable (BaseError _ _ (UnspecializedError _)) _) -> throwError (Abort @address)) (runEvaluator (loop (\continue -> do
Abstract.While cond body k -> interpose @(Resumable (BaseError (UnspecializedError (Value term address)))) (runEvaluator (loop (\continue -> do
cond' <- Evaluator (runWhileC cond)
-- `interpose` is used to handle 'UnspecializedError's and abort out of the
-- loop, otherwise under concrete semantics we run the risk of the
-- conditional always being true and getting stuck in an infinite loop.
ifthenelse cond' (Evaluator (runWhileC body) *> continue) (pure Unit)))) >>= runWhileC . k
ifthenelse cond' (Evaluator (runWhileC body) *> continue) (pure Unit))))
(\(Resumable (BaseError _ _ (UnspecializedError _)) _) -> throwError (Abort @address))
>>= runWhileC . k
where
loop x = catchLoopControl @address (fix x) $ \case
Break value -> deref value
@ -161,27 +162,6 @@ instance ( Carrier sig m
Continue _ -> loop x
interpose :: (Member eff sig, HFunctor eff, Carrier sig m)
=> (forall v. eff (Eff m) (Eff m v) -> Eff m v)
-> Eff m a
-> Eff m a
interpose handler = runInterposeC handler . interpret . upcast
upcast :: Eff m a -> Eff (InterposeC eff (Eff m)) a
upcast m = Eff (\ k -> InterposeC (\ f -> m >>= runInterposeC f . k))
newtype InterposeC eff m a = InterposeC ((forall x . eff m (m x) -> m x) -> m a)
runInterposeC :: (forall x . eff m (m x) -> m x) -> InterposeC eff m a -> m a
runInterposeC f (InterposeC m) = m f
instance (Member eff sig, HFunctor eff, Carrier sig m) => Carrier sig (InterposeC eff m) where
ret a = InterposeC (const (ret a))
eff op
| Just e <- prj op = InterposeC (\ handler -> handler (handlePure (runInterposeC handler) e))
| otherwise = InterposeC (\ handler -> eff (handlePure (runInterposeC handler) op))
instance AbstractHole (Value term address) where
hole = Hole

@ -1 +1 @@
Subproject commit fb972ef13e529cf0a5ead67c22f69a4e63472ae2
Subproject commit 9678e1d5325392a23b57a47ddc7a52a5250fb304