mirror of
https://github.com/github/semantic.git
synced 2024-11-28 10:15:55 +03:00
Merge branch 'compile-python-calls' into compile-python-function-decorators
This commit is contained in:
commit
089b45ff49
@ -36,7 +36,7 @@ install:
|
||||
script:
|
||||
- cabal new-build
|
||||
- cabal new-run semantic:test
|
||||
- cabal new-run semantic-core:spec
|
||||
- cabal new-run semantic-core:test
|
||||
- cabal new-run semantic-core:doctest
|
||||
- cabal new-run semantic-python:test
|
||||
- cabal new-run semantic-source:test
|
||||
|
@ -33,3 +33,8 @@ source-repository-package
|
||||
type: git
|
||||
location: https://github.com/tclem/proto-lens-jsonpb
|
||||
tag: e4d10b77f57ee25beb759a33e63e2061420d3dc2
|
||||
|
||||
source-repository-package
|
||||
type: git
|
||||
location: https://github.com/antitypical/fused-syntax.git
|
||||
tag: 5b7512db962d5b3f973002615b8bc86ab074d5aa
|
||||
|
@ -7,12 +7,12 @@ Semantic core intermediate language (experimental)
|
||||
|
||||
This project consists of a Haskell package named `semantic-core`. The library’s sources are in [`src`][].
|
||||
|
||||
Development of `semantic-core` is typically done using `cabal new-build`:
|
||||
Development of `semantic-core` is typically done using `cabal v2-build`:
|
||||
|
||||
```shell
|
||||
cabal new-build # build the library
|
||||
cabal new-repl # load the package into ghci
|
||||
cabal new-test # build and run the doctests
|
||||
cabal v2-build # build the library
|
||||
cabal v2-repl # load the package into ghci
|
||||
cabal v2-test # build and run the doctests
|
||||
```
|
||||
|
||||
[`src`]: https://github.com/github/semantic/tree/master/semantic-core/src
|
||||
|
@ -16,45 +16,11 @@ build-type: Simple
|
||||
stability: alpha
|
||||
extra-source-files: README.md
|
||||
|
||||
tested-with: GHC == 8.6.4
|
||||
tested-with:
|
||||
GHC == 8.6.5
|
||||
|
||||
library
|
||||
exposed-modules: Analysis.Concrete
|
||||
, Analysis.Eval
|
||||
, Analysis.FlowInsensitive
|
||||
, Analysis.ImportGraph
|
||||
, Analysis.ScopeGraph
|
||||
, Analysis.Typecheck
|
||||
, Control.Carrier.Fail.WithLoc
|
||||
, Control.Effect.Readline
|
||||
, Control.Monad.Module
|
||||
, Data.Core
|
||||
, Data.Core.Parser
|
||||
, Data.Core.Pretty
|
||||
, Data.File
|
||||
, Data.Loc
|
||||
, Data.Name
|
||||
, Data.Scope
|
||||
, Data.Stack
|
||||
, Data.Term
|
||||
build-depends: algebraic-graphs ^>= 0.3
|
||||
, base >= 4.12 && < 5
|
||||
, containers ^>= 0.6
|
||||
, directory ^>= 1.3
|
||||
, filepath ^>= 1.4
|
||||
, fused-effects ^>= 0.5
|
||||
, haskeline ^>= 0.7.5
|
||||
, parsers ^>= 0.12.10
|
||||
, prettyprinter ^>= 1.2.1
|
||||
, prettyprinter-ansi-terminal ^>= 1.1.1
|
||||
, semantic-source ^>= 0
|
||||
, semigroupoids ^>= 5.3
|
||||
, text ^>= 1.2.3.1
|
||||
, transformers ^>= 0.5.6
|
||||
, trifecta ^>= 2
|
||||
, unordered-containers ^>= 0.2.10
|
||||
hs-source-dirs: src
|
||||
default-language: Haskell2010
|
||||
common common
|
||||
default-language: Haskell2010
|
||||
ghc-options:
|
||||
-Weverything
|
||||
-Wno-missing-local-signatures
|
||||
@ -67,29 +33,74 @@ library
|
||||
-Wno-missed-specialisations
|
||||
-Wno-all-missed-specialisations
|
||||
-Wno-star-is-type
|
||||
if (impl(ghc >= 8.8))
|
||||
ghc-options: -Wno-missing-deriving-strategies
|
||||
|
||||
library
|
||||
import: common
|
||||
hs-source-dirs: src
|
||||
exposed-modules:
|
||||
Analysis.Analysis
|
||||
Analysis.Concrete
|
||||
Analysis.Eval
|
||||
Analysis.FlowInsensitive
|
||||
Analysis.ImportGraph
|
||||
Analysis.ScopeGraph
|
||||
Analysis.Typecheck
|
||||
Control.Carrier.Fail.WithLoc
|
||||
Control.Carrier.Readline.Haskeline
|
||||
Control.Effect.Readline
|
||||
Core.Core
|
||||
Core.Core.Parser
|
||||
Core.Core.Pretty
|
||||
Core.File
|
||||
Core.Loc
|
||||
Core.Name
|
||||
build-depends:
|
||||
algebraic-graphs ^>= 0.3
|
||||
, base >= 4.12 && < 5
|
||||
, containers ^>= 0.6
|
||||
, directory ^>= 1.3
|
||||
, filepath ^>= 1.4
|
||||
, fused-effects ^>= 0.5
|
||||
, fused-syntax
|
||||
, haskeline ^>= 0.7.5
|
||||
, parsers ^>= 0.12.10
|
||||
, prettyprinter ^>= 1.2.1
|
||||
, prettyprinter-ansi-terminal ^>= 1.1.1
|
||||
, semantic-source ^>= 0
|
||||
, semigroupoids ^>= 5.3
|
||||
, terminal-size ^>= 0.3
|
||||
, text ^>= 1.2.3.1
|
||||
, transformers ^>= 0.5.6
|
||||
, trifecta ^>= 2
|
||||
, unordered-containers ^>= 0.2.10
|
||||
|
||||
test-suite doctest
|
||||
type: exitcode-stdio-1.0
|
||||
main-is: Doctest.hs
|
||||
build-depends: base >=4.9 && <4.13
|
||||
, doctest >=0.7 && <1.0
|
||||
, QuickCheck
|
||||
, semantic-core
|
||||
hs-source-dirs: test
|
||||
default-language: Haskell2010
|
||||
import: common
|
||||
type: exitcode-stdio-1.0
|
||||
hs-source-dirs: test
|
||||
main-is: Doctest.hs
|
||||
build-depends:
|
||||
base >=4.9 && <4.13
|
||||
, doctest >=0.7 && <1.0
|
||||
, QuickCheck
|
||||
, semantic-core
|
||||
|
||||
test-suite spec
|
||||
type: exitcode-stdio-1.0
|
||||
main-is: Spec.hs
|
||||
other-modules: Generators
|
||||
build-depends: base
|
||||
, semantic-core
|
||||
, semantic-source ^>= 0
|
||||
, fused-effects
|
||||
, hedgehog ^>= 1
|
||||
, tasty >= 1.2 && <2
|
||||
, tasty-hedgehog ^>= 1.0.0.1
|
||||
, tasty-hunit >= 0.10 && <1
|
||||
, trifecta
|
||||
hs-source-dirs: test
|
||||
default-language: Haskell2010
|
||||
test-suite test
|
||||
import: common
|
||||
type: exitcode-stdio-1.0
|
||||
hs-source-dirs: test
|
||||
main-is: Test.hs
|
||||
other-modules: Generators
|
||||
build-depends:
|
||||
base
|
||||
, semantic-core
|
||||
, semantic-source ^>= 0
|
||||
, fused-effects
|
||||
, fused-syntax
|
||||
, hedgehog ^>= 1
|
||||
, tasty >= 1.2 && <2
|
||||
, tasty-hedgehog ^>= 1.0.0.1
|
||||
, tasty-hunit >= 0.10 && <1
|
||||
, trifecta
|
||||
|
27
semantic-core/src/Analysis/Analysis.hs
Normal file
27
semantic-core/src/Analysis/Analysis.hs
Normal file
@ -0,0 +1,27 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
module Analysis.Analysis
|
||||
( Analysis(..)
|
||||
) where
|
||||
|
||||
import Core.Name
|
||||
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 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 -> m value) -> Name -> term -> m value
|
||||
, apply :: (term -> 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)
|
||||
}
|
@ -11,7 +11,7 @@ module Analysis.Concrete
|
||||
|
||||
import qualified Algebra.Graph as G
|
||||
import qualified Algebra.Graph.Export.Dot as G
|
||||
import Analysis.Eval
|
||||
import Analysis.Analysis
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Carrier.Fail.WithLoc
|
||||
import Control.Effect
|
||||
@ -20,13 +20,13 @@ import Control.Effect.NonDet
|
||||
import Control.Effect.Reader hiding (Local)
|
||||
import Control.Effect.State
|
||||
import Control.Monad ((<=<), guard)
|
||||
import Data.File
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name
|
||||
import Data.Function (fix)
|
||||
import qualified Data.IntMap as IntMap
|
||||
import qualified Data.IntSet as IntSet
|
||||
import Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Name
|
||||
import Data.Semigroup (Last (..))
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text, pack)
|
||||
@ -221,5 +221,7 @@ data EdgeType term
|
||||
|
||||
|
||||
-- $setup
|
||||
-- >>> :seti -XFlexibleContexts
|
||||
-- >>> :seti -XOverloadedStrings
|
||||
-- >>> import qualified Data.Core as Core
|
||||
-- >>> import Analysis.Eval (eval)
|
||||
-- >>> import qualified Core.Core as Core
|
||||
|
@ -8,26 +8,25 @@ module Analysis.Eval
|
||||
, prog5
|
||||
, prog6
|
||||
, ruby
|
||||
, Analysis(..)
|
||||
) where
|
||||
|
||||
import Analysis.Analysis
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Effect.Carrier
|
||||
import Control.Effect.Fail
|
||||
import Control.Effect.Reader
|
||||
import Control.Monad ((>=>))
|
||||
import Data.Core as Core
|
||||
import Data.File
|
||||
import Core.Core as Core
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name
|
||||
import Data.Functor
|
||||
import Data.Loc
|
||||
import Data.Maybe (fromJust, fromMaybe)
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Term
|
||||
import Data.Text (Text)
|
||||
import GHC.Stack
|
||||
import Prelude hiding (fail)
|
||||
import Source.Span
|
||||
import Syntax.Scope
|
||||
import Syntax.Term
|
||||
|
||||
eval :: ( Carrier sig m
|
||||
, Member (Reader Span) sig
|
||||
@ -39,7 +38,7 @@ eval :: ( Carrier sig m
|
||||
-> (Term (Ann Span :+: Core) Name -> m value)
|
||||
eval Analysis{..} eval = \case
|
||||
Var n -> lookupEnv' n >>= deref' n
|
||||
Term (R c) -> case c of
|
||||
Alg (R c) -> case c of
|
||||
Rec (Named (Ignored n) b) -> do
|
||||
addr <- alloc n
|
||||
v <- bind n addr (eval (instantiate1 (pure n) b))
|
||||
@ -73,7 +72,7 @@ eval Analysis{..} eval = \case
|
||||
b' <- eval b
|
||||
addr <- ref a
|
||||
b' <$ assign addr b'
|
||||
Term (L (Ann span c)) -> local (const span) (eval c)
|
||||
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)
|
||||
@ -83,7 +82,7 @@ eval Analysis{..} eval = \case
|
||||
|
||||
ref = \case
|
||||
Var n -> lookupEnv' n
|
||||
Term (R c) -> case c of
|
||||
Alg (R c) -> case c of
|
||||
If c t e -> do
|
||||
c' <- eval c >>= asBool
|
||||
if c' then ref t else ref e
|
||||
@ -91,7 +90,7 @@ eval Analysis{..} eval = \case
|
||||
a' <- ref a
|
||||
a' ... b >>= maybe (freeVariable (show b)) pure
|
||||
c -> invalidRef (show c)
|
||||
Term (L (Ann span c)) -> local (const span) (ref c)
|
||||
Alg (L (Ann span c)) -> local (const span) (ref c)
|
||||
|
||||
|
||||
prog1 :: (Carrier sig t, Member Core sig) => File (t Name)
|
||||
@ -213,21 +212,3 @@ ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' stateme
|
||||
__semantic_global = "__semantic_global"
|
||||
__semantic_super = "__semantic_super"
|
||||
__semantic_truthy = "__semantic_truthy"
|
||||
|
||||
|
||||
data Analysis term 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 -> m value) -> Name -> term -> m value
|
||||
, apply :: (term -> 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)
|
||||
}
|
||||
|
@ -5,7 +5,7 @@ module Analysis.ImportGraph
|
||||
, importGraphAnalysis
|
||||
) where
|
||||
|
||||
import Analysis.Eval
|
||||
import Analysis.Analysis
|
||||
import Analysis.FlowInsensitive
|
||||
import Control.Applicative (Alternative(..))
|
||||
import Control.Carrier.Fail.WithLoc
|
||||
@ -14,13 +14,13 @@ import Control.Effect.Fresh
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.State
|
||||
import Control.Monad ((>=>))
|
||||
import Data.File
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name
|
||||
import Data.Foldable (fold, for_)
|
||||
import Data.Function (fix)
|
||||
import Data.List.NonEmpty (nonEmpty)
|
||||
import Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Name
|
||||
import Data.Proxy
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text)
|
||||
|
@ -7,7 +7,7 @@ module Analysis.ScopeGraph
|
||||
, scopeGraphAnalysis
|
||||
) where
|
||||
|
||||
import Analysis.Eval
|
||||
import Analysis.Analysis
|
||||
import Analysis.FlowInsensitive
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Carrier.Fail.WithLoc
|
||||
@ -16,13 +16,13 @@ import Control.Effect.Fresh
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.State
|
||||
import Control.Monad ((>=>))
|
||||
import Data.File
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name
|
||||
import Data.Foldable (fold)
|
||||
import Data.Function (fix)
|
||||
import Data.List.NonEmpty
|
||||
import Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Name
|
||||
import Data.Proxy
|
||||
import qualified Data.Set as Set
|
||||
import Data.Traversable (for)
|
||||
|
@ -7,7 +7,7 @@ module Analysis.Typecheck
|
||||
, typecheckingAnalysis
|
||||
) where
|
||||
|
||||
import Analysis.Eval
|
||||
import Analysis.Analysis
|
||||
import Analysis.FlowInsensitive
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Carrier.Fail.WithLoc
|
||||
@ -16,28 +16,29 @@ import Control.Effect.Fresh as Fresh
|
||||
import Control.Effect.Reader hiding (Local)
|
||||
import Control.Effect.State
|
||||
import Control.Monad ((>=>), unless)
|
||||
import Control.Monad.Module
|
||||
import Data.File
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name as Name
|
||||
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 Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe (fromJust, fromMaybe)
|
||||
import Data.Name as Name
|
||||
import Data.Proxy
|
||||
import Data.Scope
|
||||
import Data.Semigroup (Last (..))
|
||||
import qualified Data.Set as Set
|
||||
import Data.Term
|
||||
import Data.Traversable (for)
|
||||
import Data.Void
|
||||
import GHC.Generics (Generic1)
|
||||
import Prelude hiding (fail)
|
||||
import Source.Span
|
||||
import Syntax.Module
|
||||
import Syntax.Scope
|
||||
import Syntax.Term
|
||||
import Syntax.Var (closed)
|
||||
|
||||
data Monotype f a
|
||||
= Bool
|
||||
@ -166,24 +167,24 @@ typecheckingAnalysis = Analysis{..}
|
||||
arg <- meta
|
||||
assign addr arg
|
||||
ty <- eval body
|
||||
pure (Term (Arr arg ty))
|
||||
pure (Alg (Arr arg ty))
|
||||
apply _ f a = do
|
||||
_A <- meta
|
||||
_B <- meta
|
||||
unify (Term (Arr _A _B)) f
|
||||
unify (Alg (Arr _A _B)) f
|
||||
unify _A a
|
||||
pure _B
|
||||
unit = pure (Term Unit)
|
||||
bool _ = pure (Term Bool)
|
||||
asBool b = unify (Term Bool) b >> pure True <|> pure False
|
||||
string _ = pure (Term String)
|
||||
asString s = unify (Term String) s $> mempty
|
||||
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 (Term (Record (Map.fromList fields')))
|
||||
pure (Alg (Record (Map.fromList fields')))
|
||||
_ ... m = pure (Just m)
|
||||
|
||||
|
||||
@ -212,8 +213,8 @@ solve :: (Carrier sig m, Member (State Substitution) sig, MonadFail m) => Set.Se
|
||||
solve cs = for_ cs solve
|
||||
where solve = \case
|
||||
-- FIXME: how do we enforce proper subtyping? row polymorphism or something?
|
||||
Term (Record f1) :===: Term (Record f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
|
||||
Term (Arr a1 b1) :===: Term (Arr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2)
|
||||
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)
|
||||
Var m1 :===: Var m2 | m1 == m2 -> pure ()
|
||||
Var m1 :===: t2 -> do
|
||||
sol <- solution m1
|
||||
|
@ -12,7 +12,7 @@ import Control.Effect.Carrier
|
||||
import Control.Effect.Error
|
||||
import Control.Effect.Fail (Fail(..), MonadFail(..))
|
||||
import Control.Effect.Reader
|
||||
import Data.Loc
|
||||
import Core.Loc
|
||||
import Prelude hiding (fail)
|
||||
import Source.Span
|
||||
|
||||
|
66
semantic-core/src/Control/Carrier/Readline/Haskeline.hs
Normal file
66
semantic-core/src/Control/Carrier/Readline/Haskeline.hs
Normal file
@ -0,0 +1,66 @@
|
||||
{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeOperators, UndecidableInstances #-}
|
||||
module Control.Carrier.Readline.Haskeline
|
||||
( -- * Readline effect
|
||||
module Control.Effect.Readline
|
||||
-- * Readline carrier
|
||||
, runReadline
|
||||
, runReadlineWithHistory
|
||||
, ReadlineC (..)
|
||||
-- * Re-exports
|
||||
, Carrier
|
||||
, run
|
||||
, runM
|
||||
) where
|
||||
|
||||
import Control.Effect.Carrier
|
||||
import Control.Effect.Lift
|
||||
import Control.Effect.Reader
|
||||
import Control.Effect.Readline hiding (Carrier)
|
||||
import Control.Monad.Fix
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Coerce
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import Data.Text.Prettyprint.Doc.Render.Terminal (renderIO)
|
||||
import System.Console.Haskeline hiding (Handler, handle)
|
||||
import System.Console.Terminal.Size as Size
|
||||
import System.Directory
|
||||
import System.FilePath
|
||||
import System.IO (stdout)
|
||||
|
||||
runReadline :: MonadException m => Prefs -> Settings m -> ReadlineC m a -> m a
|
||||
runReadline prefs settings = runInputTWithPrefs prefs (coerce settings) . runM . runReader (Line 0) . runReadlineC
|
||||
|
||||
runReadlineWithHistory :: MonadException m => ReadlineC m a -> m a
|
||||
runReadlineWithHistory block = do
|
||||
homeDir <- liftIO getHomeDirectory
|
||||
prefs <- liftIO $ readPrefs (homeDir </> ".haskeline")
|
||||
let settingsDir = homeDir </> ".local/semantic-core"
|
||||
settings = Settings
|
||||
{ complete = noCompletion
|
||||
, historyFile = Just (settingsDir <> "/repl_history")
|
||||
, autoAddHistory = True
|
||||
}
|
||||
liftIO $ createDirectoryIfMissing True settingsDir
|
||||
|
||||
runReadline prefs settings block
|
||||
|
||||
newtype ReadlineC m a = ReadlineC { runReadlineC :: ReaderC Line (LiftC (InputT m)) a }
|
||||
deriving (Applicative, Functor, Monad, MonadFix, MonadIO)
|
||||
|
||||
instance MonadException m => Carrier Readline (ReadlineC m) where
|
||||
eff (Prompt prompt k) = ReadlineC $ do
|
||||
str <- sendM (getInputLine @m (cyan <> prompt <> plain))
|
||||
Line line <- ask
|
||||
local increment (runReadlineC (k line str))
|
||||
where cyan = "\ESC[1;36m\STX"
|
||||
plain = "\ESC[0m\STX"
|
||||
eff (Print doc k) = do
|
||||
s <- maybe 80 Size.width <$> liftIO size
|
||||
liftIO (renderIO stdout (layoutSmart defaultLayoutOptions { layoutPageWidth = AvailablePerLine s 0.8 } (doc <> line)))
|
||||
k
|
||||
|
||||
|
||||
newtype Line = Line Int
|
||||
|
||||
increment :: Line -> Line
|
||||
increment (Line n) = Line (n + 1)
|
@ -1,108 +1,30 @@
|
||||
{-# LANGUAGE DeriveAnyClass, DeriveFunctor, DeriveGeneric, DerivingStrategies, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, KindSignatures, MultiParamTypeClasses, OverloadedStrings, RankNTypes, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-}
|
||||
|
||||
{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, OverloadedStrings #-}
|
||||
module Control.Effect.Readline
|
||||
( Readline (..)
|
||||
( -- * Readline effect
|
||||
Readline (..)
|
||||
, prompt
|
||||
, print
|
||||
, println
|
||||
, askLine
|
||||
, Line (..)
|
||||
, increment
|
||||
, ReadlineC (..)
|
||||
, runReadline
|
||||
, runReadlineWithHistory
|
||||
, ControlIOC (..)
|
||||
, runControlIO
|
||||
-- * Re-exports
|
||||
, Carrier
|
||||
) where
|
||||
|
||||
import Control.Effect.Carrier
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import Data.Text.Prettyprint.Doc.Render.Terminal
|
||||
import GHC.Generics (Generic1)
|
||||
import Prelude hiding (print)
|
||||
|
||||
import Control.Effect.Carrier
|
||||
import Control.Effect.Lift
|
||||
import Control.Effect.Reader
|
||||
import Control.Monad.IO.Class
|
||||
import Control.Monad.Trans.Class
|
||||
import Data.Int
|
||||
import Data.String
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import Data.Text.Prettyprint.Doc.Render.Text
|
||||
import GHC.Generics (Generic1)
|
||||
import System.Console.Haskeline hiding (Handler, handle)
|
||||
import System.Directory
|
||||
import System.FilePath
|
||||
|
||||
data Readline m k
|
||||
= Prompt String (Maybe String -> m k)
|
||||
| Print AnyDoc (m k)
|
||||
| AskLine (Line -> m k)
|
||||
deriving stock (Functor, Generic1)
|
||||
deriving anyclass (Effect, HFunctor)
|
||||
= Prompt String (Int -> Maybe String -> m k)
|
||||
| Print (Doc AnsiStyle) (m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
newtype AnyDoc = AnyDoc { unAnyDoc :: forall a . Doc a }
|
||||
instance HFunctor Readline
|
||||
instance Effect Readline
|
||||
|
||||
prompt :: (IsString str, Member Readline sig, Carrier sig m) => String -> m (Maybe str)
|
||||
prompt p = fmap fromString <$> send (Prompt p pure)
|
||||
|
||||
print :: (Pretty a, Carrier sig m, Member Readline sig) => a -> m ()
|
||||
print s = send (Print (AnyDoc (pretty s)) (pure ()))
|
||||
prompt :: (Member Readline sig, Carrier sig m) => String -> m (Int, Maybe String)
|
||||
prompt p = send (Prompt p (curry pure))
|
||||
|
||||
println :: (Pretty a, Carrier sig m, Member Readline sig) => a -> m ()
|
||||
println s = print s >> print @String "\n"
|
||||
|
||||
askLine :: (Carrier sig m, Member Readline sig) => m Line
|
||||
askLine = send (AskLine pure)
|
||||
|
||||
newtype Line = Line Int64
|
||||
|
||||
increment :: Line -> Line
|
||||
increment (Line n) = Line (n + 1)
|
||||
|
||||
newtype ReadlineC m a = ReadlineC { runReadlineC :: ReaderC Line (LiftC (InputT m)) a }
|
||||
deriving newtype (Applicative, Functor, Monad, MonadIO)
|
||||
|
||||
runReadline :: MonadException m => Prefs -> Settings m -> ReadlineC m a -> m a
|
||||
runReadline prefs settings = runInputTWithPrefs prefs settings . runM . runReader (Line 0) . runReadlineC
|
||||
|
||||
instance (MonadException m, MonadIO m) => Carrier (Readline :+: Lift (InputT m)) (ReadlineC m) where
|
||||
eff (L (Prompt prompt k)) = ReadlineC $ do
|
||||
str <- lift (lift (getInputLine (cyan <> prompt <> plain)))
|
||||
local increment (runReadlineC (k str))
|
||||
where cyan = "\ESC[1;36m\STX"
|
||||
plain = "\ESC[0m\STX"
|
||||
eff (L (Print text k)) = liftIO (putDoc (unAnyDoc text)) *> k
|
||||
eff (L (AskLine k)) = ReadlineC ask >>= k
|
||||
eff (R other) = ReadlineC (eff (R (handleCoercible other)))
|
||||
|
||||
runReadlineWithHistory :: MonadException m => ReadlineC m a -> m a
|
||||
runReadlineWithHistory block = do
|
||||
homeDir <- liftIO getHomeDirectory
|
||||
prefs <- liftIO $ readPrefs (homeDir </> ".haskeline")
|
||||
let settingsDir = homeDir </> ".local/semantic-core"
|
||||
settings = Settings
|
||||
{ complete = noCompletion
|
||||
, historyFile = Just (settingsDir <> "/repl_history")
|
||||
, autoAddHistory = True
|
||||
}
|
||||
liftIO $ createDirectoryIfMissing True settingsDir
|
||||
|
||||
runReadline prefs settings block
|
||||
|
||||
runControlIO :: (forall x . m x -> IO x) -> ControlIOC m a -> m a
|
||||
runControlIO handler = runReader (Handler handler) . runControlIOC
|
||||
|
||||
-- | This exists to work around the 'MonadException' constraint that haskeline entails.
|
||||
newtype ControlIOC m a = ControlIOC { runControlIOC :: ReaderC (Handler m) m a }
|
||||
deriving newtype (Applicative, Functor, Monad, MonadIO)
|
||||
|
||||
newtype Handler m = Handler (forall x . m x -> IO x)
|
||||
|
||||
runHandler :: Handler m -> ControlIOC m a -> IO a
|
||||
runHandler h@(Handler handler) = handler . runReader h . runControlIOC
|
||||
|
||||
instance Carrier sig m => Carrier sig (ControlIOC m) where
|
||||
eff op = ControlIOC (eff (R (handleCoercible op)))
|
||||
|
||||
instance (Carrier sig m, MonadIO m) => MonadException (ControlIOC m) where
|
||||
controlIO f = ControlIOC $ do
|
||||
handler <- ask
|
||||
liftIO (f (RunIO (fmap pure . runHandler handler)) >>= runHandler handler)
|
||||
print :: (Carrier sig m, Member Readline sig) => Doc AnsiStyle -> m ()
|
||||
print s = send (Print s (pure ()))
|
||||
|
@ -1,50 +0,0 @@
|
||||
{-# LANGUAGE FlexibleInstances, QuantifiedConstraints, MultiParamTypeClasses, TypeOperators #-}
|
||||
module Control.Monad.Module
|
||||
( RightModule(..)
|
||||
, (>=>*)
|
||||
, (<=<*)
|
||||
, joinr
|
||||
) where
|
||||
|
||||
import Control.Effect.Carrier
|
||||
|
||||
-- | Modules over monads allow lifting of a monad’s product (i.e. 'Control.Monad.join') into another structure composed with the monad. A right-module @f m@ over a monad @m@ therefore allows one to extend @m@’s '>>=' operation to values of @f m@ using the '>>=*' operator.
|
||||
--
|
||||
-- In practical terms, this means that we can describe syntax which cannot itself bind or be substituted for variables, but which can be substituted inside when containing a substitutable expression monad. For example, we might not want to allow variables in a declaration context, but might still want to be able to substitute for e.g. globally-bound variables inside declarations; a 'RightModule' instance expresses this relationship nicely.
|
||||
--
|
||||
-- Note that we are calling this a right-module following Maciej Piróg, Nicolas Wu, & Jeremy Gibbons in _Modules Over Monads and their Algebras_; confusingly, other sources refer to this as a left-module.
|
||||
--
|
||||
-- Laws:
|
||||
--
|
||||
-- Right-identity:
|
||||
--
|
||||
-- @
|
||||
-- m >>=* return = m
|
||||
-- @
|
||||
--
|
||||
-- Associativity:
|
||||
--
|
||||
-- @
|
||||
-- m >>=* (k >=> h) = (m >>=* k) >>=* h
|
||||
-- @
|
||||
class (forall g . Functor g => Functor (f g), HFunctor f) => RightModule f where
|
||||
(>>=*) :: Monad m => f m a -> (a -> m b) -> f m b
|
||||
infixl 1 >>=*
|
||||
|
||||
instance (RightModule f, RightModule g) => RightModule (f :+: g) where
|
||||
L l >>=* f = L (l >>=* f)
|
||||
R r >>=* f = R (r >>=* f)
|
||||
|
||||
|
||||
(>=>*) :: (RightModule f, Monad m) => (a -> f m b) -> (b -> m c) -> (a -> f m c)
|
||||
f >=>* g = \x -> f x >>=* g
|
||||
|
||||
infixl 1 >=>*
|
||||
|
||||
(<=<*) :: (RightModule f, Monad m) => (b -> m c) -> (a -> f m b) -> (a -> f m c)
|
||||
g <=<* f = \x -> f x >>=* g
|
||||
|
||||
infixl 1 <=<*
|
||||
|
||||
joinr :: (RightModule f, Monad m) => f m (m a) -> f m a
|
||||
joinr = (>>=* id)
|
@ -1,6 +1,6 @@
|
||||
{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, LambdaCase, MultiParamTypeClasses, OverloadedStrings, QuantifiedConstraints, RankNTypes,
|
||||
ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
module Data.Core
|
||||
module Core.Core
|
||||
( Core(..)
|
||||
, rec
|
||||
, (>>>)
|
||||
@ -37,20 +37,20 @@ module Data.Core
|
||||
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Effect.Carrier
|
||||
import Control.Monad.Module
|
||||
import Core.Loc
|
||||
import Core.Name
|
||||
import Data.Bifunctor (Bifunctor (..))
|
||||
import Data.Foldable (foldl')
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import Data.Loc
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Stack
|
||||
import Data.Term
|
||||
import Data.Text (Text)
|
||||
import GHC.Generics (Generic1)
|
||||
import GHC.Stack
|
||||
import Source.Span
|
||||
import Syntax.Scope
|
||||
import Syntax.Stack
|
||||
import Syntax.Module
|
||||
import Syntax.Term
|
||||
|
||||
data Core f a
|
||||
-- | Recursive local binding of a name in a scope; strict evaluation of the name in the body will diverge.
|
||||
@ -118,8 +118,8 @@ a >>> b = send (a :>> b)
|
||||
infixr 1 >>>
|
||||
|
||||
unseq :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
||||
unseq (Term sig) | Just (a :>> b) <- prj sig = pure (a, b)
|
||||
unseq _ = empty
|
||||
unseq (Alg sig) | Just (a :>> b) <- prj sig = pure (a, b)
|
||||
unseq _ = empty
|
||||
|
||||
unseqs :: Member Core sig => Term sig a -> NonEmpty (Term sig a)
|
||||
unseqs = go
|
||||
@ -135,8 +135,8 @@ Named u n :<- a >>>= b = send (Named u a :>>= abstract1 n b)
|
||||
infixr 1 >>>=
|
||||
|
||||
unbind :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a :<- Term sig a, Term sig a)
|
||||
unbind n (Term sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b)
|
||||
unbind _ _ = empty
|
||||
unbind n (Alg sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b)
|
||||
unbind _ _ = empty
|
||||
|
||||
unstatement :: (Alternative m, Member 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
|
||||
@ -164,8 +164,8 @@ lams :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Named a) -> m a
|
||||
lams names body = foldr lam body names
|
||||
|
||||
unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
|
||||
unlam n (Term sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b))
|
||||
unlam _ _ = empty
|
||||
unlam n (Alg sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b))
|
||||
unlam _ _ = empty
|
||||
|
||||
($$) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
||||
f $$ a = send (f :$ a)
|
||||
@ -179,8 +179,8 @@ infixl 8 $$
|
||||
infixl 8 $$*
|
||||
|
||||
unapply :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
||||
unapply (Term sig) | Just (f :$ a) <- prj sig = pure (f, a)
|
||||
unapply _ = empty
|
||||
unapply (Alg sig) | Just (f :$ a) <- prj sig = pure (f, a)
|
||||
unapply _ = empty
|
||||
|
||||
unapplies :: Member Core sig => Term sig a -> (Term sig a, Stack (Term sig a))
|
||||
unapplies core = case unapply core of
|
||||
@ -237,6 +237,6 @@ annWith callStack = maybe id (annAt . snd) (stackLoc callStack)
|
||||
|
||||
|
||||
stripAnnotations :: forall ann a sig . (HFunctor sig, forall g . Functor g => Functor (sig g)) => Term (Ann ann :+: sig) a -> Term sig a
|
||||
stripAnnotations (Var v) = Var v
|
||||
stripAnnotations (Term (L (Ann _ b))) = stripAnnotations b
|
||||
stripAnnotations (Term (R b)) = Term (hmap stripAnnotations b)
|
||||
stripAnnotations (Var v) = Var v
|
||||
stripAnnotations (Alg (L (Ann _ b))) = stripAnnotations b
|
||||
stripAnnotations (Alg (R b)) = Alg (hmap stripAnnotations b)
|
@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE FlexibleContexts, TypeOperators #-}
|
||||
module Data.Core.Parser
|
||||
module Core.Core.Parser
|
||||
( core
|
||||
, lit
|
||||
, expr
|
||||
@ -12,11 +12,11 @@ module Data.Core.Parser
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Effect.Carrier
|
||||
import Core.Core ((:<-) (..), Core)
|
||||
import qualified Core.Core as Core
|
||||
import Core.Name
|
||||
import qualified Data.Char as Char
|
||||
import Data.Core ((:<-) (..), Core)
|
||||
import qualified Data.Core as Core
|
||||
import Data.Foldable (foldl')
|
||||
import Data.Name
|
||||
import Data.String
|
||||
import qualified Text.Parser.Token as Token
|
||||
import qualified Text.Parser.Token.Highlight as Highlight
|
@ -1,6 +1,6 @@
|
||||
{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, TypeApplications #-}
|
||||
|
||||
module Data.Core.Pretty
|
||||
module Core.Core.Pretty
|
||||
( showCore
|
||||
, printCore
|
||||
, showFile
|
||||
@ -8,16 +8,17 @@ module Data.Core.Pretty
|
||||
, prettyCore
|
||||
) where
|
||||
|
||||
import Data.Core
|
||||
import Data.File
|
||||
import Core.Core
|
||||
import Core.File
|
||||
import Core.Name
|
||||
import Data.Foldable (toList)
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Stack
|
||||
import Data.Term
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
|
||||
import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty
|
||||
import Syntax.Pretty
|
||||
import Syntax.Scope
|
||||
import Syntax.Stack
|
||||
import Syntax.Term
|
||||
|
||||
showCore :: Term Core Name -> String
|
||||
showCore = Pretty.renderString . layoutSmart defaultLayoutOptions . unAnnotate . prettyCore Ascii
|
||||
@ -45,10 +46,10 @@ name :: Name -> AnsiDoc
|
||||
name n = if needsQuotation n then enclose (symbol "#{") (symbol "}") (pretty n) else pretty n
|
||||
|
||||
prettyCore :: Style -> Term Core Name -> AnsiDoc
|
||||
prettyCore style = precBody . go . fmap name
|
||||
prettyCore style = unPrec . go . fmap name
|
||||
where go = \case
|
||||
Var v -> atom v
|
||||
Term t -> case t of
|
||||
Alg t -> case t of
|
||||
Rec (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
|
||||
[ keyword "rec" <+> name x
|
||||
, symbol "=" <+> align (withPrec 0 (go (instantiate1 (pure (name x)) b)))
|
||||
@ -66,9 +67,9 @@ prettyCore style = precBody . go . fmap name
|
||||
f :$ x -> prec 8 (withPrec 8 (go f) <+> withPrec 9 (go x))
|
||||
|
||||
If con tru fal -> prec 3 . group $ vsep
|
||||
[ keyword "if" <+> precBody (go con)
|
||||
, keyword "then" <+> precBody (go tru)
|
||||
, keyword "else" <+> precBody (go fal)
|
||||
[ keyword "if" <+> unPrec (go con)
|
||||
, keyword "then" <+> unPrec (go tru)
|
||||
, keyword "else" <+> unPrec (go fal)
|
||||
]
|
||||
|
||||
Load p -> prec 3 (keyword "load" <+> withPrec 9 (go p))
|
||||
@ -80,16 +81,16 @@ prettyCore style = precBody . go . fmap name
|
||||
]
|
||||
|
||||
statement ->
|
||||
let (bindings, return) = unstatements (Term statement)
|
||||
let (bindings, return) = unstatements (Alg statement)
|
||||
statements = toList (bindings :> (Nothing :<- return))
|
||||
names = zipWith (\ i (n :<- _) -> maybe (pretty @Int i) (name . namedName) n) [0..] statements
|
||||
statements' = map (prettyStatement names) statements
|
||||
in atom (block "; " statements')
|
||||
block _ [] = braces mempty
|
||||
block s ss = encloseSep "{ " " }" s ss
|
||||
keyValue x v = name x <+> symbol ":" <+> precBody (go v)
|
||||
prettyStatement names (Just (Named (Ignored u) _) :<- t) = name u <+> arrowL <+> precBody (go (either (names !!) id <$> t))
|
||||
prettyStatement names (Nothing :<- t) = precBody (go (either (names !!) id <$> t))
|
||||
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 (Nothing :<- t) = unPrec (go (either (names !!) id <$> t))
|
||||
lambda = case style of
|
||||
Unicode -> symbol "λ"
|
||||
Ascii -> symbol "\\"
|
||||
@ -99,21 +100,3 @@ prettyCore style = precBody . go . fmap name
|
||||
arrowL = case style of
|
||||
Unicode -> symbol "←"
|
||||
Ascii -> symbol "<-"
|
||||
|
||||
|
||||
data Prec a = Prec
|
||||
{ precLevel :: Maybe Int
|
||||
, precBody :: a
|
||||
}
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
prec :: Int -> a -> Prec a
|
||||
prec = Prec . Just
|
||||
|
||||
atom :: a -> Prec a
|
||||
atom = Prec Nothing
|
||||
|
||||
withPrec :: Int -> Prec AnsiDoc -> AnsiDoc
|
||||
withPrec d (Prec d' a)
|
||||
| maybe False (d >) d' = parens a
|
||||
| otherwise = a
|
@ -1,10 +1,10 @@
|
||||
{-# LANGUAGE DeriveTraversable #-}
|
||||
module Data.File
|
||||
module Core.File
|
||||
( File(..)
|
||||
, fromBody
|
||||
) where
|
||||
|
||||
import Data.Loc
|
||||
import Core.Loc
|
||||
import Data.Maybe (fromJust)
|
||||
import GHC.Stack
|
||||
import Source.Span
|
@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
module Data.Loc
|
||||
module Core.Loc
|
||||
( Path(..)
|
||||
, here
|
||||
, stackLoc
|
@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE DeriveGeneric, DeriveTraversable, GeneralizedNewtypeDeriving, LambdaCase, OverloadedLists #-}
|
||||
module Data.Name
|
||||
module Core.Name
|
||||
( Name (..)
|
||||
, Named(..)
|
||||
, named
|
@ -1,132 +0,0 @@
|
||||
{-# LANGUAGE DeriveTraversable, LambdaCase, RankNTypes, QuantifiedConstraints, StandaloneDeriving #-}
|
||||
module Data.Scope
|
||||
( Incr(..)
|
||||
, incr
|
||||
, closed
|
||||
, Scope(..)
|
||||
, fromScope
|
||||
, toScope
|
||||
, abstract1
|
||||
, abstract
|
||||
, abstractEither
|
||||
, instantiate1
|
||||
, instantiate
|
||||
, instantiateEither
|
||||
, unprefix
|
||||
, unprefixEither
|
||||
) where
|
||||
|
||||
import Control.Applicative (liftA2)
|
||||
import Control.Effect.Carrier
|
||||
import Control.Monad ((>=>), guard)
|
||||
import Control.Monad.Module
|
||||
import Control.Monad.Trans.Class
|
||||
import Data.Function (on)
|
||||
import Data.Stack
|
||||
|
||||
data Incr a b
|
||||
= Z a
|
||||
| S b
|
||||
deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
|
||||
|
||||
instance Applicative (Incr a) where
|
||||
pure = S
|
||||
Z a <*> _ = Z a
|
||||
S f <*> a = f <$> a
|
||||
|
||||
instance Monad (Incr a) where
|
||||
Z a >>= _ = Z a
|
||||
S a >>= f = f a
|
||||
|
||||
match :: Applicative f => (b -> Either a c) -> b -> Incr a (f c)
|
||||
match f x = either Z (S . pure) (f x)
|
||||
|
||||
matchMaybe :: (b -> Maybe a) -> (b -> Either a b)
|
||||
matchMaybe f a = maybe (Right a) Left (f a)
|
||||
|
||||
incr :: (a -> c) -> (b -> c) -> Incr a b -> c
|
||||
incr z s = \case { Z a -> z a ; S b -> s b }
|
||||
|
||||
|
||||
closed :: Traversable f => f a -> Maybe (f b)
|
||||
closed = traverse (const Nothing)
|
||||
|
||||
|
||||
newtype Scope a f b = Scope { unScope :: f (Incr a (f b)) }
|
||||
deriving (Foldable, Functor, Traversable)
|
||||
|
||||
instance HFunctor (Scope a) where
|
||||
hmap f = Scope . f . fmap (fmap f) . unScope
|
||||
|
||||
instance (Eq a, Eq b, forall a . Eq a => Eq (f a), Monad f) => Eq (Scope a f b) where
|
||||
(==) = (==) `on` fromScope
|
||||
|
||||
instance (Ord a, Ord b, forall a . Eq a => Eq (f a)
|
||||
, forall a . Ord a => Ord (f a), Monad f) => Ord (Scope a f b) where
|
||||
compare = compare `on` fromScope
|
||||
|
||||
deriving instance (Show a, Show b, forall a . Show a => Show (f a)) => Show (Scope a f b)
|
||||
|
||||
instance Applicative f => Applicative (Scope a f) where
|
||||
pure = Scope . pure . S . pure
|
||||
Scope f <*> Scope a = Scope (liftA2 (liftA2 (<*>)) f a)
|
||||
|
||||
instance Monad f => Monad (Scope a f) where
|
||||
Scope e >>= f = Scope (e >>= incr (pure . Z) (>>= unScope . f))
|
||||
|
||||
instance MonadTrans (Scope a) where
|
||||
lift = Scope . pure . S
|
||||
|
||||
instance RightModule (Scope a) where
|
||||
Scope m >>=* f = Scope (fmap (>>= f) <$> m)
|
||||
|
||||
|
||||
fromScope :: Monad f => Scope a f b -> f (Incr a b)
|
||||
fromScope = unScope >=> sequenceA
|
||||
|
||||
toScope :: Applicative f => f (Incr a b) -> Scope a f b
|
||||
toScope = Scope . fmap (fmap pure)
|
||||
|
||||
|
||||
-- | Bind occurrences of a variable in a term, producing a term in which the variable is bound.
|
||||
abstract1 :: (Applicative f, Eq a) => a -> f a -> Scope () f a
|
||||
abstract1 n = abstract (guard . (== n))
|
||||
|
||||
abstract :: Applicative f => (b -> Maybe a) -> f b -> Scope a f b
|
||||
abstract f = abstractEither (matchMaybe f)
|
||||
|
||||
abstractEither :: Applicative f => (b -> Either a c) -> f b -> Scope a f c
|
||||
abstractEither f = Scope . fmap (match f) -- FIXME: succ as little of the expression as possible, cf https://twitter.com/ollfredo/status/1145776391826358273
|
||||
|
||||
|
||||
-- | Substitute a term for the free variable in a given term, producing a closed term.
|
||||
instantiate1 :: Monad f => f b -> Scope a f b -> f b
|
||||
instantiate1 t = instantiate (const t)
|
||||
|
||||
instantiate :: Monad f => (a -> f b) -> Scope a f b -> f b
|
||||
instantiate f = instantiateEither (either f pure)
|
||||
|
||||
instantiateEither :: Monad f => (Either a b -> f c) -> Scope a f b -> f c
|
||||
instantiateEither f = unScope >=> incr (f . Left) (>>= f . Right)
|
||||
|
||||
|
||||
-- | Unwrap a (possibly-empty) prefix of @a@s wrapping a @t@ using a helper function.
|
||||
--
|
||||
-- This allows us to peel a prefix of syntax, typically binders, off of a term, returning a stack of prefixing values (e.g. variables) and the outermost subterm rejected by the function.
|
||||
unprefix
|
||||
:: (Int -> t -> Maybe (a, t)) -- ^ A function taking the 0-based index into the prefix & the current term, and optionally returning a pair of the prefixing value and the inner subterm.
|
||||
-> t -- ^ The initial term.
|
||||
-> (Stack a, t) -- ^ A stack of prefixing values & the final subterm.
|
||||
unprefix from = unprefixEither (matchMaybe . from)
|
||||
|
||||
-- | Unwrap a (possibly-empty) prefix of @a@s wrapping a @b@ within a @t@ using a helper function.
|
||||
--
|
||||
-- Compared to 'unprefix', this allows the helper function to extract inner terms of a different type, for example when @t@ is a right @b@-module.
|
||||
unprefixEither
|
||||
:: (Int -> t -> Either (a, t) b) -- ^ A function taking the 0-based index into the prefix & the current term, and returning either a pair of the prefixing value and the next inner subterm of type @t@, or the final inner subterm of type @b@.
|
||||
-> t -- ^ The initial term.
|
||||
-> (Stack a, b) -- ^ A stack of prefixing values & the final subterm.
|
||||
unprefixEither from = go (0 :: Int) Nil
|
||||
where go i bs t = case from i t of
|
||||
Left (b, t) -> go (succ i) (bs :> b) t
|
||||
Right b -> (bs, b)
|
@ -1,18 +0,0 @@
|
||||
{-# LANGUAGE DeriveTraversable #-}
|
||||
module Data.Stack
|
||||
( Stack(..)
|
||||
) where
|
||||
|
||||
data Stack a
|
||||
= Nil
|
||||
| Stack a :> a
|
||||
deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
|
||||
|
||||
infixl 4 :>
|
||||
|
||||
instance Semigroup (Stack a) where
|
||||
xs <> Nil = xs
|
||||
xs <> (ys :> y) = (xs <> ys) :> y
|
||||
|
||||
instance Monoid (Stack a) where
|
||||
mempty = Nil
|
@ -1,50 +0,0 @@
|
||||
{-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, StandaloneDeriving, UndecidableInstances #-}
|
||||
module Data.Term
|
||||
( Term(..)
|
||||
, hoistTerm
|
||||
) where
|
||||
|
||||
import Control.Effect.Carrier
|
||||
import Control.Monad (ap)
|
||||
import Control.Monad.Module
|
||||
|
||||
data Term sig a
|
||||
= Var a
|
||||
| Term (sig (Term sig) a)
|
||||
|
||||
deriving instance ( Eq a
|
||||
, RightModule sig
|
||||
, forall g x . (Eq x, Monad g, forall y . Eq y => Eq (g y)) => Eq (sig g x)
|
||||
)
|
||||
=> Eq (Term sig a)
|
||||
deriving instance ( Ord a
|
||||
, RightModule sig
|
||||
, forall g x . (Eq x, Monad g, forall y . Eq y => Eq (g y)) => Eq (sig g x)
|
||||
, forall g x . (Ord x, Monad g, forall y . Eq y => Eq (g y)
|
||||
, forall y . Ord y => Ord (g y)) => Ord (sig g x)
|
||||
)
|
||||
=> Ord (Term sig a)
|
||||
deriving instance (Show a, forall g x . (Show x, forall y . Show y => Show (g y)) => Show (sig g x)) => Show (Term sig a)
|
||||
|
||||
deriving instance ( forall g . Foldable g => Foldable (sig g)) => Foldable (Term sig)
|
||||
deriving instance ( forall g . Functor g => Functor (sig g)) => Functor (Term sig)
|
||||
deriving instance ( forall g . Foldable g => Foldable (sig g)
|
||||
, forall g . Functor g => Functor (sig g)
|
||||
, forall g . Traversable g => Traversable (sig g)) => Traversable (Term sig)
|
||||
|
||||
instance RightModule sig => Applicative (Term sig) where
|
||||
pure = Var
|
||||
(<*>) = ap
|
||||
|
||||
instance RightModule sig => Monad (Term sig) where
|
||||
Var a >>= f = f a
|
||||
Term t >>= f = Term (t >>=* f)
|
||||
|
||||
instance RightModule sig => Carrier sig (Term sig) where
|
||||
eff = Term
|
||||
|
||||
|
||||
hoistTerm :: (HFunctor sig, forall g . Functor g => Functor (sig g)) => (forall m x . sig m x -> sig' m x) -> Term sig a -> Term sig' a
|
||||
hoistTerm f = go
|
||||
where go (Var v) = Var v
|
||||
go (Term t) = Term (f (hmap (hoistTerm f) t))
|
@ -17,9 +17,8 @@ import qualified Hedgehog.Gen as Gen
|
||||
import qualified Hedgehog.Range as Range
|
||||
|
||||
import Control.Effect.Carrier
|
||||
import qualified Data.Core as Core
|
||||
import Data.Name
|
||||
import Data.Term
|
||||
import qualified Core.Core as Core
|
||||
import Core.Name
|
||||
|
||||
-- The 'prune' call here ensures that we don't spend all our time just generating
|
||||
-- fresh names for variables, since the length of variable names is not an
|
||||
@ -31,7 +30,7 @@ name = Gen.prune (named' <$> names) where
|
||||
boolean :: (Carrier sig t, Member Core.Core sig, MonadGen m) => m (t Name)
|
||||
boolean = Core.bool <$> Gen.bool
|
||||
|
||||
variable :: (Carrier sig t, Member Core.Core sig, MonadGen m) => m (t Name)
|
||||
variable :: (Applicative t, MonadGen m) => m (t Name)
|
||||
variable = pure . namedValue <$> name
|
||||
|
||||
ifthenelse :: (Carrier sig t, Member Core.Core sig, MonadGen m) => m (t Name) -> m (t Name)
|
||||
|
@ -1,7 +1,6 @@
|
||||
{-# LANGUAGE OverloadedStrings, TypeApplications, TypeOperators #-}
|
||||
module Main (main) where
|
||||
|
||||
import Data.String
|
||||
import qualified Text.Trifecta as Trifecta
|
||||
|
||||
import Hedgehog hiding (Var)
|
||||
@ -9,17 +8,15 @@ import Test.Tasty
|
||||
import Test.Tasty.Hedgehog
|
||||
import Test.Tasty.HUnit
|
||||
|
||||
import Control.Effect.Sum
|
||||
import Data.File
|
||||
import Data.Loc (Path)
|
||||
import qualified Generators as Gen
|
||||
import qualified Analysis.Eval as Eval
|
||||
import Data.Core
|
||||
import Data.Core.Pretty
|
||||
import Data.Core.Parser as Parse
|
||||
import Data.Name
|
||||
import Data.Term
|
||||
import Core.Core
|
||||
import Core.Core.Pretty
|
||||
import Core.Core.Parser as Parse
|
||||
import Core.File
|
||||
import Core.Name
|
||||
import qualified Generators as Gen
|
||||
import Source.Span
|
||||
import Syntax.Term
|
||||
|
||||
-- * Helpers
|
||||
|
@ -22,6 +22,7 @@ common haskell
|
||||
default-language: Haskell2010
|
||||
build-depends: base ^>=4.12
|
||||
, fused-effects ^>= 0.5
|
||||
, fused-syntax
|
||||
, semantic-core ^>= 0.0
|
||||
, semantic-source ^>= 0.0
|
||||
, semantic-tags ^>= 0.0
|
||||
|
@ -13,16 +13,16 @@ import AST.Element
|
||||
import Control.Effect hiding ((:+:))
|
||||
import Control.Effect.Reader
|
||||
import Control.Monad.Fail
|
||||
import Core.Core as Core
|
||||
import Core.Name as Name
|
||||
import Data.Coerce
|
||||
import Data.Core as Core
|
||||
import Data.Foldable
|
||||
import Data.Function
|
||||
import Data.Name as Name
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import Data.Stack (Stack (..))
|
||||
import qualified Data.Stack as Stack
|
||||
import GHC.Records
|
||||
import Source.Span (Span)
|
||||
import Syntax.Stack (Stack)
|
||||
import qualified Syntax.Stack as Stack
|
||||
import qualified TreeSitter.Python.AST as Py
|
||||
|
||||
-- | Keeps track of the current scope's bindings (so that we can, when
|
||||
|
@ -6,13 +6,13 @@ module Directive ( Directive (..)
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad
|
||||
import Data.Name (Name)
|
||||
import Data.Term (Term)
|
||||
import Data.Core (Core)
|
||||
import qualified Data.Core.Parser as Core.Parser
|
||||
import qualified Data.Core.Pretty as Core.Pretty
|
||||
import Core.Core (Core)
|
||||
import qualified Core.Core.Parser as Core.Parser
|
||||
import qualified Core.Core.Pretty as Core.Pretty
|
||||
import Core.Name (Name)
|
||||
import Data.ByteString.Char8 (ByteString)
|
||||
import qualified Data.ByteString.Char8 as ByteString
|
||||
import Syntax.Term (Term)
|
||||
import System.Process
|
||||
import qualified Text.Trifecta as Trifecta
|
||||
|
||||
|
@ -8,11 +8,11 @@ module Instances () where
|
||||
-- we should keep track of them in a dedicated file.
|
||||
|
||||
import Analysis.ScopeGraph
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name (Name (..))
|
||||
import Data.Aeson
|
||||
import Data.File
|
||||
import Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Name (Name (..))
|
||||
import Data.Text (Text)
|
||||
|
||||
deriving newtype instance ToJSON Name
|
||||
|
@ -3,6 +3,7 @@
|
||||
module Main (main) where
|
||||
|
||||
import qualified Analysis.Eval as Eval
|
||||
import Analysis.ScopeGraph
|
||||
import Control.Effect
|
||||
import Control.Effect.Fail
|
||||
import Control.Effect.Reader
|
||||
@ -10,21 +11,20 @@ import Control.Monad hiding (fail)
|
||||
import Control.Monad.Catch
|
||||
import Control.Monad.IO.Class
|
||||
import Control.Monad.Trans.Resource (ResourceT, runResourceT)
|
||||
import Core.Core
|
||||
import Core.Core.Pretty
|
||||
import Core.File
|
||||
import Core.Loc
|
||||
import Core.Name
|
||||
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.Core
|
||||
import Data.Core.Pretty
|
||||
import Data.File
|
||||
import Data.Foldable
|
||||
import Data.Function
|
||||
import Data.List (sort)
|
||||
import Data.Loc
|
||||
import Data.Maybe
|
||||
import Data.Name
|
||||
import Data.Term
|
||||
import GHC.Stack
|
||||
import qualified Language.Python.Core as Py
|
||||
import Prelude hiding (fail)
|
||||
@ -32,19 +32,19 @@ import Source.Span
|
||||
import Streaming
|
||||
import qualified Streaming.Prelude as Stream
|
||||
import qualified Streaming.Process
|
||||
import Syntax.Term
|
||||
import System.Directory
|
||||
import System.Exit
|
||||
import qualified TreeSitter.Python as TSP
|
||||
import qualified TreeSitter.Unmarshal as TS
|
||||
import Text.Show.Pretty (ppShow)
|
||||
import qualified System.Path as Path
|
||||
import qualified System.Path.Directory as Path
|
||||
import System.Path ((</>))
|
||||
import Text.Show.Pretty (ppShow)
|
||||
import qualified TreeSitter.Python as TSP
|
||||
import qualified TreeSitter.Unmarshal as TS
|
||||
|
||||
import qualified Test.Tasty as Tasty
|
||||
import qualified Test.Tasty.HUnit as HUnit
|
||||
|
||||
import Analysis.ScopeGraph
|
||||
import qualified Directive
|
||||
import Instances ()
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user