Commit eb78f282 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: command line option -L instead of -I to be consistent with why

parent 44e05191
...@@ -241,7 +241,7 @@ clean:: ...@@ -241,7 +241,7 @@ clean::
# test target # test target
%: %.mlw bin/whyml.byte %: %.mlw bin/whyml.byte
bin/whyml.byte -I theories $*.mlw bin/whyml.byte -L theories $*.mlw
############### ###############
# proof manager # proof manager
...@@ -474,7 +474,7 @@ clean:: ...@@ -474,7 +474,7 @@ clean::
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
sh bench/bench \ sh bench/bench \
"bin/why.@OCAMLBEST@" \ "bin/why.@OCAMLBEST@" \
"bin/whyml.@OCAMLBEST@ -I theories" "bin/whyml.@OCAMLBEST@ -L theories"
BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO)) BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
...@@ -515,7 +515,7 @@ test: bin/why.byte $(TOOLS) ...@@ -515,7 +515,7 @@ test: bin/why.byte $(TOOLS)
@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done @for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
testl: bin/whyml.byte testl: bin/whyml.byte
ocamlrun -bt bin/whyml.byte -I theories/ tests/test-pgm-jcf.mlw ocamlrun -bt bin/whyml.byte -L theories/ tests/test-pgm-jcf.mlw
############### ###############
# installation # installation
......
...@@ -27,14 +27,17 @@ let parse_only = ref false ...@@ -27,14 +27,17 @@ let parse_only = ref false
let type_only = ref false let type_only = ref false
let debug = ref false let debug = ref false
let loadpath = ref [] let loadpath = ref []
let prover = ref None
let () = let () =
Arg.parse Arg.parse
["--parse-only", Arg.Set parse_only, "stops after parsing"; ["--parse-only", Arg.Set parse_only, "stops after parsing";
"--type-only", Arg.Set type_only, "stops after type-checking"; "--type-only", Arg.Set type_only, "stops after type-checking";
"--debug", Arg.Set debug, "sets the debug flag"; "--debug", Arg.Set debug, "sets the debug flag";
"-I", Arg.String (fun s -> loadpath := s :: !loadpath), "-L", Arg.String (fun s -> loadpath := s :: !loadpath),
"<dir> adds dir to the loadpath"; "<dir> adds dir to the loadpath";
"-P", Arg.String (fun s -> prover := Some s),
"<prover> proves the verification conditions";
] ]
(fun f -> files := f :: !files) (fun f -> files := f :: !files)
"usage: whyl [options] files..." "usage: whyl [options] files..."
......
open Why open Why
open Ident
open Term
open Decl
open Theory
open Pgm_ttree
let file uc _dl = let wp _l _e = f_true (* TODO *)
let wp_recfun _l _def = f_true (* TODO *)
let add_wp_decl uc l f =
let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
let d = create_prop_decl Pgoal pr f in
add_decl uc d
let decl uc = function
| Dlet (l, e) ->
let f = wp l e in
add_wp_decl uc l f
| Dletrec dl ->
let add_one uc (l, def) = let f = wp_recfun l def in add_wp_decl uc l f in
List.fold_left add_one uc dl
| Dparam _ ->
uc
let file uc dl =
let uc = List.fold_left decl uc dl in
Theory.close_theory uc Theory.close_theory uc
...@@ -3,3 +3,6 @@ open Why ...@@ -3,3 +3,6 @@ open Why
open Theory open Theory
val file : theory_uc -> Pgm_ttree.file -> theory val file : theory_uc -> Pgm_ttree.file -> theory
(** takes as input the result of [Pgm_typing.file] and produces
a theory containing the verification conditions as goals,
one for each function *)
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