Add setOptions to CommandOptions

Author: augustepoiroux

REPL/JSON.lean

@@ -22,6 +22,7 @@ structure CommandOptions where
   -/
   infotree : Option String
   incrementality : Option Bool := none -- whether to use incremental mode optimization
+  setOptions : Option Options := none
 
 /-- Run Lean commands.
 If `env = none`, starts a new session (in which you can use `import`).

REPL/Lean/InfoTree/ToJson.lean

@@ -125,4 +125,65 @@ partial def InfoTree.toJson (t : InfoTree) (ctx? : Option ContextInfo) : IO Json
      return Lean.toJson (InfoTree.HoleJson.mk (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty)
     else throw <| IO.userError "No `ContextInfo` available."
 
+instance : ToJson DataValue where
+  toJson (v : DataValue) : Json :=
+    match v with
+    | .ofString s => toJson s
+    | .ofBool b   => toJson b
+    | .ofName n   => toJson n
+    | .ofNat n    => toJson n
+    | .ofInt i    => toJson i
+    | .ofSyntax _ => "<syntax>" -- TODO: syntax to json
+
+instance KVMapToJson : ToJson KVMap where
+  toJson (m : KVMap) : Json :=
+    Json.mkObj <| m.entries.map fun (k, v) => (k.toString, toJson v)
+
+instance : ToJson Options where
+  toJson (opts : Options) : Json := KVMapToJson.toJson opts
+
+def arrStrToName (arr : Array String) : Name :=
+  if arr.isEmpty then Name.anonymous
+  else
+    arr.foldl (init := Name.anonymous) fun acc s =>
+      if s.isEmpty then acc
+      else acc.append (Name.mkSimple s)
+
+instance : FromJson DataValue where
+  fromJson? (j : Json) : Except String DataValue :=
+    match j with
+    | .str s => Except.ok <| DataValue.ofString s
+    | .bool b => Except.ok <| DataValue.ofBool b
+    | .num _ => match j.getNat? with
+      | Except.ok n => Except.ok <| DataValue.ofNat n
+      | Except.error _ => match j.getInt? with
+        | Except.ok i => Except.ok <| DataValue.ofInt i
+        | Except.error _ => Except.error "Invalid number format"
+    | .arr a => -- we parse array of strings as a Name
+      if a.all fun e => e.getStr? |>.isOk then
+        Except.ok <| DataValue.ofName (arrStrToName (a.map fun e => e.getStr?.toOption.getD ""))
+      else
+        Except.error "Unsupported JSON type for DataValue"
+    | _ => Except.error "Unsupported JSON type for DataValue"
+
+instance KVMapFromJson : FromJson KVMap where
+  fromJson? (j : Json) : Except String KVMap :=
+    match j with
+    | .arr a => do -- array of (Name × DataValue) pairs to be converted to KVMap
+      let entries: Array (Name × DataValue) ← a.mapM fun e => do
+        match e with
+        | .arr #[.arr k, v] => do
+          let kName ← (if k.all fun e => e.getStr? |>.isOk then
+            Except.ok <| (arrStrToName (k.map fun e => e.getStr?.toOption.getD ""))
+          else
+            Except.error "Expected array of strings for Name")
+          let vData ← fromJson? v
+          return (kName, vData)
+        | _ => Except.error "Expected array of pairs for KVMap"
+      Except.ok <| KVMap.mk entries.toList
+    | _ => Except.error "Expected JSON object for KVMap"
+
+instance : FromJson Options where
+  fromJson? (j : Json) : Except String Options := KVMapFromJson.fromJson? j
+
 end Lean.Elab

REPL/Main.lean

@@ -371,15 +371,16 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
 
   let (initialCmdState, incStates, messages) ← try
+    let opts := s.setOptions.getD {}
     if s.incrementality.getD false then
       let bestIncrementalState? ← findBestIncrementalState s.cmd s.env
-      let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache
+      let (initialCmdState, incStates, messages, headerCache) ← IO.processInput s.cmd initialCmdState? bestIncrementalState? (← get).headerCache opts
       -- Store the command text and incremental states for future reuse
       modify fun st => { st with headerCache := headerCache }
       recordCommandIncrementals s.cmd incStates s.env
       pure (initialCmdState, incStates, messages)
     else
-      let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {}
+      let (initialCmdState, incStates, messages, _) ← IO.processInput s.cmd initialCmdState? none {} opts
       pure (initialCmdState, incStates, messages)
   catch ex =>
     return .inr ⟨ex.toString⟩