some support for sequence slicing in vale

run_scons.sh

@@ -5,7 +5,7 @@
 
 set -e
 
-SCONS_PYTHON_MAJOR_MINOR=3.6
+SCONS_PYTHON_MAJOR_MINOR=3
 
 # Windows-only: print out the directory of the Python associated to SCons
 windows_scons_python_dir () {

tools/Vale/src/ast.fs

@@ -48,6 +48,9 @@ type op =
 | Bop of bop
 | TupleOp of typ list option
 | Subscript
+| Slice
+| SlicePrefix
+| SliceSuffix
 | Update
 | Cond
 | FieldOp of id

tools/Vale/src/emit_common_lemmas.fs

@@ -15,6 +15,7 @@ type build_env =
     proc:proc_decl;
     loc:loc;
     is_instruction:bool;
+    is_no_inline:bool;
     is_quick:bool;
     is_operand:bool;
     is_framed:bool;
@@ -69,6 +70,11 @@ and build_code_stmts (env:env) (benv:build_env) (stmts:stmt list):exp =
   List.fold cons empty (List.rev slist)
 and build_code_block (env:env) (benv:build_env) (stmts:stmt list):exp =
   vaApp "Block" [build_code_stmts env benv stmts]
+and build_function (env:env) (benv:build_env) (stmts:stmt list):exp =
+  // printfn "this is where we emit va_Function";
+    match benv.proc.pname with
+    | Id(id) -> vaApp "Function" [EString id; build_code_stmts env benv stmts]
+    | _ -> internalErr "Function call unexpected ID"
 
 (* Build codegen_success value for body of procedure Q *)
 let rec build_codegen_success_stmt (q:id) (env:env) (s:stmt):exp option list =
@@ -255,7 +261,7 @@ let rec build_lemma_stmt (senv:stmt_env) (s:stmt):ghost * bool * stmt list =
       let codeBody = vaApp "get_whileBody" [code] in
       let i1 = string (gen_lemma_sym ()) in
       let i2 = string (gen_lemma_sym ()) in
-      let (n1, s1, sw1, fw1) = (Reserved ("n" + i1), Reserved ("s" + i1), Reserved ("sW" + i1), Reserved ("fW" + i1)) in
+      let (n1, s1, sw1, fw1) = (Id "loop_ctr", Reserved ("s" + i1), Reserved ("sW" + i1), Reserved ("fW" + i1)) in
       let (sw2, fw2) = (Reserved ("sW" + i2), Reserved ("fW" + i2)) in
       let (codeCond, codeBody, sCodeVars) =
         if !fstar then
@@ -458,6 +464,7 @@ let build_pre_code_via_transform (loc:loc) (env:env) (benv:build_env) (stmts:stm
     {
       fname = Reserved ("transform_" + string_of_id p.pname);
       fghost = NotGhost;
+      // finline = benv.binline;
       ftargs = [];
       fargs = fParams;
       fret_name = None;
@@ -482,6 +489,7 @@ function method{:opaque} va_code_Q(iii:int, dummy:va_operand_reg, dummy2:va_oper
 let build_code (loc:loc) (env:env) (benv:build_env) (stmts:stmt list):(loc * decl) list =
   let p = benv.proc in
   let isTransform = List_mem_assoc (Id "transform") p.pattrs in
+  let isNoInline = benv.is_no_inline in
   let precode = if isTransform then build_pre_code_via_transform loc env benv stmts else [] in
   if p.pghost = Ghost then [] else
   let fParams = make_fun_params p.prets p.pargs in
@@ -498,6 +506,7 @@ let build_code (loc:loc) (env:env) (benv:build_env) (stmts:stmt list):(loc * dec
       fbody =
         if benv.is_instruction then Some (attrs_get_exp (Id "instruction") p.pattrs)
         else if isTransform then Some (eapply (Reserved "get_result") [vaApp ("transform_" + string_of_id p.pname) (List.map EVar fParams)])
+        else if isNoInline then Some(build_function env benv stmts)
         else Some (build_code_block env benv stmts);
       fattrs =
         if benv.is_quick then
@@ -753,6 +762,8 @@ let rec build_proc (envBody:env) (env:env) (loc:loc) (p:proc_decl):decls =
     else []
     in
   let isInstruction = List_mem_assoc (Id "instruction") p.pattrs in
+  let isNoInline = List_mem_assoc (Id "noInline") p.pattrs in
+  // printfn "setting no inline: %b" isNoInline;
   let isOperand = List_mem_assoc (Id "operand") p.pattrs in
   let codeName prefix = Reserved ("code_" + prefix + (string_of_id p.pname)) in
   let isQuick = is_quick_body p.pattrs in
@@ -786,6 +797,7 @@ let rec build_proc (envBody:env) (env:env) (loc:loc) (p:proc_decl):decls =
             proc = p;
             loc = loc;
             is_instruction = isInstruction;
+            is_no_inline = isNoInline;
             is_quick = isQuick;
             is_operand = isOperand;
             is_framed = attrs_get_bool (Id "frame") (p.pghost = NotGhost) p.pattrs;

tools/Vale/src/emit_dafny_text.fs

@@ -87,6 +87,11 @@ let rec string_of_exp_prec prec e =
     | EApply (e, _, es, _)  when is_id e && id_of_exp e = (Id "set") -> ("{" + (String.concat ", " (List.map (r 5) es)) + "}", 90)
     | EOp (Subscript, [e1; e2], _) -> ((r 90 e1) + "[" + (r 90 e2) + "]", 90)
     | EOp (Update, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " := " + (r 90 e3) + "]", 90)
+
+    | EOp (Slice, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + (r 90 e3) + "]", 90)
+    | EOp (SlicePrefix, [e1; e2; e3], _) -> ((r 90 e1) + "[" + " .. " + (r 90 e2) + "]", 90)
+    | EOp (SliceSuffix, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + "]", 90)
+
     | EOp (Cond, [e1; e2; e3], _) -> ("if " + (r 90 e1) + " then " + (r 90 e2) + " else " + (r 90 e3), 0)
     | EOp (FieldOp x, [e], _) -> ((r 90 e) + "." + (sid x), 90)
     | EOp (FieldUpdate x, [e1; e2], _) -> ((r 90 e1) + ".(" + (sid x) + " := " + (r 90 e2) + ")", 90)
@@ -149,7 +154,7 @@ let rec emit_stmt (ps:print_state) (s:stmt):unit =
       ps.PrintLine ("ghost var " + (String.concat ", " (List.map string_of_lhs_formal lhss)) + " := " + (string_of_exp e) + ";")
   | SAssign _ -> emit_stmts ps (eliminate_assign_lhss s)
   | SLetUpdates _ -> internalErr "SLetUpdates"
-  | SBlock ss -> notImplemented "block"
+  | SBlock ss -> emit_block ps ss
   | SIfElse (_, e, ss1, []) ->
       ps.PrintLine ("if (" + (string_of_exp e) + ")");
       emit_block ps ss1

tools/Vale/src/emit_vale_text.fs

@@ -110,6 +110,11 @@ let rec string_of_exp_prec (prec:int) (e:exp):string =
     | EOp (Bop _, ([] | [_] | (_::_::_::_)), _) -> internalErr "binary operator"
     | EOp (Subscript, [e1; e2], _) -> ((r 90 e1) + "[" + (r 90 e2) + "]", 90)
     | EOp (Update, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " := " + (r 90 e3) + "]", 90)
+
+    | EOp (Slice, [e1; e2; e3], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + (r 90 e3) + "]", 90)
+    | EOp (SlicePrefix, [e1; e2], _) -> ((r 90 e1) + "[" + " .. " + (r 90 e2) + "]", 90)
+    | EOp (SliceSuffix, [e1; e2], _) -> ((r 90 e1) + "[" + (r 90 e2) + " .. " + "]", 90)
+
     | EOp (Cond, [e1; e2; e3], _) -> ("if " + (r 90 e1) + " then " + (r 90 e2) + " else " + (r 90 e3), 0)
     | EOp (FieldOp x, [e], _) -> ((r 90 e) + "." + (sid x), 90)
     | EOp (FieldUpdate x, [e1; e2], _) -> ((r 90 e1) + ".(" + (sid x) + " := " + (r 90 e2) + ")", 90)

tools/Vale/src/lex.fsl

@@ -35,6 +35,9 @@ let operatorToken (tok:string) (isCustom:bool) (s:string):(loc -> token) option
   | "=" -> Some (fun loc -> EQ (loc, (isCustom, s)))
   | "|" -> Some (fun loc -> BAR (loc, (isCustom, s)))
   | ":=" -> Some (fun loc -> COLONEQ (loc, (isCustom, s)))
+
+  | ".." -> Some (fun loc -> DOTDOT (loc, (isCustom, s)))
+
   | "@=" -> Some (fun loc -> ATEQ (loc, (isCustom, s)))
   | "<=" -> Some (fun loc -> LE (loc, (isCustom, s)))
   | ">=" -> Some (fun loc -> GE (loc, (isCustom, s)))

tools/Vale/src/parse.fsy

@@ -57,6 +57,7 @@ let storageAttrs (a:attrs):(var_storage * attrs) =
 %token <loc * (bool * string)> PLUS MINUS STAR SLASH PERCENT
 %token <loc * (bool * string)> AMPAMP BARBAR LTEQEQ EQEQGT LTEQEQGT
 %token <loc * (bool * string)> ATEQ COLONEQ
+%token <loc * (bool * string)> DOTDOT
 %token <loc> HAVOC OLD THIS
 %token <loc> IS THEN ELSE LET IN OUT INOUT REVEAL GHOST INLINE
 %token <loc> TTYPE TYPE OPERAND_TYPE VAR CONST READONLY FUNCTION AXIOM EXTERN PROCEDURE STATIC MODULE IMPORT OPERATOR
@@ -171,6 +172,11 @@ Exp1
   | Exp1 QLBRACKET Exp RBRACKET { expAt $2 (EOp (Bop BIn, [$3; $1], None)) }
   | Exp1 LBRACKET Exp RBRACKET { expAt $2 (EOp (Subscript, [$1; $3], None)) }
   | Exp1 LBRACKET Exp COLONEQ Exp RBRACKET { expAt $2 (EOp (Update, [$1; $3; $5], None)) }
+
+  | Exp1 LBRACKET Exp DOTDOT Exp RBRACKET { expAt $2 (EOp (Slice, [$1; $3; $5], None)) }
+  | Exp1 LBRACKET DOTDOT Exp RBRACKET { expAt $2 (EOp (SlicePrefix, [$1; $4], None)) } 
+  | Exp1 LBRACKET Exp DOTDOT RBRACKET { expAt $2 (EOp (SliceSuffix, [$1; $3], None)) } 
+
   | Exp1 DOT AnyId { expAt $2 (EOp (FieldOp $3, [$1], None)) }
   | Exp1 DOT AnyId LPAREN Exps RPAREN { expAt $4 (EApply (EVar (exp2id $1 $3, None), None, $5, None)) }
   | Exp1 DOT LPAREN AnyId COLONEQ Exp RPAREN { expAt $2 (EOp (FieldUpdate $4, [$1; $6], None)) }
@@ -233,6 +239,9 @@ OpToken
   | LTEQEQGT { $1 }
   | LBRACKET RBRACKET { ($1, (false, "[]")) }
   | LBRACKET COLONEQ RBRACKET { ($1, (false, "[:=]")) }
+
+  | LBRACKET DOTDOT RBRACKET { ($1, (false, "[..]")) }
+
   | QLBRACKET RBRACKET { ($1, (false, "?[]")) }
   | DOT ID { ($1, (false, "." + snd $2 )) }
   | DOT ID COLONEQ { ($1, (false, "." + snd $2 + ":=")) }

tools/Vale/src/typechecker.fs

@@ -1461,6 +1461,48 @@ and infer_exp (env:env) (u:unifier) (e:exp) (expected_typ:typ option):(typ * aex
       | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (Update, es))
       | _ -> internalErr ("EOp Update")
     )
+  | EOp (Slice, [e1; e2; e3], _) ->
+    (
+      let (t1, ae1) = infer_exp_force env u e1 expected_typ in
+      let x =
+        match t1 with
+        | TName (Id x) | TApply (Id x, _) -> x
+        | _ -> err (sprintf "cannot find overloaded operator([..]) function for collection of type %s" (string_of_typ t1))
+        in
+      let e = eapply (Operator (x + "[..]")) [e1; e2; e3] in
+      let (t, ae) = infer_exp env u e expected_typ in
+      match ae with
+      | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (Slice, es))
+      | _ -> internalErr ("EOp Slice")
+    )
+  | EOp (SlicePrefix, [e1; e2], _) ->
+    (
+      let (t1, ae1) = infer_exp_force env u e1 expected_typ in
+      let x =
+        match t1 with
+        | TName (Id x) | TApply (Id x, _) -> x
+        | _ -> err (sprintf "cannot find overloaded operator([..]) function for collection of type %s" (string_of_typ t1))
+        in
+      let e = eapply (Operator (x + "[..]")) [e1; e2; e2] in // repeated e2, probably not the best workaround
+      let (t, ae) = infer_exp env u e expected_typ in
+      match ae with
+      | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (SlicePrefix, es))
+      | _ -> internalErr ("EOp SlicePrefix")
+    )
+  | EOp (SliceSuffix, [e1; e2], _) ->
+    (
+      let (t1, ae1) = infer_exp_force env u e1 expected_typ in
+      let x =
+        match t1 with
+        | TName (Id x) | TApply (Id x, _) -> x
+        | _ -> err (sprintf "cannot find overloaded operator([..]) function for collection of type %s" (string_of_typ t1))
+        in
+      let e = eapply (Operator (x + "[..]")) [e1; e2; e2] in // repeated e2,probably not the best workaround
+      let (t, ae) = infer_exp env u e expected_typ in
+      match ae with
+      | (AE_ApplyX (_, _, _, es), _, _) -> ret t (AE_Op (SliceSuffix, es))
+      | _ -> internalErr ("EOp SliceSuffix")
+    )
   | EOp (Bop BIn, [e1; e2], _) ->
     (
       let (t2, ae2) = infer_exp_force env u e2 expected_typ in
@@ -1931,6 +1973,7 @@ let rec tc_stmt (env:env) (s:stmt):stmt =
       SIfElse (g, e, b1, b2)
   | SWhile (e, invs, ed, b) ->
       let (t, e) = tc_exp env e (Some tBool) in
+      let env = push_id env (Id "loop_ctr") (TInt (NegInf, Inf)) in
       let invs = List_mapSnd (fun e -> let (_, e) = tc_exp env e (Some tProp) in e) invs in
       let ed = mapSnd (List.map (fun e -> let (_, e) = tc_exp env e None in e)) ed in
       let (_, b) = tc_stmts env b in
@@ -2101,6 +2144,10 @@ let tc_decl (env:env) (decl:((loc * decl) * bool)):(env * ((loc * decl) * bool)
           | (Operator "[]", _) -> err "operator([]) expects two arguments (the first argument must be a named type)"
           | (Operator "[:=]", [(_, Some (TName (Id x) | (TApply (Id x, _)))); _; _]) -> Operator (x + "[:=]")
           | (Operator "[:=]", _) -> err "operator([:=]) expects three arguments (the first argument must be a named type)"
+
+          | (Operator "[..]", [(_, Some (TName (Id x) | (TApply (Id x, _)))); _; _]) -> Operator (x + "[..]")
+          | (Operator "[..]", _) -> err "operator([..]) expects three arguments (the first argument must be a named type)"
+
           | (Operator "?[]", [(_, Some (TName (Id x) | (TApply (Id x, _)))); _]) -> Operator (x + "?[]")
           | (Operator "?[]", _) -> err "operator(?[]) expects two arguments (the first argument must be a named type)"
           | (Operator xf, [(_, Some (TName (Id xt) | (TApply (Id xt, _)))); _])