CN: Add implies logical binary operator for specs

This commit adds `implies` as a new, infix logical binary operator for
the spec language.  It does not implement it for the runtime testing.
The reason we use a new keyword "implies" instead of a more natural
`==>` is that currently the lexer is shared between C and CN, and and so
we cannot add `==>` to CN without adding it to C, which is incorrect
because C does not support that token.

Fixes rems-project#329

backend/cn/cn_internal_to_ail.ml

@@ -323,7 +323,7 @@ let cn_to_ail_binop_internal bt1 bt2 =
   | SetDifference -> failwith "TODO cn_to_ail_binop: SetDifference"
   | SetMember -> failwith "TODO cn_to_ail_binop: SetMember"
   | Subset  -> failwith "TODO cn_to_ail_binop: Subset"
-  | Impl -> failwith "TODO cn_to_ail_binop: Impl"
+  | Implies -> failwith "TODO cn_to_ail_binop: Impl"
 
 (* Assume a specific shape, where sym appears on the RHS (i.e. in e2) *)
 
@@ -1449,7 +1449,7 @@ let cn_to_ail_logical_constraint_internal : type a. (_ Cn.cn_datatype) list -> (
           cn_to_ail_expr_internal dts globals it d
         | LogicalConstraints.Forall ((sym, bt), it) -> 
           let (cond_it, t) = match IT.term it with 
-            | Binop (Impl, it, it') -> (it, it')
+            | Binop (Implies, it, it') -> (it, it')
             | _ -> failwith "Incorrect form of forall logical constraint term"
         in
 

backend/cn/compile.ml

@@ -568,6 +568,8 @@ module EffectfulTranslation = struct
         return (IT (Binop (Or, e1, e2), SBT.Bool, loc))
     | CN_and, SBT.Bool ->
         return (IT (Binop (And, e1, e2), SBT.Bool, loc))
+    | CN_implies, SBT.Bool ->
+        return (IT (Binop (Implies, e1, e2), SBT.Bool, loc))
     | CN_map_get, _ ->
        let@ rbt = match IT.bt e1 with
          | Map (_, rbt) -> return rbt

backend/cn/diagnostics.ml

@@ -59,7 +59,7 @@ let term_with_model_name nm cfg x =
 let bool_subterms1 t = match IT.term t with
   | IT.Binop (And, it,it') -> [it;it']
   | IT.Binop (Or, it,it') -> [it;it']
-  | IT.Binop (Impl, x, y) -> [x; y]
+  | IT.Binop (Implies, x, y) -> [x; y]
   | IT.Unop (Not, x) -> [x]
   | IT.Binop (EQ, x, y) -> if BT.equal (IT.bt x) BT.Bool
       then [x; y] else []

backend/cn/eqTable.ml

@@ -38,7 +38,7 @@ let add_eq_sym (guard, lhs, rhs) tab =
 
 let add_one_eq (tab : table) (it : IT.t) = match IT.term it with
   | IT.Binop (IT.EQ, x, y) -> add_eq_sym (None, x, y) tab
-  | IT.Binop (Impl, guard, x) -> begin match IT.is_eq x with
+  | IT.Binop (Implies, guard, x) -> begin match IT.is_eq x with
     | Some (y, z) -> add_eq_sym (Some guard, y, z) tab
     | _ -> tab
   end

backend/cn/indexTerms.ml

@@ -453,6 +453,10 @@ let is_or = function
   | IT (Binop (Or, it, it'), _, _) -> Some (it, it')
   | _ -> None
 
+let is_implies = function
+  | IT (Binop (Implies, it, it'), _, _) -> Some (it, it')
+  | _ -> None
+
 let is_not = function
   | IT (Unop (Not, it), _, _) -> Some it
   | _ -> None
@@ -533,7 +537,7 @@ let and2_ (it, it') loc = IT (Binop (And, it, it'), BT.Bool, loc)
 let or2_ (it, it') loc = IT (Binop (Or, it, it'), BT.Bool, loc)
 let and_ its loc = vargs_binop (bool_ true loc) (Tools.curry (fun p -> and2_ p loc)) its
 let or_ its loc = vargs_binop (bool_ false loc) (Tools.curry (fun p -> or2_ p loc)) its
-let impl_ (it, it') loc = IT (Binop (Impl, it, it'), BT.Bool, loc)
+let impl_ (it, it') loc = IT (Binop (Implies, it, it'), BT.Bool, loc)
 let not_ it loc = IT (Unop (Not, it), bt it, loc)
 let ite_ (it, it', it'') loc = IT (ITE (it, it', it''), bt it', loc)
 let eq_ (it, it') loc =
@@ -558,7 +562,7 @@ let let_ ((nm, x), y) loc = IT (Let ((nm, x), y), basetype y, loc)
 (*   match term it with *)
 (*   | And xs -> or_ (List.map not_ xs) *)
 (*   | Or xs -> and_ (List.map not_ xs) *)
-(*   | Impl (x, y) -> and_ [x; not_ y] *)
+(*   | Implies (x, y) -> and_ [x; not_ y] *)
 (*   | _ -> not_ it *)
 
 

backend/cn/lemmata.ml

@@ -340,7 +340,7 @@ let it_adjust (global : Global.t) it =
             let x = f x in
             let y = f y in
             if IT.equal x y then IT.bool_ true loc else IT.eq__ x y loc
-        | IT.Binop (Impl, x, y) ->
+        | IT.Binop (Implies, x, y) ->
             let x = f x in
             let y = f y in
             if IT.is_false x || IT.is_true y then IT.bool_ true loc else IT.impl_ (x, y) loc
@@ -788,7 +788,7 @@ let it_to_coq loc global list_mono it =
        | LTPointer -> abinop (if enc_prop then "<" else "<?") x y
        | And -> abinop (if enc_prop then "/\\" else "&&") x y
        | Or -> abinop (if enc_prop then "\\/" else "||") x y
-       | Impl -> abinop (if enc_prop then "->" else "implb") x y
+       | Implies -> abinop (if enc_prop then "->" else "implb") x y
        | _ -> do_fail "arith op"
        end
     | IT.Match (x, cases) ->

backend/cn/simplify.ml

@@ -378,7 +378,7 @@ module IndexTerms = struct
       | _ when IT.equal it1 it2 -> it1
       | _ -> IT (Binop (Or, it1, it2), the_bt, the_loc)
       end
-    | Binop (Impl, a, b) ->
+    | Binop (Implies, a, b) ->
        let a = aux a in
        let b = aux b in
        if IT.equal a b then IT (Const (Bool true), the_bt, the_loc)
@@ -393,7 +393,7 @@ module IndexTerms = struct
        | _, IT (Const (Bool false), _, _) ->
           not_ a the_loc
        | _ ->
-          IT (Binop (Impl, a, b), the_bt, the_loc)
+          IT (Binop (Implies, a, b), the_bt, the_loc)
        end
     | Unop (op, a) ->
        let a = aux a in

backend/cn/solver.ml

@@ -791,7 +791,7 @@ module Translate = struct
          | LEPointer -> adj ()
          | And -> Z3.Boolean.mk_and context (map term [t1;t2])
          | Or -> Z3.Boolean.mk_or context (map term [t1;t2])
-         | Impl -> Z3.Boolean.mk_implies context (term t1) (term t2)
+         | Implies -> Z3.Boolean.mk_implies context (term t1) (term t2)
          end
       | ITE (t1, t2, t3) -> Z3.Boolean.mk_ite context (term t1) (term t2) (term t3)
       | EachI _ -> adj ()

backend/cn/terms.ml

@@ -28,7 +28,7 @@ type unop =
 type binop =
   | And
   | Or
-  | Impl
+  | Implies
   | Add
   | Sub
   | Mul
@@ -189,8 +189,8 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.document -> Pp.document) ->
           mparens (flow (break_op (ampersand ^^ ampersand)) [aux true it1; aux true it2])
        | Or ->
           mparens (flow (break_op (bar ^^ bar)) [aux true it1; aux true it2])
