1
1
mirror of https://github.com/github/semantic.git synced 2024-12-30 02:14:20 +03:00

Deal with the fallout of Evaluator changes in Value.

This commit is contained in:
Rob Rix 2018-05-04 18:40:59 -04:00
parent af7d178183
commit 488ef67c26
3 changed files with 111 additions and 101 deletions

View File

@ -1,6 +1,6 @@
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, Rank2Types #-}
module Control.Abstract.Value
( MonadValue(..)
( AbstractValue(..)
, AbstractHole(..)
, Comparator(..)
, while
@ -25,7 +25,7 @@ import Prologue hiding (TypeError)
-- | 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
-- encapsulate a traditional, boolean-returning operator, wrap it in 'Concrete';
-- if you want the generalized comparator, pass in 'Generalized'. In MonadValue
-- if you want the generalized comparator, pass in 'Generalized'. In 'AbstractValue'
-- instances, you can then then handle the different cases to return different
-- types, if that's what you need.
data Comparator
@ -38,151 +38,154 @@ class AbstractHole value where
-- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
--
-- This allows us to abstract the choice of whether to evaluate under binders for different value types.
class (Monad (m effects), Show value) => MonadValue location value (effects :: [* -> *]) m | m effects value -> location where
class Show value => AbstractValue location term value (effects :: [* -> *]) | effects value -> location where
-- | Construct an abstract unit value.
-- TODO: This might be the same as the empty tuple for some value types
unit :: m effects value
unit :: Evaluator location term value effects value
-- | Construct an abstract integral value.
integer :: Prelude.Integer -> m effects value
integer :: Prelude.Integer -> Evaluator location term value effects value
-- | Lift a unary operator over a 'Num' to a function on 'value's.
liftNumeric :: (forall a . Num a => a -> a)
-> (value -> m effects value)
-> (value -> Evaluator location term value effects value)
-- | Lift a pair of binary operators to a function on 'value's.
-- You usually pass the same operator as both arguments, except in the cases where
-- Haskell provides different functions for integral and fractional operations, such
-- as division, exponentiation, and modulus.
liftNumeric2 :: (forall a b. Number a -> Number b -> SomeNumber)
-> (value -> value -> m effects value)
-> (value -> value -> Evaluator location term value effects value)
-- | Lift a Comparator (usually wrapping a function like == or <=) to a function on values.
liftComparison :: Comparator -> (value -> value -> m effects value)
liftComparison :: Comparator -> (value -> value -> Evaluator location term value effects value)
-- | Lift a unary bitwise operator to values. This is usually 'complement'.
liftBitwise :: (forall a . Bits a => a -> a)
-> (value -> m effects value)
-> (value -> Evaluator location term value effects value)
-- | Lift a binary bitwise operator to values. The Integral constraint is
-- necessary to satisfy implementation details of Haskell left/right shift,
-- but it's fine, since these are only ever operating on integral values.
liftBitwise2 :: (forall a . (Integral a, Bits a) => a -> a -> a)
-> (value -> value -> m effects value)
-> (value -> value -> Evaluator location term value effects value)
-- | Construct an abstract boolean value.
boolean :: Bool -> m effects value
boolean :: Bool -> Evaluator location term value effects value
-- | Construct an abstract string value.
string :: ByteString -> m effects value
string :: ByteString -> Evaluator location term value effects value
-- | Construct a self-evaluating symbol value.
-- TODO: Should these be interned in some table to provide stronger uniqueness guarantees?
symbol :: ByteString -> m effects value
symbol :: ByteString -> Evaluator location term value effects value
-- | Construct a floating-point value.
float :: Scientific -> m effects value
float :: Scientific -> Evaluator location term value effects value
-- | Construct a rational value.
rational :: Prelude.Rational -> m effects value
rational :: Prelude.Rational -> Evaluator location term value effects value
-- | Construct an N-ary tuple of multiple (possibly-disjoint) values
multiple :: [value] -> m effects value
multiple :: [value] -> Evaluator location term value effects value
-- | Construct an array of zero or more values.
array :: [value] -> m effects value
array :: [value] -> Evaluator location term value effects value
-- | Construct a key-value pair for use in a hash.
kvPair :: value -> value -> m effects value
kvPair :: value -> value -> Evaluator location term value effects value
-- | Extract the contents of a key-value pair as a tuple.
asPair :: value -> m effects (value, value)
asPair :: value -> Evaluator location term value effects (value, value)
-- | Construct a hash out of pairs.
hash :: [(value, value)] -> m effects value
hash :: [(value, value)] -> Evaluator location term value effects value
-- | Extract a 'ByteString' from a given value.
asString :: value -> m effects ByteString
asString :: value -> Evaluator location term value effects ByteString
-- | Eliminate boolean values. TODO: s/boolean/truthy
ifthenelse :: value -> m effects value -> m effects value -> m effects value
ifthenelse :: value -> Evaluator location term value effects value -> Evaluator location term value effects value -> Evaluator location term value effects value
-- | Extract a 'Bool' from a given value.
asBool :: value -> m effects Bool
asBool :: value -> Evaluator location term value effects Bool
-- | Construct the nil/null datatype.
null :: m effects value
null :: Evaluator location term value effects value
-- | @index x i@ computes @x[i]@, with zero-indexing.
index :: value -> value -> m effects value
index :: value -> value -> Evaluator location term value effects value
-- | Determine whether the given datum is a 'Hole'.
isHole :: value -> m effects Bool
isHole :: value -> Evaluator location term value effects Bool
-- | Build a class value from a name and environment.
klass :: Name -- ^ The new class's identifier
-> [value] -- ^ A list of superclasses
-> Environment location value -- ^ The environment to capture
-> m effects value
-> Evaluator location term value effects value
-- | Build a namespace value from a name and environment stack
--
-- Namespaces model closures with monoidal environments.
namespace :: Name -- ^ The namespace's identifier
-> Environment location value -- ^ The environment to mappend
-> m effects value
-> Evaluator location term value effects value
-- | Extract the environment from any scoped object (e.g. classes, namespaces, etc).
scopedEnvironment :: value -> m effects (Maybe (Environment location value))
scopedEnvironment :: value -> Evaluator location term value effects (Maybe (Environment location value))
-- | Evaluate an abstraction (a binder like a lambda or method definition).
lambda :: (FreeVariables term, MonadEvaluator location term value effects m) => [Name] -> Subterm term (m effects value) -> m effects value
lambda :: FreeVariables term => [Name] -> Subterm term (Evaluator location term value effects value) -> Evaluator location term value effects value
-- | Evaluate an application (like a function call).
call :: value -> [m effects value] -> m effects value
call :: value -> [Evaluator location term value effects value] -> Evaluator location term value effects value
-- | Primitive looping combinator, approximately equivalent to 'fix'. This should be used in place of direct recursion, as it allows abstraction over recursion.
--
-- The function argument takes an action which recurs through the loop.
loop :: (m effects value -> m effects value) -> m effects value
loop :: (Evaluator location term value effects value -> Evaluator location term value effects value) -> Evaluator location term value effects value
-- | Attempt to extract a 'Prelude.Bool' from a given value.
forLoop :: (MonadEvaluator location term value effects m, MonadValue location value effects m)
=> m effects value -- ^ Initial statement
-> m effects value -- ^ Condition
-> m effects value -- ^ Increment/stepper
-> m effects value -- ^ Body
-> m effects value
forLoop :: ( AbstractValue location term value effects
, Member (State (Environment location value)) effects
)
=> Evaluator location term value effects value -- ^ Initial statement
-> Evaluator location term value effects value -- ^ Condition
-> Evaluator location term value effects value -- ^ Increment/stepper
-> Evaluator location term value effects value -- ^ Body
-> Evaluator location term value effects value
forLoop initial cond step body =
localize (initial *> while cond (body *> step))
-- | The fundamental looping primitive, built on top of ifthenelse.
while :: MonadValue location value effects m
=> m effects value
-> m effects value
-> m effects value
while :: AbstractValue location term value effects
=> Evaluator location term value effects value
-> Evaluator location term value effects value
-> Evaluator location term value effects value
while cond body = loop $ \ continue -> do
this <- cond
ifthenelse this (body *> continue) unit
-- | Do-while loop, built on top of while.
doWhile :: MonadValue location value effects m
=> m effects value
-> m effects value
-> m effects value
doWhile :: AbstractValue location term value effects
=> Evaluator location term value effects value
-> Evaluator location term value effects value
-> Evaluator location term value effects value
doWhile body cond = loop $ \ continue -> body *> do
this <- cond
ifthenelse this continue unit
makeNamespace :: ( MonadValue location value effects m
, MonadEvaluator location term value effects m
makeNamespace :: ( AbstractValue location term value effects
, Member (State (Environment location value)) effects
, Member (State (Heap location value)) effects
, Ord location
, Reducer value (Cell location value)
)
=> Name
-> Address location value
-> Maybe value
-> m effects value
-> Evaluator location term value effects value
makeNamespace name addr super = do
superEnv <- maybe (pure (Just lowerBound)) scopedEnvironment super
let env' = fromMaybe lowerBound superEnv

View File

@ -1,12 +1,14 @@
{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the MonadValue instance, which requires MonadEvaluator to resolve its functional dependency.
module Data.Abstract.Type
( Type (..)
, TypeError (..)
, unify
) where
import Control.Abstract.Analysis
import Control.Abstract.Addressable
import Control.Abstract.Evaluator
import Control.Abstract.Value
import Control.Effect (Effectful(..), throwResumable)
import Data.Abstract.Address
import Data.Abstract.Environment as Env
import Data.Align (alignWith)
@ -17,31 +19,31 @@ import Prologue hiding (TypeError)
type TName = Int
-- | A datatype representing primitive types and combinations thereof.
data Type
= Int -- ^ Primitive int type.
| Bool -- ^ Primitive boolean type.
| String -- ^ Primitive string type.
| Symbol -- ^ Type of unique symbols.
| Unit -- ^ The unit type.
| Float -- ^ Floating-point type.
| Rational -- ^ Rational type.
| Type :-> Type -- ^ Binary function types.
| Var TName -- ^ A type variable.
| Product [Type] -- ^ N-ary products.
| Array [Type] -- ^ Arrays. Note that this is heterogenous.
| Hash [(Type, Type)] -- ^ Heterogenous key-value maps.
| Object -- ^ Objects. Once we have some notion of inheritance we'll need to store a superclass.
| Null -- ^ The null type. Unlike 'Unit', this unifies with any other type.
| Hole -- ^ The hole type.
data Type location
= Int -- ^ Primitive int type.
| Bool -- ^ Primitive boolean type.
| String -- ^ Primitive string type.
| Symbol -- ^ Type of unique symbols.
| Unit -- ^ The unit type.
| Float -- ^ Floating-point type.
| Rational -- ^ Rational type.
| Type location :-> Type location -- ^ Binary function types.
| Var TName -- ^ A type variable.
| Product [Type location] -- ^ N-ary products.
| Array [Type location] -- ^ Arrays. Note that this is heterogenous.
| Hash [(Type location, Type location)] -- ^ Heterogenous key-value maps.
| Object -- ^ Objects. Once we have some notion of inheritance we'll need to store a superclass.
| Null -- ^ The null type. Unlike 'Unit', this unifies with any other type.
| Hole -- ^ The hole type.
deriving (Eq, Ord, Show)
-- TODO: À la carte representation of types.
data TypeError resume where
NumOpError :: Type -> Type -> TypeError Type
BitOpError :: Type -> Type -> TypeError Type
UnificationError :: Type -> Type -> TypeError Type
SubscriptError :: Type -> Type -> TypeError Type
NumOpError :: Type location -> Type location -> TypeError (Type location)
BitOpError :: Type location -> Type location -> TypeError (Type location)
UnificationError :: Type location -> Type location -> TypeError (Type location)
SubscriptError :: Type location -> Type location -> TypeError (Type location)
deriving instance Show (TypeError resume)
@ -52,13 +54,13 @@ instance Show1 TypeError where
liftShowsPrec _ _ _ (SubscriptError l r) = showString "SubscriptError " . shows [l, r]
instance Eq1 TypeError where
liftEq _ (BitOpError a b) (BitOpError c d) = a == c && b == d
liftEq _ (NumOpError a b) (NumOpError c d) = a == c && b == d
liftEq _ (UnificationError a b) (UnificationError c d) = a == c && b == d
liftEq eq (BitOpError a b) (BitOpError c d) = a `eq` c && b `eq` d
liftEq eq (NumOpError a b) (NumOpError c d) = a `eq` c && b `eq` d
liftEq eq (UnificationError a b) (UnificationError c d) = a `eq` c && b `eq` d
liftEq _ _ _ = False
-- | Unify two 'Type's.
unify :: (Effectful m, Applicative (m effects), Member (Resumable TypeError) effects) => Type -> Type -> m effects Type
unify :: (Effectful m, Applicative (m effects), Member (Resumable TypeError) effects) => Type location -> Type location -> m effects (Type location)
unify (a1 :-> b1) (a2 :-> b2) = (:->) <$> unify a1 a2 <*> unify b1 b2
unify a Null = pure a
unify Null b = pure b
@ -70,22 +72,24 @@ unify t1 t2
| t1 == t2 = pure t2
| otherwise = throwResumable (UnificationError t1 t2)
instance Ord location => ValueRoots location Type where
instance Ord location => ValueRoots location (Type location) where
valueRoots _ = mempty
instance AbstractHole Type where
instance AbstractHole (Type location) where
hole = Hole
-- | Discard the value arguments (if any), constructing a 'Type' instead.
instance ( Alternative (m effects)
, Member Fresh effects
, Member (Resumable TypeError) effects
, MonadAddressable location effects m
, MonadEvaluator location term Type effects m
, Reducer Type (Cell location Type)
instance ( Addressable location effects
, Members '[ Fresh
, NonDet
, Resumable TypeError
, State (Environment location (Type location))
, State (Heap location (Type location))
] effects
, Reducer (Type location) (Cell location (Type location))
)
=> MonadValue location Type effects m where
=> AbstractValue location term (Type location) effects where
lambda names (Subterm _ body) = do
(env, tvars) <- foldr (\ name rest -> do
a <- alloc name

View File

@ -4,7 +4,6 @@ module Data.Abstract.Value where
import Control.Abstract.Addressable
import Control.Abstract.Evaluator
import Control.Abstract.Value
import Control.Effect
import Data.Abstract.Address
import Data.Abstract.Environment (Environment, emptyEnv, mergeEnvs)
import qualified Data.Abstract.Environment as Env
@ -182,7 +181,7 @@ instance Show1 KVPair where liftShowsPrec = genericLiftShowsPrec
-- You would be incorrect, as we can't derive a Generic1 instance for the above,
-- and in addition a 'Map' representation would lose information given hash literals
-- that assigned multiple values to one given key. Instead, this holds KVPair
-- values. The smart constructor for hashes in MonadValue ensures that these are
-- values. The smart constructor for hashes in 'AbstractValue' ensures that these are
-- only populated with pairs.
newtype Hash value = Hash [value]
deriving (Eq, Generic1, Ord, Show)
@ -209,20 +208,24 @@ instance AbstractHole (Value location) where
hole = injValue Hole
-- | Construct a 'Value' wrapping the value arguments (if any).
instance ( Member (EvalClosure term (Value location)) effects
, Member Fail effects
, Member (LoopControl (Value location)) effects
, Member (Resumable (AddressError location (Value location))) effects
, Member (Resumable (ValueError location (Value location))) effects
, Member (Return (Value location)) effects
, Monad (m effects)
, MonadAddressable location effects m
, MonadEvaluator location term (Value location) effects m
instance ( Addressable location effects
, Members '[ EvalClosure term (Value location)
, Fail
, LoopControl (Value location)
, Reader (Environment location (Value location))
, Reader (SomeOrigin term)
, Resumable (AddressError location (Value location))
, Resumable (ValueError location (Value location))
, Return (Value location)
, State (Environment location (Value location))
, State (Heap location (Value location))
, State (JumpTable term)
] effects
, Recursive term
, Reducer (Value location) (Cell location (Value location))
, Show location
)
=> MonadValue location (Value location) effects m where
=> AbstractValue location term (Value location) effects where
unit = pure . injValue $ Unit
integer = pure . injValue . Integer . Number.Integer
boolean = pure . injValue . Boolean
@ -310,7 +313,7 @@ instance ( Member (EvalClosure term (Value location)) effects
tentative x i j = attemptUnsafeArithmetic (x i j)
-- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
specialize :: Either ArithException Number.SomeNumber -> m effects (Value location)
specialize :: Either ArithException Number.SomeNumber -> Evaluator location term (Value location) effects (Value location)
specialize (Left exc) = throwValueError (ArithmeticError exc)
specialize (Right (Number.SomeNumber (Number.Integer i))) = integer i
specialize (Right (Number.SomeNumber (Number.Ratio r))) = rational r
@ -329,7 +332,7 @@ instance ( Member (EvalClosure term (Value location)) effects
where
-- Explicit type signature is necessary here because we're passing all sorts of things
-- to these comparison functions.
go :: Ord a => a -> a -> m effects (Value location)
go :: Ord a => a -> a -> Evaluator location term (Value location) effects (Value location)
go l r = case comparator of
Concrete f -> boolean (f l r)
Generalized -> integer (orderingToInt (compare l r))
@ -368,9 +371,9 @@ instance ( Member (EvalClosure term (Value location)) effects
localEnv (mergeEnvs bindings) (evalClosure body)
Nothing -> throwValueError (CallError op)
where
evalClosure term = handleReturn @m @(Value location) (\ (Return value) -> pure value) (evaluateClosureBody term)
evalClosure term = handleReturn @(Value location) (\ (Return value) -> pure value) (evaluateClosureBody term)
loop x = catchLoopControl @m @(Value location) (fix x) (\ control -> case control of
loop x = catchLoopControl @(Value location) (fix x) (\ control -> case control of
Break value -> pure value
Continue -> loop x)
@ -413,5 +416,5 @@ deriving instance (Show value) => Show (ValueError location value resume)
instance (Show value) => Show1 (ValueError location value) where
liftShowsPrec _ _ = showsPrec
throwValueError :: (Member (Resumable (ValueError location value)) effects, MonadEvaluator location term value effects m) => ValueError location value resume -> m effects resume
throwValueError :: Member (Resumable (ValueError location value)) effects => ValueError location value resume -> Evaluator location term value effects resume
throwValueError = throwResumable