alternative syntax for logical connectives

CHANGES

 * marks an incompatible change
 
 
+  o new syntax for logical connections
+      conjunction and     /\
+      disjunction or      \/
+      negation    not     ~
+      implication implies ->
+      equivalence iff     <->
   o fixed Alt-ergo output: no triggers for "exists" quantifier
   o [IDE] tool "Replay" works
   o [IDE] does not use Threads anymore, thanks to Call_provers.query_call

src/parser/lexer.mll

@@ -57,6 +57,8 @@
 	"forall", FORALL;
 	"goal", GOAL;
 	"if", IF;
+	"iff", IFF;
+	"implies", IMPLIES;
 	"import", IMPORT;
 	"in", IN;
 	"inductive", INDUCTIVE;
@@ -235,7 +237,11 @@ rule token = parse
       { AMPAMP }
   | "||"
       { BARBAR }
-  | "\\"
+  | "/\\"
+      { AND }
+  | "\\/"
+      { OR }
+   | "\\"
       { LAMBDA }
   | "\\?"
       { PRED }
@@ -253,6 +259,8 @@ rule token = parse
       { LEFTSQ }
   | "]"
       { RIGHTSQ }
+  | "~"
+      { TILDE }
   | op_char_pref op_char_4* as s
       { OPPREF s }
   | op_char_1234* op_char_1 op_char_1234* as s

src/parser/parser.pre.mly

@@ -159,7 +159,7 @@
 
 %token AND AS AXIOM CLONE
 %token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
-%token GOAL IF IMPORT IN INDUCTIVE LEMMA
+%token GOAL IF IFF IMPLIES IMPORT IN INDUCTIVE LEMMA
 %token LET LOGIC MATCH META NAMESPACE NOT PROP OR
 %token THEN THEORY TRUE TYPE USE WITH
 
@@ -180,7 +180,7 @@
 %token LRARROW
 %token PRED QUOTE
 %token RIGHTPAR RIGHTREC RIGHTSQ
-%token UNDERSCORE
+%token TILDE UNDERSCORE
 
 %token EOF
 
@@ -204,7 +204,7 @@
 %nonassoc prec_named
 %nonassoc COLON
 
-%right ARROW LRARROW
+%right ARROW IMPLIES LRARROW IFF
 %right OR BARBAR
 %right AND AMPAMP
 %nonassoc NOT
@@ -518,8 +518,12 @@ type_var:
 lexpr:
 | lexpr ARROW lexpr
    { infix_pp $1 PPimplies $3 }
+| lexpr IMPLIES lexpr
+   { infix_pp $1 PPimplies $3 }
 | lexpr LRARROW lexpr
    { infix_pp $1 PPiff $3 }
+| lexpr IFF lexpr
+   { infix_pp $1 PPiff $3 }
 | lexpr OR lexpr
    { infix_pp $1 PPor $3 }
 | lexpr BARBAR lexpr
@@ -528,6 +532,8 @@ lexpr:
    { infix_pp $1 PPand $3 }
 | lexpr AMPAMP lexpr
    { mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPand $3)) }
+| TILDE lexpr
+   { prefix_pp PPnot $2 }
 | NOT lexpr
    { prefix_pp PPnot $2 }
 | lexpr EQUAL lexpr

tests/test-jcf.why

 
+theory T
 
