Add by/so to Why3 keywords

src/parser/lexer.mll

@@ -26,6 +26,7 @@
       [
         "as", AS;
         "axiom", AXIOM;
+        "by", BY;
         "clone", CLONE;
         "coinductive", COINDUCTIVE;
         "constant", CONSTANT;
@@ -50,6 +51,7 @@
         "not", NOT;
         "predicate", PREDICATE;
         "prop", PROP;
+        "so", SO;
         "then", THEN;
         "theory", THEORY;
         "true", TRUE;

src/parser/parser.mly

@@ -158,11 +158,11 @@ end
 
 (* keywords *)
 
-%token AS AXIOM CLONE COINDUCTIVE CONSTANT
+%token AS AXIOM BY CLONE COINDUCTIVE CONSTANT
 %token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
 %token GOAL IF IMPORT IN INDUCTIVE LEMMA
 %token LET MATCH META NAMESPACE NOT PROP PREDICATE
-%token THEN THEORY TRUE TYPE USE WITH
+%token SO THEN THEORY TRUE TYPE USE WITH
 
 (* program keywords *)
 
@@ -201,6 +201,7 @@ end
 %nonassoc COLON
 
 %right ARROW LRARROW
+%right BY SO
 %right OR BARBAR
 %right AND AMPAMP
 %nonassoc NOT
@@ -624,6 +625,8 @@ triggers:
 | BARBAR  { Tor_asym }
 | AND     { Tand }
 | AMPAMP  { Tand_asym }
+| BY      { Tby }
+| SO      { Tso }
 
 quant:
 | FORALL  { Tforall }

src/parser/ptree.ml

@@ -27,7 +27,7 @@ type quant =
   | Tforall | Texists | Tlambda
 
 type binop =
-  | Tand | Tand_asym | Tor | Tor_asym | Timplies | Tiff
+  | Tand | Tand_asym | Tor | Tor_asym | Timplies | Tiff | Tby | Tso
 
 type unop =
   | Tnot

src/parser/typing.ml

@@ -311,14 +311,21 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
   | Ptree.Tbinop (e1, op, e2) ->
       let e1 = dterm uc gvars denv e1 in
       let e2 = dterm uc gvars denv e2 in
-      let op = match op with
-        | Ptree.Tand -> DTand
-        | Ptree.Tand_asym -> DTand_asym
-        | Ptree.Tor -> DTor
-        | Ptree.Tor_asym -> DTor_asym
-        | Ptree.Timplies -> DTimplies
-        | Ptree.Tiff -> DTiff in
-      DTbinop (op, e1, e2)
+      let k op = DTbinop (op, e1, e2) in
+      let et () =
+        let loc = e1.dt_loc in
+        let top = Dterm.dterm ?loc DTtrue in
+        Dterm.dterm ?loc (DTbinop (DTor_asym,e1,top)) in
+      begin match op with
+      | Ptree.Tand -> k DTand
+      | Ptree.Tand_asym -> k DTand_asym
+      | Ptree.Tor -> k DTor
+      | Ptree.Tor_asym -> k DTor_asym
+      | Ptree.Timplies -> k DTimplies
+      | Ptree.Tiff -> k DTiff
+      | Ptree.Tby -> DTbinop (DTimplies, et (), e2)
+      | Ptree.Tso -> DTbinop (DTand, e2,et ())
+      end
   | Ptree.Tquant (q, uqu, trl, e1) ->
       let qvl = List.map (quant_var uc) uqu in
       let denv = denv_add_quant denv qvl in