From 5f8952ecbdec55c32752905b6cfeea1db1cbd135 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 26 May 2026 08:14:09 +0200 Subject: [PATCH] bullets: focusing operators behind +strict_bullets pragma When `pragma +strict_bullets` is set, the bullet tokens `-`, `+`, `*` (and their repeated forms `--`, `++`, `**`, ...) become Coq-style focusing operators: each phrase's bullet is checked against a per-proof stack so that a subgoal must be discharged before its sibling is addressed, and so that bullet characters identify nesting levels. The default behavior is unchanged: without the pragma, bullets remain pure decoration, preserving every existing proof script. Repeated bullet characters are emitted by the lexer as single PLUSn/MINUSn/STARn tokens (carrying their literal), which makes them usable both as deeper bullet levels and as user-defined binary operators (`op (--) ...`). The final sibling of a split point can be continued at the parent level without a bullet: when the previous sibling is closed and exactly one sibling remains, the inner frame pops automatically (and cascades through nested last-sibling frames). This keeps the standard phl idiom of long `seq N : ' chains flat instead of forcing ever-deeper indentation under a `+' for each continuation. Multi-way splits keep their enumeration discipline for all but the last subgoal. --- src/ecCommands.ml | 28 ++++-- src/ecLexer.mll | 23 +++++ src/ecParser.mly | 32 ++++-- src/ecParsetree.ml | 4 +- src/ecScope.ml | 157 +++++++++++++++++++++++++++--- src/ecScope.mli | 22 ++++- tests/bullets-basic.ec | 56 +++++++++++ tests/bullets-binop.ec | 21 ++++ tests/bullets-deep.ec | 39 ++++++++ tests/bullets-errors.ec | 39 ++++++++ tests/bullets-implicit-reuse.ec | 41 ++++++++ tests/bullets-last-fallthrough.ec | 65 +++++++++++++ tests/bullets-legacy.ec | 19 ++++ tests/bullets-naked-split.ec | 32 ++++++ 14 files changed, 540 insertions(+), 38 deletions(-) create mode 100644 tests/bullets-basic.ec create mode 100644 tests/bullets-binop.ec create mode 100644 tests/bullets-deep.ec create mode 100644 tests/bullets-errors.ec create mode 100644 tests/bullets-implicit-reuse.ec create mode 100644 tests/bullets-last-fallthrough.ec create mode 100644 tests/bullets-legacy.ec create mode 100644 tests/bullets-naked-split.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index e90518ff0..08f801623 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -15,6 +15,7 @@ type pragma = { pm_g_prall : bool; (* true => display all open goals *) pm_g_prpo : EcPrinting.prpo_display; pm_check : [`Check | `WeakCheck | `Report]; + pm_strict_bullets : bool; (* true => bullets focus subgoals *) } let dpragma = { @@ -22,6 +23,7 @@ let dpragma = { pm_g_prall = false ; pm_g_prpo = EcPrinting.{ prpo_pr = false; prpo_po = false; }; pm_check = `Check; + pm_strict_bullets = false; } module Pragma : sig @@ -61,10 +63,15 @@ let pragma_g_po_display (b : bool) = let pragma_check mode = Pragma.upd (fun pragma -> { pragma with pm_check = mode; }) +let pragma_strict_bullets (b : bool) = + Pragma.upd (fun pragma -> { pragma with pm_strict_bullets = b; }) + module Pragmas = struct let silent = "silent" let verbose = "verbose" + let strict_bullets = "strict_bullets" + module Proofs = struct let check = "Proofs:check" let weak = "Proofs:weak" @@ -505,7 +512,9 @@ and process_abbrev (scope : EcScope.scope) (a : pabbrev located) = (* -------------------------------------------------------------------- *) and process_axiom ?(src : string option) (scope : EcScope.scope) (ax : paxiom located) = EcScope.check_state `InTop "axiom" scope; - let (name, scope) = EcScope.Ax.add ?src scope (Pragma.get ()).pm_check ax in + let pragma = Pragma.get () in + let strict = pragma.pm_strict_bullets in + let (name, scope) = EcScope.Ax.add ?src ~strict scope pragma.pm_check ax in name |> EcUtils.oiter (fun x -> match (unloc ax).pa_kind with @@ -635,8 +644,9 @@ and process_sct_close (scope : EcScope.scope) name = and process_tactics ?(src : string option) (scope : EcScope.scope) t = let mode = (Pragma.get ()).pm_check in match t with - | `Actual t -> snd (EcScope.Tactics.process ?src scope mode t) - | `Proof -> EcScope.Tactics.proof ?src scope + | `Actual (b, t) -> + snd (EcScope.Tactics.process ?src ?bullet:b scope mode t) + | `Proof -> EcScope.Tactics.proof ?src scope (* -------------------------------------------------------------------- *) (* Add and store src for proofs *) @@ -653,8 +663,9 @@ and process_save ?(src : string option) (scope : EcScope.scope) ed = (* -------------------------------------------------------------------- *) and process_realize (scope : EcScope.scope) pr = - let mode = (Pragma.get ()).pm_check in - let (name, scope) = EcScope.Ax.realize scope mode pr in + let pragma = Pragma.get () in + let strict = pragma.pm_strict_bullets in + let (name, scope) = EcScope.Ax.realize ~strict scope pragma.pm_check pr in name |> EcUtils.oiter (fun x -> EcScope.notify scope `Info "added lemma: `%s'" x); scope @@ -689,6 +700,9 @@ and process_option (scope : EcScope.scope) (name, value) = let gs = EcEnv.gstate (EcScope.env scope) in EcGState.setflag (unloc name) value gs; scope + | `Bool value when EcLocation.unloc name = Pragmas.strict_bullets -> + pragma_strict_bullets value; scope + | (`Int _) as value -> let gs = EcEnv.gstate (EcScope.env scope) in EcGState.setvalue (unloc name) value gs; scope @@ -716,14 +730,14 @@ and process_dump_why3 scope filename = EcScope.dump_why3 scope filename; scope (* -------------------------------------------------------------------- *) -and process_dump scope (source, tc) = +and process_dump scope (source, (bullet, tc)) = let open EcCoreGoal in let input, (p1, p2) = source.tcd_source in let goals, scope = let mode = (Pragma.get ()).pm_check in - EcScope.Tactics.process scope mode tc + EcScope.Tactics.process ?bullet scope mode tc in let wrerror fname = diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 704b0e976..14f558f41 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -301,8 +301,31 @@ | '*' | '/' | '&' | '%' -> 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 n < 2 then None + else + let c = op.[0] in + if not (c = '-' || c = '+' || c = '*') then None + else + let rec all_same i = i = n || (op.[i] = c && all_same (i+1)) in + if not (all_same 1) then None + else match c with + | '-' -> Some (MINUSn op) + | '+' -> Some (PLUSn op) + | '*' -> Some (STARn op) + | _ -> None + (* ------------------------------------------------------------------ *) let lex_operators (op : string) = + match lex_bullet_chunk op with + | Some tok -> [tok] + | None -> let baseop (op : string) = try fst (Hashtbl.find operators op) with Not_found -> diff --git a/src/ecParser.mly b/src/ecParser.mly index 8633c1312..8a5b9bad5 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 { "[-]" } +| x=PLUSn { Printf.sprintf "[%s]" x } +| x=MINUSn { Printf.sprintf "[%s]" x } %inline sbinop: | EQ { "=" } @@ -842,6 +845,9 @@ inlinepat: | STAR { "*" } | SLASH { "/" } | AT { "@" } +| x=PLUSn { x } +| x=MINUSn { x } +| x=STARn { x } | OR { "\\/" } | ORA { "||" } | AND { "/\\" } @@ -3577,11 +3583,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 b.pl_desc } +| b=loc(PLUSn) { mk_loc b.pl_loc b.pl_desc } +| b=loc(STARn) { mk_loc b.pl_loc 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 9644cfde6..af3cf0b35 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..b35f55013 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -296,6 +296,23 @@ and proof_auc = { puc_jdg : proof_state; puc_flags : pucflags; puc_crt : EcDecl.axiom; + puc_bullets : bullet_frame list option; + (* [None] when bullets are decoration only (legacy mode). + [Some stack] when [+strict_bullets] was active at proof + open; head = innermost frame. Each frame records the bullet + token, opening location, and slot accounting. *) +} + +and bullet_frame = { + bf_token : string; + bf_loc : EcLocation.t; + bf_floor : int; + (* Number of open goals that must remain when this frame's + subproof is fully discharged. Computed at open as + [opened_at_open - 1] (we focus on one goal; the others stay + open at outer levels until the frame's subproof collapses). + The frame can be popped when the current open-count drops + to [bf_floor] or below. *) } and proof_ctxt = @@ -811,7 +828,109 @@ 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) = + (* ----------------------------------------------------------------- *) + (* Bullet-stack management. The "strict" mode (gated by the + [+strict-bullets] pragma) requires each phrase to discharge its + focused subgoal before moving on. The non-strict mode keeps the + historical behavior where bullets are pure decoration. + + Frames record the number of "background" open goals at the + point the bullet level was opened. A frame's currently-focused + subgoal is fully discharged iff [open_count <= bf_background]. + The bullet-level itself is fully closed when, in addition, the + last sibling has been processed; we detect that by counting open + goals and the depth stack. *) + + let bullet_error ~loc fmt = + let buf = Buffer.create 64 in + let fbuf = Format.formatter_of_buffer buf in + Format.kfprintf + (fun fbuf -> + Format.pp_print_flush fbuf (); + hierror ~loc "%s" (Buffer.contents buf)) + fbuf fmt + + let n_open juc = List.length (EcCoreGoal.all_hd_opened juc) + + (* 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_bullet ~(bullet : string located option) + (juc : EcCoreGoal.proof) (stack : bullet_frame list) + : bullet_frame list = + 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 where = + match stack with + | [] -> "top level" + | f :: _ -> + Printf.sprintf "the bullet level opened by `%s' at %s" + f.bf_token (EcLocation.tostring f.bf_loc) in + hierror + "previous tactic left %d open subgoals at %s; the next \ + phrase needs a bullet to focus one of them" opened where + 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 + bullet_error ~loc + "bullet `%s' opens a new subproof level but there are \ + no remaining subgoals" 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 : bullet_frame) -> + if opened > f.bf_floor then + bullet_error ~loc + "bullet `%s' (matches an outer level opened at %s) \ + skips past inner bullet `%s' opened at %s whose \ + subproof is not closed" + tok (EcLocation.tostring frame.bf_loc) + f.bf_token (EcLocation.tostring f.bf_loc)) + inner; + (* The matching frame's current slot must be closed. *) + if opened > frame.bf_floor then + bullet_error ~loc + "bullet `%s' reused but the previous subgoal (opened at \ + %s) is not closed" + tok (EcLocation.tostring frame.bf_loc); + { 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 : bullet_frame list) + : bullet_frame list = + 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 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 +974,8 @@ module Tactics = struct EcHiGoal.tt_redlogic = Options.get_redlogic scope; EcHiGoal.tt_und_delta = Options.get_und_delta scope; } in + let bullets = omap (open_bullet ~bullet juc) pac.puc_bullets in + let (hds, juc) = try TTC.process ttenv tac juc with EcCoreGoal.TcError tcerror -> @@ -868,7 +989,9 @@ module Tactics = struct let penv = EcCoreGoal.proofenv_of_proof juc in - let pac = { pac with puc_jdg = PSCheck juc } in + let bullets = omap (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 +1003,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 +1064,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 +1079,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 +1089,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 +1149,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 +1229,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 +1295,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 +1317,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 +1352,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..2ab02359a 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -41,6 +41,19 @@ and proof_auc = { puc_jdg : proof_state; puc_flags : pucflags; puc_crt : EcDecl.axiom; + puc_bullets : bullet_frame list option; + (* [None] when bullets are decoration only (legacy mode). + [Some stack] when [+strict_bullets] was active at proof + open; each phrase validates and updates [stack]. *) +} + +and bullet_frame = { + bf_token : string; + bf_loc : EcLocation.t; + bf_floor : int; + (* Open-count that must remain once the frame's subproof is + fully discharged ([= opened_at_open - 1]). The frame is + popped after a phrase when [n_open <= bf_floor]. *) } and proof_ctxt = @@ -128,11 +141,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 +244,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.