feat(Rewriter): introduce eraseOp!/replaceValue! and clear remaining pass sorries

Veir/Passes/CSE.lean

@@ -127,7 +127,6 @@ def key? (ctx : IRContext OpCode) (op : OperationPtr) : Option Key := do
       return ordinaryKey ctx op kind
   | _ => none
 
-set_option warn.sorry false in
 /-- Perform CSE on a single BB: Walk the operations, building up a
     hash of available values. For any operation whose value is already
     available, replace it with the earlier one. -/
@@ -143,14 +142,13 @@ def processBlock
     if let some key := key? ctx.raw op then
         match available[key]? with
         | some earlier =>
-            ctx := WfRewriter.replaceValue ctx (op.getResult 0) (earlier.getResult 0) sorry sorry sorry
-            ctx := WfRewriter.eraseOp ctx op sorry sorry sorry
+            ctx := WfRewriter.replaceValue! ctx (op.getResult 0) (earlier.getResult 0)
+            ctx := WfRewriter.eraseOp! ctx op
         | none =>
             available := available.insert key op
     current := next
   return ctx
 
-set_option warn.sorry false in
 def processAllBlocks (ctx : WfIRContext OpCode) :
     WfIRContext OpCode := Id.run do
   let mut ctx := ctx

Veir/Passes/Canonicalize.lean

@@ -16,7 +16,6 @@ def isConstOperand (ctx : IRContext OpCode) (v : ValuePtr) : Bool :=
   | some defOp => (defOp.getOpType! ctx).isConstantLike
   | none => false
 
