style: apply the signature layout

OATP/Artifacts.lean

@@ -21,17 +21,28 @@ structure Run where
   directory : System.FilePath
   deriving Repr
 
-private def safeName (value : String) : String :=
+private
+def safeName
+    (value : String)
+    : String
+    :=
   let name := String.ofList <| value.toList.map fun character =>
     if character.isAlphanum || character == '-' || character == '_' then character else '_'
   if name.isEmpty then "run" else name
 
-private def roots : IO (List System.FilePath) := do
+private
+def roots
+    : IO (List System.FilePath)
+    := do
   let current ← IO.currentDir
   let fallback ← OATP.Config.directory
   pure <| System.FilePath.join current ".oatp" :: fallback.toList
 
-def start (label : String) (problem : Problem) : IO (Option Run) := do
+def start
+    (label : String)
+    (problem : Problem)
+    : IO (Option Run)
+    := do
   let stamp ← IO.monoMsNow
   for root in ← roots do
     -- ponytail: 64 bounded suffixes cover same-millisecond concurrent runs;
@@ -48,11 +59,19 @@ def start (label : String) (problem : Problem) : IO (Option Run) := do
       catch _ => pure ()
   pure none
 
-def write (run : Run) (name content : String) : IO Unit := do
+def write
+    (run : Run)
+    (name content : String)
+    : IO Unit
+    := do
   try IO.FS.writeFile (System.FilePath.join run.directory name) content
   catch _ => pure ()
 
-def writeCommand (run : Run) (command : String) : IO Unit :=
+def writeCommand
+    (run : Run)
+    (command : String)
+    : IO Unit
+    :=
   write run "command.txt" command
 
 end OATP.Artifacts

OATP/Config.lean

@@ -21,28 +21,45 @@ structure Preferences where
 
 def default : Preferences := {}
 
-private def configRoot : IO (Option System.FilePath) := do
+private
+def configRoot
+    : IO (Option System.FilePath)
+    := do
   match ← IO.getEnv "XDG_CONFIG_HOME" with
   | some path => pure (some ⟨path⟩)
   | none =>
       match ← IO.getEnv "HOME" with
       | some path => pure (some (System.FilePath.join ⟨path⟩ ".config"))
       | none => pure none
 
-def directory : IO (Option System.FilePath) := do
+def directory
+    : IO (Option System.FilePath)
+    := do
   pure <| (← configRoot).map fun root => System.FilePath.join root "oatp"
 
-def path : IO (Option System.FilePath) := do
+def path
+    : IO (Option System.FilePath)
+    := do
   pure <| (← directory).map fun root => System.FilePath.join root "config.json"
 
 private def field (json : Json) (name : String) : Option Json := json.get? name
 
-private def stringField (json : Json) (name fallback : String) : String :=
+private
+def stringField
+    (json : Json)
+    (name fallback : String)
+    : String
+    :=
   match field json name with
   | some (.str value) => value
   | _ => fallback
 
-private def stringArrayField (json : Json) (name : String) : Array String :=
+private
+def stringArrayField
+    (json : Json)
+    (name : String)
+    : Array String
+    :=
   match field json name with
   | some (.arr values) =>
       let result : List String := values.toList.filterMap fun value =>
@@ -52,7 +69,10 @@ private def stringArrayField (json : Json) (name : String) : Array String :=
       result.toArray
   | _ => #[]
 
-private def fromJson : Json → Preferences
+private
+def fromJson
+    : Json →
+      Preferences
   | json => {
       theory := stringField json "theory" default.theory
       defaultProver := stringField json "defaultProver" default.defaultProver
@@ -64,7 +84,11 @@ private def fromJson : Json → Preferences
       theme := stringField json "theme" default.theme
     }
 
-private def toJson (preferences : Preferences) : Json :=
+private
+def toJson
+    (preferences : Preferences)
+    : Json
+    :=
   .obj #[
     ("theory", .str preferences.theory),
     ("defaultProver", .str preferences.defaultProver),
@@ -74,7 +98,9 @@ private def toJson (preferences : Preferences) : Json :=
     ("theme", .str preferences.theme)
   ]
 
-def load : IO (Preferences × Option String) := do
+def load
+    : IO (Preferences × Option String)
+    := do
   match ← path with
   | none => pure (default, none)
   | some file =>
@@ -85,7 +111,10 @@ def load : IO (Preferences × Option String) := do
         | .error _ => pure (default, some s!"invalid config `{file}`: expected a JSON object")
       catch _ => pure (default, none)
 
