Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parametric modular interpretation #659

Merged
merged 37 commits into from
Aug 24, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
38ba7d8
Define De Bruijn levels.
robrix Jul 28, 2021
14864b6
Define De Bruijn indices.
robrix Jul 28, 2021
9a13a80
Define conversions between indices and levels.
robrix Jul 28, 2021
053b62f
Define a reference datatype.
robrix Jul 28, 2021
14ceed9
Return a Reference with failures.
robrix Jul 28, 2021
a92be35
Derive some instances for Reference.
robrix Jul 28, 2021
d1c183e
Add some FIXMEs.
robrix Jul 28, 2021
c4e379b
Migrate semantic-analysis towards modular, parametric analysis.
robrix Jul 28, 2021
0826ca4
Typo.
robrix Jul 28, 2021
dd7319d
Pass references around.
robrix Jul 28, 2021
306239f
Define a module for Reference.
robrix Jul 28, 2021
27b2b86
Move Reference into its own module.
robrix Jul 28, 2021
2422a57
Rename the WithLoc module.
robrix Jul 28, 2021
4115251
File holds a Reference.
robrix Jul 28, 2021
d1d349e
Define a module for a Store effect.
robrix Jul 28, 2021
3062b20
Bring over the Store effect.
robrix Jul 28, 2021
79e34ea
Give fixity & precedence for .=.
robrix Jul 28, 2021
6118b05
Switch over to the labelled Store effect &c.
robrix Jul 28, 2021
4a8573e
Fix the API bridge.
robrix Jul 29, 2021
8e0b773
Migrate the dstring constructor to Text.
robrix Aug 5, 2021
bdfd7e1
:fire: the heap effect.
robrix Aug 5, 2021
e9e372d
Generalize dif to return any type.
robrix Aug 5, 2021
f8aadac
Add an expr module.
robrix Aug 19, 2021
3da958d
Define a simple lambda calculus.
robrix Aug 19, 2021
e1dade3
Migrate core over to the new analysis effects &c.
robrix Aug 19, 2021
777357d
Don’t use fused-syntax in semantic-python.
robrix Aug 19, 2021
81c778b
Update for References.
robrix Aug 19, 2021
6be2ff0
:fire: fused-syntax :sparkles:
robrix Aug 19, 2021
39e643d
Prune some deps.
robrix Aug 19, 2021
db9e97d
Ba-bump.
robrix Aug 19, 2021
841c179
Exclude Language.Python.Failure.
robrix Aug 19, 2021
55c349b
HIde an import.
robrix Aug 19, 2021
7696adf
Fix a spec.
robrix Aug 19, 2021
68f823e
Fix the CLI spec.
robrix Aug 19, 2021
3cd8945
This component no longer exists.
robrix Aug 19, 2021
b5b39bd
:memo: Neutral.
robrix Aug 24, 2021
26655c2
Merge branch 'master' into abstract-normalization-by-abstract-evaluation
robrix Aug 24, 2021
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .github/workflows/haskell.yml
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,6 @@ jobs:
cabal v2-run --project-file=cabal.project.ci semantic:test
cabal v2-run --project-file=cabal.project.ci semantic-tags:test
cabal v2-run --project-file=cabal.project.ci semantic-codeql:test
cabal v2-run --project-file=cabal.project.ci semantic-core:test
cabal v2-run --project-file=cabal.project.ci semantic-go:test
cabal v2-run --project-file=cabal.project.ci semantic-java:test
cabal v2-run --project-file=cabal.project.ci semantic-json:test
Expand Down
1 change: 0 additions & 1 deletion WORKSPACE
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,6 @@ stack_snapshot(
"fused-effects",
"fused-effects-exceptions",
"fused-effects-readline",
"fused-syntax",
"gauge",
"generic-lens",
"generic-monoid",
Expand Down
1 change: 0 additions & 1 deletion build/common.bzl
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,6 @@ def semantic_language_library(language, name, srcs, ts_package = "", nodetypes =
"@stackage//:aeson",
"@stackage//:algebraic-graphs",
"@stackage//:fused-effects",
"@stackage//:fused-syntax",
"@stackage//:generic-lens",
"@stackage//:hashable",
"@stackage//:lens",
Expand Down
5 changes: 0 additions & 5 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,3 @@ packages: semantic
semantic-tags
semantic-tsx
semantic-typescript

source-repository-package
type: git
location: https://github.com/antitypical/fused-syntax.git
tag: 4a383d57c8fd7592f54a33f43eb9666314a6e80e
Comment on lines -23 to -27
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🔥

fused-syntax had been used for Core (along with a few other things), but it never worked the way I wanted and I don’t think it’s a good idea to try to continue maintaining it for the sake of this, so 🔥

5 changes: 0 additions & 5 deletions cabal.project.ci
Original file line number Diff line number Diff line change
Expand Up @@ -21,11 +21,6 @@ packages: semantic
semantic-tsx
semantic-typescript

source-repository-package
type: git
location: https://github.com/antitypical/fused-syntax.git
tag: 4a383d57c8fd7592f54a33f43eb9666314a6e80e

-- Treat warnings as errors for CI builds
package semantic
ghc-options: -Werror
Expand Down
8 changes: 0 additions & 8 deletions semantic-analysis/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,8 @@ haskell_library(
"//:transformers",
"//semantic-source",
"@stackage//:aeson",
"@stackage//:algebraic-graphs",
"@stackage//:fused-effects",
"@stackage//:fused-effects-readline",
"@stackage//:fused-syntax",
"@stackage//:hashable",
"@stackage//:haskeline",
"@stackage//:pathtype",
"@stackage//:prettyprinter",
"@stackage//:prettyprinter-ansi-terminal",
"@stackage//:semilattices",
"@stackage//:terminal-size",
],
)
15 changes: 5 additions & 10 deletions semantic-analysis/semantic-analysis.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -45,30 +45,25 @@ library
hs-source-dirs: src
exposed-modules:
Analysis.Blob
Analysis.Carrier.Env.Monovariant
Analysis.Carrier.Env.Precise
Analysis.Carrier.Heap.Monovariant
Analysis.Carrier.Heap.Precise
Analysis.Carrier.Fail.WithLoc
Analysis.Carrier.Store.Monovariant
Analysis.Carrier.Store.Precise
Analysis.Concrete
Analysis.Effect.Domain
Analysis.Effect.Env
Analysis.Effect.Heap
Analysis.Effect.Store
Analysis.File
Analysis.FlowInsensitive
Analysis.Functor.Named
Analysis.ImportGraph
Analysis.Intro
Analysis.Name
Analysis.Project
Analysis.Reference
Analysis.Typecheck
Control.Carrier.Fail.WithLoc
build-depends:
, aeson ^>= 1.4
, algebraic-graphs ^>= 0.3
, base >= 4.13 && < 5
, containers ^>= 0.6
, fused-effects ^>= 1.1
, fused-syntax
, hashable
, pathtype ^>= 0.8.1
, semantic-source ^>= 0.1.0.1
Expand Down
9 changes: 5 additions & 4 deletions semantic-analysis/src/Analysis/Blob.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ module Analysis.Blob
, nullBlob
) where

