misfix _[_] and _[_op_] in logic and programs

Makefile.in

@@ -864,7 +864,7 @@ doc/bnf: doc/bnf.mll
 
 doc: $(DOC)
 
-doc/manual.pdf: $(BNFTEX) doc/apidoc.tex doc/manual.tex doc/version.tex
+doc/manual.pdf: $(BNFTEX) doc/*.tex doc/manual.tex doc/version.tex
 	cd doc; $(RUBBER) -d manual.tex
 
 # doc/manual.html: doc/manual.tex doc/version.tex

doc/operator.bnf

@@ -9,7 +9,11 @@
   \
   op-char ::= op-char-1 | op-char-2 | op-char-3 | op-char-4 ;
   \
-  infix-op ::= op-char+
+  infix-op-1 ::= op-char* op-char-1 op-char* ;
   \
-  prefix-op ::= infix-op | "!" op-char-4* | "?" op-char-4* ; %
+  infix-op ::= op-char+ ;
+  \
+  prefix-op ::= op-char+ ;
+  \
+  bang-op ::= "!" op-char-4* | "?" op-char-4* ;%
 \end{syntax}
\ No newline at end of file

doc/syntaxref.tex

@@ -46,7 +46,7 @@ characters they are built from:
 \item level 2: those containing
  characters from \textit{op-char-2}, \textit{op-char-3} or
  \textit{op-char-4};
-\item level 1: all other operators.
+\item level 1: all other operators (non-terminal \textit{infix-op-1}).
 \end{itemize}
 
 \paragraph{Terms.}
@@ -61,11 +61,14 @@ associativities, from lowest to greatest priority:
     \texttt{if then else} / \texttt{let in} & -- \\
     label & -- \\
     cast  & -- \\
-    infix level 1 & left \\
-    infix level 2 & left \\
-    infix level 3 & left \\
-    infix level 4 & left \\
-    prefix        & --   \\
+    infix-op level 1 & left \\
+    infix-op level 2 & left \\
+    infix-op level 3 & left \\
+    infix-op level 4 & left \\
+    prefix-op     & --   \\
+    function application & left \\
+    brackets / ternary brackets & -- \\
+    bang-op       & --   \\
     \hline
   \end{tabular}
 \end{center}

doc/term.bnf

@@ -3,7 +3,10 @@
        | real 			  ; real constant
        | lqualid 		  ; symbol
        | prefix-op term 	  ;
+       | bang-op term 	  ;
        | term infix-op term 	  ;
+       | term "[" term "]"	  ; brackets
+       | term "[" term infix-op-1 term "]" 	  ; ternary brackets
        | lqualid term+ 		  ; function application
        | "if" formula "then" term ;
          "else" term              ; conditional

examples/programs/binary_search.mlw

@@ -16,20 +16,20 @@ module M
   exception Not_found (* raised to signal a search failure *)
 
   let binary_search (a :array int) (v : int) =
-    { forall i1 i2 : int. 0 <= i1 <= i2 < A.length a -> a#i1 <= a#i2 }
+    { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
     try
       let l = ref 0 in
       let u = ref (length a - 1) in
       while !l <= !u do
         invariant {
-	  0 <= l and u < A.length a and 
-          forall i : int. 0 <= i < A.length a -> a#i = v -> l <= i <= u }
+	  0 <= l and u < length a and 
+          forall i : int. 0 <= i < length a -> a[i] = v -> l <= i <= u }
         variant { u - l }
         let m = !l + div (!u - !l) 2 in
         assert { l <= m <= u };
-        if get a m < v then
+        if a[m] < v then
           l := m + 1
-        else if get a m > v then
+        else if a[m] > v then
           u := m - 1
         else 
           raise (Break m)
@@ -38,8 +38,8 @@ module M
     with Break i ->
       i
     end
-    { 0 <= result < A.length a and a#result = v }
-    | Not_found -> { forall i:int. 0 <= i < A.length a -> a#i <> v }
+    { 0 <= result < length a and a[result] = v }
+    | Not_found -> { forall i:int. 0 <= i < length a -> a[i] <> v }
 
 end
 

modules/stdlib.mlw

@@ -18,19 +18,17 @@ end
 module Array
 
   use import int.Int
-  use array.ArrayLength as A
+  use export array.ArrayLength
 
-  mutable type array 'a model A.t int 'a
+  mutable type array 'a model t int 'a
 
-  logic (#) (a : A.t int 'a) (i : int) : 'a = A.get a i
+  parameter ([]) : a : array 'a -> i:int ->
+    { 0 <= i < length a } 'a reads a { result = a[i] }
 
-  parameter get : a : array 'a -> i:int ->
-    { 0 <= i < A.length a } 'a reads a { result = A.get a i }
+  parameter ([<-]) : a : array 'a -> i:int -> v:'a ->
+    { 0 <= i < length a } unit writes a { a = (old a)[i <- v] }
 
-  parameter set : a : array 'a -> i:int -> v:'a ->
-    { 0 <= i < A.length a } unit writes a { a = A.set (old a) i v }
-
-  parameter length : a : array 'a -> {} int reads a { result = A.length a }
+  parameter length : a : array 'a -> {} int reads a { result = length a }
 
 end
 

modules/string.mlw

@@ -7,7 +7,7 @@ module Char
 
   parameter chr : x:int -> { 0 <= x <= 255 } char { result = x }
 
-  parameter code : c:char -> {} int { result = c }
+  parameter code : c:char -> {} int { result = c and 0 <= c <= 255 }
 
 end
 

src/parser/parser.pre.mly

@@ -69,8 +69,9 @@
   let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
   let prefix_pp p a = prefix_ppl (loc ()) p a
 
-  let infix s = "infix " ^ s
+  let infix  s = "infix "  ^ s
   let prefix s = "prefix " ^ s
+  let misfix s = "misfix " ^ s
 
   let mk_id id loc = { id = id; id_lab = []; id_loc = loc }
 
@@ -115,6 +116,14 @@
     in
     mk_apply e
 
+  let mk_misfix2 op e1 e2 =
+    let id = { id = misfix op; id_lab = []; id_loc = loc_i 2 } in
+    mk_expr (mk_apply_id id [e1; e2])
+
+  let mk_misfix3 op e1 e2 e3 =
+    let id = { id = misfix op; id_lab = []; id_loc = loc_i 2 } in
+    mk_expr (mk_apply_id id [e1; e2; e3])
+
   let mk_infix e1 op e2 =
     let id = { id = infix op; id_lab = []; id_loc = loc_i 2 } in
     mk_expr (mk_apply_id id [e1; e2])
@@ -200,11 +209,14 @@
 %right AND AMPAMP
 %nonassoc NOT
 %left EQUAL LTGT OP1
+%nonassoc RIGHTSQ    /* stronger than OP1 for e1[e2 op1 e3] */
 %left OP2
 %left OP3
 %left OP4
 %nonassoc prefix_op
 %left prec_app
