From 5d868ffe95a53a16b5372b822967592b35ebe562 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 26 May 2026 08:14:09 +0200 Subject: [PATCH 01/11] bullets: focusing operators behind +strict_bullets pragma When `pragma +strict_bullets` is set, the bullet tokens `-`, `+`, `*` (and their repeated forms `--`, `++`, `**`, ...) become Coq-style focusing operators: each phrase's bullet is checked against a per-proof stack so that a subgoal must be discharged before its sibling is addressed, and so that bullet characters identify nesting levels. The default behavior is unchanged: without the pragma, bullets remain pure decoration, preserving every existing proof script. Repeated bullet characters are emitted by the lexer as single PLUSn/MINUSn/STARn tokens (carrying their literal), which makes them usable both as deeper bullet levels and as user-defined binary operators (`op (--) ...`). The final sibling of a split point can be continued at the parent level without a bullet: when the previous sibling is closed and exactly one sibling remains, the inner frame pops automatically (and cascades through nested last-sibling frames). This keeps the standard phl idiom of long `seq N : ' chains flat instead of forcing ever-deeper indentation under a `+' for each continuation. Multi-way splits keep their enumeration discipline for all but the last subgoal. --- src/ecBullets.ml | 121 ++++++++++++++++++++++++++++++ src/ecBullets.mli | 44 +++++++++++ src/ecCommands.ml | 28 +++++-- src/ecLexer.mll | 15 ++++ src/ecParser.mly | 32 +++++--- src/ecParsetree.ml | 4 +- src/ecScope.ml | 47 ++++++++---- src/ecScope.mli | 13 +++- tests/bullets-basic.ec | 56 ++++++++++++++ tests/bullets-binop.ec | 21 ++++++ tests/bullets-deep.ec | 39 ++++++++++ tests/bullets-errors.ec | 39 ++++++++++ tests/bullets-implicit-reuse.ec | 41 ++++++++++ tests/bullets-last-fallthrough.ec | 65 ++++++++++++++++ tests/bullets-legacy.ec | 19 +++++ tests/bullets-naked-split.ec | 32 ++++++++ 16 files changed, 578 insertions(+), 38 deletions(-) create mode 100644 src/ecBullets.ml create mode 100644 src/ecBullets.mli create mode 100644 tests/bullets-basic.ec create mode 100644 tests/bullets-binop.ec create mode 100644 tests/bullets-deep.ec create mode 100644 tests/bullets-errors.ec create mode 100644 tests/bullets-implicit-reuse.ec create mode 100644 tests/bullets-last-fallthrough.ec create mode 100644 tests/bullets-legacy.ec create mode 100644 tests/bullets-naked-split.ec diff --git a/src/ecBullets.ml b/src/ecBullets.ml new file mode 100644 index 000000000..693abdd83 --- /dev/null +++ b/src/ecBullets.ml @@ -0,0 +1,121 @@ +(* -------------------------------------------------------------------- *) +open EcLocation + +(* -------------------------------------------------------------------- *) +type frame = { + bf_token : string; + bf_loc : EcLocation.t; + bf_floor : int; +} + +type stack = frame list + +type error = + | UnbulletedSplit of { opened : int; level : [`Top | `Frame of frame] } + | NoSubgoalToOpen of { token : string } + | OuterSkipsInner of { token : string; outer : frame; inner : frame } + | ReuseBeforeClosing of { token : string; frame : frame } + +exception BulletError of EcLocation.t option * error + +(* -------------------------------------------------------------------- *) +let pp_error fmt = function + | UnbulletedSplit { opened; level = `Top } -> + Format.fprintf fmt + "previous tactic left %d open subgoals at top level; the next \ + phrase needs a bullet to focus one of them" opened + | UnbulletedSplit { opened; level = `Frame f } -> + Format.fprintf fmt + "previous tactic left %d open subgoals at the bullet level \ + opened by `%s' at %s; the next phrase needs a bullet to \ + focus one of them" + opened f.bf_token (EcLocation.tostring f.bf_loc) + | NoSubgoalToOpen { token } -> + Format.fprintf fmt + "bullet `%s' opens a new subproof level but there are no \ + remaining subgoals" token + | OuterSkipsInner { token; outer; inner } -> + Format.fprintf fmt + "bullet `%s' (matches an outer level opened at %s) skips past \ + inner bullet `%s' opened at %s whose subproof is not closed" + token (EcLocation.tostring outer.bf_loc) + inner.bf_token (EcLocation.tostring inner.bf_loc) + | ReuseBeforeClosing { token; frame } -> + Format.fprintf fmt + "bullet `%s' reused but the previous subgoal (opened at %s) \ + is not closed" + token (EcLocation.tostring frame.bf_loc) + +(* -------------------------------------------------------------------- *) +let n_open (juc : EcCoreGoal.proof) = + List.length (EcCoreGoal.all_hd_opened juc) + +let raise_error ?loc err = raise (BulletError (loc, err)) + +(* -------------------------------------------------------------------- *) +(* Validate the bullet against the current stack and return the + pre-phrase stack. Each frame's [bf_floor] records the open-count + that should remain once the frame's subproof is fully closed; the + frame becomes poppable when [n_open <= bf_floor]. *) +let open_phrase ~(bullet : string located option) + (juc : EcCoreGoal.proof) (stack : stack) : stack = + let opened = n_open juc in + (* Top-of-stack floor, or 0 if the stack is empty (top-level: one + focused goal allowed without a bullet). A phrase may run + unbulleted iff [opened <= floor_top + 1]: the focused goal + plus the goals "outside" the current level. *) + let floor_top = + match stack with [] -> 0 | f :: _ -> f.bf_floor in + match bullet with + | None -> + if opened > floor_top + 1 then begin + let level = + match stack with [] -> `Top | f :: _ -> `Frame f in + raise_error (UnbulletedSplit { opened; level }) + end; + stack + | Some b -> + let tok = unloc b in + let loc = loc b in + (* Search the stack from innermost outward for a frame matching + [tok]. Inner frames not yet drained block the match. *) + let rec scan acc = function + | [] -> `Open + | f :: rest when f.bf_token = tok -> `Match (List.rev acc, f, rest) + | f :: rest -> scan (f :: acc) rest + in + match scan [] stack with + | `Open -> + if opened = 0 then + raise_error ~loc (NoSubgoalToOpen { token = tok }); + { bf_token = tok; bf_loc = loc; bf_floor = opened - 1 } :: stack + | `Match (inner, frame, outer) -> + (* Inner frames must already be drained. *) + List.iter (fun (f : frame) -> + if opened > f.bf_floor then + raise_error ~loc + (OuterSkipsInner { token = tok; outer = frame; inner = f })) + inner; + (* The matching frame's current slot must be closed. *) + if opened > frame.bf_floor then + raise_error ~loc (ReuseBeforeClosing { token = tok; frame }); + { frame with bf_loc = loc } :: outer + +(* After a phrase has run, pop frames whose subproof has fully + closed. Cascades through nested last-sibling frames; this is what + lets the last sibling at any level be addressed by an unbulleted + phrase. *) +let close_phrase (juc : EcCoreGoal.proof) (stack : stack) : stack = + let opened = n_open juc in + let rec pop = function + | f :: rest when opened <= f.bf_floor -> pop rest + | s -> s + in + pop stack + +(* -------------------------------------------------------------------- *) +let pp_exn fmt = function + | BulletError (_, err) -> pp_error fmt err + | exn -> raise exn + +let () = EcPException.register pp_exn diff --git a/src/ecBullets.mli b/src/ecBullets.mli new file mode 100644 index 000000000..0b7d4a1ff --- /dev/null +++ b/src/ecBullets.mli @@ -0,0 +1,44 @@ +(* -------------------------------------------------------------------- *) +(* Bullet-stack management for [+strict_bullets]. A frame is pushed + on the stack each time the user opens a new bullet level, and + popped after a phrase whose subproof has fully closed (cascading + through nested last-sibling frames). *) + +open EcLocation + +(* A single bullet frame: the token that opened it (e.g. "-", "++"), + the location of that opening, and the open-goal count that should + remain once this frame's subproof is fully discharged. *) +type frame = private { + bf_token : string; + bf_loc : EcLocation.t; + bf_floor : int; +} + +type stack = frame list + +(* Structured description of every way a strict-bullet check can + fail. Each constructor carries enough context for diagnostics + without forcing the caller to pattern-match on rendered strings. *) +type error = + | UnbulletedSplit of { opened : int; level : [`Top | `Frame of frame] } + | NoSubgoalToOpen of { token : string } + | OuterSkipsInner of { token : string; outer : frame; inner : frame } + | ReuseBeforeClosing of { token : string; frame : frame } + +exception BulletError of EcLocation.t option * error + +val pp_error : Format.formatter -> error -> unit + +(* Validate the optional bullet on the next phrase against [stack], + returning the stack to install for that phrase. May raise + [BulletError]. *) +val open_phrase : + bullet:(string located) option + -> EcCoreGoal.proof + -> stack + -> stack + +(* Pop frames whose subproof has fully closed after the last phrase. + Cascades through nested last-sibling frames. *) +val close_phrase : EcCoreGoal.proof -> stack -> stack diff --git a/src/ecCommands.ml b/src/ecCommands.ml index e90518ff0..08f801623 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -15,6 +15,7 @@ type pragma = { pm_g_prall : bool; (* true => display all open goals *) pm_g_prpo : EcPrinting.prpo_display; pm_check : [`Check | `WeakCheck | `Report]; + pm_strict_bullets : bool; (* true => bullets focus subgoals *) } let dpragma = { @@ -22,6 +23,7 @@ let dpragma = { pm_g_prall = false ; pm_g_prpo = EcPrinting.{ prpo_pr = false; prpo_po = false; }; pm_check = `Check; + pm_strict_bullets = false; } module Pragma : sig @@ -61,10 +63,15 @@ let pragma_g_po_display (b : bool) = let pragma_check mode = Pragma.upd (fun pragma -> { pragma with pm_check = mode; }) +let pragma_strict_bullets (b : bool) = + Pragma.upd (fun pragma -> { pragma with pm_strict_bullets = b; }) + module Pragmas = struct let silent = "silent" let verbose = "verbose" + let strict_bullets = "strict_bullets" + module Proofs = struct let check = "Proofs:check" let weak = "Proofs:weak" @@ -505,7 +512,9 @@ and process_abbrev (scope : EcScope.scope) (a : pabbrev located) = (* -------------------------------------------------------------------- *) and process_axiom ?(src : string option) (scope : EcScope.scope) (ax : paxiom located) = EcScope.check_state `InTop "axiom" scope; - let (name, scope) = EcScope.Ax.add ?src scope (Pragma.get ()).pm_check ax in + let pragma = Pragma.get () in + let strict = pragma.pm_strict_bullets in + let (name, scope) = EcScope.Ax.add ?src ~strict scope pragma.pm_check ax in name |> EcUtils.oiter (fun x -> match (unloc ax).pa_kind with @@ -635,8 +644,9 @@ and process_sct_close (scope : EcScope.scope) name = and process_tactics ?(src : string option) (scope : EcScope.scope) t = let mode = (Pragma.get ()).pm_check in match t with - | `Actual t -> snd (EcScope.Tactics.process ?src scope mode t) - | `Proof -> EcScope.Tactics.proof ?src scope + | `Actual (b, t) -> + snd (EcScope.Tactics.process ?src ?bullet:b scope mode t) + | `Proof -> EcScope.Tactics.proof ?src scope (* -------------------------------------------------------------------- *) (* Add and store src for proofs *) @@ -653,8 +663,9 @@ and process_save ?(src : string option) (scope : EcScope.scope) ed = (* -------------------------------------------------------------------- *) and process_realize (scope : EcScope.scope) pr = - let mode = (Pragma.get ()).pm_check in - let (name, scope) = EcScope.Ax.realize scope mode pr in + let pragma = Pragma.get () in + let strict = pragma.pm_strict_bullets in + let (name, scope) = EcScope.Ax.realize ~strict scope pragma.pm_check pr in name |> EcUtils.oiter (fun x -> EcScope.notify scope `Info "added lemma: `%s'" x); scope @@ -689,6 +700,9 @@ and process_option (scope : EcScope.scope) (name, value) = let gs = EcEnv.gstate (EcScope.env scope) in EcGState.setflag (unloc name) value gs; scope + | `Bool value when EcLocation.unloc name = Pragmas.strict_bullets -> + pragma_strict_bullets value; scope + | (`Int _) as value -> let gs = EcEnv.gstate (EcScope.env scope) in EcGState.setvalue (unloc name) value gs; scope @@ -716,14 +730,14 @@ and process_dump_why3 scope filename = EcScope.dump_why3 scope filename; scope (* -------------------------------------------------------------------- *) -and process_dump scope (source, tc) = +and process_dump scope (source, (bullet, tc)) = let open EcCoreGoal in let input, (p1, p2) = source.tcd_source in let goals, scope = let mode = (Pragma.get ()).pm_check in - EcScope.Tactics.process scope mode tc + EcScope.Tactics.process ?bullet scope mode tc in let wrerror fname = diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 704b0e976..52cc4860c 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -301,8 +301,23 @@ | '*' | '/' | '&' | '%' -> LOP3 (name |> odfl op) | _ -> LOP4 (name |> odfl op) + (* ------------------------------------------------------------------ *) + (* Repeated bullet characters (`--`, `+++`, `***`, ...) are emitted as + a single token so that the parser can distinguish them from two + separate operator characters. Single-character forms keep going + through the standard operator path for backward compatibility. *) + let lex_bullet_chunk (op : string) = + let n = String.length op in + if EcRegexp.match_ (`S "^-{2,}$" ) op then Some (MINUSn n) + else if EcRegexp.match_ (`S "^\\+{2,}$") op then Some (PLUSn n) + else if EcRegexp.match_ (`S "^\\*{2,}$") op then Some (STARn n) + else None + (* ------------------------------------------------------------------ *) let lex_operators (op : string) = + match lex_bullet_chunk op with + | Some tok -> [tok] + | None -> let baseop (op : string) = try fst (Hashtbl.find operators op) with Not_found -> diff --git a/src/ecParser.mly b/src/ecParser.mly index 117ccf9a1..05a2e7e26 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -599,6 +599,7 @@ %token WP %token ZETA %token NOP LOP1 ROP1 LOP2 ROP2 LOP3 ROP3 LOP4 ROP4 NUMOP +%token PLUSn MINUSn STARn %token LTCOLON DASHLT GT LT GE LE LTSTARGT LTLTSTARGT LTSTARGTGT %token FINAL %token DOCCOMMENT @@ -623,10 +624,10 @@ %left LOP1 %right ROP1 %right QUESTION -%left LOP2 MINUS PLUS PLUSGT +%left LOP2 MINUS PLUS PLUSGT MINUSn PLUSn %right ROP2 %right RARROW -%left LOP3 STAR SLASH +%left LOP3 STAR SLASH STARn %right ROP3 %left LOP4 AT AMP HAT BACKSLASH %right ROP4 @@ -829,10 +830,12 @@ inlinepat: | LE { "<=" } %inline uniop: -| x=NOP { Printf.sprintf "[%s]" x } -| NOT { "[!]" } -| PLUS { "[+]" } -| MINUS { "[-]" } +| x=NOP { Printf.sprintf "[%s]" x } +| NOT { "[!]" } +| PLUS { "[+]" } +| MINUS { "[-]" } +| n=PLUSn { Printf.sprintf "[%s]" (String.make n '+') } +| n=MINUSn { Printf.sprintf "[%s]" (String.make n '-') } %inline sbinop: | EQ { "=" } @@ -842,6 +845,9 @@ inlinepat: | STAR { "*" } | SLASH { "/" } | AT { "@" } +| n=PLUSn { String.make n '+' } +| n=MINUSn { String.make n '-' } +| n=STARn { String.make n '*' } | OR { "\\/" } | ORA { "||" } | AND { "/\\" } @@ -3583,11 +3589,17 @@ tactics0: | ts=tactics { Pseq ts } | x=loc(empty) { Pseq [mk_core_tactic (mk_loc x.pl_loc (Pidtac None))] } +%inline bullet: +| b=loc(MINUS) { mk_loc b.pl_loc "-" } +| b=loc(PLUS) { mk_loc b.pl_loc "+" } +| b=loc(STAR) { mk_loc b.pl_loc "*" } +| b=loc(MINUSn) { mk_loc b.pl_loc (String.make b.pl_desc '-') } +| b=loc(PLUSn) { mk_loc b.pl_loc (String.make b.pl_desc '+') } +| b=loc(STARn) { mk_loc b.pl_loc (String.make b.pl_desc '*') } + toptactic: -| PLUS t=tactics { t } -| STAR t=tactics { t } -| MINUS t=tactics { t } -| t=tactics { t } +| b=bullet t=tactics { (Some b, t) } +| t=tactics { (None, t) } tactics_or_prf: | t=toptactic { `Actual t } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 7d060227e..6b5884008 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1364,8 +1364,8 @@ type global_action = | GsctOpen of osymbol_r | GsctClose of osymbol_r | Grealize of prealize located - | Gtactics of [`Proof | `Actual of ptactic list] - | Gtcdump of (tcdump * ptactic list) + | Gtactics of [`Proof | `Actual of string located option * ptactic list] + | Gtcdump of (tcdump * (string located option * ptactic list)) | Gprover_info of pprover_infos | Gsave of save located | Gpragma of psymbol diff --git a/src/ecScope.ml b/src/ecScope.ml index c7cc2fbe6..0470176df 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -296,6 +296,10 @@ and proof_auc = { puc_jdg : proof_state; puc_flags : pucflags; puc_crt : EcDecl.axiom; + puc_bullets : EcBullets.stack option; + (* [None] when bullets are decoration only (legacy mode). + [Some stack] when [+strict_bullets] was active at proof + open; see [EcBullets] for the stack semantics. *) } and proof_ctxt = @@ -811,7 +815,8 @@ module Tactics = struct | Some src -> DocState.push_srcbl scope.sc_locdoc src | None -> scope.sc_locdoc; } - let process_r ?(src : string option) ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) = + let process_r ?(src : string option) ?(bullet : string located option) + ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) = check_state `InProof "proof script" scope; let scope = @@ -855,6 +860,12 @@ module Tactics = struct EcHiGoal.tt_redlogic = Options.get_redlogic scope; EcHiGoal.tt_und_delta = Options.get_und_delta scope; } in + let bullets = + try omap (EcBullets.open_phrase ~bullet juc) pac.puc_bullets + with EcBullets.BulletError (loc, err) -> + hierror ?loc "%a" EcBullets.pp_error err + in + let (hds, juc) = try TTC.process ttenv tac juc with EcCoreGoal.TcError tcerror -> @@ -868,7 +879,9 @@ module Tactics = struct let penv = EcCoreGoal.proofenv_of_proof juc in - let pac = { pac with puc_jdg = PSCheck juc } in + let bullets = omap (EcBullets.close_phrase juc) bullets in + + let pac = { pac with puc_jdg = PSCheck juc; puc_bullets = bullets } in let puc = { puc with puc_active = Some (pac, pct); } in let scope = { scope with sc_pr_uc = Some puc; } in Some (penv, hds), scope @@ -880,8 +893,9 @@ module Tactics = struct let ts = List.map (fun t -> { pt_core = t; pt_intros = []; }) ts in snd (process_r mark mode scope ts) - let process ?(src : string option) scope mode tac = - process_r ?src true mode scope tac + let process ?(src : string option) ?(bullet : string located option) + scope mode tac = + process_r ?src ?bullet true mode scope tac end (* -------------------------------------------------------------------- *) @@ -940,7 +954,7 @@ module Ax = struct sc_locdoc = DocState.add_item scope.sc_locdoc; } (* ------------------------------------------------------------------ *) - let start_lemma scope (cont, axflags) check ?name (axd, ctxt) = + let start_lemma ?(strict = false) scope (cont, axflags) check ?name (axd, ctxt) = let puc = match check with | false -> PSNoCheck @@ -955,7 +969,8 @@ module Ax = struct ; puc_started = false ; puc_jdg = puc ; puc_flags = axflags - ; puc_crt = axd } + ; puc_crt = axd + ; puc_bullets = if strict then Some [] else None } in { puc_active = Some (active, ctxt); puc_cont = cont; @@ -964,7 +979,7 @@ module Ax = struct { scope with sc_pr_uc = Some puc } (* ------------------------------------------------------------------ *) - let rec add_r (scope : scope) (mode : proofmode) (ax : paxiom located) = + let rec add_r ?(strict = false) (scope : scope) (mode : proofmode) (ax : paxiom located) = assert (scope.sc_pr_uc = None); let env = env scope in @@ -1024,13 +1039,13 @@ module Ax = struct match tc with | None -> let scope = - start_lemma scope ~name:(unloc ax.pa_name) + start_lemma ~strict scope ~name:(unloc ax.pa_name) pucflags check (axd, None) in let scope = snd (Tactics.process1_r false `Check scope tintro) in None, scope | Some tc -> - start_lemma_with_proof scope + start_lemma_with_proof ~strict scope (Some tintro) pucflags (mode, mk_loc loc tc) check ~name:(unloc ax.pa_name) axd end @@ -1104,10 +1119,10 @@ module Ax = struct (None, { scope with sc_env = puc.puc_init }) (* ------------------------------------------------------------------ *) - and start_lemma_with_proof scope tintro pucflags (mode, tc) check ?name axd = + and start_lemma_with_proof ?(strict = false) scope tintro pucflags (mode, tc) check ?name axd = let { pl_loc = loc; pl_desc = tc } = tc in - let scope = start_lemma scope pucflags check ?name (axd, None) in + let scope = start_lemma ~strict scope pucflags check ?name (axd, None) in let scope = tintro |> ofold (fun t sc -> snd (Tactics.process1_r false `Check sc t)) @@ -1170,7 +1185,7 @@ module Ax = struct snd (save_r ~mode:`Abort scope) (* ------------------------------------------------------------------ *) - let add ?(src : string option) (scope : scope) (mode : proofmode) (ax : paxiom located) = + let add ?(src : string option) ?(strict = false) (scope : scope) (mode : proofmode) (ax : paxiom located) = let uax = unloc ax in let kind = match uax.pa_kind with @@ -1192,10 +1207,10 @@ module Ax = struct | Some src -> DocState.push_srcbl scope.sc_locdoc src | None -> scope.sc_locdoc; } in - add_r scope mode ax + add_r ~strict scope mode ax (* ------------------------------------------------------------------ *) - let realize (scope : scope) (mode : proofmode) (rl : prealize located) = + let realize ?(strict = false) (scope : scope) (mode : proofmode) (rl : prealize located) = check_state `InProof "activate" scope; let loc = rl.pl_loc and rl = rl.pl_desc in @@ -1227,10 +1242,10 @@ module Ax = struct match rl.pr_proof with | None -> - None, start_lemma scope pucflags check ?name:axname (ax, Some st) + None, start_lemma ~strict scope pucflags check ?name:axname (ax, Some st) | Some tc -> - start_lemma_with_proof scope + start_lemma_with_proof ~strict scope None pucflags (mode, mk_loc loc tc) check ?name:axname ax end diff --git a/src/ecScope.mli b/src/ecScope.mli index 953041cc2..e4a8bff31 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -41,6 +41,10 @@ and proof_auc = { puc_jdg : proof_state; puc_flags : pucflags; puc_crt : EcDecl.axiom; + puc_bullets : EcBullets.stack option; + (* [None] when bullets are decoration only (legacy mode). + [Some stack] when [+strict_bullets] was active at proof + open; see [EcBullets] for the stack semantics. *) } and proof_ctxt = @@ -128,11 +132,11 @@ end module Ax : sig type proofmode = [`WeakCheck | `Check | `Report] - val add : ?src:string -> scope -> proofmode -> paxiom located -> symbol option * scope + val add : ?src:string -> ?strict:bool -> scope -> proofmode -> paxiom located -> symbol option * scope val save : ?src:string -> scope -> string option * scope val admit : ?src:string -> scope -> string option * scope val abort : ?src:string -> scope -> scope - val realize : scope -> proofmode -> prealize located -> symbol option * scope + val realize : ?strict:bool -> scope -> proofmode -> prealize located -> symbol option * scope end (* -------------------------------------------------------------------- *) @@ -231,7 +235,10 @@ module Tactics : sig type prinfos = proofenv * (handle * handle list) type proofmode = Ax.proofmode - val process : ?src:string -> scope -> proofmode -> ptactic list -> prinfos option * scope + val process : + ?src:string + -> ?bullet:string EcLocation.located + -> scope -> proofmode -> ptactic list -> prinfos option * scope val proof : ?src:string -> scope -> scope end diff --git a/tests/bullets-basic.ec b/tests/bullets-basic.ec new file mode 100644 index 000000000..e994e5721 --- /dev/null +++ b/tests/bullets-basic.ec @@ -0,0 +1,56 @@ +(* Bullets as focusing operators: basic usage. *) +require import AllCore. + +pragma +strict_bullets. + +(* Two subgoals, two bullets. *) +lemma split2 (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- exact hp. +- exact hq. +qed. + +(* Three subgoals at the same depth. *) +lemma split3 (p q r : bool) : p => q => r => p /\ q /\ r. +proof. +move=> hp hq hr; do! split. +- exact hp. +- exact hq. +- exact hr. +qed. + +(* Nested: outer `-`, inner `+`. *) +lemma nested (p q r s : bool) : + p => q => r => s => (p /\ q) /\ (r /\ s). +proof. +move=> hp hq hr hs; split. +- split. + + exact hp. + + exact hq. +- split. + + exact hr. + + exact hs. +qed. + +(* Three-deep nesting using `-`, `+`, `*`. *) +lemma deep (a b c d : bool) : + a => b => c => d => ((a /\ b) /\ c) /\ d. +proof. +move=> ha hb hc hd; split. +- split. + + split. + * exact ha. + * exact hb. + + exact hc. +- exact hd. +qed. + +(* No bullet between sub-tactics on the same goal works fine: tactics + chained with `;' inside one phrase don't trigger new bullet checks. *) +lemma chained (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- exact hp. +- exact hq. +qed. diff --git a/tests/bullets-binop.ec b/tests/bullets-binop.ec new file mode 100644 index 000000000..0cccbd4f7 --- /dev/null +++ b/tests/bullets-binop.ec @@ -0,0 +1,21 @@ +(* Multi-character bullet tokens (`--`, `++`, `**`) are also usable as + user-defined binary operator names. *) +require import AllCore. + +(* `--` as an integer binop. *) +op ( -- ) (a b : int) : int = a - b - 1. + +lemma minusminus_test : 5 -- 2 = 2. +proof. by rewrite /(--). qed. + +(* `++` as an integer binop. *) +op ( ++ ) (a b : int) : int = a + b + 1. + +lemma plusplus_test : 3 ++ 4 = 8. +proof. by rewrite /(++). qed. + +(* `**` as an integer binop. *) +op ( ** ) (a b : int) : int = a * b * 2. + +lemma starstar_test : 3 ** 4 = 24. +proof. by rewrite /( ** ). qed. diff --git a/tests/bullets-deep.ec b/tests/bullets-deep.ec new file mode 100644 index 000000000..108f54f3c --- /dev/null +++ b/tests/bullets-deep.ec @@ -0,0 +1,39 @@ +(* Multi-character bullets (`--`, `++`, etc.) for deeper nesting. *) +require import AllCore. + +pragma +strict_bullets. + +(* `--` opens a level distinct from `-`. *) +lemma deep2 (a b c d : bool) : + a => b => c => d => (a /\ b) /\ (c /\ d). +proof. +move=> ha hb hc hd; split. +- split. + -- exact ha. + -- exact hb. +- split. + -- exact hc. + -- exact hd. +qed. + +(* `+++` and `***` also work; characters and lengths can be combined. *) +lemma deep3 (a b c d e f g h : bool) : + a => b => c => d => e => f => g => h => + ((a /\ b) /\ (c /\ d)) /\ ((e /\ f) /\ (g /\ h)). +proof. +move=> ha hb hc hd he hf hg hh; split. +- split. + + split. + * exact ha. + * exact hb. + + split. + * exact hc. + * exact hd. +- split. + + split. + * exact he. + * exact hf. + + split. + * exact hg. + * exact hh. +qed. diff --git a/tests/bullets-errors.ec b/tests/bullets-errors.ec new file mode 100644 index 000000000..55cd2686a --- /dev/null +++ b/tests/bullets-errors.ec @@ -0,0 +1,39 @@ +(* Negative tests for strict bullets: each `fail …' phrase is expected + to error out; the surrounding proof must still finish cleanly. *) +require import AllCore. + +pragma +strict_bullets. + +(* Reusing a bullet before the previous subgoal is closed. *) +lemma reuse_not_closed (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- idtac. +fail - exact hp. +exact hp. +- exact hq. +qed. + +(* Using a bullet more times than there are sibling subgoals. *) +lemma too_many (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- exact hp. +- exact hq. +fail - exact hp. +qed. + +(* Outer bullet reused while an inner bullet level still has open + subgoals. *) +lemma wrong_skip (p q r s : bool) : + p => q => r => s => (p /\ q) /\ (r /\ s). +proof. +move=> hp hq hr hs; split. +- split. + + exact hp. +fail - split. + + exact hq. +- split. + + exact hr. + + exact hs. +qed. diff --git a/tests/bullets-implicit-reuse.ec b/tests/bullets-implicit-reuse.ec new file mode 100644 index 000000000..9480cce4b --- /dev/null +++ b/tests/bullets-implicit-reuse.ec @@ -0,0 +1,41 @@ +(* Regression: after an implicit last sibling closes an inner frame, + the bullet character used inside that frame must be free to reuse + at the parent level. *) +require import AllCore. + +pragma +strict_bullets. + +(* Outer split bulleted with `+'; inner split inside the first child + uses `-'. The first child's last sibling is taken implicitly. Then + the outer's last sibling is also taken implicitly, where a fresh + `split' begins a new bullet stack and `+' must again be available. *) +lemma reuse_after_implicit (a b c d : bool) : + a => b => c => d => (a /\ b) /\ (c /\ d). +proof. +move=> ha hb hc hd; split. ++ split. + - exact ha. + exact hb. (* implicit last sibling of inner `-' frame *) +split. (* implicit last sibling of outer `+' frame *) ++ exact hc. +exact hd. +qed. + +(* Variant: longer outer enumeration; each child uses its own inner + character and an implicit final sibling. *) +lemma reuse_after_implicit3 (a b c d e f : bool) : + a => b => c => d => e => f => + (a /\ b) /\ (c /\ d) /\ (e /\ f). +proof. +move=> ha hb hc hd he hf; split. ++ split. + - exact ha. + exact hb. +split. ++ split. + - exact hc. + exact hd. +split. +- exact he. +exact hf. +qed. diff --git a/tests/bullets-last-fallthrough.ec b/tests/bullets-last-fallthrough.ec new file mode 100644 index 000000000..b5eda55c6 --- /dev/null +++ b/tests/bullets-last-fallthrough.ec @@ -0,0 +1,65 @@ +(* Under +strict_bullets, the last sibling of a split point can be + continued at the parent level without a bullet: when the previous + sibling is closed and exactly one sibling remains, the inner frame + pops automatically. *) +require import AllCore. + +pragma +strict_bullets. + +(* The motivating pattern: a flat chain of hoare `seq N : ' + phrases, each discharged with a single `+' for the side obligation; + the continuation runs at the parent level without further bullets. *) +module M = { + proc f() : int = { + var x : int; + x <- 1; + x <- x + 1; + x <- x + 1; + return x; + } +}. + +lemma seq_chain : hoare[M.f : true ==> res = 3]. +proof. +proc. +seq 1 : (x = 1). ++ by auto. +seq 1 : (x = 2). ++ by auto. +auto. +qed. + +(* A 2-way propositional split: the last subgoal can be dispatched + without a bullet. *) +lemma last_no_bullet (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- exact hp. +exact hq. +qed. + +(* A 3-way split keeps its enumeration discipline for the first two + subgoals, but the third may be unbulleted. *) +lemma three_ways (p q r : bool) : + p => q => r => p /\ q /\ r. +proof. +move=> hp hq hr; do! split. +- exact hp. +- exact hq. +exact hr. +qed. + +(* Cascading auto-pop: a nested split whose inner level reaches its + last sibling AND whose outer level reaches its last sibling can be + continued at the outermost level with no bullets. *) +lemma cascade (p q r s : bool) : + p => q => r => s => (p /\ q) /\ (r /\ s). +proof. +move=> hp hq hr hs; split. +- split. + + exact hp. + exact hq. +split. ++ exact hr. +exact hs. +qed. diff --git a/tests/bullets-legacy.ec b/tests/bullets-legacy.ec new file mode 100644 index 000000000..d8345a74f --- /dev/null +++ b/tests/bullets-legacy.ec @@ -0,0 +1,19 @@ +(* Without the pragma, bullets remain pure decoration (legacy + behavior). The bullets here would all be misused if strict mode + were on. *) +require import AllCore. + +lemma sloppy (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- exact hp. +- exact hq. +qed. + +(* Bullet character mismatch is silently accepted in non-strict mode. *) +lemma mixed (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +- exact hp. ++ exact hq. +qed. diff --git a/tests/bullets-naked-split.ec b/tests/bullets-naked-split.ec new file mode 100644 index 000000000..f1b6654fb --- /dev/null +++ b/tests/bullets-naked-split.ec @@ -0,0 +1,32 @@ +(* Under +strict_bullets, a phrase that produces multiple subgoals + must be followed by a bullet — strict mode cannot be bypassed by + simply omitting bullets entirely. Each `fail …' phrase is expected + to error out; the surrounding proof must still finish cleanly. *) +require import AllCore. + +pragma +strict_bullets. + +(* Naked split at top level: an unbulleted phrase that follows is + ambiguous and must be rejected. *) +lemma naked_top (p q : bool) : p => q => p /\ q. +proof. +move=> hp hq; split. +fail exact hp. +- exact hp. +- exact hq. +qed. + +(* Naked split nested inside a `+' frame: same rule applies at the + inner level. *) +lemma naked_nested (a b c d : bool) : + a => b => c => d => (a /\ b) /\ (c /\ d). +proof. +move=> ha hb hc hd; split. ++ split. + fail exact ha. + - exact ha. + exact hb. ++ split. + - exact hc. + exact hd. +qed. From 8a2e47f42c69aeb4c2c06f12c7361e71a9c6978b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 26 May 2026 21:07:24 +0200 Subject: [PATCH 02/11] Add LLM coding-agent REPL and goal-printing flags Introduce an interactive REPL for LLM coding agents driving EasyCrypt (`easycrypt llm`) using a line-oriented protocol over stdin/stdout, plus two CLI flags for goal inspection: - `-upto ` compile up to a given position and print the goals - `-lastgoals` print the last unproven goals at end-of-file REPL protocol (see `doc/llm/CLAUDE.md` for the full guide): - LOAD "file.ec" [LINE[:COL]] -- compile, optionally up to a position - UNDO / REVERT -- navigate proof state - GOALS / GOALS ALL -- inspect current or all subgoals - CHECKPOINT -- named bookmarks for branching - SEARCH -- lemma search - QUIET ON/OFF -- suppress goal display for bulk input - Direct EasyCrypt input (tactics, declarations, search, print, ...) Responses use a typed envelope (OK/ERROR with uuid) terminated by an `` sentinel for reliable parsing. LOAD reports the last processed line in the response tag; error messages include the offending source text; only the current subgoal is shown by default with a remaining count. --- doc/llm/CLAUDE.md | 272 +++++++++++++++++++++---- dune | 6 +- src/ec.ml | 493 +++++++++++++++++++++++++++++++++++++++++++--- src/ecOptions.ml | 48 ++--- src/ecOptions.mli | 4 +- 5 files changed, 712 insertions(+), 111 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 0cc20c5a3..c33dc1825 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -6,59 +6,246 @@ computations, program logics (Hoare logic, probabilistic Hoare logic, probabilistic relational Hoare logic), and ambient mathematical reasoning. -## Using the `llm` command +## Using the `llm` interactive mode -The `llm` subcommand is designed for non-interactive, LLM-friendly -batch compilation. It produces no progress bar and no `.eco` cache -files. +The `llm` subcommand provides an interactive REPL with a +machine-friendly protocol designed for LLM agents. The LLM sends +commands over stdin and receives structured responses on stdout. ``` -easycrypt llm [OPTIONS] FILE.ec +easycrypt llm [OPTIONS] ``` -### Options +Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are +available. Use `-help` to print this guide and exit: -- `-upto LINE` or `-upto LINE:COL` — Compile up to (but not - including) the given location, then print the current goal state to - stdout and exit with code 0. Use this to inspect the proof state at - a specific point in a file. +``` +easycrypt llm -help +``` -- `-lastgoals` — On failure, print the goal state (as it was just - before the failing command) to stdout, then print the error to - stderr, and exit with code 1. Use this to understand what the - failing tactic was supposed to prove. +### Protocol -Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are -also available. +**Startup.** EasyCrypt prints a `READY` message and waits for input: + +``` +READY [uuid:0] + +``` + +**Responses.** Every response has a typed envelope and an `` +sentinel: + +``` +OK [uuid:N] + + +``` + +``` +ERROR [uuid:N] + + +``` + +The `uuid` is a monotonically increasing integer identifying the proof +engine state. It increments with each successful command. + +### Meta-commands -### Output conventions +These are protocol-level commands, not EasyCrypt syntax: -- **Goals** are printed to **stdout**. -- **Errors** are printed to **stderr**. -- **Exit code 0** means success (or `-upto` reached its target). -- **Exit code 1** means a command failed. -- If there is no active proof at the point where goals are requested, - stdout will contain: `No active proof.` +| Command | Description | +|---------|-------------| +| `LOAD "file.ec" [LINE[:COL]] [-nosmt]` | Reset state, compile file (optionally skip SMT) | +| `UNDO` | Undo the last proof step | +| `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | +| `GOALS` | Print the current goal (first subgoal only, with remaining count) | +| `GOALS ALL` | Print all subgoals | +| `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | +| `SEARCH ` | Search for lemmas matching a pattern | +| `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | +| `` / `` | Delimit multi-line EasyCrypt input | +| `HELP` | Print this guide | +| `QUIT` | Exit | -### Workflow for writing and debugging proofs +### EasyCrypt commands -1. Try to write a pen-and-paper proof first. +Any line that is not a meta-command is parsed as EasyCrypt input. +This covers tactics, declarations, `search`, `print`, `require`, +etc. The line must be a complete EasyCrypt statement ending with `.` -2. Write the `.ec` file with your proof attempt. For a large proof, - write down skeleton and `admit` subgoals first, and then detail - the proof. +``` +smt(). +rewrite H1 H2. +search (%/). +print mulzK. +``` + +For multi-line statements, wrap with `` and ``: + +``` + +lemma test : + 0 <= n => + 0 < n + 1. + +``` + +### Workflow + +**1. Load a file up to the proof point:** -3. Run `easycrypt llm -lastgoals FILE.ec` to check the full file. - - If it succeeds (exit 0), you are done. - - If it fails (exit 1), read the error from stderr and the goal - state from stdout to understand what went wrong. +``` +LOAD "myfile.ec" 42 +``` + +This compiles the file through line 42 (processing any command whose +end is on or before that line). The response includes where it +stopped: + +``` +OK [uuid:15] [loaded:myfile.ec:42] +Current goal +... + +``` -4. Use `-upto LINE` to inspect the proof state at a specific point - without running the rest of the file. This is useful for - incremental proof development. +For large files, use `-nosmt` to skip SMT calls during prefix +compilation (safe when the prefix was already verified): -5. Fix the proof and repeat from step 2. The ultimate proof should - not contain `admit` or `admitted`. +``` +LOAD "myfile.ec" 436 -nosmt +``` + +**2. Try tactics, using REVERT to restart:** + +The uuid returned by LOAD is a revertible state. Use `REVERT` to +return to it after failed experiments — this is instant, unlike +re-doing LOAD which recompiles the prefix. + +``` +LOAD "myfile.ec" 42 +→ OK [uuid:15] [loaded:myfile.ec:42] + +smt(). ← fails, state unchanged +rewrite H1. smt(). ← succeeds (uuid:17) +rewrite H2. ← wrong direction +REVERT 17 ← back to after the successful smt() +``` + +To restart the proof from scratch, revert to the LOAD uuid: + +``` +REVERT 15 ← back to the state right after LOAD +``` + +Always note the LOAD uuid so you can return to it. + +**3. Use checkpoints for branching exploration:** + +``` +CHECKPOINT before_split +split. +smt(). ← fails +REVERT before_split +apply H. ← try a different approach +``` + +**4. Use QUIET mode to save tokens during bulk tactic application:** + +``` +QUIET ON +rewrite H1. +rewrite H2. +rewrite H3. +QUIET OFF +GOALS +``` + +**5. Search for lemmas using patterns:** + +EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as +wildcard: + +``` +search (fdom _). ← lemmas involving fdom +search (_ %/ _). ← integer division lemmas +search (card (_ `|` _)). ← card of union +search (mu _ _) (_ <= _). ← mu lemmas with inequalities +``` + +The SEARCH meta-command is a shorthand that adds `search`/`.`: + +``` +SEARCH (fdom _) +SEARCH (_ %/ _) +``` + +## EasyCrypt proof strategy + +### General approach + +- Start with a pen-and-paper proof plan before writing tactics. +- Use `smt()` aggressively. Try it first — if it fails, add hints: + `smt(lemma1 lemma2)`. +- Build proofs with `have` assertions. Establish intermediate facts + as named hypotheses, then combine with `smt()`. Avoid long rewrite + chains. +- Case split early: `case (n = 0) => [->|hn0].` Base cases often + close by computation. +- Provide specific instances of lemmas to smt: + `have h := lemma arg1 arg2.` SMT works much better with ground + instances than with universally quantified axioms. + +### Integer division (`%/`) + +- `divzK`: `d %| m => m %/ d * d = m` — recovering from exact + division +- `mulzK`: `d <> 0 => m * d %/ d = m` — canceling a known factor +- `divzMpl`: `0 < p => p * m %/ (p * d) = m %/ d` — simplifying + common factors +- To prove `a %/ d = x`, establish `a = x * d` (with `d %| a`), + then use `mulzK`. +- Don't try to rewrite inside `%/` expressions directly. Instead, + prove the equality as a `have` and use it. + +### What works, what doesn't + +- `ring` solves polynomial equalities over integers but treats + abstract ops (like `fact`) as opaque. It **cannot** simplify + `fact(n-1+1)` to `fact(n)`. +- `smt()` can do linear arithmetic and combine hypotheses, but + struggles with nonlinear integer division. Pre-compute key facts + with `have` and `divzK`/`mulzK`, then let smt combine them. +- `rewrite {k}h` rewrites the k-th occurrence only. Essential when a + term appears on both sides of an equation. +- For induction on naturals: `elim/natind: n` gives base (`n ≤ 0`) + and step (`0 ≤ n → P n → P (n+1)`). + +### SMT usage + +`smt()` and `/#` are equivalent — both call external SMT solvers. + +- Use `smt()` **only** on goals that are pure arithmetic or pure + propositional logic. If the goal contains abstract operators, + FMap terms, or `if-then-else`, reduce it first with `rewrite`, + `case`, or `have` before calling `smt()`. +- If `smt()` takes more than 1 second, the goal is too complex. + Simplify with interactive tactics instead of increasing the + timeout. + +### Common pitfalls + +- `rewrite (factS n) //` generates a side goal `0 <= n`. Use + `first smt()` or provide the precondition explicitly. +- `by` closes **all** remaining subgoals. If it fails, the error + refers to the first unclosed goal, which may not be the intended + one. +- When a tactic generates multiple subgoals, each subgoal must be + closed in order. Use `GOALS ALL` to see them all. +- `rewrite lemma in H` modifies hypothesis `H` in place (it does + not consume it). If you need to preserve the original, copy it + first: `have H' := H; rewrite lemma in H'`. ## EasyCrypt language overview @@ -91,8 +278,6 @@ proof. by ring. qed. ### Common tactics - - - `trivial` — solve trivial goals - `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints - `auto` — automatic reasoning @@ -141,9 +326,10 @@ proof. by ring. qed. ### Guidelines -* Use SMT solver only in direct mode (smt() or /#) on simple goals (arithmetic goals, pure logical goals). +* Use SMT solver only in direct mode (smt() or /#) on simple goals + (arithmetic goals, pure logical goals). * Refrain from unfolding operator definitions unless necessary. - If you need more properties on an operator, state this property in a dedicated lemma, - but avoid unfolding definitions in higher level proofs. - + If you need more properties on an operator, state this property + in a dedicated lemma, but avoid unfolding definitions in higher + level proofs. diff --git a/dune b/dune index 7c8edf709..b232abeca 100644 --- a/dune +++ b/dune @@ -1,4 +1,4 @@ -(dirs 3rdparty src etc theories examples assets scripts) +(dirs 3rdparty src etc theories examples assets scripts doc) (install (section (site (easycrypt commands))) @@ -6,7 +6,9 @@ (install (section (site (easycrypt doc))) - (files (assets/styles/styles.css as styles.css))) + (files + (assets/styles/styles.css as styles.css) + (doc/llm/CLAUDE.md as llm-guide.md))) (install (section (bin)) diff --git a/src/ec.ml b/src/ec.ml index 1a1efc5dd..95b8d39aa 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -404,6 +404,469 @@ let main () = (* Register user messages printers *) begin let open EcUserMessages in register () end; + (* -------------------------------------------------------------------- *) + (* LLM interactive mode *) + (* -------------------------------------------------------------------- *) + + let llm_guide_path () = + let (module Sites) = EcRelocate.sites in + match EcRelocate.sourceroot with + | Some root -> + Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" + | None -> + Filename.concat Sites.doc "llm-guide.md" + in + + let print_llm_guide () = + let path = llm_guide_path () in + try + let ic = open_in path in + begin try while true do + print_char (input_char ic) + done with End_of_file -> () end; + close_in ic + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + in + + let run_llm_repl (llmopts : llm_option) = + if llmopts.llmo_help then begin + print_llm_guide (); + exit 0 + end; + + let prvopts = llmopts.llmo_provers in + (* Initialize PRNG *) + Random.self_init (); + + (* Connect to external Why3 server if requested *) + prvopts.prvo_why3server |> oiter (fun server -> + try + Why3.Prove_client.connect_external server + with Why3.Prove_client.ConnectionError e -> + Format.eprintf + "cannot connect to Why3 server `%s': %s" server e; + exit 1); + + (* Add current directory to load path *) + (match relocdir with + | None -> EcCommands.addidir Filename.current_dir_name + | Some pwd -> EcCommands.addidir pwd); + + (* Proof engine configuration *) + let checkmode = { + EcCommands.cm_checkall = prvopts.prvo_checkall; + EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; + EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; + EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; + EcCommands.cm_provers = prvopts.prvo_provers; + EcCommands.cm_quorum = prvopts.prvo_quorum; + EcCommands.cm_profile = prvopts.prvo_profile; + } in + + (* Notice buffer: collects messages during command processing *) + let notices = Buffer.create 256 in + + let notifier (_ : EcGState.loglevel) (lazy msg) = + Buffer.add_string notices msg; + Buffer.add_char notices '\n' + in + + let initialized = ref false in + + let do_initialize () = + EcCommands.initialize + ~restart:!initialized ~undo:true + ~boot:ldropts.ldro_boot ~checkmode ~checkproof:true; + initialized := true; + (try + List.iter EcCommands.apply_pragma prvopts.prvo_pragmas + with EcCommands.InvalidPragma x -> + EcScope.hierror "invalid pragma: `%s'\n%!" x); + EcCommands.addnotifier notifier; + oiter (fun ppwidth -> + let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in + EcGState.setvalue "PP:width" (`Int ppwidth) gs) + prvopts.prvo_ppwidth + in + + (* Error formatting *) + let format_error ?(src="") e = + let base = match e with + | EcScope.TopError (loc, e) -> + let msg = String.strip (EcPException.tostring e) in + if loc = EcLocation._dummy then msg + else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg + | e -> + String.strip (EcPException.tostring e) + in + if src = "" then base + else Printf.sprintf "%s\nsource: %s" base src + in + + (* Output helpers *) + let goals_to_string ?(all=false) () = + let buf = Buffer.create 256 in + let fmt = Format.formatter_of_buffer buf in + EcCommands.pp_current_goal_or_noproof ~all fmt; + Format.pp_print_flush fmt (); + Buffer.contents buf + in + + let quiet = ref false in + + let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + + let reply_ok ?(tag="") body = + let n = Buffer.contents notices in + Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; + if n <> "" then print_string n; + if body <> "" then begin + print_string body; + let len = String.length body in + if len > 0 && body.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + in + + let reply_ok_goals ?(all=false) () = + if !quiet then reply_ok "" + else reply_ok (goals_to_string ~all ()) + in + + let reply_error msg = + let goals = goals_to_string () in + Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; + if goals <> "" then begin + print_string goals; + let len = String.length goals in + if len > 0 && goals.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + in + + (* Process a single EasyCrypt command, respecting gl_fail *) + let process_action ~src (p : EP.global) = + let loc = p.EP.gl_action.EcLocation.pl_loc in + let succeeded = ref false in + begin try + ignore (EcCommands.process ~src p.EP.gl_action : float option); + succeeded := true + with + | EcCommands.Restart -> raise EcCommands.Restart + | _ when p.EP.gl_fail -> () + | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) + end; + if !succeeded && p.EP.gl_fail then + raise (EcScope.toperror_of_exn ~gloc:loc + (EcScope.HiScopeError (None, + "this command is expected to fail"))) + in + + (* Process EasyCrypt input from a string (one parsed program) *) + let process_ec_input input = + Buffer.clear notices; + let reader = EcIo.from_string input in + let last_src = ref "" in + begin try + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + begin match EcLocation.unloc prog with + | EP.P_Prog (commands, _) -> + List.iter (process_action ~src) commands; + reply_ok_goals () + | EP.P_Undo i -> + EcCommands.undo i; + reply_ok_goals () + | EP.P_Exit -> + EcIo.finalize reader; exit 0 + | EP.P_DocComment doc -> + EcCommands.doc_comment doc; + reply_ok "" + end + with + | EcCommands.Restart -> + do_initialize (); + reply_ok "Session restarted" + | e -> + reply_error (format_error ~src:!last_src e) + end; + EcIo.finalize reader + in + + (* Handle LOAD "file.ec" [LINE[:COL]] *) + let handle_load args = + Buffer.clear notices; + let args = String.strip args in + let last_src = ref "" in + + try + (* Parse quoted or unquoted filename *) + let filename, rest = + if String.length args > 0 && args.[0] = '"' then + let close = + try String.index_from args 1 '"' + with Not_found -> + failwith "LOAD: unterminated filename" + in + let fn = String.sub args 1 (close - 1) in + let rest = String.strip ( + String.sub args (close + 1) + (String.length args - close - 1)) in + (fn, rest) + else + match String.split_on_char ' ' args with + | [] -> failwith "LOAD: missing filename" + | [f] -> (f, "") + | f :: rest -> (f, String.concat " " rest) + in + + (* Parse optional LINE[:COL] and flags (-nosmt) *) + let upto, nosmt = + if rest = "" then (None, false) + else + let words = String.split_on_char ' ' rest in + let words = List.filter (fun s -> s <> "") words in + let nosmt = List.mem "-nosmt" words in + let words = List.filter (fun s -> s <> "-nosmt") words in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt) + in + + (* Validate file extension *) + begin try + ignore (EcLoader.getkind + (Filename.extension filename) : EcLoader.kind) + with EcLoader.BadExtension ext -> + failwith (Format.sprintf + "unknown file extension: %s" ext) + end; + + (* Reset proof engine and process file *) + do_initialize (); + Hashtbl.clear checkpoints; + EcCommands.addidir (Filename.dirname filename); + + let reader = EcIo.from_file filename in + + let past_upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + in + + let last_loc = ref None in + + (* In -nosmt mode, admit all SMT calls during prefix loading *) + if nosmt then EcCommands.pragma_check `WeakCheck; + + begin try while true do + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter (fun p -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + process_action ~src p; + last_loc := Some loc + ) commands; + if locterm then raise Exit + | EP.P_Undo i -> + EcCommands.undo i + | EP.P_Exit -> + raise Exit + | EP.P_DocComment doc -> + EcCommands.doc_comment doc + done with + | Exit | End_of_file -> () + | e -> + EcIo.finalize reader; + if nosmt then EcCommands.pragma_check `Check; + raise e + end; + + EcIo.finalize reader; + + (* Restore full SMT checking for interactive tactics *) + if nosmt then EcCommands.pragma_check `Check; + + let tag = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + reply_ok ~tag (goals_to_string ()) + + with + | EcCommands.Restart -> + do_initialize (); + Hashtbl.clear checkpoints; + reply_ok "Session restarted" + | Failure s -> + reply_error s + | e -> + reply_error (format_error ~src:!last_src e) + in + + (* Initialize proof engine *) + do_initialize (); + + (* Signal ready *) + Printf.printf "READY [uuid:%d]\n\n%!" + (EcCommands.uuid ()); + + (* Main REPL loop *) + let multi_buf = Buffer.create 256 in + let in_multi = ref false in + + begin try while true do + let line = input_line stdin in + let line = String.strip line in + + (* Multi-line input: starts, flushes *) + if line = "" then begin + Buffer.clear multi_buf; + in_multi := true + end + else if line = "" && !in_multi then begin + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + end + else if !in_multi then begin + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf line + end + + else if line = "" then + () + else if line = "QUIT" then + exit 0 + else if line = "HELP" then begin + Buffer.clear notices; + let buf = Buffer.create 4096 in + let path = llm_guide_path () in + begin try + let ic = open_in path in + begin try while true do + Buffer.add_char buf (input_char ic) + done with End_of_file -> () end; + close_in ic; + reply_ok (Buffer.contents buf) + with Sys_error e -> + reply_error (Printf.sprintf "cannot read guide: %s" e) + end + end + else if line = "UNDO" then begin + Buffer.clear notices; + let uuid = EcCommands.uuid () in + if uuid > 0 then begin + EcCommands.undo (uuid - 1); + reply_ok_goals () + end else + reply_error "nothing to undo" + end + else if line = "GOALS ALL" then begin + Buffer.clear notices; + reply_ok (goals_to_string ~all:true ()) + end + else if line = "GOALS" then begin + Buffer.clear notices; + reply_ok (goals_to_string ()) + end + else if String.starts_with line "CHECKPOINT " then begin + Buffer.clear notices; + let name = String.strip ( + String.sub line 11 (String.length line - 11)) in + if name = "" then + reply_error "CHECKPOINT: missing name" + else begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + end + end + else if String.starts_with line "REVERT " then begin + Buffer.clear notices; + let n = String.strip ( + String.sub line 7 (String.length line - 7)) in + let target = + try Some (int_of_string n) + with Failure _ -> Hashtbl.find_opt checkpoints n + in + begin match target with + | None -> + reply_error (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" n) + | Some target -> + let uuid = EcCommands.uuid () in + if target < 0 || target > uuid then + reply_error (Printf.sprintf + "REVERT: uuid %d out of range [0, %d]" target uuid) + else begin + EcCommands.undo target; + reply_ok_goals () + end + end + end + else if line = "QUIET ON" then begin + Buffer.clear notices; + quiet := true; + reply_ok "" + end + else if line = "QUIET OFF" then begin + Buffer.clear notices; + quiet := false; + reply_ok "" + end + else if String.starts_with line "SEARCH " then begin + let query = String.strip ( + String.sub line 7 (String.length line - 7)) in + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + process_ec_input (Printf.sprintf "search %s." query) + end + else if String.starts_with line "LOAD " then + handle_load (String.sub line 5 (String.length line - 5)) + else + (* Treat as EasyCrypt input *) + process_ec_input line + done with + | End_of_file -> () + end; + + exit 0 + in + (* Initialize I/O + interaction module *) let module State = struct type t = { @@ -535,34 +998,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 -> + run_llm_repl llmopts | `Runtest _ -> (* Eagerly executed *) diff --git a/src/ecOptions.ml b/src/ecOptions.ml index bd21a69aa..3e6dc5c5c 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -49,10 +49,8 @@ and doc_option = { } and llm_option = { - llmo_input : string; llmo_provers : prv_options; - llmo_lastgoals : bool; - llmo_upto : (int * int option) option; + llmo_help : bool; } and prv_options = { @@ -370,11 +368,10 @@ let specs = { `Spec ("trace" , `Flag , "Save all goals & messages in .eco"); `Spec ("compact", `Int , "")]); - ("llm", "LLM-friendly batch compilation", [ + ("llm", "LLM-friendly interactive mode", [ `Group "loader"; `Group "provers"; - `Spec ("lastgoals" , `Flag , "Print last unproved goals on failure"); - `Spec ("upto" , `String, "Compile up to LINE or LINE:COL and print goals")]); + `Spec ("help", `Flag, "Print the LLM agent guide and exit")]); ("cli", "Run EasyCrypt top-level", [ `Group "loader"; @@ -562,26 +559,9 @@ let doc_options_of_values values input = { doco_input = input; doco_outdirp = get_string "outdir" values; } -let parse_upto values = - get_string "upto" values |> Option.map (fun s -> - let invalid () = - raise (Arg.Bad (Printf.sprintf - "invalid -upto format: expected LINE or LINE:COL, got %S" s)) in - match String.split_on_char ':' s with - | [line] -> - let line = try int_of_string line with Failure _ -> invalid () in - (line, None) - | [line; col] -> - let line = try int_of_string line with Failure _ -> invalid () in - let col = try int_of_string col with Failure _ -> invalid () in - (line, Some col) - | _ -> invalid ()) - -let llm_options_of_values ini values input = - { llmo_input = input; - llmo_provers = prv_options_of_values ini values; - llmo_lastgoals = get_flag "lastgoals" values; - llmo_upto = parse_upto values; } +let llm_options_of_values ini values = + { llmo_provers = prv_options_of_values ini values; + llmo_help = get_flag "help" values; } (* -------------------------------------------------------------------- *) let parse getini argv = @@ -654,16 +634,14 @@ let parse getini argv = raise (Arg.Bad "this command takes a single input file as argument") end - | "llm" -> begin - match anons with - | [input] -> - let ini = getini (Some input) in - let cmd = `Llm (llm_options_of_values ini values input) in - (cmd, ini, true) + | "llm" -> + if not (List.is_empty anons) then + raise (Arg.Bad "this command does not take arguments"); - | _ -> - raise (Arg.Bad "this command takes a single argument") - end + let ini = getini None in + let cmd = `Llm (llm_options_of_values ini values) in + + (cmd, ini, true) | _ -> assert false diff --git a/src/ecOptions.mli b/src/ecOptions.mli index a5c09b11d..f00aef075 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -45,10 +45,8 @@ and doc_option = { } and llm_option = { - llmo_input : string; llmo_provers : prv_options; - llmo_lastgoals : bool; - llmo_upto : (int * int option) option; + llmo_help : bool; } and prv_options = { From 56cf2d25d959a5911ce0e7fe2e641f8a43696093 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 27 May 2026 05:01:33 +0200 Subject: [PATCH 03/11] [llm] add LOAD ... -trace for before/after sentence inspection Add a -trace flag to the LOAD REPL command. When set, LOAD compiles the prefix exactly as today (using the existing LINE[:COL] argument, or up to EOF if omitted), but defers the last sentence and runs it under goal capture, then returns a response body with four delimited blocks: === BEFORE: line L (col C) === === TACTIC (lines L:C - L':C') === === AFTER: line L (col C) === === SUMMARY === open goals: N1 -> N2 Adapted from PR #1018 (-trace LINE[:COL] for batch mode): same delimiters and the same new-or-modified-head filtering for AFTER. The position is taken from LOAD's existing LINE[:COL] argument; the tag is the regular [loaded:file:LINE]. If the deferred sentence is outside a proof context, or there is no sentence to trace, the reply uses the ERROR envelope with a clear message. If the sentence fails, the BEFORE/TACTIC blocks are still delivered, AFTER carries a marker, and the formatted exception is appended. Expose EcCommands.in_proof so the REPL can check the pre-execution proof status without inspecting scope internals. --- doc/llm/CLAUDE.md | 23 +++++- src/ec.ml | 188 ++++++++++++++++++++++++++++++++++++++------- src/ecCommands.ml | 5 +- src/ecCommands.mli | 1 + 4 files changed, 186 insertions(+), 31 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index c33dc1825..7918f21fe 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -56,7 +56,7 @@ These are protocol-level commands, not EasyCrypt syntax: | Command | Description | |---------|-------------| -| `LOAD "file.ec" [LINE[:COL]] [-nosmt]` | Reset state, compile file (optionally skip SMT) | +| `LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]` | Reset state, compile file (optionally skip SMT or trace last sentence) | | `UNDO` | Undo the last proof step | | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | @@ -117,6 +117,27 @@ compilation (safe when the prefix was already verified): LOAD "myfile.ec" 436 -nosmt ``` +Add `-trace` to a LOAD to inspect the proof state around the last +loaded sentence. The reply body contains four delimited blocks: + +``` +LOAD "myfile.ec" 42 -trace + +=== BEFORE: line 42 (col 0) === + +=== TACTIC (lines 42:0 - 42:10) === + +=== AFTER: line 42 (col 0) === + +=== SUMMARY === +open goals: N1 -> N2 +``` + +The position comes from the existing `LINE[:COL]` argument; omit it to +trace the file's last sentence. On tactic failure the reply uses the +`ERROR` envelope and still includes the BEFORE/TACTIC blocks plus an +`` marker in the AFTER block. + **2. Try tactics, using REVERT to restart:** The uuid returned by LOAD is a revertible state. Use `REVERT` to diff --git a/src/ec.ml b/src/ec.ml index 95b8d39aa..ffd797399 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -604,6 +604,8 @@ let main () = Buffer.clear notices; let args = String.strip args in let last_src = ref "" in + let trace_prefix = ref "" in + let exception Trace_failed of exn in try (* Parse quoted or unquoted filename *) @@ -626,27 +628,32 @@ let main () = | f :: rest -> (f, String.concat " " rest) in - (* Parse optional LINE[:COL] and flags (-nosmt) *) - let upto, nosmt = - if rest = "" then (None, false) - else - let words = String.split_on_char ' ' rest in - let words = List.filter (fun s -> s <> "") words in - let nosmt = List.mem "-nosmt" words in - let words = List.filter (fun s -> s <> "-nosmt") words in - let upto = match words with - | [] -> None - | [w] -> - begin match String.split_on_char ':' w with - | [line] -> - Some (int_of_string line, None) - | [line; col] -> - Some (int_of_string line, Some (int_of_string col)) - | _ -> failwith "LOAD: invalid LINE[:COL] format" - end - | _ -> failwith "LOAD: unexpected arguments" - in - (upto, nosmt) + (* Parse optional LINE[:COL] and flags (-nosmt, -trace) *) + let upto, nosmt, trace = + let words = + String.split_on_char ' ' rest + |> List.filter (fun s -> s <> "") + in + let nosmt = List.mem "-nosmt" words in + let trace = List.mem "-trace" words in + let words = + List.filter + (fun s -> s <> "-nosmt" && s <> "-trace") + words + in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt, trace) in (* Validate file extension *) @@ -677,27 +684,65 @@ let main () = let last_loc = ref None in + (* For -trace: lazy whole-file bytes, used to slice the exact + source text of a sentence by byte offsets. *) + let input_bytes = lazy ( + let ic = open_in_bin filename in + let n = in_channel_length ic in + let b = Bytes.create n in + really_input ic b 0 n; + close_in ic; + Bytes.unsafe_to_string b) + in + let sentence_source (loc : EcLocation.t) = + let s = Lazy.force input_bytes in + let lo = max 0 loc.EcLocation.loc_bchar in + let hi = min (String.length s) loc.EcLocation.loc_echar in + if hi <= lo then "" else String.sub s lo (hi - lo) + in + + (* For -trace: defer execution of the last sentence within the + prefix so we can capture goals before and after it. *) + let pending : (string * EP.global) option ref = ref None in + let flush_pending () = + match !pending with + | None -> () + | Some (src, p) -> + last_src := src; + process_action ~src p; + last_loc := Some p.EP.gl_action.EcLocation.pl_loc; + pending := None + in + let step src p = + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + if trace then begin + flush_pending (); + pending := Some (src, p) + end else begin + last_src := src; + process_action ~src p; + last_loc := Some loc + end + in + (* In -nosmt mode, admit all SMT calls during prefix loading *) if nosmt then EcCommands.pragma_check `WeakCheck; begin try while true do let (src, prog) = EcIo.xparse reader in let src = String.strip src in - last_src := src; match EcLocation.unloc prog with | EP.P_Prog (commands, locterm) -> - List.iter (fun p -> - let loc = p.EP.gl_action.EcLocation.pl_loc in - if past_upto loc then raise Exit; - process_action ~src p; - last_loc := Some loc - ) commands; + List.iter (step src) commands; if locterm then raise Exit | EP.P_Undo i -> + last_src := src; EcCommands.undo i | EP.P_Exit -> raise Exit | EP.P_DocComment doc -> + last_src := src; EcCommands.doc_comment doc done with | Exit | End_of_file -> () @@ -712,6 +757,88 @@ let main () = (* Restore full SMT checking for interactive tactics *) if nosmt then EcCommands.pragma_check `Check; + (* If -trace is set, the last in-prefix sentence is still + pending. Run it with goal capture before and after, and + build the BEFORE/TACTIC/AFTER/SUMMARY response body. *) + let body = + if not trace then + goals_to_string () + else + let pre_state = + match !pending with + | None -> `Nothing + | Some _ when not (EcCommands.in_proof ()) -> `NotInProof + | Some (src, p) -> `Ready (src, p) + in + match pre_state with + | `Nothing -> failwith "trace: nothing to trace" + | `NotInProof -> + failwith + "trace: target sentence is not in a proof context" + | `Ready (src, p) -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + let (sl, sc) = loc.EcLocation.loc_start in + let (el, ec) = loc.EcLocation.loc_end in + let before_goals = EcCommands.pp_all_goals () in + let n1 = List.length before_goals in + let buf = Buffer.create 1024 in + let fmt = Format.formatter_of_buffer buf in + Format.fprintf fmt + "=== BEFORE: line %d (col %d) ===@\n" sl sc; + EcCommands.pp_current_goal_or_noproof ~all:false fmt; + Format.fprintf fmt + "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" + sl sc el ec (sentence_source loc); + last_src := src; + begin + try + process_action ~src p; + last_loc := Some loc; + pending := None; + let after_goals = EcCommands.pp_all_goals () in + let n2 = List.length after_goals in + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n" sl sc; + let before_set = + List.fold_left + (fun s g -> EcMaps.Sstr.add g s) + EcMaps.Sstr.empty before_goals + in + (* The new focused goal always counts as "modified" + (its focus status changed even if its text matches + an old sibling); the rest are printed only if + they didn't appear in BEFORE. *) + let to_print = + match after_goals with + | [] -> [] + | head :: tl -> + head :: + List.filter + (fun g -> not (EcMaps.Sstr.mem g before_set)) + tl + in + begin match to_print with + | [] -> Format.fprintf fmt "(no open goals)@\n" + | _ -> + List.iteri (fun i g -> + if i > 0 then Format.fprintf fmt "@\n"; + Format.fprintf fmt "%s@\n" g) + to_print + end; + Format.fprintf fmt + "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; + Format.pp_print_flush fmt (); + Buffer.contents buf + with e -> + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n@\n" + sl sc; + Format.pp_print_flush fmt (); + trace_prefix := Buffer.contents buf; + raise (Trace_failed e) + end + in + let tag = match !last_loc with | None -> "" @@ -719,13 +846,16 @@ let main () = let (el, _) = loc.EcLocation.loc_end in Printf.sprintf " [loaded:%s:%d]" filename el in - reply_ok ~tag (goals_to_string ()) + reply_ok ~tag body with | EcCommands.Restart -> do_initialize (); Hashtbl.clear checkpoints; reply_ok "Session restarted" + | Trace_failed e -> + let msg = format_error ~src:!last_src e in + reply_error (!trace_prefix ^ msg) | Failure s -> reply_error s | e -> diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 08f801623..3fb35e82a 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -1056,8 +1056,11 @@ let pp_current_goal ?(all = false) stream = end (* -------------------------------------------------------------------- *) +let in_proof () = + Option.is_some (S.xgoal (current ())) + 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%!" diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 7dab0b84b..acb3346c3 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -63,6 +63,7 @@ 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 pragma_verbose : bool -> unit From 9807a149fb649dcc5bc2a1d257d2efc49a8c096f Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 06:58:45 +0200 Subject: [PATCH 04/11] [llm] relax +strict_bullets in REPL, add TREE and focus tag Three small additions to make REPL-driven proof exploration pleasant without weakening +strict_bullets for saved scripts. 1. Bullet relaxation for REPL input. EcCommands.disable_repl_bullets is called at every REPL phrase; it drops pm_strict_bullets and clears puc_bullets on the active proof so REPL-typed tactics are not rejected for missing bullets. Files loaded via LOAD still respect their own pragma; only direct REPL input is relaxed. 2. TREE / TREE ALL meta-commands. List all open subgoals as a flat numbered enumeration with the focused goal marked. TREE shows a one-line conclusion per goal; TREE ALL shows the full goal bodies. Backed by EcCommands.pp_tree on top of EcCoreGoal.all_opened. 3. [focus: k/N] reply tag. When more than one subgoal is open, both tactic replies and the LOAD response carry [focus: 1/N] alongside any other tag, so the caller knows the next tactic targets goal #1 of N. Supporting plumbing: EcScope.set_xgoal exposes a way to swap the active proof_uc without going through the tactic engine. --- doc/llm/CLAUDE.md | 11 +++++++- src/ec.ml | 66 +++++++++++++++++++++++++++++++++++++++++----- src/ecCommands.ml | 53 +++++++++++++++++++++++++++++++++++++ src/ecCommands.mli | 2 ++ src/ecScope.ml | 4 +++ src/ecScope.mli | 1 + 6 files changed, 129 insertions(+), 8 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 7918f21fe..1b7a3b066 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -61,6 +61,8 @@ These are protocol-level commands, not EasyCrypt syntax: | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | | `GOALS ALL` | Print all subgoals | +| `TREE` | List open subgoals as `[N] `, marking the focused one | +| `TREE ALL` | Same as `TREE`, but with full goal bodies | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | @@ -263,7 +265,14 @@ SEARCH (_ %/ _) refers to the first unclosed goal, which may not be the intended one. - When a tactic generates multiple subgoals, each subgoal must be - closed in order. Use `GOALS ALL` to see them all. + closed in order. Use `GOALS ALL` or `TREE` to see them all. +- When more than one subgoal is open, replies carry a + `[focus: k/N]` tag (e.g. `OK [uuid:42] [focus: 1/3]`) so you know + which one the next tactic will hit. +- `pragma +strict_bullets` does **not** apply to REPL input. Files + loaded via `LOAD` still respect their own pragmas, but tactics typed + at the REPL prompt are never rejected for missing bullets — the + REPL is the focus mechanism. - `rewrite lemma in H` modifies hypothesis `H` in place (it does not consume it). If you need to preserve the original, copy it first: `have H' := H; rewrite lemma in H'`. diff --git a/src/ec.ml b/src/ec.ml index ffd797399..f0a090545 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -513,6 +513,38 @@ let main () = Buffer.contents buf in + (* Render the focus-tree of open subgoals. [all=false] gives a + one-line digest per goal (conclusion truncated); [all=true] + gives the full goal body for each. *) + let tree_to_string ?(all=false) () = + let entries = EcCommands.pp_tree ~all () in + match entries with + | [] -> "No active proof.\n" + | _ -> + let buf = Buffer.create 256 in + let one_line s = + let s = + match String.index_opt s '\n' with + | None -> s + | Some k -> String.sub s 0 k + in + let limit = 80 in + if String.length s > limit + then String.sub s 0 (limit - 1) ^ "…" + else s + in + List.iter (fun (i, focused, text) -> + let marker = if focused then " <- focused" else "" in + if all then + Buffer.add_string buf + (Printf.sprintf "[%d]%s\n%s\n" i marker text) + else + Buffer.add_string buf + (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) + ) entries; + Buffer.contents buf + in + let quiet = ref false in let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in @@ -531,9 +563,17 @@ let main () = Buffer.clear notices in + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" + in + let reply_ok_goals ?(all=false) () = - if !quiet then reply_ok "" - else reply_ok (goals_to_string ~all ()) + let tag = focus_tag () in + if !quiet then reply_ok ~tag "" + else reply_ok ~tag (goals_to_string ~all ()) in let reply_error msg = @@ -570,6 +610,7 @@ let main () = (* Process EasyCrypt input from a string (one parsed program) *) let process_ec_input input = Buffer.clear notices; + EcCommands.disable_repl_bullets (); let reader = EcIo.from_string input in let last_src = ref "" in begin try @@ -840,11 +881,14 @@ let main () = in let tag = - match !last_loc with - | None -> "" - | Some loc -> - let (el, _) = loc.EcLocation.loc_end in - Printf.sprintf " [loaded:%s:%d]" filename el + let loaded = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + loaded ^ focus_tag () in reply_ok ~tag body @@ -930,6 +974,14 @@ let main () = Buffer.clear notices; reply_ok (goals_to_string ()) end + else if line = "TREE ALL" then begin + Buffer.clear notices; + reply_ok (tree_to_string ~all:true ()) + end + else if line = "TREE" then begin + Buffer.clear notices; + reply_ok (tree_to_string ()) + end else if String.starts_with line "CHECKPOINT " then begin Buffer.clear notices; let name = String.strip ( diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 3fb35e82a..860c51927 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -931,6 +931,28 @@ let push_context scope context = ct_stack = context.ct_stack |> omap (fun st -> context.ct_current :: st); } +(* -------------------------------------------------------------------- *) +(* 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. *) +let disable_repl_bullets () = + pragma_strict_bullets false; + match !context with + | None -> () + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> () + | Some puc -> + match puc.EcScope.puc_active with + | None -> () + | Some (pac, _) when pac.EcScope.puc_bullets = None -> () + | Some (pac, pct) -> + 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 } + (* -------------------------------------------------------------------- *) let initialize ~restart ~undo ~boot ~checkmode ~checkproof = assert (restart || EcUtils.is_none !context); @@ -1098,3 +1120,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 + | _ -> [] diff --git a/src/ecCommands.mli b/src/ecCommands.mli index acb3346c3..16a53cef5 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -64,6 +64,8 @@ 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 -> unit +val pp_tree : ?all:bool -> unit -> (int * bool * string) list (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecScope.ml b/src/ecScope.ml index 0470176df..bd8391e26 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -489,6 +489,10 @@ let goal (scope : scope) = let xgoal (scope : scope) = scope.sc_pr_uc +(* -------------------------------------------------------------------- *) +let set_xgoal (scope : scope) (puc : proof_uc) = + { scope with sc_pr_uc = Some puc } + (* -------------------------------------------------------------------- *) let dump_why3 (scope : scope) (filename : string) = try EcSmt.dump_why3 (env scope) filename diff --git a/src/ecScope.mli b/src/ecScope.mli index e4a8bff31..8a2a1dede 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -87,6 +87,7 @@ val env : scope -> EcEnv.env val attop : scope -> bool val goal : scope -> proof_auc option val xgoal : scope -> proof_uc option +val set_xgoal : scope -> proof_uc -> scope (* Creates a scope that is identical to the supplied one except * that the environment and required theories are reset to the ones From 07408b7b77bf798b489e3e9c31cbf9f042e72e81 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 07:11:13 +0200 Subject: [PATCH 05/11] [llm] add FOCUS N and NEXT for explicit goal selection The REPL relies on EC's "first open goal is the focused one" convention. Until now the only way to work on a non-first goal was to discharge the earlier ones; the proving agent often wants to inspect or skip a particular sibling without that. Add two meta-commands: FOCUS N rotate the open-goal list so the goal at index N (from TREE) becomes the focused one, preserving cyclic order. NEXT shorthand for FOCUS 2 (rotate one step). Backed by a new EcCoreGoal.rotate_focus that splits and recombines pr_opened. Going through the tactic engine doesn't work for standalone rotation: tcenv1_of_proof tc_down's the siblings out of view, so Protate (the `first last` parsed form) has nothing to rotate at the top level. EcCommands.focus_goal wraps rotate_focus, applies it via the same scope-mutation path disable_repl_bullets uses, and pushes a new context so UNDO/REVERT can roll the change back. --- doc/llm/CLAUDE.md | 2 ++ src/ec.ml | 27 +++++++++++++++++++++++++++ src/ecCommands.ml | 34 ++++++++++++++++++++++++++++++++++ src/ecCommands.mli | 1 + src/ecCoreGoal.ml | 10 ++++++++++ src/ecCoreGoal.mli | 6 ++++++ 6 files changed, 80 insertions(+) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 1b7a3b066..28c8d049a 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -63,6 +63,8 @@ These are protocol-level commands, not EasyCrypt syntax: | `GOALS ALL` | Print all subgoals | | `TREE` | List open subgoals as `[N] `, marking the focused one | | `TREE ALL` | Same as `TREE`, but with full goal bodies | +| `FOCUS N` | Rotate focus so subgoal `[N]` (from `TREE`) becomes the focused goal | +| `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | diff --git a/src/ec.ml b/src/ec.ml index f0a090545..963efdf87 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -982,6 +982,33 @@ let main () = Buffer.clear notices; reply_ok (tree_to_string ()) end + else if String.starts_with line "FOCUS " || line = "NEXT" then begin + Buffer.clear notices; + let request = + if line = "NEXT" then `Next + else + let arg = String.strip ( + String.sub line 6 (String.length line - 6)) in + try `At (int_of_string arg) + with Failure _ -> `Bad arg + in + match request with + | `Bad arg -> + reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) + | _ -> + let entries = EcCommands.pp_tree () in + let n = List.length entries in + let target = + match request with + | `Next -> if n <= 1 then 1 else 2 + | `At k -> k + | `Bad _ -> 1 + in + begin match EcCommands.focus_goal target with + | Ok _ -> reply_ok_goals () + | Error msg -> reply_error msg + end + end else if String.starts_with line "CHECKPOINT " then begin Buffer.clear notices; let name = String.strip ( diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 860c51927..5d3224969 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -932,6 +932,40 @@ let push_context scope context = |> 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 diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 16a53cef5..611c57ca5 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -66,6 +66,7 @@ val pp_all_goals : unit -> string list val in_proof : unit -> bool val disable_repl_bullets : unit -> unit val pp_tree : ?all:bool -> unit -> (int * bool * string) list +val focus_goal : int -> (int, string) result (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 4b75e5b0c..0ad46a2ae 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -1015,6 +1015,16 @@ let all_opened (pf : proof) = (* -------------------------------------------------------------------- *) let closed (pf : proof) = List.is_empty pf.pr_opened +(* -------------------------------------------------------------------- *) +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 = diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index f574b49bf..8dce48377 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -205,6 +205,12 @@ val all_opened : proof -> pregoal list (* Check if a proof is done *) val closed : proof -> bool +(* 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 From f86c43093a3d77ee08424be11dc568b8fb0a3155 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 07:39:17 +0200 Subject: [PATCH 06/11] [llm] add COMMIT to emit a +strict_bullets-friendly proof body REPL phrases are recorded with (uuid, source, parent_handle, opens), where parent_handle is the focused goal right before the phrase ran. COMMIT replays them against the proof DAG to recover the bullet structure. The DAG edge is now explicit. EcCoreGoal's proofenv carries a pr_parent : handle ID.Map.t populated by FApi.newgoal (the single choke-point where every child handle is created); EcCoreGoal exposes children_of_handle / parent_of_handle on top of it. This avoids the older approach of reading children out of g_validation, which only worked for VIntros / VConv / VLConv / VRewrite / VExtern -- not for VApply, whose subgoals are added to the tcenv state outside the validation record. Algorithm: - For each phrase, walk the subtree rooted at its parent handle, registering each multi-child split's children in [sibling_depth] at the right depth. Single-child links are continuations and do not bump depth. - To decide whether a phrase needs a bullet, walk upward via parent_of from its recorded parent until hitting a registered sibling ancestor; if found, emit the bullet for that depth and consume the registration. Bullet tokens are chosen per depth from PR 1017's lexer order (-, +, *, --, ++, **, ---, +++, *** ...), skipping any token already in scope from the LOAD prefix's puc_bullets stack. The stack is snapshotted at the moment REPL input takes over (the new return value of disable_repl_bullets) so COMMIT can avoid token collisions with frames opened by the prefix. Tested patterns: simple split, nested split, case-split, multi-tactic-per-sibling, compound first phrase (move=> hp hq; split.), pHL seq N chain, list induction, have introducing a side goal, [split; split.] producing 4 goals in one phrase, UNDO/REVERT trimming, LOAD mid-proof continuation, and LOAD prefix already using bullet tokens that COMMIT must avoid. All round-trip through `ec.exe compile` under `pragma +strict_bullets`. --- doc/llm/CLAUDE.md | 1 + src/ec.ml | 206 +++++++++++++++++++++++++++++++++++++++++++-- src/ecCommands.ml | 55 +++++++++--- src/ecCommands.mli | 5 +- src/ecCoreGoal.ml | 47 +++++++++-- src/ecCoreGoal.mli | 6 ++ 6 files changed, 295 insertions(+), 25 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 28c8d049a..a06725467 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -65,6 +65,7 @@ These are protocol-level commands, not EasyCrypt syntax: | `TREE ALL` | Same as `TREE`, but with full goal bodies | | `FOCUS N` | Rotate focus so subgoal `[N]` (from `TREE`) becomes the focused goal | | `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | +| `COMMIT` | Emit recorded REPL phrases as a bulleted proof body (works under `+strict_bullets`) | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | diff --git a/src/ec.ml b/src/ec.ml index 963efdf87..9a0b57d69 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -549,6 +549,170 @@ let main () = let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + (* Transcript of REPL-typed phrases that succeeded. Each entry is + (uuid_before, src, parent, opens_at_entry), where: + - [parent] is the handle that was focused right before the + phrase ran ([None] iff outside a proof); + - [opens_at_entry] is the full open-handle list at entry time + (focused-first), used by COMMIT to seed the sibling map for + continuations whose first phrase already starts inside a + frame opened by the LOAD prefix. + Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) + let transcript : + (int * string * EcCoreGoal.handle option + * EcCoreGoal.handle list) list ref = ref [] in + + (* The bullet stack of the active proof at the moment REPL input + took over. Captured the first time [disable_repl_bullets] + actually clears a non-empty stack; subsequent (idempotent) + calls return [None] and leave this snapshot unchanged. Used by + [COMMIT] to pick bullet characters that don't collide with + tokens already in scope from the LOAD prefix. Cleared on + LOAD/Restart along with the transcript. *) + let prior_bullets : EcBullets.stack option ref = ref None in + + let transcript_trim target = + transcript := + List.filter + (fun (uuid_before, _, _, _) -> uuid_before < target) + !transcript + in + + (* Render the recorded transcript as a +strict_bullets-friendly + proof body. The algorithm reads the proof DAG via + [EcCommands.children_of]/[parent_of] (backed by [pr_parent], + which records the parent handle of every child at + [FApi.newgoal] time). Strategy: + - For each phrase, walk the subtree rooted at its parent + handle, finding every multi-child split, and register each + such child in [sibling_depth] at the corresponding depth. + Single-child links are continuations and don't bump depth. + - To decide whether a phrase needs a bullet, walk upward via + [parent_of] from its recorded parent until hitting a + registered sibling ancestor; if found, emit the bullet for + that depth and consume the registration. + Bullet tokens are chosen per depth, skipping any token + already in the LOAD prefix's [puc_bullets] stack (snapshotted + at the moment REPL input took over) so we never collide. *) + (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, + ---, +++, *** ... *) + let token_at_index i = + let chars = [| "-"; "+"; "*" |] in + let rep = i / 3 + 1 in + let chr = chars.(i mod 3) in + String.concat "" (List.init rep (fun _ -> chr)) + in + + let commit_proof_text () = + let entries = List.rev !transcript in + let buf = Buffer.create 1024 in + let emit_indent depth = + for _ = 1 to depth do Buffer.add_string buf " " done + in + let module Hmap = + Map.Make (struct + type t = EcCoreGoal.handle + let compare = compare + end) + in + let sibling_depth : int Hmap.t ref = ref Hmap.empty in + let current_depth = ref 0 in + (* Pick a bullet token for each depth, skipping tokens already + in scope from the LOAD prefix's bullet stack (so we never + collide with frames the prefix opened). State is per-COMMIT + so each invocation starts from a clean slate. *) + let in_use_tokens = + match !prior_bullets with + | None -> [] + | Some stack -> + List.map (fun (f : EcBullets.frame) -> f.bf_token) stack + in + let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in + let next_tok_idx = ref 0 in + let assigned_tokens = ref [] in + let bullet_for_depth d = + match Hashtbl.find_opt depth_cache d with + | Some t -> t + | None -> + let rec pick () = + let t = token_at_index !next_tok_idx in + incr next_tok_idx; + if List.mem t in_use_tokens || List.mem t !assigned_tokens + then pick () + else t + in + let t = pick () in + assigned_tokens := t :: !assigned_tokens; + Hashtbl.add depth_cache d t; + t + in + (* Seed: if the first recorded phrase entered a state with + multiple open goals, the LOAD prefix opened a frame whose + siblings are still pending. Register all of them as depth-1 + pending siblings so the first phrase's parent gets a bullet. *) + (match entries with + | (_, _, Some _, (_ :: _ :: _ as opens)) :: _ -> + List.iter + (fun h -> sibling_depth := Hmap.add h 1 !sibling_depth) + opens + | _ -> ()); + List.iter (fun (_uuid, src, parent_opt, _opens) -> + match parent_opt with + | None -> + Buffer.add_string buf src; + Buffer.add_char buf '\n' + | Some parent -> + (* Walk upward through pr_parent until we find a registered + sibling ancestor, or run out. If found, emit a bullet at + that depth and consume the registration. *) + let rec find_ancestor h = + match Hmap.find_opt h !sibling_depth with + | Some d -> Some (h, d) + | None -> + match EcCommands.parent_of h with + | Some p -> find_ancestor p + | None -> None + in + (match find_ancestor parent with + | Some (h, d) -> + emit_indent (d - 1); + Buffer.add_string buf (bullet_for_depth d); + Buffer.add_char buf ' '; + current_depth := d; + sibling_depth := Hmap.remove h !sibling_depth + | None -> + emit_indent !current_depth); + Buffer.add_string buf src; + Buffer.add_char buf '\n'; + (* A phrase can chain multiple sub-validations internally + (e.g. [move=> hp hq; split.] is VIntros -> VApply(split) + on a single recorded phrase). Walk single-child + validations until we hit a real split (>=2 children) or + an open leaf. *) + (* Walk the entire subtree rooted at [parent], finding every + multi-child node, and register its children at the + corresponding nesting depth. A compound phrase like + [split; split.] can produce nested splits within a single + phrase; both levels of children need to be registered. + Single-child links don't bump the depth (continuations); + multi-child links do. *) + let rec walk h d = + match EcCommands.children_of h with + | [c] -> walk c d + | (_ :: _ :: _) as cs -> + List.iter + (fun c -> + sibling_depth := + Hmap.add c d !sibling_depth; + walk c (d + 1)) + cs + | [] -> () + in + walk parent (!current_depth + 1) + ) entries; + Buffer.contents buf + in + let reply_ok ?(tag="") body = let n = Buffer.contents notices in Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; @@ -589,9 +753,20 @@ let main () = Buffer.clear notices in - (* Process a single EasyCrypt command, respecting gl_fail *) - let process_action ~src (p : EP.global) = + (* Process a single EasyCrypt command, respecting gl_fail. When + [~record:true], capture the parent handle (the focused goal + before the phrase ran) and append a transcript entry on + success. COMMIT will use [EcCommands.children_of] on each + parent to walk the proof DAG and recover bullet structure. *) + let process_action ?(record=false) ~src (p : EP.global) = let loc = p.EP.gl_action.EcLocation.pl_loc in + let pre_uuid = EcCommands.uuid () in + let opens_pre = + if record then EcCommands.open_handles () else [] + in + let parent = + match opens_pre with h :: _ -> Some h | [] -> None + in let succeeded = ref false in begin try ignore (EcCommands.process ~src p.EP.gl_action : float option); @@ -604,13 +779,21 @@ let main () = if !succeeded && p.EP.gl_fail then raise (EcScope.toperror_of_exn ~gloc:loc (EcScope.HiScopeError (None, - "this command is expected to fail"))) + "this command is expected to fail"))); + if record && !succeeded && not p.EP.gl_fail then + transcript := (pre_uuid, src, parent, opens_pre) :: !transcript in (* Process EasyCrypt input from a string (one parsed program) *) let process_ec_input input = Buffer.clear notices; - EcCommands.disable_repl_bullets (); + (* On the first REPL phrase of each proof, capture the bullet + stack that the LOAD prefix left so COMMIT can avoid token + collisions with it. Subsequent calls return [None] and don't + clobber the snapshot. *) + (match EcCommands.disable_repl_bullets () with + | None -> () + | Some _ as snapshot -> prior_bullets := snapshot); let reader = EcIo.from_string input in let last_src = ref "" in begin try @@ -619,10 +802,11 @@ let main () = last_src := src; begin match EcLocation.unloc prog with | EP.P_Prog (commands, _) -> - List.iter (process_action ~src) commands; + List.iter (process_action ~record:true ~src) commands; reply_ok_goals () | EP.P_Undo i -> EcCommands.undo i; + transcript_trim i; reply_ok_goals () | EP.P_Exit -> EcIo.finalize reader; exit 0 @@ -633,6 +817,8 @@ let main () = with | EcCommands.Restart -> do_initialize (); + transcript := []; + prior_bullets := None; reply_ok "Session restarted" | e -> reply_error (format_error ~src:!last_src e) @@ -709,6 +895,8 @@ let main () = (* Reset proof engine and process file *) do_initialize (); Hashtbl.clear checkpoints; + transcript := []; + prior_bullets := None; EcCommands.addidir (Filename.dirname filename); let reader = EcIo.from_file filename in @@ -896,6 +1084,8 @@ let main () = | EcCommands.Restart -> do_initialize (); Hashtbl.clear checkpoints; + transcript := []; + prior_bullets := None; reply_ok "Session restarted" | Trace_failed e -> let msg = format_error ~src:!last_src e in @@ -962,6 +1152,7 @@ let main () = let uuid = EcCommands.uuid () in if uuid > 0 then begin EcCommands.undo (uuid - 1); + transcript_trim (uuid - 1); reply_ok_goals () end else reply_error "nothing to undo" @@ -982,6 +1173,10 @@ let main () = Buffer.clear notices; reply_ok (tree_to_string ()) end + else if line = "COMMIT" then begin + Buffer.clear notices; + reply_ok (commit_proof_text ()) + end else if String.starts_with line "FOCUS " || line = "NEXT" then begin Buffer.clear notices; let request = @@ -1040,6 +1235,7 @@ let main () = "REVERT: uuid %d out of range [0, %d]" target uuid) else begin EcCommands.undo target; + transcript_trim target; reply_ok_goals () end end diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 5d3224969..cf1e740c2 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -969,23 +969,30 @@ let focus_goal (k : int) : (int, string) result = (* 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. *) -let disable_repl_bullets () = + 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 -> None | Some ctxt -> match EcScope.xgoal ctxt.ct_current with - | None -> () + | None -> None | Some puc -> match puc.EcScope.puc_active with - | None -> () - | Some (pac, _) when pac.EcScope.puc_bullets = None -> () + | None -> None | Some (pac, pct) -> - 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 } + 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 = @@ -1115,6 +1122,34 @@ let pp_current_goal ?(all = false) stream = 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 in_proof () then pp_current_goal ~all stream diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 611c57ca5..e36f6c4f1 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -64,9 +64,12 @@ 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 -> unit +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 diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 0ad46a2ae..753c924f5 100644 --- a/src/ecCoreGoal.ml +++ b/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 = { @@ -458,17 +462,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 @@ -991,9 +1002,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]; } @@ -1015,6 +1027,23 @@ 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 diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index 8dce48377..14b57e045 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -205,6 +205,12 @@ 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] From 037705de6b7b240c4db87fa071d56bb7e26230ef Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 10:54:50 +0200 Subject: [PATCH 07/11] [llm] extract REPL into a dedicated EcLlm module The LLM REPL accumulated ~870 lines of closures and refs inside [main]'s body, intermixed with the unrelated compile/runtest/docgen plumbing. Move it out into [src/ecLlm.ml] (with a one-line .mli exposing just [val run]). The implementation organises its closed-over state (notices buffer, transcript, prior-bullets snapshot, checkpoints, quiet flag, initialized flag) at the top of [run], then groups the helpers into nested submodules so each concern is named: - Goals goal/error formatting, focus tag, tree rendering - Wire OK/ERROR/ envelope and replies - Transcript transcript trimming and clearing - Commit bullet-token generator and DAG walk for COMMIT - Load LOAD parser, prefix processor, and -trace block [ec.ml] keeps the small [Llm] dispatch arm that calls [EcLlm.run ~relocdir ~boot llmopts]. Pure move, no behavioural change; smoke-tested with COMMIT, TREE, FOCUS, and -trace. --- src/ec.ml | 870 +------------------------------------------------- src/ecLlm.ml | 862 +++++++++++++++++++++++++++++++++++++++++++++++++ src/ecLlm.mli | 11 + 3 files changed, 874 insertions(+), 869 deletions(-) create mode 100644 src/ecLlm.ml create mode 100644 src/ecLlm.mli diff --git a/src/ec.ml b/src/ec.ml index 9a0b57d69..3a6d7bb34 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -404,874 +404,6 @@ let main () = (* Register user messages printers *) begin let open EcUserMessages in register () end; - (* -------------------------------------------------------------------- *) - (* LLM interactive mode *) - (* -------------------------------------------------------------------- *) - - let llm_guide_path () = - let (module Sites) = EcRelocate.sites in - match EcRelocate.sourceroot with - | Some root -> - Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" - | None -> - Filename.concat Sites.doc "llm-guide.md" - in - - let print_llm_guide () = - let path = llm_guide_path () in - try - let ic = open_in path in - begin try while true do - print_char (input_char ic) - done with End_of_file -> () end; - close_in ic - with Sys_error e -> - Printf.eprintf "cannot read LLM guide: %s\n%!" e - in - - let run_llm_repl (llmopts : llm_option) = - if llmopts.llmo_help then begin - print_llm_guide (); - exit 0 - end; - - let prvopts = llmopts.llmo_provers in - (* Initialize PRNG *) - Random.self_init (); - - (* Connect to external Why3 server if requested *) - prvopts.prvo_why3server |> oiter (fun server -> - try - Why3.Prove_client.connect_external server - with Why3.Prove_client.ConnectionError e -> - Format.eprintf - "cannot connect to Why3 server `%s': %s" server e; - exit 1); - - (* Add current directory to load path *) - (match relocdir with - | None -> EcCommands.addidir Filename.current_dir_name - | Some pwd -> EcCommands.addidir pwd); - - (* Proof engine configuration *) - let checkmode = { - EcCommands.cm_checkall = prvopts.prvo_checkall; - EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; - EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; - EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; - EcCommands.cm_provers = prvopts.prvo_provers; - EcCommands.cm_quorum = prvopts.prvo_quorum; - EcCommands.cm_profile = prvopts.prvo_profile; - } in - - (* Notice buffer: collects messages during command processing *) - let notices = Buffer.create 256 in - - let notifier (_ : EcGState.loglevel) (lazy msg) = - Buffer.add_string notices msg; - Buffer.add_char notices '\n' - in - - let initialized = ref false in - - let do_initialize () = - EcCommands.initialize - ~restart:!initialized ~undo:true - ~boot:ldropts.ldro_boot ~checkmode ~checkproof:true; - initialized := true; - (try - List.iter EcCommands.apply_pragma prvopts.prvo_pragmas - with EcCommands.InvalidPragma x -> - EcScope.hierror "invalid pragma: `%s'\n%!" x); - EcCommands.addnotifier notifier; - oiter (fun ppwidth -> - let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in - EcGState.setvalue "PP:width" (`Int ppwidth) gs) - prvopts.prvo_ppwidth - in - - (* Error formatting *) - let format_error ?(src="") e = - let base = match e with - | EcScope.TopError (loc, e) -> - let msg = String.strip (EcPException.tostring e) in - if loc = EcLocation._dummy then msg - else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg - | e -> - String.strip (EcPException.tostring e) - in - if src = "" then base - else Printf.sprintf "%s\nsource: %s" base src - in - - (* Output helpers *) - let goals_to_string ?(all=false) () = - let buf = Buffer.create 256 in - let fmt = Format.formatter_of_buffer buf in - EcCommands.pp_current_goal_or_noproof ~all fmt; - Format.pp_print_flush fmt (); - Buffer.contents buf - in - - (* Render the focus-tree of open subgoals. [all=false] gives a - one-line digest per goal (conclusion truncated); [all=true] - gives the full goal body for each. *) - let tree_to_string ?(all=false) () = - let entries = EcCommands.pp_tree ~all () in - match entries with - | [] -> "No active proof.\n" - | _ -> - let buf = Buffer.create 256 in - let one_line s = - let s = - match String.index_opt s '\n' with - | None -> s - | Some k -> String.sub s 0 k - in - let limit = 80 in - if String.length s > limit - then String.sub s 0 (limit - 1) ^ "…" - else s - in - List.iter (fun (i, focused, text) -> - let marker = if focused then " <- focused" else "" in - if all then - Buffer.add_string buf - (Printf.sprintf "[%d]%s\n%s\n" i marker text) - else - Buffer.add_string buf - (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) - ) entries; - Buffer.contents buf - in - - let quiet = ref false in - - let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in - - (* Transcript of REPL-typed phrases that succeeded. Each entry is - (uuid_before, src, parent, opens_at_entry), where: - - [parent] is the handle that was focused right before the - phrase ran ([None] iff outside a proof); - - [opens_at_entry] is the full open-handle list at entry time - (focused-first), used by COMMIT to seed the sibling map for - continuations whose first phrase already starts inside a - frame opened by the LOAD prefix. - Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) - let transcript : - (int * string * EcCoreGoal.handle option - * EcCoreGoal.handle list) list ref = ref [] in - - (* The bullet stack of the active proof at the moment REPL input - took over. Captured the first time [disable_repl_bullets] - actually clears a non-empty stack; subsequent (idempotent) - calls return [None] and leave this snapshot unchanged. Used by - [COMMIT] to pick bullet characters that don't collide with - tokens already in scope from the LOAD prefix. Cleared on - LOAD/Restart along with the transcript. *) - let prior_bullets : EcBullets.stack option ref = ref None in - - let transcript_trim target = - transcript := - List.filter - (fun (uuid_before, _, _, _) -> uuid_before < target) - !transcript - in - - (* Render the recorded transcript as a +strict_bullets-friendly - proof body. The algorithm reads the proof DAG via - [EcCommands.children_of]/[parent_of] (backed by [pr_parent], - which records the parent handle of every child at - [FApi.newgoal] time). Strategy: - - For each phrase, walk the subtree rooted at its parent - handle, finding every multi-child split, and register each - such child in [sibling_depth] at the corresponding depth. - Single-child links are continuations and don't bump depth. - - To decide whether a phrase needs a bullet, walk upward via - [parent_of] from its recorded parent until hitting a - registered sibling ancestor; if found, emit the bullet for - that depth and consume the registration. - Bullet tokens are chosen per depth, skipping any token - already in the LOAD prefix's [puc_bullets] stack (snapshotted - at the moment REPL input took over) so we never collide. *) - (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, - ---, +++, *** ... *) - let token_at_index i = - let chars = [| "-"; "+"; "*" |] in - let rep = i / 3 + 1 in - let chr = chars.(i mod 3) in - String.concat "" (List.init rep (fun _ -> chr)) - in - - let commit_proof_text () = - let entries = List.rev !transcript in - let buf = Buffer.create 1024 in - let emit_indent depth = - for _ = 1 to depth do Buffer.add_string buf " " done - in - let module Hmap = - Map.Make (struct - type t = EcCoreGoal.handle - let compare = compare - end) - in - let sibling_depth : int Hmap.t ref = ref Hmap.empty in - let current_depth = ref 0 in - (* Pick a bullet token for each depth, skipping tokens already - in scope from the LOAD prefix's bullet stack (so we never - collide with frames the prefix opened). State is per-COMMIT - so each invocation starts from a clean slate. *) - let in_use_tokens = - match !prior_bullets with - | None -> [] - | Some stack -> - List.map (fun (f : EcBullets.frame) -> f.bf_token) stack - in - let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in - let next_tok_idx = ref 0 in - let assigned_tokens = ref [] in - let bullet_for_depth d = - match Hashtbl.find_opt depth_cache d with - | Some t -> t - | None -> - let rec pick () = - let t = token_at_index !next_tok_idx in - incr next_tok_idx; - if List.mem t in_use_tokens || List.mem t !assigned_tokens - then pick () - else t - in - let t = pick () in - assigned_tokens := t :: !assigned_tokens; - Hashtbl.add depth_cache d t; - t - in - (* Seed: if the first recorded phrase entered a state with - multiple open goals, the LOAD prefix opened a frame whose - siblings are still pending. Register all of them as depth-1 - pending siblings so the first phrase's parent gets a bullet. *) - (match entries with - | (_, _, Some _, (_ :: _ :: _ as opens)) :: _ -> - List.iter - (fun h -> sibling_depth := Hmap.add h 1 !sibling_depth) - opens - | _ -> ()); - List.iter (fun (_uuid, src, parent_opt, _opens) -> - match parent_opt with - | None -> - Buffer.add_string buf src; - Buffer.add_char buf '\n' - | Some parent -> - (* Walk upward through pr_parent until we find a registered - sibling ancestor, or run out. If found, emit a bullet at - that depth and consume the registration. *) - let rec find_ancestor h = - match Hmap.find_opt h !sibling_depth with - | Some d -> Some (h, d) - | None -> - match EcCommands.parent_of h with - | Some p -> find_ancestor p - | None -> None - in - (match find_ancestor parent with - | Some (h, d) -> - emit_indent (d - 1); - Buffer.add_string buf (bullet_for_depth d); - Buffer.add_char buf ' '; - current_depth := d; - sibling_depth := Hmap.remove h !sibling_depth - | None -> - emit_indent !current_depth); - Buffer.add_string buf src; - Buffer.add_char buf '\n'; - (* A phrase can chain multiple sub-validations internally - (e.g. [move=> hp hq; split.] is VIntros -> VApply(split) - on a single recorded phrase). Walk single-child - validations until we hit a real split (>=2 children) or - an open leaf. *) - (* Walk the entire subtree rooted at [parent], finding every - multi-child node, and register its children at the - corresponding nesting depth. A compound phrase like - [split; split.] can produce nested splits within a single - phrase; both levels of children need to be registered. - Single-child links don't bump the depth (continuations); - multi-child links do. *) - let rec walk h d = - match EcCommands.children_of h with - | [c] -> walk c d - | (_ :: _ :: _) as cs -> - List.iter - (fun c -> - sibling_depth := - Hmap.add c d !sibling_depth; - walk c (d + 1)) - cs - | [] -> () - in - walk parent (!current_depth + 1) - ) entries; - Buffer.contents buf - in - - let reply_ok ?(tag="") body = - let n = Buffer.contents notices in - Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; - if n <> "" then print_string n; - if body <> "" then begin - print_string body; - let len = String.length body in - if len > 0 && body.[len - 1] <> '\n' then - print_char '\n' - end; - Printf.printf "\n%!"; - Buffer.clear notices - in - - let focus_tag () = - match EcCommands.pp_tree () with - | _ :: _ :: _ as entries -> - Printf.sprintf " [focus: 1/%d]" (List.length entries) - | _ -> "" - in - - let reply_ok_goals ?(all=false) () = - let tag = focus_tag () in - if !quiet then reply_ok ~tag "" - else reply_ok ~tag (goals_to_string ~all ()) - in - - let reply_error msg = - let goals = goals_to_string () in - Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; - if goals <> "" then begin - print_string goals; - let len = String.length goals in - if len > 0 && goals.[len - 1] <> '\n' then - print_char '\n' - end; - Printf.printf "\n%!"; - Buffer.clear notices - in - - (* Process a single EasyCrypt command, respecting gl_fail. When - [~record:true], capture the parent handle (the focused goal - before the phrase ran) and append a transcript entry on - success. COMMIT will use [EcCommands.children_of] on each - parent to walk the proof DAG and recover bullet structure. *) - let process_action ?(record=false) ~src (p : EP.global) = - let loc = p.EP.gl_action.EcLocation.pl_loc in - let pre_uuid = EcCommands.uuid () in - let opens_pre = - if record then EcCommands.open_handles () else [] - in - let parent = - match opens_pre with h :: _ -> Some h | [] -> None - in - let succeeded = ref false in - begin try - ignore (EcCommands.process ~src p.EP.gl_action : float option); - succeeded := true - with - | EcCommands.Restart -> raise EcCommands.Restart - | _ when p.EP.gl_fail -> () - | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) - end; - if !succeeded && p.EP.gl_fail then - raise (EcScope.toperror_of_exn ~gloc:loc - (EcScope.HiScopeError (None, - "this command is expected to fail"))); - if record && !succeeded && not p.EP.gl_fail then - transcript := (pre_uuid, src, parent, opens_pre) :: !transcript - in - - (* Process EasyCrypt input from a string (one parsed program) *) - let process_ec_input input = - Buffer.clear notices; - (* On the first REPL phrase of each proof, capture the bullet - stack that the LOAD prefix left so COMMIT can avoid token - collisions with it. Subsequent calls return [None] and don't - clobber the snapshot. *) - (match EcCommands.disable_repl_bullets () with - | None -> () - | Some _ as snapshot -> prior_bullets := snapshot); - let reader = EcIo.from_string input in - let last_src = ref "" in - begin try - let (src, prog) = EcIo.xparse reader in - let src = String.strip src in - last_src := src; - begin match EcLocation.unloc prog with - | EP.P_Prog (commands, _) -> - List.iter (process_action ~record:true ~src) commands; - reply_ok_goals () - | EP.P_Undo i -> - EcCommands.undo i; - transcript_trim i; - reply_ok_goals () - | EP.P_Exit -> - EcIo.finalize reader; exit 0 - | EP.P_DocComment doc -> - EcCommands.doc_comment doc; - reply_ok "" - end - with - | EcCommands.Restart -> - do_initialize (); - transcript := []; - prior_bullets := None; - reply_ok "Session restarted" - | e -> - reply_error (format_error ~src:!last_src e) - end; - EcIo.finalize reader - in - - (* Handle LOAD "file.ec" [LINE[:COL]] *) - let handle_load args = - Buffer.clear notices; - let args = String.strip args in - let last_src = ref "" in - let trace_prefix = ref "" in - let exception Trace_failed of exn in - - try - (* Parse quoted or unquoted filename *) - let filename, rest = - if String.length args > 0 && args.[0] = '"' then - let close = - try String.index_from args 1 '"' - with Not_found -> - failwith "LOAD: unterminated filename" - in - let fn = String.sub args 1 (close - 1) in - let rest = String.strip ( - String.sub args (close + 1) - (String.length args - close - 1)) in - (fn, rest) - else - match String.split_on_char ' ' args with - | [] -> failwith "LOAD: missing filename" - | [f] -> (f, "") - | f :: rest -> (f, String.concat " " rest) - in - - (* Parse optional LINE[:COL] and flags (-nosmt, -trace) *) - let upto, nosmt, trace = - let words = - String.split_on_char ' ' rest - |> List.filter (fun s -> s <> "") - in - let nosmt = List.mem "-nosmt" words in - let trace = List.mem "-trace" words in - let words = - List.filter - (fun s -> s <> "-nosmt" && s <> "-trace") - words - in - let upto = match words with - | [] -> None - | [w] -> - begin match String.split_on_char ':' w with - | [line] -> - Some (int_of_string line, None) - | [line; col] -> - Some (int_of_string line, Some (int_of_string col)) - | _ -> failwith "LOAD: invalid LINE[:COL] format" - end - | _ -> failwith "LOAD: unexpected arguments" - in - (upto, nosmt, trace) - in - - (* Validate file extension *) - begin try - ignore (EcLoader.getkind - (Filename.extension filename) : EcLoader.kind) - with EcLoader.BadExtension ext -> - failwith (Format.sprintf - "unknown file extension: %s" ext) - end; - - (* Reset proof engine and process file *) - do_initialize (); - Hashtbl.clear checkpoints; - transcript := []; - prior_bullets := None; - EcCommands.addidir (Filename.dirname filename); - - let reader = EcIo.from_file filename in - - let past_upto (loc : EcLocation.t) = - match upto with - | None -> false - | Some (line, col) -> - let (el, ec) = loc.loc_end in - el > line || (el = line && match col with - | None -> false - | Some c -> ec > c) - in - - let last_loc = ref None in - - (* For -trace: lazy whole-file bytes, used to slice the exact - source text of a sentence by byte offsets. *) - let input_bytes = lazy ( - let ic = open_in_bin filename in - let n = in_channel_length ic in - let b = Bytes.create n in - really_input ic b 0 n; - close_in ic; - Bytes.unsafe_to_string b) - in - let sentence_source (loc : EcLocation.t) = - let s = Lazy.force input_bytes in - let lo = max 0 loc.EcLocation.loc_bchar in - let hi = min (String.length s) loc.EcLocation.loc_echar in - if hi <= lo then "" else String.sub s lo (hi - lo) - in - - (* For -trace: defer execution of the last sentence within the - prefix so we can capture goals before and after it. *) - let pending : (string * EP.global) option ref = ref None in - let flush_pending () = - match !pending with - | None -> () - | Some (src, p) -> - last_src := src; - process_action ~src p; - last_loc := Some p.EP.gl_action.EcLocation.pl_loc; - pending := None - in - let step src p = - let loc = p.EP.gl_action.EcLocation.pl_loc in - if past_upto loc then raise Exit; - if trace then begin - flush_pending (); - pending := Some (src, p) - end else begin - last_src := src; - process_action ~src p; - last_loc := Some loc - end - in - - (* In -nosmt mode, admit all SMT calls during prefix loading *) - if nosmt then EcCommands.pragma_check `WeakCheck; - - begin try while true do - let (src, prog) = EcIo.xparse reader in - let src = String.strip src in - match EcLocation.unloc prog with - | EP.P_Prog (commands, locterm) -> - List.iter (step src) commands; - if locterm then raise Exit - | EP.P_Undo i -> - last_src := src; - EcCommands.undo i - | EP.P_Exit -> - raise Exit - | EP.P_DocComment doc -> - last_src := src; - EcCommands.doc_comment doc - done with - | Exit | End_of_file -> () - | e -> - EcIo.finalize reader; - if nosmt then EcCommands.pragma_check `Check; - raise e - end; - - EcIo.finalize reader; - - (* Restore full SMT checking for interactive tactics *) - if nosmt then EcCommands.pragma_check `Check; - - (* If -trace is set, the last in-prefix sentence is still - pending. Run it with goal capture before and after, and - build the BEFORE/TACTIC/AFTER/SUMMARY response body. *) - let body = - if not trace then - goals_to_string () - else - let pre_state = - match !pending with - | None -> `Nothing - | Some _ when not (EcCommands.in_proof ()) -> `NotInProof - | Some (src, p) -> `Ready (src, p) - in - match pre_state with - | `Nothing -> failwith "trace: nothing to trace" - | `NotInProof -> - failwith - "trace: target sentence is not in a proof context" - | `Ready (src, p) -> - let loc = p.EP.gl_action.EcLocation.pl_loc in - let (sl, sc) = loc.EcLocation.loc_start in - let (el, ec) = loc.EcLocation.loc_end in - let before_goals = EcCommands.pp_all_goals () in - let n1 = List.length before_goals in - let buf = Buffer.create 1024 in - let fmt = Format.formatter_of_buffer buf in - Format.fprintf fmt - "=== BEFORE: line %d (col %d) ===@\n" sl sc; - EcCommands.pp_current_goal_or_noproof ~all:false fmt; - Format.fprintf fmt - "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" - sl sc el ec (sentence_source loc); - last_src := src; - begin - try - process_action ~src p; - last_loc := Some loc; - pending := None; - let after_goals = EcCommands.pp_all_goals () in - let n2 = List.length after_goals in - Format.fprintf fmt - "=== AFTER: line %d (col %d) ===@\n" sl sc; - let before_set = - List.fold_left - (fun s g -> EcMaps.Sstr.add g s) - EcMaps.Sstr.empty before_goals - in - (* The new focused goal always counts as "modified" - (its focus status changed even if its text matches - an old sibling); the rest are printed only if - they didn't appear in BEFORE. *) - let to_print = - match after_goals with - | [] -> [] - | head :: tl -> - head :: - List.filter - (fun g -> not (EcMaps.Sstr.mem g before_set)) - tl - in - begin match to_print with - | [] -> Format.fprintf fmt "(no open goals)@\n" - | _ -> - List.iteri (fun i g -> - if i > 0 then Format.fprintf fmt "@\n"; - Format.fprintf fmt "%s@\n" g) - to_print - end; - Format.fprintf fmt - "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; - Format.pp_print_flush fmt (); - Buffer.contents buf - with e -> - Format.fprintf fmt - "=== AFTER: line %d (col %d) ===@\n@\n" - sl sc; - Format.pp_print_flush fmt (); - trace_prefix := Buffer.contents buf; - raise (Trace_failed e) - end - in - - let tag = - let loaded = - match !last_loc with - | None -> "" - | Some loc -> - let (el, _) = loc.EcLocation.loc_end in - Printf.sprintf " [loaded:%s:%d]" filename el - in - loaded ^ focus_tag () - in - reply_ok ~tag body - - with - | EcCommands.Restart -> - do_initialize (); - Hashtbl.clear checkpoints; - transcript := []; - prior_bullets := None; - reply_ok "Session restarted" - | Trace_failed e -> - let msg = format_error ~src:!last_src e in - reply_error (!trace_prefix ^ msg) - | Failure s -> - reply_error s - | e -> - reply_error (format_error ~src:!last_src e) - in - - (* Initialize proof engine *) - do_initialize (); - - (* Signal ready *) - Printf.printf "READY [uuid:%d]\n\n%!" - (EcCommands.uuid ()); - - (* Main REPL loop *) - let multi_buf = Buffer.create 256 in - let in_multi = ref false in - - begin try while true do - let line = input_line stdin in - let line = String.strip line in - - (* Multi-line input: starts, flushes *) - if line = "" then begin - Buffer.clear multi_buf; - in_multi := true - end - else if line = "" && !in_multi then begin - let input = Buffer.contents multi_buf in - Buffer.clear multi_buf; - in_multi := false; - if input <> "" then process_ec_input input - end - else if !in_multi then begin - if Buffer.length multi_buf > 0 then - Buffer.add_char multi_buf ' '; - Buffer.add_string multi_buf line - end - - else if line = "" then - () - else if line = "QUIT" then - exit 0 - else if line = "HELP" then begin - Buffer.clear notices; - let buf = Buffer.create 4096 in - let path = llm_guide_path () in - begin try - let ic = open_in path in - begin try while true do - Buffer.add_char buf (input_char ic) - done with End_of_file -> () end; - close_in ic; - reply_ok (Buffer.contents buf) - with Sys_error e -> - reply_error (Printf.sprintf "cannot read guide: %s" e) - end - end - else if line = "UNDO" then begin - Buffer.clear notices; - let uuid = EcCommands.uuid () in - if uuid > 0 then begin - EcCommands.undo (uuid - 1); - transcript_trim (uuid - 1); - reply_ok_goals () - end else - reply_error "nothing to undo" - end - else if line = "GOALS ALL" then begin - Buffer.clear notices; - reply_ok (goals_to_string ~all:true ()) - end - else if line = "GOALS" then begin - Buffer.clear notices; - reply_ok (goals_to_string ()) - end - else if line = "TREE ALL" then begin - Buffer.clear notices; - reply_ok (tree_to_string ~all:true ()) - end - else if line = "TREE" then begin - Buffer.clear notices; - reply_ok (tree_to_string ()) - end - else if line = "COMMIT" then begin - Buffer.clear notices; - reply_ok (commit_proof_text ()) - end - else if String.starts_with line "FOCUS " || line = "NEXT" then begin - Buffer.clear notices; - let request = - if line = "NEXT" then `Next - else - let arg = String.strip ( - String.sub line 6 (String.length line - 6)) in - try `At (int_of_string arg) - with Failure _ -> `Bad arg - in - match request with - | `Bad arg -> - reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) - | _ -> - let entries = EcCommands.pp_tree () in - let n = List.length entries in - let target = - match request with - | `Next -> if n <= 1 then 1 else 2 - | `At k -> k - | `Bad _ -> 1 - in - begin match EcCommands.focus_goal target with - | Ok _ -> reply_ok_goals () - | Error msg -> reply_error msg - end - end - else if String.starts_with line "CHECKPOINT " then begin - Buffer.clear notices; - let name = String.strip ( - String.sub line 11 (String.length line - 11)) in - if name = "" then - reply_error "CHECKPOINT: missing name" - else begin - Hashtbl.replace checkpoints name (EcCommands.uuid ()); - reply_ok (Printf.sprintf - "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) - end - end - else if String.starts_with line "REVERT " then begin - Buffer.clear notices; - let n = String.strip ( - String.sub line 7 (String.length line - 7)) in - let target = - try Some (int_of_string n) - with Failure _ -> Hashtbl.find_opt checkpoints n - in - begin match target with - | None -> - reply_error (Printf.sprintf - "REVERT: '%s' is not a valid uuid or checkpoint name" n) - | Some target -> - let uuid = EcCommands.uuid () in - if target < 0 || target > uuid then - reply_error (Printf.sprintf - "REVERT: uuid %d out of range [0, %d]" target uuid) - else begin - EcCommands.undo target; - transcript_trim target; - reply_ok_goals () - end - end - end - else if line = "QUIET ON" then begin - Buffer.clear notices; - quiet := true; - reply_ok "" - end - else if line = "QUIET OFF" then begin - Buffer.clear notices; - quiet := false; - reply_ok "" - end - else if String.starts_with line "SEARCH " then begin - let query = String.strip ( - String.sub line 7 (String.length line - 7)) in - let query = - if String.ends_with query "." - then String.sub query 0 (String.length query - 1) - else query - in - process_ec_input (Printf.sprintf "search %s." query) - end - else if String.starts_with line "LOAD " then - handle_load (String.sub line 5 (String.length line - 5)) - else - (* Treat as EasyCrypt input *) - process_ec_input line - done with - | End_of_file -> () - end; - - exit 0 - in - (* Initialize I/O + interaction module *) let module State = struct type t = { @@ -1404,7 +536,7 @@ let main () = end | `Llm llmopts -> - run_llm_repl llmopts + EcLlm.run ~relocdir ~boot:ldropts.ldro_boot llmopts | `Runtest _ -> (* Eagerly executed *) diff --git a/src/ecLlm.ml b/src/ecLlm.ml new file mode 100644 index 000000000..7b003a97a --- /dev/null +++ b/src/ecLlm.ml @@ -0,0 +1,862 @@ +(* -------------------------------------------------------------------- *) +(* The LLM coding-agent REPL. See [ecLlm.mli] for the entry point. + + Implementation note: the REPL holds a large amount of mutable state + (notice buffer, transcript, checkpoints, ...). To keep that state + sharable across the various helpers without resorting to a big + record, [run] is a single closure that opens nested [module] blocks + for grouping. The submodules are read-only views over the closed- + over refs. *) + +open EcUtils + +module EP = EcParsetree + +(* -------------------------------------------------------------------- *) +(* Path to the bundled LLM-agent guide. *) +let llm_guide_path () = + let (module Sites) = EcRelocate.sites in + match EcRelocate.sourceroot with + | Some root -> + Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" + | None -> + Filename.concat Sites.doc "llm-guide.md" + +(* Print the bundled guide to stdout. Used by [-help]. *) +let print_llm_guide () = + let path = llm_guide_path () in + try + let ic = open_in path in + begin try while true do + print_char (input_char ic) + done with End_of_file -> () end; + close_in ic + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + +(* -------------------------------------------------------------------- *) +let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = + if llmopts.llmo_help then begin + print_llm_guide (); + exit 0 + end; + + let prvopts = llmopts.llmo_provers in + Random.self_init (); + + prvopts.prvo_why3server |> oiter (fun server -> + try + Why3.Prove_client.connect_external server + with Why3.Prove_client.ConnectionError e -> + Format.eprintf + "cannot connect to Why3 server `%s': %s" server e; + exit 1); + + (match relocdir with + | None -> EcCommands.addidir Filename.current_dir_name + | Some pwd -> EcCommands.addidir pwd); + + let checkmode = { + EcCommands.cm_checkall = prvopts.prvo_checkall; + EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; + EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; + EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; + EcCommands.cm_provers = prvopts.prvo_provers; + EcCommands.cm_quorum = prvopts.prvo_quorum; + EcCommands.cm_profile = prvopts.prvo_profile; + } in + + (* ------------------------------------------------------------------ *) + (* State. *) + + (* Messages emitted by the engine during a phrase; flushed into the + next OK/ERROR reply. *) + let notices = Buffer.create 256 in + + (* Has [EcCommands.initialize] been called? Subsequent calls pass + [~restart:true]. *) + let initialized = ref false in + + (* True iff replies should suppress goal bodies. Toggled by QUIET. *) + let quiet = ref false in + + (* CHECKPOINT name -> uuid. *) + let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + + (* Transcript of REPL-typed phrases that succeeded. Each entry is + [(uuid_before, src, parent, opens_at_entry)]: + - [parent]: focused handle right before the phrase ([None] iff + outside a proof); + - [opens_at_entry]: full open-handle list (focused first), used + by [Commit] to seed the sibling map when the first recorded + phrase already sits inside a frame opened by the LOAD prefix. + Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) + let transcript : + (int * string * EcCoreGoal.handle option + * EcCoreGoal.handle list) list ref = ref [] in + + (* The bullet stack of the active proof at the moment REPL input + took over. Captured the first time [disable_repl_bullets] clears + a non-empty stack. Used by [Commit] to pick bullet characters + that don't collide with frames opened by the LOAD prefix. + Cleared with the transcript on LOAD/Restart. *) + let prior_bullets : EcBullets.stack option ref = ref None in + + let notifier (_ : EcGState.loglevel) (lazy msg) = + Buffer.add_string notices msg; + Buffer.add_char notices '\n' + in + + let do_initialize () = + EcCommands.initialize + ~restart:!initialized ~undo:true + ~boot ~checkmode ~checkproof:true; + initialized := true; + (try + List.iter EcCommands.apply_pragma prvopts.prvo_pragmas + with EcCommands.InvalidPragma x -> + EcScope.hierror "invalid pragma: `%s'\n%!" x); + EcCommands.addnotifier notifier; + oiter (fun ppwidth -> + let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in + EcGState.setvalue "PP:width" (`Int ppwidth) gs) + prvopts.prvo_ppwidth + in + + (* ------------------------------------------------------------------ *) + (* Goal/error formatting: shared between the wire layer and the + -trace block. *) + let module Goals = struct + let format_error ?(src="") e = + let base = match e with + | EcScope.TopError (loc, e) -> + let msg = String.strip (EcPException.tostring e) in + if loc = EcLocation._dummy then msg + else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg + | e -> + String.strip (EcPException.tostring e) + in + if src = "" then base + else Printf.sprintf "%s\nsource: %s" base src + + let goals_to_string ?(all=false) () = + let buf = Buffer.create 256 in + let fmt = Format.formatter_of_buffer buf in + EcCommands.pp_current_goal_or_noproof ~all fmt; + Format.pp_print_flush fmt (); + Buffer.contents buf + + (* Render the focus-tree of open subgoals. [all=false] gives a + one-line digest per goal; [all=true] gives the full goal body. *) + let tree_to_string ?(all=false) () = + let entries = EcCommands.pp_tree ~all () in + match entries with + | [] -> "No active proof.\n" + | _ -> + let buf = Buffer.create 256 in + let one_line s = + let s = + match String.index_opt s '\n' with + | None -> s + | Some k -> String.sub s 0 k + in + let limit = 80 in + if String.length s > limit + then String.sub s 0 (limit - 1) ^ "…" + else s + in + List.iter (fun (i, focused, text) -> + let marker = if focused then " <- focused" else "" in + if all then + Buffer.add_string buf + (Printf.sprintf "[%d]%s\n%s\n" i marker text) + else + Buffer.add_string buf + (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) + ) entries; + Buffer.contents buf + + (* Inline focus annotation ([focus: 1/N]) appended to reply tags + whenever the active proof has >=2 open subgoals. *) + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" + end in + + (* ------------------------------------------------------------------ *) + (* OK/ERROR/ wire envelope. *) + let module Wire = struct + let reply_ok ?(tag="") body = + let n = Buffer.contents notices in + Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; + if n <> "" then print_string n; + if body <> "" then begin + print_string body; + let len = String.length body in + if len > 0 && body.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + + let reply_ok_goals ?(all=false) () = + let tag = Goals.focus_tag () in + if !quiet then reply_ok ~tag "" + else reply_ok ~tag (Goals.goals_to_string ~all ()) + + let reply_error msg = + let goals = Goals.goals_to_string () in + Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; + if goals <> "" then begin + print_string goals; + let len = String.length goals in + if len > 0 && goals.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + end in + + (* ------------------------------------------------------------------ *) + (* Transcript manipulation. *) + let module Transcript = struct + let trim target = + transcript := + List.filter + (fun (uuid_before, _, _, _) -> uuid_before < target) + !transcript + + let clear () = + transcript := []; + prior_bullets := None + end in + + (* ------------------------------------------------------------------ *) + (* Process a single EasyCrypt command, respecting [gl_fail]. When + [~record:true], append a transcript entry on success: the parent + handle (focused goal before the phrase) and the open-handle list, + which together let [Commit] reconstruct bullet structure. *) + let process_action ?(record=false) ~src (p : EP.global) = + let loc = p.EP.gl_action.EcLocation.pl_loc in + let pre_uuid = EcCommands.uuid () in + let opens_pre = + if record then EcCommands.open_handles () else [] + in + let parent = + match opens_pre with h :: _ -> Some h | [] -> None + in + let succeeded = ref false in + begin try + ignore (EcCommands.process ~src p.EP.gl_action : float option); + succeeded := true + with + | EcCommands.Restart -> raise EcCommands.Restart + | _ when p.EP.gl_fail -> () + | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) + end; + if !succeeded && p.EP.gl_fail then + raise (EcScope.toperror_of_exn ~gloc:loc + (EcScope.HiScopeError (None, + "this command is expected to fail"))); + if record && !succeeded && not p.EP.gl_fail then + transcript := (pre_uuid, src, parent, opens_pre) :: !transcript + in + + (* ------------------------------------------------------------------ *) + (* COMMIT: replay the transcript against the proof DAG (parent_of / + children_of, backed by [EcCoreGoal.pr_parent]), inserting bullets + at multi-child splits. Bullet tokens skip any character already on + the LOAD prefix's [puc_bullets] stack so emitted bullets cannot + collide with frames opened by the prefix. *) + let module Commit = struct + (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, + ---, +++, *** ... *) + let token_at_index i = + let chars = [| "-"; "+"; "*" |] in + let rep = i / 3 + 1 in + let chr = chars.(i mod 3) in + String.concat "" (List.init rep (fun _ -> chr)) + + let proof_text () = + let entries = List.rev !transcript in + let buf = Buffer.create 1024 in + let emit_indent depth = + for _ = 1 to depth do Buffer.add_string buf " " done + in + let module Hmap = + Map.Make (struct + type t = EcCoreGoal.handle + let compare = compare + end) + in + let sibling_depth : int Hmap.t ref = ref Hmap.empty in + let current_depth = ref 0 in + (* Pick a bullet token for each depth, skipping tokens already + in scope from the LOAD prefix's bullet stack. *) + let in_use_tokens = + match !prior_bullets with + | None -> [] + | Some stack -> + List.map (fun (f : EcBullets.frame) -> f.bf_token) stack + in + let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in + let next_tok_idx = ref 0 in + let assigned_tokens = ref [] in + let bullet_for_depth d = + match Hashtbl.find_opt depth_cache d with + | Some t -> t + | None -> + let rec pick () = + let t = token_at_index !next_tok_idx in + incr next_tok_idx; + if List.mem t in_use_tokens || List.mem t !assigned_tokens + then pick () + else t + in + let t = pick () in + assigned_tokens := t :: !assigned_tokens; + Hashtbl.add depth_cache d t; + t + in + (* Seed: if the first recorded phrase entered a state with + multiple open goals, the LOAD prefix opened a frame whose + siblings are still pending. Register all of them at depth 1 + so the first phrase's parent gets a bullet. *) + (match entries with + | (_, _, Some _, (_ :: _ :: _ as opens)) :: _ -> + List.iter + (fun h -> sibling_depth := Hmap.add h 1 !sibling_depth) + opens + | _ -> ()); + List.iter (fun (_uuid, src, parent_opt, _opens) -> + match parent_opt with + | None -> + Buffer.add_string buf src; + Buffer.add_char buf '\n' + | Some parent -> + (* Walk upward via pr_parent until we hit a registered + sibling ancestor. If found, emit its bullet and consume + the registration. *) + let rec find_ancestor h = + match Hmap.find_opt h !sibling_depth with + | Some d -> Some (h, d) + | None -> + match EcCommands.parent_of h with + | Some p -> find_ancestor p + | None -> None + in + (match find_ancestor parent with + | Some (h, d) -> + emit_indent (d - 1); + Buffer.add_string buf (bullet_for_depth d); + Buffer.add_char buf ' '; + current_depth := d; + sibling_depth := Hmap.remove h !sibling_depth + | None -> + emit_indent !current_depth); + Buffer.add_string buf src; + Buffer.add_char buf '\n'; + (* Register fresh siblings: walk the subtree rooted at + [parent], finding every multi-child split, and register + each such child at the right depth. Single-child links + are continuations and don't bump depth; multi-child + links do. A compound phrase like [split; split.] can + produce nested splits within one phrase. *) + let rec walk h d = + match EcCommands.children_of h with + | [c] -> walk c d + | (_ :: _ :: _) as cs -> + List.iter + (fun c -> + sibling_depth := + Hmap.add c d !sibling_depth; + walk c (d + 1)) + cs + | [] -> () + in + walk parent (!current_depth + 1) + ) entries; + Buffer.contents buf + end in + + (* ------------------------------------------------------------------ *) + (* Process EasyCrypt input typed at the REPL prompt (single phrase + or a line ending with a "."). *) + let process_ec_input input = + Buffer.clear notices; + (* On the first REPL phrase of each proof, capture the bullet stack + the LOAD prefix left so COMMIT can avoid token collisions with + it. Subsequent calls return [None] and don't clobber the snapshot. *) + (match EcCommands.disable_repl_bullets () with + | None -> () + | Some _ as snapshot -> prior_bullets := snapshot); + let reader = EcIo.from_string input in + let last_src = ref "" in + begin try + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + begin match EcLocation.unloc prog with + | EP.P_Prog (commands, _) -> + List.iter (process_action ~record:true ~src) commands; + Wire.reply_ok_goals () + | EP.P_Undo i -> + EcCommands.undo i; + Transcript.trim i; + Wire.reply_ok_goals () + | EP.P_Exit -> + EcIo.finalize reader; exit 0 + | EP.P_DocComment doc -> + EcCommands.doc_comment doc; + Wire.reply_ok "" + end + with + | EcCommands.Restart -> + do_initialize (); + Transcript.clear (); + Wire.reply_ok "Session restarted" + | e -> + Wire.reply_error (Goals.format_error ~src:!last_src e) + end; + EcIo.finalize reader + in + + (* ------------------------------------------------------------------ *) + (* LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]. *) + let module Load = struct + let handle args = + Buffer.clear notices; + let args = String.strip args in + let last_src = ref "" in + let trace_prefix = ref "" in + let exception Trace_failed of exn in + + try + (* Parse quoted or unquoted filename. *) + let filename, rest = + if String.length args > 0 && args.[0] = '"' then + let close = + try String.index_from args 1 '"' + with Not_found -> + failwith "LOAD: unterminated filename" + in + let fn = String.sub args 1 (close - 1) in + let rest = String.strip ( + String.sub args (close + 1) + (String.length args - close - 1)) in + (fn, rest) + else + match String.split_on_char ' ' args with + | [] -> failwith "LOAD: missing filename" + | [f] -> (f, "") + | f :: rest -> (f, String.concat " " rest) + in + + (* Parse optional LINE[:COL] and flags (-nosmt, -trace). *) + let upto, nosmt, trace = + let words = + String.split_on_char ' ' rest + |> List.filter (fun s -> s <> "") + in + let nosmt = List.mem "-nosmt" words in + let trace = List.mem "-trace" words in + let words = + List.filter + (fun s -> s <> "-nosmt" && s <> "-trace") + words + in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt, trace) + in + + begin try + ignore (EcLoader.getkind + (Filename.extension filename) : EcLoader.kind) + with EcLoader.BadExtension ext -> + failwith (Format.sprintf + "unknown file extension: %s" ext) + end; + + do_initialize (); + Hashtbl.clear checkpoints; + Transcript.clear (); + EcCommands.addidir (Filename.dirname filename); + + let reader = EcIo.from_file filename in + + let past_upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + in + + let last_loc = ref None in + + (* For -trace: lazy whole-file bytes, used to slice the exact + source text of a sentence by byte offsets. *) + let input_bytes = lazy ( + let ic = open_in_bin filename in + let n = in_channel_length ic in + let b = Bytes.create n in + really_input ic b 0 n; + close_in ic; + Bytes.unsafe_to_string b) + in + let sentence_source (loc : EcLocation.t) = + let s = Lazy.force input_bytes in + let lo = max 0 loc.EcLocation.loc_bchar in + let hi = min (String.length s) loc.EcLocation.loc_echar in + if hi <= lo then "" else String.sub s lo (hi - lo) + in + + (* For -trace: defer execution of the last sentence within the + prefix so we can capture goals before and after it. *) + let pending : (string * EP.global) option ref = ref None in + let flush_pending () = + match !pending with + | None -> () + | Some (src, p) -> + last_src := src; + process_action ~src p; + last_loc := Some p.EP.gl_action.EcLocation.pl_loc; + pending := None + in + let step src p = + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + if trace then begin + flush_pending (); + pending := Some (src, p) + end else begin + last_src := src; + process_action ~src p; + last_loc := Some loc + end + in + + if nosmt then EcCommands.pragma_check `WeakCheck; + + begin try while true do + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter (step src) commands; + if locterm then raise Exit + | EP.P_Undo i -> + last_src := src; + EcCommands.undo i + | EP.P_Exit -> + raise Exit + | EP.P_DocComment doc -> + last_src := src; + EcCommands.doc_comment doc + done with + | Exit | End_of_file -> () + | e -> + EcIo.finalize reader; + if nosmt then EcCommands.pragma_check `Check; + raise e + end; + + EcIo.finalize reader; + + if nosmt then EcCommands.pragma_check `Check; + + (* If -trace is set, the last in-prefix sentence is still + pending. Run it under goal capture and build the + BEFORE/TACTIC/AFTER/SUMMARY response body. *) + let body = + if not trace then + Goals.goals_to_string () + else + let pre_state = + match !pending with + | None -> `Nothing + | Some _ when not (EcCommands.in_proof ()) -> `NotInProof + | Some (src, p) -> `Ready (src, p) + in + match pre_state with + | `Nothing -> failwith "trace: nothing to trace" + | `NotInProof -> + failwith + "trace: target sentence is not in a proof context" + | `Ready (src, p) -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + let (sl, sc) = loc.EcLocation.loc_start in + let (el, ec) = loc.EcLocation.loc_end in + let before_goals = EcCommands.pp_all_goals () in + let n1 = List.length before_goals in + let buf = Buffer.create 1024 in + let fmt = Format.formatter_of_buffer buf in + Format.fprintf fmt + "=== BEFORE: line %d (col %d) ===@\n" sl sc; + EcCommands.pp_current_goal_or_noproof ~all:false fmt; + Format.fprintf fmt + "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" + sl sc el ec (sentence_source loc); + last_src := src; + begin + try + process_action ~src p; + last_loc := Some loc; + pending := None; + let after_goals = EcCommands.pp_all_goals () in + let n2 = List.length after_goals in + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n" sl sc; + let before_set = + List.fold_left + (fun s g -> EcMaps.Sstr.add g s) + EcMaps.Sstr.empty before_goals + in + (* The new focused goal always counts as "modified" + (its focus status changed even if its text matches + an old sibling); the rest are printed only if they + didn't appear in BEFORE. *) + let to_print = + match after_goals with + | [] -> [] + | head :: tl -> + head :: + List.filter + (fun g -> not (EcMaps.Sstr.mem g before_set)) + tl + in + begin match to_print with + | [] -> Format.fprintf fmt "(no open goals)@\n" + | _ -> + List.iteri (fun i g -> + if i > 0 then Format.fprintf fmt "@\n"; + Format.fprintf fmt "%s@\n" g) + to_print + end; + Format.fprintf fmt + "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; + Format.pp_print_flush fmt (); + Buffer.contents buf + with e -> + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n@\n" + sl sc; + Format.pp_print_flush fmt (); + trace_prefix := Buffer.contents buf; + raise (Trace_failed e) + end + in + + let tag = + let loaded = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + loaded ^ Goals.focus_tag () + in + Wire.reply_ok ~tag body + + with + | EcCommands.Restart -> + do_initialize (); + Hashtbl.clear checkpoints; + Transcript.clear (); + Wire.reply_ok "Session restarted" + | Trace_failed e -> + let msg = Goals.format_error ~src:!last_src e in + Wire.reply_error (!trace_prefix ^ msg) + | Failure s -> + Wire.reply_error s + | e -> + Wire.reply_error (Goals.format_error ~src:!last_src e) + end in + + (* ------------------------------------------------------------------ *) + (* Main loop: line-by-line dispatcher. *) + + do_initialize (); + + Printf.printf "READY [uuid:%d]\n\n%!" (EcCommands.uuid ()); + + let multi_buf = Buffer.create 256 in + let in_multi = ref false in + + begin try while true do + let line = input_line stdin in + let line = String.strip line in + + if line = "" then begin + Buffer.clear multi_buf; + in_multi := true + end + else if line = "" && !in_multi then begin + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + end + else if !in_multi then begin + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf line + end + + else if line = "" then + () + else if line = "QUIT" then + exit 0 + else if line = "HELP" then begin + Buffer.clear notices; + let buf = Buffer.create 4096 in + let path = llm_guide_path () in + begin try + let ic = open_in path in + begin try while true do + Buffer.add_char buf (input_char ic) + done with End_of_file -> () end; + close_in ic; + Wire.reply_ok (Buffer.contents buf) + with Sys_error e -> + Wire.reply_error (Printf.sprintf "cannot read guide: %s" e) + end + end + else if line = "UNDO" then begin + Buffer.clear notices; + let uuid = EcCommands.uuid () in + if uuid > 0 then begin + EcCommands.undo (uuid - 1); + Transcript.trim (uuid - 1); + Wire.reply_ok_goals () + end else + Wire.reply_error "nothing to undo" + end + else if line = "GOALS ALL" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ~all:true ()) + end + else if line = "GOALS" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ()) + end + else if line = "TREE ALL" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ~all:true ()) + end + else if line = "TREE" then begin + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ()) + end + else if line = "COMMIT" then begin + Buffer.clear notices; + Wire.reply_ok (Commit.proof_text ()) + end + else if String.starts_with line "FOCUS " || line = "NEXT" then begin + Buffer.clear notices; + let request = + if line = "NEXT" then `Next + else + let arg = String.strip ( + String.sub line 6 (String.length line - 6)) in + try `At (int_of_string arg) + with Failure _ -> `Bad arg + in + match request with + | `Bad arg -> + Wire.reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) + | _ -> + let entries = EcCommands.pp_tree () in + let n = List.length entries in + let target = + match request with + | `Next -> if n <= 1 then 1 else 2 + | `At k -> k + | `Bad _ -> 1 + in + begin match EcCommands.focus_goal target with + | Ok _ -> Wire.reply_ok_goals () + | Error msg -> Wire.reply_error msg + end + end + else if String.starts_with line "CHECKPOINT " then begin + Buffer.clear notices; + let name = String.strip ( + String.sub line 11 (String.length line - 11)) in + if name = "" then + Wire.reply_error "CHECKPOINT: missing name" + else begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + Wire.reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + end + end + else if String.starts_with line "REVERT " then begin + Buffer.clear notices; + let n = String.strip ( + String.sub line 7 (String.length line - 7)) in + let target = + try Some (int_of_string n) + with Failure _ -> Hashtbl.find_opt checkpoints n + in + begin match target with + | None -> + Wire.reply_error (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" n) + | Some target -> + let uuid = EcCommands.uuid () in + if target < 0 || target > uuid then + Wire.reply_error (Printf.sprintf + "REVERT: uuid %d out of range [0, %d]" target uuid) + else begin + EcCommands.undo target; + Transcript.trim target; + Wire.reply_ok_goals () + end + end + end + else if line = "QUIET ON" then begin + Buffer.clear notices; + quiet := true; + Wire.reply_ok "" + end + else if line = "QUIET OFF" then begin + Buffer.clear notices; + quiet := false; + Wire.reply_ok "" + end + else if String.starts_with line "SEARCH " then begin + let query = String.strip ( + String.sub line 7 (String.length line - 7)) in + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + process_ec_input (Printf.sprintf "search %s." query) + end + else if String.starts_with line "LOAD " then + Load.handle (String.sub line 5 (String.length line - 5)) + else + process_ec_input line + done with + | End_of_file -> () + end; + + exit 0 diff --git a/src/ecLlm.mli b/src/ecLlm.mli new file mode 100644 index 000000000..b12dde1ef --- /dev/null +++ b/src/ecLlm.mli @@ -0,0 +1,11 @@ +(* -------------------------------------------------------------------- *) +(* The LLM coding-agent REPL: an interactive proof-development protocol + over stdin/stdout. Driven via the [easycrypt llm] command. *) + +(* Run the REPL until [QUIT] or EOF, then exit the process. Never + returns. *) +val run : + relocdir:string option + -> boot:bool + -> EcOptions.llm_option + -> 'a From 969bae20ec2f8310d2f49673bad61a5dcd0373f8 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 30 May 2026 11:01:59 +0200 Subject: [PATCH 08/11] [llm] split REPL dispatcher into Parse and Dispatch submodules The main loop was a flat ~150-line if/else chain that mixed line parsing (substrings, int_of_string, String.starts_with checks) with the actions to take. Split into: module Parse: a [command] variant covering every accepted line shape (Quit, Help, Undo, Goals of [`One|`All], Tree of [`One|`All], Commit, Focus of int, Next, Checkpoint of string, Revert of string, Quiet of bool, Search of string, Load of string, Ec of string, Begin_multi, Done_multi, Multi_line of string, Blank), plus [of_line ~multi_active] which is a stateless string -> command, and [Parse_error] for argument-shape mistakes (e.g. "FOCUS foo"). module Dispatch: a flat pattern match on the parsed command, delegating to small handlers (do_help, do_undo, do_focus_request, do_checkpoint, do_revert, do_quiet, do_search) and to the existing Load/Commit/Goals submodules. Holds the multi-line buffer state (multi_buf/in_multi) since Parse is pure. The main loop becomes 9 lines: read a line, parse to a command, dispatch, catch Parse_error and reply ERROR. Behaviour is unchanged; manual smoke tests cover COMMIT, TREE, FOCUS (good and bad arg), CHECKPOINT/REVERT, SEARCH, multi-line input, and the prior-bullets collision case. --- src/ecLlm.ml | 301 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 184 insertions(+), 117 deletions(-) diff --git a/src/ecLlm.ml b/src/ecLlm.ml index 7b003a97a..51a85ef02 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -692,38 +692,99 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = (* ------------------------------------------------------------------ *) (* Main loop: line-by-line dispatcher. *) - do_initialize (); + (* ------------------------------------------------------------------ *) + (* Surface command vocabulary. Parsing turns each stdin line into one + of these, and dispatch is a flat pattern-match. Argument + parsing/validation lives in [Parse]; commands that interact with + mutable state (checkpoints table, multi-line buffer) carry only + the raw user-supplied data and let [Dispatch] do the lookup. *) + let module Parse = struct + type command = + | Quit + | Help + | Undo + | Goals of [`One | `All] + | Tree of [`One | `All] + | Commit + | Focus of int + | Next + | Checkpoint of string + | Revert of string (* uuid-or-name; Dispatch resolves *) + | Quiet of bool + | Search of string (* trailing "." already stripped *) + | Load of string (* raw arg tail; Load.handle parses *) + | Ec of string (* fall-through: raw EasyCrypt input *) + | Begin_multi + | Done_multi + | Multi_line of string + | Blank + + exception Parse_error of string + + let rest n line = + String.strip (String.sub line n (String.length line - n)) + + let parse_focus arg = + try Focus (int_of_string arg) + with Failure _ -> + raise (Parse_error + (Printf.sprintf "FOCUS: not an integer: %s" arg)) + + let parse_checkpoint name = + if name = "" then + raise (Parse_error "CHECKPOINT: missing name"); + Checkpoint name - Printf.printf "READY [uuid:%d]\n\n%!" (EcCommands.uuid ()); + let parse_search query = + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + Search query + + let of_line ~multi_active (raw : string) : command = + let line = String.strip raw in + if multi_active then + if line = "" then Done_multi + else Multi_line line + else + match line with + | "" -> Begin_multi + | "" -> Blank + | "QUIT" -> Quit + | "HELP" -> Help + | "UNDO" -> Undo + | "GOALS" -> Goals `One + | "GOALS ALL" -> Goals `All + | "TREE" -> Tree `One + | "TREE ALL" -> Tree `All + | "COMMIT" -> Commit + | "NEXT" -> Next + | "QUIET ON" -> Quiet true + | "QUIET OFF" -> Quiet false + | _ when String.starts_with line "FOCUS " -> + parse_focus (rest 6 line) + | _ when String.starts_with line "CHECKPOINT " -> + parse_checkpoint (rest 11 line) + | _ when String.starts_with line "REVERT " -> + Revert (rest 7 line) + | _ when String.starts_with line "SEARCH " -> + parse_search (rest 7 line) + | _ when String.starts_with line "LOAD " -> + Load (rest 5 line) + | _ -> Ec line + end in + (* ------------------------------------------------------------------ *) + (* Command handlers. Each takes (already-parsed) data and produces a + wire reply via [Wire] (or exits the process). Multi-line state is + held here so [Parse] can stay pure. *) let multi_buf = Buffer.create 256 in - let in_multi = ref false in - - begin try while true do - let line = input_line stdin in - let line = String.strip line in + let in_multi = ref false in - if line = "" then begin - Buffer.clear multi_buf; - in_multi := true - end - else if line = "" && !in_multi then begin - let input = Buffer.contents multi_buf in - Buffer.clear multi_buf; - in_multi := false; - if input <> "" then process_ec_input input - end - else if !in_multi then begin - if Buffer.length multi_buf > 0 then - Buffer.add_char multi_buf ' '; - Buffer.add_string multi_buf line - end - - else if line = "" then - () - else if line = "QUIT" then - exit 0 - else if line = "HELP" then begin + let module Dispatch = struct + let do_help () = Buffer.clear notices; let buf = Buffer.create 4096 in let path = llm_guide_path () in @@ -737,8 +798,8 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = with Sys_error e -> Wire.reply_error (Printf.sprintf "cannot read guide: %s" e) end - end - else if line = "UNDO" then begin + + let do_undo () = Buffer.clear notices; let uuid = EcCommands.uuid () in if uuid > 0 then begin @@ -747,78 +808,38 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Wire.reply_ok_goals () end else Wire.reply_error "nothing to undo" - end - else if line = "GOALS ALL" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.goals_to_string ~all:true ()) - end - else if line = "GOALS" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.goals_to_string ()) - end - else if line = "TREE ALL" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ~all:true ()) - end - else if line = "TREE" then begin - Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ()) - end - else if line = "COMMIT" then begin - Buffer.clear notices; - Wire.reply_ok (Commit.proof_text ()) - end - else if String.starts_with line "FOCUS " || line = "NEXT" then begin + + let do_focus_request request = + (* [request] is the user's intent normalized; [`Next] is "second + sibling unless only one open". *) Buffer.clear notices; - let request = - if line = "NEXT" then `Next - else - let arg = String.strip ( - String.sub line 6 (String.length line - 6)) in - try `At (int_of_string arg) - with Failure _ -> `Bad arg + let entries = EcCommands.pp_tree () in + let n = List.length entries in + let target = + match request with + | `Next -> if n <= 1 then 1 else 2 + | `At k -> k in - match request with - | `Bad arg -> - Wire.reply_error (Printf.sprintf "FOCUS: not an integer: %s" arg) - | _ -> - let entries = EcCommands.pp_tree () in - let n = List.length entries in - let target = - match request with - | `Next -> if n <= 1 then 1 else 2 - | `At k -> k - | `Bad _ -> 1 - in - begin match EcCommands.focus_goal target with - | Ok _ -> Wire.reply_ok_goals () - | Error msg -> Wire.reply_error msg - end - end - else if String.starts_with line "CHECKPOINT " then begin + match EcCommands.focus_goal target with + | Ok _ -> Wire.reply_ok_goals () + | Error msg -> Wire.reply_error msg + + let do_checkpoint name = Buffer.clear notices; - let name = String.strip ( - String.sub line 11 (String.length line - 11)) in - if name = "" then - Wire.reply_error "CHECKPOINT: missing name" - else begin - Hashtbl.replace checkpoints name (EcCommands.uuid ()); - Wire.reply_ok (Printf.sprintf - "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) - end - end - else if String.starts_with line "REVERT " then begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + Wire.reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + + let do_revert spec = Buffer.clear notices; - let n = String.strip ( - String.sub line 7 (String.length line - 7)) in let target = - try Some (int_of_string n) - with Failure _ -> Hashtbl.find_opt checkpoints n + try Some (int_of_string spec) + with Failure _ -> Hashtbl.find_opt checkpoints spec in - begin match target with + match target with | None -> Wire.reply_error (Printf.sprintf - "REVERT: '%s' is not a valid uuid or checkpoint name" n) + "REVERT: '%s' is not a valid uuid or checkpoint name" spec) | Some target -> let uuid = EcCommands.uuid () in if target < 0 || target > uuid then @@ -829,32 +850,78 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Transcript.trim target; Wire.reply_ok_goals () end - end - end - else if line = "QUIET ON" then begin - Buffer.clear notices; - quiet := true; - Wire.reply_ok "" - end - else if line = "QUIET OFF" then begin + + let do_quiet on = Buffer.clear notices; - quiet := false; + quiet := on; Wire.reply_ok "" - end - else if String.starts_with line "SEARCH " then begin - let query = String.strip ( - String.sub line 7 (String.length line - 7)) in - let query = - if String.ends_with query "." - then String.sub query 0 (String.length query - 1) - else query - in + + let do_search query = process_ec_input (Printf.sprintf "search %s." query) - end - else if String.starts_with line "LOAD " then - Load.handle (String.sub line 5 (String.length line - 5)) - else - process_ec_input line + + let do_begin_multi () = + Buffer.clear multi_buf; + in_multi := true + + let do_done_multi () = + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + + let do_multi_line s = + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf s + + let run (cmd : Parse.command) = + match cmd with + | Blank -> () + | Quit -> exit 0 + | Help -> do_help () + | Undo -> do_undo () + | Goals `One -> + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ()) + | Goals `All -> + Buffer.clear notices; + Wire.reply_ok (Goals.goals_to_string ~all:true ()) + | Tree `One -> + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ()) + | Tree `All -> + Buffer.clear notices; + Wire.reply_ok (Goals.tree_to_string ~all:true ()) + | Commit -> + Buffer.clear notices; + Wire.reply_ok (Commit.proof_text ()) + | Focus k -> do_focus_request (`At k) + | Next -> do_focus_request `Next + | Checkpoint n -> do_checkpoint n + | Revert s -> do_revert s + | Quiet on -> do_quiet on + | Search q -> do_search q + | Load args -> Load.handle args + | Ec input -> process_ec_input input + | Begin_multi -> do_begin_multi () + | Done_multi -> do_done_multi () + | Multi_line s -> do_multi_line s + end in + + (* ------------------------------------------------------------------ *) + (* Main loop. *) + + do_initialize (); + + Printf.printf "READY [uuid:%d]\n\n%!" (EcCommands.uuid ()); + + begin try while true do + let line = input_line stdin in + (try + let cmd = Parse.of_line ~multi_active:!in_multi line in + Dispatch.run cmd + with Parse.Parse_error msg -> + Wire.reply_error msg) done with | End_of_file -> () end; From 799f38f165fb649eed0ec4fc971fcb3aaab16e05 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 31 May 2026 07:47:08 +0200 Subject: [PATCH 09/11] [llm] diagnose missing-argument REPL commands at parse time Before, lines like "CHECKPOINT" (no trailing argument) silently fell through to EC input because the dispatcher used [String.starts_with "CHECKPOINT "] -- requiring the trailing space that [String.strip] on the input line had just removed. The user saw EC's generic "parse error" instead of a command-specific message. Same shape applied to LOAD, FOCUS, REVERT, and SEARCH. Introduce a small [keyword_arg kw line] helper that accepts both [line = kw] and [line = kw ^ " " ^ ...], returning the stripped argument tail. Each prefix command now routes to its own parser even when the argument is empty, and each parser produces a specific [Parse_error] message: FOCUS -> "FOCUS: missing argument" CHECKPOINT -> "CHECKPOINT: missing name" REVERT -> "REVERT: missing uuid or checkpoint name" SEARCH -> "SEARCH: missing query" LOAD -> "LOAD: missing filename" (Load.handle, which already had this branch but it was unreachable) --- src/ecLlm.ml | 52 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 38 insertions(+), 14 deletions(-) diff --git a/src/ecLlm.ml b/src/ecLlm.ml index 51a85ef02..d3d178688 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -434,9 +434,10 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = let exception Trace_failed of exn in try + if args = "" then failwith "LOAD: missing filename"; (* Parse quoted or unquoted filename. *) let filename, rest = - if String.length args > 0 && args.[0] = '"' then + if args.[0] = '"' then let close = try String.index_from args 1 '"' with Not_found -> @@ -453,6 +454,7 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = | [f] -> (f, "") | f :: rest -> (f, String.concat " " rest) in + if filename = "" then failwith "LOAD: missing filename"; (* Parse optional LINE[:COL] and flags (-nosmt, -trace). *) let upto, nosmt, trace = @@ -721,10 +723,23 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = exception Parse_error of string - let rest n line = - String.strip (String.sub line n (String.length line - n)) + (* Match [kw] as a prefix: succeeds on exactly [kw] (no argument) + or [kw ^ " " ^ ...] (with argument), returning the stripped + argument tail. Returns [None] otherwise. This recognises both + "CHECKPOINT" and "CHECKPOINT foo" the same way, so we can + diagnose the missing-name case ourselves instead of falling + through to EC's parser. *) + let keyword_arg kw line = + if line = kw then Some "" + else if String.starts_with line (kw ^ " ") then + let n = String.length kw + 1 in + Some (String.strip + (String.sub line n (String.length line - n))) + else None let parse_focus arg = + if arg = "" then + raise (Parse_error "FOCUS: missing argument"); try Focus (int_of_string arg) with Failure _ -> raise (Parse_error @@ -735,7 +750,15 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = raise (Parse_error "CHECKPOINT: missing name"); Checkpoint name + let parse_revert spec = + if spec = "" then + raise (Parse_error + "REVERT: missing uuid or checkpoint name"); + Revert spec + let parse_search query = + if query = "" then + raise (Parse_error "SEARCH: missing query"); let query = if String.ends_with query "." then String.sub query 0 (String.length query - 1) @@ -743,6 +766,11 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = in Search query + let parse_load args = + (* [Load.handle] accepts an empty argument and reports a + specific error; keep that responsibility there. *) + Load args + let of_line ~multi_active (raw : string) : command = let line = String.strip raw in if multi_active then @@ -763,17 +791,13 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = | "NEXT" -> Next | "QUIET ON" -> Quiet true | "QUIET OFF" -> Quiet false - | _ when String.starts_with line "FOCUS " -> - parse_focus (rest 6 line) - | _ when String.starts_with line "CHECKPOINT " -> - parse_checkpoint (rest 11 line) - | _ when String.starts_with line "REVERT " -> - Revert (rest 7 line) - | _ when String.starts_with line "SEARCH " -> - parse_search (rest 7 line) - | _ when String.starts_with line "LOAD " -> - Load (rest 5 line) - | _ -> Ec line + | _ -> + match keyword_arg "FOCUS" line with Some a -> parse_focus a | None -> + match keyword_arg "CHECKPOINT" line with Some a -> parse_checkpoint a | None -> + match keyword_arg "REVERT" line with Some a -> parse_revert a | None -> + match keyword_arg "SEARCH" line with Some a -> parse_search a | None -> + match keyword_arg "LOAD" line with Some a -> parse_load a | None -> + Ec line end in (* ------------------------------------------------------------------ *) From 9d46ad065d1e58992931055d0690df1b5fdf87ef Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 31 May 2026 08:00:48 +0200 Subject: [PATCH 10/11] [llm] nested TREE and dotted-path FOCUS Introduce a frame tree derived from pr_opened + parent_of: each open leaf's chain of multi-child ancestors (skipping single-child continuations) becomes its path through the tree. The same data structure backs both TREE rendering and FOCUS path lookup. TREE now shows depth-indented entries labelled with dotted paths matching what FOCUS accepts. Leading singleton frames are unwrapped: when all opens share an outermost split, the rendering starts at that split's branches, not at a redundant [1.] wrapper. FOCUS N1.N2.N3 walks the tree following each component and focuses the resolved leaf. A single integer (FOCUS k) still works (degree-1 path). The path must resolve to a leaf; selecting an internal frame yields "FOCUS: path must select a leaf goal, not a frame" and overshooting a leaf yields "FOCUS: path overshoots a leaf goal". After [split. split. split.] on [((a /\ b) /\ c) /\ d], TREE prints: [1.1.1] a = a <- focused [1.1.2] b = b [1.2] c = c [2] d = d and FOCUS 1.2 selects c, FOCUS 2 selects d, FOCUS 1.1.2 selects b. NEXT semantics unchanged. Flat proofs render unindented as before. --- doc/llm/CLAUDE.md | 4 +- src/ecLlm.ml | 221 +++++++++++++++++++++++++++++++++++++--------- 2 files changed, 183 insertions(+), 42 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index a06725467..1c215cd82 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -61,9 +61,9 @@ These are protocol-level commands, not EasyCrypt syntax: | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | | `GOALS ALL` | Print all subgoals | -| `TREE` | List open subgoals as `[N] `, marking the focused one | +| `TREE` | List open subgoals with dotted-path labels showing nesting, marking the focused one | | `TREE ALL` | Same as `TREE`, but with full goal bodies | -| `FOCUS N` | Rotate focus so subgoal `[N]` (from `TREE`) becomes the focused goal | +| `FOCUS P` | Rotate focus to the leaf addressed by path `P` (`N` or `N1.N2.N3...`) | | `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | | `COMMIT` | Emit recorded REPL phrases as a bulleted proof body (works under `+strict_bullets`) | | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | diff --git a/src/ecLlm.ml b/src/ecLlm.ml index d3d178688..76220f42b 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -146,14 +146,108 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Format.pp_print_flush fmt (); Buffer.contents buf - (* Render the focus-tree of open subgoals. [all=false] gives a - one-line digest per goal; [all=true] gives the full goal body. *) - let tree_to_string ?(all=false) () = - let entries = EcCommands.pp_tree ~all () in - match entries with - | [] -> "No active proof.\n" - | _ -> - let buf = Buffer.create 256 in + (* Inline focus annotation ([focus: 1/N]) appended to reply tags + whenever the active proof has >=2 open subgoals. *) + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" + end in + + (* ------------------------------------------------------------------ *) + (* Frame tree: group currently-open goals by their shared multi-child + ancestors. Used by [Tree] (rendering) and [Focus] (path lookup). + The tree is a *derivation*: it depends only on [pr_opened] and + [parent_of], no recorded transcript. *) + let module FrameTree = struct + (* Internal nodes are split-point frames; leaves carry a handle + (the open goal), its index in [pr_opened] (1-based, used by + [EcCoreGoal.rotate_focus]), and its rendered text. *) + type node = + | Frame of node list (* >=2 child branches *) + | Leaf of + { idx : int (* 1-based in pr_opened *) + ; focused : bool (* idx = 1 *) + ; text : string } (* one-line conclusion *) + + (* Multi-child ancestors of [h], outermost first (= root-most + split first, deepest split last). This ordering means leaves + sharing the same OUTER frame will agree on the chain's first + element, which is what [group] partitions on. *) + let split_chain h = + let rec walk h acc = + match EcCommands.parent_of h with + | None -> acc + | Some p -> + match EcCommands.children_of p with + | [_] -> walk p acc + | _ -> walk p (p :: acc) + in + (* [walk] prepends each ancestor as we go up; the result has + outermost at the FRONT (we add it last). No reverse needed. *) + walk h [] + + (* Build the tree by grouping leaves with a common ancestor prefix. + [leaves] is a list of (chain, leaf) in [pr_opened] order. The + grouping is done recursively on the head of each chain. *) + let rec group (leaves : (EcCoreGoal.handle list * node) list) : node list = + let rec runs acc = function + | [] -> List.rev acc + | (chain, leaf) :: rest -> + match chain with + | [] -> runs (`Bare leaf :: acc) rest + | hd :: tl -> + let same_head, others = + List.partition_map (fun (c, l) -> + match c with + | h :: tail when EcCoreGoal.eq_handle h hd -> + Left (tail, l) + | _ -> Right (c, l)) + rest + in + runs (`Group ((tl, leaf) :: same_head) :: acc) others + in + List.map + (function + | `Bare leaf -> leaf + | `Group children -> Frame (group children)) + (runs [] leaves) + + (* Strip leading singleton frames so the top-level forest's + indices match what the user thinks of as "top-level subgoals + of the current frame." When all open leaves descend from a + single outermost split, the top-level forest has one Frame + containing the actual user-visible siblings; unwrap it. *) + let rec unwrap forest = + match forest with + | [Frame children] -> unwrap children + | _ -> forest + + let build () = + let handles = EcCommands.open_handles () in + let texts = EcCommands.pp_tree () in + if handles = [] then [] + else + let leaves = + List.mapi (fun i (h, (_, focused, text)) -> + let leaf = Leaf { idx = i + 1; focused; text } in + (split_chain h, leaf)) + (List.combine handles texts) + in + unwrap (group leaves) + + (* Render the tree with dotted-path labels matching what FOCUS + accepts. [all] requests full goal bodies (we re-query via + [pp_tree ~all:true] keyed by leaf index). *) + let render ?(all=false) () = + let forest = build () in + if forest = [] then "No active proof.\n" + else + let texts_all = + if all then Some (EcCommands.pp_tree ~all:true ()) + else None + in let one_line s = let s = match String.index_opt s '\n' with @@ -165,26 +259,61 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = then String.sub s 0 (limit - 1) ^ "…" else s in - List.iter (fun (i, focused, text) -> - let marker = if focused then " <- focused" else "" in - if all then - Buffer.add_string buf - (Printf.sprintf "[%d]%s\n%s\n" i marker text) - else - Buffer.add_string buf - (Printf.sprintf "[%d] %s%s\n" i (one_line text) marker) - ) entries; + let buf = Buffer.create 256 in + let rec emit ~depth ~path = function + | Leaf { idx; focused; text } -> + let label = String.concat "." (List.rev_map string_of_int path) in + let marker = if focused then " <- focused" else "" in + for _ = 1 to depth do Buffer.add_string buf " " done; + (match texts_all with + | None -> + Buffer.add_string buf + (Printf.sprintf "[%s] %s%s\n" + label (one_line text) marker) + | Some entries -> + let (_, _, full) = + List.nth entries (idx - 1) + in + Buffer.add_string buf + (Printf.sprintf "[%s]%s\n%s\n" label marker full)) + | Frame children -> + List.iteri (fun i child -> + emit ~depth:(depth + 1) ~path:((i + 1) :: path) child) + children + in + List.iteri (fun i node -> + emit ~depth:0 ~path:[i + 1] node) + forest; Buffer.contents buf - (* Inline focus annotation ([focus: 1/N]) appended to reply tags - whenever the active proof has >=2 open subgoals. *) - let focus_tag () = - match EcCommands.pp_tree () with - | _ :: _ :: _ as entries -> - Printf.sprintf " [focus: 1/%d]" (List.length entries) - | _ -> "" + (* Resolve a dotted path against the tree. Returns [Ok idx] where + [idx] is the 1-based position in [pr_opened] of the selected + leaf, or [Error msg]. *) + let resolve_path (path : int list) : (int, string) result = + let forest = build () in + let rec walk ~components nodes = + match components with + | [] -> Error "FOCUS: path must select a leaf goal" + | k :: rest -> + if k < 1 || k > List.length nodes then + Error (Printf.sprintf + "FOCUS: index %d out of range (1..%d)" + k (List.length nodes)) + else + match List.nth nodes (k - 1), rest with + | Leaf { idx; _ }, [] -> Ok idx + | Leaf _, _ -> + Error "FOCUS: path overshoots a leaf goal" + | Frame _, [] -> + Error "FOCUS: path must select a leaf goal, \ + not a frame" + | Frame kids, _ -> walk ~components:rest kids + in + if forest = [] then Error "FOCUS: no active proof" + else walk ~components:path forest end in + (* ------------------------------------------------------------------ *) (* OK/ERROR/ wire envelope. *) let module Wire = struct @@ -708,7 +837,7 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = | Goals of [`One | `All] | Tree of [`One | `All] | Commit - | Focus of int + | Focus of int list (* dotted path; [k] = "FOCUS k" *) | Next | Checkpoint of string | Revert of string (* uuid-or-name; Dispatch resolves *) @@ -740,10 +869,17 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = let parse_focus arg = if arg = "" then raise (Parse_error "FOCUS: missing argument"); - try Focus (int_of_string arg) - with Failure _ -> + let parts = String.split_on_char '.' arg in + let path = + try List.map int_of_string parts + with Failure _ -> + raise (Parse_error + (Printf.sprintf "FOCUS: not a path of integers: %s" arg)) + in + if List.exists (fun k -> k < 1) path then raise (Parse_error - (Printf.sprintf "FOCUS: not an integer: %s" arg)) + (Printf.sprintf "FOCUS: path indices must be >= 1: %s" arg)); + Focus path let parse_checkpoint name = if name = "" then @@ -834,19 +970,24 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Wire.reply_error "nothing to undo" let do_focus_request request = - (* [request] is the user's intent normalized; [`Next] is "second - sibling unless only one open". *) + (* [request] is the user's intent normalized: + - [`Next] = rotate to the second open goal (or stay if <=1) + - [`Path p] = resolve dotted path [p] against the frame tree + and focus the matching leaf. *) Buffer.clear notices; - let entries = EcCommands.pp_tree () in - let n = List.length entries in - let target = + let resolved = match request with - | `Next -> if n <= 1 then 1 else 2 - | `At k -> k + | `Next -> + let n = List.length (EcCommands.open_handles ()) in + Ok (if n <= 1 then 1 else 2) + | `Path path -> FrameTree.resolve_path path in - match EcCommands.focus_goal target with - | Ok _ -> Wire.reply_ok_goals () + match resolved with | Error msg -> Wire.reply_error msg + | Ok target -> + match EcCommands.focus_goal target with + | Ok _ -> Wire.reply_ok_goals () + | Error msg -> Wire.reply_error msg let do_checkpoint name = Buffer.clear notices; @@ -912,14 +1053,14 @@ let run ~relocdir ~boot (llmopts : EcOptions.llm_option) = Wire.reply_ok (Goals.goals_to_string ~all:true ()) | Tree `One -> Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ()) + Wire.reply_ok (FrameTree.render ()) | Tree `All -> Buffer.clear notices; - Wire.reply_ok (Goals.tree_to_string ~all:true ()) + Wire.reply_ok (FrameTree.render ~all:true ()) | Commit -> Buffer.clear notices; Wire.reply_ok (Commit.proof_text ()) - | Focus k -> do_focus_request (`At k) + | Focus path -> do_focus_request (`Path path) | Next -> do_focus_request `Next | Checkpoint n -> do_checkpoint n | Revert s -> do_revert s From 7f13cec50eca9c7170c123d861d7336e31d0c07c Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 31 May 2026 19:51:21 +0200 Subject: [PATCH 11/11] [llm] update CLAUDE.md with current workflow status Add two workflow sections that were missing or stale: 4. Inspect and navigate nested subgoals with TREE and FOCUS Documents the dotted-path syntax (FOCUS 1.2.3), the [focus: k/N] reply tag, and the fact that TREE labels are dynamic (focus-first, not stable across focus changes). 5. Build a +strict_bullets-friendly proof with COMMIT Documents how COMMIT replays the recorded transcript and inserts bullets, plus the cycle (-, +, *, --, ++, **, ...) and the prior- bullet collision avoidance. Re-number the existing QUIET and SEARCH sections from 4/5 to 6/7. Fix one outdated pitfall ("subgoals must be closed in order") -- FOCUS path now lets the agent address them in any order. Reflects what's live in EcLlm; the protocol/meta-command table was already up to date. --- doc/llm/CLAUDE.md | 72 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 68 insertions(+), 4 deletions(-) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 1c215cd82..f18137631 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -177,7 +177,69 @@ REVERT before_split apply H. ← try a different approach ``` -**4. Use QUIET mode to save tokens during bulk tactic application:** +**4. Inspect and navigate nested subgoals with `TREE` and `FOCUS`:** + +When a tactic opens multiple subgoals, the engine focuses the first +one. By default subsequent tactics act on it; siblings wait their +turn. Use `TREE` to see the structure, including nested splits: + +``` +TREE +→ OK [uuid:N] + [1.1.1] x = 0 <- focused + [1.1.2] y = 1 + [1.2] z = 2 +[2] w = 3 + +``` + +The labels are dotted paths. `FOCUS P` rotates focus to the leaf at +path `P`: + +``` +FOCUS 1.2 ← work on `z = 2` +FOCUS 2 ← work on `w = 3` +FOCUS 1.1.1 ← back to `x = 0` +``` + +`FOCUS k` (a single integer) targets the k-th open goal in the flat +listing. `NEXT` is shorthand for `FOCUS 2`. Selecting an internal +frame errors (`FOCUS: path must select a leaf goal, not a frame`). + +Replies carry a `[focus: k/N]` tag when more than one goal is open +(e.g. `OK [uuid:42] [focus: 1/3]`) so you always know which goal the +next tactic will hit. **TREE labels are not stable across focus +changes** — `FOCUS 1.2` from one state may name a different goal in +another, because the tree always shows the focused goal first. + +**5. Build a `+strict_bullets`-friendly proof with `COMMIT`:** + +The REPL records every successful interactive phrase. `COMMIT` walks +the proof DAG and emits the recorded tactics with bullets inserted +at every multi-child split. The output is a proof body that compiles +under `pragma +strict_bullets`: + +``` +LOAD "myfile.ec" 42 +split. +- rewrite H. trivial. ← REPL accepts the unbulleted form +- exact hq. +COMMIT +→ OK [uuid:N] +split. +- rewrite H. trivial. +- exact hq. + +``` + +Bullet characters cycle through `-`, `+`, `*`, `--`, `++`, `**`, ... +and are chosen to avoid colliding with any frames the LOAD prefix +already opened. Use `COMMIT` once the proof is complete (or at any +checkpoint) and paste the result back into the source file. + +`UNDO` / `REVERT` trim the COMMIT transcript automatically. + +**6. Use QUIET mode to save tokens during bulk tactic application:** ``` QUIET ON @@ -188,7 +250,7 @@ QUIET OFF GOALS ``` -**5. Search for lemmas using patterns:** +**7. Search for lemmas using patterns:** EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as wildcard: @@ -267,8 +329,10 @@ SEARCH (_ %/ _) - `by` closes **all** remaining subgoals. If it fails, the error refers to the first unclosed goal, which may not be the intended one. -- When a tactic generates multiple subgoals, each subgoal must be - closed in order. Use `GOALS ALL` or `TREE` to see them all. +- When a tactic generates multiple subgoals, the engine focuses the + first one. Address them in any order via `FOCUS path`, or in the + default order by closing each in turn. Use `TREE` or `GOALS ALL` + to see what's open. - When more than one subgoal is open, replies carry a `[focus: k/N]` tag (e.g. `OK [uuid:42] [focus: 1/3]`) so you know which one the next tactic will hit.