Implemented missing operators.

frontend/coq_ast.ml

@@ -28,7 +28,7 @@ type un_op =
 
 type bin_op =
   | AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
-  | ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | RoundDownOp | RoundUpOp
+  | ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
 
 type value =
   | Null

frontend/coq_pp.ml

@@ -110,9 +110,9 @@ let pp_bin_op : Coq_ast.bin_op pp = fun ff op ->
   | MulOp       -> "×"
   | DivOp       -> "/"
   | ModOp       -> "%"
-  | AndOp       -> "..." (* TODO *)
-  | OrOp        -> "..." (* TODO *)
-  | XorOp       -> "..." (* TODO *)
+  | AndOp       -> "&"
+  | OrOp        -> "|"
+  | XorOp       -> "^"
   | ShlOp       -> "<<"
   | ShrOp       -> ">>"
   | EqOp        -> "="
@@ -121,8 +121,6 @@ let pp_bin_op : Coq_ast.bin_op pp = fun ff op ->
   | GtOp        -> ">"
   | LeOp        -> "≤"
   | GeOp        -> "≥"
-  | RoundDownOp -> "..." (* TODO *)
-  | RoundUpOp   -> "..." (* TODO *)
 
 let rec pp_expr : Coq_ast.expr pp = fun ff e ->
   let pp fmt = Format.fprintf ff fmt in

theories/lang/lang.v

@@ -133,7 +133,7 @@ Definition u64 : int_type := {| it_size := 3; it_signed := false; |}.
 (* see http://compcert.inria.fr/doc/html/compcert.cfrontend.Cop.html#binary_operation *)
 Inductive bin_op : Set :=
 | AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
-| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp | RoundDownOp | RoundUpOp
+| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
 (* Ptr is the second argument and pffset the first *)
 | PtrOffsetOp (ly : layout).
 

theories/lang/notation.v

@@ -40,6 +40,12 @@ Notation "e1 <<{ ot1 , ot2 } e2" := (BinOp ShlOp ot1 ot2 e1%E e2%E)
   (at level 70, format "e1  <<{ ot1 ,  ot2 }  e2") : expr_scope.
 Notation "e1 >>{ ot1 , ot2 } e2" := (BinOp ShrOp ot1 ot2 e1%E e2%E)
   (at level 70, format "e1  >>{ ot1 ,  ot2 }  e2") : expr_scope.
+Notation "e1 &{ ot1 , ot2 } e2" := (BinOp AndOp ot1 ot2 e1%E e2%E)
+  (at level 70, format "e1  &{ ot1 ,  ot2 }  e2") : expr_scope.
+Notation "e1 |{ ot1 , ot2 } e2" := (BinOp OrOp ot1 ot2 e1%E e2%E)
+  (at level 70, format "e1  |{ ot1 ,  ot2 }  e2") : expr_scope.
+Notation "e1 ^{ ot1 , ot2 } e2" := (BinOp XorOp ot1 ot2 e1%E e2%E)
+  (at level 70, format "e1  ^{ ot1 ,  ot2 }  e2") : expr_scope.
 (* The offset must be evaluated first for the type system to work, thus the order is switched here. *)
 Notation "e1 'at_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrOffsetOp ly) ot2 ot1 e2%E e1%E)
   (at level 70, format "e1  at_offset{ ly ,  ot1 ,  ot2 }  e2") : expr_scope.