Refactoring Velvet macros (#20)

* fix macros

* fix macros

* fix macros

* add comment on VelvetM.extract

* add some examples containing continue and break

* remove debug info

* fix PBT

---------

Co-authored-by: Vexoben <Vexoben@gmail.com>
Co-authored-by: zqy1018 <zqy1018@hotmail.com>

Author: 3 people

CaseStudies/Cashmere/Syntax_Cashmere.lean

@@ -297,6 +297,7 @@ elab_rules : command
       ret := ret
       pre := pre
       post := post
+      modIds := #[]
     }
     return (defCmd, obligation)
   elabCommand defCmd

CaseStudies/Extension.lean

@@ -26,6 +26,7 @@ initialize
 
 structure VelvetObligation where
   binderIdents : TSyntaxArray `Lean.Parser.Term.bracketedBinder
+  modIds : Array Ident
   ids : Array Ident
   retId : Ident
   ret : Term
@@ -48,8 +49,9 @@ initialize velvetObligations :
 
 /-- Storing slightly more information than `VelvetObligation`.  -/
 structure VelvetTestingCtx extends VelvetObligation where
-  newIds : Array Ident
+  /-- The _original_ (i.e., without `Old` suffix) binders of mutable arguments. -/
   modBinders : Array (TSyntax `Lean.Parser.Term.bracketedBinder)
+  retType : Term
 deriving Inhabited
 
 abbrev VelvetTestingContextMap := Std.HashMap Name VelvetTestingCtx

CaseStudies/TestingUtil.lean

@@ -23,8 +23,8 @@ def deriveDecidableNatUpperBound (tms : List <| TSyntax `term)
       constructor
       next => (intro $h:ident ; intros ; apply $h:ident <;> (try split_ands) <;> (solve
           | omega
-          | aesop))
-      next => aesop)
+          | grind))
+      next => grind)
 
 macro "decidable_by_nat_upperbound" "[" tms:term,* "]" : term => do
   let res ← deriveDecidableNatUpperBound tms.getElems.toList

CaseStudies/Velvet/Syntax.lean

@@ -88,7 +88,8 @@ private def toBracketedBinderArrayLeafny (stx : Array (TSyntax `leafny_binder))
       let fb ← `(bracketedBinder| ($id : $tp:term))
       binders := binders.push fb
     | `(leafny_binder| (mut $id:ident : $tp:term)) => do
-      let fb ← `(bracketedBinder| ($id : $tp:term))
+      let idOld := mkIdent <| id.getId.appendAfter "Old"
+      let fb ← `(bracketedBinder| ($idOld : $tp:term))
       binders := binders.push fb
     | _ => throwError "unexpected syntax in leafny binder: {b}"
   return binders
