Commit 3d5022d0 authored by Francois Bobot's avatar Francois Bobot

bench_plugins : mise à jour des plugins

parent 82884097
......@@ -234,9 +234,9 @@ BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte
bin/why.byte --driver bench/plugins/helloworld.drv -I theories/ \
--output-dir - --goal Test.G src/test.why
--output-file - --goal Test.G src/test.why
bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I theories/ \
--output-dir - --goal Test.G src/test.why
--output-file - --goal Test.G src/test.why
bin/why.$(OCAMLBEST) --driver bench/plugins/simplify_array.drv -I theories/ \
--output-file - --goal Test_simplify_array.G src/test.why
......
......@@ -19,7 +19,7 @@
let print_context _ fmt _ = Format.fprintf fmt "helloworld@\n"
let transform_context = Register.identity_trans
let transform_context = Register.identity
let () =
Driver.register_printer "helloworld" print_context;
......
......@@ -21,13 +21,18 @@ open Term
open Theory
open Env
let prelude = ["prelude"]
let prelude = ["array"]
let array = "Array"
let store = ["store"]
let select = ["select"]
let make_rt_rf env =
let array = find_theory env prelude array in
let array =
try
find_theory env prelude array
with TheoryNotFound (l,s) ->
Format.eprintf "The theory %a is unknown" print_theorynotfound (l,s);
exit 1 in
let store = (ns_find_ls array.th_export store).ls_name in
let select = (ns_find_ls array.th_export select).ls_name in
let rec rt t =
......
......@@ -63,3 +63,5 @@ let find_theory env sl s =
let env_tag env = env.env_tag
let print_theorynotfound fmt (l,s) =
Format.fprintf fmt "%s.%s" (String.concat "." l) s
......@@ -33,3 +33,4 @@ val env_tag : env -> int
exception TheoryNotFound of string list * string
val print_theorynotfound : Format.formatter -> string list * string -> unit
......@@ -226,8 +226,8 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = try
find_theory env qfile id
with Env.TheoryNotFound(l,s) -> errorm ~loc "theory %s.%s not found"
(String.concat "." l) s in
with Env.TheoryNotFound (l,s) -> errorm ~loc "theory %a not found"
Env.print_theorynotfound (l,s) in
let add_htheory cloned id t =
try
let t2,t3 = Hid.find driver.drv_theory id in
......
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