diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index dcdddc2b97..7c60131a55 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -1,6 +1,9 @@ {-# LANGUAGE FunctionalDependencies #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# OPTIONS_GHC -Wno-unused-type-patterns #-} +{-# HLINT ignore "Avoid restricted flags" #-} + module Juvix.Compiler.Concrete.Data.NameSignature.Builder ( mkNameSignature, mkRecordNameSignature, @@ -32,7 +35,8 @@ data BuilderState (s :: Stage) = BuilderState -- | maps to itself _stateSymbols :: HashMap Symbol (SymbolType s), _stateReverseClosedBlocks :: [NameBlock s], - _stateCurrentBlock :: HashMap Symbol (NameItem s) + -- | Items stored in reverse order + _stateCurrentBlockReverse :: [NameItem s] } makeLenses ''BuilderState @@ -116,7 +120,7 @@ iniBuilderState = _stateNextIx = 0, _stateSymbols = mempty, _stateReverseClosedBlocks = [], - _stateCurrentBlock = mempty + _stateCurrentBlockReverse = mempty } fromBuilderState :: forall s. BuilderState s -> NameSignature s @@ -126,11 +130,16 @@ fromBuilderState b = } where addCurrent :: [NameBlock s] -> [NameBlock s] - addCurrent - | null (b ^. stateCurrentBlock) = id - | Just i <- b ^. stateCurrentImplicit = - (NameBlock (b ^. stateCurrentBlock) i :) - | otherwise = id + addCurrent = case (nonEmpty (reverse (b ^. stateCurrentBlockReverse)), b ^. stateCurrentImplicit) of + (Just newBlock, Just i) -> (mkNameBlock newBlock i :) + _ -> id + +mkNameBlock :: NonEmpty (NameItem s) -> IsImplicit -> NameBlock s +mkNameBlock items impl = + NameBlock + { _nameBlockItems = items, + _nameBlockImplicit = impl + } addExpression :: forall r. (Members '[NameSignatureBuilder 'Scoped] r) => Expression -> Sem r () addExpression = \case @@ -185,18 +194,19 @@ addSigArg a = case a ^. sigArgNames of SigArgNamesInstance {} -> addArg (ArgumentWildcard (Wildcard (getLoc a))) SigArgNames ns -> mapM_ addArg ns where + defaultType :: ExpressionType s defaultType = run (runReader (getLoc a) Gen.smallUniverseExpression) addArg :: Argument s -> Sem r () - addArg arg = + addArg arg = do 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)) + addArgument + (a ^. sigArgImplicit) + (a ^. sigArgDefault) + sym + (fromMaybe defaultType (a ^. sigArgType)) type Re s r = State (BuilderState s) ': Error (BuilderState s) ': Error NameSignatureError ': r @@ -244,28 +254,29 @@ addArgument' impl mdef msym ty = do addToCurrentBlock = do idx <- getNextIx whenJust msym $ \(sym :: SymbolType s) -> do - let itm = - NameItem - { _nameItemDefault = mdef, - _nameItemSymbol = sym, - _nameItemImplicit = impl, - _nameItemIndex = idx, - _nameItemType = ty - } - psym = symbolParsed sym + let 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)) + let itm = + NameItem + { _nameItemDefault = mdef, + _nameItemSymbol = msym, + _nameItemImplicit = impl, + _nameItemIndex = idx, + _nameItemType = ty + } + modify' @(BuilderState s) (over (stateCurrentBlockReverse) (itm :)) startNewBlock :: Sem (Re s r) () startNewBlock = do - curBlock <- gets @(BuilderState s) (^. stateCurrentBlock) + curBlock <- nonEmpty' . reverse <$> gets @(BuilderState s) (^. stateCurrentBlockReverse) mcurImpl <- gets @(BuilderState s) (^. stateCurrentImplicit) modify' @(BuilderState s) (set stateCurrentImplicit (Just impl)) - modify' @(BuilderState s) (set stateCurrentBlock mempty) + modify' @(BuilderState s) (set stateCurrentBlockReverse mempty) modify' @(BuilderState s) (set stateNextIx 0) whenJust mcurImpl $ \curImpl -> - modify' (over stateReverseClosedBlocks (NameBlock curBlock curImpl :)) + let newBlock = mkNameBlock curBlock curImpl + in modify' (over stateReverseClosedBlocks (newBlock :)) addArgument' impl mdef msym ty endBuild' :: forall s r a. Sem (Re s r) a @@ -275,9 +286,9 @@ mkRecordNameSignature :: forall s. (SingI s) => RhsRecord s -> RecordNameSignatu mkRecordNameSignature rhs = RecordNameSignature $ hashMap - [ ( symbolParsed _nameItemSymbol, + [ ( symbolParsed sym, NameItem - { _nameItemSymbol, + { _nameItemSymbol = Just sym, _nameItemIndex, _nameItemType = field ^. fieldType, _nameItemImplicit = fromIsImplicitField (field ^. fieldIsImplicit), @@ -285,5 +296,5 @@ mkRecordNameSignature rhs = } ) | (Indexed _nameItemIndex field) <- indexFrom 0 (toList (rhs ^.. rhsRecordStatements . each . _RecordStatementField)), - let _nameItemSymbol :: SymbolType s = field ^. fieldName + let sym :: SymbolType s = field ^. fieldName ] diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 25c122fc75..fdd482376d 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -156,7 +156,9 @@ type family ModuleEndType t = res | res -> t where type ParsedPragmas = WithLoc (WithSource Pragmas) data NameItem (s :: Stage) = NameItem - { _nameItemSymbol :: SymbolType s, + { -- | The symbol cannot be omitted for explicit arguments + _nameItemSymbol :: Maybe (SymbolType s), + -- | NOTE the index is wrt to the block, not the whole signature _nameItemIndex :: Int, _nameItemImplicit :: IsImplicit, _nameItemType :: ExpressionType s, @@ -173,10 +175,8 @@ instance Serialize (NameItem 'Parsed) instance NFData (NameItem 'Parsed) data NameBlock (s :: Stage) = NameBlock - { -- | Symbols map to themselves so we can retrieve the location - -- | NOTE the index is wrt to the block, not the whole signature. - _nameBlock :: HashMap Symbol (NameItem s), - _nameImplicit :: IsImplicit + { _nameBlockItems :: NonEmpty (NameItem s), + _nameBlockImplicit :: IsImplicit } deriving stock (Generic) @@ -3519,6 +3519,9 @@ fromParsedIteratorInfo ParsedIteratorInfo {..} = _iteratorInfoRangeNum = (^. withLocParam) <$> _parsedIteratorInfoRangeNum } +nameBlockSymbols :: forall s. Traversal' (NameBlock s) (SymbolType s) +nameBlockSymbols = nameBlockItems . each . nameItemSymbol . _Just + instance HasFixity PostfixApplication where getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIdenSrcName . S.nameFixity) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 0bb4d9be43..c34e083876 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -195,15 +195,23 @@ instance (SingI s) => PrettyPrint (ListPattern s) where instance PrettyPrint Interval where ppCode = noLoc . pretty +instance PrettyPrint Int where + ppCode = noLoc . pretty + instance PrettyPrint Void where ppCode = absurd instance (SingI s) => PrettyPrint (NameItem s) where + ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => NameItem s -> Sem r () ppCode NameItem {..} = do let defaultVal = do d <- _nameItemDefault return (noLoc C.kwAssign <+> ppExpressionType (d ^. argDefaultValue)) - isImplicitDelims _nameItemImplicit (ppSymbolType _nameItemSymbol) + ppSym :: Maybe (SymbolType s) -> Sem r () + ppSym = \case + Nothing -> ppCode Kw.kwWildcard + Just s -> ppSymbolType s + isImplicitDelims _nameItemImplicit (ppSym _nameItemSymbol) <> ppCode Kw.kwExclamation <> noLoc (pretty _nameItemIndex) <+> ppCode Kw.kwColon @@ -218,7 +226,10 @@ isImplicitDelims = \case instance (SingI s) => PrettyPrint (NameBlock s) where ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => NameBlock s -> Sem r () - ppCode NameBlock {..} = isImplicitDelims _nameImplicit (vsepSemicolon (map ppCode (toList _nameBlock))) + ppCode NameBlock {..} = + isImplicitDelims _nameBlockImplicit + . vsepSemicolon + $ fmap ppCode _nameBlockItems instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (HashMap a b) where ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => HashMap a b -> Sem r () diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index e16052d2e0..00cb69e4c2 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -2715,7 +2715,12 @@ checkNamedApplicationNew napp = do if | null nargs -> return (NameSignature []) | otherwise -> getNameSignatureParsed aname - let namesInSignature = hashSet (concatMap (HashMap.keys . (^. nameBlock)) (sig ^. nameSignatureArgs)) + let namesInSignature = + hashSet $ + sig + ^.. nameSignatureArgs + . each + . nameBlockSymbols forM_ nargs (checkNameInSignature namesInSignature . (^. namedArgumentNewSymbol)) puns <- scopePuns args' <- withLocalScope . localBindings . ignoreSyntax $ do @@ -2723,8 +2728,8 @@ checkNamedApplicationNew napp = do mapM (checkNamedArgumentNew puns) nargs let signatureExplicitNames = hashSet - . concatMap (HashMap.keys . (^. nameBlock)) - . filter (not . isImplicitOrInstance . (^. nameImplicit)) + . concatMap (^.. nameBlockSymbols) + . filter (not . isImplicitOrInstance . (^. nameBlockImplicit)) $ sig ^. nameSignatureArgs givenNames :: HashSet Symbol = hashSet (map (^. namedArgumentNewSymbol) nargs) missingArgs = HashSet.difference signatureExplicitNames givenNames @@ -2807,7 +2812,8 @@ checkRecordUpdate RecordUpdate {..} = do where bindRecordUpdateVariable :: NameItem 'Parsed -> Sem r (IsImplicit, S.Symbol) bindRecordUpdateVariable NameItem {..} = do - v <- bindVariableSymbol _nameItemSymbol + -- all fields have names so it is safe to use fromJust + v <- bindVariableSymbol (fromJust _nameItemSymbol) return (_nameItemImplicit, v) checkUpdateField :: diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 251cda09c7..69f94f487c 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -383,32 +383,26 @@ goFunctionDef FunctionDef {..} = do _funDefPragmas <- goPragmas _signPragmas _funDefBody <- goBody msig <- asks (^. S.infoNameSigs . at (_funDefName ^. Internal.nameId)) - _funDefArgsInfo <- maybe (return mempty) goNameSignature msig + _funDefArgsInfo <- maybe (return mempty) (fmap toList . goNameSignature) msig let _funDefDocComment = fmap ppPrintJudoc _signDoc fun = Internal.FunctionDef {..} whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam)) return fun where goNameSignature :: NameSignature 'Scoped -> Sem r [Internal.ArgInfo] - goNameSignature = concatMapM goBlock . (^. nameSignatureArgs) + goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs) where - goBlock :: NameBlock 'Scoped -> Sem r [Internal.ArgInfo] - goBlock blk = do - let tbl = indexedByInt (^. nameItemIndex) (blk ^. nameBlock) - mmaxIx :: Maybe Int = fst <$> IntMap.lookupMax tbl - execOutputList $ case mmaxIx of - Nothing -> output Internal.emptyArgInfo - Just maxIx -> - forM_ [0 .. maxIx] $ \idx -> - case tbl ^. at idx of - Nothing -> output Internal.emptyArgInfo - Just i -> do - _argInfoDefault' <- mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue) - output - Internal.ArgInfo - { _argInfoDefault = _argInfoDefault', - _argInfoName = Just (goSymbol (i ^. nameItemSymbol)) - } + goBlock :: NameBlock 'Scoped -> Sem r (NonEmpty Internal.ArgInfo) + goBlock blk = mapM goItem (blk ^. nameBlockItems) + where + goItem :: NameItem 'Scoped -> Sem r Internal.ArgInfo + goItem i = do + _argInfoDefault' <- mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue) + return + Internal.ArgInfo + { _argInfoDefault = _argInfoDefault', + _argInfoName = goSymbol <$> (i ^. nameItemSymbol) + } goBody :: Sem r Internal.Expression goBody = do @@ -761,9 +755,10 @@ goListPattern l = localBuiltins $ do where loc = getLoc l -createArgumentBlocks :: NonEmpty (NamedArgumentNew 'Scoped) -> [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped] +createArgumentBlocks :: NonEmpty (NamedArgumentNew 'Scoped) -> [NameBlock 'Scoped] -> NonEmpty (ArgumentBlock 'Scoped) createArgumentBlocks appargs = - run + nonEmpty' + . run . execOutputList . evalState args0 . mapM_ goBlock @@ -778,11 +773,11 @@ createArgumentBlocks appargs = (Members '[State (HashSet S.Symbol), Output (ArgumentBlock 'Scoped)] r) => NameBlock 'Scoped -> Sem r () - goBlock NameBlock {..} = do + goBlock b@NameBlock {..} = do args <- get let namesInBlock :: HashSet Symbol = HashSet.intersection - (HashMap.keysSet _nameBlock) + (hashSet (symbolParsed <$> b ^.. nameBlockSymbols)) (HashSet.map (^. S.nameConcrete) args) argNames :: HashMap Symbol S.Symbol = indexedByHash (^. S.nameConcrete) args getName sym = fromJust (argNames ^. at sym) @@ -790,7 +785,7 @@ createArgumentBlocks appargs = let block' = ArgumentBlock { _argBlockDelims = Irrelevant Nothing, - _argBlockImplicit = _nameImplicit, + _argBlockImplicit = _nameBlockImplicit, _argBlockArgs = goArg . getName <$> namesInBlock1 } modify (HashSet.filter (not . flip HashSet.member namesInBlock . (^. S.nameConcrete))) @@ -857,7 +852,7 @@ goExpression = \case let name = napp ^. namedApplicationNewName . scopedIdenFinal sig <- fromJust <$> asks (^. S.infoNameSigs . at (name ^. S.nameId)) let fun = napp ^. namedApplicationNewName - blocks = nonEmpty' (createArgumentBlocks appargs (sig ^. nameSignatureArgs)) + blocks = createArgumentBlocks appargs (sig ^. nameSignatureArgs) compiledNameApp <- goNamedApplication fun blocks extraArgs case nonEmpty (appargs ^.. each . _NamedArgumentNewFunction) of Nothing -> return compiledNameApp @@ -883,48 +878,69 @@ goExpression = \case goDesugaredNamedApplication :: DesugaredNamedApplication -> Sem r Internal.Expression goDesugaredNamedApplication a = do let fun = goScopedIden (a ^. dnamedAppIdentifier) - updateKind :: Internal.Subs = Internal.subsKind (a ^.. dnamedAppArgs . each . argName . to goSymbol) KNameFunction - mkAppArg :: Arg -> Internal.ApplicationArg - mkAppArg arg = - Internal.ApplicationArg - { _appArgIsImplicit = arg ^. argImplicit, - _appArg = Internal.toExpression (goSymbol (arg ^. argName)) - } - namedArgNames :: NonEmpty Internal.ApplicationArg = mkAppArg <$> a ^. dnamedAppArgs - allArgs = toList namedArgNames <> a ^. dnamedExtraArgs + updateKind :: Internal.Subs = + Internal.subsKind + ( a + ^.. dnamedAppArgs + . each + . argName + . _Just + . to goSymbol + ) + KNameFunction + mkAppArg :: Arg -> Sem r Internal.ApplicationArg + mkAppArg arg = do + expr <- case arg ^. argName of + Nothing -> goExpression (arg ^. argValue) + Just argname -> return (Internal.toExpression (goSymbol argname)) + + return + Internal.ApplicationArg + { _appArgIsImplicit = arg ^. argImplicit, + _appArg = expr + } + namedArgNames :: NonEmpty Internal.ApplicationArg <- mapM mkAppArg (a ^. dnamedAppArgs) + let allArgs = toList namedArgNames <> a ^. dnamedExtraArgs app = Internal.foldApplication (Internal.toExpression fun) allArgs - clauses <- mapM mkClause (a ^. dnamedAppArgs) + clauses :: [Internal.LetClause] <- mapMaybeM mkClause (toList (a ^. dnamedAppArgs)) + expr <- Internal.substitutionE updateKind $ - Internal.ExpressionLet - Internal.Let - { _letExpression = app, - _letClauses = clauses - } + case nonEmpty clauses of + Nothing -> app + Just clauses1 -> + Internal.ExpressionLet + Internal.Let + { _letExpression = app, + _letClauses = clauses1 + } Internal.clone expr where - mkClause :: Arg -> Sem r Internal.LetClause - mkClause arg = do - checkCycle - let name = arg ^. argName - adjust - | arg ^. argAutoInserted = over defaultArgsStack (name :) - | otherwise = id - local adjust $ do - body' <- goExpression (arg ^. argValue) - ty <- goExpression (arg ^. argType) - return $ - Internal.LetFunDef - (Internal.simpleFunDef (goSymbol name) ty body') - where - checkCycle :: Sem r () - checkCycle = do - st <- asks (^. defaultArgsStack) - case span (/= (arg ^. argName)) st of - (_, []) -> return () - (c, _) -> - let cyc = NonEmpty.reverse ((arg ^. argName) :| c) - in throw (ErrDefaultArgCycle (DefaultArgCycle cyc)) + mkClause :: Arg -> Sem r (Maybe Internal.LetClause) + mkClause arg = case arg ^. argName of + Nothing -> return Nothing + Just name -> do + checkCycle + let adjust :: DefaultArgsStack -> DefaultArgsStack + | arg ^. argAutoInserted = over defaultArgsStack (name :) + | otherwise = id + local adjust $ do + body' <- goExpression (arg ^. argValue) + ty <- goExpression (arg ^. argType) + return $ + Just + ( Internal.LetFunDef + (Internal.simpleFunDef (goSymbol name) ty body') + ) + where + checkCycle :: Sem r () + checkCycle = do + st <- asks (^. defaultArgsStack) + case span (/= name) st of + (_, []) -> return () + (c, _) -> + let cyc = NonEmpty.reverse (name :| c) + in throw (ErrDefaultArgCycle (DefaultArgCycle cyc)) goRecordUpdate :: Concrete.RecordUpdate 'Scoped -> Sem r Internal.Lambda goRecordUpdate r = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs index e35cfcd669..3f5d5e8086 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs @@ -16,6 +16,7 @@ where import Data.HashMap.Strict qualified as HashMap import Data.IntMap.Strict qualified as IntMap import Juvix.Compiler.Concrete.Data.ScopedName qualified as S +import Juvix.Compiler.Concrete.Pretty (ppTrace) import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Internal.Extra.Base qualified as Internal import Juvix.Prelude @@ -28,7 +29,8 @@ data BuilderState = BuilderState } data Arg = Arg - { _argName :: S.Symbol, + { -- | Explicit arguments cannot omit the name + _argName :: Maybe S.Symbol, _argImplicit :: IsImplicit, _argType :: Expression, _argAutoInserted :: Bool, @@ -95,8 +97,8 @@ helper loc = do whenJustM nextArgumentGroup $ \(impl, args, isLastBlock) -> do checkRepeated args names :: [NameItem 'Scoped] <- nextNameGroup impl - (pendingArgs, (omittedNames, argmap)) <- scanGroup impl names args - emitArgs impl isLastBlock (mkNamesIndex names) omittedNames argmap + (pendingArgs, (omittedItems, argmap)) <- scanGroup impl names args + emitArgs impl isLastBlock (mkNamesIndex names) omittedItems argmap whenJust (nonEmpty pendingArgs) $ \pendingArgs' -> do sig <- nextNameGroup Implicit emitImplicit False (mkNamesIndex sig) sig mempty @@ -112,10 +114,11 @@ helper loc = do case remb of [] -> return mempty (b :: NameBlock 'Scoped) : bs -> do - let implSig = b ^. nameImplicit - namesByIx = mkNamesIndex (toList (b ^. nameBlock)) + let implSig = b ^. nameBlockImplicit + itemsList = toList (b ^. nameBlockItems) + namesByIx :: NamesByIndex = mkNamesIndex itemsList modify' (set stateRemainingNames bs) - let r = toList (b ^. nameBlock) + let r = itemsList matches = return r case (implArgs, implSig) of (Explicit, Explicit) -> matches @@ -161,12 +164,15 @@ helper loc = do -- omitting arguments is only allowed at the end emitExplicit :: Bool -> NamesByIndex -> [NameItem 'Scoped] -> IntMap Arg -> Sem r () emitExplicit lastBlock _ omittedArgs args = do + -- Explicit arguments must have a name, so it is safe to use fromJust + let itemName :: NameItem 'Scoped -> SymbolType 'Scoped + itemName = fromJust . (^. nameItemSymbol) if | lastBlock -> unless (IntMap.keys args == [0 .. IntMap.size args - 1]) - (missingErr (nonEmpty' (map (^. nameItemSymbol) (filterMissing omittedArgs)))) - | otherwise -> whenJust (nonEmpty (map (^. nameItemSymbol) omittedArgs)) missingErr + (missingErr (nonEmpty' (map itemName (filterMissing omittedArgs)))) + | otherwise -> whenJust (nonEmpty (map itemName omittedArgs)) missingErr forM_ args output where filterMissing :: [NameItem 'Scoped] -> [NameItem 'Scoped] @@ -204,12 +210,20 @@ helper loc = do fillPosition :: (Members '[NameIdGen] r') => Int -> Sem r' Arg fillPosition idx = do - let nm :: NameItem 'Scoped = namesByIx ^?! at idx . _Just + let nm :: NameItem 'Scoped = fromMaybe err (namesByIx ^. at idx) + err :: forall x. x + err = + impossibleError + ( "namesByIx ^. at " + <> prettyText idx + <> " = Nothing" + <> "\nnamesByIx = " + <> ppTrace (IntMap.toList namesByIx) + ) _argValue <- case nm ^. nameItemDefault of Nothing -> exprHole . mkHole loc <$> freshNameId -- TODO update location Just d -> return (d ^. argDefaultValue) - return Arg { _argName = nm ^. nameItemSymbol, @@ -218,6 +232,7 @@ helper loc = do _argAutoInserted = True, _argValue } + maxIx :: Maybe Int maxIx = fmap maximum1 . nonEmpty . map (^. nameItemIndex) $ omittedArgs @@ -233,14 +248,24 @@ helper loc = do [NamedArgumentAssign 'Scoped] -> Sem r ([NamedArgumentAssign 'Scoped], ([NameItem 'Scoped], IntMap Arg)) scanGroup impl names = - fmap (second (first toList)) + fmap (second (first ((<> noNameItems) . toList))) . runOutputList . runState namesBySymbol . execState mempty . mapM_ go where + -- Symbols omitted because they don't have a name + noNameItems :: [NameItem 'Scoped] + noNameItems = filter (isNothing . (^. nameItemSymbol)) names + namesBySymbol :: HashMap Symbol (NameItem 'Scoped) - namesBySymbol = HashMap.fromList [(symbolParsed (i ^. nameItemSymbol), i) | i <- names] + namesBySymbol = + hashMap + [ (symbolParsed sym, i) + | i <- names, + Just sym <- [i ^. nameItemSymbol] + ] + go :: (Members '[State (IntMap Arg), State (HashMap Symbol (NameItem 'Scoped)), State BuilderState, Output (NamedArgumentAssign 'Scoped), Error NamedArgumentsError] r') => NamedArgumentAssign 'Scoped -> diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index bb84182627..204e25905a 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -346,6 +346,9 @@ nonEmpty = NonEmpty.nonEmpty . toList foldr1 :: (a -> a -> a) -> NonEmpty a -> a foldr1 = List.foldr1 +sconcatMapM :: (Semigroup c, Monad m) => (a -> m c) -> NonEmpty a -> m c +sconcatMapM f = fmap sconcat . mapM f + sconcatMap :: (Semigroup c) => (a -> c) -> NonEmpty a -> c sconcatMap f = sconcat . fmap f diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 3ea6ac2d34..6c03c4ecd5 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -265,6 +265,13 @@ tests = $(mkRelFile "Main.juvix") $ \case ErrWrongType {} -> Nothing + _ -> wrongError, + negTest + "Implicit name argument without name" + $(mkRelDir "Internal") + $(mkRelFile "issue3074.juvix") + $ \case + ErrUnsolvedMeta {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/Internal/issue3074.juvix b/tests/negative/Internal/issue3074.juvix new file mode 100644 index 0000000000..086aa083f3 --- /dev/null +++ b/tests/negative/Internal/issue3074.juvix @@ -0,0 +1,7 @@ +module issue3074; + +type T := mkT; + +fun {_ : T} : {A : Type} -> T := mkT; + +x : T := fun@{A := T};