mirror of
https://github.com/github/semantic.git
synced 2024-12-25 07:55:12 +03:00
Merge remote-tracking branch 'origin/master' into semantic-scope-graph
This commit is contained in:
commit
3345967836
@ -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
|
||||
|
2
.github/workflows/haskell.yml
vendored
2
.github/workflows/haskell.yml
vendored
@ -53,7 +53,7 @@ jobs:
|
||||
|
||||
- name: hlint
|
||||
run: |
|
||||
cabal install hlint --installdir=dist-newstyle
|
||||
test -f dist-newstyle/hlint || cabal install hlint --installdir=dist-newstyle
|
||||
dist-newstyle/hlint src semantic-python
|
||||
|
||||
- name: Build & test
|
||||
|
@ -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.
|
||||
|
@ -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 {
|
||||
@ -45,6 +42,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-tsx/src"
|
||||
echo "-isemantic-typescript/src"
|
||||
|
@ -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 $@
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
}
|
22
semantic-analysis/src/Analysis/Carrier/Env/Monovariant.hs
Normal file
22
semantic-analysis/src/Analysis/Carrier/Env/Monovariant.hs
Normal file
@ -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))
|
33
semantic-analysis/src/Analysis/Carrier/Env/Precise.hs
Normal file
33
semantic-analysis/src/Analysis/Carrier/Env/Precise.hs
Normal file
@ -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))
|
31
semantic-analysis/src/Analysis/Carrier/Heap/Monovariant.hs
Normal file
31
semantic-analysis/src/Analysis/Carrier/Heap/Monovariant.hs
Normal file
@ -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))
|
28
semantic-analysis/src/Analysis/Carrier/Heap/Precise.hs
Normal file
28
semantic-analysis/src/Analysis/Carrier/Heap/Precise.hs
Normal file
@ -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))
|
@ -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)
|
||||
. runReader @Env mempty
|
||||
. A.runEnv
|
||||
. fix (\ eval' -> runDomain eval' . fix eval)
|
||||
|
||||
|
||||
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
|
||||
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)
|
||||
|
||||
runHeap :: StateC (Heap term name) m a -> m (Heap term name, a)
|
||||
runHeap = runState mempty
|
||||
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)
|
||||
|
111
semantic-analysis/src/Analysis/Effect/Domain.hs
Normal file
111
semantic-analysis/src/Analysis/Effect/Domain.hs
Normal file
@ -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
|
44
semantic-analysis/src/Analysis/Effect/Env.hs
Normal file
44
semantic-analysis/src/Analysis/Effect/Env.hs
Normal file
@ -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)
|
29
semantic-analysis/src/Analysis/Effect/Heap.hs
Normal file
29
semantic-analysis/src/Analysis/Effect/Heap.hs
Normal file
@ -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)
|
@ -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.
|
||||
|
@ -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))
|
||||
=> (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))
|
||||
:: ( Monad term
|
||||
, forall a . Eq a => Eq (term a)
|
||||
, forall a . Ord a => Ord (term a)
|
||||
)
|
||||
-> [File (term name)]
|
||||
-> ( Heap name (Value term name)
|
||||
, [File (Either (Path.AbsRelFile, Span, String) (Value term name))]
|
||||
=> (forall sig m
|
||||
. (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 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))
|
||||
|
63
semantic-analysis/src/Analysis/Intro.hs
Normal file
63
semantic-analysis/src/Analysis/Intro.hs
Normal file
@ -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
|
40
semantic-analysis/src/Analysis/Name.hs
Normal file
40
semantic-analysis/src/Analysis/Name.hs
Normal file
@ -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
|
@ -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)
|
@ -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 via (Last (Term Monotype a)) instance Semigroup (Term Monotype 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 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 HFunctor (Monotype name)
|
||||
|
||||
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))
|
||||
|
||||
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)
|
||||
. convergeTerm 1 (A.runHeap @Addr @Type . fix (\ eval' -> runDomain eval' . fix (cacheTerm . eval)))
|
||||
|
||||
|
||||
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))
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
|
@ -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"
|
||||
|
@ -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 "λ"
|
||||
|
@ -19,7 +19,6 @@ module Language.Go.Tags
|
||||
import AST.Element
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.Writer
|
||||
import Data.Monoid (Ap (..))
|
||||
import Data.Text as Text
|
||||
import GHC.Generics
|
||||
import Source.Loc
|
||||
@ -92,13 +91,13 @@ gtags
|
||||
:: ( Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc
|
||||
-> m ()
|
||||
gtags = getAp . Tags.gfoldMap1 @ToTags (Ap . tags) . from1
|
||||
gtags = Tags.traverse1_ @ToTags (const (pure ())) tags . Tags.Generics
|
||||
|
||||
instance (Generic1 t, Tags.GFoldable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
instance (Generic1 t, Tags.GTraversable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
tags' = gtags
|
||||
|
||||
yieldTag :: (Has (Reader Source) sig m, Has (Writer Tags.Tags) sig m) => Text -> Kind -> Loc -> Range -> m ()
|
||||
|
@ -5,7 +5,6 @@ module Language.Java.Tags
|
||||
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.Writer
|
||||
import Data.Monoid (Ap(..))
|
||||
import GHC.Generics
|
||||
import Source.Loc
|
||||
import Source.Range
|
||||
@ -90,11 +89,11 @@ gtags
|
||||
:: ( Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc
|
||||
-> m ()
|
||||
gtags = getAp . Tags.gfoldMap1 @ToTags (Ap . tags) . from1
|
||||
gtags = Tags.traverse1_ @ToTags (const (pure ())) tags . Tags.Generics
|
||||
|
||||
instance (Generic1 t, Tags.GFoldable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
instance (Generic1 t, Tags.GTraversable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
tags' = gtags
|
||||
|
@ -20,7 +20,6 @@ import AST.Element
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.Writer
|
||||
import Data.Maybe (listToMaybe)
|
||||
import Data.Monoid (Ap(..))
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
import Data.Text as Text
|
||||
import GHC.Generics
|
||||
@ -80,7 +79,7 @@ keywordFunctionCall
|
||||
:: ( Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc -> Loc -> Range -> Text -> m ()
|
||||
keywordFunctionCall t loc range name = do
|
||||
@ -162,11 +161,11 @@ gtags
|
||||
:: ( Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc
|
||||
-> m ()
|
||||
gtags = getAp . Tags.gfoldMap1 @ToTags (Ap . tags) . from1
|
||||
gtags = Tags.traverse1_ @ToTags (const (pure ())) tags . Tags.Generics
|
||||
|
||||
instance (Generic1 t, Tags.GFoldable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
instance (Generic1 t, Tags.GTraversable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
tags' = gtags
|
||||
|
@ -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 = "<expect failure>"
|
||||
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)
|
||||
|
@ -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
|
||||
|
@ -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 "<interactive>") (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 "<interactive>") (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
|
||||
|
@ -1 +0,0 @@
|
||||
# CHECK-JQ: .scope | has("__semantic_prelude") # prelude should be present
|
@ -1,2 +1 @@
|
||||
# CHECK-JQ: .scope | has("__semantic_prelude")
|
||||
pass
|
||||
|
@ -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 = ()
|
||||
|
@ -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():
|
||||
|
@ -22,7 +22,6 @@ import Control.Effect.Reader
|
||||
import Control.Effect.State
|
||||
import Control.Effect.Writer
|
||||
import Control.Monad
|
||||
import Data.Monoid (Ap (..))
|
||||
import Data.Foldable
|
||||
import Data.Text as Text
|
||||
import GHC.Generics
|
||||
@ -153,7 +152,7 @@ yieldMethodNameTag
|
||||
, Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
) => t Loc -> Loc -> Range -> Rb.MethodName Loc -> m ()
|
||||
yieldMethodNameTag t loc range (Rb.MethodName expr) = enterScope True $ case expr of
|
||||
Prj Rb.Identifier { text = name } -> yield name
|
||||
@ -307,11 +306,11 @@ gtags
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Has (State [Text]) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc
|
||||
-> m ()
|
||||
gtags = getAp . Tags.gfoldMap1 @ToTags (Ap . tags) . from1
|
||||
gtags = Tags.traverse1_ @ToTags (const (pure ())) tags . Tags.Generics
|
||||
|
||||
instance (Generic1 t, Tags.GFoldable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
instance (Generic1 t, Tags.GTraversable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
tags' = gtags
|
||||
|
@ -1,23 +1,44 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TypeApplications, TypeOperators #-}
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE DefaultSignatures #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Tags.Tagging.Precise
|
||||
( Tags
|
||||
, ToTags(..)
|
||||
, yield
|
||||
, runTagging
|
||||
, firstLine
|
||||
, GFoldable1(..)
|
||||
, Traversable1(..)
|
||||
, for1
|
||||
, traverse1_
|
||||
, for1_
|
||||
, foldMap1
|
||||
, foldMapDefault1
|
||||
, fmapDefault1
|
||||
, traverseDefault1
|
||||
, GTraversable1(..)
|
||||
, Generics(..)
|
||||
) where
|
||||
|
||||
import Control.Carrier.Reader
|
||||
import Control.Carrier.Writer.Strict
|
||||
import Data.Functor (void)
|
||||
import Data.Functor.Const
|
||||
import Data.Functor.Identity
|
||||
import Data.Monoid (Endo(..))
|
||||
import Data.Monoid (Ap (..), Endo (..))
|
||||
import Data.Text as Text (Text, takeWhile)
|
||||
import GHC.Generics
|
||||
import Prelude hiding (span)
|
||||
import Source.Loc (Loc(..))
|
||||
import Source.Span
|
||||
import Source.Loc (Loc (..))
|
||||
import Source.Source as Source
|
||||
import Source.Span
|
||||
import Tags.Tag
|
||||
|
||||
type Tags = Endo [Tag]
|
||||
@ -43,36 +64,135 @@ firstLine :: Source -> Text
|
||||
firstLine = Text.takeWhile (/= '\n') . toText . Source.take 180
|
||||
|
||||
|
||||
-- FIXME: move GFoldable1 into semantic-ast.
|
||||
class GFoldable1 c t where
|
||||
-- | Generically map functions over fields of kind @* -> *@, monoidally combining the results.
|
||||
gfoldMap1
|
||||
:: Monoid b
|
||||
=> (forall f . c f => f a -> b)
|
||||
-- FIXME: move Traversable1 into semantic-ast.
|
||||
-- FIXME: derive Traversable1 instances for TH-generated syntax types.
|
||||
|
||||
-- | Simultaneous traversal of subterms of kind @*@ and @* -> *@ in an 'Applicative' context.
|
||||
--
|
||||
-- 'Traversable1' can express any combination of first- and second-order mapping, folding, and traversal.
|
||||
--
|
||||
-- Note that the @1@ suffix is used in the manner of 'Data.Functor.Classes.Show1' or 'Generic1', rather than 'foldr1'; it’s a higher-order traversal which is simultaneously able to traverse (and alter) annotations.
|
||||
class Traversable1 c t where
|
||||
-- | Map annotations of kind @*@ and heterogeneously-typed subterms of kind @* -> *@ under some constraint @c@ into an 'Applicative' context. The constraint is necessary to operate on otherwise universally-quantified subterms, since otherwise there would be insufficient information to inspect them at all.
|
||||
--
|
||||
-- No proxy is provided for the constraint @c@; instead, @-XTypeApplications@ should be used. E.g. here we ignore the annotations and print all the @* -> *@ subterms using 'Show1':
|
||||
--
|
||||
-- @
|
||||
-- 'traverse1' \@'Data.Functor.Classes.Show1' 'pure' (\ t -> t '<$' 'putStrLn' ('Data.Functor.Classes.showsPrec1' 0 t ""))
|
||||
-- @
|
||||
--
|
||||
-- Note that this traversal is non-recursive: any recursion through subterms must be performed by the second function argument.
|
||||
traverse1
|
||||
:: Applicative f
|
||||
=> (a -> f b)
|
||||
-> (forall t' . c t' => t' a -> f (t' b))
|
||||
-> t a
|
||||
-> b
|
||||
-> f (t b)
|
||||
default traverse1
|
||||
:: (Applicative f, Generic1 t, GTraversable1 c (Rep1 t))
|
||||
=> (a -> f b)
|
||||
-> (forall t' . c t' => t' a -> f (t' b))
|
||||
-> t a
|
||||
-> f (t b)
|
||||
traverse1 f g = fmap to1 . gtraverse1 @c f g . from1
|
||||
|
||||
instance GFoldable1 c f => GFoldable1 c (M1 i c' f) where
|
||||
gfoldMap1 alg = gfoldMap1 @c alg . unM1
|
||||
for1
|
||||
:: forall c t f a b
|
||||
. (Traversable1 c t, Applicative f)
|
||||
=> t a
|
||||
-> (a -> f b)
|
||||
-> (forall t' . c t' => t' a -> f (t' b))
|
||||
-> f (t b)
|
||||
for1 t f g = traverse1 @c f g t
|
||||
|
||||
instance (GFoldable1 c f, GFoldable1 c g) => GFoldable1 c (f :*: g) where
|
||||
gfoldMap1 alg (f :*: g) = gfoldMap1 @c alg f <> gfoldMap1 @c alg g
|
||||
traverse1_
|
||||
:: forall c t f a a' a''
|
||||
. (Traversable1 c t, Applicative f)
|
||||
=> (a -> f a')
|
||||
-> (forall t' . c t' => t' a -> f a'')
|
||||
-> t a
|
||||
-> f ()
|
||||
traverse1_ f g = getAp . foldMap1 @c (Ap . void . f) (Ap . void . g)
|
||||
|
||||
instance (GFoldable1 c f, GFoldable1 c g) => GFoldable1 c (f :+: g) where
|
||||
gfoldMap1 alg (L1 l) = gfoldMap1 @c alg l
|
||||
gfoldMap1 alg (R1 r) = gfoldMap1 @c alg r
|
||||
for1_
|
||||
:: forall c t f a a' a''
|
||||
. (Traversable1 c t, Applicative f)
|
||||
=> t a
|
||||
-> (a -> f a')
|
||||
-> (forall t' . c t' => t' a -> f a'')
|
||||
-> f ()
|
||||
for1_ t f g = getAp $ foldMap1 @c (Ap . void . f) (Ap . void . g) t
|
||||
|
||||
instance GFoldable1 c (K1 R t) where
|
||||
gfoldMap1 _ _ = mempty
|
||||
foldMap1 :: forall c t b a . (Traversable1 c t, Monoid b) => (a -> b) -> (forall t' . c t' => t' a -> b) -> t a -> b
|
||||
foldMap1 f g = getConst . traverse1 @c (Const . f) (Const . g)
|
||||
|
||||
instance GFoldable1 c Par1 where
|
||||
gfoldMap1 _ _ = mempty
|
||||
|
||||
instance c t => GFoldable1 c (Rec1 t) where
|
||||
gfoldMap1 alg (Rec1 t) = alg t
|
||||
-- | This function may be used as a value for 'foldMap' in a 'Foldable' instance.
|
||||
foldMapDefault1 :: (Traversable1 Foldable t, Monoid b) => (a -> b) -> t a -> b
|
||||
foldMapDefault1 f = foldMap1 @Foldable f (foldMap f)
|
||||
|
||||
instance (Foldable f, GFoldable1 c g) => GFoldable1 c (f :.: g) where
|
||||
gfoldMap1 alg = foldMap (gfoldMap1 @c alg) . unComp1
|
||||
-- | This function may be used as a value for 'fmap' in a 'Functor' instance.
|
||||
fmapDefault1 :: Traversable1 Functor t => (a -> b) -> t a -> t b
|
||||
fmapDefault1 f = runIdentity . traverse1 @Functor (Identity . f) (Identity . fmap f)
|
||||
|
||||
instance GFoldable1 c U1 where
|
||||
gfoldMap1 _ _ = mempty
|
||||
-- | This function may be used as a value for 'traverse' in a 'Traversable' instance.
|
||||
traverseDefault1 :: (Traversable1 Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
|
||||
traverseDefault1 f = traverse1 @Traversable f (traverse f)
|
||||
|
||||
|
||||
-- FIXME: move GTraversable1 into semantic-ast.
|
||||
class GTraversable1 c t where
|
||||
-- | Generically map annotations and subterms of kind @* -> *@ into an 'Applicative' context.
|
||||
gtraverse1
|
||||
:: Applicative f
|
||||
=> (a -> f b)
|
||||
-> (forall t' . c t' => t' a -> f (t' b))
|
||||
-> t a
|
||||
-> f (t b)
|
||||
|
||||
instance GTraversable1 c f => GTraversable1 c (M1 i c' f) where
|
||||
gtraverse1 f g = fmap M1 . gtraverse1 @c f g . unM1
|
||||
|
||||
instance (GTraversable1 c f, GTraversable1 c g) => GTraversable1 c (f :*: g) where
|
||||
gtraverse1 f g (l :*: r) = (:*:) <$> gtraverse1 @c f g l <*> gtraverse1 @c f g r
|
||||
|
||||
instance (GTraversable1 c f, GTraversable1 c g) => GTraversable1 c (f :+: g) where
|
||||
gtraverse1 f g (L1 l) = L1 <$> gtraverse1 @c f g l
|
||||
gtraverse1 f g (R1 r) = R1 <$> gtraverse1 @c f g r
|
||||
|
||||
instance GTraversable1 c (K1 R t) where
|
||||
gtraverse1 _ _ (K1 k) = pure (K1 k)
|
||||
|
||||
instance GTraversable1 c Par1 where
|
||||
gtraverse1 f _ (Par1 a) = Par1 <$> f a
|
||||
|
||||
instance c t => GTraversable1 c (Rec1 t) where
|
||||
gtraverse1 _ g (Rec1 t) = Rec1 <$> g t
|
||||
|
||||
instance (Traversable f, GTraversable1 c g) => GTraversable1 c (f :.: g) where
|
||||
gtraverse1 f g = fmap Comp1 . traverse (gtraverse1 @c f g) . unComp1
|
||||
|
||||
instance GTraversable1 c U1 where
|
||||
gtraverse1 _ _ _ = pure U1
|
||||
|
||||
|
||||
-- | @'Generics' t@ has a 'Traversable1' instance when @'Rep1' t@ has a 'GTraversable1' instance, making this convenient for applying 'traverse1' to 'Generic1' types lacking 'Traversable1' instances:
|
||||
--
|
||||
-- @
|
||||
-- 'getGenerics' '<$>' 'traverse1' f g ('Generics' t) = 'to1' '<$>' 'gtraverse1' f g ('from1' t)
|
||||
-- @
|
||||
--
|
||||
-- It further defines its 'Foldable', 'Functor', and 'Traversable' instances using 'Traversable1', making it suitable for deriving with @-XDerivingVia@.
|
||||
newtype Generics t a = Generics { getGenerics :: t a }
|
||||
|
||||
instance (Generic1 t, GTraversable1 Foldable (Rep1 t)) => Foldable (Generics t) where
|
||||
foldMap = foldMapDefault1
|
||||
|
||||
instance (Generic1 t, GTraversable1 Functor (Rep1 t)) => Functor (Generics t) where
|
||||
fmap = fmapDefault1
|
||||
|
||||
instance (Generic1 t, GTraversable1 Foldable (Rep1 t), GTraversable1 Functor (Rep1 t), GTraversable1 Traversable (Rep1 t)) => Traversable (Generics t) where
|
||||
traverse = traverseDefault1
|
||||
|
||||
instance (Generic1 t, GTraversable1 c (Rep1 t)) => Traversable1 c (Generics t) where
|
||||
traverse1 f g = fmap (Generics . to1) . gtraverse1 @c f g . from1 . getGenerics
|
||||
|
@ -21,7 +21,6 @@ import AST.Element
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.Writer
|
||||
import Data.Foldable
|
||||
import Data.Monoid (Ap (..))
|
||||
import Data.Text as Text
|
||||
import GHC.Generics
|
||||
import Source.Loc
|
||||
@ -133,13 +132,13 @@ gtags
|
||||
:: ( Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc
|
||||
-> m ()
|
||||
gtags = getAp . Tags.gfoldMap1 @ToTags (Ap . tags) . from1
|
||||
gtags = Tags.traverse1_ @ToTags (const (pure ())) tags . Tags.Generics
|
||||
|
||||
instance (Generic1 t, Tags.GFoldable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
instance (Generic1 t, Tags.GTraversable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
tags' = gtags
|
||||
|
||||
yieldTag :: (Has (Reader Source) sig m, Has (Writer Tags.Tags) sig m) => Text -> Kind -> Loc -> Range -> m ()
|
||||
|
@ -21,7 +21,6 @@ import AST.Element
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.Writer
|
||||
import Data.Foldable
|
||||
import Data.Monoid (Ap (..))
|
||||
import Data.Text as Text
|
||||
import GHC.Generics
|
||||
import Source.Loc
|
||||
@ -125,13 +124,13 @@ gtags
|
||||
:: ( Has (Reader Source) sig m
|
||||
, Has (Writer Tags.Tags) sig m
|
||||
, Generic1 t
|
||||
, Tags.GFoldable1 ToTags (Rep1 t)
|
||||
, Tags.GTraversable1 ToTags (Rep1 t)
|
||||
)
|
||||
=> t Loc
|
||||
-> m ()
|
||||
gtags = getAp . Tags.gfoldMap1 @ToTags (Ap . tags) . from1
|
||||
gtags = Tags.traverse1_ @ToTags (const (pure ())) tags . Tags.Generics
|
||||
|
||||
instance (Generic1 t, Tags.GFoldable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
instance (Generic1 t, Tags.GTraversable1 ToTags (Rep1 t)) => ToTagsBy 'Generic t where
|
||||
tags' = gtags
|
||||
|
||||
yieldTag :: (Has (Reader Source) sig m, Has (Writer Tags.Tags) sig m) => Text -> Kind -> Loc -> Range -> m ()
|
||||
|
Loading…
Reference in New Issue
Block a user