Commit 55f2ec5d authored by MARCHE Claude's avatar MARCHE Claude

theories and goals weel ordered in gui

parent f7831b6d
......@@ -7,33 +7,33 @@
logic mem rbt key value
}
parameter create :
d:value ->
{}
ref rbt
parameter create :
d:value ->
{}
ref rbt
{ default !result = d and
forall k:key, v:value. mem !result k v <-> v = d }
parameter replace :
m:ref rbt -> k:key -> v:value ->
{}
unit writes m
{}
unit writes m
{ default !m = default (old !m) and
forall k':key, v':value.
forall k':key, v':value.
mem !m k' v' <-> if k' = k then v' = v else mem (old !m) k' v' }
parameter lookup :
m:ref rbt -> k:key ->
{}
value reads m
m:ref rbt -> k:key ->
{}
value reads m
{ mem !m k result }
parameter remove :
m:ref rbt -> k:key ->
{}
m:ref rbt -> k:key ->
{}
unit writes m
{ default !m = default (old !m) and
forall k':key, v':value.
forall k':key, v':value.
mem !m k' v' <-> if k' = k then v' = default !m else mem (old !m) k' v' }
let harness () =
......@@ -53,7 +53,7 @@ let harness () =
()
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_red_black_trees_harness"
End:
End:
*)
......@@ -3,14 +3,14 @@ name = "Alt-Ergo"
exec = "ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.91"
exec = "alt-ergo-0.92.1"
version_switch = "-version"
version_regexp = ".*Ergo \\([^ \n]*\\)"
version_ok = "0.91"
version_ok = "0.92"
version_ok = "0.92.2"
version_ok = "0.92.1"
version_old = "0.8"
version_ok = "0.92"
version_ok = "0.91"
version_old = "0.9"
version_old = "0.8"
command = "why3-cpulimit %t %m %e %f"
driver = "drivers/alt_ergo.drv"
......@@ -38,11 +38,11 @@ exec = "gappa"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.13.0"
version_old = "0.11.2"
version_old = "0.12.0"
version_old = "0.12.1"
version_old = "0.12.2"
version_old = "0.12.3"
version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/gappa.drv"
......@@ -54,8 +54,8 @@ exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
version_switch = "-version"
version_regexp = "Simplify version \\([^ \n,]+\\)"
version_ok = "1.5.4"
version_ok = "1.5.5"
version_ok = "1.5.4"
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/simplify.drv"
......@@ -67,6 +67,14 @@ version_regexp = "SPASS V \\([^ \n\t]+\\)"
command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
[ATP verit]
name = "veriT"
exec = "verit"
version_switch = "--proof-format-and-exit"
version_regexp = "verit \\([^ \n\r]+\\) -"
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/verit.drv"
[ATP z3]
name = "Z3"
exec = "z3"
......@@ -84,11 +92,11 @@ name = "Coq"
exec = "coqc"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.0"
version_ok = "8.1"
version_ok = "8.2"
version_ok = "8.2pl2"
version_ok = "8.2pl1"
version_old = "7.4"
version_ok = "8.2"
version_old = "8.1"
version_old = "8.0"
command = "%e %f"
driver = "drivers/coq.drv"
editor = "coqide"
......
This diff is collapsed.
......@@ -101,8 +101,10 @@ val transformations : goal -> transf Htransf.t
(*
val parent_goal : transf -> goal
*)
(*
val transf_id : transf -> transf_id
val subgoals : transf -> goal list
*)
val subgoals : transf -> goal Why.Util.Mstr.t
(** theory accessors *)
val theory_name : theory -> string
......@@ -115,7 +117,7 @@ val verified : theory -> bool
(*
val file_name : file -> string
*)
val theories : file -> theory list
val theories : file -> theory Why.Util.Mstr.t
(** {2 The persistent database} *)
......
......@@ -115,6 +115,21 @@ let () =
raise e
let read_file fn =
let theories = Env.read_file gconfig.env fn in
let theories =
Theory.Mnm.fold
(fun name th acc ->
match th.Theory.th_name.Ident.id_origin with
| Ident.User l -> (Loc.extract l,name,th)::acc
| _ -> assert false)
theories []
in
let theories = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
theories
in theories
(****************)
(* goals widget *)
......@@ -434,7 +449,7 @@ module Helpers = struct
goal_row = row;
goal_db = db_goal;
external_proofs = Hashtbl.create 7;
transformations = [];
transformations = [];
proved = false;
}
in
......@@ -563,20 +578,19 @@ module Helpers = struct
let add_file f =
try
let theories = Env.read_file gconfig.env f in
let dbfile = Db.add_file f in
let mfile = add_file_row f dbfile in
let theories =
Theory.Mnm.fold
(fun thname t acc ->
let theories = read_file f in
let mths =
List.fold_left
(fun acc (_,thname,t) ->
eprintf "Adding theory '%s'@." thname;
let mth = add_theory mfile t in
mth :: acc
)
theories
[]
[] theories
in
mfile.theories <- List.rev theories;
mfile.theories <- List.rev mths;
if theories = [] then set_file_verified mfile
with e ->
fprintf str_formatter
......@@ -591,85 +605,130 @@ end
(* read previous data from db *)
(*********************************)
let rec reimport_root_task mth tname goals t : bool =
(* re-imports DB informations of a task in theory mth (named tname)
goals is a table of DB goals known to be a possible match for t.
returns true whenever the task t is known to be proved *)
let gname =
(Task.task_goal t).Decl.pr_name.Ident.id_string
in
let sum = task_checksum t in
let db_goal,goal_obsolete =
try
let dbg = Util.Mstr.find gname goals in
let db_sum = Db.task_checksum dbg in
let goal_obsolete = sum <> db_sum in
if goal_obsolete then
begin
eprintf "Goal %s.%s has changed@." tname gname;
Db.change_checksum dbg sum
end;
dbg,goal_obsolete
with Not_found ->
let dbg = Db.add_goal mth.Model.theory_db gname sum in
dbg,false
in
let goal = Helpers.add_goal_row mth gname t db_goal in
let proved = ref false in
let external_proofs = Db.external_proofs db_goal in
Db.Hprover.iter
(fun pid a ->
let p =
Util.Mstr.find (Db.prover_name pid) gconfig.provers
in
let s,t,o = Db.status_and_time a in
if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Scheduler.HighFailure
| Db.Success ->
if not obsolete then proved := true;
Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Timeout -> Scheduler.Timeout
| Db.Failure -> Scheduler.HighFailure
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete goal p a s t
in
((* something TODO ?*))
)
external_proofs;
(*
let transformations = Db.transformations db_goal in
Db.Htransf.iter
(fun tr_id tr ->
let tr = Db.trans_name tr_id in
assert (tr = "split_goal"); (* TODO *)
let s,t,o = Db.status_and_time a in
if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Scheduler.HighFailure
| Db.Success ->
if not obsolete then proved := true;
Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Timeout -> Scheduler.Timeout
| Db.Failure -> Scheduler.HighFailure
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete goal p a s t
in
((* something TODO ?*))
)
transformations;
*)
if !proved then Helpers.set_proved ~propagate:false goal;
!proved
let () =
let files = Db.files () in
List.iter
(fun (f,fn) ->
eprintf "Reimporting file '%s'@." fn;
let theories = Env.read_file gconfig.env fn in
let mfile = Helpers.add_file_row fn f in
let theories = Env.read_file gconfig.env fn in
let theories =
Theory.Mnm.fold
(fun name th acc ->
match th.Theory.th_name.Ident.id_origin with
| Ident.User l -> (Loc.extract l,name,th)::acc
| _ -> assert false)
theories []
in
let theories = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
theories
in
let ths = Db.theories f in
let file_proved = ref true in
List.iter
(fun db_th ->
let tname = Db.theory_name db_th in
(fun (_,tname,th) ->
eprintf "Reimporting theory '%s'@."tname;
let th = Theory.Mnm.find tname theories in
(* TODO: capturer Not_found, cad detecter si la theorie a ete supprmee du fichier *)
(* on pourrait retrouver l'ordre des theories dans le fichier source
en comparant les locations des idents de ces theories *)
let db_th =
try
Util.Mstr.find tname ths
with Not_found ->
assert false (* TODO *)
(* la theorie n'existe pas encore dans la db *)
in
let mth = Helpers.add_theory_row mfile th db_th in
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
let theory_proved = ref true in
List.iter
(fun t ->
let gname =
(Task.task_goal t).Decl.pr_name.Ident.id_string
in
let sum = task_checksum t in
let db_goal,goal_obsolete =
try
let dbg = Util.Mstr.find gname goals in
let db_sum = Db.task_checksum dbg in
let goal_obsolete = sum <> db_sum in
if goal_obsolete then
begin
eprintf "Goal %s.%s has changed@." tname gname;
Db.change_checksum dbg sum
end;
dbg,goal_obsolete
with Not_found ->
let dbg = Db.add_goal db_th gname sum in
dbg,false
in
let goal = Helpers.add_goal_row mth gname t db_goal in
let external_proofs = Db.external_proofs db_goal in
let proved = ref false in
Db.Hprover.iter
(fun pid a ->
let p =
Util.Mstr.find (Db.prover_name pid) gconfig.provers
in
let s,t,o = Db.status_and_time a in
if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Scheduler.HighFailure
| Db.Success ->
if not obsolete then proved := true;
Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Timeout -> Scheduler.Timeout
| Db.Failure -> Scheduler.HighFailure
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete goal p a s t
in
((* TODO ?*))
)
external_proofs;
if !proved then Helpers.set_proved ~propagate:false goal
else theory_proved := false;
)
(fun t -> theory_proved := reimport_root_task mth tname goals t && !theory_proved)
tasks;
(* TODO: what to do with remaining goals in Db ??? *)
(* TODO: what to do with remaining tasks in Db ???
for the moment they remain in the db, but they are not shown
*)
if !theory_proved then Helpers.set_theory_proved ~propagate:false mth
else file_proved := false
)
ths;
(* TODO: detecter d'eventuelles nouvelles theories, qui seraient donc
dans [theories] mais pas dans [ths]
theories;
(* TODO: detecter d'eventuelles vieilles theories, qui seraient donc
dans [ths] mais pas dans [theories]
*)
if !file_proved then Helpers.set_file_verified mfile
)
......
......@@ -51,6 +51,7 @@ let report_line fmt l = fprintf fmt "%s:%d:" l.pos_fname l.pos_lnum
type position = Lexing.position * Lexing.position
exception Located of position * exn
let set_file file lb =
......@@ -74,6 +75,13 @@ let extract (b,e) =
let lc = e.pos_cnum - b.pos_bol in
(f,l,fc,lc)
let compare (_,l1,b1,e1) (_,l2,b2,e2) =
let c = Pervasives.compare l1 l2 in
if c <> 0 then c else
let c = Pervasives.compare b1 b2 in
if c <> 0 then c else
Pervasives.compare e1 e2
let gen_report_position fmt loc =
gen_report_line fmt (extract loc)
......
......@@ -38,6 +38,8 @@ val dummy_position : position
type floc = string * int * int * int
val compare : floc -> floc -> int
val dummy_floc : floc
val extract : position -> floc
......
......@@ -43,6 +43,24 @@ theory TestDiv
end
theory TestList
use import int.Int
use import list.List
logic x : list int
(*
goal Test1:
match x with
| Nil -> 1 = 0 /\ 2 = 3
| Cons _ Nil -> 4 = 5 and 6 = 7
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
*)
end
theory TestReal
......@@ -67,20 +85,3 @@ end
theory TestList
use import int.Int
use import list.List
logic x : list int
(*
goal Test1:
match x with
| Nil -> 1 = 0 /\ 2 = 3
| Cons _ Nil -> 4 = 5 and 6 = 7
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
*)
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