Port over Environment, Primitive, Type, Value

semantic-diff.cabal

@@ -15,10 +15,14 @@ library
   hs-source-dirs:      src
   exposed-modules:     Algorithm
                      , Alignment
+                     , Abstract.Environment
                      , Abstract.Eval
                      , Abstract.FreeVariables
+                     , Abstract.Primitive
                      , Abstract.Set
                      , Abstract.Store
+                     , Abstract.Type
+                     , Abstract.Value
                      , Control.Effect
                      , Category
                      , Data.Align.Generic

src/Abstract/Environment.hs

@@ -0,0 +1,54 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, DeriveFoldable, DeriveFunctor, DeriveTraversable, DeriveGeneric, GeneralizedNewtypeDeriving #-}
+module Abstract.Environment where
+
+import Abstract.Store
+import Abstract.FreeVariables
+import Data.Term
+import Control.Monad.Effect
+import Control.Monad.Effect.Reader
+import Data.Functor.Classes
+import Data.Functor.Classes.Show.Generic
+import Data.Pointed
+import Data.Semigroup
+import GHC.Generics
+import qualified Data.Map as Map
+
+
+newtype Environment l a = Environment { unEnvironment :: Map.Map Name (Address l a) }
+  deriving (Eq, Foldable, Functor, Monoid, Ord, Semigroup, Show, Traversable, Generic1)
+
+envLookup :: Name -> Environment l a -> Maybe (Address l a)
+envLookup = (. unEnvironment) . Map.lookup
+
+envInsert :: Name -> Address l a -> Environment l a -> Environment l a
+envInsert name value (Environment m) = Environment (Map.insert name value m)
+
+envRoots :: (Foldable t, Ord l) => Environment l a -> t Name -> Set (Address l a)
+envRoots env = foldr ((<>) . maybe mempty point . flip envLookup env) mempty
+
+
+class Monad m => MonadEnv l a m where
+  askEnv :: m (Environment l a)
+  localEnv :: (Environment l a -> Environment l a) -> m b -> m b
+
+instance (Reader (Environment l a) :< fs) => MonadEnv l a (Eff fs) where
+  askEnv = ask
+  localEnv = local
+
+
+-- Instances
+
+instance Eq2 Environment where
+  liftEq2 eqL eqA (Environment m1) (Environment m2) = liftEq (liftEq2 eqL eqA) m1 m2
+
+instance Eq l => Eq1 (Environment l) where
+  liftEq = liftEq2 (==)
+
+instance Ord2 Environment where
+  liftCompare2 compareL compareA (Environment m1) (Environment m2) = liftCompare (liftCompare2 compareL compareA) m1 m2
+
+instance Ord l => Ord1 (Environment l) where
+  liftCompare = liftCompare2 compare
+
+instance Show l => Show1 (Environment l) where
+  liftShowsPrec = genericLiftShowsPrec

src/Abstract/Primitive.hs

