mirror of
https://github.com/github/semantic.git
synced 2025-01-03 04:51:57 +03:00
Abstract Addressable over the evaluator.
This commit is contained in:
parent
590374884b
commit
06d24471f3
@ -34,9 +34,9 @@ type Evaluating t v
|
||||
--
|
||||
-- Looks up the term's name in the cache of evaluated modules first, returns a value if found, otherwise loads/evaluates the module.
|
||||
require :: ( AbstractFunction effects term v
|
||||
, Addressable (LocationFor v) effects
|
||||
, Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor v) v (Evaluator effects term v)
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
@ -49,9 +49,9 @@ require term = getModuleTable >>= maybe (load term) pure . linkerLookup name
|
||||
--
|
||||
-- Always loads/evaluates.
|
||||
load :: ( AbstractFunction effects term v
|
||||
, Addressable (LocationFor v) effects
|
||||
, Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor v) v (Evaluator effects term v)
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
@ -74,9 +74,9 @@ moduleName term = let [n] = toList (freeVariables term) in BC.unpack n
|
||||
evaluate :: forall v term.
|
||||
( Ord (LocationFor v)
|
||||
, AbstractFunction (Evaluating term v) term v
|
||||
, Addressable (LocationFor v) (Evaluating term v)
|
||||
, Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor v) v (Evaluator (Evaluating term v) term v)
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
@ -88,9 +88,9 @@ evaluate = run @(Evaluating term v) . runEvaluator . foldSubterms eval
|
||||
evaluates :: forall v term.
|
||||
( Ord (LocationFor v)
|
||||
, AbstractFunction (Evaluating term v) term v
|
||||
, Addressable (LocationFor v) (Evaluating term v)
|
||||
, Evaluatable (Base term)
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor v) v (Evaluator (Evaluating term v) term v)
|
||||
, Recursive term
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
|
@ -12,7 +12,7 @@ import Data.Abstract.Linker
|
||||
import Data.Abstract.Value
|
||||
import Prelude hiding (fail)
|
||||
|
||||
class Monad m => MonadEvaluator term value m | m -> term, m -> value where
|
||||
class MonadFail m => MonadEvaluator term value m | m -> term, m -> value where
|
||||
getGlobalEnv :: m (EnvironmentFor value)
|
||||
modifyGlobalEnv :: (EnvironmentFor value -> EnvironmentFor value) -> m ()
|
||||
|
||||
|
@ -1,11 +1,10 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
|
||||
{-# LANGUAGE FunctionalDependencies, TypeFamilies, UndecidableInstances #-}
|
||||
module Control.Monad.Effect.Addressable where
|
||||
|
||||
import Analysis.Abstract.Evaluator
|
||||
import Control.Applicative
|
||||
import Control.Monad ((<=<))
|
||||
import Control.Monad.Effect.Fail
|
||||
import Control.Monad.Effect.NonDetEff
|
||||
import Data.Abstract.Address
|
||||
import Data.Abstract.Environment
|
||||
import Data.Abstract.FreeVariables
|
||||
@ -14,68 +13,65 @@ import Data.Abstract.Value
|
||||
import Data.Foldable (asum, toList)
|
||||
import Data.Pointed
|
||||
import Data.Semigroup
|
||||
import Data.Union
|
||||
import Prelude hiding (fail)
|
||||
|
||||
-- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Store.
|
||||
class (Ord l, Pointed (Cell l)) => Addressable l es where
|
||||
deref :: (l ~ LocationFor a)
|
||||
=> Address l a
|
||||
-> Evaluator es t a a
|
||||
class (Monad m, Ord l, Pointed (Cell l), l ~ LocationFor a) => MonadAddressable l a m | m -> a where
|
||||
deref :: Address l a
|
||||
-> m a
|
||||
|
||||
alloc :: (l ~ LocationFor a)
|
||||
=> Name
|
||||
-> Evaluator es t a (Address l a)
|
||||
alloc :: Name
|
||||
-> m (Address l a)
|
||||
|
||||
-- | Look up or allocate an address for a 'Name' free in a given term & assign it a given value, returning the 'Name' paired with the address.
|
||||
--
|
||||
-- The term is expected to contain one and only one free 'Name', meaning that care should be taken to apply this only to e.g. identifiers.
|
||||
lookupOrAlloc ::
|
||||
( FreeVariables t
|
||||
lookupOrAlloc :: ( FreeVariables t
|
||||
, MonadAddressable (LocationFor a) a m
|
||||
, MonadEvaluator t a m
|
||||
, Semigroup (Cell (LocationFor a) a)
|
||||
, Addressable (LocationFor a) es
|
||||
)
|
||||
=> t
|
||||
-> a
|
||||
-> Environment (LocationFor a) a
|
||||
-> Evaluator es t a (Name, Address (LocationFor a) a)
|
||||
-> m (Name, Address (LocationFor a) a)
|
||||
lookupOrAlloc term = let [name] = toList (freeVariables term) in
|
||||
lookupOrAlloc' name
|
||||
where
|
||||
-- | Look up or allocate an address for a 'Name' & assign it a given value, returning the 'Name' paired with the address.
|
||||
lookupOrAlloc' ::
|
||||
( Semigroup (Cell (LocationFor a) a)
|
||||
, Addressable (LocationFor a) es
|
||||
lookupOrAlloc' :: ( Semigroup (Cell (LocationFor a) a)
|
||||
, MonadAddressable (LocationFor a) a m
|
||||
, MonadEvaluator t a m
|
||||
)
|
||||
=> Name
|
||||
-> a
|
||||
-> Environment (LocationFor a) a
|
||||
-> Evaluator es t a (Name, Address (LocationFor a) a)
|
||||
-> m (Name, Address (LocationFor a) a)
|
||||
lookupOrAlloc' name v env = do
|
||||
a <- maybe (alloc name) pure (envLookup name env)
|
||||
assign a v
|
||||
pure (name, a)
|
||||
|
||||
-- | Write a value to the given 'Address' in the 'Store'.
|
||||
assign ::
|
||||
( Ord (LocationFor a)
|
||||
, Semigroup (Cell (LocationFor a) a)
|
||||
, Pointed (Cell (LocationFor a))
|
||||
)
|
||||
=> Address (LocationFor a) a
|
||||
-> a
|
||||
-> Evaluator es t a ()
|
||||
assign :: ( Ord (LocationFor a)
|
||||
, MonadEvaluator t a m
|
||||
, Pointed (Cell (LocationFor a))
|
||||
, Semigroup (Cell (LocationFor a) a)
|
||||
)
|
||||
=> Address (LocationFor a) a
|
||||
-> a
|
||||
-> m ()
|
||||
assign address = modifyStore . storeInsert address
|
||||
|
||||
|
||||
-- Instances
|
||||
|
||||
-- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
|
||||
instance Addressable Precise es where
|
||||
instance (Monad m, MonadEvaluator t v m, LocationFor v ~ Precise) => MonadAddressable Precise v m where
|
||||
deref = maybe uninitializedAddress (pure . unLatest) <=< flip fmap getStore . storeLookup
|
||||
where
|
||||
-- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
|
||||
uninitializedAddress :: Evaluator es t a b
|
||||
uninitializedAddress :: MonadFail m => m a
|
||||
uninitializedAddress = fail "uninitialized address"
|
||||
|
||||
alloc _ = fmap allocPrecise getStore
|
||||
@ -84,7 +80,7 @@ instance Addressable Precise es where
|
||||
|
||||
|
||||
-- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
|
||||
instance Member NonDetEff es => Addressable Monovariant es where
|
||||
instance (Alternative m, LocationFor v ~ Monovariant, Monad m, MonadEvaluator t v m) => MonadAddressable Monovariant v m where
|
||||
deref = asum . maybe [] (map pure . toList) <=< flip fmap getStore . storeLookup
|
||||
|
||||
alloc = pure . Address . Monovariant
|
||||
|
@ -34,8 +34,8 @@ import qualified Data.Union as U
|
||||
-- | The 'Evaluatable' class defines the necessary interface for a term to be evaluated. While a default definition of 'eval' is given, instances with computational content must implement 'eval' to perform their small-step operational semantics.
|
||||
class Evaluatable constr where
|
||||
eval :: ( AbstractFunction effects term value
|
||||
, Addressable (LocationFor value) effects
|
||||
, FreeVariables term
|
||||
, MonadAddressable (LocationFor value) value (Evaluator effects term value)
|
||||
, Ord (LocationFor value)
|
||||
, Semigroup (Cell (LocationFor value) value)
|
||||
)
|
||||
@ -77,9 +77,9 @@ class AbstractValue v => AbstractFunction effects t v | v -> t where
|
||||
abstract :: [Name] -> Subterm t (Evaluator effects t v v) -> Evaluator effects t v v
|
||||
apply :: v -> [Subterm t (Evaluator effects t v v)] -> Evaluator effects t v v
|
||||
|
||||
instance ( Addressable location effects
|
||||
, Evaluatable (Base t)
|
||||
instance ( Evaluatable (Base t)
|
||||
, FreeVariables t
|
||||
, MonadAddressable location (Value location t) (Evaluator effects t (Value location t))
|
||||
, Recursive t
|
||||
, Semigroup (Cell location (Value location t))
|
||||
)
|
||||
|
Loading…
Reference in New Issue
Block a user