Commit ce8468c6 authored by MARCHE Claude's avatar MARCHE Claude

prover can now parse TPTP files (but still cannot run on them...)

parent fd472796
...@@ -34,8 +34,8 @@ MLALL=$(MLTYPES) $(MLIMPL) ...@@ -34,8 +34,8 @@ MLALL=$(MLTYPES) $(MLIMPL)
ML=$(patsubst %,%.ml,$(MLALL)) ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL)) CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDE) INCLUDES=-I $(BD) $(INCLUDEALL) -I ../../../plugins/tptp
LIBS=unix.cmxa $(BIGINTLIB).cmxa why3extract.cmxa LIBS=unix.cmxa nums.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx
WHY3FLAGS=-L . --debug ignore_unused_vars WHY3FLAGS=-L . --debug ignore_unused_vars
MLFLAGS= MLFLAGS=
...@@ -45,6 +45,7 @@ MLEXECFLAGS= ...@@ -45,6 +45,7 @@ MLEXECFLAGS=
.PHONY: clean depend extract replay .PHONY: clean depend extract replay
$(BD)/prover: $(CMX) run.cmx $(BD)/prover: $(CMX) run.cmx
echo "WHY3SHARE="$(WHY3SHARE)
$(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \ $(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $^ -o $(BD)/prover $^
......
...@@ -77,7 +77,7 @@ let run_test name l = ...@@ -77,7 +77,7 @@ let run_test name l =
let t = Unix.gettimeofday () -. t in let t = Unix.gettimeofday () -. t in
Format.printf "Unsat (time = %.02f)@.@." t Format.printf "Unsat (time = %.02f)@.@." t
let () = let run_all_tests () =
run_test "drinker" (ProverTest__Impl.drinker ()); run_test "drinker" (ProverTest__Impl.drinker ());
run_test "group" (ProverTest__Impl.group ()); run_test "group" (ProverTest__Impl.group ());
run_test "bidon1" (ProverTest__Impl.bidon1 ()); run_test "bidon1" (ProverTest__Impl.bidon1 ());
...@@ -103,3 +103,31 @@ let () = ...@@ -103,3 +103,31 @@ let () =
run_test "zenon10 14" (ProverTest__Impl.zenon10 (n 14)); run_test "zenon10 14" (ProverTest__Impl.zenon10 (n 14));
*) *)
printf "End of tests.@." printf "End of tests.@."
let run_file file =
try
let _ast = Tptp_lexer.load file in
(* check_file ast; *)
(* printf "%a@." pr_file ast; *)
printf "File '%s' is OK.@." file;
exit 0
with
| Tptp_lexer.FileNotFound f ->
eprintf "File not found: %s@." f; exit 2
(*
| Unsupported s ->
eprintf "File %s: '%s' is not supported@." file s; exit 1
*)
| e ->
eprintf "Parsing error: %a@." Why3.Exn_printer.exn_printer e;
exit 2
let () =
if Array.length Sys.argv = 1 then run_all_tests ()
else
if Array.length Sys.argv = 2 then run_file Sys.argv.(1)
else
begin
eprintf "Usage: %s [file]@\nInternal tests are run if no file is given@." Sys.argv.(0);
exit 2
end
...@@ -41,6 +41,7 @@ DATADIR = $datadir ...@@ -41,6 +41,7 @@ DATADIR = $datadir
OCAMLBEST = @OCAMLBEST@ OCAMLBEST = @OCAMLBEST@
BIGINTLIB = @BIGINTLIB@ BIGINTLIB = @BIGINTLIB@
INCLUDE = @BIGINTINCLUDE@ -I @OCAMLINSTALLLIB@/why3 INCLUDE = @BIGINTINCLUDE@ -I @OCAMLINSTALLLIB@/why3
INCLUDEALL = @BIGINTINCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ -I @OCAMLINSTALLLIB@/why3
" > $makefileconfig " > $makefileconfig
fi fi
...@@ -85,7 +85,7 @@ let check_op op = ...@@ -85,7 +85,7 @@ let check_op op =
let rec check_expr e = match e.e_node with let rec check_expr e = match e.e_node with
| Elet(e1,e2) -> unsupported "let" | Elet(e1,e2) -> unsupported "let"
| Eite(e1,e2,e3) -> unsupported "ite" | Eite(e1,e2,e3) -> unsupported "ite"
| Eqnt(q,vl,e) -> unsupported "qnt" | Eqnt(q,vl,e) -> check_expr e
| Ebin(op,e1,e2) -> check_op op; check_expr e1; check_expr e2 | Ebin(op,e1,e2) -> check_op op; check_expr e1; check_expr e2
| Enot e -> check_expr e | Enot e -> check_expr e
| Eequ(e1,e2) -> unsupported "equ" | Eequ(e1,e2) -> unsupported "equ"
...@@ -101,7 +101,19 @@ let check_top_formula f = ...@@ -101,7 +101,19 @@ let check_top_formula f =
| TypedAtom _ -> unsupported "TypedAtom" | TypedAtom _ -> unsupported "TypedAtom"
| Sequent _ -> unsupported "Sequent" | Sequent _ -> unsupported "Sequent"
let check_role _r = () let check_role r =
match r with
| Axiom -> ()
| Hypothesis -> ()
| Definition -> unsupported "Definition"
| Assumption -> ()
| Corollary -> ()
| Lemma -> ()
| Theorem -> ()
| Conjecture -> ()
| Negated_conjecture -> ()
| Type -> unsupported "Type"
let check_kind k = let check_kind k =
match k with match k with
...@@ -119,18 +131,26 @@ let check_file a = List.iter check_decl a ...@@ -119,18 +131,26 @@ let check_file a = List.iter check_decl a
let () = let () =
if Array.length Sys.argv <> 2 then if Array.length Sys.argv <> 2 then
eprintf "Usage: %s <file>@." Sys.argv.(0) begin
eprintf "Usage: %s <file>@." Sys.argv.(0);
exit 2
end
else else
let file = Sys.argv.(1) in let file = Sys.argv.(1) in
try try
let ast = Tptp_lexer.load file in let ast = Tptp_lexer.load file in
check_file ast; check_file ast;
printf "%a@." pr_file ast (* printf "%a@." pr_file ast; *)
printf "File '%s' is OK.@." file;
exit 0
with with
| Tptp_lexer.FileNotFound f -> eprintf "File not found: %s@." f | Tptp_lexer.FileNotFound f ->
| Unsupported s -> eprintf "File %s: '%s' is not supported@." file s eprintf "File not found: %s@." f; exit 2
| Unsupported s ->
eprintf "File %s: '%s' is not supported@." file s; exit 1
| e -> | e ->
eprintf "Parsing error: %a@." Exn_printer.exn_printer e eprintf "Parsing error: %a@." Exn_printer.exn_printer e;
exit 2
(* (*
Local Variables: Local Variables:
......
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