@@ -0,0 +1,141 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-}
+module Abstract.Primitive where
+
+import Abstract.Type
+import Control.Applicative
+import Control.Monad hiding (fail)
+import Control.Monad.Fail
+import Prelude hiding (fail)
+
+data Op1 = Negate | Abs | Signum | Not
+  deriving (Eq, Ord, Show)
+
+data Op2 = Plus | Minus | Times | DividedBy | Quotient | Remainder | Modulus | And | Or | Eq | Lt | LtE | Gt | GtE
+  deriving (Eq, Ord, Show)
+
+arithmeticOperators :: [Op2]
+arithmeticOperators = [Plus, Minus, Times, DividedBy, Quotient, Remainder, Modulus]
+
+booleanOperators :: [Op2]
+booleanOperators = [And, Or]
+
+relationOperators :: [Op2]
+relationOperators = [Eq, Lt, LtE, Gt, GtE]
+
+
+data Prim
+  = PInt  {-# UNPACK #-} !Int
+  | PBool !Bool
+  deriving (Eq, Ord, Show)
+
+class Monad m => MonadPrim a m where
+  delta1 :: Op1 -> a -> m a
+  delta2 :: Op2 -> a -> a -> m a
+  truthy :: a -> m Bool
+
+
+divisionByZero :: MonadFail m => m a
+divisionByZero = fail "division by zero"
+
+nonNumeric :: MonadFail m => m a
+nonNumeric = fail "numeric operation on non-numeric value"
+
+nonBoolean :: MonadFail m => m a
+nonBoolean = fail "boolean operation on non-boolean value"
+
+disjointComparison :: MonadFail m => m a
+disjointComparison = fail "comparison of disjoint values"
+
+undefinedComparison :: MonadFail m => m a
+undefinedComparison = fail "undefined comparison"
+
+
+isZero :: (Num a, MonadPrim a m) => a -> m Bool
+isZero = truthy <=< delta2 Eq 0
+
+instance MonadFail m => MonadPrim Prim m where
+  delta1 o a = case (o, a) of
+    (Negate, PInt a)  -> pure (PInt (negate a))
+    (Abs,    PInt a)  -> pure (PInt (abs a))
+    (Signum, PInt a)  -> pure (PInt (signum a))
+    (Not,    PBool a) -> pure (PBool (not a))
+    (Not,    _)       -> nonBoolean
+    _                 -> nonNumeric
+
+  delta2 o (PInt a) (PInt b) = case o of
+    Plus      -> pure (PInt (a + b))
+    Minus     -> pure (PInt (a - b))
+    Times     -> pure (PInt (a * b))
+    DividedBy -> isZero (PInt b) >>= flip when divisionByZero >> pure (PInt (a `div` b))
+    Quotient  -> isZero (PInt b) >>= flip when divisionByZero >> pure (PInt (a `quot` b))
+    Remainder -> isZero (PInt b) >>= flip when divisionByZero >> pure (PInt (a `rem` b))
+    Modulus   -> isZero (PInt b) >>= flip when divisionByZero >> pure (PInt (a `mod` b))
+    Eq        -> pure (PBool (a == b))
+    Lt        -> pure (PBool (a < b))
+    LtE       -> pure (PBool (a <= b))
+    Gt        -> pure (PBool (a > b))
+    GtE       -> pure (PBool (a >= b))
+    _         -> nonBoolean
+  delta2 o (PBool a) (PBool b) = case o of
+    And -> pure (PBool (a && b))
+    Or  -> pure (PBool (a || b))
+    Eq  -> pure (PBool (a == b))
+    Lt  -> pure (PBool (a < b))
+    LtE -> pure (PBool (a <= b))
+    Gt  -> pure (PBool (a > b))
+    GtE -> pure (PBool (a >= b))
+    _   -> nonNumeric
+  delta2 _ _ _ = disjointComparison
+
+  truthy (PBool a) = pure a
+  truthy _         = nonBoolean
+
+instance (MonadFail m, Alternative m) => MonadPrim Type m where
+  delta1 Not Bool = pure Bool
+  delta1 Not _    = nonBoolean
+  delta1 _   Int  = pure Int
+  delta1 _   _    = nonNumeric
+
+  delta2 o a b
+    | o `elem` booleanOperators = case (a, b) of
+      (Bool,   Bool)   -> pure Bool
+      (TVar _, Bool)   -> pure Bool
+      (Bool,   TVar _) -> pure Bool
+      (TVar _, TVar _) -> pure Bool
+      _                -> nonBoolean
+    | o `elem` relationOperators = case (a, b) of
+      _ | a == b       -> pure Bool
+      (TVar _, _)      -> pure Bool
+      (_,      TVar _) -> pure Bool
+      _                -> disjointComparison
+    | o `elem` arithmeticOperators = case (a, b) of
+      (Int,    Int)    -> pure Int
+      (TVar _, Int)    -> pure Int
+      (Int,    TVar _) -> pure Int
+      (TVar _, TVar _) -> pure Int
+      _                -> nonNumeric
+  delta2 DividedBy Int  Int  = pure Int <|> divisionByZero
+  delta2 Quotient  Int  Int  = pure Int <|> divisionByZero
+  delta2 Remainder Int  Int  = pure Int <|> divisionByZero
+  delta2 Modulus   Int  Int  = pure Int <|> divisionByZero
+  delta2 _         _    _    = nonNumeric
+
+  truthy Bool     = pure True <|> pure False
+  truthy (TVar _) = pure True <|> pure False
+  truthy _        = nonBoolean
+
+
+instance Num Prim where
+  fromInteger = PInt . fromInteger
+
+  negate (PInt a) = PInt (negate a)
+  negate _        = error "negate of non-integer"
+  abs (PInt a) = PInt (abs a)
+  abs _        = error "abs of non-integer"
+  signum (PInt a) = PInt (signum a)
+  signum _        = error "signum of non-integer"
+
+  PInt a + PInt b = PInt (a + b)
+  _      + _      = error "(+) of non-integer"
+  PInt a * PInt b = PInt (a * b)
+  _      * _      = error "(*) of non-integer"

src/Abstract/Type.hs

@@ -0,0 +1,41 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-}
+module Abstract.Type where
+
+import Control.Effect
+import Control.Monad.Effect.Internal
+import Control.Monad.Fail
+import Prelude hiding (fail)
+
+type TName = Int
+
+data Type = Int | Bool | Type :-> Type | Type :* Type | TVar TName
+  deriving (Eq, Ord, Show)
+
+
+unify :: MonadFail m => Type -> Type -> m Type
+unify Int  Int  = pure Int
+unify Bool Bool = pure Bool
+unify (a1 :-> b1) (a2 :-> b2) = (:->) <$> unify a1 a2 <*> unify b1 b2
+unify (a1 :* b1)  (a2 :* b2)  = (:*)  <$> unify a1 a2 <*> unify b1 b2
+unify (TVar _) b = pure b
+unify a (TVar _) = pure a
+unify t1 t2 = fail ("cannot unify " ++ show t1 ++ " with " ++ show t2)
+
+
+data Fresh a where
+  Reset :: Int -> Fresh ()
+  Fresh :: Fresh Int
+
+class Monad m => MonadFresh m where
+  fresh :: m TName
+  reset :: TName -> m ()
+
+instance (Fresh :< fs) => MonadFresh (Eff fs) where
+  fresh = send Fresh
+  reset = send . Reset
+
+
+instance RunEffect Fresh a where
+  runEffect = relayState (0 :: TName) (const pure) (\ s action k -> case action of
+    Fresh -> k (succ s) s
+    Reset s' -> k s' ())

