Merge pull request #155 from edwinb/nameless-pi

Allow _ in pi binders

docs/source/tutorial/multiplicities.rst

@@ -109,7 +109,17 @@ If we use ``x`` for one part of the pair...
   -------------------------------------
   help : a
 
-The same happens if we try defining ``duplicate x = (?help, x)`` (try it!)
+The same happens if we try defining ``duplicate x = (?help, x)`` (try it!).
+
+In order to avoid parsing ambiguities, if you give an explicit multiplicity
+for a variable as with he argument to ``duplicate``, you need to give the
+name too. But, if the name isn't used in the scope of the type, you
+can use ``_`` instead of a name, as follows:
+
+.. code-block:: idris
+
+    duplicate : (1 _ : a) -> (a, a)
+
 The intution behind multiplicity ``1`` is that if we have a function with
 a type of the following form...
 
@@ -135,10 +145,10 @@ wraps an argument with unrestricted use
 .. code-block:: idris
 
     data Lin : Type -> Type where
-         MkLin : (1 x : a) -> Lin a
+         MkLin : (1 _ : a) -> Lin a
   
     data Unr : Type -> Type where
-         MkUnr : (x : a) -> Unr a
+         MkUnr : a -> Unr a
   
 If ``MkLin x`` is used once, then ``x`` is used once. But if ``MkUnr x`` is
 used once, there is no guarantee on how often ``x`` is used. We can see this a
@@ -147,10 +157,10 @@ bit more clearly by starting to write projection functions for ``Lin`` and
 
 .. code-block:: idris
 
-    getLin : (1 val : Lin a) -> a
+    getLin : (1 _ : Lin a) -> a
     getLin (MkLin x) = ?howmanyLin
   
-    getUnr : (1 val : Unr a) -> a
+    getUnr : (1 _ : Unr a) -> a
     getUnr (MkUnr x) = ?howmanyUnr
   
 Checking the types of the holes shows us that, for ``getLin``, we must use
@@ -178,7 +188,7 @@ If ``getLin`` has an unrestricted argument...
 
 .. code-block:: idris
 
-    getLin : (val : Lin a) -> a
+    getLin : Lin a -> a
     getLin (MkLin x) = ?howmanyLin
 
 ...then ``x`` is unrestricted in ``howmanyLin``::

src/Idris/Parser.idr

@@ -445,7 +445,7 @@ mutual
                    Rule (List (RigCount, Name, PTerm))
   pibindListName fname start indents
        = do rigc <- multiplicity
-            ns <- sepBy1 (symbol ",") unqualifiedName
+            ns <- sepBy1 (symbol ",") binderName
             symbol ":"
             ty <- expr pdef fname indents
             atEnd indents
@@ -453,11 +453,15 @@ mutual
             pure (map (\n => (rig, UN n, ty)) ns)
      <|> sepBy1 (symbol ",")
                 (do rigc <- multiplicity
-                    n <- name
+                    n <- binderName
                     symbol ":"
                     ty <- expr pdef fname indents
                     rig <- getMult rigc
-                    pure (rig, n, ty))
+                    pure (rig, UN n, ty))
+    where
+      -- _ gets treated specially here, it means "I don't care about the name"
+      binderName : Rule String
+      binderName = unqualifiedName <|> do symbol "_"; pure "_"
 
   pibindList : FileName -> FilePos -> IndentInfo ->
                Rule (List (RigCount, Maybe Name, PTerm))

src/TTImp/Elab/Term.idr

@@ -110,8 +110,6 @@ checkTerm rig elabinfo nest env (IVar fc n) exp
       -- type is expecting an implicit argument, so check it as an
       -- application with no arguments
       checkApp rig elabinfo nest env fc (IVar fc n) [] [] exp
-checkTerm rig elabinfo nest env (IPi fc r p (Just n) argTy retTy) exp
-    = checkPi rig elabinfo nest env fc r p n argTy retTy exp
 checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
     = do n <- case p of
                    Explicit => genVarName "arg"
@@ -119,6 +117,10 @@ checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
                    AutoImplicit => genVarName "conArg"
                    (DefImplicit _) => genVarName "defArg"
          checkPi rig elabinfo nest env fc r p n argTy retTy exp
+checkTerm rig elabinfo nest env (IPi fc r p (Just (UN "_")) argTy retTy) exp
+    = checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
+checkTerm rig elabinfo nest env (IPi fc r p (Just n) argTy retTy) exp
+    = checkPi rig elabinfo nest env fc r p n argTy retTy exp
 checkTerm rig elabinfo nest env (ILam fc r p (Just n) argTy scope) exp
     = checkLambda rig elabinfo nest env fc r p n argTy scope exp
 checkTerm rig elabinfo nest env (ILam fc r p Nothing argTy scope) exp

src/TTImp/Unelab.idr

@@ -224,8 +224,11 @@ mutual
   unelabBinder umode fc env x (Pi rig p ty) sctm sc scty
       = do (ty', _) <- unelabTy umode env ty
            p' <- unelabPi umode env p
-           let nm = if used 0 sctm || rig /= top || isDefImp p
-                       then Just x else Nothing
+           let nm = if used 0 sctm
+                       then Just x
+                       else if rig /= top || isDefImp p
+                               then Just (UN "_")
+                               else Nothing
            pure (IPi fc rig p' nm ty' sc, gType fc)
     where
       isDefImp : PiInfo t -> Bool

tests/Main.idr

@@ -26,7 +26,7 @@ ttimpTests
        "nest001", "nest002",
        "perf001", "perf002", "perf003",
        "record001", "record002", "record003",
-       "qtt001", "qtt002", "qtt003",
+       "qtt001", "qtt003",
        "total001", "total002", "total003"]
 
 idrisTests : List String
@@ -69,7 +69,7 @@ idrisTests
        "lazy001",
        -- QTT and linearity related
        "linear001", "linear002", "linear003", "linear004", "linear005",
-       "linear006", "linear007", "linear008",
+       "linear006", "linear007", "linear008", "linear009",
        -- Parameters blocks
        "params001",
        -- Performance: things which have been slow in the past, or which

tests/idris2/basic019/expected

@@ -3,6 +3,6 @@ Main> Main.foo : (x : Nat) -> (case x of { 0 => Nat -> Nat ; S k => Nat })
 Main> Prelude.elem : Eq a => a -> List a -> Bool
 elem x [] = False
 elem x (y :: ys) = if x == y then True else elem x ys
-Main> PrimIO.io_bind : (1 act : IO a) -> (1 k : (a -> IO b)) -> IO b
+Main> PrimIO.io_bind : (1 _ : IO a) -> (1 _ : (a -> IO b)) -> IO b
 io_bind (MkIO fn) k = MkIO (\1 w => (case fn w of { MkIORes x' w' => case k x' of { MkIO res => res w' } }))
 Main> Bye for now!

tests/idris2/basic030/expected

@@ -1,7 +1,7 @@
 1/1: Building arity (arity.idr)
 arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
-When unifying (1 {arg:241} : Nat) -> MyN and MyN
+When unifying (1 _ : Nat) -> MyN and MyN
 Mismatch between:
-	(1 {arg:241} : Nat) -> MyN
+	(1 _ : Nat) -> MyN
 and
 	MyN

tests/idris2/basic036/expected

@@ -1,5 +1,5 @@
 1/1: Building defimp (defimp.idr)
-Main> Main.dvec : (n : Nat) -> {default (replicate n 1) xs : Vect n Nat} -> Nat
+Main> Main.dvec : (n : Nat) -> {default (replicate n 1) _ : Vect n Nat} -> Nat
 Main> 3
 Main> 6
 Main> Bye for now!

tests/idris2/linear004/expected

@@ -4,22 +4,22 @@ Main> S Z
 Main> S (S Z)
 Main> S Z
 Main> (interactive):1:15--1:16:x is not accessible in this context
-Main> (interactive):1:5--1:31:When unifying Nat -> Nat -> Nat and (0 x : Nat) -> Nat -> Nat
+Main> (interactive):1:5--1:31:When unifying Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat
 Mismatch between:
 	Nat -> Nat -> Nat
 and
