diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 0cc20c5a3..f18137631 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -6,59 +6,343 @@ 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: -### Output conventions +``` +READY [uuid:0] + +``` -- **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.` +**Responses.** Every response has a typed envelope and an `` +sentinel: -### Workflow for writing and debugging proofs +``` +OK [uuid:N] + + +``` -1. Try to write a pen-and-paper proof first. +``` +ERROR [uuid:N] + + +``` -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. +The `uuid` is a monotonically increasing integer identifying the proof +engine state. It increments with each successful command. + +### Meta-commands + +These are protocol-level commands, not EasyCrypt syntax: + +| Command | Description | +|---------|-------------| +| `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) | +| `GOALS ALL` | Print all subgoals | +| `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 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` | +| `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 | + +### EasyCrypt commands + +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 `.` -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. +``` +smt(). +rewrite H1 H2. +search (%/). +print mulzK. +``` + +For multi-line statements, wrap with `` and ``: + +``` + +lemma test : + 0 <= n => + 0 < n + 1. + +``` -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. +### Workflow -5. Fix the proof and repeat from step 2. The ultimate proof should - not contain `admit` or `admitted`. +**1. Load a file up to the proof point:** + +``` +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 +... + +``` + +For large files, use `-nosmt` to skip SMT calls during prefix +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 +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. 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 +rewrite H1. +rewrite H2. +rewrite H3. +QUIET OFF +GOALS +``` + +**7. 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, 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. +- `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'`. ## EasyCrypt language overview @@ -91,8 +375,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 +423,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..3a6d7bb34 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -535,34 +535,8 @@ let main () = end - | `Llm llmopts -> begin - let name = llmopts.llmo_input in - - begin try - let ext = Filename.extension name in - ignore (EcLoader.getkind ext : EcLoader.kind) - with EcLoader.BadExtension ext -> - Format.eprintf "do not know what to do with %s@." ext; - exit 1 - end; - - let lastgoals = llmopts.llmo_lastgoals in - let terminal = - lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name)) - in - - { prvopts = llmopts.llmo_provers - ; input = Some name - ; terminal = terminal - ; interactive = false - ; eco = true - ; gccompact = None - ; docgen = false - ; outdirp = None - ; upto = llmopts.llmo_upto - ; trace = None } - - end + | `Llm llmopts -> + EcLlm.run ~relocdir ~boot:ldropts.ldro_boot llmopts | `Runtest _ -> (* Eagerly executed *) 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..cf1e740c2 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 = @@ -917,6 +931,69 @@ let push_context scope context = ct_stack = context.ct_stack |> omap (fun st -> context.ct_current :: st); } +(* -------------------------------------------------------------------- *) +(* Rotate the focus of the currently active proof so that the goal at + 1-based index [k] becomes the focused one. The change is persisted + in the context with a new uuid so UNDO/REVERT can roll it back. + Returns the new number of open goals on success, or an error + message on failure. *) +let focus_goal (k : int) : (int, string) result = + match !context with + | None -> Error "no active context" + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> Error "no active proof" + | Some puc -> + match puc.EcScope.puc_active with + | None -> Error "no active proof" + | Some (pac, pct) -> + match pac.EcScope.puc_jdg with + | EcScope.PSNoCheck -> Error "proof is in no-check mode" + | EcScope.PSCheck pf -> + let n = List.length (EcCoreGoal.all_hd_opened pf) in + if n = 0 then Error "no open goals" + else if k < 1 || k > n then + Error (Printf.sprintf + "focus: index %d out of range (1..%d)" k n) + else if k = 1 then Ok n + else begin + let pf = EcCoreGoal.rotate_focus k pf in + let pac = { pac with EcScope.puc_jdg = EcScope.PSCheck pf } in + let puc = + { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some (push_context scope ctxt); + Ok n + end + +(* Disable bullet enforcement for REPL-driven phrases. Drops the global + pragma so newly-opened proofs have no bullet stack, and clears the + stack on any currently active proof so REPL phrases are not checked + against it. Idempotent. Does not advance the undo level. Returns + the stack that was in place (if any) at the moment the active + proof's bullets were first cleared; returns [None] on idempotent + calls (where the stack is already gone). Callers use the returned + stack to drive bullet-character selection in [COMMIT]. *) +let disable_repl_bullets () : EcBullets.stack option = + pragma_strict_bullets false; + match !context with + | None -> None + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> None + | Some puc -> + match puc.EcScope.puc_active with + | None -> None + | Some (pac, pct) -> + match pac.EcScope.puc_bullets with + | None -> None + | Some _ as prior -> + let pac = { pac with EcScope.puc_bullets = None } in + let puc = { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some { ctxt with ct_current = scope }; + prior + (* -------------------------------------------------------------------- *) let initialize ~restart ~undo ~boot ~checkmode ~checkproof = assert (restart || EcUtils.is_none !context); @@ -1042,8 +1119,39 @@ let pp_current_goal ?(all = false) stream = end (* -------------------------------------------------------------------- *) +let in_proof () = + Option.is_some (S.xgoal (current ())) + +(* Return the list of open-goal handles at the top level of the active + proof, focused-first, or [] if no proof is active. *) +let open_handles () : EcCoreGoal.handle list = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.all_hd_opened pf + | _ -> [] + +(* Direct DAG children of [h] in the active proof. [] if no proof. *) +let children_of (h : EcCoreGoal.handle) : EcCoreGoal.handle list = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.children_of_handle + (EcCoreGoal.proofenv_of_proof pf) h + | _ -> [] + +(* Parent of [h] in the active proof's DAG, or [None] if [h] is the + root or no proof is active. *) +let parent_of (h : EcCoreGoal.handle) : EcCoreGoal.handle option = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.parent_of_handle + (EcCoreGoal.proofenv_of_proof pf) h + | _ -> None + let pp_current_goal_or_noproof ?(all = false) stream = - if Option.is_some (S.xgoal (current ())) then + if in_proof () then pp_current_goal ~all stream else Format.fprintf stream "No active proof.@\n%!" @@ -1081,3 +1189,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 7dab0b84b..e36f6c4f1 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -63,6 +63,13 @@ val pp_current_goal : ?all:bool -> Format.formatter -> unit val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit val pp_all_goals : unit -> string list +val in_proof : unit -> bool +val disable_repl_bullets : unit -> EcBullets.stack option +val pp_tree : ?all:bool -> unit -> (int * bool * string) list +val focus_goal : int -> (int, string) result +val open_handles : unit -> EcCoreGoal.handle list +val children_of : EcCoreGoal.handle -> EcCoreGoal.handle list +val parent_of : EcCoreGoal.handle -> EcCoreGoal.handle option (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 4b75e5b0c..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,33 @@ let all_opened (pf : proof) = (* -------------------------------------------------------------------- *) let closed (pf : proof) = List.is_empty pf.pr_opened +(* -------------------------------------------------------------------- *) +(* Direct children of [h] in the proof DAG, in creation order. This is + driven by [pr_parent], the explicit parent edge recorded by + [FApi.newgoal] at the moment each child handle is allocated. The + iteration order matches creation order because handles are + generated by a monotonic counter and [ID.Map] iterates by key. *) +let children_of_handle (pe : proofenv) (h : handle) : handle list = + ID.Map.fold + (fun child parent acc -> + if eq_handle parent h then child :: acc else acc) + pe.pr_parent [] + |> List.rev + +(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *) +let parent_of_handle (pe : proofenv) (h : handle) : handle option = + ID.Map.find_opt h pe.pr_parent + +(* -------------------------------------------------------------------- *) +let rotate_focus (k : int) (pf : proof) = + let n = List.length pf.pr_opened in + if k < 1 || k > n then + invalid_arg "EcCoreGoal.rotate_focus"; + if k = 1 then pf + else + let pre, post = List.split_at (k - 1) pf.pr_opened in + { pf with pr_opened = post @ pre } + (* -------------------------------------------------------------------- *) module Exn = struct let recast pe _hyps f x = diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index f574b49bf..14b57e045 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -205,6 +205,18 @@ val all_opened : proof -> pregoal list (* Check if a proof is done *) val closed : proof -> bool +(* Direct children of [h] in the proof DAG, in creation order. *) +val children_of_handle : proofenv -> handle -> handle list + +(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *) +val parent_of_handle : proofenv -> handle -> handle option + +(* Rotate the list of opened goals at the top level. [rotate_focus k pf] + makes the goal currently at 1-based index [k] the new focused goal, + preserving the cyclic order of the others. Raises [Invalid_argument] + if [k] is out of range. *) +val rotate_focus : int -> proof -> proof + (* -------------------------------------------------------------------- *) val tc_error : proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string 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/ecLlm.ml b/src/ecLlm.ml new file mode 100644 index 000000000..76220f42b --- /dev/null +++ b/src/ecLlm.ml @@ -0,0 +1,1094 @@ +(* -------------------------------------------------------------------- *) +(* 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 + + (* 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 + | 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 + 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 + + (* 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 + 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 + if args = "" then failwith "LOAD: missing filename"; + (* Parse quoted or unquoted filename. *) + let filename, rest = + if 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 + if filename = "" then failwith "LOAD: missing filename"; + + (* 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. *) + + (* ------------------------------------------------------------------ *) + (* 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 list (* dotted path; [k] = "FOCUS k" *) + | 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 + + (* 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"); + 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: path indices must be >= 1: %s" arg)); + Focus path + + let parse_checkpoint name = + if name = "" then + 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) + else query + 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 + 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 + | _ -> + 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 + + (* ------------------------------------------------------------------ *) + (* 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 + + let module Dispatch = struct + let do_help () = + 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 + + let do_undo () = + 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" + + let do_focus_request request = + (* [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 resolved = + match request with + | `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 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; + 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 target = + try Some (int_of_string spec) + with Failure _ -> Hashtbl.find_opt checkpoints spec + in + match target with + | None -> + Wire.reply_error (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" spec) + | 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 + + let do_quiet on = + Buffer.clear notices; + quiet := on; + Wire.reply_ok "" + + let do_search query = + process_ec_input (Printf.sprintf "search %s." query) + + 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 (FrameTree.render ()) + | Tree `All -> + Buffer.clear notices; + Wire.reply_ok (FrameTree.render ~all:true ()) + | Commit -> + Buffer.clear notices; + Wire.reply_ok (Commit.proof_text ()) + | Focus path -> do_focus_request (`Path path) + | 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; + + 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 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 = { 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..bd8391e26 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 = @@ -485,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 @@ -811,7 +819,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 +864,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 +883,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 +897,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 +958,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 +973,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 +983,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 +1043,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 +1123,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 +1189,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 +1211,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 +1246,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..8a2a1dede 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 = @@ -83,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 @@ -128,11 +133,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 +236,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.