src/Abstract/Value.hs

@@ -0,0 +1,80 @@
+{-# LANGUAGE ConstraintKinds, FunctionalDependencies, AllowAmbiguousTypes, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
+module Abstract.Value where
+
+import Abstract.Environment
+import Abstract.Primitive
+import Abstract.Set
+import Abstract.Store
+import Abstract.Type
+import Abstract.FreeVariables
+import Data.Term
+import Control.Monad hiding (fail)
+import Control.Monad.Fail
+import Data.Functor.Classes
+import Data.Semigroup
+import Prelude hiding (fail)
+
+
+data Value syntax ann l
+  = I Prim
+  | Closure Name (Term syntax ann) (Environment l (Value syntax ann l))
+  deriving (Eq, Ord, Show)
+
+
+-- Instances
+
+instance (Eq1 syntax, Eq ann) => Eq1 (Value syntax ann) where
+  liftEq eqL = go
+    where go v1 v2 = case (v1, v2) of
+            (I a, I b) -> a == b
+            (Closure s1 t1 e1, Closure s2 t2 e2) -> s1 == s2 && t1 == t2 && liftEq2 eqL go e1 e2
+            _ -> False
+
+instance (Ord1 syntax, Ord ann) => Ord1 (Value syntax ann) where
+  liftCompare compareL = go
+    where go v1 v2 = case (v1, v2) of
+            (I a, I b) -> compare a b
+            (Closure s1 t1 e1, Closure s2 t2 e2) -> compare s1 s2 <> compare t1 t2 <> liftCompare2 compareL go e1 e2
+            (I _, _) -> LT
+            _ -> GT
+
+instance MonadFail m => MonadPrim (Value s a l) m where
+  delta1 o   (I a) = fmap I (delta1 o a)
+  delta1 Not _     = nonBoolean
+  delta1 _   _     = nonNumeric
+
+  delta2 o   (I a)     (I b)     = fmap I (delta2 o a b)
+  delta2 And _         _         = nonBoolean
+  delta2 Or  _         _         = nonBoolean
+  delta2 Eq  Closure{} Closure{} = undefinedComparison
+  delta2 Eq  _         _         = disjointComparison
+  delta2 Lt  Closure{} Closure{} = undefinedComparison
+  delta2 Lt  _         _         = disjointComparison
+  delta2 LtE Closure{} Closure{} = undefinedComparison
+  delta2 LtE _         _         = disjointComparison
+  delta2 Gt  Closure{} Closure{} = undefinedComparison
+  delta2 Gt  _         _         = disjointComparison
+  delta2 GtE Closure{} Closure{} = undefinedComparison
+  delta2 GtE _         _         = disjointComparison
+  delta2 _   _         _         = nonNumeric
+
+  truthy (I a) = truthy a
+  truthy _     = nonBoolean
+
+
+
+class AbstractValue l v | v -> l where
+  literal :: Prim -> v
+  valueRoots :: v -> Set (Address l v)
+
+instance (FreeVariables1 (TermF syntax ann), Functor syntax, Ord l) => AbstractValue l (Value syntax ann l) where
+  valueRoots (I _) = mempty
+  valueRoots (Closure name body env) = envRoots env (delete name (freeVariables body))
+
+  literal = I
+
+instance AbstractValue Monovariant Type where
+  valueRoots _ = mempty
+
+  literal (PInt _)  = Int
+  literal (PBool _) = Bool