import Analysis.File
import Analysis.File as A
import Analysis.Reference as A
import Data.Aeson
import Source.Language as Language
import Source.Source as Source
Expand All @@ -34,13 +35,13 @@ instance FromJSON Blob where
-- The resulting Blob's span is taken from the 'totalSpan' of the source.
fromSource :: Path.PartClass.AbsRel ar => Path.File ar -> Language -> Source -> Blob
fromSource filepath language source
= Blob source (Analysis.File.File (Path.toAbsRel filepath) (totalSpan source) language)
= Blob source (A.File (A.Reference (Path.toAbsRel filepath) (totalSpan source)) language)

blobLanguage :: Blob -> Language
blobLanguage = Analysis.File.fileBody . blobFile
blobLanguage = A.fileBody . blobFile

blobPath :: Blob -> Path.AbsRelFile
blobPath = Analysis.File.filePath . blobFile
blobPath = A.refPath . A.fileRef . blobFile

-- | Show FilePath for error or json outputs.
blobFilePath :: Blob -> String
Expand Down
1 change: 0 additions & 1 deletion semantic-analysis/src/Analysis/Carrier/Env/Monovariant.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ newtype EnvC m a = EnvC { runEnv :: m a }
instance Algebra sig m
=> Algebra (Env Name :+: sig) (EnvC m) where
alg hdl sig ctx = case sig of
L (Alloc name) -> pure (name <$ ctx)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should never have been here.

