Commit 139d7f44 authored by MARCHE Claude's avatar MARCHE Claude

[Interp] support for Array.copy

parent c8375280
......@@ -146,8 +146,7 @@ execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
# fails: needs support for Array.copy
# examples/verifythis_PrefixSumRec.mlw --exec PrefixSumRec.bench
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
execute examples/vstte10_queens.mlw NQueens.test8
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
# examples/queens.mlw --exec NQueensBits.test8
......
......@@ -112,7 +112,8 @@ module Test
if a[0] <> 4 then raise BenchFailure;
if a[1] <> 3 then raise BenchFailure;
if a[2] <> 1 then raise BenchFailure;
if a[3] <> 0 then raise BenchFailure
if a[3] <> 0 then raise BenchFailure;
a
end
......
......@@ -174,6 +174,8 @@ module Euler001
exception BenchFailure
let bench () raises { BenchFailure -> true } =
if run () <> 233168 then raise BenchFailure
let x = run () in
if x <> 233168 then raise BenchFailure;
x
end
......@@ -157,6 +157,8 @@ module Solve
exception BenchFailure
let bench () raises { BenchFailure -> true } =
if run () <> 4613732 then raise BenchFailure
let x = run () in
if x <> 4613732 then raise BenchFailure;
x
end
......@@ -58,7 +58,8 @@ module InsertionSort
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure
if a[7] <> 413 then raise BenchFailure;
a
end
......
......@@ -62,6 +62,7 @@ module Quicksort
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure
if a[7] <> 413 then raise BenchFailure;
a
end
......@@ -54,6 +54,7 @@ module SelectionSort
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure
if a[7] <> 413 then raise BenchFailure;
a
end
......@@ -216,6 +216,7 @@ module PrefixSumRec
if a[4] <> 11 then raise BenchFailure;
if a[5] <> 15 then raise BenchFailure;
if a[6] <> 16 then raise BenchFailure;
if a[7] <> 22 then raise BenchFailure
if a[7] <> 22 then raise BenchFailure;
a
end
......@@ -184,7 +184,8 @@ let test () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let x = lcp arr 1 2 in
if x <> 1 then raise BenchFailure
if x <> 1 then raise BenchFailure;
x
end
......@@ -309,7 +310,8 @@ module SuffixSort_test
if suf[0] <> 3 then raise BenchFailure;
if suf[1] <> 0 then raise BenchFailure;
if suf[2] <> 2 then raise BenchFailure;
if suf[3] <> 1 then raise BenchFailure
if suf[3] <> 1 then raise BenchFailure;
suf
end
......@@ -419,7 +421,8 @@ let test () =
if sa.suffixes[0] <> 3 then raise BenchFailure;
if sa.suffixes[1] <> 0 then raise BenchFailure;
if sa.suffixes[2] <> 2 then raise BenchFailure;
if sa.suffixes[3] <> 1 then raise BenchFailure
if sa.suffixes[3] <> 1 then raise BenchFailure;
sa
end
......@@ -531,6 +534,7 @@ module LRS_test
arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-6;
lrs arr;
if !solStart <> 1 then raise BenchFailure;
if !solLength <> 1 then raise BenchFailure
if !solLength <> 1 then raise BenchFailure;
(!solStart, !solLength)
end
......@@ -78,6 +78,7 @@ module TestCase
assert { m = 10 };
(* bench of --exec *)
if s <> 45 then raise BenchFailure;
if m <> 10 then raise BenchFailure
if m <> 10 then raise BenchFailure;
(s,m)
end
......@@ -88,12 +88,13 @@ module Combinators
constant i : term = App (App S K) K
let test_SKK ()
diverges
diverges (* would be hard to prove terminating *)
raises { BenchFailure -> true }
= let t = reduction (App i i) in
if t <> i then raise BenchFailure;
let t = reduction (App (App (App (App K K) K) K) K) in
if t <> K then raise BenchFailure
= let t1 = reduction (App i i) in
if t1 <> i then raise BenchFailure;
let t2 = reduction (App (App (App (App K K) K) K) K) in
if t2 <> K then raise BenchFailure;
(t1, t2)
(* an irreducible term is a value *)
......
......@@ -604,18 +604,28 @@ let builtin_array_type kn its =
let exec_array_make env s vty args =
match args with
| [Vnum n;def] ->
(**)
let m = Vmap(def,Nummap.empty) in
let v = Vapp(!array_cons_ls,[Vnum n;m]) in
let s',v' = to_program_value env s vty v in
(**)
(*
let v = Varray(n,def,Nummap.empty) in
*)
Normal v',s'
| _ ->
raise CannotCompute
let exec_array_copy env s vty args =
match args with
| [Vapp(ls,[len;m])] when ls_equal ls !array_cons_ls ->
begin
match m with
| Vreg r ->
let m = Mreg.find r s in
let v = Vapp(!array_cons_ls,[len;m]) in
let s',v' = to_program_value env s vty v in
Normal v',s'
| _ -> raise CannotCompute
end
| _ ->
raise CannotCompute
let exec_array_get _env s _vty args =
match args with
| [t;Vnum i] ->
......@@ -704,6 +714,7 @@ let built_in_modules =
"mixfix []", None, exec_array_get ;
"length", None, exec_array_length ;
"mixfix []<-", None, exec_array_set ;
"copy", None, exec_array_copy ;
] ;
]
......
(* obsolete
module M
use import int.Int
use import module ref.Ref
val x : ref int
goal A : !x = 0
goal B : (old !x) = 0
function f (n:int) : int = n + ! x
goal C : f(3) = 4
use import ref.Ref
val f (n:int) : bool
ensures { if result then n >= 0 else n <= 0 }
end
*)
module Termination
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment