[ new ] Quantity for proof in with-clauses (#3415)

* [ new ] Quantity for proof in with-clauses

* [ test ] Add failing tests for quantities of proofs

* [ cleanup ] Match on pairs

* [ test ] Add test for 0 proof in elaborator script

* [ cleanup ] Use `So` and `All` from base in tests

CHANGELOG_NEXT.md

@@ -76,6 +76,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Bind expressions in `do` blocks can now have a type ascription.
   See [#3327](https://github.com/idris-lang/Idris2/issues/3327).
 
+* Added syntax to specifying quantity for proof in with-clause.
+
 ### Compiler changes
 
 * The compiler now differentiates between "package search path" and "package

libs/base/Language/Reflection/TTImp.idr

@@ -171,7 +171,7 @@ mutual
        PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
        WithClause : FC -> (lhs : TTImp) ->
                     (rig : Count) -> (wval : TTImp) -> -- with'd expression (& quantity)
-                    (prf : Maybe Name) -> -- optional name for the proof
+                    (prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity)
                     (flags : List WithFlag) ->
                     List Clause -> Clause
        ImpossibleClause : FC -> (lhs : TTImp) -> Clause
@@ -605,7 +605,8 @@ mutual
   showClause mode (WithClause fc lhs rig wval prf flags cls) -- TODO print flags
       = unwords
       [ show lhs, "with"
-      , showCount rig $ maybe id (\ nm => (++ " proof \{show nm}")) prf
+        -- TODO: remove `the` after fix idris-lang/Idris2#3418
+      , showCount rig $ maybe id (the (_ -> _) $ \(rg, nm) => (++ " proof \{showCount rg $ show nm}")) prf
                       $ showParens True (show wval)
       , "{", joinBy "; " (assert_total $ map (showClause mode) cls), "}"
       ]

src/Idris/Desugar.idr

@@ -926,7 +926,7 @@ mutual
     {auto m : Ref MD Metadata} ->
     {auto o : Ref ROpts REPLOpts} ->
     List Name -> PWithProblem ->
-    Core (RigCount, RawImp, Maybe Name)
+    Core (RigCount, RawImp, Maybe (RigCount, Name))
   desugarWithProblem ps (MkPWithProblem rig wval mnm)
     = (rig,,mnm) <$> desugar AnyExpr ps wval
 

src/Idris/Parser.idr

@@ -1222,8 +1222,9 @@ withProblem fname col indents
   = do rig <- multiplicity fname
        start <- mustWork $ bounds (decoratedSymbol fname "(")
        wval <- bracketedExpr fname start indents
-       prf <- optional (decoratedKeyword fname "proof"
-              *> UN . Basic <$> decoratedSimpleBinderName fname)
+       prf <- optional $ do
+                decoratedKeyword fname "proof"
+                pure (!(multiplicity fname), UN $ Basic !(decoratedSimpleBinderName fname))
        pure (MkPWithProblem rig wval prf)
 
 mutual

src/Idris/REPL.idr

@@ -224,11 +224,12 @@ printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw)
     = do lhs <- pterm $ map defaultKindedName lhsraw -- hack
          wval <- pterm $ map defaultKindedName wvraw -- hack
          cs <- traverse (printClause l (i + 2)) csraw
-         pure (relit l ((pack (replicate i ' ')
+         pure (relit l (pack (replicate i ' ')
                 ++ show lhs
-                ++ " with " ++ elimSemi "0 " "1 " (const "") rig ++ "(" ++ show wval ++ ")"
-                ++ maybe "" (\ nm => " proof " ++ show nm) prf
-                ++ "\n"))
+                ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")"
+                   -- TODO: remove `the` after fix idris-lang/Idris2#3418
+                ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf
+                ++ "\n")
                ++ showSep "\n" cs)
 printClause l i (ImpossibleClause _ lhsraw)
     = do lhs <- pterm $ map defaultKindedName lhsraw -- hack

src/Idris/Syntax.idr

@@ -342,7 +342,7 @@ mutual
     constructor MkPWithProblem
     withRigCount : RigCount
     withRigValue : PTerm' nm
-    withRigProof : Maybe Name -- This ought to be a `Basic` username
+    withRigProof : Maybe (RigCount, Name) -- This ought to be a `Basic` username
 
   public export
   PClause : Type

src/TTImp/Parser.idr

@@ -522,7 +522,9 @@ mutual
            symbol "("
            wval <- expr fname indents
            symbol ")"
-           prf <- optional (keyword "proof" *> name)
+           prf <- optional $ do
+                    keyword "proof"
+                    pure (!(getMult !multiplicity), !name)
            ws <- nonEmptyBlock (clause (S withArgs) fname)
            end <- location
            let fc = MkFC fname start end

src/TTImp/ProcessDef.idr

@@ -600,7 +600,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
                       Just _  =>
                        let fc = emptyFC in
                        let refl = IVar fc (NS builtinNS (UN $ Basic "Refl")) in
-                       [(mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)]
+                       [(map snd mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)]
 
          let rhs_in = gapply (IVar vfc wname)
                     $ map (\ nm => (Nothing, IVar vfc nm)) envns
@@ -633,7 +633,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
     mkExplicit (b :: env) = b :: mkExplicit env
 
     bindWithArgs :
-       (rig : RigCount) -> (wvalTy : Term xs) -> Maybe (Name, Term xs) ->
+       (rig : RigCount) -> (wvalTy : Term xs) -> Maybe ((RigCount, Name), Term xs) ->
        (wvalEnv : Env Term xs) ->
        Core (ext : List Name
          ** ( Env Term (ext ++ xs)
@@ -657,7 +657,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
 
       in pure (wargs ** (scenv, var, binder))
 
-    bindWithArgs {xs} rig wvalTy (Just (name, wval)) wvalEnv = do
+    bindWithArgs {xs} rig wvalTy (Just ((rigPrf, name), wval)) wvalEnv = do
       defs <- get Ctxt
 
       let eqName = NS builtinNS (UN $ Basic "Equal")
@@ -689,7 +689,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
 
           binder : Term (wargs ++ xs) -> Term xs
                  := \ t => Bind vfc wargn (Pi vfc rig Explicit wvalTy)
-                         $ Bind vfc name  (Pi vfc rig Implicit eqTy) t
+                         $ Bind vfc name  (Pi vfc rigPrf Implicit eqTy) t
 
       pure (wargs ** (scenv, var, binder))
 

src/TTImp/TTImp.idr

@@ -427,7 +427,7 @@ mutual
        PatClause : FC -> (lhs : RawImp' nm) -> (rhs : RawImp' nm) -> ImpClause' nm
        WithClause : FC -> (lhs : RawImp' nm) ->
                     (rig : RigCount) -> (wval : RawImp' nm) -> -- with'd expression (& quantity)
-                    (prf : Maybe Name) -> -- optional name for the proof
+                    (prf : Maybe (RigCount, Name)) -> -- optional name for the proof
                     (flags : List WithFlag) ->
                     List (ImpClause' nm) -> ImpClause' nm
        ImpossibleClause : FC -> (lhs : RawImp' nm) -> ImpClause' nm
@@ -441,8 +441,9 @@ mutual
        = show lhs ++ " = " ++ show rhs
     show (WithClause fc lhs rig wval prf flags block)
        = show lhs
-       ++ " with (" ++ show rig ++ " " ++ show wval ++ ")"
-       ++ maybe "" (\ nm => " proof " ++ show nm) prf
+       ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")"
+          -- TODO: remove `the` after fix idris-lang/Idris2#3418
+       ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf
        ++ "\n\t" ++ show block
     show (ImpossibleClause fc lhs)
        = show lhs ++ " impossible"
@@ -518,7 +519,7 @@ mutual
 
 
 export
-mkWithClause : FC -> RawImp' nm -> List1 (RigCount, RawImp' nm, Maybe Name) ->
+mkWithClause : FC -> RawImp' nm -> List1 (RigCount, RawImp' nm, Maybe (RigCount, Name)) ->
                List WithFlag -> List (ImpClause' nm) -> ImpClause' nm
 mkWithClause fc lhs ((rig, wval, prf) ::: []) flags cls
   = WithClause fc lhs rig wval prf flags cls

tests/idris2/with/with012/WithProof0.idr

@@ -0,0 +1,20 @@
+module WithProof0
+
+%default total
+
+%hide List.filter
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+
+filterSquared : (p : a -> Bool) -> (xs : List a) ->
+                filter p (filter p xs) === filter p xs
+filterSquared p [] = Refl
+filterSquared p (x :: xs) with (p x) proof 0 eq
+  filterSquared p (x :: xs) | False = filterSquared p xs -- easy
+  filterSquared p (x :: xs) | True
+    = rewrite eq in cong (x ::) (filterSquared p xs)

tests/idris2/with/with012/WithProof0ElabFail.idr

@@ -0,0 +1,26 @@
+module WithProof0ElabFail
+
+import Data.So
+import Data.List.Quantifiers
+import Language.Reflection
+
+%default total
+
+%language ElabReflection
+
+%hide List.filter
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+failing "While processing right hand side of with block in allFilter. prf is not accessible in this context"
+  %runElab declare `[
+    allFilter : (p : a -> Bool) -> (xs : List a) -> All (So . p) (filter p xs)
+    allFilter p [] = []
+    allFilter p (x :: xs) with (p x) proof 0 prf
+      allFilter p (x :: xs) | False = allFilter p xs
+      allFilter p (x :: xs) | True = eqToSo prf :: allFilter p xs
+  ]

tests/idris2/with/with012/WithProof0Fail.idr

@@ -0,0 +1,21 @@
+module WithProof0Fail
+
+import Data.So
+import Data.List.Quantifiers
+
+%default total
+
+%hide List.filter
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+failing "While processing right hand side of with block in allFilter. prf is not accessible in this context"
+  allFilter : (p : a -> Bool) -> (xs : List a) -> All (So . p) (filter p xs)
+  allFilter p [] = []
+  allFilter p (x :: xs) with (p x) proof 0 prf
+    allFilter p (x :: xs) | False = allFilter p xs
+    allFilter p (x :: xs) | True = eqToSo prf :: allFilter p xs

tests/idris2/with/with012/WithProof1.idr

@@ -0,0 +1,23 @@
+module WithProof1
+
+%default total
+
+%hide List.filter
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+consumeEq : (1 _ : x === y) -> ()
+consumeEq Refl = ()
+
+filterSquared : (p : a -> Bool) -> (xs : List a) ->
+                filter p (filter p xs) === filter p xs
+filterSquared p [] = Refl
+filterSquared p (x :: xs) with (p x) proof 1 eq
+  filterSquared p (x :: xs) | False = case consumeEq eq of
+    () => filterSquared p xs
+  filterSquared p (x :: xs) | True = case consumeEq eq of
+    () => rewrite eq in cong (x ::) (filterSquared p xs)

tests/idris2/with/with012/WithProof1Fail.idr

@@ -0,0 +1,19 @@
+module WithProof1Fail
+
+%default total
+
+%hide List.filter
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+failing "While processing right hand side of with block in filterSquared. There are 0 uses of linear name eq"
+  filterSquared : (p : a -> Bool) -> (xs : List a) ->
+                  filter p (filter p xs) === filter p xs
+  filterSquared p [] = Refl
+  filterSquared p (x :: xs) with (p x) proof 1 eq
+    filterSquared p (x :: xs) | False = filterSquared p xs
+    filterSquared p (x :: xs) | True = filterSquared p xs

tests/idris2/with/with012/expected

@@ -0,0 +1,5 @@
+1/1: Building WithProof0 (WithProof0.idr)
+1/1: Building WithProof1 (WithProof1.idr)
+1/1: Building WithProof0Fail (WithProof0Fail.idr)
+1/1: Building WithProof1Fail (WithProof1Fail.idr)
+1/1: Building WithProof0ElabFail (WithProof0ElabFail.idr)

tests/idris2/with/with012/run

@@ -0,0 +1,7 @@
+. ../../../testutils.sh
+
+check WithProof0.idr
+check WithProof1.idr
+check WithProof0Fail.idr
+check WithProof1Fail.idr
+check WithProof0ElabFail.idr