Commit c8cb2b78 authored by Martin Clochard's avatar Martin Clochard

by/so: moved precedence to the same level as arrow

  Reason for that change: interpret correctly both
  (1) A by B -> C and (2) A -> B by C
  Case (2) is common, and we expect by to take precendence,
  so that A is the context for the proof of B.
  Case (1) is rarer, and is troublesome if by take precendence
  cause (A by B) -> C is almost certainly not what the user
  intended to write. Putting precendence of by/so at the same level as
  the arrow fix this
parent fe59898d
......@@ -296,12 +296,12 @@ and print_tnode pri fmt t = match t.t_node with
fprintf fmt "false"
| Tbinop (Tand,f1,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) })
when Slab.mem Term.asym_split f2.t_label ->
fprintf fmt (protect_on (pri > 2) "@[<hov 1>%a so@ %a@]")
(print_lterm 3) f1 (print_lterm 2) f2
fprintf fmt (protect_on (pri > 1) "@[<hov 1>%a so@ %a@]")
(print_lterm 2) f1 (print_lterm 1) f2
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },f1)
when Slab.mem Term.asym_split f2.t_label ->
fprintf fmt (protect_on (pri > 2) "@[<hov 1>%a by@ %a@]")
(print_lterm 3) f1 (print_lterm 2) f2
fprintf fmt (protect_on (pri > 1) "@[<hov 1>%a by@ %a@]")
(print_lterm 2) f1 (print_lterm 1) f2
| Tbinop (b,f1,f2) ->
let asym = Slab.mem Term.asym_split f1.t_label in
let p = prio_binop b in
......
......@@ -165,8 +165,7 @@
%nonassoc DOT ELSE GHOST
%nonassoc prec_named
%nonassoc COLON (* weaker than -> because of t: a -> b *)
%right ARROW LRARROW
%right BY SO
%right ARROW LRARROW BY SO
%right OR BARBAR
%right AND AMPAMP
%nonassoc NOT
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment