diff --git a/.ghci.sample b/.ghci.sample index dcbd090ba3..8a1e7f5068 100644 --- a/.ghci.sample +++ b/.ghci.sample @@ -1,10 +1,8 @@ -- Consider copying this to your ~/.ghc/ghci.conf file: -- Pretty-printing -:set -ignore-package pretty-simple -package pretty-simple -:def! pretty \ _ -> pure ":set -interactive-print Text.Pretty.Simple.pPrint" -:def! no-pretty \ _ -> pure ":set -interactive-print System.IO.print" -:def! r \_ -> pure ":reload\n:pretty" +:set -package-id prtty-smpl-3.1.1.0-c89f0500 +:set -interactive-print Text.Pretty.Simple.pPrint -- Turn on some language extensions you use a lot :seti -XFlexibleContexts -XOverloadedStrings -XTypeApplications @@ -26,6 +24,3 @@ -- Better typed holes :set -funclutter-valid-hole-fits -fabstract-refinement-hole-fits -frefinement-level-hole-fits=2 - --- Enable pretty-printing immediately -:pretty diff --git a/.stylish-haskell.yaml b/.stylish-haskell.yaml index 19825baca3..086cfc319e 100644 --- a/.stylish-haskell.yaml +++ b/.stylish-haskell.yaml @@ -173,7 +173,7 @@ steps: # `{-#LANGUAGE #-}'. # # Default: vertical. - style: compact + style: vertical # Align affects alignment of closing pragma brackets. # @@ -183,7 +183,7 @@ steps: # between actual import and closing bracket. # # Default: true - align: true + align: false # stylish-haskell can detect redundancy of some language pragmas. If this # is set to true, it will remove those redundant pragmas. Default: true. diff --git a/script/ghci-flags b/script/ghci-flags index 34e3b145ff..dd9636bfe3 100755 --- a/script/ghci-flags +++ b/script/ghci-flags @@ -10,9 +10,6 @@ ghc_version="$(ghc --numeric-version)" # recent hie-bios requires us to output to the file at $HIE_BIOS_OUTPUT, but older builds & script/repl don’t set that var, so we default it to stdout output_file="${HIE_BIOS_OUTPUT:-/dev/stdout}" -# do a build of dependencies up front to ensure they’re all available -cabal v2-build -v0 all --only-dependencies - build_products_dir="dist-newstyle/build/x86_64-osx/ghc-$ghc_version/build-repl" function flags { @@ -43,6 +40,7 @@ function flags { echo "-isemantic-java/src" echo "-isemantic-json/src" echo "-isemantic-python/src" + echo "-isemantic-python/test" echo "-isemantic-ruby/src" echo "-isemantic-tags/src" echo "-iapp" diff --git a/script/repl b/script/repl index 668f14d305..389a07cf06 100755 --- a/script/repl +++ b/script/repl @@ -6,5 +6,8 @@ set -e cd "$(dirname "$0")/.." +# do a build of dependencies up front to ensure they’re all available +cabal v2-build all --enable-benchmarks --enable-tests --only-dependencies + # exec ghci with the appropriate flags, and without the $GHC_ENVIRONMENT variable interfering cabal v2-exec env -- -u GHC_ENVIRONMENT ghci -ghci-script=.ghci.repl $(script/ghci-flags) -no-ignore-dot-ghci $@ diff --git a/semantic-analysis/semantic-analysis.cabal b/semantic-analysis/semantic-analysis.cabal index 4e1ef28ce7..22c61b6891 100644 --- a/semantic-analysis/semantic-analysis.cabal +++ b/semantic-analysis/semantic-analysis.cabal @@ -40,12 +40,19 @@ library import: common hs-source-dirs: src exposed-modules: - Analysis.Analysis + Analysis.Carrier.Env.Monovariant + Analysis.Carrier.Env.Precise + Analysis.Carrier.Heap.Monovariant + Analysis.Carrier.Heap.Precise Analysis.Concrete + Analysis.Effect.Domain + Analysis.Effect.Env + Analysis.Effect.Heap Analysis.File Analysis.FlowInsensitive Analysis.ImportGraph - Analysis.ScopeGraph + Analysis.Intro + Analysis.Name Analysis.Typecheck Control.Carrier.Fail.WithLoc build-depends: @@ -62,3 +69,4 @@ library , semantic-source ^>= 0 , terminal-size ^>= 0.3 , text ^>= 1.2.3.1 + , transformers ^>= 0.5 diff --git a/semantic-analysis/src/Analysis/Analysis.hs b/semantic-analysis/src/Analysis/Analysis.hs deleted file mode 100644 index f9cd0549df..0000000000 --- a/semantic-analysis/src/Analysis/Analysis.hs +++ /dev/null @@ -1,26 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -module Analysis.Analysis -( Analysis(..) -) where - -import Data.Text (Text) - --- | A record of functions necessary to perform analysis. --- --- This is intended to be replaced with a selection of algebraic effects providing these interfaces and carriers providing reusable implementations. -data Analysis term name address value m = Analysis - { alloc :: name -> m address - , bind :: forall a . name -> address -> m a -> m a - , lookupEnv :: name -> m (Maybe address) - , deref :: address -> m (Maybe value) - , assign :: address -> value -> m () - , abstract :: (term name -> m value) -> name -> term name -> m value - , apply :: (term name -> 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 :: [(name, value)] -> m value - , (...) :: address -> name -> m (Maybe address) - } diff --git a/semantic-analysis/src/Analysis/Carrier/Env/Monovariant.hs b/semantic-analysis/src/Analysis/Carrier/Env/Monovariant.hs new file mode 100644 index 0000000000..3c834d0aae --- /dev/null +++ b/semantic-analysis/src/Analysis/Carrier/Env/Monovariant.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-} +module Analysis.Carrier.Env.Monovariant +( -- * Env carrier + EnvC(..) + -- * Env effect +, module Analysis.Effect.Env +) where + +import Analysis.Effect.Env +import Analysis.Name +import Control.Algebra +import qualified Control.Monad.Fail as Fail + +newtype EnvC m a = EnvC { runEnv :: m a } + deriving (Applicative, Functor, Monad, Fail.MonadFail) + +instance Algebra sig m + => Algebra (Env Name :+: sig) (EnvC m) where + alg (L (Alloc name k)) = k name + alg (L (Bind _ _ m k)) = m >>= k + alg (L (Lookup name k)) = k (Just name) + alg (R other) = EnvC (alg (handleCoercible other)) diff --git a/semantic-analysis/src/Analysis/Carrier/Env/Precise.hs b/semantic-analysis/src/Analysis/Carrier/Env/Precise.hs new file mode 100644 index 0000000000..1e0b7666e1 --- /dev/null +++ b/semantic-analysis/src/Analysis/Carrier/Env/Precise.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-} +module Analysis.Carrier.Env.Precise +( -- * Env carrier + EnvC(..) + -- * Env effect +, A.alloc +, A.bind +, A.lookupEnv +, A.Env(..) +) where + +import qualified Analysis.Effect.Env as A +import Analysis.Name +import Control.Algebra +import Control.Effect.Fresh +import Control.Effect.Reader +import qualified Control.Monad.Fail as Fail +import qualified Data.Map as Map + +type Precise = Int +type Env = Map.Map Name Precise + +newtype EnvC m a = EnvC { runEnv :: m a } + deriving (Applicative, Functor, Monad, Fail.MonadFail) + +instance ( Has Fresh sig m + , Has (Reader Env) sig m + ) + => Algebra (A.Env Precise :+: sig) (EnvC m) where + alg (L (A.Alloc _ k)) = fresh >>= k + alg (L (A.Bind name addr m k)) = local (Map.insert name addr) m >>= k + alg (L (A.Lookup name k)) = asks (Map.lookup name) >>= k + alg (R other) = EnvC (alg (handleCoercible other)) diff --git a/semantic-analysis/src/Analysis/Carrier/Heap/Monovariant.hs b/semantic-analysis/src/Analysis/Carrier/Heap/Monovariant.hs new file mode 100644 index 0000000000..1aec53052b --- /dev/null +++ b/semantic-analysis/src/Analysis/Carrier/Heap/Monovariant.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-} +module Analysis.Carrier.Heap.Monovariant +( -- * Heap carrier + HeapC(..) + -- * Heap effect +, module Analysis.Effect.Heap +) where + +import Analysis.Effect.Heap +import Control.Applicative (Alternative) +import Control.Algebra +import Control.Effect.State +import Control.Monad ((>=>)) +import qualified Control.Monad.Fail as Fail +import Data.List.NonEmpty (nonEmpty) +import qualified Data.Map as Map +import Data.Monoid (Alt(..)) +import qualified Data.Set as Set + +newtype HeapC addr value m a = HeapC { runHeap :: m a } + deriving (Alternative, Applicative, Functor, Monad, Fail.MonadFail) + +instance ( Alternative m + , Has (State (Map.Map addr (Set.Set value))) sig m + , Ord addr + , Ord value + ) + => Algebra (Heap addr value :+: sig) (HeapC addr value m) where + alg (L (Deref addr k)) = gets (Map.lookup addr >=> nonEmpty . Set.toList) >>= maybe (pure Nothing) (getAlt . foldMap (Alt . pure . Just)) >>= k + alg (L (Assign addr value k)) = modify (Map.insertWith (<>) addr (Set.singleton value)) >> k + alg (R other) = HeapC (alg (handleCoercible other)) diff --git a/semantic-analysis/src/Analysis/Carrier/Heap/Precise.hs b/semantic-analysis/src/Analysis/Carrier/Heap/Precise.hs new file mode 100644 index 0000000000..2f8a738a98 --- /dev/null +++ b/semantic-analysis/src/Analysis/Carrier/Heap/Precise.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, TypeOperators, UndecidableInstances #-} +module Analysis.Carrier.Heap.Precise +( -- * Heap carrier + runHeap +, HeapC(..) + -- * Heap effect +, module Analysis.Effect.Heap +) where + +import Analysis.Effect.Heap +import Control.Algebra +import Control.Carrier.State.Strict +import qualified Control.Monad.Fail as Fail +import qualified Data.IntMap as IntMap + +type Precise = Int + +runHeap :: HeapC value m a -> m (IntMap.IntMap value, a) +runHeap (HeapC m) = runState mempty m + +newtype HeapC value m a = HeapC (StateC (IntMap.IntMap value) m a) + deriving (Applicative, Functor, Monad, Fail.MonadFail) + +instance (Algebra sig m, Effect sig) + => Algebra (Heap Precise value :+: State (IntMap.IntMap value) :+: sig) (HeapC value m) where + alg (L (Deref addr k)) = HeapC (gets (IntMap.lookup addr)) >>= k + alg (L (Assign addr value k)) = HeapC (modify (IntMap.insert addr value)) >> k + alg (R other) = HeapC (alg (handleCoercible other)) diff --git a/semantic-analysis/src/Analysis/Concrete.hs b/semantic-analysis/src/Analysis/Concrete.hs index 2bc8fb6183..0931a37150 100644 --- a/semantic-analysis/src/Analysis/Concrete.hs +++ b/semantic-analysis/src/Analysis/Concrete.hs @@ -1,10 +1,22 @@ -{-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, - OverloadedStrings, RankNTypes, RecordWildCards, ScopedTypeVariables, TypeApplications, TypeOperators, - UndecidableInstances #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Analysis.Concrete ( Concrete(..) , concrete -, concreteAnalysis , heapGraph , heapValueGraph , heapAddressGraph @@ -13,175 +25,132 @@ module Analysis.Concrete import qualified Algebra.Graph as G import qualified Algebra.Graph.Export.Dot as G -import Analysis.Analysis +import qualified Analysis.Carrier.Env.Precise as A +import qualified Analysis.Carrier.Heap.Precise as A +import qualified Analysis.Effect.Domain as A import Analysis.File +import Analysis.Name import Control.Algebra import Control.Carrier.Fail.WithLoc import Control.Carrier.Fresh.Strict -import Control.Carrier.NonDet.Church import Control.Carrier.Reader hiding (Local) -import Control.Carrier.State.Strict -import Control.Monad ((<=<)) +import Control.Monad.Trans.Class (MonadTrans (..)) import Data.Function (fix) import qualified Data.IntMap as IntMap -import qualified Data.IntSet as IntSet import qualified Data.Map as Map import Data.Semigroup (Last (..)) -import qualified Data.Set as Set -import Data.String (IsString) import Data.Text (Text, pack) import Data.Traversable (for) import Prelude hiding (fail) import Source.Span +import Syntax.Scope import qualified System.Path as Path -type Precise = Int -type Env name = Map.Map name Precise +type Addr = Int +type Env = Map.Map Name Addr -newtype FrameId = FrameId { unFrameId :: Precise } - deriving (Eq, Ord, Show) - -data Concrete term name - = Closure Path.AbsRelFile Span name (term name) (Env name) +data Concrete term + = Closure Path.AbsRelFile Span (Named (Scope () term Addr)) | Unit | Bool Bool | String Text - | Record (Env name) - deriving (Eq, Ord, Show) + | Record Env -- 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 term name) + deriving Semigroup via Last (Concrete term) -recordFrame :: Concrete term name -> Maybe (Env name) -recordFrame (Record frame) = Just frame -recordFrame _ = Nothing +deriving instance ( forall a . Eq a => Eq (f a), Monad f) => Eq (Concrete f) +deriving instance ( forall a . Eq a => Eq (f a) + , forall a . Ord a => Ord (f a), Monad f) => Ord (Concrete f) +deriving instance ( forall a . Show a => Show (f a)) => Show (Concrete f) -newtype Frame name = Frame - { frameSlots :: Env name - } - deriving (Eq, Ord, Show) -type Heap term name = IntMap.IntMap (Concrete term name) - -data Edge = Lexical | Import - deriving (Eq, Ord, Show) +type Heap = IntMap.IntMap concrete - :: ( Foldable term - , IsString name - , Ord name - , Show name - , Show (term name) - ) + :: Applicative term => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name Precise (Concrete term name) m - -> (term name -> m (Concrete term name)) - -> (term name -> m (Concrete term name)) + . (Has (A.Domain term Addr (Concrete term) :+: A.Env Addr :+: A.Heap Addr (Concrete term) :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) + => (term Addr -> m (Concrete term)) + -> (term Addr -> m (Concrete term)) ) - -> [File (term name)] - -> (Heap term name, [File (Either (Path.AbsRelFile, Span, String) (Concrete term name))]) + -> [File (term Addr)] + -> (Heap (Concrete term), [File (Either (Path.AbsRelFile, Span, String) (Concrete term))]) concrete eval = run . evalFresh 0 - . runHeap + . A.runHeap . traverse (runFile eval) runFile - :: forall term name m sig - . ( Effect sig - , Foldable term - , IsString name + :: forall term m sig + . ( Applicative term + , Effect sig , Has Fresh sig m - , Has (State (Heap term name)) sig m - , Ord name - , Show name - , Show (term name) + , Has (A.Heap Addr (Concrete term)) sig m ) => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name Precise (Concrete term name) m - -> (term name -> m (Concrete term name)) - -> (term name -> m (Concrete term name)) + . (Has (A.Domain term Addr (Concrete term) :+: A.Env Addr :+: A.Heap Addr (Concrete term) :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) + => (term Addr -> m (Concrete term)) + -> (term Addr -> m (Concrete term)) ) - -> File (term name) - -> m (File (Either (Path.AbsRelFile, Span, String) (Concrete term name))) + -> File (term Addr) + -> m (File (Either (Path.AbsRelFile, Span, String) (Concrete term))) runFile eval file = traverse run file where run = runReader (filePath file) . runReader (fileSpan file) . runFail - . runReader @(Env name) mempty - . fix (eval concreteAnalysis) - -concreteAnalysis - :: ( Foldable term - , IsString name - , Has Fresh sig m - , Has (Reader (Env name)) sig m - , Has (Reader Path.AbsRelFile) sig m - , Has (Reader Span) sig m - , Has (State (Heap term name)) sig m - , MonadFail m - , Ord name - , Show name - , Show (term name) - ) - => Analysis term name Precise (Concrete term name) m -concreteAnalysis = Analysis{..} - where alloc _ = fresh - bind name addr m = local (Map.insert name addr) m - lookupEnv n = asks (Map.lookup n) - deref = gets . IntMap.lookup - assign addr value = modify (IntMap.insert addr value) - abstract _ name body = do - path <- ask - span <- ask - env <- asks (flip Map.restrictKeys (Set.delete name (foldMap Set.singleton body))) - pure (Closure path span name body env) - apply eval (Closure path span name body env) a = do - local (const path) . local (const span) $ do - addr <- alloc name - assign addr a - local (const (Map.insert name addr env)) (eval body) - apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function" - unit = pure Unit - bool b = pure (Bool b) - asBool (Bool b) = pure b - asBool v = fail $ "Cannot coerce " <> show v <> " to Bool" - string s = pure (String s) - asString (String s) = pure s - asString v = fail $ "Cannot coerce " <> show v <> " to String" - record fields = do - fields' <- for fields $ \ (name, value) -> do - addr <- alloc name - assign addr value - pure (name, addr) - pure (Record (Map.fromList fields')) - addr ... n = do - val <- deref addr - heap <- get - pure (val >>= lookupConcrete heap n) - - -lookupConcrete :: (IsString name, Ord name) => Heap term name -> name -> Concrete term name -> Maybe Precise -lookupConcrete heap name = run . evalState IntSet.empty . runNonDetA . inConcrete - where -- look up the name in a concrete value - inConcrete = inFrame <=< maybeA . recordFrame - -- look up the name in a specific 'Frame', with slots taking precedence over parents - inFrame fs = maybeA (Map.lookup name fs) <|> (maybeA (Map.lookup "__semantic_super" fs) >>= inAddress) - -- look up the name in the value an address points to, if we haven’t already visited it - inAddress addr = do - visited <- get - guard (addr `IntSet.notMember` visited) - -- FIXME: throw an error if we can’t deref @addr@ - val <- maybeA (IntMap.lookup addr heap) - modify (IntSet.insert addr) - inConcrete val - maybeA = maybe empty pure - - -runHeap :: StateC (Heap term name) m a -> m (Heap term name, a) -runHeap = runState mempty + . runReader @Env mempty + . A.runEnv + . fix (\ eval' -> runDomain eval' . fix eval) + + +runDomain :: (term Addr -> m (Concrete term)) -> DomainC term m a -> m a +runDomain eval (DomainC m) = runReader eval m + +newtype DomainC term m a = DomainC (ReaderC (term Addr -> m (Concrete term)) m a) + deriving (Applicative, Functor, Monad, MonadFail) + +instance MonadTrans (DomainC term) where + lift = DomainC . lift + +instance ( Applicative term + , Has (A.Env Addr) sig m + , Has (A.Heap Addr (Concrete term)) sig m + , Has (Reader Path.AbsRelFile) sig m + , Has (Reader Span) sig m + , MonadFail m + ) + => Algebra (A.Domain term Addr (Concrete term) :+: sig) (DomainC term m) where + alg = \case + L (L (A.Unit k)) -> k Unit + L (R (L (A.Bool b k))) -> k (Bool b) + L (R (L (A.AsBool c k))) -> case c of + Bool b -> k b + _ -> fail "expected Bool" + L (R (R (L (A.String s k)))) -> k (String s) + L (R (R (L (A.AsString c k)))) -> case c of + String s -> k s + _ -> fail "expected String" + L (R (R (R (L (A.Lam b k))))) -> do + path <- ask + span <- ask + k (Closure path span b) + L (R (R (R (L (A.AsLam c k))))) -> case c of + Closure _ _ b -> k b + _ -> fail "expected Closure" + L (R (R (R (R (A.Record fields k))))) -> do + eval <- DomainC ask + fields' <- for fields $ \ (name, t) -> do + addr <- A.alloc name + v <- lift (eval t) + A.assign @Addr @(Concrete term) addr v + pure (name, addr) + k (Record (Map.fromList fields')) + L (R (R (R (R (A.AsRecord c k))))) -> case c of + Record fields -> k (map (fmap pure) (Map.toList fields)) + _ -> fail "expected Record" + R other -> DomainC (send (handleCoercible other)) -- | 'heapGraph', 'heapValueGraph', and 'heapAddressGraph' allow us to conveniently export SVGs of the heap: @@ -189,25 +158,25 @@ 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 term name -> a) -> (Either Edge name -> Precise -> G.Graph a) -> Heap term name -> G.Graph a +heapGraph :: Foldable term => (Addr -> Concrete term -> a) -> (Either Edge Name -> Addr -> G.Graph a) -> Heap (Concrete 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 Unit -> G.empty Bool _ -> G.empty String _ -> G.empty - Closure _ _ _ _ env -> foldr (G.overlay . edge (Left Lexical)) G.empty env + Closure _ _ (Named _ b) -> foldr (G.overlay . edge (Left Lexical)) G.empty b Record frame -> Map.foldrWithKey (\ k -> G.overlay . edge (Right k)) G.empty frame -heapValueGraph :: Heap term name -> G.Graph (Concrete term name) +heapValueGraph :: Foldable term => Heap (Concrete 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 term name -> G.Graph (EdgeType term name, Precise) +heapAddressGraph :: Foldable term => Heap (Concrete term) -> G.Graph (EdgeType (Concrete term), Addr) heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G.vertex . (,) . either Edge Slot) -addressStyle :: (name -> Text) -> Heap term name -> G.Style (EdgeType term name, Precise) Text -addressStyle unName heap = (G.defaultStyle vertex) { G.edgeAttributes } +addressStyle :: Heap (Concrete term) -> G.Style (EdgeType (Concrete term), Addr) 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.:= unName name] edgeAttributes _ (Edge Import, _) = ["color" G.:= "blue"] @@ -217,12 +186,15 @@ addressStyle unName heap = (G.defaultStyle vertex) { G.edgeAttributes } Unit -> "()" Bool b -> pack $ show b String s -> pack $ show s - Closure p (Span s e) n _ _ -> "\\\\ " <> unName n <> " [" <> pack (Path.toString p) <> ":" <> showPos s <> "-" <> showPos e <> "]" + Closure p (Span s e) (Named n _) -> "\\\\ " <> unName n <> " [" <> pack (Path.toString p) <> ":" <> showPos s <> "-" <> showPos e <> "]" Record _ -> "{}" showPos (Pos l c) = pack (show l) <> ":" <> pack (show c) -data EdgeType term name +data EdgeType value = Edge Edge - | Slot name - | Value (Concrete term name) + | Slot Name + | Value value + deriving (Eq, Ord, Show) + +data Edge = Lexical | Import deriving (Eq, Ord, Show) diff --git a/semantic-analysis/src/Analysis/Effect/Domain.hs b/semantic-analysis/src/Analysis/Effect/Domain.hs new file mode 100644 index 0000000000..1b8c479516 --- /dev/null +++ b/semantic-analysis/src/Analysis/Effect/Domain.hs @@ -0,0 +1,111 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE TypeOperators #-} +module Analysis.Effect.Domain +( -- * Domain effect + unit +, UnitDomain(..) +, bool +, asBool +, BoolDomain(..) +, string +, asString +, StringDomain(..) +, lam +, asLam +, FunctionDomain(..) +, record +, asRecord +, RecordDomain(..) +, Domain + -- * Re-exports +, Algebra +, Has +, run +) where + +import Analysis.Name +import Control.Algebra +import Data.Text (Text) +import GHC.Generics (Generic1) +import Syntax.Scope (Scope) + +unit :: Has (UnitDomain value) sig m => m value +unit = send (Unit pure) + +data UnitDomain value m k + = Unit (value -> m k) + deriving (Functor, Generic1) + +instance HFunctor (UnitDomain value) +instance Effect (UnitDomain value) + + +bool :: Has (BoolDomain value) sig m => Bool -> m value +bool b = send (Bool b pure) + +asBool :: Has (BoolDomain value) sig m => value -> m Bool +asBool v = send (AsBool v pure) + +data BoolDomain value m k + = Bool Bool (value -> m k) + | AsBool value (Bool -> m k) + deriving (Functor, Generic1) + +instance HFunctor (BoolDomain value) +instance Effect (BoolDomain value) + + +string :: Has (StringDomain value) sig m => Text -> m value +string s = send (String s pure) + +asString :: Has (StringDomain value) sig m => value -> m Text +asString v = send (AsString v pure) + +data StringDomain value m k + = String Text (value -> m k) + | AsString value (Text -> m k) + deriving (Functor, Generic1) + +instance HFunctor (StringDomain value) +instance Effect (StringDomain value) + + +lam :: Has (FunctionDomain term addr value) sig m => Named (Scope () term addr) -> m value +lam b = send (Lam b pure) + +-- FIXME: Support partial concretization of lambdas. +asLam :: Has (FunctionDomain term addr value) sig m => value -> m (Named (Scope () term addr)) +asLam v = send (AsLam v pure) + +data FunctionDomain term addr value m k + = Lam (Named (Scope () term addr)) (value -> m k) + | AsLam value (Named (Scope () term addr) -> m k) + deriving (Functor, Generic1) + +instance HFunctor (FunctionDomain term addr value) +instance Effect (FunctionDomain term addr value) + + +record :: Has (RecordDomain term addr value) sig m => [(Name, term addr)] -> m value +record fs = send (Record fs pure) + +-- FIXME: Support partial concretization of records. +asRecord :: Has (RecordDomain term addr value) sig m => value -> m [(Name, term addr)] +asRecord v = send (AsRecord v pure) + +data RecordDomain term addr value m k + = Record [(Name, term addr)] (value -> m k) + | AsRecord value ([(Name, term addr)] -> m k) + deriving (Functor, Generic1) + +instance HFunctor (RecordDomain term addr value) +instance Effect (RecordDomain term addr value) + + +type Domain term addr value + = UnitDomain value + :+: BoolDomain value + :+: StringDomain value + :+: FunctionDomain term addr value + :+: RecordDomain term addr value diff --git a/semantic-analysis/src/Analysis/Effect/Env.hs b/semantic-analysis/src/Analysis/Effect/Env.hs new file mode 100644 index 0000000000..0e7c3a63c3 --- /dev/null +++ b/semantic-analysis/src/Analysis/Effect/Env.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE DeriveFunctor, ExistentialQuantification, FlexibleContexts, LambdaCase, StandaloneDeriving #-} +module Analysis.Effect.Env +( -- * Env effect + alloc +, bind +, lookupEnv +, Env(..) + -- * Re-exports +, Algebra +, Has +, run +) where + +import Analysis.Name +import Control.Algebra + +alloc :: Has (Env addr) sig m => Name -> m addr +alloc name = send (Alloc name pure) + +bind :: Has (Env addr) sig m => Name -> addr -> m a -> m a +bind name addr m = send (Bind name addr m pure) + +lookupEnv :: Has (Env addr) sig m => Name -> m (Maybe addr) +lookupEnv name = send (Lookup name pure) + + +data Env addr m k + = Alloc Name (addr -> m k) + | forall a . Bind Name addr (m a) (a -> m k) + | Lookup Name (Maybe addr -> m k) + +deriving instance Functor m => Functor (Env addr m) + +instance HFunctor (Env addr) where + hmap f = \case + Alloc name k -> Alloc name (f . k) + Bind name addr m k -> Bind name addr (f m) (f . k) + Lookup name k -> Lookup name (f . k) + +instance Effect (Env addr) where + thread ctx hdl = \case + Alloc name k -> Alloc name (hdl . (<$ ctx) . k) + Bind name addr m k -> Bind name addr (hdl (m <$ ctx)) (hdl . fmap k) + Lookup name k -> Lookup name (hdl . (<$ ctx) . k) diff --git a/semantic-analysis/src/Analysis/Effect/Heap.hs b/semantic-analysis/src/Analysis/Effect/Heap.hs new file mode 100644 index 0000000000..94c2cb18c0 --- /dev/null +++ b/semantic-analysis/src/Analysis/Effect/Heap.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts #-} +module Analysis.Effect.Heap +( -- * Heap effect + deref +, assign +, Heap(..) + -- * Re-exports +, Algebra +, Has +, run +) where + +import Control.Algebra +import GHC.Generics (Generic1) + +deref :: Has (Heap addr value) sig m => addr -> m (Maybe value) +deref addr = send (Deref addr pure) + +assign :: Has (Heap addr value) sig m => addr -> value -> m () +assign addr value = send (Assign addr value (pure ())) + + +data Heap addr value m k + = Deref addr (Maybe value -> m k) + | Assign addr value (m k) + deriving (Functor, Generic1) + +instance HFunctor (Heap addr value) +instance Effect (Heap addr value) diff --git a/semantic-analysis/src/Analysis/FlowInsensitive.hs b/semantic-analysis/src/Analysis/FlowInsensitive.hs index bb744194ca..4b5701a8d0 100644 --- a/semantic-analysis/src/Analysis/FlowInsensitive.hs +++ b/semantic-analysis/src/Analysis/FlowInsensitive.hs @@ -1,14 +1,13 @@ {-# LANGUAGE FlexibleContexts, OverloadedStrings, ScopedTypeVariables, TypeOperators #-} module Analysis.FlowInsensitive ( Heap -, FrameId(..) -, Cache , convergeTerm , cacheTerm , runHeap , foldMapA ) where +import Analysis.Name import Control.Algebra import Control.Carrier.Fresh.Strict import Control.Carrier.NonDet.Church @@ -18,55 +17,50 @@ import qualified Data.Map as Map import Data.Maybe (fromMaybe) import qualified Data.Set as Set -newtype Cache term a = Cache { unCache :: Map.Map term (Set.Set a) } +newtype Cache term value = Cache { unCache :: Map.Map term (Set.Set value) } deriving (Eq, Ord, Show) -type Heap address a = Map.Map address (Set.Set a) - -newtype FrameId name = FrameId { unFrameId :: name } - deriving (Eq, Ord, Show) +type Heap value = Map.Map Name (Set.Set value) -convergeTerm :: forall m sig a term address proxy +convergeTerm :: forall term value m sig . ( Effect sig - , Eq address , Has Fresh sig m - , Has (State (Heap address a)) sig m - , Ord a + , Has (State (Heap value)) sig m , Ord term + , Ord value ) - => proxy address - -> Int - -> (term -> NonDetC (FreshC (ReaderC (Cache term a) (StateC (Cache term a) m))) a) + => Int + -> (term -> NonDetC (FreshC (ReaderC (Cache term value) (StateC (Cache term value) m))) value) -> term - -> m (Set.Set a) -convergeTerm _ n eval body = do + -> m (Set.Set value) +convergeTerm n eval body = do heap <- get - (cache, _) <- converge (Cache Map.empty :: Cache term a, heap :: Heap address a) $ \ (prevCache, _) -> runState (Cache Map.empty) . runReader prevCache $ do - _ <- runFresh n . runNonDetM Set.singleton $ eval body + (cache, _) <- converge (Cache Map.empty :: Cache term value, heap :: Heap value) $ \ (prevCache, _) -> runState (Cache Map.empty) . runReader prevCache $ do + _ <- evalFresh n . runNonDetM Set.singleton $ eval body get pure (fromMaybe mempty (Map.lookup body (unCache cache))) -cacheTerm :: forall m sig a term +cacheTerm :: forall term value m sig . ( Alternative m - , Has (Reader (Cache term a)) sig m - , Has (State (Cache term a)) sig m - , Ord a + , Has (Reader (Cache term value)) sig m + , Has (State (Cache term value)) sig m , Ord term + , Ord value ) - => (term -> m a) - -> (term -> m a) + => (term -> m value) + -> (term -> m value) cacheTerm eval term = do cached <- gets (Map.lookup term . unCache) - case cached :: Maybe (Set.Set a) of + case cached :: Maybe (Set.Set value) of Just results -> foldMapA pure results Nothing -> do results <- asks (fromMaybe mempty . Map.lookup term . unCache) - modify (Cache . Map.insert term (results :: Set.Set a) . unCache) + modify (Cache . Map.insert term (results :: Set.Set value) . unCache) result <- eval term - result <$ modify (Cache . Map.insertWith (<>) term (Set.singleton (result :: a)) . unCache) + result <$ modify (Cache . Map.insertWith (<>) term (Set.singleton (result :: value)) . unCache) -runHeap :: StateC (Heap address a) m b -> m (Heap address a, b) +runHeap :: StateC (Heap value) m a -> m (Heap value, a) runHeap m = runState Map.empty m -- | Iterate a monadic action starting from some initial seed until the results converge. diff --git a/semantic-analysis/src/Analysis/ImportGraph.hs b/semantic-analysis/src/Analysis/ImportGraph.hs index 88a3082b66..ee2af77c23 100644 --- a/semantic-analysis/src/Analysis/ImportGraph.hs +++ b/semantic-analysis/src/Analysis/ImportGraph.hs @@ -1,64 +1,86 @@ -{-# LANGUAGE FlexibleContexts, RankNTypes, RecordWildCards, ScopedTypeVariables, TypeApplications #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Analysis.ImportGraph ( ImportGraph , importGraph -, importGraphAnalysis ) where -import Analysis.Analysis +import Analysis.Carrier.Env.Monovariant +import qualified Analysis.Carrier.Heap.Monovariant as A +import qualified Analysis.Effect.Domain as A import Analysis.File import Analysis.FlowInsensitive -import Control.Applicative (Alternative(..)) +import Analysis.Name import Control.Algebra +import Control.Applicative (Alternative (..)) import Control.Carrier.Fail.WithLoc import Control.Carrier.Fresh.Strict import Control.Carrier.Reader import Control.Carrier.State.Strict -import Control.Monad ((>=>)) -import Data.Foldable (fold, for_) +import Control.Monad.Trans.Class +import Data.Foldable (fold) import Data.Function (fix) -import Data.List.NonEmpty (nonEmpty) import qualified Data.Map as Map -import Data.Proxy import qualified Data.Set as Set import Data.Text (Text) +import Data.Traversable (for) import Prelude hiding (fail) import Source.Span +import Syntax.Scope (Scope) import qualified System.Path as Path type ImportGraph = Map.Map Text (Set.Set Text) -data Value term name = Value - { valueSemi :: Semi term name +type Addr = Name + +data Value semi = Value + { valueSemi :: semi , valueGraph :: ImportGraph } deriving (Eq, Ord, Show) -instance Semigroup (Value term name) where +instance Semigroup (Value (Semi term)) where Value _ g1 <> Value _ g2 = Value Abstract (Map.unionWith (<>) g1 g2) -instance Monoid (Value term name) where +instance Monoid (Value (Semi term)) where mempty = Value Abstract mempty -data Semi term name - = Closure Path.AbsRelFile Span name (term name) +data Semi term + = Closure Path.AbsRelFile Span (Named (Scope () term Addr)) -- FIXME: Bound String values. | String Text | Abstract - deriving (Eq, Ord, Show) + +deriving instance ( forall a . Eq a => Eq (f a), Monad f) => Eq (Semi f) +deriving instance ( forall a . Eq a => Eq (f a) + , forall a . Ord a => Ord (f a), Monad f) => Ord (Semi f) +deriving instance ( forall a . Show a => Show (f a)) => Show (Semi f) importGraph - :: (Ord name, Ord (term name), Show name, Show (term name)) + :: ( Monad term + , forall a . Eq a => Eq (term a) + , forall a . Ord a => Ord (term a) + ) => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name name (Value term name) m - -> (term name -> m (Value term name)) - -> (term name -> m (Value term name)) + . (Has (A.Domain term Addr (Value (Semi term)) :+: Env Addr :+: A.Heap Addr (Value (Semi term)) :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) + => (term Addr -> m (Value (Semi term))) + -> (term Addr -> m (Value (Semi term))) ) - -> [File (term name)] - -> ( Heap name (Value term name) - , [File (Either (Path.AbsRelFile, Span, String) (Value term name))] + -> [File (term Addr)] + -> ( Heap (Value (Semi term)) + , [File (Either (Path.AbsRelFile, Span, String) (Value (Semi term)))] ) importGraph eval = run @@ -67,66 +89,61 @@ importGraph eval . traverse (runFile eval) runFile - :: forall term name m sig + :: forall term m sig . ( Effect sig , Has Fresh sig m - , Has (State (Heap name (Value term name))) sig m - , Ord name - , Ord (term name) - , Show name - , Show (term name) + , Has (State (Heap (Value (Semi term)))) sig m + , Monad term + , forall a . Eq a => Eq (term a) + , forall a . Ord a => Ord (term a) ) => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name name (Value term name) m - -> (term name -> m (Value term name)) - -> (term name -> m (Value term name)) + . (Has (A.Domain term Addr (Value (Semi term)) :+: Env Addr :+: A.Heap Addr (Value (Semi term)) :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) + => (term Addr -> m (Value (Semi term))) + -> (term Addr -> m (Value (Semi term))) ) - -> File (term name) - -> m (File (Either (Path.AbsRelFile, Span, String) (Value term name))) + -> File (term Addr) + -> m (File (Either (Path.AbsRelFile, Span, String) (Value (Semi term)))) runFile eval file = traverse run file where run = runReader (filePath file) . runReader (fileSpan file) + . runEnv . runFail . fmap fold - . convergeTerm (Proxy @name) 0 (fix (cacheTerm . eval importGraphAnalysis)) + . convergeTerm 0 (A.runHeap @Addr @(Value (Semi term)) . fix (\ eval' -> runDomain eval' . fix (cacheTerm . eval))) + + +runDomain :: (term Addr -> m (Value (Semi term))) -> DomainC term m a -> m a +runDomain eval (DomainC m) = runReader eval m + +newtype DomainC term m a = DomainC (ReaderC (term Addr -> m (Value (Semi term))) m a) + deriving (Alternative, Applicative, Functor, Monad, MonadFail) + +instance MonadTrans (DomainC term) where + lift = DomainC . lift -- FIXME: decompose into a product domain and two atomic domains -importGraphAnalysis :: ( Alternative m - , Has (Reader Path.AbsRelFile) sig m - , Has (Reader Span) sig m - , Has (State (Heap name (Value term name))) sig m - , MonadFail m - , Ord name - , Ord (term name) - , Show name - , Show (term name) - ) - => Analysis term name name (Value term name) m -importGraphAnalysis = Analysis{..} - where alloc = pure - bind _ _ m = m - lookupEnv = pure . Just - deref addr = gets (Map.lookup addr >=> nonEmpty . Set.toList) >>= maybe (pure Nothing) (foldMapA (pure . Just)) - assign addr v = modify (Map.insertWith (<>) addr (Set.singleton v)) - abstract _ name body = do - path <- ask - span <- ask - pure (Value (Closure path span name body) mempty) - apply eval (Value (Closure path span name body) _) a = local (const path) . local (const span) $ do - addr <- alloc name - assign addr a - bind name addr (eval body) - apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function" - unit = pure mempty - bool _ = pure mempty - asBool _ = pure True <|> pure False - string s = pure (Value (String s) mempty) - asString (Value (String s) _) = pure s - asString _ = pure mempty - record fields = do - for_ fields $ \ (k, v) -> do - addr <- alloc k - assign addr v - pure (Value Abstract (foldMap (valueGraph . snd) fields)) - _ ... m = pure (Just m) +instance (Alternative m, Has (Env Addr :+: A.Heap Addr (Value (Semi term)) :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) => Algebra (A.Domain term Addr (Value (Semi term)) :+: sig) (DomainC term m) where + alg = \case + L (L (A.Unit k)) -> k mempty + L (R (L (A.Bool _ k))) -> k mempty + L (R (L (A.AsBool _ k))) -> k True <|> k False + L (R (R (L (A.String s k)))) -> k (Value (String s) mempty) + L (R (R (L (A.AsString _ k)))) -> k mempty + L (R (R (R (L (A.Lam b k))))) -> do + path <- ask + span <- ask + k (Value (Closure path span b) mempty) + L (R (R (R (L (A.AsLam (Value v _) k))))) -> case v of + Closure _ _ b -> k b + String _ -> fail $ "expected closure, got String" + Abstract -> fail $ "expected closure, got Abstract" + L (R (R (R (R (A.Record f k))))) -> do + eval <- DomainC ask + fields <- for f $ \ (k, t) -> do + addr <- alloc @Addr k + v <- lift (eval t) + v <$ A.assign @Addr @(Value (Semi term)) addr v + k (fold fields) + L (R (R (R (R (A.AsRecord _ k))))) -> k [] + R other -> DomainC (send (handleCoercible other)) diff --git a/semantic-analysis/src/Analysis/Intro.hs b/semantic-analysis/src/Analysis/Intro.hs new file mode 100644 index 0000000000..440f177e3e --- /dev/null +++ b/semantic-analysis/src/Analysis/Intro.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE StandaloneDeriving #-} +module Analysis.Intro +( Intro(..) +, unit +, bool +, string +, lam +, record +) where + +import Analysis.Name +import Control.Algebra +import Data.Text (Text) +import GHC.Generics (Generic1) +import Syntax.Foldable +import Syntax.Module +import Syntax.Scope +import Syntax.Traversable + +data Intro t a + = Unit + | Bool Bool + | String Text + | Lam (Named (Scope () t a)) + | Record [(Name, t a)] + deriving (Foldable, Functor, Generic1, Traversable) + +deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Intro f a) +deriving instance (Ord a, forall a . Eq a => Eq (f a) + , forall a . Ord a => Ord (f a), Monad f) => Ord (Intro f a) +deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Intro f a) + +instance HFunctor Intro +instance HFoldable Intro +instance HTraversable Intro + +instance RightModule Intro where + Unit >>=* _ = Unit + Bool b >>=* _ = Bool b + String s >>=* _ = String s + Lam b >>=* f = Lam ((>>=* f) <$> b) + Record t >>=* f = Record (map (fmap (>>= f)) t) + + +unit :: Has Intro sig m => m a +unit = send Unit + +bool :: Has Intro sig m => Bool -> m a +bool = send . Bool + +string :: Has Intro sig m => Text -> m a +string = send . String + + +lam :: (Eq a, Has Intro sig m) => Named a -> m a -> m a +lam (Named u n) b = send (Lam (Named u (abstract1 n b))) + + +record :: Has Intro sig m => [(Name, m a)] -> m a +record = send . Record diff --git a/semantic-analysis/src/Analysis/Name.hs b/semantic-analysis/src/Analysis/Name.hs new file mode 100644 index 0000000000..024b4eda1c --- /dev/null +++ b/semantic-analysis/src/Analysis/Name.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE DeriveTraversable, GeneralizedNewtypeDeriving #-} +module Analysis.Name +( Name(..) +, Named(..) +, named +, named' +, namedName +, namedValue +) where + +import Data.Function (on) +import Data.String (IsString) +import Data.Text (Text) + +-- | User-specified and -relevant names. +newtype Name = Name { unName :: Text } + deriving (Eq, IsString, Ord, Show) + + +-- | Annotates an @a@ with a 'Name'-provided name, which is ignored for '==' and 'compare'. +data Named a = Named Name a + deriving (Foldable, Functor, Show, Traversable) + +named :: Name -> a -> Named a +named = Named + +named' :: Name -> Named Name +named' u = Named u u + +namedName :: Named a -> Name +namedName (Named n _) = n + +namedValue :: Named a -> a +namedValue (Named _ a) = a + +instance Eq a => Eq (Named a) where + (==) = (==) `on` namedValue + +instance Ord a => Ord (Named a) where + compare = compare `on` namedValue diff --git a/semantic-analysis/src/Analysis/ScopeGraph.hs b/semantic-analysis/src/Analysis/ScopeGraph.hs deleted file mode 100644 index 58e93c5b7d..0000000000 --- a/semantic-analysis/src/Analysis/ScopeGraph.hs +++ /dev/null @@ -1,140 +0,0 @@ -{-# LANGUAGE FlexibleContexts, OverloadedStrings, RankNTypes, RecordWildCards, ScopedTypeVariables, TypeApplications, TypeOperators #-} -module Analysis.ScopeGraph -( ScopeGraph(..) -, Ref (..) -, Decl(..) -, scopeGraph -, scopeGraphAnalysis -) where - -import Analysis.Analysis -import Analysis.File -import Analysis.FlowInsensitive -import Control.Algebra -import Control.Applicative (Alternative (..)) -import Control.Carrier.Reader -import Control.Carrier.Fail.WithLoc -import Control.Carrier.Fresh.Strict -import Control.Effect.State -import Control.Monad ((>=>)) -import Data.Foldable (fold) -import Data.Function (fix) -import Data.List.NonEmpty -import qualified Data.Map as Map -import Data.Proxy -import qualified Data.Set as Set -import Data.Traversable (for) -import Prelude hiding (fail) -import Source.Span -import qualified System.Path as Path - -data Decl name = Decl - { declSymbol :: name - , declPath :: Path.AbsRelFile - , declSpan :: Span - } - deriving (Eq, Ord, Show) - -data Ref = Ref - { refPath :: Path.AbsRelFile - , refSpan :: Span - } - deriving (Eq, Ord, Show) - -newtype ScopeGraph name = ScopeGraph { unScopeGraph :: Map.Map (Decl name) (Set.Set Ref) } - deriving (Eq, Ord, Show) - -instance Ord name => Semigroup (ScopeGraph name) where - ScopeGraph a <> ScopeGraph b = ScopeGraph (Map.unionWith (<>) a b) - -instance Ord name => Monoid (ScopeGraph name) where - mempty = ScopeGraph Map.empty - -scopeGraph - :: (Ord name, Ord (term name)) - => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name name (ScopeGraph name) m - -> (term name -> m (ScopeGraph name)) - -> (term name -> m (ScopeGraph name)) - ) - -> [File (term name)] - -> (Heap name (ScopeGraph name), [File (Either (Path.AbsRelFile, Span, String) (ScopeGraph name))]) -scopeGraph eval - = run - . evalFresh 0 - . runHeap - . traverse (runFile eval) - -runFile - :: forall term name m sig - . ( Effect sig - , Has Fresh sig m - , Has (State (Heap name (ScopeGraph name))) sig m - , Ord name - , Ord (term name) - ) - => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name name (ScopeGraph name) m - -> (term name -> m (ScopeGraph name)) - -> (term name -> m (ScopeGraph name)) - ) - -> File (term name) - -> m (File (Either (Path.AbsRelFile, Span, String) (ScopeGraph name))) -runFile eval file = traverse run file - where run = runReader (filePath file) - . runReader (fileSpan file) - . runReader (Map.empty @name @Ref) - . runFail - . fmap fold - . convergeTerm (Proxy @name) 0 (fix (cacheTerm . eval scopeGraphAnalysis)) - -scopeGraphAnalysis - :: ( Alternative m - , Has (Reader Path.AbsRelFile) sig m - , Has (Reader Span) sig m - , Has (Reader (Map.Map name Ref)) sig m - , Has (State (Heap name (ScopeGraph name))) sig m - , Ord name - ) - => Analysis term name name (ScopeGraph name) m -scopeGraphAnalysis = Analysis{..} - where alloc = pure - bind name _ m = do - ref <- askRef - local (Map.insert name ref) m - lookupEnv = pure . Just - deref addr = do - ref <- askRef - bindRef <- asks (Map.lookup addr) - cell <- gets (Map.lookup addr >=> nonEmpty . Set.toList) - let extending = mappend (extendBinding addr ref bindRef) - maybe (pure Nothing) (foldMapA (pure . Just . extending)) cell - assign addr v = do - ref <- askRef - bindRef <- asks (Map.lookup addr) - modify (Map.insertWith (<>) addr (Set.singleton (extendBinding addr ref bindRef <> v))) - abstract eval name body = do - addr <- alloc name - assign name mempty - bind name addr (eval body) - apply _ f a = pure (f <> a) - unit = pure mempty - bool _ = pure mempty - asBool _ = pure True <|> pure False - string _ = pure mempty - asString _ = pure mempty - record fields = do - fields' <- for fields $ \ (k, v) -> do - addr <- alloc k - path <- ask - span <- ask - let v' = ScopeGraph (Map.singleton (Decl k path span) mempty) <> v - (k, v') <$ assign addr v' - pure (foldMap snd fields') - _ ... m = pure (Just m) - - askRef = Ref <$> ask <*> ask - - extendBinding addr ref bindRef = ScopeGraph (maybe Map.empty (\ (Ref path span) -> Map.singleton (Decl addr path span) (Set.singleton ref)) bindRef) diff --git a/semantic-analysis/src/Analysis/Typecheck.hs b/semantic-analysis/src/Analysis/Typecheck.hs index 3f38575b98..01c83bfdb5 100644 --- a/semantic-analysis/src/Analysis/Typecheck.hs +++ b/semantic-analysis/src/Analysis/Typecheck.hs @@ -1,31 +1,48 @@ -{-# LANGUAGE DeriveGeneric, DeriveTraversable, DerivingVia, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Analysis.Typecheck ( Monotype (..) , Meta , Polytype (..) , typecheckingFlowInsensitive -, typecheckingAnalysis ) where -import Analysis.Analysis +import Analysis.Carrier.Env.Monovariant +import qualified Analysis.Carrier.Heap.Monovariant as A +import qualified Analysis.Effect.Domain as A import Analysis.File import Analysis.FlowInsensitive +import qualified Analysis.Intro as Intro +import Analysis.Name import Control.Algebra import Control.Applicative (Alternative (..)) import Control.Carrier.Fail.WithLoc import Control.Carrier.Fresh.Strict as Fresh import Control.Carrier.Reader hiding (Local) import Control.Carrier.State.Strict -import Control.Monad ((>=>), unless) +import Control.Monad (unless) +import Control.Monad.Trans.Class import Data.Foldable (for_) import Data.Function (fix) import Data.Functor (($>)) import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet -import Data.List.NonEmpty (nonEmpty) import qualified Data.Map as Map import Data.Maybe (fromJust, fromMaybe) -import Data.Proxy import Data.Semigroup (Last (..)) import qualified Data.Set as Set import Data.Traversable (for) @@ -39,35 +56,37 @@ import Syntax.Term import Syntax.Var (closed) import qualified System.Path as Path -data Monotype name f a +data Monotype f a = Bool | Unit | String - | Arr (f a) (f a) - | Record (Map.Map name (f a)) + | f a :-> f a + | Record (Map.Map Name (f a)) deriving (Foldable, Functor, Generic1, Traversable) -type Type name = Term (Monotype name) Meta +infixr 0 :-> + +type Type = Term Monotype Meta + +type Addr = Name -- 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 name) a)) instance Semigroup (Term (Monotype name) a) - -deriving instance (Eq name, Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Monotype name f a) -deriving instance (Ord name, Ord a, forall a . Eq a => Eq (f a) - , forall a . Ord a => Ord (f a), Monad f) => Ord (Monotype name f a) -deriving instance (Show name, Show a, forall a . Show a => Show (f a)) => Show (Monotype name f a) +deriving via (Last (Term Monotype a)) instance Semigroup (Term Monotype a) -instance HFunctor (Monotype name) +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) +deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Monotype f a) -instance RightModule (Monotype name) where - item >>=* go = case item of - Bool -> Bool - Unit -> Unit - String -> String - Arr l r -> Arr (l >>= go) (r >>= go) - Record items -> Record (fmap (>>= go) items) +instance HFunctor Monotype +instance RightModule Monotype where + Unit >>=* _ = Unit + Bool >>=* _ = Bool + String >>=* _ = String + (a :-> b) >>=* f = a >>= f :-> b >>= f + Record m >>=* f = Record ((>>= f) <$> m) type Meta = Int @@ -86,21 +105,20 @@ forAll n body = send (PForAll (abstract1 n body)) forAlls :: (Eq a, Has Polytype sig m, Foldable t) => t a -> m a -> m a forAlls ns body = foldr forAll body ns -generalize :: Term (Monotype name) Meta -> Term (Polytype :+: Monotype name) Void +generalize :: Term Monotype Meta -> Term (Polytype :+: Monotype) Void generalize ty = fromJust (closed (forAlls (IntSet.toList (mvs ty)) (hoistTerm R ty))) typecheckingFlowInsensitive - :: (Ord name, Ord (term name), Show name) + :: (Has Intro.Intro syn term, Ord (term Addr)) => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name name (Type name) m - -> (term name -> m (Type name)) - -> (term name -> m (Type name)) + . (Has (A.Domain term Addr Type :+: Env Addr :+: A.Heap Addr Type :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) + => (term Addr -> m Type) + -> (term Addr -> m Type) ) - -> [File (term name)] - -> ( Heap name (Type name) - , [File (Either (Path.AbsRelFile, Span, String) (Term (Polytype :+: Monotype name) Void))] + -> [File (term Addr)] + -> ( Heap Type + , [File (Either (Path.AbsRelFile, Span, String) (Term (Polytype :+: Monotype) Void))] ) typecheckingFlowInsensitive eval = run @@ -110,110 +128,68 @@ typecheckingFlowInsensitive eval . traverse (runFile eval) runFile - :: forall term name m sig - . ( Effect sig + :: ( Effect sig , Has Fresh sig m - , Has (State (Heap name (Type name))) sig m - , Ord name - , Ord (term name) - , Show name + , Has (State (Heap Type)) sig m + , Has Intro.Intro syn term + , Ord (term Addr) ) => (forall sig m - . (Has (Reader Path.AbsRelFile) sig m, Has (Reader Span) sig m, MonadFail m) - => Analysis term name name (Type name) m - -> (term name -> m (Type name)) - -> (term name -> m (Type name)) + . (Has (A.Domain term Addr Type :+: Env Addr :+: A.Heap Addr Type :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) + => (term Addr -> m Type) + -> (term Addr -> m Type) ) - -> File (term name) - -> m (File (Either (Path.AbsRelFile, Span, String) (Type name))) + -> File (term Addr) + -> m (File (Either (Path.AbsRelFile, Span, String) Type)) runFile eval file = traverse run file where run = (\ m -> do (subst, t) <- m - modify @(Heap name (Type name)) (fmap (Set.map (substAll subst))) + modify @(Heap Type) (fmap (Set.map (substAll subst))) pure (substAll subst <$> t)) - . runState (mempty :: (Substitution name)) + . runState @Substitution mempty . runReader (filePath file) . runReader (fileSpan file) + . runEnv . runFail . (\ m -> do (cs, t) <- m - t <$ solve @name cs) - . runState (Set.empty :: Set.Set (Constraint name)) + t <$ solve cs) + . runState @(Set.Set Constraint) mempty . (\ m -> do v <- meta bs <- m v <$ for_ bs (unify v)) - . convergeTerm (Proxy @name) 1 (fix (cacheTerm . eval typecheckingAnalysis)) + . convergeTerm 1 (A.runHeap @Addr @Type . fix (\ eval' -> runDomain eval' . fix (cacheTerm . eval))) -typecheckingAnalysis - :: ( Alternative m - , Has Fresh sig m - , Has (State (Set.Set (Constraint name))) sig m - , Has (State (Heap name (Type name))) sig m - , Ord name - ) - => Analysis term name name (Type name) m -typecheckingAnalysis = Analysis{..} - where alloc = pure - bind _ _ m = m - lookupEnv = pure . Just - 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 - addr <- alloc name - arg <- meta - assign addr arg - ty <- eval body - pure (Alg (Arr arg ty)) - apply _ f a = do - _A <- meta - _B <- meta - unify (Alg (Arr _A _B)) f - unify _A a - pure _B - unit = pure (Alg Unit) - bool _ = pure (Alg Bool) - asBool b = unify (Alg Bool) b >> pure True <|> pure False - string _ = pure (Alg String) - asString s = unify (Alg String) s $> mempty - record fields = do - fields' <- for fields $ \ (k, v) -> do - addr <- alloc k - (k, v) <$ assign addr v - -- FIXME: should records reference types by address instead? - pure (Alg (Record (Map.fromList fields'))) - _ ... m = pure (Just m) - - -data Constraint name = Type name :===: Type name + +data Constraint = Type :===: Type deriving (Eq, Ord, Show) infix 4 :===: -data Solution name - = Int := Type name +data Solution + = Int := Type deriving (Eq, Ord, Show) infix 5 := -meta :: Has Fresh sig m => m (Type name) +meta :: Has Fresh sig m => m Type meta = pure <$> Fresh.fresh -unify :: (Has (State (Set.Set (Constraint name))) sig m, Ord name) => Type name -> Type name -> m () +unify :: Has (State (Set.Set Constraint)) sig m => Type -> Type -> m () unify t1 t2 | t1 == t2 = pure () | otherwise = modify (<> Set.singleton (t1 :===: t2)) -type Substitution name = IntMap.IntMap (Type name) +type Substitution = IntMap.IntMap Type -solve :: (Has (State (Substitution name)) sig m, MonadFail m, Ord name, Show name) => Set.Set (Constraint name) -> m () +solve :: (Has (State Substitution) sig m, MonadFail m) => Set.Set Constraint -> m () solve cs = for_ cs solve where solve = \case -- FIXME: how do we enforce proper subtyping? row polymorphism or something? Alg (Record f1) :===: Alg (Record f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> () - Alg (Arr a1 b1) :===: Alg (Arr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2) + Alg (a1 :-> b1) :===: Alg (a2 :-> b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2) Var m1 :===: Var m2 | m1 == m2 -> pure () Var m1 :===: t2 -> do sol <- solution m1 @@ -222,7 +198,7 @@ solve cs = for_ cs solve Nothing | m1 `IntSet.member` mvs t2 -> fail ("Occurs check failure: " <> show m1 <> " :===: " <> show t2) | otherwise -> modify (IntMap.insert m1 t2 . fmap (substAll (IntMap.singleton m1 t2))) t1 :===: Var m2 -> solve (Var m2 :===: t1) - t1 :===: t2 -> unless (t1 == t2) $ fail ("Type mismatch:\nexpected: " <> show t1 <> "\n actual: " <> show t2) + t1 :===: t2 -> unless (t1 == t2) $ fail ("Type mismatch:\nexpected: " <> show t1 <> "\n actual: " <> show t2) solution m = fmap (m :=) <$> gets (IntMap.lookup m) @@ -232,3 +208,67 @@ mvs = foldMap IntSet.singleton substAll :: Monad t => IntMap.IntMap (t Meta) -> t Meta -> t Meta substAll s a = a >>= \ i -> fromMaybe (pure i) (IntMap.lookup i s) + + +runDomain :: (term Addr -> m Type) -> DomainC term m a -> m a +runDomain eval (DomainC m) = runReader eval m + +newtype DomainC term m a = DomainC (ReaderC (term Addr -> m Type) m a) + deriving (Alternative, Applicative, Functor, Monad, MonadFail) + +instance MonadTrans (DomainC term) where + lift = DomainC . lift + +instance ( Alternative m + , Has (Env Addr) sig m + , Has Fresh sig m + , Has (A.Heap Addr Type) sig m + , Has (State (Set.Set Constraint)) sig m + , Monad term + , MonadFail m + , Has Intro.Intro syn term + ) + => Algebra (A.Domain term Addr Type :+: sig) (DomainC term m) where + alg = \case + L (L (A.Unit k)) -> k (Alg Unit) + L (R (L (A.Bool _ k))) -> k (Alg Bool) + L (R (L (A.AsBool t k))) -> do + unify t (Alg Bool) + k True <|> k False + L (R (R (L (A.String _ k)))) -> k (Alg String) + L (R (R (L (A.AsString t k)))) -> do + unify t (Alg String) + k mempty + L (R (R (R (L (A.Lam (Named n b) k))))) -> do + eval <- DomainC ask + addr <- alloc @Name n + arg <- meta + A.assign addr arg + ty <- lift (eval (instantiate1 (pure n) b)) + k (Alg (arg :-> ty)) + L (R (R (R (L (A.AsLam t k))))) -> do + arg <- meta + ret <- meta + unify t (Alg (arg :-> ret)) + b <- concretize ret + k (Named (Name mempty) (lift b)) where + concretize = \case + Alg Unit -> pure Intro.unit + Alg Bool -> pure (Intro.bool True) <|> pure (Intro.bool False) + Alg String -> pure (Intro.string mempty) + Alg (_ :-> b) -> send . Intro.Lam . Named (Name mempty) . lift <$> concretize b + Alg (Record t) -> Intro.record <$> traverse (traverse concretize) (Map.toList t) + t -> fail $ "can’t concretize " <> show t -- FIXME: concretize type variables by incrementally solving constraints + L (R (R (R (R (A.Record fields k))))) -> do + eval <- DomainC ask + fields' <- for fields $ \ (k, t) -> do + addr <- alloc @Addr k + v <- lift (eval t) + (k, v) <$ A.assign addr v + -- FIXME: should records reference types by address instead? + k (Alg (Record (Map.fromList fields'))) + L (R (R (R (R (A.AsRecord t k))))) -> do + unify t (Alg (Record mempty)) + k mempty -- FIXME: return whatever fields we have, when it’s actually a Record + + R other -> DomainC (send (handleCoercible other)) diff --git a/semantic-core/src/Core/Core.hs b/semantic-core/src/Core/Core.hs index 4d12cecc43..95609be7ce 100644 --- a/semantic-core/src/Core/Core.hs +++ b/semantic-core/src/Core/Core.hs @@ -1,4 +1,16 @@ -{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, LambdaCase, MultiParamTypeClasses, OverloadedStrings, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Core.Core ( Core(..) , rec @@ -57,7 +69,7 @@ import Syntax.Traversable data Core f a -- | Recursive local binding of a name in a scope; strict evaluation of the name in the body will diverge. -- - -- Simultaneous (and therefore potentially mutually-recursive) bidnings can be made by binding a 'Record' recursively within 'Rec' and projecting from it with ':.'. + -- Simultaneous (and therefore potentially mutually-recursive) bindings can be made by binding a 'Record' recursively within 'Rec' and projecting from it with ':.'. = Rec (Named (Scope () f a)) -- | Sequencing without binding; analogous to '>>' or '*>'. | f a :>> f a @@ -125,8 +137,9 @@ a >>> b = send (a :>> b) infixr 1 >>> unseq :: (Alternative m, Project Core sig) => Term sig a -> m (Term sig a, Term sig a) -unseq (Alg sig) | Just (a :>> b) <- prj sig = pure (a, b) -unseq _ = empty +unseq = \case + Alg sig | Just (a :>> b) <- prj sig -> pure (a, b) + _ -> empty unseqs :: Project Core sig => Term sig a -> NonEmpty (Term sig a) unseqs = go @@ -142,8 +155,9 @@ Named u n :<- a >>>= b = send (Named u a :>>= abstract1 n b) infixr 1 >>>= unbind :: (Alternative m, Project Core sig, RightModule sig) => a -> Term sig a -> m (Named a :<- Term sig a, Term sig a) -unbind n (Alg sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b) -unbind _ _ = empty +unbind n = \case + Alg sig | Just (Named u a :>>= b) <- prj sig -> pure (Named u n :<- a, instantiate1 (pure n) b) + _ -> empty unstatement :: (Alternative m, Project Core sig, RightModule sig) => a -> Term sig a -> m (Maybe (Named a) :<- Term sig a, Term sig a) unstatement n t = first (first Just) <$> unbind n t <|> first (Nothing :<-) <$> unseq t @@ -171,8 +185,9 @@ lams :: (Eq a, Foldable t, Has Core sig m) => t (Named a) -> m a -> m a lams names body = foldr lam body names unlam :: (Alternative m, Project Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a) -unlam n (Alg sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b)) -unlam _ _ = empty +unlam n = \case + Alg sig | Just (Lam b) <- prj sig -> pure (n <$ b, instantiate1 (pure n) (namedValue b)) + _ -> empty ($$) :: Has Core sig m => m a -> m a -> m a f $$ a = send (f :$ a) @@ -186,8 +201,9 @@ infixl 8 $$ infixl 8 $$* unapply :: (Alternative m, Project Core sig) => Term sig a -> m (Term sig a, Term sig a) -unapply (Alg sig) | Just (f :$ a) <- prj sig = pure (f, a) -unapply _ = empty +unapply = \case + Alg sig | Just (f :$ a) <- prj sig -> pure (f, a) + _ -> empty unapplies :: Project Core sig => Term sig a -> (Term sig a, Stack (Term sig a)) unapplies core = case unapply core of diff --git a/semantic-core/src/Core/Eval.hs b/semantic-core/src/Core/Eval.hs index ba9c473608..78229077a7 100644 --- a/semantic-core/src/Core/Eval.hs +++ b/semantic-core/src/Core/Eval.hs @@ -1,4 +1,11 @@ -{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards, TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} module Core.Eval ( eval , prog1 @@ -10,95 +17,103 @@ module Core.Eval , ruby ) where -import Analysis.Analysis -import Analysis.File -import Control.Algebra -import Control.Applicative (Alternative (..)) -import Control.Effect.Fail -import Control.Effect.Reader -import Control.Monad ((>=>)) -import Core.Core as Core -import Core.Name -import Data.Functor -import Data.Maybe (fromMaybe, isJust) -import GHC.Stack -import Prelude hiding (fail) -import Source.Span -import Syntax.Scope -import Syntax.Term +import qualified Analysis.Effect.Domain as A +import Analysis.Effect.Env as A +import Analysis.Effect.Heap as A +import Analysis.File +import Control.Algebra +import Control.Applicative (Alternative (..)) +import Control.Effect.Fail +import Control.Effect.Reader +import Control.Monad ((>=>)) +import Core.Core as Core +import Core.Name +import Data.Functor +import Data.Maybe (fromMaybe, isJust) +import GHC.Stack +import Prelude hiding (fail) +import Source.Span +import Syntax.Scope +import qualified Syntax.Term as Term import qualified System.Path as Path -eval :: ( Has (Reader Span) sig m +type Term = Term.Term (Ann Span :+: Core) + +eval :: forall address value m sig + . ( Has (A.Domain Term address value) sig m + , Has (Env address) sig m + , Has (Heap address value) sig m + , Has (Reader Span) sig m , MonadFail m , Semigroup value + , Show address ) - => Analysis (Term (Ann Span :+: Core)) Name address value m - -> (Term (Ann Span :+: Core) Name -> m value) - -> (Term (Ann Span :+: Core) Name -> m value) -eval Analysis{..} eval = \case - Var n -> lookupEnv' n >>= deref' n - Alg (R c) -> case c of - Rec (Named (Ignored n) b) -> do - addr <- alloc n - v <- bind n addr (eval (instantiate1 (pure n) b)) - v <$ assign addr v + => (Term address -> m value) + -> (Term address -> m value) +eval eval = \case + Term.Var n -> deref' n n + Term.Alg (R c) -> case c of + Rec (Named n b) -> do + addr <- A.alloc @address n + v <- A.bind n addr (eval (instantiate1 (pure addr) b)) + v <$ A.assign addr v -- 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 + Named n a :>>= b -> do a' <- eval a - addr <- alloc n - assign addr a' - bind n addr ((a' <>) <$> eval (instantiate1 (pure n) b)) - Lam (Named (Ignored n) b) -> abstract eval n (instantiate1 (pure n) b) + addr <- A.alloc @address n + A.assign addr a' + A.bind n addr ((a' <>) <$> eval (instantiate1 (pure addr) b)) + Lam b -> A.lam b f :$ a -> do - f' <- eval f + Named n b <- eval f >>= A.asLam a' <- eval a - apply eval f' a' - Unit -> unit - Bool b -> bool b + addr <- A.alloc @address n + A.assign addr a' + A.bind n addr (eval (instantiate1 (pure addr) b)) If c t e -> do - c' <- eval c >>= asBool + c' <- eval c >>= A.asBool if c' then eval t else eval e - String s -> string s - Load p -> eval p >>= asString >> unit -- FIXME: add a load command or something - Record fields -> traverse (traverse eval) fields >>= record + Load p -> eval p >>= A.asString >> A.unit -- FIXME: add a load command or something + Unit -> A.unit + Bool b -> A.bool b + String s -> A.string s + Record fields -> A.record fields a :. b -> do - a' <- ref a - a' ... b >>= maybe (freeVariable (show b)) (deref' b) + a' <- eval a >>= A.asRecord + maybe (freeVariable (show b)) eval (lookup b a') a :? b -> do - a' <- ref a - mFound <- a' ... b - bool (isJust mFound) + a' <- eval a >>= A.asRecord @Term @address + A.bool (isJust (lookup b a')) a := b -> do b' <- eval b addr <- ref a - b' <$ assign addr b' - Alg (L (Ann span c)) -> local (const span) (eval c) + b' <$ A.assign addr b' + Term.Alg (L (Ann span c)) -> local (const span) (eval c) where freeVariable s = fail ("free variable: " <> s) uninitialized s = fail ("uninitialized variable: " <> s) invalidRef s = fail ("invalid ref: " <> s) - lookupEnv' n = lookupEnv n >>= maybe (freeVariable (show n)) pure - deref' n = deref >=> maybe (uninitialized (show n)) pure + deref' n = A.deref @address >=> maybe (uninitialized (show n)) pure ref = \case - Var n -> lookupEnv' n - Alg (R c) -> case c of + Term.Var n -> pure n + Term.Alg (R c) -> case c of If c t e -> do - c' <- eval c >>= asBool + c' <- eval c >>= A.asBool if c' then ref t else ref e a :. b -> do - a' <- ref a - a' ... b >>= maybe (freeVariable (show b)) pure + a' <- eval a >>= A.asRecord + maybe (freeVariable (show b)) ref (lookup b a') c -> invalidRef (show c) - Alg (L (Ann span c)) -> local (const span) (ref c) + Term.Alg (L (Ann span c)) -> local (const span) (ref c) prog1 :: Has Core sig t => File (t Name) -prog1 = fromBody $ lam (named' "foo") +prog1 = fromBody $ Core.lam (named' "foo") ( named' "bar" :<- pure "foo" >>>= Core.if' (pure "bar") (Core.bool False) diff --git a/semantic-core/src/Core/Name.hs b/semantic-core/src/Core/Name.hs index 01efa8b650..af10a53b3e 100644 --- a/semantic-core/src/Core/Name.hs +++ b/semantic-core/src/Core/Name.hs @@ -1,51 +1,16 @@ {-# LANGUAGE DeriveGeneric, DeriveTraversable, GeneralizedNewtypeDeriving, LambdaCase, OverloadedLists #-} module Core.Name -( Name (..) -, Named(..) -, named -, named' -, namedName -, namedValue -, Ignored(..) +( module Analysis.Name , reservedNames , isSimpleCharacter , needsQuotation ) where +import Analysis.Name import qualified Data.Char as Char import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet -import Data.String (IsString) -import Data.Text as Text (Text, any, unpack) -import Data.Text.Prettyprint.Doc (Pretty) -import GHC.Generics (Generic) - --- | User-specified and -relevant names. -newtype Name = Name { unName :: Text } - deriving (Eq, Generic, IsString, Ord, Pretty, Show) - --- | Annotates an @a@ with a 'Name'-provided name, which is ignored for '==' and 'compare'. -data Named a = Named (Ignored Name) a - deriving (Eq, Foldable, Functor, Ord, Show, Traversable) - -named :: Name -> a -> Named a -named = Named . Ignored - -named' :: Name -> Named Name -named' u = Named (Ignored u) u - -namedName :: Named a -> Name -namedName (Named (Ignored n) _) = n - -namedValue :: Named a -> a -namedValue (Named _ a) = a - -newtype Ignored a = Ignored a - deriving (Foldable, Functor, Show, Traversable) - -instance Eq (Ignored a) where _ == _ = True -instance Ord (Ignored a) where compare _ _ = EQ - +import Data.Text as Text (any, unpack) reservedNames :: HashSet String reservedNames = [ "#true", "#false", "if", "then", "else" diff --git a/semantic-core/src/Core/Pretty.hs b/semantic-core/src/Core/Pretty.hs index 5babed821e..6b4d4e9144 100644 --- a/semantic-core/src/Core/Pretty.hs +++ b/semantic-core/src/Core/Pretty.hs @@ -43,19 +43,19 @@ primitive = keyword . mappend "#" data Style = Unicode | Ascii name :: Name -> AnsiDoc -name n = if needsQuotation n then enclose (symbol "#{") (symbol "}") (pretty n) else pretty n +name (Name n) = if needsQuotation (Name n) then enclose (symbol "#{") (symbol "}") (pretty n) else pretty n prettyCore :: Style -> Term Core Name -> AnsiDoc prettyCore style = unPrec . go . fmap name where go = \case Var v -> atom v Alg t -> case t of - Rec (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep + Rec (Named x b) -> prec 3 . group . nest 2 $ vsep [ keyword "rec" <+> name x , symbol "=" <+> align (withPrec 0 (go (instantiate1 (pure (name x)) b))) ] - Lam (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep + Lam (Named x b) -> prec 3 . group . nest 2 $ vsep [ lambda <> name x, arrow <+> withPrec 0 (go (instantiate1 (pure (name x)) b)) ] Record fs -> atom . group . nest 2 $ vsep [ primitive "record", block ", " (map (uncurry keyValue) fs) ] @@ -90,7 +90,7 @@ prettyCore style = unPrec . go . fmap name block _ [] = braces mempty block s ss = encloseSep "{ " " }" s ss keyValue x v = name x <+> symbol ":" <+> unPrec (go v) - prettyStatement names (Just (Named (Ignored u) _) :<- t) = name u <+> arrowL <+> unPrec (go (either (names !!) id <$> t)) + prettyStatement names (Just (Named u _) :<- t) = name u <+> arrowL <+> unPrec (go (either (names !!) id <$> t)) prettyStatement names (Nothing :<- t) = unPrec (go (either (names !!) id <$> t)) lambda = case style of Unicode -> symbol "λ" diff --git a/semantic-python/test/Directive.hs b/semantic-python/test/Directive.hs index 83634e2350..6725cdc3f1 100644 --- a/semantic-python/test/Directive.hs +++ b/semantic-python/test/Directive.hs @@ -4,12 +4,10 @@ module Directive ( Directive (..) , readDirectivesFromFile , describe - , toProcess ) where import Analysis.Concrete (Concrete (..)) import Control.Algebra -import Control.Applicative import Control.Monad import Control.Monad.Trans.Resource (ResourceT, runResourceT) import Core.Core (Core) @@ -27,7 +25,6 @@ import qualified Streaming.Prelude as Stream import Syntax.Term (Term) import qualified System.Path as Path import qualified System.Path.PartClass as Path.Class -import System.Process import qualified Text.Parser.Token.Style as Style import Text.Trifecta (CharParsing, TokenParsing (..)) import qualified Text.Trifecta as Trifecta @@ -39,13 +36,11 @@ describe to the test suite how to query the results of a given test case. A directive that looks like this: @ - # CHECK-JQ: has("mach") + # CHECK-RESULT: key: value @ -would, after converting the contents of the file to a Core expression, -dump that expression to JSON and pipe said JSON to @jq -e -'has("mach")@, which will return an error code unless the passed JSON -is a hash containing the @"mach"@ key. +would test that the value for @key@ in the result evaluates to the given +concrete value. This syntax was inspired by LLVM's [FileCheck](https://llvm.org/docs/CommandGuide/FileCheck.html). This @@ -56,9 +51,8 @@ significantly and has been a successful strategy for the LLVM and Rust projects. -} -data Directive = JQ ByteString -- | @# CHECK-JQ: expr@ - | Tree (Term Core Name) -- | @# CHECK-TREE: core@ - | Result Text (Concrete (Term (Core.Ann Source.Span :+: Core)) Name) -- | @# CHECK-RESULT key: expected +data Directive = Tree (Term Core Name) -- | @# CHECK-TREE: core@ + | Result Text (Concrete (Term (Core.Ann Source.Span :+: Core))) -- | @# CHECK-RESULT key: expected | Fails -- | @# CHECK-FAILS@ fails unless translation fails. deriving (Eq, Show) @@ -81,17 +75,11 @@ readDirectivesFromFile describe :: Directive -> String describe Fails = "" describe (Tree t) = Core.Pretty.showCore t -describe (JQ b) = ByteString.unpack b describe (Result t e) = T.unpack t <> ": " <> show e fails :: CharParsing m => m Directive fails = Fails <$ Trifecta.string "# CHECK-FAILS" -jq :: (Monad m, CharParsing m) => m Directive -jq = do - void $ Trifecta.string "# CHECK-JQ: " - JQ . ByteString.pack <$> many (Trifecta.noneOf "\n") - tree :: (Monad m, TokenParsing m) => m Directive tree = do void $ Trifecta.string "# CHECK-TREE: " @@ -104,7 +92,7 @@ result = do void $ Trifecta.symbolic ':' Result key <$> concrete -concrete :: TokenParsing m => m (Concrete term Name) +concrete :: TokenParsing m => m (Concrete term) concrete = Trifecta.choice [ String <$> Trifecta.stringLiteral , Bool True <$ Trifecta.symbol "#true" @@ -113,12 +101,8 @@ concrete = Trifecta.choice ] directive :: (Monad m, TokenParsing m) => m Directive -directive = Trifecta.choice [ fails, result, jq, tree ] +directive = Trifecta.choice [ fails, result, tree ] parseDirective :: ByteString -> Either String Directive parseDirective = Trifecta.foldResult (Left . show) Right . Trifecta.parseByteString (directive <* Trifecta.eof) mempty - -toProcess :: Directive -> CreateProcess -toProcess (JQ d) = proc "jq" ["-e", ByteString.unpack d] -toProcess x = error ("can't call toProcess on " <> show x) diff --git a/semantic-python/test/Instances.hs b/semantic-python/test/Instances.hs index 857f0f7b88..0ba7abf06b 100644 --- a/semantic-python/test/Instances.hs +++ b/semantic-python/test/Instances.hs @@ -8,11 +8,9 @@ module Instances () where -- we should keep track of them in a dedicated file. import Analysis.File -import Analysis.ScopeGraph import Core.Name (Name (..)) import Data.Aeson -import qualified Data.Map as Map -import Data.Text (Text, pack) +import Data.Text (pack) import qualified System.Path as Path deriving newtype instance ToJSON Name @@ -27,21 +25,3 @@ instance ToJSON a => ToJSON (File a) where instance ToJSON Path.AbsRelFile where toJSON p = toJSON (pack (Path.toString p)) - -instance ToJSON Ref where - toJSON (Ref path span) = object - [ "kind" .= ("ref" :: Text) - , "path" .= path - , "span" .= span - ] - -instance ToJSON (Decl Name) where - toJSON Decl{declSymbol, declPath, declSpan} = object - [ "kind" .= ("decl" :: Text) - , "symbol" .= declSymbol - , "path" .= declPath - , "span" .= declSpan - ] - -instance ToJSON (ScopeGraph Name) where - toJSON (ScopeGraph sc) = toJSON . Map.mapKeys declSymbol $ sc diff --git a/semantic-python/test/Test.hs b/semantic-python/test/Test.hs index 2931598d4a..e95ccab1d0 100644 --- a/semantic-python/test/Test.hs +++ b/semantic-python/test/Test.hs @@ -1,27 +1,21 @@ {-# LANGUAGE OverloadedStrings, ScopedTypeVariables, TypeApplications, TypeOperators #-} - +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} module Main (main) where import Analysis.Concrete (Concrete) import qualified Analysis.Concrete as Concrete import Analysis.File -import Analysis.ScopeGraph import Control.Algebra import Control.Carrier.Fail.Either import Control.Carrier.Reader import Control.Monad hiding (fail) -import Control.Monad.Catch import Control.Monad.IO.Class import Core.Core import qualified Core.Eval as Eval import Core.Name import qualified Core.Parser import Core.Pretty -import qualified Data.Aeson as Aeson -import qualified Data.Aeson.Encode.Pretty as Aeson import qualified Data.ByteString.Char8 as ByteString -import qualified Data.ByteString.Lazy.Char8 as ByteString.Lazy -import qualified Data.ByteString.Streaming.Char8 as ByteStream import Data.Foldable import Data.Function import qualified Data.IntMap as IntMap @@ -34,15 +28,13 @@ import qualified Language.Python.Core as Py import Language.Python.Failure import Prelude hiding (fail) import Source.Span -import Streaming -import qualified Streaming.Process import Syntax.Term +import Syntax.Var (closed) import System.Directory import System.Exit import System.Path (()) import qualified System.Path as Path import qualified System.Path.Directory as Path -import Text.Show.Pretty (ppShow) import qualified Text.Trifecta as Trifecta import qualified TreeSitter.Python as TSP import qualified TreeSitter.Unmarshal as TS @@ -61,37 +53,12 @@ parsePrelude = do Right r -> pure r Left s -> HUnit.assertFailure ("Couldn't parse prelude: " <> s) -assertJQExpressionSucceeds :: Show a => Directive.Directive -> a -> Term (Ann Span :+: Core) Name -> HUnit.Assertion -assertJQExpressionSucceeds directive tree core = do - prelude <- parsePrelude - let allTogether = (named' "__semantic_prelude" :<- prelude) >>>= core - - bod <- case scopeGraph Eval.eval [File (Path.absRel "") (Span (Pos 1 1) (Pos 1 1)) allTogether] of - (heap, [File _ _ (Right result)]) -> pure $ Aeson.object - [ "scope" Aeson..= heap - , "heap" Aeson..= result - ] - other -> HUnit.assertFailure ("Couldn't run scope dumping mechanism: " <> showCore (stripAnnotations allTogether) <> "\n" <> show other) - - let ignore = ByteStream.effects . hoist ByteStream.effects - sgJSON = ByteStream.fromLazy $ Aeson.encode bod - jqPipeline = Streaming.Process.withStreamingProcess (Directive.toProcess directive) sgJSON ignore - errorMsg = "jq(1) returned non-zero exit code" - dirMsg = "jq expression: " <> show directive - jsonMsg = "JSON value: " <> ByteString.Lazy.unpack (Aeson.encodePretty bod) - astMsg = "AST (pretty): " <> ppShow tree - treeMsg = "Core expr (pretty): " <> showCore (stripAnnotations core) - treeMsg' = "Core expr (Show): " <> ppShow (stripAnnotations core) - - - catch @_ @Streaming.Process.ProcessExitedUnsuccessfully jqPipeline $ \err -> do - HUnit.assertFailure (unlines [errorMsg, dirMsg, jsonMsg, astMsg, treeMsg, treeMsg', show err]) - -- handles CHECK-RESULT directives -assertEvaluatesTo :: Term (Ann Span :+: Core) Name -> Text -> Concrete (Term (Ann Span :+: Core)) Name -> HUnit.Assertion +assertEvaluatesTo :: Term (Ann Span :+: Core) Name -> Text -> Concrete (Term (Ann Span :+: Core)) -> HUnit.Assertion assertEvaluatesTo core k val = do prelude <- parsePrelude - let allTogether = (named' "__semantic_prelude" :<- prelude) >>>= core + let withPrelude = (named' "__semantic_prelude" :<- prelude) >>>= core + allTogether <- maybe (HUnit.assertFailure ("Can’t evaluate open term: " <> showCore (stripAnnotations withPrelude))) pure (closed withPrelude) let filius = [File (Path.absRel "") (Span (Pos 1 1) (Pos 1 1)) allTogether] (heap, env) <- case Concrete.concrete Eval.eval filius of @@ -104,6 +71,7 @@ assertEvaluatesTo core k val = do let found = Map.lookup (Name k) env >>= flip IntMap.lookup heap found HUnit.@?= Just val +{-# HLINT ignore assertEvaluatesTo #-} -- handles CHECK-TREE directives assertTreeEqual :: Term Core Name -> Term Core Name -> HUnit.Assertion @@ -135,7 +103,6 @@ checkPythonFile fp = HUnit.testCaseSteps (Path.toString fp) $ \step -> withFroze (Right (Left err), _) -> HUnit.assertFailure ("Compilation failed: " <> err) (Right (Right _), Directive.Fails) -> HUnit.assertFailure "Expected translation to fail" (Right (Right item), Directive.Result k v) -> assertEvaluatesTo item k v - (Right (Right item), Directive.JQ _) -> assertJQExpressionSucceeds directive result item (Right (Right item), Directive.Tree t) -> assertTreeEqual (stripAnnotations item) t milestoneFixtures :: IO Tasty.TestTree diff --git a/semantic-python/test/fixtures/1-01-empty-module.py b/semantic-python/test/fixtures/1-01-empty-module.py index 95226452b6..e69de29bb2 100644 --- a/semantic-python/test/fixtures/1-01-empty-module.py +++ b/semantic-python/test/fixtures/1-01-empty-module.py @@ -1 +0,0 @@ -# CHECK-JQ: .scope | has("__semantic_prelude") # prelude should be present diff --git a/semantic-python/test/fixtures/1-02-pass-statement.py b/semantic-python/test/fixtures/1-02-pass-statement.py index d9f8dda1b0..2ae28399f5 100644 --- a/semantic-python/test/fixtures/1-02-pass-statement.py +++ b/semantic-python/test/fixtures/1-02-pass-statement.py @@ -1,2 +1 @@ -# CHECK-JQ: .scope | has("__semantic_prelude") pass diff --git a/semantic-python/test/fixtures/1-04-toplevel-assignment.py b/semantic-python/test/fixtures/1-04-toplevel-assignment.py index a09f7dc347..995157e5fe 100644 --- a/semantic-python/test/fixtures/1-04-toplevel-assignment.py +++ b/semantic-python/test/fixtures/1-04-toplevel-assignment.py @@ -1,4 +1,3 @@ -# CHECK-JQ: .scope | has("hello") and has("goodbye") # CHECK-TREE: { hello <- #unit; goodbye <- #unit; #record { hello: hello, goodbye: goodbye }} # CHECK-RESULT hello: #unit hello = () diff --git a/semantic-python/test/fixtures/2-07-closure-over-scope.py b/semantic-python/test/fixtures/2-07-closure-over-scope.py index 0d38c9d0d7..582b7b89c3 100644 --- a/semantic-python/test/fixtures/2-07-closure-over-scope.py +++ b/semantic-python/test/fixtures/2-07-closure-over-scope.py @@ -1,5 +1,3 @@ -# CHECK-JQ: .scope.zilch[0].b[0].span == { start: [8, 8], end: [ 8, 16 ] } -# CHECK-JQ: .scope.result[0].a[0].span == { start: [5, 8], end: [ 5, 16 ] } def const(a, b): def result():