Merge pull request #1519 from github/if-evaluation

Support ifthenelse evaluation

semantic.cabal

@@ -33,7 +33,7 @@ library
                      , Control.Abstract.Addressable
                      , Control.Abstract.Analysis
                      , Control.Abstract.Evaluator
-                     , Control.Abstract.Function
+                     , Control.Abstract.Value
                      -- Control flow
                      , Control.Effect
                      -- Effects used for program analysis

src/Analysis/Abstract/Dead.hs

@@ -29,13 +29,12 @@ type DeadCodeEffects t v
 
 -- | Run a dead code analysis of the given program.
 evaluateDead :: forall term value
-             .  ( AbstractValue value
-                , Corecursive term
+             .  ( Corecursive term
                 , Evaluatable (Base term)
                 , Foldable (Base term)
                 , FreeVariables term
                 , MonadAddressable (LocationFor value) value (DeadCodeAnalysis term value)
-                , MonadFunction term value (DeadCodeAnalysis term value)
+                , MonadValue term value (DeadCodeAnalysis term value)
                 , Ord (LocationFor value)
                 , Ord term
                 , Recursive term
@@ -70,12 +69,11 @@ revive :: Ord t => t -> DeadCodeAnalysis t v ()
 revive t = DeadCodeAnalysis (Evaluator (modify (Dead . delete t . unDead)))
 
 
-instance ( AbstractValue v
-         , Corecursive t
+instance ( Corecursive t
          , Evaluatable (Base t)
          , FreeVariables t
          , MonadAddressable (LocationFor v) v (DeadCodeAnalysis t v)
-         , MonadFunction t v (DeadCodeAnalysis t v)
+         , MonadValue t v (DeadCodeAnalysis t v)
          , Ord t
          , Recursive t
          , Semigroup (Cell (LocationFor v) v)

src/Analysis/Abstract/Evaluating.hs

@@ -30,11 +30,10 @@ type EvaluationEffects t v
 
 -- | Evaluate a term to a value.
 evaluate :: forall v term
-         .  ( AbstractValue v
-            , Evaluatable (Base term)
+         .  ( Evaluatable (Base term)
             , FreeVariables term
             , MonadAddressable (LocationFor v) v (Evaluation term v)
-            , MonadFunction term v (Evaluation term v)
+            , MonadValue term v (Evaluation term v)
             , Ord (LocationFor v)
             , Recursive term
             , Semigroup (Cell (LocationFor v) v)
@@ -45,11 +44,10 @@ evaluate = run @(EvaluationEffects term v) . runEvaluator . runEvaluation . eval
 
 -- | Evaluate terms and an entry point to a value.
 evaluates :: forall v term
-          .  ( AbstractValue v
-             , Evaluatable (Base term)
+          .  ( Evaluatable (Base term)
              , FreeVariables term
              , MonadAddressable (LocationFor v) v (Evaluation term v)
-             , MonadFunction term v (Evaluation term v)
+             , MonadValue term v (Evaluation term v)
              , Ord (LocationFor v)
              , Recursive term
              , Semigroup (Cell (LocationFor v) v)
@@ -70,11 +68,10 @@ newtype Evaluation term value a = Evaluation { runEvaluation :: Evaluator (Evalu
 
 deriving instance MonadEvaluator term value (Evaluation term value)
 
-instance ( AbstractValue v
-         , Evaluatable (Base t)
+instance ( Evaluatable (Base t)
          , FreeVariables t
          , MonadAddressable (LocationFor v) v (Evaluation t v)
-         , MonadFunction t v (Evaluation t v)
+         , MonadValue t v (Evaluation t v)
          , Recursive t
          , Semigroup (Cell (LocationFor v) v)
          )

src/Control/Abstract/Value.hs

@@ -1,5 +1,5 @@
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
-module Control.Abstract.Function where
+module Control.Abstract.Value where
 
 import Control.Abstract.Addressable
 import Control.Abstract.Analysis
@@ -8,20 +8,36 @@ import Control.Monad.Effect.Fresh
 import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
-import Data.Abstract.Value
-import Data.Abstract.Type
+import Data.Abstract.Value as Value
+import Data.Abstract.Type as Type
 import Prologue
 import Prelude hiding (fail)
 
 -- | 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 MonadEvaluator t v m => MonadFunction t v m where
+class (MonadEvaluator t v m) => MonadValue t v m where
+    -- | Construct an abstract unit value.
+  unit :: m v
+
+  -- | Construct an abstract integral value.
+  integer :: Prelude.Integer -> m v
+
+  -- | Construct an abstract boolean value.
+  boolean :: Bool -> m v
+
+  -- | Construct an abstract string value.
+  string :: ByteString -> m v
+
+  -- | Eliminate boolean values. TODO: s/boolean/truthy
+  ifthenelse :: v -> m v -> m v -> m v
+
   -- | Evaluate an abstraction (a binder like a lambda or method definition).
   abstract :: [Name] -> Subterm t (m v) -> m v
   -- | Evaluate an application (like a function call).
   apply :: v -> [Subterm t (m v)] -> m v
 
+-- | Construct a 'Value' wrapping the value arguments (if any).
 instance ( FreeVariables t
          , MonadAddressable location (Value location t) m
          , MonadAnalysis t (Value location t) m
@@ -29,7 +45,17 @@ instance ( FreeVariables t
          , Recursive t
          , Semigroup (Cell location (Value location t))
          )
-         => MonadFunction t (Value location t) m where
+         => MonadValue t (Value location t) m where
+
+  unit    = pure $ inj Value.Unit
+  integer = pure . inj . Integer
+  boolean = pure . inj . Boolean
+  string  = pure . inj . Value.String
+
+  ifthenelse cond if' else'
+    | Just (Boolean b) <- prj cond = if b then if' else else'
+    | otherwise = fail "not defined for non-boolean conditions"
+
   abstract names (Subterm body _) = inj . Closure names body <$> askLocalEnv
 
   apply op params = do
@@ -41,7 +67,8 @@ instance ( FreeVariables t
       envInsert name a <$> rest) (pure env) (zip names params)
     localEnv (mappend bindings) (evaluateTerm body)
 
-instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadFunction t Type m where
+-- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
+instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadValue t Type m where
   abstract names (Subterm _ body) = do
     (env, tvars) <- foldr (\ name rest -> do
       a <- alloc name
@@ -52,6 +79,13 @@ instance (Alternative m, MonadEvaluator t Type m, MonadFresh m) => MonadFunction
     ret <- localEnv (mappend env) body
     pure (Product tvars :-> ret)
 
+  unit      = pure Type.Unit
+  integer _ = pure Int
+  boolean _ = pure Bool
+  string _  = pure Type.String
+
+  ifthenelse cond if' else' = unify cond Bool *> (if' <|> else')
+
   apply op params = do
     tvar <- fresh
     paramTypes <- traverse subtermValue params

src/Data/Abstract/Evaluatable.hs

@@ -1,11 +1,10 @@
 {-# LANGUAGE DefaultSignatures, FunctionalDependencies, UndecidableInstances #-}
 module Data.Abstract.Evaluatable
 ( Evaluatable(..)
-, AbstractValue(..)
 , module Addressable
 , module Analysis
 , module FreeVariables
-, module Function
+, module Value
 , MonadEvaluator(..)
 , require
 , load
@@ -14,7 +13,7 @@ module Data.Abstract.Evaluatable
 import Control.Abstract.Addressable as Addressable
 import Control.Abstract.Analysis as Analysis
 import Control.Abstract.Evaluator
-import Control.Abstract.Function as Function
+import Control.Abstract.Value as Value
 import Control.Monad.Effect.Fail
 import Data.Abstract.Address
 import Data.Abstract.Environment
@@ -33,12 +32,11 @@ import Prologue
 
 -- | 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 :: ( AbstractValue value
-          , FreeVariables term
+  eval :: ( FreeVariables term
           , MonadAddressable (LocationFor value) value m
           , MonadAnalysis term value m
           , MonadEvaluator term value m
-          , MonadFunction term value m
+          , MonadValue term value m
           , Ord (LocationFor value)
           , Semigroup (Cell (LocationFor value) value)
           )
@@ -63,7 +61,7 @@ instance Evaluatable s => Evaluatable (TermF s a) where
 --   2. Each statement can affect the environment of later statements (e.g. by 'modify'-ing the environment); and
 --   3. Only the last statement’s return value is returned.
 instance Evaluatable [] where
-  eval []     = pure unit      -- Return unit value if this is an empty list of terms
+  eval []     = unit           -- Return unit value if this is an empty list of terms
   eval [x]    = subtermValue x -- Return the value for the last term
   eval (x:xs) = do
     _ <- subtermValue x        -- Evaluate the head term

src/Data/Abstract/Value.hs

@@ -9,7 +9,7 @@ import Data.Abstract.Live
 import qualified Data.Abstract.Type as Type
 import qualified Data.Set as Set
 import Prologue
-import Prelude hiding (Integer, String)
+import Prelude hiding (Integer, String, fail)
 import qualified Prelude
 
 type ValueConstructors location
@@ -92,42 +92,11 @@ class ValueRoots l v | v -> l where
   -- | Compute the set of addresses rooted by a given value.
   valueRoots :: v -> Live l v
 
--- | An interface for constructing abstract values.
-class AbstractValue v where
-  -- | Construct an abstract unit value.
-  unit :: v
-
-  -- | Construct an abstract integral value.
-  integer :: Prelude.Integer -> v
-
-  -- | Construct an abstract boolean value.
-  boolean :: Bool -> v
-
-  -- | Construct an abstract string value.
-  string :: ByteString -> v
-
-
--- Instances
-
 instance (FreeVariables term, Ord location) => ValueRoots location (Value location term) where
   valueRoots v
     | Just (Closure names body env) <- prj v = envRoots env (foldr Set.delete (freeVariables body) names)
     | Just (Interface _ env) <- prj v        = envAll env
     | otherwise                              = mempty
 
--- | Construct a 'Value' wrapping the value arguments (if any).
-instance AbstractValue (Value location term) where
-  unit = inj Unit
-  integer = inj . Integer
-  boolean = inj . Boolean
-  string = inj . String
-
 instance ValueRoots Monovariant Type.Type where
   valueRoots _ = mempty
-
--- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
-instance AbstractValue Type.Type where
-  unit = Type.Unit
-  integer _ = Type.Int
-  boolean _ = Type.Bool
-  string _ = Type.String

src/Data/Syntax.hs

@@ -127,7 +127,7 @@ instance Evaluatable Program where
     where
       interface val = pure val -- inj . Value.Interface val <$> askLocalEnv
 
-      eval' [] = interface unit
+      eval' [] = unit >>= interface
       eval' [x] = subtermValue x >>= interface
       eval' (x:xs) = do
         _ <- subtermValue x
@@ -156,7 +156,7 @@ instance Ord1 Empty where liftCompare _ _ _ = EQ
 instance Show1 Empty where liftShowsPrec _ _ _ _ = showString "Empty"
 
 instance Evaluatable Empty where
-  eval _ = pure unit
+  eval _ = unit
 
 
 -- | Syntax representing a parsing or assignment error.

src/Data/Syntax/Comment.hs

@@ -14,7 +14,7 @@ instance Ord1 Comment where liftCompare = genericLiftCompare
 instance Show1 Comment where liftShowsPrec = genericLiftShowsPrec
 
 instance Evaluatable Comment where
-  eval _ = pure unit
+  eval _ = unit
 
 -- TODO: nested comment types
 -- TODO: documentation comment types

src/Data/Syntax/Declaration.hs

@@ -217,7 +217,7 @@ instance Ord1 Import where liftCompare = genericLiftCompare
 instance Show1 Import where liftShowsPrec = genericLiftShowsPrec
 
 instance Evaluatable Import where
-  eval (Import from _ _) = require (subterm from) >> pure unit
+  eval (Import from _ _) = require (subterm from) *> unit
 
 
 -- | An imported symbol

src/Data/Syntax/Literal.hs

@@ -22,7 +22,7 @@ instance Ord1 Boolean where liftCompare = genericLiftCompare
 instance Show1 Boolean where liftShowsPrec = genericLiftShowsPrec
 
 instance Evaluatable Boolean where
-  eval (Boolean x) = pure (boolean x)
+  eval (Boolean x) = boolean x
 
 
 -- Numeric
@@ -37,7 +37,7 @@ instance Show1 Data.Syntax.Literal.Integer where liftShowsPrec = genericLiftShow
 
 instance Evaluatable Data.Syntax.Literal.Integer where
   -- TODO: This instance probably shouldn't have readInteger?
-  eval (Data.Syntax.Literal.Integer x) = pure (integer (maybe 0 fst (readInteger x)))
+  eval (Data.Syntax.Literal.Integer x) = integer (maybe 0 fst (readInteger x))
 
 
 -- TODO: Should IntegerLiteral hold an Integer instead of a ByteString?
@@ -115,7 +115,7 @@ instance Ord1 TextElement where liftCompare = genericLiftCompare
 instance Show1 TextElement where liftShowsPrec = genericLiftShowsPrec
 
 instance Evaluatable TextElement where
-  eval (TextElement x) = pure (string x)
+  eval (TextElement x) = string x
 
 data Null a = Null
   deriving (Diffable, Eq, Foldable, Functor, GAlign, Generic1, Mergeable, Ord, Show, Traversable, FreeVariables1)

src/Data/Syntax/Statement.hs

@@ -14,9 +14,10 @@ instance Eq1 If where liftEq = genericLiftEq
 instance Ord1 If where liftCompare = genericLiftCompare
 instance Show1 If where liftShowsPrec = genericLiftShowsPrec
 
--- TODO: Implement Eval instance for If
-instance Evaluatable If
-
+instance Evaluatable If where
+  eval (If cond if' else') = do
+    bool <- subtermValue cond
+    ifthenelse bool (subtermValue if') (subtermValue else')
 
 -- | Else statement. The else condition is any term, that upon successful completion, continues evaluation to the elseBody, e.g. `for ... else` in Python.
 data Else a = Else { elseCondition :: !a, elseBody :: !a }
@@ -185,8 +186,8 @@ instance Ord1 NoOp where liftCompare = genericLiftCompare
 instance Show1 NoOp where liftShowsPrec = genericLiftShowsPrec
 
 -- TODO: Implement Eval instance for NoOp
-instance Evaluatable NoOp
-
+instance Evaluatable NoOp where
+  eval _ = unit
 
 -- Loops