+  type answer = Yes | No | MayBe
+
+  type tree 'a = Leaf | Node (tree 'a) 'a (tree 'a)
+
+  type answer_tree 'a = (tree 'a, answer)
+
+  use import int.Int
+  use import int.MinMax
+
+  logic height (t: tree 'a) : int = match t with
+    | Leaf -> 0
+    | Node l _ r -> 1 + max (height l) (height r)
+  end
+
+  logic sorted (t: tree int) (min: int) (max: int) = match t with
+    | Leaf -> true
+    | Node l x r -> sorted l min x /\ min <= x <= max /\ sorted r x max
+  end
+
+  use import list.List
+
+  inductive sub (list 'a) (list 'a) =
+    | empty: sub (Nil: list 'a) (Nil: list 'a)
+    | cons : forall x: 'a, s1 s2: list 'a. 
+             sub s1 s2 -> sub (Cons x s1) (Cons x s2)
+    | dive : forall x: 'a, s1 s2: list 'a. 
+             sub s1 s2 -> sub s1 (Cons x s2)
+
+  logic abs (x: int) : int = if x >= 0 then x else -x
+
+end
+
+theory T2 
+
+  type tree = Node int forest
+  with forest = Empty | Cons tree forest
+
+end
 
 theory Records
 

theories/int.why

@@ -6,7 +6,7 @@ theory Int
 
   logic (< ) int int
   logic (> ) (x y : int) = y < x
-  logic (<=) (x y : int) = x < y or x = y
+  logic (<=) (x y : int) = x < y \/ x = y
 
   clone export algebra.OrderedUnitaryCommutativeRing with
      type t = int, logic zero = zero, logic one = one, logic (<=) = (<=)
@@ -43,7 +43,7 @@ theory EuclideanDivision
     forall x y:int. y <> 0 -> x = y * div x y + mod x y
 
   axiom Div_bound:
-    forall x y:int. x >= 0 and y > 0 -> 0 <= div x y <= x
+    forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
 
   axiom Mod_bound:
     forall x y:int. y <> 0 -> 0 <= mod x y < abs y
@@ -66,22 +66,22 @@ theory ComputerDivision
     forall x y:int. y <> 0 -> x = y * div x y + mod x y
 
   axiom Div_bound:
-    forall x y:int. x >= 0 and y > 0 -> 0 <= div x y <= x
+    forall x y:int. x >= 0 /\ y > 0 -> 0 <= div x y <= x
 
   axiom Mod_bound:
     forall x y:int. y <> 0 -> - abs y < mod x y < abs y
 
   axiom Div_sign_pos:
-    forall x y:int. x >= 0 and y > 0 -> div x y >= 0
+    forall x y:int. x >= 0 /\ y > 0 -> div x y >= 0
 
   axiom Div_sign_neg:
-    forall x y:int. x <= 0 and y > 0 -> div x y <= 0
+    forall x y:int. x <= 0 /\ y > 0 -> div x y <= 0
 
   axiom Mod_sign_pos:
-    forall x y:int. x >= 0 and y <> 0 -> mod x y >= 0
+    forall x y:int. x >= 0 /\ y <> 0 -> mod x y >= 0
 
   axiom Mod_sign_neg:
-    forall x y:int. x <= 0 and y <> 0 -> mod x y <= 0
+    forall x y:int. x <= 0 /\ y <> 0 -> mod x y <= 0
 
   lemma Rounds_toward_zero:
     forall x y:int. y <> 0 -> abs (div x y * y) <= abs x
@@ -95,11 +95,11 @@ theory ComputerDivision
   lemma Mod_inf: forall x y:int. 0 <= x < y -> mod x y = x
 
   lemma Div_mult: forall x y z:int [div (x * y + z) x]. 
-          x > 0 and y >= 0 and z >= 0 ->
+          x > 0 /\ y >= 0 /\ z >= 0 ->
           div (x * y + z) x = y + div z x
 
   lemma Mod_mult: forall x y z:int [mod (x * y + z) x]. 
-          x > 0 and y >= 0 and z >= 0 ->
+          x > 0 /\ y >= 0 /\ z >= 0 ->
           mod (x * y + z) x = mod z x
 
 end
@@ -227,8 +227,8 @@ theory Gcd
   use import Divisibility
 
   logic gcd (a b g : int) =
-    divides g a and
-    divides g b and
+    divides g a /\
+    divides g b /\
     forall x : int. divides x a -> divides x b -> divides x g
 
   lemma Gcd_sym : forall a b g : int. gcd a b g -> gcd b a g