Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 79b0c0a0 authored by MARCHE Claude's avatar MARCHE Claude

interp: fixed last bug with arrays, added some tests in bench

parent 951ca18f
......@@ -66,6 +66,18 @@ valid_goals () {
done
}
execute () {
echo -n "$1 $2... "
if $pgm $1 --exec $2 > /dev/null 2>&1; then
echo "ok"
else
echo "execution test failed!"
echo $pgm $1 --exec $2
$pgm $1 --exec $2
exit 1
fi
}
list_stuff () {
echo -n "$1 "
if $pgm $1 > /dev/null 2>&1; then
......@@ -109,6 +121,13 @@ goods examples/bitvectors "-I examples/bitvectors"
goods examples/in_progress
echo ""
echo "=== Checking execution ==="
execute examples/euler001.mlw Euler001.run
execute examples/euler002.mlw Solve.run
# fails execute examples/same_fringe.mlw Test.test1
execute examples/selection_sort.mlw SelectionSort.test2
echo ""
echo "=== Checking drivers ==="
drivers drivers
echo ""
......@@ -125,3 +144,4 @@ list_stuff --list-formats
list_stuff --list-metas
list_stuff --list-debug-flags
echo ""
......@@ -169,5 +169,5 @@ module Euler001
div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2
let run () = solve 1000
(* should return 233168 *)
end
......@@ -589,7 +589,7 @@ let do_exec env fname cin exec =
| [pvs] when Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
printf "@[<hov 2>Execution of %s ():@\n" x;
let body = lam.Mlw_expr.l_expr in
printf "type : @[%a@]@\n"
printf "type : @[%a@]"
Mlw_pretty.print_vty body.Mlw_expr.e_vty;
(* printf "effect: %a@\n" *)
(* Mlw_pretty.print_effect body.Mlw_expr.e_effect; *)
......@@ -598,9 +598,17 @@ let do_exec env fname cin exec =
m.Mlw_module.mod_known m.Mlw_module.mod_theory.Theory.th_known
lam.Mlw_expr.l_expr
in
printf "result: %a@\nstate: %a@]@."
Mlw_interp.print_result res
Mlw_interp.print_state st
begin
match res with
| Mlw_interp.Normal _ | Mlw_interp.Excep _ ->
printf "@\nresult: %a@\nstate: %a@]@."
Mlw_interp.print_result res
Mlw_interp.print_state st
| Mlw_interp.Irred _ | Mlw_interp.Fun _ ->
printf "@]@.";
eprintf "Execution error: %a@." Mlw_interp.print_result res;
exit 1
end
| _ ->
eprintf "Only functions with one unit argument can be executed.@.";
exit 1
......
This diff is collapsed.
......@@ -17,7 +17,11 @@ val print_value: Format.formatter -> value -> unit
val eval_global_term: Env.env -> Decl.known_map -> Term.term -> value
type result
type result = private
| Normal of value
| Excep of Mlw_ty.xsymbol * value
| Irred of Mlw_expr.expr
| Fun of Mlw_expr.psymbol * Mlw_ty.pvsymbol list * int
val print_result: Format.formatter -> result -> unit
......
......@@ -95,9 +95,9 @@ theory T
constant t2 : map int int = t[2<-37]
constant y0 : int = t2[0]
constant y1 : int = t2[1]
constant y2 : int = t2[2]
constant y0 : int = t2[0] (* should be 0 *)
constant y1 : int = t2[1] (* should be 42 *)
constant y2 : int = t2[2] (* should be 37 *)
constant t3 : map int int = t2[1<-12]
......
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