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 : <post>' 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.

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"
@@ -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 =

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