+%nonassoc LEFTSQ
+%nonassoc OPPREF
 
 /* Entry points */
 
@@ -570,6 +582,11 @@ lexpr_arg:
    { mk_pp (PPtuple ($2 :: $4)) }
 | OPPREF lexpr_arg
    { mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
+| lexpr_arg LEFTSQ lexpr RIGHTSQ
+   { mk_pp (PPapp (Qident (mk_id (misfix "[]") (loc ())), [$1; $3])) }
+| lexpr_arg LEFTSQ lexpr OP1 lexpr RIGHTSQ
+   { let op = "[" ^ $4 ^ "]" in
+     mk_pp (PPapp (Qident (mk_id (misfix op) (loc ())), [$1; $3; $5])) }
 ;
 
 quant:
@@ -733,6 +750,10 @@ lident_rich:
     { mk_id (prefix $2) (loc ()) }
 | LEFTPAR OPPREF RIGHTPAR
     { mk_id (prefix $2) (loc ()) }
+| LEFTPAR LEFTSQ RIGHTSQ RIGHTPAR
+    { mk_id (misfix "[]") (loc ()) }
+| LEFTPAR LEFTSQ OP1 RIGHTSQ RIGHTPAR
+    { mk_id (misfix ("[" ^ $3 ^ "]")) (loc ()) }
 ;
 
 lident:
@@ -1002,6 +1023,10 @@ simple_expr:
     { mk_expr Eskip }
 | OPPREF simple_expr
     { mk_prefix $1 $2 }
+| simple_expr LEFTSQ expr RIGHTSQ
+    { mk_misfix2 "[]" $1 $3 }
+| simple_expr LEFTSQ expr OP1 expr RIGHTSQ
+    { let op = "[" ^ $4 ^ "]" in mk_misfix3 op $1 $3 $5 }
 ;
 
 list1_simple_expr:

src/programs/TODO

@@ -5,12 +5,8 @@ o what about pervasives old, at, label, unit = ()
 
 o fmla_effect
 
-o bench/programs/good/recfun: FIXME
-
 o fixed precedence of label (label L: e) wrt sequence (e ; e)
 
-o misfix _[_] and _[_] := _ for arrays (both in logic and programs)
-
 o model types (abstract but not mutable)
   abstract types (no model)
 

tests/test-pgm-jcf.mlw

 
+(* theory T *)
+(*   type t *)
+(* end *)
+
 module P
 
   use import int.Int
-  use import module string.String
-
-  let foo (s:string) = { S.length s = 1 } get s 0 { true }
+  use import module stdlib.Array
 
+  let foo (t : array int) = 
+    { A.length t >= 1 && t[0] = 1 }
+    t[0 <- 1];
+    t[0] + 3
+    { result = 3 }
 
 end
 

theories/array.why

@@ -6,6 +6,10 @@ theory Array "Theory of arrays"
   logic get (t 'a 'b) 'a : 'b
   logic set (t 'a 'b) 'a 'b : t 'a 'b
 
+  (* syntactic sugar *)
+  logic ([]) (a : t 'a 'b) (i : 'a) : 'b = get a i
+  logic ([<-]) (a : t 'a 'b) (i : 'a) (v : 'b) : t 'a 'b = set a i v
+
   axiom Select_eq :
     forall m : t 'a 'b. forall a1 a2 : 'a.
     forall b : 'b [get (set m a1 b) a2].
@@ -182,6 +186,6 @@ end
 
 (*
 Local Variables: 
-compile-command: "cd ..; bin/why.opt theories/array.why"
+compile-command: "make -C .. theories/array"
 End: 
 *)