[llm] playground for LLM-related interaction

src/ec.ml

@@ -535,34 +535,8 @@ let main () =
 
       end
 
-    | `Llm llmopts -> begin
-        let name = llmopts.llmo_input in
-
-        begin try
-          let ext = Filename.extension name in
-          ignore (EcLoader.getkind ext : EcLoader.kind)
-        with EcLoader.BadExtension ext ->
-          Format.eprintf "do not know what to do with %s@." ext;
-          exit 1
-        end;
-
-        let lastgoals = llmopts.llmo_lastgoals in
-        let terminal =
-          lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name))
-        in
-
-        { prvopts     = llmopts.llmo_provers
-        ; input       = Some name
-        ; terminal    = terminal
-        ; interactive = false
-        ; eco         = true
-        ; gccompact   = None
-        ; docgen      = false
-        ; outdirp     = None
-        ; upto        = llmopts.llmo_upto
-        ; trace       = None }
-
-      end
+    | `Llm llmopts ->
+        EcLlm.run ~relocdir ~boot:ldropts.ldro_boot llmopts
 
     | `Runtest _ ->
         (* Eagerly executed *)

src/ecCommands.ml

@@ -987,6 +987,69 @@ let push_context scope context =
     ct_stack   = context.ct_stack
       |> omap (fun st -> context.ct_current :: st); }
 
+(* -------------------------------------------------------------------- *)
+(* Rotate the focus of the currently active proof so that the goal at
+   1-based index [k] becomes the focused one. The change is persisted
+   in the context with a new uuid so UNDO/REVERT can roll it back.
+   Returns the new number of open goals on success, or an error
+   message on failure. *)
+let focus_goal (k : int) : (int, string) result =
+  match !context with
+  | None -> Error "no active context"
+  | Some ctxt ->
+    match EcScope.xgoal ctxt.ct_current with
+    | None -> Error "no active proof"
+    | Some puc ->
+      match puc.EcScope.puc_active with
+      | None -> Error "no active proof"
+      | Some (pac, pct) ->
+        match pac.EcScope.puc_jdg with
+        | EcScope.PSNoCheck -> Error "proof is in no-check mode"
+        | EcScope.PSCheck pf ->
+          let n = List.length (EcCoreGoal.all_hd_opened pf) in
+          if n = 0 then Error "no open goals"
+          else if k < 1 || k > n then
+            Error (Printf.sprintf
+              "focus: index %d out of range (1..%d)" k n)
+          else if k = 1 then Ok n
+          else begin
+            let pf = EcCoreGoal.rotate_focus k pf in
+            let pac = { pac with EcScope.puc_jdg = EcScope.PSCheck pf } in
+            let puc =
+              { puc with EcScope.puc_active = Some (pac, pct) } in
+            let scope = EcScope.set_xgoal ctxt.ct_current puc in
+            context := Some (push_context scope ctxt);
+            Ok n
+          end
+
+(* Disable bullet enforcement for REPL-driven phrases. Drops the global
+   pragma so newly-opened proofs have no bullet stack, and clears the
+   stack on any currently active proof so REPL phrases are not checked
+   against it. Idempotent. Does not advance the undo level. Returns
+   the stack that was in place (if any) at the moment the active
+   proof's bullets were first cleared; returns [None] on idempotent
+   calls (where the stack is already gone). Callers use the returned
+   stack to drive bullet-character selection in [COMMIT]. *)
+let disable_repl_bullets () : EcBullets.stack option =
+  pragma_strict_bullets false;
+  match !context with
+  | None -> None
+  | Some ctxt ->
+    match EcScope.xgoal ctxt.ct_current with
+    | None -> None
+    | Some puc ->
+      match puc.EcScope.puc_active with
+      | None -> None
+      | Some (pac, pct) ->
+        match pac.EcScope.puc_bullets with
+        | None -> None
+        | Some _ as prior ->
+          let pac = { pac with EcScope.puc_bullets = None } in
+          let puc = { puc with EcScope.puc_active = Some (pac, pct) } in
+          let scope = EcScope.set_xgoal ctxt.ct_current puc in
+          context := Some { ctxt with ct_current = scope };
+          prior
+
 (* -------------------------------------------------------------------- *)
 let initialize ~restart ~undo ~boot ~checkmode ~checkproof =
   assert (restart || EcUtils.is_none !context);
@@ -1127,8 +1190,39 @@ let pp_current_goal ?(all = false) stream =
   end
 
 (* -------------------------------------------------------------------- *)
+let in_proof () =
+  Option.is_some (S.xgoal (current ()))
+
+(* Return the list of open-goal handles at the top level of the active
+   proof, focused-first, or [] if no proof is active. *)
+let open_handles () : EcCoreGoal.handle list =
+  match S.xgoal (current ()) with
+  | Some { S.puc_active =
+             Some ({ S.puc_jdg = S.PSCheck pf }, _) } ->
+    EcCoreGoal.all_hd_opened pf
+  | _ -> []
+
+(* Direct DAG children of [h] in the active proof. [] if no proof. *)
+let children_of (h : EcCoreGoal.handle) : EcCoreGoal.handle list =
+  match S.xgoal (current ()) with
+  | Some { S.puc_active =
+             Some ({ S.puc_jdg = S.PSCheck pf }, _) } ->
+    EcCoreGoal.children_of_handle
+      (EcCoreGoal.proofenv_of_proof pf) h
+  | _ -> []
+
+(* Parent of [h] in the active proof's DAG, or [None] if [h] is the
+   root or no proof is active. *)
+let parent_of (h : EcCoreGoal.handle) : EcCoreGoal.handle option =
+  match S.xgoal (current ()) with
+  | Some { S.puc_active =
+             Some ({ S.puc_jdg = S.PSCheck pf }, _) } ->
+    EcCoreGoal.parent_of_handle
+      (EcCoreGoal.proofenv_of_proof pf) h
+  | _ -> None
+
 let pp_current_goal_or_noproof ?(all = false) stream =
-  if Option.is_some (S.xgoal (current ())) then
+  if in_proof () then
     pp_current_goal ~all stream
   else
     Format.fprintf stream "No active proof.@\n%!"
@@ -1166,3 +1260,34 @@ let pp_all_goals () =
   end
 
   | _ -> []
+
+(* -------------------------------------------------------------------- *)
+(* Render the open-subgoals tree. Each entry is (index, is_focused,
+   text). [index] is 1-based, [is_focused] marks the focused goal
+   (always at index 1 with EC's current focus model), and [text] is
+   either a one-line conclusion digest (when [~all = false]) or the
+   full goal body (when [~all = true]). *)
+let pp_tree ?(all = false) () : (int * bool * string) list =
+  let scope = current () in
+  match S.xgoal scope with
+  | Some { S.puc_active = Some ({ puc_jdg = S.PSCheck pf }, _) } -> begin
+    match EcCoreGoal.opened pf with
+    | None -> []
+    | Some _ ->
+      let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
+      let goals = EcCoreGoal.all_opened pf in
+      List.mapi (fun i { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } ->
+        let text =
+          if all then
+            let buf = Buffer.create 256 in
+            let hc  = (EcEnv.LDecl.tohyps g_hyps, g_concl) in
+            Format.fprintf
+              (Format.formatter_of_buffer buf)
+              "%a@?" (EcPrinting.pp_goal1 ppe) hc;
+            Buffer.contents buf
+          else
+            Format.asprintf "%a" (EcPrinting.pp_form ppe) g_concl
+        in
+        (i + 1, i = 0, text)) goals
+  end
+  | _ -> []

src/ecCommands.mli

@@ -64,6 +64,13 @@ val pp_current_goal : ?all:bool -> Format.formatter -> unit
 val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit
 val pp_maybe_current_goal : Format.formatter -> unit
 val pp_all_goals : unit -> string list
+val in_proof : unit -> bool
+val disable_repl_bullets : unit -> EcBullets.stack option
+val pp_tree : ?all:bool -> unit -> (int * bool * string) list
+val focus_goal : int -> (int, string) result
+val open_handles : unit -> EcCoreGoal.handle list
+val children_of : EcCoreGoal.handle -> EcCoreGoal.handle list
+val parent_of : EcCoreGoal.handle -> EcCoreGoal.handle option
 
 (* -------------------------------------------------------------------- *)
 val pragma_verbose : bool -> unit

src/ecCoreGoal.ml

@@ -132,9 +132,13 @@ type proof = {
 }
 
 and proofenv = {
-  pr_uid   : ID.id;          (* unique ID for this proof *)
-  pr_main  : ID.id;          (* top goal, contains the final result *)
-  pr_goals : goal ID.Map.t;  (* set of all goals, closed and opened *)
+  pr_uid    : ID.id;            (* unique ID for this proof *)
+  pr_main   : ID.id;            (* top goal, contains the final result *)
+  pr_goals  : goal ID.Map.t;    (* set of all goals, closed and opened *)
+  pr_parent : handle ID.Map.t;
+    (* For each non-root handle, the parent in the proof DAG: i.e.
+       the handle that was being worked on when this one was created
+       via [FApi.newgoal]. The root [pr_main] is absent. *)
 }
 
 and pregoal = {
@@ -459,17 +463,24 @@ module FApi = struct
     tcenv
 
   (* ------------------------------------------------------------------ *)
-  let pf_newgoal (pe : proofenv) ?vx hyps concl =
+  let pf_newgoal (pe : proofenv) ?parent ?vx hyps concl =
     let hid     = ID.gen () in
     let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; } in
     let goal    = { g_goal = pregoal; g_validation = vx; } in
-    let pe      = { pe with pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals; } in
+    let pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals in
+    let pr_parent =
+      match parent with
+      | None -> pe.pr_parent
+      | Some p -> ID.Map.add pregoal.g_uid p pe.pr_parent
+    in
+    let pe = { pe with pr_goals; pr_parent } in
       (pe, pregoal)
 
   (* ------------------------------------------------------------------ *)
   let newgoal (tc : tcenv) ?(hyps : LDecl.hyps option) (concl : form) =
     let hyps     = ofdfl (fun () -> tc_hyps tc) hyps in
-    let (pe, pg) = pf_newgoal (tc_penv tc) hyps concl in
+    let parent   = tc.tce_tcenv.tce_goal |> Option.map (fun g -> g.g_uid) in
+    let (pe, pg) = pf_newgoal (tc_penv tc) ?parent hyps concl in
 
     let tc = tc_update_tcenv (fun te -> { te with tce_penv = pe }) tc in
     let tc = { tc with tce_goals = tc.tce_goals @ [pg.g_uid] } in
@@ -992,9 +1003,10 @@ let start (hyps : LDecl.hyps) (goal : form) =
 
   let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; } in
   let goal = { g_goal = goal; g_validation = None; } in
-  let env  = { pr_uid   = uid;
-               pr_main  = hid;
-               pr_goals = ID.Map.singleton hid goal; } in
+  let env  = { pr_uid    = uid;
+               pr_main   = hid;
+               pr_goals  = ID.Map.singleton hid goal;
+               pr_parent = ID.Map.empty; } in
 
     { pr_env = env; pr_opened = [hid]; }
 
@@ -1016,6 +1028,33 @@ let all_opened (pf : proof) =
 (* -------------------------------------------------------------------- *)
 let closed (pf : proof) = List.is_empty pf.pr_opened
 
+(* -------------------------------------------------------------------- *)
+(* Direct children of [h] in the proof DAG, in creation order. This is
+   driven by [pr_parent], the explicit parent edge recorded by
+   [FApi.newgoal] at the moment each child handle is allocated. The
+   iteration order matches creation order because handles are
+   generated by a monotonic counter and [ID.Map] iterates by key. *)
+let children_of_handle (pe : proofenv) (h : handle) : handle list =
+  ID.Map.fold
+    (fun child parent acc ->
+      if eq_handle parent h then child :: acc else acc)
+    pe.pr_parent []
+  |> List.rev
+
+(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *)
+let parent_of_handle (pe : proofenv) (h : handle) : handle option =
+  ID.Map.find_opt h pe.pr_parent
+
+(* -------------------------------------------------------------------- *)
+let rotate_focus (k : int) (pf : proof) =
+  let n = List.length pf.pr_opened in
+  if k < 1 || k > n then
+    invalid_arg "EcCoreGoal.rotate_focus";
+  if k = 1 then pf
+  else
+    let pre, post = List.split_at (k - 1) pf.pr_opened in
+    { pf with pr_opened = post @ pre }
+
 (* -------------------------------------------------------------------- *)
 module Exn = struct
   let recast pe _hyps f x =

src/ecCoreGoal.mli

@@ -206,6 +206,18 @@ val all_opened : proof -> pregoal list
 (* Check if a proof is done *)
 val closed : proof -> bool
 
+(* Direct children of [h] in the proof DAG, in creation order. *)
+val children_of_handle : proofenv -> handle -> handle list
+
+(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *)
+val parent_of_handle : proofenv -> handle -> handle option
+
+(* Rotate the list of opened goals at the top level. [rotate_focus k pf]
+   makes the goal currently at 1-based index [k] the new focused goal,
+   preserving the cyclic order of the others. Raises [Invalid_argument]
+   if [k] is out of range. *)
+val rotate_focus : int -> proof -> proof
+
 (* -------------------------------------------------------------------- *)
 val tc_error :
      proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string