Interp: debug array support

src/whyml/mlw_interp.ml

@@ -329,6 +329,8 @@ let exec_array_get _env _spec s args =
               | _ -> assert false
             in
             let t = eval_map_get (Some ty) !ls_map_get [m;i] in
+            eprintf "[interp] t[%a] -> %a@."
+              Pretty.print_term i Pretty.print_term t;
             Normal t,s
           | _ -> assert false
       end
@@ -362,6 +364,8 @@ let exec_array_set env spec s args =
               with Not_found -> reg
             in
             let s' = Mreg.add reg t s in
+            eprintf "[interp] t[%a] <- %a@."
+              Pretty.print_term i Pretty.print_term v; 
             Normal (Mlw_expr.t_void),s'
           | _ -> assert false
       end

tests/test_exec.mlw

@@ -158,6 +158,11 @@ module Array
     with Found i -> i
     end
 
+  let incr (t:array int) : unit =
+    for i=0 to t.length - 1 do
+      t[i] <- t[i]+1
+    done
+
   let test0 () = let t = Array.make 2 21 in t[0]+t[1]
 
   let test1 () =
@@ -178,19 +183,12 @@ module Array
      t[2] <- 67;
      t
 
-  let tbis () = t ()
-
-  let t0 () =
-     let t = Array.make 3 0 in
-     t[0] <- 12;
-     t[1] <- 42;
-     t[2] <- 67;
-     t[0] + t[1] + t[2] (* 121 *)
-
   let t1 () = 
     let t = t () in
     t[0] + t[1] + t[2] (* 121 *)
 
+  let i () = incr (t ())
+
   let test12 () = search (t ()) 12
   let test42 () = search (t ()) 42
   let test67 () = search (t ()) 67