-def save (preferences : Preferences) : IO (Option String) := do
+def save
+    (preferences : Preferences)
+    : IO (Option String)
+    := do
   match ← path with
   | none => pure (some "cannot persist preferences: HOME/XDG_CONFIG_HOME is unset")
   | some file =>

OATP/Core.lean

@@ -25,11 +25,15 @@ inductive RunStrategy where
 
 namespace RunStrategy
 
-def name : RunStrategy → String
+def name
+    : RunStrategy →
+      String
   | .all => "all"
   | .firstSuccess => "first-success"
 
-def ofString : String → Option RunStrategy
+def ofString
+    : String →
+      Option RunStrategy
   | "all" => some .all
   | "first-success" => some .firstSuccess
   | _ => none
@@ -45,7 +49,10 @@ structure Prover where
 
 namespace Prover
 
-def label (prover : Prover) : String :=
+def label
+    (prover : Prover)
+    : String
+    :=
   match prover.version with
   | some version => s!"{prover.name} {version}"
   | none => prover.name
@@ -67,7 +74,10 @@ namespace SZSStatus
 
 private def statusPrefixes : List String := ["% SZS status ", "# SZS status "]
 
-def tokenFromLine (line : String) : Option String :=
+def tokenFromLine
+    (line : String)
+    : Option String
+    :=
   let line := line.trimAscii.toString
   let rec find : List String → Option String
     | [] => none
@@ -78,24 +88,36 @@ def tokenFromLine (line : String) : Option String :=
         else find markers
   find statusPrefixes
 
-private def tokenFromLines : List String → Option String
+private
+def tokenFromLines
+    : List String →
+      Option String
   | [] => none
   | line :: lines => tokenFromLine line |>.orElse (fun _ => tokenFromLines lines)
 
-private def resultTokenFromLine (line : String) : Option String :=
+private
+def resultTokenFromLine
+    (line : String)
+    : Option String
+    :=
   let line := line.trimAscii.toString
   match line.splitOn " says " with
   | _ :: result :: _ =>
       let token := result.splitOn " " |>.headD ""
       if token.isEmpty then none else some token
   | _ => none
 
-def tokenFromOutput (output : String) : Option String :=
+def tokenFromOutput
+    (output : String)
+    : Option String
+    :=
   let lines := output.splitOn "\n"
   tokenFromLines lines |>.orElse fun _ =>
     lines.findSome? resultTokenFromLine
 
-def ofString : String → Option SZSStatus
+def ofString
+    : String →
+      Option SZSStatus
   | "Theorem" | "theorem" => some .theorem
   | "Unsatisfiable" | "unsatisfiable" => some .unsatisfiable
   | "Satisfiable" | "satisfiable" => some .satisfiable
@@ -107,10 +129,15 @@ def ofString : String → Option SZSStatus
   | "Unknown" | "unknown" => some .unknown
   | _ => none
 
-def ofOutput (output : String) : Option SZSStatus :=
+def ofOutput
+    (output : String)
+    : Option SZSStatus
+    :=
   tokenFromOutput output >>= ofString
 
-def toString : SZSStatus → String
+def toString
+    : SZSStatus →
+      String
   | .theorem => "Theorem"
   | .unsatisfiable => "Unsatisfiable"
   | .satisfiable => "Satisfiable"
@@ -120,11 +147,15 @@ def toString : SZSStatus → String
   | .error => "Error"
   | .unknown => "Unknown"
 
-def isSuccess : SZSStatus → Bool
+def isSuccess
+    : SZSStatus →
+      Bool
   | .theorem | .unsatisfiable => true
   | _ => false
 
-instance : ToString SZSStatus where
+instance
+    : ToString SZSStatus
+    where
   toString := toString
 
 end SZSStatus
@@ -155,12 +186,16 @@ inductive Outcome where
   | failed (message : String) (artifact : Option Artifact := none)
   deriving Repr
 
-def Outcome.artifact : Outcome → Option Artifact
+def Outcome.artifact
+    : Outcome →
+      Option Artifact
   | .candidate artifact => some artifact
   | .timedOut artifact => some artifact
   | .failed _ artifact => artifact
 
-def Outcome.status : Outcome → String
+def Outcome.status
+    : Outcome →
+      String
   | .candidate artifact => s!"candidate ({artifact.status})"
   | .timedOut _ => "timeout"
   | .failed message _ => s!"failed: {message}"