From d1ad4d631813446e819c4abb1ccf9d4d02eeed70 Mon Sep 17 00:00:00 2001 From: Timothy Clem Date: Fri, 13 Oct 2017 11:03:58 -0700 Subject: [PATCH] Port over Environment, Primitive, Type, Value --- semantic-diff.cabal | 4 + src/Abstract/Environment.hs | 54 ++++++++++++++ src/Abstract/Primitive.hs | 141 ++++++++++++++++++++++++++++++++++++ src/Abstract/Type.hs | 41 +++++++++++ src/Abstract/Value.hs | 80 ++++++++++++++++++++ 5 files changed, 320 insertions(+) create mode 100644 src/Abstract/Environment.hs create mode 100644 src/Abstract/Primitive.hs create mode 100644 src/Abstract/Type.hs create mode 100644 src/Abstract/Value.hs diff --git a/semantic-diff.cabal b/semantic-diff.cabal index b17543f5b..2a5c35681 100644 --- a/semantic-diff.cabal +++ b/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 diff --git a/src/Abstract/Environment.hs b/src/Abstract/Environment.hs new file mode 100644 index 000000000..e5c0eea36 --- /dev/null +++ b/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 diff --git a/src/Abstract/Primitive.hs b/src/Abstract/Primitive.hs new file mode 100644 index 000000000..22e9ea5e4 --- /dev/null +++ b/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" diff --git a/src/Abstract/Type.hs b/src/Abstract/Type.hs new file mode 100644 index 000000000..be840f4ff --- /dev/null +++ b/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' ()) diff --git a/src/Abstract/Value.hs b/src/Abstract/Value.hs new file mode 100644 index 000000000..b55677a1d --- /dev/null +++ b/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