From e78918337b2994af8224bc94941db836b354fe0c Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 18 Sep 2026 14:11:55 -0500 Subject: [PATCH 1/4] style: apply the signature layout Reformat col-0 declarations to the diff-minimizing layout: name alone on the keyword line, one binder group per line, leading colon on the ascribed type. Whitespace only. --- OATP/Artifacts.lean | 10 +- OATP/Config.lean | 22 +- OATP/Core.lean | 54 +++- OATP/Http.lean | 50 ++- OATP/Lean.lean | 5 +- OATP/Lean/Repl.lean | 34 ++- OATP/Portfolio.lean | 43 ++- OATP/Process.lean | 4 +- OATP/Proof.lean | 9 +- OATP/Properties/Basic.lean | 7 +- OATP/ProverReference.lean | 20 +- OATP/Repl.lean | 188 +++++++++--- OATP/Repl/Context.lean | 108 +++++-- OATP/ReplView.lean | 606 +++++++++++++++++++++++++++++-------- OATP/Runtime.lean | 4 +- OATP/SystemOnTPTP.lean | 118 ++++++-- OATP/TPTP.lean | 27 +- OATP/Term.lean | 12 +- OATP/Translate.lean | 19 +- examples/Cli.lean | 74 ++++- examples/Repl.lean | 208 ++++++++++--- test/Tests.lean | 11 +- 22 files changed, 1280 insertions(+), 353 deletions(-) diff --git a/OATP/Artifacts.lean b/OATP/Artifacts.lean index 0a5460b..42d87d1 100644 --- a/OATP/Artifacts.lean +++ b/OATP/Artifacts.lean @@ -21,7 +21,10 @@ 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 @@ -52,7 +55,10 @@ 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 diff --git a/OATP/Config.lean b/OATP/Config.lean index b00257f..087c02c 100644 --- a/OATP/Config.lean +++ b/OATP/Config.lean @@ -37,12 +37,20 @@ def path : IO (Option System.FilePath) := do 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 +60,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 +75,10 @@ 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), diff --git a/OATP/Core.lean b/OATP/Core.lean index e901550..bccd1f6 100644 --- a/OATP/Core.lean +++ b/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,9 @@ 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 +73,9 @@ 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,11 +86,17 @@ 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 :: _ => @@ -90,12 +104,16 @@ private def resultTokenFromLine (line : String) : Option String := 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 +125,14 @@ 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,7 +142,9 @@ def toString : SZSStatus → String | .error => "Error" | .unknown => "Unknown" -def isSuccess : SZSStatus → Bool +def isSuccess + : SZSStatus → + Bool | .theorem | .unsatisfiable => true | _ => false @@ -155,12 +179,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}" diff --git a/OATP/Http.lean b/OATP/Http.lean index 779ad50..71cee59 100644 --- a/OATP/Http.lean +++ b/OATP/Http.lean @@ -26,29 +26,41 @@ structure Field where value : String deriving BEq, DecidableEq, Repr -private def hexDigits : Array Char := +private +def hexDigits + : Array Char := #[ '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'A', 'B', 'C', 'D', 'E', 'F' ] -private def isUnreserved (byte : UInt8) : Bool := +private +def isUnreserved + (byte : UInt8) + : Bool := (byte >= 48 && byte <= 57) || (byte >= 65 && byte <= 90) || (byte >= 97 && byte <= 122) || byte == 45 || byte == 46 || byte == 95 || byte == 126 -private def encodeByte (byte : UInt8) : String := +private +def encodeByte + (byte : UInt8) + : String := if isUnreserved byte then Char.ofNat byte.toNat |>.toString else let n := byte.toNat s!"%{hexDigits[n / 16]!}{hexDigits[n % 16]!}" -def encodeComponent (value : String) : String := +def encodeComponent + (value : String) + : String := String.join (value.toUTF8.toList.map encodeByte) -def encodeUrlEncoded (fields : Array Field) : String := +def encodeUrlEncoded + (fields : Array Field) + : String := String.intercalate "&" <| fields.toList.map fun field => s!"{encodeComponent field.name}={encodeComponent field.value}" @@ -59,7 +71,10 @@ structure MultipartPart where contentType : Option String := none deriving BEq, DecidableEq, Repr -private def validHeaderValue (value : String) : Bool := +private +def validHeaderValue + (value : String) + : Bool := value.toList.all fun character => character != '"' && character != '\\' && character != '\r' && character != '\n' @@ -95,7 +110,9 @@ inductive Method where | post deriving BEq, DecidableEq, Repr -def Method.toString : Method → String +def Method.toString + : Method → + String | .get => "GET" | .post => "POST" @@ -142,7 +159,9 @@ inductive Error where | bodyTooLarge (actual limit : Nat) deriving Repr -def Error.message : Error → String +def Error.message + : Error → + String | .io message => s!"HTTP IO failed: {message}" | .invalidRequest message => s!"invalid HTTP request: {message}" | .transport message => s!"HTTP transport failed: {message}" @@ -158,7 +177,10 @@ inductive Transport where def statusMarker := "OATP_HTTP_STATUS:" -private def statusFromOutput (output : String) : Option (String × Nat) := +private +def statusFromOutput + (output : String) + : Option (String × Nat) := let parts := output.splitOn statusMarker match parts.reverse with | code :: before :: _ => @@ -195,13 +217,19 @@ private def requestWithCurlUnsafe (request : Request) : IO (Except Error Respons else return Except.ok { statusCode := statusCode, body := body, stderr := output.stderr } -private def statusFromWgetLine (line : String) : Option Nat := +private +def statusFromWgetLine + (line : String) + : Option Nat := let fields := line.trimAscii.toString.splitOn " " |>.filter (!·.isEmpty) match fields with | _ :: code :: _ => code.toNat? | _ => none -private def statusFromWgetOutput (output : String) : Option Nat := +private +def statusFromWgetOutput + (output : String) + : Option Nat := let rec find : List String → Option Nat | [] => none | line :: lines => diff --git a/OATP/Lean.lean b/OATP/Lean.lean index d39cea9..0ca2b4d 100644 --- a/OATP/Lean.lean +++ b/OATP/Lean.lean @@ -41,7 +41,10 @@ def snapshot (mvarId : MVarId) : MetaM GoalSnapshot := mvarId.withContext do target := ← prettyExpr target } -def check (mvarId : MVarId) (candidate : Expr) : MetaM (Except String CheckedProof) := +def check + (mvarId : MVarId) + (candidate : Expr) + : MetaM (Except String CheckedProof) := mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) let candidate ← instantiateMVars candidate diff --git a/OATP/Lean/Repl.lean b/OATP/Lean/Repl.lean index e0e32fa..58cc4d0 100644 --- a/OATP/Lean/Repl.lean +++ b/OATP/Lean/Repl.lean @@ -62,16 +62,28 @@ private def runMeta {α : Type} (runtime : Runtime) (action : MetaM α) : runtime.metaState pure (value, { runtime with coreState, metaState }) -private def addAtom (atoms : Array String) (name : String) : Array String := +private +def addAtom + (atoms : Array String) + (name : String) + : Array String := if atoms.contains name then atoms else atoms.push name private abbrev TranslationM := ExceptT String MetaM -private def translationError {α : Type} (message : String) : TranslationM α := +private +def translationError + {α : Type} + (message : String) + : TranslationM α := ExceptT.mk (pure (.error message)) -private partial def atomNames (formula : _root_.TPTP.Formula.Expr) (atoms : Array String) : - Array String := +private +partial +def atomNames + (formula : _root_.TPTP.Formula.Expr) + (atoms : Array String) + : Array String := match formula with | .atom predicate arguments => if arguments.isEmpty then addAtom atoms predicate else atoms @@ -81,15 +93,23 @@ private partial def atomNames (formula : _root_.TPTP.Formula.Expr) (atoms : Arra atomNames right (atomNames left atoms) | .forall _ body | .exists _ body => atomNames body atoms -private def withAtoms {α : Type} (atoms : List String) - (action : Array (String × Expr) → TranslationM α) : MetaM (Except String α) := +private +def withAtoms + {α : Type} + (atoms : List String) + (action : Array (String × Expr) → TranslationM α) + : MetaM (Except String α) := match atoms with | [] => (action #[]).run | atom :: rest => withLocalDeclD (Name.mkSimple atom) (mkSort .zero) fun fvar => withAtoms rest fun locals => action (locals.push (atom, fvar)) -private def lookupAtom (atoms : Array (String × Expr)) (name : String) : Option Expr := +private +def lookupAtom + (atoms : Array (String × Expr)) + (name : String) + : Option Expr := atoms.find? (·.1 == name) |>.map Prod.snd private partial def toLean (atoms : Array (String × Expr)) diff --git a/OATP/Portfolio.lean b/OATP/Portfolio.lean index 6adf772..876268e 100644 --- a/OATP/Portfolio.lean +++ b/OATP/Portfolio.lean @@ -40,13 +40,19 @@ inductive Result where | failed (attempt : Attempt) (failure : Failure) deriving Repr -private def responseErrorMessage : SystemOnTPTP.ResponseError → String +private +def responseErrorMessage + : SystemOnTPTP.ResponseError → + String | .httpStatus status => s!"SystemOnTPTP returned HTTP {status}" | .missingStatus => "SystemOnTPTP response did not contain an SZS status" | .unsupportedStatus status => s!"SystemOnTPTP returned unsupported SZS status `{status}`" | .malformedBody message => s!"SystemOnTPTP response was not valid HTML: {message}" -private def httpErrorMessage : Http.Error → String +private +def httpErrorMessage + : Http.Error → + String | .io message => s!"HTTP IO failed: {message}" | .invalidRequest message => s!"invalid HTTP request: {message}" | .transport message => s!"HTTP transport failed: {message}" @@ -54,12 +60,16 @@ private def httpErrorMessage : Http.Error → String | .requestBodyTooLarge actual limit => s!"HTTP request exceeded {limit} bytes ({actual} captured)" | .bodyTooLarge actual limit => s!"HTTP response exceeded {limit} bytes ({actual} captured)" -def Failure.message : Failure → String +def Failure.message + : Failure → + String | .process message => message | .http error => httpErrorMessage error | .response error _ => responseErrorMessage error -def Failure.output : Failure → String +def Failure.output + : Failure → + String | .http (.malformedStatus output) => output | .process _ | .http _ => "" | .response _ output => output @@ -97,16 +107,25 @@ private partial def collect (pending : List (Task (Except IO.Error Result))) onResult result collect remaining (results.push result) onResult -def runWith (problem : Problem) (attempts : Array Attempt) - (onResult : Result → IO Unit := fun _ => pure ()) : IO (Array Result) := do +def runWith + (problem : Problem) + (attempts : Array Attempt) + (onResult : Result → IO Unit := fun _ => pure ()) + : IO (Array Result) := do let tasks ← attempts.toList.mapM fun attempt => IO.asTask (execute problem attempt) Task.Priority.dedicated collect tasks #[] onResult -def run (problem : Problem) (attempts : Array Attempt) : IO (Array Result) := +def run + (problem : Problem) + (attempts : Array Attempt) + : IO (Array Result) := runWith problem attempts -private def successful : Result → Bool +private +def successful + : Result → + Bool | .artifact _ artifact => SZSStatus.isSuccess artifact.status | .failed _ _ => false @@ -120,8 +139,12 @@ private def runUntilSuccess (problem : Problem) (attempts : List Attempt) if successful result then pure (results.push result) else runUntilSuccess problem rest (results.push result) onResult -def runWithStrategy (problem : Problem) (attempts : Array Attempt) (strategy : RunStrategy) - (onResult : Result → IO Unit := fun _ => pure ()) : IO (Array Result) := +def runWithStrategy + (problem : Problem) + (attempts : Array Attempt) + (strategy : RunStrategy) + (onResult : Result → IO Unit := fun _ => pure ()) + : IO (Array Result) := match strategy with | .all => runWith problem attempts onResult | .firstSuccess => runUntilSuccess problem attempts.toList #[] onResult diff --git a/OATP/Process.lean b/OATP/Process.lean index d007ec4..bd9f65b 100644 --- a/OATP/Process.lean +++ b/OATP/Process.lean @@ -24,7 +24,9 @@ structure Command where deriving BEq, DecidableEq, Repr /-- Add the stdin filename expected by local provers that require one. -/ -def Command.withStdinProblem (command : Command) : Command := +def Command.withStdinProblem + (command : Command) + : Command := let executable := (command.executable.splitOn "/").getLast?.getD command.executable if executable == "metis" && !command.arguments.any (· == "-") then { command with arguments := command.arguments.push "-" } diff --git a/OATP/Proof.lean b/OATP/Proof.lean index 57176cc..87adaa8 100644 --- a/OATP/Proof.lean +++ b/OATP/Proof.lean @@ -29,7 +29,8 @@ inductive Step where | implicationIntro (localName : Name) (body : Step) deriving Repr -def stepNames : List String := +def stepNames + : List String := ["true-intro", "exact", "and-left", "and-right", "and-intro", "implication-intro"] private def andParts (target : Expr) : MetaM (Option (Expr × Expr)) := do @@ -50,7 +51,11 @@ private def projection (target : Expr) (localName : Name) (useLeft : Bool) : else pure (.error s!"conjunction projection from `{localName}` has the wrong target") -private def build (target : Expr) : Step → MetaM (Except String Expr) +private +def build + (target : Expr) + : Step → + MetaM (Except String Expr) | .exact localName => do let hypothesis ← getFVarFromUserName localName let hypothesisType ← inferType hypothesis diff --git a/OATP/Properties/Basic.lean b/OATP/Properties/Basic.lean index 3479d9b..1e1f179 100644 --- a/OATP/Properties/Basic.lean +++ b/OATP/Properties/Basic.lean @@ -13,11 +13,12 @@ namespace OATP.Properties open OATP OATP.TPTP -theorem empty_plain_render : OATP.Term.renderPlain #[] = "" := by +theorem empty_plain_render + : OATP.Term.renderPlain #[] = "" := by rfl -theorem note_plain_render : - OATP.Term.renderPlain #[.note "ready"] = "note: ready" := by +theorem note_plain_render + : OATP.Term.renderPlain #[.note "ready"] = "note: ready" := by rfl theorem goal_context_plain_render : diff --git a/OATP/ProverReference.lean b/OATP/ProverReference.lean index babaf54..5537e4a 100644 --- a/OATP/ProverReference.lean +++ b/OATP/ProverReference.lean @@ -29,13 +29,19 @@ namespace ProverReference def fromLocal (name : String) : ProverReference := { name, kind := .local } -def fromOnline (name : String) : ProverReference := +def fromOnline + (name : String) + : ProverReference := { name := OATP.SystemOnTPTP.onlineSystemId name, kind := .online } -def ofString (name : String) : ProverReference := +def ofString + (name : String) + : ProverReference := if OATP.SystemOnTPTP.isOnlineReference name then fromOnline name else fromLocal name -def fromPersisted (value : String) : Option ProverReference := +def fromPersisted + (value : String) + : Option ProverReference := if value.startsWith "local:" then let name := value.drop "local:".length |>.toString if name.isEmpty then none else some (fromLocal name) @@ -44,12 +50,16 @@ def fromPersisted (value : String) : Option ProverReference := if name.isEmpty then none else some (fromOnline name) else if value.isEmpty then none else some (ofString value) -def persisted (reference : ProverReference) : String := +def persisted + (reference : ProverReference) + : String := match reference.kind with | .local => "local:" ++ reference.name | .online => "online:" ++ reference.name -def display (reference : ProverReference) : String := +def display + (reference : ProverReference) + : String := match reference.kind with | .local => reference.name | .online => OATP.SystemOnTPTP.onlineReference reference.name diff --git a/OATP/Repl.lean b/OATP/Repl.lean index 019f7fb..7245964 100644 --- a/OATP/Repl.lean +++ b/OATP/Repl.lean @@ -27,7 +27,8 @@ open OATP.TPTP open _root_.Argus open _root_.Grip -def helpTopics : List String := +def helpTopics + : List String := ["cnf", "fof", "tff", "lean", "run", "context", "grammar", "roles"] def grammarTopics : List String := OATP.TPTP.supportedTheories @@ -36,13 +37,19 @@ def roleFormats : List String := OATP.TPTP.supportedTheories def runStrategyChoices : List String := OATP.RunStrategy.choices -def completionParam (typeName : String) (values : List String) : Param String := +def completionParam + (typeName : String) + (values : List String) + : Param String := Param.named typeName (Param.enum (values.map fun value => (value, value))) -def contextIndexParam : Param Nat := +def contextIndexParam + : Param Nat := Param.ofParser "INDEX" (GParser.seqR (GParser.optional (GParser.ch '#')) GParser.nat) -def staticCompletionValues (typeName : String) : List String := +def staticCompletionValues + (typeName : String) + : List String := match typeName with | "TOPIC" => helpTopics | "FORMAT" => roleFormats @@ -162,27 +169,41 @@ argus_opts SystemsOptions where online : Bool := Spec.switch "online" (some 'o') "Also fetch online provers"; catalogue : OATP.Argus.CatalogueOptions := OATP.Argus.CatalogueOptions.spec -private def parseSpec {α : Type} {g : Grade} (spec : Argus.Spec g α) - (args : List String) : Except String α := +private +def parseSpec + {α : Type} + {g : Grade} + (spec : Argus.Spec g α) + (args : List String) + : Except String α := match Argus.run spec args with | .ok value => .ok value | .error errors => .error (String.intercalate "\n" (errors.map Argus.Err.message)) -private def splitArguments : List String → List String × List String +private +def splitArguments + : List String → + List String × List String | [] => ([], []) | "__OATP_ARGS__" :: rest => ([], rest) | value :: rest => let (before, after) := splitArguments rest (value :: before, after) -private def splitTerminator : List String → List String × Option (List String) +private +def splitTerminator + : List String → + List String × Option (List String) | [] => ([], none) | "--" :: rest => ([], some rest) | value :: rest => let (before, after) := splitTerminator rest (value :: before, after) -private def runRequestOf (options : RunOptions) : RunRequest := +private +def runRequestOf + (options : RunOptions) + : RunRequest := let (references, arguments) := splitArguments options.references { references := (references ++ options.provers).map ProverReference.ofString all := options.all @@ -193,46 +214,65 @@ private def runRequestOf (options : RunOptions) : RunRequest := maxOutput := options.resources.maxOutput.getD OATP.defaultMaxOutputBytes arguments } -private def localRequestOf (options : LocalOptions) : LocalRequest := +private +def localRequestOf + (options : LocalOptions) + : LocalRequest := let (_, arguments) := splitArguments options.arguments { executable := options.executable timeout := options.resources.timeout.getD OATP.defaultTimeoutSeconds maxOutput := options.resources.maxOutput.getD OATP.defaultMaxOutputBytes arguments := if arguments.isEmpty then options.arguments else arguments } -private def onlineRequestOf (options : OnlineOptions) : OnlineRequest := +private +def onlineRequestOf + (options : OnlineOptions) + : OnlineRequest := { system := options.system endpoint := options.remote.endpoint timeout := options.remote.resources.timeout.getD OATP.defaultTimeoutSeconds maxOutput := options.remote.resources.maxOutput.getD OATP.defaultMaxOutputBytes } -private def systemsRequestOf (options : SystemsOptions) : SystemsRequest := +private +def systemsRequestOf + (options : SystemsOptions) + : SystemsRequest := { online := options.online, endpoint := options.catalogue.endpoint, refresh := options.catalogue.refresh, noCache := options.catalogue.noCache } -def parseRunRequest (args : List String) : Except String RunRequest := +def parseRunRequest + (args : List String) + : Except String RunRequest := let (args, tail) := splitTerminator args parseSpec RunOptions.spec args |>.map fun request => { runRequestOf request with arguments := tail.getD (runRequestOf request).arguments } -def parseLocalRequest (args : List String) : Except String LocalRequest := +def parseLocalRequest + (args : List String) + : Except String LocalRequest := let (args, tail) := splitTerminator args parseSpec LocalOptions.spec args |>.map fun request => { localRequestOf request with arguments := tail.getD (localRequestOf request).arguments } -def parseOnlineRequest (args : List String) : Except String OnlineRequest := +def parseOnlineRequest + (args : List String) + : Except String OnlineRequest := let (args, tail) := splitTerminator args match tail with | some (_ :: _) => .error "online commands do not accept arguments after --" | _ => parseSpec OnlineOptions.spec args |>.map onlineRequestOf -def parseSystemsRequest (args : List String) : Except String SystemsRequest := +def parseSystemsRequest + (args : List String) + : Except String SystemsRequest := let (args, tail) := splitTerminator args match tail with | some (_ :: _) => .error "systems does not accept arguments after --" | _ => parseSpec SystemsOptions.spec args |>.map systemsRequestOf -def splitWords (source : String) : List String := +def splitWords + (source : String) + : List String := let whitespace (character : Char) : Bool := character.isWhitespace let (current, words) := source.toList.foldl (fun (current, words) character => if whitespace character then @@ -242,13 +282,17 @@ def splitWords (source : String) : List String := let words := if current.isEmpty then words else String.ofList current.reverse :: words words.reverse -private def textSpec (name help : String) : Spec (1 * (1 * conditional * flexible)) String := +private +def textSpec + (name help : String) + : Spec (1 * (1 * conditional * flexible)) String := Spec.map (fun values : List String => String.intercalate " " values) (Spec.map2 (fun value values => value :: values) (Spec.arg name help (Param.named name Param.str)) (Spec.many (Spec.arg name help (Param.named name Param.str)))) -def commandSpec : Argus.Command Command := +def commandSpec + : Argus.Command Command := Argus.group "oatp" [ Argus.cmd "help" (Spec.map Command.help (Spec.opt (Spec.arg "TOPIC" "Help topic" (Param.named "TOPIC" Param.str)))) @@ -338,7 +382,10 @@ def commandSpec : Argus.Command Command := , Argus.cmd "quit" (Spec.const .quit) (description := "Leave the REPL") , Argus.cmd "exit" (Spec.const .quit) (description := "Leave the REPL") ] -private def commandArgv (source : String) : List String × Option (List String) := +private +def commandArgv + (source : String) + : List String × Option (List String) := match splitWords source.trimAscii.toString with | command :: args => let command := (command.drop 1).toString @@ -346,8 +393,11 @@ private def commandArgv (source : String) : List String × Option (List String) (command :: args, tail) | [] => ([], none) -private def appendCommandArguments (command : Command) (tail : Option (List String)) : - Except String Command := +private +def appendCommandArguments + (command : Command) + (tail : Option (List String)) + : Except String Command := match tail with | none => .ok command | some arguments => @@ -361,7 +411,9 @@ private def appendCommandArguments (command : Command) (tail : Option (List Stri if arguments.isEmpty then .ok command else .error "command does not accept arguments after --" -def parseCommandSpec (source : String) : Except String Command := +def parseCommandSpec + (source : String) + : Except String Command := let line := source.trimAscii.toString if !line.startsWith "/" then .error "commands start with `/`; try `/help`" else @@ -378,15 +430,21 @@ def parseCommandSpec (source : String) : Except String Command := | [] => "" .error (message ++ hint) -private def commandChildren : List (Argus.Command Command) := +private +def commandChildren + : List (Argus.Command Command) := match commandSpec.body with | .subs children => children | .opts _ => [] def commandNames : List String := commandChildren.map (·.name) -private def usageArguments : {g : Grade} → {α : Type} → Spec g α → - List (String × Bool × Bool) +private +def usageArguments + : {g : Grade} → + {α : Type} → + Spec g α → + List (String × Bool × Bool) | _, _, .const _ | _, _, .switch _ _ _ | _, _, .flag _ _ _ _ => [] | _, _, .arg name _ _ => [(name, false, false)] | _, _, .ap function argument => usageArguments function ++ usageArguments argument @@ -396,7 +454,10 @@ private def usageArguments : {g : Grade} → {α : Type} → Spec g α → | _, _, .many argument => usageArguments argument |>.map fun (name, _, _) => (name, true, true) -private def usageLine (command : Argus.Command Command) : String := +private +def usageLine + (command : Argus.Command Command) + : String := let flags := if command.toMeta.flags.isEmpty then "" else " [OPTIONS]" let arguments := match command.body with | .opts spec => usageArguments spec @@ -406,26 +467,34 @@ private def usageLine (command : Argus.Command Command) : String := output ++ if optional then " [" ++ value ++ "]" else " " ++ value) "" command.name ++ flags ++ arguments -def commandHelpText : String := +def commandHelpText + : String := String.intercalate "\n" <| ["OATP REPL commands"] ++ commandChildren.map fun command => " /" ++ usageLine command ++ " " ++ command.description -def parseCommand (source : String) : Command := +def parseCommand + (source : String) + : Command := let line := source.trimAscii.toString match parseCommandSpec line with | .ok command => command | .error _ => .unknown line -def parseInput (source : String) : Submission := +def parseInput + (source : String) + : Submission := if source.trimAscii.toString.startsWith "/" then .command (parseCommand source) else .source source -def helpText : String := +def helpText + : String := commandHelpText -private def cnfHelp : String := +private +def cnfHelp + : String := String.intercalate "\n" [ "CNF — clause normal form", "statement: cnf(NAME, ROLE, CLAUSE).", @@ -445,7 +514,9 @@ private def cnfHelp : String := " /state formulas /roles cnf /run --prover eprover" ] -private def fofHelp : String := +private +def fofHelp + : String := String.intercalate "\n" [ "FOF — first-order formulas", "statement: fof(NAME, ROLE, FORMULA).", @@ -463,7 +534,9 @@ private def fofHelp : String := "use FOF when the problem needs implication, conjunction, or quantifiers" ] -private def tffHelp : String := +private +def tffHelp + : String := String.intercalate "\n" [ "TFF — typed first-order formulas", "type: tff(nat_type, type, nat: $tType).", @@ -476,7 +549,9 @@ private def tffHelp : String := "TFF is parsed as TPTP input; use /state to inspect collected symbols" ] -private def grammarHelp : String := +private +def grammarHelp + : String := String.intercalate "\n" [ "Grammar lookup", "/grammar cnf clause normal form", @@ -490,7 +565,10 @@ private def grammarHelp : String := "Use /help cnf, /help fof, or /help tff for examples." ] -private def roleHelp (topic : Option String) : String := +private +def roleHelp + (topic : Option String) + : String := let format := topic.getD "all" String.intercalate "\n" [ s!"Roles ({format})", @@ -511,7 +589,9 @@ private def roleHelp (topic : Option String) : String := s!"Use /grammar {format} for the syntax." ] -private def leanHelp : String := +private +def leanHelp + : String := String.intercalate "\n" [ "Lean bridge", "1. /goal p => p create a Lean goal", @@ -524,7 +604,9 @@ private def leanHelp : String := "example result: fun h => h : _fvar.1 → _fvar.1" ] -private def runHelp : String := +private +def runHelp + : String := String.intercalate "\n" [ "Provers", "/run run the configured or first local prover", @@ -553,7 +635,9 @@ private def runHelp : String := " /local vampire -- --mode casc" ] -private def contextHelp : String := +private +def contextHelp + : String := String.intercalate "\n" [ "Context drawer", "/state [TARGET] open context or focus a box", @@ -574,7 +658,10 @@ private def contextHelp : String := "theory: /theory fof|cnf|tff (tf1 alias); provers: /provers; theme: /theme NAME" ] -private def commandHelp (command : Argus.Command Command) : String := +private +def commandHelp + (command : Argus.Command Command) + : String := let details := match command.name with | "goal" | "to-lean" | "translate-to-lean" | "snapshot" | "to-tptp" | "reconstruct" | "term" => leanHelp @@ -587,11 +674,16 @@ private def commandHelp (command : Argus.Command Command) : String := String.intercalate "\n" <| [s!"/{usageLine command}", command.description] ++ (if details.isEmpty then [] else ["", details]) -private def normalizeHelpTopic (topic : String) : String := +private +def normalizeHelpTopic + (topic : String) + : String := let topic := topic.trimAscii.toString if topic.startsWith "/" then topic.drop 1 |>.trimAscii.toString else topic -def helpFor : Option String → String +def helpFor + : Option String → + String | none => helpText | some rawTopic => let topic := normalizeHelpTopic rawTopic @@ -616,11 +708,17 @@ def helpFor : Option String → String "/help run, /help context" ] -private def addFormulaCommand (session : Session) (input name role formula : String) : - Except String Session := +private +def addFormulaCommand + (session : Session) + (input name role formula : String) + : Except String Session := parseSource session input s!"fof({name}, {role}, {formula})." -def apply (session : Session) (input : String) : Except String Session := +def apply + (session : Session) + (input : String) + : Except String Session := match parseInput input with | .source source => parseSource session source source | .command command => diff --git a/OATP/Repl/Context.lean b/OATP/Repl/Context.lean index f5d7343..639723a 100644 --- a/OATP/Repl/Context.lean +++ b/OATP/Repl/Context.lean @@ -63,11 +63,19 @@ structure Session where history : Array HistoryEntry := #[] deriving Repr -private def addSymbol (symbols : Array Symbol) (symbol : Symbol) : Array Symbol := +private +def addSymbol + (symbols : Array Symbol) + (symbol : Symbol) + : Array Symbol := if symbols.any (· == symbol) then symbols else symbols.push symbol -private partial def collectTerm (term : _root_.TPTP.Formula.Term) (symbols : Array Symbol) : - Array Symbol := +private +partial +def collectTerm + (term : _root_.TPTP.Formula.Term) + (symbols : Array Symbol) + : Array Symbol := match term with | .var name => addSymbol symbols { kind := .variable, name } | .constant name => addSymbol symbols { kind := .constant, name } @@ -75,8 +83,12 @@ private partial def collectTerm (term : _root_.TPTP.Formula.Term) (symbols : Arr let symbols := addSymbol symbols { kind := .function, name, arity := arguments.size } arguments.foldl (fun symbols term => collectTerm term symbols) symbols -private partial def collectFormula (formula : _root_.TPTP.Formula.Expr) - (symbols : Array Symbol) : Array Symbol := +private +partial +def collectFormula + (formula : _root_.TPTP.Formula.Expr) + (symbols : Array Symbol) + : Array Symbol := match formula with | .atom predicate arguments => let symbols := addSymbol symbols @@ -91,7 +103,11 @@ private partial def collectFormula (formula : _root_.TPTP.Formula.Expr) addSymbol symbols { kind := .variable, name }) symbols collectFormula body symbols -private def formulaView (id cell : Nat) (statement : _root_.TPTP.Statement) : FormulaView := +private +def formulaView + (id cell : Nat) + (statement : _root_.TPTP.Statement) + : FormulaView := match OATP.TPTP.Statement.parseFormula statement with | .ok formula => { id, cell @@ -111,56 +127,90 @@ private def formulaView (id cell : Nat) (statement : _root_.TPTP.Statement) : Fo source := statement.render formula := statement.formula } -private def contextItems (nextId cell : Nat) (document : _root_.TPTP.Document) : - Array ContextItem × Nat := +private +def contextItems + (nextId cell : Nat) + (document : _root_.TPTP.Document) + : Array ContextItem × Nat := document.items.foldl (fun (items, nextId) item => (items.push { id := nextId, cell, value := item }, nextId + 1)) (#[], nextId) -private def viewsOf (items : Array ContextItem) : Array FormulaView := +private +def viewsOf + (items : Array ContextItem) + : Array FormulaView := items.foldl (fun views item => match item.value with | .statement statement => views.push (formulaView item.id item.cell statement) | .include _ => views) #[] -private def symbolsOf (views : Array FormulaView) : Array Symbol := +private +def symbolsOf + (views : Array FormulaView) + : Array Symbol := views.foldl (fun symbols view => view.symbols.foldl addSymbol symbols) #[] -private def problemSourceOf (items : Array ContextItem) : String := +private +def problemSourceOf + (items : Array ContextItem) + : String := String.intercalate "\n" (items.toList.map (fun item => item.value.render)) -private def rebuildContext (session : Session) : Session := +private +def rebuildContext + (session : Session) + : Session := let formulas := viewsOf session.context { session with problemSource := problemSourceOf session.context formulas symbols := symbolsOf formulas } -private def record (session : Session) (input result : String) : Session := +private +def record + (session : Session) + (input result : String) + : Session := { session with nextCell := session.nextCell + 1 history := session.history.push { cell := session.nextCell, input, result } } -def note (session : Session) (input result : String) : Session := +def note + (session : Session) + (input result : String) + : Session := record session input result -def addDocument (session : Session) (input : String) (document : _root_.TPTP.Document) : Session := +def addDocument + (session : Session) + (input : String) + (document : _root_.TPTP.Document) + : Session := let (items, nextContextId) := contextItems session.nextContextId session.nextCell document let session := rebuildContext { session with context := session.context ++ items nextContextId } record session input s!"parsed {viewsOf items |>.size} statement(s)" -def clearContext (session : Session) : Session := +def clearContext + (session : Session) + : Session := rebuildContext { session with context := #[] } -private def validateStatement (statement : _root_.TPTP.Statement) : Except String Unit := +private +def validateStatement + (statement : _root_.TPTP.Statement) + : Except String Unit := match statement.kind, statement.role with | .cnf, .conjecture => .error ("CNF does not support the `conjecture` role; use " ++ "`negated_conjecture` with a negated clause") | _, _ => pure () -private def validateDocument (document : _root_.TPTP.Document) : Except String Unit := +private +def validateDocument + (document : _root_.TPTP.Document) + : Except String Unit := document.items.toList.mapM (fun item => match item with | _root_.TPTP.Item.statement statement => validateStatement statement | _root_.TPTP.Item.include _ => pure ()) |>.map (fun _ => ()) @@ -172,18 +222,28 @@ private def parseDocument (source : String) : Except String _root_.TPTP.Document validateDocument document pure document -def parseSource (session : Session) (input source : String) : Except String Session := +def parseSource + (session : Session) + (input source : String) + : Except String Session := match parseDocument source with | .ok document => pure (addDocument session input document) | .error message => .error message private def contextIndexText (index : Nat) : String := s!"#{index}" -private def missingContextIndices (session : Session) (indices : List Nat) : List Nat := +private +def missingContextIndices + (session : Session) + (indices : List Nat) + : List Nat := indices.filter (fun index => !session.context.any (·.id == index)) -def removeContext (session : Session) (input : String) (indices : List Nat) : - Except String Session := +def removeContext + (session : Session) + (input : String) + (indices : List Nat) + : Except String Session := let indices := indices.eraseDups if indices.isEmpty then .error "remove expects at least one context index" @@ -220,7 +280,9 @@ def updateContext (session : Session) (input : String) (index : Nat) (source : S pure (record session input s!"updated {contextIndexText index}") | none => .error s!"unknown context index {contextIndexText index}" -def problem (session : Session) : Option Problem := +def problem + (session : Session) + : Option Problem := if session.problemSource.isEmpty then none else some { name := "oatp-repl" source := session.problemSource diff --git a/OATP/ReplView.lean b/OATP/ReplView.lean index 9bdb735..1d3329b 100644 --- a/OATP/ReplView.lean +++ b/OATP/ReplView.lean @@ -35,7 +35,9 @@ open scoped TermColor.Style def version : String := OATP.version -def aurora : ColorScheme where +def aurora + : ColorScheme + where background := .rgb 13 24 37 foreground := .rgb 225 241 245 selection := .rgb 39 70 83 @@ -49,7 +51,8 @@ def aurora : ColorScheme where purple := .rgb 178 146 255 pink := .rgb 245 132 203 -def themes : List (String × ColorScheme) := +def themes + : List (String × ColorScheme) := [("aurora", aurora), ("terracotta", { background := .rgb 26 28 38 foreground := .rgb 214 216 226 @@ -78,7 +81,10 @@ structure SemanticColors where functionColor : Color predicateColor : Color -def semanticColors (scheme : ColorScheme) : SemanticColors where +def semanticColors + (scheme : ColorScheme) + : SemanticColors + where format := scheme.cyan role := scheme.purple error := scheme.red @@ -124,7 +130,9 @@ inductive AppContext | history | historyInput -def AppContext.name : AppContext → String +def AppContext.name + : AppContext → + String | .default => "default" | .run => "run" | .runInput => "run-input" @@ -135,7 +143,9 @@ def AppContext.name : AppContext → String | .history => "history" | .historyInput => "history-input" -def AppContext.keyContext : AppContext → KeyContext +def AppContext.keyContext + : AppContext → + KeyContext | .default => KeyContext.ofString "default" | .run => KeyContext.ofString "run" | .runInput => KeyContext.ofString "run-input" @@ -146,15 +156,21 @@ def AppContext.keyContext : AppContext → KeyContext | .history => KeyContext.ofString "history" | .historyInput => KeyContext.ofString "history-input" -private def appBinding (keys : List Key) (action : AppKeyAction) - (context : Option AppContext) (description : String) : BindingSpec AppKeyAction := +private +def appBinding + (keys : List Key) + (action : AppKeyAction) + (context : Option AppContext) + (description : String) + : BindingSpec AppKeyAction := { keys action context := context.map AppContext.keyContext label := String.intercalate "/" (keys.map Keymap.keyLabel) description } -def appBindings : List (BindingSpec AppKeyAction) := +def appBindings + : List (BindingSpec AppKeyAction) := [ appBinding [.ctrl 'R', .ctrl 'r'] .toggleRun none "toggle the run drawer" , appBinding [.ctrl 'H', .ctrl 'h'] .toggleHistory none "toggle the history drawer" , appBinding [.ctrl 'S', .ctrl 's'] .toggleState none "toggle the state drawer" @@ -180,12 +196,17 @@ def appBindings : List (BindingSpec AppKeyAction) := , appBinding [.pageUp] .transcriptPageUp (some .default) "scroll transcript up" , appBinding [.pageDown] .transcriptPageDown (some .default) "scroll transcript down" ] -def appKeyLabel (action : AppKeyAction) (context : AppContext) : String := +def appKeyLabel + (action : AppKeyAction) + (context : AppContext) + : String := (appBindings.find? (fun binding => binding.action == action && (binding.context == none || binding.context == some (AppContext.keyContext context)))).map (·.label) |>.getD "?" -def themeByName (name : String) : Option ColorScheme := +def themeByName + (name : String) + : Option ColorScheme := themes.find? (fun pair => pair.1 == name) |>.map Prod.snd def themeNames : String := String.intercalate ", " (themes.map Prod.fst) @@ -221,7 +242,9 @@ inductive RunStatus where namespace RunStatus -def label : RunStatus → String +def label + : RunStatus → + String | .queued => "queued" | .running => "running" | .result status => s!"{status}" @@ -253,10 +276,13 @@ inductive ContextTarget where namespace ContextTarget -def all : List ContextTarget := +def all + : List ContextTarget := [.formulas, .symbols, .problem, .goal, .translation, .term] -def name : ContextTarget → String +def name + : ContextTarget → + String | .formulas => "formulas" | .symbols => "symbols" | .problem => "problem" @@ -264,7 +290,9 @@ def name : ContextTarget → String | .translation => "translation" | .term => "term" -def label : ContextTarget → String +def label + : ContextTarget → + String | .formulas => "FORMULAS" | .symbols => "SYMBOLS" | .problem => "PROBLEM" @@ -272,7 +300,9 @@ def label : ContextTarget → String | .translation => "LEAN → TPTP" | .term => "CHECKED TERM" -def aliases : ContextTarget → List String +def aliases + : ContextTarget → + List String | .formulas => ["form", "formula", "formulas"] | .symbols => ["symbol", "symbols"] | .problem => ["problem"] @@ -280,7 +310,12 @@ def aliases : ContextTarget → List String | .translation => ["translation", "tptp"] | .term => ["term", "checked-term", "checked"] -private def indexOf (value : String) : List ContextTarget → Nat → Option Nat +private +def indexOf + (value : String) + : List ContextTarget → + Nat → + Option Nat | [], _ => none | contextTarget :: rest, index => if (aliases contextTarget).any (· == value) then some index @@ -336,21 +371,28 @@ def fallbackSize : Size := { columns := 110, rows := 28 } def inputConfig : TextInputConfig := { width := 160, maxLength := 16_384 } -def multilineConfig : MultilineConfig := +def multilineConfig + : MultilineConfig := { text := inputConfig, lineBreak := .ctrl 'n' } private def minFrameWidth : Nat := 34 private def frameWidth (width : Nat) : Nat := max minFrameWidth width -private def boxInnerWidth (outer : Nat) : Nat := +private +def boxInnerWidth + (outer : Nat) + : Nat := Layout.boxInnerWidth { padding := 1 } outer private def panelWidth (width : Nat) : Nat := frameWidth width - 2 private def stateDrawerMinWidth : Nat := 70 -private def stateDrawerWidths (width : Nat) : Option (Nat × Nat) := +private +def stateDrawerWidths + (width : Nat) + : Option (Nat × Nat) := let total := frameWidth width if total < stateDrawerMinWidth then none else @@ -358,36 +400,64 @@ private def stateDrawerWidths (width : Nat) : Option (Nat × Nat) := let right := max 34 (available * 2 / 5) some (available - right, right) -def drawerWidths (width : Nat) : Option (Nat × Nat) := +def drawerWidths + (width : Nat) + : Option (Nat × Nat) := stateDrawerWidths width -private def joinLines : List Text → Text +private +def joinLines + : List Text → + Text | [] => Text.empty | line :: lines => lines.foldl (fun result next => result ++ Text.plain "\n" ++ next) line -private def fitText (width : Nat) (value : String) : Text := +private +def fitText + (width : Nat) + (value : String) + : Text := truncate width (Text.plain value) -private def fillHeight (height : Nat) (text : Text) : Text := +private +def fillHeight + (height : Nat) + (text : Text) + : Text := let height := max 1 height let lines := (splitLines text).take height joinLines (lines ++ List.replicate (height - lines.length) Text.empty) -private def withBackground (scheme : ColorScheme) (text : Text) : Text := +private +def withBackground + (scheme : ColorScheme) + (text : Text) + : Text := { segments := text.segments.map fun segment => { segment with style := Style.bg scheme.background <+> segment.style } } -private def dimText (text : Text) : Text := +private +def dimText + (text : Text) + : Text := { segments := text.segments.map fun segment => { segment with style := Style.dim <+> segment.style } } -private def base64Alphabet : String := +private +def base64Alphabet + : String := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/" -private def base64Char (index : Nat) : Char := +private +def base64Char + (index : Nat) + : Char := base64Alphabet.toList.getD index 'A' -private def base64 : List UInt8 → String +private +def base64 + : List UInt8 → + String | a :: b :: c :: rest => let value := a.toNat * 65_536 + b.toNat * 256 + c.toNat String.ofList [base64Char (value / 262_144), base64Char ((value / 4_096) % 64), @@ -401,11 +471,19 @@ private def base64 : List UInt8 → String String.ofList [base64Char (value / 4), base64Char ((value % 4) * 16), '=', '='] | [] => "" -private def clipboardSequence (value : String) : String := +private +def clipboardSequence + (value : String) + : String := "\u001b]52;c;" ++ base64 value.toUTF8.toList ++ "\u0007" -private def opaqueScreen (scheme : ColorScheme) (size : Size) (content : Text) - (copyPending : Option String := none) : Text := +private +def opaqueScreen + (scheme : ColorScheme) + (size : Size) + (content : Text) + (copyPending : Option String := none) + : Text := let width := max 1 size.columns let rows := max 1 size.rows let blank := Text.styled (String.ofList (List.replicate width ' ')) @@ -417,29 +495,48 @@ private def opaqueScreen (scheme : ColorScheme) (size : Size) (content : Text) | some value => screen ++ Text.plain (clipboardSequence value) | none => screen -def formatElapsed (milliseconds : Nat) : String := +def formatElapsed + (milliseconds : Nat) + : String := if milliseconds == 0 then "<1 ms" else if milliseconds < 1_000 then s!"{milliseconds} ms" else s!"{milliseconds / 1_000}.{milliseconds % 1_000 / 100} s" -private def diagnosticView (scheme : ColorScheme) (width : Nat) (sources : Sources) - (diagnostic : Diagnostic) : Text := +private +def diagnosticView + (scheme : ColorScheme) + (width : Nat) + (sources : Sources) + (diagnostic : Diagnostic) + : Text := TermColor.Diagnostics.render sources diagnostic { width := max 1 (frameWidth width - 2), contextLines := 0, hyperlinks := false } scheme -private def identifierChar (character : Char) : Bool := +private +def identifierChar + (character : Char) + : Bool := character.isAlpha || character.isDigit || character == '_' || character == '$' || character == '\'' -private def roleStyle (semantic : SemanticColors) : _root_.TPTP.Role → Option Style +private +def roleStyle + (semantic : SemanticColors) + : _root_.TPTP.Role → + Option Style | .axiom | .hypothesis | .definition | .assumption | .lemma | .theorem | .corollary | .conjecture | .negatedConjecture | .plain | .type | .interpretation | .logic | .unknown | .finiteDomain | .finiteFunctor | .finitePredicate => some (Style.fg semantic.role) | .other _ => none -private def symbolStyle (scheme : ColorScheme) (symbols : Array Symbol) (token : String) - (highlightSyntax : Bool := true) : Style := +private +def symbolStyle + (scheme : ColorScheme) + (symbols : Array Symbol) + (token : String) + (highlightSyntax : Bool := true) + : Style := let lower := token.toLower let semantic := semanticColors scheme if token.startsWith "/" then Style.bold <+> Style.fg scheme.orange @@ -463,14 +560,23 @@ private def symbolStyle (scheme : ColorScheme) (symbols : Array Symbol) (token : | .predicate => Style.fg semantic.predicateColor | none => Style.fg scheme.foreground -private def operatorStyle (scheme : ColorScheme) (token : String) : Style := +private +def operatorStyle + (scheme : ColorScheme) + (token : String) + : Style := if token == "!" || token == "?" then Style.fg scheme.pink else if token == "(" || token == ")" || token == "[" || token == "]" || token == "," || token == ":" || token == "." || token == ";" then Style.fg scheme.purple else Style.fg scheme.blue -private def semanticText (scheme : ColorScheme) (symbols : Array Symbol) (value : String) - (highlightSyntax : Bool := true) : Text := +private +def semanticText + (scheme : ColorScheme) + (symbols : Array Symbol) + (value : String) + (highlightSyntax : Bool := true) + : Text := let flush := fun (state : Text × String) => if state.2.isEmpty then state else (state.1 ++ Text.styled state.2 @@ -492,11 +598,19 @@ private def semanticText (scheme : ColorScheme) (symbols : Array Symbol) (value (state.1 ++ Text.plain token, "") (flush (value.toList.foldl step (Text.empty, ""))).1 -private def semanticFormula (scheme : ColorScheme) (formula : FormulaView) : Text := +private +def semanticFormula + (scheme : ColorScheme) + (formula : FormulaView) + : Text := semanticText scheme formula.symbols formula.formula -private def formulaLine (scheme : ColorScheme) (selected : Option Nat) - (formula : FormulaView) : Text := +private +def formulaLine + (scheme : ColorScheme) + (selected : Option Nat) + (formula : FormulaView) + : Text := let marker := if selected == some formula.id then "▸ " else " " Text.styled s!"{marker}index #{formula.id} • cell {formula.cell} • {formula.role} " (Style.dim <+> Style.fg scheme.comment) ++ @@ -513,20 +627,35 @@ private def reportWidgetConfig (scheme : ColorScheme) : CollapsibleConfig := { overflowText := Text.styled "… more" (Style.dim <+> Style.fg scheme.comment) emptyText := Text.styled "(no report details)" (Style.dim <+> Style.fg scheme.comment) } -private def reportSummary (scheme : ColorScheme) (report : Report) : Text := +private +def reportSummary + (scheme : ColorScheme) + (report : Report) + : Text := let marker := match report.severity with | .error => Text.styled "issues" (Style.bold <+> Style.fg scheme.red) | .warning => Text.styled "warning" (Style.bold <+> Style.fg scheme.yellow) | _ => Text.styled "check" (Style.bold <+> Style.fg scheme.green) marker ++ Text.plain s!" • {report.title} • click to expand • Ctrl-R full output" -private def reportBody (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat) - (entry : TranscriptEntry) (report : Report) : Text := +private +def reportBody + (scheme : ColorScheme) + (symbols : Array Symbol) + (width : Nat) + (entry : TranscriptEntry) + (report : Report) + : Text := renderReport report { width := max 1 (width - 6) } scheme ++ Text.plain "\n" ++ semanticText scheme symbols entry.output false -private def transcriptLine (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat) - (entry : TranscriptEntry) : Text := +private +def transcriptLine + (scheme : ColorScheme) + (symbols : Array Symbol) + (width : Nat) + (entry : TranscriptEntry) + : Text := let input := Text.styled s!"[{entry.cell}] " (Style.dim <+> Style.fg scheme.comment) ++ Text.styled "› " (Style.bold <+> Style.fg scheme.orange) ++ semanticText scheme symbols entry.input false @@ -558,13 +687,21 @@ private def transcriptLine (scheme : ColorScheme) (symbols : Array Symbol) (widt (Style.dim <+> Style.fg scheme.comment)) |>.getD Text.empty input ++ Text.plain "\n" ++ output ++ timing -private def spacedEntries : List Text → List Text +private +def spacedEntries + : List Text → + List Text | [] => [] | [entry] => [entry] | entry :: rest => entry :: Text.empty :: spacedEntries rest -private def transcriptLines (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat) - (entries : List TranscriptEntry) : List Text := +private +def transcriptLines + (scheme : ColorScheme) + (symbols : Array Symbol) + (width : Nat) + (entries : List TranscriptEntry) + : List Text := let views := entries.reverse.map (transcriptLine scheme symbols width) (spacedEntries views).flatMap splitLines @@ -575,7 +712,10 @@ private def reportWidget (scheme : ColorScheme) (symbols : Array Symbol) (width (reportSummary scheme report) (reportBody scheme symbols width entry report) { expanded := entry.reportExpanded } -def reportAtTranscriptRow (app : App) (width row : Nat) : Option Nat := +def reportAtTranscriptRow + (app : App) + (width row : Nat) + : Option Nat := let rec find : List TranscriptEntry → Nat → Option Nat | [], _ => none | entry :: rest, offset => @@ -590,19 +730,30 @@ def reportAtTranscriptRow (app : App) (width row : Nat) : Option Nat := | _, _ => find rest (offset + lineCount + 1) find app.entries.reverse 0 -def toggleReportCell (app : App) (cell : Nat) : App := +def toggleReportCell + (app : App) + (cell : Nat) + : App := { app with entries := app.entries.map fun entry => if entry.cell == cell then { entry with reportExpanded := !entry.reportExpanded } else entry } -private def visibleTranscriptLines (app : App) (width budget : Nat) : List Text := +private +def visibleTranscriptLines + (app : App) + (width budget : Nat) + : List Text := let lines := transcriptLines app.theme app.session.symbols width app.entries let scroll := min app.transcriptScroll (lines.length - budget) let visibleEnd := lines.length - scroll let start := visibleEnd - min budget visibleEnd (lines.drop start).take (visibleEnd - start) -private def transcript (app : App) (width budget bodyStart : Nat) : Text := +private +def transcript + (app : App) + (width budget bodyStart : Nat) + : Text := let lines := visibleTranscriptLines app width budget if lines.isEmpty then Text.styled "Type a TPTP statement or /help." (Style.dim <+> Style.fg app.theme.comment) @@ -620,25 +771,43 @@ private def transcript (app : App) (width budget bodyStart : Nat) : Text := else line | _, _ => body -private def selectionLines (app : App) (width budget : Nat) : List String := +private +def selectionLines + (app : App) + (width budget : Nat) + : List String := (visibleTranscriptLines app width budget).map (·.plainText) -def scrollTranscriptUp (app : App) : App := +def scrollTranscriptUp + (app : App) + : App := { app with transcriptScroll := app.transcriptScroll + 3 } -def scrollTranscriptDown (app : App) : App := +def scrollTranscriptDown + (app : App) + : App := { app with transcriptScroll := app.transcriptScroll - min 3 app.transcriptScroll } -def scrollTranscriptPageUp (app : App) : App := +def scrollTranscriptPageUp + (app : App) + : App := { app with transcriptScroll := app.transcriptScroll + 10 } -def scrollTranscriptPageDown (app : App) : App := +def scrollTranscriptPageDown + (app : App) + : App := { app with transcriptScroll := app.transcriptScroll - min 10 app.transcriptScroll } -def clearSelection (app : App) : App := +def clearSelection + (app : App) + : App := { app with selectionStart := none, selectionEnd := none } -private def symbolLine (scheme : ColorScheme) (symbol : Symbol) : Text := +private +def symbolLine + (scheme : ColorScheme) + (symbol : Symbol) + : Text := let kind := match symbol.kind with | .variable => "var" | .constant => "const" @@ -649,7 +818,11 @@ private def symbolLine (scheme : ColorScheme) (symbol : Symbol) : Text := Text.styled symbol.name (symbolStyle scheme #[symbol] symbol.name) ++ Text.styled s!"/{symbol.arity}" (Style.dim <+> Style.fg scheme.comment) -private def contextWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where +private +def contextWidgetConfig + (scheme : ColorScheme) + : CollapsibleConfig + where collapsedMarker := Text.styled "▸ " (Style.fg scheme.comment) expandedMarker := Text.styled "▾ " (Style.fg scheme.orange) summaryStyle := Style.bold <+> Style.fg scheme.purple @@ -660,7 +833,10 @@ private def contextWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where overflowText := Text.styled "… more" (Style.dim <+> Style.fg scheme.comment) emptyText := Text.styled "(none)" (Style.dim <+> Style.fg scheme.comment) -private def contextSections (app : App) : List (Nat × Text × Text) := +private +def contextSections + (app : App) + : List (Nat × Text × Text) := let formulas := app.session.formulas.toList.reverse.take 8 let symbols := app.session.symbols.toList.take 12 let problem := if app.session.context.isEmpty then @@ -703,14 +879,26 @@ private def contextSections (app : App) : List (Nat × Text × Text) := #guard (contextSections ({} : App)).isEmpty -private def contextExpandedAt (app : App) (index : Nat) : Bool := +private +def contextExpandedAt + (app : App) + (index : Nat) + : Bool := app.contextExpanded.getD index true -private def contextState (app : App) (index : Nat) : CollapsibleState := +private +def contextState + (app : App) + (index : Nat) + : CollapsibleState := { expanded := contextExpandedAt app index focused := app.contextFocus == index } -private def contextRenders (app : App) (width : Nat) : List (Nat × CollapsibleRender) := +private +def contextRenders + (app : App) + (width : Nat) + : List (Nat × CollapsibleRender) := let innerWidth := max 1 (boxInnerWidth width) let rec go : List (Nat × Text × Text) → List (Nat × CollapsibleRender) | [] => [] @@ -719,10 +907,17 @@ private def contextRenders (app : App) (width : Nat) : List (Nat × CollapsibleR (contextState app index)) :: go sections go (contextSections app) -private def contextTexts (app : App) (width : Nat) : List Text := +private +def contextTexts + (app : App) + (width : Nat) + : List Text := (contextRenders app width).map (fun (_, widget) => widget.text) -def contextHitAtRow (app : App) (width row : Nat) : Option (Nat × Bool) := +def contextHitAtRow + (app : App) + (width row : Nat) + : Option (Nat × Bool) := if row < 2 then none else let relativeRow := row - 2 @@ -734,7 +929,10 @@ def contextHitAtRow (app : App) (width row : Nat) : Option (Nat × Bool) := else find renders (offset + widget.lineCount) find (contextRenders app width) 0 -def contextFormulaAtRow (app : App) (width row : Nat) : Option Nat := +def contextFormulaAtRow + (app : App) + (width row : Nat) + : Option Nat := match contextHitAtRow app width row with | some (0, false) => let relativeRow := row - 2 @@ -746,16 +944,31 @@ def contextFormulaAtRow (app : App) (width row : Nat) : Option Nat := | [] => none | _ => none -private def updateContextExpanded (app : App) (index : Nat) (expanded : Bool) : App := +private +def updateContextExpanded + (app : App) + (index : Nat) + (expanded : Bool) + : App := { app with contextExpanded := app.contextExpanded.set! index expanded } -def focusContext (app : App) (index : Nat) : App := +def focusContext + (app : App) + (index : Nat) + : App := { app with contextFocus := min (contextSectionCount - 1) index } -private def visibleContextIndices (app : App) : Array Nat := +private +def visibleContextIndices + (app : App) + : Array Nat := (contextSections app).map (fun (index, _, _) => index) |>.toArray -private def moveContext (app : App) (forward : Bool) : App := +private +def moveContext + (app : App) + (forward : Bool) + : App := let indices := visibleContextIndices app if indices.isEmpty then app @@ -768,21 +981,37 @@ private def moveContext (app : App) (forward : Bool) : App := let offset := if forward then 1 else indices.size - 1 focusContext app (indices[(current + offset) % indices.size]?.getD app.contextFocus) -def focusNextContext (app : App) : App := +def focusNextContext + (app : App) + : App := moveContext app true -def focusPreviousContext (app : App) : App := +def focusPreviousContext + (app : App) + : App := moveContext app false -private def formulaIds (app : App) : List Nat := +private +def formulaIds + (app : App) + : List Nat := app.session.formulas.toList.reverse.map (·.id) -private def indexOfFormula : Nat → Nat → List Nat → Option Nat +private +def indexOfFormula + : Nat → + Nat → + List Nat → + Option Nat | _, _, [] => none | wanted, index, id :: ids => if wanted == id then some index else indexOfFormula wanted (index + 1) ids -private def nextFormulaId (app : App) (forward : Bool) : Option Nat := +private +def nextFormulaId + (app : App) + (forward : Bool) + : Option Nat := let ids := formulaIds app |>.take 8 match ids with | [] => none @@ -793,66 +1022,99 @@ private def nextFormulaId (app : App) (forward : Bool) : Option Nat := let index := (indexOfFormula current 0 ids).getD 0 if forward then ids[index + 1]? else if index == 0 then none else ids[index - 1]? -def focusContextItem (app : App) (id : Nat) : App := +def focusContextItem + (app : App) + (id : Nat) + : App := if app.session.formulas.any (·.id == id) then { app with contextFocus := 0, contextItemFocus := some id } else app -def focusNextContextItem (app : App) : App := +def focusNextContextItem + (app : App) + : App := match nextFormulaId app true with | some id => focusContextItem app id | none => { app with contextItemFocus := none } -def focusPreviousContextItem (app : App) : App := +def focusPreviousContextItem + (app : App) + : App := match nextFormulaId app false with | some id => focusContextItem app id | none => { app with contextItemFocus := none } -def focusNextContextEntry (app : App) : App := +def focusNextContextEntry + (app : App) + : App := if app.contextFocus == 0 && app.session.formulas.isEmpty == false then match nextFormulaId app true with | some id => focusContextItem app id | none => moveContext app true else focusNextContext app -def focusPreviousContextEntry (app : App) : App := +def focusPreviousContextEntry + (app : App) + : App := if app.contextFocus == 0 && app.session.formulas.isEmpty == false then match nextFormulaId app false with | some id => focusContextItem app id | none => moveContext app false else focusPreviousContext app -def toggleFocusedContext (app : App) : App := +def toggleFocusedContext + (app : App) + : App := updateContextExpanded app app.contextFocus (!contextExpandedAt app app.contextFocus) -def expandFocusedContext (app : App) : App := +def expandFocusedContext + (app : App) + : App := updateContextExpanded app app.contextFocus true -def collapseFocusedContext (app : App) : App := +def collapseFocusedContext + (app : App) + : App := updateContextExpanded app app.contextFocus false -def focusProver (app : App) (index : Nat) : App := +def focusProver + (app : App) + (index : Nat) + : App := let focus := if app.proverChoices.isEmpty then 0 else min (app.proverChoices.size - 1) index { app with proverFocus := focus } -def focusNextProver (app : App) : App := +def focusNextProver + (app : App) + : App := focusProver app ((app.proverFocus + 1) % max 1 app.proverChoices.size) -def focusPreviousProver (app : App) : App := +def focusPreviousProver + (app : App) + : App := focusProver app (if app.proverFocus == 0 then max 1 app.proverChoices.size - 1 else app.proverFocus - 1) -def focusRun (app : App) (index : Nat) : App := +def focusRun + (app : App) + (index : Nat) + : App := let focus := if app.runRows.isEmpty then 0 else min (app.runRows.size - 1) index { app with runFocus := focus } -def focusNextRun (app : App) : App := +def focusNextRun + (app : App) + : App := focusRun app ((app.runFocus + 1) % max 1 app.runRows.size) -def focusPreviousRun (app : App) : App := +def focusPreviousRun + (app : App) + : App := focusRun app (if app.runFocus == 0 then max 1 app.runRows.size - 1 else app.runFocus - 1) -def toggleFocusedProver (app : App) : App := +def toggleFocusedProver + (app : App) + : App := if app.proverChoices.isEmpty then app else let reference := app.proverChoices[app.proverFocus]! let enabled := app.enabledProvers.any (· == reference) @@ -863,13 +1125,20 @@ def toggleFocusedProver (app : App) : App := { updated with statusNotice := some s!"{ProverReference.display reference} { if enabled then "disabled" else "enabled"}" } -def contextTargetNames : List String := +def contextTargetNames + : List String := ContextTarget.all.map ContextTarget.name -def contextTargetOfString (value : String) : Option Nat := +def contextTargetOfString + (value : String) + : Option Nat := ContextTarget.indexOfString value -private def prepareContextCommand (app : App) (command : String) : App := +private +def prepareContextCommand + (app : App) + (command : String) + : App := match app.contextItemFocus with | none => { app with statusNotice := some "select a formula in the FORMULAS box first" } | some id => @@ -890,7 +1159,10 @@ def removeContextItem (app : App) : App := prepareContextCommand app "remove" def editContextItem (app : App) : App := prepareContextCommand app "update" -def openContextTarget (app : App) (target : String) : Option App := +def openContextTarget + (app : App) + (target : String) + : Option App := if target.toLower == "all" then let app := { app with stateOpen := true } some { app with contextExpanded := Array.replicate contextSectionCount true } @@ -901,7 +1173,9 @@ def openContextTarget (app : App) (target : String) : Option App := some (if index == 0 then focusNextContextItem app else app) | none => none -def toggleStatePanel (app : App) : App := +def toggleStatePanel + (app : App) + : App := if app.stateOpen && app.panelFocus == .drawer then { app with stateOpen := false, panelFocus := .main } else @@ -912,7 +1186,9 @@ def toggleStatePanel (app : App) : App := runOpen := false panelFocus := .drawer } -def toggleHistoryPanel (app : App) : App := +def toggleHistoryPanel + (app : App) + : App := if app.historyOpen && app.panelFocus == .drawer then { app with historyOpen := false, panelFocus := .main } else @@ -923,7 +1199,9 @@ def toggleHistoryPanel (app : App) : App := runOpen := false panelFocus := .drawer } -def toggleRunPanel (app : App) : App := +def toggleRunPanel + (app : App) + : App := if app.runRows.isEmpty then { app with statusNotice := some "no prover run to inspect" } else if app.runOpen && app.panelFocus == .drawer then @@ -936,7 +1214,11 @@ def toggleRunPanel (app : App) : App := proversOpen := false panelFocus := .drawer } -private def contextPanel (app : App) (width height : Nat) : Text := +private +def contextPanel + (app : App) + (width height : Nat) + : Text := let body := joinLines (contextTexts app width) let innerWidth := boxInnerWidth width let body := padRight innerWidth (fillHeight (max 1 (height - 2)) body) @@ -947,7 +1229,11 @@ private def contextPanel (app : App) (width height : Nat) : Text := , borderStyle := Style.fg (if active then app.theme.selection else app.theme.comment) , maxWidth := some width } -private def historyWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where +private +def historyWidgetConfig + (scheme : ColorScheme) + : CollapsibleConfig + where collapsedMarker := Text.styled "▸ " (Style.fg scheme.comment) expandedMarker := Text.styled "▾ " (Style.fg scheme.orange) summaryStyle := Style.bold <+> Style.fg scheme.purple @@ -957,8 +1243,12 @@ private def historyWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where overflowText := Text.styled "… more" (Style.dim <+> Style.fg scheme.comment) emptyText := Text.styled "(empty help)" (Style.dim <+> Style.fg scheme.comment) -private def historyWidget (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntry) : - Option CollapsibleRender := +private +def historyWidget + (app : App) + (width : Nat) + (entry : OATP.Repl.HistoryEntry) + : Option CollapsibleRender := if entry.input.startsWith "/help" then let expanded := app.historyExpanded.any (· == entry.cell) let lines := entry.result.splitOn "\n" |>.length @@ -968,7 +1258,12 @@ private def historyWidget (app : App) (width : Nat) (entry : OATP.Repl.HistoryEn (max 1 (boxInnerWidth width - 2)) summary (Text.plain entry.result) { expanded } else none -private def historyLine (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntry) : Text := +private +def historyLine + (app : App) + (width : Nat) + (entry : OATP.Repl.HistoryEntry) + : Text := let input := Text.styled s!"[{entry.cell}] " (Style.dim <+> Style.fg app.theme.comment) ++ semanticText app.theme app.session.symbols entry.input false match historyWidget app width entry with @@ -978,7 +1273,11 @@ private def historyLine (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntr semanticText app.theme app.session.symbols (fitText (max 1 (width - 6)) entry.result).plainText false -private def historyPanel (app : App) (width height : Nat) : Text := +private +def historyPanel + (app : App) + (width height : Nat) + : Text := let rows := app.session.history.toList.reverse.take 18 let body := if rows.isEmpty then Text.styled "No commands yet." (Style.dim <+> Style.fg app.theme.comment) @@ -989,7 +1288,10 @@ private def historyPanel (app : App) (width height : Nat) : Text := (Style.bold <+> Style.fg app.theme.cyan)) , borderStyle := Style.fg app.theme.selection, maxWidth := some width } -def historyCellAtRow (app : App) (width row : Nat) : Option Nat := +def historyCellAtRow + (app : App) + (width row : Nat) + : Option Nat := let rows := app.session.history.toList.reverse.take 18 let rec find : List OATP.Repl.HistoryEntry → Nat → Option Nat | [], _ => none @@ -1002,17 +1304,27 @@ def historyCellAtRow (app : App) (width row : Nat) : Option Nat := if hit then some entry.cell else find rest (offset + line.height + 1) find rows 0 -def toggleHistoryCell (app : App) (cell : Nat) : App := +def toggleHistoryCell + (app : App) + (cell : Nat) + : App := let expanded := if app.historyExpanded.any (· == cell) then app.historyExpanded.filter (· != cell) else app.historyExpanded.push cell { app with historyExpanded := expanded } -def proverVisibleStart (app : App) (height : Nat) : Nat := +def proverVisibleStart + (app : App) + (height : Nat) + : Nat := let visible := max 1 (height - 2) if app.proverFocus >= visible then app.proverFocus - visible + 1 else 0 -private def proverPanel (app : App) (width height : Nat) : Text := +private +def proverPanel + (app : App) + (width height : Nat) + : Text := let visible := max 1 (height - 2) let start := proverVisibleStart app height let rows := if app.proverChoices.isEmpty then @@ -1035,13 +1347,20 @@ private def proverPanel (app : App) (width height : Nat) : Text := , borderStyle := Style.fg (if active then app.theme.selection else app.theme.comment) , maxWidth := some width } -private def runStatusStyle (scheme : ColorScheme) : RunStatus → Style +private +def runStatusStyle + (scheme : ColorScheme) + : RunStatus → + Style | .result .theorem | .result .unsatisfiable => Style.bold <+> Style.fg scheme.green | .running | .queued => Style.fg scheme.yellow | .result .error | .failed => Style.bold <+> Style.fg scheme.red | _ => Style.fg scheme.comment -private def runDetail (row : RunRow) : String := +private +def runDetail + (row : RunRow) + : String := if !row.detail.isEmpty then row.detail else match row.status with | .queued => "queued; waiting for the previous prover" | .running => "waiting for the prover result" @@ -1049,7 +1368,11 @@ private def runDetail (row : RunRow) : String := | .failed => "the prover failed without additional output" | .cancelled => "run cancelled" -private def runPanel (app : App) (width height : Nat) : Text := +private +def runPanel + (app : App) + (width height : Nat) + : Text := let innerWidth := boxInnerWidth width let rows := if app.runRows.isEmpty then [Text.styled "No active prover run." (Style.dim <+> Style.fg app.theme.comment)] @@ -1076,7 +1399,10 @@ private def runPanel (app : App) (width height : Nat) : Text := , borderStyle := Style.fg (if active then app.theme.selection else app.theme.comment) , maxWidth := some width } -private def mascot (scheme : ColorScheme) : Text := +private +def mascot + (scheme : ColorScheme) + : Text := let arrow := Text.styled "──▶" (Style.fg scheme.cyan) joinLines [ Text.styled "TPTP" (Style.fg scheme.yellow) ++ Text.plain " " ++ arrow ++ Text.plain " " ++ Text.styled "OATP" (Style.bold <+> Style.fg scheme.green) ++ @@ -1085,7 +1411,11 @@ private def mascot (scheme : ColorScheme) : Text := , Text.plain " " ++ Text.styled "▼" (Style.fg scheme.cyan) , Text.plain " " ++ Text.styled "LEAN ✓" (Style.fg scheme.blue) ] -private def banner (scheme : ColorScheme) (width : Nat) : Text := +private +def banner + (scheme : ColorScheme) + (width : Nat) + : Text := let outer := frameWidth width let inner := boxInnerWidth outer let leftContent := @@ -1133,7 +1463,11 @@ private def banner (scheme : ColorScheme) (width : Nat) : Text := , titleAlignment := .left, borderStyle := Style.fg scheme.orange , maxWidth := some outer } -private def compactHeader (scheme : ColorScheme) (width : Nat) : Text := +private +def compactHeader + (scheme : ColorScheme) + (width : Nat) + : Text := let outer := frameWidth width let title := s!" oatp repl v{version} " let used := title.length + 2 @@ -1142,14 +1476,22 @@ private def compactHeader (scheme : ColorScheme) (width : Nat) : Text := Text.styled (String.ofList (List.replicate (if outer > used then outer - used else 0) '─')) (Style.fg scheme.selection) -def reportAtScreenRow (app : App) (size : Size) (row : Nat) : Option Nat := +def reportAtScreenRow + (app : App) + (size : Size) + (row : Nat) + : Option Nat := let width := frameWidth size.columns let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width let bodyStart := head.height + 1 if row < bodyStart then none else reportAtTranscriptRow app width (row - bodyStart) -def prompt (scheme : ColorScheme) (width : Nat) (state : Repl.State) - (focused : Bool := true) : Text := +def prompt + (scheme : ColorScheme) + (width : Nat) + (state : Repl.State) + (focused : Bool := true) + : Text := let outer := frameWidth width let input := box (Text.styled "› " (Style.bold <+> Style.fg scheme.orange) ++ TermColor.Repl.renderMultilineTextInputBody @@ -1165,7 +1507,11 @@ def prompt (scheme : ColorScheme) (width : Nat) (state : Repl.State) textStyle := Style.fg scheme.foreground kindStyle := Style.dim <+> Style.fg scheme.comment } menu -private def footer (app : App) (width : Nat) : Text := +private +def footer + (app : App) + (width : Nat) + : Text := let outer := frameWidth width let state := if app.busy then "[BUSY]" else "[READY]" let closeRun := appKeyLabel .closeRun .runInput @@ -1209,7 +1555,10 @@ private def footer (app : App) (width : Nat) : Text := , truncate rightWidth (Text.styled hint (Style.dim <+> Style.fg app.theme.comment)) ] [.left, .left] -def selectedText (app : App) (size : Size) : String := +def selectedText + (app : App) + (size : Size) + : String := let width := frameWidth size.columns let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width let foot := prompt app.theme width app.repl (app.panelFocus == .main) ++ @@ -1227,7 +1576,11 @@ def selectedText (app : App) (size : Size) : String := String.intercalate "\n" (lines.drop low |>.take (high - low + 1)) | _, _ => "" -private def calcContent (app : App) (size : Size) : Text := +private +def calcContent + (app : App) + (size : Size) + : Text := let width := frameWidth size.columns let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width let foot := prompt app.theme width app.repl (app.panelFocus == .main) ++ @@ -1237,7 +1590,10 @@ private def calcContent (app : App) (size : Size) : Text := let body := transcript app width budget (head.height + 1) head ++ Text.plain "\n" ++ fillHeight budget body ++ Text.plain "\n" ++ foot -def screen (app : App) (size : Size) : Text := +def screen + (app : App) + (size : Size) + : Text := let width := frameWidth size.columns let size := { size with columns := width } let drawerOpen := app.runOpen || app.proversOpen || diff --git a/OATP/Runtime.lean b/OATP/Runtime.lean index 89219b0..943c217 100644 --- a/OATP/Runtime.lean +++ b/OATP/Runtime.lean @@ -56,7 +56,9 @@ def catalogueLocation (cacheNamespace endpoint : String) : let directory := System.FilePath.join root cacheName (directory, System.FilePath.join directory s!"systems-{hash normalizedEndpoint}.html") -def httpErrorMessage : OATP.Http.Error → String +def httpErrorMessage + : OATP.Http.Error → + String | .io message => s!"HTTP IO failed: {message}" | .invalidRequest message => s!"invalid HTTP request: {message}" | .transport message => s!"HTTP transport failed: {message}" diff --git a/OATP/SystemOnTPTP.lean b/OATP/SystemOnTPTP.lean index 2466222..4a71687 100644 --- a/OATP/SystemOnTPTP.lean +++ b/OATP/SystemOnTPTP.lean @@ -40,7 +40,9 @@ def isOnlineReference (reference : String) : Bool := reference.startsWith online def onlineReference (systemId : String) : String := onlineReferencePrefix ++ systemId -def onlineSystemId (reference : String) : String := +def onlineSystemId + (reference : String) + : String := if isOnlineReference reference then (reference.drop onlineReferencePrefix.length).toString else reference @@ -60,19 +62,30 @@ private inductive HtmlPart where open Grip GParser -private def htmlTag : GParser conditional HtmlPart := +private +def htmlTag + : GParser conditional HtmlPart := HtmlPart.tag <$> GParser.capture (GParser.ch '<' *> GParser.takeWhile (· != 62) <* GParser.ch '>') -private def htmlText : GParser conditional HtmlPart := +private +def htmlText + : GParser conditional HtmlPart := HtmlPart.text <$> GParser.capture (GParser.takeWhile1 (· != 60)) -private def htmlPart : GParser conditional HtmlPart := +private +def htmlPart + : GParser conditional HtmlPart := GParser.chooseG htmlTag [htmlText] -private def htmlDocument : Grip.Parser (List HtmlPart) := +private +def htmlDocument + : Grip.Parser (List HtmlPart) := GParser.seqL (GParser.many htmlPart) GParser.eof -private def parseHtml (source : String) : Except Grip.ParseError (List HtmlPart) := +private +def parseHtml + (source : String) + : Except Grip.ParseError (List HtmlPart) := htmlDocument.parse source.toUTF8 namespace Catalogue @@ -83,29 +96,44 @@ structure SystemInfo where timeLimit : Nat := defaultSystemTimeLimit deriving BEq, DecidableEq, Repr -private def quotedAfter (marker line : String) : Option String := +private +def quotedAfter + (marker line : String) + : Option String := match line.splitOn marker with | _ :: value :: _ => some (value.splitOn "\"" |>.headD "") | _ => none -private def systemId (line : String) : Option String := +private +def systemId + (line : String) + : Option String := (quotedAfter "NAME=\"System___" line).orElse fun _ => quotedAfter "name=\"System___" line -private def fieldValue (field id current line : String) : String := +private +def fieldValue + (field id current line : String) + : String := let lower := quotedAfter s!"name=\"{field}___{id}\"" line let upper := quotedAfter s!"NAME=\"{field}___{id}\"" line if lower.isSome || upper.isSome then (quotedAfter "value=\"" line).getD current else current -private def updateInfo (line : String) (system : SystemInfo) : SystemInfo := +private +def updateInfo + (line : String) + (system : SystemInfo) + : SystemInfo := let command := fieldValue "Command" system.id system.command line let timeLimit := (fieldValue "TimeLimit" system.id (toString system.timeLimit) line).toNat?.getD system.timeLimit { system with command, timeLimit } -def parse (html : String) : Array SystemInfo := +def parse + (html : String) + : Array SystemInfo := match parseHtml html with | .error _ => #[] | .ok parts => parts.foldl (init := #[]) fun systems part => @@ -121,22 +149,34 @@ def parse (html : String) : Array SystemInfo := def baseName (id : String) : String := id.splitOn "---" |>.headD id -def matchesReference (reference : String) (system : SystemInfo) : Bool := +def matchesReference + (reference : String) + (system : SystemInfo) + : Bool := let reference := onlineSystemId reference let wanted := reference.toLower let id := system.id.toLower id == wanted || (baseName system.id).toLower == wanted || id.startsWith (wanted ++ "---") -def resolve (systems : Array SystemInfo) (reference : String) : Option SystemInfo := +def resolve + (systems : Array SystemInfo) + (reference : String) + : Option SystemInfo := systems.toList.find? (matchesReference reference) end Catalogue -def labels (config : Config) : Array String := +def labels + (config : Config) + : Array String := if config.systemLabels.isEmpty then #[config.systemLabel] else config.systemLabels -private def command (config : Config) (label : String) : String := +private +def command + (config : Config) + (label : String) + : String := config.systemCommands.toList.find? (·.1 == label) |>.map (·.2) |>.getD "default" inductive ResponseError where @@ -146,13 +186,18 @@ inductive ResponseError where | malformedBody (message : String) deriving Repr -def ResponseError.message : ResponseError → String +def ResponseError.message + : ResponseError → + String | .httpStatus status => s!"SystemOnTPTP returned HTTP {status}" | .missingStatus => "SystemOnTPTP response did not contain an SZS status" | .unsupportedStatus status => s!"SystemOnTPTP returned unsupported SZS status `{status}`" | .malformedBody message => s!"SystemOnTPTP response was not valid HTML: {message}" -def fields (config : Config) (problem : Problem) : Array Field := +def fields + (config : Config) + (problem : Problem) + : Array Field := let base : Array Field := #[ { name := "ProblemSource", value := "FORMULAE" }, { name := "FORMULAEProblem", value := problem.source }, @@ -169,7 +214,11 @@ def fields (config : Config) (problem : Problem) : Array Field := { name := s!"Transform___{label}", value := "none" } ]) base -def request (config : Config) (problem : Problem) : Http.Request where +def request + (config : Config) + (problem : Problem) + : Http.Request + where method := .post url := config.endpoint body := encodeUrlEncoded (fields config problem) @@ -196,10 +245,17 @@ def submit (config : Config) (problem : Problem) : OATP.Artifacts.write run "response.error" (Http.Error.message error) pure response -private def tagStarts (needle : String) (tag : String) : Bool := +private +def tagStarts + (needle : String) + (tag : String) + : Bool := tag.toLower.startsWith needle -private def bodyText (parts : List HtmlPart) : String := +private +def bodyText + (parts : List HtmlPart) + : String := let hasBody := parts.any fun part => match part with | .tag tag => tagStarts " false @@ -219,11 +275,16 @@ private def bodyText (parts : List HtmlPart) : String := else collect inside rest String.intercalate "" (collect (!hasBody) parts) -private def decodeHtmlEntities (value : String) : String := +private +def decodeHtmlEntities + (value : String) + : String := value.replace ">" ">" |>.replace "<" "<" |>.replace "&" "&" |>.replace """ "\"" |>.replace "'" "'" -def parseResponseText (body : String) : Except Grip.ParseError String := +def parseResponseText + (body : String) + : Except Grip.ParseError String := let body := body.trimAscii.toString if !body.startsWith " .error error | .ok parts => .ok <| decodeHtmlEntities (bodyText parts).trimAscii.toString -def responseText (body : String) : String := +def responseText + (body : String) + : String := match parseResponseText body with | .ok text => text | .error _ => body -def catalogueRequest (endpoint : String) : Http.Request where +def catalogueRequest + (endpoint : String) + : Http.Request + where method := .get url := if endpoint == defaultEndpoint then defaultCatalogueEndpoint else endpoint maxSeconds := defaultCatalogueTimeoutSeconds maxBodyBytes := defaultCatalogueMaxBodyBytes maxRequestBodyBytes := defaultCatalogueMaxBodyBytes -def fetchCatalogue (endpoint : String) : IO (Except Http.Error Http.Response) := +def fetchCatalogue + (endpoint : String) + : IO (Except Http.Error Http.Response) := Http.requestWithTransport (catalogueRequest endpoint) def parseResponse (config : Config) (problem : Problem) (response : Http.Response) : diff --git a/OATP/TPTP.lean b/OATP/TPTP.lean index 32d0a27..2373188 100644 --- a/OATP/TPTP.lean +++ b/OATP/TPTP.lean @@ -33,15 +33,21 @@ def defaultTheory : String := supportedTheories.headD "fof" def theoryChoices : List String := supportedTheories ++ theoryAliases.map Prod.fst -def normalizeTheory (value : String) : Option String := +def normalizeTheory + (value : String) + : Option String := let value := value.toLower if value ∈ supportedTheories then some value else theoryAliases.find? (·.1 == value) |>.map Prod.snd -def parse (source : String) : Except Grip.ParseError Document := +def parse + (source : String) + : Except Grip.ParseError Document := _root_.TPTP.parseString source -def parseStatement (source : String) : Except Grip.ParseError Statement := +def parseStatement + (source : String) + : Except Grip.ParseError Statement := _root_.TPTP.parseStatementString source namespace Syntax @@ -49,7 +55,9 @@ namespace Syntax abbrev Term := _root_.TPTP.Formula.Term abbrev Formula := _root_.TPTP.Formula.Expr -def parseFormula (source : String) : Except Grip.ParseError Formula := +def parseFormula + (source : String) + : Except Grip.ParseError Formula := _root_.TPTP.Formula.parseFormulaString source end Syntax @@ -66,8 +74,9 @@ def ofFof (name : String) (role : Role) (formula : _root_.TPTP.Formula.Expr) : formula } -def parseFormula (statement : _root_.TPTP.Statement) : - Except Grip.ParseError _root_.TPTP.Formula.Expr := +def parseFormula + (statement : _root_.TPTP.Statement) + : Except Grip.ParseError _root_.TPTP.Formula.Expr := _root_.TPTP.Statement.parseFormula statement end Statement @@ -76,7 +85,11 @@ end OATP.TPTP namespace OATP -def Problem.ofStatement (name : String) (statement : _root_.TPTP.Statement) : Problem where +def Problem.ofStatement + (name : String) + (statement : _root_.TPTP.Statement) + : Problem + where name := name source := _root_.TPTP.Statement.render statement diff --git a/OATP/Term.lean b/OATP/Term.lean index 00914ed..d2586d9 100644 --- a/OATP/Term.lean +++ b/OATP/Term.lean @@ -16,7 +16,9 @@ namespace OATP.Term open OATP TermColor -def eventText : SearchEvent → Text +def eventText + : SearchEvent → + Text | .goal snapshot => let context := if snapshot.context.isEmpty then "" else "\n" ++ String.intercalate "\n" (snapshot.context.toList.map (fun line => " " ++ line)) @@ -28,10 +30,14 @@ def eventText : SearchEvent → Text | .result outcome => Text.styled "result: " Style.bold ++ Text.plain outcome.status | .note message => Text.styled "note: " Style.dim ++ Text.plain message -def renderPlain (events : Array SearchEvent) : String := +def renderPlain + (events : Array SearchEvent) + : String := String.intercalate "\n" (events.toList.map (fun event => (eventText event).plainText)) -def renderAnsi16 (events : Array SearchEvent) : String := +def renderAnsi16 + (events : Array SearchEvent) + : String := String.intercalate "\n" (events.toList.map (fun event => Text.render RenderTarget.ansi16 (eventText event))) diff --git a/OATP/Translate.lean b/OATP/Translate.lean index 4e05af0..b3a8f46 100644 --- a/OATP/Translate.lean +++ b/OATP/Translate.lean @@ -28,10 +28,16 @@ structure GoalTranslation where target : String deriving Repr -private def hexDigit (value : Nat) : Char := +private +def hexDigit + (value : Nat) + : Char := if value < 10 then Char.ofNat (48 + value) else Char.ofNat (97 + (value - 10)) -private def symbolName (raw : String) : String := +private +def symbolName + (raw : String) + : String := let body := raw.toUTF8.toList.map fun byte => let value := byte.toNat s!"{hexDigit (value / 16)}{hexDigit (value % 16)}" @@ -90,10 +96,15 @@ private def renderStatement (name : String) (role : _root_.TPTP.Role) let statement ← OATP.TPTP.Statement.ofFof name role formula pure <| _root_.TPTP.Statement.render statement -private def renderFormula (formula : TPTP.Formula.Expr) : Except String String := +private +def renderFormula + (formula : TPTP.Formula.Expr) + : Except String String := formula.toTPTP -def translateGoal (mvarId : MVarId) : MetaM (Except String GoalTranslation) := +def translateGoal + (mvarId : MVarId) + : MetaM (Except String GoalTranslation) := mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) unless ← isProp target do diff --git a/examples/Cli.lean b/examples/Cli.lean index acd953a..3e6ba1d 100644 --- a/examples/Cli.lean +++ b/examples/Cli.lean @@ -63,7 +63,9 @@ inductive ConfigAction where | show | path -private def configActionParam : Param ConfigAction := +private +def configActionParam + : Param ConfigAction := Param.named "ACTION" (Param.enum [("show", .show), ("path", .path)]) inductive Action where @@ -75,7 +77,9 @@ inductive Action where | repl | doctor -def cli (identity : CliIdentity) : Argus.Command Action := +def cli + (identity : CliIdentity) + : Argus.Command Action := Argus.group identity.name [ Argus.cmd "run" (Spec.map Action.run RunOptions.spec) (description := "Run a local or explicitly selected online portfolio") @@ -131,8 +135,11 @@ private def doctorOnlineProblem : Problem := { source := "fof(oatp_doctor, conjecture, (p => p)).\n" } -private def doctorOnlineAttempts (endpoint : String) - (systems : Array SystemOnTPTP.Catalogue.SystemInfo) : Array Portfolio.Attempt := +private +def doctorOnlineAttempts + (endpoint : String) + (systems : Array SystemOnTPTP.Catalogue.SystemInfo) + : Array Portfolio.Attempt := let timeout := OATP.Runtime.doctorTimeoutSeconds let outputLimit := OATP.Runtime.doctorMaxOutputBytes systems.map fun system => { @@ -160,14 +167,20 @@ structure DoctorIssue where kind : DoctorIssueKind detail : String -private def doctorIssueKindLabel : DoctorIssueKind → String +private +def doctorIssueKindLabel + : DoctorIssueKind → + String | .noSZSStatus => "no SZS status" | .transportTimeout => "transport timeout" | .transportFailure => "transport failure" | .httpError => "HTTP error" | .requestFailure => "request failed" -private def doctorIssueKind : Portfolio.Failure → DoctorIssueKind +private +def doctorIssueKind + : Portfolio.Failure → + DoctorIssueKind | .process _ => .requestFailure | .http (.transport message) => if message.contains "timed out" then .transportTimeout else .transportFailure @@ -177,7 +190,10 @@ private def doctorIssueKind : Portfolio.Failure → DoctorIssueKind | .response (.unsupportedStatus _) _ => .requestFailure | .response (.malformedBody _) _ => .requestFailure -private def doctorIssue : Portfolio.Result → Option DoctorIssue +private +def doctorIssue + : Portfolio.Result → + Option DoctorIssue | .artifact _ _ => none | .failed attempt failure => match failure with @@ -187,11 +203,17 @@ private def doctorIssue : Portfolio.Result → Option DoctorIssue failure.message ++ "\n\n" ++ failure.output some { prover := attempt.name, kind := doctorIssueKind failure, detail } -private def portfolioName : Portfolio.Result → String +private +def portfolioName + : Portfolio.Result → + String | .artifact attempt _ => attempt.name | .failed attempt _ => attempt.name -private def doctorIssueSummary (issues : List DoctorIssue) : String := +private +def doctorIssueSummary + (issues : List DoctorIssue) + : String := let kinds : List DoctorIssueKind := [.noSZSStatus, .transportTimeout, .transportFailure, .httpError, .requestFailure] String.intercalate " · " <| kinds.filterMap fun kind => @@ -218,10 +240,16 @@ private def printDiagnostic (message : String) : IO UInt32 := do stderr.putStr "\n" pure 1 -private def configProverName (value : String) : String := +private +def configProverName + (value : String) + : String := OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value -private def configSelectedProvers (preferences : OATP.Config.Preferences) : String := +private +def configSelectedProvers + (preferences : OATP.Config.Preferences) + : String := if !preferences.proverSelectionSet then "automatic" else if preferences.enabledProvers.isEmpty then @@ -296,7 +324,11 @@ private def showArtifact (artifact : Artifact) : IO UInt32 := do unless artifact.stderr.isEmpty do IO.eprint artifact.stderr pure <| if SZSStatus.isSuccess artifact.status then 0 else 1 -private def processErrorMessage (toolName executable : String) : OATP.Process.Error → String +private +def processErrorMessage + (toolName executable : String) + : OATP.Process.Error → + String | .io message => s!"could not start local prover `{executable}`: {message}; " ++ s!"check the path or run `{toolName} doctor`" @@ -325,13 +357,19 @@ private def noLocalProverMessage : IO String := do pure <| s!"no local ATP found; tried {String.intercalate ", " candidates.toList}. " ++ "Install one, pass --prover PATH, or explicitly select an online-* prover" -private def responseErrorMessage : SystemOnTPTP.ResponseError → String +private +def responseErrorMessage + : SystemOnTPTP.ResponseError → + String | .httpStatus status => s!"SystemOnTPTP returned HTTP {status}" | .missingStatus => "SystemOnTPTP response did not contain an SZS status" | .unsupportedStatus status => s!"SystemOnTPTP returned unsupported SZS status `{status}`" | .malformedBody message => s!"SystemOnTPTP response was not valid HTML: {message}" -private def showPortfolioResult : Portfolio.Result → IO Bool +private +def showPortfolioResult + : Portfolio.Result → + IO Bool | .artifact _ artifact => do let marker := if SZSStatus.isSuccess artifact.status then "✓" else "!" IO.eprintln s!"{marker} {artifact.prover.label}: {artifact.status} ({artifact.elapsedMs}ms)" @@ -347,8 +385,12 @@ private def showPortfolioResult : Portfolio.Result → IO Bool unless failure.output.isEmpty do IO.eprint failure.output pure false -private def portfolioView (total : Nat) (progress : Widgets.IndeterminateProgressState) - (results : List Portfolio.Result) : Text := +private +def portfolioView + (total : Nat) + (progress : Widgets.IndeterminateProgressState) + (results : List Portfolio.Result) + : Text := let latest := match results.getLast? with | some result => s!" · latest {portfolioName result}" | none => "" diff --git a/examples/Repl.lean b/examples/Repl.lean index 0809c4a..3a91173 100644 --- a/examples/Repl.lean +++ b/examples/Repl.lean @@ -30,8 +30,14 @@ open TermColor.Widgets private def catalogueNamespace : String := "oatp-repl" -private def appendEntry (app : App) (cell : Nat) (input output : String) (ok : Bool) - (elapsedMs : Option Nat := none) (sources : Sources := #[]) +private +def appendEntry + (app : App) + (cell : Nat) + (input output : String) + (ok : Bool) + (elapsedMs : Option Nat := none) + (sources : Sources := #[]) (diagnostic : Option Diagnostic := none) (report : Option Report := none) : App := { app with entries := { cell, input, output, ok, elapsedMs, sources, diagnostic, report } :: app.entries @@ -41,7 +47,10 @@ private def appendEntry (app : App) (cell : Nat) (input output : String) (ok : B #guard (appendEntry { repl := { history := #["first"] } } 1 "input" "output" true).repl.history == #["first"] -private def diagnosticFor (source message : String) : Source × Diagnostic := +private +def diagnosticFor + (source message : String) + : Source × Diagnostic := let sourceText := source let source := Source.fromBytes "input" source.toUTF8 let title := message.splitOn "\n" |>.headD message @@ -49,8 +58,14 @@ private def diagnosticFor (source message : String) : Source × Diagnostic := (Label.primary (Span.range 0 0 sourceText.toUTF8.size)) (source, diagnostic) -private def note (app : App) (cell : Nat) (input output : String) (ok : Bool) - (elapsedMs : Option Nat := none) : App := +private +def note + (app : App) + (cell : Nat) + (input output : String) + (ok : Bool) + (elapsedMs : Option Nat := none) + : App := let (sources, diagnostic) := if ok then (#[], none) else @@ -59,8 +74,15 @@ private def note (app : App) (cell : Nat) (input output : String) (ok : Bool) appendEntry { app with session := OATP.Repl.note app.session input output } cell input output ok elapsedMs sources diagnostic -private def notePlain (app : App) (cell : Nat) (input output : String) (ok : Bool) - (elapsedMs : Option Nat := none) (report : Option Report := none) : App := +private +def notePlain + (app : App) + (cell : Nat) + (input output : String) + (ok : Bool) + (elapsedMs : Option Nat := none) + (report : Option Report := none) + : App := appendEntry { app with session := OATP.Repl.note app.session input output } cell input output ok elapsedMs #[] none report @@ -68,23 +90,37 @@ private def notePlain (app : App) (cell : Nat) (input output : String) (ok : Boo | entry :: _ => match entry.diagnostic with | none => true | some _ => false | [] => false -private def noteDiagnostic (app : App) (cell : Nat) (input source message : String) : App := +private +def noteDiagnostic + (app : App) + (cell : Nat) + (input source message : String) + : App := let (source, diagnostic) := diagnosticFor source message appendEntry { app with session := OATP.Repl.note app.session input message } cell input message false none #[source] (some diagnostic) -private def clearDerived (app : App) : App := +private +def clearDerived + (app : App) + : App := { app with goal := none, translation := none, term := none, leanGoal := none } -private def invalidateContext (app : App) : App := +private +def invalidateContext + (app : App) + : App := { clearDerived app with runRows := #[] runOpen := false runFocus := 0 contextItemFocus := none } -private def clearTranscript (app : App) : App := +private +def clearTranscript + (app : App) + : App := { app with entries := [] transcriptScroll := 0 @@ -94,17 +130,26 @@ private def clearTranscript (app : App) : App := copyPending := none repl := { app.repl with input := {}, historyIndex := none, completion := none } } -private def changesContext (input : String) : Bool := +private +def changesContext + (input : String) + : Bool := match OATP.Repl.parseInput input with | .source _ => true | .command command => match command with | .parse _ | .axiom _ _ | .conjecture _ _ | .remove _ | .update _ _ | .reset => true | _ => false -private def lastHistory (session : OATP.Repl.Session) : String := +private +def lastHistory + (session : OATP.Repl.Session) + : String := session.history.toList.reverse.head?.map (·.result) |>.getD "ok" -private def artifactText : Portfolio.Result → (String × Bool) +private +def artifactText + : Portfolio.Result → + (String × Bool) | .artifact attempt artifact => let head := s!"{attempt.name}: {artifact.status} ({artifact.elapsedMs}ms)" let details := if artifact.stderr.contains "no input problem files" then @@ -118,19 +163,32 @@ private def artifactText : Portfolio.Result → (String × Bool) (head ++ details, SZSStatus.isSuccess artifact.status) | .failed attempt failure => (s!"{attempt.name}: failed: {failure.message}", false) -private def resultHasIssue : Portfolio.Result → Bool +private +def resultHasIssue + : Portfolio.Result → + Bool | .artifact _ artifact => !SZSStatus.isSuccess artifact.status | .failed _ _ => true -private def resultSucceeded : Portfolio.Result → Bool +private +def resultSucceeded + : Portfolio.Result → + Bool | .artifact _ artifact => SZSStatus.isSuccess artifact.status | .failed _ _ => false -private def resultIssueText : Portfolio.Result → String +private +def resultIssueText + : Portfolio.Result → + String | .artifact attempt artifact => s!"{attempt.name}: returned {artifact.status}" | .failed attempt failure => s!"{attempt.name}: {failure.message}" -private def runReport (strategy : OATP.RunStrategy) (results : List Portfolio.Result) : Report := +private +def runReport + (strategy : OATP.RunStrategy) + (results : List Portfolio.Result) + : Report := let issues := results.filter resultHasIssue let report := if strategy == .firstSuccess && results.any resultSucceeded then Report.info "first successful prover completed" @@ -149,10 +207,16 @@ structure RunOutput where ok : Bool report : Report -private def failedRunOutput (code message : String) : RunOutput := +private +def failedRunOutput + (code message : String) + : RunOutput := { text := message, ok := false, report := (Report.error message).withCode code } -private def runRow : Portfolio.Result → RunRow +private +def runRow + : Portfolio.Result → + RunRow | .artifact attempt artifact => { name := attempt.name status := .result artifact.status @@ -165,14 +229,21 @@ private def runRow : Portfolio.Result → RunRow | .failed attempt failure => { name := attempt.name, status := .failed, detail := failure.message } -private def runRowsFor (attempts : Array Portfolio.Attempt) (strategy : OATP.RunStrategy) : - Array RunRow := +private +def runRowsFor + (attempts : Array Portfolio.Attempt) + (strategy : OATP.RunStrategy) + : Array RunRow := attempts.mapIdx fun index attempt => { name := attempt.name status := if strategy == .all || index == 0 then .running else .queued } -private def finishRunRows (rows : Array RunRow) (results : List Portfolio.Result) - (strategy : OATP.RunStrategy) : Array RunRow := +private +def finishRunRows + (rows : Array RunRow) + (results : List Portfolio.Result) + (strategy : OATP.RunStrategy) + : Array RunRow := let rows := results.foldl (fun rows result => let completed := runRow result rows.map fun current => if current.name == completed.name then completed else current) rows @@ -191,11 +262,17 @@ private def currentRunRows (app : App) : IO (Array RunRow) := do | some progress => progress.get | none => pure app.runRows -private def currentProblem (app : App) : Option Problem := +private +def currentProblem + (app : App) + : Option Problem := app.translation.map (fun source => { name := "lean-goal", source }) |>.orElse (fun _ => OATP.Repl.problem app.session) -private def theoryStatus (theory : String) : String := +private +def theoryStatus + (theory : String) + : String := s!"theory: {theory}; available: {String.intercalate ", " OATP.TPTP.supportedTheories}" #guard theoryStatus "fof" == "theory: fof; available: fof, cnf, tff" @@ -209,7 +286,10 @@ private def preferences (app : App) : OATP.Config.Preferences := { theme := app.themeName } -private def configProverName (value : String) : String := +private +def configProverName + (value : String) + : String := OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value private def configOutput (app : App) : IO (String × Report) := do @@ -311,8 +391,12 @@ private def selectedProvers (app : App) (all includeDefault : Bool := false) : pure <| defaults.foldl (fun selected reference => if selected.any (· == reference) then selected else selected.push reference) selected -private def runRequest (app : App) (request : OATP.Repl.RunRequest) - (includeDefault : Bool := false) : IO RunOutput := do +private +def runRequest + (app : App) + (request : OATP.Repl.RunRequest) + (includeDefault : Bool := false) + : IO RunOutput := do match currentProblem app with | none => let message := @@ -420,15 +504,20 @@ private def runRequest (app : App) (request : OATP.Repl.RunRequest) pure <| RunOutput.mk (String.intercalate "\n" (rendered.map Prod.fst)) (rendered.any Prod.snd) (runReport app.strategy results.toList) -private def backendLine (input : String) : Bool := +private +def backendLine + (input : String) + : Bool := match OATP.Repl.parseCommandSpec input with | .ok command => match command with | .run _ | .local _ | .online _ | .check => true | _ => false | .error _ => false -private def backendRequest (input : String) : - Except String (OATP.Repl.RunRequest × Bool) := +private +def backendRequest + (input : String) + : Except String (OATP.Repl.RunRequest × Bool) := match OATP.Repl.parseCommandSpec input with | .ok (.run request) => pure (request, false) | .ok (.local request) => pure ({ @@ -445,7 +534,10 @@ private def backendRequest (input : String) : | .ok _ => .error "not a prover command" | .error message => .error message -private def startingRunRows (input : String) : Array RunRow := +private +def startingRunRows + (input : String) + : Array RunRow := match backendRequest input with | .ok (request, includeDefault) => if request.references.isEmpty then #[{ name := if includeDefault then @@ -454,7 +546,10 @@ private def startingRunRows (input : String) : Array RunRow := { name := OATP.ProverReference.display reference, status := .running } | .error _ => #[{ name := "run", status := .running }] -private def backgroundJobs : TermColor.Repl.Terminal.JobConfig App where +private +def backgroundJobs + : TermColor.Repl.Terminal.JobConfig App + where shouldRun := fun app input => !app.busy && backendLine input start := fun app input => { app with busy := true @@ -558,12 +653,20 @@ private def doctorText : IO String := do "Use /systems --online to inspect the remote catalogue." ] -private def fuzzy (query : String) (value : String) : Bool := +private +def fuzzy + (query : String) + (value : String) + : Bool := let query := query.toLower let value := value.toLower value == query || value.startsWith query || value.contains query -private def proverMatches (query : String) (reference : OATP.ProverReference) : Bool := +private +def proverMatches + (query : String) + (reference : OATP.ProverReference) + : Bool := fuzzy query (OATP.ProverReference.display reference) || fuzzy query reference.name private def infoText (app : App) (query : String) : IO (String × Bool) := do @@ -615,7 +718,11 @@ private def infoText (app : App) (query : String) : IO (String × Bool) := do String.intercalate ", " (online.toList.map (fun system => SystemOnTPTP.onlineReference system.id))}", false) -private partial def parseStepTokens : List String → Except String (OATP.Proof.Step × List String) +private +partial +def parseStepTokens + : List String → + Except String (OATP.Proof.Step × List String) | "true-intro" :: rest => pure (.trueIntro, rest) | "exact" :: [] => .error "exact expects a hypothesis name" | "exact" :: name :: rest => pure (.exact (Name.mkSimple name), rest) @@ -924,10 +1031,17 @@ private def commandValues (typeName : String) : IO (List String) := do pure (localNames.toList ++ online.toList) | _ => pure [] -private def complete (_app : App) (input : TextInputState) : IO (List Completion) := +private +def complete + (_app : App) + (input : TextInputState) + : IO (List Completion) := completeCommandWith OATP.Repl.commandSpec commandValues input -private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where +private +def appKeymap + : TermColor.Repl.Terminal.AppKeymap App + where Action := AppKeyAction keymap := Keymap.fromSpecs appBindings contexts := fun app => @@ -997,7 +1111,12 @@ private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where #guard (Keymap.fromSpecs appBindings).resolve [AppContext.keyContext .state] (.char 'e') == some AppKeyAction.prepareUpdateContext -private def handleMouse (app : App) (size : Size) (mouse : MouseEvent) : Option App := +private +def handleMouse + (app : App) + (size : Size) + (mouse : MouseEvent) + : Option App := if app.runOpen then match drawerWidths size.columns with | none => none @@ -1179,14 +1298,19 @@ private def staticOutput (app : App) : IO Unit := do s!" ({formatElapsed milliseconds})") |>.getD "" IO.println s!" {(if entry.ok then "=" else "!")} {entry.output}{timing}" -private def usage : String := +private +def usage + : String := "oatp repl — interactive theorem-proving workbench\n\n" ++ "usage:\n lake exe oatp repl\n lake exe oatp repl --script FILE\n\n" ++ "examples:\n /load problem.p\n /to-lean p => p\n /snapshot\n " ++ "/to-tptp\n " ++ "/reconstruct implication-intro h exact h\n /term" -private def scriptExitCode (app : App) : UInt32 := +private +def scriptExitCode + (app : App) + : UInt32 := if app.entries.all (·.ok) then 0 else 1 private def initialApp (runtime : OATP.Lean.Repl.Runtime) : IO App := do diff --git a/test/Tests.lean b/test/Tests.lean index 302755d..e287466 100644 --- a/test/Tests.lean +++ b/test/Tests.lean @@ -254,13 +254,16 @@ open OATP OATP.TPTP { columns := 100, rows := 24 }).plainText.contains "state •" #guard (OATP.ReplView.screen { stateOpen := true, panelFocus := .drawer } { columns := 100, rows := 24 }).plainText.contains "state • active" -def completionApp : OATP.ReplView.App := +def completionApp + : OATP.ReplView.App := { repl := { input := { value := "/st", cursor := 3 } completion := some { candidates := #[{ replacement := "/state" }] } } } #guard (OATP.ReplView.screen completionApp { columns := 100, rows := 24 }).plainText.contains "/state" #guard OATP.ReplView.formatElapsed 1_500 == "1.5 s" -private def timedEntry : OATP.ReplView.TranscriptEntry := +private +def timedEntry + : OATP.ReplView.TranscriptEntry := { cell := 1 input := "/to-lean p => p" output := "goal created" @@ -268,7 +271,9 @@ private def timedEntry : OATP.ReplView.TranscriptEntry := #guard (OATP.ReplView.screen { entries := [timedEntry] } { columns := 100, rows := 24 }).plainText.contains "(12 ms)" -private def plainEntry : OATP.ReplView.TranscriptEntry := +private +def plainEntry + : OATP.ReplView.TranscriptEntry := { cell := 1 input := "/to-lean p => p" output := "goal created" } From 98c6c45d85c32b4bc403a7da09d0dc75a76cf556 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 18 Sep 2026 15:25:26 -0500 Subject: [PATCH 2/4] style: stop splitting headers nothing forces apart Recompute the signature-layout pass with the fixed converter: binder defaults in brackets no longer truncate the header, `do` bodies are no longer misread as one-liners, anonymous `instance : T where` now converts, and single-operand headers with no binders stay on one line instead of splitting for nothing. The `do`-body fix reaches roughly a hundred declarations across the REPL and SystemOnTPTP modules that the buggy pass had skipped outright. Properties/Basic.lean and test/Tests.lean revert to base: their only touched declarations were pure churn under the last bug. --- OATP/Artifacts.lean | 10 ++- OATP/Config.lean | 4 +- OATP/Http.lean | 46 +++++++++--- OATP/Lean.lean | 5 +- OATP/Lean/Repl.lean | 47 ++++++++---- OATP/Portfolio.lean | 23 ++++-- OATP/Process.lean | 26 +++++-- OATP/Proof.lean | 16 ++-- OATP/Properties/Basic.lean | 7 +- OATP/Repl.lean | 47 ++++-------- OATP/Repl/Context.lean | 18 ++++- OATP/ReplView.lean | 32 ++++---- OATP/Runtime.lean | 28 ++++--- OATP/SystemOnTPTP.lean | 29 ++++--- OATP/TPTP.lean | 7 +- OATP/Translate.lean | 20 +++-- examples/Cli.lean | 132 +++++++++++++++++++++++++------- examples/Repl.lean | 150 +++++++++++++++++++++++++++---------- test/Tests.lean | 11 +-- 19 files changed, 446 insertions(+), 212 deletions(-) diff --git a/OATP/Artifacts.lean b/OATP/Artifacts.lean index 42d87d1..e837f07 100644 --- a/OATP/Artifacts.lean +++ b/OATP/Artifacts.lean @@ -34,7 +34,10 @@ private def roots : IO (List System.FilePath) := do 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; @@ -51,7 +54,10 @@ 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 () diff --git a/OATP/Config.lean b/OATP/Config.lean index 087c02c..7030162 100644 --- a/OATP/Config.lean +++ b/OATP/Config.lean @@ -99,7 +99,9 @@ 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 => diff --git a/OATP/Http.lean b/OATP/Http.lean index 71cee59..8fb3914 100644 --- a/OATP/Http.lean +++ b/OATP/Http.lean @@ -26,9 +26,7 @@ structure Field where value : String deriving BEq, DecidableEq, Repr -private -def hexDigits - : Array Char := +private def hexDigits : Array Char := #[ '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'A', 'B', 'C', 'D', 'E', 'F' @@ -78,7 +76,10 @@ def validHeaderValue value.toList.all fun character => character != '"' && character != '\\' && character != '\r' && character != '\n' -def encodeMultipart (boundary : String) (parts : Array MultipartPart) : Except String String := do +def encodeMultipart + (boundary : String) + (parts : Array MultipartPart) + : Except String String := do if boundary.isEmpty || !boundary.toList.all (fun character => character.isAlphanum || character == '-' || character == '_') then throw "multipart boundary must contain only letters, digits, '-' or '_'" @@ -132,7 +133,9 @@ structure Response where stderr : String := "" deriving Repr -def commandVersion (command : String) : IO (Option String) := do +def commandVersion + (command : String) + : IO (Option String) := do try let output ← IO.Process.output { cmd := command, args := #["--version"] } if output.exitCode != 0 then @@ -189,7 +192,10 @@ def statusFromOutput | none => none | _ => none -private def requestWithCurlUnsafe (request : Request) : IO (Except Error Response) := do +private +def requestWithCurlUnsafe + (request : Request) + : IO (Except Error Response) := do let base : Array String := #[ "--silent", "--show-error", "--max-time", toString request.maxSeconds, @@ -240,7 +246,10 @@ def statusFromWgetOutput else find lines find (output.splitOn "\n") -private def requestWithWgetUnsafe (request : Request) : IO (Except Error Response) := do +private +def requestWithWgetUnsafe + (request : Request) + : IO (Except Error Response) := do let base : Array String := #[ "--quiet", "--server-response", "--max-redirect=0", "--tries=1", "--timeout=" ++ toString request.maxSeconds, @@ -266,7 +275,10 @@ private def requestWithWgetUnsafe (request : Request) : IO (Except Error Respons else return Except.ok { statusCode, body := output.stdout } -private def validateRequest (request : Request) : Except Error Unit := do +private +def validateRequest + (request : Request) + : Except Error Unit := do if request.url.isEmpty then throw (.invalidRequest "HTTP request URL must not be empty") if request.maxSeconds == 0 then @@ -277,7 +289,10 @@ private def validateRequest (request : Request) : Except Error Unit := do if actual > request.maxRequestBodyBytes then throw (.requestBodyTooLarge actual request.maxRequestBodyBytes) -private def requestWithTransportUnsafe (request : Request) : IO (Except Error Response) := do +private +def requestWithTransportUnsafe + (request : Request) + : IO (Except Error Response) := do match validateRequest request with | .error error => return .error error | .ok _ => pure () @@ -289,13 +304,18 @@ private def requestWithTransportUnsafe (request : Request) : IO (Except Error Re else pure <| Except.error (.transport "OATP requires curl or wget for HTTPS transport") -def requestWithTransport (request : Request) : IO (Except Error Response) := do +def requestWithTransport + (request : Request) + : IO (Except Error Response) := do try requestWithTransportUnsafe request catch error => pure (.error (.io s!"{error}")) -def requestWith (transport : Transport) (request : Request) : IO (Except Error Response) := do +def requestWith + (transport : Transport) + (request : Request) + : IO (Except Error Response) := do try match validateRequest request with | .error error => pure (.error error) @@ -306,7 +326,9 @@ def requestWith (transport : Transport) (request : Request) : IO (Except Error R catch error => pure (.error (.io s!"{error}")) -def requestWithCurl (request : Request) : IO (Except Error Response) := do +def requestWithCurl + (request : Request) + : IO (Except Error Response) := do requestWith .curl request end OATP.Http diff --git a/OATP/Lean.lean b/OATP/Lean.lean index 0ca2b4d..c21d2d2 100644 --- a/OATP/Lean.lean +++ b/OATP/Lean.lean @@ -24,7 +24,10 @@ structure CheckedProof where proof : Expr target : Expr -private def prettyExpr (expression : Expr) : MetaM String := do +private +def prettyExpr + (expression : Expr) + : MetaM String := do let formatted ← ppExpr expression pure s!"{formatted}" diff --git a/OATP/Lean/Repl.lean b/OATP/Lean/Repl.lean index 58cc4d0..7596e92 100644 --- a/OATP/Lean/Repl.lean +++ b/OATP/Lean/Repl.lean @@ -56,8 +56,12 @@ def create : IO Runtime := do metaState := {} } -private def runMeta {α : Type} (runtime : Runtime) (action : MetaM α) : - IO (α × Runtime) := do +private +def runMeta + {α : Type} + (runtime : Runtime) + (action : MetaM α) + : IO (α × Runtime) := do let (value, coreState, metaState) ← action.toIO runtime.coreContext runtime.coreState {} runtime.metaState pure (value, { runtime with coreState, metaState }) @@ -112,8 +116,12 @@ def lookupAtom : Option Expr := atoms.find? (·.1 == name) |>.map Prod.snd -private partial def toLean (atoms : Array (String × Expr)) - (formula : _root_.TPTP.Formula.Expr) : TranslationM Expr := do +private +partial +def toLean + (atoms : Array (String × Expr)) + (formula : _root_.TPTP.Formula.Expr) + : TranslationM Expr := do match formula with | .atom predicate arguments => if !arguments.isEmpty then @@ -143,33 +151,46 @@ where let right ← toLean atoms right ExceptT.lift <| mkAppM name #[left, right] -private def makeGoal (source : String) (formula : _root_.TPTP.Formula.Expr) : - MetaM (Except String Goal) := do +private +def makeGoal + (source : String) + (formula : _root_.TPTP.Formula.Expr) + : MetaM (Except String Goal) := do let atoms := atomNames formula #[] withAtoms atoms.toList fun locals => do let target ← toLean locals formula let goal ← ExceptT.lift <| mkFreshExprMVar (some target) pure { mvarId := goal.mvarId!, source, atoms } -def goalFromFormula (runtime : Runtime) (source : String) : - IO (Except String (Runtime × Goal)) := do +def goalFromFormula + (runtime : Runtime) + (source : String) + : IO (Except String (Runtime × Goal)) := do match OATP.TPTP.Syntax.parseFormula source with | .error error => pure (.error (error.pretty source.toUTF8)) | .ok formula => let (result, runtime) ← runMeta runtime (makeGoal source formula) pure <| result.map fun goal => (runtime, goal) -def snapshot (runtime : Runtime) (goal : Goal) : IO (Runtime × OATP.GoalSnapshot) := do +def snapshot + (runtime : Runtime) + (goal : Goal) + : IO (Runtime × OATP.GoalSnapshot) := do let (value, runtime) ← runMeta runtime (OATP.Lean.snapshot goal.mvarId) pure (runtime, value) -def translateToTPTP (runtime : Runtime) (goal : Goal) : - IO (Runtime × Except String OATP.Lean.GoalTranslation) := do +def translateToTPTP + (runtime : Runtime) + (goal : Goal) + : IO (Runtime × Except String OATP.Lean.GoalTranslation) := do let (value, runtime) ← runMeta runtime (OATP.Lean.translateGoal goal.mvarId) pure (runtime, value) -def reconstruct (runtime : Runtime) (goal : Goal) (step : OATP.Proof.Step) : - IO (Runtime × Except String RenderedTerm) := do +def reconstruct + (runtime : Runtime) + (goal : Goal) + (step : OATP.Proof.Step) + : IO (Runtime × Except String RenderedTerm) := do let action : MetaM (Except String RenderedTerm) := do match ← OATP.Proof.reconstruct goal.mvarId step with | .error message => pure (.error message) diff --git a/OATP/Portfolio.lean b/OATP/Portfolio.lean index 876268e..4eb0f40 100644 --- a/OATP/Portfolio.lean +++ b/OATP/Portfolio.lean @@ -74,7 +74,10 @@ def Failure.output | .process _ | .http _ => "" | .response _ output => output -def execute (problem : Problem) (attempt : Attempt) : IO Result := do +def execute + (problem : Problem) + (attempt : Attempt) + : IO Result := do match attempt.backend with | .local command => match ← Process.run { name := attempt.name } problem attempt.limits command with @@ -97,8 +100,13 @@ def execute (problem : Problem) (attempt : Attempt) : IO Result := do pure (.failed attempt (.response error output)) -- partiality: task completion is external and waitAny' controls progress through the pending set. -private partial def collect (pending : List (Task (Except IO.Error Result))) - (results : Array Result) (onResult : Result → IO Unit) : IO (Array Result) := do +private +partial +def collect + (pending : List (Task (Except IO.Error Result))) + (results : Array Result) + (onResult : Result → IO Unit) + : IO (Array Result) := do match pending with | [] => pure results | task :: rest => @@ -129,8 +137,13 @@ def successful | .artifact _ artifact => SZSStatus.isSuccess artifact.status | .failed _ _ => false -private def runUntilSuccess (problem : Problem) (attempts : List Attempt) - (results : Array Result) (onResult : Result → IO Unit) : IO (Array Result) := do +private +def runUntilSuccess + (problem : Problem) + (attempts : List Attempt) + (results : Array Result) + (onResult : Result → IO Unit) + : IO (Array Result) := do match attempts with | [] => pure results | attempt :: rest => diff --git a/OATP/Process.lean b/OATP/Process.lean index bd9f65b..9965799 100644 --- a/OATP/Process.lean +++ b/OATP/Process.lean @@ -39,8 +39,13 @@ inductive Error where -- partiality: process completion and the monotonic clock are external; the deadline bounds -- polling behavior, not kernel recursion. -private partial def waitForExit {cfg : IO.Process.StdioConfig} - (child : IO.Process.Child cfg) (deadline : Nat) : IO (Bool × UInt32) := do +private +partial +def waitForExit + {cfg : IO.Process.StdioConfig} + (child : IO.Process.Child cfg) + (deadline : Nat) + : IO (Bool × UInt32) := do match ← child.tryWait with | some exitCode => pure (false, exitCode) | none => @@ -54,8 +59,13 @@ private partial def waitForExit {cfg : IO.Process.StdioConfig} IO.sleep (min 10 remaining).toUInt32 waitForExit child deadline -private def runUnsafe (prover : Prover) (problem : Problem) (limits : Limits) (command : Command) : - IO (Except Error Artifact) := do +private +def runUnsafe + (prover : Prover) + (problem : Problem) + (limits : Limits) + (command : Command) + : IO (Except Error Artifact) := do let command := command.withStdinProblem let artifacts ← OATP.Artifacts.start s!"local {command.executable}" problem for run in artifacts do @@ -121,8 +131,12 @@ private def runUnsafe (prover : Prover) (problem : Problem) (limits : Limits) (c OATP.Artifacts.write run "result.txt" s!"{status}\n" return .ok artifact -def run (prover : Prover) (problem : Problem) (limits : Limits) (command : Command) : - IO (Except Error Artifact) := do +def run + (prover : Prover) + (problem : Problem) + (limits : Limits) + (command : Command) + : IO (Except Error Artifact) := do try runUnsafe prover problem limits command catch error => diff --git a/OATP/Proof.lean b/OATP/Proof.lean index 87adaa8..cdf99e9 100644 --- a/OATP/Proof.lean +++ b/OATP/Proof.lean @@ -29,17 +29,23 @@ inductive Step where | implicationIntro (localName : Name) (body : Step) deriving Repr -def stepNames - : List String := +def stepNames : List String := ["true-intro", "exact", "and-left", "and-right", "and-intro", "implication-intro"] -private def andParts (target : Expr) : MetaM (Option (Expr × Expr)) := do +private +def andParts + (target : Expr) + : MetaM (Option (Expr × Expr)) := do match ← whnf target with | .app (.app (.const ``And _) left) right => pure (some (left, right)) | _ => pure none -private def projection (target : Expr) (localName : Name) (useLeft : Bool) : - MetaM (Except String Expr) := do +private +def projection + (target : Expr) + (localName : Name) + (useLeft : Bool) + : MetaM (Except String Expr) := do let hypothesis ← getFVarFromUserName localName match ← andParts (← inferType hypothesis) with | none => pure (.error s!"local hypothesis `{localName}` is not a conjunction") diff --git a/OATP/Properties/Basic.lean b/OATP/Properties/Basic.lean index 1e1f179..3479d9b 100644 --- a/OATP/Properties/Basic.lean +++ b/OATP/Properties/Basic.lean @@ -13,12 +13,11 @@ namespace OATP.Properties open OATP OATP.TPTP -theorem empty_plain_render - : OATP.Term.renderPlain #[] = "" := by +theorem empty_plain_render : OATP.Term.renderPlain #[] = "" := by rfl -theorem note_plain_render - : OATP.Term.renderPlain #[.note "ready"] = "note: ready" := by +theorem note_plain_render : + OATP.Term.renderPlain #[.note "ready"] = "note: ready" := by rfl theorem goal_context_plain_render : diff --git a/OATP/Repl.lean b/OATP/Repl.lean index 7245964..f24061d 100644 --- a/OATP/Repl.lean +++ b/OATP/Repl.lean @@ -27,8 +27,7 @@ open OATP.TPTP open _root_.Argus open _root_.Grip -def helpTopics - : List String := +def helpTopics : List String := ["cnf", "fof", "tff", "lean", "run", "context", "grammar", "roles"] def grammarTopics : List String := OATP.TPTP.supportedTheories @@ -43,8 +42,7 @@ def completionParam : Param String := Param.named typeName (Param.enum (values.map fun value => (value, value))) -def contextIndexParam - : Param Nat := +def contextIndexParam : Param Nat := Param.ofParser "INDEX" (GParser.seqR (GParser.optional (GParser.ch '#')) GParser.nat) def staticCompletionValues @@ -291,8 +289,7 @@ def textSpec (Spec.arg name help (Param.named name Param.str)) (Spec.many (Spec.arg name help (Param.named name Param.str)))) -def commandSpec - : Argus.Command Command := +def commandSpec : Argus.Command Command := Argus.group "oatp" [ Argus.cmd "help" (Spec.map Command.help (Spec.opt (Spec.arg "TOPIC" "Help topic" (Param.named "TOPIC" Param.str)))) @@ -430,9 +427,7 @@ def parseCommandSpec | [] => "" .error (message ++ hint) -private -def commandChildren - : List (Argus.Command Command) := +private def commandChildren : List (Argus.Command Command) := match commandSpec.body with | .subs children => children | .opts _ => [] @@ -467,8 +462,7 @@ def usageLine output ++ if optional then " [" ++ value ++ "]" else " " ++ value) "" command.name ++ flags ++ arguments -def commandHelpText - : String := +def commandHelpText : String := String.intercalate "\n" <| ["OATP REPL commands"] ++ commandChildren.map fun command => " /" ++ usageLine command ++ " " ++ command.description @@ -488,13 +482,10 @@ def parseInput else .source source -def helpText - : String := +def helpText : String := commandHelpText -private -def cnfHelp - : String := +private def cnfHelp : String := String.intercalate "\n" [ "CNF — clause normal form", "statement: cnf(NAME, ROLE, CLAUSE).", @@ -514,9 +505,7 @@ def cnfHelp " /state formulas /roles cnf /run --prover eprover" ] -private -def fofHelp - : String := +private def fofHelp : String := String.intercalate "\n" [ "FOF — first-order formulas", "statement: fof(NAME, ROLE, FORMULA).", @@ -534,9 +523,7 @@ def fofHelp "use FOF when the problem needs implication, conjunction, or quantifiers" ] -private -def tffHelp - : String := +private def tffHelp : String := String.intercalate "\n" [ "TFF — typed first-order formulas", "type: tff(nat_type, type, nat: $tType).", @@ -549,9 +536,7 @@ def tffHelp "TFF is parsed as TPTP input; use /state to inspect collected symbols" ] -private -def grammarHelp - : String := +private def grammarHelp : String := String.intercalate "\n" [ "Grammar lookup", "/grammar cnf clause normal form", @@ -589,9 +574,7 @@ def roleHelp s!"Use /grammar {format} for the syntax." ] -private -def leanHelp - : String := +private def leanHelp : String := String.intercalate "\n" [ "Lean bridge", "1. /goal p => p create a Lean goal", @@ -604,9 +587,7 @@ def leanHelp "example result: fun h => h : _fvar.1 → _fvar.1" ] -private -def runHelp - : String := +private def runHelp : String := String.intercalate "\n" [ "Provers", "/run run the configured or first local prover", @@ -635,9 +616,7 @@ def runHelp " /local vampire -- --mode casc" ] -private -def contextHelp - : String := +private def contextHelp : String := String.intercalate "\n" [ "Context drawer", "/state [TARGET] open context or focus a box", diff --git a/OATP/Repl/Context.lean b/OATP/Repl/Context.lean index 639723a..f476cb9 100644 --- a/OATP/Repl/Context.lean +++ b/OATP/Repl/Context.lean @@ -215,7 +215,10 @@ def validateDocument | _root_.TPTP.Item.statement statement => validateStatement statement | _root_.TPTP.Item.include _ => pure ()) |>.map (fun _ => ()) -private def parseDocument (source : String) : Except String _root_.TPTP.Document := do +private +def parseDocument + (source : String) + : Except String _root_.TPTP.Document := do match OATP.TPTP.parse source with | .error error => .error (error.pretty source.toUTF8) | .ok document => @@ -258,15 +261,22 @@ def removeContext let removed := String.intercalate ", " (indices.map contextIndexText) .ok (record session input s!"removed {removed}") -private def singleStatement (source : String) : Except String _root_.TPTP.Statement := do +private +def singleStatement + (source : String) + : Except String _root_.TPTP.Statement := do let document ← parseDocument source match document.items.toList with | [.statement statement] => pure statement | [] => .error "update expects one TPTP statement" | _ => .error "update expects exactly one TPTP statement" -def updateContext (session : Session) (input : String) (index : Nat) (source : String) : - Except String Session := do +def updateContext + (session : Session) + (input : String) + (index : Nat) + (source : String) + : Except String Session := do let statement ← singleStatement source match session.context.find? (·.id == index) with | some item => diff --git a/OATP/ReplView.lean b/OATP/ReplView.lean index 1d3329b..92ea18c 100644 --- a/OATP/ReplView.lean +++ b/OATP/ReplView.lean @@ -35,9 +35,7 @@ open scoped TermColor.Style def version : String := OATP.version -def aurora - : ColorScheme - where +def aurora : ColorScheme where background := .rgb 13 24 37 foreground := .rgb 225 241 245 selection := .rgb 39 70 83 @@ -51,8 +49,7 @@ def aurora purple := .rgb 178 146 255 pink := .rgb 245 132 203 -def themes - : List (String × ColorScheme) := +def themes : List (String × ColorScheme) := [("aurora", aurora), ("terracotta", { background := .rgb 26 28 38 foreground := .rgb 214 216 226 @@ -169,8 +166,7 @@ def appBinding label := String.intercalate "/" (keys.map Keymap.keyLabel) description } -def appBindings - : List (BindingSpec AppKeyAction) := +def appBindings : List (BindingSpec AppKeyAction) := [ appBinding [.ctrl 'R', .ctrl 'r'] .toggleRun none "toggle the run drawer" , appBinding [.ctrl 'H', .ctrl 'h'] .toggleHistory none "toggle the history drawer" , appBinding [.ctrl 'S', .ctrl 's'] .toggleState none "toggle the state drawer" @@ -276,8 +272,7 @@ inductive ContextTarget where namespace ContextTarget -def all - : List ContextTarget := +def all : List ContextTarget := [.formulas, .symbols, .problem, .goal, .translation, .term] def name @@ -371,8 +366,7 @@ def fallbackSize : Size := { columns := 110, rows := 28 } def inputConfig : TextInputConfig := { width := 160, maxLength := 16_384 } -def multilineConfig - : MultilineConfig := +def multilineConfig : MultilineConfig := { text := inputConfig, lineBreak := .ctrl 'n' } private def minFrameWidth : Nat := 34 @@ -443,9 +437,7 @@ def dimText { segments := text.segments.map fun segment => { segment with style := Style.dim <+> segment.style } } -private -def base64Alphabet - : String := +private def base64Alphabet : String := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/" private @@ -705,8 +697,13 @@ def transcriptLines let views := entries.reverse.map (transcriptLine scheme symbols width) (spacedEntries views).flatMap splitLines -private def reportWidget (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat) - (entry : TranscriptEntry) : Option CollapsibleRender := do +private +def reportWidget + (scheme : ColorScheme) + (symbols : Array Symbol) + (width : Nat) + (entry : TranscriptEntry) + : Option CollapsibleRender := do let report ← entry.report pure <| renderCollapsible (reportWidgetConfig scheme) (max 1 (width - 2)) (reportSummary scheme report) (reportBody scheme symbols width entry report) @@ -1125,8 +1122,7 @@ def toggleFocusedProver { updated with statusNotice := some s!"{ProverReference.display reference} { if enabled then "disabled" else "enabled"}" } -def contextTargetNames - : List String := +def contextTargetNames : List String := ContextTarget.all.map ContextTarget.name def contextTargetOfString diff --git a/OATP/Runtime.lean b/OATP/Runtime.lean index 943c217..c607340 100644 --- a/OATP/Runtime.lean +++ b/OATP/Runtime.lean @@ -24,7 +24,9 @@ inductive CatalogueCache where | refresh | noCache -def readProblem (path : String) : IO Problem := do +def readProblem + (path : String) + : IO Problem := do pure { name := path, source := ← IO.FS.readFile path } def defaultLocalProverCandidates : Array String := #["eprover", "vampire", "metis"] @@ -41,8 +43,9 @@ def localProverCandidates : IO (Array String) := do pure <| value.splitOn "," |>.map (·.trimAscii.toString) |>.filter (!·.isEmpty) |>.toArray | none => pure defaultLocalProverCandidates -def catalogueLocation (cacheNamespace endpoint : String) : - IO (Option (System.FilePath × System.FilePath)) := do +def catalogueLocation + (cacheNamespace endpoint : String) + : IO (Option (System.FilePath × System.FilePath)) := do let root ← match ← IO.getEnv "XDG_CACHE_HOME" with | some path => pure (some (⟨path⟩ : System.FilePath)) | none => match ← IO.getEnv "HOME" with @@ -68,9 +71,11 @@ def httpErrorMessage | .bodyTooLarge actual limit => s!"HTTP response exceeded {limit} bytes ({actual} captured)" -def fetchCatalogue (endpoint : String) +def fetchCatalogue + (endpoint : String) (location : Option (System.FilePath × System.FilePath)) - (writeCache : Bool) : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do + (writeCache : Bool) + : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do match ← SystemOnTPTP.fetchCatalogue endpoint with | .error error => pure (.error (httpErrorMessage error)) | .ok response => @@ -89,8 +94,10 @@ def fetchCatalogue (endpoint : String) catch _ => pure () pure (.ok systems) -def loadCatalogue (cacheNamespace endpoint : String) (mode : CatalogueCache) : - IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do +def loadCatalogue + (cacheNamespace endpoint : String) + (mode : CatalogueCache) + : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do let location ← catalogueLocation cacheNamespace endpoint match mode with | .normal => @@ -113,8 +120,11 @@ def installedProvers : IO (Array String) := do found := found.push executable pure found -def resolveOnline (toolName : String) (systems : Array SystemOnTPTP.Catalogue.SystemInfo) - (references : List String) : Except String (Array SystemOnTPTP.Catalogue.SystemInfo) := do +def resolveOnline + (toolName : String) + (systems : Array SystemOnTPTP.Catalogue.SystemInfo) + (references : List String) + : Except String (Array SystemOnTPTP.Catalogue.SystemInfo) := do let resolved ← references.mapM fun reference => match SystemOnTPTP.Catalogue.resolve systems reference with | some system => pure system diff --git a/OATP/SystemOnTPTP.lean b/OATP/SystemOnTPTP.lean index 4a71687..c2bfc3a 100644 --- a/OATP/SystemOnTPTP.lean +++ b/OATP/SystemOnTPTP.lean @@ -62,24 +62,16 @@ private inductive HtmlPart where open Grip GParser -private -def htmlTag - : GParser conditional HtmlPart := +private def htmlTag : GParser conditional HtmlPart := HtmlPart.tag <$> GParser.capture (GParser.ch '<' *> GParser.takeWhile (· != 62) <* GParser.ch '>') -private -def htmlText - : GParser conditional HtmlPart := +private def htmlText : GParser conditional HtmlPart := HtmlPart.text <$> GParser.capture (GParser.takeWhile1 (· != 60)) -private -def htmlPart - : GParser conditional HtmlPart := +private def htmlPart : GParser conditional HtmlPart := GParser.chooseG htmlTag [htmlText] -private -def htmlDocument - : Grip.Parser (List HtmlPart) := +private def htmlDocument : Grip.Parser (List HtmlPart) := GParser.seqL (GParser.many htmlPart) GParser.eof private @@ -227,8 +219,10 @@ def request maxBodyBytes := config.maxBodyBytes maxRequestBodyBytes := config.maxBodyBytes -def submit (config : Config) (problem : Problem) : - IO (Except Http.Error Http.Response) := do +def submit + (config : Config) + (problem : Problem) + : IO (Except Http.Error Http.Response) := do let label := String.intercalate ", " (labels config).toList let request := request config problem let artifacts ← OATP.Artifacts.start s!"online {label}" problem @@ -315,8 +309,11 @@ def fetchCatalogue : IO (Except Http.Error Http.Response) := Http.requestWithTransport (catalogueRequest endpoint) -def parseResponse (config : Config) (problem : Problem) (response : Http.Response) : - Except ResponseError Artifact := do +def parseResponse + (config : Config) + (problem : Problem) + (response : Http.Response) + : Except ResponseError Artifact := do if response.statusCode < 200 || response.statusCode ≥ 300 then throw (.httpStatus response.statusCode) let token ← match SZSStatus.tokenFromOutput response.body with diff --git a/OATP/TPTP.lean b/OATP/TPTP.lean index 2373188..1be2295 100644 --- a/OATP/TPTP.lean +++ b/OATP/TPTP.lean @@ -64,8 +64,11 @@ end Syntax namespace Statement -def ofFof (name : String) (role : Role) (formula : _root_.TPTP.Formula.Expr) : - Except String _root_.TPTP.Statement := do +def ofFof + (name : String) + (role : Role) + (formula : _root_.TPTP.Formula.Expr) + : Except String _root_.TPTP.Statement := do let formula ← formula.toTPTP pure { kind := .fof diff --git a/OATP/Translate.lean b/OATP/Translate.lean index b3a8f46..06d80f9 100644 --- a/OATP/Translate.lean +++ b/OATP/Translate.lean @@ -43,15 +43,21 @@ def symbolName s!"{hexDigit (value / 16)}{hexDigit (value % 16)}" "oatp_" ++ if body.isEmpty then "atom" else String.intercalate "" body -private def unsupported (expression : Expr) : MetaM (Except String TPTP.Formula.Expr) := do +private +def unsupported + (expression : Expr) + : MetaM (Except String TPTP.Formula.Expr) := do let rendered ← ppExpr expression pure <| Except.error (s!"unsupported Lean proposition `{rendered}`; supported fragment is " ++ "propositional logic over named atoms") -- partiality: Lean Expr stores recursive applications in arrays; this private MetaM traversal -- is conservative and tested at the translation trust boundary. -private partial def translateProp (expression : Expr) : - MetaM (Except String TPTP.Formula.Expr) := do +private +partial +def translateProp + (expression : Expr) + : MetaM (Except String TPTP.Formula.Expr) := do let expression ← instantiateMVars expression let (function, arguments) := expression.getAppFnArgs if function == ``True && arguments.isEmpty then @@ -91,8 +97,12 @@ private partial def translateProp (expression : Expr) : return ← unsupported expression | _ => return ← unsupported expression -private def renderStatement (name : String) (role : _root_.TPTP.Role) - (formula : TPTP.Formula.Expr) : Except String String := do +private +def renderStatement + (name : String) + (role : _root_.TPTP.Role) + (formula : TPTP.Formula.Expr) + : Except String String := do let statement ← OATP.TPTP.Statement.ofFof name role formula pure <| _root_.TPTP.Statement.render statement diff --git a/examples/Cli.lean b/examples/Cli.lean index 3e6ba1d..20c6cf5 100644 --- a/examples/Cli.lean +++ b/examples/Cli.lean @@ -63,9 +63,7 @@ inductive ConfigAction where | show | path -private -def configActionParam - : Param ConfigAction := +private def configActionParam : Param ConfigAction := Param.named "ACTION" (Param.enum [("show", .show), ("path", .path)]) inductive Action where @@ -101,11 +99,18 @@ def cli private def doctorPalette : ColorScheme := ColorScheme.catppuccin -private def doctorSection (title : String) : IO Unit := do +private +def doctorSection + (title : String) + : IO Unit := do writeTextLine Text.empty writeTextLine (Text.styled title (Style.bold <+> Style.fg doctorPalette.purple)) -private def doctorRow (label value : String) (ok : Bool) : IO Unit := do +private +def doctorRow + (label value : String) + (ok : Bool) + : IO Unit := do let marker := if ok then Text.styled "✓" (Style.bold <+> Style.fg doctorPalette.green) else @@ -116,7 +121,10 @@ private def doctorRow (label value : String) (ok : Bool) : IO Unit := do writeTextLine (Text.plain " " ++ marker ++ Text.plain " " ++ label ++ Text.plain " " ++ Text.styled value valueStyle) -private def doctorTool (command : String) : IO Unit := do +private +def doctorTool + (command : String) + : IO Unit := do match ← Http.commandVersion command with | some version => doctorRow command version true | none => doctorRow command "not found" false @@ -222,7 +230,10 @@ def doctorIssueSummary private def doctorIssueFile : String := "oatp-doctor-issues.txt" -private def writeDoctorIssues (issues : List DoctorIssue) : IO (Option String) := do +private +def writeDoctorIssues + (issues : List DoctorIssue) + : IO (Option String) := do let entries := issues.map fun issue => s!"[{doctorIssueKindLabel issue.kind}] {issue.prover}\n{issue.detail}" try @@ -231,7 +242,10 @@ private def writeDoctorIssues (issues : List DoctorIssue) : IO (Option String) : pure (some doctorIssueFile) catch _ => pure none -private def printDiagnostic (message : String) : IO UInt32 := do +private +def printDiagnostic + (message : String) + : IO UInt32 := do let stderr ← IO.getStderr let target ← TermColor.targetWithTty .auto (← stderr.isTty) let report := (Report.error "command failed").withCode "cli" @@ -257,7 +271,11 @@ def configSelectedProvers else String.intercalate ", " (preferences.enabledProvers.toList.map configProverName) -private def runConfig (identity : CliIdentity) (action : ConfigAction) : IO UInt32 := do +private +def runConfig + (identity : CliIdentity) + (action : ConfigAction) + : IO UInt32 := do match action with | .path => match ← OATP.Config.path with @@ -287,9 +305,14 @@ private def runConfig (identity : CliIdentity) (action : ConfigAction) : IO UInt | none => pure 0 -- partiality: this live UI loop runs until an external IO action sets finished. -private partial def progressLoop (finished : IO.Ref Bool) - (config : Widgets.ProgressConfig) (state : Widgets.IndeterminateProgressState) - (region : LiveRegion) : IO Unit := do +private +partial +def progressLoop + (finished : IO.Ref Bool) + (config : Widgets.ProgressConfig) + (state : Widgets.IndeterminateProgressState) + (region : LiveRegion) + : IO Unit := do if ← finished.get then let _ ← region.finish pure () @@ -299,7 +322,12 @@ private partial def progressLoop (finished : IO.Ref Bool) IO.sleep 120 progressLoop finished config state region -private def withProgress {α : Type} (label : String) (action : IO α) : IO α := do +private +def withProgress + {α : Type} + (label : String) + (action : IO α) + : IO α := do if !(← stdoutSupportsControl) then return ← action withHiddenCursor do @@ -316,7 +344,10 @@ private def withProgress {α : Type} (label : String) (action : IO α) : IO α : let _ ← IO.ofExcept progress.get pure result -private def showArtifact (artifact : Artifact) : IO UInt32 := do +private +def showArtifact + (artifact : Artifact) + : IO UInt32 := do let marker := if SZSStatus.isSuccess artifact.status then "✓" else "!" IO.eprintln s!"{marker} {artifact.prover.label}: {artifact.status} ({artifact.elapsedMs}ms)" unless artifact.stdout.isEmpty || artifact.stdout.trimAscii.toString.startsWith " s!"local prover output exceeded {limit} bytes ({actual} captured)" -private def runLocal (toolName : String) (options : LocalOptions) : IO UInt32 := do +private +def runLocal + (toolName : String) + (options : LocalOptions) + : IO UInt32 := do try let problem ← readProblem options.problem let limits : Limits := { @@ -403,10 +438,15 @@ def portfolioView } { progress with label := Text.styled label (Style.fg doctorPalette.foreground) } -- partiality: this live UI loop runs until an external portfolio action sets finished. -private partial def portfolioProgressLoop (finished : IO.Ref Bool) +private +partial +def portfolioProgressLoop + (finished : IO.Ref Bool) (progress : IO.Ref Widgets.IndeterminateProgressState) - (results : IO.Ref (List Portfolio.Result)) (region : IO.Ref LiveRegion) - (total : Nat) : IO Unit := do + (results : IO.Ref (List Portfolio.Result)) + (region : IO.Ref LiveRegion) + (total : Nat) + : IO Unit := do if ← finished.get then pure () else @@ -420,8 +460,12 @@ private partial def portfolioProgressLoop (finished : IO.Ref Bool) IO.sleep 120 portfolioProgressLoop finished progress results region total -private def withPortfolioProgress {α : Type} (total : Nat) - (action : (Portfolio.Result → IO Unit) → IO α) : IO α := do +private +def withPortfolioProgress + {α : Type} + (total : Nat) + (action : (Portfolio.Result → IO Unit) → IO α) + : IO α := do if !(← stdoutSupportsControl) then return ← action (fun _ => pure ()) withHiddenCursor do @@ -450,7 +494,11 @@ private def withPortfolioProgress {α : Type} (total : Nat) let _ ← next.finish pure value -private def runDoctorOnline (identity : CliIdentity) (transports : Array String) : IO Bool := do +private +def runDoctorOnline + (identity : CliIdentity) + (transports : Array String) + : IO Bool := do doctorSection "ONLINE ATP (probe)" if transports.isEmpty then doctorRow "service" "unavailable (no HTTP transport)" false @@ -481,7 +529,10 @@ private def runDoctorOnline (identity : CliIdentity) (transports : Array String) | none => doctorRow "details" "could not write issue report" false pure (responsive > 0) -private def runDoctor (identity : CliIdentity) : IO UInt32 := do +private +def runDoctor + (identity : CliIdentity) + : IO UInt32 := do let transports ← Http.availableTransports let (online, ready) := if transports.contains "curl" then @@ -508,7 +559,11 @@ private def runDoctor (identity : CliIdentity) : IO UInt32 := do pure <| if transports.isEmpty || !onlineWorking then 1 else 0 -private def runPortfolio (problem : Problem) (attempts : Array Portfolio.Attempt) : IO UInt32 := do +private +def runPortfolio + (problem : Problem) + (attempts : Array Portfolio.Attempt) + : IO UInt32 := do let results ← withPortfolioProgress attempts.size fun onResult => Portfolio.runWith problem attempts onResult let mut success := false @@ -516,7 +571,11 @@ private def runPortfolio (problem : Problem) (attempts : Array Portfolio.Attempt success := (← showPortfolioResult result) || success pure <| if success then 0 else 1 -private def runDefault (identity : CliIdentity) (options : RunOptions) : IO UInt32 := do +private +def runDefault + (identity : CliIdentity) + (options : RunOptions) + : IO UInt32 := do try let problem ← readProblem options.problem let rawReferences ← if options.provers.isEmpty then @@ -578,7 +637,11 @@ private def runDefault (identity : CliIdentity) (options : RunOptions) : IO UInt else runPortfolio problem attempts catch error => printDiagnostic s!"could not read problem: {error}" -private def runSystems (identity : CliIdentity) (options : SystemsOptions) : IO UInt32 := do +private +def runSystems + (identity : CliIdentity) + (options : SystemsOptions) + : IO UInt32 := do writeTextLine (Text.styled s!"{identity.name} systems {identity.version}" (Style.bold <+> Style.fg doctorPalette.purple)) writeTextLine (Text.styled "LOCAL" (Style.bold <+> Style.fg doctorPalette.cyan)) @@ -612,8 +675,13 @@ private def runSystems (identity : CliIdentity) (options : SystemsOptions) : IO (Style.fg doctorPalette.comment)) pure 0 -private def submitOnline (options : OnlineOptions) (problem : Problem) (endpoint : String) - (system : SystemOnTPTP.Catalogue.SystemInfo) : IO UInt32 := do +private +def submitOnline + (options : OnlineOptions) + (problem : Problem) + (endpoint : String) + (system : SystemOnTPTP.Catalogue.SystemInfo) + : IO UInt32 := do let config : SystemOnTPTP.Config := { systemLabel := system.id systemCommands := if system.command.isEmpty then #[] else #[(system.id, system.command)] @@ -630,7 +698,11 @@ private def submitOnline (options : OnlineOptions) (problem : Problem) (endpoint | .error error => printDiagnostic (responseErrorMessage error) | .ok artifact => showArtifact { artifact with elapsedMs := (← IO.monoMsNow) - started } -private def runOnline (identity : CliIdentity) (options : OnlineOptions) : IO UInt32 := do +private +def runOnline + (identity : CliIdentity) + (options : OnlineOptions) + : IO UInt32 := do try let problem ← readProblem options.problem let endpoint := options.remote.endpoint.getD identity.endpoint @@ -645,7 +717,9 @@ private def runOnline (identity : CliIdentity) (options : OnlineOptions) : IO UI s!"run `{identity.name} systems --online`") catch error => printDiagnostic s!"could not read problem: {error}" -def main (argv : List String) : IO UInt32 := do +def main + (argv : List String) + : IO UInt32 := do if let "repl" :: replArgs := argv then return ← oatpReplMain replArgs let identity ← cliIdentity diff --git a/examples/Repl.lean b/examples/Repl.lean index 3a91173..435c27e 100644 --- a/examples/Repl.lean +++ b/examples/Repl.lean @@ -38,7 +38,9 @@ def appendEntry (ok : Bool) (elapsedMs : Option Nat := none) (sources : Sources := #[]) - (diagnostic : Option Diagnostic := none) (report : Option Report := none) : App := + (diagnostic : Option Diagnostic := none) + (report : Option Report := none) + : App := { app with entries := { cell, input, output, ok, elapsedMs, sources, diagnostic, report } :: app.entries transcriptScroll := 0 @@ -252,12 +254,19 @@ def finishRunRows { row with status := .cancelled, detail := "skipped after first success" } else row else rows -private def publishRunRows (app : App) (rows : Array RunRow) : IO Unit := do +private +def publishRunRows + (app : App) + (rows : Array RunRow) + : IO Unit := do match app.runProgress with | some progress => progress.set rows | none => pure () -private def currentRunRows (app : App) : IO (Array RunRow) := do +private +def currentRunRows + (app : App) + : IO (Array RunRow) := do match app.runProgress with | some progress => progress.get | none => pure app.runRows @@ -292,7 +301,10 @@ def configProverName : String := OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value -private def configOutput (app : App) : IO (String × Report) := do +private +def configOutput + (app : App) + : IO (String × Report) := do let path := (← OATP.Config.path).map (fun value => s!"{value}") |>.getD "unavailable" let (_, warning) ← OATP.Config.load let current := preferences app @@ -329,7 +341,10 @@ private def configOutput (app : App) : IO (String × Report) := do | none => [] pure (output, report) -private def savePreferences (before after : App) : IO App := do +private +def savePreferences + (before after : App) + : IO App := do if preferences before == preferences after then pure after else @@ -353,7 +368,10 @@ private def selectableProvers : IO (Array OATP.ProverReference × Option String) | .ok online => pure (installed ++ online, none) | .error message => pure (installed, some message) -private def defaultProvers (app : App) : IO (Array OATP.ProverReference) := do +private +def defaultProvers + (app : App) + : IO (Array OATP.ProverReference) := do let installed ← installedProverReferences match app.defaultProver with | some reference => match reference.kind with @@ -366,8 +384,11 @@ private def defaultProvers (app : App) : IO (Array OATP.ProverReference) := do | some name => pure #[OATP.ProverReference.fromLocal name] | none => pure #[] -private def selectedProvers (app : App) (all includeDefault : Bool := false) : - IO (Array OATP.ProverReference) := do +private +def selectedProvers + (app : App) + (all includeDefault : Bool := false) + : IO (Array OATP.ProverReference) := do let installed ← installedProverReferences let selected ← if all then pure installed @@ -546,10 +567,7 @@ def startingRunRows { name := OATP.ProverReference.display reference, status := .running } | .error _ => #[{ name := "run", status := .running }] -private -def backgroundJobs - : TermColor.Repl.Terminal.JobConfig App - where +private def backgroundJobs : TermColor.Repl.Terminal.JobConfig App where shouldRun := fun app input => !app.busy && backendLine input start := fun app input => { app with busy := true @@ -606,7 +624,10 @@ def backgroundJobs #guard (backgroundJobs.start { repl := { history := #["first"] } } "/help").repl.history == #["first"] -private def systemsText (request : OATP.Repl.SystemsRequest) : IO String := do +private +def systemsText + (request : OATP.Repl.SystemsRequest) + : IO String := do let installed ← OATP.Runtime.installedProvers let lines := if installed.isEmpty then ["LOCAL: none"] else ["LOCAL:"] ++ installed.toList.map (fun prover => " " ++ prover) @@ -669,7 +690,11 @@ def proverMatches : Bool := fuzzy query (OATP.ProverReference.display reference) || fuzzy query reference.name -private def infoText (app : App) (query : String) : IO (String × Bool) := do +private +def infoText + (app : App) + (query : String) + : IO (String × Bool) := do let installed ← OATP.Runtime.installedProvers let found := installed.filter (fuzzy query) if found.size == 1 then @@ -743,13 +768,21 @@ def parseStepTokens | [] => .error "expected a proof step" | token :: _ => .error s!"unknown proof step `{token}`" -private def parseStep (source : String) : Except String OATP.Proof.Step := do +private +def parseStep + (source : String) + : Except String OATP.Proof.Step := do let (step, rest) ← parseStepTokens (OATP.Repl.splitWords source) match rest with | [] => pure step | token :: _ => .error s!"unexpected proof step token `{token}`" -private def submitGoal (app : App) (cell : Nat) (input formula : String) : IO App := do +private +def submitGoal + (app : App) + (cell : Nat) + (input formula : String) + : IO App := do let runtime ← match app.leanRuntime with | some runtime => pure runtime | none => OATP.Lean.Repl.create @@ -766,8 +799,13 @@ private def submitGoal (app : App) (cell : Nat) (input formula : String) : IO Ap translation := none term := none } cell input output true -private def submitTheoryFormula (app : App) (cell : Nat) (input : String) - (command : OATP.Repl.Command) : IO (Option App) := do +private +def submitTheoryFormula + (app : App) + (cell : Nat) + (input : String) + (command : OATP.Repl.Command) + : IO (Option App) := do match command with | .axiom name formula | .conjecture name formula => let role := match command with | .axiom _ _ => "axiom" | _ => "conjecture" @@ -778,8 +816,13 @@ private def submitTheoryFormula (app : App) (cell : Nat) (input : String) | .error message => pure (some (note app cell input message false)) | _ => pure none -private def submitLeanCommand (app : App) (cell : Nat) (input : String) - (command : OATP.Repl.Command) : IO (Option App) := do +private +def submitLeanCommand + (app : App) + (cell : Nat) + (input : String) + (command : OATP.Repl.Command) + : IO (Option App) := do match command with | .goal formula | .toLean formula => do return some (← submitGoal app cell input formula) @@ -822,7 +865,12 @@ private def submitLeanCommand (app : App) (cell : Nat) (input : String) | none => return some (note app cell input "no rendered term" false) | _ => pure none -private def applyPureCommand (app : App) (cell : Nat) (input : String) : IO App := do +private +def applyPureCommand + (app : App) + (cell : Nat) + (input : String) + : IO App := do match OATP.Repl.apply app.session input with | .ok session => let app := if changesContext input then invalidateContext { app with session } @@ -833,8 +881,13 @@ private def applyPureCommand (app : App) (cell : Nat) (input : String) : IO App pure <| appendEntry app cell input (lastHistory session) true | .error message => pure (note app cell input message false) -private def submitCommand (app : App) (cell : Nat) (input : String) - (command : OATP.Repl.Command) : IO App := do +private +def submitCommand + (app : App) + (cell : Nat) + (input : String) + (command : OATP.Repl.Command) + : IO App := do match command with | .quit => pure { app with running := false } | .load path => do @@ -982,7 +1035,11 @@ private def submitCommand (app : App) (cell : Nat) (input : String) pure (notePlain app cell input result.text result.ok none (some result.report)) | _ => applyPureCommand app cell input -private def submitCore (app : App) (input : String) : IO App := do +private +def submitCore + (app : App) + (input : String) + : IO App := do let input := input.trimAscii.toString let cell := app.session.nextCell let firstWord := (OATP.Repl.splitWords input).headD "" @@ -999,7 +1056,11 @@ private def submitCore (app : App) (input : String) : IO App := do else return (← applyPureCommand app cell input) -private def submit (app : App) (input : String) : IO App := do +private +def submit + (app : App) + (input : String) + : IO App := do let started ← IO.monoMsNow let updated ← submitCore app input let updated := clearSelection updated @@ -1009,7 +1070,10 @@ private def submit (app : App) (input : String) : IO App := do | entry :: rest => pure { app with entries := { entry with elapsedMs := some elapsedMs } :: rest } | [] => pure app -private def commandValues (typeName : String) : IO (List String) := do +private +def commandValues + (typeName : String) + : IO (List String) := do match typeName with | "TOPIC" => pure (List.eraseDups (OATP.Repl.helpTopics ++ OATP.Repl.commandNames)) | "FORMAT" | "THEORY" | "STEP" => @@ -1038,10 +1102,7 @@ def complete : IO (List Completion) := completeCommandWith OATP.Repl.commandSpec commandValues input -private -def appKeymap - : TermColor.Repl.Terminal.AppKeymap App - where +private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where Action := AppKeyAction keymap := Keymap.fromSpecs appBindings contexts := fun app => @@ -1261,7 +1322,10 @@ private def reportTestApp : App := { | some app => app.transcriptScroll == 3 && app.panelFocus == .main | none => false -private def interactive (initial : App) : IO Unit := do +private +def interactive + (initial : App) + : IO Unit := do withAlternateScreen do clearScreen TermColor.Repl.Terminal.run { @@ -1283,7 +1347,11 @@ private def interactive (initial : App) : IO Unit := do quit := fun app => { app with running := false } } -private def runScript (app : App) (lines : List String) : IO App := do +private +def runScript + (app : App) + (lines : List String) + : IO App := do let mut app := app for line in lines do if app.running then @@ -1291,16 +1359,17 @@ private def runScript (app : App) (lines : List String) : IO App := do app ← submit app line pure app -private def staticOutput (app : App) : IO Unit := do +private +def staticOutput + (app : App) + : IO Unit := do for entry in app.entries.reverse do IO.println s!"[{entry.cell}] › {entry.input}" let timing := entry.elapsedMs.map (fun milliseconds => s!" ({formatElapsed milliseconds})") |>.getD "" IO.println s!" {(if entry.ok then "=" else "!")} {entry.output}{timing}" -private -def usage - : String := +private def usage : String := "oatp repl — interactive theorem-proving workbench\n\n" ++ "usage:\n lake exe oatp repl\n lake exe oatp repl --script FILE\n\n" ++ "examples:\n /load problem.p\n /to-lean p => p\n /snapshot\n " ++ @@ -1313,7 +1382,10 @@ def scriptExitCode : UInt32 := if app.entries.all (·.ok) then 0 else 1 -private def initialApp (runtime : OATP.Lean.Repl.Runtime) : IO App := do +private +def initialApp + (runtime : OATP.Lean.Repl.Runtime) + : IO App := do let (prefs, warning) ← OATP.Config.load let runProgress ← IO.mkRef (#[] : Array RunRow) let scheme := themeByName prefs.theme |>.getD aurora @@ -1336,7 +1408,9 @@ private def initialApp (runtime : OATP.Lean.Repl.Runtime) : IO App := do statusNotice := warning } -def oatpReplMain (args : List String) : IO UInt32 := do +def oatpReplMain + (args : List String) + : IO UInt32 := do if args == ["--help"] || args == ["-h"] then IO.println usage return 0 diff --git a/test/Tests.lean b/test/Tests.lean index e287466..302755d 100644 --- a/test/Tests.lean +++ b/test/Tests.lean @@ -254,16 +254,13 @@ open OATP OATP.TPTP { columns := 100, rows := 24 }).plainText.contains "state •" #guard (OATP.ReplView.screen { stateOpen := true, panelFocus := .drawer } { columns := 100, rows := 24 }).plainText.contains "state • active" -def completionApp - : OATP.ReplView.App := +def completionApp : OATP.ReplView.App := { repl := { input := { value := "/st", cursor := 3 } completion := some { candidates := #[{ replacement := "/state" }] } } } #guard (OATP.ReplView.screen completionApp { columns := 100, rows := 24 }).plainText.contains "/state" #guard OATP.ReplView.formatElapsed 1_500 == "1.5 s" -private -def timedEntry - : OATP.ReplView.TranscriptEntry := +private def timedEntry : OATP.ReplView.TranscriptEntry := { cell := 1 input := "/to-lean p => p" output := "goal created" @@ -271,9 +268,7 @@ def timedEntry #guard (OATP.ReplView.screen { entries := [timedEntry] } { columns := 100, rows := 24 }).plainText.contains "(12 ms)" -private -def plainEntry - : OATP.ReplView.TranscriptEntry := +private def plainEntry : OATP.ReplView.TranscriptEntry := { cell := 1 input := "/to-lean p => p" output := "goal created" } From 1e544ea1c330e654ac39d2e953cbfb9c9632f13a Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 18 Sep 2026 16:29:27 -0500 Subject: [PATCH 3/4] style: give the assignment its own line Move a trailing := / := by off the ascribed type's last line onto its own line at indent 4, matching the bare := shape. --- OATP/Artifacts.lean | 6 +- OATP/Config.lean | 9 +- OATP/Core.lean | 15 ++- OATP/Http.lean | 24 ++-- OATP/Lean.lean | 3 +- OATP/Lean/Repl.lean | 15 ++- OATP/Portfolio.lean | 6 +- OATP/Process.lean | 3 +- OATP/ProverReference.lean | 15 ++- OATP/Repl.lean | 72 ++++++---- OATP/Repl/Context.lean | 57 +++++--- OATP/ReplView.lean | 273 +++++++++++++++++++++++++------------- OATP/SystemOnTPTP.lean | 54 +++++--- OATP/TPTP.lean | 15 ++- OATP/Term.lean | 6 +- OATP/Translate.lean | 12 +- examples/Cli.lean | 18 ++- examples/Repl.lean | 75 +++++++---- 18 files changed, 452 insertions(+), 226 deletions(-) diff --git a/OATP/Artifacts.lean b/OATP/Artifacts.lean index e837f07..336effa 100644 --- a/OATP/Artifacts.lean +++ b/OATP/Artifacts.lean @@ -24,7 +24,8 @@ structure Run where private def safeName (value : String) - : 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 @@ -64,7 +65,8 @@ def write def writeCommand (run : Run) (command : String) - : IO Unit := + : IO Unit + := write run "command.txt" command end OATP.Artifacts diff --git a/OATP/Config.lean b/OATP/Config.lean index 7030162..186321f 100644 --- a/OATP/Config.lean +++ b/OATP/Config.lean @@ -41,7 +41,8 @@ private def stringField (json : Json) (name fallback : String) - : String := + : String + := match field json name with | some (.str value) => value | _ => fallback @@ -50,7 +51,8 @@ private def stringArrayField (json : Json) (name : String) - : Array String := + : Array String + := match field json name with | some (.arr values) => let result : List String := values.toList.filterMap fun value => @@ -78,7 +80,8 @@ def fromJson private def toJson (preferences : Preferences) - : Json := + : Json + := .obj #[ ("theory", .str preferences.theory), ("defaultProver", .str preferences.defaultProver), diff --git a/OATP/Core.lean b/OATP/Core.lean index bccd1f6..5492f7a 100644 --- a/OATP/Core.lean +++ b/OATP/Core.lean @@ -51,7 +51,8 @@ namespace Prover def label (prover : Prover) - : String := + : String + := match prover.version with | some version => s!"{prover.name} {version}" | none => prover.name @@ -75,7 +76,8 @@ private def statusPrefixes : List String := ["% SZS status ", "# SZS status "] def tokenFromLine (line : String) - : Option String := + : Option String + := let line := line.trimAscii.toString let rec find : List String → Option String | [] => none @@ -96,7 +98,8 @@ def tokenFromLines private def resultTokenFromLine (line : String) - : Option String := + : Option String + := let line := line.trimAscii.toString match line.splitOn " says " with | _ :: result :: _ => @@ -106,7 +109,8 @@ def resultTokenFromLine def tokenFromOutput (output : String) - : Option String := + : Option String + := let lines := output.splitOn "\n" tokenFromLines lines |>.orElse fun _ => lines.findSome? resultTokenFromLine @@ -127,7 +131,8 @@ def ofString def ofOutput (output : String) - : Option SZSStatus := + : Option SZSStatus + := tokenFromOutput output >>= ofString def toString diff --git a/OATP/Http.lean b/OATP/Http.lean index 8fb3914..13f3685 100644 --- a/OATP/Http.lean +++ b/OATP/Http.lean @@ -35,7 +35,8 @@ private def hexDigits : Array Char := private def isUnreserved (byte : UInt8) - : Bool := + : Bool + := (byte >= 48 && byte <= 57) || (byte >= 65 && byte <= 90) || (byte >= 97 && byte <= 122) || @@ -44,7 +45,8 @@ def isUnreserved private def encodeByte (byte : UInt8) - : String := + : String + := if isUnreserved byte then Char.ofNat byte.toNat |>.toString else @@ -53,12 +55,14 @@ def encodeByte def encodeComponent (value : String) - : String := + : String + := String.join (value.toUTF8.toList.map encodeByte) def encodeUrlEncoded (fields : Array Field) - : String := + : String + := String.intercalate "&" <| fields.toList.map fun field => s!"{encodeComponent field.name}={encodeComponent field.value}" @@ -72,7 +76,8 @@ structure MultipartPart where private def validHeaderValue (value : String) - : Bool := + : Bool + := value.toList.all fun character => character != '"' && character != '\\' && character != '\r' && character != '\n' @@ -183,7 +188,8 @@ def statusMarker := "OATP_HTTP_STATUS:" private def statusFromOutput (output : String) - : Option (String × Nat) := + : Option (String × Nat) + := let parts := output.splitOn statusMarker match parts.reverse with | code :: before :: _ => @@ -226,7 +232,8 @@ def requestWithCurlUnsafe private def statusFromWgetLine (line : String) - : Option Nat := + : Option Nat + := let fields := line.trimAscii.toString.splitOn " " |>.filter (!·.isEmpty) match fields with | _ :: code :: _ => code.toNat? @@ -235,7 +242,8 @@ def statusFromWgetLine private def statusFromWgetOutput (output : String) - : Option Nat := + : Option Nat + := let rec find : List String → Option Nat | [] => none | line :: lines => diff --git a/OATP/Lean.lean b/OATP/Lean.lean index c21d2d2..3e14bf8 100644 --- a/OATP/Lean.lean +++ b/OATP/Lean.lean @@ -47,7 +47,8 @@ def snapshot (mvarId : MVarId) : MetaM GoalSnapshot := mvarId.withContext do def check (mvarId : MVarId) (candidate : Expr) - : MetaM (Except String CheckedProof) := + : MetaM (Except String CheckedProof) + := mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) let candidate ← instantiateMVars candidate diff --git a/OATP/Lean/Repl.lean b/OATP/Lean/Repl.lean index 7596e92..ae27063 100644 --- a/OATP/Lean/Repl.lean +++ b/OATP/Lean/Repl.lean @@ -70,7 +70,8 @@ private def addAtom (atoms : Array String) (name : String) - : Array String := + : Array String + := if atoms.contains name then atoms else atoms.push name private abbrev TranslationM := ExceptT String MetaM @@ -79,7 +80,8 @@ private def translationError {α : Type} (message : String) - : TranslationM α := + : TranslationM α + := ExceptT.mk (pure (.error message)) private @@ -87,7 +89,8 @@ partial def atomNames (formula : _root_.TPTP.Formula.Expr) (atoms : Array String) - : Array String := + : Array String + := match formula with | .atom predicate arguments => if arguments.isEmpty then addAtom atoms predicate else atoms @@ -102,7 +105,8 @@ def withAtoms {α : Type} (atoms : List String) (action : Array (String × Expr) → TranslationM α) - : MetaM (Except String α) := + : MetaM (Except String α) + := match atoms with | [] => (action #[]).run | atom :: rest => @@ -113,7 +117,8 @@ private def lookupAtom (atoms : Array (String × Expr)) (name : String) - : Option Expr := + : Option Expr + := atoms.find? (·.1 == name) |>.map Prod.snd private diff --git a/OATP/Portfolio.lean b/OATP/Portfolio.lean index 4eb0f40..111b474 100644 --- a/OATP/Portfolio.lean +++ b/OATP/Portfolio.lean @@ -127,7 +127,8 @@ def runWith def run (problem : Problem) (attempts : Array Attempt) - : IO (Array Result) := + : IO (Array Result) + := runWith problem attempts private @@ -157,7 +158,8 @@ def runWithStrategy (attempts : Array Attempt) (strategy : RunStrategy) (onResult : Result → IO Unit := fun _ => pure ()) - : IO (Array Result) := + : IO (Array Result) + := match strategy with | .all => runWith problem attempts onResult | .firstSuccess => runUntilSuccess problem attempts.toList #[] onResult diff --git a/OATP/Process.lean b/OATP/Process.lean index 9965799..cd400c6 100644 --- a/OATP/Process.lean +++ b/OATP/Process.lean @@ -26,7 +26,8 @@ structure Command where /-- Add the stdin filename expected by local provers that require one. -/ def Command.withStdinProblem (command : Command) - : Command := + : Command + := let executable := (command.executable.splitOn "/").getLast?.getD command.executable if executable == "metis" && !command.arguments.any (· == "-") then { command with arguments := command.arguments.push "-" } diff --git a/OATP/ProverReference.lean b/OATP/ProverReference.lean index 5537e4a..da8ecf9 100644 --- a/OATP/ProverReference.lean +++ b/OATP/ProverReference.lean @@ -31,17 +31,20 @@ def fromLocal (name : String) : ProverReference := { name, kind := .local } def fromOnline (name : String) - : ProverReference := + : ProverReference + := { name := OATP.SystemOnTPTP.onlineSystemId name, kind := .online } def ofString (name : String) - : ProverReference := + : ProverReference + := if OATP.SystemOnTPTP.isOnlineReference name then fromOnline name else fromLocal name def fromPersisted (value : String) - : Option ProverReference := + : Option ProverReference + := if value.startsWith "local:" then let name := value.drop "local:".length |>.toString if name.isEmpty then none else some (fromLocal name) @@ -52,14 +55,16 @@ def fromPersisted def persisted (reference : ProverReference) - : String := + : String + := match reference.kind with | .local => "local:" ++ reference.name | .online => "online:" ++ reference.name def display (reference : ProverReference) - : String := + : String + := match reference.kind with | .local => reference.name | .online => OATP.SystemOnTPTP.onlineReference reference.name diff --git a/OATP/Repl.lean b/OATP/Repl.lean index f24061d..d917128 100644 --- a/OATP/Repl.lean +++ b/OATP/Repl.lean @@ -39,7 +39,8 @@ def runStrategyChoices : List String := OATP.RunStrategy.choices def completionParam (typeName : String) (values : List String) - : Param String := + : Param String + := Param.named typeName (Param.enum (values.map fun value => (value, value))) def contextIndexParam : Param Nat := @@ -47,7 +48,8 @@ def contextIndexParam : Param Nat := def staticCompletionValues (typeName : String) - : List String := + : List String + := match typeName with | "TOPIC" => helpTopics | "FORMAT" => roleFormats @@ -173,7 +175,8 @@ def parseSpec {g : Grade} (spec : Argus.Spec g α) (args : List String) - : Except String α := + : Except String α + := match Argus.run spec args with | .ok value => .ok value | .error errors => .error (String.intercalate "\n" (errors.map Argus.Err.message)) @@ -201,7 +204,8 @@ def splitTerminator private def runRequestOf (options : RunOptions) - : RunRequest := + : RunRequest + := let (references, arguments) := splitArguments options.references { references := (references ++ options.provers).map ProverReference.ofString all := options.all @@ -215,7 +219,8 @@ def runRequestOf private def localRequestOf (options : LocalOptions) - : LocalRequest := + : LocalRequest + := let (_, arguments) := splitArguments options.arguments { executable := options.executable timeout := options.resources.timeout.getD OATP.defaultTimeoutSeconds @@ -225,7 +230,8 @@ def localRequestOf private def onlineRequestOf (options : OnlineOptions) - : OnlineRequest := + : OnlineRequest + := { system := options.system endpoint := options.remote.endpoint timeout := options.remote.resources.timeout.getD OATP.defaultTimeoutSeconds @@ -234,27 +240,31 @@ def onlineRequestOf private def systemsRequestOf (options : SystemsOptions) - : SystemsRequest := + : SystemsRequest + := { online := options.online, endpoint := options.catalogue.endpoint, refresh := options.catalogue.refresh, noCache := options.catalogue.noCache } def parseRunRequest (args : List String) - : Except String RunRequest := + : Except String RunRequest + := let (args, tail) := splitTerminator args parseSpec RunOptions.spec args |>.map fun request => { runRequestOf request with arguments := tail.getD (runRequestOf request).arguments } def parseLocalRequest (args : List String) - : Except String LocalRequest := + : Except String LocalRequest + := let (args, tail) := splitTerminator args parseSpec LocalOptions.spec args |>.map fun request => { localRequestOf request with arguments := tail.getD (localRequestOf request).arguments } def parseOnlineRequest (args : List String) - : Except String OnlineRequest := + : Except String OnlineRequest + := let (args, tail) := splitTerminator args match tail with | some (_ :: _) => .error "online commands do not accept arguments after --" @@ -262,7 +272,8 @@ def parseOnlineRequest def parseSystemsRequest (args : List String) - : Except String SystemsRequest := + : Except String SystemsRequest + := let (args, tail) := splitTerminator args match tail with | some (_ :: _) => .error "systems does not accept arguments after --" @@ -270,7 +281,8 @@ def parseSystemsRequest def splitWords (source : String) - : List String := + : List String + := let whitespace (character : Char) : Bool := character.isWhitespace let (current, words) := source.toList.foldl (fun (current, words) character => if whitespace character then @@ -283,7 +295,8 @@ def splitWords private def textSpec (name help : String) - : Spec (1 * (1 * conditional * flexible)) String := + : Spec (1 * (1 * conditional * flexible)) String + := Spec.map (fun values : List String => String.intercalate " " values) (Spec.map2 (fun value values => value :: values) (Spec.arg name help (Param.named name Param.str)) @@ -382,7 +395,8 @@ def commandSpec : Argus.Command Command := private def commandArgv (source : String) - : List String × Option (List String) := + : List String × Option (List String) + := match splitWords source.trimAscii.toString with | command :: args => let command := (command.drop 1).toString @@ -394,7 +408,8 @@ private def appendCommandArguments (command : Command) (tail : Option (List String)) - : Except String Command := + : Except String Command + := match tail with | none => .ok command | some arguments => @@ -410,7 +425,8 @@ def appendCommandArguments def parseCommandSpec (source : String) - : Except String Command := + : Except String Command + := let line := source.trimAscii.toString if !line.startsWith "/" then .error "commands start with `/`; try `/help`" else @@ -452,7 +468,8 @@ def usageArguments private def usageLine (command : Argus.Command Command) - : String := + : String + := let flags := if command.toMeta.flags.isEmpty then "" else " [OPTIONS]" let arguments := match command.body with | .opts spec => usageArguments spec @@ -468,7 +485,8 @@ def commandHelpText : String := def parseCommand (source : String) - : Command := + : Command + := let line := source.trimAscii.toString match parseCommandSpec line with | .ok command => command @@ -476,7 +494,8 @@ def parseCommand def parseInput (source : String) - : Submission := + : Submission + := if source.trimAscii.toString.startsWith "/" then .command (parseCommand source) else @@ -553,7 +572,8 @@ private def grammarHelp : String := private def roleHelp (topic : Option String) - : String := + : String + := let format := topic.getD "all" String.intercalate "\n" [ s!"Roles ({format})", @@ -640,7 +660,8 @@ private def contextHelp : String := private def commandHelp (command : Argus.Command Command) - : String := + : String + := let details := match command.name with | "goal" | "to-lean" | "translate-to-lean" | "snapshot" | "to-tptp" | "reconstruct" | "term" => leanHelp @@ -656,7 +677,8 @@ def commandHelp private def normalizeHelpTopic (topic : String) - : String := + : String + := let topic := topic.trimAscii.toString if topic.startsWith "/" then topic.drop 1 |>.trimAscii.toString else topic @@ -691,13 +713,15 @@ private def addFormulaCommand (session : Session) (input name role formula : String) - : Except String Session := + : Except String Session + := parseSource session input s!"fof({name}, {role}, {formula})." def apply (session : Session) (input : String) - : Except String Session := + : Except String Session + := match parseInput input with | .source source => parseSource session source source | .command command => diff --git a/OATP/Repl/Context.lean b/OATP/Repl/Context.lean index f476cb9..7a1cf10 100644 --- a/OATP/Repl/Context.lean +++ b/OATP/Repl/Context.lean @@ -67,7 +67,8 @@ private def addSymbol (symbols : Array Symbol) (symbol : Symbol) - : Array Symbol := + : Array Symbol + := if symbols.any (· == symbol) then symbols else symbols.push symbol private @@ -75,7 +76,8 @@ partial def collectTerm (term : _root_.TPTP.Formula.Term) (symbols : Array Symbol) - : Array Symbol := + : Array Symbol + := match term with | .var name => addSymbol symbols { kind := .variable, name } | .constant name => addSymbol symbols { kind := .constant, name } @@ -88,7 +90,8 @@ partial def collectFormula (formula : _root_.TPTP.Formula.Expr) (symbols : Array Symbol) - : Array Symbol := + : Array Symbol + := match formula with | .atom predicate arguments => let symbols := addSymbol symbols @@ -107,7 +110,8 @@ private def formulaView (id cell : Nat) (statement : _root_.TPTP.Statement) - : FormulaView := + : FormulaView + := match OATP.TPTP.Statement.parseFormula statement with | .ok formula => { id, cell @@ -131,14 +135,16 @@ private def contextItems (nextId cell : Nat) (document : _root_.TPTP.Document) - : Array ContextItem × Nat := + : Array ContextItem × Nat + := document.items.foldl (fun (items, nextId) item => (items.push { id := nextId, cell, value := item }, nextId + 1)) (#[], nextId) private def viewsOf (items : Array ContextItem) - : Array FormulaView := + : Array FormulaView + := items.foldl (fun views item => match item.value with | .statement statement => views.push (formulaView item.id item.cell statement) @@ -147,19 +153,22 @@ def viewsOf private def symbolsOf (views : Array FormulaView) - : Array Symbol := + : Array Symbol + := views.foldl (fun symbols view => view.symbols.foldl addSymbol symbols) #[] private def problemSourceOf (items : Array ContextItem) - : String := + : String + := String.intercalate "\n" (items.toList.map (fun item => item.value.render)) private def rebuildContext (session : Session) - : Session := + : Session + := let formulas := viewsOf session.context { session with problemSource := problemSourceOf session.context @@ -170,7 +179,8 @@ private def record (session : Session) (input result : String) - : Session := + : Session + := { session with nextCell := session.nextCell + 1 history := session.history.push { cell := session.nextCell, input, result } } @@ -178,14 +188,16 @@ def record def note (session : Session) (input result : String) - : Session := + : Session + := record session input result def addDocument (session : Session) (input : String) (document : _root_.TPTP.Document) - : Session := + : Session + := let (items, nextContextId) := contextItems session.nextContextId session.nextCell document let session := rebuildContext { session with context := session.context ++ items @@ -194,13 +206,15 @@ def addDocument def clearContext (session : Session) - : Session := + : Session + := rebuildContext { session with context := #[] } private def validateStatement (statement : _root_.TPTP.Statement) - : Except String Unit := + : Except String Unit + := match statement.kind, statement.role with | .cnf, .conjecture => .error ("CNF does not support the `conjecture` role; use " ++ @@ -210,7 +224,8 @@ def validateStatement private def validateDocument (document : _root_.TPTP.Document) - : Except String Unit := + : Except String Unit + := document.items.toList.mapM (fun item => match item with | _root_.TPTP.Item.statement statement => validateStatement statement | _root_.TPTP.Item.include _ => pure ()) |>.map (fun _ => ()) @@ -228,7 +243,8 @@ def parseDocument def parseSource (session : Session) (input source : String) - : Except String Session := + : Except String Session + := match parseDocument source with | .ok document => pure (addDocument session input document) | .error message => .error message @@ -239,14 +255,16 @@ private def missingContextIndices (session : Session) (indices : List Nat) - : List Nat := + : List Nat + := indices.filter (fun index => !session.context.any (·.id == index)) def removeContext (session : Session) (input : String) (indices : List Nat) - : Except String Session := + : Except String Session + := let indices := indices.eraseDups if indices.isEmpty then .error "remove expects at least one context index" @@ -292,7 +310,8 @@ def updateContext def problem (session : Session) - : Option Problem := + : Option Problem + := if session.problemSource.isEmpty then none else some { name := "oatp-repl" source := session.problemSource diff --git a/OATP/ReplView.lean b/OATP/ReplView.lean index 92ea18c..cec163d 100644 --- a/OATP/ReplView.lean +++ b/OATP/ReplView.lean @@ -159,7 +159,8 @@ def appBinding (action : AppKeyAction) (context : Option AppContext) (description : String) - : BindingSpec AppKeyAction := + : BindingSpec AppKeyAction + := { keys action context := context.map AppContext.keyContext @@ -195,14 +196,16 @@ def appBindings : List (BindingSpec AppKeyAction) := def appKeyLabel (action : AppKeyAction) (context : AppContext) - : String := + : String + := (appBindings.find? (fun binding => binding.action == action && (binding.context == none || binding.context == some (AppContext.keyContext context)))).map (·.label) |>.getD "?" def themeByName (name : String) - : Option ColorScheme := + : Option ColorScheme + := themes.find? (fun pair => pair.1 == name) |>.map Prod.snd def themeNames : String := String.intercalate ", " (themes.map Prod.fst) @@ -376,7 +379,8 @@ private def frameWidth (width : Nat) : Nat := max minFrameWidth width private def boxInnerWidth (outer : Nat) - : Nat := + : Nat + := Layout.boxInnerWidth { padding := 1 } outer private def panelWidth (width : Nat) : Nat := frameWidth width - 2 @@ -386,7 +390,8 @@ private def stateDrawerMinWidth : Nat := 70 private def stateDrawerWidths (width : Nat) - : Option (Nat × Nat) := + : Option (Nat × Nat) + := let total := frameWidth width if total < stateDrawerMinWidth then none else @@ -396,7 +401,8 @@ def stateDrawerWidths def drawerWidths (width : Nat) - : Option (Nat × Nat) := + : Option (Nat × Nat) + := stateDrawerWidths width private @@ -410,14 +416,16 @@ private def fitText (width : Nat) (value : String) - : Text := + : Text + := truncate width (Text.plain value) private def fillHeight (height : Nat) (text : Text) - : Text := + : Text + := let height := max 1 height let lines := (splitLines text).take height joinLines (lines ++ List.replicate (height - lines.length) Text.empty) @@ -426,14 +434,16 @@ private def withBackground (scheme : ColorScheme) (text : Text) - : Text := + : Text + := { segments := text.segments.map fun segment => { segment with style := Style.bg scheme.background <+> segment.style } } private def dimText (text : Text) - : Text := + : Text + := { segments := text.segments.map fun segment => { segment with style := Style.dim <+> segment.style } } @@ -443,7 +453,8 @@ private def base64Alphabet : String := private def base64Char (index : Nat) - : Char := + : Char + := base64Alphabet.toList.getD index 'A' private @@ -466,7 +477,8 @@ def base64 private def clipboardSequence (value : String) - : String := + : String + := "\u001b]52;c;" ++ base64 value.toUTF8.toList ++ "\u0007" private @@ -475,7 +487,8 @@ def opaqueScreen (size : Size) (content : Text) (copyPending : Option String := none) - : Text := + : Text + := let width := max 1 size.columns let rows := max 1 size.rows let blank := Text.styled (String.ofList (List.replicate width ' ')) @@ -489,7 +502,8 @@ def opaqueScreen def formatElapsed (milliseconds : Nat) - : String := + : String + := if milliseconds == 0 then "<1 ms" else if milliseconds < 1_000 then s!"{milliseconds} ms" else s!"{milliseconds / 1_000}.{milliseconds % 1_000 / 100} s" @@ -500,14 +514,16 @@ def diagnosticView (width : Nat) (sources : Sources) (diagnostic : Diagnostic) - : Text := + : Text + := TermColor.Diagnostics.render sources diagnostic { width := max 1 (frameWidth width - 2), contextLines := 0, hyperlinks := false } scheme private def identifierChar (character : Char) - : Bool := + : Bool + := character.isAlpha || character.isDigit || character == '_' || character == '$' || character == '\'' @@ -528,7 +544,8 @@ def symbolStyle (symbols : Array Symbol) (token : String) (highlightSyntax : Bool := true) - : Style := + : Style + := let lower := token.toLower let semantic := semanticColors scheme if token.startsWith "/" then Style.bold <+> Style.fg scheme.orange @@ -556,7 +573,8 @@ private def operatorStyle (scheme : ColorScheme) (token : String) - : Style := + : Style + := if token == "!" || token == "?" then Style.fg scheme.pink else if token == "(" || token == ")" || token == "[" || token == "]" || token == "," || token == ":" || token == "." || token == ";" then Style.fg scheme.purple @@ -568,7 +586,8 @@ def semanticText (symbols : Array Symbol) (value : String) (highlightSyntax : Bool := true) - : Text := + : Text + := let flush := fun (state : Text × String) => if state.2.isEmpty then state else (state.1 ++ Text.styled state.2 @@ -594,7 +613,8 @@ private def semanticFormula (scheme : ColorScheme) (formula : FormulaView) - : Text := + : Text + := semanticText scheme formula.symbols formula.formula private @@ -602,7 +622,8 @@ def formulaLine (scheme : ColorScheme) (selected : Option Nat) (formula : FormulaView) - : Text := + : Text + := let marker := if selected == some formula.id then "▸ " else " " Text.styled s!"{marker}index #{formula.id} • cell {formula.cell} • {formula.role} " (Style.dim <+> Style.fg scheme.comment) ++ @@ -623,7 +644,8 @@ private def reportSummary (scheme : ColorScheme) (report : Report) - : Text := + : Text + := let marker := match report.severity with | .error => Text.styled "issues" (Style.bold <+> Style.fg scheme.red) | .warning => Text.styled "warning" (Style.bold <+> Style.fg scheme.yellow) @@ -637,7 +659,8 @@ def reportBody (width : Nat) (entry : TranscriptEntry) (report : Report) - : Text := + : Text + := renderReport report { width := max 1 (width - 6) } scheme ++ Text.plain "\n" ++ semanticText scheme symbols entry.output false @@ -647,7 +670,8 @@ def transcriptLine (symbols : Array Symbol) (width : Nat) (entry : TranscriptEntry) - : Text := + : Text + := let input := Text.styled s!"[{entry.cell}] " (Style.dim <+> Style.fg scheme.comment) ++ Text.styled "› " (Style.bold <+> Style.fg scheme.orange) ++ semanticText scheme symbols entry.input false @@ -693,7 +717,8 @@ def transcriptLines (symbols : Array Symbol) (width : Nat) (entries : List TranscriptEntry) - : List Text := + : List Text + := let views := entries.reverse.map (transcriptLine scheme symbols width) (spacedEntries views).flatMap splitLines @@ -712,7 +737,8 @@ def reportWidget def reportAtTranscriptRow (app : App) (width row : Nat) - : Option Nat := + : Option Nat + := let rec find : List TranscriptEntry → Nat → Option Nat | [], _ => none | entry :: rest, offset => @@ -730,7 +756,8 @@ def reportAtTranscriptRow def toggleReportCell (app : App) (cell : Nat) - : App := + : App + := { app with entries := app.entries.map fun entry => if entry.cell == cell then { entry with reportExpanded := !entry.reportExpanded } else entry } @@ -739,7 +766,8 @@ private def visibleTranscriptLines (app : App) (width budget : Nat) - : List Text := + : List Text + := let lines := transcriptLines app.theme app.session.symbols width app.entries let scroll := min app.transcriptScroll (lines.length - budget) let visibleEnd := lines.length - scroll @@ -750,7 +778,8 @@ private def transcript (app : App) (width budget bodyStart : Nat) - : Text := + : Text + := let lines := visibleTranscriptLines app width budget if lines.isEmpty then Text.styled "Type a TPTP statement or /help." (Style.dim <+> Style.fg app.theme.comment) @@ -772,39 +801,46 @@ private def selectionLines (app : App) (width budget : Nat) - : List String := + : List String + := (visibleTranscriptLines app width budget).map (·.plainText) def scrollTranscriptUp (app : App) - : App := + : App + := { app with transcriptScroll := app.transcriptScroll + 3 } def scrollTranscriptDown (app : App) - : App := + : App + := { app with transcriptScroll := app.transcriptScroll - min 3 app.transcriptScroll } def scrollTranscriptPageUp (app : App) - : App := + : App + := { app with transcriptScroll := app.transcriptScroll + 10 } def scrollTranscriptPageDown (app : App) - : App := + : App + := { app with transcriptScroll := app.transcriptScroll - min 10 app.transcriptScroll } def clearSelection (app : App) - : App := + : App + := { app with selectionStart := none, selectionEnd := none } private def symbolLine (scheme : ColorScheme) (symbol : Symbol) - : Text := + : Text + := let kind := match symbol.kind with | .variable => "var" | .constant => "const" @@ -833,7 +869,8 @@ def contextWidgetConfig private def contextSections (app : App) - : List (Nat × Text × Text) := + : List (Nat × Text × Text) + := let formulas := app.session.formulas.toList.reverse.take 8 let symbols := app.session.symbols.toList.take 12 let problem := if app.session.context.isEmpty then @@ -880,14 +917,16 @@ private def contextExpandedAt (app : App) (index : Nat) - : Bool := + : Bool + := app.contextExpanded.getD index true private def contextState (app : App) (index : Nat) - : CollapsibleState := + : CollapsibleState + := { expanded := contextExpandedAt app index focused := app.contextFocus == index } @@ -895,7 +934,8 @@ private def contextRenders (app : App) (width : Nat) - : List (Nat × CollapsibleRender) := + : List (Nat × CollapsibleRender) + := let innerWidth := max 1 (boxInnerWidth width) let rec go : List (Nat × Text × Text) → List (Nat × CollapsibleRender) | [] => [] @@ -908,13 +948,15 @@ private def contextTexts (app : App) (width : Nat) - : List Text := + : List Text + := (contextRenders app width).map (fun (_, widget) => widget.text) def contextHitAtRow (app : App) (width row : Nat) - : Option (Nat × Bool) := + : Option (Nat × Bool) + := if row < 2 then none else let relativeRow := row - 2 @@ -929,7 +971,8 @@ def contextHitAtRow def contextFormulaAtRow (app : App) (width row : Nat) - : Option Nat := + : Option Nat + := match contextHitAtRow app width row with | some (0, false) => let relativeRow := row - 2 @@ -946,26 +989,30 @@ def updateContextExpanded (app : App) (index : Nat) (expanded : Bool) - : App := + : App + := { app with contextExpanded := app.contextExpanded.set! index expanded } def focusContext (app : App) (index : Nat) - : App := + : App + := { app with contextFocus := min (contextSectionCount - 1) index } private def visibleContextIndices (app : App) - : Array Nat := + : Array Nat + := (contextSections app).map (fun (index, _, _) => index) |>.toArray private def moveContext (app : App) (forward : Bool) - : App := + : App + := let indices := visibleContextIndices app if indices.isEmpty then app @@ -980,18 +1027,21 @@ def moveContext def focusNextContext (app : App) - : App := + : App + := moveContext app true def focusPreviousContext (app : App) - : App := + : App + := moveContext app false private def formulaIds (app : App) - : List Nat := + : List Nat + := app.session.formulas.toList.reverse.map (·.id) private @@ -1008,7 +1058,8 @@ private def nextFormulaId (app : App) (forward : Bool) - : Option Nat := + : Option Nat + := let ids := formulaIds app |>.take 8 match ids with | [] => none @@ -1022,28 +1073,32 @@ def nextFormulaId def focusContextItem (app : App) (id : Nat) - : App := + : App + := if app.session.formulas.any (·.id == id) then { app with contextFocus := 0, contextItemFocus := some id } else app def focusNextContextItem (app : App) - : App := + : App + := match nextFormulaId app true with | some id => focusContextItem app id | none => { app with contextItemFocus := none } def focusPreviousContextItem (app : App) - : App := + : App + := match nextFormulaId app false with | some id => focusContextItem app id | none => { app with contextItemFocus := none } def focusNextContextEntry (app : App) - : App := + : App + := if app.contextFocus == 0 && app.session.formulas.isEmpty == false then match nextFormulaId app true with | some id => focusContextItem app id @@ -1052,7 +1107,8 @@ def focusNextContextEntry def focusPreviousContextEntry (app : App) - : App := + : App + := if app.contextFocus == 0 && app.session.formulas.isEmpty == false then match nextFormulaId app false with | some id => focusContextItem app id @@ -1061,57 +1117,67 @@ def focusPreviousContextEntry def toggleFocusedContext (app : App) - : App := + : App + := updateContextExpanded app app.contextFocus (!contextExpandedAt app app.contextFocus) def expandFocusedContext (app : App) - : App := + : App + := updateContextExpanded app app.contextFocus true def collapseFocusedContext (app : App) - : App := + : App + := updateContextExpanded app app.contextFocus false def focusProver (app : App) (index : Nat) - : App := + : App + := let focus := if app.proverChoices.isEmpty then 0 else min (app.proverChoices.size - 1) index { app with proverFocus := focus } def focusNextProver (app : App) - : App := + : App + := focusProver app ((app.proverFocus + 1) % max 1 app.proverChoices.size) def focusPreviousProver (app : App) - : App := + : App + := focusProver app (if app.proverFocus == 0 then max 1 app.proverChoices.size - 1 else app.proverFocus - 1) def focusRun (app : App) (index : Nat) - : App := + : App + := let focus := if app.runRows.isEmpty then 0 else min (app.runRows.size - 1) index { app with runFocus := focus } def focusNextRun (app : App) - : App := + : App + := focusRun app ((app.runFocus + 1) % max 1 app.runRows.size) def focusPreviousRun (app : App) - : App := + : App + := focusRun app (if app.runFocus == 0 then max 1 app.runRows.size - 1 else app.runFocus - 1) def toggleFocusedProver (app : App) - : App := + : App + := if app.proverChoices.isEmpty then app else let reference := app.proverChoices[app.proverFocus]! let enabled := app.enabledProvers.any (· == reference) @@ -1127,14 +1193,16 @@ def contextTargetNames : List String := def contextTargetOfString (value : String) - : Option Nat := + : Option Nat + := ContextTarget.indexOfString value private def prepareContextCommand (app : App) (command : String) - : App := + : App + := match app.contextItemFocus with | none => { app with statusNotice := some "select a formula in the FORMULAS box first" } | some id => @@ -1158,7 +1226,8 @@ def editContextItem (app : App) : App := prepareContextCommand app "update" def openContextTarget (app : App) (target : String) - : Option App := + : Option App + := if target.toLower == "all" then let app := { app with stateOpen := true } some { app with contextExpanded := Array.replicate contextSectionCount true } @@ -1171,7 +1240,8 @@ def openContextTarget def toggleStatePanel (app : App) - : App := + : App + := if app.stateOpen && app.panelFocus == .drawer then { app with stateOpen := false, panelFocus := .main } else @@ -1184,7 +1254,8 @@ def toggleStatePanel def toggleHistoryPanel (app : App) - : App := + : App + := if app.historyOpen && app.panelFocus == .drawer then { app with historyOpen := false, panelFocus := .main } else @@ -1197,7 +1268,8 @@ def toggleHistoryPanel def toggleRunPanel (app : App) - : App := + : App + := if app.runRows.isEmpty then { app with statusNotice := some "no prover run to inspect" } else if app.runOpen && app.panelFocus == .drawer then @@ -1214,7 +1286,8 @@ private def contextPanel (app : App) (width height : Nat) - : Text := + : Text + := let body := joinLines (contextTexts app width) let innerWidth := boxInnerWidth width let body := padRight innerWidth (fillHeight (max 1 (height - 2)) body) @@ -1244,7 +1317,8 @@ def historyWidget (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntry) - : Option CollapsibleRender := + : Option CollapsibleRender + := if entry.input.startsWith "/help" then let expanded := app.historyExpanded.any (· == entry.cell) let lines := entry.result.splitOn "\n" |>.length @@ -1259,7 +1333,8 @@ def historyLine (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntry) - : Text := + : Text + := let input := Text.styled s!"[{entry.cell}] " (Style.dim <+> Style.fg app.theme.comment) ++ semanticText app.theme app.session.symbols entry.input false match historyWidget app width entry with @@ -1273,7 +1348,8 @@ private def historyPanel (app : App) (width height : Nat) - : Text := + : Text + := let rows := app.session.history.toList.reverse.take 18 let body := if rows.isEmpty then Text.styled "No commands yet." (Style.dim <+> Style.fg app.theme.comment) @@ -1287,7 +1363,8 @@ def historyPanel def historyCellAtRow (app : App) (width row : Nat) - : Option Nat := + : Option Nat + := let rows := app.session.history.toList.reverse.take 18 let rec find : List OATP.Repl.HistoryEntry → Nat → Option Nat | [], _ => none @@ -1303,7 +1380,8 @@ def historyCellAtRow def toggleHistoryCell (app : App) (cell : Nat) - : App := + : App + := let expanded := if app.historyExpanded.any (· == cell) then app.historyExpanded.filter (· != cell) else app.historyExpanded.push cell @@ -1312,7 +1390,8 @@ def toggleHistoryCell def proverVisibleStart (app : App) (height : Nat) - : Nat := + : Nat + := let visible := max 1 (height - 2) if app.proverFocus >= visible then app.proverFocus - visible + 1 else 0 @@ -1320,7 +1399,8 @@ private def proverPanel (app : App) (width height : Nat) - : Text := + : Text + := let visible := max 1 (height - 2) let start := proverVisibleStart app height let rows := if app.proverChoices.isEmpty then @@ -1356,7 +1436,8 @@ def runStatusStyle private def runDetail (row : RunRow) - : String := + : String + := if !row.detail.isEmpty then row.detail else match row.status with | .queued => "queued; waiting for the previous prover" | .running => "waiting for the prover result" @@ -1368,7 +1449,8 @@ private def runPanel (app : App) (width height : Nat) - : Text := + : Text + := let innerWidth := boxInnerWidth width let rows := if app.runRows.isEmpty then [Text.styled "No active prover run." (Style.dim <+> Style.fg app.theme.comment)] @@ -1398,7 +1480,8 @@ def runPanel private def mascot (scheme : ColorScheme) - : Text := + : Text + := let arrow := Text.styled "──▶" (Style.fg scheme.cyan) joinLines [ Text.styled "TPTP" (Style.fg scheme.yellow) ++ Text.plain " " ++ arrow ++ Text.plain " " ++ Text.styled "OATP" (Style.bold <+> Style.fg scheme.green) ++ @@ -1411,7 +1494,8 @@ private def banner (scheme : ColorScheme) (width : Nat) - : Text := + : Text + := let outer := frameWidth width let inner := boxInnerWidth outer let leftContent := @@ -1463,7 +1547,8 @@ private def compactHeader (scheme : ColorScheme) (width : Nat) - : Text := + : Text + := let outer := frameWidth width let title := s!" oatp repl v{version} " let used := title.length + 2 @@ -1476,7 +1561,8 @@ def reportAtScreenRow (app : App) (size : Size) (row : Nat) - : Option Nat := + : Option Nat + := let width := frameWidth size.columns let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width let bodyStart := head.height + 1 @@ -1487,7 +1573,8 @@ def prompt (width : Nat) (state : Repl.State) (focused : Bool := true) - : Text := + : Text + := let outer := frameWidth width let input := box (Text.styled "› " (Style.bold <+> Style.fg scheme.orange) ++ TermColor.Repl.renderMultilineTextInputBody @@ -1507,7 +1594,8 @@ private def footer (app : App) (width : Nat) - : Text := + : Text + := let outer := frameWidth width let state := if app.busy then "[BUSY]" else "[READY]" let closeRun := appKeyLabel .closeRun .runInput @@ -1554,7 +1642,8 @@ def footer def selectedText (app : App) (size : Size) - : String := + : String + := let width := frameWidth size.columns let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width let foot := prompt app.theme width app.repl (app.panelFocus == .main) ++ @@ -1576,7 +1665,8 @@ private def calcContent (app : App) (size : Size) - : Text := + : Text + := let width := frameWidth size.columns let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width let foot := prompt app.theme width app.repl (app.panelFocus == .main) ++ @@ -1589,7 +1679,8 @@ def calcContent def screen (app : App) (size : Size) - : Text := + : Text + := let width := frameWidth size.columns let size := { size with columns := width } let drawerOpen := app.runOpen || app.proversOpen || diff --git a/OATP/SystemOnTPTP.lean b/OATP/SystemOnTPTP.lean index c2bfc3a..c5959a5 100644 --- a/OATP/SystemOnTPTP.lean +++ b/OATP/SystemOnTPTP.lean @@ -42,7 +42,8 @@ def onlineReference (systemId : String) : String := onlineReferencePrefix ++ sys def onlineSystemId (reference : String) - : String := + : String + := if isOnlineReference reference then (reference.drop onlineReferencePrefix.length).toString else reference @@ -77,7 +78,8 @@ private def htmlDocument : Grip.Parser (List HtmlPart) := private def parseHtml (source : String) - : Except Grip.ParseError (List HtmlPart) := + : Except Grip.ParseError (List HtmlPart) + := htmlDocument.parse source.toUTF8 namespace Catalogue @@ -91,7 +93,8 @@ structure SystemInfo where private def quotedAfter (marker line : String) - : Option String := + : Option String + := match line.splitOn marker with | _ :: value :: _ => some (value.splitOn "\"" |>.headD "") | _ => none @@ -99,14 +102,16 @@ def quotedAfter private def systemId (line : String) - : Option String := + : Option String + := (quotedAfter "NAME=\"System___" line).orElse fun _ => quotedAfter "name=\"System___" line private def fieldValue (field id current line : String) - : String := + : String + := let lower := quotedAfter s!"name=\"{field}___{id}\"" line let upper := quotedAfter s!"NAME=\"{field}___{id}\"" line if lower.isSome || upper.isSome then @@ -117,7 +122,8 @@ private def updateInfo (line : String) (system : SystemInfo) - : SystemInfo := + : SystemInfo + := let command := fieldValue "Command" system.id system.command line let timeLimit := (fieldValue "TimeLimit" system.id (toString system.timeLimit) line).toNat?.getD system.timeLimit @@ -125,7 +131,8 @@ def updateInfo def parse (html : String) - : Array SystemInfo := + : Array SystemInfo + := match parseHtml html with | .error _ => #[] | .ok parts => parts.foldl (init := #[]) fun systems part => @@ -144,7 +151,8 @@ def baseName (id : String) : String := id.splitOn "---" |>.headD id def matchesReference (reference : String) (system : SystemInfo) - : Bool := + : Bool + := let reference := onlineSystemId reference let wanted := reference.toLower let id := system.id.toLower @@ -154,21 +162,24 @@ def matchesReference def resolve (systems : Array SystemInfo) (reference : String) - : Option SystemInfo := + : Option SystemInfo + := systems.toList.find? (matchesReference reference) end Catalogue def labels (config : Config) - : Array String := + : Array String + := if config.systemLabels.isEmpty then #[config.systemLabel] else config.systemLabels private def command (config : Config) (label : String) - : String := + : String + := config.systemCommands.toList.find? (·.1 == label) |>.map (·.2) |>.getD "default" inductive ResponseError where @@ -189,7 +200,8 @@ def ResponseError.message def fields (config : Config) (problem : Problem) - : Array Field := + : Array Field + := let base : Array Field := #[ { name := "ProblemSource", value := "FORMULAE" }, { name := "FORMULAEProblem", value := problem.source }, @@ -243,13 +255,15 @@ private def tagStarts (needle : String) (tag : String) - : Bool := + : Bool + := tag.toLower.startsWith needle private def bodyText (parts : List HtmlPart) - : String := + : String + := let hasBody := parts.any fun part => match part with | .tag tag => tagStarts " false @@ -272,13 +286,15 @@ def bodyText private def decodeHtmlEntities (value : String) - : String := + : String + := value.replace ">" ">" |>.replace "<" "<" |>.replace "&" "&" |>.replace """ "\"" |>.replace "'" "'" def parseResponseText (body : String) - : Except Grip.ParseError String := + : Except Grip.ParseError String + := let body := body.trimAscii.toString if !body.startsWith " text | .error _ => body @@ -306,7 +323,8 @@ def catalogueRequest def fetchCatalogue (endpoint : String) - : IO (Except Http.Error Http.Response) := + : IO (Except Http.Error Http.Response) + := Http.requestWithTransport (catalogueRequest endpoint) def parseResponse diff --git a/OATP/TPTP.lean b/OATP/TPTP.lean index 1be2295..43bc99e 100644 --- a/OATP/TPTP.lean +++ b/OATP/TPTP.lean @@ -35,19 +35,22 @@ def theoryChoices : List String := supportedTheories ++ theoryAliases.map Prod.f def normalizeTheory (value : String) - : Option String := + : Option String + := let value := value.toLower if value ∈ supportedTheories then some value else theoryAliases.find? (·.1 == value) |>.map Prod.snd def parse (source : String) - : Except Grip.ParseError Document := + : Except Grip.ParseError Document + := _root_.TPTP.parseString source def parseStatement (source : String) - : Except Grip.ParseError Statement := + : Except Grip.ParseError Statement + := _root_.TPTP.parseStatementString source namespace Syntax @@ -57,7 +60,8 @@ abbrev Formula := _root_.TPTP.Formula.Expr def parseFormula (source : String) - : Except Grip.ParseError Formula := + : Except Grip.ParseError Formula + := _root_.TPTP.Formula.parseFormulaString source end Syntax @@ -79,7 +83,8 @@ def ofFof def parseFormula (statement : _root_.TPTP.Statement) - : Except Grip.ParseError _root_.TPTP.Formula.Expr := + : Except Grip.ParseError _root_.TPTP.Formula.Expr + := _root_.TPTP.Statement.parseFormula statement end Statement diff --git a/OATP/Term.lean b/OATP/Term.lean index d2586d9..055f38a 100644 --- a/OATP/Term.lean +++ b/OATP/Term.lean @@ -32,12 +32,14 @@ def eventText def renderPlain (events : Array SearchEvent) - : String := + : String + := String.intercalate "\n" (events.toList.map (fun event => (eventText event).plainText)) def renderAnsi16 (events : Array SearchEvent) - : String := + : String + := String.intercalate "\n" (events.toList.map (fun event => Text.render RenderTarget.ansi16 (eventText event))) diff --git a/OATP/Translate.lean b/OATP/Translate.lean index 06d80f9..866b49c 100644 --- a/OATP/Translate.lean +++ b/OATP/Translate.lean @@ -31,13 +31,15 @@ structure GoalTranslation where private def hexDigit (value : Nat) - : Char := + : Char + := if value < 10 then Char.ofNat (48 + value) else Char.ofNat (97 + (value - 10)) private def symbolName (raw : String) - : String := + : String + := let body := raw.toUTF8.toList.map fun byte => let value := byte.toNat s!"{hexDigit (value / 16)}{hexDigit (value % 16)}" @@ -109,12 +111,14 @@ def renderStatement private def renderFormula (formula : TPTP.Formula.Expr) - : Except String String := + : Except String String + := formula.toTPTP def translateGoal (mvarId : MVarId) - : MetaM (Except String GoalTranslation) := + : MetaM (Except String GoalTranslation) + := mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) unless ← isProp target do diff --git a/examples/Cli.lean b/examples/Cli.lean index 20c6cf5..6fb8702 100644 --- a/examples/Cli.lean +++ b/examples/Cli.lean @@ -77,7 +77,8 @@ inductive Action where def cli (identity : CliIdentity) - : Argus.Command Action := + : Argus.Command Action + := Argus.group identity.name [ Argus.cmd "run" (Spec.map Action.run RunOptions.spec) (description := "Run a local or explicitly selected online portfolio") @@ -147,7 +148,8 @@ private def doctorOnlineAttempts (endpoint : String) (systems : Array SystemOnTPTP.Catalogue.SystemInfo) - : Array Portfolio.Attempt := + : Array Portfolio.Attempt + := let timeout := OATP.Runtime.doctorTimeoutSeconds let outputLimit := OATP.Runtime.doctorMaxOutputBytes systems.map fun system => { @@ -221,7 +223,8 @@ def portfolioName private def doctorIssueSummary (issues : List DoctorIssue) - : String := + : String + := let kinds : List DoctorIssueKind := [.noSZSStatus, .transportTimeout, .transportFailure, .httpError, .requestFailure] String.intercalate " · " <| kinds.filterMap fun kind => @@ -257,13 +260,15 @@ def printDiagnostic private def configProverName (value : String) - : String := + : String + := OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value private def configSelectedProvers (preferences : OATP.Config.Preferences) - : String := + : String + := if !preferences.proverSelectionSet then "automatic" else if preferences.enabledProvers.isEmpty then @@ -425,7 +430,8 @@ def portfolioView (total : Nat) (progress : Widgets.IndeterminateProgressState) (results : List Portfolio.Result) - : Text := + : Text + := let latest := match results.getLast? with | some result => s!" · latest {portfolioName result}" | none => "" diff --git a/examples/Repl.lean b/examples/Repl.lean index 435c27e..f8fff40 100644 --- a/examples/Repl.lean +++ b/examples/Repl.lean @@ -40,7 +40,8 @@ def appendEntry (sources : Sources := #[]) (diagnostic : Option Diagnostic := none) (report : Option Report := none) - : App := + : App + := { app with entries := { cell, input, output, ok, elapsedMs, sources, diagnostic, report } :: app.entries transcriptScroll := 0 @@ -52,7 +53,8 @@ def appendEntry private def diagnosticFor (source message : String) - : Source × Diagnostic := + : Source × Diagnostic + := let sourceText := source let source := Source.fromBytes "input" source.toUTF8 let title := message.splitOn "\n" |>.headD message @@ -67,7 +69,8 @@ def note (input output : String) (ok : Bool) (elapsedMs : Option Nat := none) - : App := + : App + := let (sources, diagnostic) := if ok then (#[], none) else @@ -84,7 +87,8 @@ def notePlain (ok : Bool) (elapsedMs : Option Nat := none) (report : Option Report := none) - : App := + : App + := appendEntry { app with session := OATP.Repl.note app.session input output } cell input output ok elapsedMs #[] none report @@ -97,7 +101,8 @@ def noteDiagnostic (app : App) (cell : Nat) (input source message : String) - : App := + : App + := let (source, diagnostic) := diagnosticFor source message appendEntry { app with session := OATP.Repl.note app.session input message } cell input message false @@ -106,13 +111,15 @@ def noteDiagnostic private def clearDerived (app : App) - : App := + : App + := { app with goal := none, translation := none, term := none, leanGoal := none } private def invalidateContext (app : App) - : App := + : App + := { clearDerived app with runRows := #[] runOpen := false @@ -122,7 +129,8 @@ def invalidateContext private def clearTranscript (app : App) - : App := + : App + := { app with entries := [] transcriptScroll := 0 @@ -135,7 +143,8 @@ def clearTranscript private def changesContext (input : String) - : Bool := + : Bool + := match OATP.Repl.parseInput input with | .source _ => true | .command command => match command with @@ -145,7 +154,8 @@ def changesContext private def lastHistory (session : OATP.Repl.Session) - : String := + : String + := session.history.toList.reverse.head?.map (·.result) |>.getD "ok" private @@ -190,7 +200,8 @@ private def runReport (strategy : OATP.RunStrategy) (results : List Portfolio.Result) - : Report := + : Report + := let issues := results.filter resultHasIssue let report := if strategy == .firstSuccess && results.any resultSucceeded then Report.info "first successful prover completed" @@ -212,7 +223,8 @@ structure RunOutput where private def failedRunOutput (code message : String) - : RunOutput := + : RunOutput + := { text := message, ok := false, report := (Report.error message).withCode code } private @@ -235,7 +247,8 @@ private def runRowsFor (attempts : Array Portfolio.Attempt) (strategy : OATP.RunStrategy) - : Array RunRow := + : Array RunRow + := attempts.mapIdx fun index attempt => { name := attempt.name status := if strategy == .all || index == 0 then .running else .queued } @@ -245,7 +258,8 @@ def finishRunRows (rows : Array RunRow) (results : List Portfolio.Result) (strategy : OATP.RunStrategy) - : Array RunRow := + : Array RunRow + := let rows := results.foldl (fun rows result => let completed := runRow result rows.map fun current => if current.name == completed.name then completed else current) rows @@ -274,14 +288,16 @@ def currentRunRows private def currentProblem (app : App) - : Option Problem := + : Option Problem + := app.translation.map (fun source => { name := "lean-goal", source }) |>.orElse (fun _ => OATP.Repl.problem app.session) private def theoryStatus (theory : String) - : String := + : String + := s!"theory: {theory}; available: {String.intercalate ", " OATP.TPTP.supportedTheories}" #guard theoryStatus "fof" == "theory: fof; available: fof, cnf, tff" @@ -298,7 +314,8 @@ private def preferences (app : App) : OATP.Config.Preferences := { private def configProverName (value : String) - : String := + : String + := OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value private @@ -528,7 +545,8 @@ def runRequest private def backendLine (input : String) - : Bool := + : Bool + := match OATP.Repl.parseCommandSpec input with | .ok command => match command with | .run _ | .local _ | .online _ | .check => true @@ -538,7 +556,8 @@ def backendLine private def backendRequest (input : String) - : Except String (OATP.Repl.RunRequest × Bool) := + : Except String (OATP.Repl.RunRequest × Bool) + := match OATP.Repl.parseCommandSpec input with | .ok (.run request) => pure (request, false) | .ok (.local request) => pure ({ @@ -558,7 +577,8 @@ def backendRequest private def startingRunRows (input : String) - : Array RunRow := + : Array RunRow + := match backendRequest input with | .ok (request, includeDefault) => if request.references.isEmpty then #[{ name := if includeDefault then @@ -678,7 +698,8 @@ private def fuzzy (query : String) (value : String) - : Bool := + : Bool + := let query := query.toLower let value := value.toLower value == query || value.startsWith query || value.contains query @@ -687,7 +708,8 @@ private def proverMatches (query : String) (reference : OATP.ProverReference) - : Bool := + : Bool + := fuzzy query (OATP.ProverReference.display reference) || fuzzy query reference.name private @@ -1099,7 +1121,8 @@ private def complete (_app : App) (input : TextInputState) - : IO (List Completion) := + : IO (List Completion) + := completeCommandWith OATP.Repl.commandSpec commandValues input private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where @@ -1177,7 +1200,8 @@ def handleMouse (app : App) (size : Size) (mouse : MouseEvent) - : Option App := + : Option App + := if app.runOpen then match drawerWidths size.columns with | none => none @@ -1379,7 +1403,8 @@ private def usage : String := private def scriptExitCode (app : App) - : UInt32 := + : UInt32 + := if app.entries.all (·.ok) then 0 else 1 private From c2ef2b942a21343a5edd3500cb7c8026219789e9 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 18 Sep 2026 19:21:57 -0500 Subject: [PATCH 4/4] style: split every declaration that spans lines Treat := do like := by so those declarations convert too, hoist attributes above the keyword line, and split any multi-line header in full, not just ones with binders. --- OATP/Artifacts.lean | 11 ++-- OATP/Config.lean | 20 +++++-- OATP/Core.lean | 4 +- OATP/Http.lean | 36 +++++++++---- OATP/Lean.lean | 10 ++-- OATP/Lean/Repl.lean | 25 ++++++--- OATP/Portfolio.lean | 12 +++-- OATP/Process.lean | 9 ++-- OATP/Proof.lean | 17 ++++-- OATP/Properties/Basic.lean | 9 ++-- OATP/Repl.lean | 60 ++++++++++++++++----- OATP/Repl/Context.lean | 9 ++-- OATP/ReplView.lean | 32 +++++++++--- OATP/Runtime.lean | 23 +++++--- OATP/SystemOnTPTP.lean | 26 +++++++--- OATP/TPTP.lean | 3 +- OATP/Translate.lean | 9 ++-- examples/Cli.lean | 80 +++++++++++++++++++--------- examples/Demo.lean | 4 +- examples/ProofDemo.lean | 9 +++- examples/Repl.lean | 104 ++++++++++++++++++++++++++----------- test/Tests.lean | 18 +++++-- 22 files changed, 382 insertions(+), 148 deletions(-) diff --git a/OATP/Artifacts.lean b/OATP/Artifacts.lean index 336effa..862eb92 100644 --- a/OATP/Artifacts.lean +++ b/OATP/Artifacts.lean @@ -30,7 +30,10 @@ def safeName 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 @@ -38,7 +41,8 @@ private def roots : IO (List System.FilePath) := do def start (label : String) (problem : Problem) - : IO (Option Run) := do + : IO (Option Run) + := do let stamp ← IO.monoMsNow for root in ← roots do -- ponytail: 64 bounded suffixes cover same-millisecond concurrent runs; @@ -58,7 +62,8 @@ def start def write (run : Run) (name content : String) - : IO Unit := do + : IO Unit + := do try IO.FS.writeFile (System.FilePath.join run.directory name) content catch _ => pure () diff --git a/OATP/Config.lean b/OATP/Config.lean index 186321f..16aa317 100644 --- a/OATP/Config.lean +++ b/OATP/Config.lean @@ -21,7 +21,10 @@ 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 => @@ -29,10 +32,14 @@ private def configRoot : IO (Option System.FilePath) := do | 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 @@ -91,7 +98,9 @@ def toJson ("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 => @@ -104,7 +113,8 @@ def load : IO (Preferences × Option String) := do def save (preferences : Preferences) - : IO (Option String) := do + : IO (Option String) + := do match ← path with | none => pure (some "cannot persist preferences: HOME/XDG_CONFIG_HOME is unset") | some file => diff --git a/OATP/Core.lean b/OATP/Core.lean index 5492f7a..66b94b7 100644 --- a/OATP/Core.lean +++ b/OATP/Core.lean @@ -153,7 +153,9 @@ def isSuccess | .theorem | .unsatisfiable => true | _ => false -instance : ToString SZSStatus where +instance + : ToString SZSStatus + where toString := toString end SZSStatus diff --git a/OATP/Http.lean b/OATP/Http.lean index 13f3685..8825bfe 100644 --- a/OATP/Http.lean +++ b/OATP/Http.lean @@ -26,7 +26,10 @@ structure Field where value : String deriving BEq, DecidableEq, Repr -private def hexDigits : Array Char := +private +def hexDigits + : Array Char + := #[ '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'A', 'B', 'C', 'D', 'E', 'F' @@ -84,7 +87,8 @@ def validHeaderValue def encodeMultipart (boundary : String) (parts : Array MultipartPart) - : Except String String := do + : Except String String + := do if boundary.isEmpty || !boundary.toList.all (fun character => character.isAlphanum || character == '-' || character == '_') then throw "multipart boundary must contain only letters, digits, '-' or '_'" @@ -140,7 +144,8 @@ structure Response where def commandVersion (command : String) - : IO (Option String) := do + : IO (Option String) + := do try let output ← IO.Process.output { cmd := command, args := #["--version"] } if output.exitCode != 0 then @@ -151,7 +156,9 @@ def commandVersion pure <| if line.isEmpty then none else some line catch _ => pure none -def availableTransports : IO (Array String) := do +def availableTransports + : IO (Array String) + := do let mut available := #[] for command in #["curl", "wget"] do if (← commandVersion command).isSome then @@ -201,7 +208,8 @@ def statusFromOutput private def requestWithCurlUnsafe (request : Request) - : IO (Except Error Response) := do + : IO (Except Error Response) + := do let base : Array String := #[ "--silent", "--show-error", "--max-time", toString request.maxSeconds, @@ -257,7 +265,8 @@ def statusFromWgetOutput private def requestWithWgetUnsafe (request : Request) - : IO (Except Error Response) := do + : IO (Except Error Response) + := do let base : Array String := #[ "--quiet", "--server-response", "--max-redirect=0", "--tries=1", "--timeout=" ++ toString request.maxSeconds, @@ -286,7 +295,8 @@ def requestWithWgetUnsafe private def validateRequest (request : Request) - : Except Error Unit := do + : Except Error Unit + := do if request.url.isEmpty then throw (.invalidRequest "HTTP request URL must not be empty") if request.maxSeconds == 0 then @@ -300,7 +310,8 @@ def validateRequest private def requestWithTransportUnsafe (request : Request) - : IO (Except Error Response) := do + : IO (Except Error Response) + := do match validateRequest request with | .error error => return .error error | .ok _ => pure () @@ -314,7 +325,8 @@ def requestWithTransportUnsafe def requestWithTransport (request : Request) - : IO (Except Error Response) := do + : IO (Except Error Response) + := do try requestWithTransportUnsafe request catch error => @@ -323,7 +335,8 @@ def requestWithTransport def requestWith (transport : Transport) (request : Request) - : IO (Except Error Response) := do + : IO (Except Error Response) + := do try match validateRequest request with | .error error => pure (.error error) @@ -336,7 +349,8 @@ def requestWith def requestWithCurl (request : Request) - : IO (Except Error Response) := do + : IO (Except Error Response) + := do requestWith .curl request end OATP.Http diff --git a/OATP/Lean.lean b/OATP/Lean.lean index 3e14bf8..fc4ce30 100644 --- a/OATP/Lean.lean +++ b/OATP/Lean.lean @@ -27,7 +27,8 @@ structure CheckedProof where private def prettyExpr (expression : Expr) - : MetaM String := do + : MetaM String + := do let formatted ← ppExpr expression pure s!"{formatted}" @@ -60,8 +61,11 @@ def check let actual ← prettyExpr candidateType pure (.error s!"candidate type mismatch: expected {expected}, got {actual}") -def checkAndAssign (mvarId : MVarId) (candidate : Expr) : - MetaM (Except String CheckedProof) := mvarId.withContext do +def checkAndAssign + (mvarId : MVarId) + (candidate : Expr) + : MetaM (Except String CheckedProof) + := mvarId.withContext do match ← check mvarId candidate with | .error message => pure (.error message) | .ok checked => diff --git a/OATP/Lean/Repl.lean b/OATP/Lean/Repl.lean index ae27063..d0e72ad 100644 --- a/OATP/Lean/Repl.lean +++ b/OATP/Lean/Repl.lean @@ -47,7 +47,9 @@ private def coreContext : Core.Context := { quotContext := `OATP } -def create : IO Runtime := do +def create + : IO Runtime + := do Lean.initSearchPath (← Lean.getBuildDir) let env ← Lean.importModules #[{ module := `Init.Prelude }] {} pure { @@ -61,7 +63,8 @@ def runMeta {α : Type} (runtime : Runtime) (action : MetaM α) - : IO (α × Runtime) := do + : IO (α × Runtime) + := do let (value, coreState, metaState) ← action.toIO runtime.coreContext runtime.coreState {} runtime.metaState pure (value, { runtime with coreState, metaState }) @@ -126,7 +129,8 @@ partial def toLean (atoms : Array (String × Expr)) (formula : _root_.TPTP.Formula.Expr) - : TranslationM Expr := do + : TranslationM Expr + := do match formula with | .atom predicate arguments => if !arguments.isEmpty then @@ -160,7 +164,8 @@ private def makeGoal (source : String) (formula : _root_.TPTP.Formula.Expr) - : MetaM (Except String Goal) := do + : MetaM (Except String Goal) + := do let atoms := atomNames formula #[] withAtoms atoms.toList fun locals => do let target ← toLean locals formula @@ -170,7 +175,8 @@ def makeGoal def goalFromFormula (runtime : Runtime) (source : String) - : IO (Except String (Runtime × Goal)) := do + : IO (Except String (Runtime × Goal)) + := do match OATP.TPTP.Syntax.parseFormula source with | .error error => pure (.error (error.pretty source.toUTF8)) | .ok formula => @@ -180,14 +186,16 @@ def goalFromFormula def snapshot (runtime : Runtime) (goal : Goal) - : IO (Runtime × OATP.GoalSnapshot) := do + : IO (Runtime × OATP.GoalSnapshot) + := do let (value, runtime) ← runMeta runtime (OATP.Lean.snapshot goal.mvarId) pure (runtime, value) def translateToTPTP (runtime : Runtime) (goal : Goal) - : IO (Runtime × Except String OATP.Lean.GoalTranslation) := do + : IO (Runtime × Except String OATP.Lean.GoalTranslation) + := do let (value, runtime) ← runMeta runtime (OATP.Lean.translateGoal goal.mvarId) pure (runtime, value) @@ -195,7 +203,8 @@ def reconstruct (runtime : Runtime) (goal : Goal) (step : OATP.Proof.Step) - : IO (Runtime × Except String RenderedTerm) := do + : IO (Runtime × Except String RenderedTerm) + := do let action : MetaM (Except String RenderedTerm) := do match ← OATP.Proof.reconstruct goal.mvarId step with | .error message => pure (.error message) diff --git a/OATP/Portfolio.lean b/OATP/Portfolio.lean index 111b474..e46a99c 100644 --- a/OATP/Portfolio.lean +++ b/OATP/Portfolio.lean @@ -77,7 +77,8 @@ def Failure.output def execute (problem : Problem) (attempt : Attempt) - : IO Result := do + : IO Result + := do match attempt.backend with | .local command => match ← Process.run { name := attempt.name } problem attempt.limits command with @@ -106,7 +107,8 @@ def collect (pending : List (Task (Except IO.Error Result))) (results : Array Result) (onResult : Result → IO Unit) - : IO (Array Result) := do + : IO (Array Result) + := do match pending with | [] => pure results | task :: rest => @@ -119,7 +121,8 @@ def runWith (problem : Problem) (attempts : Array Attempt) (onResult : Result → IO Unit := fun _ => pure ()) - : IO (Array Result) := do + : IO (Array Result) + := do let tasks ← attempts.toList.mapM fun attempt => IO.asTask (execute problem attempt) Task.Priority.dedicated collect tasks #[] onResult @@ -144,7 +147,8 @@ def runUntilSuccess (attempts : List Attempt) (results : Array Result) (onResult : Result → IO Unit) - : IO (Array Result) := do + : IO (Array Result) + := do match attempts with | [] => pure results | attempt :: rest => diff --git a/OATP/Process.lean b/OATP/Process.lean index cd400c6..3727438 100644 --- a/OATP/Process.lean +++ b/OATP/Process.lean @@ -46,7 +46,8 @@ def waitForExit {cfg : IO.Process.StdioConfig} (child : IO.Process.Child cfg) (deadline : Nat) - : IO (Bool × UInt32) := do + : IO (Bool × UInt32) + := do match ← child.tryWait with | some exitCode => pure (false, exitCode) | none => @@ -66,7 +67,8 @@ def runUnsafe (problem : Problem) (limits : Limits) (command : Command) - : IO (Except Error Artifact) := do + : IO (Except Error Artifact) + := do let command := command.withStdinProblem let artifacts ← OATP.Artifacts.start s!"local {command.executable}" problem for run in artifacts do @@ -137,7 +139,8 @@ def run (problem : Problem) (limits : Limits) (command : Command) - : IO (Except Error Artifact) := do + : IO (Except Error Artifact) + := do try runUnsafe prover problem limits command catch error => diff --git a/OATP/Proof.lean b/OATP/Proof.lean index cdf99e9..fcb368b 100644 --- a/OATP/Proof.lean +++ b/OATP/Proof.lean @@ -29,13 +29,16 @@ inductive Step where | implicationIntro (localName : Name) (body : Step) deriving Repr -def stepNames : List String := +def stepNames + : List String + := ["true-intro", "exact", "and-left", "and-right", "and-intro", "implication-intro"] private def andParts (target : Expr) - : MetaM (Option (Expr × Expr)) := do + : MetaM (Option (Expr × Expr)) + := do match ← whnf target with | .app (.app (.const ``And _) left) right => pure (some (left, right)) | _ => pure none @@ -45,7 +48,8 @@ def projection (target : Expr) (localName : Name) (useLeft : Bool) - : MetaM (Except String Expr) := do + : MetaM (Except String Expr) + := do let hypothesis ← getFVarFromUserName localName match ← andParts (← inferType hypothesis) with | none => pure (.error s!"local hypothesis `{localName}` is not a conjunction") @@ -93,8 +97,11 @@ def build | .ok proof => pure (.ok (← mkLambdaFVars #[localVar] proof)) | _ => pure (.error "implication-intro requires an implication target") -def reconstruct (mvarId : MVarId) (step : Step) : - MetaM (Except String OATP.Lean.CheckedProof) := mvarId.withContext do +def reconstruct + (mvarId : MVarId) + (step : Step) + : MetaM (Except String OATP.Lean.CheckedProof) + := mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) match ← build target step with | .error message => pure (.error message) diff --git a/OATP/Properties/Basic.lean b/OATP/Properties/Basic.lean index 3479d9b..94995fe 100644 --- a/OATP/Properties/Basic.lean +++ b/OATP/Properties/Basic.lean @@ -13,11 +13,14 @@ namespace OATP.Properties open OATP OATP.TPTP -theorem empty_plain_render : OATP.Term.renderPlain #[] = "" := by +theorem empty_plain_render + : OATP.Term.renderPlain #[] = "" + := by rfl -theorem note_plain_render : - OATP.Term.renderPlain #[.note "ready"] = "note: ready" := by +theorem note_plain_render + : OATP.Term.renderPlain #[.note "ready"] = "note: ready" + := by rfl theorem goal_context_plain_render : diff --git a/OATP/Repl.lean b/OATP/Repl.lean index d917128..8dfeb7a 100644 --- a/OATP/Repl.lean +++ b/OATP/Repl.lean @@ -27,7 +27,9 @@ open OATP.TPTP open _root_.Argus open _root_.Grip -def helpTopics : List String := +def helpTopics + : List String + := ["cnf", "fof", "tff", "lean", "run", "context", "grammar", "roles"] def grammarTopics : List String := OATP.TPTP.supportedTheories @@ -43,7 +45,9 @@ def completionParam := Param.named typeName (Param.enum (values.map fun value => (value, value))) -def contextIndexParam : Param Nat := +def contextIndexParam + : Param Nat + := Param.ofParser "INDEX" (GParser.seqR (GParser.optional (GParser.ch '#')) GParser.nat) def staticCompletionValues @@ -302,7 +306,9 @@ def textSpec (Spec.arg name help (Param.named name Param.str)) (Spec.many (Spec.arg name help (Param.named name Param.str)))) -def commandSpec : Argus.Command Command := +def commandSpec + : Argus.Command Command + := Argus.group "oatp" [ Argus.cmd "help" (Spec.map Command.help (Spec.opt (Spec.arg "TOPIC" "Help topic" (Param.named "TOPIC" Param.str)))) @@ -443,7 +449,10 @@ def parseCommandSpec | [] => "" .error (message ++ hint) -private def commandChildren : List (Argus.Command Command) := +private +def commandChildren + : List (Argus.Command Command) + := match commandSpec.body with | .subs children => children | .opts _ => [] @@ -479,7 +488,9 @@ def usageLine output ++ if optional then " [" ++ value ++ "]" else " " ++ value) "" command.name ++ flags ++ arguments -def commandHelpText : String := +def commandHelpText + : String + := String.intercalate "\n" <| ["OATP REPL commands"] ++ commandChildren.map fun command => " /" ++ usageLine command ++ " " ++ command.description @@ -501,10 +512,15 @@ def parseInput else .source source -def helpText : String := +def helpText + : String + := commandHelpText -private def cnfHelp : String := +private +def cnfHelp + : String + := String.intercalate "\n" [ "CNF — clause normal form", "statement: cnf(NAME, ROLE, CLAUSE).", @@ -524,7 +540,10 @@ private def cnfHelp : String := " /state formulas /roles cnf /run --prover eprover" ] -private def fofHelp : String := +private +def fofHelp + : String + := String.intercalate "\n" [ "FOF — first-order formulas", "statement: fof(NAME, ROLE, FORMULA).", @@ -542,7 +561,10 @@ private def fofHelp : String := "use FOF when the problem needs implication, conjunction, or quantifiers" ] -private def tffHelp : String := +private +def tffHelp + : String + := String.intercalate "\n" [ "TFF — typed first-order formulas", "type: tff(nat_type, type, nat: $tType).", @@ -555,7 +577,10 @@ private def tffHelp : String := "TFF is parsed as TPTP input; use /state to inspect collected symbols" ] -private def grammarHelp : String := +private +def grammarHelp + : String + := String.intercalate "\n" [ "Grammar lookup", "/grammar cnf clause normal form", @@ -594,7 +619,10 @@ def roleHelp s!"Use /grammar {format} for the syntax." ] -private def leanHelp : String := +private +def leanHelp + : String + := String.intercalate "\n" [ "Lean bridge", "1. /goal p => p create a Lean goal", @@ -607,7 +635,10 @@ private def leanHelp : String := "example result: fun h => h : _fvar.1 → _fvar.1" ] -private def runHelp : String := +private +def runHelp + : String + := String.intercalate "\n" [ "Provers", "/run run the configured or first local prover", @@ -636,7 +667,10 @@ private def runHelp : String := " /local vampire -- --mode casc" ] -private def contextHelp : String := +private +def contextHelp + : String + := String.intercalate "\n" [ "Context drawer", "/state [TARGET] open context or focus a box", diff --git a/OATP/Repl/Context.lean b/OATP/Repl/Context.lean index 7a1cf10..0bbcd18 100644 --- a/OATP/Repl/Context.lean +++ b/OATP/Repl/Context.lean @@ -233,7 +233,8 @@ def validateDocument private def parseDocument (source : String) - : Except String _root_.TPTP.Document := do + : Except String _root_.TPTP.Document + := do match OATP.TPTP.parse source with | .error error => .error (error.pretty source.toUTF8) | .ok document => @@ -282,7 +283,8 @@ def removeContext private def singleStatement (source : String) - : Except String _root_.TPTP.Statement := do + : Except String _root_.TPTP.Statement + := do let document ← parseDocument source match document.items.toList with | [.statement statement] => pure statement @@ -294,7 +296,8 @@ def updateContext (input : String) (index : Nat) (source : String) - : Except String Session := do + : Except String Session + := do let statement ← singleStatement source match session.context.find? (·.id == index) with | some item => diff --git a/OATP/ReplView.lean b/OATP/ReplView.lean index cec163d..d72e882 100644 --- a/OATP/ReplView.lean +++ b/OATP/ReplView.lean @@ -35,7 +35,9 @@ open scoped TermColor.Style def version : String := OATP.version -def aurora : ColorScheme where +def aurora + : ColorScheme + where background := .rgb 13 24 37 foreground := .rgb 225 241 245 selection := .rgb 39 70 83 @@ -49,7 +51,9 @@ def aurora : ColorScheme where purple := .rgb 178 146 255 pink := .rgb 245 132 203 -def themes : List (String × ColorScheme) := +def themes + : List (String × ColorScheme) + := [("aurora", aurora), ("terracotta", { background := .rgb 26 28 38 foreground := .rgb 214 216 226 @@ -167,7 +171,9 @@ def appBinding label := String.intercalate "/" (keys.map Keymap.keyLabel) description } -def appBindings : List (BindingSpec AppKeyAction) := +def appBindings + : List (BindingSpec AppKeyAction) + := [ appBinding [.ctrl 'R', .ctrl 'r'] .toggleRun none "toggle the run drawer" , appBinding [.ctrl 'H', .ctrl 'h'] .toggleHistory none "toggle the history drawer" , appBinding [.ctrl 'S', .ctrl 's'] .toggleState none "toggle the state drawer" @@ -275,7 +281,9 @@ inductive ContextTarget where namespace ContextTarget -def all : List ContextTarget := +def all + : List ContextTarget + := [.formulas, .symbols, .problem, .goal, .translation, .term] def name @@ -369,7 +377,9 @@ def fallbackSize : Size := { columns := 110, rows := 28 } def inputConfig : TextInputConfig := { width := 160, maxLength := 16_384 } -def multilineConfig : MultilineConfig := +def multilineConfig + : MultilineConfig + := { text := inputConfig, lineBreak := .ctrl 'n' } private def minFrameWidth : Nat := 34 @@ -447,7 +457,10 @@ def dimText { segments := text.segments.map fun segment => { segment with style := Style.dim <+> segment.style } } -private def base64Alphabet : String := +private +def base64Alphabet + : String + := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/" private @@ -728,7 +741,8 @@ def reportWidget (symbols : Array Symbol) (width : Nat) (entry : TranscriptEntry) - : Option CollapsibleRender := do + : Option CollapsibleRender + := do let report ← entry.report pure <| renderCollapsible (reportWidgetConfig scheme) (max 1 (width - 2)) (reportSummary scheme report) (reportBody scheme symbols width entry report) @@ -1188,7 +1202,9 @@ def toggleFocusedProver { updated with statusNotice := some s!"{ProverReference.display reference} { if enabled then "disabled" else "enabled"}" } -def contextTargetNames : List String := +def contextTargetNames + : List String + := ContextTarget.all.map ContextTarget.name def contextTargetOfString diff --git a/OATP/Runtime.lean b/OATP/Runtime.lean index c607340..21d944c 100644 --- a/OATP/Runtime.lean +++ b/OATP/Runtime.lean @@ -26,7 +26,8 @@ inductive CatalogueCache where def readProblem (path : String) - : IO Problem := do + : IO Problem + := do pure { name := path, source := ← IO.FS.readFile path } def defaultLocalProverCandidates : Array String := #["eprover", "vampire", "metis"] @@ -37,7 +38,9 @@ def doctorTimeoutSeconds : Nat := 5 def doctorMaxOutputBytes : Nat := 1024 * 1024 -def localProverCandidates : IO (Array String) := do +def localProverCandidates + : IO (Array String) + := do match ← IO.getEnv "OATP_LOCAL_PROVERS" with | some value => pure <| value.splitOn "," |>.map (·.trimAscii.toString) |>.filter (!·.isEmpty) |>.toArray @@ -45,7 +48,8 @@ def localProverCandidates : IO (Array String) := do def catalogueLocation (cacheNamespace endpoint : String) - : IO (Option (System.FilePath × System.FilePath)) := do + : IO (Option (System.FilePath × System.FilePath)) + := do let root ← match ← IO.getEnv "XDG_CACHE_HOME" with | some path => pure (some (⟨path⟩ : System.FilePath)) | none => match ← IO.getEnv "HOME" with @@ -75,7 +79,8 @@ def fetchCatalogue (endpoint : String) (location : Option (System.FilePath × System.FilePath)) (writeCache : Bool) - : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do + : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) + := do match ← SystemOnTPTP.fetchCatalogue endpoint with | .error error => pure (.error (httpErrorMessage error)) | .ok response => @@ -97,7 +102,8 @@ def fetchCatalogue def loadCatalogue (cacheNamespace endpoint : String) (mode : CatalogueCache) - : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do + : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) + := do let location ← catalogueLocation cacheNamespace endpoint match mode with | .normal => @@ -113,7 +119,9 @@ def loadCatalogue | .refresh => fetchCatalogue endpoint location true | .noCache => fetchCatalogue endpoint none false -def installedProvers : IO (Array String) := do +def installedProvers + : IO (Array String) + := do let mut found := #[] for executable in ← localProverCandidates do if (← Http.commandVersion executable).isSome then @@ -124,7 +132,8 @@ def resolveOnline (toolName : String) (systems : Array SystemOnTPTP.Catalogue.SystemInfo) (references : List String) - : Except String (Array SystemOnTPTP.Catalogue.SystemInfo) := do + : Except String (Array SystemOnTPTP.Catalogue.SystemInfo) + := do let resolved ← references.mapM fun reference => match SystemOnTPTP.Catalogue.resolve systems reference with | some system => pure system diff --git a/OATP/SystemOnTPTP.lean b/OATP/SystemOnTPTP.lean index c5959a5..6ed8571 100644 --- a/OATP/SystemOnTPTP.lean +++ b/OATP/SystemOnTPTP.lean @@ -63,16 +63,28 @@ private inductive HtmlPart where open Grip GParser -private def htmlTag : GParser conditional HtmlPart := +private +def htmlTag + : GParser conditional HtmlPart + := HtmlPart.tag <$> GParser.capture (GParser.ch '<' *> GParser.takeWhile (· != 62) <* GParser.ch '>') -private def htmlText : GParser conditional HtmlPart := +private +def htmlText + : GParser conditional HtmlPart + := HtmlPart.text <$> GParser.capture (GParser.takeWhile1 (· != 60)) -private def htmlPart : GParser conditional HtmlPart := +private +def htmlPart + : GParser conditional HtmlPart + := GParser.chooseG htmlTag [htmlText] -private def htmlDocument : Grip.Parser (List HtmlPart) := +private +def htmlDocument + : Grip.Parser (List HtmlPart) + := GParser.seqL (GParser.many htmlPart) GParser.eof private @@ -234,7 +246,8 @@ def request def submit (config : Config) (problem : Problem) - : IO (Except Http.Error Http.Response) := do + : IO (Except Http.Error Http.Response) + := do let label := String.intercalate ", " (labels config).toList let request := request config problem let artifacts ← OATP.Artifacts.start s!"online {label}" problem @@ -331,7 +344,8 @@ def parseResponse (config : Config) (problem : Problem) (response : Http.Response) - : Except ResponseError Artifact := do + : Except ResponseError Artifact + := do if response.statusCode < 200 || response.statusCode ≥ 300 then throw (.httpStatus response.statusCode) let token ← match SZSStatus.tokenFromOutput response.body with diff --git a/OATP/TPTP.lean b/OATP/TPTP.lean index 43bc99e..f646783 100644 --- a/OATP/TPTP.lean +++ b/OATP/TPTP.lean @@ -72,7 +72,8 @@ def ofFof (name : String) (role : Role) (formula : _root_.TPTP.Formula.Expr) - : Except String _root_.TPTP.Statement := do + : Except String _root_.TPTP.Statement + := do let formula ← formula.toTPTP pure { kind := .fof diff --git a/OATP/Translate.lean b/OATP/Translate.lean index 866b49c..c367074 100644 --- a/OATP/Translate.lean +++ b/OATP/Translate.lean @@ -48,7 +48,8 @@ def symbolName private def unsupported (expression : Expr) - : MetaM (Except String TPTP.Formula.Expr) := do + : MetaM (Except String TPTP.Formula.Expr) + := do let rendered ← ppExpr expression pure <| Except.error (s!"unsupported Lean proposition `{rendered}`; supported fragment is " ++ "propositional logic over named atoms") @@ -59,7 +60,8 @@ private partial def translateProp (expression : Expr) - : MetaM (Except String TPTP.Formula.Expr) := do + : MetaM (Except String TPTP.Formula.Expr) + := do let expression ← instantiateMVars expression let (function, arguments) := expression.getAppFnArgs if function == ``True && arguments.isEmpty then @@ -104,7 +106,8 @@ def renderStatement (name : String) (role : _root_.TPTP.Role) (formula : TPTP.Formula.Expr) - : Except String String := do + : Except String String + := do let statement ← OATP.TPTP.Statement.ofFof name role formula pure <| _root_.TPTP.Statement.render statement diff --git a/examples/Cli.lean b/examples/Cli.lean index 6fb8702..594c1b2 100644 --- a/examples/Cli.lean +++ b/examples/Cli.lean @@ -25,7 +25,10 @@ structure CliIdentity where version : String endpoint : String -private def cliIdentity : IO CliIdentity := do +private +def cliIdentity + : IO CliIdentity + := do let executable ← Std.IO.Process.getExecutablePath let executableName := executable.fileName.getD "tool" pure { @@ -63,7 +66,10 @@ inductive ConfigAction where | show | path -private def configActionParam : Param ConfigAction := +private +def configActionParam + : Param ConfigAction + := Param.named "ACTION" (Param.enum [("show", .show), ("path", .path)]) inductive Action where @@ -103,7 +109,8 @@ private def doctorPalette : ColorScheme := ColorScheme.catppuccin private def doctorSection (title : String) - : IO Unit := do + : IO Unit + := do writeTextLine Text.empty writeTextLine (Text.styled title (Style.bold <+> Style.fg doctorPalette.purple)) @@ -111,7 +118,8 @@ private def doctorRow (label value : String) (ok : Bool) - : IO Unit := do + : IO Unit + := do let marker := if ok then Text.styled "✓" (Style.bold <+> Style.fg doctorPalette.green) else @@ -125,12 +133,16 @@ def doctorRow private def doctorTool (command : String) - : IO Unit := do + : IO Unit + := do match ← Http.commandVersion command with | some version => doctorRow command version true | none => doctorRow command "not found" false -private def doctorPlatform : IO String := do +private +def doctorPlatform + : IO String + := do try let output ← IO.Process.output { cmd := "uname", args := #["-s", "-m"] } if output.exitCode == 0 then @@ -236,7 +248,8 @@ private def doctorIssueFile : String := "oatp-doctor-issues.txt" private def writeDoctorIssues (issues : List DoctorIssue) - : IO (Option String) := do + : IO (Option String) + := do let entries := issues.map fun issue => s!"[{doctorIssueKindLabel issue.kind}] {issue.prover}\n{issue.detail}" try @@ -248,7 +261,8 @@ def writeDoctorIssues private def printDiagnostic (message : String) - : IO UInt32 := do + : IO UInt32 + := do let stderr ← IO.getStderr let target ← TermColor.targetWithTty .auto (← stderr.isTty) let report := (Report.error "command failed").withCode "cli" @@ -280,7 +294,8 @@ private def runConfig (identity : CliIdentity) (action : ConfigAction) - : IO UInt32 := do + : IO UInt32 + := do match action with | .path => match ← OATP.Config.path with @@ -317,7 +332,8 @@ def progressLoop (config : Widgets.ProgressConfig) (state : Widgets.IndeterminateProgressState) (region : LiveRegion) - : IO Unit := do + : IO Unit + := do if ← finished.get then let _ ← region.finish pure () @@ -332,7 +348,8 @@ def withProgress {α : Type} (label : String) (action : IO α) - : IO α := do + : IO α + := do if !(← stdoutSupportsControl) then return ← action withHiddenCursor do @@ -352,7 +369,8 @@ def withProgress private def showArtifact (artifact : Artifact) - : IO UInt32 := do + : IO UInt32 + := do let marker := if SZSStatus.isSuccess artifact.status then "✓" else "!" IO.eprintln s!"{marker} {artifact.prover.label}: {artifact.status} ({artifact.elapsedMs}ms)" unless artifact.stdout.isEmpty || artifact.stdout.trimAscii.toString.startsWith " printDiagnostic (processErrorMessage toolName options.executable error) catch error => printDiagnostic s!"could not read problem: {error}" -private def noLocalProverMessage : IO String := do +private +def noLocalProverMessage + : IO String + := do let candidates ← localProverCandidates pure <| s!"no local ATP found; tried {String.intercalate ", " candidates.toList}. " ++ "Install one, pass --prover PATH, or explicitly select an online-* prover" @@ -452,7 +474,8 @@ def portfolioProgressLoop (results : IO.Ref (List Portfolio.Result)) (region : IO.Ref LiveRegion) (total : Nat) - : IO Unit := do + : IO Unit + := do if ← finished.get then pure () else @@ -471,7 +494,8 @@ def withPortfolioProgress {α : Type} (total : Nat) (action : (Portfolio.Result → IO Unit) → IO α) - : IO α := do + : IO α + := do if !(← stdoutSupportsControl) then return ← action (fun _ => pure ()) withHiddenCursor do @@ -504,7 +528,8 @@ private def runDoctorOnline (identity : CliIdentity) (transports : Array String) - : IO Bool := do + : IO Bool + := do doctorSection "ONLINE ATP (probe)" if transports.isEmpty then doctorRow "service" "unavailable (no HTTP transport)" false @@ -538,7 +563,8 @@ def runDoctorOnline private def runDoctor (identity : CliIdentity) - : IO UInt32 := do + : IO UInt32 + := do let transports ← Http.availableTransports let (online, ready) := if transports.contains "curl" then @@ -569,7 +595,8 @@ private def runPortfolio (problem : Problem) (attempts : Array Portfolio.Attempt) - : IO UInt32 := do + : IO UInt32 + := do let results ← withPortfolioProgress attempts.size fun onResult => Portfolio.runWith problem attempts onResult let mut success := false @@ -581,7 +608,8 @@ private def runDefault (identity : CliIdentity) (options : RunOptions) - : IO UInt32 := do + : IO UInt32 + := do try let problem ← readProblem options.problem let rawReferences ← if options.provers.isEmpty then @@ -647,7 +675,8 @@ private def runSystems (identity : CliIdentity) (options : SystemsOptions) - : IO UInt32 := do + : IO UInt32 + := do writeTextLine (Text.styled s!"{identity.name} systems {identity.version}" (Style.bold <+> Style.fg doctorPalette.purple)) writeTextLine (Text.styled "LOCAL" (Style.bold <+> Style.fg doctorPalette.cyan)) @@ -687,7 +716,8 @@ def submitOnline (problem : Problem) (endpoint : String) (system : SystemOnTPTP.Catalogue.SystemInfo) - : IO UInt32 := do + : IO UInt32 + := do let config : SystemOnTPTP.Config := { systemLabel := system.id systemCommands := if system.command.isEmpty then #[] else #[(system.id, system.command)] @@ -708,7 +738,8 @@ private def runOnline (identity : CliIdentity) (options : OnlineOptions) - : IO UInt32 := do + : IO UInt32 + := do try let problem ← readProblem options.problem let endpoint := options.remote.endpoint.getD identity.endpoint @@ -725,7 +756,8 @@ def runOnline def main (argv : List String) - : IO UInt32 := do + : IO UInt32 + := do if let "repl" :: replArgs := argv then return ← oatpReplMain replArgs let identity ← cliIdentity diff --git a/examples/Demo.lean b/examples/Demo.lean index 28a80a8..6ab56ef 100644 --- a/examples/Demo.lean +++ b/examples/Demo.lean @@ -20,7 +20,9 @@ def sampleEvents : Array SearchEvent := #[ elapsedMs := 8 })] -def main : IO Unit := do +def main + : IO Unit + := do IO.println (OATP.Term.renderPlain sampleEvents) IO.println "" IO.print (OATP.Term.renderAnsi16 sampleEvents) diff --git a/examples/ProofDemo.lean b/examples/ProofDemo.lean index 5305814..b3d3d19 100644 --- a/examples/ProofDemo.lean +++ b/examples/ProofDemo.lean @@ -12,7 +12,10 @@ def demoP : Prop := True def demoQ : Prop := True def demoPredicate (_ : Nat) : Prop := True -private def runProofDemo : TermElabM Unit := do +private +def runProofDemo + : TermElabM Unit + := do let goal ← mkFreshExprMVar (some (mkConst ``True)) match ← OATP.Proof.reconstruct goal.mvarId! .trueIntro with | .ok _ => logInfo "OATP proof demo: kernel-checked True introduction" @@ -68,6 +71,8 @@ meta def elabOATPProofDemo : CommandElab := fun stx => #oatp_proof_demo -def main : IO UInt32 := do +def main + : IO UInt32 + := do IO.println "OATP proof demo passed" return 0 diff --git a/examples/Repl.lean b/examples/Repl.lean index f8fff40..19d19b4 100644 --- a/examples/Repl.lean +++ b/examples/Repl.lean @@ -272,7 +272,8 @@ private def publishRunRows (app : App) (rows : Array RunRow) - : IO Unit := do + : IO Unit + := do match app.runProgress with | some progress => progress.set rows | none => pure () @@ -280,7 +281,8 @@ def publishRunRows private def currentRunRows (app : App) - : IO (Array RunRow) := do + : IO (Array RunRow) + := do match app.runProgress with | some progress => progress.get | none => pure app.runRows @@ -321,7 +323,8 @@ def configProverName private def configOutput (app : App) - : IO (String × Report) := do + : IO (String × Report) + := do let path := (← OATP.Config.path).map (fun value => s!"{value}") |>.getD "unavailable" let (_, warning) ← OATP.Config.load let current := preferences app @@ -361,7 +364,8 @@ def configOutput private def savePreferences (before after : App) - : IO App := do + : IO App + := do if preferences before == preferences after then pure after else @@ -369,17 +373,26 @@ def savePreferences | none => pure after | some message => pure { after with statusNotice := some message } -private def installedProverReferences : IO (Array OATP.ProverReference) := do +private +def installedProverReferences + : IO (Array OATP.ProverReference) + := do let installed ← OATP.Runtime.installedProvers pure (installed.map OATP.ProverReference.fromLocal) -private def onlineProverNames : IO (Except String (Array OATP.ProverReference)) := do +private +def onlineProverNames + : IO (Except String (Array OATP.ProverReference)) + := do match ← OATP.Runtime.loadCatalogue catalogueNamespace SystemOnTPTP.defaultCatalogueEndpoint .normal with | .error message => pure (.error message) | .ok systems => pure (.ok (systems.map fun system => OATP.ProverReference.fromOnline system.id)) -private def selectableProvers : IO (Array OATP.ProverReference × Option String) := do +private +def selectableProvers + : IO (Array OATP.ProverReference × Option String) + := do let installed ← installedProverReferences match ← onlineProverNames with | .ok online => pure (installed ++ online, none) @@ -388,7 +401,8 @@ private def selectableProvers : IO (Array OATP.ProverReference × Option String) private def defaultProvers (app : App) - : IO (Array OATP.ProverReference) := do + : IO (Array OATP.ProverReference) + := do let installed ← installedProverReferences match app.defaultProver with | some reference => match reference.kind with @@ -405,7 +419,8 @@ private def selectedProvers (app : App) (all includeDefault : Bool := false) - : IO (Array OATP.ProverReference) := do + : IO (Array OATP.ProverReference) + := do let installed ← installedProverReferences let selected ← if all then pure installed @@ -434,7 +449,8 @@ def runRequest (app : App) (request : OATP.Repl.RunRequest) (includeDefault : Bool := false) - : IO RunOutput := do + : IO RunOutput + := do match currentProblem app with | none => let message := @@ -587,7 +603,10 @@ def startingRunRows { name := OATP.ProverReference.display reference, status := .running } | .error _ => #[{ name := "run", status := .running }] -private def backgroundJobs : TermColor.Repl.Terminal.JobConfig App where +private +def backgroundJobs + : TermColor.Repl.Terminal.JobConfig App + where shouldRun := fun app input => !app.busy && backendLine input start := fun app input => { app with busy := true @@ -647,7 +666,8 @@ private def backgroundJobs : TermColor.Repl.Terminal.JobConfig App where private def systemsText (request : OATP.Repl.SystemsRequest) - : IO String := do + : IO String + := do let installed ← OATP.Runtime.installedProvers let lines := if installed.isEmpty then ["LOCAL: none"] else ["LOCAL:"] ++ installed.toList.map (fun prover => " " ++ prover) @@ -664,7 +684,10 @@ def systemsText pure <| String.intercalate "\n" (lines ++ ["ONLINE:"] ++ systems.toList.map (fun system => " " ++ SystemOnTPTP.onlineReference system.id)) -private def doctorText : IO String := do +private +def doctorText + : IO String + := do let transports ← Http.availableTransports let installed ← OATP.Runtime.installedProvers let platform ← try @@ -716,7 +739,8 @@ private def infoText (app : App) (query : String) - : IO (String × Bool) := do + : IO (String × Bool) + := do let installed ← OATP.Runtime.installedProvers let found := installed.filter (fuzzy query) if found.size == 1 then @@ -793,7 +817,8 @@ def parseStepTokens private def parseStep (source : String) - : Except String OATP.Proof.Step := do + : Except String OATP.Proof.Step + := do let (step, rest) ← parseStepTokens (OATP.Repl.splitWords source) match rest with | [] => pure step @@ -804,7 +829,8 @@ def submitGoal (app : App) (cell : Nat) (input formula : String) - : IO App := do + : IO App + := do let runtime ← match app.leanRuntime with | some runtime => pure runtime | none => OATP.Lean.Repl.create @@ -827,7 +853,8 @@ def submitTheoryFormula (cell : Nat) (input : String) (command : OATP.Repl.Command) - : IO (Option App) := do + : IO (Option App) + := do match command with | .axiom name formula | .conjecture name formula => let role := match command with | .axiom _ _ => "axiom" | _ => "conjecture" @@ -844,7 +871,8 @@ def submitLeanCommand (cell : Nat) (input : String) (command : OATP.Repl.Command) - : IO (Option App) := do + : IO (Option App) + := do match command with | .goal formula | .toLean formula => do return some (← submitGoal app cell input formula) @@ -892,7 +920,8 @@ def applyPureCommand (app : App) (cell : Nat) (input : String) - : IO App := do + : IO App + := do match OATP.Repl.apply app.session input with | .ok session => let app := if changesContext input then invalidateContext { app with session } @@ -909,7 +938,8 @@ def submitCommand (cell : Nat) (input : String) (command : OATP.Repl.Command) - : IO App := do + : IO App + := do match command with | .quit => pure { app with running := false } | .load path => do @@ -1061,7 +1091,8 @@ private def submitCore (app : App) (input : String) - : IO App := do + : IO App + := do let input := input.trimAscii.toString let cell := app.session.nextCell let firstWord := (OATP.Repl.splitWords input).headD "" @@ -1082,7 +1113,8 @@ private def submit (app : App) (input : String) - : IO App := do + : IO App + := do let started ← IO.monoMsNow let updated ← submitCore app input let updated := clearSelection updated @@ -1095,7 +1127,8 @@ def submit private def commandValues (typeName : String) - : IO (List String) := do + : IO (List String) + := do match typeName with | "TOPIC" => pure (List.eraseDups (OATP.Repl.helpTopics ++ OATP.Repl.commandNames)) | "FORMAT" | "THEORY" | "STEP" => @@ -1125,7 +1158,10 @@ def complete := completeCommandWith OATP.Repl.commandSpec commandValues input -private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where +private +def appKeymap + : TermColor.Repl.Terminal.AppKeymap App + where Action := AppKeyAction keymap := Keymap.fromSpecs appBindings contexts := fun app => @@ -1349,7 +1385,8 @@ private def reportTestApp : App := { private def interactive (initial : App) - : IO Unit := do + : IO Unit + := do withAlternateScreen do clearScreen TermColor.Repl.Terminal.run { @@ -1375,7 +1412,8 @@ private def runScript (app : App) (lines : List String) - : IO App := do + : IO App + := do let mut app := app for line in lines do if app.running then @@ -1386,14 +1424,18 @@ def runScript private def staticOutput (app : App) - : IO Unit := do + : IO Unit + := do for entry in app.entries.reverse do IO.println s!"[{entry.cell}] › {entry.input}" let timing := entry.elapsedMs.map (fun milliseconds => s!" ({formatElapsed milliseconds})") |>.getD "" IO.println s!" {(if entry.ok then "=" else "!")} {entry.output}{timing}" -private def usage : String := +private +def usage + : String + := "oatp repl — interactive theorem-proving workbench\n\n" ++ "usage:\n lake exe oatp repl\n lake exe oatp repl --script FILE\n\n" ++ "examples:\n /load problem.p\n /to-lean p => p\n /snapshot\n " ++ @@ -1410,7 +1452,8 @@ def scriptExitCode private def initialApp (runtime : OATP.Lean.Repl.Runtime) - : IO App := do + : IO App + := do let (prefs, warning) ← OATP.Config.load let runProgress ← IO.mkRef (#[] : Array RunRow) let scheme := themeByName prefs.theme |>.getD aurora @@ -1435,7 +1478,8 @@ def initialApp def oatpReplMain (args : List String) - : IO UInt32 := do + : IO UInt32 + := do if args == ["--help"] || args == ["-h"] then IO.println usage return 0 diff --git a/test/Tests.lean b/test/Tests.lean index 302755d..b68104d 100644 --- a/test/Tests.lean +++ b/test/Tests.lean @@ -254,13 +254,18 @@ open OATP OATP.TPTP { columns := 100, rows := 24 }).plainText.contains "state •" #guard (OATP.ReplView.screen { stateOpen := true, panelFocus := .drawer } { columns := 100, rows := 24 }).plainText.contains "state • active" -def completionApp : OATP.ReplView.App := +def completionApp + : OATP.ReplView.App + := { repl := { input := { value := "/st", cursor := 3 } completion := some { candidates := #[{ replacement := "/state" }] } } } #guard (OATP.ReplView.screen completionApp { columns := 100, rows := 24 }).plainText.contains "/state" #guard OATP.ReplView.formatElapsed 1_500 == "1.5 s" -private def timedEntry : OATP.ReplView.TranscriptEntry := +private +def timedEntry + : OATP.ReplView.TranscriptEntry + := { cell := 1 input := "/to-lean p => p" output := "goal created" @@ -268,7 +273,10 @@ private def timedEntry : OATP.ReplView.TranscriptEntry := #guard (OATP.ReplView.screen { entries := [timedEntry] } { columns := 100, rows := 24 }).plainText.contains "(12 ms)" -private def plainEntry : OATP.ReplView.TranscriptEntry := +private +def plainEntry + : OATP.ReplView.TranscriptEntry + := { cell := 1 input := "/to-lean p => p" output := "goal created" } @@ -390,7 +398,9 @@ private def plainEntry : OATP.ReplView.TranscriptEntry := | _ => false #guard (OATP.ReplView.clearSelection { selectionStart := some (1, 2), selectionEnd := some (3, 4) }).selectionStart.isNone -def main : IO UInt32 := do +def main + : IO UInt32 + := do let commandCompletions ← TermColor.Repl.completeCommand OATP.Repl.commandSpec { value := "/st", cursor := 3 } if !(commandCompletions.any (·.replacement == "/state")) then