diff --git a/semantic-core/src/Analysis/Concrete.hs b/semantic-core/src/Analysis/Concrete.hs index f1db97213c..a12bf16e83 100644 --- a/semantic-core/src/Analysis/Concrete.hs +++ b/semantic-core/src/Analysis/Concrete.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RankNTypes, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} module Analysis.Concrete ( Concrete(..) , concrete @@ -20,7 +20,6 @@ import Control.Effect.NonDet import Control.Effect.Reader hiding (Local) import Control.Effect.State import Control.Monad ((<=<), guard) -import qualified Data.Core as Core import Data.File import Data.Function (fix) import qualified Data.IntMap as IntMap @@ -30,7 +29,6 @@ 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) import Data.Traversable (for) import Prelude hiding (fail) @@ -41,17 +39,17 @@ type Env = Map.Map User Precise newtype FrameId = FrameId { unFrameId :: Precise } deriving (Eq, Ord, Show) -data Concrete - = Closure Loc User (Term (Core.Ann :+: Core.Core) User) Env +data Concrete term + = Closure Loc User term Env | Unit | Bool Bool | 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 + deriving Semigroup via Last (Concrete term) -recordFrame :: Concrete -> Maybe Env +recordFrame :: Concrete term -> Maybe Env recordFrame (Record frame) = Just frame recordFrame _ = Nothing @@ -60,7 +58,7 @@ newtype Frame = Frame } deriving (Eq, Ord, Show) -type Heap = IntMap.IntMap Concrete +type Heap term = IntMap.IntMap (Concrete term) data Edge = Lexical | Import deriving (Eq, Ord, Show) @@ -68,36 +66,56 @@ data Edge = Lexical | Import -- | Concrete evaluation of a term to a value. -- --- >>> map fileBody (snd (concrete [File (Loc "bool" emptySpan) (Core.bool True)])) +-- >>> map fileBody (snd (concrete eval [File (Loc "bool" emptySpan) (Core.bool True)])) -- [Right (Bool True)] -concrete :: [File (Term (Core.Ann :+: Core.Core) User)] -> (Heap, [File (Either (Loc, String) Concrete)]) concrete + :: (Foldable term, Show (term User)) + => (forall sig m + . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) + => Analysis (term User) Precise (Concrete (term User)) m + -> (term User -> m (Concrete (term User))) + -> (term User -> m (Concrete (term User))) + ) + -> [File (term User)] + -> (Heap (term User), [File (Either (Loc, String) (Concrete (term User)))]) +concrete eval = run . runFresh . runHeap - . traverse runFile - -runFile :: ( Carrier sig m - , Effect sig - , Member Fresh sig - , Member (State Heap) sig - ) - => File (Term (Core.Ann :+: Core.Core) User) - -> m (File (Either (Loc, String) Concrete)) -runFile file = traverse run file + . traverse (runFile eval) + +runFile + :: ( Carrier sig m + , Effect sig + , Foldable term + , Member Fresh sig + , Member (State (Heap (term User))) sig + , Show (term User) + ) + => (forall sig m + . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) + => Analysis (term User) Precise (Concrete (term User)) m + -> (term User -> m (Concrete (term User))) + -> (term User -> m (Concrete (term User))) + ) + -> File (term User) + -> m (File (Either (Loc, String) (Concrete (term User)))) +runFile eval file = traverse run file where run = runReader (fileLoc file) . runFailWithLoc . runReader @Env mempty . fix (eval concreteAnalysis) concreteAnalysis :: ( Carrier sig m + , Foldable term , Member Fresh sig , Member (Reader Env) sig , Member (Reader Loc) sig - , Member (State Heap) sig + , Member (State (Heap (term User))) sig , MonadFail m + , Show (term User) ) - => Analysis Precise Concrete m + => Analysis (term User) Precise (Concrete (term User)) m concreteAnalysis = Analysis{..} where alloc _ = fresh bind name addr m = local (Map.insert name addr) m @@ -133,7 +151,7 @@ concreteAnalysis = Analysis{..} pure (val >>= lookupConcrete heap n) -lookupConcrete :: Heap -> User -> Concrete -> Maybe Precise +lookupConcrete :: Heap term -> User -> Concrete term -> Maybe Precise lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete where -- look up the name in a concrete value inConcrete = inFrame <=< maybeA . recordFrame @@ -150,7 +168,7 @@ lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete maybeA = maybe empty pure -runHeap :: StateC Heap m a -> m (Heap, a) +runHeap :: StateC (Heap term) m a -> m (Heap term, a) runHeap = runState mempty @@ -159,7 +177,7 @@ runHeap = runState mempty -- > λ let (heap, res) = concrete [ruby] -- > λ writeFile "/Users/rob/Desktop/heap.dot" (export (addressStyle heap) (heapAddressGraph heap)) -- > λ :!dot -Tsvg < ~/Desktop/heap.dot > ~/Desktop/heap.svg -heapGraph :: (Precise -> Concrete -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a +heapGraph :: (Precise -> Concrete term -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap term -> G.Graph a heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h) where graph k v rest = (G.vertex (vertex k v) `G.connect` outgoing v) `G.overlay` rest outgoing = \case @@ -169,14 +187,14 @@ heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h) Closure _ _ _ env -> foldr (G.overlay . edge (Left Lexical)) G.empty env Record frame -> Map.foldrWithKey (\ k -> G.overlay . edge (Right k)) G.empty frame -heapValueGraph :: Heap -> G.Graph Concrete +heapValueGraph :: Heap term -> G.Graph (Concrete term) heapValueGraph h = heapGraph (const id) (const fromAddr) h where fromAddr addr = maybe G.empty G.vertex (IntMap.lookup addr h) -heapAddressGraph :: Heap -> G.Graph (EdgeType, Precise) +heapAddressGraph :: Heap term -> G.Graph (EdgeType term, Precise) heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G.vertex . (,) . either Edge Slot) -addressStyle :: Heap -> G.Style (EdgeType, Precise) Text +addressStyle :: Heap term -> G.Style (EdgeType term, Precise) Text addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes } where vertex (_, addr) = pack (show addr) <> " = " <> maybe "?" fromConcrete (IntMap.lookup addr heap) edgeAttributes _ (Slot name, _) = ["label" G.:= name] @@ -191,12 +209,13 @@ addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes } Record _ -> "{}" showPos (Pos l c) = pack (show l) <> ":" <> pack (show c) -data EdgeType +data EdgeType term = Edge Edge | Slot User - | Value Concrete + | Value (Concrete term) deriving (Eq, Ord, Show) -- $setup -- >>> :seti -XOverloadedStrings +-- >>> import qualified Data.Core as Core diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index 1080a740db..515bf12c4a 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -33,7 +33,7 @@ eval :: ( Carrier sig m , MonadFail m , Semigroup value ) - => Analysis address value m + => Analysis (Term (Ann :+: Core) User) address value m -> (Term (Ann :+: Core) User -> m value) -> (Term (Ann :+: Core) User -> m value) eval Analysis{..} eval = \case @@ -214,14 +214,14 @@ ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' stateme __semantic_truthy = "__semantic_truthy" -data Analysis address value m = Analysis +data Analysis term 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 (Ann :+: Core) User -> m value) -> User -> Term (Ann :+: Core) User -> m value - , apply :: (Term (Ann :+: Core) User -> m value) -> value -> value -> m value + , abstract :: (term -> m value) -> User -> term -> m value + , apply :: (term -> m value) -> value -> value -> m value , unit :: m value , bool :: Bool -> m value , asBool :: value -> m Bool diff --git a/semantic-core/src/Analysis/FlowInsensitive.hs b/semantic-core/src/Analysis/FlowInsensitive.hs index fdf0cc7fa4..b3c6bcaa08 100644 --- a/semantic-core/src/Analysis/FlowInsensitive.hs +++ b/semantic-core/src/Analysis/FlowInsensitive.hs @@ -13,60 +13,62 @@ import Control.Effect.Fresh import Control.Effect.NonDet import Control.Effect.Reader import Control.Effect.State -import qualified Data.Core as Core import qualified Data.Map as Map import Data.Maybe (fromMaybe) import Data.Monoid (Alt(..)) import qualified Data.Set as Set -import Data.Term (Term) -type Cache name a = Map.Map (Term (Core.Ann :+: Core.Core) name) (Set.Set a) -type Heap name a = Map.Map name (Set.Set a) +newtype Cache term a = Cache { unCache :: Map.Map term (Set.Set a) } + deriving (Eq, Ord, Show) + +type Heap address a = Map.Map address (Set.Set a) newtype FrameId name = FrameId { unFrameId :: name } deriving (Eq, Ord, Show) -convergeTerm :: forall m sig a name +convergeTerm :: forall m sig a term address proxy . ( Carrier sig m , Effect sig + , Eq address , Member Fresh sig - , Member (State (Heap name a)) sig + , Member (State (Heap address a)) sig , Ord a - , Ord name + , Ord term ) - => (Term (Core.Ann :+: Core.Core) name -> NonDetC (ReaderC (Cache name a) (StateC (Cache name a) m)) a) - -> Term (Core.Ann :+: Core.Core) name + => proxy address + -> (term -> NonDetC (ReaderC (Cache term a) (StateC (Cache term a) m)) a) + -> term -> m (Set.Set a) -convergeTerm eval body = do +convergeTerm _ eval body = do heap <- get - (cache, _) <- converge (Map.empty :: Cache name a, heap :: Heap name a) $ \ (prevCache, _) -> runState Map.empty . runReader prevCache $ do + (cache, _) <- converge (Cache Map.empty :: Cache term a, heap :: Heap address a) $ \ (prevCache, _) -> runState (Cache Map.empty) . runReader prevCache $ do _ <- resetFresh . runNonDetM Set.singleton $ eval body get - pure (fromMaybe mempty (Map.lookup body cache)) + pure (fromMaybe mempty (Map.lookup body (unCache cache))) -cacheTerm :: forall m sig a name +cacheTerm :: forall m sig a term . ( Alternative m , Carrier sig m - , Member (Reader (Cache name a)) sig - , Member (State (Cache name a)) sig + , Member (Reader (Cache term a)) sig + , Member (State (Cache term a)) sig , Ord a - , Ord name + , Ord term ) - => (Term (Core.Ann :+: Core.Core) name -> m a) - -> (Term (Core.Ann :+: Core.Core) name -> m a) + => (term -> m a) + -> (term -> m a) cacheTerm eval term = do - cached <- gets (Map.lookup term) + cached <- gets (Map.lookup term . unCache) case cached :: Maybe (Set.Set a) of Just results -> foldMapA pure results Nothing -> do - results <- asks (fromMaybe mempty . Map.lookup term) - modify (Map.insert term (results :: Set.Set a)) + results <- asks (fromMaybe mempty . Map.lookup term . unCache) + modify (Cache . Map.insert term (results :: Set.Set a) . unCache) result <- eval term - result <$ modify (Map.insertWith (<>) term (Set.singleton (result :: a))) + result <$ modify (Cache . Map.insertWith (<>) term (Set.singleton (result :: a)) . unCache) -runHeap :: name -> ReaderC (FrameId name) (StateC (Heap name a) m) b -> m (Heap name a, b) -runHeap addr m = runState (Map.singleton addr Set.empty) (runReader (FrameId addr) m) +runHeap :: StateC (Heap address a) m b -> m (Heap address a, b) +runHeap m = runState (Map.empty) m -- | Fold a collection by mapping each element onto an 'Alternative' action. foldMapA :: (Alternative m, Foldable t) => (b -> m a) -> t b -> m a diff --git a/semantic-core/src/Analysis/ImportGraph.hs b/semantic-core/src/Analysis/ImportGraph.hs index f5b8a8d827..6b3bf28cdc 100644 --- a/semantic-core/src/Analysis/ImportGraph.hs +++ b/semantic-core/src/Analysis/ImportGraph.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts, OverloadedStrings, RecordWildCards, TypeOperators #-} +{-# LANGUAGE FlexibleContexts, RankNTypes, RecordWildCards, TypeApplications #-} module Analysis.ImportGraph ( ImportGraph , importGraph @@ -13,7 +13,7 @@ import Control.Effect.Fail import Control.Effect.Fresh import Control.Effect.Reader import Control.Effect.State -import qualified Data.Core as Core +import Control.Monad ((>=>)) import Data.File import Data.Foldable (fold) import Data.Function (fix) @@ -21,74 +21,93 @@ import Data.List.NonEmpty (nonEmpty) import Data.Loc import qualified Data.Map as Map import Data.Name +import Data.Proxy import qualified Data.Set as Set -import Data.Term import Data.Text (Text) import Prelude hiding (fail) type ImportGraph = Map.Map Text (Set.Set Text) -data Value = Value - { valueSemi :: Semi +data Value term = Value + { valueSemi :: Semi term , valueGraph :: ImportGraph } deriving (Eq, Ord, Show) -instance Semigroup Value where +instance Semigroup (Value term) where Value _ g1 <> Value _ g2 = Value Abstract (Map.unionWith (<>) g1 g2) -instance Monoid Value where +instance Monoid (Value term) where mempty = Value Abstract mempty -data Semi - = Closure Loc User (Term (Core.Ann :+: Core.Core) User) User +data Semi term + = Closure Loc User term -- FIXME: Bound String values. | String Text | Abstract deriving (Eq, Ord, Show) -importGraph :: [File (Term (Core.Ann :+: Core.Core) User)] -> (Heap User Value, [File (Either (Loc, String) Value)]) importGraph + :: (Ord term, Show term) + => (forall sig m + . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) + => Analysis term User (Value term) m + -> (term -> m (Value term)) + -> (term -> m (Value term)) + ) + -> [File term] + -> ( Heap User (Value term) + , [File (Either (Loc, String) (Value term))] + ) +importGraph eval = run . runFresh - . runHeap "__semantic_root" - . traverse runFile + . runHeap + . traverse (runFile eval) -runFile :: ( Carrier sig m - , Effect sig - , Member Fresh sig - , Member (Reader (FrameId User)) sig - , Member (State (Heap User Value)) sig - ) - => File (Term (Core.Ann :+: Core.Core) User) - -> m (File (Either (Loc, String) Value)) -runFile file = traverse run file +runFile + :: ( Carrier sig m + , Effect sig + , Member Fresh sig + , Member (State (Heap User (Value term))) sig + , Ord term + , Show term + ) + => (forall sig m + . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) + => Analysis term User (Value term) m + -> (term -> m (Value term)) + -> (term -> m (Value term)) + ) + -> File term + -> m (File (Either (Loc, String) (Value term))) +runFile eval file = traverse run file where run = runReader (fileLoc file) . runFailWithLoc . fmap fold - . convergeTerm (fix (cacheTerm . eval importGraphAnalysis)) + . convergeTerm (Proxy @User) (fix (cacheTerm . eval importGraphAnalysis)) -- FIXME: decompose into a product domain and two atomic domains importGraphAnalysis :: ( Alternative m , Carrier sig m - , Member (Reader (FrameId User)) sig , Member (Reader Loc) sig - , Member (State (Heap User Value)) sig + , Member (State (Heap User (Value term))) sig , MonadFail m + , Ord term + , Show term ) - => Analysis User Value m + => Analysis term User (Value term) m importGraphAnalysis = Analysis{..} where alloc = pure bind _ _ m = m lookupEnv = pure . Just - deref addr = gets (Map.lookup addr) >>= maybe (pure Nothing) (foldMapA (pure . Just)) . nonEmpty . maybe [] Set.toList + deref addr = gets (Map.lookup addr >=> nonEmpty . Set.toList) >>= maybe (pure Nothing) (foldMapA (pure . Just)) assign addr ty = modify (Map.insertWith (<>) addr (Set.singleton ty)) abstract _ name body = do loc <- ask - FrameId parentAddr <- ask - pure (Value (Closure loc name body parentAddr) mempty) - apply eval (Value (Closure loc name body _) _) a = local (const loc) $ do + pure (Value (Closure loc name body) mempty) + apply eval (Value (Closure loc name body) _) a = local (const loc) $ do addr <- alloc name assign addr a bind name addr (eval body) diff --git a/semantic-core/src/Analysis/Typecheck.hs b/semantic-core/src/Analysis/Typecheck.hs index 25d9268e1a..4e66af150e 100644 --- a/semantic-core/src/Analysis/Typecheck.hs +++ b/semantic-core/src/Analysis/Typecheck.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DeriveGeneric, DeriveTraversable, DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-} +{-# LANGUAGE DeriveGeneric, DeriveTraversable, DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, QuantifiedConstraints, RankNTypes, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-} module Analysis.Typecheck ( Monotype (..) , Meta @@ -15,9 +15,8 @@ import Control.Effect.Fail import Control.Effect.Fresh as Fresh import Control.Effect.Reader hiding (Local) import Control.Effect.State -import Control.Monad (unless) +import Control.Monad ((>=>), unless) import Control.Monad.Module -import qualified Data.Core as Core import Data.File import Data.Foldable (for_) import Data.Function (fix) @@ -29,6 +28,7 @@ import Data.Loc import qualified Data.Map as Map import Data.Maybe (fromJust, fromMaybe) import Data.Name as Name +import Data.Proxy import Data.Scope import Data.Semigroup (Last (..)) import qualified Data.Set as Set @@ -45,6 +45,8 @@ data Monotype f a | Record (Map.Map User (f a)) deriving (Foldable, Functor, Generic1, Traversable) +type Type = Term Monotype Meta + -- 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. @@ -88,26 +90,45 @@ generalize :: Term Monotype Meta -> Term (Polytype :+: Monotype) Void generalize ty = fromJust (closed (forAlls (IntSet.toList (mvs ty)) (hoistTerm R ty))) -typecheckingFlowInsensitive :: [File (Term (Core.Ann :+: Core.Core) User)] -> (Heap User (Term Monotype Meta), [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))]) typecheckingFlowInsensitive + :: Ord term + => (forall sig m + . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) + => Analysis term User Type m + -> (term -> m Type) + -> (term -> m Type) + ) + -> [File term] + -> ( Heap User Type + , [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))] + ) +typecheckingFlowInsensitive eval = run . runFresh - . runHeap "__semantic_root" + . runHeap . fmap (fmap (fmap (fmap generalize))) - . traverse runFile - -runFile :: ( Carrier sig m - , Effect sig - , Member Fresh sig - , Member (State (Heap User (Term Monotype Meta))) sig - ) - => File (Term (Core.Ann :+: Core.Core) User) - -> m (File (Either (Loc, String) (Term Monotype Meta))) -runFile file = traverse run file + . traverse (runFile eval) + +runFile + :: ( Carrier sig m + , Effect sig + , Member Fresh sig + , Member (State (Heap User Type)) sig + , Ord term + ) + => (forall sig m + . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) + => Analysis term User Type m + -> (term -> m Type) + -> (term -> m Type) + ) + -> File term + -> m (File (Either (Loc, String) Type)) +runFile eval file = traverse run file where run = (\ m -> do (subst, t) <- m - modify @(Heap User (Term Monotype Meta)) (fmap (Set.map (substAll subst))) + modify @(Heap User Type) (fmap (Set.map (substAll subst))) pure (substAll subst <$> t)) . runState (mempty :: Substitution) . runReader (fileLoc file) @@ -120,21 +141,21 @@ runFile file = traverse run file v <- meta bs <- m v <$ for_ bs (unify v)) - . convergeTerm (fix (cacheTerm . eval typecheckingAnalysis)) + . convergeTerm (Proxy @User) (fix (cacheTerm . eval typecheckingAnalysis)) typecheckingAnalysis :: ( Alternative m , Carrier sig m , Member Fresh sig , Member (State (Set.Set Constraint)) sig - , Member (State (Heap User (Term Monotype Meta))) sig + , Member (State (Heap User Type)) sig ) - => Analysis User (Term Monotype Meta) m + => Analysis term User Type m typecheckingAnalysis = Analysis{..} where alloc = pure bind _ _ m = m lookupEnv = pure . Just - deref addr = gets (Map.lookup addr) >>= maybe (pure Nothing) (foldMapA (pure . Just)) . nonEmpty . maybe [] Set.toList + deref addr = gets (Map.lookup addr >=> nonEmpty . Set.toList) >>= maybe (pure Nothing) (foldMapA (pure . Just)) assign addr ty = modify (Map.insertWith (<>) addr (Set.singleton ty)) abstract eval name body = do -- FIXME: construct the associated scope @@ -169,7 +190,7 @@ data Solution infix 5 := -meta :: (Carrier sig m, Member Fresh sig) => m (Term Monotype Meta) +meta :: (Carrier sig m, Member Fresh sig) => m Type meta = pure <$> Fresh.fresh unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Term Monotype Meta -> Term Monotype Meta -> m () @@ -177,7 +198,7 @@ unify t1 t2 | t1 == t2 = pure () | otherwise = modify (<> Set.singleton (t1 :===: t2)) -type Substitution = IntMap.IntMap (Term Monotype Meta) +type Substitution = IntMap.IntMap Type solve :: (Carrier sig m, Member (State Substitution) sig, MonadFail m) => Set.Set Constraint -> m () solve cs = for_ cs solve