From 9e817a62fa418e475383c42f39fd4d822857d148 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 21 Jun 2022 17:53:35 +0200 Subject: [PATCH] Fix: Add check for constructor return types (#182) * Checking indtype declar (return type) * Add missing semicolon * Fix typo --- src/MiniJuvix/Pipeline.hs | 2 +- src/MiniJuvix/Syntax/MicroJuvix/Error.hs | 2 + .../Syntax/MicroJuvix/Error/Types.hs | 29 +++++++ .../Syntax/MicroJuvix/Language/Extra.hs | 13 ++- .../Translation/AbstractToMicroJuvix.hs | 87 ++++++++++++------- test/TypeCheck/Negative.hs | 14 +++ .../MicroJuvix/FunctionApplied.mjuvix | 2 +- .../MicroJuvix/WrongReturnType.mjuvix | 8 ++ .../WrongReturnTypeParameters.mjuvix | 7 ++ tests/positive/Polymorphism.mjuvix | 3 +- tests/positive/PolymorphismHoles.mjuvix | 3 +- 11 files changed, 133 insertions(+), 37 deletions(-) create mode 100644 tests/negative/MicroJuvix/WrongReturnType.mjuvix create mode 100644 tests/negative/MicroJuvix/WrongReturnTypeParameters.mjuvix diff --git a/src/MiniJuvix/Pipeline.hs b/src/MiniJuvix/Pipeline.hs index 93c854892..aa2b3b55b 100644 --- a/src/MiniJuvix/Pipeline.hs +++ b/src/MiniJuvix/Pipeline.hs @@ -113,7 +113,7 @@ pipelineMicroJuvix :: Members '[Error MiniJuvixError] r => Abstract.AbstractResult -> Sem r MicroJuvix.MicroJuvixResult -pipelineMicroJuvix = mapError (MiniJuvixError @MicroJuvix.TerminationError) . MicroJuvix.entryMicroJuvix +pipelineMicroJuvix = MicroJuvix.entryMicroJuvix pipelineMicroJuvixArity :: Members '[Error MiniJuvixError, NameIdGen] r => diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs index b09d4e991..df9724d73 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs @@ -13,6 +13,7 @@ import MiniJuvix.Syntax.MicroJuvix.Error.Types data TypeCheckerError = ErrWrongConstructorType WrongConstructorType + | ErrWrongReturnType WrongReturnType | ErrArity ArityCheckerError | ErrWrongType WrongType | ErrUnsolvedMeta UnsolvedMeta @@ -22,6 +23,7 @@ instance ToGenericError TypeCheckerError where genericError :: TypeCheckerError -> GenericError genericError = \case ErrWrongConstructorType e -> genericError e + ErrWrongReturnType e -> genericError e ErrArity e -> genericError e ErrWrongType e -> genericError e ErrUnsolvedMeta e -> genericError e diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs index 93f335862..90c437724 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs @@ -4,6 +4,7 @@ import MiniJuvix.Prelude import MiniJuvix.Prelude.Pretty import MiniJuvix.Syntax.MicroJuvix.Error.Pretty import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.MicroJuvix.Language.Extra -- | the type of the constructor used in a pattern does -- not match the type of the inductive being matched @@ -34,6 +35,34 @@ instance ToGenericError WrongConstructorType where <> line <> indent' (ppCode (e ^. wrongCtorTypeExpected)) +data WrongReturnType = WrongReturnType + { _wrongReturnTypeConstructorName :: Name, + _wrongReturnTypeExpected :: Type, + _wrongReturnTypeActual :: Type + } + +makeLenses ''WrongReturnType + +instance ToGenericError WrongReturnType where + genericError e = + GenericError + { _genericErrorLoc = j, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i, j] + } + where + ctorName = e ^. wrongReturnTypeConstructorName + i = getLoc ctorName + j = getLoc (typeAsExpression (e ^. wrongReturnTypeActual)) + msg = + "The constructor" <+> ppCode ctorName <+> "has the wrong return type:" + <> line + <> indent' (ppCode (e ^. wrongReturnTypeActual)) + <> line + <> "but is expected to have type:" + <> line + <> indent' (ppCode (e ^. wrongReturnTypeExpected)) + newtype UnsolvedMeta = UnsolvedMeta { _unsolvedMeta :: Hole } diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs index 192e75546..574dcc5ed 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs @@ -411,7 +411,7 @@ foldExplicitApplication :: Expression -> [Expression] -> Expression foldExplicitApplication f = foldApplication f . zip (repeat Explicit) foldApplication :: Expression -> [(IsImplicit, Expression)] -> Expression -foldApplication f args = case args of +foldApplication f = \case [] -> f ((i, a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as @@ -434,3 +434,14 @@ unfoldTypeApplication (TypeApplication l' r' _) = second (|: r') (unfoldType l') unfoldType t = case t of TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l) _ -> (t, []) + +foldTypeApp :: Type -> [Type] -> Type +foldTypeApp ty = \case + [] -> ty + (p : ps) -> foldTypeApp (TypeApp (TypeApplication ty p Explicit)) ps + +foldTypeAppName :: Name -> [Name] -> Type +foldTypeAppName tyName indParams = + foldTypeApp + (TypeIden (TypeIdenInductive tyName)) + (map (TypeIden . TypeIdenVariable) indParams) diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs index 411670787..2fae83f76 100644 --- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs +++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs @@ -10,7 +10,9 @@ import MiniJuvix.Pipeline.EntryPoint qualified as E import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract import MiniJuvix.Syntax.Abstract.Language qualified as Abstract +import MiniJuvix.Syntax.MicroJuvix.Error import MiniJuvix.Syntax.MicroJuvix.Language +import MiniJuvix.Syntax.MicroJuvix.Language.Extra import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult import MiniJuvix.Syntax.Universe import MiniJuvix.Syntax.Usage @@ -30,15 +32,23 @@ iniState = makeLenses ''TranslationState entryMicroJuvix :: - Members '[Error TerminationError] r => + Members '[Error MiniJuvixError] r => Abstract.AbstractResult -> Sem r MicroJuvixResult entryMicroJuvix abstractResults = do - unless noTerminationOption (checkTermination topModule infoTable) + unless + noTerminationOption + ( mapError + (MiniJuvixError @TerminationError) + (checkTermination topModule infoTable) + ) _resultModules' <- evalState iniState - (mapM goModule (abstractResults ^. Abstract.resultModules)) + ( mapM + (mapError (MiniJuvixError @TypeCheckerError) . goModule) + (abstractResults ^. Abstract.resultModules) + ) return MicroJuvixResult { _resultAbstract = abstractResults, @@ -49,10 +59,11 @@ entryMicroJuvix abstractResults = do infoTable = abstractResults ^. Abstract.resultTable noTerminationOption = abstractResults - ^. Abstract.abstractResultEntryPoint . E.entryPointNoTermination + ^. Abstract.abstractResultEntryPoint + . E.entryPointNoTermination goModule :: - Member (State TranslationState) r => + Members '[State TranslationState, Error TypeCheckerError] r => Abstract.TopModule -> Sem r Module goModule m = do @@ -66,10 +77,10 @@ goModule m = do unsupported :: Text -> a unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing) -goModuleBody :: Member (State TranslationState) r => Abstract.ModuleBody -> Sem r ModuleBody +goModuleBody :: Members '[State TranslationState, Error TypeCheckerError] r => Abstract.ModuleBody -> Sem r ModuleBody goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. Abstract.moduleStatements) -goImport :: Member (State TranslationState) r => Abstract.TopModule -> Sem r (Maybe Include) +goImport :: Members '[State TranslationState, Error TypeCheckerError] r => Abstract.TopModule -> Sem r (Maybe Include) goImport m = do inc <- gets (HashSet.member (m ^. Abstract.moduleName) . (^. translationStateIncluded)) if @@ -85,7 +96,7 @@ goImport m = do ) goStatement :: - Member (State TranslationState) r => + Members [State TranslationState, Error TypeCheckerError] r => Abstract.Statement -> Sem r (Maybe Statement) goStatement = \case @@ -97,7 +108,7 @@ goStatement = \case Abstract.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i goTypeIden :: Abstract.Iden -> TypeIden -goTypeIden i = case i of +goTypeIden = \case Abstract.IdenFunction {} -> unsupported "functions in types" Abstract.IdenConstructor {} -> unsupported "constructors in types" Abstract.IdenVar v -> TypeIdenVariable v @@ -254,31 +265,47 @@ goInductiveParameter f = (Just {}, _, _) -> unsupported "only type variables of small types are allowed" (Nothing, _, _) -> unsupported "unnamed inductive parameters" -goInductiveDef :: forall r. Abstract.InductiveDef -> Sem r InductiveDef +goConstructorType :: Abstract.Expression -> Sem r [Type] +goConstructorType = fmap fst . viewConstructorType + +goInductiveDef :: + forall r. + Members '[Error TypeCheckerError] r => + Abstract.InductiveDef -> + Sem r InductiveDef goInductiveDef i = case i ^. Abstract.inductiveType of + Just Abstract.ExpressionUniverse {} -> helper Just {} -> unsupported "inductive indices" - _ -> do - _inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters) - _inductiveConstructors' <- mapM goConstructorDef (i ^. Abstract.inductiveConstructors) - return - InductiveDef - { _inductiveName = indName, - _inductiveParameters = _inductiveParameters', - _inductiveConstructors = _inductiveConstructors' - } + _ -> helper where - indName = i ^. Abstract.inductiveName - goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef - goConstructorDef c = do - _constructorParameters' <- goConstructorType (c ^. Abstract.constructorType) + indTypeName = i ^. Abstract.inductiveName + helper = do + inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters) + let indTy :: Type = foldTypeAppName indTypeName (map (^. inductiveParamName) inductiveParameters') + inductiveConstructors' <- mapM (goConstructorDef indTy) (i ^. Abstract.inductiveConstructors) return - InductiveConstructorDef - { _constructorName = c ^. Abstract.constructorName, - _constructorParameters = _constructorParameters' + InductiveDef + { _inductiveName = indTypeName, + _inductiveParameters = inductiveParameters', + _inductiveConstructors = inductiveConstructors' } - -- TODO check that the return type corresponds with the inductive type - goConstructorType :: Abstract.Expression -> Sem r [Type] - goConstructorType = fmap fst . viewConstructorType + where + goConstructorDef :: Type -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef + goConstructorDef expectedReturnType c = do + (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType) + let ctorName = c ^. Abstract.constructorName + if + | actualReturnType == expectedReturnType -> + return + InductiveConstructorDef + { _constructorName = ctorName, + _constructorParameters = _constructorParameters' + } + | otherwise -> + throw + ( ErrWrongReturnType + (WrongReturnType ctorName expectedReturnType actualReturnType) + ) goTypeApplication :: Abstract.Application -> Sem r TypeApplication goTypeApplication (Abstract.Application l r i) = do @@ -292,7 +319,7 @@ goTypeApplication (Abstract.Application l r i) = do } viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type) -viewConstructorType e = case e of +viewConstructorType = \case Abstract.ExpressionFunction f -> first toList <$> viewFunctionType f Abstract.ExpressionIden i -> return ([], TypeIden (goTypeIden i)) Abstract.ExpressionHole {} -> unsupported "holes in constructor type" diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs index 913b81c5c..e2f48cde7 100644 --- a/test/TypeCheck/Negative.hs +++ b/test/TypeCheck/Negative.hs @@ -76,5 +76,19 @@ tests = "MultiWrongType.mjuvix" $ \case ErrWrongType {} -> Nothing + _ -> wrongError, + NegTest + "Wrong return type name for a constructor of a simple data type" + "MicroJuvix" + "WrongReturnType.mjuvix" + $ \case + ErrWrongReturnType {} -> Nothing + _ -> wrongError, + NegTest + "Wrong return type for a constructor of a data type with parameters " + "MicroJuvix" + "WrongReturnTypeParameters.mjuvix" + $ \case + ErrWrongReturnType {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/MicroJuvix/FunctionApplied.mjuvix b/tests/negative/MicroJuvix/FunctionApplied.mjuvix index 3d19e931c..bd84a5f83 100644 --- a/tests/negative/MicroJuvix/FunctionApplied.mjuvix +++ b/tests/negative/MicroJuvix/FunctionApplied.mjuvix @@ -1,6 +1,6 @@ module FunctionApplied; inductive T (A : Type) { - c : A → T; + c : A → T A; }; f : {A : Type} → A → T A; diff --git a/tests/negative/MicroJuvix/WrongReturnType.mjuvix b/tests/negative/MicroJuvix/WrongReturnType.mjuvix new file mode 100644 index 000000000..5baf85178 --- /dev/null +++ b/tests/negative/MicroJuvix/WrongReturnType.mjuvix @@ -0,0 +1,8 @@ +module WrongReturnType; + +axiom B : Type; +inductive A { +c : B; +}; + +end; diff --git a/tests/negative/MicroJuvix/WrongReturnTypeParameters.mjuvix b/tests/negative/MicroJuvix/WrongReturnTypeParameters.mjuvix new file mode 100644 index 000000000..066bc46f6 --- /dev/null +++ b/tests/negative/MicroJuvix/WrongReturnTypeParameters.mjuvix @@ -0,0 +1,7 @@ +module WrongReturnTypeParameters; + +inductive A (B : Type) { +c : A; +}; + +end; diff --git a/tests/positive/Polymorphism.mjuvix b/tests/positive/Polymorphism.mjuvix index f36ce4eb1..8be9a976c 100644 --- a/tests/positive/Polymorphism.mjuvix +++ b/tests/positive/Polymorphism.mjuvix @@ -11,8 +11,7 @@ inductive Nat { inductive List (A : Type) { nil : List A; - -- TODO check that the return type is saturated with the proper variable - cons : A → List A → Nat; + cons : A → List A → List A; }; inductive Bool { diff --git a/tests/positive/PolymorphismHoles.mjuvix b/tests/positive/PolymorphismHoles.mjuvix index d7b173f23..3cc60dcf1 100644 --- a/tests/positive/PolymorphismHoles.mjuvix +++ b/tests/positive/PolymorphismHoles.mjuvix @@ -11,8 +11,7 @@ inductive Nat { inductive List (A : Type) { nil : List A; - -- TODO check that the return type is saturated with the proper variable - cons : A → List A → Nat; + cons : A → List A → List A; }; inductive Bool {