mirror of
https://github.com/anoma/juvix.git
synced 2025-01-05 14:34:03 +03:00
setup InfoTable for parser
This commit is contained in:
Jan Mas Rovira
parent
743b5b153a
commit
22b5de42f3
37
app/Main.hs
37
app/Main.hs
@ -16,6 +16,7 @@ import qualified MiniJuvix.Syntax.Concrete.Language as M
|
||||
import qualified MiniJuvix.Syntax.Concrete.Parser as M
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.InfoTable as Scoped
|
||||
import qualified MiniJuvix.Syntax.Concrete.Parser.InfoTable as Parser
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Highlight as Scoped
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
|
||||
@ -35,6 +36,7 @@ import MiniJuvix.Utils.Version (runDisplayVersion)
|
||||
import Options.Applicative
|
||||
import Options.Applicative.Help.Pretty
|
||||
import Text.Show.Pretty hiding (Html)
|
||||
import MiniJuvix.Syntax.Concrete.Parser.InfoTable (infoParsedItems)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -265,6 +267,10 @@ mkScopePrettyOptions ScopeOptions {..} =
|
||||
parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
|
||||
parseModuleIO = fromRightIO id . M.runModuleParserIO
|
||||
|
||||
parseModuleIO' :: FilePath -> IO (Parser.InfoTable, M.Module 'M.Parsed 'M.ModuleTop)
|
||||
parseModuleIO' = fromRightIO id . M.runModuleParserIO'
|
||||
|
||||
|
||||
minijuvixYamlFile :: FilePath
|
||||
minijuvixYamlFile = "minijuvix.yaml"
|
||||
|
||||
@ -275,8 +281,9 @@ findRoot = do
|
||||
Left err -> do
|
||||
putStrLn "Something went wrong when figuring out the root of the project."
|
||||
putStrLn (pack (IO.displayException err))
|
||||
putStrLn "I will try to use the current directory."
|
||||
getCurrentDirectory
|
||||
cur <- getCurrentDirectory
|
||||
putStrLn ("I will try to use the current directory: " <> pack cur)
|
||||
return cur
|
||||
Right root -> return root
|
||||
where
|
||||
possiblePaths :: FilePath -> [FilePath]
|
||||
@ -300,7 +307,7 @@ runCommand c = do
|
||||
Scope opts@ScopeOptions {..} -> do
|
||||
forM_ _scopeInputFiles $ \scopeInputFile -> do
|
||||
m <- parseModuleIO scopeInputFile
|
||||
(_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
s <- head . M._resultModules <$> fromRightIO' printErrorAnsi (M.scopeCheck1IO root m)
|
||||
printer (mkScopePrettyOptions opts) s
|
||||
where
|
||||
printer :: M.Options -> M.Module 'M.Scoped 'M.ModuleTop -> IO ()
|
||||
@ -308,15 +315,19 @@ runCommand c = do
|
||||
| not _scopeNoColors = M.printPrettyCode
|
||||
| otherwise = T.printPrettyCode
|
||||
Highlight HighlightOptions {..} -> do
|
||||
m <- parseModuleIO _highlightInputFile
|
||||
(i , _) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
putStrLn (Scoped.go (i ^. Scoped.infoNames))
|
||||
(tbl, m) <- parseModuleIO' _highlightInputFile
|
||||
res <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
let
|
||||
names = res ^. M.resultScoperTable . Scoped.infoNames
|
||||
parsedItems = res ^. M.resultParserTable . Parser.infoParsedItems
|
||||
<> tbl ^. infoParsedItems
|
||||
putStrLn (Scoped.go parsedItems names)
|
||||
Parse ParseOptions {..} -> do
|
||||
m <- parseModuleIO _parseInputFile
|
||||
if _parseNoPrettyShow then print m else pPrint m
|
||||
Html HtmlOptions {..} -> do
|
||||
m <- parseModuleIO _htmlInputFile
|
||||
(_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
s <- head . M._resultModules <$> fromRightIO' printErrorAnsi (M.scopeCheck1IO root m)
|
||||
genHtml defaultOptions _htmlRecursive _htmlTheme s
|
||||
MicroJuvix (Pretty MicroJuvixOptions {..}) -> do
|
||||
micro <- miniToMicro root _mjuvixInputFile
|
||||
@ -328,8 +339,8 @@ runCommand c = do
|
||||
Left es -> sequence_ (intersperse (putStrLn "") (printErrorAnsi <$> toList es)) >> exitFailure
|
||||
MiniHaskell MiniHaskellOptions {..} -> do
|
||||
m <- parseModuleIO _mhaskellInputFile
|
||||
(_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
(_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
|
||||
s <- head . M._resultModules <$> fromRightIO' printErrorAnsi (M.scopeCheck1IO root m)
|
||||
(_, a) <- fromRightIO' putStrLn (return (A.translateModule s))
|
||||
let micro = Micro.translateModule a
|
||||
case Micro.checkModule micro of
|
||||
Right checkedMicro -> do
|
||||
@ -338,7 +349,7 @@ runCommand c = do
|
||||
Left es -> mapM_ printErrorAnsi es >> exitFailure
|
||||
Termination (Calls opts@CallsOptions {..}) -> do
|
||||
m <- parseModuleIO _callsInputFile
|
||||
(_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
s <- head . M._resultModules <$> fromRightIO' printErrorAnsi (M.scopeCheck1IO root m)
|
||||
(_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
|
||||
let callMap0 = T.buildCallMap a
|
||||
callMap = case _callsFunctionNameFilter of
|
||||
@ -349,8 +360,8 @@ runCommand c = do
|
||||
putStrLn ""
|
||||
Termination (CallGraph CallGraphOptions {..}) -> do
|
||||
m <- parseModuleIO _graphInputFile
|
||||
(_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
(_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
|
||||
s <- head . M._resultModules <$> fromRightIO' printErrorAnsi (M.scopeCheck1IO root m)
|
||||
(_, a) <- fromRightIO' putStrLn (return (A.translateModule s))
|
||||
let callMap = T.buildCallMap a
|
||||
opts' = A.defaultOptions
|
||||
completeGraph = T.completeCallGraph callMap
|
||||
@ -370,7 +381,7 @@ runCommand c = do
|
||||
miniToMicro :: FilePath -> FilePath -> IO Micro.Module
|
||||
miniToMicro root p = do
|
||||
m <- parseModuleIO p
|
||||
(_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
|
||||
s <- head . M._resultModules <$> fromRightIO' printErrorAnsi (M.scopeCheck1IO root m)
|
||||
(_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
|
||||
return (Micro.translateModule a)
|
||||
|
||||
|
||||
@ -48,5 +48,21 @@
|
||||
"The face used for axioms."
|
||||
:group 'minijuvix-highlight-faces)
|
||||
|
||||
(defface minijuvix-highlight-string-face
|
||||
'((((background light))
|
||||
(:foreground "#f07171"))
|
||||
(((background dark))
|
||||
(:foreground "#bf616a")))
|
||||
"The face used for string literals."
|
||||
:group 'minijuvix-highlight-faces)
|
||||
|
||||
(defface minijuvix-highlight-number-face
|
||||
'((((background light))
|
||||
(:foreground "#000000"))
|
||||
(((background dark))
|
||||
(:foreground "#d8dee9")))
|
||||
"The face used for numbers."
|
||||
:group 'minijuvix-highlight-faces)
|
||||
|
||||
|
||||
(provide 'minijuvix-highlight)
|
||||
|
||||
@ -27,6 +27,7 @@ dependencies:
|
||||
- directory == 1.3.*
|
||||
- edit-distance == 0.2.*
|
||||
- extra == 1.7.*
|
||||
- transformers == 0.5.*
|
||||
- filepath == 1.4.*
|
||||
- gitrev == 1.3.*
|
||||
- hashable == 1.4.*
|
||||
|
||||
@ -65,12 +65,21 @@ let_ = "let"
|
||||
public :: IsString s => s
|
||||
public = "public"
|
||||
|
||||
number :: IsString s => s
|
||||
number = "number"
|
||||
|
||||
string :: IsString s => s
|
||||
string = "string"
|
||||
|
||||
any :: IsString s => s
|
||||
any = "Any"
|
||||
|
||||
type_ :: IsString s => s
|
||||
type_ = "Type"
|
||||
|
||||
keyword :: IsString s => s
|
||||
keyword = "keyword"
|
||||
|
||||
using :: IsString s => s
|
||||
using = "using"
|
||||
|
||||
|
||||
@ -42,7 +42,6 @@ module MiniJuvix.Prelude.Base
|
||||
module Polysemy.Output,
|
||||
module Polysemy.Reader,
|
||||
module Polysemy.State,
|
||||
module Polysemy.View,
|
||||
module Prettyprinter,
|
||||
module System.Directory,
|
||||
module System.Exit,
|
||||
@ -115,7 +114,6 @@ import Polysemy.Fixpoint
|
||||
import Polysemy.Output
|
||||
import Polysemy.Reader
|
||||
import Polysemy.State
|
||||
import Polysemy.View
|
||||
import Prettyprinter (Doc, (<+>))
|
||||
import System.Directory
|
||||
import System.Exit
|
||||
|
||||
@ -4,6 +4,7 @@ module MiniJuvix.Syntax.Concrete.Base
|
||||
module Text.Megaparsec.Char,
|
||||
module Control.Monad.Combinators.Expr,
|
||||
module Control.Monad.Combinators.NonEmpty,
|
||||
module Control.Monad.Trans.Class
|
||||
)
|
||||
where
|
||||
|
||||
@ -13,3 +14,4 @@ import Data.List.NonEmpty (NonEmpty)
|
||||
import MiniJuvix.Prelude hiding (some)
|
||||
import Text.Megaparsec hiding (sepBy1, sepEndBy1, some)
|
||||
import Text.Megaparsec.Char
|
||||
import Control.Monad.Trans.Class (lift)
|
||||
|
||||
@ -1,19 +1,17 @@
|
||||
module MiniJuvix.Syntax.Concrete.Lexer where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import qualified Data.Text as Text
|
||||
import GHC.Unicode
|
||||
import qualified MiniJuvix.Internal.Strings as Str
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Base hiding (Pos, space)
|
||||
import MiniJuvix.Syntax.Concrete.Parser.InfoTableBuilder
|
||||
import qualified MiniJuvix.Syntax.Concrete.Base as P
|
||||
import MiniJuvix.Syntax.Concrete.Loc
|
||||
import qualified Text.Megaparsec.Char.Lexer as L
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type OperatorSym = Text
|
||||
type ParsecS r = ParsecT Void Text (Sem r)
|
||||
|
||||
space :: forall m e. MonadParsec e Text m => m ()
|
||||
space = L.space space1 lineComment block
|
||||
@ -30,10 +28,10 @@ symbol = void . L.symbol space
|
||||
decimal :: (MonadParsec e Text m, Num n) => m n
|
||||
decimal = lexeme L.decimal
|
||||
|
||||
identifier :: MonadParsec e Text m => m Text
|
||||
identifier :: Member InfoTableBuilder r => ParsecS r Text
|
||||
identifier = fmap fst identifierL
|
||||
|
||||
identifierL :: MonadParsec e Text m => m (Text, Interval)
|
||||
identifierL :: Member InfoTableBuilder r => ParsecS r (Text, Interval)
|
||||
identifierL = lexeme bareIdentifier
|
||||
|
||||
fromPos :: P.Pos -> Pos
|
||||
@ -78,9 +76,6 @@ curLoc = do
|
||||
offset <- stateOffset <$> getParserState
|
||||
return (mkLoc offset sp)
|
||||
|
||||
withLoc :: MonadParsec e Text m => (Loc -> m a) -> m a
|
||||
withLoc ma = curLoc >>= ma
|
||||
|
||||
interval :: MonadParsec e Text m => m a -> m (a, Interval)
|
||||
interval ma = do
|
||||
start <- curLoc
|
||||
@ -88,10 +83,16 @@ interval ma = do
|
||||
end <- curLoc
|
||||
return (res, mkInterval start end)
|
||||
|
||||
keyword :: Member InfoTableBuilder r => Text -> ParsecS r ()
|
||||
keyword kw = do
|
||||
l <- snd <$> interval (symbol kw)
|
||||
lift (registerKeyword l)
|
||||
|
||||
-- | Same as @identifier@ but does not consume space after it.
|
||||
-- TODO: revise.
|
||||
bareIdentifier :: MonadParsec e Text m => m (Text, Interval)
|
||||
bareIdentifier :: Member InfoTableBuilder r => ParsecS r (Text, Interval)
|
||||
bareIdentifier = interval $ do
|
||||
-- TODO how to ignore these keywords for the InfoTableBuilder?
|
||||
notFollowedBy (choice allKeywords)
|
||||
h <- P.satisfy validFirstChar
|
||||
t <- P.takeWhileP Nothing validChar
|
||||
@ -117,13 +118,13 @@ bareIdentifier = interval $ do
|
||||
dot :: forall e m. MonadParsec e Text m => m Char
|
||||
dot = P.char '.'
|
||||
|
||||
dottedIdentifier :: forall e m. MonadParsec e Text m => m (NonEmpty (Text, Interval))
|
||||
dottedIdentifier :: Member InfoTableBuilder r => ParsecS r (NonEmpty (Text, Interval))
|
||||
dottedIdentifier = lexeme $ P.sepBy1 bareIdentifier dot
|
||||
|
||||
braces :: MonadParsec e Text m => m a -> m a
|
||||
braces = between (symbol "{") (symbol "}")
|
||||
|
||||
allKeywords :: MonadParsec e Text m => [m ()]
|
||||
allKeywords :: Member InfoTableBuilder r => [ParsecS r ()]
|
||||
allKeywords =
|
||||
[ kwAssignment,
|
||||
kwAxiom,
|
||||
@ -131,7 +132,6 @@ allKeywords =
|
||||
kwColonOmega,
|
||||
kwColonOne,
|
||||
kwColonZero,
|
||||
kwCompile,
|
||||
kwEnd,
|
||||
kwEval,
|
||||
kwForeign,
|
||||
@ -168,105 +168,102 @@ rparen = symbol ")"
|
||||
parens :: MonadParsec e Text m => m a -> m a
|
||||
parens = between lparen rparen
|
||||
|
||||
kwAssignment :: MonadParsec e Text m => m ()
|
||||
kwAssignment = symbol Str.assignUnicode <|> symbol Str.assignAscii
|
||||
kwAssignment :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii
|
||||
|
||||
kwAxiom :: MonadParsec e Text m => m ()
|
||||
kwAxiom = symbol Str.axiom
|
||||
kwAxiom :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwAxiom = keyword Str.axiom
|
||||
|
||||
-- | Note that the trailing space is needed to distinguish it from ':='.
|
||||
kwColon :: MonadParsec e Text m => m ()
|
||||
kwColon = symbol Str.colonSpace
|
||||
kwColon :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwColon = keyword Str.colonSpace
|
||||
|
||||
kwColonOmega :: MonadParsec e Text m => m ()
|
||||
kwColonOmega = symbol Str.colonOmegaUnicode <|> symbol Str.colonOmegaAscii
|
||||
kwColonOmega :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwColonOmega = keyword Str.colonOmegaUnicode <|> keyword Str.colonOmegaAscii
|
||||
|
||||
kwColonOne :: MonadParsec e Text m => m ()
|
||||
kwColonOne = symbol Str.colonOne
|
||||
kwColonOne :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwColonOne = keyword Str.colonOne
|
||||
|
||||
kwColonZero :: MonadParsec e Text m => m ()
|
||||
kwColonZero = symbol Str.colonZero
|
||||
kwColonZero :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwColonZero = keyword Str.colonZero
|
||||
|
||||
kwEnd :: MonadParsec e Text m => m ()
|
||||
kwEnd = symbol Str.end
|
||||
kwEnd :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwEnd = keyword Str.end
|
||||
|
||||
kwEval :: MonadParsec e Text m => m ()
|
||||
kwEval = symbol Str.eval
|
||||
kwEval :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwEval = keyword Str.eval
|
||||
|
||||
kwHiding :: MonadParsec e Text m => m ()
|
||||
kwHiding = symbol Str.hiding
|
||||
kwHiding :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwHiding = keyword Str.hiding
|
||||
|
||||
kwImport :: MonadParsec e Text m => m ()
|
||||
kwImport = symbol Str.import_
|
||||
kwImport :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwImport = keyword Str.import_
|
||||
|
||||
kwForeign :: MonadParsec e Text m => m ()
|
||||
kwForeign = symbol Str.foreign_
|
||||
kwForeign :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwForeign = keyword Str.foreign_
|
||||
|
||||
kwCompile :: MonadParsec e Text m => m ()
|
||||
kwCompile = symbol Str.compile
|
||||
kwIn :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwIn = keyword Str.in_
|
||||
|
||||
kwIn :: MonadParsec e Text m => m ()
|
||||
kwIn = symbol Str.in_
|
||||
kwInductive :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwInductive = keyword Str.inductive
|
||||
|
||||
kwInductive :: MonadParsec e Text m => m ()
|
||||
kwInductive = symbol Str.inductive
|
||||
kwInfix :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwInfix = keyword Str.infix_
|
||||
|
||||
kwInfix :: MonadParsec e Text m => m ()
|
||||
kwInfix = symbol Str.infix_
|
||||
kwInfixl :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwInfixl = keyword Str.infixl_
|
||||
|
||||
kwInfixl :: MonadParsec e Text m => m ()
|
||||
kwInfixl = symbol Str.infixl_
|
||||
kwInfixr :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwInfixr = keyword Str.infixr_
|
||||
|
||||
kwInfixr :: MonadParsec e Text m => m ()
|
||||
kwInfixr = symbol Str.infixr_
|
||||
kwLambda :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwLambda = keyword Str.lambdaUnicode <|> keyword Str.lambdaAscii
|
||||
|
||||
kwLambda :: MonadParsec e Text m => m ()
|
||||
kwLambda = symbol Str.lambdaUnicode <|> symbol Str.lambdaAscii
|
||||
kwLet :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwLet = keyword Str.let_
|
||||
|
||||
kwLet :: MonadParsec e Text m => m ()
|
||||
kwLet = symbol Str.let_
|
||||
kwMapsTo :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwMapsTo = keyword Str.mapstoUnicode <|> keyword Str.mapstoAscii
|
||||
|
||||
kwMapsTo :: MonadParsec e Text m => m ()
|
||||
kwMapsTo = symbol Str.mapstoUnicode <|> symbol Str.mapstoAscii
|
||||
kwMatch :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwMatch = keyword Str.match
|
||||
|
||||
kwMatch :: MonadParsec e Text m => m ()
|
||||
kwMatch = symbol Str.match
|
||||
kwModule :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwModule = keyword Str.module_
|
||||
|
||||
kwModule :: MonadParsec e Text m => m ()
|
||||
kwModule = symbol Str.module_
|
||||
kwOpen :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwOpen = keyword Str.open
|
||||
|
||||
kwOpen :: MonadParsec e Text m => m ()
|
||||
kwOpen = symbol Str.open
|
||||
kwPostfix :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwPostfix = keyword Str.postfix
|
||||
|
||||
kwPostfix :: MonadParsec e Text m => m ()
|
||||
kwPostfix = symbol Str.postfix
|
||||
kwPrint :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwPrint = keyword Str.print
|
||||
|
||||
kwPrint :: MonadParsec e Text m => m ()
|
||||
kwPrint = symbol Str.print
|
||||
kwPublic :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwPublic = keyword Str.public
|
||||
|
||||
kwPublic :: MonadParsec e Text m => m ()
|
||||
kwPublic = symbol Str.public
|
||||
kwRightArrow :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwRightArrow = keyword Str.toUnicode <|> keyword Str.toAscii
|
||||
|
||||
kwRightArrow :: MonadParsec e Text m => m ()
|
||||
kwRightArrow = symbol Str.toUnicode <|> symbol Str.toAscii
|
||||
kwSemicolon :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwSemicolon = keyword Str.semicolon
|
||||
|
||||
kwSemicolon :: MonadParsec e Text m => m ()
|
||||
kwSemicolon = symbol Str.semicolon
|
||||
kwType :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwType = keyword Str.type_
|
||||
|
||||
kwType :: MonadParsec e Text m => m ()
|
||||
kwType = symbol Str.type_
|
||||
kwUsing :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwUsing = keyword Str.using
|
||||
|
||||
kwUsing :: MonadParsec e Text m => m ()
|
||||
kwUsing = symbol Str.using
|
||||
kwWhere :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwWhere = keyword Str.where_
|
||||
|
||||
kwWhere :: MonadParsec e Text m => m ()
|
||||
kwWhere = symbol Str.where_
|
||||
kwWildcard :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwWildcard = keyword Str.underscore
|
||||
|
||||
kwWildcard :: MonadParsec e Text m => m ()
|
||||
kwWildcard = symbol Str.underscore
|
||||
ghc :: Member InfoTableBuilder r => ParsecS r ()
|
||||
ghc = keyword Str.ghc
|
||||
|
||||
ghc :: MonadParsec e Text m => m ()
|
||||
ghc = symbol Str.ghc
|
||||
|
||||
agda :: MonadParsec e Text m => m ()
|
||||
agda = symbol Str.agda
|
||||
agda :: Member InfoTableBuilder r => ParsecS r ()
|
||||
agda = keyword Str.agda
|
||||
|
||||
@ -1,7 +1,5 @@
|
||||
module MiniJuvix.Syntax.Concrete.Parser where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import qualified Data.List.NonEmpty.Extra as NonEmpty
|
||||
import Data.Singletons
|
||||
import qualified Data.Text as Text
|
||||
@ -10,46 +8,48 @@ import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Base (MonadParsec)
|
||||
import qualified MiniJuvix.Syntax.Concrete.Base as P
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Parser.InfoTableBuilder
|
||||
import MiniJuvix.Syntax.Concrete.Lexer hiding (symbol)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Running the parser
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
debugModuleParser :: FilePath -> IO ()
|
||||
debugModuleParser fileName = do
|
||||
r <- runModuleParserIO fileName
|
||||
case r of
|
||||
Left err -> error err
|
||||
Right m -> print m
|
||||
|
||||
runModuleParserIO :: FilePath -> IO (Either Text (Module 'Parsed 'ModuleTop))
|
||||
runModuleParserIO fileName = do
|
||||
runModuleParserIO fileName =
|
||||
fmap (fmap snd) (runModuleParserIO' fileName)
|
||||
|
||||
runModuleParserIO' :: FilePath -> IO (Either Text (InfoTable, Module 'Parsed 'ModuleTop))
|
||||
runModuleParserIO' fileName = do
|
||||
input <- Text.readFile fileName
|
||||
return (runModuleParser fileName input)
|
||||
return (runModuleParser' fileName input)
|
||||
|
||||
|
||||
runModuleParser :: FilePath -> Text -> Either Text (Module 'Parsed 'ModuleTop)
|
||||
runModuleParser fileName input = fmap snd (runModuleParser' fileName input)
|
||||
|
||||
-- | The 'FilePath' is only used for reporting errors. It is safe to pass
|
||||
-- an empty string.
|
||||
runModuleParser :: FilePath -> Text -> Either Text (Module 'Parsed 'ModuleTop)
|
||||
runModuleParser fileName input =
|
||||
case P.runParser topModuleDef fileName input of
|
||||
Left err -> Left $ Text.pack (P.errorBundlePretty err)
|
||||
Right r -> return r
|
||||
runModuleParser' :: FilePath -> Text -> Either Text (InfoTable, Module 'Parsed 'ModuleTop)
|
||||
runModuleParser' fileName input =
|
||||
case run $ runInfoTableBuilder $ P.runParserT topModuleDef fileName input of
|
||||
(_, Left err) -> Left (Text.pack (P.errorBundlePretty err))
|
||||
(tbl, Right r) -> return (tbl, r)
|
||||
|
||||
topModuleDef :: MonadParsec Void Text m => m (Module 'Parsed 'ModuleTop)
|
||||
topModuleDef :: Member InfoTableBuilder r => ParsecS r (Module 'Parsed 'ModuleTop)
|
||||
topModuleDef = space >> moduleDef <* (optional kwSemicolon >> P.eof)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Symbols and names
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
symbol :: MonadParsec e Text m => m Symbol
|
||||
symbol :: Member InfoTableBuilder r => ParsecS r Symbol
|
||||
symbol = uncurry Symbol <$> identifierL
|
||||
|
||||
dottedSymbol :: forall e m. MonadParsec e Text m => m (NonEmpty Symbol)
|
||||
dottedSymbol :: Member InfoTableBuilder r => ParsecS r (NonEmpty Symbol)
|
||||
dottedSymbol = fmap (uncurry Symbol) <$> dottedIdentifier
|
||||
|
||||
name :: forall e m. MonadParsec e Text m => m Name
|
||||
name :: Member InfoTableBuilder r => ParsecS r Name
|
||||
name = do
|
||||
parts <- dottedSymbol
|
||||
return $ case nonEmptyUnsnoc parts of
|
||||
@ -59,17 +59,17 @@ name = do
|
||||
mkTopModulePath :: NonEmpty Symbol -> TopModulePath
|
||||
mkTopModulePath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
|
||||
|
||||
symbolList :: MonadParsec e Text m => m (NonEmpty Symbol)
|
||||
symbolList :: Member InfoTableBuilder r => ParsecS r (NonEmpty Symbol)
|
||||
symbolList = braces (P.sepBy1 symbol kwSemicolon)
|
||||
|
||||
topModulePath :: MonadParsec e Text m => m TopModulePath
|
||||
topModulePath :: Member InfoTableBuilder r => ParsecS r TopModulePath
|
||||
topModulePath = mkTopModulePath <$> dottedSymbol
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Top level statement
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
statement :: forall e m. MonadParsec e Text m => m (Statement 'Parsed)
|
||||
statement :: Member InfoTableBuilder r => ParsecS r (Statement 'Parsed)
|
||||
statement =
|
||||
(StatementOperator <$> operatorSyntaxDef)
|
||||
<|> (StatementOpenModule <$> openModule)
|
||||
@ -88,11 +88,11 @@ statement =
|
||||
-- Foreign
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
backend :: forall e m. MonadParsec e Text m => m Backend
|
||||
backend :: Member InfoTableBuilder r => ParsecS r Backend
|
||||
backend = ghc $> BackendGhc
|
||||
<|> agda $> BackendAgda
|
||||
|
||||
foreignBlock :: forall e m. MonadParsec e Text m => m ForeignBlock
|
||||
foreignBlock :: Member InfoTableBuilder r => ParsecS r ForeignBlock
|
||||
foreignBlock = do
|
||||
kwForeign
|
||||
_foreignBackend <- backend
|
||||
@ -106,7 +106,7 @@ foreignBlock = do
|
||||
precedence :: MonadParsec e Text m => m Precedence
|
||||
precedence = PrecNat <$> decimal
|
||||
|
||||
operatorSyntaxDef :: forall e m. MonadParsec e Text m => m OperatorSyntaxDef
|
||||
operatorSyntaxDef :: forall r. Member InfoTableBuilder r => ParsecS r OperatorSyntaxDef
|
||||
operatorSyntaxDef = do
|
||||
fixityArity <- arity
|
||||
fixityPrecedence <- precedence
|
||||
@ -114,7 +114,7 @@ operatorSyntaxDef = do
|
||||
let opFixity = Fixity {..}
|
||||
return OperatorSyntaxDef {..}
|
||||
where
|
||||
arity :: m OperatorArity
|
||||
arity :: ParsecS r OperatorArity
|
||||
arity =
|
||||
do
|
||||
Binary AssocRight <$ kwInfixr
|
||||
@ -126,7 +126,7 @@ operatorSyntaxDef = do
|
||||
-- Import statement
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import_ :: MonadParsec e Text m => m (Import 'Parsed)
|
||||
import_ :: Member InfoTableBuilder r => ParsecS r (Import 'Parsed)
|
||||
import_ = do
|
||||
kwImport
|
||||
importModule <- topModulePath
|
||||
@ -136,7 +136,7 @@ import_ = do
|
||||
-- Expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
expressionAtom :: MonadParsec e Text m => m (ExpressionAtom 'Parsed)
|
||||
expressionAtom :: Member InfoTableBuilder r => ParsecS r (ExpressionAtom 'Parsed)
|
||||
expressionAtom =
|
||||
do
|
||||
AtomLiteral <$> P.try literal
|
||||
@ -149,7 +149,7 @@ expressionAtom =
|
||||
<|> (AtomFunArrow <$ kwRightArrow)
|
||||
<|> parens (AtomParens <$> expressionAtoms)
|
||||
|
||||
expressionAtoms :: MonadParsec e Text m => m (ExpressionAtoms 'Parsed)
|
||||
expressionAtoms :: Member InfoTableBuilder r => ParsecS r (ExpressionAtoms 'Parsed)
|
||||
expressionAtoms = ExpressionAtoms <$> P.some expressionAtom
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -166,21 +166,24 @@ literalString = do
|
||||
(x, loc) <- interval string
|
||||
return (LiteralLoc (LitString x) loc)
|
||||
|
||||
literal :: MonadParsec e Text m => m LiteralLoc
|
||||
literal = literalInteger <|> literalString
|
||||
literal :: Member InfoTableBuilder r => ParsecS r LiteralLoc
|
||||
literal = do
|
||||
l <- literalInteger
|
||||
<|> literalString
|
||||
P.lift (registerLiteral l)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Match expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
matchAlt :: MonadParsec e Text m => m (MatchAlt 'Parsed)
|
||||
matchAlt :: Member InfoTableBuilder r => ParsecS r (MatchAlt 'Parsed)
|
||||
matchAlt = do
|
||||
matchAltPattern <- patternAtom
|
||||
kwMapsTo
|
||||
matchAltBody <- expressionAtoms
|
||||
return MatchAlt {..}
|
||||
|
||||
match :: MonadParsec e Text m => m (Match 'Parsed)
|
||||
match :: Member InfoTableBuilder r => ParsecS r (Match 'Parsed)
|
||||
match = do
|
||||
kwMatch
|
||||
matchExpression <- expressionAtoms
|
||||
@ -191,11 +194,11 @@ match = do
|
||||
-- Let expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
letClause :: MonadParsec e Text m => m (LetClause 'Parsed)
|
||||
letClause :: Member InfoTableBuilder r => ParsecS r (LetClause 'Parsed)
|
||||
letClause = do
|
||||
either LetTypeSig LetFunClause <$> auxTypeSigFunClause
|
||||
|
||||
letBlock :: MonadParsec e Text m => m (LetBlock 'Parsed)
|
||||
letBlock :: Member InfoTableBuilder r => ParsecS r (LetBlock 'Parsed)
|
||||
letBlock = do
|
||||
kwLet
|
||||
letClauses <- braces (P.sepEndBy letClause kwSemicolon)
|
||||
@ -207,7 +210,7 @@ letBlock = do
|
||||
-- Universe expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
universe :: MonadParsec e Text m => m Universe
|
||||
universe :: Member InfoTableBuilder r => ParsecS r Universe
|
||||
universe = do
|
||||
kwType
|
||||
Universe <$> optional decimal
|
||||
@ -216,11 +219,7 @@ universe = do
|
||||
-- Type signature declaration
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
typeSignature ::
|
||||
forall e m.
|
||||
MonadParsec e Text m =>
|
||||
Symbol ->
|
||||
m (TypeSignature 'Parsed)
|
||||
typeSignature :: Member InfoTableBuilder r => Symbol -> ParsecS r (TypeSignature 'Parsed)
|
||||
typeSignature _sigName = do
|
||||
kwColon
|
||||
_sigType <- expressionAtoms
|
||||
@ -231,10 +230,8 @@ typeSignature _sigName = do
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
-- | Used to minimize the amount of required @P.try@s.
|
||||
auxTypeSigFunClause ::
|
||||
forall e m.
|
||||
MonadParsec e Text m =>
|
||||
m (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed))
|
||||
auxTypeSigFunClause :: Member InfoTableBuilder r =>
|
||||
ParsecS r (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed))
|
||||
auxTypeSigFunClause = do
|
||||
s <- symbol
|
||||
(Left <$> typeSignature s)
|
||||
@ -244,7 +241,7 @@ auxTypeSigFunClause = do
|
||||
-- Axioms
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
axiomDef :: forall e m. MonadParsec e Text m => m (AxiomDef 'Parsed)
|
||||
axiomDef :: Member InfoTableBuilder r => ParsecS r (AxiomDef 'Parsed)
|
||||
axiomDef = do
|
||||
kwAxiom
|
||||
_axiomName <- symbol
|
||||
@ -264,10 +261,7 @@ axiomDef = do
|
||||
-- Function expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
functionParam ::
|
||||
forall e m.
|
||||
MonadParsec e Text m =>
|
||||
m (FunctionParameter 'Parsed)
|
||||
functionParam :: forall r. Member InfoTableBuilder r => ParsecS r (FunctionParameter 'Parsed)
|
||||
functionParam = do
|
||||
(paramName, paramUsage) <- P.try $ do
|
||||
lparen
|
||||
@ -278,18 +272,18 @@ functionParam = do
|
||||
rparen
|
||||
return $ FunctionParameter {..}
|
||||
where
|
||||
pName :: m (Maybe Symbol)
|
||||
pName :: ParsecS r (Maybe Symbol)
|
||||
pName =
|
||||
(Just <$> symbol)
|
||||
<|> (Nothing <$ kwWildcard)
|
||||
pUsage :: m (Maybe Usage)
|
||||
pUsage :: ParsecS r (Maybe Usage)
|
||||
pUsage =
|
||||
(Just UsageNone <$ kwColonZero)
|
||||
<|> (Just UsageOnce <$ kwColonOne)
|
||||
<|> (Just UsageOmega <$ kwColonOmega)
|
||||
<|> (Nothing <$ kwColon)
|
||||
|
||||
function :: MonadParsec e Text m => m (Function 'Parsed)
|
||||
function :: Member InfoTableBuilder r => ParsecS r (Function 'Parsed)
|
||||
function = do
|
||||
funParameter <- functionParam
|
||||
kwRightArrow
|
||||
@ -300,31 +294,31 @@ function = do
|
||||
-- Where block clauses
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
whereBlock :: MonadParsec e Text m => m (WhereBlock 'Parsed)
|
||||
whereBlock :: Member InfoTableBuilder r => ParsecS r (WhereBlock 'Parsed)
|
||||
whereBlock = do
|
||||
kwWhere
|
||||
WhereBlock <$> braces (P.sepEndBy1 whereClause kwSemicolon)
|
||||
|
||||
whereClause :: forall e m. MonadParsec e Text m => m (WhereClause 'Parsed)
|
||||
whereClause :: forall r. Member InfoTableBuilder r => ParsecS r (WhereClause 'Parsed)
|
||||
whereClause =
|
||||
(WhereOpenModule <$> openModule)
|
||||
<|> sigOrFun
|
||||
where
|
||||
sigOrFun :: m (WhereClause 'Parsed)
|
||||
sigOrFun :: ParsecS r (WhereClause 'Parsed)
|
||||
sigOrFun = either WhereTypeSig WhereFunClause <$> auxTypeSigFunClause
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Lambda expression
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
lambdaClause :: MonadParsec e Text m => m (LambdaClause 'Parsed)
|
||||
lambdaClause :: Member InfoTableBuilder r => ParsecS r (LambdaClause 'Parsed)
|
||||
lambdaClause = do
|
||||
lambdaParameters <- P.some patternAtom
|
||||
kwMapsTo
|
||||
lambdaBody <- expressionAtoms
|
||||
return LambdaClause {..}
|
||||
|
||||
lambda :: MonadParsec e Text m => m (Lambda 'Parsed)
|
||||
lambda :: Member InfoTableBuilder r => ParsecS r (Lambda 'Parsed)
|
||||
lambda = do
|
||||
kwLambda
|
||||
lambdaClauses <- braces (P.sepEndBy lambdaClause kwSemicolon)
|
||||
@ -334,7 +328,7 @@ lambda = do
|
||||
-- Data type construction declaration
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
inductiveDef :: MonadParsec e Text m => m (InductiveDef 'Parsed)
|
||||
inductiveDef :: Member InfoTableBuilder r => ParsecS r (InductiveDef 'Parsed)
|
||||
inductiveDef = do
|
||||
kwInductive
|
||||
_inductiveName <- symbol
|
||||
@ -343,14 +337,14 @@ inductiveDef = do
|
||||
_inductiveConstructors <- braces $ P.sepEndBy constructorDef kwSemicolon
|
||||
return InductiveDef {..}
|
||||
|
||||
inductiveParam :: MonadParsec e Text m => m (InductiveParameter 'Parsed)
|
||||
inductiveParam :: Member InfoTableBuilder r => ParsecS r (InductiveParameter 'Parsed)
|
||||
inductiveParam = parens $ do
|
||||
_inductiveParameterName <- symbol
|
||||
kwColon
|
||||
_inductiveParameterType <- expressionAtoms
|
||||
return InductiveParameter {..}
|
||||
|
||||
constructorDef :: MonadParsec e Text m => m (InductiveConstructorDef 'Parsed)
|
||||
constructorDef :: Member InfoTableBuilder r => ParsecS r (InductiveConstructorDef 'Parsed)
|
||||
constructorDef = do
|
||||
_constructorName <- symbol
|
||||
kwColon
|
||||
@ -361,27 +355,20 @@ constructorDef = do
|
||||
-- Pattern section
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
patternAtom :: forall e m. MonadParsec e Text m => m (PatternAtom 'Parsed)
|
||||
patternAtom :: Member InfoTableBuilder r => ParsecS r (PatternAtom 'Parsed)
|
||||
patternAtom =
|
||||
PatternAtomIden <$> name
|
||||
<|> PatternAtomWildcard <$ kwWildcard
|
||||
<|> (PatternAtomParens <$> parens patternAtoms)
|
||||
|
||||
patternAtoms ::
|
||||
forall e m.
|
||||
MonadParsec e Text m =>
|
||||
m (PatternAtoms 'Parsed)
|
||||
patternAtoms :: Member InfoTableBuilder r => ParsecS r (PatternAtoms 'Parsed)
|
||||
patternAtoms = PatternAtoms <$> P.some patternAtom
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Function binding declaration
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
functionClause ::
|
||||
forall e m.
|
||||
MonadParsec e Text m =>
|
||||
Symbol ->
|
||||
m (FunctionClause 'Parsed)
|
||||
functionClause :: Member InfoTableBuilder r => Symbol -> ParsecS r (FunctionClause 'Parsed)
|
||||
functionClause _clauseOwnerFunction = do
|
||||
_clausePatterns <- P.many patternAtom
|
||||
kwAssignment
|
||||
@ -393,15 +380,12 @@ functionClause _clauseOwnerFunction = do
|
||||
-- Module declaration
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
pmodulePath ::
|
||||
forall t e m.
|
||||
(SingI t, MonadParsec e Text m) =>
|
||||
m (ModulePathType 'Parsed t)
|
||||
pmodulePath :: forall t r. (SingI t, Member InfoTableBuilder r) => ParsecS r (ModulePathType 'Parsed t)
|
||||
pmodulePath = case sing :: SModuleIsTop t of
|
||||
SModuleTop -> topModulePath
|
||||
SModuleLocal -> symbol
|
||||
|
||||
moduleDef :: (SingI t, MonadParsec e Text m) => m (Module 'Parsed t)
|
||||
moduleDef :: (SingI t, Member InfoTableBuilder r) => ParsecS r (Module 'Parsed t)
|
||||
moduleDef = do
|
||||
kwModule
|
||||
_modulePath <- pmodulePath
|
||||
@ -412,7 +396,7 @@ moduleDef = do
|
||||
return Module {..}
|
||||
|
||||
-- | An ExpressionAtom which is a valid expression on its own.
|
||||
atomicExpression :: forall e m. MonadParsec e Text m => m (ExpressionType 'Parsed)
|
||||
atomicExpression :: Member InfoTableBuilder r => ParsecS r (ExpressionType 'Parsed)
|
||||
atomicExpression = do
|
||||
atom <- expressionAtom
|
||||
case atom of
|
||||
@ -420,7 +404,7 @@ atomicExpression = do
|
||||
_ -> return ()
|
||||
return $ ExpressionAtoms (NonEmpty.singleton atom)
|
||||
|
||||
openModule :: forall e m. MonadParsec e Text m => m (OpenModule 'Parsed)
|
||||
openModule :: forall r. Member InfoTableBuilder r => ParsecS r (OpenModule 'Parsed)
|
||||
openModule = do
|
||||
kwOpen
|
||||
_openModuleName <- name
|
||||
@ -429,7 +413,7 @@ openModule = do
|
||||
_openPublic <- maybe NoPublic (const Public) <$> optional kwPublic
|
||||
return OpenModule {..}
|
||||
where
|
||||
usingOrHiding :: m UsingHiding
|
||||
usingOrHiding :: ParsecS r UsingHiding
|
||||
usingOrHiding =
|
||||
(kwUsing >> (Using <$> symbolList))
|
||||
<|> (kwHiding >> (Hiding <$> symbolList))
|
||||
@ -438,12 +422,12 @@ openModule = do
|
||||
-- Debugging statements
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
eval :: MonadParsec e Text m => m (Eval 'Parsed)
|
||||
eval :: Member InfoTableBuilder r => ParsecS r (Eval 'Parsed)
|
||||
eval = do
|
||||
kwEval
|
||||
Eval <$> expressionAtoms
|
||||
|
||||
printS :: MonadParsec e Text m => m (Print 'Parsed)
|
||||
printS :: Member InfoTableBuilder r => ParsecS r (Print 'Parsed)
|
||||
printS = do
|
||||
kwPrint
|
||||
Print <$> expressionAtoms
|
||||
|
||||
11
src/MiniJuvix/Syntax/Concrete/Parser/InfoTable.hs
Normal file
11
src/MiniJuvix/Syntax/Concrete/Parser/InfoTable.hs
Normal file
@ -0,0 +1,11 @@
|
||||
module MiniJuvix.Syntax.Concrete.Parser.InfoTable where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Parser.ParsedItem
|
||||
|
||||
newtype InfoTable = InfoTable {
|
||||
_infoParsedItems :: [ParsedItem]
|
||||
}
|
||||
deriving newtype (Semigroup, Monoid)
|
||||
|
||||
makeLenses ''InfoTable
|
||||
75
src/MiniJuvix/Syntax/Concrete/Parser/InfoTableBuilder.hs
Normal file
75
src/MiniJuvix/Syntax/Concrete/Parser/InfoTableBuilder.hs
Normal file
@ -0,0 +1,75 @@
|
||||
module MiniJuvix.Syntax.Concrete.Parser.InfoTableBuilder (
|
||||
InfoTableBuilder,
|
||||
registerLiteral,
|
||||
registerKeyword,
|
||||
ignoring,
|
||||
mergeTable,
|
||||
runInfoTableBuilder,
|
||||
module MiniJuvix.Syntax.Concrete.Parser.InfoTable,
|
||||
) where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Parser.ParsedItem
|
||||
import MiniJuvix.Syntax.Concrete.Parser.InfoTable
|
||||
import MiniJuvix.Syntax.Concrete.Literal
|
||||
import MiniJuvix.Syntax.Concrete.Loc
|
||||
import MiniJuvix.Syntax.Concrete.Language (LiteralLoc(..))
|
||||
|
||||
data InfoTableBuilder m a where
|
||||
RegisterItem :: ParsedItem -> InfoTableBuilder m ()
|
||||
Ignoring :: m a -> InfoTableBuilder m a
|
||||
MergeTable :: InfoTable -> InfoTableBuilder m ()
|
||||
|
||||
makeSem ''InfoTableBuilder
|
||||
|
||||
registerKeyword :: Member (InfoTableBuilder) r => Interval -> Sem r ()
|
||||
registerKeyword i = registerItem ParsedItem {
|
||||
_parsedLoc = i,
|
||||
_parsedTag = ParsedTagKeyword
|
||||
}
|
||||
|
||||
registerLiteral :: Member (InfoTableBuilder) r => LiteralLoc -> Sem r LiteralLoc
|
||||
registerLiteral l =
|
||||
l <$ registerItem ParsedItem {
|
||||
_parsedLoc = loc,
|
||||
_parsedTag = tag
|
||||
}
|
||||
where
|
||||
tag = case _literalLocLiteral l of
|
||||
LitString {} -> ParsedTagLiteralString
|
||||
LitInteger {} -> ParsedTagLiteralInt
|
||||
loc = getLoc l
|
||||
|
||||
data BuilderState = BuilderState {
|
||||
_stateIgnoring :: Bool,
|
||||
_stateItems :: [ParsedItem]
|
||||
}
|
||||
deriving stock (Show)
|
||||
makeLenses ''BuilderState
|
||||
|
||||
iniState :: BuilderState
|
||||
iniState = BuilderState {
|
||||
_stateIgnoring = False,
|
||||
_stateItems = []
|
||||
}
|
||||
|
||||
build :: BuilderState -> InfoTable
|
||||
build st = InfoTable (st ^. stateItems)
|
||||
|
||||
runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
|
||||
runInfoTableBuilder = fmap (first build) . runState iniState . reinterpretH
|
||||
(\case
|
||||
RegisterItem i -> do
|
||||
unlessM (gets (^. stateIgnoring))
|
||||
(modify' (over stateItems (i :)))
|
||||
pureT ()
|
||||
Ignoring m -> do
|
||||
s0 <- gets (^. stateIgnoring)
|
||||
modify (set stateIgnoring True)
|
||||
r <- runTSimple m
|
||||
modify (over stateIgnoring (const s0))
|
||||
return r
|
||||
MergeTable tbl -> do
|
||||
modify' (over stateItems ((tbl ^. infoParsedItems) <>))
|
||||
pureT ()
|
||||
)
|
||||
21
src/MiniJuvix/Syntax/Concrete/Parser/ParsedItem.hs
Normal file
21
src/MiniJuvix/Syntax/Concrete/Parser/ParsedItem.hs
Normal file
@ -0,0 +1,21 @@
|
||||
module MiniJuvix.Syntax.Concrete.Parser.ParsedItem where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Loc
|
||||
|
||||
data ParsedItem = ParsedItem {
|
||||
_parsedLoc :: Interval,
|
||||
_parsedTag :: ParsedItemTag
|
||||
}
|
||||
deriving stock (Show)
|
||||
|
||||
instance HasLoc ParsedItem where
|
||||
getLoc = _parsedLoc
|
||||
|
||||
data ParsedItemTag =
|
||||
ParsedTagKeyword
|
||||
| ParsedTagLiteralInt
|
||||
| ParsedTagLiteralString
|
||||
deriving stock (Show)
|
||||
|
||||
makeLenses ''ParsedItem
|
||||
@ -2,6 +2,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Highlight where
|
||||
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name
|
||||
import MiniJuvix.Syntax.Concrete.Loc
|
||||
import MiniJuvix.Syntax.Concrete.Parser.ParsedItem
|
||||
import qualified MiniJuvix.Internal.Strings as Str
|
||||
import MiniJuvix.Prelude
|
||||
import Prettyprinter
|
||||
@ -13,6 +14,9 @@ data Face =
|
||||
| FaceFunction
|
||||
| FaceModule
|
||||
| FaceAxiom
|
||||
| FaceKeyword
|
||||
| FaceString
|
||||
| FaceNumber
|
||||
|
||||
data Property =
|
||||
PropertyFace Face
|
||||
@ -31,8 +35,11 @@ data SExp =
|
||||
|
||||
makeLenses ''Instruction
|
||||
|
||||
go :: [Name] -> Text
|
||||
go = renderSExp . progn . mapMaybe goName
|
||||
go :: [ParsedItem] -> [Name] -> Text
|
||||
go items names =
|
||||
renderSExp (progn (map goParsedItem items
|
||||
<> mapMaybe goName names
|
||||
))
|
||||
|
||||
progn :: [SExp] -> SExp
|
||||
progn l = List (Symbol "progn" : l)
|
||||
@ -57,14 +64,27 @@ instr i f =
|
||||
pos l = Int (succ (l ^. locOffset . unPos))
|
||||
start = pos (i ^. intStart)
|
||||
end = pos (i ^. intEnd)
|
||||
face = Quote (List [Symbol "face", faceSymbol ])
|
||||
faceSymbol = Symbol ("minijuvix-highlight-" <> faceSymbolStr <> "-face")
|
||||
face = Quote (List [Symbol "face", faceSymbol faceSymbolStr])
|
||||
faceSymbolStr = case f of
|
||||
FaceAxiom -> Str.axiom
|
||||
FaceInductive -> Str.inductive
|
||||
FaceConstructor -> Str.constructor
|
||||
FaceModule -> Str.module_
|
||||
FaceKeyword -> Str.keyword
|
||||
FaceFunction -> Str.function
|
||||
FaceNumber -> Str.number
|
||||
FaceString -> Str.string
|
||||
|
||||
faceSymbol :: Text -> SExp
|
||||
faceSymbol faceSymbolStr = Symbol ("minijuvix-highlight-" <> faceSymbolStr <> "-face")
|
||||
|
||||
goParsedItem :: ParsedItem -> SExp
|
||||
goParsedItem i = instr (getLoc i) face
|
||||
where
|
||||
face = case i ^. parsedTag of
|
||||
ParsedTagKeyword -> FaceKeyword
|
||||
ParsedTagLiteralInt -> FaceNumber
|
||||
ParsedTagLiteralString -> FaceString
|
||||
|
||||
goName :: Name -> Maybe SExp
|
||||
goName n = do
|
||||
|
||||
@ -5,7 +5,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base
|
||||
where
|
||||
|
||||
import qualified Data.List.NonEmpty.Extra as NonEmpty
|
||||
import MiniJuvix.Internal.Strings as Str
|
||||
import qualified MiniJuvix.Internal.Strings as Str
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name (AbsModulePath)
|
||||
|
||||
@ -1,7 +1,10 @@
|
||||
-- | Limitations:
|
||||
-- 1. A symbol introduced by a type signature can only be used once per Module.
|
||||
--
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scoper where
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scoper (
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scoper,
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scoper.ScoperResult,
|
||||
) where
|
||||
|
||||
import qualified Control.Monad.Combinators.Expr as P
|
||||
import Data.Functor.Identity
|
||||
@ -13,55 +16,63 @@ import Lens.Micro.Platform
|
||||
import MiniJuvix.Prelude
|
||||
import qualified MiniJuvix.Syntax.Concrete.Base as P
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Parser (runModuleParser)
|
||||
import MiniJuvix.Syntax.Concrete.Parser (runModuleParser')
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Error
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
|
||||
import qualified MiniJuvix.Syntax.Concrete.Name as N
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scope
|
||||
import qualified MiniJuvix.Syntax.Concrete.Parser.InfoTableBuilder as Parser
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scoper.Files
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scoper.ScoperResult
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
scopeCheck1IO :: FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError (InfoTable, Module 'Scoped 'ModuleTop))
|
||||
scopeCheck1IO :: FilePath -> Module 'Parsed 'ModuleTop -> IO (Either ScopeError ScoperResult)
|
||||
scopeCheck1IO root = runFinal . embedToFinal @IO . runFilesIO . fixpointToFinal @IO . scopeCheck1 root
|
||||
|
||||
scopeCheck1Pure :: HashMap FilePath Text -> FilePath -> Module 'Parsed 'ModuleTop -> Either ScopeError (InfoTable, Module 'Scoped 'ModuleTop)
|
||||
scopeCheck1Pure :: HashMap FilePath Text -> FilePath -> Module 'Parsed 'ModuleTop -> Either ScopeError ScoperResult
|
||||
scopeCheck1Pure fs root = runIdentity . runFinal . runFilesPure fs . fixpointToFinal @Identity . scopeCheck1 root
|
||||
|
||||
scopeCheck1 ::
|
||||
Members [Files, Fixpoint] r =>
|
||||
FilePath ->
|
||||
Module 'Parsed 'ModuleTop ->
|
||||
Sem r (Either ScopeError (InfoTable, Module 'Scoped 'ModuleTop))
|
||||
scopeCheck1 root m = fmap (second head) <$> scopeCheck root (pure m)
|
||||
Sem r (Either ScopeError ScoperResult)
|
||||
scopeCheck1 root m = scopeCheck root (pure m)
|
||||
|
||||
scopeCheck ::
|
||||
Members [Files, Fixpoint] r =>
|
||||
FilePath ->
|
||||
NonEmpty (Module 'Parsed 'ModuleTop) ->
|
||||
Sem r (Either ScopeError (InfoTable, NonEmpty (Module 'Scoped 'ModuleTop)))
|
||||
Sem r (Either ScopeError ScoperResult)
|
||||
scopeCheck root modules =
|
||||
runError $
|
||||
fmap mkResult $
|
||||
Parser.runInfoTableBuilder $
|
||||
runInfoTableBuilder $
|
||||
runReader scopeParameters $
|
||||
evalState iniScoperState $
|
||||
mapM checkTopModule_ modules
|
||||
where
|
||||
iniScoperState :: ScoperState
|
||||
iniScoperState =
|
||||
ScoperState
|
||||
{ _scoperModulesCache = ModulesCache mempty,
|
||||
_scoperFreeNames = S.allNameIds,
|
||||
_scoperModules = mempty
|
||||
}
|
||||
scopeParameters :: ScopeParameters
|
||||
scopeParameters =
|
||||
ScopeParameters
|
||||
{ _scopeRootPath = root,
|
||||
_scopeFileExtension = ".mjuvix",
|
||||
_scopeTopParents = mempty
|
||||
}
|
||||
mkResult :: (Parser.InfoTable, (InfoTable, NonEmpty (Module 'Scoped 'ModuleTop))) -> ScoperResult
|
||||
mkResult (pt, (st, ms)) = ScoperResult {
|
||||
_resultParserTable = pt,
|
||||
_resultScoperTable = st,
|
||||
_resultModules = ms
|
||||
}
|
||||
iniScoperState :: ScoperState
|
||||
iniScoperState =
|
||||
ScoperState
|
||||
{ _scoperModulesCache = ModulesCache mempty,
|
||||
_scoperFreeNames = S.allNameIds,
|
||||
_scoperModules = mempty
|
||||
}
|
||||
scopeParameters :: ScopeParameters
|
||||
scopeParameters =
|
||||
ScopeParameters
|
||||
{ _scopeRootPath = root,
|
||||
_scopeFileExtension = ".mjuvix",
|
||||
_scopeTopParents = mempty
|
||||
}
|
||||
|
||||
freshNameId ::
|
||||
Members '[State ScoperState] r =>
|
||||
@ -198,7 +209,7 @@ bindLocalModuleSymbol _moduleExportInfo _moduleRefModule =
|
||||
|
||||
checkImport ::
|
||||
forall r.
|
||||
Members '[Error ScopeError, State Scope, Reader ScopeParameters, Files, State ScoperState, Fixpoint, InfoTableBuilder] r =>
|
||||
Members '[Error ScopeError, State Scope, Reader ScopeParameters, Files, State ScoperState, Fixpoint, InfoTableBuilder, Parser.InfoTableBuilder] r =>
|
||||
Import 'Parsed ->
|
||||
Sem r (Import 'Scoped)
|
||||
checkImport import_@(Import path) = do
|
||||
@ -362,15 +373,15 @@ exportScope Scope {..} = do
|
||||
)
|
||||
|
||||
readParseModule ::
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files] r =>
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, Parser.InfoTableBuilder] r =>
|
||||
TopModulePath ->
|
||||
Sem r (Module 'Parsed 'ModuleTop)
|
||||
readParseModule mp = do
|
||||
path <- modulePathToFilePath mp
|
||||
txt <- readFile' path
|
||||
case runModuleParser path txt of
|
||||
case runModuleParser' path txt of
|
||||
Left err -> throw (ErrParser (MegaParsecError err))
|
||||
Right r -> return r
|
||||
Right (t, r) -> Parser.mergeTable t $> r
|
||||
|
||||
modulePathToFilePath ::
|
||||
Members '[Reader ScopeParameters] r =>
|
||||
@ -463,14 +474,14 @@ checkInductiveDef InductiveDef {..} = do
|
||||
|
||||
checkTopModule_ ::
|
||||
forall r.
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint , InfoTableBuilder] r =>
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint , InfoTableBuilder, Parser.InfoTableBuilder] r =>
|
||||
Module 'Parsed 'ModuleTop ->
|
||||
Sem r (Module 'Scoped 'ModuleTop)
|
||||
checkTopModule_ = fmap (^. moduleRefModule) . checkTopModule
|
||||
|
||||
checkTopModule ::
|
||||
forall r.
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint , InfoTableBuilder ] r =>
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, State ScoperState, Fixpoint , InfoTableBuilder, Parser.InfoTableBuilder] r =>
|
||||
Module 'Parsed 'ModuleTop ->
|
||||
Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
|
||||
checkTopModule m@(Module path params body) = do
|
||||
@ -479,54 +490,54 @@ checkTopModule m@(Module path params body) = do
|
||||
modify (over (scoperModulesCache . cachedModules) (HashMap.insert path r))
|
||||
return r
|
||||
where
|
||||
checkPath :: Members '[Files, Reader ScopeParameters, Error ScopeError] s => Sem s ()
|
||||
checkPath = do
|
||||
expectedPath <- modulePathToFilePath path
|
||||
let actualPath = getLoc path ^. intFile
|
||||
unlessM (fromMaybe True <$> equalPaths' expectedPath actualPath) $
|
||||
throw
|
||||
( ErrWrongTopModuleName
|
||||
WrongTopModuleName
|
||||
{ _wrongTopModuleNameActualName = path,
|
||||
_wrongTopModuleNameExpectedPath = expectedPath,
|
||||
_wrongTopModuleNameActualPath = actualPath
|
||||
}
|
||||
)
|
||||
freshTopModulePath ::
|
||||
forall s.
|
||||
Members '[State ScoperState] s =>
|
||||
Sem s S.TopModulePath
|
||||
freshTopModulePath = do
|
||||
_nameId <- freshNameId
|
||||
let _nameDefinedIn = S.topModulePathToAbsPath path
|
||||
_nameConcrete = path
|
||||
_nameDefined = getLoc (_modulePathName path)
|
||||
_nameKind = S.KNameTopModule
|
||||
_nameFixity = Nothing
|
||||
-- This visibility annotation is not relevant
|
||||
_nameVisibilityAnn = VisPublic
|
||||
_nameWhyInScope = S.BecauseDefined
|
||||
_nameVerbatim = N.topModulePathToDottedPath path
|
||||
moduleName = S.Name' {..}
|
||||
-- registerName moduleName
|
||||
return moduleName
|
||||
iniScope :: Scope
|
||||
iniScope = emptyScope (getTopModulePath m)
|
||||
checkedModule :: Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
|
||||
checkedModule = do
|
||||
evalState iniScope $ do
|
||||
path' <- freshTopModulePath
|
||||
localScope $
|
||||
withParams params $ \params' -> do
|
||||
(_moduleExportInfo, body') <- checkModuleBody body
|
||||
let _moduleRefModule =
|
||||
Module
|
||||
{ _modulePath = path',
|
||||
_moduleParameters = params',
|
||||
_moduleBody = body'
|
||||
}
|
||||
_moduleRefName = set S.nameConcrete () path'
|
||||
return ModuleRef'' {..}
|
||||
checkPath :: Members '[Files, Reader ScopeParameters, Error ScopeError] s => Sem s ()
|
||||
checkPath = do
|
||||
expectedPath <- modulePathToFilePath path
|
||||
let actualPath = getLoc path ^. intFile
|
||||
unlessM (fromMaybe True <$> equalPaths' expectedPath actualPath) $
|
||||
throw
|
||||
( ErrWrongTopModuleName
|
||||
WrongTopModuleName
|
||||
{ _wrongTopModuleNameActualName = path,
|
||||
_wrongTopModuleNameExpectedPath = expectedPath,
|
||||
_wrongTopModuleNameActualPath = actualPath
|
||||
}
|
||||
)
|
||||
freshTopModulePath ::
|
||||
forall s.
|
||||
Members '[State ScoperState] s =>
|
||||
Sem s S.TopModulePath
|
||||
freshTopModulePath = do
|
||||
_nameId <- freshNameId
|
||||
let _nameDefinedIn = S.topModulePathToAbsPath path
|
||||
_nameConcrete = path
|
||||
_nameDefined = getLoc (_modulePathName path)
|
||||
_nameKind = S.KNameTopModule
|
||||
_nameFixity = Nothing
|
||||
-- This visibility annotation is not relevant
|
||||
_nameVisibilityAnn = VisPublic
|
||||
_nameWhyInScope = S.BecauseDefined
|
||||
_nameVerbatim = N.topModulePathToDottedPath path
|
||||
moduleName = S.Name' {..}
|
||||
-- registerName moduleName
|
||||
return moduleName
|
||||
iniScope :: Scope
|
||||
iniScope = emptyScope (getTopModulePath m)
|
||||
checkedModule :: Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
|
||||
checkedModule = do
|
||||
evalState iniScope $ do
|
||||
path' <- freshTopModulePath
|
||||
localScope $
|
||||
withParams params $ \params' -> do
|
||||
(_moduleExportInfo, body') <- checkModuleBody body
|
||||
let _moduleRefModule =
|
||||
Module
|
||||
{ _modulePath = path',
|
||||
_moduleParameters = params',
|
||||
_moduleBody = body'
|
||||
}
|
||||
_moduleRefName = set S.nameConcrete () path'
|
||||
return ModuleRef'' {..}
|
||||
|
||||
withScope :: Members '[State Scope] r => Sem r a -> Sem r a
|
||||
withScope ma = do
|
||||
@ -537,7 +548,7 @@ withScope ma = do
|
||||
|
||||
checkModuleBody ::
|
||||
forall r.
|
||||
Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint , InfoTableBuilder ] r =>
|
||||
Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint , InfoTableBuilder, Parser.InfoTableBuilder] r =>
|
||||
[Statement 'Parsed] ->
|
||||
Sem r (ExportInfo, [Statement 'Scoped])
|
||||
checkModuleBody body = do
|
||||
@ -549,7 +560,7 @@ checkModuleBody body = do
|
||||
|
||||
checkLocalModule ::
|
||||
forall r.
|
||||
Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint , InfoTableBuilder ] r =>
|
||||
Members '[Error ScopeError, State Scope, Reader ScopeParameters, State ScoperState, Files, Reader LocalVars, Fixpoint , InfoTableBuilder, Parser.InfoTableBuilder] r =>
|
||||
Module 'Parsed 'ModuleLocal ->
|
||||
Sem r (Module 'Scoped 'ModuleLocal)
|
||||
checkLocalModule Module {..} = do
|
||||
@ -1058,7 +1069,7 @@ checkParsePatternAtom ::
|
||||
checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
|
||||
|
||||
checkStatement ::
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars, Fixpoint , InfoTableBuilder] r =>
|
||||
Members '[Error ScopeError, Reader ScopeParameters, Files, State Scope, State ScoperState, Reader LocalVars, Fixpoint , InfoTableBuilder, Parser.InfoTableBuilder] r =>
|
||||
Statement 'Parsed ->
|
||||
Sem r (Statement 'Scoped)
|
||||
checkStatement s = case s of
|
||||
|
||||
14
src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/ScoperResult.hs
Normal file
14
src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/ScoperResult.hs
Normal file
@ -0,0 +1,14 @@
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scoper.ScoperResult where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.InfoTable as Scoped
|
||||
import qualified MiniJuvix.Syntax.Concrete.Parser.InfoTable as Parser
|
||||
|
||||
|
||||
data ScoperResult = ScoperResult {
|
||||
_resultParserTable :: Parser.InfoTable,
|
||||
_resultScoperTable :: Scoped.InfoTable,
|
||||
_resultModules :: NonEmpty (Module 'Scoped 'ModuleTop)
|
||||
}
|
||||
makeLenses ''ScoperResult
|
||||
@ -147,4 +147,3 @@ vp token keys-changed verifiers :=
|
||||
auxVP (foldl (check-keys verifiers) (MakePair 0 false) keys-changed);
|
||||
|
||||
end;
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user