Commit 42f7b67e authored by David Hauzar's avatar David Hauzar

Merge branch 'master' into counter-examples

parents 86cdaeee 016365db
......@@ -1426,8 +1426,15 @@ install_local:: bin/why3doc
# trywhy3
#########
ALTERGODIR=src/trywhy3/alt-ergo-0.99.1
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3
-syntax camlp4o -I src/trywhy3 -I $(ALTERGODIR)/src/parsing
ALTERGOMODS=util/numbers util/version util/options parsing/why_parser parsing/why_lexer
TRYWHY3CMO=lib/why3/why3.cma
# $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
......@@ -1438,7 +1445,7 @@ src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
src/trywhy3/trywhy3.byte: lib/why3/why3.cma src/trywhy3/trywhy3.cmo
src/trywhy3/trywhy3.byte: $(TRYWHY3CMO) src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/%.cmo: src/trywhy3/%.ml
......
......@@ -65,8 +65,8 @@ let do_input f =
exit 1
| Some d ->
try
printf "@[<hov 2>Execution of %s.%s ():@\n" mid name;
Mlw_interp.eval_global_symbol env m d;
printf "@[<hov 2>Execution of %s.%s ():@\n%a" mid name
(Mlw_interp.eval_global_symbol env m) d
with e when Debug.test_noflag Debug.stack_trace ->
printf "@\n@]@.";
raise e in
......
......@@ -5,12 +5,9 @@
*)
let get_opt o =
Js.Opt.get o (fun () -> assert false)
let log s =
Firebug.console ## log (Js.string s)
let get_opt o = Js.Opt.get o (fun () -> assert false)
let log s = Firebug.console ## log (Js.string s)
(*
......@@ -86,9 +83,14 @@ let run_alt_ergo_on_task t =
(* printing the task in a string *)
Driver.print_task alt_ergo_driver str_formatter t;
let text = flush_str_formatter () in
(* TODO ! *)
(* from Alt-Ergo:
let lb = Lexing.from_string text in
(* from Alt-Ergo *)
(* does not work yet: it requires zarith
--> investigate how to compile alt-ergo with nums instead
let a = Why_parser.file Why_lexer.token lb in
*)
(* TODO ! *)
(*
let ltd, typ_env = Why_typing.file false Why_typing.empty_env a in
let declss = Why_typing.split_goals ltd in
SAT.start ();
......@@ -156,8 +158,35 @@ let why3_execute (modules,_theories) =
Stdlib.Mstr.fold
(fun _k m acc ->
let th = m.Mlw_module.mod_theory in
let name = th.Theory.th_name.Ident.id_string in
[Html.of_string ("Module " ^ name)] :: acc)
let modname = th.Theory.th_name.Ident.id_string in
try
let ps =
Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
in
let moduleans = Html.of_string ("Module " ^ modname ^ ": ") in
let ans =
match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
| None ->
[moduleans;
Html.ul
[[Html.of_string "function main has no definition"]]]
| Some d ->
try
[moduleans;
Html.ul
[[Html.of_string
(Pp.sprintf "Execution of main () returns:@\n%a"
(Mlw_interp.eval_global_symbol env m) d)]]]
with e ->
[moduleans;
Html.ul
[[Html.of_string
(Pp.sprintf
"exception during execution of function main : %a (%s)"
Exn_printer.exn_printer e
(Printexc.to_string e))]]]
in ans :: acc
with Not_found -> acc)
modules []
in
Html.ul mods
......
......@@ -19,7 +19,7 @@ let rev_split c s =
let rec aux acc i =
try
let j = String.index_from s i c in
aux ((String.sub s i (j-i))::acc) (j + 1)
aux (String.sub s i (j-i) :: acc) (j + 1)
with Not_found -> (String.sub s i (String.length s - i))::acc
| Invalid_argument _ -> ""::acc in
aux [] 0
......@@ -28,12 +28,12 @@ let split c s = List.rev (rev_split c s)
let rev_bounded_split c s n =
let rec aux acc i n =
let get_rest_of_s = (String.sub s i (String.length s - i)) in
if n = 1 then get_rest_of_s::acc else
let get_rest_of_s i = (String.sub s i (String.length s - i)) in
if n = 1 then get_rest_of_s i :: acc else
try
let j = String.index_from s i c in
aux ((String.sub s i (j-i))::acc) (j+1) (n-1)
with Not_found -> get_rest_of_s::acc
aux (String.sub s i (j-i) :: acc) (j+1) (n-1)
with Not_found -> get_rest_of_s i :: acc
| Invalid_argument _ -> ""::acc in
aux [] 0 n
......
......@@ -1373,7 +1373,7 @@ let eval_global_expr env mkm tkm _writes e =
let eval_global_symbol env m d =
let eval_global_symbol env m fmt d =
let lam = d.Mlw_expr.fun_lambda in
match lam.Mlw_expr.l_args with
| [pvs] when Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
......@@ -1382,7 +1382,7 @@ let eval_global_symbol env m d =
let eff = spec.Mlw_ty.c_effect in
let writes = eff.Mlw_ty.eff_writes in
let body = lam.Mlw_expr.l_expr in
printf "@[<hov 2> type:@ %a@]@."
fprintf fmt "@[<hov 2> type:@ %a@]@."
Mlw_pretty.print_vty body.Mlw_expr.e_vty;
(* printf "effect: %a@\n" *)
(* Mlw_pretty.print_effect body.Mlw_expr.e_effect; *)
......@@ -1393,26 +1393,26 @@ let eval_global_symbol env m d =
in
match res with
| Normal _ ->
printf "@[<hov 2> result:@ %a@\nglobals:@ %a@]@."
fprintf fmt "@[<hov 2> result:@ %a@\nglobals:@ %a@]@."
print_logic_result res print_vsenv final_env
(*
printf "@[<hov 2> result:@ %a@\nstate :@ %a@]@."
fprintf fmt "@[<hov 2> result:@ %a@\nstate :@ %a@]@."
(print_result m.Mlw_module.mod_known
m.Mlw_module.mod_theory.Theory.th_known st) res
print_state st
*)
| Excep _ ->
printf "@[<hov 2>exceptional result:@ %a@\nglobals:@ %a@]@."
fprintf fmt "@[<hov 2>exceptional result:@ %a@\nglobals:@ %a@]@."
print_logic_result res print_vsenv final_env;
(*
printf "@[<hov 2>exceptional result:@ %a@\nstate:@ %a@]@."
fprintf fmt "@[<hov 2>exceptional result:@ %a@\nstate:@ %a@]@."
(print_result m.Mlw_module.mod_known
m.Mlw_module.mod_theory.Theory.th_known st) res
print_state st;
*)
exit 1
| Irred _ | Fun _ ->
printf "@\n@]@.";
fprintf fmt "@\n@]@.";
eprintf "Execution error: %a@." print_logic_result res;
exit 2
end
......
......@@ -15,8 +15,8 @@ type value
val print_value: Format.formatter -> value -> unit
val eval_global_term:
val eval_global_term:
Env.env -> Decl.known_map -> Term.term -> value
val eval_global_symbol:
Env.env -> Mlw_module.modul -> Mlw_expr.fun_defn -> unit
Env.env -> Mlw_module.modul -> Format.formatter -> Mlw_expr.fun_defn -> unit
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