Commit 54d845ec authored by MARCHE Claude's avatar MARCHE Claude
Browse files

test, en attendant whyconf

parent 94ea9df4
......@@ -717,6 +717,12 @@ module Goal = struct
end
*)
let from_id db id : goal =
assert false
(*
let sql="SELECT goal.id, goal.task_checksum, goal.parent_id, goal.name, goal.pos_id, goal.proved, goal_pos.id, goal_pos.file, goal_pos.line, goal_pos.start, goal_pos.stop, goal_parent.id, goal_parent.name, goal_parent.obsolete FROM goal LEFT JOIN transf AS goal_parent ON (goal_parent.id = goal.parent_id) LEFT JOIN loc AS goal_pos ON (goal_pos.id = goal.pos_id) " ^ q in
let stmt=Sqlite3.prepare db.db sql in
*)
(* General get function for any of the columns *)
(*
......@@ -1022,6 +1028,26 @@ module Transf = struct
end
module Main = struct
let init db =
let sql = "create table if not exists rootgoals (goal_id integer);" in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
()
let all_root_goals db =
let sql="SELECT goal_id FROM rootgoals" in
let stmt=Sqlite3.prepare db.raw_db sql in
let of_stmt stmt =
match Sqlite3.column stmt 0 with
| Sqlite3.Data.INT i -> i
| x -> (try Int64.of_string (Sqlite3.Data.to_string x)
with _ -> failwith "Db.all_root_goals")
in
let goals_ids = step_fold db stmt of_stmt in
goals_ids
end
let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
match !current_db with
......@@ -1035,17 +1061,23 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
in
current_db := Some db;
Loc.init db;
External_proof.init db;
(*
External_proof.init db;
Goal.init db;
Transf.init db;
*)
Main.init db
| Some _ -> failwith "database already opened"
let init_base f = init_db f
let root_goals () = assert false (* TODO *)
let root_goals () =
let db = current () in
let l = Main.all_root_goals db in
List.rev_map (Goal.from_id db) l
......
open Format
open Why
let autodetection () =
......@@ -16,7 +17,7 @@ let () =
try
Whyconf.read_config_file ()
with Not_found ->
Format.eprintf "No .why.conf file found. Running autodetection of provers.@.";
eprintf "No .why.conf file found. Running autodetection of provers.@.";
autodetection ();
exit 0
......@@ -24,8 +25,6 @@ let () =
let provers = Whyconf.known_provers ()
open Format
let () =
printf "Provers: ";
List.iter
......@@ -41,15 +40,47 @@ let loadpath = ["../theories"]
let env = Why.Env.create_env (Why.Typing.retrieve loadpath)
let m =
let cin = open_in (fname ^ ".why") in
let m = Why.Typing.read_channel env fname cin in
close_in cin;
m
let () = Db.init_base (fname ^ ".prm")
let () =
printf "previously known goals:@\n";
List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
printf "@."
let rec report fmt = function
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e
| Parsing.Parse_error ->
fprintf fmt "syntax error"
| Denv.Error e ->
Denv.report fmt e
| Typing.Error e ->
Typing.report fmt e
| Decl.UnknownIdent i ->
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short
| Driver.Error e ->
Driver.report fmt e
| Dynlink_compat.Dynlink.Error e ->
fprintf fmt "Dynlink : %s" (Dynlink_compat.Dynlink.error_message e)
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let m : Why.Theory.theory Why.Theory.Mnm.t =
try
let cin = open_in (fname ^ ".why") in
let m = Why.Typing.read_channel env fname cin in
close_in cin;
eprintf "Parsing/Typing Ok@.";
m
with e ->
eprintf "%a@." report e;
exit 1
let do_task tname (th : Why.Theory.theory) (task : Why.Task.task) : unit =
(*
if !opt_prove then begin
......@@ -93,10 +124,25 @@ let do_theory tname th glist =
List.iter (do_task tname th) tasks
let () =
eprintf "looking for goals@.";
let glist = Queue.create () in
let add_th t th mi = Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi in
let do_th _ (t,th) = do_theory t th glist in
Why.Ident.Mid.iter do_th (Why.Theory.Mnm.fold add_th m Why.Ident.Mid.empty)
let add_th t th mi =
eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi
in
let do_th _ (t,th) =
eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
do_theory t th glist
in
Why.Ident.Mid.iter do_th (Why.Theory.Mnm.fold add_th m Why.Ident.Mid.empty);
eprintf "Done@."
(*
Local Variables:
compile-command: "make -C ../.. bin/manager.byte"
End:
*)
......
theory Test
use import int.Int
goal Test1: 2+2 = 4
goal Test2: forall x:int. x*x >= 0
end
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