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 (--) ...`).

Author: strub

src/ecCommands.ml

@@ -15,13 +15,15 @@ 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 = {
   pm_verbose = true  ;
   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"
@@ -633,10 +640,13 @@ and process_sct_close (scope : EcScope.scope) name =
 (* -------------------------------------------------------------------- *)
 (* Add and store src for proofs *)
 and process_tactics ?(src : string option) (scope : EcScope.scope) t =
-  let mode = (Pragma.get ()).pm_check in
+  let pragma = Pragma.get () in
+  let mode = pragma.pm_check in
+  let strict_bullets = pragma.pm_strict_bullets 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 ~strict_bullets scope mode t)
+  | `Proof -> EcScope.Tactics.proof ?src scope
 
 (* -------------------------------------------------------------------- *)
 (* Add and store src for proofs *)
@@ -689,6 +699,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 +729,16 @@ 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
+    let pragma = Pragma.get () in
+    let mode = pragma.pm_check in
+    let strict_bullets = pragma.pm_strict_bullets in
+    EcScope.Tactics.process ?bullet ~strict_bullets scope mode tc
   in
 
   let wrerror fname =

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 ->

src/ecParser.mly

@@ -599,6 +599,7 @@
 %token WP
 %token ZETA
 %token <string> NOP LOP1 ROP1 LOP2 ROP2 LOP3 ROP3 LOP4 ROP4 NUMOP
+%token <string> PLUSn MINUSn STARn
 %token LTCOLON DASHLT GT LT GE LE LTSTARGT LTLTSTARGT LTSTARGTGT
 %token <Lexing.position> FINAL
 %token <EcParsetree.dockind * string> 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 }

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

src/ecScope.ml

@@ -296,6 +296,18 @@ and proof_auc = {
   puc_jdg     : proof_state;
   puc_flags   : pucflags;
   puc_crt     : EcDecl.axiom;
+  puc_bullets : bullet_frame list;
+    (* Active bullet stack (head = innermost). Each frame records the
+       focused goal handle, the still-to-process sibling handles at
+       that depth, the bullet token (e.g. "-", "--"), and the location
+       where the bullet was opened — used for diagnostics. *)
+}
+
+and bullet_frame = {
+  bf_token   : string;
+  bf_loc     : EcLocation.t;
+  bf_at_open : int;
+  bf_used    : int;
 }
 
 and proof_ctxt =
@@ -811,7 +823,108 @@ 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 new
+     stack to install for this phrase. *)
+  let open_bullet ~(bullet : string located option)
+      (juc : EcCoreGoal.proof) (stack : bullet_frame list)
+      : bullet_frame list =
+    match bullet with
+    | None -> stack
+    | Some b ->
+        let tok = unloc b in
+        let loc = loc b in
+        let opened = n_open juc in
+        (* Search the stack from innermost outward for a frame matching
+           [tok]. Any frames strictly inside the matched one are popped
+           (must already be drained, i.e. opened <= bf_background). *)
+        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 ->
+            (* Push a new deeper frame; this bullet consumes slot #1
+               (out of [opened]) immediately. *)
+            if opened = 0 then
+              bullet_error ~loc
+                "bullet `%s' opens a new subproof level but there are \
+                 no remaining subgoals" tok;
+            let frame = {
+              bf_token   = tok;
+              bf_loc     = loc;
+              bf_at_open = opened;
+              bf_used    = 1;
+            } in
+            frame :: stack
+        | `Match (inner, frame, outer) ->
+            (* The expected open count after fully discharging the
+               previous slot, given the frame's history. *)
+            let expected = frame.bf_at_open - frame.bf_used in
+            (* Each inner frame must already be drained — i.e., its
+               outer view of the open count must be reachable. *)
+            List.iter (fun (f : bullet_frame) ->
+              if opened > f.bf_at_open - f.bf_used 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 > expected then
+              bullet_error ~loc
+                "bullet `%s' reused but the previous subgoal (opened at \
+                 %s) is not closed"
+                tok (EcLocation.tostring frame.bf_loc);
+            (* Slots remaining? *)
+            if frame.bf_used >= frame.bf_at_open then
+              bullet_error ~loc
+                "bullet `%s' reused but no sibling subgoals remain at \
+                 this level (opened at %s)"
+                tok (EcLocation.tostring frame.bf_loc);
+            let frame = { frame with
+              bf_loc = loc;
+              bf_used = frame.bf_used + 1;
+            } in
+            frame :: outer
+
+  (* Close the phrase: validate that the (possibly bulleted) phrase
+     made progress on the focused subgoal. We do NOT pop drained
+     frames here; that's done at the next [open_bullet] or on save. *)
+  let close_bullet ~(bullet : _) (juc : EcCoreGoal.proof)
+      (stack : bullet_frame list) : bullet_frame list =
+    let _ = bullet in let _ = juc in
+    stack
+
+  let process_r ?(src : string option) ?(bullet : string located option)
+      ?(strict_bullets : bool = false)
+      ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) =
     check_state `InProof "proof script" scope;
 
     let scope =
@@ -855,6 +968,11 @@ module Tactics = struct
           EcHiGoal.tt_redlogic   = Options.get_redlogic scope;
           EcHiGoal.tt_und_delta  = Options.get_und_delta scope; } in
 
+        let bullets =
+          if strict_bullets then open_bullet ~bullet juc pac.puc_bullets
+          else pac.puc_bullets
+        in
+
         let (hds, juc) =
           try  TTC.process ttenv tac juc
           with EcCoreGoal.TcError tcerror ->
@@ -866,9 +984,14 @@ module Tactics = struct
             in raise (EcCoreGoal.TcError tcerror)
         in
 
+        let bullets =
+          if strict_bullets then close_bullet ~bullet juc bullets
+          else bullets
+        in
+
         let penv = EcCoreGoal.proofenv_of_proof juc in
 
-        let pac = { pac with puc_jdg = PSCheck juc } 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)
+      ?(strict_bullets : bool = false) scope mode tac =
+    process_r ?src ?bullet ~strict_bullets true mode scope tac
 end
 
 (* -------------------------------------------------------------------- *)
@@ -955,7 +1079,8 @@ module Ax = struct
         ; puc_started = false
         ; puc_jdg     = puc
         ; puc_flags   = axflags
-        ; puc_crt     = axd }
+        ; puc_crt     = axd
+        ; puc_bullets = [] }
       in
         { puc_active    = Some (active, ctxt);
           puc_cont      = cont;