-set_option warn.sorry false in
 def commutativeConstantRHS (rewriter : PatternRewriter OpCode) (op : OperationPtr)
     (_ : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do
   let opType := op.getOpType! rewriter.ctx.raw
@@ -28,9 +27,9 @@ def commutativeConstantRHS (rewriter : PatternRewriter OpCode) (op : OperationPt
   if reordered == operands then return rewriter
   let resultTypes := op.getResultTypes! rewriter.ctx.raw
   let properties := op.getProperties! rewriter.ctx.raw opType
-  let (rewriter, newOp) ← rewriter.createOp opType resultTypes reordered
-    #[] #[] properties (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! opType resultTypes reordered
+    #[] #[] properties (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
 /-! ## Pass implementation -/
 

Veir/Passes/CastsReconciliation/Reconciliation.lean

@@ -29,46 +29,44 @@ def isPreservingIntegerTypeRoundTrip (inputType interType : TypeAttr) : Bool :=
   | _, _ => false
 
 /- Reconciles round-trip casts of the form X->Y->X if allowed for these types by `legal X Y` -/
-set_option warn.sorry false in
 def reconcilePairingCast (legal : TypeAttr → TypeAttr → Bool) (rewriter : PatternRewriter OpCode)
-    (op : OperationPtr) (opInBounds : op.InBounds rewriter.ctx.raw) :
+    (op : OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
-  let some cast := matchCastOp op rewriter.ctx.raw | return rewriter
+  let some _ := matchCastOp op rewriter.ctx.raw | return rewriter
   let input := op.getOperand! rewriter.ctx.raw 0
   /- Note that reconciliation matches on the second casting operation, so the input type of this op would be the intermediate type -/
   let interType := input.getType! rewriter.ctx.raw
   let resultType := ((op.getResult 0).get! rewriter.ctx.raw).type
   /- If the operand's parent is a cast operation -/
   let .opResult op' := input | return rewriter
-  let some cast := matchCastOp op'.op rewriter.ctx.raw | return rewriter
+  let some _ := matchCastOp op'.op rewriter.ctx.raw | return rewriter
   let parentInput := (op'.op.getOperand! rewriter.ctx.raw 0)
   /- And the result's type coincides with the parent operation operand's type -/
   let inputType := parentInput.getType! rewriter.ctx.raw
   if resultType ≠ inputType then return rewriter
   /- And the reconciliation is legal -/
   if ¬ legal inputType interType then return rewriter
   /- Replace the initial operation's output with the parent operations input -/
-  let rewriter := rewriter.replaceValue (op.getResult 0) parentInput sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) parentInput
   /- Erase the redundant cast operation -/
-  let rewriter ← rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.eraseOp! op
   /- If unused and side-effect-free, erase the parent cast operation as well.
     These need to be erased in this order, otherwise the parent operation will always be used. -/
   if ¬ op'.op.hasUses! rewriter.ctx.raw && ¬ op'.op.hasSideEffects rewriter.ctx.raw then
-    rewriter.eraseOp op'.op sorry sorry sorry
+    return rewriter.eraseOp! op'.op
   else
     return rewriter
 
-set_option warn.sorry false in
 def reconcileIdentityCast (rewriter : PatternRewriter OpCode) (op : OperationPtr)
-  (opInBounds : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do
-  let some cast := matchCastOp op rewriter.ctx.raw | return rewriter
+  (_ : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do
+  let some _ := matchCastOp op rewriter.ctx.raw | return rewriter
   /- get the input and output types -/
   let input := op.getOperand! rewriter.ctx.raw 0
   let inputType := input.getType! rewriter.ctx.raw
   let resultType := ((op.getResult 0).get! rewriter.ctx.raw).type
   if inputType ≠ resultType then return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) input sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) input
+  return rewriter.eraseOp! op
 
 def CastReconcilePass.impl (ctx : WfIRContext OpCode) (op : OperationPtr) (_ : op.InBounds ctx.raw) :
     ExceptT String IO (WfIRContext OpCode) := do

Veir/Passes/DCE/dce.lean

@@ -6,12 +6,11 @@ namespace Veir
 
 /-! We implement a dead code elimination pass. -/
 
-set_option warn.sorry false in
 def eliminateDeadOp (rewriter: PatternRewriter OpCode) (op: OperationPtr)
-    (opInBounds : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do
+    (_ : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do
   /- delete operations that are not used and have no side effects -/
   if ¬ op.hasUses! rewriter.ctx.raw && ¬ op.hasSideEffects rewriter.ctx.raw then
-    rewriter.eraseOp op sorry sorry sorry
+    return rewriter.eraseOp! op
   else
     return rewriter
 

Veir/Passes/InstCombine.lean

@@ -13,7 +13,6 @@ namespace Veir
 
 /-! ## Pattern Rewrites -/
 
-set_option warn.sorry false in
 /-- Rewrites `x * 2` to `x + x`. -/
 def mulITwoToAddi (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -23,15 +22,14 @@ def mulITwoToAddi (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.
     | return rewriter
   if cst.value ≠ 2 then
     return rewriter
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .add) #[lhs.getType! rewriter.ctx.raw] #[lhs, lhs]
-    #[] #[] properties (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .add) #[lhs.getType! rewriter.ctx.raw] #[lhs, lhs]
+    #[] #[] properties (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
-set_option warn.sorry false in
 /-- Rewrites `x * 0` to `0`. -/
 def mulIZeroToCst (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
-  let some (lhs, rhs, properties) := matchMuli op rewriter.ctx
+  let some (lhs, rhs, _) := matchMuli op rewriter.ctx
     | return rewriter
   let some cst := matchConstantIntVal rhs rewriter.ctx
     | return rewriter
@@ -40,11 +38,10 @@ def mulIZeroToCst (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.
   let .integerType type := (lhs.getType! rewriter.ctx.raw).val
     | return rewriter
   let cstProp := LLVMConstantProperties.mk (.integer (IntegerAttr.mk 0 type))
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
-    #[] #[] cstProp (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
+    #[] #[] cstProp (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
-set_option warn.sorry false in
 /-- Rewrites `x + 0` to `x`. -/
 def addiZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -54,10 +51,9 @@ def addiZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.In
     | return rewriter
   if cst.value ≠ 0 then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x * 1` to `x`. -/
 def mulIOneToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -67,10 +63,9 @@ def mulIOneToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InB
     | return rewriter
   if cst.value ≠ 1 then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x - 0` to `x`. -/
 def subiZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -80,10 +75,9 @@ def subiZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.In
     | return rewriter
   if cst.value ≠ 0 then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x - x` to `0`. -/
 def subiSelfToZero (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -94,22 +88,20 @@ def subiSelfToZero (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op
   let .integerType type := (lhs.getType! rewriter.ctx.raw).val
     | return rewriter
   let cstProp := LLVMConstantProperties.mk (.integer (IntegerAttr.mk 0 type))
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
-    #[] #[] cstProp (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
+    #[] #[] cstProp (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
-set_option warn.sorry false in
 /-- Rewrites `x & x` to `x`. -/
 def andiSelfToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
   let some (lhs, rhs) := matchAndi op rewriter.ctx
     | return rewriter
   if lhs ≠ rhs then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x & 0` to `0`. -/
 def andiZeroToZero (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -122,11 +114,10 @@ def andiZeroToZero (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op
   let .integerType type := (lhs.getType! rewriter.ctx.raw).val
     | return rewriter
   let cstProp := LLVMConstantProperties.mk (.integer (IntegerAttr.mk 0 type))
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
-    #[] #[] cstProp (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
+    #[] #[] cstProp (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
-set_option warn.sorry false in
 /-- Rewrites `x | 0` to `x`. -/
 def oriZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -136,21 +127,19 @@ def oriZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InB
     | return rewriter
   if cst.value ≠ 0 then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x | x` to `x`. -/
 def oriSelfToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
   let some (lhs, rhs, _) := matchOri op rewriter.ctx
     | return rewriter
   if lhs ≠ rhs then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x ^ 0` to `x`. -/
 def xoriZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -160,10 +149,9 @@ def xoriZeroToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.In
     | return rewriter
   if cst.value ≠ 0 then
     return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) lhs
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `x ^ x` to `0`. -/
 def xoriSelfToZero (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
@@ -174,22 +162,20 @@ def xoriSelfToZero (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op
   let .integerType type := (lhs.getType! rewriter.ctx.raw).val
     | return rewriter
   let cstProp := LLVMConstantProperties.mk (.integer (IntegerAttr.mk 0 type))
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
-    #[] #[] cstProp (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .mlir__constant) #[lhs.getType! rewriter.ctx.raw] #[]
+    #[] #[] cstProp (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
-set_option warn.sorry false in
 /-- Rewrites `~~x` to `x`. -/
 def notNotToX (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
     Option (PatternRewriter OpCode) := do
   let some outerNotted := matchNot (op.getResult 0) rewriter.ctx
     | return rewriter
   let some inner := matchNot outerNotted rewriter.ctx
     | return rewriter
-  let rewriter := rewriter.replaceValue (op.getResult 0) inner sorry sorry sorry
-  rewriter.eraseOp op sorry sorry sorry
+  let rewriter := rewriter.replaceValue! (op.getResult 0) inner
+  return rewriter.eraseOp! op
 
-set_option warn.sorry false in
 /-- Rewrites `~(~a & ~b)` to `a | b` (DeMorgan). -/
 /- TODO: the precondition should be strengthened by some hasOneUse() checks -/
 def deMorganAndToOr (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
@@ -206,11 +192,10 @@ def deMorganAndToOr (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : o
     | return rewriter
   let resultType := a.getType! rewriter.ctx.raw
   let orProps : DisjointProperties := { disjoint := false }
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .or) #[resultType] #[a, b]
-    #[] #[] orProps (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .or) #[resultType] #[a, b]
+    #[] #[] orProps (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
-set_option warn.sorry false in
 /-- Rewrites `~(~a | ~b)` to `a & b` (DeMorgan). -/
 /- TODO: the precondition should be strengthened by some hasOneUse() checks -/
 def deMorganOrToAnd (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : op.InBounds rewriter.ctx.raw) :
@@ -226,9 +211,9 @@ def deMorganOrToAnd (rewriter: PatternRewriter OpCode) (op: OperationPtr) (_ : o
   let some b := matchNot orR rewriter.ctx
     | return rewriter
   let resultType := a.getType! rewriter.ctx.raw
-  let (rewriter, newOp) ← rewriter.createOp (.llvm .and) #[resultType] #[a, b]
-    #[] #[] () (some $ .before op) sorry sorry sorry sorry
-  rewriter.replaceOp op newOp sorry sorry sorry sorry sorry
+  let (rewriter, newOp) := rewriter.createOp! (.llvm .and) #[resultType] #[a, b]
+    #[] #[] () (some $ .before op)
+  return rewriter.replaceOp! op newOp
 
 def InstCombinePass.impl (ctx : WfIRContext OpCode) (op : OperationPtr) (_ : op.InBounds ctx.raw) :
     ExceptT String IO (WfIRContext OpCode) := do

Veir/Passes/InstructionSelection/Common.lean

@@ -7,18 +7,16 @@ namespace Veir
   Shared helpers for the RISC-V instruction-selection lowering patterns.
 -/
 
-set_option warn.sorry false in
 /--
   Insert `unrealized_conversion_cast : (typeof v) -> !riscv.reg` before `op`,
   returning the updated rewriter and the register-typed result value.
 -/
 def castToReg (rewriter : PatternRewriter OpCode) (op : OperationPtr) (v : ValuePtr) :
     Option (PatternRewriter OpCode × ValuePtr) := do
-  let (rewriter, castOp) ← rewriter.createOp (.builtin .unrealized_conversion_cast)
-      #[RegisterType.mk] #[v] #[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
+  let (rewriter, castOp) := rewriter.createOp! (.builtin .unrealized_conversion_cast)
+      #[RegisterType.mk] #[v] #[] #[] () (some $ .before op)
   return (rewriter, castOp.getResult 0)
 
-set_option warn.sorry false in
 /--
   Cast the register value `reg` back to `op`'s result type and replace `op` with
   the cast. The target type is read from `op`, so this is type-agnostic (it also
@@ -27,8 +25,8 @@ set_option warn.sorry false in
 def replaceWithReg (rewriter : PatternRewriter OpCode) (op : OperationPtr) (reg : ValuePtr) :
     Option (PatternRewriter OpCode) := do
   let type := ((op.getResult 0).get! rewriter.ctx.raw).type
-  let (rewriter, castOp) ← rewriter.createOp (.builtin .unrealized_conversion_cast)
-      #[type] #[reg] #[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
-  rewriter.replaceOp op castOp sorry sorry sorry sorry sorry
+  let (rewriter, castOp) := rewriter.createOp! (.builtin .unrealized_conversion_cast)
+      #[type] #[reg] #[] #[] () (some $ .before op)
+  return rewriter.replaceOp! op castOp
 
 end Veir