Parser: rename [_.._] to [..] for consistency with other bracket ops

doc/qualid.bnf

@@ -12,7 +12,7 @@
               | "[]"              ;   collection access
               | "[<-]"            ;   collection update
               | "[]<-"            ;   in-place collection update
-              | "[_.._]"          ;   collection slice
+              | "[..]"            ;   collection slice
               | "[_..]"           ;   right-open slice
               | "[.._]"           ;   left-open slice %
 \end{syntax}

doc/term1.bnf

@@ -44,7 +44,7 @@
               | "[]"              ;   collection access
               | "[<-]"            ;   collection update
               | "[]<-"            ;   in-place update
-              | "[_.._]"          ;   collection slice
+              | "[..]"            ;   collection slice
               | "[_..]"           ;   right-open slice
               | "[.._]"           ;   left-open slice %
 \end{syntax}

src/core/pretty.ml

@@ -158,9 +158,9 @@ let print_ts fmt ts =
 let print_ls fmt ({ls_name = {id_string = nm}} as ls) =
   if nm = "mixfix []" then pp_print_string fmt "([])" else
   if nm = "mixfix [<-]" then pp_print_string fmt "([<-])" else
+  if nm = "mixfix [..]" then pp_print_string fmt "([..])" else
   if nm = "mixfix [_..]" then pp_print_string fmt "([_..])" else
   if nm = "mixfix [.._]" then pp_print_string fmt "([.._])" else
-  if nm = "mixfix [_.._]" then pp_print_string fmt "([_.._])" else
   let s = id_unique iprinter ls.ls_name in
   match extract_op s with
   | Some s -> fprintf fmt "(%s)" (escape_op s)
@@ -291,15 +291,15 @@ and print_app pri ls fmt tl =
   | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [<-]" ->
       fprintf fmt (protect_on (pri > 7) "@[%a@,[%a <-@ %a]@]")
         (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
+  | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [..]" ->
+      fprintf fmt (protect_on (pri > 7) "%a[%a..%a]")
+        (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
   | _, [t1;t2] when ls.ls_name.id_string = "mixfix [_..]" ->
       fprintf fmt (protect_on (pri > 7) "%a[%a..]")
         (print_lterm 7) t1 print_term t2
   | _, [t1;t2] when ls.ls_name.id_string = "mixfix [.._]" ->
       fprintf fmt (protect_on (pri > 7) "%a[..%a]")
         (print_lterm 7) t1 print_term t2
-  | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [_.._]" ->
-      fprintf fmt (protect_on (pri > 7) "%a[%a..%a]")
-        (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
   | _, tl ->
       fprintf fmt (protect_on (pri > 6) "@[%a@ %a@]")
         print_ls ls (print_list space (print_lterm 7)) tl

src/driver/driver_lexer.mll

@@ -89,6 +89,8 @@ rule token = parse
       { RIGHTPAR }
   | "."
       { DOT }
+  | ".."
+      { DOTDOT }
   | ","
       { COMMA }
   | "'"

src/driver/driver_parser.mly

@@ -22,7 +22,7 @@
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING
 %token VALID INVALID UNKNOWN FAIL
 %token TIMEOUT OUTOFMEMORY STEPLIMITEXCEEDED TIME STEPS
-%token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
+%token UNDERSCORE LEFTPAR RIGHTPAR DOT DOTDOT QUOTE EOF
 %token BLACKLIST
 %token MODULE EXCEPTION VAL CONVERTER LITERAL
 %token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
@@ -141,6 +141,9 @@ operator:
 | LEFTSQ RIGHTSQ        { Ident.mixfix "[]" }
 | LEFTSQ LARROW RIGHTSQ { Ident.mixfix "[<-]" }
 | LEFTSQ RIGHTSQ LARROW { Ident.mixfix "[]<-" }
+| LEFTSQ DOTDOT RIGHTSQ { Ident.mixfix "[..]" }
+| LEFTSQ UNDERSCORE DOTDOT RIGHTSQ { Ident.mixfix "[_..]" }
+| LEFTSQ DOTDOT UNDERSCORE RIGHTSQ { Ident.mixfix "[.._]" }
 
 (* Types *)
 

src/mlw/expr.ml

@@ -1184,9 +1184,9 @@ let print_rs fmt ({rs_name = {id_string = nm}} as s) =
   if nm = Ident.mixfix "[]" then pp_print_string fmt "([])" else
   if nm = Ident.mixfix "[]<-" then pp_print_string fmt "([]<-)" else
   if nm = Ident.mixfix "[<-]" then pp_print_string fmt "([<-])" else
+  if nm = Ident.mixfix "[..]" then pp_print_string fmt "([..])" else
   if nm = Ident.mixfix "[_..]" then pp_print_string fmt "([_..])" else
   if nm = Ident.mixfix "[.._]" then pp_print_string fmt "([.._])" else
-  if nm = Ident.mixfix "[_.._]" then pp_print_string fmt "([_.._])" else
   match extract_op s.rs_name, s.rs_logic with
   | Some x, _ ->
       fprintf fmt "(%s%s%s)"
@@ -1265,13 +1265,13 @@ let print_capp pri ({rs_name = id} as s) fmt vl =
   | _, [t1;t2;t3] when id.id_string = "mixfix []<-" ->
       fprintf fmt (protect_on (pri > 0) "%a[%a] <- %a")
         print_pv t1 print_pv t2 print_pv t3
+  | _, [t1;t2;t3] when id.id_string = "mixfix [..]" ->
+      fprintf fmt (protect_on (pri > 6) "%a[%a..%a]")
+        print_pv t1 print_pv t2 print_pv t3
   | _, [t1;t2] when id.id_string = "mixfix [_..]" ->
       fprintf fmt (protect_on (pri > 6) "%a[%a..]") print_pv t1 print_pv t2
   | _, [t1;t2] when id.id_string = "mixfix [.._]" ->
       fprintf fmt (protect_on (pri > 6) "%a[..%a]") print_pv t1 print_pv t2
-  | _, [t1;t2;t3] when id.id_string = "mixfix [_.._]" ->
-      fprintf fmt (protect_on (pri > 6) "%a[%a..%a]")
-        print_pv t1 print_pv t2 print_pv t3
   | _, tl ->
       fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
         print_rs s (Pp.print_list Pp.space print_pv) tl
@@ -1284,9 +1284,9 @@ let print_cpur pri ({ls_name = id} as s) fmt vl =
     | _, [_;_] when id.id_string = "mixfix []" -> Some "[]"
     | _, [_;_;_] when id.id_string = "mixfix [<-]" -> Some "[<-]"
     | _, [_;_;_] when id.id_string = "mixfix []<-" -> Some "[]<-"
+    | _, [_;_;_] when id.id_string = "mixfix [..]" -> Some "[..]"
     | _, [_;_] when id.id_string = "mixfix [_..]" -> Some "[_..]"
     | _, [_;_] when id.id_string = "mixfix [.._]" -> Some "[.._]"
-    | _, [_;_;_] when id.id_string = "mixfix [_.._]" -> Some "[_.._]"
     | _ -> None in
   match op, vl with
   | None, [] ->

src/mlw/pmodule.ml

@@ -1215,9 +1215,9 @@ let get_rs_name nm =
   if nm = "mixfix []" then "([])" else
   if nm = "mixfix []<-" then "([]<-)" else
   if nm = "mixfix [<-]" then "([<-])" else
+  if nm = "mixfix [..]" then "([..])" else
   if nm = "mixfix [_..]" then "([_..])" else
   if nm = "mixfix [.._]" then "([.._])" else
-  if nm = "mixfix [_.._]" then "([_.._])" else
   try "(" ^ Strings.remove_prefix "infix " nm ^ ")" with Not_found ->
   try "(" ^ Strings.remove_prefix "prefix " nm ^ "_)" with Not_found ->
   nm

src/parser/parser.mly

@@ -56,7 +56,7 @@
 
   let get_op s e = Qident (mk_id (Ident.mixfix "[]") s e)
   let set_op s e = Qident (mk_id (Ident.mixfix "[<-]") s e)
-  let sub_op s e = Qident (mk_id (Ident.mixfix "[_.._]") s e)
+  let sub_op s e = Qident (mk_id (Ident.mixfix "[..]") s e)
   let above_op s e = Qident (mk_id (Ident.mixfix "[_..]") s e)
   let below_op s e = Qident (mk_id (Ident.mixfix "[.._]") s e)
 
@@ -1183,9 +1183,9 @@ lident_op:
 | LEFTSQ RIGHTSQ          { Ident.mixfix "[]" }
 | LEFTSQ LARROW RIGHTSQ   { Ident.mixfix "[<-]" }
 | LEFTSQ RIGHTSQ LARROW   { Ident.mixfix "[]<-" }
-| LEFTSQ UNDERSCORE DOTDOT UNDERSCORE RIGHTSQ { Ident.mixfix "[_.._]" }
-| LEFTSQ            DOTDOT UNDERSCORE RIGHTSQ { Ident.mixfix "[.._]" }
-| LEFTSQ UNDERSCORE DOTDOT            RIGHTSQ { Ident.mixfix "[_..]" }
+| LEFTSQ DOTDOT RIGHTSQ   { Ident.mixfix "[..]" }
+| LEFTSQ UNDERSCORE DOTDOT RIGHTSQ  { Ident.mixfix "[_..]" }
+| LEFTSQ DOTDOT UNDERSCORE RIGHTSQ  { Ident.mixfix "[.._]" }
 
 op_symbol:
 | OP1 { $1 }

stdlib/seq.mlw

@@ -91,7 +91,7 @@ module Seq
 
   (** [s[i..j]] is the sub-sequence of [s] from element [i] included
       to element [j] excluded *)
-  let function ([_.._]) (s:seq 'a) (i:int) (j:int) : seq 'a
+  let function ([..]) (s:seq 'a) (i:int) (j:int) : seq 'a
     requires { 0 <= i <= j <= length s }
     ensures { length result = j - i }
     ensures { forall k. 0 <= k < j - i -> result[k] = s[i + k] }