Exec: support for the "for" loop

src/whyml/mlw_interp.ml

@@ -461,6 +461,27 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
         | Normal _, s' -> eval_expr env s' e
         | _ -> r
     end
+  | Efor(pvs,(pvs1,dir,pvs2),_inv,e1) ->
+    begin 
+      try
+        let a = big_int_of_term (Mvs.find pvs1.pv_vs env.vsenv) in
+        let b = big_int_of_term (Mvs.find pvs2.pv_vs env.vsenv) in
+        let le,suc = match dir with
+          | To -> Big_int.le_big_int, Big_int.succ_big_int
+          | DownTo -> Big_int.ge_big_int, Big_int.pred_big_int
+        in
+        let rec iter i s =
+          if le i b then
+            let env' = bind_vs pvs.pv_vs (term_of_big_int i) env in
+            match eval_expr env' s e1 with
+              | Normal _,s' -> iter (suc i) s'
+              | r -> r
+          else Normal t_void, s
+        in
+        iter a s
+      with
+          NotNum -> Irred e,s
+    end
   | Ecase(e1,ebl) ->
     begin
       match eval_expr env s e1 with
@@ -474,7 +495,6 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
   | Eassign _
   | Eghost _
   | Eany _
-  | Efor _
   | Eabstr _
   | Eassert _
   | Eabsurd ->

tests/test_exec.mlw

@@ -11,6 +11,35 @@ module M
   let y () : list int =
     Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)
 
+end
+
+module Map
+
+  use import int.Int
+  use import map.Map
+
+  exception Found int
+
+  let search (t:map int int) (len:int) (v:int) : int =
+    try
+      for i=0 to len-1 do
+        if t[i] = v then raise (Found i)
+      done;
+      -1
+    with Found i -> i
+    end
+
+  constant t : map int int = (const 0)[0 <- 12][1 <- 42][2 <- 67]
+
+  let test12 () = search t 3 12
+  let test42 () = search t 3 42
+  let test67 () = search t 3 67
+  let test0 () = search t 3 0
+
+end
+
+module Ref
+
   use import ref.Ref
 
   val r: ref int