diff --git a/semantic-core/src/Analysis/Concrete.hs b/semantic-core/src/Analysis/Concrete.hs index 8cc45b8cbb..7ae7801714 100644 --- a/semantic-core/src/Analysis/Concrete.hs +++ b/semantic-core/src/Analysis/Concrete.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} module Analysis.Concrete ( Concrete(..) , concrete @@ -28,6 +28,7 @@ import qualified Data.IntSet as IntSet import Data.Loc import qualified Data.Map as Map import Data.Name +import Data.Semigroup (Last (..)) import qualified Data.Set as Set import Data.Term import Data.Text (Text, pack) @@ -47,6 +48,8 @@ data Concrete | String Text | Record Env deriving (Eq, Ord, Show) + -- NB: We derive the 'Semigroup' instance for 'Concrete' to take the second argument. This is equivalent to stating that the return value of an imperative sequence of statements is the value of its final statement. + deriving Semigroup via Last Concrete recordFrame :: Concrete -> Maybe Env recordFrame (Record frame) = Just frame diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index 2e68a8530f..15abe28087 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -30,6 +30,7 @@ import Prelude hiding (fail) eval :: ( Carrier sig m , Member (Reader Loc) sig , MonadFail m + , Semigroup value ) => Analysis address value m -> (Term Core User -> m value) @@ -41,12 +42,15 @@ eval Analysis{..} eval = \case addr <- alloc n v <- bind n addr (eval (instantiate1 (pure n) b)) v <$ assign addr v - a :>> b -> eval a >> eval b + -- NB: Combining the results of the evaluations allows us to model effects in abstract domains. This in turn means that we can define an abstract domain modelling the types-and-effects of computations by means of a 'Semigroup' instance which takes the type of its second operand and the union of both operands’ effects. + -- + -- It’s also worth noting that we use a semigroup instead of a semilattice because the lattice structure of our abstract domains is instead modelled by nondeterminism effects used by some of them. + a :>> b -> (<>) <$> eval a <*> eval b Named (Ignored n) a :>>= b -> do a' <- eval a addr <- alloc n assign addr a' - bind n addr (eval (instantiate1 (pure n) b)) + bind n addr ((a' <>) <$> eval (instantiate1 (pure n) b)) Lam (Named (Ignored n) b) -> abstract eval n (instantiate1 (pure n) b) f :$ a -> do f' <- eval f @@ -210,18 +214,18 @@ ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' stateme data Analysis address value m = Analysis - { alloc :: User -> m address - , bind :: forall a . User -> address -> m a -> m a - , lookupEnv :: User -> m (Maybe address) - , deref :: address -> m (Maybe value) - , assign :: address -> value -> m () - , abstract :: (Term Core User -> m value) -> User -> Term Core User -> m value - , apply :: (Term Core User -> m value) -> value -> value -> m value - , unit :: m value - , bool :: Bool -> m value - , asBool :: value -> m Bool - , string :: Text -> m value - , asString :: value -> m Text - , record :: [(User, value)] -> m value - , (...) :: address -> User -> m (Maybe address) + { alloc :: User -> m address + , bind :: forall a . User -> address -> m a -> m a + , lookupEnv :: User -> m (Maybe address) + , deref :: address -> m (Maybe value) + , assign :: address -> value -> m () + , abstract :: (Term Core User -> m value) -> User -> Term Core User -> m value + , apply :: (Term Core User -> m value) -> value -> value -> m value + , unit :: m value + , bool :: Bool -> m value + , asBool :: value -> m Bool + , string :: Text -> m value + , asString :: value -> m Text + , record :: [(User, value)] -> m value + , (...) :: address -> User -> m (Maybe address) } diff --git a/semantic-core/src/Analysis/Typecheck.hs b/semantic-core/src/Analysis/Typecheck.hs index f2bf865964..916b21559f 100644 --- a/semantic-core/src/Analysis/Typecheck.hs +++ b/semantic-core/src/Analysis/Typecheck.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-} +{-# LANGUAGE DeriveGeneric, DeriveTraversable, DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-} module Analysis.Typecheck ( Monotype (..) , Meta @@ -30,6 +30,7 @@ import qualified Data.Map as Map import Data.Maybe (fromJust, fromMaybe) import Data.Name as Name import Data.Scope +import Data.Semigroup (Last (..)) import qualified Data.Set as Set import Data.Term import Data.Void @@ -44,6 +45,11 @@ data Monotype f a | Record (Map.Map User (f a)) deriving (Foldable, Functor, Generic1, Traversable) +-- FIXME: Union the effects/annotations on the operands. + +-- | We derive the 'Semigroup' instance for types to take the second argument. This is equivalent to stating that the type of an imperative sequence of statements is the type of its final statement. +deriving via (Last (Term Monotype a)) instance Semigroup (Term Monotype a) + deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Monotype f a) deriving instance (Ord a, forall a . Eq a => Eq (f a) , forall a . Ord a => Ord (f a), Monad f) => Ord (Monotype f a)