L (Bind _ _ m) -> hdl (m <$ ctx)
L (Lookup name) -> pure (Just name <$ ctx)
R other -> EnvC (alg (runEnv . hdl) other ctx)
23 changes: 8 additions & 15 deletions semantic-analysis/src/Analysis/Carrier/Env/Precise.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,32 +8,25 @@ module Analysis.Carrier.Env.Precise
( -- * Env carrier
EnvC(..)
-- * Env effect
, A.alloc
, A.bind
, A.lookupEnv
, A.Env(..)
, module Analysis.Effect.Env
) where

import qualified Analysis.Effect.Env as A
import Analysis.Effect.Env
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
type PreciseEnv = 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
instance Has (Reader PreciseEnv) sig m
=> Algebra (Env Precise :+: sig) (EnvC m) where
alg hdl sig ctx = case sig of
L (A.Alloc _) -> (<$ ctx) <$> fresh
L (A.Bind name addr m) -> local (Map.insert name addr) (hdl (m <$ ctx))
L (A.Lookup name) -> (<$ ctx) <$> asks (Map.lookup name)
R other -> EnvC (alg (runEnv . hdl) other ctx)
L (Bind name addr m) -> local (Map.insert name addr) (hdl (m <$ ctx))
L (Lookup name) -> (<$ ctx) <$> asks (Map.lookup name)
R other -> EnvC (alg (runEnv . hdl) other ctx)
37 changes: 37 additions & 0 deletions semantic-analysis/src/Analysis/Carrier/Fail/WithLoc.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Analysis.Carrier.Fail.WithLoc
( -- * Fail carrier
runFail
, FailC(..)
-- * Fail effect
, module Control.Effect.Fail
) where

import Analysis.Reference
import Control.Algebra
import Control.Applicative
import Control.Carrier.Error.Either
import Control.Effect.Fail
import Control.Effect.Reader
import Prelude hiding (fail)

-- Fail carrier

runFail :: FailC m a -> m (Either (Reference, String) a)
runFail = runError . runFailC

newtype FailC m a = FailC { runFailC :: ErrorC (Reference, String) m a }
deriving (Alternative, Applicative, Functor, Monad)

instance Has (Reader Reference) sig m => MonadFail (FailC m) where
fail s = do
ref <- ask
FailC (throwError (ref :: Reference, s))

instance Has (Reader Reference) sig m => Algebra (Fail :+: sig) (FailC m) where
alg _ (L (Fail s)) _ = fail s
alg hdl (R other) ctx = FailC (alg (runFailC . hdl) (R other) ctx)
Comment on lines +24 to +37
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This used to live elsewhere in the project. I’ve moved it here, and simplified it slightly by use of the Reference type (introduced in this PR, see below).

37 changes: 0 additions & 37 deletions semantic-analysis/src/Analysis/Carrier/Heap/Monovariant.hs

This file was deleted.

34 changes: 0 additions & 34 deletions semantic-analysis/src/Analysis/Carrier/Heap/Precise.hs

This file was deleted.

