Commit 04da3988 authored by MARCHE Claude's avatar MARCHE Claude

menage dans db.ml

parent ef522d6f
......@@ -254,8 +254,8 @@ MNGCMX = $(addsuffix .cmx, $(MNGMODULES))
$(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3
$(MNGCMO) $(MNGCMX): src/why.cmi
#byte: bin/manager.byte
#opt: bin/manager.opt
byte: bin/manager.byte
opt: bin/manager.opt
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3
......@@ -339,7 +339,7 @@ clean::
ifeq (@enable_coq_support@,yes)
#byte: src/coq-plugin/whytac.cmo
opt: src/coq-plugin/whytac.cmxs
#opt: src/coq-plugin/whytac.cmxs
endif
COQTREES = kernel lib interp parsing proofs pretyping tactics library
......
......@@ -33,7 +33,7 @@ let drv =
let filename =
try Sys.getenv "WHYDRIVER" with Not_found -> "drivers/alt_ergo.drv"
in
Driver.load_driver filename env
Driver.load_driver env filename
(* Coq constants *)
let logic_dir = ["Coq";"Logic";"Decidable"]
......@@ -317,7 +317,7 @@ and tr_global_ts env r =
let j = ith_mutual_inductive i j in
let ts = lookup_global global_ts (IndRef j) in
let tyj = Ty.ty_app ts (List.map Ty.ty_var ts.Ty.ts_args) in
let mk_constructor k tyk = (* k-th constructor *)
let mk_constructor k _tyk = (* k-th constructor *)
let r = ConstructRef (j, k+1) in
let ty = Global.type_of_global r in
let vars, env, t = decomp_type_quantifiers env ty in
......@@ -484,12 +484,12 @@ and tr_formula tv bv env f =
if is_imp_term f && is_Prop (type_of env Evd.empty a) then
Term.f_implies (tr_formula tv bv env a) (tr_formula tv bv env b)
else
let vs, t, bv, env, b = quantifiers n a b tv bv env in
let vs, _t, bv, env, b = quantifiers n a b tv bv env in
Term.f_forall [vs] [] (tr_formula tv bv env b)
| _, [_; a] when c = build_coq_ex () ->
begin match kind_of_term a with
| Lambda(n, a, b) ->
let vs, t, bv, env, b = quantifiers n a b tv bv env in
let vs, _t, bv, env, b = quantifiers n a b tv bv env in
Term.f_exists [vs] [] (tr_formula tv bv env b)
| _ ->
(* unusual case of the shape (ex p) *)
......
This diff is collapsed.
......@@ -153,7 +153,8 @@ let add_task (tname : string) (task : Why.Task.task) acc =
| Why.Task.Use _ | Why.Task.Clone _ -> assert false
| Why.Task.Decl d ->
match d.Why.Decl.d_node with
| Why.Decl.Dtype _ | Why.Decl.Dlogic _ | Why.Decl.Dind _ -> assert false
| Why.Decl.Dtype _ | Why.Decl.Dlogic _ | Why.Decl.Dind _
-> assert false
| Why.Decl.Dprop (_kind,name,_f) ->
eprintf "doing task: tname=%s, name=%s@." tname
name.Why.Decl.pr_name.Why.Ident.id_long;
......@@ -185,7 +186,7 @@ let goal_menu g =
let p = List.assoc i menu in
let call =
try
Db.try_prover ~debug:true ~timelimit ~memlimit:0
Db.try_prover ~debug:false ~timelimit ~memlimit:0
~prover:p.prover ~command:p.command ~driver:p.driver g
with Db.AlreadyAttempted ->
printf "Proof already attempted, no need to rerun@.";
......@@ -206,14 +207,18 @@ let main_loop goals =
let _,menu = List.fold_left
(fun (i,acc) g ->
let i = succ i in
printf "%2d: name='%s', proved=%b@." i (Db.goal_name g) (Db.goal_proved g);
printf "%2d: name='%s', proved=%b@." i
(Db.goal_name g) (Db.goal_proved g);
let e = Db.external_proofs g in
List.iter (fun e ->
let p = Db.prover e in
printf " external proof: prover=%s, obsolete=%b, result=%a, time=%f@."
(Db.prover_name p) (Db.proof_obsolete e)
Db.print_status (Db.status e)
(Db.result_time e))
List.iter
(fun e ->
let p = Db.prover e in
printf
" external proof: prover=%s, obsolete=%b\
, result=%a, time=%.2f@."
(Db.prover_name p) (Db.proof_obsolete e)
Db.print_status (Db.status e)
(Db.result_time e))
e;
(i,(i,g)::acc)) (0,[]) goals
......
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