refactor: purify parsing APIs

LeanSAT/External/DimacsLRAT.lean

@@ -59,13 +59,12 @@ def loadProblem (path : System.FilePath) : CommandElabM (Σ n : Nat, Array (Opti
     throwError "The problem line stated there were {numClauses} clauses but there are actually {res.size} (res: {res})"
   return ⟨numVarsSucc, res⟩
 
-def intToLiteralIO {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : IO (Option (Literal (PosFin n))) := do
+def intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Literal (PosFin n)) := do
   if h : x.natAbs < n then
-    if x > 0 then return some (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
-    else return some (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
+    if x > 0 then some (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
+    else some (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
   else
-    IO.println "Given literal {x} is outside of the bounds specified by the number of variables"
-    return none
+    none
 
 /-- `parseProblem` takes in the path of a CNF file and attempts to output a number `n` (indicating the total number
     of variables + 1) along with an Array of `DefaultClause n` Option expressions. This Array should match the
@@ -98,7 +97,7 @@ def parseProblem (path : System.FilePath) : IO (Option (Σ n : Nat, Array (Optio
       let some lit := String.toInt? lit
         | IO.println s!"Clause {c} contains non-int {lit}"; return none
       if h : lit ≠ 0 then
-        let some lit ← intToLiteralIO lit h
+        let some lit := intToLiteralPure lit h
           | return none
         match curClause.insert lit with
         | some updatedClause => curClause := updatedClause

LeanSAT/LRAT/Actions.lean

@@ -46,82 +46,44 @@ def wellFormedAction [Clause α β] : Action β α → Prop
   | addRat _ c p _ _ => Sat.limplies α p c -- Note that `Sat.limplies α p c` is equivalent to `p ∈ toList c` by `limplies_iff_mem` in CNF.lean
   | _ => True
 
-def natLiteralToPosFinLiteralIO {n : Nat} (x : Literal Nat) (x_ne_zero : x.1 ≠ 0) : IO (Option (Literal (PosFin n))) := do
+def natLiteralToPosFinLiteral {n : Nat} (x : Literal Nat) (x_ne_zero : x.1 ≠ 0) : Option (Literal (PosFin n)) := do
   if h : x.1 < n then
-    return some (⟨x.1, ⟨Nat.zero_lt_of_ne_zero x_ne_zero, h⟩⟩, x.2)
+    some (⟨x.1, ⟨Nat.zero_lt_of_ne_zero x_ne_zero, h⟩⟩, x.2)
   else
-    IO.println s!"Given literal {x} is outside of the bounds specified by the number of variables"
-    return none
+    none
 
 /-- Since `IntAction` is a convenient parsing target and `DefaultClauseAction` is a useful Action type for working with default
     clauses, an expected workflow pattern is to parse an external LRAT proof into a list of `IntAction`s, and then use this function
     to convert that list of `IntAction`s to `DefaultClauseAction`s.
 
     This function returns an `Option` type so that `none` can be returned if converting from the `IntAction` to `DefaultClauseAction`
     fails. This can occur if any of the literals in the `IntAction` are 0 or ≥ n. -/
-def intActionToDefaultClauseActionIO (n : Nat) : IntAction → IO (Option (DefaultClauseAction n))
-  | addEmpty cId rupHints => return some $ addEmpty cId rupHints
+def intActionToDefaultClauseAction (n : Nat) : IntAction → Option (DefaultClauseAction n)
+  | addEmpty cId rupHints => some $ addEmpty cId rupHints
   | addRup cId c rupHints => do
-    let c : Array (Option (Literal (PosFin n))) ←
-      c.mapM (fun x => if h : x ≠ 0 then Dimacs.intToLiteralIO x h else return none)
+    let c : Array (Option (Literal (PosFin n))) :=
+      c.map (fun x => if h : x ≠ 0 then Dimacs.intToLiteralPure x h else none)
     if c.contains none then
-      IO.println s!"Failed to convert at least one literal in {c}"
-      return none
+      none
     else
       let c := c.filterMap id
       match Clause.ofArray c with
-      | none => IO.println s!"Clause {c} contains complementary literals"; return none
-      | some c => return some $ addRup cId c rupHints
+      | none => none
+      | some c => some $ addRup cId c rupHints
   | addRat cId c pivot rupHints ratHints => do
     if h : pivot.1 ≠ 0 then
-      let some pivot ← natLiteralToPosFinLiteralIO pivot h
-        | IO.println s!"Failed to turn {pivot} to a literal"; return none
-      let c : Array (Option (Literal (PosFin n))) ←
-        c.mapM (fun x => if h : x ≠ 0 then Dimacs.intToLiteralIO x h else return none)
+      let some pivot := natLiteralToPosFinLiteral pivot h
+        | none
+      let c : Array (Option (Literal (PosFin n))) :=
+        c.map (fun x => if h : x ≠ 0 then Dimacs.intToLiteralPure x h else none)
       if c.contains none then
-        IO.println s!"Failed to convert at least one literal in {c}"
-        return none
+        none
       else
         let c := c.filterMap id
         match Clause.ofArray c with
-        | none => IO.println s!"Clause {c} contains complementary literals"; return none
-        | some c => return some $ addRat cId c pivot rupHints ratHints
+        | none => none
+        | some c => some $ addRat cId c pivot rupHints ratHints
     else
-      return none
-  | del ids => return some $ del ids
+      none
+  | del ids => some $ del ids
 
-open Lean Parser Elab Command
-
-/-- Since `IntAction` is a convenient parsing target and `DefaultClauseAction` is a useful Action type for working with default
-    clauses, an expected workflow pattern is to parse an external LRAT proof into a list of `IntAction`s, and then use this function
-    to convert that list of `IntAction`s to `DefaultClauseAction`s.
-
-    This function throws an error if any of the literals in the `IntAction` are 0 or ≥ n. -/
-def intActionToDefaultClauseAction (n : Nat) : IntAction → CommandElabM (DefaultClauseAction n)
-  | addEmpty cId rupHints => return addEmpty cId rupHints
-  | addRup cId c rupHints => do
-    let c : Array (Option (Literal (PosFin n))) ←
-      c.mapM (fun x => if h : x ≠ 0 then Dimacs.intToLiteralIO x h else throwError "Parsing error")
-    if c.contains none then
-      throwError "Failed to convert at least one literal in {c}"
-    else
-      let c := c.filterMap id
-      match Clause.ofArray c with
-      | none => throwError "Clause {c} contains complementary literals"
-      | some c => return addRup cId c rupHints
-  | addRat cId c pivot rupHints ratHints => do
-    if h : pivot.1 ≠ 0 then
-      let some pivot ← natLiteralToPosFinLiteralIO pivot h
-        | throwError "Failed to turn {pivot} to a literal"
-      let c : Array (Option (Literal (PosFin n))) ←
-        c.mapM (fun x => if h : x ≠ 0 then Dimacs.intToLiteralIO x h else throwError "Parsing error")
-      if c.contains none then
-        throwError "Failed to convert at least one literal in {c}"
-      else
-        let c := c.filterMap id
-        match Clause.ofArray c with
-        | none => throwError "Clause {c} contains complementary literals"
-        | some c => return addRat cId c pivot rupHints ratHints
-    else
-      throwError "pivot cannot be 0"
-  | del ids => return del ids

Test/PHPDemo/Formula.lean

@@ -60,7 +60,7 @@ def load_php3_lrat_proof : IO (List ({act : DefaultClauseAction 13 // wellFormed
   let _ ← satQuery cnfPath.toString lratPath.toString
   match ← parseLRATProof lratPath.toString with
   | some lratProof =>
-    let lratProof ← lratProof.mapM (intActionToDefaultClauseActionIO 13)
+    let lratProof := lratProof.map (intActionToDefaultClauseAction 13)
     let lratProof :=
       lratProof.filterMap
         (fun actOpt =>