Adding a whole bunch of tuple sections (#680)

src/Idris/Parser.idr

@@ -250,8 +250,7 @@ mutual
            pure (PUnit (boundToFC fname (mergeBounds s b)))
       -- dependent pairs with type annotation (so, the type form)
     <|> do dpairType fname s indents <* symbol ")"
-    <|> do here <- location
-           e <- bounds (expr pdef fname indents)
+    <|> do e <- bounds (expr pdef fname indents)
            -- dependent pairs with no type annotation
            (do loc <- bounds (symbol "**")
                rest <- bounds ((nestedDpair fname loc indents <|> expr pdef fname indents) <* symbol ")")
@@ -265,6 +264,11 @@ mutual
                <|>
               -- all the other bracketed expressions
               tuple fname s indents e.val))
+    <|> do here <- location
+           let fc = MkFC fname here here
+           let var = PRef fc (MN "__leftTupleSection" 0)
+           ts <- bounds (nonEmptyTuple fname s indents var)
+           pure (PLam fc top Explicit var (PInfer fc) ts.val)
 
   getInitRange : List PTerm -> SourceEmptyRule (PTerm, Maybe PTerm)
   getInitRange [x] = pure (x, Nothing)
@@ -297,20 +301,44 @@ mutual
              <|> (do b <- bounds (symbol "]")
                      pure (PList (boundToFC fname (mergeBounds s b)) xs))
 
+  nonEmptyTuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
+  nonEmptyTuple fname s indents e
+      = do rest <- bounds (some (bounds (symbol "," *> optional (bounds (expr pdef fname indents))))
+                           <* continueWith indents ")")
+           pure $ buildOutput rest (mergePairs 0 rest rest.val)
+    where
+
+      lams : List (FC, PTerm) -> PTerm -> PTerm
+      lams [] e = e
+      lams ((fc, var) :: vars) e
+        = PLam fc top Explicit var (PInfer fc)
+        $ lams vars e
+
+      buildOutput : WithBounds t' -> (List (FC, PTerm), PTerm) -> PTerm
+      buildOutput rest (vars, scope) = lams vars $ PPair (boundToFC fname (mergeBounds s rest)) e scope
+
+      optionalPair : Int -> WithBounds (Maybe (WithBounds PTerm)) -> (Int, (List (FC, PTerm), PTerm))
+      optionalPair i exp = case exp.val of
+        Just e  => (i, ([], e.val))
+        Nothing => let fc = boundToFC fname exp in
+                   let var = PRef fc (MN "__infixTupleSection" i) in
+                   (i+1, ([(fc, var)], var))
+
+      mergePairs : Int -> WithBounds t' -> List (WithBounds (Maybe (WithBounds PTerm))) ->
+                   (List (FC, PTerm), PTerm)
+      mergePairs _ end [] = ([], PUnit (boundToFC fname (mergeBounds s end)))
+      mergePairs i end [exp] = snd (optionalPair i exp)
+      mergePairs i end (exp :: rest)
+          = let (j, (var, t)) = optionalPair i exp in
+            let (vars, ts)    = mergePairs j end rest in
+            (var ++ vars, PPair (boundToFC fname (mergeBounds exp end)) t ts)
+
   -- A pair, dependent pair, or just a single expression
   tuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
   tuple fname s indents e
-      = do rest <- bounds (some (symbol "," *> bounds (expr pdef fname indents)) <* continueWith indents ")")
-           pure (PPair (boundToFC fname (mergeBounds s rest)) e
-                       (mergePairs rest rest.val))
+     =   nonEmptyTuple fname s indents e
      <|> do end <- bounds (continueWith indents ")")
             pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
-    where
-      mergePairs : WithBounds t' -> List (WithBounds PTerm) -> PTerm
-      mergePairs end [] = PUnit (boundToFC fname (mergeBounds s end))
-      mergePairs end [exp] = exp.val
-      mergePairs end (exp :: rest)
-          = PPair (boundToFC fname (mergeBounds exp end)) exp.val (mergePairs end rest)
 
   postfixApp : FileName -> IndentInfo -> Rule PTerm
   postfixApp fname indents

tests/Main.idr

@@ -42,6 +42,7 @@ idrisTests
        "basic031", "basic032", "basic033", "basic034", "basic035",
        "basic036", "basic037", "basic038", "basic039", "basic040",
        "basic041", "basic042", "basic043", "basic044", "basic045",
+       "basic046",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",

tests/idris2/basic046/TupleSections.idr

@@ -0,0 +1,14 @@
+import Data.Vect
+
+distrL : a -> List b -> List (a, b)
+distrL a = map (a,)
+
+distrR : b -> List a -> List (a, b)
+distrR b = map (, b)
+
+-- closeVect : List (n ** Vect n Nat)
+-- closeVect = map (** flip replicate 3) [0..10]
+
+insert : List (Nat,Nat,Nat,Nat)
+insert = map (\ f => f (the Nat 0) (the Nat 1))
+         [(,,2,3), (2,,,3), (2,3,,)]

tests/idris2/basic046/expected

@@ -0,0 +1,6 @@
+1/1: Building TupleSections (TupleSections.idr)
+Main> [("begin", 0), ("begin", 1), ("begin", 2)]
+Main> [(0, "end"), (1, "end"), (2, "end")]
+Main> [(0, (1, (2, 3))), (2, (0, (1, 3))), (2, (3, (0, 1)))]
+Main> Main> 
+Bye for now!

tests/idris2/basic046/input

@@ -0,0 +1,5 @@
+distrL "begin" [0..2]
+distrR "end" [0..2]
+insert
+
+:q

tests/idris2/basic046/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 TupleSections.idr < input
+
+rm -rf build