@@ -118,7 +119,8 @@ def getIds (stx : Array (TSyntax `leafny_binder)) : MetaM (Array Ident) := do
   for b in stx do
     match b with
     | `(leafny_binder| (mut $id:ident : $_:term)) => do
-      ids := ids.push id
+      let idOld := mkIdent <| id.getId.appendAfter "Old"
+      ids := ids.push idOld
     | `(leafny_binder| ($id:ident : $_:term)) => do
       ids := ids.push id
     | _ => throwError "unexpected syntax in leafny binder: {b}"
@@ -139,15 +141,19 @@ partial def expandLeafnyDoSeqItem (modIds : Array Ident) (stx : doSeqItem) : Ter
   | `(Term.doSeqItem| $stx ;) => expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| $stx:doElem)
   | `(Term.doSeqItem| return) => expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| return ())
   | `(Term.doSeqItem| return $t) =>
-    let mut ret <- `(term| ())
-    for modId in modIds do
-      ret <- `(term| ⟨$modId, $ret⟩)
-    return #[<-`(Term.doSeqItem| return ⟨$t, $ret⟩)]
+    let ret <-
+      if modIds.size = 0 then
+      `(term| $t)
+     else
+       `(term| ($t, $[$modIds:term],*))
+    return #[<-`(Term.doSeqItem| return $ret)]
   | `(Term.doSeqItem| pure $t) =>
-    let mut ret <- `(term| ())
-    for modId in modIds do
-      ret <- `(term| ⟨$modId, $ret⟩)
-    return #[<-`(Term.doSeqItem| pure ⟨$t, $ret⟩)]
+    let ret <-
+      if modIds.size = 0 then
+      `(term| $t)
+     else
+       `(term| ($t, $[$modIds:term],*))
+    return #[<-`(Term.doSeqItem| pure $ret)]
   | `(Term.doSeqItem| if $h:ident : $t:term then $thn:doSeq else $els:doSeq) =>
     let thn <- expandLeafnyDoSeq modIds thn
     let els <- expandLeafnyDoSeq modIds els
@@ -227,6 +233,13 @@ private def Array.andList (ts : Array (TSyntax `term)) : TermElabM (TSyntax `ter
       t <- `(term| $t' ∧ $t)
     return t
 
+private def addPreludeToPreCond (pre : Term) (modIds : Array Ident) : CoreM (TSyntax `term) := do
+  let mut pre := pre
+  for modId in modIds do
+    let modIdOld := mkIdent <| modId.getId.appendAfter "Old"
+    pre ← `(term| let $modId:ident := $modIdOld:ident; $pre)
+  pure pre
+
 elab_rules : command
   | `(command|
   method $name:ident $binders:leafny_binder* return ( $retId:ident : $type:term )
@@ -244,17 +257,22 @@ elab_rules : command
 
     let mut mods := #[]
     for modId in modIds do
-      -- let modIdOld := mkIdent <| modId.getId.appendAfter "Old"
+      let modIdOld := mkIdent <| modId.getId.appendAfter "Old"
       -- let modOld <- `(Term.doSeqItem| let $modIdOld:ident := $modId:ident)
-      let mod <- `(Term.doSeqItem| let mut $modId:ident := $modId:ident)
+      let mod <- `(Term.doSeqItem| let mut $modId:ident := $modIdOld:ident)
       mods := mods.push mod
     let mutTypes ← getMutTypes binders
-    let mut retType <- `(Unit)
-    for mutType in mutTypes, modId in modIds do
-      retType <- `(($modId:ident : $mutType) × $retType)
+    let mut retType : Term <- `($type)
+    if mutTypes.size != 0 then
+      let lastMutType := mutTypes[mutTypes.size - 1]!
+      let mutTypes := mutTypes.pop.reverse
+      let mut mutTypeProd := lastMutType
+      for mutType in mutTypes do
+        mutTypeProd <- `($mutType × $mutTypeProd)
+      retType <- `($retType × $mutTypeProd)
     let defCmd <- `(command|
       set_option linter.unusedVariables false in
-      def $name $bindersIdents* : VelvetM (($retId:ident : $type) × $retType) := do $mods* $doSeq*
+      def $name $bindersIdents* : VelvetM $retType:term := do $mods* $doSeq*
       $suf:suffix)
     -- let lemmaName := mkIdent <| name.getId.appendAfter "_correct"
 
@@ -264,12 +282,13 @@ elab_rules : command
     let post <- ens.andListWithName ensName
 
     let namelessPre <- req.andList
+    let namelessPre <- addPreludeToPreCond namelessPre modIds
     let namelessPost <- ens.andList
 
-    let mut ret <- `(term| ())
-    for modId in modIds do
-      let modId := mkIdent <| modId.getId.appendAfter "New"
-      ret <- `(term| ⟨$modId, $ret⟩)
+    let ret <- if modIds.size = 0 then
+      `(term| $retId)
+    else
+      `(term| ($retId, $[$modIds:term],*))
 
     let ids ← getIds binders
     let obligation : VelvetObligation := {
@@ -279,17 +298,16 @@ elab_rules : command
       ret := ret
       pre := pre
       post := post
+      modIds := modIds
     }
-    let newIds := modIds.map (fun x => Lean.mkIdent <| x.getId.appendAfter "New")
-    let modBinders ← newIds.zip mutTypes |>.mapM fun (newId, mutType) =>
-      `(bracketedBinder| ($newId : $mutType))
-    return (defCmd, obligation, { obligation with pre := namelessPre , post := namelessPost , modBinders , newIds })
+    let modBinders ← modIds.zip mutTypes |>.mapM fun (mId, mutType) =>
+      `(bracketedBinder| ($mId : $mutType))
+    return (defCmd, obligation, { obligation with pre := namelessPre , post := namelessPost , modBinders , retType := type })
   elabCommand defCmd
   velvetObligations.modify (·.insert name.getId obligation)
   velvetTestingContextMap.modify (·.insert name.getId testingCtx)
 
 notation "{" P "}" c "{" v "," Q "}" => triple P c (fun v => Q)
-
 /-
 example:
 open TotalCorrectness DemonicChoice
@@ -305,22 +323,24 @@ elab_rules : command
     let .some obligation := ctx[name.getId]? | throwError "no obligation found"
     let bindersIdents := obligation.binderIdents
     let ids := obligation.ids
-    let retId := obligation.retId
+    -- let retId := obligation.retId
     let ret := obligation.ret
-    let pre := obligation.pre
+    let pre ← liftCoreM <| addPreludeToPreCond obligation.pre obligation.modIds
     let post := obligation.post
     let lemmaName := mkIdent <| name.getId.appendAfter "_correct"
     -- let proof <- withRef tkp ``()
     let proofSeq ← withRef tkp `(tacticSeq|
       unfold $name
       ($proof))
+
     let thmCmd <- withRef tkp `(command|
       @[loomSpec]
       lemma $lemmaName $bindersIdents* :
       triple
         $pre
         ($name $ids*)
-        (fun ⟨$retId, $ret⟩ => $post) := by $proofSeq $suf:suffix)
+        (fun $ret => $post) := by $proofSeq $suf:suffix)
+    trace[Loom] "{thmCmd}"
     Command.elabCommand thmCmd
     velvetObligations.modify (·.erase name.getId)
 
@@ -358,7 +378,7 @@ def elabDefiningDecidableInstancesForVelvetSpec (nameRaw : Ident)
   let (target, suffix, binders) :=
     if pre?
     then (ctx.pre, "PreDecidable", bindersIdents)
-    else (ctx.post, "PostDecidable", bindersIdents ++ ctx.modBinders)
+    else (ctx.post, "PostDecidable", bindersIdents ++ ctx.modBinders |>.push ⟨mkExplicitBinder ctx.retId ctx.retType⟩)
   let decidableInstName := name.appendAfter suffix
   -- let proof := tac.getD (← `(term| (by infer_instance) ))
   let tac := tac.getD (← `(Lean.Parser.Tactic.tacticSeq| skip ))
@@ -394,7 +414,7 @@ elab_rules : command
   let bindersIdents := ctx.binderIdents
   let bundle (pre? : Bool) := if pre?
     then (ctx.pre, name.appendAfter "PreDecidable", ids)
-    else (ctx.post, name.appendAfter "PostDecidable", ids ++ ctx.newIds)
+    else (ctx.post, name.appendAfter "PostDecidable", ids ++ ctx.modIds |>.push retId)
   let decideTerm bundled : CommandElabM (TSyntax `term) := do
     let (target, instname, args) := bundled
     try
@@ -404,7 +424,7 @@ elab_rules : command
       `(term| ($(mkIdent ``decide) ($target)))
   let matcherTerm ← `(term|
       match ($(Syntax.mkApp (mkIdent execName) ids)) with
-      | $(mkIdent ``DivM.res) ⟨$retId, $ret⟩ => $(← decideTerm <| bundle false)
+      | $(mkIdent ``DivM.res) $ret => $(← decideTerm <| bundle false)
       | _ => false)
   let ifTerm ← `(term| if $(← decideTerm <| bundle true) then $matcherTerm else true)
   let testerName := name.appendAfter "Tester"

CaseStudies/Velvet/VelvetExamples/Examples.lean

@@ -56,25 +56,23 @@ attribute [grind] Array.multiset_swap
 method insertionSort
   (mut arr: Array Int) return (u: Unit)
   require 1 ≤ arr.size
-  ensures forall i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arrNew[i]! ≤ arrNew[j]!
-  ensures arr.toMultiset = arrNew.toMultiset
+  ensures forall i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arr[i]! ≤ arr[j]!
+  ensures arr.toMultiset = arrOld.toMultiset
   do
-    let arr₀ := arr
-    let arr_size := arr.size
     let mut n := 1
     while n ≠ arr.size
-    invariant arr.size = arr_size
+    invariant arr.size = arrOld.size
     invariant 1 ≤ n ∧ n ≤ arr.size
     invariant forall i j, 0 ≤ i ∧ i < j ∧ j <= n - 1 → arr[i]! ≤ arr[j]!
-    invariant arr.toMultiset = arr₀.toMultiset
+    invariant arr.toMultiset = arrOld.toMultiset
     done_with n = arr.size
     do
       let mut mind := n
       while mind ≠ 0
-      invariant arr.size = arr_size
+      invariant arr.size = arrOld.size
       invariant mind ≤ n
       invariant forall i j, 0 ≤ i ∧ i < j ∧ j ≤ n ∧ j ≠ mind → arr[i]! ≤ arr[j]!
-      invariant arr.toMultiset = arr₀.toMultiset
+      invariant arr.toMultiset = arrOld.toMultiset
       done_with mind = 0
       do
         if arr[mind]! < arr[mind - 1]! then
@@ -119,14 +117,13 @@ method sqrt (x: ℕ) return (res: ℕ)
   do
     if x = 0 then
       return 0
-    else
-      let mut i := 0
-      while i * i ≤ x
-      invariant ∀ j, j < i → j * j ≤ x
-      done_with x < i * i
-      do
-        i := i + 1
-      return i - 1
+    let mut i := 0
+    while i * i ≤ x
+    invariant ∀ j, j < i → j * j ≤ x
+    done_with x < i * i
+    do
+      i := i + 1
+    return i - 1
 
 set_option auto.smt.trust true
 set_option auto.smt true

CaseStudies/Velvet/VelvetExamples/Examples_Total.lean

@@ -54,8 +54,8 @@ method insertionSort(arr: array<int>)
 method insertionSort_total
   (mut arr: Array Int) return (u: Unit)
   require 1 ≤ arr.size
-  ensures forall i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arrNew[i]! ≤ arrNew[j]!
-  ensures arr.toMultiset = arrNew.toMultiset
+  ensures forall i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arr[i]! ≤ arr[j]!
+  ensures arrOld.toMultiset = arr.toMultiset
   do
     let arr₀ := arr
     let arr_size := arr.size

CaseStudies/Velvet/VelvetExamples/GCD.lean

@@ -22,7 +22,7 @@ method gcd (a : Nat) (b : Nat) return (res : Nat)
     else
       let remainder := a % b
       let result ← gcd b remainder
-      return result.1
+      return result
   termination_by b
   decreasing_by
     apply Nat.mod_lt

CaseStudies/Velvet/VelvetExamples/Recursion.lean

@@ -21,7 +21,7 @@ method simple_recursion (x : Nat) return (res: Nat)
       return 0
     else
       let pre_res ← simple_recursion (x - 1)
-      return pre_res.1 + 1
+      return pre_res + 1
 
 prove_correct simple_recursion by
   loom_solve
@@ -45,8 +45,8 @@ method pickGreaterN (n: Nat) return (res: Nat)
       return 0
     else
       let pre_res ← pickGreaterN (n - 1)
-      let pre_res_big ← pickGreater pre_res.1
-      return pre_res_big.1
+      let pre_res_big ← pickGreater pre_res
+      return pre_res_big
 
 prove_correct pickGreaterN by
   loom_solve
@@ -69,11 +69,11 @@ method calc_fact (n: Nat) return (res: Nat)
       let pre_res_n ← calc_fact (n - 1)
       while i < n
         invariant i <= n
-        invariant i * pre_res_n.1 = ans
+        invariant i * pre_res_n = ans
         decreasing n - i
         do
           let pre_res ← calc_fact (n - 1)
-          ans := ans + pre_res.1
+          ans := ans + pre_res
           i := i + 1
       return ans
 
@@ -101,7 +101,7 @@ method SimpleList (li: List Nat) return (res: Nat)
     match li with
     | x :: xs =>
       let prev ← SimpleList xs
-      return (prev.1 + x)
+      return (prev + x)
     | [] =>
       return 1
 
@@ -139,10 +139,10 @@ method insertTree (tree: mt1 Nat) (elem: Nat) return (res: mt1 Nat)
         else
           if el < elem then
             let right_res ← insertTree r elem
-            pure (.Node l right_res.1 el)
+            pure (.Node l right_res el)
           else
             let left_res ← insertTree l elem
-            pure (.Node left_res.1 r el)
+            pure (.Node left_res r el)
       | .Leaf el =>
         if el = elem then
           pure tree
@@ -170,10 +170,10 @@ method complex_measure_binsearch (l : Nat) (r: Nat) (x: Nat) return (res: Nat)
       let m := l + (r - l) / 2
       if m * m ≤ x then
         let pre_res_l ← complex_measure_binsearch m r x
-        return pre_res_l.1
+        return pre_res_l
       else
         let pre_res_r ← complex_measure_binsearch l m x
-        return pre_res_r.1
+        return pre_res_r
 
 prove_correct complex_measure_binsearch by
   loom_solve
@@ -199,7 +199,7 @@ method pow2 (n: Nat) return (res: Nat)
         decreasing n - i
         do
           let pre_res ← pow2 i
-          ans := ans + pre_res.1
+          ans := ans + pre_res
           i := i + 1
       return ans