diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 5db1059dd..fd0d3a593 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -17,7 +17,12 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Prelude data NameSignatureBuilder s :: Effect where - AddSymbol :: IsImplicit -> Maybe (ArgDefault s) -> SymbolType s -> ExpressionType s -> NameSignatureBuilder s m () + AddArgument :: + IsImplicit -> + Maybe (ArgDefault s) -> + Maybe (SymbolType s) -> + ExpressionType s -> + NameSignatureBuilder s m () EndBuild :: Proxy s -> NameSignatureBuilder s m a -- | for debugging GetBuilder :: NameSignatureBuilder s m (BuilderState s) @@ -34,6 +39,15 @@ data BuilderState (s :: Stage) = BuilderState makeLenses ''BuilderState makeSem ''NameSignatureBuilder +addSymbol :: + (Members '[NameSignatureBuilder s] r) => + IsImplicit -> + Maybe (ArgDefault s) -> + SymbolType s -> + ExpressionType s -> + Sem r () +addSymbol isImplicit mdefault sym ty = addArgument isImplicit mdefault (Just sym) ty + class HasNameSignature (s :: Stage) d | d -> s where addArgs :: (Members '[NameSignatureBuilder s] r) => d -> Sem r () @@ -167,17 +181,23 @@ addInductiveParams = addInductiveParams' Explicit addConstructorParams :: (SingI s, Members '[NameSignatureBuilder s] r) => InductiveParameters s -> Sem r () addConstructorParams = addInductiveParams' Implicit -addSigArg :: (SingI s, Members '[NameSignatureBuilder s] r) => SigArg s -> Sem r () -addSigArg a = forM_ (a ^. sigArgNames) $ \case - ArgumentSymbol s -> - addSymbol - (a ^. sigArgImplicit) - (a ^. sigArgDefault) - s - (fromMaybe defaultType (a ^. sigArgType)) - where - defaultType = run (runReader (getLoc a) Gen.smallUniverseExpression) - ArgumentWildcard {} -> return () +addSigArg :: forall s r. (SingI s, Members '[NameSignatureBuilder s] r) => SigArg s -> Sem r () +addSigArg a = case a ^. sigArgNames of + SigArgNamesInstance {} -> addArg (ArgumentWildcard (Wildcard (getLoc a))) + SigArgNames ns -> mapM_ addArg ns + where + defaultType = run (runReader (getLoc a) Gen.smallUniverseExpression) + + addArg :: Argument s -> Sem r () + addArg arg = + let sym :: Maybe (SymbolType s) = case arg of + ArgumentSymbol sy -> Just sy + ArgumentWildcard {} -> Nothing + in addArgument + (a ^. sigArgImplicit) + (a ^. sigArgDefault) + sym + (fromMaybe defaultType (a ^. sigArgType)) type Re s r = State (BuilderState s) ': Error (BuilderState s) ': Error NameSignatureError ': r @@ -187,20 +207,27 @@ re :: Sem (NameSignatureBuilder s ': r) a -> Sem (Re s r) a re = interpretTop3 $ \case - AddSymbol impl mdef k ty -> addSymbol' impl mdef k ty + AddArgument impl mdef k ty -> addArgument' impl mdef k ty EndBuild {} -> endBuild' GetBuilder -> get {-# INLINE re #-} -addSymbol' :: forall s r. (SingI s) => IsImplicit -> Maybe (ArgDefault s) -> SymbolType s -> ExpressionType s -> Sem (Re s r) () -addSymbol' impl mdef sym ty = do +addArgument' :: + forall s r. + (SingI s) => + IsImplicit -> + Maybe (ArgDefault s) -> + Maybe (SymbolType s) -> + ExpressionType s -> + Sem (Re s r) () +addArgument' impl mdef msym ty = do curImpl <- gets @(BuilderState s) (^. stateCurrentImplicit) if | Just impl == curImpl -> addToCurrentBlock | otherwise -> startNewBlock where - errDuplicateName :: Symbol -> Sem (Re s r) () - errDuplicateName _dupNameFirst = + errDuplicateName :: SymbolType s -> Symbol -> Sem (Re s r) () + errDuplicateName sym _dupNameFirst = throw $ ErrDuplicateName DuplicateName @@ -208,22 +235,28 @@ addSymbol' impl mdef sym ty = do .. } + getNextIx :: (Members '[State (BuilderState s)] r') => Sem r' Int + getNextIx = do + idx <- gets @(BuilderState s) (^. stateNextIx) + modify' @(BuilderState s) (over stateNextIx succ) + return idx + addToCurrentBlock :: Sem (Re s r) () addToCurrentBlock = do - idx <- gets @(BuilderState s) (^. stateNextIx) - let itm = - NameItem - { _nameItemDefault = mdef, - _nameItemSymbol = sym, - _nameItemImplicit = impl, - _nameItemIndex = idx, - _nameItemType = ty - } - psym = symbolParsed sym - modify' @(BuilderState s) (over stateNextIx succ) - whenJustM (gets @(BuilderState s) (^. stateSymbols . at psym)) (errDuplicateName . symbolParsed) - modify' @(BuilderState s) (set (stateSymbols . at psym) (Just sym)) - modify' @(BuilderState s) (set (stateCurrentBlock . at psym) (Just itm)) + idx <- getNextIx + whenJust msym $ \(sym :: SymbolType s) -> do + let itm = + NameItem + { _nameItemDefault = mdef, + _nameItemSymbol = sym, + _nameItemImplicit = impl, + _nameItemIndex = idx, + _nameItemType = ty + } + psym = symbolParsed sym + whenJustM (gets @(BuilderState s) (^. stateSymbols . at psym)) (errDuplicateName sym . symbolParsed) + modify' @(BuilderState s) (set (stateSymbols . at psym) (Just sym)) + modify' @(BuilderState s) (set (stateCurrentBlock . at psym) (Just itm)) startNewBlock :: Sem (Re s r) () startNewBlock = do @@ -234,7 +267,7 @@ addSymbol' impl mdef sym ty = do modify' @(BuilderState s) (set stateNextIx 0) whenJust mcurImpl $ \curImpl -> modify' (over stateReverseClosedBlocks (NameBlock curBlock curImpl :)) - addSymbol' impl mdef sym ty + addArgument' impl mdef msym ty endBuild' :: forall s r a. Sem (Re s r) a endBuild' = get @(BuilderState s) >>= throw diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 109e9e684..5db132990 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -532,11 +532,37 @@ deriving stock instance Ord (ArgDefault 'Parsed) deriving stock instance Ord (ArgDefault 'Scoped) +-- | This type makes explicit that only instance arguments are allowed to not +-- have a name +data SigArgNames (s :: Stage) + = SigArgNamesInstance + | SigArgNames (NonEmpty (Argument s)) + deriving stock (Generic) + +instance Serialize (SigArgNames 'Scoped) + +instance NFData (SigArgNames 'Scoped) + +instance Serialize (SigArgNames 'Parsed) + +instance NFData (SigArgNames 'Parsed) + +deriving stock instance Show (SigArgNames 'Parsed) + +deriving stock instance Show (SigArgNames 'Scoped) + +deriving stock instance Eq (SigArgNames 'Parsed) + +deriving stock instance Eq (SigArgNames 'Scoped) + +deriving stock instance Ord (SigArgNames 'Parsed) + +deriving stock instance Ord (SigArgNames 'Scoped) + data SigArg (s :: Stage) = SigArg { _sigArgDelims :: Irrelevant (KeywordRef, KeywordRef), _sigArgImplicit :: IsImplicit, - -- | Allowed to be empty only for Instance arguments - _sigArgNames :: [Argument s], + _sigArgNames :: SigArgNames s, _sigArgColon :: Maybe (Irrelevant KeywordRef), -- | The type is only optional for implicit arguments. Omitting the rhs is -- equivalent to writing `: Type`. diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index a10018ddd..ec0bcc501 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -240,7 +240,7 @@ instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (a, b) where instance (SingI s) => PrettyPrint (NameSignature s) where ppCode NameSignature {..} | null _nameSignatureArgs = noLoc (pretty @Text "") - | otherwise = hsep . map ppCode $ _nameSignatureArgs + | otherwise = itemize . map ppCode $ _nameSignatureArgs instance (SingI s) => PrettyPrint (WildcardConstructor s) where ppCode WildcardConstructor {..} = do @@ -1110,11 +1110,16 @@ instance (SingI s) => PrettyPrint (ArgDefault s) where ppCode ArgDefault {..} = do ppCode _argDefaultAssign <+> ppExpressionType _argDefaultValue +instance (SingI s) => PrettyPrint (SigArgNames s) where + ppCode = \case + SigArgNamesInstance -> return () + SigArgNames ns -> hsep (fmap ppCode ns) + instance (SingI s) => PrettyPrint (SigArg s) where ppCode :: (Members '[ExactPrint, Reader Options] r) => SigArg s -> Sem r () ppCode SigArg {..} = do let Irrelevant (l, r) = _sigArgDelims - names' = hsep (fmap ppCode _sigArgNames) + names' = ppCode _sigArgNames colon' = ppCode <$> _sigArgColon ty = ppExpressionType <$> _sigArgType arg = case _sigArgImplicit of diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 2bb813d7a..d9f8572d5 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1098,11 +1098,16 @@ checkFunctionDef FunctionDef {..} = do registerNameSignature (sigName' ^. S.nameId) def registerFunctionDef @$> def where + checkSigArgNames :: SigArgNames 'Parsed -> Sem r (SigArgNames 'Scoped) + checkSigArgNames = \case + SigArgNamesInstance -> return SigArgNamesInstance + SigArgNames ns -> fmap SigArgNames . forM ns $ \case + ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s + ArgumentWildcard w -> return (ArgumentWildcard w) + checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped) checkArg arg@SigArg {..} = do - names' <- forM _sigArgNames $ \case - ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s - ArgumentWildcard w -> return $ ArgumentWildcard w + names' <- checkSigArgNames _sigArgNames ty' <- mapM checkParseExpressionAtoms _sigArgType default' <- case _sigArgDefault of Nothing -> return Nothing diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 5f6da993b..77ba8a873 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1400,18 +1400,18 @@ functionDefinition allowOmitType allowInstance _signBuiltin = P.label " kw kwColon return (n, c) - (ns, c) <- case impl of + (ns :: SigArgNames 'Parsed, c) <- case impl of ImplicitInstance -> do ma <- optional parseArgumentNameColon return $ case ma of - Just (ns', c') -> ([ns'], Just c') - Nothing -> ([], Nothing) + Just (ns', c') -> (SigArgNames (pure ns'), Just c') + Nothing -> (SigArgNamesInstance, Nothing) Implicit -> do - ns <- some parseArgumentName + ns <- SigArgNames <$> some1 parseArgumentName c <- optional (Irrelevant <$> kw kwColon) return (ns, c) Explicit -> do - ns <- some parseArgumentName + ns <- SigArgNames <$> some1 parseArgumentName c <- Just . Irrelevant <$> kw kwColon return (ns, c) return (opn, ns, impl, c) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index d9078eac0..40b10142e 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -37,6 +37,12 @@ instance PrettyCode Name where showNameId <- asks (^. optShowNameIds) return (prettyName showNameId n) +instance PrettyCode ArgInfo where + ppCode ArgInfo {..} = do + name <- maybe (return kwWildcard) ppCode _argInfoName + defVal <- mapM (fmap (kwAssign <+>) . ppCode) _argInfoDefault + return (name <+?> defVal) + instance PrettyCode Iden where ppCode :: (Member (Reader Options) r) => Iden -> Sem r (Doc Ann) ppCode i = case i of diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index af2d30ae9..f4932b6f5 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -20,6 +20,7 @@ import Juvix.Compiler.Concrete.Extra qualified as Concrete import Juvix.Compiler.Concrete.Gen qualified as Gen import Juvix.Compiler.Concrete.Language qualified as Concrete import Juvix.Compiler.Concrete.Pretty +import Juvix.Compiler.Concrete.Print import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Internal.Builtins @@ -393,11 +394,11 @@ goFunctionDef FunctionDef {..} = do goBlock :: NameBlock 'Scoped -> Sem r [Internal.ArgInfo] goBlock blk = do let tbl = indexedByInt (^. nameItemIndex) (blk ^. nameBlock) - mmaxIx = fst <$> IntMap.lookupMax tbl - case mmaxIx of - Nothing -> return [] + mmaxIx :: Maybe Int = fst <$> IntMap.lookupMax tbl + execOutputList $ case mmaxIx of + Nothing -> output Internal.emptyArgInfo Just maxIx -> - execOutputList $ forM_ [0 .. maxIx] $ \idx -> + forM_ [0 .. maxIx] $ \idx -> case tbl ^. at idx of Nothing -> output Internal.emptyArgInfo Just i -> do @@ -462,7 +463,12 @@ goFunctionDef FunctionDef {..} = do Concrete.ArgumentWildcard {} -> Nothing in Internal.FunctionParameter {..} - return . fromMaybe (pure noName) $ nonEmpty (mk <$> _sigArgNames) + arguments :: Maybe (NonEmpty (Argument 'Scoped)) + arguments = case _sigArgNames of + SigArgNamesInstance -> Nothing + SigArgNames ns -> Just ns + + return (maybe (pure noName) (fmap mk) arguments) argToPattern :: SigArg 'Scoped -> Sem r (NonEmpty Internal.PatternArg) argToPattern arg@SigArg {..} = do @@ -478,7 +484,12 @@ goFunctionDef FunctionDef {..} = do let _patternArgPattern = Internal.PatternVariable (goSymbol s) in return Internal.PatternArg {..} Concrete.ArgumentWildcard w -> goWildcard w - maybe (pure <$> noName) (mapM mk) (nonEmpty _sigArgNames) + + arguments :: Maybe (NonEmpty (Argument 'Scoped)) + arguments = case _sigArgNames of + SigArgNamesInstance -> Nothing + SigArgNames ns -> Just ns + maybe (pure <$> noName) (mapM mk) arguments goInductiveParameters :: forall r. diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index d61d479ee..55928a82c 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -326,7 +326,11 @@ tests = posTestAbsDir "Typecheck orphan file" (relToProject $(mkRelDir "tests/WithoutPackageFile")) - $(mkRelFile "Good.juvix") + $(mkRelFile "Good.juvix"), + posTest + "Default argument with trait in signature" + $(mkRelDir ".") + $(mkRelFile "issue2994.juvix") ] <> [ compilationTest t | t <- Compilation.tests ] diff --git a/tests/positive/issue2994.juvix b/tests/positive/issue2994.juvix new file mode 100644 index 000000000..2867242c3 --- /dev/null +++ b/tests/positive/issue2994.juvix @@ -0,0 +1,12 @@ +module issue2994; + +type T := t; + +type Maybe (a : Type) := + | nothing + | just a; + +trait +type SomeTrait A := mkSomeTrait {baz : A -> T}; + +bar {{SomeTrait T}} (value : T) {maybeValue : Maybe T := nothing} : T := t;