Disallow iterators with zero ranges (#2267)

* Closes #2265
2024-12-01 00:04:58 +03:00 · 2023-08-03 11:43:59 +02:00 · 2023-08-03 11:43:59 +02:00 · 22de9d0233
commit 22de9d0233
parent f38123c550
8 changed files with 100 additions and 207 deletions
--- 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
-                }
-        }
--- 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
--- 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
--- 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.
--- 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 "<expression>" $
    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 "<named application>" $ 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
--- 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
--- 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;
--- 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;