-	(0 x : Nat) -> Nat -> Nat
-Main> (interactive):1:5--1:31:When unifying (1 x : Nat) -> Nat -> Nat and (0 x : Nat) -> Nat -> Nat
+	(0 _ : Nat) -> Nat -> Nat
+Main> (interactive):1:5--1:31:When unifying (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat
 Mismatch between:
-	(1 x : Nat) -> Nat -> Nat
+	(1 _ : Nat) -> Nat -> Nat
 and
-	(0 x : Nat) -> Nat -> Nat
+	(0 _ : Nat) -> Nat -> Nat
 Main> (interactive):1:20--1:22:x is not accessible in this context
 Main> S (S Z)
 Main> S (S Z)
-Main> (interactive):1:6--1:31:When unifying (0 x : Nat) -> Nat -> Nat and Nat -> Nat -> Nat
+Main> (interactive):1:6--1:31:When unifying (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat
 Mismatch between:
-	(0 x : Nat) -> Nat -> Nat
+	(0 _ : Nat) -> Nat -> Nat
 and
 	Nat -> Nat -> Nat
 Main> Bye for now!

tests/idris2/linear009/expected

@@ -0,0 +1,31 @@
+1/1: Building qtt (qtt.idr)
+Main>  0 m : Nat
+ 0 a : Type
+   x : a
+ 0 y : a
+ 0 ws : Vect k a
+ 1 zs : Vect (S k) a
+   ys : Vect m a
+ 0 n : Nat
+-------------------------------------
+foo : Vect (S (S (plus k m))) a
+Main>  0 m : Nat
+ 0 a : Type
+   ys : Vect m a
+   x : a
+ 1 zs : Vect k a
+ 0 xs : Vect (S k) a
+ 0 n : Nat
+-------------------------------------
+bar : Vect (S (plus k m)) a
+Main>  0 m : Nat
+ 0 a : Type
+   ys : Vect m a
+   x : a
+ 0 zs : Vect k a
+ 0 xs : Vect (S k) a
+ 0 n : Nat
+ 1 ts : Vect k a
+-------------------------------------
+baz : Vect (S (plus k m)) a
+Main> Bye for now!

tests/idris2/linear009/qtt.idr

@@ -0,0 +1,19 @@
+data Vect : Nat -> Type -> Type where 
+     Nil : Vect Z a 
+     (::) : a -> (1 xs : Vect k a) -> Vect (S k) a 
+ 
+partial
+append : (1 _ : Vect n a) -> Vect m a -> Vect (n + m) a 
+append (x :: zs@(y :: ws)) ys = ?foo -- zs usable, y+ws not 
+ 
+cappend : (1 _ : Vect n a) -> Vect m a -> Vect (plus n m) $a 
+cappend xs ys 
+    = case xs of 
+           Nil => ys 
+           x :: zs => ?bar -- zs usable, xs not 
+ 
+cappend2 : (1 _ : Vect n a) -> Vect m a -> Vect (plus n m) a 
+cappend2 xs ys 
+    = case xs of 
+           Nil => ys 
+           x :: zs => let ts = zs in ?baz -- ts usable, xs+zs not 

tests/idris2/linear009/run

@@ -0,0 +1,3 @@
+$1 --no-banner qtt.idr < input
+
+rm -rf build

tests/idris2/reg017/expected

@@ -1,7 +1,7 @@
 1/1: Building lammult (lammult.idr)
 lammult.idr:2:15--2:24:While processing right hand side of badmap at lammult.idr:2:1--3:1:
-When unifying (0 x : ?a) -> ?b and ?a -> ?b
+When unifying (0 _ : ?a) -> ?b and ?a -> ?b
 Mismatch between:
-	(0 x : ?a) -> ?b
+	(0 _ : ?a) -> ?b
 and
 	?a -> ?b

tests/ttimp/basic003/expected

@@ -1,8 +1,8 @@
 Processing as TTImp
 Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!
 Processing as TTC
 Read TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!

tests/ttimp/qtt001/expected

@@ -1,8 +1,8 @@
 Processing as TTImp
 QTT.yaff:14:1--16:1:When elaborating right hand side of Main.dupbad:
 QTT.yaff:14:13--16:1:There are 2 uses of linear name x
-Yaffle> Main.foo : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just x a a))
-Yaffle> Main.bar : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just x a a))
-Yaffle> Main.baz1 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just x a a))
-Yaffle> Main.baz2 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just x a a))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
+Yaffle> Main.bar : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
+Yaffle> Main.baz1 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
+Yaffle> Main.baz2 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
 Yaffle> Bye for now!

tests/ttimp/qtt002/QTT.yaff

@@ -1,26 +0,0 @@
-data Nat : Type where
-     Z : Nat
-     S : Nat -> Nat
-
-plus : Nat -> Nat -> Nat
-plus Z $y = y
-plus (S $k) $y = S (plus k y)
-
-data Vect : Nat -> Type -> Type where
-     Nil : Vect Z $a
-     Cons : $a -> (1 xs : Vect $k $a) -> Vect (S $k) $a
-
-append : (1 xs : Vect $n $a) -> Vect $m $a -> Vect (plus $n $m) $a
-append (Cons $x zs@(Cons $y $ws)) $ys = ?foo -- zs usable, y+ws not
-
-cappend : (1 xs : Vect $n $a) -> Vect $m $a -> Vect (plus $n $m) $a
-cappend $xs $ys
-    = case xs of
-           Nil => ys
-           Cons $x $zs => ?bar -- zs usable, xs not
-
-cappend2 : (1 xs : Vect $n $a) -> Vect $m $a -> Vect (plus $n $m) $a
-cappend2 $xs $ys
-    = case xs of
-           Nil => ys
-           Cons $x $zs => let ts = zs in ?baz -- ts usable, xs+zs not

tests/ttimp/qtt002/expected

@@ -1,6 +0,0 @@
-Processing as TTImp
-Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:21} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:21}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:21})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:21}))) m)) a))))))))))
-Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:76} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:76}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:76})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:76})) m)) a)))))))))
-Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:108} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:108}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:108})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:108}) a) ((Main.Vect ((Main.plus (Main.S {k:108})) m)) a))))))))))
-Yaffle> Bye for now!

tests/ttimp/qtt002/run

@@ -1,3 +0,0 @@
-$1 --yaffle QTT.yaff < input
-
-rm -rf build