Abstract abstraction.

src/Analysis/Abstract/Evaluating.hs

@@ -71,7 +71,7 @@ moduleName term = let [n] = toList (freeVariables term) in BC.unpack n
 evaluate :: forall v term.
          ( Ord v
          , Ord (LocationFor v)
-         , AbstractValue term v
+         , AbstractFunction (Evaluating v) term v
          , Evaluatable (Evaluating v) term v (Base term)
          , FreeVariables term
          , Recursive term
@@ -84,7 +84,7 @@ evaluate = run @(Evaluating v) . foldSubterms eval
 evaluates :: forall v term.
           ( Ord v
           , Ord (LocationFor v)
-          , AbstractValue term v
+          , AbstractFunction (Evaluating v) term v
           , FreeVariables term
           , Evaluatable (Evaluating v) term v (Base term)
           , Recursive term

src/Control/Monad/Effect/Evaluatable.hs

@@ -1,18 +1,23 @@
-{-# LANGUAGE MultiParamTypeClasses, Rank2Types, GADTs, TypeOperators, DefaultSignatures, UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds, FunctionalDependencies, MultiParamTypeClasses, Rank2Types, GADTs, TypeOperators, DefaultSignatures, UndecidableInstances, ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 module Control.Monad.Effect.Evaluatable
 ( Evaluatable(..)
 , Recursive(..)
 , Base
 , Subterm(..)
+, AbstractFunction(..)
 ) where
 
+import Control.Monad.Effect.Addressable
 import Control.Monad.Effect.Fail
+import Control.Monad.Effect.Fresh
 import Control.Monad.Effect.Internal
+import Control.Monad.Effect.NonDetEff
 import Control.Monad.Effect.Reader
 import Control.Monad.Effect.State
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
+import Data.Abstract.Type as Type
 import Data.Abstract.Value
 import Data.Algebra
 import Data.Functor.Classes
@@ -26,7 +31,7 @@ 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 effects term value constr where
-  eval :: (AbstractValue term value, FreeVariables term) => SubtermAlgebra constr term (Eff effects value)
+  eval :: (AbstractFunction effects term value, FreeVariables term) => SubtermAlgebra constr term (Eff effects value)
   default eval :: (Fail :< effects, FreeVariables term, Show1 constr) => SubtermAlgebra constr term (Eff effects value)
   eval expr = fail $ "Eval unspecialized for " ++ liftShowsPrec (const (const id)) (const id) 0 expr ""
 
@@ -67,3 +72,20 @@ instance ( Ord (LocationFor v)
     -- environment each time where the free variables in those terms are bound
     -- to the global environment.
     local (const (bindEnv (liftFreeVariables (freeVariables . subterm) xs) env)) (eval xs)
+
+class AbstractValue v => AbstractFunction effects t v | v -> t where
+  abstract :: [Name] -> (t, Eff effects v) -> Eff effects v
+
+instance Reader (EnvironmentFor (Value location t)) :< effects => AbstractFunction effects t (Value location t) where
+  abstract names (body, _) = inj . Closure names body <$> ask @(EnvironmentFor (Value location t))
+
+instance Members '[Fresh, NonDetEff, Reader (EnvironmentFor (Type t)), State (StoreFor (Type t))] effects => AbstractFunction effects t (Type t) where
+  abstract names (_, body) = do
+    (env, tvars) <- foldr (\ name rest -> do
+      a <- alloc name
+      tvar <- Var <$> fresh
+      assign a tvar
+      (env, tvars) <- rest
+      pure (envInsert name a env, tvar : tvars)) (pure mempty) names
+    ret <- local (mappend env) body
+    pure (Type.Product tvars :-> ret)

src/Data/Abstract/Value.hs

@@ -97,7 +97,7 @@ class ValueRoots l v | v -> l where
   valueRoots :: v -> Live l v
 
 -- | An interface for constructing abstract values.
-class AbstractValue t v | v -> t where
+class AbstractValue v where
   -- | Construct an abstract unit value.
   unit :: v
 
@@ -110,8 +110,6 @@ class AbstractValue t v | v -> t where
   -- | Construct an abstract string value.
   string :: ByteString -> v
 
-  -- abstract :: Monad m => [Name] -> (t, m v) -> m v
-
 
 -- Instances
 
@@ -122,18 +120,17 @@ instance (FreeVariables term, Ord location) => ValueRoots location (Value locati
     | otherwise                              = mempty
 
 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance AbstractValue term (Value location term) where
+instance AbstractValue (Value location term) where
   unit = inj Unit
   integer = inj . Integer
   boolean = inj . Boolean
   string = inj . String
-  -- abstract names (term, _) = inj . Closure names term <$> ask
 
 instance ValueRoots Monovariant (Type.Type term) where
   valueRoots _ = mempty
 
 -- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
-instance AbstractValue term (Type.Type term) where
+instance AbstractValue (Type.Type term) where
   unit = Type.Unit
   integer _ = Type.Int
   boolean _ = Type.Bool