From 2cf3f854392b4dbdcaff0772458fdd1a13efb5c9 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Mon, 13 Jun 2022 14:25:22 +0200 Subject: [PATCH] Support implicit arguments (#144) * work in progress towards implicit arguments * Wip towards implicit types * improve arity checker * Add version of SimpleFungibleToken with implicit arguments * guess arity of body before checking the lhs of a clause * add ArityUnknown and fix some tests * wip: proper errors in arity checker * fix bugs, improve errors and add tests * format * set hlint version to 3.4 in the ci * update pre-commit version to 3.0.0 * minor changes * added more revisions * minor Co-authored-by: Jonathan Cubides --- .github/workflows/ci.yml | 14 +- app/App.hs | 2 +- app/Commands/MicroJuvix.hs | 11 + app/Main.hs | 4 + minijuvix-mode/minijuvix-mode.el | 1 + src/MiniJuvix/Pipeline.hs | 20 +- src/MiniJuvix/Prelude/Error/GenericError.hs | 16 +- src/MiniJuvix/Prelude/Pretty.hs | 16 + src/MiniJuvix/Syntax/Abstract/Language.hs | 13 +- .../Syntax/Abstract/Language/Extra.hs | 6 +- src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs | 13 +- src/MiniJuvix/Syntax/Concrete/Language.hs | 17 +- src/MiniJuvix/Syntax/Concrete/Lexer.hs | 17 +- src/MiniJuvix/Syntax/Concrete/Loc.hs | 22 + src/MiniJuvix/Syntax/Concrete/Parser.hs | 30 +- src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs | 2 + .../Syntax/Concrete/Scoped/Error/Types.hs | 21 + .../Syntax/Concrete/Scoped/Pretty/Base.hs | 36 +- .../Syntax/Concrete/Scoped/Scoper.hs | 56 ++- src/MiniJuvix/Syntax/IsImplicit.hs | 8 + .../Syntax/MicroJuvix/ArityChecker.hs | 403 ++++++++++++++++++ .../Syntax/MicroJuvix/ArityChecker/Arity.hs | 45 ++ .../Syntax/MicroJuvix/ArityChecker/Error.hs | 28 ++ .../MicroJuvix/ArityChecker/Error/Types.hs | 195 +++++++++ .../MicroJuvix/ArityChecker/LocalVars.hs | 24 ++ src/MiniJuvix/Syntax/MicroJuvix/Error.hs | 10 +- .../Syntax/MicroJuvix/Error/Pretty.hs | 24 +- .../Syntax/MicroJuvix/Error/Pretty/Ansi.hs | 2 +- .../Syntax/MicroJuvix/Error/Types.hs | 41 +- src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs | 41 +- src/MiniJuvix/Syntax/MicroJuvix/Language.hs | 54 ++- .../Syntax/MicroJuvix/Language/Extra.hs | 65 +-- src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs | 1 - .../MicroJuvix/MicroJuvixArityResult.hs | 18 + .../MicroJuvix/MicroJuvixTypedResult.hs | 4 +- .../Syntax/MicroJuvix/Pretty/Base.hs | 28 +- .../Syntax/MicroJuvix/Pretty/Options.hs | 2 +- .../Syntax/MicroJuvix/TypeChecker.hs | 108 ++--- .../MicroJuvix/TypeChecker/Inference.hs | 10 +- src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs | 1 - .../Syntax/MonoJuvix/MonoJuvixResult.hs | 16 +- src/MiniJuvix/Syntax/Wildcard.hs | 26 ++ src/MiniJuvix/Termination/Checker.hs | 2 +- src/MiniJuvix/Termination/FunctionCall.hs | 2 +- .../Translation/AbstractToMicroJuvix.hs | 21 +- .../Translation/MicroJuvixToMonoJuvix.hs | 1 + src/MiniJuvix/Translation/ScopedToAbstract.hs | 191 +++++---- test/Arity.hs | 10 + test/Arity/Negative.hs | 87 ++++ test/Main.hs | 2 + test/MonoJuvix/Positive.hs | 2 +- test/TypeCheck/Negative.hs | 21 - test/TypeCheck/Positive.hs | 4 +- .../ExpectedExplicitArgument.mjuvix | 8 + .../MicroJuvix/ExpectedExplicitPattern.mjuvix | 8 + .../MicroJuvix/ExpectedFunctionType.mjuvix | 8 +- .../MicroJuvix/FunctionApplied.mjuvix | 8 + .../MicroJuvix/FunctionPattern.mjuvix | 8 + .../MicroJuvix/LhsTooManyPatterns.mjuvix | 8 + .../MicroJuvix/PatternConstructorApp.mjuvix | 13 - .../MicroJuvix/TooManyArguments.mjuvix | 8 + .../MicroJuvix/TooManyPatterns.mjuvix | 8 - tests/negative/MicroJuvix/UnsolvedMeta.mjuvix | 2 +- .../MicroJuvix/WrongConstructorArity.mjuvix | 4 +- .../PolySimpleFungibleToken.mjuvix | 329 -------------- ...vix => SimpleFungibleTokenImplicit.mjuvix} | 80 ++-- tests/positive/Implicit.mjuvix | 73 ++++ .../MicroJuvix/HoleInSignature.mjuvix | 4 +- .../positive/MiniC/MultiModules/Input.mjuvix | 2 +- .../positive/MiniC/Polymorphism/Input.mjuvix | 2 +- .../MiniC/PolymorphismHoles/Input.mjuvix | 6 +- tests/positive/Polymorphism.mjuvix | 36 +- tests/positive/PolymorphismHoles.mjuvix | 39 +- 73 files changed, 1647 insertions(+), 821 deletions(-) create mode 100644 src/MiniJuvix/Syntax/IsImplicit.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/ArityChecker.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Arity.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/LocalVars.hs create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs create mode 100644 src/MiniJuvix/Syntax/Wildcard.hs create mode 100644 test/Arity.hs create mode 100644 test/Arity/Negative.hs create mode 100644 tests/negative/MicroJuvix/ExpectedExplicitArgument.mjuvix create mode 100644 tests/negative/MicroJuvix/ExpectedExplicitPattern.mjuvix create mode 100644 tests/negative/MicroJuvix/FunctionApplied.mjuvix create mode 100644 tests/negative/MicroJuvix/FunctionPattern.mjuvix create mode 100644 tests/negative/MicroJuvix/LhsTooManyPatterns.mjuvix delete mode 100644 tests/negative/MicroJuvix/PatternConstructorApp.mjuvix create mode 100644 tests/negative/MicroJuvix/TooManyArguments.mjuvix delete mode 100644 tests/negative/MicroJuvix/TooManyPatterns.mjuvix delete mode 100644 tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix rename tests/positive/FullExamples/{PolySimpleFungibleTokenHoles.mjuvix => SimpleFungibleTokenImplicit.mjuvix} (77%) create mode 100644 tests/positive/Implicit.mjuvix diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 73aeb5e61..6549a7825 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -72,7 +72,7 @@ jobs: - name: 'Set up HLint' uses: rwe/actions-hlint-setup@v1 with: - version: '3.1.6' + version: '3.4' - name: 'Run HLint' uses: rwe/actions-hlint-run@v2.0.1 with: @@ -84,27 +84,27 @@ jobs: steps: - uses: actions/checkout@v2 - uses: actions/setup-python@v2 - - uses: pre-commit/action@v2.0.3 + - uses: pre-commit/action@v3.0.0 with: extra_args: trailing-whitespace --all-files - - uses: pre-commit/action@v2.0.3 + - uses: pre-commit/action@v3.0.0 with: extra_args: end-of-file-fixer --all-files - - uses: pre-commit/action@v2.0.3 + - uses: pre-commit/action@v3.0.0 with: extra_args: check-yaml --all-files - - uses: pre-commit/action@v2.0.3 + - uses: pre-commit/action@v3.0.0 with: extra_args: check-added-large-files --all-files - - uses: pre-commit/action@v2.0.3 + - uses: pre-commit/action@v3.0.0 with: extra_args: check-case-conflict --all-files - - uses: pre-commit/action@v2.0.3 + - uses: pre-commit/action@v3.0.0 with: extra_args: mixed-line-ending --all-files diff --git a/app/App.hs b/app/App.hs index 71c980022..8beea8b51 100644 --- a/app/App.hs +++ b/app/App.hs @@ -30,7 +30,7 @@ runAppIO g = interpret $ \case | g ^. globalOnlyErrors -> return () | otherwise -> embed (putStrLn t) ExitMiniJuvixError e -> do - (embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors))) e + (embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors)) (g ^. globalOnlyErrors)) e embed exitFailure ExitMsg exitCode t -> embed (putStrLn t >> exitWith exitCode) diff --git a/app/Commands/MicroJuvix.hs b/app/Commands/MicroJuvix.hs index 8587ae33c..30305d97d 100644 --- a/app/Commands/MicroJuvix.hs +++ b/app/Commands/MicroJuvix.hs @@ -6,6 +6,7 @@ import Options.Applicative data MicroJuvixCommand = Pretty | TypeCheck MicroJuvixTypeOptions + | Arity newtype MicroJuvixTypeOptions = MicroJuvixTypeOptions { _microJuvixTypePrint :: Bool @@ -18,15 +19,25 @@ parseMicroJuvixCommand = hsubparser $ mconcat [ commandPretty, + commandArity, commandTypeCheck ] where + commandArity :: Mod CommandFields MicroJuvixCommand + commandArity = command "arity" arityInfo + commandPretty :: Mod CommandFields MicroJuvixCommand commandPretty = command "pretty" prettyInfo commandTypeCheck :: Mod CommandFields MicroJuvixCommand commandTypeCheck = command "typecheck" typeCheckInfo + arityInfo :: ParserInfo MicroJuvixCommand + arityInfo = + info + (pure Arity) + (progDesc "Translate a MiniJuvix file to MicroJuvix and insert holes") + prettyInfo :: ParserInfo MicroJuvixCommand prettyInfo = info diff --git a/app/Main.hs b/app/Main.hs index 1fa657091..f4dc5ef8b 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -19,6 +19,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper import MiniJuvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as MicroArity import MiniJuvix.Syntax.MicroJuvix.Pretty qualified as Micro import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroTyped import MiniJuvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell @@ -133,6 +134,9 @@ runCommand cmdWithOpts = do { Micro._optShowNameIds = globalOpts ^. globalShowNameIds } App.renderStdOut (Micro.ppOut ppOpts micro) + MicroJuvix Arity -> do + micro <- head . (^. MicroArity.resultModules) <$> runPipeline (upToMicroJuvixArity entryPoint) + App.renderStdOut (Micro.ppOut Micro.defaultOptions micro) MicroJuvix (TypeCheck localOpts) -> do res <- runPipeline (upToMicroJuvixTyped entryPoint) say "Well done! It type checks" diff --git a/minijuvix-mode/minijuvix-mode.el b/minijuvix-mode/minijuvix-mode.el index 8209cb022..ea13e32dd 100644 --- a/minijuvix-mode/minijuvix-mode.el +++ b/minijuvix-mode/minijuvix-mode.el @@ -29,6 +29,7 @@ (with-eval-after-load 'evil (evil-define-key 'normal minijuvix-mode-map (kbd "SPC m l") 'minijuvix-load) (evil-define-key 'normal minijuvix-mode-map (kbd "SPC m g") 'minijuvix-goto-definition) + (evil-define-key 'normal minijuvix-mode-map (kbd "g d") 'minijuvix-goto-definition) (evil-normalize-keymaps)))) ) diff --git a/src/MiniJuvix/Pipeline.hs b/src/MiniJuvix/Pipeline.hs index ab4923a91..e93c78c15 100644 --- a/src/MiniJuvix/Pipeline.hs +++ b/src/MiniJuvix/Pipeline.hs @@ -13,6 +13,7 @@ import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract import MiniJuvix.Syntax.Concrete.Parser qualified as Parser import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper +import MiniJuvix.Syntax.MicroJuvix.ArityChecker qualified as MicroJuvix import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix import MiniJuvix.Syntax.MicroJuvix.TypeChecker qualified as MicroJuvix @@ -77,11 +78,17 @@ upToMicroJuvix :: Sem r MicroJuvix.MicroJuvixResult upToMicroJuvix = upToAbstract >=> pipelineMicroJuvix +upToMicroJuvixArity :: + Members '[Files, NameIdGen, Error MiniJuvixError] r => + EntryPoint -> + Sem r MicroJuvix.MicroJuvixArityResult +upToMicroJuvixArity = upToMicroJuvix >=> pipelineMicroJuvixArity + upToMicroJuvixTyped :: Members '[Files, NameIdGen, Error MiniJuvixError] r => EntryPoint -> Sem r MicroJuvix.MicroJuvixTypedResult -upToMicroJuvixTyped = upToMicroJuvix >=> pipelineMicroJuvixTyped +upToMicroJuvixTyped = upToMicroJuvixArity >=> pipelineMicroJuvixTyped upToMonoJuvix :: Members '[Files, NameIdGen, Error MiniJuvixError] r => @@ -116,9 +123,10 @@ pipelineScoper :: pipelineScoper = mapError (MiniJuvixError @Scoper.ScoperError) . Scoper.entryScoper pipelineAbstract :: + Members '[Error MiniJuvixError] r => Scoper.ScoperResult -> Sem r Abstract.AbstractResult -pipelineAbstract = Abstract.entryAbstract +pipelineAbstract = mapError (MiniJuvixError @Scoper.ScoperError) . Abstract.entryAbstract pipelineMicroJuvix :: Members '[Error MiniJuvixError] r => @@ -126,9 +134,15 @@ pipelineMicroJuvix :: Sem r MicroJuvix.MicroJuvixResult pipelineMicroJuvix = mapError (MiniJuvixError @MicroJuvix.TerminationError) . MicroJuvix.entryMicroJuvix +pipelineMicroJuvixArity :: + Members '[Error MiniJuvixError, NameIdGen] r => + MicroJuvix.MicroJuvixResult -> + Sem r MicroJuvix.MicroJuvixArityResult +pipelineMicroJuvixArity = mapError (MiniJuvixError @MicroJuvix.ArityCheckerError) . MicroJuvix.entryMicroJuvixArity + pipelineMicroJuvixTyped :: Members '[Files, NameIdGen, Error MiniJuvixError] r => - MicroJuvix.MicroJuvixResult -> + MicroJuvix.MicroJuvixArityResult -> Sem r MicroJuvix.MicroJuvixTypedResult pipelineMicroJuvixTyped = mapError (MiniJuvixError @MicroJuvix.TypeCheckerError) . MicroJuvix.entryMicroJuvixTyped diff --git a/src/MiniJuvix/Prelude/Error/GenericError.hs b/src/MiniJuvix/Prelude/Error/GenericError.hs index 8c0466d7c..fd53e87d1 100644 --- a/src/MiniJuvix/Prelude/Error/GenericError.hs +++ b/src/MiniJuvix/Prelude/Error/GenericError.hs @@ -38,13 +38,13 @@ class ToGenericError a where errorIntervals :: ToGenericError e => e -> [Interval] errorIntervals = (^. genericErrorIntervals) . genericError -render :: ToGenericError e => Bool -> e -> Text -render ansi err +render :: ToGenericError e => Bool -> Bool -> e -> Text +render ansi endChar err | ansi = helper Ansi.renderStrict (toAnsiDoc gMsg) | otherwise = helper renderStrict (toTextDoc gMsg) where helper :: (SimpleDocStream a -> Text) -> Doc a -> Text - helper f x = (f . layoutPretty defaultLayoutOptions) (header <> x <> endChar) + helper f x = (f . layoutPretty defaultLayoutOptions) (header <> x <> lastChar) g :: GenericError g = genericError err @@ -55,16 +55,18 @@ render ansi err header :: Doc a header = genericErrorHeader g - endChar :: Doc a - endChar = "ת" + lastChar :: Doc a + lastChar + | endChar = "ת" + | otherwise = "" -- | Render the error to Text. renderText :: ToGenericError e => e -> Text -renderText = render False +renderText = render False False -- | Render the error with Ansi formatting (if any). renderAnsiText :: ToGenericError e => e -> Text -renderAnsiText = render True +renderAnsiText = render True False printErrorAnsi :: ToGenericError e => e -> IO () printErrorAnsi = hPutStrLn stderr . renderAnsiText diff --git a/src/MiniJuvix/Prelude/Pretty.hs b/src/MiniJuvix/Prelude/Pretty.hs index b748154d0..c790b5fd3 100644 --- a/src/MiniJuvix/Prelude/Pretty.hs +++ b/src/MiniJuvix/Prelude/Pretty.hs @@ -87,3 +87,19 @@ hsepMaybe :: Foldable f => f (Doc a) -> Maybe (Doc a) hsepMaybe l | null l = Nothing | otherwise = Just (hsep l) + +ordinal :: Int -> Doc a +ordinal = \case + 1 -> "first" + 2 -> "second" + 3 -> "third" + 4 -> "fourth" + 5 -> "fifth" + 6 -> "sixth" + 7 -> "seventh" + 8 -> "eighth" + 9 -> "ninth" + 10 -> "tenth" + 11 -> "eleventh" + 12 -> "twelfth" + n -> pretty n <> "th" diff --git a/src/MiniJuvix/Syntax/Abstract/Language.hs b/src/MiniJuvix/Syntax/Abstract/Language.hs index 3d4d1f17b..020c9034e 100644 --- a/src/MiniJuvix/Syntax/Abstract/Language.hs +++ b/src/MiniJuvix/Syntax/Abstract/Language.hs @@ -2,6 +2,8 @@ module MiniJuvix.Syntax.Abstract.Language ( module MiniJuvix.Syntax.Abstract.Language, module MiniJuvix.Syntax.Concrete.Language, module MiniJuvix.Syntax.Hole, + module MiniJuvix.Syntax.Wildcard, + module MiniJuvix.Syntax.IsImplicit, ) where @@ -11,7 +13,9 @@ import MiniJuvix.Syntax.Concrete.Name qualified as C import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S import MiniJuvix.Syntax.Fixity import MiniJuvix.Syntax.Hole +import MiniJuvix.Syntax.IsImplicit import MiniJuvix.Syntax.Universe +import MiniJuvix.Syntax.Wildcard type TopModuleName = S.TopModulePath @@ -110,7 +114,7 @@ data Expression deriving stock (Eq, Show) instance HasAtomicity Expression where - atomicity e = case e of + atomicity = \case ExpressionIden {} -> Atom ExpressionHole {} -> Atom ExpressionUniverse u -> atomicity u @@ -132,7 +136,8 @@ data MatchAlt = MatchAlt data Application = Application { _appLeft :: Expression, - _appRight :: Expression + _appRight :: Expression, + _appImplicit :: IsImplicit } deriving stock (Eq, Show) @@ -152,6 +157,7 @@ data LambdaClause = LambdaClause data FunctionParameter = FunctionParameter { _paramName :: Maybe VarName, _paramUsage :: Usage, + _paramImplicit :: IsImplicit, _paramType :: Expression } deriving stock (Eq, Show) @@ -175,8 +181,9 @@ data ConstructorApp = ConstructorApp data Pattern = PatternVariable VarName | PatternConstructorApp ConstructorApp - | PatternWildcard + | PatternWildcard Wildcard | PatternEmpty + | PatternBraces Pattern deriving stock (Eq, Show) data InductiveDef = InductiveDef diff --git a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs index 154e8bb1e..7b816bd39 100644 --- a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs +++ b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs @@ -8,10 +8,11 @@ import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.Language patternVariables :: Pattern -> [VarName] -patternVariables pat = case pat of +patternVariables = \case PatternVariable v -> [v] PatternWildcard {} -> [] PatternEmpty {} -> [] + PatternBraces b -> patternVariables b PatternConstructorApp app -> appVariables app appVariables :: ConstructorApp -> [VarName] @@ -20,13 +21,14 @@ appVariables (ConstructorApp _ ps) = concatMap patternVariables ps smallerPatternVariables :: Pattern -> [VarName] smallerPatternVariables = \case PatternVariable {} -> [] + PatternBraces b -> smallerPatternVariables b PatternWildcard {} -> [] PatternEmpty {} -> [] PatternConstructorApp app -> appVariables app viewApp :: Expression -> (Expression, [Expression]) viewApp e = case e of - ExpressionApplication (Application l r) -> + ExpressionApplication (Application l r _) -> second (`snoc` r) (viewApp l) _ -> (e, []) diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs index 769dd1974..560aa09c3 100644 --- a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs @@ -73,6 +73,11 @@ kwColonOmega = keyword Str.colonOmegaUnicode parensCond :: Bool -> Doc Ann -> Doc Ann parensCond t d = if t then parens d else d +implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann +implicitDelim = \case + Implicit -> braces + Explicit -> parens + ppPostExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => Fixity -> @@ -116,9 +121,11 @@ instance PrettyCode Iden where ppCode = ppSCode . idenName instance PrettyCode Application where - ppCode (Application l r) = do + ppCode (Application l r i) = do l' <- ppLeftExpression appFixity l - r' <- ppRightExpression appFixity r + r' <- case i of + Explicit -> ppRightExpression appFixity r + Implicit -> implicitDelim i <$> ppCode r return $ l' <+> r' instance PrettyCode Universe where @@ -147,7 +154,7 @@ instance PrettyCode FunctionParameter where paramName' <- ppSCode n paramType' <- ppCode _paramType paramUsage' <- ppCode _paramUsage - return $ parens (paramName' <+> paramUsage' <+> paramType') + return $ implicitDelim _paramImplicit (paramName' <+> paramUsage' <+> paramType') instance PrettyCode Function where ppCode Function {..} = do diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs index 76ee3cdd6..176eb7437 100644 --- a/src/MiniJuvix/Syntax/Concrete/Language.hs +++ b/src/MiniJuvix/Syntax/Concrete/Language.hs @@ -7,12 +7,14 @@ module MiniJuvix.Syntax.Concrete.Language module MiniJuvix.Syntax.Concrete.Loc, module MiniJuvix.Syntax.Hole, module MiniJuvix.Syntax.Concrete.LiteralLoc, + module MiniJuvix.Syntax.IsImplicit, module MiniJuvix.Syntax.Backends, module MiniJuvix.Syntax.ForeignBlock, module MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn, module MiniJuvix.Syntax.Concrete.PublicAnn, module MiniJuvix.Syntax.Concrete.ModuleIsTop, module MiniJuvix.Syntax.Concrete.Language.Stage, + module MiniJuvix.Syntax.Wildcard, module MiniJuvix.Syntax.Fixity, module MiniJuvix.Syntax.Usage, module MiniJuvix.Syntax.Universe, @@ -36,8 +38,10 @@ import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn import MiniJuvix.Syntax.Fixity import MiniJuvix.Syntax.ForeignBlock import MiniJuvix.Syntax.Hole +import MiniJuvix.Syntax.IsImplicit import MiniJuvix.Syntax.Universe import MiniJuvix.Syntax.Usage +import MiniJuvix.Syntax.Wildcard import Prelude (show) -------------------------------------------------------------------------------- @@ -280,7 +284,8 @@ data Pattern | PatternApplication PatternApp | PatternInfixApplication PatternInfixApp | PatternPostfixApplication PatternPostfixApp - | PatternWildcard + | PatternBraces Pattern + | PatternWildcard Wildcard | PatternEmpty deriving stock (Show, Eq, Ord) @@ -291,7 +296,8 @@ instance HasAtomicity Pattern where PatternApplication {} -> Aggregate appFixity PatternInfixApplication a -> Aggregate (getFixity a) PatternPostfixApplication p -> Aggregate (getFixity p) - PatternWildcard -> Atom + PatternWildcard {} -> Atom + PatternBraces {} -> Atom PatternEmpty -> Atom -------------------------------------------------------------------------------- @@ -305,9 +311,10 @@ data PatternScopedIden data PatternAtom (s :: Stage) = PatternAtomIden (PatternAtomIdenType s) - | PatternAtomWildcard + | PatternAtomWildcard Wildcard | PatternAtomEmpty | PatternAtomParens (PatternAtoms s) + | PatternAtomBraces (PatternAtoms s) data PatternAtoms (s :: Stage) = PatternAtoms { _patternAtoms :: NonEmpty (PatternAtom s), @@ -542,6 +549,7 @@ data Expression | ExpressionLiteral LiteralLoc | ExpressionFunction (Function 'Scoped) | ExpressionHole (HoleType 'Scoped) + | ExpressionBraces (WithLoc Expression) deriving stock (Show, Eq, Ord) instance HasAtomicity Expression where @@ -556,6 +564,7 @@ instance HasAtomicity Expression where ExpressionLiteral {} -> Atom ExpressionMatch {} -> Atom ExpressionLetBlock {} -> Atom + ExpressionBraces {} -> Atom ExpressionUniverse {} -> Atom ExpressionFunction {} -> Aggregate funFixity @@ -616,6 +625,7 @@ deriving stock instance data FunctionParameter (s :: Stage) = FunctionParameter { _paramName :: Maybe (SymbolType s), _paramUsage :: Maybe Usage, + _paramImplicit :: IsImplicit, _paramType :: ExpressionType s } @@ -912,6 +922,7 @@ data ExpressionAtom (s :: Stage) = AtomIdentifier (IdentifierType s) | AtomLambda (Lambda s) | AtomHole (HoleType s) + | AtomBraces (WithLoc (ExpressionType s)) | AtomLetBlock (LetBlock s) | AtomUniverse Universe | AtomFunction (Function s) diff --git a/src/MiniJuvix/Syntax/Concrete/Lexer.hs b/src/MiniJuvix/Syntax/Concrete/Lexer.hs index 218ac5d43..b60c784aa 100644 --- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs +++ b/src/MiniJuvix/Syntax/Concrete/Lexer.hs @@ -94,6 +94,11 @@ interval ma = do end <- curLoc return (res, mkInterval start end) +withLoc :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (WithLoc a) +withLoc ma = do + (a, i) <- interval ma + return (WithLoc i a) + keyword :: Members '[Reader ParserParams, InfoTableBuilder] r => Text -> ParsecS r () keyword kw = do l <- symbolInterval kw @@ -130,9 +135,6 @@ dot = P.char '.' dottedIdentifier :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (NonEmpty (Text, Interval)) dottedIdentifier = lexeme $ P.sepBy1 bareIdentifier dot -braces :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a -braces = between (symbol "{") (symbol "}") - allKeywords :: Members '[Reader ParserParams, InfoTableBuilder] r => [ParsecS r ()] allKeywords = [ kwAssignment, @@ -170,6 +172,12 @@ allKeywords = kwWildcard ] +lbrace :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () +lbrace = symbol "{" + +rbrace :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () +rbrace = symbol "}" + lparen :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () lparen = symbol "(" @@ -179,6 +187,9 @@ rparen = symbol ")" parens :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a parens = between lparen rparen +braces :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a +braces = between (symbol "{") (symbol "}") + kwAssignment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii diff --git a/src/MiniJuvix/Syntax/Concrete/Loc.hs b/src/MiniJuvix/Syntax/Concrete/Loc.hs index 8f9411f6a..0d85171e3 100644 --- a/src/MiniJuvix/Syntax/Concrete/Loc.hs +++ b/src/MiniJuvix/Syntax/Concrete/Loc.hs @@ -64,14 +64,36 @@ instance Hashable Interval class HasLoc t where getLoc :: t -> Interval +getLocSpan :: HasLoc t => NonEmpty t -> Interval +getLocSpan = foldr1 (<>) . fmap getLoc + -- | Assumes the file is the same instance Semigroup Interval where Interval f s e <> Interval _f s' e' = Interval f (min s s') (max e e') +data WithLoc a = WithLoc + { _withLocInt :: Interval, + _withLocParam :: a + } + deriving stock (Show) + makeLenses ''Interval makeLenses ''FileLoc makeLenses ''Loc makeLenses ''Pos +makeLenses ''WithLoc + +instance HasLoc (WithLoc a) where + getLoc = (^. withLocInt) + +instance Eq a => Eq (WithLoc a) where + (==) = (==) `on` (^. withLocParam) + +instance Ord a => Ord (WithLoc a) where + compare = compare `on` (^. withLocParam) + +instance Functor WithLoc where + fmap = over withLocParam singletonInterval :: Loc -> Interval singletonInterval l = diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs index d4c23923b..64444525b 100644 --- a/src/MiniJuvix/Syntax/Concrete/Parser.hs +++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs @@ -177,7 +177,7 @@ import_ = do expressionAtom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (ExpressionAtom 'Parsed) expressionAtom = - do AtomLiteral <$> P.try literal + AtomLiteral <$> P.try literal <|> (AtomIdentifier <$> name) <|> (AtomUniverse <$> universe) <|> (AtomLambda <$> lambda) @@ -187,6 +187,8 @@ expressionAtom = <|> (AtomFunArrow <$ kwRightArrow) <|> (AtomHole <$> hole) <|> parens (AtomParens <$> parseExpressionAtoms) + -- TODO: revise this try. Necessary to avoid confusion with match + <|> P.try (braces (AtomBraces <$> withLoc parseExpressionAtoms)) parseExpressionAtoms :: Members '[Reader ParserParams, InfoTableBuilder] r => @@ -309,16 +311,26 @@ axiomDef = do -- Function expression -------------------------------------------------------------------------------- +implicitOpen :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r IsImplicit +implicitOpen = + lbrace $> Implicit + <|> lparen $> Explicit + +implicitClose :: Members '[Reader ParserParams, InfoTableBuilder] r => IsImplicit -> ParsecS r () +implicitClose = \case + Implicit -> rbrace + Explicit -> rparen + functionParam :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (FunctionParameter 'Parsed) functionParam = do - (_paramName, _paramUsage) <- P.try $ do - lparen + (_paramName, _paramUsage, _paramImplicit) <- P.try $ do + impl <- implicitOpen n <- pName u <- pUsage - return (n, u) + return (n, u, impl) _paramType <- parseExpressionAtoms - rparen - return $ FunctionParameter {..} + implicitClose _paramImplicit + return FunctionParameter {..} where pName :: ParsecS r (Maybe Symbol) pName = @@ -399,6 +411,9 @@ constructorDef = do _constructorType <- parseExpressionAtoms return InductiveConstructorDef {..} +wildcard :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Wildcard +wildcard = Wildcard . snd <$> interval kwWildcard + -------------------------------------------------------------------------------- -- Pattern section -------------------------------------------------------------------------------- @@ -406,8 +421,9 @@ constructorDef = do patternAtom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (PatternAtom 'Parsed) patternAtom = PatternAtomIden <$> name - <|> PatternAtomWildcard <$ kwWildcard + <|> PatternAtomWildcard <$> wildcard <|> (PatternAtomParens <$> parens parsePatternAtoms) + <|> (PatternAtomBraces <$> braces parsePatternAtoms) parsePatternAtoms :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (PatternAtoms 'Parsed) parsePatternAtoms = do diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs index bbc4e9207..64cde6f5f 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error.hs @@ -12,6 +12,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Error.Types data ScoperError = ErrParser MegaParsecError | ErrInfixParser InfixError + | ErrAppLeftImplicit AppLeftImplicit | ErrInfixPattern InfixErrorP | ErrMultipleDeclarations MultipleDeclarations | ErrLacksTypeSig LacksTypeSig @@ -37,6 +38,7 @@ instance ToGenericError ScoperError where genericError = \case ErrParser e -> genericError e ErrInfixParser e -> genericError e + ErrAppLeftImplicit e -> genericError e ErrInfixPattern e -> genericError e ErrMultipleDeclarations e -> genericError e ErrLacksTypeSig e -> genericError e diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs index 5075ec96a..e82e2a852 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs @@ -277,6 +277,27 @@ instance ToGenericError NotInScope where instance HasLoc NotInScope where getLoc = getLoc . (^. notInScopeSymbol) +newtype AppLeftImplicit = AppLeftImplicit + { _appLeftImplicit :: WithLoc Expression + } + deriving stock (Show) + +makeLenses ''AppLeftImplicit + +instance ToGenericError AppLeftImplicit where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLoc (e ^. appLeftImplicit) + msg = + "The expression" <+> ppCode (e ^. appLeftImplicit) <+> "cannot appear by itself." + <> line + <> "It needs to be the argument of a function expecting an implicit argument." + newtype ModuleNotInScope = ModuleNotInScope { _moduleNotInScopeName :: Name } diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs index 2f5ff7284..82bf9e3ea 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs @@ -173,6 +173,11 @@ braces = enclose kwBraceL kwBraceR parens :: Doc Ann -> Doc Ann parens = enclose kwParenL kwParenR +implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann +implicitDelim = \case + Implicit -> braces + Explicit -> parens + doubleQuotes :: Doc Ann -> Doc Ann doubleQuotes = enclose kwDQuote kwDQuote @@ -512,13 +517,23 @@ instance SingI s => PrettyCode (TypeSignature s) where instance SingI s => PrettyCode (Function s) where ppCode :: forall r. Members '[Reader Options] r => Function s -> Sem r (Doc Ann) ppCode Function {..} = do - funParameter' <- ppFunParameter _funParameter + funParameter' <- ppCode _funParameter funReturn' <- ppRightExpression' funFixity _funReturn return $ funParameter' <+> kwArrowR <+> funReturn' where ppRightExpression' = case sing :: SStage s of SParsed -> ppRightExpression SScoped -> ppRightExpression + +instance SingI s => PrettyCode (FunctionParameter s) where + ppCode FunctionParameter {..} = do + case _paramName of + Nothing -> ppLeftExpression' funFixity _paramType + Just n -> do + paramName' <- annDef n <$> ppSymbol n + paramType' <- ppExpression _paramType + return $ implicitDelim _paramImplicit (paramName' <+> ppUsage _paramUsage <+> paramType') + where ppLeftExpression' = case sing :: SStage s of SParsed -> ppLeftExpression SScoped -> ppLeftExpression @@ -529,14 +544,6 @@ instance SingI s => PrettyCode (Function s) where UsageNone -> kwColonZero UsageOnce -> kwColonOne UsageOmega -> kwColonOmega - ppFunParameter :: FunctionParameter s -> Sem r (Doc Ann) - ppFunParameter FunctionParameter {..} = do - case _paramName of - Nothing -> ppLeftExpression' funFixity _paramType - Just n -> do - paramName' <- annDef n <$> ppSymbol n - paramType' <- ppExpression _paramType - return $ parens (paramName' <+> ppUsage _paramUsage <+> paramType') instance PrettyCode Universe where ppCode (Universe n) = return $ kwType <+?> (pretty <$> n) @@ -646,9 +653,10 @@ instance SingI s => PrettyCode (PatternAtom s) where PatternAtomIden n -> case sing :: SStage s of SParsed -> ppCode n SScoped -> ppCode n - PatternAtomWildcard -> return kwWildcard + PatternAtomWildcard {} -> return kwWildcard PatternAtomEmpty -> return $ parens mempty PatternAtomParens p -> parens <$> ppCode p + PatternAtomBraces p -> braces <$> ppCode p instance SingI s => PrettyCode (PatternAtoms s) where ppCode (PatternAtoms ps _) = hsep . toList <$> mapM ppCode ps @@ -710,11 +718,15 @@ instance PrettyCode ScopedIden where ScopedFunction f -> ppCode f ScopedConstructor c -> ppCode c +instance PrettyCode c => PrettyCode (WithLoc c) where + ppCode = ppCode . (^. withLocParam) + instance PrettyCode Expression where ppCode e = case e of ExpressionIdentifier n -> ppCode n ExpressionHole w -> ppHole w ExpressionParensIdentifier n -> parens <$> ppCode n + ExpressionBraces b -> braces <$> ppCode b ExpressionApplication a -> ppCode a ExpressionInfixApplication a -> ppCode a ExpressionPostfixApplication a -> ppCode a @@ -733,8 +745,9 @@ instance PrettyCode Pattern where l' <- ppLeftExpression appFixity l r' <- ppRightExpression appFixity r return $ l' <+> r' - PatternWildcard -> return kwWildcard + PatternWildcard {} -> return kwWildcard PatternEmpty -> return $ parens mempty + PatternBraces p -> braces <$> ppCode p PatternConstructor constr -> ppCode constr PatternInfixApplication i -> ppPatternInfixApp i PatternPostfixApplication i -> ppPatternPostfixApp i @@ -812,6 +825,7 @@ instance SingI s => PrettyCode (ExpressionAtom s) where AtomFunArrow -> return kwArrowR AtomMatch m -> ppCode m AtomParens e -> parens <$> ppExpression e + AtomBraces e -> braces <$> ppExpression (e ^. withLocParam) AtomHole w -> ppHole w instance SingI s => PrettyCode (ExpressionAtoms s) where diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs index d4b8ccfd3..75af7cd31 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs @@ -911,6 +911,7 @@ checkFunction Function {..} = do FunctionParameter { _paramName = paramName', _paramUsage = _paramUsage, + _paramImplicit = _paramImplicit, _paramType = paramType' } where @@ -1088,10 +1089,11 @@ checkPatternAtom :: PatternAtom 'Parsed -> Sem r (PatternAtom 'Scoped) checkPatternAtom p = case p of - PatternAtomWildcard -> return PatternAtomWildcard + PatternAtomWildcard i -> return (PatternAtomWildcard i) PatternAtomEmpty -> return PatternAtomEmpty PatternAtomParens e -> PatternAtomParens <$> checkPatternAtoms e PatternAtomIden n -> PatternAtomIden <$> checkPatternName n + PatternAtomBraces n -> PatternAtomBraces <$> checkPatternAtoms n checkName :: Members '[Error ScoperError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r => @@ -1112,6 +1114,7 @@ checkExpressionAtom e = case e of AtomUniverse uni -> return (AtomUniverse uni) AtomFunction fun -> AtomFunction <$> checkFunction fun AtomParens par -> AtomParens <$> checkParens par + AtomBraces br -> AtomBraces <$> traverseOf withLocParam checkParseExpressionAtoms br AtomFunArrow -> return AtomFunArrow AtomHole h -> AtomHole <$> checkHole h AtomLiteral l -> return (AtomLiteral l) @@ -1206,9 +1209,10 @@ checkStatement s = case s of ------------------------------------------------------------------------------- -- Infix Expression ------------------------------------------------------------------------------- + makeExpressionTable2 :: ExpressionAtoms 'Scoped -> [[P.Operator Parse Expression]] -makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functionOp]] +makeExpressionTable2 (ExpressionAtoms atoms _) = [appOpExplicit] : operators ++ [[functionOp]] where operators = mkSymbolTable idens idens :: [ScopedIden] @@ -1253,8 +1257,8 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functi _ -> Nothing -- Application by juxtaposition. - appOp :: P.Operator Parse Expression - appOp = P.InfixL (return app) + appOpExplicit :: P.Operator Parse Expression + appOpExplicit = P.InfixL (return app) where app :: Expression -> Expression -> Expression app f x = @@ -1263,6 +1267,7 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functi { _applicationFunction = f, _applicationParameter = x } + -- Non-dependent function type: A → B functionOp :: P.Operator Parse Expression functionOp = P.InfixR (nonDepFun <$ P.single AtomFunArrow) @@ -1279,6 +1284,7 @@ makeExpressionTable2 (ExpressionAtoms atoms _) = [appOp] : operators ++ [[functi FunctionParameter { _paramName = Nothing, _paramUsage = Nothing, + _paramImplicit = Explicit, _paramType = a } @@ -1325,6 +1331,7 @@ parseTerm = <|> parseLiteral <|> parseMatch <|> parseLetBlock + <|> parseBraces where parseHole :: Parse Expression parseHole = ExpressionHole <$> P.token lit mempty @@ -1391,6 +1398,14 @@ parseTerm = | not (S.hasFixity (identifierName iden)) -> Just iden _ -> Nothing + parseBraces :: Parse Expression + parseBraces = ExpressionBraces <$> P.token bracedExpr mempty + where + bracedExpr :: ExpressionAtom 'Scoped -> Maybe (WithLoc Expression) + bracedExpr = \case + AtomBraces l -> Just l + _ -> Nothing + parseParens :: Parse Expression parseParens = P.token parenExpr mempty where @@ -1457,7 +1472,13 @@ makePatternTable atom = [appOp] : operators appOp = P.InfixL (return app) where app :: Pattern -> Pattern -> Pattern - app l = PatternApplication . PatternApp l + app l r = + PatternApplication + ( PatternApp + { _patAppLeft = l, + _patAppRight = r + } + ) parsePatternTerm :: forall r. @@ -1469,6 +1490,7 @@ parsePatternTerm = do parseNoInfixConstructor <|> parseVariable <|> parseParens pPat + <|> parseBraces pPat <|> parseWildcard <|> parseEmpty where @@ -1486,12 +1508,12 @@ parsePatternTerm = do _ -> Nothing parseWildcard :: ParsePat Pattern - parseWildcard = PatternWildcard <$ P.satisfy isWildcard + parseWildcard = PatternWildcard <$> P.token isWildcard mempty where - isWildcard :: PatternAtom 'Scoped -> Bool + isWildcard :: PatternAtom 'Scoped -> Maybe Wildcard isWildcard s = case s of - PatternAtomWildcard -> True - _ -> False + PatternAtomWildcard i -> Just i + _ -> Nothing parseEmpty :: ParsePat Pattern parseEmpty = PatternEmpty <$ P.satisfy isEmpty @@ -1509,15 +1531,25 @@ parsePatternTerm = do PatternAtomIden (PatternScopedVar sym) -> Just sym _ -> Nothing + parseBraces :: ParsePat Pattern -> ParsePat Pattern + parseBraces patternParser = do + exprs <- P.token bracesPat mempty + case P.parse patternParser "" exprs of + Right r -> return (PatternBraces r) + Left {} -> mzero + where + bracesPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped] + bracesPat s = case s of + PatternAtomBraces (PatternAtoms ss _) -> Just (toList ss) + _ -> Nothing + parseParens :: ParsePat Pattern -> ParsePat Pattern parseParens patternParser = do exprs <- P.token parenPat mempty - case P.parse patternParser strPath exprs of + case P.parse patternParser "" exprs of Right r -> return r Left {} -> mzero where - strPath :: FilePath - strPath = "inner parens" parenPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped] parenPat s = case s of PatternAtomParens (PatternAtoms ss _) -> Just (toList ss) diff --git a/src/MiniJuvix/Syntax/IsImplicit.hs b/src/MiniJuvix/Syntax/IsImplicit.hs new file mode 100644 index 000000000..55ef46dc4 --- /dev/null +++ b/src/MiniJuvix/Syntax/IsImplicit.hs @@ -0,0 +1,8 @@ +module MiniJuvix.Syntax.IsImplicit where + +import MiniJuvix.Prelude + +data IsImplicit = Explicit | Implicit + deriving stock (Show, Eq, Ord, Generic) + +instance Hashable IsImplicit diff --git a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker.hs new file mode 100644 index 000000000..85a215295 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker.hs @@ -0,0 +1,403 @@ +module MiniJuvix.Syntax.MicroJuvix.ArityChecker + ( module MiniJuvix.Syntax.MicroJuvix.ArityChecker, + module MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult, + module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error, + ) +where + +import MiniJuvix.Internal.NameIdGen +import MiniJuvix.Prelude hiding (fromEither) +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Arity +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.LocalVars +import MiniJuvix.Syntax.MicroJuvix.InfoTable +import MiniJuvix.Syntax.MicroJuvix.Language.Extra +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult + +entryMicroJuvixArity :: + Members '[Error ArityCheckerError, NameIdGen] r => + MicroJuvixResult -> + Sem r MicroJuvixArityResult +entryMicroJuvixArity res@MicroJuvixResult {..} = do + r <- runReader table (mapM checkModule _resultModules) + return + MicroJuvixArityResult + { _resultMicroJuvixResult = res, + _resultModules = r + } + where + table :: InfoTable + table = buildTable _resultModules + +checkModule :: + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + Module -> + Sem r Module +checkModule Module {..} = do + _moduleBody' <- checkModuleBody _moduleBody + return + Module + { _moduleBody = _moduleBody', + .. + } + +checkModuleBody :: + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + ModuleBody -> + Sem r ModuleBody +checkModuleBody ModuleBody {..} = do + _moduleStatements' <- mapM checkStatement _moduleStatements + return + ModuleBody + { _moduleStatements = _moduleStatements' + } + +checkInclude :: + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + Include -> + Sem r Include +checkInclude = traverseOf includeModule checkModule + +checkStatement :: + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + Statement -> + Sem r Statement +checkStatement s = case s of + StatementFunction fun -> StatementFunction <$> checkFunctionDef fun + StatementInclude i -> StatementInclude <$> checkInclude i + StatementForeign {} -> return s + StatementInductive {} -> return s + StatementAxiom {} -> return s + +checkFunctionDef :: + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + FunctionDef -> + Sem r FunctionDef +checkFunctionDef FunctionDef {..} = do + arity <- typeArity _funDefType + _funDefClauses' <- mapM (checkFunctionClause arity) _funDefClauses + return + FunctionDef + { _funDefClauses = _funDefClauses', + .. + } + +checkFunctionClause :: + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + Arity -> + FunctionClause -> + Sem r FunctionClause +checkFunctionClause ari cl = do + hint <- guessArity (cl ^. clauseBody) + (patterns', locals, bodyAri) <- checkLhs loc hint ari (cl ^. clausePatterns) + body' <- runReader locals (checkExpression bodyAri (cl ^. clauseBody)) + return + FunctionClause + { _clauseName = cl ^. clauseName, + _clausePatterns = patterns', + _clauseBody = body' + } + where + name = cl ^. clauseName + loc = getLoc name + +guessArity :: + forall r. + Members '[Reader InfoTable] r => + Expression -> + Sem r (Maybe Arity) +guessArity = \case + ExpressionTyped {} -> impossible + ExpressionHole {} -> return Nothing + ExpressionFunction {} -> return (Just ArityUnit) + ExpressionLiteral {} -> return (Just arityLiteral) + ExpressionApplication a -> appHelper a + ExpressionIden i -> idenHelper i + where + idenHelper :: Iden -> Sem r (Maybe Arity) + idenHelper i = case i of + IdenVar {} -> return Nothing + _ -> Just <$> runReader (LocalVars mempty) (idenArity i) + + appHelper :: Application -> Sem r (Maybe Arity) + appHelper a = do + f' <- arif + return (f' >>= \f'' -> foldArity <$> refine (unfoldArity f'') args) + where + (f, args) = second (map fst . toList) (unfoldApplication' a) + + refine :: [ArityParameter] -> [IsImplicit] -> Maybe [ArityParameter] + refine ps as = case (ps, as) of + (ParamExplicit {} : ps', Explicit : as') -> refine ps' as' + (ParamImplicit {} : ps', Implicit : as') -> refine ps' as' + (ParamImplicit {} : ps', as'@(Explicit : _)) -> refine ps' as' + (ParamExplicit {} : _, Implicit : _) -> Nothing + (ps', []) -> Just ps' + ([], _ : _) -> Nothing + + arif :: Sem r (Maybe Arity) + arif = case f of + ExpressionHole {} -> return Nothing + ExpressionApplication {} -> impossible + ExpressionFunction {} -> return (Just ArityUnit) + ExpressionLiteral {} -> return (Just arityLiteral) + ExpressionTyped {} -> impossible + ExpressionIden i -> idenHelper i + +arityLiteral :: Arity +arityLiteral = ArityUnit + +checkLhs :: + forall r. + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r => + Interval -> + Maybe Arity -> + Arity -> + [Pattern] -> + Sem r ([Pattern], LocalVars, Arity) +checkLhs loc hint ariSignature pats = do + (locals, (pats', bodyAri)) <- runState emptyLocalVars (goLhs ariSignature pats) + return (pats', locals, bodyAri) + where + -- returns the expanded patterns and the rest of the Arity (the arity of the + -- body once all the patterns have been processed). + -- Does not insert holes greedily. I.e. implicit wildcards are only inserted + -- between explicit parameters already in the pattern. + goLhs :: Arity -> [Pattern] -> Sem (State LocalVars ': r) ([Pattern], Arity) + goLhs a = \case + [] -> return $ case hint >>= tailHelper a of + Nothing -> ([], a) + Just tailUnderscores -> + let a' = foldArity (drop tailUnderscores (unfoldArity a)) + in (replicate tailUnderscores wildcard, a') + lhs@(p : ps) -> case a of + ArityUnit -> + throw + ( ErrLhsTooManyPatterns + LhsTooManyPatterns + { _lhsTooManyPatternsRemaining = p :| ps + } + ) + ArityUnknown -> do + p' <- checkPattern ArityUnknown p + first (p' :) <$> goLhs ArityUnknown ps + ArityFunction (FunctionArity l r) -> + case (getPatternBraces p, l) of + (Just b, ParamImplicit) -> do + b' <- checkPattern (arityParameter l) b + first (b' :) <$> goLhs r ps + (Just x, ParamExplicit {}) -> + throw + ( ErrExpectedExplicitPattern + ExpectedExplicitPattern + { _expectedExplicitPattern = x + } + ) + (Nothing, ParamImplicit) -> + first (wildcard :) <$> goLhs r lhs + (Nothing, ParamExplicit pa) -> do + p' <- checkPattern pa p + first (p' :) <$> goLhs r ps + where + wildcard :: Pattern + wildcard = PatternBraces (PatternWildcard (Wildcard loc)) + + tailHelper :: Arity -> Arity -> Maybe Int + tailHelper a target + | notNull a' && all (== ParamImplicit) a' = Just (length a') + | otherwise = Nothing + where + a' = dropSuffix target' (unfoldArity a) + target' = unfoldArity target + + getPatternBraces :: Pattern -> Maybe Pattern + getPatternBraces p = case p of + PatternBraces {} -> Just p + _ -> Nothing + +checkPattern :: + Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r => + Arity -> + Pattern -> + Sem r Pattern +checkPattern ari = \case + PatternBraces p -> checkPattern ari p + PatternVariable v -> addArity v ari $> PatternVariable v + PatternWildcard i -> return (PatternWildcard i) + PatternConstructorApp c -> case ari of + ArityUnit -> PatternConstructorApp <$> checkConstructorApp c + ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c + ArityFunction {} -> + throw + ( ErrPatternFunction + PatternFunction + { _patternFunction = c + } + ) + +checkConstructorApp :: + forall r. + Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r => + ConstructorApp -> + Sem r ConstructorApp +checkConstructorApp ca@(ConstructorApp c ps) = do + args <- (^. constructorInfoArgs) <$> lookupConstructor c + arities <- mapM typeArity args + let n = length arities + lps = length ps + when + (n /= lps) + ( throw + ( ErrWrongConstructorAppLength + WrongConstructorAppLength + { _wrongConstructorAppLength = ca, + _wrongConstructorAppLengthExpected = n + } + ) + ) + ps' <- zipWithM checkPattern arities ps + return (ConstructorApp c ps') + +idenArity :: Members '[Reader LocalVars, Reader InfoTable] r => Iden -> Sem r Arity +idenArity = \case + IdenFunction f -> lookupFunction f >>= typeArity . (^. functionInfoDef . funDefType) + IdenConstructor c -> constructorType c >>= typeArity + IdenVar v -> getLocalArity v + IdenAxiom a -> lookupAxiom a >>= typeArity . (^. axiomInfoType) + IdenInductive i -> inductiveType i >>= typeArity + +typeArity :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Arity +typeArity = go + where + go :: Type -> Sem r Arity + go = \case + TypeIden i -> goIden i + TypeApp {} -> return ArityUnit + TypeFunction f -> ArityFunction <$> goFun f + TypeAbs f -> ArityFunction <$> goAbs f + TypeHole {} -> return ArityUnknown + TypeUniverse {} -> return ArityUnit + TypeAny {} -> return ArityUnknown + + goIden :: TypeIden -> Sem r Arity + goIden = \case + TypeIdenVariable {} -> return ArityUnknown + TypeIdenInductive {} -> return ArityUnit + TypeIdenAxiom ax -> do + ty <- (^. axiomInfoType) <$> lookupAxiom ax + go ty + + goFun :: Function -> Sem r FunctionArity + goFun (Function l r) = do + l' <- ParamExplicit <$> go l + r' <- go r + return + FunctionArity + { _functionArityLeft = l', + _functionArityRight = r' + } + goAbs :: TypeAbstraction -> Sem r FunctionArity + goAbs t = do + r' <- go (t ^. typeAbsBody) + return (FunctionArity l r') + where + l :: ArityParameter + l = case t ^. typeAbsImplicit of + Implicit -> ParamImplicit + Explicit -> ParamExplicit ArityUnit + +checkExpression :: + forall r. + Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r => + Arity -> + Expression -> + Sem r Expression +checkExpression hintArity expr = case expr of + ExpressionIden {} -> appHelper expr [] + ExpressionApplication a -> goApp a + ExpressionLiteral {} -> return expr + ExpressionFunction {} -> return expr + ExpressionHole {} -> return expr + ExpressionTyped {} -> impossible + where + goApp :: Application -> Sem r Expression + goApp = uncurry appHelper . second toList . unfoldApplication' + + appHelper :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression + appHelper fun args = do + args' :: [(IsImplicit, Expression)] <- case fun of + ExpressionHole {} -> mapM (secondM (checkExpression ArityUnknown)) args + ExpressionIden i -> do + ari <- idenArity i + let argsAris :: [Arity] + argsAris = map toArity (unfoldArity ari) + toArity :: ArityParameter -> Arity + toArity = \case + ParamExplicit a -> a + ParamImplicit -> ArityUnit + mapM + (secondM (uncurry checkExpression)) + [(i', (a, e')) | (a, (i', e')) <- zip (argsAris ++ repeat ArityUnknown) args] + >>= addHoles (getLoc i) hintArity ari + ExpressionLiteral {} -> error "TODO literals on the left of an application" + ExpressionFunction f -> + throw + ( ErrFunctionApplied + FunctionApplied + { _functionAppliedFunction = f, + _functionAppliedArguments = args + } + ) + ExpressionApplication {} -> impossible + ExpressionTyped {} -> impossible + return (foldApplication fun args') + where + addHoles :: + Interval -> + Arity -> + Arity -> + [(IsImplicit, Expression)] -> + Sem r [(IsImplicit, Expression)] + addHoles loc hint = go 0 + where + go :: + Int -> + Arity -> + [(IsImplicit, Expression)] -> + Sem r [(IsImplicit, Expression)] + go idx ari goargs = case (ari, goargs) of + (ArityFunction (FunctionArity ParamImplicit r), (Implicit, e) : rest) -> + ((Implicit, e) :) <$> go (succ idx) r rest + (ArityFunction (FunctionArity (ParamExplicit {}) r), (Explicit, e) : rest) -> + ((Explicit, e) :) <$> go (succ idx) r rest + (ArityFunction (FunctionArity ParamImplicit _), []) + -- When there are no remaining arguments and the expected arity of the + -- expression matches the current arity we should *not* insert a hole. + | ari == hint -> return [] + (ArityFunction (FunctionArity ParamImplicit r), _) -> do + h <- newHole loc + ((Implicit, ExpressionHole h) :) <$> go (succ idx) r goargs + (ArityFunction (FunctionArity (ParamExplicit {}) _), (Implicit, _) : _) -> + throw + ( ErrExpectedExplicitArgument + ExpectedExplicitArgument + { _expectedExplicitArgumentApp = (fun, args), + _expectedExplicitArgumentIx = idx + } + ) + (ArityUnit, []) -> return [] + (ArityFunction (FunctionArity (ParamExplicit _) _), []) -> return [] + (ArityUnit, _ : _) -> + throw + ( ErrTooManyArguments + TooManyArguments + { _tooManyArgumentsApp = (fun, args), + _tooManyArgumentsUnexpected = length goargs + } + ) + (ArityUnknown, []) -> return [] + (ArityUnknown, p : ps) -> (p :) <$> go (succ idx) ArityUnknown ps + +newHole :: Member NameIdGen r => Interval -> Sem r Hole +newHole loc = (`Hole` loc) <$> freshNameId diff --git a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Arity.hs b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Arity.hs new file mode 100644 index 000000000..9f2ee1a78 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Arity.hs @@ -0,0 +1,45 @@ +module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Arity where + +import MiniJuvix.Prelude + +data Arity + = ArityUnit + | ArityFunction FunctionArity + | ArityUnknown + deriving stock (Eq) + +data FunctionArity = FunctionArity + { _functionArityLeft :: ArityParameter, + _functionArityRight :: Arity + } + deriving stock (Eq) + +data ArityParameter + = ParamExplicit Arity + | ParamImplicit + deriving stock (Eq) + +arityParameter :: ArityParameter -> Arity +arityParameter = \case + ParamImplicit -> ArityUnit + ParamExplicit a -> a + +unfoldArity :: Arity -> [ArityParameter] +unfoldArity = go + where + go :: Arity -> [ArityParameter] + go = \case + ArityUnit -> [] + ArityUnknown -> [] + ArityFunction (FunctionArity l r) -> l : unfoldArity r + +foldArity :: [ArityParameter] -> Arity +foldArity = go + where + go = \case + [] -> ArityUnit + (a : as) -> ArityFunction (FunctionArity l (go as)) + where + l = case a of + ParamExplicit e -> ParamExplicit e + ParamImplicit -> ParamImplicit diff --git a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error.hs new file mode 100644 index 000000000..185eca025 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error.hs @@ -0,0 +1,28 @@ +module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error + ( module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error, + module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error.Types, + ) +where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error.Types + +data ArityCheckerError + = ErrWrongConstructorAppLength WrongConstructorAppLength + | ErrLhsTooManyPatterns LhsTooManyPatterns + | ErrExpectedExplicitPattern ExpectedExplicitPattern + | ErrExpectedExplicitArgument ExpectedExplicitArgument + | ErrPatternFunction PatternFunction + | ErrTooManyArguments TooManyArguments + | ErrFunctionApplied FunctionApplied + +instance ToGenericError ArityCheckerError where + genericError :: ArityCheckerError -> GenericError + genericError = \case + ErrWrongConstructorAppLength e -> genericError e + ErrLhsTooManyPatterns e -> genericError e + ErrExpectedExplicitPattern e -> genericError e + ErrExpectedExplicitArgument e -> genericError e + ErrPatternFunction e -> genericError e + ErrTooManyArguments e -> genericError e + ErrFunctionApplied e -> genericError e diff --git a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs new file mode 100644 index 000000000..61ec88471 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs @@ -0,0 +1,195 @@ +module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error.Types where + +-- import MiniJuvix.Syntax.MicroJuvix.Error.Pretty +import MiniJuvix.Prelude +import MiniJuvix.Prelude.Pretty +import MiniJuvix.Syntax.MicroJuvix.Error.Pretty +import MiniJuvix.Syntax.MicroJuvix.Language.Extra + +data WrongConstructorAppLength = WrongConstructorAppLength + { _wrongConstructorAppLength :: ConstructorApp, + _wrongConstructorAppLengthExpected :: Int + } + +makeLenses ''WrongConstructorAppLength + +instance ToGenericError WrongConstructorAppLength where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLoc (e ^. wrongConstructorAppLength) + msg = + "The constructor" + <+> ppCode (e ^. wrongConstructorAppLength . constrAppConstructor) + <+> "should have" + <+> arguments (e ^. wrongConstructorAppLengthExpected) + <> ", but has been given" + <+> pretty actual + + actual :: Int + actual = length (e ^. wrongConstructorAppLength . constrAppParameters) + arguments :: Int -> Doc ann + arguments n = num <+> plural "argument" "arguments" n + where + num + | n == 0 = "no" + | otherwise = pretty n + +newtype LhsTooManyPatterns = LhsTooManyPatterns + { _lhsTooManyPatternsRemaining :: NonEmpty Pattern + } + +makeLenses ''LhsTooManyPatterns + +instance ToGenericError LhsTooManyPatterns where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLocSpan (e ^. lhsTooManyPatternsRemaining) + n = length (e ^. lhsTooManyPatternsRemaining) + howMany = + "The last" <+> case n of + 1 -> "pattern" + _ -> pretty n <+> "patterns" + msg = + howMany <+> "on the left hand side of the function clause" <+> wasWere <+> "not expected" + wasWere + | n == 1 = "was" + | otherwise = "were" + +newtype ExpectedExplicitPattern = ExpectedExplicitPattern + { _expectedExplicitPattern :: Pattern + } + +makeLenses ''ExpectedExplicitPattern + +instance ToGenericError ExpectedExplicitPattern where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLoc (e ^. expectedExplicitPattern) + msg = + "Expected an explicit pattern but found an implicit pattern" + <+> ppCode (e ^. expectedExplicitPattern) + +data ExpectedExplicitArgument = ExpectedExplicitArgument + { _expectedExplicitArgumentApp :: (Expression, [(IsImplicit, Expression)]), + _expectedExplicitArgumentIx :: Int + } + +makeLenses ''ExpectedExplicitArgument + +instance ToGenericError ExpectedExplicitArgument where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + app@(f, args) = e ^. expectedExplicitArgumentApp + idx = e ^. expectedExplicitArgumentIx + arg :: Expression + arg = snd (toList args !! idx) + i = getLoc arg + msg = + "Expected an explicit argument as the" <+> ordinal (succ idx) <+> "argument of" + <+> ppCode f + <+> "but found" + <+> ppArg Implicit arg + <> "." + <> softline + <> "In the application" + <+> ppApp app + +newtype PatternFunction = PatternFunction + { _patternFunction :: ConstructorApp + } + +makeLenses ''PatternFunction + +instance ToGenericError PatternFunction where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLoc (e ^. patternFunction) + msg = + "Invalid pattern" <+> ppCode (e ^. patternFunction) <> "." + <+> "Function types cannot be pattern matched" + +data TooManyArguments = TooManyArguments + { _tooManyArgumentsApp :: (Expression, [(IsImplicit, Expression)]), + _tooManyArgumentsUnexpected :: Int + } + +makeLenses ''TooManyArguments + +instance ToGenericError TooManyArguments where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLocSpan (fromJust (nonEmpty (map snd unexpectedArgs))) + (fun, args) = e ^. tooManyArgumentsApp + numUnexpected :: Int + numUnexpected = e ^. tooManyArgumentsUnexpected + unexpectedArgs :: [(IsImplicit, Expression)] + unexpectedArgs = reverse . take numUnexpected . reverse $ args + ppUnexpectedArgs = hsep (map (uncurry ppArg) unexpectedArgs) + app :: Expression + app = foldApplication fun args + msg = + "Too many arguments in the application" <+> ppCode app <> "." + <+> "The last" + <+> numArguments + <> ", namely" + <+> ppUnexpectedArgs + <> "," + <+> wasNotExpected + numArguments :: Doc ann + numArguments = plural "argument" (pretty numUnexpected <+> "arguments") numUnexpected + wasNotExpected :: Doc ann + wasNotExpected + | numUnexpected == 1 = "was not expected" + | otherwise = "were not expected" + +data FunctionApplied = FunctionApplied + { _functionAppliedFunction :: FunctionExpression, + _functionAppliedArguments :: [(IsImplicit, Expression)] + } + +makeLenses ''FunctionApplied + +instance ToGenericError FunctionApplied where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i = getLocSpan (fun :| map snd args) + args = e ^. functionAppliedArguments + fun = ExpressionFunction (e ^. functionAppliedFunction) + msg = + "A function type cannot be applied." <> softline + <> "In the application" <+> ppApp (fun, args) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/LocalVars.hs b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/LocalVars.hs new file mode 100644 index 000000000..dfe50f208 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/LocalVars.hs @@ -0,0 +1,24 @@ +module MiniJuvix.Syntax.MicroJuvix.ArityChecker.LocalVars where + +import Data.HashMap.Strict qualified as HashMap +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Arity +import MiniJuvix.Syntax.MicroJuvix.Language + +newtype LocalVars = LocalVars + { _localArities :: HashMap VarName Arity + } + +makeLenses ''LocalVars + +addArity :: Member (State LocalVars) r => VarName -> Arity -> Sem r () +addArity v t = modify (over localArities (HashMap.insert v t)) + +getLocalArity :: Member (Reader LocalVars) r => VarName -> Sem r Arity +getLocalArity v = fromJust <$> asks (^. localArities . at v) + +emptyLocalVars :: LocalVars +emptyLocalVars = + LocalVars + { _localArities = mempty + } diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs index 038eec67c..b09d4e991 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs @@ -2,17 +2,18 @@ module MiniJuvix.Syntax.MicroJuvix.Error ( module MiniJuvix.Syntax.MicroJuvix.Error, module MiniJuvix.Syntax.MicroJuvix.Error.Pretty, module MiniJuvix.Syntax.MicroJuvix.Error.Types, + module MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error, ) where import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error import MiniJuvix.Syntax.MicroJuvix.Error.Pretty import MiniJuvix.Syntax.MicroJuvix.Error.Types data TypeCheckerError - = ErrTooManyPatterns TooManyPatterns - | ErrWrongConstructorType WrongConstructorType - | ErrWrongConstructorAppArgs WrongConstructorAppArgs + = ErrWrongConstructorType WrongConstructorType + | ErrArity ArityCheckerError | ErrWrongType WrongType | ErrUnsolvedMeta UnsolvedMeta | ErrExpectedFunctionType ExpectedFunctionType @@ -20,9 +21,8 @@ data TypeCheckerError instance ToGenericError TypeCheckerError where genericError :: TypeCheckerError -> GenericError genericError = \case - ErrTooManyPatterns e -> genericError e ErrWrongConstructorType e -> genericError e - ErrWrongConstructorAppArgs e -> genericError e + ErrArity e -> genericError e ErrWrongType e -> genericError e ErrUnsolvedMeta e -> genericError e ErrExpectedFunctionType e -> genericError e diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs index 7216891a0..04da692aa 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs @@ -1,17 +1,26 @@ module MiniJuvix.Syntax.MicroJuvix.Error.Pretty ( module MiniJuvix.Syntax.MicroJuvix.Error.Pretty, module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ann, + module MiniJuvix.Prelude.Pretty, ) where import MiniJuvix.Prelude import MiniJuvix.Prelude.Pretty +import MiniJuvix.Syntax.Fixity import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ann import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi qualified as Ansi +import MiniJuvix.Syntax.MicroJuvix.Language.Extra import MiniJuvix.Syntax.MicroJuvix.Pretty.Base qualified as Micro ppCode :: Micro.PrettyCode c => c -> Doc Eann -ppCode = reAnnotate MicroAnn . Micro.runPrettyCode Micro.defaultOptions +ppCode = runPP . Micro.ppCode + +ppAtom :: (Micro.PrettyCode c, HasAtomicity c) => c -> Doc Eann +ppAtom = runPP . Micro.ppCodeAtom + +runPP :: Sem '[Reader Micro.Options] (Doc Micro.Ann) -> Doc Eann +runPP = highlight_ . reAnnotate MicroAnn . run . runReader Micro.defaultOptions newtype PPOutput = PPOutput (Doc Eann) @@ -29,5 +38,14 @@ instance HasTextBackend PPOutput where indent' :: Doc ann -> Doc ann indent' = indent 2 -highlight :: Doc Eann -> Doc Eann -highlight = annotate Highlight +highlight_ :: Doc Eann -> Doc Eann +highlight_ = annotate Highlight + +ppApp :: (Expression, [(IsImplicit, Expression)]) -> Doc Eann +ppApp (fun, args) = + hsep (ppAtom fun : map (uncurry ppArg) args) + +ppArg :: IsImplicit -> Expression -> Doc Eann +ppArg im arg = case im of + Implicit -> braces (ppCode arg) + Explicit -> ppAtom arg diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs index 06a18763f..fe7e2df83 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs @@ -11,5 +11,5 @@ renderAnsi = renderStrict . reAnnotateS stylize stylize :: Eann -> AnsiStyle stylize a = case a of - Highlight -> colorDull Red + Highlight -> bold MicroAnn m -> M.stylize m diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs index 866aff5ec..93f335862 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs @@ -13,7 +13,6 @@ data WrongConstructorType = WrongConstructorType _wrongCtorTypeActual :: InductiveName, _wrongCtorTypeFunName :: Name } - deriving stock (Show) makeLenses ''WrongConstructorType @@ -60,7 +59,6 @@ data WrongConstructorAppArgs = WrongConstructorAppArgs _wrongCtorAppTypes :: [FunctionArgType], _wrongCtorAppName :: Name } - deriving stock (Show) makeLenses ''WrongConstructorAppArgs @@ -98,7 +96,6 @@ data WrongType = WrongType _wrongTypeExpectedType :: Type, _wrongTypeInferredType :: Type } - deriving stock (Show) makeLenses ''WrongType @@ -112,7 +109,7 @@ instance ToGenericError WrongType where where i = getLoc (e ^. wrongTypeExpression) msg = - "Type error near" <+> highlight (pretty (getLoc subjectExpr)) <> "." + "Type error near" <+> pretty (getLoc subjectExpr) <> "." <> line <> "The expression" <+> ppCode subjectExpr <+> "has type:" <> line @@ -132,7 +129,6 @@ data ExpectedFunctionType = ExpectedFunctionType _expectedFunctionTypeApp :: Expression, _expectedFunctionTypeType :: Type } - deriving stock (Show) makeLenses ''ExpectedFunctionType @@ -146,7 +142,7 @@ instance ToGenericError ExpectedFunctionType where where i = getLoc (e ^. expectedFunctionTypeExpression) msg = - "Type error near" <+> highlight (pretty (getLoc subjectExpr)) <> "." + "Type error near" <+> pretty (getLoc subjectExpr) <> "." <> line <> "In the expression:" <> line @@ -157,36 +153,3 @@ instance ToGenericError ExpectedFunctionType where <> indent' (ppCode (e ^. expectedFunctionTypeType)) subjectExpr :: Expression subjectExpr = e ^. expectedFunctionTypeExpression - --- | A function definition clause matches too many arguments -data TooManyPatterns = TooManyPatterns - { _tooManyPatternsClause :: FunctionClause, - _tooManyPatternsTypes :: [FunctionArgType] - } - deriving stock (Show) - -makeLenses ''TooManyPatterns - -instance ToGenericError TooManyPatterns where - genericError e = - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [i] - } - where - i = getLoc (e ^. tooManyPatternsClause . clauseName) - - name :: Name - name = e ^. tooManyPatternsClause . clauseName - - msg = - "Type error near" <+> highlight (pretty (name ^. nameDefined)) - <> line - <> "In in the definition of" <+> ppCode name <+> "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/InfoTable.hs b/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs index 430c0f960..585bb2ee2 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs @@ -2,7 +2,7 @@ module MiniJuvix.Syntax.MicroJuvix.InfoTable where import Data.HashMap.Strict qualified as HashMap import MiniJuvix.Prelude -import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.MicroJuvix.Language.Extra data ConstructorInfo = ConstructorInfo { _constructorInfoInductiveParameters :: [InductiveParameter], @@ -103,3 +103,42 @@ 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) + +inductiveType :: Member (Reader InfoTable) r => Name -> Sem r Type +inductiveType v = do + info <- lookupInductive v + let ps = info ^. inductiveInfoDef . inductiveParameters + return $ + foldr + (\p k -> TypeAbs (TypeAbstraction (p ^. inductiveParamName) Explicit k)) + TypeUniverse + ps + +constructorArgTypes :: ConstructorInfo -> ([VarName], [Type]) +constructorArgTypes i = + ( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters), + i ^. constructorInfoArgs + ) + +constructorType :: Member (Reader InfoTable) r => Name -> Sem r Type +constructorType c = do + info <- lookupConstructor c + let (inductiveParams, constrArgs) = constructorArgTypes info + args = + map (\ty -> FunctionArgTypeAbstraction (Implicit, ty)) inductiveParams + ++ map FunctionArgTypeType constrArgs + ind = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) + saturatedTy = + foldl' + ( \t v -> + TypeApp + ( TypeApplication + { _typeAppLeft = t, + _typeAppRight = TypeIden (TypeIdenVariable v), + _typeAppImplicit = Implicit + } + ) + ) + ind + inductiveParams + return (foldFunType args saturatedTy) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs index 685ec7607..64cf02780 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs @@ -3,18 +3,23 @@ module MiniJuvix.Syntax.MicroJuvix.Language module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind, module MiniJuvix.Syntax.Concrete.Scoped.Name, module MiniJuvix.Syntax.Concrete.Loc, + module MiniJuvix.Syntax.IsImplicit, module MiniJuvix.Syntax.Hole, + module MiniJuvix.Syntax.Wildcard, + module MiniJuvix.Syntax.Concrete.LiteralLoc, ) where import MiniJuvix.Prelude -import MiniJuvix.Syntax.Concrete.Language (LiteralLoc) +import MiniJuvix.Syntax.Concrete.LiteralLoc import MiniJuvix.Syntax.Concrete.Loc import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..)) import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind import MiniJuvix.Syntax.Fixity import MiniJuvix.Syntax.ForeignBlock import MiniJuvix.Syntax.Hole +import MiniJuvix.Syntax.IsImplicit +import MiniJuvix.Syntax.Wildcard import Prettyprinter type FunctionName = Name @@ -97,7 +102,6 @@ data FunctionClause = FunctionClause _clausePatterns :: [Pattern], _clauseBody :: Expression } - deriving stock (Show) data Iden = IdenFunction Name @@ -105,19 +109,16 @@ data Iden | IdenVar VarName | IdenAxiom Name | IdenInductive Name - deriving stock (Show) data TypedExpression = TypedExpression { _typedType :: Type, _typedExpression :: Expression } - deriving stock (Show) data FunctionExpression = FunctionExpression { _functionExpressionLeft :: Expression, _functionExpressionRight :: Expression } - deriving stock (Show) data Expression = ExpressionIden Iden @@ -126,19 +127,18 @@ data Expression | ExpressionLiteral LiteralLoc | ExpressionHole Hole | ExpressionTyped TypedExpression - deriving stock (Show) data Application = Application { _appLeft :: Expression, - _appRight :: Expression + _appRight :: Expression, + _appImplicit :: IsImplicit } - deriving stock (Show) data Function = Function { _funLeft :: Type, _funRight :: Type } - deriving stock (Show, Generic, Eq) + deriving stock (Eq, Generic) instance Hashable Function @@ -147,18 +147,17 @@ data ConstructorApp = ConstructorApp { _constrAppConstructor :: Name, _constrAppParameters :: [Pattern] } - deriving stock (Show) data Pattern = PatternVariable VarName | PatternConstructorApp ConstructorApp - | PatternWildcard - deriving stock (Show) + | PatternWildcard Wildcard + | PatternBraces Pattern newtype InductiveParameter = InductiveParameter { _inductiveParamName :: VarName } - deriving stock (Show, Eq) + deriving stock (Eq) data InductiveDef = InductiveDef { _inductiveName :: InductiveName, @@ -175,23 +174,25 @@ data TypeIden = TypeIdenInductive InductiveName | TypeIdenAxiom AxiomName | TypeIdenVariable VarName - deriving stock (Show, Eq, Generic) + deriving stock (Eq, Generic) instance Hashable TypeIden data TypeApplication = TypeApplication { _typeAppLeft :: Type, - _typeAppRight :: Type + _typeAppRight :: Type, + _typeAppImplicit :: IsImplicit } - deriving stock (Show, Generic, Eq) + deriving stock (Generic, Eq) instance Hashable TypeApplication data TypeAbstraction = TypeAbstraction { _typeAbsVar :: VarName, + _typeAbsImplicit :: IsImplicit, _typeAbsBody :: Type } - deriving stock (Show, Eq, Generic) + deriving stock (Eq, Generic) instance Hashable TypeAbstraction @@ -203,14 +204,13 @@ data Type | TypeHole Hole | TypeUniverse | TypeAny - deriving stock (Eq, Show, Generic) + deriving stock (Eq, Generic) instance Hashable Type data FunctionArgType - = FunctionArgTypeAbstraction VarName + = FunctionArgTypeAbstraction (IsImplicit, VarName) | FunctionArgTypeType Type - deriving stock (Show) makeLenses ''Module makeLenses ''Include @@ -276,6 +276,7 @@ instance HasAtomicity Pattern where PatternConstructorApp a -> atomicity a PatternVariable {} -> Atom PatternWildcard {} -> Atom + PatternBraces {} -> Atom instance HasLoc FunctionExpression where getLoc (FunctionExpression l r) = getLoc l <> getLoc r @@ -296,3 +297,16 @@ instance HasLoc Iden where IdenVar v -> getLoc v IdenAxiom a -> getLoc a IdenInductive a -> getLoc a + +instance HasLoc Pattern where + getLoc = \case + PatternVariable v -> getLoc v + PatternConstructorApp a -> getLoc a + PatternBraces p -> getLoc p + PatternWildcard i -> getLoc i + +instance HasLoc ConstructorApp where + getLoc (ConstructorApp c ps) = + case last <$> nonEmpty ps of + Just p -> getLoc c <> getLoc p + Nothing -> getLoc c diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs index 2cf296b67..3a9c370de 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs @@ -88,10 +88,10 @@ mkConcreteType = fmap ConcreteType . go where go :: Type -> Maybe Type go t = case t of - TypeApp (TypeApplication l r) -> do + TypeApp (TypeApplication l r i) -> do l' <- go l r' <- go r - return (TypeApp (TypeApplication l' r')) + return (TypeApp (TypeApplication l' r' i)) TypeAny -> return TypeAny TypeUniverse -> return TypeUniverse TypeFunction (Function l r) -> do @@ -115,9 +115,9 @@ findHoles = go go :: Type -> HashSet Hole go = \case TypeIden {} -> mempty - TypeApp (TypeApplication a b) -> go a <> go b + TypeApp (TypeApplication a b _) -> go a <> go b TypeFunction (Function a b) -> go a <> go b - TypeAbs (TypeAbstraction _ t) -> go t + TypeAbs a -> go (a ^. typeAbsBody) TypeHole h -> HashSet.singleton h TypeUniverse -> mempty TypeAny -> mempty @@ -145,7 +145,7 @@ typeAsExpression = go TypeIdenAxiom a -> IdenAxiom a TypeIdenVariable v -> IdenVar v goApp :: TypeApplication -> Application - goApp (TypeApplication l r) = Application (go l) (go r) + goApp (TypeApplication l r i) = Application (go l) (go r) i goFunction :: Function -> FunctionExpression goFunction (Function l r) = FunctionExpression (go l) (go r) @@ -179,7 +179,7 @@ fillHoles m = goe ) where goApp :: Application -> Application - goApp (Application l r) = Application (goe l) (goe r) + goApp (Application l r i) = Application (goe l) (goe r) i goFunction :: FunctionExpression -> FunctionExpression goFunction (FunctionExpression l r) = FunctionExpression (goe l) (goe r) goHole :: Hole -> Expression @@ -201,9 +201,9 @@ fillHolesType m = go TypeHole h -> goHole h where goApp :: TypeApplication -> TypeApplication - goApp (TypeApplication l r) = TypeApplication (go l) (go r) + goApp (TypeApplication l r i) = TypeApplication (go l) (go r) i goAbs :: TypeAbstraction -> TypeAbstraction - goAbs (TypeAbstraction v b) = TypeAbstraction v (go b) + goAbs (TypeAbstraction v i b) = TypeAbstraction v i (go b) goFunction :: Function -> Function goFunction (Function l r) = Function (go l) (go r) goHole :: Hole -> Type @@ -235,10 +235,10 @@ expressionAsType = go IdenAxiom a -> Just (TypeIdenAxiom a) IdenInductive i -> Just (TypeIdenInductive i) goApp :: Application -> Maybe TypeApplication - goApp (Application l r) = do + goApp (Application l r i) = do l' <- go l r' <- go r - return (TypeApplication l' r') + return (TypeApplication l' r' i) substituteIndParams :: [(InductiveParameter, Type)] -> Type -> Type substituteIndParams = substitution . HashMap.fromList . map (first (^. inductiveParamName)) @@ -263,7 +263,8 @@ patternVariables :: Pattern -> [VarName] patternVariables = \case PatternVariable v -> [v] PatternConstructorApp a -> goApp a - PatternWildcard -> [] + PatternBraces b -> patternVariables b + PatternWildcard {} -> [] where goApp :: ConstructorApp -> [VarName] goApp (ConstructorApp _ ps) = concatMap patternVariables ps @@ -326,7 +327,7 @@ concreteTypeToExpr = go . (^. unconcreteType) go = \case TypeAbs {} -> impossible TypeIden i -> ExpressionIden (goIden i) - TypeApp (TypeApplication l r) -> ExpressionApplication (Application (go l) (go r)) + TypeApp (TypeApplication l r i) -> ExpressionApplication (Application (go l) (go r) i) TypeFunction (Function l r) -> ExpressionFunction (FunctionExpression (go l) (go r)) TypeUniverse {} -> impossible TypeAny {} -> impossible @@ -352,7 +353,7 @@ substitutionE m = go ExpressionFunction f -> ExpressionFunction (goFunction f) ExpressionTyped t -> ExpressionTyped (over typedExpression go t) goApp :: Application -> Application - goApp (Application l r) = Application (go l) (go r) + goApp (Application l r i) = Application (go l) (go r) i goFunction :: FunctionExpression -> FunctionExpression goFunction (FunctionExpression l r) = FunctionExpression (go l) (go r) goIden :: Iden -> Expression @@ -373,12 +374,16 @@ substitution m = go TypeUniverse -> TypeUniverse TypeAny -> TypeAny TypeHole h -> TypeHole h + goApp :: TypeApplication -> TypeApplication - goApp (TypeApplication l r) = TypeApplication (go l) (go r) + goApp (TypeApplication l r i) = TypeApplication (go l) (go r) i + goAbs :: TypeAbstraction -> TypeAbstraction - goAbs (TypeAbstraction v b) = TypeAbstraction v (go b) + goAbs (TypeAbstraction v i b) = TypeAbstraction v i (go b) + goFunction :: Function -> Function goFunction (Function l r) = Function (go l) (go r) + goIden :: TypeIden -> Type goIden i = case i of TypeIdenInductive {} -> TypeIden i @@ -394,14 +399,14 @@ foldFunType l r = case l of (a : as) -> let r' = foldFunType as r in case a of - FunctionArgTypeAbstraction v -> TypeAbs (TypeAbstraction v r') + FunctionArgTypeAbstraction (i, v) -> TypeAbs (TypeAbstraction v i r') FunctionArgTypeType t -> TypeFunction (Function t r') -- | a -> (b -> c) ==> ([a, b], c) unfoldFunType :: Type -> ([FunctionArgType], Type) unfoldFunType t = case t of TypeFunction (Function l r) -> first (FunctionArgTypeType l :) (unfoldFunType r) - TypeAbs (TypeAbstraction var r) -> first (FunctionArgTypeAbstraction var :) (unfoldFunType r) + TypeAbs (TypeAbstraction var i r) -> first (FunctionArgTypeAbstraction (i, var) :) (unfoldFunType r) _ -> ([], t) unfoldFunConcreteType :: ConcreteType -> ([ConcreteType], ConcreteType) @@ -414,28 +419,34 @@ unfoldFunConcreteType = bimap (map mkConcreteType') mkConcreteType' . go . (^. u unfoldTypeAbsType :: Type -> ([VarName], Type) unfoldTypeAbsType t = case t of - TypeAbs (TypeAbstraction var r) -> first (var :) (unfoldTypeAbsType r) + TypeAbs (TypeAbstraction var _ r) -> first (var :) (unfoldTypeAbsType r) _ -> ([], t) -foldApplication :: Expression -> [Expression] -> Expression +foldExplicitApplication :: Expression -> [Expression] -> Expression +foldExplicitApplication f = foldApplication f . zip (repeat Explicit) + +foldApplication :: Expression -> [(IsImplicit, Expression)] -> Expression foldApplication f args = case args of [] -> f - (a : as) -> foldApplication (ExpressionApplication (Application f a)) as + ((i, a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as -unfoldApplication :: Application -> (Expression, NonEmpty Expression) -unfoldApplication (Application l' r') = second (|: r') (unfoldExpression l') +unfoldApplication' :: Application -> (Expression, NonEmpty (IsImplicit, Expression)) +unfoldApplication' (Application l' r' i') = second (|: (i', r')) (unfoldExpression l') where - unfoldExpression :: Expression -> (Expression, [Expression]) + unfoldExpression :: Expression -> (Expression, [(IsImplicit, Expression)]) unfoldExpression e = case e of - ExpressionApplication (Application l r) -> - second (`snoc` r) (unfoldExpression l) + ExpressionApplication (Application l r i) -> + second (`snoc` (i, r)) (unfoldExpression l) ExpressionTyped t -> unfoldExpression (t ^. typedExpression) _ -> (e, []) +unfoldApplication :: Application -> (Expression, NonEmpty Expression) +unfoldApplication = fmap (fmap snd) . unfoldApplication' + unfoldTypeApplication :: TypeApplication -> (Type, NonEmpty Type) -unfoldTypeApplication (TypeApplication l' r') = second (|: r') (unfoldType l') +unfoldTypeApplication (TypeApplication l' r' _) = second (|: r') (unfoldType l') where unfoldType :: Type -> (Type, [Type]) unfoldType t = case t of - TypeApp (TypeApplication l r) -> second (`snoc` r) (unfoldType l) + TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l) _ -> (t, []) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs b/src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs index c4cd8db35..daec12806 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/LocalVars.hs @@ -8,7 +8,6 @@ data LocalVars = LocalVars { _localTypes :: HashMap VarName Type, _localTyMap :: HashMap VarName VarName } - deriving stock (Show) makeLenses ''LocalVars diff --git a/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs b/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs new file mode 100644 index 000000000..7c463ffd8 --- /dev/null +++ b/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs @@ -0,0 +1,18 @@ +module MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult + ( module MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult, + ) +where + +import MiniJuvix.Prelude +import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult (MicroJuvixResult) + +data MicroJuvixArityResult = MicroJuvixArityResult + { _resultMicroJuvixResult :: MicroJuvixResult, + _resultModules :: NonEmpty Module + } + +makeLenses ''MicroJuvixArityResult + +mainModule :: Lens' MicroJuvixArityResult Module +mainModule = resultModules . _head diff --git a/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs b/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs index 949baccd4..f4617e73f 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs @@ -7,10 +7,10 @@ where import MiniJuvix.Prelude import MiniJuvix.Syntax.MicroJuvix.InfoTable import MiniJuvix.Syntax.MicroJuvix.Language -import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult (MicroJuvixResult) +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult (MicroJuvixArityResult) data MicroJuvixTypedResult = MicroJuvixTypedResult - { _resultMicroJuvixResult :: MicroJuvixResult, + { _resultMicroJuvixArityResult :: MicroJuvixArityResult, _resultModules :: NonEmpty Module } diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs index 4270da676..05988675f 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs @@ -52,15 +52,19 @@ instance PrettyCode Iden where IdenInductive a -> ppCode a instance PrettyCode TypeApplication where - ppCode (TypeApplication l r) = do + ppCode (TypeApplication l r i) = do l' <- ppLeftExpression appFixity l - r' <- ppRightExpression appFixity r - return $ l' <+> r' + r' <- case i of + Explicit -> ppRightExpression appFixity r + Implicit -> braces <$> ppCode r + return (l' <+> r') instance PrettyCode Application where ppCode a = do l' <- ppLeftExpression appFixity (a ^. appLeft) - r' <- ppRightExpression appFixity (a ^. appRight) + r' <- case a ^. appImplicit of + Explicit -> ppRightExpression appFixity (a ^. appRight) + Implicit -> braces <$> ppCode (a ^. appRight) return $ l' <+> r' instance PrettyCode TypedExpression where @@ -88,7 +92,7 @@ kwInclude :: Doc Ann kwInclude = keyword Str.include kwArrow :: Doc Ann -kwArrow = keyword Str.toAscii +kwArrow = keyword Str.toUnicode kwMapsto :: Doc Ann kwMapsto = keyword Str.mapstoUnicode @@ -148,9 +152,9 @@ instance PrettyCode BackendItem where backend <+> kwMapsto <+> pretty _backendItemCode instance PrettyCode TypeAbstraction where - ppCode (TypeAbstraction v r) = do + ppCode (TypeAbstraction v i r) = do v' <- ppCode v - let l' = parens (v' <+> colon <+> kwType) + let l' = implicitDelim i (v' <+> colon <+> kwType) r' <- ppRightExpression funFixity r return $ l' <+> kwArrow <+> r' @@ -169,7 +173,7 @@ instance PrettyCode TypeIden where instance PrettyCode FunctionArgType where ppCode = \case FunctionArgTypeType t -> ppCode t - FunctionArgTypeAbstraction v -> ppCode v + FunctionArgTypeAbstraction (_, v) -> ppCode v instance PrettyCode Hole where ppCode _ = return kwHole @@ -201,6 +205,11 @@ ppBlock :: Sem r (Doc Ann) ppBlock items = mapM ppCode items >>= bracesIndent . vsep . toList +implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann +implicitDelim = \case + Implicit -> braces + Explicit -> parens + bracesIndent :: Members '[Reader Options] r => Doc Ann -> Sem r (Doc Ann) bracesIndent d = do d' <- indent' d @@ -229,7 +238,8 @@ instance PrettyCode Pattern where ppCode p = case p of PatternVariable v -> ppCode v PatternConstructorApp a -> ppCode a - PatternWildcard -> return kwWildcard + PatternWildcard {} -> return kwWildcard + PatternBraces b -> braces <$> ppCode b instance PrettyCode FunctionDef where ppCode f = do diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Options.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Options.hs index 04b7441b9..aad94b3e5 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Options.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Options.hs @@ -11,7 +11,7 @@ defaultOptions :: Options defaultOptions = Options { _optIndent = 2, - _optShowNameIds = True + _optShowNameIds = False } makeLenses ''Options diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs index 4fb7a9201..9b47feddd 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs @@ -7,24 +7,23 @@ where import Data.HashMap.Strict qualified as HashMap import MiniJuvix.Prelude hiding (fromEither) -import MiniJuvix.Syntax.Concrete.Language (LiteralLoc) import MiniJuvix.Syntax.MicroJuvix.Error import MiniJuvix.Syntax.MicroJuvix.InfoTable import MiniJuvix.Syntax.MicroJuvix.Language.Extra import MiniJuvix.Syntax.MicroJuvix.LocalVars -import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult import MiniJuvix.Syntax.MicroJuvix.TypeChecker.Inference entryMicroJuvixTyped :: Member (Error TypeCheckerError) r => - MicroJuvixResult -> + MicroJuvixArityResult -> Sem r MicroJuvixTypedResult -entryMicroJuvixTyped res@MicroJuvixResult {..} = do +entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do r <- runReader table (mapM checkModule _resultModules) return MicroJuvixTypedResult - { _resultMicroJuvixResult = res, + { _resultMicroJuvixArityResult = res, _resultModules = r } where @@ -98,11 +97,11 @@ checkFunctionDefType = go TypeAny -> return () TypeUniverse -> return () goApp :: TypeApplication -> Sem r () - goApp (TypeApplication a b) = go a >> go b + goApp (TypeApplication a b _) = go a >> go b goFunction :: Function -> Sem r () goFunction (Function a b) = go a >> go b goAbs :: TypeAbstraction -> Sem r () - goAbs (TypeAbstraction _ b) = go b + goAbs (TypeAbstraction _ _ b) = go b checkExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars, Inference] r => @@ -133,33 +132,6 @@ inferExpression = fmap ExpressionTyped . inferExpression' 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 (as, bs) = constructorArgTypes info - args = - map FunctionArgTypeAbstraction as - ++ map FunctionArgTypeType bs - ind = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) - saturatedTy = - foldl' - ( \t v -> - TypeApp - ( TypeApplication - t - (TypeIden (TypeIdenVariable v)) - ) - ) - ind - as - return (foldFunType args saturatedTy) - -constructorArgTypes :: ConstructorInfo -> ([VarName], [Type]) -constructorArgTypes i = - ( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters), - i ^. constructorInfoArgs - ) - checkFunctionClauseBody :: Members '[Reader InfoTable, Error TypeCheckerError, Inference] r => LocalVars -> @@ -174,12 +146,12 @@ checkFunctionClause :: FunctionInfo -> FunctionClause -> Sem r FunctionClause -checkFunctionClause info clause@FunctionClause {..} = do +checkFunctionClause info FunctionClause {..} = do let (argTys, rty) = unfoldFunType (info ^. functionInfoDef . funDefType) (patTys, restTys) = splitAt (length _clausePatterns) argTys bodyTy = foldFunType restTys rty if - | length patTys /= length _clausePatterns -> throw (tyErr patTys) + | length patTys /= length _clausePatterns -> impossible | otherwise -> do locals <- checkPatterns _clauseName (zipExact patTys _clausePatterns) let bodyTy' = @@ -195,28 +167,13 @@ checkFunctionClause info clause@FunctionClause {..} = do { _clauseBody = _clauseBody', .. } - where - tyErr :: [FunctionArgType] -> TypeCheckerError - tyErr patTys = - ErrTooManyPatterns - ( TooManyPatterns - { _tooManyPatternsClause = clause, - _tooManyPatternsTypes = patTys - } - ) checkPatterns :: Members '[Reader InfoTable, Error TypeCheckerError] r => FunctionName -> [(FunctionArgType, Pattern)] -> Sem r LocalVars -checkPatterns name = execState emptyLocalVars . go - where - go :: - Members '[Error TypeCheckerError, Reader InfoTable, State LocalVars] r => - [(FunctionArgType, Pattern)] -> - Sem r () - go = mapM_ (uncurry (checkPattern name)) +checkPatterns name = execState emptyLocalVars . mapM_ (uncurry (checkPattern name)) typeOfArg :: FunctionArgType -> Type typeOfArg a = case a of @@ -236,12 +193,16 @@ checkPattern funName = go go argTy p = do tyVarMap <- fmap (TypeIden . TypeIdenVariable) . (^. localTyMap) <$> get let ty = substitution tyVarMap (typeOfArg argTy) - case p of - PatternWildcard -> return () + unbrace = \case + PatternBraces b -> b + x -> x + case unbrace p of + PatternWildcard {} -> return () + PatternBraces {} -> impossible PatternVariable v -> do modify (addType v ty) case argTy of - FunctionArgTypeAbstraction v' -> do + FunctionArgTypeAbstraction (_, v') -> do modify (over localTyMap (HashMap.insert v' v)) _ -> return () PatternConstructorApp a -> do @@ -263,16 +224,17 @@ checkPattern funName = go let psTys' = map (substituteIndParams ctx) psTys expectedNum = length psTys let w = map FunctionArgTypeType psTys' - when (expectedNum /= length ps) (throw (appErr app w)) + when (expectedNum /= length ps) (throw (appErr app expectedNum)) zipWithM_ go w ps - appErr :: ConstructorApp -> [FunctionArgType] -> TypeCheckerError - appErr app tys = - ErrWrongConstructorAppArgs - ( WrongConstructorAppArgs - { _wrongCtorAppApp = app, - _wrongCtorAppTypes = tys, - _wrongCtorAppName = funName - } + appErr :: ConstructorApp -> Int -> TypeCheckerError + appErr app expected = + ErrArity + ( ErrWrongConstructorAppLength + ( WrongConstructorAppLength + { _wrongConstructorAppLength = app, + _wrongConstructorAppLengthExpected = expected + } + ) ) checkSaturatedInductive :: Type -> Sem r (InductiveName, [(InductiveParameter, Type)]) checkSaturatedInductive t = do @@ -306,6 +268,7 @@ inferExpression' e = case e of return (TypedExpression TypeUniverse (ExpressionFunction (FunctionExpression l' r'))) goLiteral :: LiteralLoc -> Sem r TypedExpression goLiteral l = return (TypedExpression TypeAny (ExpressionLiteral l)) + inferIden :: Iden -> Sem r TypedExpression inferIden i = case i of IdenFunction fun -> do @@ -321,17 +284,12 @@ inferExpression' e = case e of info <- lookupAxiom v return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i)) IdenInductive v -> do - info <- lookupInductive v - let ps = info ^. inductiveInfoDef . inductiveParameters - kind = - foldr - (\p k -> TypeAbs (TypeAbstraction (p ^. inductiveParamName) k)) - TypeUniverse - ps + kind <- inductiveType v return (TypedExpression kind (ExpressionIden i)) inferApplication :: Application -> Sem r TypedExpression inferApplication a = do let leftExp = a ^. appLeft + i = a ^. appImplicit l <- inferExpression' leftExp fun <- getFunctionType leftExp (l ^. typedType) case fun of @@ -344,7 +302,8 @@ inferExpression' e = case e of ExpressionApplication Application { _appLeft = ExpressionTyped l, - _appRight = r + _appRight = r, + _appImplicit = i }, _typedType = substituteType1 (ta ^. typeAbsVar, tr) (ta ^. typeAbsBody) } @@ -356,7 +315,8 @@ inferExpression' e = case e of ExpressionApplication Application { _appLeft = ExpressionTyped l, - _appRight = r + _appRight = r, + _appImplicit = i }, _typedType = f ^. funRight } @@ -389,6 +349,6 @@ viewInductiveApp ty = case t of viewTypeApp :: Type -> (Type, [Type]) viewTypeApp t = case t of - TypeApp (TypeApplication l r) -> + TypeApp (TypeApplication l r _) -> second (`snoc` r) (viewTypeApp l) _ -> (t, []) diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker/Inference.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker/Inference.hs index 254775757..d9aeeb16c 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker/Inference.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker/Inference.hs @@ -50,15 +50,15 @@ closeState = \case goType :: Type -> Sem r' Type goType t = case t of TypeIden {} -> return t - TypeApp (TypeApplication a b) -> do + TypeApp (TypeApplication a b i) -> do a' <- goType a b' <- goType b - return (TypeApp (TypeApplication a' b')) + return (TypeApp (TypeApplication a' b' i)) TypeFunction (Function a b) -> do a' <- goType a b' <- goType b return (TypeFunction (Function a' b')) - TypeAbs (TypeAbstraction v b) -> TypeAbs . TypeAbstraction v <$> goType b + TypeAbs (TypeAbstraction v i b) -> TypeAbs . TypeAbstraction v i <$> goType b TypeUniverse -> return TypeUniverse TypeAny -> return TypeAny TypeHole h' -> @@ -142,11 +142,11 @@ re = reinterpret $ \case return (a == b || mappedEq) _ -> return False goApp :: TypeApplication -> TypeApplication -> Sem r Bool - goApp (TypeApplication f x) (TypeApplication f' x') = andM [go f f', go x x'] + goApp (TypeApplication f x _) (TypeApplication f' x' _) = andM [go f f', go x x'] goFunction :: Function -> Function -> Sem r Bool goFunction (Function l r) (Function l' r') = andM [go l l', go r r'] goAbs :: TypeAbstraction -> TypeAbstraction -> Sem r Bool - goAbs (TypeAbstraction v1 r) (TypeAbstraction v2 r') = + goAbs (TypeAbstraction v1 _ r) (TypeAbstraction v2 _ r') = local (HashMap.insert v1 v2) (go r r') runInference :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem r Expression diff --git a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs b/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs index ee99ae643..f11dd2188 100644 --- a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs +++ b/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs @@ -23,7 +23,6 @@ data InfoTable = InfoTable _infoFunctions :: HashMap Name FunctionInfo } --- TODO temporary function. buildTable :: Module -> InfoTable buildTable m = InfoTable {..} where diff --git a/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs b/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs index 17efcd0bb..3f2269ce8 100644 --- a/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs +++ b/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs @@ -6,16 +6,17 @@ where import Data.HashMap.Strict qualified as HashMap import MiniJuvix.Prelude -import MiniJuvix.Syntax.Abstract.AbstractResult qualified as A -import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as S -import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S +import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract +import MiniJuvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoper +import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper +import MiniJuvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as Micro import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult qualified as Micro import MiniJuvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro import MiniJuvix.Syntax.MonoJuvix.InfoTable import MiniJuvix.Syntax.MonoJuvix.Language -type CompileInfoTable = HashMap S.NameId S.CompileInfo +type CompileInfoTable = HashMap Scoper.NameId Scoper.CompileInfo data MonoJuvixResult = MonoJuvixResult { _resultMicroTyped :: Micro.MicroJuvixTypedResult, @@ -27,12 +28,13 @@ makeLenses ''MonoJuvixResult compileInfoTable :: MonoJuvixResult -> CompileInfoTable compileInfoTable r = HashMap.mapKeys - (^. S.nameId) + (^. Scoper.nameId) ( r ^. resultMicroTyped + . Micro.resultMicroJuvixArityResult . Micro.resultMicroJuvixResult . Micro.resultAbstract - . A.resultScoper + . Abstract.resultScoper . Scoper.resultScoperTable - . S.infoCompilationRules + . Scoper.infoCompilationRules ) diff --git a/src/MiniJuvix/Syntax/Wildcard.hs b/src/MiniJuvix/Syntax/Wildcard.hs new file mode 100644 index 000000000..b31edaad5 --- /dev/null +++ b/src/MiniJuvix/Syntax/Wildcard.hs @@ -0,0 +1,26 @@ +module MiniJuvix.Syntax.Wildcard where + +import MiniJuvix.Prelude +import Prettyprinter + +newtype Wildcard = Wildcard + { _wildcardLoc :: Interval + } + deriving stock (Show) + +makeLenses ''Wildcard + +instance Eq Wildcard where + _ == _ = True + +instance Ord Wildcard where + compare _ _ = EQ + +instance Hashable Wildcard where + hashWithSalt s _ = hashWithSalt s (0 :: Int) + +instance HasLoc Wildcard where + getLoc = (^. wildcardLoc) + +instance Pretty Wildcard where + pretty = const "_" diff --git a/src/MiniJuvix/Termination/Checker.hs b/src/MiniJuvix/Termination/Checker.hs index 467fb1a06..dd8683d79 100644 --- a/src/MiniJuvix/Termination/Checker.hs +++ b/src/MiniJuvix/Termination/Checker.hs @@ -102,7 +102,7 @@ checkApplication :: Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r => Application -> Sem r () -checkApplication (Application l r) = do +checkApplication (Application l r _) = do checkExpression l checkExpression r diff --git a/src/MiniJuvix/Termination/FunctionCall.hs b/src/MiniJuvix/Termination/FunctionCall.hs index 9e0b96b90..da44c8bb4 100644 --- a/src/MiniJuvix/Termination/FunctionCall.hs +++ b/src/MiniJuvix/Termination/FunctionCall.hs @@ -14,7 +14,7 @@ viewCall :: Expression -> Sem r (Maybe FunCall) viewCall = \case - ExpressionApplication (Application f x) -> do + ExpressionApplication (Application f x _) -> do c <- viewCall f x' <- callArg return $ over callArgs (`snoc` x') <$> c diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs index 512aeabc4..6e4e0ab74 100644 --- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs +++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs @@ -151,7 +151,14 @@ goFunction (Abstract.Function l r) = do l' <- goFunctionParameter l r' <- goType r return $ case l' of - Left tyvar -> TypeAbs (TypeAbstraction tyvar r') + Left tyVar -> + TypeAbs + ( TypeAbstraction + { _typeAbsVar = tyVar, + _typeAbsImplicit = l ^. Abstract.paramImplicit, + _typeAbsBody = r' + } + ) Right ty -> TypeFunction (Function ty r') goFunctionDef :: Abstract.FunctionDef -> Sem r FunctionDef @@ -183,7 +190,8 @@ goPattern :: Abstract.Pattern -> Sem r Pattern goPattern p = case p of Abstract.PatternVariable v -> return (PatternVariable (goSymbol v)) Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c - Abstract.PatternWildcard -> return PatternWildcard + Abstract.PatternWildcard i -> return (PatternWildcard i) + Abstract.PatternBraces b -> PatternBraces <$> goPattern b Abstract.PatternEmpty -> unsupported "pattern empty" goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp @@ -218,10 +226,10 @@ goType e = case e of Abstract.ExpressionHole h -> return (TypeHole h) goApplication :: Abstract.Application -> Sem r Application -goApplication (Abstract.Application f x) = do +goApplication (Abstract.Application f x i) = do f' <- goExpression f x' <- goExpression x - return (Application f' x') + return (Application f' x' i) goIden :: Abstract.Iden -> Iden goIden i = case i of @@ -291,13 +299,14 @@ goInductiveDef i = case i ^. Abstract.inductiveType of goConstructorType = fmap fst . viewConstructorType goTypeApplication :: Abstract.Application -> Sem r TypeApplication -goTypeApplication (Abstract.Application l r) = do +goTypeApplication (Abstract.Application l r i) = do l' <- goType l r' <- goType r return TypeApplication { _typeAppLeft = l', - _typeAppRight = r' + _typeAppRight = r', + _typeAppImplicit = i } viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type) diff --git a/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs b/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs index 108df8cec..32fefca39 100644 --- a/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs +++ b/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs @@ -451,6 +451,7 @@ goPattern' ty = \case Micro.PatternVariable v -> return (PatternVariable (goName v)) Micro.PatternConstructorApp capp -> PatternConstructorApp <$> goApp capp Micro.PatternWildcard {} -> return PatternWildcard + Micro.PatternBraces b -> goPattern' ty b where goApp :: Micro.ConstructorApp -> Sem r ConstructorApp goApp capp = case ty ^. Micro.unconcreteType of diff --git a/src/MiniJuvix/Translation/ScopedToAbstract.hs b/src/MiniJuvix/Translation/ScopedToAbstract.hs index cf2ae2cdb..167d1637b 100644 --- a/src/MiniJuvix/Translation/ScopedToAbstract.hs +++ b/src/MiniJuvix/Translation/ScopedToAbstract.hs @@ -8,16 +8,16 @@ import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.AbstractResult import MiniJuvix.Syntax.Abstract.InfoTableBuilder import MiniJuvix.Syntax.Abstract.Language (FunctionDef (_funDefTypeSig)) -import MiniJuvix.Syntax.Abstract.Language qualified as A -import MiniJuvix.Syntax.Concrete.Language -import MiniJuvix.Syntax.Concrete.Language qualified as C +import MiniJuvix.Syntax.Abstract.Language qualified as Abstract +import MiniJuvix.Syntax.Concrete.Language qualified as Concrete +import MiniJuvix.Syntax.Concrete.Scoped.Error import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper unsupported :: Text -> a unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported" -entryAbstract :: Scoper.ScoperResult -> Sem r AbstractResult +entryAbstract :: Member (Error ScoperError) r => Scoper.ScoperResult -> Sem r AbstractResult entryAbstract _resultScoper = do (_resultTable, _resultModules) <- runInfoTableBuilder (mapM goTopModule ms) return AbstractResult {..} @@ -25,33 +25,33 @@ entryAbstract _resultScoper = do ms = _resultScoper ^. Scoper.resultModules goTopModule :: - Members '[InfoTableBuilder] r => + Members '[InfoTableBuilder, Error ScoperError] r => Module 'Scoped 'ModuleTop -> - Sem r A.TopModule + Sem r Abstract.TopModule goTopModule = goModule goLocalModule :: - Members '[InfoTableBuilder] r => + Members '[InfoTableBuilder, Error ScoperError] r => Module 'Scoped 'ModuleLocal -> - Sem r A.LocalModule + Sem r Abstract.LocalModule goLocalModule = goModule goModule :: - (Members '[InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) => + (Members '[InfoTableBuilder, Error ScoperError] r, ModulePathType 'Scoped t ~ S.Name' c) => Module 'Scoped t -> - Sem r (A.Module c) + Sem r (Abstract.Module c) goModule (Module n par b) = case par of - [] -> A.Module n <$> goModuleBody b + [] -> Abstract.Module n <$> goModuleBody b _ -> unsupported "Module parameters" goModuleBody :: forall r. - Members '[InfoTableBuilder] r => + Members '[InfoTableBuilder, Error ScoperError] r => [Statement 'Scoped] -> - Sem r A.ModuleBody + Sem r Abstract.ModuleBody goModuleBody ss' = do otherThanFunctions <- mapMaybeM goStatement ss - functions <- map (fmap A.StatementFunction) <$> compiledFunctions + functions <- map (fmap Abstract.StatementFunction) <$> compiledFunctions let _moduleStatements = map (^. indexedThing) @@ -59,12 +59,12 @@ goModuleBody ss' = do (^. indexedIx) (otherThanFunctions <> functions) ) - return A.ModuleBody {..} + return Abstract.ModuleBody {..} where ss :: [Indexed (Statement 'Scoped)] ss = zipWith Indexed [0 ..] ss' - compiledFunctions :: Sem r [Indexed A.FunctionDef] + compiledFunctions :: Sem r [Indexed Abstract.FunctionDef] compiledFunctions = sequence $ [ Indexed i <$> funDef @@ -83,46 +83,47 @@ goModuleBody ss' = do goStatement :: forall r. - Members '[InfoTableBuilder] r => + Members '[InfoTableBuilder, Error ScoperError] r => Indexed (Statement 'Scoped) -> - Sem r (Maybe (Indexed A.Statement)) + Sem r (Maybe (Indexed Abstract.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 + StatementAxiom d -> Just . Abstract.StatementAxiom <$> goAxiom d + StatementImport (Import t) -> Just . Abstract.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 + StatementInductive i -> Just . Abstract.StatementInductive <$> goInductive i + StatementForeign f -> return (Just (Abstract.StatementForeign f)) + StatementModule f -> Just . Abstract.StatementLocalModule <$> goLocalModule f StatementTypeSignature {} -> return Nothing StatementFunctionClause {} -> return Nothing StatementCompile {} -> return Nothing goFunctionDef :: forall r. - Members '[InfoTableBuilder] r => + Members '[InfoTableBuilder, Error ScoperError] r => TypeSignature 'Scoped -> NonEmpty (FunctionClause 'Scoped) -> - Sem r A.FunctionDef + Sem r Abstract.FunctionDef goFunctionDef TypeSignature {..} clauses = do let _funDefName = _sigName _funDefTerminating = _sigTerminating _funDefClauses <- mapM goFunctionClause clauses _funDefTypeSig <- goExpression _sigType - registerFunction' A.FunctionDef {..} + registerFunction' Abstract.FunctionDef {..} goFunctionClause :: + Member (Error ScoperError) r => FunctionClause 'Scoped -> - Sem r A.FunctionClause + Sem r Abstract.FunctionClause goFunctionClause FunctionClause {..} = do _clausePatterns' <- mapM goPattern _clausePatterns _clauseBody' <- goExpression _clauseBody goWhereBlock _clauseWhere return - A.FunctionClause + Abstract.FunctionClause { _clausePatterns = _clausePatterns', _clauseBody = _clauseBody' } @@ -135,28 +136,30 @@ goWhereBlock w = case w of Nothing -> return () goInductiveParameter :: + Member (Error ScoperError) r => InductiveParameter 'Scoped -> - Sem r A.FunctionParameter + Sem r Abstract.FunctionParameter goInductiveParameter InductiveParameter {..} = do paramType' <- goExpression _inductiveParameterType return - A.FunctionParameter + Abstract.FunctionParameter { _paramType = paramType', _paramName = Just _inductiveParameterName, + _paramImplicit = Explicit, _paramUsage = UsageOmega } goInductive :: - Members '[InfoTableBuilder] r => + Members '[InfoTableBuilder, Error ScoperError] r => InductiveDef 'Scoped -> - Sem r A.InductiveDef + Sem r Abstract.InductiveDef goInductive InductiveDef {..} = do _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters _inductiveType' <- mapM goExpression _inductiveType _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors inductiveInfo <- registerInductive - A.InductiveDef + Abstract.InductiveDef { _inductiveParameters = _inductiveParameters', _inductiveName = _inductiveName, _inductiveType = _inductiveType', @@ -164,67 +167,75 @@ goInductive InductiveDef {..} = do } forM_ _inductiveConstructors' (registerConstructor inductiveInfo) - return (inductiveInfo ^. inductiveInfoDef) goConstructorDef :: + Member (Error ScoperError) r => InductiveConstructorDef 'Scoped -> - Sem r A.InductiveConstructorDef + Sem r Abstract.InductiveConstructorDef goConstructorDef (InductiveConstructorDef c ty) = - A.InductiveConstructorDef c <$> goExpression ty + Abstract.InductiveConstructorDef c <$> goExpression ty goExpression :: + forall r. + Member (Error ScoperError) r => Expression -> - Sem r A.Expression + Sem r Abstract.Expression goExpression = \case ExpressionIdentifier nt -> return (goIden nt) ExpressionParensIdentifier nt -> return (goIden nt) - ExpressionApplication a -> A.ExpressionApplication <$> goApplication a - ExpressionInfixApplication ia -> A.ExpressionApplication <$> goInfix ia - ExpressionPostfixApplication pa -> A.ExpressionApplication <$> goPostfix pa - ExpressionLiteral l -> return (A.ExpressionLiteral l) + ExpressionApplication a -> Abstract.ExpressionApplication <$> goApplication a + ExpressionInfixApplication ia -> Abstract.ExpressionApplication <$> goInfix ia + ExpressionPostfixApplication pa -> Abstract.ExpressionApplication <$> goPostfix pa + ExpressionLiteral l -> return (Abstract.ExpressionLiteral l) ExpressionLambda {} -> unsupported "Lambda" + ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b)) ExpressionMatch {} -> unsupported "Match" ExpressionLetBlock {} -> unsupported "Let Block" - ExpressionUniverse uni -> return $ A.ExpressionUniverse (goUniverse uni) - ExpressionFunction func -> A.ExpressionFunction <$> goFunction func - ExpressionHole h -> return (A.ExpressionHole h) + ExpressionUniverse uni -> return (Abstract.ExpressionUniverse (goUniverse uni)) + ExpressionFunction func -> Abstract.ExpressionFunction <$> goFunction func + ExpressionHole h -> return (Abstract.ExpressionHole h) where - goIden :: C.ScopedIden -> A.Expression - goIden x = A.ExpressionIden $ case x of - 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 (A.FunctionRef (fun ^. C.functionRefName)) - ScopedConstructor c -> A.IdenConstructor (A.ConstructorRef (c ^. C.constructorRefName)) + goIden :: Concrete.ScopedIden -> Abstract.Expression + goIden x = Abstract.ExpressionIden $ case x of + ScopedAxiom a -> Abstract.IdenAxiom (Abstract.AxiomRef (a ^. Concrete.axiomRefName)) + ScopedInductive i -> Abstract.IdenInductive (Abstract.InductiveRef (i ^. Concrete.inductiveRefName)) + ScopedVar v -> Abstract.IdenVar v + ScopedFunction fun -> Abstract.IdenFunction (Abstract.FunctionRef (fun ^. Concrete.functionRefName)) + ScopedConstructor c -> Abstract.IdenConstructor (Abstract.ConstructorRef (c ^. Concrete.constructorRefName)) - goApplication :: Application -> Sem r A.Application - goApplication (Application l r) = do + goApplication :: Application -> Sem r Abstract.Application + goApplication (Application l arg) = do l' <- goExpression l r' <- goExpression r - return (A.Application l' r') + return (Abstract.Application l' r' i) + where + (r, i) = case arg of + ExpressionBraces b -> (b ^. withLocParam, Implicit) + _ -> (arg, Explicit) - goPostfix :: PostfixApplication -> Sem r A.Application + goPostfix :: PostfixApplication -> Sem r Abstract.Application goPostfix (PostfixApplication l op) = do l' <- goExpression l let op' = goIden op - return (A.Application op' l') + return (Abstract.Application op' l' Explicit) - goInfix :: InfixApplication -> Sem r A.Application + goInfix :: InfixApplication -> Sem r Abstract.Application goInfix (InfixApplication l op r) = do l' <- goExpression l let op' = goIden op + l'' = Abstract.ExpressionApplication (Abstract.Application op' l' Explicit) r' <- goExpression r - return $ A.Application (A.ExpressionApplication (A.Application op' l')) r' + return (Abstract.Application l'' r' Explicit) goUniverse :: Universe -> Universe goUniverse = id -goFunction :: Function 'Scoped -> Sem r A.Function +goFunction :: Member (Error ScoperError) r => Function 'Scoped -> Sem r Abstract.Function goFunction (Function l r) = do _funParameter <- goFunctionParameter l _funReturn <- goExpression r - return A.Function {..} + return Abstract.Function {..} defaultUsage :: Usage defaultUsage = UsageOmega @@ -233,34 +244,40 @@ goUsage :: Maybe Usage -> Usage goUsage = fromMaybe defaultUsage goFunctionParameter :: + Member (Error ScoperError) r => FunctionParameter 'Scoped -> - Sem r A.FunctionParameter -goFunctionParameter (FunctionParameter _paramName u ty) = do - _paramType <- goExpression ty - let _paramUsage = goUsage u - return A.FunctionParameter {..} + Sem r Abstract.FunctionParameter +goFunctionParameter (FunctionParameter {..}) = do + _paramType' <- goExpression _paramType + return + Abstract.FunctionParameter + { Abstract._paramUsage = goUsage _paramUsage, + Abstract._paramType = _paramType', + Abstract._paramImplicit = _paramImplicit, + Abstract._paramName = _paramName + } goPatternApplication :: PatternApp -> - Sem r A.ConstructorApp -goPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternApplication a) + Sem r Abstract.ConstructorApp +goPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternApplication a) goPatternConstructor :: ConstructorRef -> - Sem r A.ConstructorApp -goPatternConstructor a = uncurry A.ConstructorApp <$> viewApp (PatternConstructor a) + Sem r Abstract.ConstructorApp +goPatternConstructor a = uncurry Abstract.ConstructorApp <$> viewApp (PatternConstructor a) goInfixPatternApplication :: PatternInfixApp -> - Sem r A.ConstructorApp -goInfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternInfixApplication a) + Sem r Abstract.ConstructorApp +goInfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternInfixApplication a) goPostfixPatternApplication :: PatternPostfixApp -> - Sem r A.ConstructorApp -goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPostfixApplication a) + Sem r Abstract.ConstructorApp +goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a) -viewApp :: forall r. Pattern -> Sem r (A.ConstructorRef, [A.Pattern]) +viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.Pattern]) viewApp = \case PatternConstructor c -> return (goConstructorRef c, []) PatternApplication (PatternApp l r) -> do @@ -275,25 +292,27 @@ viewApp = \case return (goConstructorRef c, [l']) PatternVariable {} -> err PatternWildcard {} -> err + PatternBraces {} -> err PatternEmpty {} -> err where err :: a err = error "constructor expected on the left of a pattern application" -goConstructorRef :: ConstructorRef -> A.ConstructorRef -goConstructorRef (ConstructorRef' n) = A.ConstructorRef n +goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef +goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef n -goPattern :: Pattern -> Sem r A.Pattern +goPattern :: Pattern -> Sem r Abstract.Pattern goPattern p = case p of - PatternVariable a -> return $ A.PatternVariable a - PatternConstructor c -> A.PatternConstructorApp <$> goPatternConstructor c - PatternApplication a -> A.PatternConstructorApp <$> goPatternApplication a - PatternInfixApplication a -> A.PatternConstructorApp <$> goInfixPatternApplication a - PatternPostfixApplication a -> A.PatternConstructorApp <$> goPostfixPatternApplication a - PatternWildcard -> return A.PatternWildcard - PatternEmpty -> return A.PatternEmpty + PatternVariable a -> return $ Abstract.PatternVariable a + PatternConstructor c -> Abstract.PatternConstructorApp <$> goPatternConstructor c + PatternApplication a -> Abstract.PatternConstructorApp <$> goPatternApplication a + PatternInfixApplication a -> Abstract.PatternConstructorApp <$> goInfixPatternApplication a + PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a + PatternWildcard i -> return (Abstract.PatternWildcard i) + PatternEmpty -> return Abstract.PatternEmpty + PatternBraces b -> Abstract.PatternBraces <$> goPattern b -goAxiom :: Members '[InfoTableBuilder] r => AxiomDef 'Scoped -> Sem r A.AxiomDef +goAxiom :: Members '[InfoTableBuilder, Error ScoperError] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef goAxiom AxiomDef {..} = do _axiomType' <- goExpression _axiomType - registerAxiom' A.AxiomDef {_axiomType = _axiomType', ..} + registerAxiom' Abstract.AxiomDef {_axiomType = _axiomType', ..} diff --git a/test/Arity.hs b/test/Arity.hs new file mode 100644 index 000000000..bccf7b5c4 --- /dev/null +++ b/test/Arity.hs @@ -0,0 +1,10 @@ +module Arity + ( allTests, + ) +where + +import Arity.Negative qualified as N +import Base + +allTests :: TestTree +allTests = testGroup "Arity tests" [N.allTests] diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs new file mode 100644 index 000000000..a04f28883 --- /dev/null +++ b/test/Arity/Negative.hs @@ -0,0 +1,87 @@ +module Arity.Negative (allTests) where + +import Base +import MiniJuvix.Pipeline +import MiniJuvix.Syntax.MicroJuvix.ArityChecker.Error + +type FailMsg = String + +data NegTest = NegTest + { _name :: String, + _relDir :: FilePath, + _file :: FilePath, + _checkErr :: ArityCheckerError -> Maybe FailMsg + } + +testDescr :: NegTest -> TestDescr +testDescr NegTest {..} = + let tRoot = root _relDir + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Single $ do + let entryPoint = defaultEntryPoint _file + result <- runIOEither (upToMicroJuvixArity entryPoint) + case mapLeft fromMiniJuvixError result of + Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure + Left Nothing -> assertFailure "The arity checker did not find an error." + Right _ -> assertFailure "An error ocurred but it was not in the arity checker." + } + +allTests :: TestTree +allTests = + testGroup + "Arity checker negative tests" + (map (mkTest . testDescr) tests) + +root :: FilePath +root = "tests/negative" + +wrongError :: Maybe FailMsg +wrongError = Just "Incorrect error" + +tests :: [NegTest] +tests = + [ NegTest + "Too many arguments in expression" + "MicroJuvix" + "TooManyArguments.mjuvix" + $ \case + ErrTooManyArguments {} -> Nothing + _ -> wrongError, + NegTest + "Pattern match a function type" + "MicroJuvix" + "FunctionPattern.mjuvix" + $ \case + ErrPatternFunction {} -> Nothing + _ -> wrongError, + NegTest + "Function type (* → *) application" + "MicroJuvix" + "FunctionApplied.mjuvix" + $ \case + ErrFunctionApplied {} -> Nothing + _ -> wrongError, + NegTest + "Expected explicit pattern" + "MicroJuvix" + "ExpectedExplicitPattern.mjuvix" + $ \case + ErrExpectedExplicitPattern {} -> Nothing + _ -> wrongError, + NegTest + "Expected explicit argument" + "MicroJuvix" + "ExpectedExplicitArgument.mjuvix" + $ \case + ErrExpectedExplicitArgument {} -> Nothing + _ -> wrongError, + NegTest + "Function clause with two many patterns in the lhs" + "MicroJuvix" + "LhsTooManyPatterns.mjuvix" + $ \case + ErrLhsTooManyPatterns {} -> Nothing + _ -> wrongError + ] diff --git a/test/Main.hs b/test/Main.hs index a2486bf87..c5982d36b 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -1,5 +1,6 @@ module Main (main) where +import Arity qualified import BackendC qualified import Base import MonoJuvix qualified @@ -19,6 +20,7 @@ fastTests = "MiniJuvix fast tests" [ Scope.allTests, Termination.allTests, + Arity.allTests, TypeCheck.allTests, MonoJuvix.allTests ] diff --git a/test/MonoJuvix/Positive.hs b/test/MonoJuvix/Positive.hs index 3f2b48fcd..0715d73cd 100644 --- a/test/MonoJuvix/Positive.hs +++ b/test/MonoJuvix/Positive.hs @@ -38,7 +38,7 @@ tests = PosTest "Polymorphic Simple Fungible Token" "FullExamples" - "PolySimpleFungibleToken.mjuvix", + "SimpleFungibleTokenImplicit.mjuvix", PosTest "Polymorphism and higher rank functions with explicit holes" "." diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs index 8d5f069ed..913b81c5c 100644 --- a/test/TypeCheck/Negative.hs +++ b/test/TypeCheck/Negative.hs @@ -49,13 +49,6 @@ tests = $ \case ErrWrongConstructorType {} -> Nothing _ -> wrongError, - NegTest - "Constructor pattern length mismatch" - "MicroJuvix" - "PatternConstructorApp.mjuvix" - $ \case - ErrWrongConstructorAppArgs {} -> Nothing - _ -> wrongError, NegTest "Type vs inferred type mismatch" "MicroJuvix" @@ -70,13 +63,6 @@ tests = $ \case ErrExpectedFunctionType {} -> Nothing _ -> wrongError, - NegTest - "Function definition clause with two many match patterns" - "MicroJuvix" - "TooManyPatterns.mjuvix" - $ \case - ErrTooManyPatterns {} -> Nothing - _ -> wrongError, NegTest "Unsolved hole" "MicroJuvix" @@ -90,12 +76,5 @@ tests = "MultiWrongType.mjuvix" $ \case ErrWrongType {} -> Nothing - _ -> wrongError, - NegTest - "Constructor pattern with arity greater than the constructor" - "MicroJuvix" - "WrongConstructorArity.mjuvix" - $ \case - ErrWrongConstructorAppArgs {} -> Nothing _ -> wrongError ] diff --git a/test/TypeCheck/Positive.hs b/test/TypeCheck/Positive.hs index 936b3ed72..3920243f3 100644 --- a/test/TypeCheck/Positive.hs +++ b/test/TypeCheck/Positive.hs @@ -48,9 +48,9 @@ tests = "MiniHaskell" "HelloWorld.mjuvix", PosTest - "PolySimpleFungibleToken with explicit holes" + "PolySimpleFungibleToken" "FullExamples" - "PolySimpleFungibleTokenHoles.mjuvix", + "SimpleFungibleTokenImplicit.mjuvix", PosTest "GHC backend MonoSimpleFungibleToken" "FullExamples" diff --git a/tests/negative/MicroJuvix/ExpectedExplicitArgument.mjuvix b/tests/negative/MicroJuvix/ExpectedExplicitArgument.mjuvix new file mode 100644 index 000000000..43e6f4220 --- /dev/null +++ b/tests/negative/MicroJuvix/ExpectedExplicitArgument.mjuvix @@ -0,0 +1,8 @@ +module ExpectedExplicitArgument; + inductive T (A : Type) { + c : A → T A; + }; + + f : {A : Type} → A → T A; + f {A} a ≔ c {A} {a}; +end; diff --git a/tests/negative/MicroJuvix/ExpectedExplicitPattern.mjuvix b/tests/negative/MicroJuvix/ExpectedExplicitPattern.mjuvix new file mode 100644 index 000000000..7f604351a --- /dev/null +++ b/tests/negative/MicroJuvix/ExpectedExplicitPattern.mjuvix @@ -0,0 +1,8 @@ +module ExpectedExplicitPattern; + inductive T (A : Type) { + c : A → T A; + }; + + f : {A : Type} → T A → A; + f {_} {c a} ≔ a; +end; diff --git a/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix b/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix index 5b37fb6a0..c9a49e321 100644 --- a/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix +++ b/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix @@ -1,12 +1,12 @@ module ExpectedFunctionType; - inductive A { - a : A; + inductive Pair (A : Type) { + mkPair : A → A → Pair A; }; inductive B { b : B; }; - f : A; - f ≔ a b; + f : Pair B → Pair B; + f (mkPair a b) ≔ a b; end; diff --git a/tests/negative/MicroJuvix/FunctionApplied.mjuvix b/tests/negative/MicroJuvix/FunctionApplied.mjuvix new file mode 100644 index 000000000..3d19e931c --- /dev/null +++ b/tests/negative/MicroJuvix/FunctionApplied.mjuvix @@ -0,0 +1,8 @@ +module FunctionApplied; + inductive T (A : Type) { + c : A → T; + }; + + f : {A : Type} → A → T A; + f {A} a ≔ c {(A → A) A} a; +end; diff --git a/tests/negative/MicroJuvix/FunctionPattern.mjuvix b/tests/negative/MicroJuvix/FunctionPattern.mjuvix new file mode 100644 index 000000000..913dea1db --- /dev/null +++ b/tests/negative/MicroJuvix/FunctionPattern.mjuvix @@ -0,0 +1,8 @@ +module FunctionPattern; + inductive T { + A : T; + }; + + f : (T → T) → T; + f A ≔ A; +end; diff --git a/tests/negative/MicroJuvix/LhsTooManyPatterns.mjuvix b/tests/negative/MicroJuvix/LhsTooManyPatterns.mjuvix new file mode 100644 index 000000000..eecb85fb0 --- /dev/null +++ b/tests/negative/MicroJuvix/LhsTooManyPatterns.mjuvix @@ -0,0 +1,8 @@ +module LhsTooManyPatterns; + inductive T { + A : T; + }; + + f : T → T; + f A x ≔ A; +end; diff --git a/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix b/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix deleted file mode 100644 index 96d9474bb..000000000 --- a/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix +++ /dev/null @@ -1,13 +0,0 @@ -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/TooManyArguments.mjuvix b/tests/negative/MicroJuvix/TooManyArguments.mjuvix new file mode 100644 index 000000000..8ac5aab4b --- /dev/null +++ b/tests/negative/MicroJuvix/TooManyArguments.mjuvix @@ -0,0 +1,8 @@ +module TooManyArguments; + inductive T (A : Type) { + c : A → T A; + }; + + f : {A : Type} → A → T A; + f {A} a ≔ c {A} a a {a} ; +end; diff --git a/tests/negative/MicroJuvix/TooManyPatterns.mjuvix b/tests/negative/MicroJuvix/TooManyPatterns.mjuvix deleted file mode 100644 index 446ec489e..000000000 --- a/tests/negative/MicroJuvix/TooManyPatterns.mjuvix +++ /dev/null @@ -1,8 +0,0 @@ -module TooManyPatterns; - inductive A { - a : A; - }; - - f : A -> A; - f a _ ≔ a; -end; diff --git a/tests/negative/MicroJuvix/UnsolvedMeta.mjuvix b/tests/negative/MicroJuvix/UnsolvedMeta.mjuvix index f9c8f51cb..5dba2237d 100644 --- a/tests/negative/MicroJuvix/UnsolvedMeta.mjuvix +++ b/tests/negative/MicroJuvix/UnsolvedMeta.mjuvix @@ -5,6 +5,6 @@ inductive Proxy (A : Type) { }; t : Proxy _; -t ≔ x _; +t ≔ x; end; diff --git a/tests/negative/MicroJuvix/WrongConstructorArity.mjuvix b/tests/negative/MicroJuvix/WrongConstructorArity.mjuvix index 4c552d549..52009e959 100644 --- a/tests/negative/MicroJuvix/WrongConstructorArity.mjuvix +++ b/tests/negative/MicroJuvix/WrongConstructorArity.mjuvix @@ -1,8 +1,8 @@ module WrongConstructorArity; inductive T { - A : T; + A : T → T; }; f : T → T; - f (A i) ≔ i; + f (A i x) ≔ i; end; diff --git a/tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix b/tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix deleted file mode 100644 index db08eded2..000000000 --- a/tests/positive/FullExamples/PolySimpleFungibleToken.mjuvix +++ /dev/null @@ -1,329 +0,0 @@ -module PolySimpleFungibleToken; - -foreign ghc { - import Anoma -}; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -inductive Bool { - true : Bool; - false : Bool; -}; - -infixr 2 ||; -|| : Bool → Bool → Bool; -|| false a ≔ a; -|| true _ ≔ true; - -infixr 3 &&; -&& : Bool → Bool → Bool; -&& false _ ≔ false; -&& true a ≔ a; - -if : (A : Type) → Bool → A → A → A; -if _ true a _ ≔ a; -if _ false _ b ≔ b; - --------------------------------------------------------------------------------- --- Backend Booleans --------------------------------------------------------------------------------- - -axiom BackendBool : Type; - -compile BackendBool { - ghc ↦ "Bool"; -}; - -axiom backend-true : BackendBool; -compile backend-true { - ghc ↦ "True"; -}; - -axiom backend-false : BackendBool; -compile backend-false { - ghc ↦ "False"; -}; - --------------------------------------------------------------------------------- --- Backend Bridge --------------------------------------------------------------------------------- - -foreign ghc { - bool :: Bool -> a -> a -> a - bool True x _ = x - bool False _ y = y -}; - -axiom bool : BackendBool → Bool → Bool → Bool; -compile bool { - ghc ↦ "bool"; -}; - -from-backend-bool : BackendBool → Bool; -from-backend-bool bb ≔ bool bb true false; - --------------------------------------------------------------------------------- --- Functions --------------------------------------------------------------------------------- - -const : (A : Type) → (B : Type) → A → B → A; -const _ _ a _ ≔ a; - -id : (A : Type) → A → A; -id _ a ≔ a; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; -compile Int { - ghc ↦ "Int"; -}; - -infix 4 <'; -axiom <' : Int → Int → BackendBool; -compile <' { - ghc ↦ "(<)"; -}; - -infix 4 <; -< : Int → Int → Bool; -< i1 i2 ≔ from-backend-bool (i1 <' i2); - -axiom eqInt : Int → Int → BackendBool; -compile eqInt { - ghc ↦ "(==)"; -}; - -infix 4 ==Int; -==Int : Int → Int → Bool; -==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2); - -infixl 6 -; -axiom - : Int -> Int -> Int; -compile - { - ghc ↦ "(-)"; -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - ghc ↦ "(+)"; -}; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -axiom String : Type; -compile String { - ghc ↦ "[Char]"; -}; - -axiom eqString : String → String → BackendBool; -compile eqString { - ghc ↦ "(==)"; -}; - -infix 4 ==String; -==String : String → String → Bool; -==String s1 s2 ≔ from-backend-bool (eqString s1 s2); - --------------------------------------------------------------------------------- --- Lists --------------------------------------------------------------------------------- - -inductive List (A : Type) { - nil : List A; - cons : A → List A → List A; -}; - -elemGen : (A : Type) → (A → A → Bool) → A → List A → Bool; -elemGen _ _ _ nil ≔ false; -elemGen A eq s (cons x xs) ≔ eq s x || elemGen A eq s xs; - -elem : String → List String → Bool; -elem s l ≔ elemGen String (==String) s l; - -foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B; -foldl _ _ f z nil ≔ z; -foldl A B f z (cons h hs) ≔ foldl A B f (f z h) hs; - --------------------------------------------------------------------------------- --- Pair --------------------------------------------------------------------------------- - --- inductive PairIntBool { --- MakePair : Int → Bool → PairIntBool; --- }; - -inductive Pair (A : Type) (B : Type) { - mkPair : A → B → Pair A B; -}; - -if-pairIntBool : Bool → Pair Int Bool → Pair Int Bool → Pair Int Bool; -if-pairIntBool ≔ if (Pair Int Bool); - --------------------------------------------------------------------------------- --- Maybe --------------------------------------------------------------------------------- - -inductive Maybe (A : Type) { - nothing : Maybe A; - just : A → Maybe A; -}; - -if-optionInt : Bool → Maybe Int → Maybe Int → Maybe Int; -if-optionInt ≔ if (Maybe Int); - -from-int : Int → Maybe Int; -from-int i ≔ if-optionInt (i < 0) (nothing Int) (just Int i); - -maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B; -maybe _ _ b _ nothing ≔ b; -maybe _ _ _ f (just x) ≔ f x; - -maybe-int : Int → Maybe Int → Int; -maybe-int d ≔ maybe Int Int d (id Int); - -if-optionString : Bool → Maybe String → Maybe String → Maybe String; -if-optionString ≔ if (Maybe String); - -from-string : String → Maybe String; -from-string s ≔ if-optionString (s ==String "") (nothing String) (just String s); - -pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool; -pair-from-optionString ≔ maybe String (Pair Int Bool) (mkPair Int Bool 0 false); - --------------------------------------------------------------------------------- --- foldl --------------------------------------------------------------------------------- - -foldl' : (Pair Int Bool → String → Pair Int Bool) → Pair Int Bool → List String → Pair Int Bool; -foldl' ≔ foldl String (Pair Int Bool) ; - --------------------------------------------------------------------------------- --- Anoma --------------------------------------------------------------------------------- - -axiom readPre : String → Int; -compile readPre { - ghc ↦ "readPre"; -}; - -axiom readPost : String → Int; -compile readPost { - ghc ↦ "readPost"; -}; - -axiom isBalanceKey : String → String → String; -compile isBalanceKey { - ghc ↦ "isBalanceKey"; -}; - -read-pre : String → Maybe Int; -read-pre s ≔ from-int (readPre s); - -read-post : String → Maybe Int; -read-post s ≔ from-int (readPost s); - -is-balance-key : String → String → Maybe String; -is-balance-key token key ≔ from-string (isBalanceKey token key); - -unwrap-default : Maybe Int → Int; -unwrap-default o ≔ maybe-int 0 o; - --------------------------------------------------------------------------------- --- Validity Predicate --------------------------------------------------------------------------------- - -change-from-key : String → Int; -change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key); - -check-vp : List String → String → Int → String → Pair Int Bool; -check-vp verifiers key change owner ≔ - if-pairIntBool - (change-from-key key < 0) - -- make sure the spender approved the transaction - (mkPair Int Bool (change + (change-from-key key)) (elem owner verifiers)) - (mkPair Int Bool (change + (change-from-key key)) true); - -check-keys : String → List String → Pair Int Bool → String → Pair Int Bool; -check-keys token verifiers (mkPair change is-success) key ≔ - if-pairIntBool - is-success - (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) - (mkPair Int Bool 0 false); - -check-result : Pair Int Bool → Bool; -check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked; - -vp : String → List String → List String → Bool; -vp token keys-changed verifiers ≔ - check-result - (foldl' - (check-keys token verifiers) - (mkPair Int Bool 0 true) - keys-changed); - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; -compile Action { - ghc ↦ "IO ()"; -}; - -axiom putStr : String → Action; -compile putStr { - ghc ↦ "putStr"; -}; - -axiom putStrLn : String → Action; -compile putStrLn { - ghc ↦ "putStrLn"; -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; -compile >> { - ghc ↦ "(>>)"; -}; - -show-result : Bool → String; -show-result true ≔ "OK"; -show-result false ≔ "FAIL"; - --------------------------------------------------------------------------------- --- Testing VP --------------------------------------------------------------------------------- - -token : String; -token ≔ "owner-token"; - -owner-address : String; -owner-address ≔ "owner-address"; - -change1-key : String; -change1-key ≔ "change1-key"; - -change2-key : String; -change2-key ≔ "change2-key"; - -verifiers : List String; -verifiers ≔ cons String owner-address (nil String); - -keys-changed : List String; -keys-changed ≔ cons String change1-key (cons String change2-key (nil String)); - -main : Action; -main ≔ - (putStr "VP Status: ") - >> (putStrLn (show-result (vp token keys-changed verifiers))); - -end; diff --git a/tests/positive/FullExamples/PolySimpleFungibleTokenHoles.mjuvix b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.mjuvix similarity index 77% rename from tests/positive/FullExamples/PolySimpleFungibleTokenHoles.mjuvix rename to tests/positive/FullExamples/SimpleFungibleTokenImplicit.mjuvix index cdf56be85..8ca83c9e6 100644 --- a/tests/positive/FullExamples/PolySimpleFungibleTokenHoles.mjuvix +++ b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.mjuvix @@ -1,4 +1,4 @@ -module PolySimpleFungibleTokenHoles; +module SimpleFungibleTokenImplicit; foreign ghc { import Anoma @@ -23,9 +23,9 @@ infixr 3 &&; && false _ ≔ false; && true a ≔ a; -if : (A : Type) → Bool → A → A → A; -if _ true a _ ≔ a; -if _ false _ b ≔ b; +if : {A : Type} → Bool → A → A → A; +if true a _ ≔ a; +if false _ b ≔ b; -------------------------------------------------------------------------------- -- Backend Booleans @@ -69,11 +69,8 @@ from-backend-bool bb ≔ bool bb true false; -- Functions -------------------------------------------------------------------------------- -const : (A : Type) → (B : Type) → A → B → A; -const _ _ a _ ≔ a; - -id : (A : Type) → A → A; -id _ a ≔ a; +id : {A : Type} → A → A; +id a ≔ a; -------------------------------------------------------------------------------- -- Integers @@ -137,25 +134,28 @@ infix 4 ==String; -- Lists -------------------------------------------------------------------------------- +infixr 5 ∷; inductive List (A : Type) { nil : List A; - cons : A → List A → List A; + ∷ : A → List A → List A; }; -elem : (A : Type) → (A → A → Bool) → A → List A → Bool; -elem _ _ _ nil ≔ false; -elem _ eq s (cons x xs) ≔ eq s x || elem _ eq s xs; +elem : {A : Type} → (A → A → Bool) → A → List A → Bool; +elem _ _ nil ≔ false; +elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs; -foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B; -foldl _ _ f z nil ≔ z; -foldl _ _ f z (cons h hs) ≔ foldl _ _ f (f z h) hs; +foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; +foldl f z nil ≔ z; +foldl f z (h ∷ hs) ≔ foldl f (f z h) hs; -------------------------------------------------------------------------------- -- Pair -------------------------------------------------------------------------------- -inductive Pair (A : Type) (B : Type) { - mkPair : A → B → Pair A B; +infixr 4 ,; +infixr 2 ×; +inductive × (A : Type) (B : Type) { + , : A → B → A × B; }; -------------------------------------------------------------------------------- @@ -168,17 +168,17 @@ inductive Maybe (A : Type) { }; from-int : Int → Maybe Int; -from-int i ≔ if _ (i < 0) (nothing _) (just _ i); +from-int i ≔ if (i < 0) nothing (just i); -maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B; -maybe _ _ b _ nothing ≔ b; -maybe _ _ _ f (just x) ≔ f x; +maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; +maybe b _ nothing ≔ b; +maybe _ f (just x) ≔ f x; from-string : String → Maybe String; -from-string s ≔ if _ (s ==String "") (nothing _) (just _ s); +from-string s ≔ if (s ==String "") nothing (just s); -pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool; -pair-from-optionString ≔ maybe _ _ (mkPair _ _ 0 false); +pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; +pair-from-optionString ≔ maybe (0 , false); -------------------------------------------------------------------------------- -- Anoma @@ -209,7 +209,7 @@ is-balance-key : String → String → Maybe String; is-balance-key token key ≔ from-string (isBalanceKey token key); unwrap-default : Maybe Int → Int; -unwrap-default o ≔ maybe _ _ 0 (id _) o; +unwrap-default ≔ maybe 0 id; -------------------------------------------------------------------------------- -- Validity Predicate @@ -218,30 +218,30 @@ unwrap-default o ≔ maybe _ _ 0 (id _) o; change-from-key : String → Int; change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key); -check-vp : List String → String → Int → String → Pair Int Bool; +check-vp : List String → String → Int → String → Int × Bool; check-vp verifiers key change owner ≔ - if _ + if (change-from-key key < 0) -- make sure the spender approved the transaction - (mkPair _ _ (change + (change-from-key key)) (elem _ (==String) owner verifiers)) - (mkPair _ _ (change + (change-from-key key)) true); + (change + (change-from-key key), elem (==String) owner verifiers) + (change + (change-from-key key), true); -check-keys : String → List String → Pair Int Bool → String → Pair Int Bool; -check-keys token verifiers (mkPair change is-success) key ≔ - if _ +check-keys : String → List String → Int × Bool → String → Int × Bool; +check-keys token verifiers (change , is-success) key ≔ + if is-success (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) - (mkPair _ _ 0 false); + (0 , false); -check-result : Pair Int Bool → Bool; -check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked; +check-result : Int × Bool → Bool; +check-result (change , all-checked) ≔ (change ==Int 0) && all-checked; vp : String → List String → List String → Bool; vp token keys-changed verifiers ≔ check-result - (foldl _ _ + (foldl (check-keys token verifiers) - (mkPair _ _ 0 true) + (0 , true) keys-changed); -------------------------------------------------------------------------------- @@ -290,10 +290,10 @@ change2-key : String; change2-key ≔ "change2-key"; verifiers : List String; -verifiers ≔ cons _ owner-address (nil _); +verifiers ≔ owner-address ∷ nil; keys-changed : List String; -keys-changed ≔ cons _ change1-key (cons _ change2-key (nil _)); +keys-changed ≔ change1-key ∷ change2-key ∷ nil; main : Action; main ≔ diff --git a/tests/positive/Implicit.mjuvix b/tests/positive/Implicit.mjuvix new file mode 100644 index 000000000..bb0d78f69 --- /dev/null +++ b/tests/positive/Implicit.mjuvix @@ -0,0 +1,73 @@ +module Implicit; + +infixr 9 ∘; +∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C; +∘ f g x ≔ f (g x); + +inductive Nat { + zero : Nat; + suc : Nat → Nat; +}; + +infixr 5 ∷; +inductive List (A : Type) { + nil : List A; + ∷ : A → List A → List A; +}; + +upToTwo : _; +upToTwo ≔ zero ∷ suc zero ∷ suc (suc zero) ∷ nil; + +infixr 4 ,; +inductive Pair (A : Type) (B : Type) { + , : A → B → Pair A B; +}; + +p1 : Nat → Nat → Pair Nat Nat; +p1 a b ≔ a , b ; + +inductive Proxy (A : Type) { + proxy : Proxy A; +}; + +t2' : {A : Type} → Proxy A; +t2' ≔ proxy; + +t2 : {A : Type} → Proxy A; +t2 ≔ proxy; + +t3 : ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B; +t3 _ _ ≔ proxy; + +t4 : {B : Type} → Proxy B; +t4 {_} ≔ t3 proxy proxy; + +t4' : {B : Type} → Proxy B; +t4' ≔ t3 proxy proxy ; + +map : {A : Type} → {B : Type} → (A → B) → List A → List B; +map f nil ≔ nil; +map f (x ∷ xs) ≔ f x ∷ map f xs; + +t : {A : Type} → Proxy A; +t {_} ≔ proxy; + +t' : {A : Type} → Proxy A; +t' ≔ proxy; + +t5 : {A : Type} → Proxy A → Proxy A; +t5 p ≔ p; + +t5' : {A : Type} → Proxy A → Proxy A; +t5' proxy ≔ proxy; + +f : {A : Type} → {B : Type} → A → B → _; +f a b ≔ a; + +pairEval : {A : Type} → {B : Type} → Pair (A → B) A → B; +pairEval (f , x) ≔ f x; + +pairEval' : {A : Type} → {B : Type} → Pair ({C : Type} → A → B) A → B; +pairEval' {A} (f , x) ≔ f {Nat} x; + +end; diff --git a/tests/positive/MicroJuvix/HoleInSignature.mjuvix b/tests/positive/MicroJuvix/HoleInSignature.mjuvix index a381e58bb..f225dfc25 100644 --- a/tests/positive/MicroJuvix/HoleInSignature.mjuvix +++ b/tests/positive/MicroJuvix/HoleInSignature.mjuvix @@ -9,9 +9,9 @@ inductive Bool { }; p : Pair _ _; -p := mkPair _ _ true false; +p := mkPair true false; p2 : (A : Type) → (B : Type) → _ → B → Pair A _; -p2 _ _ a b ≔ mkPair _ _ a b; +p2 _ _ a b ≔ mkPair a b; end; diff --git a/tests/positive/MiniC/MultiModules/Input.mjuvix b/tests/positive/MiniC/MultiModules/Input.mjuvix index 836aeb516..4b60ef6e0 100644 --- a/tests/positive/MiniC/MultiModules/Input.mjuvix +++ b/tests/positive/MiniC/MultiModules/Input.mjuvix @@ -26,7 +26,7 @@ bool-to-str false ≔ "False"; fst-of-pair : Action; fst-of-pair ≔ (put-str "fst (True, False) = ") - >> put-str-ln (bool-to-str (fst Bool Bool (mkPair Bool Bool true false))); + >> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false))); main : Action; main ≔ fst-of-pair; diff --git a/tests/positive/MiniC/Polymorphism/Input.mjuvix b/tests/positive/MiniC/Polymorphism/Input.mjuvix index b712068c1..b077c3de2 100644 --- a/tests/positive/MiniC/Polymorphism/Input.mjuvix +++ b/tests/positive/MiniC/Polymorphism/Input.mjuvix @@ -81,7 +81,7 @@ fst _ _ (mkPair a b) ≔ a; fst-of-pair : Action; fst-of-pair ≔ (put-str "fst (True, False) = ") - >> put-str-ln (bool-to-str (fst Bool Bool (mkPair Bool Bool true false))); + >> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false))); main : Action; main ≔ fst-of-pair; diff --git a/tests/positive/MiniC/PolymorphismHoles/Input.mjuvix b/tests/positive/MiniC/PolymorphismHoles/Input.mjuvix index 80008107a..ad86454cc 100644 --- a/tests/positive/MiniC/PolymorphismHoles/Input.mjuvix +++ b/tests/positive/MiniC/PolymorphismHoles/Input.mjuvix @@ -72,8 +72,8 @@ inductive Pair (A : Type) (B : Type) { mkPair : A → B → Pair A B; }; -fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) ≔ a; +fst : {A : Type} → {B : Type} → Pair A B → A; +fst (mkPair a b) ≔ a; -------------------------------------------------------------------------------- -- Main @@ -81,7 +81,7 @@ fst _ _ (mkPair a b) ≔ a; fst-of-pair : Action; fst-of-pair ≔ (put-str "fst (True, False) = ") - >> put-str-ln (bool-to-str (fst _ _ (mkPair _ _ true false))); + >> put-str-ln (bool-to-str (fst (mkPair true false))); main : Action; main ≔ fst-of-pair; diff --git a/tests/positive/Polymorphism.mjuvix b/tests/positive/Polymorphism.mjuvix index 39f1ab1a1..f36ce4eb1 100644 --- a/tests/positive/Polymorphism.mjuvix +++ b/tests/positive/Polymorphism.mjuvix @@ -32,24 +32,24 @@ add zero b ≔ b; add (suc a) b ≔ suc (add a b); nil' : (E : Type) → List E; -nil' A ≔ nil A; +nil' A ≔ nil; -- currying nil'' : (E : Type) → List E; -nil'' ≔ nil; +nil'' E ≔ nil; fst : (A : Type) → (B : Type) → Pair A B → A; fst _ _ (mkPair a b) ≔ a; p : Pair Bool Bool; -p ≔ mkPair Bool Bool true false; +p ≔ mkPair true false; swap : (A : Type) → (B : Type) → Pair A B → Pair B A; -swap A B (mkPair a b) ≔ mkPair B A b a; +swap A B (mkPair a b) ≔ mkPair b a; curry : (A : Type) → (B : Type) → (C : Type) → (Pair A B → C) → A → B → C; -curry A B C f a b ≔ f (mkPair A B a b) ; +curry A B C f a b ≔ f (mkPair a b) ; ap : (A : Type) → (B : Type) → (A → B) → A → B; @@ -64,42 +64,42 @@ headDef _ d nil ≔ d; headDef A _ (cons h _) ≔ h; filter : (A : Type) → (A → Bool) → List A → List A; -filter A f nil ≔ nil A; -filter A f (cons x xs) ≔ ite (List A) (f x) (cons A x (filter A f xs)) (filter A f xs); +filter A f nil ≔ nil; +filter A f (cons x xs) ≔ ite (List A) (f x) (cons x (filter A f xs)) (filter A f xs); map : (A : Type) → (B : Type) → (A → B) → List A → List B; -map A B f nil ≔ nil B ; -map A B f (cons x xs) ≔ cons B (f x) (map A B f xs); +map A B f nil ≔ nil ; +map A B f (cons x xs) ≔ cons (f x) (map A B f xs); zip : (A : Type) → (B : Type) → List A → List B → List (Pair A B); -zip A B nil _ ≔ nil (Pair A B); -zip A B _ nil ≔ nil (Pair A B); -zip A B (cons a as) (cons b bs) ≔ nil (Pair A B); +zip A B nil _ ≔ nil; +zip A B _ nil ≔ nil; +zip A B (cons a as) (cons b bs) ≔ nil; zipWith : (A : Type) → (B : Type) → (C : Type) → (A → B → C) → List A → List B → List C; -zipWith A B C f nil _ ≔ nil C; -zipWith A B C f _ nil ≔ nil C; -zipWith A B C f (cons a as) (cons b bs) ≔ cons C (f a b) (zipWith A B C f as bs); +zipWith A B C f nil _ ≔ nil; +zipWith A B C f _ nil ≔ nil; +zipWith A B C f (cons a as) (cons b bs) ≔ cons (f a b) (zipWith A B C f as bs); rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat; -rankn f b n ≔ mkPair Bool Nat (f Bool b) (f Nat n); +rankn f b n ≔ mkPair (f Bool b) (f Nat n); -- currying trankn : Pair Bool Nat; trankn ≔ rankn id false zero; l1 : List Nat; -l1 ≔ cons Nat zero (nil Nat); +l1 ≔ cons zero nil; pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B; pairEval _ _ (mkPair f x) ≔ f x; main : Nat; -main ≔ headDef Nat (pairEval Nat Nat (mkPair (Nat → Nat) Nat (add zero) zero)) +main ≔ headDef Nat (pairEval Nat Nat (mkPair (add zero) zero)) (zipWith Nat Nat Nat add l1 l1); end; diff --git a/tests/positive/PolymorphismHoles.mjuvix b/tests/positive/PolymorphismHoles.mjuvix index 6e8044be9..d7b173f23 100644 --- a/tests/positive/PolymorphismHoles.mjuvix +++ b/tests/positive/PolymorphismHoles.mjuvix @@ -31,25 +31,18 @@ add : Nat → Nat → Nat; add zero b ≔ b; add (suc a) b ≔ suc (add a b); -nil' : (E : Type) → List E; -nil' A ≔ nil _; - --- currying -nil'' : (E : Type) → List E; -nil'' ≔ nil; - fst : (A : Type) → (B : Type) → Pair A B → A; fst _ _ (mkPair a b) ≔ a; p : Pair Bool Bool; -p ≔ mkPair _ _ true false; +p ≔ mkPair true false; swap : (A : Type) → (B : Type) → Pair A B → Pair B A; -swap A B (mkPair a b) ≔ mkPair _ _ b a; +swap A B (mkPair a b) ≔ mkPair b a; curry : (A : Type) → (B : Type) → (C : Type) → (Pair A B → C) → A → B → C; -curry A B C f a b ≔ f (mkPair _ _ a b) ; +curry A B C f a b ≔ f (mkPair a b) ; ap : (A : Type) → (B : Type) → (A → B) → A → B; @@ -64,42 +57,42 @@ ite _ true tt _ ≔ tt; ite _ false _ ff ≔ ff; filter : (A : Type) → (A → Bool) → List A → List A; -filter _ f nil ≔ nil _; -filter _ f (cons x xs) ≔ ite _ (f x) (cons _ x (filter _ f xs)) (filter _ f xs); +filter _ f nil ≔ nil; +filter _ f (cons x xs) ≔ ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs); map : (A : Type) → (B : Type) → (A → B) → List _ → List _; -map _ _ f nil ≔ nil _; -map _ _ f (cons x xs) ≔ cons _ (f x) (map _ _ f xs); +map _ _ f nil ≔ nil; +map _ _ f (cons x xs) ≔ cons (f x) (map _ _ f xs); zip : (A : Type) → (B : Type) → List A → List B → List (Pair A B); -zip A _ nil _ ≔ nil _; -zip _ _ _ nil ≔ nil _; -zip _ _ (cons a as) (cons b bs) ≔ nil _; +zip A _ nil _ ≔ nil; +zip _ _ _ nil ≔ nil; +zip _ _ (cons a as) (cons b bs) ≔ nil; zipWith : (A : Type) → (B : Type) → (C : Type) → (A → B → C) → List A → List B → List C; -zipWith _ _ C f nil _ ≔ nil C; -zipWith _ _ C f _ nil ≔ nil C; -zipWith _ _ _ f (cons a as) (cons b bs) ≔ cons _ (f a b) (zipWith _ _ _ f as bs); +zipWith _ _ C f nil _ ≔ nil; +zipWith _ _ C f _ nil ≔ nil; +zipWith _ _ _ f (cons a as) (cons b bs) ≔ cons (f a b) (zipWith _ _ _ f as bs); rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat; -rankn f b n ≔ mkPair _ _ (f _ b) (f _ n); +rankn f b n ≔ mkPair (f _ b) (f _ n); -- currying trankn : Pair Bool Nat; trankn ≔ rankn id false zero; l1 : List Nat; -l1 ≔ cons _ zero (nil _); +l1 ≔ cons zero nil; pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B; pairEval _ _ (mkPair f x) ≔ f x; main : Nat; -main ≔ headDef _ (pairEval _ _ (mkPair _ _ (add zero) zero)) +main ≔ headDef _ (pairEval _ _ (mkPair (add zero) zero)) (zipWith _ _ _ add l1 l1); end;