Skip to content

bullets: focusing operators behind +strict_bullets pragma #1017

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
strub wants to merge 1 commit into
base: main
Choose a base branch
from
Open

bullets: focusing operators behind +strict_bullets pragma #1017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 21 additions & 7 deletions src/ecCommands.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
23 changes: 23 additions & 0 deletions src/ecLexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
32 changes: 22 additions & 10 deletions src/ecParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 { "=" }
Expand All @@ -842,6 +845,9 @@ inlinepat:
| STAR { "*" }
| SLASH { "/" }
| AT { "@" }
| x=PLUSn { x }
| x=MINUSn { x }
| x=STARn { x }
| OR { "\\/" }
| ORA { "||" }
| AND { "/\\" }
Expand Down Expand Up @@ -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 }
Expand Down
4 changes: 2 additions & 2 deletions src/ecParsetree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading