From 22de9d0233fba74a18ee0d075b8b834e4ce80a21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Thu, 3 Aug 2023 11:43:59 +0200 Subject: [PATCH] Disallow iterators with zero ranges (#2267) * Closes #2265 --- src/Juvix/Compiler/Concrete/Extra.hs | 45 ----- src/Juvix/Compiler/Concrete/Language.hs | 21 -- src/Juvix/Compiler/Concrete/Print/Base.hs | 10 - .../FromParsed/Analysis/Scoping.hs | 13 -- .../Concrete/Translation/FromSource.hs | 189 ++++++++---------- src/Juvix/Data/IteratorAttribs.hs | 3 + tests/negative/Iterators2.juvix | 4 +- tests/positive/Iterators.juvix | 22 +- 8 files changed, 100 insertions(+), 207 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 1a125237f..ddfff6566 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -7,8 +7,6 @@ module Juvix.Compiler.Concrete.Extra groupStatements, flattenStatement, migrateFunctionSyntax, - fromAmbiguousIterator, - ambiguousIteratorToAtoms, ) where @@ -193,46 +191,3 @@ migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m } getClauses :: S.Symbol -> [FunctionClause 'Scoped] getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction] - -fromAmbiguousIterator :: AmbiguousIterator -> Iterator 'Parsed -fromAmbiguousIterator AmbiguousIterator {..} = - Iterator - { _iteratorName = _ambiguousIteratorName, - _iteratorRanges = [], - _iteratorBody = _ambiguousIteratorBody, - _iteratorBodyBraces = _ambiguousIteratorBodyBraces, - _iteratorInitializers = map mkInitializer (toList _ambiguousIteratorInitializers), - _iteratorParens = _ambiguousIteratorParens - } - where - mkInitializer :: NamedArgument 'Parsed -> Initializer 'Parsed - mkInitializer a@NamedArgument {..} = - Initializer - { _initializerAssignKw = _namedArgAssignKw, - _initializerPattern = PatternAtoms (pure (PatternAtomIden (NameUnqualified _namedArgName))) (Irrelevant (getLoc a)), - _initializerExpression = _namedArgValue - } - -ambiguousIteratorToAtoms :: AmbiguousIterator -> ExpressionAtoms 'Parsed -ambiguousIteratorToAtoms AmbiguousIterator {..} = - ExpressionAtoms - { _expressionAtomsLoc = Irrelevant (getLoc napp), - _expressionAtoms = pure (AtomNamedApplication napp) <> body - } - where - body :: NonEmpty (ExpressionAtom 'Parsed) - body - | _ambiguousIteratorBodyBraces = pure (AtomBraces (WithLoc (getLoc _ambiguousIteratorBody) _ambiguousIteratorBody)) - | otherwise = _ambiguousIteratorBody ^. expressionAtoms - napp = - NamedApplication - { _namedAppName = _ambiguousIteratorName, - _namedAppSignature = Irrelevant (), - _namedAppArgs = - pure - ArgumentBlock - { _argBlockDelims = Irrelevant Nothing, - _argBlockImplicit = Explicit, - _argBlockArgs = _ambiguousIteratorInitializers - } - } diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 8b30a770a..4d2f08a2a 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -101,11 +101,6 @@ type family NameSignatureType s = res | res -> s where NameSignatureType 'Parsed = () NameSignatureType 'Scoped = NameSignature -type AmbiguousIteratorType :: Stage -> GHC.Type -type family AmbiguousIteratorType s = res | res -> s where - AmbiguousIteratorType 'Parsed = AmbiguousIterator - AmbiguousIteratorType 'Scoped = Void - type ModulePathType :: Stage -> ModuleIsTop -> GHC.Type type family ModulePathType s t = res | res -> t s where ModulePathType 'Parsed 'ModuleTop = TopModulePath @@ -1184,20 +1179,6 @@ deriving stock instance Ord (Iterator 'Parsed) deriving stock instance Ord (Iterator 'Scoped) --- | Either an Iterator or a NamedApplication. Has the form: --- f (sym := expr; .. ; symn := expr) -- not followed by range -data AmbiguousIterator = AmbiguousIterator - { _ambiguousIteratorName :: Name, - _ambiguousIteratorInitializers :: NonEmpty (NamedArgument 'Parsed), - _ambiguousIteratorBody :: ExpressionType 'Parsed, - -- | Was the body enclosed in braces? - _ambiguousIteratorBodyBraces :: Bool, - -- | Due to limitations of the pretty printing algorithm, we store whether - -- the iterator was surrounded by parentheses in the code. - _ambiguousIteratorParens :: Bool - } - deriving stock (Show, Eq, Ord) - data List (s :: Stage) = List { _listBracketL :: Irrelevant KeywordRef, _listBracketR :: Irrelevant KeywordRef, @@ -1285,7 +1266,6 @@ data ExpressionAtom (s :: Stage) | AtomLiteral LiteralLoc | AtomParens (ExpressionType s) | AtomIterator (Iterator s) - | AtomAmbiguousIterator (AmbiguousIteratorType s) | AtomNamedApplication (NamedApplication s) deriving stock instance Show (ExpressionAtom 'Parsed) @@ -1493,7 +1473,6 @@ makeLenses ''PatternBinding makeLenses ''PatternAtoms makeLenses ''ExpressionAtoms makeLenses ''Iterator -makeLenses ''AmbiguousIterator makeLenses ''Initializer makeLenses ''Range makeLenses ''ModuleIndex diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index cdcb7e5c2..25bea1905 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -13,7 +13,6 @@ import Juvix.Compiler.Concrete.Data.InfoTable import Juvix.Compiler.Concrete.Data.NameSignature.Base import Juvix.Compiler.Concrete.Data.Scope.Base import Juvix.Compiler.Concrete.Data.ScopedName qualified as S -import Juvix.Compiler.Concrete.Extra (fromAmbiguousIterator) import Juvix.Compiler.Concrete.Extra qualified as Concrete import Juvix.Compiler.Concrete.Keywords qualified as Kw import Juvix.Compiler.Concrete.Language @@ -122,11 +121,6 @@ ppExpressionType = case sing :: SStage s of SParsed -> ppCode SScoped -> ppCode -ppAmbiguousIteratorType :: forall s. SingI s => PrettyPrinting (AmbiguousIteratorType s) -ppAmbiguousIteratorType = case sing :: SStage s of - SParsed -> ppCode - SScoped -> ppCode - ppPatternAtomType :: forall s. SingI s => PrettyPrinting (PatternAtomType s) ppPatternAtomType = case sing :: SStage s of SParsed -> ppCodeAtom @@ -247,9 +241,6 @@ instance SingI s => PrettyPrint (List s) where e = hsepSemicolon (map ppExpressionType _listItems) l <> e <> r -instance PrettyPrint AmbiguousIterator where - ppCode = ppCode . fromAmbiguousIterator - instance SingI s => PrettyPrint (NamedArgument s) where ppCode NamedArgument {..} = do let s = ppCode _namedArgName @@ -286,7 +277,6 @@ instance SingI s => PrettyPrint (ExpressionAtom s) where AtomBraces e -> braces (ppExpressionType (e ^. withLocParam)) AtomHole w -> ppHoleType w AtomIterator i -> ppCode i - AtomAmbiguousIterator i -> ppAmbiguousIteratorType i AtomNamedApplication i -> ppCode i instance PrettyPrint PatternScopedIden where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c8d68575d..ed78a4e9b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -15,7 +15,6 @@ import Juvix.Compiler.Concrete.Data.Name qualified as N import Juvix.Compiler.Concrete.Data.NameSignature import Juvix.Compiler.Concrete.Data.Scope import Juvix.Compiler.Concrete.Data.ScopedName qualified as S -import Juvix.Compiler.Concrete.Extra (fromAmbiguousIterator) import Juvix.Compiler.Concrete.Extra qualified as P import Juvix.Compiler.Concrete.Gen qualified as G import Juvix.Compiler.Concrete.Language @@ -1792,18 +1791,6 @@ checkExpressionAtom e = case e of AtomList l -> pure . AtomList <$> checkList l AtomIterator i -> pure . AtomIterator <$> checkIterator i AtomNamedApplication i -> pure . AtomNamedApplication <$> checkNamedApplication i - AtomAmbiguousIterator i -> checkAmbiguousIterator i - -checkAmbiguousIterator :: - forall r. - Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => - AmbiguousIterator -> - Sem r (NonEmpty (ExpressionAtom 'Scoped)) -checkAmbiguousIterator a = do - nm <- checkName (a ^. ambiguousIteratorName) - if - | isJust (identifierName nm ^. S.nameIterator) -> pure . AtomIterator <$> checkIterator (fromAmbiguousIterator a) - | otherwise -> (^. expressionAtoms) <$> checkExpressionAtoms (P.ambiguousIteratorToAtoms a) checkNamedApplication :: forall r. diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index e9d0545a4..0be50a007 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -599,7 +599,7 @@ expressionAtom :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdG expressionAtom = P.label "" $ AtomLiteral <$> P.try literal - <|> either AtomIterator AtomAmbiguousIterator <$> iterator + <|> AtomIterator <$> iterator <|> AtomNamedApplication <$> namedApplication <|> AtomList <$> parseList <|> AtomIdentifier <$> name @@ -624,100 +624,76 @@ parseExpressionAtoms = do -- Iterators -------------------------------------------------------------------------------- --- | Checks whether an iterator is ambiguous -ambiguousIterator :: Iterator 'Parsed -> Either (Iterator 'Parsed) AmbiguousIterator -ambiguousIterator i@Iterator {..} = maybe (Left i) Right . run . runFail $ mkAmbiguousIterator - where - mkAmbiguousIterator :: forall r. Members '[Fail] r => Sem r AmbiguousIterator - mkAmbiguousIterator = do - failUnless (null _iteratorRanges) - _ambiguousIteratorInitializers <- nonEmpty' <$> mapM mkNamedArgument _iteratorInitializers - let _ambiguousIteratorBodyBraces = _iteratorBodyBraces - _ambiguousIteratorParens = _iteratorParens - _ambiguousIteratorName = _iteratorName - _ambiguousIteratorBody = _iteratorBody - return AmbiguousIterator {..} - where - mkNamedArgument :: Initializer 'Parsed -> Sem r (NamedArgument 'Parsed) - mkNamedArgument Initializer {..} = do - let _namedArgAssignKw = _initializerAssignKw - _namedArgValue = _initializerExpression - _namedArgName <- case _initializerPattern ^. patternAtoms of - PatternAtomIden (NameUnqualified n) :| [] -> return n - _ -> fail - return NamedArgument {..} - iterator :: forall r. Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => - ParsecS r (Either (Iterator 'Parsed) AmbiguousIterator) -iterator = fmap ambiguousIterator iteratorHelper + ParsecS r (Iterator 'Parsed) +iterator = P.try $ do + off <- P.getOffset + (firstIsInit, keywordRef, _iteratorName, pat) <- P.try $ do + n <- name + lparen + pat <- parsePatternAtoms + (isInit, kwr) <- + (True,) <$> kw kwAssign + <|> (False,) <$> kw kwIn + return (isInit, Irrelevant kwr, n, pat) + val <- parseExpressionAtoms + _iteratorInitializers <- + if + | firstIsInit -> do + inis <- many (semicolon >> initializer) + rparen + let ini = + Initializer + { _initializerPattern = pat, + _initializerAssignKw = keywordRef, + _initializerExpression = val + } + return (ini : inis) + | otherwise -> return [] + _iteratorRanges <- + if + | not firstIsInit -> do + rngs <- many (semicolon >> range) + rparen + let ran = + Range + { _rangeExpression = val, + _rangePattern = pat, + _rangeInKw = keywordRef + } + return (ran : rngs) + | otherwise -> fmap (maybe [] toList) . optional $ do + lparen + rngs <- P.sepBy1 range semicolon + rparen + return rngs + when (null _iteratorRanges) $ + parseFailure off "an iterator must have at least one range" + (_iteratorBody, _iteratorBodyBraces) <- + (,True) <$> braces parseExpressionAtoms + <|> (,False) <$> parseExpressionAtoms + let _iteratorParens = False + return Iterator {..} where - iteratorHelper :: ParsecS r (Iterator 'Parsed) - iteratorHelper = P.try $ do - -- TODO remove top P.Try - (firstIsInit, keywordRef, _iteratorName, pat) <- P.try $ do - n <- name - lparen + initializer :: ParsecS r (Initializer 'Parsed) + initializer = do + (_initializerPattern, _initializerAssignKw) <- P.try $ do pat <- parsePatternAtoms - (isInit, kwr) <- - (True,) <$> kw kwAssign - <|> (False,) <$> kw kwIn - return (isInit, Irrelevant kwr, n, pat) - val <- parseExpressionAtoms - _iteratorInitializers <- - if - | firstIsInit -> do - inis <- many (semicolon >> initializer) - rparen - let ini = - Initializer - { _initializerPattern = pat, - _initializerAssignKw = keywordRef, - _initializerExpression = val - } - return (ini : inis) - | otherwise -> return [] - _iteratorRanges <- - if - | not firstIsInit -> do - rngs <- many (semicolon >> range) - rparen - let ran = - Range - { _rangeExpression = val, - _rangePattern = pat, - _rangeInKw = keywordRef - } - return (ran : rngs) - | otherwise -> fmap (maybe [] toList) . optional $ do - lparen - rngs <- P.sepBy1 range semicolon - rparen - return rngs - (_iteratorBody, _iteratorBodyBraces) <- - (,True) <$> braces parseExpressionAtoms - <|> (,False) <$> parseExpressionAtoms - let _iteratorParens = False - return Iterator {..} - where - initializer :: ParsecS r (Initializer 'Parsed) - initializer = do - (_initializerPattern, _initializerAssignKw) <- P.try $ do - pat <- parsePatternAtoms - r <- Irrelevant <$> kw kwAssign - return (pat, r) - _initializerExpression <- parseExpressionAtoms - return Initializer {..} + r <- Irrelevant <$> kw kwAssign + return (pat, r) + _initializerExpression <- parseExpressionAtoms + return Initializer {..} - range :: ParsecS r (Range 'Parsed) - range = do - (_rangePattern, _rangeInKw) <- P.try $ do - pat <- parsePatternAtoms - r <- Irrelevant <$> kw kwIn - return (pat, r) - _rangeExpression <- parseExpressionAtoms - return Range {..} + range :: ParsecS r (Range 'Parsed) + range = do + (_rangePattern, _rangeInKw) <- P.try $ do + pat <- parsePatternAtoms + r <- Irrelevant <$> kw kwIn + return (pat, r) + _rangeExpression <- parseExpressionAtoms + return Range {..} namedApplication :: forall r. @@ -732,20 +708,27 @@ namedApplication = P.label "" $ do let _namedAppArgs = firstBlock :| tailBlocks _namedAppSignature = Irrelevant () return NamedApplication {..} - where - namedArgument :: ParsecS r (NamedArgument 'Parsed) - namedArgument = do - _namedArgName <- symbol - _namedArgAssignKw <- Irrelevant <$> kw kwAssign - _namedArgValue <- parseExpressionAtoms - return NamedArgument {..} - argumentBlock :: ParsecS r (ArgumentBlock 'Parsed) - argumentBlock = P.try $ do - (l, _argBlockImplicit) <- implicitOpen - _argBlockArgs <- P.sepEndBy1 namedArgument semicolon - r <- implicitClose _argBlockImplicit - let _argBlockDelims = Irrelevant (Just (l, r)) - return ArgumentBlock {..} + +namedArgument :: + forall r. + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => + ParsecS r (NamedArgument 'Parsed) +namedArgument = do + _namedArgName <- symbol + _namedArgAssignKw <- Irrelevant <$> kw kwAssign + _namedArgValue <- parseExpressionAtoms + return NamedArgument {..} + +argumentBlock :: + forall r. + Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => + ParsecS r (ArgumentBlock 'Parsed) +argumentBlock = P.try $ do + (l, _argBlockImplicit) <- implicitOpen + _argBlockArgs <- P.sepEndBy1 namedArgument semicolon + r <- implicitClose _argBlockImplicit + let _argBlockDelims = Irrelevant (Just (l, r)) + return ArgumentBlock {..} hole :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (HoleType 'Parsed) hole = kw kwHole diff --git a/src/Juvix/Data/IteratorAttribs.hs b/src/Juvix/Data/IteratorAttribs.hs index d6d95b639..714872d46 100644 --- a/src/Juvix/Data/IteratorAttribs.hs +++ b/src/Juvix/Data/IteratorAttribs.hs @@ -17,6 +17,9 @@ instance FromJSON IteratorAttribs where checkYamlKeys ["init", "range"] _iteratorAttribsInitNum <- keyMay "init" asIntegral _iteratorAttribsRangeNum <- keyMay "range" asIntegral + unless + (maybe True (> 0) _iteratorAttribsRangeNum) + (throwCustomError "the iterator must have at least one range") return IteratorAttribs {..} emptyIteratorAttribs :: IteratorAttribs diff --git a/tests/negative/Iterators2.juvix b/tests/negative/Iterators2.juvix index a8d64ab11..5b0ce5d74 100644 --- a/tests/negative/Iterators2.juvix +++ b/tests/negative/Iterators2.juvix @@ -1,6 +1,6 @@ module Iterators2; -syntax iterator bind {range: 0}; +syntax iterator bind {range: 1}; bind : {A B : Type} → (A → B) → A → B; bind f x := f x; @@ -10,4 +10,4 @@ type Bool := | false : Bool; main : Bool; -main := bind (x in true) x; +main := bind (x in true; y in false) x; diff --git a/tests/positive/Iterators.juvix b/tests/positive/Iterators.juvix index 855841e75..b91d4916c 100644 --- a/tests/positive/Iterators.juvix +++ b/tests/positive/Iterators.juvix @@ -2,13 +2,8 @@ module Iterators; syntax iterator for {init: 1, range: 1}; -for : {A B : Type} → (A → B → A) → A → B → A - | f x y := f x y; - -syntax iterator bind {init: 1, range: 0}; - -bind : {A B : Type} → (A → B) → A → B - | f x := f x; +for {A B : Type} (f : A → B → A) (x : A) (y : B) : A := + f x y; syntax iterator itconst {init: 2, range: 2}; @@ -22,9 +17,10 @@ type Bool := | false : Bool; main : Bool := - bind (z := false) - itconst (a := true; b := false) (c in false; d in false) - for (x := true) (y in false) - case x - | true := y - | false := z; + let + z : Bool := false; + in itconst (a := true; b := false) (c in false; d in false) + for (x := true) (y in false) + case x + | true := y + | false := z;