From 31b1cfcd3d0db9caa68d373798734297e6ad6f90 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 20 Nov 2023 10:16:03 +0100 Subject: [PATCH 01/15] wip --- .../Concrete/Data/NameSignature/Builder.hs | 61 ++++++++++++++----- .../FromParsed/Analysis/Scoping.hs | 16 ++--- .../Internal/Translation/FromConcrete.hs | 40 ++++++++---- src/Juvix/Prelude/Base.hs | 3 + 4 files changed, 86 insertions(+), 34 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 092499f1ce..8a8da6f5f0 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -9,7 +9,6 @@ module Juvix.Compiler.Concrete.Data.NameSignature.Builder ) where -import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Extra (symbolParsed) import Juvix.Compiler.Concrete.Gen qualified as Gen @@ -46,14 +45,14 @@ instance (SingI s) => HasNameSignature s (FunctionDef s) where mapM_ addSigArg (a ^. signArgs) whenJust (a ^. signRetType) addExpressionType -instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where +instance (SingI s) => HasNameSignature s ([InductiveParameters s], ConstructorDef s) where addArgs :: forall r. (Members '[NameSignatureBuilder s] r) => - (InductiveDef s, ConstructorDef s) -> + ([InductiveParameters s], ConstructorDef s) -> Sem r () - addArgs (i, c) = do - mapM_ addConstructorParams (i ^. inductiveParameters) + addArgs (iparams, c) = do + mapM_ addConstructorParams iparams addRhs (c ^. constructorRhs) where addRecord :: RhsRecord s -> Sem r () @@ -63,6 +62,7 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) wher addField = \case RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType RecordStatementOperator {} -> return () + addRhs :: ConstructorRhs s -> Sem r () addRhs = \case ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType) @@ -231,13 +231,44 @@ addSymbol' impl mdef sym ty = do endBuild' :: forall s r a. Sem (Re s r) a endBuild' = get @(BuilderState s) >>= throw -mkRecordNameSignature :: forall s. (SingI s) => RhsRecord s -> RecordNameSignature s -mkRecordNameSignature rhs = - RecordNameSignature $ - HashMap.fromList - [ (symbolParsed _nameItemSymbol, NameItem {..}) - | (Indexed _nameItemIndex field) <- indexFrom 0 (toList (rhs ^.. rhsRecordStatements . each . _RecordStatementField)), - let _nameItemSymbol :: SymbolType s = field ^. fieldName - _nameItemType = field ^. fieldType - _nameItemDefault :: Maybe (ArgDefault s) = Nothing - ] +-- FIXME is this ever used??? +mkRecordNameSignature :: forall s. (SingI s) => [InductiveParameters s] -> RhsRecord s -> RecordNameSignature s +mkRecordNameSignature ps rhs = + undefined $ + RecordNameSignature $ + indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) + where + helper :: forall r. (r ~ '[State Int, Output (NameItem s)]) => Sem r () + helper = do + forM_ ps emitParameters + forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField + where + emitItem :: (Int -> NameItem s) -> Sem r () + emitItem mkitem = do + idx <- get + output (mkitem idx) + put (idx + 1) + + emitField :: RecordField s -> Sem r () + emitField field = emitItem $ \_nameItemIndex -> + NameItem + { _nameItemSymbol = field ^. fieldName, + _nameItemType = field ^. fieldType, + _nameItemDefault = Nothing, + _nameItemIndex + } + + emitParameters :: InductiveParameters s -> Sem r () + emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam + where + -- TODO implicitness!! + emitParam :: SymbolType s -> Sem r () + emitParam sym = error "nameblock" $ emitItem $ \_nameItemIndex -> + NameItem + { _nameItemSymbol = sym, + _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType), + _nameItemDefault = Nothing, + _nameItemIndex + } + where + defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index daf79539b9..b566d69495 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -315,7 +315,7 @@ reserveConstructorSymbol :: InductiveDef 'Parsed -> ConstructorDef 'Parsed -> Sem r S.Symbol -reserveConstructorSymbol d c = reserveSymbolSignatureOf SKNameConstructor (d, c) (c ^. constructorName) +reserveConstructorSymbol d c = reserveSymbolSignatureOf SKNameConstructor (d ^. inductiveParameters, c) (c ^. constructorName) reserveFunctionSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r) => @@ -903,7 +903,7 @@ checkInductiveDef InductiveDef {..} = do inductiveConstructors' <- nonEmpty' <$> sequence - [ checkConstructorDef inductiveName' cname cdef + [ checkConstructorDef inductiveName' inductiveParameters' cname cdef | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors) ] return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') @@ -923,12 +923,12 @@ checkInductiveDef InductiveDef {..} = do } registerDefaultArgs (inductiveName' ^. S.nameId) indDef forM_ inductiveConstructors' $ \c -> - registerDefaultArgs (c ^. constructorName . S.nameId) (indDef, c) + registerDefaultArgs (c ^. constructorName . S.nameId) (indDef ^. inductiveParameters, c) registerInductive @$> indDef where -- note that the constructor name is not bound here - checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) - checkConstructorDef tyName constructorName' ConstructorDef {..} = do + checkConstructorDef :: S.Symbol -> [InductiveParameters 'Scoped] -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) + checkConstructorDef tyName tyParams constructorName' ConstructorDef {..} = do doc' <- mapM checkJudoc _constructorDoc rhs' <- checkRhs _constructorRhs registerConstructor tyName @@ -954,7 +954,7 @@ checkInductiveDef InductiveDef {..} = do { _rhsRecordStatements = fields', _rhsRecordDelim } - modify' (set (scoperScopedConstructorFields . at (constructorName' ^. S.nameId)) (Just (mkRecordNameSignature rhs'))) + modify' (set (scoperScopedConstructorFields . at (constructorName' ^. S.nameId)) (Just (mkRecordNameSignature tyParams rhs'))) return rhs' where checkRecordStatements :: [RecordStatement 'Parsed] -> Sem r [RecordStatement 'Scoped] @@ -1262,7 +1262,7 @@ checkSections sec = do c' <- reserveConstructorSymbol d c let storeSig :: RecordNameSignature 'Parsed -> Sem r' () storeSig sig = modify' (set (scoperConstructorFields . at (c' ^. S.nameId)) (Just sig)) - whenJust (c ^? constructorRhs . _ConstructorRhsRecord) (storeSig . mkRecordNameSignature) + whenJust (c ^? constructorRhs . _ConstructorRhsRecord) (storeSig . mkRecordNameSignature (d ^. inductiveParameters)) return c' registerRecordType :: S.Symbol -> S.Symbol -> Sem (Fail ': r') () @@ -1276,7 +1276,7 @@ checkSections sec = do mkRec ^? constructorRhs . _ConstructorRhsRecord - . to mkRecordNameSignature + . to (mkRecordNameSignature (d ^. inductiveParameters)) let info = RecordInfo { _recordInfoSignature = fs, diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 6dcccdf5a1..1b0ffa19ac 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -18,6 +18,7 @@ import Juvix.Compiler.Builtins import Juvix.Compiler.Concrete.Data.Scope.Base (ScoperState, scoperScopedConstructorFields, scoperScopedSignatures) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S 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.Translation.FromParsed.Analysis.Scoping qualified as Scoper import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error @@ -774,7 +775,7 @@ goExpression = \case Just appargs -> do let name = napp ^. namedApplicationNewName . scopedIdenName sig <- fromJust <$> asks @NameSignatures (^. at (name ^. S.nameId)) - cls <- goArgs appargs + cls <- goArgs sig appargs let args :: [Internal.Name] = appargs ^.. each . namedArgumentNewFunDef . signName . to goSymbol -- changes the kind from Variable to Function updateKind :: Internal.Subs = @@ -784,7 +785,7 @@ goExpression = \case napp' = Concrete.NamedApplication { _namedAppName = napp ^. namedApplicationNewName, - _namedAppArgs = nonEmpty' $ createArgumentBlocks (sig ^. nameSignatureArgs) + _namedAppArgs = nonEmpty' (createArgumentBlocks (sig ^. nameSignatureArgs)) } e <- goNamedApplication napp' expr <- @@ -796,14 +797,31 @@ goExpression = \case } Internal.clone expr where - goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) - goArgs args = nonEmpty' . mkLetClauses <$> mapM goArg args + goArgs :: NameSignature 'Scoped -> NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) + goArgs sig args = nonEmpty' . mkLetClauses <$> mapM goArg args where goArg :: NamedArgumentNew 'Scoped -> Sem r Internal.PreLetStatement - goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentNewFunDef) + goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . addType . (^. namedArgumentNewFunDef) + + getTypeFromSig :: Symbol -> Expression + getTypeFromSig s = fromMaybe impossible (firstJust goBlock (sig ^. nameSignatureArgs)) + where + goBlock :: NameBlock 'Scoped -> Maybe Expression + goBlock b = b ^? nameBlock . at s . _Just . nameItemType + + -- NOTE Because of https://github.com/anoma/juvix/issues/2247, we + -- cannot put a hole in the type and rely on inference. + addType :: FunctionDef 'Scoped -> FunctionDef 'Scoped + addType d + | True = d + | otherwise = case d ^. signRetType of + Just {} -> d + Nothing -> case nonEmpty (d ^. signArgs) of + Just {} -> impossible + Nothing -> set signRetType (Just (getTypeFromSig (Concrete.symbolParsed (d ^. signName)))) d createArgumentBlocks :: [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped] - createArgumentBlocks sblocks = snd $ foldr goBlock (args0, []) sblocks + createArgumentBlocks = snd . foldr goBlock (args0, []) where args0 :: HashSet S.Symbol = HashSet.fromList $ fmap (^. namedArgumentNewFunDef . signName) (toList appargs) goBlock :: NameBlock 'Scoped -> (HashSet S.Symbol, [ArgumentBlock 'Scoped]) -> (HashSet S.Symbol, [ArgumentBlock 'Scoped]) @@ -813,11 +831,11 @@ goExpression = \case where namesInBlock = HashSet.intersection - (HashSet.fromList $ HashMap.keys _nameBlock) + (HashSet.fromList (HashMap.keys _nameBlock)) (HashSet.map (^. S.nameConcrete) args) - argNames = HashMap.fromList $ map (\n -> (n ^. S.nameConcrete, n)) $ toList args + argNames = HashMap.fromList . map (\n -> (n ^. S.nameConcrete, n)) $ toList args args' = HashSet.filter (not . flip HashSet.member namesInBlock . (^. S.nameConcrete)) args - _argBlockArgs = nonEmpty' $ map goArg (toList namesInBlock) + _argBlockArgs = nonEmpty' (map goArg (toList namesInBlock)) block' = ArgumentBlock { _argBlockDelims = Irrelevant Nothing, @@ -829,11 +847,11 @@ goExpression = \case NamedArgument { _namedArgName = sym, _namedArgAssignKw = Irrelevant dummyKw, - _namedArgValue = Concrete.ExpressionIdentifier $ ScopedIden name Nothing + _namedArgValue = Concrete.ExpressionIdentifier (ScopedIden name Nothing) } where name = over S.nameConcrete NameUnqualified $ fromJust $ HashMap.lookup sym argNames - dummyKw = KeywordRef (asciiKw ":=") dummyLoc Ascii + dummyKw = run (runReader dummyLoc (Gen.kw Gen.kwAssign)) dummyLoc = getLoc sym goDesugaredNamedApplication :: DesugaredNamedApplication -> Sem r Internal.Expression diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs index 1e302690a5..9ed64fcba7 100644 --- a/src/Juvix/Prelude/Base.hs +++ b/src/Juvix/Prelude/Base.hs @@ -553,3 +553,6 @@ uncurryF g input = uncurry g <$> input indexedByInt :: (Foldable f) => (a -> Int) -> f a -> IntMap a indexedByInt getIx l = IntMap.fromList [(getIx i, i) | i <- toList l] + +indexedByHash :: (Foldable f, Hashable k) => (a -> k) -> f a -> HashMap k a +indexedByHash getIx l = HashMap.fromList [(getIx i, i) | i <- toList l] From d2cc166139306c6479c6a17c5058b6965384c46c Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 21 Nov 2023 14:49:40 +0100 Subject: [PATCH 02/15] wip inline --- .../Compiler/Core/Translation/FromInternal.hs | 4 +- src/Juvix/Compiler/Internal/Extra.hs | 39 ++++++++++++ src/Juvix/Compiler/Internal/Extra/Base.hs | 12 ++-- src/Juvix/Compiler/Internal/Pretty/Base.hs | 3 +- .../Internal/Translation/FromConcrete.hs | 59 ++++++++++--------- .../Analysis/ArityChecking/Data/Types.hs | 3 +- .../Analysis/TypeChecking/CheckerNew.hs | 2 +- .../Analysis/TypeChecking/CheckerNew/Arity.hs | 3 +- tests/positive/Monads/StateT.juvix | 55 ++++++++--------- 9 files changed, 112 insertions(+), 68 deletions(-) diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 6ea58ab6de..21406dc78f 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -21,6 +21,7 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qu import Juvix.Data.Loc qualified as Loc import Juvix.Data.PPOutput import Juvix.Extra.Strings qualified as Str +import Juvix.Compiler.Internal.Pretty (ppTrace) type MVisit = Visit Internal.ModuleIndex @@ -856,7 +857,8 @@ goIden i = do ) case i of Internal.IdenVar n -> do - k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars) + let err = error ("impossible: var not found: " <> ppTrace n <> " at " <> prettyText (getLoc n)) + k <- HashMap.lookupDefault err id_ <$> asks (^. indexTableVars) varsNum <- asks (^. indexTableVarsNum) return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1)) Internal.IdenFunction n -> do diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index ba8416713f..2f5cd2754a 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -180,3 +180,42 @@ mkLetClauses pre = goSCC <$> (toList (buildLetMutualBlocks pre)) getFun :: PreLetStatement -> FunctionDef getFun = \case PreLetFunctionDef f -> f + +inlineLet :: forall r. (Members '[NameIdGen] r) => Let -> Sem r Expression +inlineLet l = do + (lclauses, subs) <- + runOutputList + . execState (mempty @Subs) + $ forM (l ^. letClauses) helper + body' <- substitutionE subs (l ^. letExpression) + return $ case nonEmpty lclauses of + Nothing -> body' + Just cl' -> + ExpressionLet + Let + { _letClauses = cl', + _letExpression = body' + } + where + helper :: forall r'. (r' ~ (State Subs ': Output LetClause ': r)) => LetClause -> Sem r' () + helper c = do + subs <- get + c' <- substitutionE subs c + case subsClause c' of + Nothing -> output c' + Just (n, b) -> modify' @Subs (set (at n) (Just b)) + + subsClause :: LetClause -> Maybe (Name, Expression) + subsClause = \case + LetMutualBlock {} -> Nothing + LetFunDef f -> mkAssoc f + where + mkAssoc :: FunctionDef -> Maybe (Name, Expression) + mkAssoc = \case + FunctionDef + { _funDefType = ExpressionHole {}, + _funDefBody = body, + _funDefName = name, + _funDefArgsInfo = [] + } -> Just (name, body) + _ -> Nothing diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index 69b3f35200..43508eaf08 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -305,13 +305,13 @@ substitutionE m = leafExpressions goLeaf where goLeaf :: Expression -> Sem r Expression goLeaf = \case - ExpressionIden i -> goIden i + ExpressionIden i -> goName (i ^. idenName) e -> return e - goIden :: Iden -> Sem r Expression - goIden i = case i of - IdenVar v - | Just e <- HashMap.lookup v m -> clone e - _ -> return $ ExpressionIden i + goName :: Name -> Sem r Expression + goName n = + case HashMap.lookup n m of + Just e -> clone e + Nothing -> return (toExpression n) smallUniverseE :: Interval -> Expression smallUniverseE = ExpressionUniverse . SmallUniverse diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 794ee6bf60..d157185df8 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -11,7 +11,8 @@ import Juvix.Compiler.Internal.Data.InstanceInfo (instanceInfoResult, instanceTa import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Data.NameDependencyInfo import Juvix.Compiler.Internal.Data.TypedHole -import Juvix.Compiler.Internal.Extra +import Juvix.Compiler.Internal.Extra.Base +import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty.Options import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types (Arity) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 1b0ffa19ac..f97b9cd5c9 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -775,7 +775,7 @@ goExpression = \case Just appargs -> do let name = napp ^. namedApplicationNewName . scopedIdenName sig <- fromJust <$> asks @NameSignatures (^. at (name ^. S.nameId)) - cls <- goArgs sig appargs + cls <- goArgs appargs let args :: [Internal.Name] = appargs ^.. each . namedArgumentNewFunDef . signName . to goSymbol -- changes the kind from Variable to Function updateKind :: Internal.Subs = @@ -788,37 +788,40 @@ goExpression = \case _namedAppArgs = nonEmpty' (createArgumentBlocks (sig ^. nameSignatureArgs)) } e <- goNamedApplication napp' + let l = + Internal.Let + { _letClauses = cls, + _letExpression = e + } expr <- - Internal.substitutionE updateKind - . Internal.ExpressionLet - $ Internal.Let - { _letClauses = cls, - _letExpression = e - } - Internal.clone expr + Internal.substitutionE updateKind l + -- >>= Internal.inlineLet + -- pure (Internal.ExpressionLet l) + Internal.clone (Internal.ExpressionLet expr) where - goArgs :: NameSignature 'Scoped -> NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) - goArgs sig args = nonEmpty' . mkLetClauses <$> mapM goArg args + goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) + goArgs args = nonEmpty' . mkLetClauses <$> mapM goArg args where goArg :: NamedArgumentNew 'Scoped -> Sem r Internal.PreLetStatement - goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . addType . (^. namedArgumentNewFunDef) - - getTypeFromSig :: Symbol -> Expression - getTypeFromSig s = fromMaybe impossible (firstJust goBlock (sig ^. nameSignatureArgs)) - where - goBlock :: NameBlock 'Scoped -> Maybe Expression - goBlock b = b ^? nameBlock . at s . _Just . nameItemType - - -- NOTE Because of https://github.com/anoma/juvix/issues/2247, we - -- cannot put a hole in the type and rely on inference. - addType :: FunctionDef 'Scoped -> FunctionDef 'Scoped - addType d - | True = d - | otherwise = case d ^. signRetType of - Just {} -> d - Nothing -> case nonEmpty (d ^. signArgs) of - Just {} -> impossible - Nothing -> set signRetType (Just (getTypeFromSig (Concrete.symbolParsed (d ^. signName)))) d + -- goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . addType . (^. namedArgumentNewFunDef) + goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentNewFunDef) + + -- getTypeFromSig :: Symbol -> Expression + -- getTypeFromSig s = fromMaybe impossible (firstJust goBlock (sig ^. nameSignatureArgs)) + -- where + -- goBlock :: NameBlock 'Scoped -> Maybe Expression + -- goBlock b = b ^? nameBlock . at s . _Just . nameItemType + + -- NOTE Because of https://github.com/anoma/juvix/issues/2247, we + -- cannot put a hole in the type and rely on inference. + -- addType :: FunctionDef 'Scoped -> FunctionDef 'Scoped + -- addType d + -- | True = d + -- | otherwise = case d ^. signRetType of + -- Just {} -> d + -- Nothing -> case nonEmpty (d ^. signArgs) of + -- Just {} -> impossible + -- Nothing -> set signRetType (Just (getTypeFromSig (Concrete.symbolParsed (d ^. signName)))) d createArgumentBlocks :: [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped] createArgumentBlocks = snd . foldr goBlock (args0, []) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs index 47661cef43..89a6c9809b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs @@ -1,6 +1,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types where -import Juvix.Compiler.Internal.Extra +import Juvix.Compiler.Internal.Extra.Base +import Juvix.Compiler.Internal.Language import Juvix.Prelude import Juvix.Prelude.Pretty diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index f696d9e950..ac27e2caa1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -1129,7 +1129,7 @@ holesHelper mhint expr = do where goImplArgs :: Int -> [ApplicationArg] -> Sem r [ApplicationArg] goImplArgs 0 as = return as - goImplArgs k ((ApplicationArg Implicit _) : as) = goImplArgs (k - 1) as + goImplArgs k (ApplicationArg Implicit _ : as) = goImplArgs (k - 1) as goImplArgs _ as = return as goArgs :: forall r'. (r' ~ State AppBuilder ': r) => Sem r' () diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs index 4c4cf557bc..11e5b50ae3 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs @@ -1,6 +1,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity where -import Juvix.Compiler.Internal.Extra +import Juvix.Compiler.Internal.Extra.Base +import Juvix.Compiler.Internal.Language import Juvix.Prelude import Juvix.Prelude.Pretty diff --git a/tests/positive/Monads/StateT.juvix b/tests/positive/Monads/StateT.juvix index f7d3c7c1f7..6b19625562 100644 --- a/tests/positive/Monads/StateT.juvix +++ b/tests/positive/Monads/StateT.juvix @@ -21,34 +21,31 @@ StateT-Functor {S : Type} {M : Type → Type} {{func : Functor λ {s := λ {(a, s') := f a, s'} MFunctor.<$> S→M⟨A×S⟩ s} }; -instance -StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} - : Monad (StateT S M) := - mkMonad@{ - functor := - StateT-Functor@{ - func := MMonad.functor - }; - return {A : Type} (a : A) : StateT S M A := - mkStateT λ {s := MMonad.return (a, s)}; - >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B) - : StateT S M B := - mkStateT - λ {s := - StateT.runStateT x s - MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}} - }; +-- instance +-- StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} +-- : Monad (StateT S M) := +-- mkMonad@{ +-- functor := +-- StateT-Functor@{ +-- func := MMonad.functor +-- }; +-- return {A : Type} (a : A) : StateT S M A := +-- mkStateT λ {s := MMonad.return (a, s)}; +-- >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B) +-- : StateT S M B := +-- mkStateT +-- λ {s := +-- StateT.runStateT x s +-- MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}} +-- }; -import MonadState open; -import Stdlib.Data.Unit open; +-- import MonadState open; +-- import Stdlib.Data.Unit open; -instance -StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} - : MonadState S (StateT S M) := - mkMonadState@{ - monad := StateT-Monad; - get : StateT S M S := - mkStateT λ {s := MMonad.return (s, s)}; - put (s : S) : StateT S M Unit := - mkStateT λ {_ := MMonad.return (unit, s)} - }; +-- instance +-- StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} : MonadState S (StateT S M) := +-- mkMonadState@{ +-- monad := StateT-Monad; +-- get : StateT S M S := mkStateT λ {s := MMonad.return (s, s)}; +-- put (s : S) : StateT S M Unit := mkStateT λ {_ := MMonad.return (unit, s)}; +-- }; From 956998c2a60aac6624320ad80ae1517c9309fb19 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 22 Nov 2023 10:41:40 +0100 Subject: [PATCH 03/15] clone generated projections --- src/Juvix/Compiler/Internal/Extra.hs | 7 ++++++- src/Juvix/Compiler/Internal/Extra/Clonable.hs | 3 ++- src/Juvix/Compiler/Internal/Language.hs | 2 +- src/Juvix/Compiler/Internal/Translation/FromConcrete.hs | 4 ++-- .../FromInternal/Analysis/TypeChecking/CheckerNew.hs | 3 +-- 5 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 2f5cd2754a..a0a6c01263 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -109,7 +109,7 @@ genFieldProjection _funDefName _funDefBuiltin info fieldIx = do saturatedTy = unnamedParameter' implicity (constructorReturnType info) inductiveArgs = map inductiveToFunctionParam inductiveParams retTy = constrArgs !! fieldIx - return + cloneFunctionDefSameName FunctionDef { _funDefExamples = [], _funDefTerminating = False, @@ -219,3 +219,8 @@ inlineLet l = do _funDefArgsInfo = [] } -> Just (name, body) _ -> Nothing + +cloneFunctionDefSameName :: Members '[NameIdGen] r => FunctionDef -> Sem r FunctionDef +cloneFunctionDefSameName f = do + f' <- clone f + return (set funDefName (f ^. funDefName) f') diff --git a/src/Juvix/Compiler/Internal/Extra/Clonable.hs b/src/Juvix/Compiler/Internal/Extra/Clonable.hs index 7de9c1abb3..e825ff71ec 100644 --- a/src/Juvix/Compiler/Internal/Extra/Clonable.hs +++ b/src/Juvix/Compiler/Internal/Extra/Clonable.hs @@ -234,6 +234,8 @@ instance Clonable ArgInfo where _argInfoName } +-- | Note that the name of the function is fresh. This is desirable when the +-- functionDef is part of a let. instance Clonable FunctionDef where freshNameIds :: (Members '[Reader FreshBindersContext, NameIdGen] r) => FunctionDef -> Sem r FunctionDef freshNameIds fun@FunctionDef {..} = do @@ -241,7 +243,6 @@ instance Clonable FunctionDef where underBinder fun $ \fun' -> do body' <- freshNameIds _funDefBody defaultSig' <- freshNameIds _funDefArgsInfo - return FunctionDef { _funDefName = fun' ^. funDefName, diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index bdc661b765..6f28e8d526 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -427,7 +427,7 @@ instance HasAtomicity ConstructorApp where instance HasAtomicity PatternArg where atomicity p - | Implicit <- p ^. patternArgIsImplicit = Atom + | isImplicitOrInstance (p ^. patternArgIsImplicit) = Atom | isJust (p ^. patternArgName) = Atom | otherwise = atomicity (p ^. patternArgPattern) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index f97b9cd5c9..b302f5123b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -795,9 +795,9 @@ goExpression = \case } expr <- Internal.substitutionE updateKind l - -- >>= Internal.inlineLet + >>= Internal.inlineLet -- pure (Internal.ExpressionLet l) - Internal.clone (Internal.ExpressionLet expr) + Internal.clone expr where goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) goArgs args = nonEmpty' . mkLetClauses <$> mapM goArg args diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index ac27e2caa1..023787bbeb 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -561,8 +561,7 @@ checkClause clauseLoc clauseType clausePats body = do ty' = foldFunType bodyParams' bodyRest wildcards <- mapM (genWildcard clauseLoc) pref' return (wildcards, ty') - | otherwise -> do - return ([], bodyTy) + | otherwise -> return ([], bodyTy) p : ps -> do bodyTy' <- weakNormalize bodyTy case bodyTy' of From 9843d81c66244ed652e63fd1f97514a37eaf97ff Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 22 Nov 2023 16:25:14 +0100 Subject: [PATCH 04/15] comment out named inductive parameters for constructors --- .../Concrete/Data/NameSignature/Builder.hs | 32 +++++++++---------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 8a8da6f5f0..1974360631 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -231,16 +231,14 @@ addSymbol' impl mdef sym ty = do endBuild' :: forall s r a. Sem (Re s r) a endBuild' = get @(BuilderState s) >>= throw --- FIXME is this ever used??? mkRecordNameSignature :: forall s. (SingI s) => [InductiveParameters s] -> RhsRecord s -> RecordNameSignature s mkRecordNameSignature ps rhs = - undefined $ RecordNameSignature $ indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) where helper :: forall r. (r ~ '[State Int, Output (NameItem s)]) => Sem r () helper = do - forM_ ps emitParameters + -- forM_ ps emitParameters forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField where emitItem :: (Int -> NameItem s) -> Sem r () @@ -258,17 +256,17 @@ mkRecordNameSignature ps rhs = _nameItemIndex } - emitParameters :: InductiveParameters s -> Sem r () - emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam - where - -- TODO implicitness!! - emitParam :: SymbolType s -> Sem r () - emitParam sym = error "nameblock" $ emitItem $ \_nameItemIndex -> - NameItem - { _nameItemSymbol = sym, - _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType), - _nameItemDefault = Nothing, - _nameItemIndex - } - where - defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression) + -- emitParameters :: InductiveParameters s -> Sem r () + -- emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam + -- where + -- -- FIXME implicitness!! + -- emitParam :: SymbolType s -> Sem r () + -- emitParam sym = emitItem $ \_nameItemIndex -> + -- NameItem + -- { _nameItemSymbol = sym, + -- _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType), + -- _nameItemDefault = Nothing, + -- _nameItemIndex + -- } + -- where + -- defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression) From 7a09e12b0811600df4bb59e822919b6704178dff Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 22 Nov 2023 17:42:06 +0100 Subject: [PATCH 05/15] add LocalVars info to guessArity --- .../Concrete/Data/NameSignature/Builder.hs | 32 +++++++++---------- .../Compiler/Core/Translation/FromInternal.hs | 2 +- src/Juvix/Compiler/Internal/Data/LocalVars.hs | 3 ++ src/Juvix/Compiler/Internal/Extra.hs | 2 +- .../Analysis/TypeChecking/CheckerNew.hs | 13 ++++---- 5 files changed, 28 insertions(+), 24 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 1974360631..1dbe1e8f04 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -233,8 +233,8 @@ endBuild' = get @(BuilderState s) >>= throw mkRecordNameSignature :: forall s. (SingI s) => [InductiveParameters s] -> RhsRecord s -> RecordNameSignature s mkRecordNameSignature ps rhs = - RecordNameSignature $ - indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) + RecordNameSignature $ + indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) where helper :: forall r. (r ~ '[State Int, Output (NameItem s)]) => Sem r () helper = do @@ -256,17 +256,17 @@ mkRecordNameSignature ps rhs = _nameItemIndex } - -- emitParameters :: InductiveParameters s -> Sem r () - -- emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam - -- where - -- -- FIXME implicitness!! - -- emitParam :: SymbolType s -> Sem r () - -- emitParam sym = emitItem $ \_nameItemIndex -> - -- NameItem - -- { _nameItemSymbol = sym, - -- _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType), - -- _nameItemDefault = Nothing, - -- _nameItemIndex - -- } - -- where - -- defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression) +-- emitParameters :: InductiveParameters s -> Sem r () +-- emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam +-- where +-- -- FIXME implicitness!! +-- emitParam :: SymbolType s -> Sem r () +-- emitParam sym = emitItem $ \_nameItemIndex -> +-- NameItem +-- { _nameItemSymbol = sym, +-- _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType), +-- _nameItemDefault = Nothing, +-- _nameItemIndex +-- } +-- where +-- defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression) diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 21406dc78f..2569f98ae0 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -15,13 +15,13 @@ import Juvix.Compiler.Core.Translation.FromInternal.Builtins.Nat import Juvix.Compiler.Core.Translation.FromInternal.Data import Juvix.Compiler.Internal.Data.Name import Juvix.Compiler.Internal.Extra qualified as Internal +import Juvix.Compiler.Internal.Pretty (ppTrace) import Juvix.Compiler.Internal.Pretty qualified as Internal import Juvix.Compiler.Internal.Translation.Extra qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped import Juvix.Data.Loc qualified as Loc import Juvix.Data.PPOutput import Juvix.Extra.Strings qualified as Str -import Juvix.Compiler.Internal.Pretty (ppTrace) type MVisit = Visit Internal.ModuleIndex diff --git a/src/Juvix/Compiler/Internal/Data/LocalVars.hs b/src/Juvix/Compiler/Internal/Data/LocalVars.hs index 7fc3b93aa3..24d3821f9a 100644 --- a/src/Juvix/Compiler/Internal/Data/LocalVars.hs +++ b/src/Juvix/Compiler/Internal/Data/LocalVars.hs @@ -43,3 +43,6 @@ addTypeMapping v v' = over localTyMap (HashMap.insert v v') withEmptyLocalVars :: Sem (Reader LocalVars ': r) a -> Sem r a withEmptyLocalVars = runReader emptyLocalVars + +withLocalVars :: LocalVars -> Sem (Reader LocalVars ': r) a -> Sem r a +withLocalVars = runReader diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index a0a6c01263..086ae64300 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -220,7 +220,7 @@ inlineLet l = do } -> Just (name, body) _ -> Nothing -cloneFunctionDefSameName :: Members '[NameIdGen] r => FunctionDef -> Sem r FunctionDef +cloneFunctionDefSameName :: (Members '[NameIdGen] r) => FunctionDef -> Sem r FunctionDef cloneFunctionDefSameName f = do f' <- clone f return (set funDefName (f ^. funDefName) f') diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 023787bbeb..7983813f61 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -548,7 +548,8 @@ checkClause clauseLoc clauseType clausePats body = do go pats bodyTy = case pats of [] -> do (bodyParams, bodyRest) <- unfoldFunType' bodyTy - guessedBodyParams <- unfoldArity <$> guessArity body + locals <- get + guessedBodyParams <- withLocalVars locals (unfoldArity <$> guessArity body) let pref' :: [IsImplicit] = map (^. paramImplicit) (take pref bodyParams) pref :: Int = aI - targetI preImplicits = length . takeWhile isImplicitOrInstance @@ -1431,7 +1432,7 @@ typeArity = weakNormalize >=> go guessArity :: forall r. - (Members '[Reader InfoTable, Inference] r) => + (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Expression -> Sem r Arity guessArity = \case @@ -1448,7 +1449,7 @@ guessArity = \case ExpressionCase l -> arityCase l where idenHelper :: Iden -> Sem r Arity - idenHelper = withEmptyLocalVars . idenArity + idenHelper = idenArity appHelper :: Application -> Sem r Arity appHelper a = do @@ -1483,7 +1484,7 @@ arityUniverse = ArityUnit simplelambda :: a simplelambda = error "simple lambda expressions are not supported by the arity checker" -arityLambda :: forall r. (Members '[Reader InfoTable, Inference] r) => Lambda -> Sem r Arity +arityLambda :: forall r. (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Lambda -> Sem r Arity arityLambda l = do aris <- mapM guessClauseArity (l ^. lambdaClauses) return $ @@ -1520,13 +1521,13 @@ guessPatternArgArity p = } } -arityLet :: (Members '[Reader InfoTable, Inference] r) => Let -> Sem r Arity +arityLet :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Let -> Sem r Arity arityLet l = guessArity (l ^. letExpression) -- | All branches should have the same arity. If they are all the same, we -- return that, otherwise we return ArityBlocking. Probably something better can -- be done. -arityCase :: (Members '[Reader InfoTable, Inference] r) => Case -> Sem r Arity +arityCase :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Case -> Sem r Arity arityCase c = do aris <- mapM (guessArity . (^. caseBranchExpression)) (c ^. caseBranches) return From 98564f80904640dd7d6e7868eebba54e139f59cd Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 22 Nov 2023 17:56:58 +0100 Subject: [PATCH 06/15] unused arg --- src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 1dbe1e8f04..d87739f645 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -232,7 +232,7 @@ endBuild' :: forall s r a. Sem (Re s r) a endBuild' = get @(BuilderState s) >>= throw mkRecordNameSignature :: forall s. (SingI s) => [InductiveParameters s] -> RhsRecord s -> RecordNameSignature s -mkRecordNameSignature ps rhs = +mkRecordNameSignature _ps rhs = RecordNameSignature $ indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) where From 9a2ef79b4dfe7ff81816e149caf410f9a7cefe2c Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 23 Nov 2023 11:13:29 +0100 Subject: [PATCH 07/15] clean test --- .../Concrete/Data/NameSignature/Builder.hs | 19 +----- tests/positive/Monads/Identity.juvix | 2 + tests/positive/Monads/Monad.juvix | 6 ++ tests/positive/Monads/MonadReader.juvix | 2 + tests/positive/Monads/MonadState.juvix | 6 ++ tests/positive/Monads/ReaderT.juvix | 22 +++++- tests/positive/Monads/StateT.juvix | 68 +++++++++++-------- 7 files changed, 76 insertions(+), 49 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index d87739f645..69f26284b3 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -237,9 +237,7 @@ mkRecordNameSignature _ps rhs = indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) where helper :: forall r. (r ~ '[State Int, Output (NameItem s)]) => Sem r () - helper = do - -- forM_ ps emitParameters - forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField + helper = forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField where emitItem :: (Int -> NameItem s) -> Sem r () emitItem mkitem = do @@ -255,18 +253,3 @@ mkRecordNameSignature _ps rhs = _nameItemDefault = Nothing, _nameItemIndex } - --- emitParameters :: InductiveParameters s -> Sem r () --- emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam --- where --- -- FIXME implicitness!! --- emitParam :: SymbolType s -> Sem r () --- emitParam sym = emitItem $ \_nameItemIndex -> --- NameItem --- { _nameItemSymbol = sym, --- _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType), --- _nameItemDefault = Nothing, --- _nameItemIndex --- } --- where --- defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression) diff --git a/tests/positive/Monads/Identity.juvix b/tests/positive/Monads/Identity.juvix index 7a4b6cb8b2..1d84c8fad2 100644 --- a/tests/positive/Monads/Identity.juvix +++ b/tests/positive/Monads/Identity.juvix @@ -5,6 +5,8 @@ import Functor open; type Identity (a : Type) := mkIdentity {runIdentity : a}; +open Identity public; + instance Identity-Functor : Functor Identity := mkFunctor@{ diff --git a/tests/positive/Monads/Monad.juvix b/tests/positive/Monads/Monad.juvix index 19c8c55ae5..81a4dfb960 100644 --- a/tests/positive/Monads/Monad.juvix +++ b/tests/positive/Monads/Monad.juvix @@ -13,3 +13,9 @@ type Monad (f : Type -> Type) := syntax operator >>= bind; >>= : {A B : Type} -> f A -> (A -> f B) -> f B }; + +open Monad public; + +syntax operator >> bind; +>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M + A) (y : M B) : M B := x >>= λ {_ := y}; diff --git a/tests/positive/Monads/MonadReader.juvix b/tests/positive/Monads/MonadReader.juvix index 6d0c93b600..8aeda8fd8d 100644 --- a/tests/positive/Monads/MonadReader.juvix +++ b/tests/positive/Monads/MonadReader.juvix @@ -10,3 +10,5 @@ type MonadReader (S : Type) (M : Type -> Type) := ask : M S; reader : {A : Type} → (S → A) → M A }; + +open MonadReader public; diff --git a/tests/positive/Monads/MonadState.juvix b/tests/positive/Monads/MonadState.juvix index 71caaf942c..fc9eb31de0 100644 --- a/tests/positive/Monads/MonadState.juvix +++ b/tests/positive/Monads/MonadState.juvix @@ -10,3 +10,9 @@ type MonadState (S : Type) (M : Type -> Type) := get : M S; put : S -> M Unit }; + +open MonadState public; + +modify {S : Type} {M : Type → Type} {{Monad M}} {{MonadState + S + M}} (f : S → S) : M Unit := get >>= λ {s := put (f s)}; diff --git a/tests/positive/Monads/ReaderT.juvix b/tests/positive/Monads/ReaderT.juvix index 2cb8e872d0..95d4d7d3dd 100644 --- a/tests/positive/Monads/ReaderT.juvix +++ b/tests/positive/Monads/ReaderT.juvix @@ -8,6 +8,10 @@ import Functor open using {module Functor as MFunctor}; type ReaderT (S : Type) (M : Type → Type) (A : Type) := mkReaderT {runReaderT : S → M A}; +runReader {S A : Type} {M : Type + → Type} (r : S) (m : ReaderT S M A) : M A := + ReaderT.runReaderT m r; + instance ReaderT-Functor {S : Type} {M : Type → Type} {{func : Functor M}} : Functor (ReaderT S M) := @@ -34,9 +38,7 @@ ReaderT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} >>= {A B : Type} (x : ReaderT S M A) (f : A → ReaderT S M B) : ReaderT S M B := mkReaderT - λ {s := - ReaderT.runReaderT x s - MMonad.>>= λ {a := ReaderT.runReaderT (f a) s}} + λ {s := runReader s x MMonad.>>= λ {a := runReader s (f a)}} }; import MonadReader open; @@ -55,6 +57,7 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}} import MonadState open; import StateT open; +import Identity open; import Stdlib.Data.Product open; liftReaderT {R A : Type} {M : Type → Type} (m : M A) @@ -65,6 +68,19 @@ liftStateT {S A : Type} {M : Type → Type} {{Monad M}} (m : M mkStateT λ {s := m MMonad.>>= λ {a := MMonad.return (a, s)}}; +import Stdlib.Data.Nat open; + +askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat := + ask; + +monadic : ReaderT Nat (StateT Nat Identity) Nat := + askNat + >>= λ {n := + liftReaderT (modify λ {m := m * n}) >> liftReaderT get}; + +main : Nat := + runIdentity (evalState 2 (runReader 5 monadic)); + -- FIXME fails instance termination -- instance -- StateT-MonadReader {R S : Type} {M : Type diff --git a/tests/positive/Monads/StateT.juvix b/tests/positive/Monads/StateT.juvix index 6b19625562..f804233f37 100644 --- a/tests/positive/Monads/StateT.juvix +++ b/tests/positive/Monads/StateT.juvix @@ -9,6 +9,15 @@ import Stdlib.Data.Product open; type StateT (S : Type) (M : Type → Type) (A : Type) := mkStateT {runStateT : S → M (A × S)}; +runState {S A : Type} {M : Type → Type} (s : S) (m : StateT + S + M + A) : M (A × S) := StateT.runStateT m s; + +evalState {S A : Type} {M : Type → Type} {{Functor + M}} (s : S) (m : StateT S M A) : M A := + fst Functor.<$> runState s m; + instance StateT-Functor {S : Type} {M : Type → Type} {{func : Functor M}} : Functor (StateT S M) := @@ -21,31 +30,34 @@ StateT-Functor {S : Type} {M : Type → Type} {{func : Functor λ {s := λ {(a, s') := f a, s'} MFunctor.<$> S→M⟨A×S⟩ s} }; --- instance --- StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} --- : Monad (StateT S M) := --- mkMonad@{ --- functor := --- StateT-Functor@{ --- func := MMonad.functor --- }; --- return {A : Type} (a : A) : StateT S M A := --- mkStateT λ {s := MMonad.return (a, s)}; --- >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B) --- : StateT S M B := --- mkStateT --- λ {s := --- StateT.runStateT x s --- MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}} --- }; - --- import MonadState open; --- import Stdlib.Data.Unit open; - --- instance --- StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} : MonadState S (StateT S M) := --- mkMonadState@{ --- monad := StateT-Monad; --- get : StateT S M S := mkStateT λ {s := MMonad.return (s, s)}; --- put (s : S) : StateT S M Unit := mkStateT λ {_ := MMonad.return (unit, s)}; --- }; +instance +StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} + : Monad (StateT S M) := + mkMonad@{ + functor := + StateT-Functor@{ + func := MMonad.functor + }; + return {A : Type} (a : A) : StateT S M A := + mkStateT λ {s := MMonad.return (a, s)}; + >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B) + : StateT S M B := + mkStateT + λ {s := + StateT.runStateT x s + MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}} + }; + +import MonadState open; +import Stdlib.Data.Unit open; + +instance +StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} + : MonadState S (StateT S M) := + mkMonadState@{ + monad := StateT-Monad; + get : StateT S M S := + mkStateT λ {s := MMonad.return (s, s)}; + put (s : S) : StateT S M Unit := + mkStateT λ {_ := MMonad.return (unit, s)} + }; From 21797d8c9a86ee8900a0ae5a61d719d881c93cee Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 23 Nov 2023 12:10:40 +0100 Subject: [PATCH 08/15] remove comments --- .../Internal/Translation/FromConcrete.hs | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index b302f5123b..826096ae86 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -796,33 +796,14 @@ goExpression = \case expr <- Internal.substitutionE updateKind l >>= Internal.inlineLet - -- pure (Internal.ExpressionLet l) Internal.clone expr where goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) goArgs args = nonEmpty' . mkLetClauses <$> mapM goArg args where goArg :: NamedArgumentNew 'Scoped -> Sem r Internal.PreLetStatement - -- goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . addType . (^. namedArgumentNewFunDef) goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentNewFunDef) - -- getTypeFromSig :: Symbol -> Expression - -- getTypeFromSig s = fromMaybe impossible (firstJust goBlock (sig ^. nameSignatureArgs)) - -- where - -- goBlock :: NameBlock 'Scoped -> Maybe Expression - -- goBlock b = b ^? nameBlock . at s . _Just . nameItemType - - -- NOTE Because of https://github.com/anoma/juvix/issues/2247, we - -- cannot put a hole in the type and rely on inference. - -- addType :: FunctionDef 'Scoped -> FunctionDef 'Scoped - -- addType d - -- | True = d - -- | otherwise = case d ^. signRetType of - -- Just {} -> d - -- Nothing -> case nonEmpty (d ^. signArgs) of - -- Just {} -> impossible - -- Nothing -> set signRetType (Just (getTypeFromSig (Concrete.symbolParsed (d ^. signName)))) d - createArgumentBlocks :: [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped] createArgumentBlocks = snd . foldr goBlock (args0, []) where From c50236c7c9127b3b8fb1f35c57021904a1ebabc2 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 23 Nov 2023 12:11:25 +0100 Subject: [PATCH 09/15] revert name signature changes --- .../Concrete/Data/NameSignature/Builder.hs | 40 +++++++------------ .../FromParsed/Analysis/Scoping.hs | 16 ++++---- 2 files changed, 22 insertions(+), 34 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 69f26284b3..092499f1ce 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -9,6 +9,7 @@ module Juvix.Compiler.Concrete.Data.NameSignature.Builder ) where +import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Extra (symbolParsed) import Juvix.Compiler.Concrete.Gen qualified as Gen @@ -45,14 +46,14 @@ instance (SingI s) => HasNameSignature s (FunctionDef s) where mapM_ addSigArg (a ^. signArgs) whenJust (a ^. signRetType) addExpressionType -instance (SingI s) => HasNameSignature s ([InductiveParameters s], ConstructorDef s) where +instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where addArgs :: forall r. (Members '[NameSignatureBuilder s] r) => - ([InductiveParameters s], ConstructorDef s) -> + (InductiveDef s, ConstructorDef s) -> Sem r () - addArgs (iparams, c) = do - mapM_ addConstructorParams iparams + addArgs (i, c) = do + mapM_ addConstructorParams (i ^. inductiveParameters) addRhs (c ^. constructorRhs) where addRecord :: RhsRecord s -> Sem r () @@ -62,7 +63,6 @@ instance (SingI s) => HasNameSignature s ([InductiveParameters s], ConstructorDe addField = \case RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType RecordStatementOperator {} -> return () - addRhs :: ConstructorRhs s -> Sem r () addRhs = \case ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType) @@ -231,25 +231,13 @@ addSymbol' impl mdef sym ty = do endBuild' :: forall s r a. Sem (Re s r) a endBuild' = get @(BuilderState s) >>= throw -mkRecordNameSignature :: forall s. (SingI s) => [InductiveParameters s] -> RhsRecord s -> RecordNameSignature s -mkRecordNameSignature _ps rhs = +mkRecordNameSignature :: forall s. (SingI s) => RhsRecord s -> RecordNameSignature s +mkRecordNameSignature rhs = RecordNameSignature $ - indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper))) - where - helper :: forall r. (r ~ '[State Int, Output (NameItem s)]) => Sem r () - helper = forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField - where - emitItem :: (Int -> NameItem s) -> Sem r () - emitItem mkitem = do - idx <- get - output (mkitem idx) - put (idx + 1) - - emitField :: RecordField s -> Sem r () - emitField field = emitItem $ \_nameItemIndex -> - NameItem - { _nameItemSymbol = field ^. fieldName, - _nameItemType = field ^. fieldType, - _nameItemDefault = Nothing, - _nameItemIndex - } + HashMap.fromList + [ (symbolParsed _nameItemSymbol, NameItem {..}) + | (Indexed _nameItemIndex field) <- indexFrom 0 (toList (rhs ^.. rhsRecordStatements . each . _RecordStatementField)), + let _nameItemSymbol :: SymbolType s = field ^. fieldName + _nameItemType = field ^. fieldType + _nameItemDefault :: Maybe (ArgDefault s) = Nothing + ] diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index b566d69495..daf79539b9 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -315,7 +315,7 @@ reserveConstructorSymbol :: InductiveDef 'Parsed -> ConstructorDef 'Parsed -> Sem r S.Symbol -reserveConstructorSymbol d c = reserveSymbolSignatureOf SKNameConstructor (d ^. inductiveParameters, c) (c ^. constructorName) +reserveConstructorSymbol d c = reserveSymbolSignatureOf SKNameConstructor (d, c) (c ^. constructorName) reserveFunctionSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r) => @@ -903,7 +903,7 @@ checkInductiveDef InductiveDef {..} = do inductiveConstructors' <- nonEmpty' <$> sequence - [ checkConstructorDef inductiveName' inductiveParameters' cname cdef + [ checkConstructorDef inductiveName' cname cdef | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors) ] return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') @@ -923,12 +923,12 @@ checkInductiveDef InductiveDef {..} = do } registerDefaultArgs (inductiveName' ^. S.nameId) indDef forM_ inductiveConstructors' $ \c -> - registerDefaultArgs (c ^. constructorName . S.nameId) (indDef ^. inductiveParameters, c) + registerDefaultArgs (c ^. constructorName . S.nameId) (indDef, c) registerInductive @$> indDef where -- note that the constructor name is not bound here - checkConstructorDef :: S.Symbol -> [InductiveParameters 'Scoped] -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) - checkConstructorDef tyName tyParams constructorName' ConstructorDef {..} = do + checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) + checkConstructorDef tyName constructorName' ConstructorDef {..} = do doc' <- mapM checkJudoc _constructorDoc rhs' <- checkRhs _constructorRhs registerConstructor tyName @@ -954,7 +954,7 @@ checkInductiveDef InductiveDef {..} = do { _rhsRecordStatements = fields', _rhsRecordDelim } - modify' (set (scoperScopedConstructorFields . at (constructorName' ^. S.nameId)) (Just (mkRecordNameSignature tyParams rhs'))) + modify' (set (scoperScopedConstructorFields . at (constructorName' ^. S.nameId)) (Just (mkRecordNameSignature rhs'))) return rhs' where checkRecordStatements :: [RecordStatement 'Parsed] -> Sem r [RecordStatement 'Scoped] @@ -1262,7 +1262,7 @@ checkSections sec = do c' <- reserveConstructorSymbol d c let storeSig :: RecordNameSignature 'Parsed -> Sem r' () storeSig sig = modify' (set (scoperConstructorFields . at (c' ^. S.nameId)) (Just sig)) - whenJust (c ^? constructorRhs . _ConstructorRhsRecord) (storeSig . mkRecordNameSignature (d ^. inductiveParameters)) + whenJust (c ^? constructorRhs . _ConstructorRhsRecord) (storeSig . mkRecordNameSignature) return c' registerRecordType :: S.Symbol -> S.Symbol -> Sem (Fail ': r') () @@ -1276,7 +1276,7 @@ checkSections sec = do mkRec ^? constructorRhs . _ConstructorRhsRecord - . to (mkRecordNameSignature (d ^. inductiveParameters)) + . to mkRecordNameSignature let info = RecordInfo { _recordInfoSignature = fs, From f49be1845e4e4fc91ea5a251937647f995fd86b7 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 23 Nov 2023 17:28:22 +0100 Subject: [PATCH 10/15] tests --- .../Analysis/TypeChecking/Checker.hs | 2 +- test/Compilation.hs | 3 +- test/Compilation/Base.hs | 15 ++++- test/Compilation/Positive.hs | 2 +- test/Compilation/PositiveNew.hs | 55 +++++++++++++++++++ tests/Compilation/positive/out/test072.out | 1 + .../positive/test072}/Functor.juvix | 0 .../positive/test072}/Identity.juvix | 0 .../positive/test072}/Monad.juvix | 0 .../positive/test072}/MonadReader.juvix | 0 .../positive/test072}/MonadState.juvix | 0 .../positive/test072}/Package.juvix | 0 .../positive/test072}/Reader.juvix | 0 .../positive/test072}/ReaderT.juvix | 0 .../positive/test072}/State.juvix | 0 .../positive/test072}/StateT.juvix | 0 16 files changed, 73 insertions(+), 5 deletions(-) create mode 100644 test/Compilation/PositiveNew.hs create mode 100644 tests/Compilation/positive/out/test072.out rename tests/{positive/Monads => Compilation/positive/test072}/Functor.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/Identity.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/Monad.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/MonadReader.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/MonadState.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/Package.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/Reader.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/ReaderT.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/State.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/StateT.juvix (100%) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index 1185a65f50..45f866271a 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -559,7 +559,7 @@ checkPattern = go go :: FunctionParameter -> PatternArg -> Sem r PatternArg go argTy patArg = do matchIsImplicit (argTy ^. paramImplicit) patArg - tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get + tyVarMap <- localsToSubsE <$> get ty <- substitutionE tyVarMap (argTy ^. paramType) let pat = patArg ^. patternArgPattern name = patArg ^. patternArgName diff --git a/test/Compilation.hs b/test/Compilation.hs index 0d8e28fd82..0da457bc1c 100644 --- a/test/Compilation.hs +++ b/test/Compilation.hs @@ -3,6 +3,7 @@ module Compilation where import Base import Compilation.Negative qualified as N import Compilation.Positive qualified as P +import Compilation.PositiveNew qualified as New allTests :: TestTree -allTests = testGroup "Juvix compilation pipeline tests" [P.allTestsNoOptimize, P.allTests, N.allTests] +allTests = testGroup "Juvix compilation pipeline tests" [New.allTestsNoOptimize, P.allTestsNoOptimize, P.allTests, N.allTests] diff --git a/test/Compilation/Base.hs b/test/Compilation/Base.hs index 60cc0215dd..3e1ebdf133 100644 --- a/test/Compilation/Base.hs +++ b/test/Compilation/Base.hs @@ -21,9 +21,20 @@ compileAssertion :: Path Abs File -> (String -> IO ()) -> Assertion -compileAssertion root' optLevel mode mainFile expectedFile step = do +compileAssertion = compileAssertionEntry id + +compileAssertionEntry :: + (EntryPoint -> EntryPoint) -> + Path Abs Dir -> + Int -> + CompileAssertionMode -> + Path Abs File -> + Path Abs File -> + (String -> IO ()) -> + Assertion +compileAssertionEntry adjustEntry root' optLevel mode mainFile expectedFile step = do step "Translate to JuvixCore" - entryPoint <- defaultEntryPointIO' LockModeExclusive root' mainFile + entryPoint <- adjustEntry <$> defaultEntryPointIO' LockModeExclusive root' mainFile tab <- (^. Core.coreResultTable) . snd <$> runIOExclusive entryPoint upToCore case run $ runReader Core.defaultCoreOptions $ runError $ Core.toEval' tab of Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err))) diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 87b5d0ebc7..2e599b804c 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -414,7 +414,7 @@ tests = $(mkRelFile "test070.juvix") $(mkRelFile "out/test070.out"), posTest - "Test071: Named application" + "Test071: Named application (Ord instance with default cmp)" $(mkRelDir ".") $(mkRelFile "test071.juvix") $(mkRelFile "out/test071.out") diff --git a/test/Compilation/PositiveNew.hs b/test/Compilation/PositiveNew.hs new file mode 100644 index 0000000000..8352dfcaa5 --- /dev/null +++ b/test/Compilation/PositiveNew.hs @@ -0,0 +1,55 @@ +module Compilation.PositiveNew where + +import Base +import Compilation.Base +import Compilation.Positive qualified as Old +import Data.HashSet qualified as HashSet + +root :: Path Abs Dir +root = relToProject $(mkRelDir "tests/positive") + +posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Old.PosTest +posTest = posTest' EvalAndCompile + +posTest' :: CompileAssertionMode -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Old.PosTest +posTest' _assertionMode _name rdir rfile routfile = + let _dir = root rdir + _file = _dir rfile + _expectedFile = root routfile + in Old.PosTest {..} + +testDescr :: Int -> Old.PosTest -> TestDescr +testDescr optLevel Old.PosTest {..} = + TestDescr + { _testName = _name, + _testRoot = _dir, + _testAssertion = + Steps $ + let f = set entryPointNewTypeCheckingAlgorithm True + in compileAssertionEntry f _dir optLevel _assertionMode _file _expectedFile + } + +allTestsNoOptimize :: TestTree +allTestsNoOptimize = + testGroup + "New typechecker compilation positive tests (no optimization)" + (map (mkTest . testDescr 0) (filter (not . isIgnored) (extraTests <> Old.tests))) + +isIgnored :: Old.PosTest -> Bool +isIgnored t = HashSet.member (t ^. Old.name) ignored + +extraTests :: [Old.PosTest] +extraTests = + [ Old.posTest + "Test073: Monad transformers (ReaderT + StateT + Identity)" + $(mkRelDir "test072") + $(mkRelFile "ReaderT.juvix") + $(mkRelFile "out/test072.out") + ] + +ignored :: HashSet String +ignored = + HashSet.fromList + ["Test070: Nested default values and named arguments", + "Test071: Named application (Ord instance with default cmp)" + ] diff --git a/tests/Compilation/positive/out/test072.out b/tests/Compilation/positive/out/test072.out new file mode 100644 index 0000000000..f599e28b8a --- /dev/null +++ b/tests/Compilation/positive/out/test072.out @@ -0,0 +1 @@ +10 diff --git a/tests/positive/Monads/Functor.juvix b/tests/Compilation/positive/test072/Functor.juvix similarity index 100% rename from tests/positive/Monads/Functor.juvix rename to tests/Compilation/positive/test072/Functor.juvix diff --git a/tests/positive/Monads/Identity.juvix b/tests/Compilation/positive/test072/Identity.juvix similarity index 100% rename from tests/positive/Monads/Identity.juvix rename to tests/Compilation/positive/test072/Identity.juvix diff --git a/tests/positive/Monads/Monad.juvix b/tests/Compilation/positive/test072/Monad.juvix similarity index 100% rename from tests/positive/Monads/Monad.juvix rename to tests/Compilation/positive/test072/Monad.juvix diff --git a/tests/positive/Monads/MonadReader.juvix b/tests/Compilation/positive/test072/MonadReader.juvix similarity index 100% rename from tests/positive/Monads/MonadReader.juvix rename to tests/Compilation/positive/test072/MonadReader.juvix diff --git a/tests/positive/Monads/MonadState.juvix b/tests/Compilation/positive/test072/MonadState.juvix similarity index 100% rename from tests/positive/Monads/MonadState.juvix rename to tests/Compilation/positive/test072/MonadState.juvix diff --git a/tests/positive/Monads/Package.juvix b/tests/Compilation/positive/test072/Package.juvix similarity index 100% rename from tests/positive/Monads/Package.juvix rename to tests/Compilation/positive/test072/Package.juvix diff --git a/tests/positive/Monads/Reader.juvix b/tests/Compilation/positive/test072/Reader.juvix similarity index 100% rename from tests/positive/Monads/Reader.juvix rename to tests/Compilation/positive/test072/Reader.juvix diff --git a/tests/positive/Monads/ReaderT.juvix b/tests/Compilation/positive/test072/ReaderT.juvix similarity index 100% rename from tests/positive/Monads/ReaderT.juvix rename to tests/Compilation/positive/test072/ReaderT.juvix diff --git a/tests/positive/Monads/State.juvix b/tests/Compilation/positive/test072/State.juvix similarity index 100% rename from tests/positive/Monads/State.juvix rename to tests/Compilation/positive/test072/State.juvix diff --git a/tests/positive/Monads/StateT.juvix b/tests/Compilation/positive/test072/StateT.juvix similarity index 100% rename from tests/positive/Monads/StateT.juvix rename to tests/Compilation/positive/test072/StateT.juvix From b857aa8ce94457cdf2690c246006c0a25d0e0983 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 23 Nov 2023 20:53:27 +0100 Subject: [PATCH 11/15] fix wildcard generation for named arguments --- .../Analysis/TypeChecking/CheckerNew.hs | 45 ++++++++++++------- test/Compilation/PositiveNew.hs | 8 ++-- 2 files changed, 32 insertions(+), 21 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 7983813f61..e0d3f7ad24 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -544,13 +544,24 @@ checkClause clauseLoc clauseType clausePats body = do helper :: [PatternArg] -> Expression -> Sem r (LocalVars, ([PatternArg], Expression)) helper pats ty = runState emptyLocalVars (go pats ty) + genPatternWildcard :: Interval -> FunctionParameter -> Sem (State LocalVars ': r) PatternArg + genPatternWildcard loc par = do + let impl = par ^. paramImplicit + var <- maybe (varFromWildcard (Wildcard loc)) return (par ^. paramName) + return + PatternArg + { _patternArgIsImplicit = impl, + _patternArgName = Nothing, + _patternArgPattern = PatternVariable var + } + go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) ([PatternArg], Expression) go pats bodyTy = case pats of [] -> do (bodyParams, bodyRest) <- unfoldFunType' bodyTy locals <- get guessedBodyParams <- withLocalVars locals (unfoldArity <$> guessArity body) - let pref' :: [IsImplicit] = map (^. paramImplicit) (take pref bodyParams) + let pref' :: [FunctionParameter] = take pref bodyParams pref :: Int = aI - targetI preImplicits = length . takeWhile isImplicitOrInstance aI :: Int = preImplicits (map (^. paramImplicit) bodyParams) @@ -560,7 +571,7 @@ checkClause clauseLoc clauseType clausePats body = do let n = length pref' bodyParams' = drop n bodyParams ty' = foldFunType bodyParams' bodyRest - wildcards <- mapM (genWildcard clauseLoc) pref' + wildcards <- mapM (genPatternWildcard clauseLoc) pref' return (wildcards, ty') | otherwise -> return ([], bodyTy) p : ps -> do @@ -581,9 +592,9 @@ checkClause clauseLoc clauseType clausePats body = do loc :: Interval loc = getLoc par - insertWildcard :: IsImplicit -> Sem (State LocalVars ': r) ([PatternArg], Expression) - insertWildcard impl = do - w <- genWildcard loc impl + insertWildcard :: Sem (State LocalVars ': r) ([PatternArg], Expression) + insertWildcard = do + w <- genPatternWildcard loc par go (w : p : ps) bodyTy' case (p ^. patternArgIsImplicit, par ^. paramImplicit) of @@ -592,10 +603,10 @@ checkClause clauseLoc clauseType clausePats body = do (ImplicitInstance, ImplicitInstance) -> checkPatternAndContinue (Implicit, Explicit) -> throwWrongIsImplicit p Implicit (ImplicitInstance, Explicit) -> throwWrongIsImplicit p ImplicitInstance - (Explicit, Implicit) -> insertWildcard Implicit - (ImplicitInstance, Implicit) -> insertWildcard Implicit - (Explicit, ImplicitInstance) -> insertWildcard ImplicitInstance - (Implicit, ImplicitInstance) -> insertWildcard ImplicitInstance + (Explicit, Implicit) -> insertWildcard + (ImplicitInstance, Implicit) -> insertWildcard + (Explicit, ImplicitInstance) -> insertWildcard + (Implicit, ImplicitInstance) -> insertWildcard where throwWrongIsImplicit :: (Members '[Error TypeCheckerError] r') => PatternArg -> IsImplicit -> Sem r' a throwWrongIsImplicit patArg expected = @@ -647,6 +658,12 @@ matchIsImplicit expected actual = _wrongPatternIsImplicitActual = actual } +addPatternVar :: (Members '[State LocalVars, Inference] r) => VarName -> Expression -> Maybe Name -> Sem r () +addPatternVar v ty argName = do + modify (addType v ty) + registerIdenType v ty + whenJust argName (\v' -> modify (addTypeMapping v' v)) + checkPattern :: forall r. (Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, State FunctionsTable] r) => @@ -662,9 +679,9 @@ checkPattern = go ty <- substitutionE tyVarMap (argTy ^. paramType) let pat = patArg ^. patternArgPattern name = patArg ^. patternArgName - whenJust name (\n -> addVar n ty argTy) + whenJust name (\n -> addPatternVar n ty (argTy ^. paramName)) pat' <- case pat of - PatternVariable v -> addVar v ty argTy $> pat + PatternVariable v -> addPatternVar v ty (argTy ^. paramName) $> pat PatternWildcardConstructor {} -> impossible PatternConstructorApp a -> goPatternConstructor pat ty a return (set patternArgPattern pat' patArg) @@ -714,12 +731,6 @@ checkPattern = go ) PatternConstructorApp <$> goConstr (IdenInductive ind) a tyArgs - addVar :: VarName -> Expression -> FunctionParameter -> Sem r () - addVar v ty argType = do - modify (addType v ty) - registerIdenType v ty - whenJust (argType ^. paramName) (\v' -> modify (addTypeMapping v' v)) - goConstr :: Iden -> ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ConstructorApp goConstr inductivename app@(ConstructorApp c ps _) ctx = do (_, psTys) <- constructorArgTypes <$> lookupConstructor c diff --git a/test/Compilation/PositiveNew.hs b/test/Compilation/PositiveNew.hs index 8352dfcaa5..d145efc672 100644 --- a/test/Compilation/PositiveNew.hs +++ b/test/Compilation/PositiveNew.hs @@ -25,8 +25,8 @@ testDescr optLevel Old.PosTest {..} = _testRoot = _dir, _testAssertion = Steps $ - let f = set entryPointNewTypeCheckingAlgorithm True - in compileAssertionEntry f _dir optLevel _assertionMode _file _expectedFile + let f = set entryPointNewTypeCheckingAlgorithm True + in compileAssertionEntry f _dir optLevel _assertionMode _file _expectedFile } allTestsNoOptimize :: TestTree @@ -50,6 +50,6 @@ extraTests = ignored :: HashSet String ignored = HashSet.fromList - ["Test070: Nested default values and named arguments", - "Test071: Named application (Ord instance with default cmp)" + [ "Test070: Nested default values and named arguments", + "Test071: Named application (Ord instance with default cmp)" ] From a3b84fe5f8955da1bc7e47c58da6000c8f8e71e9 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 23 Nov 2023 22:08:51 +0100 Subject: [PATCH 12/15] register type of wildcard --- .../FromInternal/Analysis/TypeChecking/CheckerNew.hs | 1 + test/Compilation/PositiveNew.hs | 3 ++- tests/Compilation/positive/test027.juvix | 1 - tests/Compilation/positive/test046.juvix | 1 - 4 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index e0d3f7ad24..355994a8e8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -548,6 +548,7 @@ checkClause clauseLoc clauseType clausePats body = do genPatternWildcard loc par = do let impl = par ^. paramImplicit var <- maybe (varFromWildcard (Wildcard loc)) return (par ^. paramName) + addPatternVar var (par ^. paramType) Nothing return PatternArg { _patternArgIsImplicit = impl, diff --git a/test/Compilation/PositiveNew.hs b/test/Compilation/PositiveNew.hs index d145efc672..84c906b96a 100644 --- a/test/Compilation/PositiveNew.hs +++ b/test/Compilation/PositiveNew.hs @@ -51,5 +51,6 @@ ignored :: HashSet String ignored = HashSet.fromList [ "Test070: Nested default values and named arguments", - "Test071: Named application (Ord instance with default cmp)" + "Test071: Named application (Ord instance with default cmp)", + "Test046: Polymorphic type arguments" ] diff --git a/tests/Compilation/positive/test027.juvix b/tests/Compilation/positive/test027.juvix index 189a20de16..e5bda901db 100644 --- a/tests/Compilation/positive/test027.juvix +++ b/tests/Compilation/positive/test027.juvix @@ -31,4 +31,3 @@ main : IO := printNatLn (toNat (num 7)) >> printNatLn (toNat (add (num 7) (num 3))) >> printNatLn (toNat (mul (num 7) (num 3))); - diff --git a/tests/Compilation/positive/test046.juvix b/tests/Compilation/positive/test046.juvix index b2edd3ca27..839b3573ec 100644 --- a/tests/Compilation/positive/test046.juvix +++ b/tests/Compilation/positive/test046.juvix @@ -11,4 +11,3 @@ id' : Ty fun : {A : Type} → A → Ty := id λ {_ := id'}; main : Nat := fun 5 {Nat} 7; - From 17ccffa09586a9fdab42d82b8c2846a21e103dff Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 10:25:56 +0100 Subject: [PATCH 13/15] ignore church numerals test --- test/Compilation/PositiveNew.hs | 4 +++- tests/Compilation/positive/test032.juvix | 1 - 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/test/Compilation/PositiveNew.hs b/test/Compilation/PositiveNew.hs index 84c906b96a..6d7d00cfb6 100644 --- a/test/Compilation/PositiveNew.hs +++ b/test/Compilation/PositiveNew.hs @@ -52,5 +52,7 @@ ignored = HashSet.fromList [ "Test070: Nested default values and named arguments", "Test071: Named application (Ord instance with default cmp)", - "Test046: Polymorphic type arguments" + "Test046: Polymorphic type arguments", + -- TODO allow lambda branches of different number of patterns + "Test027: Church numerals" ] diff --git a/tests/Compilation/positive/test032.juvix b/tests/Compilation/positive/test032.juvix index 775f0a8ecd..ade2b960b5 100644 --- a/tests/Compilation/positive/test032.juvix +++ b/tests/Compilation/positive/test032.juvix @@ -56,4 +56,3 @@ main : IO := (take 10 (uniq (sort (flatten (gen2 nil 9 80))))) >> printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 80))))); - From c81ddf9c6b121daaa170d53e7b159c58ee332ebe Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 10:33:41 +0100 Subject: [PATCH 14/15] remove extra tests --- test/Typecheck/PositiveNew.hs | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/test/Typecheck/PositiveNew.hs b/test/Typecheck/PositiveNew.hs index a2ae510b22..83493a0ce9 100644 --- a/test/Typecheck/PositiveNew.hs +++ b/test/Typecheck/PositiveNew.hs @@ -37,20 +37,7 @@ isIgnored :: Old.PosTest -> Bool isIgnored t = HashSet.member (t ^. Old.name) ignored extraTests :: [Old.PosTest] -extraTests = - [ Old.posTest - "Monad transformers (State)" - $(mkRelDir "Monads") - $(mkRelFile "State.juvix"), - Old.posTest - "Monad transformers (Reader)" - $(mkRelDir "Monads") - $(mkRelFile "Reader.juvix"), - Old.posTest - "Monad transformers (ReaderT)" - $(mkRelDir "Monads") - $(mkRelFile "ReaderT.juvix") - ] +extraTests = [] -- | Default values are not supported by the new type checker at the moment ignored :: HashSet String From 9f4b30ba70c0257c4a5b559f8adef45cdca5d71b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 24 Nov 2023 10:58:45 +0100 Subject: [PATCH 15/15] fix ignore list --- test/Typecheck/PositiveNew.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Typecheck/PositiveNew.hs b/test/Typecheck/PositiveNew.hs index 83493a0ce9..0577942e61 100644 --- a/test/Typecheck/PositiveNew.hs +++ b/test/Typecheck/PositiveNew.hs @@ -44,7 +44,7 @@ ignored :: HashSet String ignored = HashSet.fromList [ "Test070: Nested default values and named arguments", - "Test071: Named application", + "Test071: Named application (Ord instance with default cmp)", -- This test does not pass with the new hole insertion algorithm "Test046: Polymorphic type arguments" ]