keep explicit asymmetric and/or until typechecking (fixes #17001)

src/core/dterm.ml

@@ -157,6 +157,9 @@ and dpattern_node =
   | DPor of dpattern * dpattern
   | DPas of dpattern * preid
 
+type dbinop =
+  | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff
+
 type dterm = {
   dt_node  : dterm_node;
   dt_dty   : dty option;
@@ -174,7 +177,7 @@ and dterm_node =
   | DTcase of dterm * (dpattern * dterm) list
   | DTeps of preid * dty * dterm
   | DTquant of quant * (preid * dty) list * dterm list list * dterm
-  | DTbinop of binop * dterm * dterm
+  | DTbinop of dbinop * dterm * dterm
   | DTnot of dterm
   | DTtrue
   | DTfalse
@@ -493,8 +496,18 @@ and try_term strict keep_loc uloc env prop dty node =
       List.iter (check_used_var f) vl;
       check_exists_implies q f;
       t_quant_close q vl trl f
-  | DTbinop (op,df1,df2) ->
-      t_binary op (get env true df1) (get env true df2)
+  | DTbinop (DTand,df1,df2) ->
+      t_and (get env true df1) (get env true df2)
+  | DTbinop (DTand_asym,df1,df2) ->
+      t_and_asym (get env true df1) (get env true df2)
+  | DTbinop (DTor,df1,df2) ->
+      t_or (get env true df1) (get env true df2)
+  | DTbinop (DTor_asym,df1,df2) ->
+      t_or_asym (get env true df1) (get env true df2)
+  | DTbinop (DTimplies,df1,df2) ->
+      t_implies (get env true df1) (get env true df2)
+  | DTbinop (DTiff,df1,df2) ->
+      t_iff (get env true df1) (get env true df2)
   | DTnot df ->
       t_not (get env true df)
   | DTtrue ->

src/core/dterm.mli

@@ -38,6 +38,9 @@ and dpattern_node =
   | DPor of dpattern * dpattern
   | DPas of dpattern * preid
 
+type dbinop =
+  | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff
+
 type dterm = private {
   dt_node  : dterm_node;
   dt_dty   : dty option;
@@ -55,7 +58,7 @@ and dterm_node =
   | DTcase of dterm * (dpattern * dterm) list
   | DTeps of preid * dty * dterm
   | DTquant of quant * (preid * dty) list * dterm list list * dterm
-  | DTbinop of binop * dterm * dterm
+  | DTbinop of dbinop * dterm * dterm
   | DTnot of dterm
   | DTtrue
   | DTfalse

src/parser/parser.mly

@@ -586,11 +586,11 @@ lexpr:
 | lexpr OR lexpr
    { infix_pp $1 PPor $3 }
 | lexpr BARBAR lexpr
-   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPor $3 }
+   { infix_pp $1 PPor_asym $3 }
 | lexpr AND lexpr
    { infix_pp $1 PPand $3 }
 | lexpr AMPAMP lexpr
-   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPand $3 }
+   { infix_pp $1 PPand_asym $3 }
 | NOT lexpr
    { prefix_pp PPnot $2 }
 | lexpr EQUAL lexpr

src/parser/ptree.ml

@@ -27,7 +27,7 @@ type pp_quant =
   | PPforall | PPexists | PPlambda
 
 type pp_binop =
-  | PPand | PPor | PPimplies | PPiff
+  | PPand | PPand_asym | PPor | PPor_asym | PPimplies | PPiff
 
 type pp_unop =
   | PPnot

src/parser/typing.ml

@@ -254,7 +254,7 @@ let rec dterm uc gvars denv {pp_desc = desc; pp_loc = loc} =
         | (op,de2) :: ch ->
             let de12 = Dterm.dterm ~loc (make_app de1 op de2) in
             let de23 = Dterm.dterm ~loc (make_chain de2 ch) in
-            DTbinop (Tand, de12, de23)
+            DTbinop (DTand, de12, de23)
         | [] -> assert false in
       let rec get_chain e12 acc = match e12.pp_desc with
         | PPinfix (e1, op1, e2) when chainable_op uc op1 ->
@@ -294,10 +294,12 @@ let rec dterm uc gvars denv {pp_desc = desc; pp_loc = loc} =
       let e1 = dterm uc gvars denv e1 in
       let e2 = dterm uc gvars denv e2 in
       let op = match op with
-        | PPand -> Tand
-        | PPor -> Tor
-        | PPimplies -> Timplies
-        | PPiff -> Tiff in
+        | PPand -> DTand
+        | PPand_asym -> DTand_asym
+        | PPor -> DTor
+        | PPor_asym -> DTor_asym
+        | PPimplies -> DTimplies
+        | PPiff -> DTiff in
       DTbinop (op, e1, e2)
   | PPquant (q, uqu, trl, e1) ->
       let qvl = List.map (quant_var uc) uqu in