From 93595b85c80af21c0d863868d3e67f220a99972c Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 28 Sep 2023 18:01:47 +0200 Subject: [PATCH 1/5] add user error for unsupported types --- .../FromParsed/Analysis/Scoping/Error.hs | 2 ++ .../FromParsed/Analysis/Scoping/Error/Types.hs | 18 ++++++++++++++++++ .../Internal/Translation/FromConcrete.hs | 11 +++++++---- 3 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 2d078b058d..0e30a8e5f8 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -50,6 +50,7 @@ data ScoperError | ErrIncomparablePrecedences IncomaprablePrecedences | ErrAliasCycle AliasCycle | ErrInvalidRangeNumber InvalidRangeNumber + | ErrUnsupported Unsupported instance ToGenericError ScoperError where genericError = \case @@ -91,3 +92,4 @@ instance ToGenericError ScoperError where ErrIncomparablePrecedences e -> genericError e ErrAliasCycle e -> genericError e ErrInvalidRangeNumber e -> genericError e + ErrUnsupported e -> genericError e diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index 83433cd0b7..172974eba2 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -929,3 +929,21 @@ instance ToGenericError AliasCycle where where i :: Interval i = getLoc _aliasCycleDef + +data Unsupported = Unsupported + { _unsupportedMsg :: Text, + _unsupportedLoc :: Interval + } + deriving stock (Show) + +instance ToGenericError Unsupported where + genericError Unsupported {..} = do + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText _unsupportedMsg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = _unsupportedLoc diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index aa01ef04b3..c54f72a7c4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -39,9 +39,6 @@ type MCache = Cache Concrete.ModuleIndex Internal.Module -- | Needed to generate field projections. type ConstructorInfos = HashMap Internal.ConstructorName ConstructorInfo -unsupported :: Text -> a -unsupported msg = error $ msg <> "Scoped to Internal: not yet supported" - fromConcrete :: (Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen, Termination] r) => Scoper.ScoperResult -> @@ -537,7 +534,13 @@ goInductiveParameters params@InductiveParameters {..} = do paramType' <- goRhs _inductiveParametersRhs case paramType' of Internal.ExpressionUniverse {} -> return () - _ -> unsupported "only type variables of small types are allowed" + _ -> + throw $ + ErrUnsupported + Unsupported + { _unsupportedMsg = "only type variables of small types are allowed", + _unsupportedLoc = getLoc params + } let goInductiveParameter :: S.Symbol -> Internal.InductiveParameter goInductiveParameter var = From 4c5c2187865ef619fb8d894c2f239d919e174beb Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 28 Sep 2023 18:02:01 +0200 Subject: [PATCH 2/5] support holes --- src/Juvix/Compiler/Internal/Translation/FromConcrete.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index c54f72a7c4..b862328998 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -534,6 +534,7 @@ goInductiveParameters params@InductiveParameters {..} = do paramType' <- goRhs _inductiveParametersRhs case paramType' of Internal.ExpressionUniverse {} -> return () + Internal.ExpressionHole {} -> return () _ -> throw $ ErrUnsupported From 90a22e0fbdf00af0f1f07acba3fe6fdd1ca08829 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 28 Sep 2023 18:02:09 +0200 Subject: [PATCH 3/5] add positive test --- test/Typecheck/Positive.hs | 6 +++++- tests/positive/HoleTypeParameter.juvix | 5 +++++ 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 tests/positive/HoleTypeParameter.juvix diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 1ae27582f5..1072c10dc3 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -292,7 +292,11 @@ tests = posTest "Hole as numeric type" $(mkRelDir "issue2373") - $(mkRelFile "Main.juvix") + $(mkRelFile "Main.juvix"), + posTest, + "Hole in type parameter" + $(mkRelDir ".") + $(mkRelFile "HoleTypeParameter.juvix") ] <> [ compilationTest t | t <- Compilation.tests ] diff --git a/tests/positive/HoleTypeParameter.juvix b/tests/positive/HoleTypeParameter.juvix new file mode 100644 index 0000000000..b93983ec63 --- /dev/null +++ b/tests/positive/HoleTypeParameter.juvix @@ -0,0 +1,5 @@ +module HoleTypeParameter; + +type List' (A : _) := + | nil' + | cons' A (List' A); From dc7c89b1fd227663b767cf7108dbf66e68e7d956 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 28 Sep 2023 18:02:19 +0200 Subject: [PATCH 4/5] add negative test --- test/Scope/Negative.hs | 7 +++++++ tests/negative/UnsupportedType.juvix | 5 +++++ 2 files changed, 12 insertions(+) create mode 100644 tests/negative/UnsupportedType.juvix diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index 5de2a590b3..a9ea7ae838 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -350,5 +350,12 @@ scoperErrorTests = $(mkRelFile "DanglingDoubleBrace.juvix") $ \case ErrDanglingDoubleBrace {} -> Nothing + _ -> wrongError, + NegTest + "Unsupported type" + $(mkRelDir ".") + $(mkRelFile "UnsupportedType.juvix") + $ \case + ErrUnsupported {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/UnsupportedType.juvix b/tests/negative/UnsupportedType.juvix new file mode 100644 index 0000000000..76fa64a9c1 --- /dev/null +++ b/tests/negative/UnsupportedType.juvix @@ -0,0 +1,5 @@ +module UnsupportedType; + +type List' (A : Type -> Type) := + | nil' + | cons' A (List' A); From 061b9140d170e33e63dae936063427fa2ce54f44 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 29 Sep 2023 23:58:26 +0200 Subject: [PATCH 5/5] fix comma --- test/Typecheck/Positive.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 1072c10dc3..f002f416dc 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -293,8 +293,8 @@ tests = "Hole as numeric type" $(mkRelDir "issue2373") $(mkRelFile "Main.juvix"), - posTest, - "Hole in type parameter" + posTest + "Hole in type parameter" $(mkRelDir ".") $(mkRelFile "HoleTypeParameter.juvix") ]