From fd3622a274fabdac2a84e0746f1bcfafa62f94d7 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 1 Apr 2022 13:00:15 +0200 Subject: [PATCH] Adds many new features (w.i.p v0.1.2) (#28) * add references to the syntax and cleanup code * [make] add .PHONY to Makefile targets * [parser] add parser / pretty for axiom backends * Pairing progress * [scoper] Add support for Axiom backends * [parser] Fix foreign block parsing * [ app ] adds --no-colors flag for the scope command * [ghc] upgrade to ghc 9.2.2 * use GHC2021 * [doc] Remove out-of-date comment * [test] Add ambiguity tests * [scoper] Improve resolution of local symbols * [error] WIP improving ambiguity error messages * [ clean-up ] new lab folder for experimentation * [ app ] ixes the lint warning * [ Termination ] removes Alga dependency * [error] Add message for ambiguous symbol error * [error] Add ambiguous module message * [scoper] Remove ErrGeneric * [test] Add test to suite * [test] show diff when ast's are different * [ lab ] folder organization * [ Makefile ] add targets with --watch option (stack cmds) and remove unused things * [ app ] add --version flag and fixed warnings and formatting * [test] remove fromRightIO to fix ambiguity error * [test] Add test of shadowing public open * [scoper] Add visibility annotation for Name * prepare buildIntoTable * [ Concrete ] add instance of hashable for refs. * add InfoTableBuilder effect * [ scoper ] add InfoTableBuilder effect * [ CHANGELOG ] updated v0.1.1 * [ README ] org version now * fix package.yaml * fix readme * [microjuvix] implement basic typechecker * add simple test for MicroJuvix type checker * fix checking for constructors apps in patterns * [scope] Move InfoTable to a new module * [abstract] Make Iden use references instead of Name * [abstract] Add InfoTable for abstract syntax * [scoper] Add function clauses to scoped InfoTable * [abstract] Add InfoTableBuilder for scoped to abstract * [main] Fix callsites of translateModule * [doc] Remove empty docs * [scoper] Update emptyInfoTable with missing field * rename some functions * [minihaskell] add compilation to MiniHaskell * [microjuvix] improve wrong type message * Add a validity predicate example written in MiniJuvix * [typecheck] Add error infrastructure for type errors Add a pretty error for mismatched constructor type in a pattern match * [test] Adds negative typecheck test for constructor * [app] Adds microjuvix subcommands for printing / typechecking * [typecheck] Add error message for ctor match args mistmatch * [typecheck] Add descriptive messages for remainng errors * [typecheck] Updates to error message copy * [typecheck] fix merge conflicts: * [highlight] add basic support for highlighting symbols * [minijuvix-mode] add minijuvix-mode and basic description in the readme * [readme] improve formatting * automatically detect the root of the project and add --show-root flag Co-authored-by: Jan Mas Rovira Co-authored-by: Paul Cadman Co-authored-by: Paul Cadman --- README.org | 36 +++- app/Commands/MicroJuvix.hs | 30 +++ app/Main.hs | 139 +++++++++--- minijuvix-mode/minijuvix-highlight.el | 52 +++++ minijuvix-mode/minijuvix-mode.el | 29 +++ package.yaml | 3 - src/MiniJuvix/Internal/Strings.hs | 3 + src/MiniJuvix/Syntax/Abstract/InfoTable.hs | 43 ++++ .../Syntax/Abstract/InfoTableBuilder.hs | 60 ++++++ src/MiniJuvix/Syntax/Abstract/Language.hs | 61 +++++- .../Syntax/Abstract/Language/Extra.hs | 2 +- src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs | 19 +- src/MiniJuvix/Syntax/Backends.hs | 14 ++ src/MiniJuvix/Syntax/Concrete/Language.hs | 37 +--- src/MiniJuvix/Syntax/Concrete/Lexer.hs | 10 +- src/MiniJuvix/Syntax/Concrete/Literal.hs | 23 ++ src/MiniJuvix/Syntax/Concrete/Loc.hs | 10 +- .../Syntax/Concrete/Scoped/Highlight.hs | 85 ++++++++ .../Syntax/Concrete/Scoped/InfoTable.hs | 48 +++++ src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs | 13 +- .../Syntax/Concrete/Scoped/Pretty/Base.hs | 4 +- src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs | 49 +---- .../Syntax/Concrete/Scoped/Scoper.hs | 79 ++++--- .../Scoped/Scoper/InfoTableBuilder.hs | 31 +-- src/MiniJuvix/Syntax/ForeignBlock.hs | 13 ++ src/MiniJuvix/Syntax/MicroJuvix/Error.hs | 37 ++++ .../Syntax/MicroJuvix/Error/Pretty.hs | 9 + .../Syntax/MicroJuvix/Error/Pretty/Ansi.hs | 16 ++ .../Syntax/MicroJuvix/Error/Pretty/Base.hs | 65 ++++++ .../Syntax/MicroJuvix/Error/Pretty/Text.hs | 9 + .../Syntax/MicroJuvix/Error/Types.hs | 46 ++++ src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs | 52 +++++ src/MiniJuvix/Syntax/MicroJuvix/Language.hs | 76 +++++-- src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs | 9 + .../Syntax/MicroJuvix/Pretty/Base.hs | 95 ++++++-- .../Syntax/MicroJuvix/Pretty/Text.hs | 29 +++ .../Syntax/MicroJuvix/TypeChecker.hs | 203 ++++++++++++++++++ src/MiniJuvix/Syntax/MiniHaskell/Language.hs | 39 +++- .../Syntax/MiniHaskell/Pretty/Base.hs | 29 ++- src/MiniJuvix/Syntax/NameId.hs | 15 ++ src/MiniJuvix/Syntax/Universe.hs | 4 +- src/MiniJuvix/Termination/CallGraph.hs | 6 +- src/MiniJuvix/Termination/CallMap.hs | 41 ++-- src/MiniJuvix/Termination/Types.hs | 14 +- .../Translation/AbstractToMicroJuvix.hs | 79 +++---- .../Translation/MicroJuvixToMiniHaskell.hs | 196 +++++++++++++++++ src/MiniJuvix/Translation/ScopedToAbstract.hs | 137 ++++++------ test/Base.hs | 5 + test/Main.hs | 4 +- test/TypeCheck.hs | 7 + test/TypeCheck/Negative.hs | 64 ++++++ .../MicroJuvix/ExpectedFunctionType.mjuvix | 12 ++ .../MicroJuvix/PatternConstructor.mjuvix | 13 ++ .../MicroJuvix/PatternConstructorApp.mjuvix | 13 ++ .../MicroJuvix/TooManyPatterns.mjuvix | 8 + tests/negative/MicroJuvix/WrongType.mjuvix | 12 ++ tests/positive/MicroJuvix/Simple.mjuvix | 44 ++++ tests/positive/MiniHaskell/HelloWorld.mjuvix | 49 +++++ tests/positive/StdlibList/Data/Bool.mjuvix | 18 +- tests/positive/VP/SimpleFungibleToken.mjuvix | 150 +++++++++++++ 60 files changed, 2105 insertions(+), 393 deletions(-) create mode 100644 minijuvix-mode/minijuvix-highlight.el create mode 100644 minijuvix-mode/minijuvix-mode.el create mode 100644 src/MiniJuvix/Syntax/Abstract/InfoTable.hs create mode 100644 src/MiniJuvix/Syntax/Abstract/InfoTableBuilder.hs create mode 100644 src/MiniJuvix/Syntax/Backends.hs create mode 100644 src/MiniJuvix/Syntax/Concrete/Literal.hs create mode 100644 src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs create mode 100644 src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs create mode 100644 src/MiniJuvix/Syntax/ForeignBlock.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Pretty/Text.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs create mode 100644 src/MiniJuvix/Syntax/NameId.hs create mode 100644 src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs create mode 100644 test/TypeCheck.hs create mode 100644 test/TypeCheck/Negative.hs create mode 100644 tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix create mode 100644 tests/negative/MicroJuvix/PatternConstructor.mjuvix create mode 100644 tests/negative/MicroJuvix/PatternConstructorApp.mjuvix create mode 100644 tests/negative/MicroJuvix/TooManyPatterns.mjuvix create mode 100644 tests/negative/MicroJuvix/WrongType.mjuvix create mode 100644 tests/positive/MicroJuvix/Simple.mjuvix create mode 100644 tests/positive/MiniHaskell/HelloWorld.mjuvix create mode 100644 tests/positive/VP/SimpleFungibleToken.mjuvix diff --git a/README.org b/README.org index c90ccd353..2b41ba8e9 100644 --- a/README.org +++ b/README.org @@ -1,7 +1,17 @@ -MiniJuvix -[[file:LICENSE][[[https://img.shields.io/badge/license-GPL--3.0--only-blue.svg]]]] -[[https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml][[[https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml/badge.svg?branch=qtt]]]] -==== +* MiniJuvix + +#+begin_html + +LICENSE + +#+end_html + +#+begin_html + +CI status + +#+end_html + ** Description @@ -57,6 +67,24 @@ It is required at least 8GB RAM for =stack= installation. $ stack test #+end_src +** Emacs mode + There is an emacs mode available for MiniJuvix. Currently it supports syntax + highlighting for well-scoped modules. It is a work in progress. + + To install it add the following lines to your emacs configuration file: + #+begin_src elisp + (push "/path/to/minijuvix/minijuvix-mode/" load-path) + (require 'minijuvix-mode) + #+end_src + Also, =minijuvix= must be installed in your =PATH=. + + The MiniJuvix major mode will be activated automatically for =.mjuvix= files. +*** Keybindings + + | Key | Function Name | Description | + |-----------+------------------+-------------------------------------------------------| + | =C-c C-l= | =minijuvix-load= | Runs the scoper and adds semantic syntax highlighting | + ** Community We would love to hear what you think of MiniJuvix! Join us on diff --git a/app/Commands/MicroJuvix.hs b/app/Commands/MicroJuvix.hs index b4f9156d3..343b030f0 100644 --- a/app/Commands/MicroJuvix.hs +++ b/app/Commands/MicroJuvix.hs @@ -6,10 +6,40 @@ import Commands.Extra import MiniJuvix.Prelude hiding (Doc) import Options.Applicative +data MicroJuvixCommand + = Pretty MicroJuvixOptions + | TypeCheck MicroJuvixOptions + newtype MicroJuvixOptions = MicroJuvixOptions { _mjuvixInputFile :: FilePath } +parseMicroJuvixCommand :: Parser MicroJuvixCommand +parseMicroJuvixCommand = + hsubparser $ + mconcat + [ commandPretty + , commandTypeCheck + ] + where + commandPretty :: Mod CommandFields MicroJuvixCommand + commandPretty = command "pretty" prettyInfo + + commandTypeCheck :: Mod CommandFields MicroJuvixCommand + commandTypeCheck = command "typecheck" typeCheckInfo + + prettyInfo :: ParserInfo MicroJuvixCommand + prettyInfo = + info + (Pretty <$> parseMicroJuvix) + (progDesc "Translate a MiniJuvix file to MicroJuvix and pretty print the result") + + typeCheckInfo :: ParserInfo MicroJuvixCommand + typeCheckInfo = + info + (TypeCheck <$> parseMicroJuvix) + (progDesc "Translate a MiniJuvix file to MicroJuvix and typecheck the result") + parseMicroJuvix :: Parser MicroJuvixOptions parseMicroJuvix = do _mjuvixInputFile <- parseInputFile diff --git a/app/Main.hs b/app/Main.hs index fe671c72d..3f7615e52 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -9,21 +9,28 @@ import Commands.MicroJuvix import Commands.MiniHaskell import Commands.Termination as T import Control.Monad.Extra +import qualified Control.Exception as IO import MiniJuvix.Prelude hiding (Doc) import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A 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.Scoped.Highlight as Scoped import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions) import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text as T import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro +import qualified MiniJuvix.Syntax.MicroJuvix.TypeChecker as Micro +import qualified MiniJuvix.Syntax.MicroJuvix.Language as Micro import qualified MiniJuvix.Termination as T import qualified MiniJuvix.Termination.CallGraph as A import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro import qualified MiniJuvix.Translation.ScopedToAbstract as A +import qualified MiniJuvix.Translation.MicroJuvixToMiniHaskell as Hask +import qualified MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi as Hask import MiniJuvix.Utils.Version (runDisplayVersion) import Options.Applicative import Options.Applicative.Help.Pretty @@ -37,8 +44,10 @@ data Command | Html HtmlOptions | Termination TerminationCommand | MiniHaskell MiniHaskellOptions - | MicroJuvix MicroJuvixOptions + | MicroJuvix MicroJuvixCommand | DisplayVersion + | DisplayRoot + | Highlight HighlightOptions data ScopeOptions = ScopeOptions { _scopeRootDir :: FilePath, @@ -53,6 +62,10 @@ data ParseOptions = ParseOptions _parseNoPrettyShow :: Bool } +data HighlightOptions = HighlightOptions + { _highlightInputFile :: FilePath + } + data HtmlOptions = HtmlOptions { _htmlInputFile :: FilePath, _htmlRecursive :: Bool, @@ -84,6 +97,11 @@ parseHtml = do "ayu" -> Right Ayu _ -> Left $ "unrecognised theme: " <> s +parseHighlight :: Parser HighlightOptions +parseHighlight = do + _highlightInputFile <- parseInputFile + pure HighlightOptions {..} + parseParse :: Parser ParseOptions parseParse = do _parseInputFile <- parseInputFile @@ -135,6 +153,13 @@ parseDisplayVersion = DisplayVersion (long "version" <> short 'v' <> help "Print the version and exit") +parseDisplayRoot :: Parser Command +parseDisplayRoot = + flag' + DisplayRoot + (long "show-root" <> help "Print the detected root of the project") + + descr :: ParserInfo Command descr = info @@ -154,16 +179,18 @@ descr = parseCommand :: Parser Command parseCommand = parseDisplayVersion - <|> ( hsubparser $ - mconcat - [ commandParse, - commandScope, - commandHtml, - commandTermination, - commandMicroJuvix, - commandMiniHaskell - ] - ) + <|> parseDisplayRoot + <|> ( hsubparser $ + mconcat + [ commandParse, + commandScope, + commandHtml, + commandTermination, + commandMicroJuvix, + commandMiniHaskell, + commandHighlight + ] + ) where commandMicroJuvix :: Mod CommandFields Command commandMicroJuvix = command "microjuvix" minfo @@ -171,8 +198,8 @@ parseCommand = minfo :: ParserInfo Command minfo = info - (MicroJuvix <$> parseMicroJuvix) - (progDesc "Translate a MiniJuvix file to MicroJuvix") + (MicroJuvix <$> parseMicroJuvixCommand) + (progDesc "Subcommands related to MicroJuvix") commandMiniHaskell :: Mod CommandFields Command commandMiniHaskell = command "minihaskell" minfo @@ -183,6 +210,15 @@ parseCommand = (MiniHaskell <$> parseMiniHaskell) (progDesc "Translate a MiniJuvix file to MiniHaskell") + commandHighlight :: Mod CommandFields Command + commandHighlight = command "highlight" minfo + where + minfo :: ParserInfo Command + minfo = + info + (Highlight <$> parseHighlight) + (progDesc "Highlight a MiniJuvix file") + commandParse :: Mod CommandFields Command commandParse = command "parse" minfo where @@ -229,11 +265,38 @@ mkScopePrettyOptions ScopeOptions {..} = parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop) parseModuleIO = fromRightIO id . M.runModuleParserIO -go :: Command -> IO () -go c = do - root <- getCurrentDirectory +minijuvixYamlFile :: FilePath +minijuvixYamlFile = "minijuvix.yaml" + +findRoot :: IO FilePath +findRoot = do + r <- IO.try go :: IO (Either IO.SomeException FilePath) + case r of + 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 + Right root -> return root + where + possiblePaths :: FilePath -> [FilePath] + possiblePaths start = takeWhile (/= "/") (aux start) + where + aux f = f : aux (takeDirectory f) + go :: IO FilePath + go = do + c <- getCurrentDirectory + l <- findFile (possiblePaths c) minijuvixYamlFile + case l of + Nothing -> return c + Just yaml -> return (takeDirectory yaml) + +runCommand :: Command -> IO () +runCommand c = do + root <- findRoot case c of DisplayVersion -> runDisplayVersion + DisplayRoot -> putStrLn (pack root) Scope opts@ScopeOptions {..} -> do forM_ _scopeInputFiles $ \scopeInputFile -> do m <- parseModuleIO scopeInputFile @@ -244,6 +307,10 @@ go c = do printer | 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)) Parse ParseOptions {..} -> do m <- parseModuleIO _parseInputFile if _parseNoPrettyShow then print m else pPrint m @@ -251,25 +318,26 @@ go c = do m <- parseModuleIO _htmlInputFile (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m genHtml defaultOptions _htmlRecursive _htmlTheme s - MicroJuvix MicroJuvixOptions {..} -> do - m <- parseModuleIO _mjuvixInputFile - (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m - a <- fromRightIO' putStrLn (return $ A.translateModule s) - let mini = Micro.translateModule a - Micro.printPrettyCodeDefault mini + MicroJuvix (Pretty MicroJuvixOptions {..}) -> do + micro <- miniToMicro root _mjuvixInputFile + Micro.printPrettyCodeDefault micro + MicroJuvix (TypeCheck MicroJuvixOptions {..}) -> do + micro <- miniToMicro root _mjuvixInputFile + case Micro.checkModule micro of + Left er -> printErrorAnsi er + Right {} -> putStrLn "Well done! It type checks" MiniHaskell MiniHaskellOptions {..} -> do m <- parseModuleIO _mhaskellInputFile - (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m - -- a <- fromRightIO' putStrLn (return $ A.translateModule s) - _ <- fromRightIO' putStrLn (return $ A.translateModule s) - -- let mini = Micro.translateModule a - -- Micro.printPrettyCodeDefault mini - -- TODO - error "todo" + (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m + (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s) + let micro = Micro.translateModule a + checkedMicro <- fromRightIO' printErrorAnsi (return $ Micro.checkModule micro) + minihaskell <- fromRightIO' putStrLn (return $ Hask.translateModule checkedMicro) + Hask.printPrettyCodeDefault minihaskell Termination (Calls opts@CallsOptions {..}) -> do m <- parseModuleIO _callsInputFile (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m - a <- fromRightIO' putStrLn (return $ A.translateModule s) + (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s) let callMap0 = T.buildCallMap a callMap = case _callsFunctionNameFilter of Nothing -> callMap0 @@ -280,7 +348,7 @@ go c = do Termination (CallGraph CallGraphOptions {..}) -> do m <- parseModuleIO _graphInputFile (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m - a <- fromRightIO' putStrLn (return $ A.translateModule s) + (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s) let callMap = T.buildCallMap a opts' = A.defaultOptions completeGraph = T.completeCallGraph callMap @@ -296,6 +364,13 @@ go c = do Nothing -> putStrLn (n <> " Fails the termination checking") Just (T.LexOrder k) -> putStrLn (n <> " Terminates with order " <> show (toList k)) putStrLn "" + where + miniToMicro :: FilePath -> FilePath -> IO Micro.Module + miniToMicro root p = do + m <- parseModuleIO p + (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m + (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s) + return (Micro.translateModule a) main :: IO () -main = execParser descr >>= go +main = execParser descr >>= runCommand diff --git a/minijuvix-mode/minijuvix-highlight.el b/minijuvix-mode/minijuvix-highlight.el new file mode 100644 index 000000000..bd3c9af8f --- /dev/null +++ b/minijuvix-mode/minijuvix-highlight.el @@ -0,0 +1,52 @@ +(require 'font-lock) + +(defgroup minijuvix-highlight nil + "Syntax highlighting for MiniJuvix." + :group 'minijuvix) + +(defgroup agda2-highlight-faces nil + "Faces used to highlight MiniJuvix code." + :group 'minijuvix-highlight) + +(defface minijuvix-highlight-keyword-face + '((((background light)) + (:foreground "#399ee6")) + (((background dark)) + (:foreground "#81a1c1"))) + "The face used for keywords." + :group 'minijuvix-highlight-faces) + +(defface minijuvix-highlight-function-face + '((((background light)) + (:foreground "#f2ae49")) + (((background dark)) + (:foreground "#ebcb8b"))) + "The face used for functions." + :group 'minijuvix-highlight-faces) + +(defface minijuvix-highlight-inductive-face + '((((background light)) + (:foreground "#86b300")) + (((background dark)) + (:foreground "#a3be8c"))) + "The face used for inductive types." + :group 'minijuvix-highlight-faces) + +(defface minijuvix-highlight-constructor-face + '((((background light)) + (:foreground "#a37acc")) + (((background dark)) + (:foreground "#b48ead"))) + "The face used for constructors." + :group 'minijuvix-highlight-faces) + +(defface minijuvix-highlight-axiom-face + '((((background light)) + (:foreground "#f07171")) + (((background dark)) + (:foreground "#bf616a"))) + "The face used for axioms." + :group 'minijuvix-highlight-faces) + + +(provide 'minijuvix-highlight) diff --git a/minijuvix-mode/minijuvix-mode.el b/minijuvix-mode/minijuvix-mode.el new file mode 100644 index 000000000..597cfede3 --- /dev/null +++ b/minijuvix-mode/minijuvix-mode.el @@ -0,0 +1,29 @@ +(require 'minijuvix-highlight) + +(defgroup minijuvix nil + "Major mode for MiniJuvix files." + :group 'languages) + +(defvar minijuvix-mode-map + (let ((map (make-sparse-keymap)) + (menu-map (make-sparse-keymap "MiniJuvix"))) + (define-key map "\C-c\C-l" 'minijuvix-load) + map) + "Keymap for MiniJuvix mode.") + + +;;;###autoload +(add-to-list 'auto-mode-alist '("\\.m?juvix\\'" . minijuvix-mode)) + +(define-derived-mode minijuvix-mode prog-mode "MiniJuvix" + + (font-lock-mode 0) + ) + +(defun minijuvix-load () + "Load current buffer." + (interactive) + (eval (read (shell-command-to-string (concat "minijuvix highlight " (buffer-file-name))))) + ) + +(provide 'minijuvix-mode) diff --git a/package.yaml b/package.yaml index 02045f134..1892c5197 100644 --- a/package.yaml +++ b/package.yaml @@ -77,9 +77,6 @@ default-extensions: - TypeFamilyDependencies - UnicodeSyntax -# verbatim: -# default-language: GHC2021 - library: source-dirs: src verbatim: diff --git a/src/MiniJuvix/Internal/Strings.hs b/src/MiniJuvix/Internal/Strings.hs index ddfeffbbb..4efa3c53b 100644 --- a/src/MiniJuvix/Internal/Strings.hs +++ b/src/MiniJuvix/Internal/Strings.hs @@ -65,6 +65,9 @@ let_ = "let" public :: IsString s => s public = "public" +any :: IsString s => s +any = "Any" + type_ :: IsString s => s type_ = "Type" diff --git a/src/MiniJuvix/Syntax/Abstract/InfoTable.hs b/src/MiniJuvix/Syntax/Abstract/InfoTable.hs new file mode 100644 index 000000000..b950a90e9 --- /dev/null +++ b/src/MiniJuvix/Syntax/Abstract/InfoTable.hs @@ -0,0 +1,43 @@ +module MiniJuvix.Syntax.Abstract.InfoTable where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.Abstract.Language + +newtype FunctionInfo = FunctionInfo { + _functionInfoDef :: FunctionDef + } + +data ConstructorInfo = ConstructorInfo { + _constructorInfoInductive :: InductiveInfo, + _constructorInfoType :: Expression + } + +data AxiomInfo = AxiomInfo { + _axiomInfoType :: Expression, + _axiomInfoBackends :: [BackendItem] + } + +newtype InductiveInfo = InductiveInfo { + _inductiveInfoDef :: InductiveDef + } + +data InfoTable = InfoTable { + _infoConstructors :: HashMap ConstructorRef ConstructorInfo, + _infoAxioms :: HashMap AxiomRef AxiomInfo, + _infoInductives :: HashMap InductiveRef InductiveInfo, + _infoFunctions :: HashMap FunctionRef FunctionInfo + } + +emptyInfoTable :: InfoTable +emptyInfoTable = InfoTable { + _infoConstructors = mempty, + _infoAxioms = mempty, + _infoInductives = mempty, + _infoFunctions = mempty + } + +makeLenses ''InfoTable +makeLenses ''InductiveInfo +makeLenses ''ConstructorInfo +makeLenses ''AxiomInfo +makeLenses ''FunctionInfo diff --git a/src/MiniJuvix/Syntax/Abstract/InfoTableBuilder.hs b/src/MiniJuvix/Syntax/Abstract/InfoTableBuilder.hs new file mode 100644 index 000000000..334b5923c --- /dev/null +++ b/src/MiniJuvix/Syntax/Abstract/InfoTableBuilder.hs @@ -0,0 +1,60 @@ +module MiniJuvix.Syntax.Abstract.InfoTableBuilder + ( module MiniJuvix.Syntax.Abstract.InfoTableBuilder, + module MiniJuvix.Syntax.Abstract.InfoTable) +where + +import qualified Data.HashMap.Strict as HashMap +import MiniJuvix.Syntax.Abstract.InfoTable +import MiniJuvix.Prelude +import MiniJuvix.Syntax.Abstract.Language +import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol) + + +data InfoTableBuilder m a where + RegisterAxiom :: AxiomDef -> InfoTableBuilder m () + RegisterConstructor :: InductiveInfo -> InductiveConstructorDef -> InfoTableBuilder m () + RegisterInductive :: InductiveDef -> InfoTableBuilder m InductiveInfo + RegisterFunction :: FunctionDef -> InfoTableBuilder m () + +makeSem ''InfoTableBuilder + +registerFunction' :: + Member InfoTableBuilder r => + FunctionDef -> Sem r FunctionDef +registerFunction' ts = registerFunction ts $> ts + +registerAxiom' :: Member InfoTableBuilder r => + AxiomDef -> Sem r AxiomDef +registerAxiom' a = registerAxiom a $> a + +toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a +toState = reinterpret $ \case + RegisterAxiom d -> + let ref = AxiomRef (unqualifiedSymbol (d ^. axiomName)) + info = AxiomInfo { + _axiomInfoType = d ^. axiomType, + _axiomInfoBackends = d ^. axiomBackendItems + } + in modify (over infoAxioms (HashMap.insert ref info)) + RegisterConstructor _constructorInfoInductive def -> let + ref = ConstructorRef (unqualifiedSymbol (def ^. constructorName)) + info = ConstructorInfo { + _constructorInfoType = def ^. constructorType, + .. + } + in modify (over infoConstructors (HashMap.insert ref info)) + RegisterInductive ity -> let + ref = InductiveRef (unqualifiedSymbol (ity ^. inductiveName)) + info = InductiveInfo { + _inductiveInfoDef = ity + } + in modify (over infoInductives (HashMap.insert ref info)) $> info + RegisterFunction _functionInfoDef -> let + ref = FunctionRef (unqualifiedSymbol (_functionInfoDef ^. funDefName)) + info = FunctionInfo { + .. + } + in modify (over infoFunctions (HashMap.insert ref info)) + +runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a) +runInfoTableBuilder = runState emptyInfoTable . toState diff --git a/src/MiniJuvix/Syntax/Abstract/Language.hs b/src/MiniJuvix/Syntax/Abstract/Language.hs index 80425f535..1002b9a73 100644 --- a/src/MiniJuvix/Syntax/Abstract/Language.hs +++ b/src/MiniJuvix/Syntax/Abstract/Language.hs @@ -25,6 +25,9 @@ type InductiveName = S.Symbol type AxiomName = S.Symbol +-- TODO: Perhaps we could use a different Name type +-- that just includes fields (nameId + debug info) +-- requried in future passes. type Name = S.Name type TopModule = Module C.TopModulePath @@ -38,14 +41,19 @@ data Module s = Module deriving stock (Show, Eq) data ModuleBody = ModuleBody - { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef), - _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef), - _moduleImports :: [Indexed TopModule], - _moduleForeigns :: [Indexed ForeignBlock], - _moduleLocalModules :: HashMap LocalModuleName (Indexed LocalModule) + { _moduleStatements :: [Statement] } deriving stock (Show, Eq) +data Statement = + StatementInductive InductiveDef + | StatementFunction FunctionDef + | StatementImport TopModule + | StatementForeign ForeignBlock + | StatementLocalModule LocalModule + | StatementAxiom AxiomDef + deriving stock (Show, Eq) + data FunctionDef = FunctionDef { _funDefName :: FunctionName, _funDefTypeSig :: Expression, @@ -59,12 +67,32 @@ data FunctionClause = FunctionClause } deriving stock (Show, Eq) +newtype FunctionRef = FunctionRef + { _functionRefName :: Name } + deriving stock (Show, Eq) + deriving newtype Hashable + +newtype ConstructorRef = ConstructorRef + { _constructorRefName :: Name } + deriving stock (Show, Eq) + deriving newtype Hashable + +newtype InductiveRef = InductiveRef + { _inductiveRefName :: Name } + deriving stock (Show, Eq) + deriving newtype Hashable + +newtype AxiomRef = AxiomRef + { _axiomRefName :: Name } + deriving stock (Show, Eq) + deriving newtype Hashable + data Iden - = IdenFunction Name - | IdenConstructor Name + = IdenFunction FunctionRef + | IdenConstructor ConstructorRef | IdenVar VarName - | IdenInductive Name - | IdenAxiom Name + | IdenInductive InductiveRef + | IdenAxiom AxiomRef deriving stock (Show, Eq) data Expression @@ -134,7 +162,7 @@ instance HasAtomicity Function where -- | Fully applied constructor in a pattern. data ConstructorApp = ConstructorApp - { _constrAppConstructor :: Name, + { _constrAppConstructor :: ConstructorRef, _constrAppParameters :: [Pattern] } deriving stock (Show, Eq) @@ -176,3 +204,16 @@ makeLenses ''InductiveDef makeLenses ''ModuleBody makeLenses ''InductiveConstructorDef makeLenses ''ConstructorApp +makeLenses ''FunctionRef +makeLenses ''ConstructorRef +makeLenses ''InductiveRef +makeLenses ''AxiomRef +makeLenses ''AxiomDef + +idenName :: Iden -> Name +idenName = \case + IdenFunction n -> n ^. functionRefName + IdenConstructor n -> n ^. constructorRefName + IdenInductive n -> n ^. inductiveRefName + IdenVar n -> S.unqualifiedSymbol n + IdenAxiom n -> n ^. axiomRefName diff --git a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs index f4b2d4c47..f16cbbca2 100644 --- a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs +++ b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs @@ -43,7 +43,7 @@ viewExpressionAsPattern e = case viewApp e of | Just v <- getVariable f -> Just (PatternVariable v) _ -> Nothing where - getConstructor :: Expression -> Maybe Name + getConstructor :: Expression -> Maybe ConstructorRef getConstructor f = case f of ExpressionIden (IdenConstructor n) -> Just n _ -> Nothing diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs index 2d9b3be4c..4a323f1eb 100644 --- a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs @@ -52,12 +52,7 @@ runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann runPrettyCode opts = run . runReader opts . ppCode instance PrettyCode Iden where - ppCode i = case i of - IdenFunction n -> ppSCode n - IdenConstructor n -> ppSCode n - IdenInductive n -> ppSCode n - IdenVar n -> ppSCode n - IdenAxiom n -> ppSCode n + ppCode = ppSCode . idenName instance PrettyCode Application where ppCode (Application l r) = do @@ -119,6 +114,18 @@ instance PrettyCode Function where funReturn' <- ppRightExpression funFixity _funReturn return $ funParameter' <+> kwTo <+> funReturn' +instance PrettyCode FunctionRef where + ppCode FunctionRef {..} = ppSCode _functionRefName + +instance PrettyCode ConstructorRef where + ppCode ConstructorRef {..} = ppSCode _constructorRefName + +instance PrettyCode InductiveRef where + ppCode InductiveRef {..} = ppSCode _inductiveRefName + +instance PrettyCode AxiomRef where + ppCode AxiomRef {..} = ppSCode _axiomRefName + parensCond :: Bool -> Doc Ann -> Doc Ann parensCond t d = if t then parens d else d diff --git a/src/MiniJuvix/Syntax/Backends.hs b/src/MiniJuvix/Syntax/Backends.hs new file mode 100644 index 000000000..eb05b5756 --- /dev/null +++ b/src/MiniJuvix/Syntax/Backends.hs @@ -0,0 +1,14 @@ +module MiniJuvix.Syntax.Backends where + +import MiniJuvix.Prelude + +data Backend = BackendGhc | BackendAgda + deriving stock (Show, Eq, Ord) + +data BackendItem = BackendItem + { _backendItemBackend :: Backend, + _backendItemCode :: Text + } + deriving stock (Show, Eq, Ord) + +makeLenses ''BackendItem diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs index f0a5f1c02..89b50c89b 100644 --- a/src/MiniJuvix/Syntax/Concrete/Language.hs +++ b/src/MiniJuvix/Syntax/Concrete/Language.hs @@ -3,6 +3,9 @@ module MiniJuvix.Syntax.Concrete.Language ( module MiniJuvix.Syntax.Concrete.Language, module MiniJuvix.Syntax.Concrete.Name, module MiniJuvix.Syntax.Concrete.Loc, + module MiniJuvix.Syntax.Concrete.Literal, + module MiniJuvix.Syntax.Backends, + module MiniJuvix.Syntax.ForeignBlock, module MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn, module MiniJuvix.Syntax.Concrete.PublicAnn, module MiniJuvix.Syntax.Concrete.ModuleIsTop, @@ -18,7 +21,10 @@ where import qualified Data.Kind as GHC import MiniJuvix.Prelude hiding (show) import MiniJuvix.Syntax.Concrete.Language.Stage +import MiniJuvix.Syntax.Backends +import MiniJuvix.Syntax.ForeignBlock import MiniJuvix.Syntax.Concrete.Loc +import MiniJuvix.Syntax.Concrete.Literal import MiniJuvix.Syntax.Concrete.ModuleIsTop import MiniJuvix.Syntax.Concrete.Name import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn @@ -132,12 +138,6 @@ deriving stock instance ) => Ord (Statement s) -data ForeignBlock = ForeignBlock - { _foreignBackend :: Backend, - _foreignCode :: Text - } - deriving stock (Eq, Ord, Show) - -------------------------------------------------------------------------------- -- Import statement -------------------------------------------------------------------------------- @@ -662,11 +662,6 @@ data Expression | ExpressionFunction (Function 'Scoped) deriving stock (Show, Eq, Ord) -instance HasAtomicity Literal where - atomicity = \case - LitInteger {} -> Atom - LitString {} -> Atom - instance HasAtomicity Expression where atomicity e = case e of ExpressionIdentifier {} -> Atom @@ -685,11 +680,6 @@ instance HasAtomicity Expression where -- Expression atom -------------------------------------------------------------------------------- -data Literal - = LitString Text - | LitInteger Integer - deriving stock (Show, Eq, Ord) - -- | Expressions without application data ExpressionAtom (s :: Stage) = AtomIdentifier (IdentifierType s) @@ -1058,19 +1048,6 @@ deriving stock instance ) => Ord (LetClause s) --------------------------------------------------------------------------------- --- Backends --------------------------------------------------------------------------------- - -data Backend = BackendGhc | BackendAgda - deriving stock (Show, Eq, Ord) - -data BackendItem = BackendItem - { _backendItemBackend :: Backend, - _backendItemCode :: Text - } - deriving stock (Show, Eq, Ord) - -------------------------------------------------------------------------------- -- Debugging statements -------------------------------------------------------------------------------- @@ -1117,14 +1094,12 @@ makeLenses ''TypeSignature makeLenses ''AxiomDef makeLenses ''FunctionClause makeLenses ''InductiveParameter -makeLenses ''ForeignBlock makeLenses ''AxiomRef' makeLenses ''InductiveRef' makeLenses ''ModuleRef' makeLenses ''ModuleRef'' makeLenses ''FunctionRef' makeLenses ''ConstructorRef' -makeLenses ''BackendItem makeLenses ''OpenModule makeLenses ''PatternApp makeLenses ''PatternInfixApp diff --git a/src/MiniJuvix/Syntax/Concrete/Lexer.hs b/src/MiniJuvix/Syntax/Concrete/Lexer.hs index 5180087d1..1833a0960 100644 --- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs +++ b/src/MiniJuvix/Syntax/Concrete/Lexer.hs @@ -62,17 +62,21 @@ bracedString = string :: MonadParsec e Text m => m Text string = pack <$> (char '"' >> manyTill L.charLiteral (char '"')) -mkLoc :: SourcePos -> Loc -mkLoc SourcePos {..} = Loc {..} +mkLoc :: Int -> SourcePos -> Loc +mkLoc offset SourcePos {..} = Loc {..} where _locFile = sourceName + _locOffset = Pos (fromIntegral offset) _locFileLoc = FileLoc {..} where _locLine = fromPos sourceLine _locCol = fromPos sourceColumn curLoc :: MonadParsec e Text m => m Loc -curLoc = mkLoc <$> getSourcePos +curLoc = do + sp <- getSourcePos + offset <- stateOffset <$> getParserState + return (mkLoc offset sp) withLoc :: MonadParsec e Text m => (Loc -> m a) -> m a withLoc ma = curLoc >>= ma diff --git a/src/MiniJuvix/Syntax/Concrete/Literal.hs b/src/MiniJuvix/Syntax/Concrete/Literal.hs new file mode 100644 index 000000000..58f929139 --- /dev/null +++ b/src/MiniJuvix/Syntax/Concrete/Literal.hs @@ -0,0 +1,23 @@ +module MiniJuvix.Syntax.Concrete.Literal where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.Fixity +import Prettyprinter + +data Literal + = LitString Text + | LitInteger Integer + deriving stock (Show, Eq, Ord) + +instance HasAtomicity Literal where + atomicity = \case + LitInteger {} -> Atom + LitString {} -> Atom + +instance Pretty Literal where + pretty = \case + LitInteger n -> pretty n + LitString s -> ppStringLit s + where + ppStringLit :: Text -> Doc a + ppStringLit = dquotes . pretty diff --git a/src/MiniJuvix/Syntax/Concrete/Loc.hs b/src/MiniJuvix/Syntax/Concrete/Loc.hs index bb0c5f956..29dcfb152 100644 --- a/src/MiniJuvix/Syntax/Concrete/Loc.hs +++ b/src/MiniJuvix/Syntax/Concrete/Loc.hs @@ -3,7 +3,7 @@ module MiniJuvix.Syntax.Concrete.Loc where import MiniJuvix.Prelude import Prettyprinter -newtype Pos = Pos Word64 +newtype Pos = Pos {_unPos :: Word64 } deriving stock (Show, Eq, Ord) instance Semigroup Pos where @@ -16,12 +16,14 @@ data FileLoc = FileLoc { -- | Line number _locLine :: !Pos, -- | Column number - _locCol :: !Pos + _locCol :: !Pos, + -- | Offset wrt the start of the input. Used for syntax highlighting. + _locOffset :: !Pos } deriving stock (Show, Eq) instance Ord FileLoc where - compare (FileLoc l c) (FileLoc l' c') = compare (l, c) (l', c') + compare (FileLoc l c o) (FileLoc l' c' o') = compare (l, c, o) (l', c', o') data Loc = Loc { -- | Name of source file @@ -79,4 +81,6 @@ instance Pretty Interval where | otherwise = pretty s <> hyphen <> pretty e makeLenses ''Interval +makeLenses ''FileLoc makeLenses ''Loc +makeLenses ''Pos diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs new file mode 100644 index 000000000..128792b3f --- /dev/null +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs @@ -0,0 +1,85 @@ +module MiniJuvix.Syntax.Concrete.Scoped.Highlight where + +import MiniJuvix.Syntax.Concrete.Scoped.Name +import MiniJuvix.Syntax.Concrete.Loc +import qualified MiniJuvix.Internal.Strings as Str +import MiniJuvix.Prelude +import Prettyprinter +import Prettyprinter.Render.Text + +data Face = + FaceConstructor + | FaceInductive + | FaceFunction + | FaceModule + | FaceAxiom + +data Property = + PropertyFace Face + +data Instruction = + SetProperty { + _setPropertyInterval :: Interval, + _setPropertyProperty :: Property + } + +data SExp = + Symbol Text + | List [SExp] + | Quote SExp + | Int Word64 + +makeLenses ''Instruction + +go :: [Name] -> Text +go = renderSExp . progn . mapMaybe goName + +progn :: [SExp] -> SExp +progn l = List (Symbol "progn" : l) + +nameKindFace :: NameKind -> Maybe Face +nameKindFace = \case + KNameConstructor -> Just FaceConstructor + KNameInductive -> Just FaceInductive + KNameFunction -> Just FaceFunction + KNameTopModule -> Just FaceModule + KNameLocalModule -> Just FaceModule + KNameAxiom -> Just FaceAxiom + KNameLocal -> Nothing + +-- | Example instruction: +-- (add-text-properties 20 28 +-- '(face minijuvix-highlight-constructor-face)) +instr :: Interval -> Face -> SExp +instr i f = + List [Symbol "add-text-properties", start , end, face] + where + 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") + faceSymbolStr = case f of + FaceAxiom -> Str.axiom + FaceInductive -> Str.inductive + FaceConstructor -> Str.constructor + FaceModule -> Str.module_ + FaceFunction -> Str.function + +goName :: Name -> Maybe SExp +goName n = do + f <- nameKindFace (n ^. nameKind) + return (instr (getLoc n) f) + +renderSExp :: SExp -> Text +renderSExp = + renderStrict + . layoutPretty defaultLayoutOptions + . pretty + +instance Pretty SExp where + pretty = \case + Symbol s -> pretty s + Int s -> pretty s + List l -> parens (sep (map pretty l)) + Quote l -> pretty '`' <> pretty l diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs new file mode 100644 index 000000000..00809ead2 --- /dev/null +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs @@ -0,0 +1,48 @@ +-- | + +module MiniJuvix.Syntax.Concrete.Scoped.InfoTable where +import MiniJuvix.Prelude +import MiniJuvix.Syntax.Concrete.Language +import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S + +newtype FunctionInfo = FunctionInfo { + _functionInfoType :: Expression + } + +newtype ConstructorInfo = ConstructorInfo { + _constructorInfoType :: Expression + } + +data AxiomInfo = AxiomInfo { + _axiomInfoType :: Expression, + _axiomInfoBackends :: [BackendItem] + } + +newtype InductiveInfo = InductiveInfo { + _inductiveInfoDef :: InductiveDef 'Scoped + } + +data InfoTable = InfoTable { + _infoConstructors :: HashMap ConstructorRef ConstructorInfo, + _infoAxioms :: HashMap AxiomRef AxiomInfo, + _infoInductives :: HashMap InductiveRef InductiveInfo, + _infoFunctions :: HashMap FunctionRef FunctionInfo, + _infoFunctionClauses :: HashMap S.Symbol (FunctionClause 'Scoped), + _infoNames :: [S.Name] + } + +emptyInfoTable :: InfoTable +emptyInfoTable = InfoTable { + _infoConstructors = mempty, + _infoAxioms = mempty, + _infoInductives = mempty, + _infoFunctions = mempty, + _infoFunctionClauses = mempty, + _infoNames = mempty + } + +makeLenses ''InfoTable +makeLenses ''InductiveInfo +makeLenses ''ConstructorInfo +makeLenses ''AxiomInfo +makeLenses ''FunctionInfo diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs index 63d06e18e..9a4e6dfc4 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs @@ -1,8 +1,7 @@ -{-# LANGUAGE StandaloneKindSignatures #-} - module MiniJuvix.Syntax.Concrete.Scoped.Name ( module MiniJuvix.Syntax.Concrete.Scoped.Name, module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind, + module MiniJuvix.Syntax.NameId ) where @@ -12,9 +11,9 @@ import MiniJuvix.Prelude import MiniJuvix.Syntax.Concrete.Loc import qualified MiniJuvix.Syntax.Concrete.Name as C import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn +import MiniJuvix.Syntax.NameId import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind import qualified MiniJuvix.Syntax.Fixity as C -import Prettyprinter -------------------------------------------------------------------------------- -- Names @@ -24,12 +23,6 @@ data IsConcrete = NotConcrete | Concrete $(genSingletons [''IsConcrete]) -newtype NameId = NameId Word64 - deriving stock (Show, Eq, Ord, Generic) - -instance Pretty NameId where - pretty (NameId w) = pretty w - data AbsModulePath = AbsModulePath { absTopModulePath :: C.TopModulePath, absLocalPath :: [C.Symbol] @@ -62,8 +55,6 @@ allNameIds = NameId <$> ids ids = aux minBound aux i = Cons i (aux (succ i)) -instance Hashable NameId - -- | Why a symbol is in scope. data WhyInScope = -- | Inherited from the parent module. diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs index 91a62ca7b..a4786767c 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs @@ -422,7 +422,7 @@ ppName = case sing :: SStage s of SScoped -> ppCode instance PrettyCode S.NameId where - ppCode (S.NameId k) = return $ pretty k + ppCode (S.NameId k) = return (pretty k) annDef :: forall s. SingI s => SymbolType s -> Doc Ann -> Doc Ann annDef nm = case sing :: SStage s of @@ -673,7 +673,7 @@ instance PrettyCode Application where return $ l' <+> r' instance PrettyCode Literal where - ppCode l = case l of + ppCode = \case LitInteger n -> return $ annotate AnnLiteralInteger (pretty n) LitString s -> return $ ppStringLit s diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs index 5302a35d6..b32328f7e 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scope.hs @@ -1,9 +1,12 @@ -module MiniJuvix.Syntax.Concrete.Scoped.Scope where +module MiniJuvix.Syntax.Concrete.Scoped.Scope + ( module MiniJuvix.Syntax.Concrete.Scoped.Scope, + module MiniJuvix.Syntax.Concrete.Scoped.InfoTable ) +where import MiniJuvix.Prelude import MiniJuvix.Syntax.Concrete.Language +import MiniJuvix.Syntax.Concrete.Scoped.InfoTable import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S -import qualified Data.HashMap.Strict as HashMap newtype LocalVariable = LocalVariable { variableName :: S.Symbol @@ -36,41 +39,7 @@ data Scope = Scope deriving stock (Show) -newtype FunctionInfo = FunctionInfo { - _functionInfoType :: Expression - } - -newtype ConstructorInfo = ConstructorInfo { - _constructorInfoType :: Expression - } - -data AxiomInfo = AxiomInfo { - _axiomInfoType :: Expression, - _axiomInfoBackends :: [BackendItem] - } - -newtype InductiveInfo = InductiveInfo { - _inductiveInfoDef :: InductiveDef 'Scoped - } - -data InfoTable = InfoTable { - _infoConstructors :: HashMap ConstructorRef ConstructorInfo, - _infoAxioms :: HashMap AxiomRef AxiomInfo, - _infoInductives :: HashMap InductiveRef InductiveInfo, - _infoFunctions :: HashMap FunctionRef FunctionInfo - } - -instance Semigroup InfoTable where - (<>) = undefined -instance Monoid InfoTable where - mempty = undefined - makeLenses ''ExportInfo -makeLenses ''InfoTable -makeLenses ''InductiveInfo -makeLenses ''ConstructorInfo -makeLenses ''AxiomInfo -makeLenses ''FunctionInfo makeLenses ''SymbolInfo makeLenses ''LocalVars makeLenses ''Scope @@ -109,11 +78,3 @@ emptyScope absPath = _scopeTopModules = mempty, _scopeBindGroup = mempty } - -emptyInfoTable :: InfoTable -emptyInfoTable = InfoTable { - _infoConstructors = mempty, - _infoAxioms = mempty, - _infoInductives = mempty, - _infoFunctions = mempty - } diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs index 65c18668e..5557dc942 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs @@ -138,7 +138,7 @@ bindReservedSymbol s' entry = do Just SymbolInfo {..} -> SymbolInfo (HashMap.insert path entry _symbolInfo) bindSymbolOf :: - Members '[Error ScopeError, State ScoperState, State Scope] r => + Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r => S.NameKind -> (S.Name' () -> SymbolEntry) -> Symbol -> @@ -146,10 +146,11 @@ bindSymbolOf :: bindSymbolOf k e s = do s' <- reserveSymbolOf k s bindReservedSymbol s' (e (set S.nameConcrete () s')) + registerName (S.unqualifiedSymbol s') return s' bindFunctionSymbol :: - Members '[Error ScopeError, State ScoperState, State Scope] r => + Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r => Symbol -> Sem r S.Symbol bindFunctionSymbol = @@ -158,7 +159,7 @@ bindFunctionSymbol = (\s' -> EntryFunction (FunctionRef' s')) bindInductiveSymbol :: - Members '[Error ScopeError, State ScoperState, State Scope] r => + Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r => Symbol -> Sem r S.Symbol bindInductiveSymbol = @@ -167,7 +168,7 @@ bindInductiveSymbol = (\s' -> EntryInductive (InductiveRef' s')) bindAxiomSymbol :: - Members '[Error ScopeError, State ScoperState, State Scope] r => + Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r => Symbol -> Sem r S.Symbol bindAxiomSymbol = @@ -176,7 +177,7 @@ bindAxiomSymbol = (\s' -> EntryAxiom (AxiomRef' s')) bindConstructorSymbol :: - Members '[Error ScopeError, State ScoperState, State Scope] r => + Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r => Symbol -> Sem r S.Symbol bindConstructorSymbol = @@ -185,7 +186,7 @@ bindConstructorSymbol = (\s' -> EntryConstructor (ConstructorRef' s')) bindLocalModuleSymbol :: - Members '[Error ScopeError, State ScoperState, State Scope] r => + Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r => ExportInfo -> Module 'Scoped 'ModuleLocal -> Symbol -> @@ -307,29 +308,33 @@ lookupQualifiedSymbol (path, sym) = do ((fmap (^. moduleExportInfo) . HashMap.lookup topPath) >=> lookInExport sym remaining) <$> gets _scopeTopModules checkQualifiedExpr :: - Members '[Error ScopeError, State Scope, State ScoperState] r => + Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r => QualifiedName -> Sem r ScopedIden checkQualifiedExpr q@(QualifiedName (Path p) sym) = do es <- lookupQualifiedSymbol (toList p, sym) case es of [] -> notInScope - [e] -> return (entryToScopedIden q' e) + [e] -> entryToScopedIden q' e _ -> throw (ErrAmbiguousSym (AmbiguousSym q' es)) where q' = NameQualified q notInScope = throw (ErrQualSymNotInScope q) -entryToScopedIden :: Name -> SymbolEntry -> ScopedIden -entryToScopedIden name = \case - EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref) - EntryInductive ref -> - ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref) - EntryConstructor ref -> - ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref) - EntryFunction ref -> - ScopedFunction (set (functionRefName . S.nameConcrete) name ref) - EntryModule {} -> impossible +entryToScopedIden :: Members '[InfoTableBuilder] r => Name -> SymbolEntry -> Sem r ScopedIden +entryToScopedIden name e = do + let scopedName :: S.Name + scopedName = set S.nameConcrete name (entryName e) + registerName scopedName + return $ case e of + EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref) + EntryInductive ref -> + ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref) + EntryConstructor ref -> + ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref) + EntryFunction ref -> + ScopedFunction (set (functionRefName . S.nameConcrete) name ref) + EntryModule {} -> impossible -- | We gather all symbols which have been defined or marked to be public in the given scope. exportScope :: forall r. Members '[State Scope, Error ScopeError] r => Scope -> Sem r ExportInfo @@ -502,7 +507,9 @@ checkTopModule m@(Module path params body) = do _nameVisibilityAnn = VisPublic _nameWhyInScope = S.BecauseDefined _nameVerbatim = N.topModulePathToDottedPath path - return S.Name' {..} + moduleName = S.Name' {..} + -- registerName moduleName + return moduleName iniScope :: Scope iniScope = emptyScope (getTopModulePath m) checkedModule :: Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop) @@ -712,6 +719,7 @@ checkFunctionClause :: Sem r (FunctionClause 'Scoped) checkFunctionClause clause@FunctionClause {..} = do clauseOwnerFunction' <- checkTypeSigInScope + registerName (S.unqualifiedSymbol clauseOwnerFunction') (clausePatterns', clauseWhere', clauseBody') <- do clp <- mapM checkParsePatternAtom _clausePatterns withBindCurrentGroup $ do @@ -720,13 +728,12 @@ checkFunctionClause clause@FunctionClause {..} = do clb <- checkParseExpressionAtoms _clauseBody put s return (clp, clw, clb) - return - FunctionClause - { _clauseOwnerFunction = clauseOwnerFunction', - _clausePatterns = clausePatterns', - _clauseBody = clauseBody', - _clauseWhere = clauseWhere' - } + registerFunctionClause' FunctionClause + { _clauseOwnerFunction = clauseOwnerFunction', + _clausePatterns = clausePatterns', + _clauseBody = clauseBody', + _clauseWhere = clauseWhere' + } where fun = _clauseOwnerFunction checkTypeSigInScope :: Sem r S.Symbol @@ -852,7 +859,7 @@ checkLambdaClause LambdaClause {..} = do } checkUnqualified :: - Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r => + Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r => Symbol -> Sem r ScopedIden checkUnqualified s = do @@ -870,20 +877,22 @@ checkUnqualified s = do <$> lookupQualifiedSymbol ([], s) case entries of [] -> err - [x] -> return (entryToScopedIden n x) + [x] -> entryToScopedIden n x es -> throw (ErrAmbiguousSym (AmbiguousSym n es)) where n = NameUnqualified s checkPatternName :: forall r. - Members '[Error ScopeError, State Scope, State ScoperState] r => + Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r => Name -> Sem r PatternScopedIden checkPatternName n = do c <- getConstructorRef case c of - Just constr -> return (PatternScopedConstructor constr) -- the symbol is a constructor + Just constr -> do + registerName (constr ^. constructorRefName) + return (PatternScopedConstructor constr) -- the symbol is a constructor Nothing -> PatternScopedVar <$> groupBindLocalVariable sym -- the symbol is a variable where (path, sym) = case n of @@ -955,13 +964,13 @@ groupBindLocalVariable s = do return n checkPatternAtoms :: - Members '[Error ScopeError, State Scope, State ScoperState] r => + Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r => PatternAtoms 'Parsed -> Sem r (PatternAtoms 'Scoped) checkPatternAtoms (PatternAtoms s) = PatternAtoms <$> mapM checkPatternAtom s checkPatternAtom :: - Members '[Error ScopeError, State Scope, State ScoperState] r => + Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r => PatternAtom 'Parsed -> Sem r (PatternAtom 'Scoped) checkPatternAtom p = case p of @@ -971,7 +980,7 @@ checkPatternAtom p = case p of PatternAtomIden n -> PatternAtomIden <$> checkPatternName n checkName :: - Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r => + Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r => Name -> Sem r ScopedIden checkName n = case n of @@ -1037,13 +1046,13 @@ checkExpressionAtoms :: checkExpressionAtoms (ExpressionAtoms l) = ExpressionAtoms <$> mapM checkExpressionAtom l checkParseExpressionAtoms :: - Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder ] r => + Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder] r => ExpressionAtoms 'Parsed -> Sem r Expression checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms checkParsePatternAtom :: - Members '[Error ScopeError, State Scope, State ScoperState] r => + Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r => PatternAtom 'Parsed -> Sem r Pattern checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs index ae1abfb1b..96859732a 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs @@ -3,15 +3,16 @@ module MiniJuvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder where import qualified Data.HashMap.Strict as HashMap import MiniJuvix.Prelude import MiniJuvix.Syntax.Concrete.Language -import MiniJuvix.Syntax.Concrete.Language +import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S import MiniJuvix.Syntax.Concrete.Scoped.Scope -import MiniJuvix.Syntax.Concrete.Scoped.Name data InfoTableBuilder m a where RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m () RegisterConstructor :: InductiveConstructorDef 'Scoped -> InfoTableBuilder m () RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m () RegisterFunction :: TypeSignature 'Scoped -> InfoTableBuilder m () + RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m () + RegisterName :: S.Name -> InfoTableBuilder m () makeSem ''InfoTableBuilder @@ -32,36 +33,42 @@ registerAxiom' :: Member InfoTableBuilder r => AxiomDef 'Scoped -> Sem r (AxiomDef 'Scoped) registerAxiom' a = registerAxiom a $> a +registerFunctionClause' :: Member InfoTableBuilder r => + FunctionClause 'Scoped -> Sem r (FunctionClause 'Scoped) +registerFunctionClause' a = registerFunctionClause a $> a + toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a toState = reinterpret $ \case RegisterAxiom d -> - let ref = AxiomRef' (unqualifiedSymbol (d ^. axiomName)) + let ref = AxiomRef' (S.unqualifiedSymbol (d ^. axiomName)) info = AxiomInfo { _axiomInfoType = d ^. axiomType, _axiomInfoBackends = d ^. axiomBackendItems } in modify (over infoAxioms (HashMap.insert ref info)) RegisterConstructor c -> let - ref = ConstructorRef' (unqualifiedSymbol (c ^. constructorName)) + ref = ConstructorRef' (S.unqualifiedSymbol (c ^. constructorName)) info = ConstructorInfo { _constructorInfoType = c ^. constructorType } - in modify (over infoConstructors (HashMap.insert ref info) - ) + in modify (over infoConstructors (HashMap.insert ref info)) RegisterInductive ity -> let - ref = InductiveRef' (unqualifiedSymbol (ity ^. inductiveName)) + ref = InductiveRef' (S.unqualifiedSymbol (ity ^. inductiveName)) info = InductiveInfo { _inductiveInfoDef = ity } - in modify (over infoInductives (HashMap.insert ref info) - ) + in modify (over infoInductives (HashMap.insert ref info)) RegisterFunction f -> let - ref = FunctionRef' (unqualifiedSymbol (f ^. sigName)) + ref = FunctionRef' (S.unqualifiedSymbol (f ^. sigName)) info = FunctionInfo { _functionInfoType = f ^. sigType } - in modify (over infoFunctions (HashMap.insert ref info) - ) + in modify (over infoFunctions (HashMap.insert ref info)) + RegisterFunctionClause c -> let + key = c ^. clauseOwnerFunction + value = c + in modify (over infoFunctionClauses (HashMap.insert key value)) + RegisterName n -> modify (over infoNames (cons n)) runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a) runInfoTableBuilder = runState emptyInfoTable . toState diff --git a/src/MiniJuvix/Syntax/ForeignBlock.hs b/src/MiniJuvix/Syntax/ForeignBlock.hs new file mode 100644 index 000000000..e80c0a22c --- /dev/null +++ b/src/MiniJuvix/Syntax/ForeignBlock.hs @@ -0,0 +1,13 @@ +module MiniJuvix.Syntax.ForeignBlock where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.Backends + +data ForeignBlock = ForeignBlock + { _foreignBackend :: Backend, + _foreignCode :: Text + } + deriving stock (Eq, Ord, Show) + + +makeLenses ''ForeignBlock diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs new file mode 100644 index 000000000..7e7726671 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs @@ -0,0 +1,37 @@ +module MiniJuvix.Syntax.MicroJuvix.Error + ( module MiniJuvix.Syntax.MicroJuvix.Error, + module MiniJuvix.Syntax.MicroJuvix.Error.Pretty, + module MiniJuvix.Syntax.MicroJuvix.Error.Types, + ) +where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty +import qualified MiniJuvix.Syntax.MicroJuvix.Error.Pretty as P +import MiniJuvix.Syntax.MicroJuvix.Error.Types +import Prettyprinter + +data TypeCheckerError + = ErrTooManyPatterns TooManyPatterns + | ErrWrongConstructorType WrongConstructorType + | ErrWrongConstructorAppArgs WrongConstructorAppArgs + | ErrWrongType WrongType + | ErrExpectedFunctionType ExpectedFunctionType + +ppTypeCheckerError :: TypeCheckerError -> Doc Eann +ppTypeCheckerError = \case + ErrWrongConstructorType e -> ppError e + ErrTooManyPatterns e -> ppError e + ErrWrongConstructorAppArgs e -> ppError e + ErrWrongType e -> ppError e + ErrExpectedFunctionType e -> ppError e + +docStream :: TypeCheckerError -> SimpleDocStream Eann +docStream = layoutPretty defaultLayoutOptions . ppTypeCheckerError + +instance JuvixError TypeCheckerError where + renderAnsiText :: TypeCheckerError -> Text + renderAnsiText = renderAnsi . docStream + + renderText :: TypeCheckerError -> Text + renderText = P.renderText . docStream diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs new file mode 100644 index 000000000..350ff9756 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs @@ -0,0 +1,9 @@ +module MiniJuvix.Syntax.MicroJuvix.Error.Pretty + ( module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base, + module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi, + module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text) +where + +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs new file mode 100644 index 000000000..4de4d0da0 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs @@ -0,0 +1,16 @@ +module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi where + +import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as M + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base +import Prettyprinter +import Prettyprinter.Render.Terminal + +renderAnsi :: SimpleDocStream Eann -> Text +renderAnsi = renderStrict . reAnnotateS stylize + +stylize :: Eann -> AnsiStyle +stylize a = case a of + Highlight -> colorDull Red + MicroAnn m -> M.stylize m diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs new file mode 100644 index 000000000..856cad993 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs @@ -0,0 +1,65 @@ +module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base where + +import qualified MiniJuvix.Syntax.MicroJuvix.Pretty as M +import Prettyprinter +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Error.Types +import MiniJuvix.Syntax.MicroJuvix.Language + +data Eann = Highlight + | MicroAnn M.Ann + +ppCode :: M.PrettyCode c => c -> Doc Eann +ppCode = reAnnotate MicroAnn . M.runPrettyCode M.defaultOptions + +indent' :: Doc ann -> Doc ann +indent' = indent 2 + +prettyT :: Text -> Doc Eann +prettyT = pretty + +class PrettyError e where + ppError :: e -> Doc Eann + +instance PrettyError WrongConstructorType where + ppError e = "Type error during pattern matching." + <> line <> "The constructor" <+> (ppCode (e ^. wrongCtorTypeName)) <+> "has type:" + <> line <> indent' (ppCode (e ^. wrongCtorTypeActual)) + <> line <> "but is expected to have type:" + <> line <> indent' (ppCode (e ^. wrongCtorTypeExpected)) + +instance PrettyError WrongConstructorAppArgs where + ppError e = "Type error during pattern matching." + <> line <> "The constructor:" <+> ctorName <+> "is being matched against" <+> numPats <> ":" + <> line <> indent' (ppCode (e ^. wrongCtorAppApp)) + <> line <> "but is expected to be matched against" <+> numTypes <+> "with the following types:" + <> line <> indent' (hsep (ctorName : (ppCode <$> (e ^. wrongCtorAppTypes)))) + where + numPats :: Doc ann + numPats = pat (length (e ^. wrongCtorAppApp . constrAppParameters)) + numTypes :: Doc ann + numTypes = pat (length (e ^. wrongCtorAppTypes)) + ctorName :: Doc Eann + ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor) + pat :: Int -> Doc ann + pat n = pretty n <+> plural "pattern" "patterns" n + +instance PrettyError WrongType where + ppError e = "Type error." + <> line <> "The expression" <+> ppCode (e ^. wrongTypeExpression) <+> "has type:" + <> line <> indent' (ppCode (e ^. wrongTypeInferredType)) + <> line <> "but is expected to have type:" + <> line <> indent' (ppCode (e ^. wrongTypeExpectedType)) + +instance PrettyError ExpectedFunctionType where + ppError e = "Type error in the expression:" + <> line <> indent' (ppCode (e ^. expectedFunctionTypeExpression)) + <> line <> "the expression" <+> ppCode (e ^. expectedFunctionTypeApp) <+> "is expected to have a function type but has type:" + <> line <> indent' (ppCode (e ^. expectedFunctionTypeType)) + +instance PrettyError TooManyPatterns where + ppError e = "Type error in the definition of" <+> ppCode (e ^. tooManyPatternsClause . clauseName) <> "." + <> line <> "The function clause:" + <> line <> indent' (ppCode (e ^. tooManyPatternsClause)) + <> line <> "matches too many patterns. It should match the following types:" + <> line <> indent' (hsep (ppCode <$> (e ^. tooManyPatternsTypes))) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs new file mode 100644 index 000000000..83cdf4a7d --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs @@ -0,0 +1,9 @@ +module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base +import Prettyprinter +import Prettyprinter.Render.Text + +renderText :: SimpleDocStream Eann -> Text +renderText = renderStrict diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs new file mode 100644 index 000000000..7104e5595 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs @@ -0,0 +1,46 @@ +module MiniJuvix.Syntax.MicroJuvix.Error.Types where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Language + +-- | the type of the constructor used in a pattern does +-- not match the type of the inductive being matched +data WrongConstructorType = WrongConstructorType + { _wrongCtorTypeName :: Name, + _wrongCtorTypeExpected :: Type, + _wrongCtorTypeActual :: Type + } + +-- | the arguments of a constructor pattern do not match +-- the expected arguments of the constructor +data WrongConstructorAppArgs = WrongConstructorAppArgs + { _wrongCtorAppApp :: ConstructorApp, + _wrongCtorAppTypes :: [Type] + } + +-- | the type of an expression does not match the inferred type +data WrongType = WrongType + { _wrongTypeExpression :: Expression, + _wrongTypeExpectedType :: Type, + _wrongTypeInferredType :: Type + } + +-- | The left hand expression of a function application is not +-- a function type. +data ExpectedFunctionType = ExpectedFunctionType + { _expectedFunctionTypeExpression :: Expression, + _expectedFunctionTypeApp :: Expression, + _expectedFunctionTypeType :: Type + } + +-- | A function definition clause matches too many arguments +data TooManyPatterns = TooManyPatterns + { _tooManyPatternsClause :: FunctionClause, + _tooManyPatternsTypes :: [Type] + } + +makeLenses ''WrongConstructorType +makeLenses ''WrongConstructorAppArgs +makeLenses ''WrongType +makeLenses ''ExpectedFunctionType +makeLenses ''TooManyPatterns diff --git a/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs b/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs new file mode 100644 index 000000000..4c2a366a8 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs @@ -0,0 +1,52 @@ +module MiniJuvix.Syntax.MicroJuvix.InfoTable where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.Backends +import qualified Data.HashMap.Strict as HashMap + +data ConstructorInfo = ConstructorInfo { + _constructorInfoArgs :: [Type], + _constructorInfoInductive :: InductiveName + } + +data FunctionInfo = FunctionInfo { + _functionInfoType :: Type + } + +data AxiomInfo = AxiomInfo { + _axiomInfoType :: Type, + _axiomInfoBackends :: [BackendItem] + } + +data InfoTable = InfoTable { + _infoConstructors :: HashMap Name ConstructorInfo, + _infoAxioms :: HashMap Name AxiomInfo, + _infoFunctions :: HashMap Name FunctionInfo + } + +buildTable :: Module -> InfoTable +buildTable m = InfoTable {..} + where + _infoConstructors :: HashMap Name ConstructorInfo + _infoConstructors = HashMap.fromList + [ (c ^. constructorName, ConstructorInfo args ind) | + StatementInductive d <- ss, + let ind = d ^. inductiveName, + c <- d ^. inductiveConstructors, + let args = c ^. constructorParameters + ] + _infoFunctions :: HashMap Name FunctionInfo + _infoFunctions = HashMap.fromList + [ (f ^. funDefName, FunctionInfo (f ^. funDefType)) | + StatementFunction f <- ss] + _infoAxioms :: HashMap Name AxiomInfo + _infoAxioms = HashMap.fromList + [ (d ^. axiomName , AxiomInfo (d ^. axiomType) (d ^. axiomBackendItems)) + | StatementAxiom d <- ss ] + ss = m ^. moduleBody ^. moduleStatements + +makeLenses ''InfoTable +makeLenses ''FunctionInfo +makeLenses ''ConstructorInfo +makeLenses ''AxiomInfo diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs index 5d3fba9fe..df196139c 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs @@ -2,17 +2,23 @@ module MiniJuvix.Syntax.MicroJuvix.Language ( module MiniJuvix.Syntax.MicroJuvix.Language, module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind, module MiniJuvix.Syntax.Concrete.Scoped.Name, + module MiniJuvix.Syntax.Concrete.Literal, ) where import MiniJuvix.Prelude -import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..)) +import MiniJuvix.Syntax.ForeignBlock +import MiniJuvix.Syntax.Backends import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..)) import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind +import MiniJuvix.Syntax.Concrete.Literal import MiniJuvix.Syntax.Fixity +import Prettyprinter type FunctionName = Name +type AxiomName = Name + type VarName = Name type ConstrName = Name @@ -23,7 +29,9 @@ data Name = Name { _nameText :: Text, _nameId :: NameId, _nameKind :: NameKind + -- TODO: Add Location here so we can print out line numbers } + deriving stock (Show) makeLenses ''Name @@ -39,25 +47,39 @@ instance Hashable Name where instance HasNameKind Name where getNameKind = _nameKind +instance Pretty Name where + pretty = pretty . _nameText + data Module = Module { _moduleName :: Name, _moduleBody :: ModuleBody } data ModuleBody = ModuleBody - { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef), - _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef), - _moduleForeigns :: [Indexed ForeignBlock] + { _moduleStatements :: [Statement] + } + +data Statement = + StatementInductive InductiveDef + | StatementFunction FunctionDef + | StatementForeign ForeignBlock + | StatementAxiom AxiomDef + +data AxiomDef = AxiomDef + { _axiomName :: AxiomName, + _axiomType :: Type, + _axiomBackendItems :: [BackendItem] } data FunctionDef = FunctionDef { _funDefName :: FunctionName, - _funDefTypeSig :: Type, + _funDefType :: Type, _funDefClauses :: NonEmpty FunctionClause } data FunctionClause = FunctionClause - { _clausePatterns :: [Pattern], + { _clauseName :: FunctionName, + _clausePatterns :: [Pattern], _clauseBody :: Expression } @@ -65,20 +87,33 @@ data Iden = IdenFunction Name | IdenConstructor Name | IdenVar VarName + | IdenAxiom Name + deriving stock (Show) + +data TypedExpression = TypedExpression { + _typedType :: Type, + _typedExpression :: Expression + } + deriving stock (Show) data Expression = ExpressionIden Iden | ExpressionApplication Application + | ExpressionLiteral Literal + | ExpressionTyped TypedExpression + deriving stock (Show) data Application = Application { _appLeft :: Expression, _appRight :: Expression } + deriving stock (Show) data Function = Function { _funLeft :: Type, _funRight :: Type } + deriving stock (Show, Eq) -- | Fully applied constructor in a pattern. data ConstructorApp = ConstructorApp @@ -101,39 +136,30 @@ data InductiveConstructorDef = InductiveConstructorDef _constructorParameters :: [Type] } -newtype TypeIden +data TypeIden = TypeIdenInductive InductiveName + | TypeIdenAxiom AxiomName + deriving stock (Show, Eq) data Type = TypeIden TypeIden | TypeFunction Function + | TypeUniverse + | TypeAny + deriving stock (Show, Eq) makeLenses ''Module makeLenses ''Function makeLenses ''FunctionDef makeLenses ''FunctionClause makeLenses ''InductiveDef +makeLenses ''AxiomDef makeLenses ''ModuleBody makeLenses ''Application +makeLenses ''TypedExpression makeLenses ''InductiveConstructorDef makeLenses ''ConstructorApp -instance Semigroup ModuleBody where - a <> b = - ModuleBody - { _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives, - _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions, - _moduleForeigns = a ^. moduleForeigns <> b ^. moduleForeigns - } - -instance Monoid ModuleBody where - mempty = - ModuleBody - { _moduleInductives = mempty, - _moduleForeigns = mempty, - _moduleFunctions = mempty - } - instance HasAtomicity Application where atomicity = const (Aggregate appFixity) @@ -141,6 +167,8 @@ instance HasAtomicity Expression where atomicity e = case e of ExpressionIden {} -> Atom ExpressionApplication a -> atomicity a + ExpressionTyped t -> atomicity (t ^. typedExpression) + ExpressionLiteral l -> atomicity l instance HasAtomicity Function where atomicity = const (Aggregate funFixity) @@ -149,6 +177,8 @@ instance HasAtomicity Type where atomicity t = case t of TypeIden {} -> Atom TypeFunction f -> atomicity f + TypeUniverse -> Atom + TypeAny -> Atom instance HasAtomicity ConstructorApp where atomicity (ConstructorApp _ args) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs new file mode 100644 index 000000000..0f9cc47d6 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs @@ -0,0 +1,9 @@ +module MiniJuvix.Syntax.MicroJuvix.Pretty + ( module MiniJuvix.Syntax.MicroJuvix.Pretty.Base, + module MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi, + module MiniJuvix.Syntax.MicroJuvix.Pretty.Ann, + ) where + +import MiniJuvix.Syntax.MicroJuvix.Pretty.Base +import MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi +import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs index d112cb28d..ee1f28754 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs @@ -1,10 +1,10 @@ --- TODO handle capital letters and characters not supported by Haskell. module MiniJuvix.Syntax.MicroJuvix.Pretty.Base where import qualified MiniJuvix.Internal.Strings as Str import MiniJuvix.Prelude -import MiniJuvix.Syntax.Concrete.Language (Backend (..), ForeignBlock (..)) import MiniJuvix.Syntax.Fixity +import MiniJuvix.Syntax.Backends +import MiniJuvix.Syntax.ForeignBlock import MiniJuvix.Syntax.MicroJuvix.Language import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann import Prettyprinter @@ -22,6 +22,9 @@ defaultOptions = class PrettyCode c where ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann) +runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann +runPrettyCode opts = run . runReader opts . ppCode + instance PrettyCode Name where ppCode n = return $ @@ -34,6 +37,7 @@ instance PrettyCode Iden where IdenFunction na -> ppCode na IdenConstructor na -> ppCode na IdenVar na -> ppCode na + IdenAxiom a -> ppCode a instance PrettyCode Application where ppCode a = do @@ -41,10 +45,15 @@ instance PrettyCode Application where r' <- ppRightExpression appFixity (a ^. appRight) return $ l' <+> r' +instance PrettyCode TypedExpression where + ppCode e = ppCode (e ^. typedExpression) + instance PrettyCode Expression where - ppCode e = case e of + ppCode = \case ExpressionIden i -> ppCode i ExpressionApplication a -> ppCode a + ExpressionTyped a -> ppCode a + ExpressionLiteral l -> return (pretty l) keyword :: Text -> Doc Ann keyword = annotate AnnKeyword . pretty @@ -52,6 +61,9 @@ keyword = annotate AnnKeyword . pretty kwArrow :: Doc Ann kwArrow = keyword Str.toAscii +kwMapsto :: Doc Ann +kwMapsto = keyword Str.mapstoUnicode + kwForeign :: Doc Ann kwForeign = keyword Str.foreign_ @@ -61,6 +73,8 @@ kwAgda = keyword Str.agda kwGhc :: Doc Ann kwGhc = keyword Str.ghc +kwColon :: Doc Ann +kwColon = keyword Str.colon kwData :: Doc Ann kwData = keyword Str.data_ @@ -74,25 +88,47 @@ kwColonColon = keyword (Str.colon <> Str.colon) kwPipe :: Doc Ann kwPipe = keyword Str.pipe +kwAxiom :: Doc Ann +kwAxiom = keyword Str.axiom + kwWhere :: Doc Ann kwWhere = keyword Str.where_ kwModule :: Doc Ann kwModule = keyword Str.module_ +kwAny :: Doc Ann +kwAny = keyword Str.any + +kwType :: Doc Ann +kwType = keyword Str.type_ + kwWildcard :: Doc Ann kwWildcard = keyword Str.underscore +instance PrettyCode BackendItem where + ppCode BackendItem {..} = do + backend <- ppCode _backendItemBackend + return $ + backend <+> kwMapsto <+> pretty _backendItemCode + instance PrettyCode Function where ppCode (Function l r) = do l' <- ppLeftExpression funFixity l r' <- ppRightExpression funFixity r return $ l' <+> kwArrow <+> r' +instance PrettyCode TypeIden where + ppCode = \case + TypeIdenInductive i -> ppCode i + TypeIdenAxiom i -> ppCode i + instance PrettyCode Type where - ppCode t = case t of - TypeIden (TypeIdenInductive n) -> ppCode n + ppCode = \case + TypeIden i -> ppCode i TypeFunction f -> ppCode f + TypeUniverse -> return kwType + TypeAny -> return kwAny instance PrettyCode InductiveConstructorDef where ppCode c = do @@ -105,6 +141,14 @@ indent' d = do i <- asks _optIndent return $ indent i d +ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann) +ppBlock items = mapM ppCode items >>= bracesIndent . vsep . toList + +bracesIndent :: Members '[Reader Options] r => Doc Ann -> Sem r (Doc Ann) +bracesIndent d = do + d' <- indent' d + return $ braces (line <> d' <> line) + instance PrettyCode InductiveDef where ppCode d = do inductiveName' <- ppCode (d ^. inductiveName) @@ -127,16 +171,18 @@ instance PrettyCode Pattern where instance PrettyCode FunctionDef where ppCode f = do funDefName' <- ppCode (f ^. funDefName) - funDefTypeSig' <- ppCode (f ^. funDefTypeSig) - clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses) + funDefType' <- ppCode (f ^. funDefType) + clauses' <- mapM ppCode (f ^. funDefClauses) return $ - funDefName' <+> kwColonColon <+> funDefTypeSig' <> line + funDefName' <+> kwColonColon <+> funDefType' <> line <> vsep (toList clauses') - where - ppClause fun c = do - clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns) - clauseBody' <- ppCode (c ^. clauseBody) - return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody' + +instance PrettyCode FunctionClause where + ppCode c = do + funName <- ppCode (c ^. clauseName) + clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns) + clauseBody' <- ppCode (c ^. clauseBody) + return $ funName <+> hsep clausePatterns' <+> kwEquals <+> clauseBody' instance PrettyCode Backend where ppCode = \case @@ -152,13 +198,26 @@ instance PrettyCode ForeignBlock where <> line <> rbrace --- TODO Jonathan review +instance PrettyCode AxiomDef where + ppCode AxiomDef {..} = do + axiomName' <- ppCode _axiomName + axiomType' <- ppCode _axiomType + axiomBackendItems' <- case _axiomBackendItems of + [] -> return Nothing + bs -> Just <$> ppBlock bs + return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType' <+?> axiomBackendItems' + + +instance PrettyCode Statement where + ppCode = \case + StatementForeign f -> ppCode f + StatementFunction f -> ppCode f + StatementInductive f -> ppCode f + StatementAxiom f -> ppCode f + instance PrettyCode ModuleBody where ppCode m = do - types' <- mapM (mapM ppCode) (toList (m ^. moduleInductives)) - funs' <- mapM (mapM ppCode) (toList (m ^. moduleFunctions)) - foreigns' <- mapM (mapM ppCode) (toList (m ^. moduleForeigns)) - let everything = map (^. indexedThing) (sortOn (^. indexedIx) (types' ++ funs' ++ foreigns')) + everything <- mapM ppCode (m ^. moduleStatements) return $ vsep2 everything where vsep2 = concatWith (\a b -> a <> line <> line <> b) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Text.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Text.hs new file mode 100644 index 000000000..63b1fc50d --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Text.hs @@ -0,0 +1,29 @@ +module MiniJuvix.Syntax.MicroJuvix.Pretty.Text where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Pretty.Base +import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann +import Prettyprinter +import Prettyprinter.Render.Text + +printPrettyCodeDefault :: PrettyCode c => c -> IO () +printPrettyCodeDefault = printPrettyCode defaultOptions + +printPrettyCode :: PrettyCode c => Options -> c -> IO () +printPrettyCode = hPrintPrettyCode stdout + +hPrintPrettyCode :: PrettyCode c => Handle -> Options -> c -> IO () +hPrintPrettyCode h opts = renderIO h . docStream opts + +renderPrettyCodeDefault :: PrettyCode c => c -> Text +renderPrettyCodeDefault = renderStrict . docStream defaultOptions + +renderPrettyCode :: PrettyCode c => Options -> c -> Text +renderPrettyCode opts = renderStrict . docStream opts + +docStream :: PrettyCode c => Options -> c -> SimpleDocStream Ann +docStream opts = + layoutPretty defaultLayoutOptions + . run + . runReader opts + . ppCode diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs new file mode 100644 index 000000000..96c015a5b --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs @@ -0,0 +1,203 @@ +module MiniJuvix.Syntax.MicroJuvix.TypeChecker where +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.MicroJuvix.InfoTable +import qualified Data.HashMap.Strict as HashMap +import MiniJuvix.Syntax.MicroJuvix.Error + +type Err = Text + +newtype LocalVars = LocalVars { + _localTypes :: HashMap VarName Type + } + deriving newtype (Semigroup, Monoid) +makeLenses ''LocalVars + +checkModule :: Module -> Either TypeCheckerError Module +checkModule m = run $ runError $ runReader (buildTable m) (checkModule' m) + +checkModule' :: Members '[Reader InfoTable, Error TypeCheckerError] r => + Module -> Sem r Module +checkModule' Module {..} = do + _moduleBody' <- checkModuleBody _moduleBody + return Module { + _moduleBody = _moduleBody', + .. + } + +checkModuleBody :: Members '[Reader InfoTable, Error TypeCheckerError] r => + ModuleBody -> Sem r ModuleBody +checkModuleBody ModuleBody {..} = do + _moduleStatements' <- mapM checkStatement _moduleStatements + return ModuleBody { + _moduleStatements = _moduleStatements' + } + +checkStatement :: Members '[Reader InfoTable, Error TypeCheckerError] r => + Statement -> Sem r Statement +checkStatement s = case s of + StatementFunction fun -> StatementFunction <$> checkFunctionDef fun + StatementForeign {} -> return s + StatementInductive {} -> return s + StatementAxiom {} -> return s + +checkFunctionDef :: Members '[Reader InfoTable, Error TypeCheckerError] r => + FunctionDef -> Sem r FunctionDef +checkFunctionDef FunctionDef {..} = do + info <- lookupFunction _funDefName + _funDefClauses' <- mapM (checkFunctionClause info) _funDefClauses + return FunctionDef { + _funDefClauses = _funDefClauses', + .. + } + +checkExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r => + Type -> Expression -> Sem r Expression +checkExpression t e = do + t' <- inferExpression' e + let inferredType = t' ^. typedType + when (t /= inferredType) (throw (ErrWrongType (WrongType { _wrongTypeExpression = e, + _wrongTypeInferredType = inferredType, + _wrongTypeExpectedType = t}))) + return (ExpressionTyped t') + +inferExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r => + Expression -> Sem r Expression +inferExpression = fmap ExpressionTyped . inferExpression' + +lookupConstructor :: Member (Reader InfoTable) r => Name -> Sem r ConstructorInfo +lookupConstructor f = HashMap.lookupDefault impossible f <$> asks _infoConstructors + +lookupFunction :: Member (Reader InfoTable) r => Name -> Sem r FunctionInfo +lookupFunction f = HashMap.lookupDefault impossible f <$> asks _infoFunctions + +lookupAxiom :: Member (Reader InfoTable) r => Name -> Sem r AxiomInfo +lookupAxiom f = HashMap.lookupDefault impossible f <$> asks _infoAxioms + +lookupVar :: Member (Reader LocalVars) r => Name -> Sem r Type +lookupVar v = HashMap.lookupDefault impossible v <$> asks _localTypes + +constructorType :: Member (Reader InfoTable) r => Name -> Sem r Type +constructorType c = do + info <- lookupConstructor c + let r = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) + return (foldFunType (info ^. constructorInfoArgs) r) + +-- | [a, b] c ==> a -> (b -> c) +foldFunType :: [Type] -> Type -> Type +foldFunType l r = case l of + [] -> r + (a : as) -> TypeFunction (Function a (foldFunType as r)) + +-- | a -> (b -> c) ==> ([a, b], c) +unfoldFunType :: Type -> ([Type], Type) +unfoldFunType t = case t of + TypeFunction (Function l r) -> first (l:) (unfoldFunType r) + _ -> ([], t) + +checkFunctionClause :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r => + FunctionInfo -> FunctionClause -> Sem r FunctionClause +checkFunctionClause info clause@FunctionClause{..} = do + let (argTys, rty) = unfoldFunType (info ^. functionInfoType) + (patTys, restTys) = splitAt (length _clausePatterns) argTys + bodyTy = foldFunType restTys rty + when (length patTys /= length _clausePatterns) (throw (ErrTooManyPatterns (TooManyPatterns { + _tooManyPatternsClause = clause, + _tooManyPatternsTypes = patTys}))) + locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns + clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody) + return FunctionClause { + _clauseBody = clauseBody', + .. + } + +checkPattern :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r => + Type -> Pattern -> Sem r LocalVars +checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat + where + go :: Type -> Pattern -> Sem r [(VarName, Type)] + go ty p = case p of + PatternWildcard -> return [] + PatternVariable v -> return [(v, ty)] + PatternConstructorApp a -> do + info <- lookupConstructor (a ^. constrAppConstructor) + let inductiveTy = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) + when + (inductiveTy /= ty) + (throw + (ErrWrongConstructorType (WrongConstructorType (a ^. constrAppConstructor) ty inductiveTy))) + goConstr a + where + goConstr :: ConstructorApp -> Sem r [(VarName, Type)] + goConstr app@(ConstructorApp c ps) = do + tys <- (^. constructorInfoArgs) <$> lookupConstructor c + when + (length tys /= length ps) + (throw (ErrWrongConstructorAppArgs (appErr app tys))) + concat <$> zipWithM go tys ps + appErr :: ConstructorApp -> [Type] -> WrongConstructorAppArgs + appErr app tys = WrongConstructorAppArgs { _wrongCtorAppApp = app, + _wrongCtorAppTypes = tys} + +-- TODO currently equivalent to id +normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type +normalizeType t = case t of + TypeAny -> return TypeAny + TypeUniverse -> return TypeUniverse + TypeFunction f -> TypeFunction <$> normalizeFunction f + TypeIden i -> normalizeIden i + where + normalizeIden :: TypeIden -> Sem r Type + normalizeIden i = case i of + TypeIdenInductive {} -> return (TypeIden i) + TypeIdenAxiom {} -> return (TypeIden i) + normalizeFunction :: Function -> Sem r Function + normalizeFunction (Function l r) = do + l' <- normalizeType l + r' <- normalizeType r + return (Function l' r') + +inferExpression' :: forall r. Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r => + Expression -> Sem r TypedExpression +inferExpression' e = case e of + ExpressionIden i -> inferIden i + ExpressionApplication a -> inferApplication a + ExpressionTyped {} -> impossible + ExpressionLiteral l -> goLiteral l + where + goLiteral :: Literal -> Sem r TypedExpression + goLiteral l = return (TypedExpression TypeAny (ExpressionLiteral l)) + inferIden :: Iden -> Sem r TypedExpression + inferIden i = case i of + IdenFunction fun -> do + info <- lookupFunction fun + return (TypedExpression (info ^. functionInfoType) (ExpressionIden i)) + IdenConstructor c -> do + ty <- constructorType c + return (TypedExpression ty (ExpressionIden i)) + IdenVar v -> do + ty <- lookupVar v + return (TypedExpression ty (ExpressionIden i)) + IdenAxiom v -> do + info <- lookupAxiom v + return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i)) + inferApplication :: Application -> Sem r TypedExpression + inferApplication a = do + let leftExp = a ^. appLeft + l <- inferExpression' leftExp + fun <- getFunctionType leftExp (l ^. typedType) + r <- checkExpression (fun ^. funLeft) (a ^. appRight) + return TypedExpression { + _typedExpression = ExpressionApplication Application { + _appLeft = ExpressionTyped l, + _appRight = r + }, + _typedType = fun ^. funRight + } + where + getFunctionType :: Expression -> Type -> Sem r Function + getFunctionType appExp t = case t of + TypeFunction f -> return f + _ -> throw (ErrExpectedFunctionType (ExpectedFunctionType { _expectedFunctionTypeExpression = e, + _expectedFunctionTypeApp = appExp, + _expectedFunctionTypeType = t})) diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Language.hs b/src/MiniJuvix/Syntax/MiniHaskell/Language.hs index 87b6dbc24..38f2690df 100644 --- a/src/MiniJuvix/Syntax/MiniHaskell/Language.hs +++ b/src/MiniJuvix/Syntax/MiniHaskell/Language.hs @@ -1,13 +1,15 @@ module MiniJuvix.Syntax.MiniHaskell.Language ( module MiniJuvix.Syntax.MiniHaskell.Language, module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind, - module MiniJuvix.Syntax.Concrete.Scoped.Name, + module MiniJuvix.Syntax.NameId, + module MiniJuvix.Syntax.Concrete.Literal, ) where import MiniJuvix.Prelude -import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..)) +import MiniJuvix.Syntax.NameId import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind +import MiniJuvix.Syntax.Concrete.Literal import MiniJuvix.Syntax.Fixity type FunctionName = Name @@ -22,6 +24,7 @@ data Name = Name { _nameText :: Text, _nameKind :: NameKind } + deriving stock (Show) makeLenses ''Name @@ -32,71 +35,88 @@ data Module = Module { _moduleName :: Name, _moduleBody :: ModuleBody } + deriving stock (Show) newtype ModuleBody = ModuleBody { _moduleStatements :: [Statement] } + deriving stock (Show) deriving newtype (Monoid, Semigroup) data Statement - = StatementInductiveDef InductiveDef - | StatementFunctionDef FunctionDef + = StatementInductive InductiveDef + | StatementFunction FunctionDef + | StatementVerbatim Text + deriving stock (Show) data FunctionDef = FunctionDef { _funDefName :: FunctionName, - _funDefTypeSig :: Type, + _funDefType :: Type, _funDefClauses :: NonEmpty FunctionClause } + deriving stock (Show) data FunctionClause = FunctionClause { _clausePatterns :: [Pattern], _clauseBody :: Expression } + deriving stock (Show) type Iden = Name data Expression = ExpressionIden Iden | ExpressionApplication Application - --- TODO Add a constructor for literals + | ExpressionLiteral Literal + | ExpressionVerbatim Text + deriving stock (Show) data Application = Application { _appLeft :: Expression, _appRight :: Expression } + deriving stock (Show) data Function = Function { _funLeft :: Type, _funRight :: Type } + deriving stock (Show) -- | Fully applied constructor in a pattern. data ConstructorApp = ConstructorApp { _constrAppConstructor :: Name, _constrAppParameters :: [Pattern] } + deriving stock (Show) data Pattern = PatternVariable VarName | PatternConstructorApp ConstructorApp | PatternWildcard + deriving stock (Show) data InductiveDef = InductiveDef { _inductiveName :: InductiveName, _inductiveConstructors :: [InductiveConstructorDef] } + deriving stock (Show) data InductiveConstructorDef = InductiveConstructorDef { _constructorName :: ConstrName, _constructorParameters :: [Type] } + deriving stock (Show) -type TypeIden = InductiveName +data TypeIden + = TypeIdenInductive InductiveName + deriving stock (Show) data Type = TypeIden TypeIden | TypeFunction Function + | TypeVerbatim Text + deriving stock (Show) makeLenses ''Module makeLenses ''Function @@ -115,6 +135,8 @@ instance HasAtomicity Expression where atomicity e = case e of ExpressionIden {} -> Atom ExpressionApplication a -> atomicity a + ExpressionVerbatim {} -> Atom + ExpressionLiteral l -> atomicity l instance HasAtomicity Function where atomicity = const (Aggregate funFixity) @@ -123,6 +145,7 @@ instance HasAtomicity Type where atomicity t = case t of TypeIden {} -> Atom TypeFunction f -> atomicity f + TypeVerbatim {} -> Atom instance HasAtomicity ConstructorApp where atomicity (ConstructorApp _ args) diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs index 3b6cec309..cfe61686f 100644 --- a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs @@ -37,6 +37,8 @@ instance PrettyCode Expression where ppCode e = case e of ExpressionIden i -> ppCode i ExpressionApplication a -> ppCode a + ExpressionVerbatim c -> return (pretty c) + ExpressionLiteral l -> ppCode l keyword :: Text -> Doc Ann keyword = annotate AnnKeyword . pretty @@ -71,10 +73,15 @@ instance PrettyCode Function where r' <- ppRightExpression funFixity r return $ l' <+> kwArrow <+> r' +instance PrettyCode TypeIden where + ppCode = \case + TypeIdenInductive t -> ppCode t + instance PrettyCode Type where ppCode t = case t of TypeIden n -> ppCode n TypeFunction f -> ppCode f + TypeVerbatim c -> return (pretty c) instance PrettyCode InductiveConstructorDef where ppCode c = do @@ -109,7 +116,7 @@ instance PrettyCode Pattern where instance PrettyCode FunctionDef where ppCode f = do funDefName' <- ppCode (f ^. funDefName) - funDefTypeSig' <- ppCode (f ^. funDefTypeSig) + funDefTypeSig' <- ppCode (f ^. funDefType) clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses) return $ funDefName' <+> kwColonColon <+> funDefTypeSig' <> line @@ -122,8 +129,9 @@ instance PrettyCode FunctionDef where instance PrettyCode Statement where ppCode = \case - StatementFunctionDef f -> ppCode f - StatementInductiveDef d -> ppCode d + StatementFunction f -> ppCode f + StatementInductive d -> ppCode d + StatementVerbatim t -> return (pretty t) instance PrettyCode ModuleBody where ppCode m = do @@ -132,6 +140,21 @@ instance PrettyCode ModuleBody where where vsep2 = concatWith (\a b -> a <> line <> line <> b) +instance PrettyCode Literal where + ppCode = \case + LitInteger n -> return $ annotate AnnLiteralInteger (pretty n) + LitString s -> return $ ppStringLit s + +doubleQuotes :: Doc Ann -> Doc Ann +doubleQuotes = enclose kwDQuote kwDQuote + +kwDQuote :: Doc Ann +kwDQuote = pretty ("\"" :: Text) + +ppStringLit :: Text -> Doc Ann +ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty + + instance PrettyCode Module where ppCode m = do name' <- ppCode (m ^. moduleName) diff --git a/src/MiniJuvix/Syntax/NameId.hs b/src/MiniJuvix/Syntax/NameId.hs new file mode 100644 index 000000000..a74b32757 --- /dev/null +++ b/src/MiniJuvix/Syntax/NameId.hs @@ -0,0 +1,15 @@ +module MiniJuvix.Syntax.NameId where + +import Prettyprinter +import MiniJuvix.Prelude + +newtype NameId = NameId { + _unNameId :: Word64 + } + deriving stock (Show, Eq, Ord, Generic) +makeLenses ''NameId + +instance Pretty NameId where + pretty (NameId w) = pretty w + +instance Hashable NameId diff --git a/src/MiniJuvix/Syntax/Universe.hs b/src/MiniJuvix/Syntax/Universe.hs index c88afc7cf..0e787a77f 100644 --- a/src/MiniJuvix/Syntax/Universe.hs +++ b/src/MiniJuvix/Syntax/Universe.hs @@ -4,9 +4,11 @@ import MiniJuvix.Prelude import MiniJuvix.Syntax.Fixity newtype Universe = Universe - { universeLevel :: Maybe Natural + { _universeLevel :: Maybe Natural } deriving stock (Show, Eq, Ord) instance HasAtomicity Universe where atomicity = const Atom + +makeLenses ''Universe diff --git a/src/MiniJuvix/Termination/CallGraph.hs b/src/MiniJuvix/Termination/CallGraph.hs index 3c9eb5dfe..80b261ae1 100644 --- a/src/MiniJuvix/Termination/CallGraph.hs +++ b/src/MiniJuvix/Termination/CallGraph.hs @@ -63,11 +63,11 @@ composeEdge a b = do _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices) } -fromFunCall :: FunctionName -> FunCall -> Call +fromFunCall :: FunctionRef -> FunCall -> Call fromFunCall caller fc = Call - { _callFrom = caller, - _callTo = fc ^. callName, + { _callFrom = S.nameUnqualify (caller ^. functionRefName), + _callTo = S.nameUnqualify (fc ^. callRef . functionRefName), _callMatrix = map fst (fc ^. callArgs) } diff --git a/src/MiniJuvix/Termination/CallMap.hs b/src/MiniJuvix/Termination/CallMap.hs index d023f28b2..32f26ec66 100644 --- a/src/MiniJuvix/Termination/CallMap.hs +++ b/src/MiniJuvix/Termination/CallMap.hs @@ -7,8 +7,8 @@ where import qualified Data.HashMap.Strict as HashMap import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.Language.Extra -import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S import MiniJuvix.Termination.Types +import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol) -- | i = SizeInfo [v] ⇔ v is smaller than argument i of the caller function. -- Indexes are 0 based @@ -55,23 +55,23 @@ viewCall e = case e of return (Just (singletonCall x)) _ -> return Nothing where - singletonCall :: Name -> FunCall - singletonCall n = FunCall (S.nameUnqualify n) [] + singletonCall :: FunctionRef -> FunCall + singletonCall r = FunCall r [] -addCall :: FunctionName -> FunCall -> CallMap -> CallMap +addCall :: FunctionRef -> FunCall -> CallMap -> CallMap addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun) where - insertCall :: FunCall -> Maybe (HashMap FunctionName [FunCall]) -> HashMap FunctionName [FunCall] + insertCall :: FunCall -> Maybe (HashMap FunctionRef [FunCall]) -> HashMap FunctionRef [FunCall] insertCall f m = case m of Nothing -> singl f Just m' -> addFunCall f m' - singl :: FunCall -> HashMap FunctionName [FunCall] - singl f = HashMap.singleton (f ^. callName) [f] - addFunCall :: FunCall -> HashMap FunctionName [FunCall] -> HashMap FunctionName [FunCall] - addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callName) [fc] + singl :: FunCall -> HashMap FunctionRef [FunCall] + singl f = HashMap.singleton (f ^. callRef) [f] + addFunCall :: FunCall -> HashMap FunctionRef [FunCall] -> HashMap FunctionRef [FunCall] + addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callRef) [fc] registerCall :: - Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => + Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => FunCall -> Sem r () registerCall c = do @@ -86,18 +86,21 @@ checkModule m = checkModuleBody (m ^. moduleBody) checkModuleBody :: Members '[State CallMap] r => ModuleBody -> Sem r () checkModuleBody body = do - mapM_ (checkFunctionDef . (^. indexedThing)) (toList $ body ^. moduleFunctions) - mapM_ (checkLocalModule . (^. indexedThing)) (toList $ body ^. moduleLocalModules) + mapM_ checkFunctionDef moduleFunctions + mapM_ checkLocalModule moduleLocalModules + where + moduleFunctions = [ f | StatementFunction f <- body ^. moduleStatements ] + moduleLocalModules = [ f | StatementLocalModule f <- body ^. moduleStatements ] checkLocalModule :: Members '[State CallMap] r => LocalModule -> Sem r () checkLocalModule m = checkModuleBody (m ^. moduleBody) checkFunctionDef :: Members '[State CallMap] r => FunctionDef -> Sem r () -checkFunctionDef def = runReader (def ^. funDefName) $ do +checkFunctionDef def = runReader (FunctionRef (unqualifiedSymbol (def ^. funDefName))) $ do checkTypeSignature (def ^. funDefTypeSig) mapM_ checkFunctionClause (def ^. funDefClauses) -checkTypeSignature :: Members '[State CallMap, Reader FunctionName] r => Expression -> Sem r () +checkTypeSignature :: Members '[State CallMap, Reader FunctionRef] r => Expression -> Sem r () checkTypeSignature = runReader (emptySizeInfo :: SizeInfo) . checkExpression emptySizeInfo :: SizeInfo @@ -117,14 +120,14 @@ mkSizeInfo ps = SizeInfo {..} ] checkFunctionClause :: - Members '[State CallMap, Reader FunctionName] r => + Members '[State CallMap, Reader FunctionRef] r => FunctionClause -> Sem r () checkFunctionClause cl = runReader (mkSizeInfo (cl ^. clausePatterns)) $ checkExpression (cl ^. clauseBody) -checkExpression :: Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => Expression -> Sem r () +checkExpression :: Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => Expression -> Sem r () checkExpression e = do mc <- viewCall e case mc of @@ -139,7 +142,7 @@ checkExpression e = do ExpressionLiteral {} -> return () checkApplication :: - Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => + Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => Application -> Sem r () checkApplication (Application l r) = do @@ -147,7 +150,7 @@ checkApplication (Application l r) = do checkExpression r checkFunction :: - Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => + Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => Function -> Sem r () checkFunction (Function l r) = do @@ -155,7 +158,7 @@ checkFunction (Function l r) = do checkExpression r checkFunctionParameter :: - Members '[State CallMap, Reader FunctionName, Reader SizeInfo] r => + Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => FunctionParameter -> Sem r () checkFunctionParameter p = checkExpression (p ^. paramType) diff --git a/src/MiniJuvix/Termination/Types.hs b/src/MiniJuvix/Termination/Types.hs index 294e52698..9e19c0ce9 100644 --- a/src/MiniJuvix/Termination/Types.hs +++ b/src/MiniJuvix/Termination/Types.hs @@ -11,14 +11,16 @@ import MiniJuvix.Syntax.Abstract.Pretty.Base import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S import MiniJuvix.Termination.Types.SizeRelation import Prettyprinter as PP +import MiniJuvix.Syntax.Abstract.Language (functionRefName) +import MiniJuvix.Syntax.Concrete.Scoped.Name (nameUnqualify) newtype CallMap = CallMap - { _callMap :: HashMap A.FunctionName (HashMap A.FunctionName [FunCall]) + { _callMap :: HashMap A.FunctionRef (HashMap A.FunctionRef [FunCall]) } deriving newtype (Semigroup, Monoid) data FunCall = FunCall - { _callName :: A.FunctionName, + { _callRef :: A.FunctionRef, _callArgs :: [(CallRow, A.Expression)] } @@ -46,7 +48,7 @@ instance PrettyCode FunCall where ppCode :: forall r. Members '[Reader Options] r => FunCall -> Sem r (Doc Ann) ppCode (FunCall f args) = do args' <- mapM ppArg args - f' <- ppSCode f + f' <- ppCode f return $ f' <+> hsep args' where ppArg :: (CallRow, A.Expression) -> Sem r (Doc Ann) @@ -72,9 +74,9 @@ instance PrettyCode CallMap where ppCode :: forall r. Members '[Reader Options] r => CallMap -> Sem r (Doc Ann) ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m) where - ppEntry :: (A.FunctionName, HashMap A.FunctionName [FunCall]) -> Sem r (Doc Ann) + ppEntry :: (A.FunctionRef, HashMap A.FunctionRef [FunCall]) -> Sem r (Doc Ann) ppEntry (fun, mcalls) = do - fun' <- annotate AnnImportant <$> ppSCode fun + fun' <- annotate AnnImportant <$> ppCode fun calls' <- vsep <$> mapM ppCode calls return $ fun' <+> waveFun <+> align calls' where @@ -99,4 +101,4 @@ instance PrettyCode CallMatrix where ppCode l = vsep <$> mapM ppCode l filterCallMap :: Foldable f => f Text -> CallMap -> CallMap -filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText k `elem` funNames)) +filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText (nameUnqualify (k ^. functionRefName)) `elem` funNames)) diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs index e49d4dfc4..0021f9516 100644 --- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs +++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs @@ -1,10 +1,10 @@ module MiniJuvix.Translation.AbstractToMicroJuvix where -import qualified Data.HashMap.Strict as HashMap import MiniJuvix.Prelude import qualified MiniJuvix.Syntax.Abstract.Language.Extra as A import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.Universe import qualified MiniJuvix.Syntax.Usage as A translateModule :: A.TopModule -> Module @@ -25,42 +25,40 @@ goSymbol s = Name { _nameText = S.symbolText s, _nameId = S._nameId s, - _nameKind = getNameKind s - } + _nameKind = getNameKind s } unsupported :: Text -> a -unsupported thing = error ("Not yet supported: " <> thing) +unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing) goImport :: A.TopModule -> ModuleBody goImport m = goModuleBody (m ^. A.moduleBody) goModuleBody :: A.ModuleBody -> ModuleBody -goModuleBody b - | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules" - | otherwise = - ModuleBody - { _moduleInductives = - HashMap.fromList - [ (d ^. indexedThing . inductiveName, d) - | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives)) - ], - _moduleFunctions = - HashMap.fromList - [ (f ^. indexedThing . funDefName, f) - | f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions)) - ], - _moduleForeigns = b ^. A.moduleForeigns - } +goModuleBody b = ModuleBody (map goStatement (b ^. A.moduleStatements)) --- <> mconcatMap goImport (b ^. A.moduleImports) +goStatement :: A.Statement -> Statement +goStatement = \case + A.StatementAxiom d -> StatementAxiom (goAxiomDef d) + A.StatementForeign f -> StatementForeign f + A.StatementFunction f -> StatementFunction (goFunctionDef f) + A.StatementImport {} -> unsupported "imports" + A.StatementLocalModule {} -> unsupported "local modules" + A.StatementInductive i -> StatementInductive (goInductiveDef i) goTypeIden :: A.Iden -> TypeIden goTypeIden i = case i of A.IdenFunction {} -> unsupported "functions in types" A.IdenConstructor {} -> unsupported "constructors in types" A.IdenVar {} -> unsupported "type variables" - A.IdenInductive d -> TypeIdenInductive (goName d) - A.IdenAxiom {} -> unsupported "axioms in types" + A.IdenInductive d -> TypeIdenInductive (goName (d ^. A.inductiveRefName)) + A.IdenAxiom a -> TypeIdenAxiom (goName (a ^. A.axiomRefName)) + +goAxiomDef :: A.AxiomDef -> AxiomDef +goAxiomDef a = + AxiomDef { + _axiomName = goSymbol (a ^. A.axiomName), + _axiomType = goType (a ^. A.axiomType), + _axiomBackendItems = a ^. A.axiomBackendItems } goFunctionParameter :: A.FunctionParameter -> Type goFunctionParameter f = case f ^. A.paramName of @@ -75,15 +73,19 @@ goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r) goFunctionDef :: A.FunctionDef -> FunctionDef goFunctionDef f = FunctionDef - { _funDefName = goSymbol (f ^. A.funDefName), - _funDefTypeSig = goType (f ^. A.funDefTypeSig), - _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses) + { _funDefName = _funDefName', + _funDefType = goType (f ^. A.funDefTypeSig), + _funDefClauses = fmap (goFunctionClause _funDefName') (f ^. A.funDefClauses) } + where + _funDefName' :: Name + _funDefName' = goSymbol (f ^. A.funDefName) -goFunctionClause :: A.FunctionClause -> FunctionClause -goFunctionClause c = +goFunctionClause :: Name -> A.FunctionClause -> FunctionClause +goFunctionClause n c = FunctionClause - { _clausePatterns = map goPattern (c ^. A.clausePatterns), + { _clauseName = n, + _clausePatterns = map goPattern (c ^. A.clausePatterns), _clauseBody = goExpression (c ^. A.clauseBody) } @@ -97,13 +99,18 @@ goPattern p = case p of goConstructorApp :: A.ConstructorApp -> ConstructorApp goConstructorApp c = ConstructorApp - (goName (c ^. A.constrAppConstructor)) + (goName (c ^. A.constrAppConstructor . A.constructorRefName)) (map goPattern (c ^. A.constrAppParameters)) +goTypeUniverse :: Universe -> Type +goTypeUniverse u + | 0 == fromMaybe 0 (u ^. universeLevel) = TypeUniverse + | otherwise = unsupported "big universes" + goType :: A.Expression -> Type goType e = case e of A.ExpressionIden i -> TypeIden (goTypeIden i) - A.ExpressionUniverse {} -> unsupported "universes in types" + A.ExpressionUniverse u -> goTypeUniverse u A.ExpressionApplication {} -> unsupported "application in types" A.ExpressionFunction f -> TypeFunction (goFunction f) A.ExpressionLiteral {} -> unsupported "literals in types" @@ -113,10 +120,10 @@ goApplication (A.Application f x) = Application (goExpression f) (goExpression x goIden :: A.Iden -> Iden goIden i = case i of - A.IdenFunction n -> IdenFunction (goName n) - A.IdenConstructor c -> IdenConstructor (goName c) + A.IdenFunction n -> IdenFunction (goName (n ^. A.functionRefName)) + A.IdenConstructor c -> IdenConstructor (goName (c ^. A.constructorRefName)) A.IdenVar v -> IdenVar (goSymbol v) - A.IdenAxiom {} -> unsupported "axiom identifier" + A.IdenAxiom a -> IdenAxiom (goName (a ^. A.axiomRefName)) A.IdenInductive {} -> unsupported "inductive identifier" goExpression :: A.Expression -> Expression @@ -125,7 +132,7 @@ goExpression e = case e of A.ExpressionUniverse {} -> unsupported "universes in expression" A.ExpressionFunction {} -> unsupported "function type in expressions" A.ExpressionApplication a -> ExpressionApplication (goApplication a) - A.ExpressionLiteral {} -> unsupported "literals in expression" + A.ExpressionLiteral l -> ExpressionLiteral l goInductiveDef :: A.InductiveDef -> InductiveDef goInductiveDef i = case i ^. A.inductiveType of @@ -152,7 +159,7 @@ viewExpressionFunctionType e = case e of A.ExpressionFunction f -> first toList (viewFunctionType f) A.ExpressionIden i -> ([], TypeIden (goTypeIden i)) A.ExpressionApplication {} -> unsupported "application in a type" - A.ExpressionUniverse {} -> unsupported "universe in a type" + A.ExpressionUniverse {} -> ([], TypeUniverse) A.ExpressionLiteral {} -> unsupported "literal in a type" viewFunctionType :: A.Function -> (NonEmpty Type, Type) diff --git a/src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs b/src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs new file mode 100644 index 000000000..73438b32c --- /dev/null +++ b/src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs @@ -0,0 +1,196 @@ +module MiniJuvix.Translation.MicroJuvixToMiniHaskell where +import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Prelude +import qualified MiniJuvix.Syntax.MiniHaskell.Language as H +import MiniJuvix.Syntax.MicroJuvix.InfoTable +import MiniJuvix.Syntax.ForeignBlock +import MiniJuvix.Syntax.Backends +import MiniJuvix.Syntax.NameId +import Prettyprinter +import qualified Data.Text as Text + +translateModule :: Module -> Either Err H.Module +translateModule m = run (runError (runReader table (goModule m))) + where + table = buildTable m + +type Err = Text + +goModule :: Members '[Error Err, Reader InfoTable] r => Module -> Sem r H.Module +goModule Module {..} = do + _moduleBody' <- goModuleBody _moduleBody + return H.Module { + _moduleName = goName (_moduleName), + _moduleBody = _moduleBody' + } + +unsupported :: Text -> a +unsupported msg = error $ msg <> " not yet supported" + +goModuleBody :: Members '[Error Err, Reader InfoTable] r => + ModuleBody -> Sem r H.ModuleBody +goModuleBody ModuleBody {..} = + H.ModuleBody <$> mapMaybeM goStatement _moduleStatements + +goStatement :: Members '[Error Err, Reader InfoTable] r => Statement -> Sem r (Maybe H.Statement) +goStatement = \case + StatementInductive d -> Just . H.StatementInductive <$> goInductive d + StatementFunction d -> Just . H.StatementFunction <$> goFunctionDef d + StatementForeign d -> return (goForeign d) + StatementAxiom {} -> return Nothing + +goForeign :: ForeignBlock -> Maybe H.Statement +goForeign b = case b ^. foreignBackend of + BackendGhc -> Just (H.StatementVerbatim (b ^. foreignCode)) + _ -> Nothing + +lookupAxiom :: Members '[Error Err, Reader InfoTable] r => Name -> Sem r AxiomInfo +lookupAxiom n = + fromMaybe impossible . (^. infoAxioms . at n) <$> ask + +goIden :: Members '[Error Err, Reader InfoTable] r => Iden -> Sem r H.Expression +goIden = \case + IdenFunction fun -> return (goName' fun) + IdenConstructor c -> return (goName' c) + IdenVar v -> return (goName' v) + IdenAxiom a -> H.ExpressionVerbatim <$> goAxiomIden a + +throwErr :: Member (Error Err) r => Text -> Sem r a +throwErr = throw + +goAxiomIden :: Members '[Error Err, Reader InfoTable] r => Name -> Sem r Text +goAxiomIden n = do + backends <- (^. axiomInfoBackends) <$> lookupAxiom n + case firstJust getCode backends of + Nothing -> throwErr ("ghc does not support this primitive:" <> show (pretty n)) + Just t -> return t + where + getCode :: BackendItem -> Maybe Text + getCode b = + guard (BackendGhc == b ^. backendItemBackend) + $> b ^. backendItemCode + +goName' :: Name -> H.Expression +goName' = H.ExpressionIden . goName + +goName :: Name -> H.Name +goName n = H.Name { + _nameText = goNameText n, + _nameKind = n ^. nameKind + } + +goNameText :: Name -> Text +goNameText n = + adaptFirstLetter lexeme <> "_" <> show (n ^. nameId . unNameId) + where + lexeme + | Text.null lexeme' = "v" + | otherwise = lexeme' + where + lexeme' = Text.filter isValidChar (n ^. nameText) + isValidChar :: Char -> Bool + isValidChar c = isLetter c && isAscii c + adaptFirstLetter :: Text -> Text + adaptFirstLetter t = case Text.uncons t of + Nothing -> impossible + Just (h, r) -> Text.cons (capitalize h) r + where + capitalize :: Char -> Char + capitalize + | capital = toUpper + | otherwise = toLower + capital = case n ^. nameKind of + KNameConstructor -> True + KNameInductive -> True + KNameTopModule -> True + KNameLocalModule -> True + _ -> False + +goFunctionDef :: Members '[Error Err, Reader InfoTable] r => FunctionDef -> Sem r H.FunctionDef +goFunctionDef FunctionDef {..} = do + _funDefType' <- goType _funDefType + _funDefClauses' <- mapM goFunctionClause _funDefClauses + return H.FunctionDef { + _funDefName = goName _funDefName, + _funDefType = _funDefType', + _funDefClauses = _funDefClauses' + } + +goPattern :: Pattern -> H.Pattern +goPattern = \case + PatternVariable v -> H.PatternVariable (goName v) + PatternConstructorApp a -> H.PatternConstructorApp (goConstructorApp a) + PatternWildcard -> H.PatternWildcard + +goConstructorApp :: ConstructorApp -> H.ConstructorApp +goConstructorApp c = H.ConstructorApp { + _constrAppConstructor = goName (c ^. constrAppConstructor), + _constrAppParameters = map goPattern (c ^. constrAppParameters) + } + +goExpression :: Members '[Error Err, Reader InfoTable] r => + Expression -> Sem r H.Expression +goExpression = \case + ExpressionIden i -> goIden i + ExpressionTyped t -> goExpression (t ^. typedExpression) + ExpressionApplication a -> H.ExpressionApplication <$> goApplication a + ExpressionLiteral l -> return (H.ExpressionLiteral l) + +goApplication :: Members '[Error Err, Reader InfoTable] r => + Application -> Sem r H.Application +goApplication Application {..} = do + _appLeft' <- goExpression _appLeft + _appRight' <- goExpression _appRight + return H.Application { + _appLeft = _appLeft', + _appRight = _appRight' + } + +goFunctionClause :: Members '[Error Err, Reader InfoTable] r => + FunctionClause -> Sem r H.FunctionClause +goFunctionClause FunctionClause {..} = do + _clauseBody' <- goExpression _clauseBody + let _clausePatterns' = map goPattern _clausePatterns + return H.FunctionClause { + _clauseBody = _clauseBody', + _clausePatterns = _clausePatterns' + } + +goInductive :: Members '[Error Err, Reader InfoTable] r => + InductiveDef -> Sem r H.InductiveDef +goInductive InductiveDef {..} = do + _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors + return H.InductiveDef { + _inductiveName = goName _inductiveName, + _inductiveConstructors = _inductiveConstructors' + } + +goConstructorDef :: Members '[Error Err, Reader InfoTable] r => + InductiveConstructorDef -> Sem r H.InductiveConstructorDef +goConstructorDef InductiveConstructorDef {..} = do + _constructorParameters' <- mapM goType _constructorParameters + return H.InductiveConstructorDef { + _constructorName = goName _constructorName, + _constructorParameters = _constructorParameters' + } + +goFunction :: Members '[Error Err, Reader InfoTable] r => Function -> Sem r H.Function +goFunction Function {..} = do + _funLeft' <- goType _funLeft + _funRight' <- goType _funRight + return H.Function { + _funLeft = _funLeft', + _funRight = _funRight' + } + +goTypeIden :: Members '[Error Err, Reader InfoTable] r => TypeIden -> Sem r H.Type +goTypeIden = \case + TypeIdenInductive n -> return (H.TypeIden (H.TypeIdenInductive (goName n))) + TypeIdenAxiom n -> H.TypeVerbatim <$> goAxiomIden n + +goType :: Members '[Error Err, Reader InfoTable] r => Type -> Sem r H.Type +goType = \case + TypeIden t -> goTypeIden t + TypeFunction f -> H.TypeFunction <$> goFunction f + TypeUniverse -> throwErr "MiniHaskell: universes in types not supported" + TypeAny -> impossible diff --git a/src/MiniJuvix/Translation/ScopedToAbstract.hs b/src/MiniJuvix/Translation/ScopedToAbstract.hs index 5fb963d6f..7fd924a98 100644 --- a/src/MiniJuvix/Translation/ScopedToAbstract.hs +++ b/src/MiniJuvix/Translation/ScopedToAbstract.hs @@ -1,88 +1,82 @@ module MiniJuvix.Translation.ScopedToAbstract where -import qualified Data.HashMap.Strict as HashMap import MiniJuvix.Prelude import qualified MiniJuvix.Syntax.Abstract.Language as A import MiniJuvix.Syntax.Concrete.Language import qualified MiniJuvix.Syntax.Concrete.Language as C import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S +import MiniJuvix.Syntax.Abstract.InfoTableBuilder +import MiniJuvix.Syntax.Abstract.Language (FunctionDef(_funDefTypeSig)) type Err = Text unsupported :: Members '[Error Err] r => Err -> Sem r a -unsupported msg = throw $ msg <> " not yet supported" +unsupported msg = throw $ msg <> "Scoped to Abstract: not yet supported" -translateModule :: Module 'Scoped 'ModuleTop -> Either Err A.TopModule -translateModule = run . runError . goTopModule +translateModule :: Module 'Scoped 'ModuleTop -> Either Err (InfoTable, A.TopModule) +translateModule = run . runError . runInfoTableBuilder . goTopModule -goTopModule :: Members '[Error Err] r => Module 'Scoped 'ModuleTop -> Sem r A.TopModule +goTopModule :: Members '[Error Err, InfoTableBuilder] r => Module 'Scoped 'ModuleTop -> Sem r A.TopModule goTopModule = goModule -goLocalModule :: Members '[Error Err] r => Module 'Scoped 'ModuleLocal -> Sem r A.LocalModule +goLocalModule :: Members '[Error Err, InfoTableBuilder] r => Module 'Scoped 'ModuleLocal -> Sem r A.LocalModule goLocalModule = goModule -goModule :: (Members '[Error Err] r, ModulePathType 'Scoped t ~ S.Name' c) => Module 'Scoped t -> Sem r (A.Module c) +goModule :: (Members '[Error Err, InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) => Module 'Scoped t -> Sem r (A.Module c) goModule (Module n par b) = case par of [] -> A.Module n <$> goModuleBody b _ -> unsupported "Module parameters" -goModuleBody :: forall r. Members '[Error Err] r => [Statement 'Scoped] -> Sem r A.ModuleBody +goModuleBody :: forall r. Members '[Error Err, InfoTableBuilder] r + => [Statement 'Scoped] -> Sem r A.ModuleBody goModuleBody ss' = do - _moduleInductives <- inductives - _moduleLocalModules <- locals - _moduleFunctions <- functions - _moduleImports <- imports - _moduleForeigns <- foreigns + otherThanFunctions <- mapMaybeM goStatement ss + functions <- map (fmap A.StatementFunction) <$> compiledFunctions + let _moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx) + (otherThanFunctions <> functions)) return A.ModuleBody {..} where ss :: [Indexed (Statement 'Scoped)] ss = zipWith Indexed [0 ..] ss' - inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef)) - inductives = + compiledFunctions :: Sem r [Indexed A.FunctionDef] + compiledFunctions = sequence $ - HashMap.fromList - [ (def ^. inductiveName, Indexed i <$> goInductive def) - | Indexed i (StatementInductive def) <- ss - ] - locals :: Sem r (HashMap A.InductiveName (Indexed A.LocalModule)) - locals = - sequence $ - HashMap.fromList - [ (m ^. modulePath, Indexed i <$> goLocalModule m) - | Indexed i (StatementModule m) <- ss - ] - foreigns :: Sem r [Indexed ForeignBlock] - foreigns = - return - [ Indexed i f - | Indexed i (StatementForeign f) <- ss - ] - imports :: Sem r [Indexed A.TopModule] - imports = - sequence $ - [ Indexed i <$> goModule m - | Indexed i (StatementImport (Import m)) <- ss - ] - functions :: Sem r (HashMap A.FunctionName (Indexed A.FunctionDef)) - functions = do - sequence $ - HashMap.fromList - [ (name, Indexed i <$> funDef) + [ Indexed i <$> funDef | Indexed i sig <- sigs, let name = sig ^. sigName, - let clauses = mapM goFunctionClause (getClauses name), - let funDef = liftA2 (A.FunctionDef name) (goExpression (sig ^. sigType)) clauses - ] + let funDef = goFunctionDef sig (getClauses name) ] where getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped) getClauses name = fromMaybe impossible $ nonEmpty - [ c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction - ] + [ c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction ] sigs :: [Indexed (TypeSignature 'Scoped)] sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss] +goStatement :: forall r. Members '[Error Err, InfoTableBuilder] r + => Indexed (Statement 'Scoped) -> Sem r (Maybe (Indexed A.Statement)) +goStatement (Indexed idx s) = fmap (Indexed idx) <$> case s of + StatementAxiom d -> Just . A.StatementAxiom <$> goAxiom d + StatementImport (Import t) -> Just . A.StatementImport <$> goModule t + StatementOperator {} -> return Nothing + StatementOpenModule {} -> return Nothing + StatementEval {} -> unsupported "eval statements" + StatementPrint {} -> unsupported "print statements" + StatementInductive i -> Just . A.StatementInductive <$> goInductive i + StatementForeign f -> return (Just (A.StatementForeign f)) + StatementModule f -> Just . A.StatementLocalModule <$> goLocalModule f + StatementTypeSignature {} -> return Nothing + StatementFunctionClause {} -> return Nothing + + +goFunctionDef :: forall r. Members '[Error Err, InfoTableBuilder] r => TypeSignature 'Scoped -> NonEmpty (FunctionClause 'Scoped) -> Sem r A.FunctionDef +goFunctionDef sig clauses = do + let _funDefName = sig ^. sigName + _funDefClauses <- mapM goFunctionClause clauses + _funDefTypeSig <- goExpression (sig ^. sigType) + registerFunction' A.FunctionDef {..} + goFunctionClause :: forall r. Members '[Error Err] r => FunctionClause 'Scoped -> Sem r A.FunctionClause goFunctionClause FunctionClause {..} = do _clausePatterns' <- mapM goPattern _clausePatterns @@ -109,25 +103,27 @@ goInductiveParameter InductiveParameter {..} = do _paramUsage = UsageOmega } -goInductive :: Members '[Error Err] r => InductiveDef 'Scoped -> Sem r A.InductiveDef +goInductive :: Members '[Error Err, InfoTableBuilder] r => InductiveDef 'Scoped -> Sem r A.InductiveDef goInductive InductiveDef {..} = do _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters _inductiveType' <- sequence $ goExpression <$> _inductiveType _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors - return - A.InductiveDef - { _inductiveParameters = _inductiveParameters', - _inductiveName = _inductiveName, - _inductiveType = _inductiveType', - _inductiveConstructors = _inductiveConstructors' - } + inductiveInfo <- registerInductive A.InductiveDef + { _inductiveParameters = _inductiveParameters', + _inductiveName = _inductiveName, + _inductiveType = _inductiveType', + _inductiveConstructors = _inductiveConstructors' + } + + forM_ _inductiveConstructors' (registerConstructor inductiveInfo) + + return (inductiveInfo ^. inductiveInfoDef) goConstructorDef :: Members '[Error Err] r => InductiveConstructorDef 'Scoped -> Sem r A.InductiveConstructorDef goConstructorDef (InductiveConstructorDef c ty) = A.InductiveConstructorDef c <$> goExpression ty goExpression :: forall r. Members '[Error Err] r => Expression -> Sem r A.Expression goExpression e = case e of - -- TODO: Continue here ExpressionIdentifier nt -> return (goIden nt) ExpressionParensIdentifier nt -> return (goIden nt) ExpressionApplication a -> A.ExpressionApplication <$> goApplication a @@ -142,11 +138,11 @@ goExpression e = case e of where goIden :: C.ScopedIden -> A.Expression goIden x = A.ExpressionIden $ case x of - ScopedAxiom a -> A.IdenAxiom (a ^. C.axiomRefName) - ScopedInductive i -> A.IdenInductive (i ^. C.inductiveRefName) + ScopedAxiom a -> A.IdenAxiom (A.AxiomRef (a ^. C.axiomRefName)) + ScopedInductive i -> A.IdenInductive (A.InductiveRef (i ^. C.inductiveRefName)) ScopedVar v -> A.IdenVar v - ScopedFunction fun -> A.IdenFunction (fun ^. C.functionRefName) - ScopedConstructor c -> A.IdenConstructor (c ^. C.constructorRefName) + ScopedFunction fun -> A.IdenFunction (A.FunctionRef (fun ^. C.functionRefName)) + ScopedConstructor c -> A.IdenConstructor (A.ConstructorRef (c ^. C.constructorRefName)) goApplication :: Application -> Sem r A.Application goApplication (Application l r) = do @@ -200,19 +196,19 @@ goInfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternInfix goPostfixPatternApplication :: forall r. Members '[Error Err] r => PatternPostfixApp -> Sem r A.ConstructorApp goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPostfixApplication a) -viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.Name, [A.Pattern]) +viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.ConstructorRef, [A.Pattern]) viewApp p = case p of - PatternConstructor c -> return (c ^. constructorRefName, []) + PatternConstructor c -> return (goConstructorRef c, []) PatternApplication (PatternApp l r) -> do r' <- goPattern r second (`snoc` r') <$> viewApp l PatternInfixApplication (PatternInfixApp l c r) -> do l' <- goPattern l r' <- goPattern r - return (c ^. constructorRefName, [l', r']) + return (goConstructorRef c, [l', r']) PatternPostfixApplication (PatternPostfixApp l c) -> do l' <- goPattern l - return (c ^. constructorRefName, [l']) + return (goConstructorRef c, [l']) PatternVariable {} -> err PatternWildcard {} -> err PatternEmpty {} -> err @@ -220,6 +216,9 @@ viewApp p = case p of err :: Sem r a err = throw ("constructor expected on the left of a pattern application" :: Err) +goConstructorRef :: ConstructorRef -> A.ConstructorRef +goConstructorRef (ConstructorRef' n) = A.ConstructorRef n + goPattern :: forall r. Members '[Error Err] r => Pattern -> Sem r A.Pattern goPattern p = case p of PatternVariable a -> return $ A.PatternVariable a @@ -230,7 +229,7 @@ goPattern p = case p of PatternWildcard -> return A.PatternWildcard PatternEmpty -> return A.PatternEmpty -goAxiom :: Members '[Error Err] r => AxiomDef 'Scoped -> Sem r A.AxiomDef -goAxiom (AxiomDef n m bs) = do - e <- goExpression m - return (A.AxiomDef n e bs) +goAxiom :: Members '[Error Err, InfoTableBuilder] r => AxiomDef 'Scoped -> Sem r A.AxiomDef +goAxiom (AxiomDef {..}) = do + _axiomType' <- goExpression _axiomType + registerAxiom' A.AxiomDef { _axiomType = _axiomType', ..} diff --git a/test/Base.hs b/test/Base.hs index f66ccd062..53b800649 100644 --- a/test/Base.hs +++ b/test/Base.hs @@ -9,8 +9,10 @@ import Test.Tasty import Test.Tasty.HUnit import MiniJuvix.Prelude import qualified MiniJuvix.Syntax.Concrete.Language as M +import qualified MiniJuvix.Syntax.Abstract.Language as A import qualified MiniJuvix.Syntax.Concrete.Parser as M import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M +import qualified MiniJuvix.Translation.ScopedToAbstract as A parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop) parseModuleIO = fromRightIO id . M.runModuleParserIO @@ -21,6 +23,9 @@ parseTextModuleIO = fromRightIO id . return . M.runModuleParser "literal string" scopeModuleIO :: M.Module 'M.Parsed 'M.ModuleTop -> IO (M.Module 'M.Scoped 'M.ModuleTop) scopeModuleIO = fmap snd . fromRightIO' printErrorAnsi . M.scopeCheck1IO "." +translateModuleIO :: M.Module 'M.Scoped 'M.ModuleTop -> IO A.TopModule +translateModuleIO = fmap snd . fromRightIO id . return . A.translateModule + data AssertionDescr = Single Assertion | Steps ((String -> IO ()) -> Assertion) diff --git a/test/Main.hs b/test/Main.hs index f0c9b0941..d2f4bd982 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -2,12 +2,14 @@ module Main (main) where import Base +import qualified TypeCheck import qualified Scope negatives :: TestTree negatives = testGroup "MiniJuvix tests" $ [ - Scope.allTests + Scope.allTests, + TypeCheck.allTests ] allTests :: TestTree diff --git a/test/TypeCheck.hs b/test/TypeCheck.hs new file mode 100644 index 000000000..052d06ba7 --- /dev/null +++ b/test/TypeCheck.hs @@ -0,0 +1,7 @@ +module TypeCheck (allTests) where + +import Base +import qualified TypeCheck.Negative as N + +allTests :: TestTree +allTests = testGroup "TypeCheck tests" [N.allTests] diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs new file mode 100644 index 000000000..f068293b0 --- /dev/null +++ b/test/TypeCheck/Negative.hs @@ -0,0 +1,64 @@ +module TypeCheck.Negative (allTests) where + +import Base +import MiniJuvix.Syntax.MicroJuvix.Error +import qualified MiniJuvix.Syntax.MicroJuvix.TypeChecker as T +import qualified MiniJuvix.Translation.AbstractToMicroJuvix as A + +type FailMsg = String + +data NegTest = NegTest + { name :: String, + relDir :: FilePath, + file :: FilePath, + checkErr :: TypeCheckerError -> Maybe FailMsg } + +testDescr :: NegTest -> TestDescr +testDescr NegTest {..} = TestDescr { + testName = name, + testRoot = root relDir, + testAssertion = Single $ do + p <- parseModuleIO file + >>= scopeModuleIO + >>= translateModuleIO + >>| A.translateModule + >>| T.checkModule + + case p of + Left err -> whenJust (checkErr err) assertFailure + Right _ -> assertFailure "The type checker did not find an error." + } + +allTests :: TestTree +allTests = testGroup "TypeCheck negative tests" + (map (mkTest . testDescr) tests) + +root :: FilePath +root = "tests/negative" + +wrongError :: Maybe FailMsg +wrongError = Just "Incorrect error" + +tests :: [NegTest] +tests = [ + NegTest "Constructor in pattern type error" "MicroJuvix" + "PatternConstructor.mjuvix" $ \case + ErrWrongConstructorType {} -> Nothing + _ -> wrongError + , NegTest "Constructor pattern length mismatch" "MicroJuvix" + "PatternConstructorApp.mjuvix" $ \case + ErrWrongConstructorAppArgs {} -> Nothing + _ -> wrongError + , NegTest "Type vs inferred type mismatch" "MicroJuvix" + "WrongType.mjuvix" $ \case + ErrWrongType {} -> Nothing + _ -> wrongError + , NegTest "Function application with non-function type" "MicroJuvix" + "ExpectedFunctionType.mjuvix" $ \case + ErrExpectedFunctionType {} -> Nothing + _ -> wrongError + , NegTest "Function definition clause with two many match patterns" "MicroJuvix" + "TooManyPatterns.mjuvix" $ \case + ErrTooManyPatterns {} -> Nothing + _ -> wrongError + ] diff --git a/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix b/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix new file mode 100644 index 000000000..5b37fb6a0 --- /dev/null +++ b/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix @@ -0,0 +1,12 @@ +module ExpectedFunctionType; + inductive A { + a : A; + }; + + inductive B { + b : B; + }; + + f : A; + f ≔ a b; +end; diff --git a/tests/negative/MicroJuvix/PatternConstructor.mjuvix b/tests/negative/MicroJuvix/PatternConstructor.mjuvix new file mode 100644 index 000000000..20fe40383 --- /dev/null +++ b/tests/negative/MicroJuvix/PatternConstructor.mjuvix @@ -0,0 +1,13 @@ +module PatternConstructor; + inductive A { + a : A; + }; + + inductive B { + b : B; + }; + + f : A → B; + f b ≔ b; + +end; diff --git a/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix b/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix new file mode 100644 index 000000000..96d9474bb --- /dev/null +++ b/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix @@ -0,0 +1,13 @@ +module PatternConstructorApp; + inductive A { + a : A -> A; + }; + + inductive B { + b : B; + }; + + f : A → B; + f (a x _) ≔ b; + +end; diff --git a/tests/negative/MicroJuvix/TooManyPatterns.mjuvix b/tests/negative/MicroJuvix/TooManyPatterns.mjuvix new file mode 100644 index 000000000..446ec489e --- /dev/null +++ b/tests/negative/MicroJuvix/TooManyPatterns.mjuvix @@ -0,0 +1,8 @@ +module TooManyPatterns; + inductive A { + a : A; + }; + + f : A -> A; + f a _ ≔ a; +end; diff --git a/tests/negative/MicroJuvix/WrongType.mjuvix b/tests/negative/MicroJuvix/WrongType.mjuvix new file mode 100644 index 000000000..d3e6111a7 --- /dev/null +++ b/tests/negative/MicroJuvix/WrongType.mjuvix @@ -0,0 +1,12 @@ +module WrongType; + inductive A { + a : A; + }; + + inductive B { + b : B; + }; + + f : A; + f ≔ b; +end; diff --git a/tests/positive/MicroJuvix/Simple.mjuvix b/tests/positive/MicroJuvix/Simple.mjuvix new file mode 100644 index 000000000..5788c80e6 --- /dev/null +++ b/tests/positive/MicroJuvix/Simple.mjuvix @@ -0,0 +1,44 @@ +module Simple; + inductive T { + tt : T; + }; + + someT : T; + someT ≔ tt; + + inductive Bool { + false : Bool; + true : Bool; + }; + + + inductive Nat { + zero : Nat; + suc : Nat → Nat; + }; + + infix 3 ==; + == : Nat → Nat → Bool; + == zero zero ≔ true; + == (suc a) (suc b) ≔ a == b; + == _ _ ≔ false; + + infixl 4 +; + + : Nat → Nat → Nat; + + zero b ≔ b; + + (suc a) b ≔ suc (a + b); + + infixr 5 ∷; + inductive List { + nil : List; + ∷ : Nat → List → List; + }; + + foldr : (Nat → Nat → Nat) → Nat → List → Nat; + foldr _ v nil ≔ v; + foldr f v (a ∷ as) ≔ f a (foldr f v as); + + sum : List → Nat; + sum ≔ foldr (+) zero; + +end; \ No newline at end of file diff --git a/tests/positive/MiniHaskell/HelloWorld.mjuvix b/tests/positive/MiniHaskell/HelloWorld.mjuvix new file mode 100644 index 000000000..fe3aaaa27 --- /dev/null +++ b/tests/positive/MiniHaskell/HelloWorld.mjuvix @@ -0,0 +1,49 @@ +module HelloWorld; + +inductive ℕ { + zero : ℕ; + suc : ℕ → ℕ; +}; + +inductive V { + zeroV : V; + sucV : V; +}; + + +infixl 6 +; ++ : ℕ → ℕ → ℕ; ++ zero b ≔ b; ++ (suc a) b ≔ suc (a + b); + +infixl 7 *; +* : ℕ → ℕ → ℕ; +* zero b ≔ zero; +* (suc a) b ≔ b + (a * b); + +axiom Action : Type { + ghc ↦ "IO ()"; +}; + +infixl 1 >>; +axiom >> : Action → Action → Action { + ghc ↦ "(>>)"; +}; + +axiom String : Type; + +axiom putStr : String → Action { + ghc ↦ "putStrLn"; +}; + +doTimes : ℕ → Action → Action; +doTimes zero _ ≔ putStr "done"; +doTimes (suc n) a ≔ a >> doTimes n a; + +three : ℕ; +three ≔ suc (suc (suc zero)); + +main : Action; +main := doTimes three (putStr "hello world"); + +end; diff --git a/tests/positive/StdlibList/Data/Bool.mjuvix b/tests/positive/StdlibList/Data/Bool.mjuvix index f4e666011..a10e90af5 100644 --- a/tests/positive/StdlibList/Data/Bool.mjuvix +++ b/tests/positive/StdlibList/Data/Bool.mjuvix @@ -8,14 +8,14 @@ module Data.Bool; not true ≔ false; not false ≔ true; - infixr 2 ||; - || : Bool → Bool → Bool; - || false a ≔ a; - || true _ ≔ true; + -- infixr 2 ||; + -- || : Bool → Bool → Bool; + -- || false a ≔ a; + -- || true _ ≔ true; - infixr 2 &&; - && : Bool → Bool → Bool; - && false _ ≔ false; - && true a ≔ a; + -- infixr 2 &&; + -- && : Bool → Bool → Bool; + -- && false _ ≔ false; + -- && true a ≔ a; -end; \ No newline at end of file +end; diff --git a/tests/positive/VP/SimpleFungibleToken.mjuvix b/tests/positive/VP/SimpleFungibleToken.mjuvix new file mode 100644 index 000000000..0d283c2f0 --- /dev/null +++ b/tests/positive/VP/SimpleFungibleToken.mjuvix @@ -0,0 +1,150 @@ +module SimpleFungibleToken; + +axiom String : Type { + ghc ↦ "[Char]"; +}; + +axiom Int : Type { + ghc ↦ "Int"; +}; + +inductive OptionInt { + Nothing : OptionInt; + Just : Int -> OptionInt; +}; + +inductive OptionString { + NothingString : OptionString; + JustString : String -> OptionString; +}; + +foreign ghc { defaultinteger = 0;}; + +axiom defaultinteger : Int { + ghc ↦ "defaultinteger"; +}; + +fromOptionInt : OptionInt -> Int; +fromOptionInt Nothing := defaultinteger; + +fromOptionInt (Just n) := n; + +foreign ghc { +foreign import ccall "read_pre" read_pre :: String -> Maybe Int +foreign import ccall "read_post" read_post :: String -> Maybe Int +foreign import ccall "is_balance_key" is_balance_key :: String -> String -> Maybe String +}; + +axiom read-pre : String -> OptionInt { + ghc ↦ "read_pre"; +}; + +axiom read-post : String -> OptionInt { + ghc ↦ "read_post"; +}; + +axiom is-balance-key : String -> String -> OptionString { + ghc ↦ "is_balance_key"; +}; + +inductive ListString { + Nil : ListString; + Cons : String -> ListString -> ListString; +}; + +inductive Bool { + true : Bool; + false : Bool; +}; + +infixr 2 ||; +|| : Bool → Bool → Bool; +|| false a ≔ a; +|| true _ ≔ true; + +and : Bool → Bool → Bool; +and false _ ≔ false; +and true a ≔ a; + +infix 4 ==String; +axiom ==String : String -> String -> Bool { + ghc ↦ "(==)"; +}; + +infix 4 ==Int; +axiom ==Int : Int -> Int -> Bool { + ghc ↦ "(==)"; +}; + + +elem : String -> ListString -> Bool; +elem s Nil := false; +elem s (Cons x xs) := (s ==String x) || elem s xs; + +inductive PairIntBool { + MakePair : Int -> Bool -> PairIntBool; +}; + +ifthenelse : Bool -> PairIntBool -> PairIntBool -> PairIntBool; +ifthenelse true case1 _ := case1; +ifthenelse false _ case2 := case2; + +infix 4 <; +axiom < : Int -> Int -> Bool { + ghc ↦ "(<)"; +}; + +infixl 6 -; +axiom - : Int -> Int -> Int { + ghc ↦ "(-)"; +}; + +infixl 6 +; +axiom + : Int -> Int -> Int { + ghc ↦ "(+)"; +}; + +check-vp : ListString -> String -> String -> Int -> PairIntBool; +check-vp verifiers key owner change := + ifthenelse + (((fromOptionInt (read-post key)) - (fromOptionInt (read-pre key))) < 0) + (MakePair (change + ((fromOptionInt (read-post key)) - (fromOptionInt (read-pre key)))) + (elem owner verifiers)) + (MakePair + (change + + ((fromOptionInt (read-post key)) - (fromOptionInt (read-pre key)))) + true); + +check-vp' : ListString -> String -> Int -> String -> PairIntBool; +check-vp' verifiers key change owner := check-vp verifiers key owner change; + +pairFromOptionString : (String -> PairIntBool) -> OptionString -> PairIntBool; +pairFromOptionString _ NothingString := MakePair 0 false; +pairFromOptionString f (JustString o) := f o; + +foreign ghc { + token = "secret"; +}; +axiom token : String { + ghc ↦ "token"; +}; + +check-keys : ListString -> PairIntBool -> String -> PairIntBool; +check-keys verifiers (MakePair change is-success) key := + ifthenelse is-success + (pairFromOptionString (check-vp' verifiers key change) (is-balance-key token key)) + (MakePair 0 false); + +foldl : (PairIntBool -> String -> PairIntBool) → PairIntBool → ListString → PairIntBool; +foldl f z Nil ≔ z ; +foldl f z (Cons h hs) ≔ foldl f (f z h) hs; + +auxVP : PairIntBool -> Bool; +auxVP (MakePair change all-checked) := and (change ==Int 0) all-checked; + +vp : String -> ListString -> ListString -> Bool; +vp token keys-changed verifiers := + auxVP (foldl (check-keys verifiers) (MakePair 0 false) keys-changed); + +end; +