-       | Impl ->
-          mparens (flow (break_op (minus ^^ rangle ())) [aux true it1; aux true it2])
+       | Implies ->
+         c_app !^"implies" [aux true it1; aux true it2]
        | Add ->
           mparens (flow (break_op plus) [aux true it1; aux true it2])
        | Sub ->
@@ -393,7 +393,7 @@ let rec dtree (IT (it_, bt, loc)) =
   | Binop (op, t1, t2) ->
      Dnode (pp_ctor (show_binop op), [dtree t1; dtree t2])
   | ITE (t1, t2, t3) ->
-     Dnode (pp_ctor "Impl", [dtree t1; dtree t2; dtree t3])
+     Dnode (pp_ctor "Implies", [dtree t1; dtree t2; dtree t3])
   | EachI ((starti,(i,_),endi), body) ->
      Dnode (pp_ctor "EachI", [
            Dleaf !^(string_of_int starti);

backend/cn/wellTyped.ml

@@ -551,10 +551,10 @@ module WIT = struct
             let@ t = check loc Bool t in
             let@ t' = check loc Bool t' in
             return (IT (Binop (Or, t, t'), Bool, loc))
-         | Impl ->
+         | Implies ->
             let@ t = check loc Bool t in
             let@ t' = check loc Bool t' in
-            return (IT (Binop (Impl, t, t'), Bool, loc))
+            return (IT (Binop (Implies, t, t'), Bool, loc))
          end
       | ITE (t,t',t'') ->
          let@ t = check loc Bool t in

frontend/model/cn.lem

@@ -53,6 +53,7 @@ type cn_binop =
   | CN_ge
   | CN_or
   | CN_and
+  | CN_implies
   | CN_map_get
 
 

ocaml_frontend/cn_ocaml.ml

@@ -103,6 +103,7 @@ module MakePp (Conf: PP_CN) = struct
     | CN_ge -> P.rangle ^^ P.equals
     | CN_or -> P.bar ^^ P.bar
     | CN_and -> P.ampersand ^^ P.ampersand
+    | CN_implies -> P.equals ^^ P.equals ^^ P.rangle
     | CN_map_get -> P.string "CN_map_get"
 
   let pp_cn_c_kind = function

ocaml_frontend/pprinters/pp_ail.ml

@@ -378,7 +378,6 @@ let pp_binaryOperator = function
   | Eq             -> P.equals ^^ P.equals
   | Ne             -> P.bang   ^^ P.equals
 
-
 let pp_unaryOperator = function
   | Plus        -> P.plus
   | Minus       -> P.minus

parsers/c/c_lexer.mll

@@ -83,7 +83,6 @@ let keywords: (string * Tokens.token) list = [
     "__volatile__", ASM_VOLATILE;
     "__builtin_types_compatible_p", BUILTIN_TYPES_COMPATIBLE_P;
     "__builtin_choose_expr", BUILTIN_CHOOSE_EXPR;
-
   ]
 
 let lexicon: (string, token) Hashtbl.t =
@@ -150,6 +149,7 @@ let cn_keywords: (string * Tokens.token) list = [
     "datatype"      , CN_DATATYPE;
     "type_synonym"  , CN_TYPE_SYNONYM;
     "_"             , CN_WILD;
+    "implies"       , CN_IMPLIES;
   ]
 
 let cn_lexicon: (string, token) Hashtbl.t =

parsers/c/c_parser.mly

@@ -151,7 +151,7 @@ type asm_qualifier =
 %token CN_LET CN_TAKE CN_OWNED CN_BLOCK CN_EACH CN_FUNCTION CN_LEMMA CN_PREDICATE
 %token CN_DATATYPE CN_TYPE_SYNONYM CN_SPEC CN_ARRAY_SHIFT CN_MEMBER_SHIFT
 %token CN_UNCHANGED CN_WILD CN_MATCH
-%token CN_GOOD CN_NULL CN_TRUE CN_FALSE
+%token CN_GOOD CN_NULL CN_TRUE CN_FALSE CN_IMPLIES
 %token <string * [`U|`I] * int> CN_CONSTANT
 
 %token EOF
@@ -1978,10 +1978,18 @@ bool_and_expr:
 | e1= bool_and_expr AMPERSAND_AMPERSAND e2= rel_expr
     { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos, $endpos) (PointCursor $startpos($2)))
                                , CNExpr_binop (CN_and, e1, e2))) }
-bool_or_expr:
+
+bool_implies_expr:
 | e = bool_and_expr
     { e }
-| e1= bool_or_expr PIPE_PIPE e2= bool_and_expr
+| e1= bool_and_expr CN_IMPLIES e2= bool_implies_expr (* implication arrow ==> *)
+    { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos, $endpos) (PointCursor $startpos($2)))
+                               , CNExpr_binop (CN_implies, e1, e2))) }
+
+bool_or_expr:
+| e = bool_implies_expr
+    { e }
+| e1= bool_or_expr PIPE_PIPE e2= bool_implies_expr
     { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos, $endpos) (PointCursor $startpos($2)))
                                , CNExpr_binop (CN_or, e1, e2))) }
 
@@ -2497,4 +2505,4 @@ cn_toplevel:
     { elems }
 
 
-(* END CN *)
+(* END CN *)