85 changes: 85 additions & 0 deletions semantic-analysis/src/Analysis/Carrier/Store/Monovariant.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Analysis.Carrier.Store.Monovariant
( -- * Store carrier
MAddr(..)
, MStore(..)
, runStoreState
, runStore
, StoreC(..)
-- * Store effect
, module Analysis.Effect.Store
-- * Env carrier
, EnvC(..)
-- * Env effect
, module Analysis.Effect.Env
) where

import Analysis.Effect.Env
import Analysis.Effect.Store
import Analysis.Name
import Control.Algebra
import Control.Carrier.State.Church
import Control.Effect.Labelled
import Control.Effect.NonDet
import Control.Monad.Fail as Fail
import Data.Map as Map
import Data.Set as Set

newtype MAddr = MAddr Name
deriving (Eq, Ord, Show)

newtype MStore value = MStore { getMStore :: Map.Map MAddr (Set.Set value) }
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎩 @patrickt for the suggestion of using a hash map here; MAddr is well-suited for hashing in terms of its information content, and its representation can be tuned for that as well without much effort. I haven’t undertaken the effort to do that in this PR, but it’s worth keeping in mind as we begin to lean on this.

deriving (Eq, Ord, Show)

instance Ord value => Semigroup (MStore value) where
MStore s1 <> MStore s2 = MStore (Map.unionWith Set.union s1 s2)

instance Ord value => Monoid (MStore value) where
mempty = MStore Map.empty


-- Store carrier

runStoreState :: Applicative m => StateC (MStore value) m a -> m (MStore value, a)
runStoreState = runState (curry pure) (MStore Map.empty)

runStore :: Labelled Store (StoreC value) m a -> m a
runStore = runStoreC . runLabelled

newtype StoreC value m a = StoreC { runStoreC :: m a }
deriving (Alternative, Applicative, Functor, Monad, Fail.MonadFail)

instance (Has (State (MStore value)) sig m, Alternative m, Ord value) => Algebra (Store MAddr value :+: sig) (StoreC value m) where
alg hdl sig ctx = StoreC $ do
MStore store <- get @(MStore value)
case sig of
L op -> case op of
Alloc name -> let addr = MAddr name in addr <$ ctx <$ put (MStore (Map.insertWith Set.union addr Set.empty store))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I decided against abstracting out a full module for the monovariant store to model insertion with the correct monoidal semantics vs. just doing the insertWith here. We can always revisit that if/when we want to use the store a bunch outside the normal flow of analysis, e.g. to walk the store graph to format or search analytic results.

Assign addr value -> ctx <$ put (MStore (Map.insertWith Set.union addr (Set.singleton value) store))
Fetch addr -> foldMapA ((<$ put (MStore store)) . (<$ ctx)) (Map.findWithDefault Set.empty addr store)

R other -> alg (runStoreC . hdl) other ctx


-- Env carrier
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For convenience, I’ve placed both the Store and Env carriers in a single module. This makes it very slightly less convenient to mix-and-match, but that’s not something we expect to do in the short to medium term anyway.


newtype EnvC value m a = EnvC { runEnv :: m a }
deriving (Applicative, Functor, Monad, Fail.MonadFail)

instance Has (State (MStore value)) sig m
=> Algebra (Env MAddr :+: sig) (EnvC value m) where
alg hdl sig ctx = case sig of
L op -> case op of
Bind _ _ m -> hdl (m <$ ctx)
Lookup n -> do
MStore store <- get @(MStore value)
pure (MAddr n <$ Map.lookup (MAddr n) store <$ ctx)
Comment on lines +81 to +83
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the hallmark of monovariant addressing: there’s no need for a separate environment because the keys of the store are precisely the addresses we’d track anyway. This distinct representation of stores and environments between the monovariant and precise addressing strategies stands in contrast to the old analysis suite in the semantic package, which suffered some pretty gnarly coupling that made it difficult if not impossible to disentangle these responsibilities. Turns out abstraction can win you space and time!


R other -> EnvC (alg (runEnv . hdl) other ctx)
Loading