From d6c1a74cec2acf3594f0bbc248f560b8e2435d47 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 28 Nov 2023 16:43:14 +0100 Subject: [PATCH] Improve inference for `--new-typechecker` (#2524) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This pr applies a number of fixes to the new typechecker. The fixes implemented are: 1. When guessing the arity of the body, we properly use the type information of the variables in the patterns. 2. When generating wildcards, we name them properly so that they align with the name in the type signature. 3. When compiling named applications, we inline all clauses of the form `fun : _ := body`. This is a workaround to https://github.com/anoma/juvix/issues/2247 and https://github.com/anoma/juvix/issues/2517 4. I've had to ignore test027 (Church numerals). While the typechecker passes and one can see that the types are correct, there is a lambda where its clauses have different number of patterns. Our goal is to support that in the near future (https://github.com/anoma/juvix/issues/1706). This is the conflicting lambda: ``` mutual num : Nat → Num := λ : Nat → Num {| (zero : Nat) := czero | ((suc n : Nat)) {A} := csuc (num n) {A}} ``` 5. I've added non-trivial a compilation test involving monad transformers. --- .../Compiler/Core/Translation/FromInternal.hs | 4 +- src/Juvix/Compiler/Internal/Data/LocalVars.hs | 3 + src/Juvix/Compiler/Internal/Extra.hs | 46 ++++++++++++- src/Juvix/Compiler/Internal/Extra/Base.hs | 12 ++-- src/Juvix/Compiler/Internal/Extra/Clonable.hs | 3 +- src/Juvix/Compiler/Internal/Language.hs | 2 +- src/Juvix/Compiler/Internal/Pretty/Base.hs | 3 +- .../Internal/Translation/FromConcrete.hs | 28 ++++---- .../Analysis/ArityChecking/Data/Types.hs | 3 +- .../Analysis/TypeChecking/Checker.hs | 2 +- .../Analysis/TypeChecking/CheckerNew.hs | 64 +++++++++++-------- .../Analysis/TypeChecking/CheckerNew/Arity.hs | 3 +- src/Juvix/Prelude/Base.hs | 3 + test/Compilation.hs | 3 +- test/Compilation/Base.hs | 15 ++++- test/Compilation/Positive.hs | 2 +- test/Compilation/PositiveNew.hs | 58 +++++++++++++++++ test/Typecheck/PositiveNew.hs | 17 +---- tests/Compilation/positive/out/test072.out | 1 + tests/Compilation/positive/test027.juvix | 1 - tests/Compilation/positive/test032.juvix | 1 - tests/Compilation/positive/test046.juvix | 1 - .../positive/test072}/Functor.juvix | 0 .../positive/test072}/Identity.juvix | 2 + .../positive/test072}/Monad.juvix | 6 ++ .../positive/test072}/MonadReader.juvix | 2 + .../positive/test072}/MonadState.juvix | 6 ++ .../positive/test072}/Package.juvix | 0 .../positive/test072}/Reader.juvix | 0 .../positive/test072}/ReaderT.juvix | 22 ++++++- .../positive/test072}/State.juvix | 0 .../positive/test072}/StateT.juvix | 9 +++ 32 files changed, 244 insertions(+), 78 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 (95%) rename tests/{positive/Monads => Compilation/positive/test072}/Monad.juvix (68%) rename tests/{positive/Monads => Compilation/positive/test072}/MonadReader.juvix (89%) rename tests/{positive/Monads => Compilation/positive/test072}/MonadState.juvix (57%) 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 (81%) rename tests/{positive/Monads => Compilation/positive/test072}/State.juvix (100%) rename tests/{positive/Monads => Compilation/positive/test072}/StateT.juvix (86%) diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 6ea58ab6de..2569f98ae0 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -15,6 +15,7 @@ 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 @@ -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/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 ba8416713f..086ae64300 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, @@ -180,3 +180,47 @@ 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 + +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/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/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/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 6dcccdf5a1..826096ae86 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 @@ -784,16 +785,17 @@ goExpression = \case napp' = Concrete.NamedApplication { _namedAppName = napp ^. namedApplicationNewName, - _namedAppArgs = nonEmpty' $ createArgumentBlocks (sig ^. nameSignatureArgs) + _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.substitutionE updateKind l + >>= Internal.inlineLet Internal.clone expr where goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause) @@ -803,7 +805,7 @@ goExpression = \case goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentNewFunDef) 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 +815,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 +831,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/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/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/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index f696d9e950..355994a8e8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -544,12 +544,25 @@ 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) + addPatternVar var (par ^. paramType) Nothing + 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 - guessedBodyParams <- unfoldArity <$> guessArity body - let pref' :: [IsImplicit] = map (^. paramImplicit) (take pref bodyParams) + locals <- get + guessedBodyParams <- withLocalVars locals (unfoldArity <$> guessArity body) + let pref' :: [FunctionParameter] = take pref bodyParams pref :: Int = aI - targetI preImplicits = length . takeWhile isImplicitOrInstance aI :: Int = preImplicits (map (^. paramImplicit) bodyParams) @@ -559,10 +572,9 @@ 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 -> do - return ([], bodyTy) + | otherwise -> return ([], bodyTy) p : ps -> do bodyTy' <- weakNormalize bodyTy case bodyTy' of @@ -581,9 +593,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 +604,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 +659,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 +680,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 +732,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 @@ -1129,7 +1141,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' () @@ -1432,7 +1444,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 @@ -1449,7 +1461,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 @@ -1484,7 +1496,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 $ @@ -1521,13 +1533,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 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/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] 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..6d7d00cfb6 --- /dev/null +++ b/test/Compilation/PositiveNew.hs @@ -0,0 +1,58 @@ +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)", + "Test046: Polymorphic type arguments", + -- TODO allow lambda branches of different number of patterns + "Test027: Church numerals" + ] diff --git a/test/Typecheck/PositiveNew.hs b/test/Typecheck/PositiveNew.hs index a2ae510b22..0577942e61 100644 --- a/test/Typecheck/PositiveNew.hs +++ b/test/Typecheck/PositiveNew.hs @@ -37,27 +37,14 @@ 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 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" ] 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/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/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))))); - 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; - 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 95% rename from tests/positive/Monads/Identity.juvix rename to tests/Compilation/positive/test072/Identity.juvix index 7a4b6cb8b2..1d84c8fad2 100644 --- a/tests/positive/Monads/Identity.juvix +++ b/tests/Compilation/positive/test072/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/Compilation/positive/test072/Monad.juvix similarity index 68% rename from tests/positive/Monads/Monad.juvix rename to tests/Compilation/positive/test072/Monad.juvix index 19c8c55ae5..81a4dfb960 100644 --- a/tests/positive/Monads/Monad.juvix +++ b/tests/Compilation/positive/test072/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/Compilation/positive/test072/MonadReader.juvix similarity index 89% rename from tests/positive/Monads/MonadReader.juvix rename to tests/Compilation/positive/test072/MonadReader.juvix index 6d0c93b600..8aeda8fd8d 100644 --- a/tests/positive/Monads/MonadReader.juvix +++ b/tests/Compilation/positive/test072/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/Compilation/positive/test072/MonadState.juvix similarity index 57% rename from tests/positive/Monads/MonadState.juvix rename to tests/Compilation/positive/test072/MonadState.juvix index 71caaf942c..fc9eb31de0 100644 --- a/tests/positive/Monads/MonadState.juvix +++ b/tests/Compilation/positive/test072/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/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 81% rename from tests/positive/Monads/ReaderT.juvix rename to tests/Compilation/positive/test072/ReaderT.juvix index 2cb8e872d0..95d4d7d3dd 100644 --- a/tests/positive/Monads/ReaderT.juvix +++ b/tests/Compilation/positive/test072/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/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 86% rename from tests/positive/Monads/StateT.juvix rename to tests/Compilation/positive/test072/StateT.juvix index f7d3c7c1f7..f804233f37 100644 --- a/tests/positive/Monads/StateT.juvix +++ b/tests/Compilation/positive/test072/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) :=