1
1
mirror of https://github.com/github/semantic.git synced 2024-12-20 05:11:44 +03:00

WIP - implement while/looping as an effect

This commit is contained in:
Timothy Clem 2018-09-19 15:00:51 -07:00
parent 4016c6f3d8
commit 0341f21901
8 changed files with 142 additions and 45 deletions

View File

@ -16,6 +16,7 @@ module Control.Abstract.Value
, while
, doWhile
, forLoop
, While(..)
, makeNamespace
, evaluateInScopedEnv
, address
@ -36,7 +37,7 @@ import Data.Abstract.Number as Number
import Data.Abstract.Ref
import Data.Scientific (Scientific)
import Data.Span
import Prologue hiding (TypeError)
import Prologue hiding (TypeError, catchError)
-- | This datum is passed into liftComparison to handle the fact that Ruby and PHP
-- have built-in generalized-comparison ("spaceship") operators. If you want to
@ -102,6 +103,58 @@ instance PureEffect (Boolean value) where
handle handler (Request (AsBool v) k) = Request (AsBool v) (handler . k)
handle handler (Request (Disjunction a b) k) = Request (Disjunction (handler a) (handler b)) (handler . k)
-- | The fundamental looping primitive, built on top of 'ifthenelse'.
while :: Member (While value) effects
=> Evaluator address value effects value -- ^ Condition
-> Evaluator address value effects value -- ^ Body
-> Evaluator address value effects value
while (Evaluator cond) (Evaluator body) = send (While cond body)
-- | Do-while loop, built on top of while.
doWhile :: (AbstractValue address value effects, Member (Boolean value) effects)
=> Evaluator address value effects value
-> Evaluator address value effects value
-> Evaluator address value effects value
doWhile body cond = undefined
-- | C-style for loops.
forLoop :: ( AbstractValue address value effects
, Member (Boolean value) effects
, Member (While value) effects
, Member (Env address) effects
)
=> Evaluator address value effects value -- ^ Initial statement
-> Evaluator address value effects value -- ^ Condition
-> Evaluator address value effects value -- ^ Increment/stepper
-> Evaluator address value effects value -- ^ Body
-> Evaluator address value effects value
forLoop initial cond step body =
locally (initial *> while cond (body *> step))
-- -- | The fundamental looping primitive, built on top of 'ifthenelse'.
-- while :: (AbstractValue address value effects, Member (Boolean value) effects)
-- => Evaluator address value effects value
-- -> Evaluator address value effects value
-- -> Evaluator address value effects value
-- while cond body = loop $ \ continue -> do
-- this <- cond
-- ifthenelse this (body *> continue) (pure unit)
--
-- -- | Do-while loop, built on top of while.
-- doWhile :: (AbstractValue address value effects, Member (Boolean value) effects)
-- => Evaluator address value effects value
-- -> Evaluator address value effects value
-- -> Evaluator address value effects value
-- doWhile body cond = loop $ \ continue -> body *> do
-- this <- cond
-- ifthenelse this continue (pure unit)
data While value m result where
While :: m value -> m value -> While value m value
instance PureEffect (While value) where
handle handler (Request (While cond body) k) = Request (While (handler cond) (handler body)) (handler . k)
class Show value => AbstractIntro value where
-- | Construct an abstract unit value.
@ -210,37 +263,6 @@ class AbstractIntro value => AbstractValue address value effects where
loop :: (Evaluator address value effects value -> Evaluator address value effects value) -> Evaluator address value effects value
-- | C-style for loops.
forLoop :: ( AbstractValue address value effects
, Member (Boolean value) effects
, Member (Env address) effects
)
=> Evaluator address value effects value -- ^ Initial statement
-> Evaluator address value effects value -- ^ Condition
-> Evaluator address value effects value -- ^ Increment/stepper
-> Evaluator address value effects value -- ^ Body
-> Evaluator address value effects value
forLoop initial cond step body =
locally (initial *> while cond (body *> step))
-- | The fundamental looping primitive, built on top of 'ifthenelse'.
while :: (AbstractValue address value effects, Member (Boolean value) effects)
=> Evaluator address value effects value
-> Evaluator address value effects value
-> Evaluator address value effects value
while cond body = loop $ \ continue -> do
this <- cond
ifthenelse this (body *> continue) (pure unit)
-- | Do-while loop, built on top of while.
doWhile :: (AbstractValue address value effects, Member (Boolean value) effects)
=> Evaluator address value effects value
-> Evaluator address value effects value
-> Evaluator address value effects value
doWhile body cond = loop $ \ continue -> body *> do
this <- cond
ifthenelse this continue (pure unit)
makeNamespace :: ( AbstractValue address value effects
, Member (Deref value) effects
, Member (Env address) effects

View File

@ -27,7 +27,7 @@ import Control.Abstract.Environment as X hiding (runEnvironmentError, runEnviron
import Control.Abstract.Evaluator as X hiding (LoopControl(..), Return(..), catchLoopControl, runLoopControl, catchReturn, runReturn)
import Control.Abstract.Heap as X hiding (runAddressError, runAddressErrorWith)
import Control.Abstract.Modules as X (Modules, ModuleResult, ResolutionError(..), load, lookupModule, listModulesInDir, require, resolve, throwResolutionError)
import Control.Abstract.Value as X hiding (Boolean(..), Function(..))
import Control.Abstract.Value as X hiding (Boolean(..), Function(..), While(..))
import Control.Abstract.ScopeGraph
import Data.Abstract.Declarations as X
import Data.Abstract.Environment as X
@ -53,6 +53,7 @@ class (Show1 constr, Foldable constr) => Evaluatable constr where
, FreeVariables term
, Member (Allocator address) effects
, Member (Boolean value) effects
, Member (While value) effects
, Member (Deref value) effects
, Member (ScopeEnv address) effects
, Member (Env address) effects
@ -93,6 +94,7 @@ type ModuleEffects address value rest
type ValueEffects address value rest
= Function address value
': While value
': Boolean value
': rest

View File

@ -3,6 +3,7 @@ module Data.Abstract.Value.Abstract
( Abstract (..)
, runFunction
, runBoolean
, runWhile
) where
import Control.Abstract as Abstract
@ -50,6 +51,23 @@ runBoolean = interpret $ \case
AsBool _ -> pure True <|> pure False
Disjunction a b -> runBoolean (Evaluator (a <|> b))
runWhile ::
( Member (Allocator address) effects
, Member (Deref Abstract) effects
, Member (Env address) effects
, Member (Exc (Return address)) effects
, Member Fresh effects
, Member (Reader ModuleInfo) effects
, Member (Reader Span) effects
, Member (Resumable (BaseError (AddressError address Abstract))) effects
, Member (State (Heap address Abstract)) effects
, Ord address
, PureEffects effects
)
=> Evaluator address Abstract (While Abstract ': effects) a
-> Evaluator address Abstract effects a
runWhile = undefined
instance Ord address => ValueRoots address Abstract where
valueRoots = mempty

View File

@ -1,18 +1,20 @@
{-# LANGUAGE GADTs, RankNTypes, TypeOperators, UndecidableInstances, LambdaCase #-}
{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables, UndecidableInstances, LambdaCase #-}
module Data.Abstract.Value.Concrete
( Value (..)
, ValueError (..)
, ClosureBody (..)
, runFunction
, runBoolean
, runWhile
, materializeEnvironment
, runValueError
, runValueErrorWith
) where
import qualified Control.Abstract as Abstract
import Control.Abstract hiding (Boolean(..), Function(..))
import Control.Abstract hiding (Boolean(..), Function(..), While(..))
import Data.Abstract.BaseError
import Data.Abstract.Evaluatable (UnspecializedError)
import Data.Abstract.Environment (Environment, Bindings, EvalContext(..))
import qualified Data.Abstract.Environment as Env
import Data.Abstract.Name
@ -24,7 +26,7 @@ import Data.Scientific (Scientific, coefficient, normalize)
import Data.Scientific.Exts
import qualified Data.Set as Set
import Data.Word
import Prologue
import Prologue hiding (catchError)
data Value address body
= Closure PackageInfo ModuleInfo (Maybe Name) [Name] (ClosureBody address body) (Environment address)
@ -116,6 +118,39 @@ runBoolean = interpret $ \case
if a'' then pure a' else runBoolean (Evaluator b)
runWhile :: forall effects address body a .
( PureEffects effects
, Member (Deref (Value address body)) effects
, Member (Abstract.Boolean (Value address body)) effects
, Member (Exc (LoopControl address)) effects
, Member (Reader ModuleInfo) effects
, Member (Reader Span) effects
, Member (Resumable (BaseError (AddressError address (Value address body)))) effects
, Member (Resumable (BaseError (ValueError address body))) effects
, Member (Resumable (BaseError (UnspecializedError (Value address body)))) effects
, Member (State (Heap address (Value address body))) effects
, Ord address
, Show address
)
=> Evaluator address (Value address body) (Abstract.While (Value address body) ': effects) a
-> Evaluator address (Value address body) effects a
runWhile = interpret $ \case
Abstract.While cond body -> loop $ \continue -> do
cond' <- runWhile (raiseEff cond)
-- let body' = interpose @(Resumable (BaseError (UnspecializedError (Value address body)))) (\(Resumable _) -> pure hole) $
-- runWhile (raiseEff body) *> continue
let body' = (runWhile (raiseEff body) *> continue) `catchError` (\_ -> pure unit)
-- let body' = runWhile (raiseEff body) *> continue
ifthenelse cond' body' (pure unit)
where
loop x = catchLoopControl (fix x) (\ control -> case control of
Break value -> deref value
-- FIXME: Figure out how to deal with this. Ruby treats this as the result
-- of the current block iteration, while PHP specifies a breakout level
-- and TypeScript appears to take a label.
Continue _ -> loop x)
instance AbstractHole (Value address body) where
hole = Hole

View File

@ -8,10 +8,11 @@ module Data.Abstract.Value.Type
, unify
, runFunction
, runBoolean
, runWhile
) where
import qualified Control.Abstract as Abstract
import Control.Abstract hiding (Boolean(..), Function(..), raiseHandler)
import Control.Abstract hiding (Boolean(..), Function(..), While(..), raiseHandler)
import Control.Monad.Effect.Internal (raiseHandler)
import Data.Abstract.Environment as Env
import Data.Abstract.BaseError
@ -277,6 +278,25 @@ runBoolean = interpret $ \case
Abstract.Disjunction t1 t2 -> (runBoolean (Evaluator t1) >>= unify Bool) <|> (runBoolean (Evaluator t2) >>= unify Bool)
runWhile ::
( Member (Allocator address) effects
, Member (Deref Type) effects
, Member (Env address) effects
, Member (Exc (Return address)) effects
, Member Fresh effects
, Member (Reader ModuleInfo) effects
, Member (Reader Span) effects
, Member (Resumable (BaseError TypeError)) effects
, Member (Resumable (BaseError (AddressError address Type))) effects
, Member (State (Heap address Type)) effects
, Member (State TypeMap) effects
, Ord address
, PureEffects effects
)
=> Evaluator address Type (Abstract.While Type ': effects) a
-> Evaluator address Type effects a
runWhile = undefined
instance AbstractHole Type where
hole = Hole

View File

@ -42,7 +42,7 @@ import qualified Data.Abstract.ModuleTable as ModuleTable
import Data.Abstract.Package as Package
import Data.Abstract.Value.Abstract as Abstract
import Data.Abstract.Value.Concrete as Concrete
(Value, ValueError (..), runBoolean, runFunction, runValueErrorWith)
(Value, ValueError (..), runWhile, runBoolean, runFunction, runValueErrorWith)
import Data.Abstract.Value.Type as Type
import Data.Blob
import Data.Coerce
@ -130,7 +130,7 @@ runCallGraph lang includePackages modules package = do
runAddressEffects
= Hole.runAllocator (Located.handleAllocator Monovariant.handleAllocator)
. Hole.runDeref (Located.handleDeref Monovariant.handleDeref)
extractGraph <$> runEvaluator (runGraphAnalysis (evaluate lang analyzeModule analyzeTerm runAddressEffects (Abstract.runBoolean . Abstract.runFunction) modules))
extractGraph <$> runEvaluator (runGraphAnalysis (evaluate lang analyzeModule analyzeTerm runAddressEffects (Abstract.runBoolean . Abstract.runWhile . Abstract.runFunction) modules))
runImportGraphToModuleInfos :: ( Declarations term
, Evaluatable (Base term)
@ -198,7 +198,7 @@ runImportGraph lang (package :: Package term) f =
runAddressEffects
= Hole.runAllocator Precise.handleAllocator
. Hole.runDeref Precise.handleDeref
in extractGraph <$> runEvaluator (runImportGraphAnalysis (evaluate lang analyzeModule id runAddressEffects (Concrete.runBoolean . Concrete.runFunction coerce coerce) (ModuleTable.toPairs (packageModules package) >>= toList . snd)))
in extractGraph <$> runEvaluator (runImportGraphAnalysis (evaluate lang analyzeModule id runAddressEffects (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) (ModuleTable.toPairs (packageModules package) >>= toList . snd)))
type ConcreteEffects address rest
= Reader Span
@ -285,7 +285,7 @@ parsePythonPackage parser project = do
strat <- case find ((== (projectRootDir project </> "setup.py")) . filePath) (projectFiles project) of
Just setupFile -> do
setupModule <- fmap snd <$> parseModule project parser setupFile
fst <$> runAnalysis (evaluate (Proxy @'Language.Python) id id runAddressEffects (Concrete.runBoolean . Concrete.runFunction coerce coerce . runPythonPackaging) [ setupModule ])
fst <$> runAnalysis (evaluate (Proxy @'Language.Python) id id runAddressEffects (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce . runPythonPackaging) [ setupModule ])
Nothing -> pure PythonPackage.Unknown
case strat of
PythonPackage.Unknown -> do

View File

@ -106,7 +106,7 @@ repl proxy parser paths = defaultConfig debugOptions >>= \ config -> runM . runD
. runReader (packageInfo package)
. runState (lowerBound @Span)
. runReader (lowerBound @Span)
$ evaluate proxy id (withTermSpans . step (fmap (\ (x:|_) -> moduleBody x) <$> ModuleTable.toPairs (packageModules (fst <$> package)))) (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runFunction coerce coerce) modules
$ evaluate proxy id (withTermSpans . step (fmap (\ (x:|_) -> moduleBody x) <$> ModuleTable.toPairs (packageModules (fst <$> package)))) (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) modules
-- TODO: REPL for typechecking/abstract semantics
-- TODO: drive the flow from within the REPL instead of from without

View File

@ -108,7 +108,7 @@ evaluateProject' (TaskConfig config logger statter) proxy parser paths = either
(runReader (packageInfo package)
(runState (lowerBound @Span)
(runReader (lowerBound @Span)
(evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runFunction coerce coerce) modules)))))))
(evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) modules)))))))
evaluatePythonProjects proxy parser lang path = runTaskWithOptions debugOptions $ do
project <- readProject Nothing path lang []
@ -121,7 +121,7 @@ evaluatePythonProjects proxy parser lang path = runTaskWithOptions debugOptions
(runReader (packageInfo package)
(runState (lowerBound @Span)
(runReader (lowerBound @Span)
(evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runFunction coerce coerce) modules)))))))
(evaluate proxy id withTermSpans (Precise.runAllocator . Precise.runDeref) (Concrete.runBoolean . Concrete.runWhile . Concrete.runFunction coerce coerce) modules)))))))
evaluateProjectWithCaching proxy parser path = runTaskWithOptions debugOptions $ do
@ -133,7 +133,7 @@ evaluateProjectWithCaching proxy parser path = runTaskWithOptions debugOptions $
(runReader (lowerBound @Span)
(runReader (lowerBound @(ModuleTable (NonEmpty (Module (ModuleResult Monovariant)))))
(raiseHandler (runModules (ModuleTable.modulePaths (packageModules package)))
(evaluate proxy id withTermSpans (Monovariant.runAllocator . Monovariant.runDeref) (Type.runBoolean . Type.runFunction) modules))))))
(evaluate proxy id withTermSpans (Monovariant.runAllocator . Monovariant.runDeref) (Type.runBoolean . Type.runWhile . Type.runFunction) modules))))))
parseFile :: Parser term -> FilePath -> IO term