1
(* Authors: Nicolas Ayache and Jean-Christophe Filli�tre *)
2
(* Tactics to call decision procedures *)
6
- first the Coq context and the current goal are translated in
7
Polymorphic First-Order Logic (see fol.mli in this directory)
9
- then the resulting query is passed to the Why tool that translates
10
it to the syntax of the selected prover (Simplify, CVC Lite, haRVey,
33
let set_debug b = debug := b
35
let set_trace b = trace := b
37
let set_timeout n = timeout := n
39
let (dp_timeout_obj,_) =
41
{(default_object "Dp_timeout") with
42
cache_function = (fun (_,x) -> set_timeout x);
43
load_function = (fun _ (_,x) -> set_timeout x);
44
export_function = (fun x -> Some x)}
46
let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
48
let (dp_debug_obj,_) =
50
{(default_object "Dp_debug") with
51
cache_function = (fun (_,x) -> set_debug x);
52
load_function = (fun _ (_,x) -> set_debug x);
53
export_function = (fun x -> Some x)}
55
let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
57
let (dp_trace_obj,_) =
59
{(default_object "Dp_trace") with
60
cache_function = (fun (_,x) -> set_trace x);
61
load_function = (fun _ (_,x) -> set_trace x);
62
export_function = (fun x -> Some x)}
64
let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
66
let logic_dir = ["Coq";"Logic";"Decidable"]
68
init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
69
@ [["Coq"; "ZArith"; "BinInt"]]
70
@ [["Coq"; "omega"; "OmegaLemmas"]]
72
let constant = gen_constant_in_modules "dp" coq_modules
74
let coq_Z = lazy (constant "Z")
75
let coq_Zplus = lazy (constant "Zplus")
76
let coq_Zmult = lazy (constant "Zmult")
77
let coq_Zopp = lazy (constant "Zopp")
78
let coq_Zminus = lazy (constant "Zminus")
79
let coq_Zdiv = lazy (constant "Zdiv")
80
let coq_Zs = lazy (constant "Zs")
81
let coq_Zgt = lazy (constant "Zgt")
82
let coq_Zle = lazy (constant "Zle")
83
let coq_Zge = lazy (constant "Zge")
84
let coq_Zlt = lazy (constant "Zlt")
85
let coq_Z0 = lazy (constant "Z0")
86
let coq_Zpos = lazy (constant "Zpos")
87
let coq_Zneg = lazy (constant "Zneg")
88
let coq_xH = lazy (constant "xH")
89
let coq_xI = lazy (constant "xI")
90
let coq_xO = lazy (constant "xO")
91
let coq_iff = lazy (constant "iff")
93
(* not Prop typed expressions *)
96
(* not first-order expressions *)
99
(* Renaming of Coq globals *)
101
let global_names = Hashtbl.create 97
102
let used_names = Hashtbl.create 97
104
let rename_global r =
106
Hashtbl.find global_names r
109
if Hashtbl.mem used_names id then
112
Hashtbl.add used_names id ();
113
let s = string_of_id id in
114
Hashtbl.add global_names r s;
118
loop (Nametab.id_of_global r)
122
(fun (x,t) p -> Forall (x, t, p))
124
let fresh_var = function
125
| Anonymous -> rename_global (VarRef (id_of_string "x"))
126
| Name x -> rename_global (VarRef x)
128
(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
129
env names, and returns the new variables together with the new
131
let coq_rename_vars env vars =
132
let avoid = ref (ids_of_named_context (Environ.named_context env)) in
134
(fun (na,t) (newvars, newenv) ->
135
let id = next_name_away na !avoid in
136
avoid := id :: !avoid;
137
id :: newvars, Environ.push_named (id, None, t) newenv)
140
(* extract the prenex type quantifications i.e.
141
type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
142
let decomp_type_quantifiers env t =
143
let rec loop vars t = match kind_of_term t with
144
| Prod (n, a, t) when is_Set a || is_Type a ->
145
loop ((n,a) :: vars) t
147
let vars, env = coq_rename_vars env vars in
148
let t = substl (List.map mkVar vars) t in
149
List.rev vars, env, t
153
(* same thing with lambda binders (for axiomatize body) *)
154
let decomp_type_lambdas env t =
155
let rec loop vars t = match kind_of_term t with
156
| Lambda (n, a, t) when is_Set a || is_Type a ->
157
loop ((n,a) :: vars) t
159
let vars, env = coq_rename_vars env vars in
160
let t = substl (List.map mkVar vars) t in
161
List.rev vars, env, t
165
let decompose_arrows =
166
let rec arrows_rec l c = match kind_of_term c with
167
| Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
168
| Cast (c,_,_) -> arrows_rec l c
173
let rec eta_expanse t vars env i =
178
match kind_of_term (Typing.type_of env Evd.empty t) with
179
| Prod (n, a, b) when not (dependent (mkRel 1) b) ->
180
let avoid = ids_of_named_context (Environ.named_context env) in
181
let id = next_name_away n avoid in
182
let env' = Environ.push_named (id, None, a) env in
183
let t' = mkApp (t, [| mkVar id |]) in
184
eta_expanse t' (id :: vars) env' (pred i)
188
let rec skip_k_args k cl = match k, cl with
190
| _, _ :: cl -> skip_k_args (k-1) cl
191
| _, [] -> raise NotFO
193
(* Coq global references *)
195
type global = Gnot_fo | Gfo of Fol.decl
197
let globals = ref Refmap.empty
198
let globals_stack = ref []
200
(* synchronization *)
202
Summary.declare_summary "Dp globals"
203
{ Summary.freeze_function = (fun () -> !globals, !globals_stack);
204
Summary.unfreeze_function =
205
(fun (g,s) -> globals := g; globals_stack := s);
206
Summary.init_function = (fun () -> ());
207
Summary.survive_module = false;
208
Summary.survive_section = false }
210
let add_global r d = globals := Refmap.add r d !globals
211
let mem_global r = Refmap.mem r !globals
212
let lookup_global r = match Refmap.find r !globals with
213
| Gnot_fo -> raise NotFO
216
let locals = Hashtbl.create 97
218
let lookup_local r = match Hashtbl.find locals r with
219
| Gnot_fo -> raise NotFO
222
let iter_all_constructors i f =
223
let _, oib = Global.lookup_inductive i in
225
(fun j tj -> f j (mkConstruct (i, j+1)))
229
(* injection c [t1,...,tn] adds the injection axiom
230
forall x1:t1,...,xn:tn,y1:t1,...,yn:tn.
231
c(x1,...,xn)=c(y1,...,yn) -> x1=y1 /\ ... /\ xn=yn *)
235
let var s = incr i; id_of_string (s ^ string_of_int !i) in
236
let xl = List.map (fun t -> rename_global (VarRef (var "x")), t) l in
238
let yl = List.map (fun t -> rename_global (VarRef (var "y")), t) l in
241
(fun (x,_) (y,_) p -> And (Fatom (Eq (App (x,[]),App (y,[]))), p))
244
let vars = List.map (fun (x,_) -> App(x,[])) in
245
let f = Imp (Fatom (Eq (App (c, vars xl), App (c, vars yl))), f) in
246
let foralls = List.fold_right (fun (x,t) p -> Forall (x, t, p)) in
247
let f = foralls xl (foralls yl f) in
248
let ax = Axiom ("injection_" ^ c, f) in
249
globals_stack := ax :: !globals_stack
251
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
252
identifiers n1...nk with the same path as c, if they exist; otherwise
254
let rec_names_for c =
255
let mp,dp,_ = Names.repr_con c in
259
let c' = Names.make_con mp dp (label_of_id id) in
260
ignore (Global.lookup_constant c');
261
msgnl (Printer.pr_constr (mkConst c'));
266
(* abstraction tables *)
268
let term_abstractions = Hashtbl.create 97
270
let new_abstraction =
271
let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r
273
(* Arithmetic constants *)
275
exception NotArithConstant
277
(* translates a closed Coq term p:positive into a FOL term of type int *)
278
let rec tr_positive p = match kind_of_term p with
279
| Term.Construct _ when p = Lazy.force coq_xH ->
281
| Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
282
Plus (Mult (Cst 2, tr_positive a), Cst 1)
283
| Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
284
Mult (Cst 2, tr_positive a)
285
| Term.Cast (p, _, _) ->
288
raise NotArithConstant
290
(* translates a closed Coq term t:Z into a FOL term of type int *)
291
let rec tr_arith_constant t = match kind_of_term t with
292
| Term.Construct _ when t = Lazy.force coq_Z0 ->
294
| Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
296
| Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
297
Moins (Cst 0, tr_positive a)
298
| Term.Cast (t, _, _) ->
301
raise NotArithConstant
303
(* translate a Coq term t:Set into a FOL type expression;
304
tv = list of type variables *)
305
and tr_type tv env t =
306
let t = Reductionops.nf_betadeltaiota env Evd.empty t in
307
if t = Lazy.force coq_Z then
309
else match kind_of_term t with
310
| Var x when List.mem x tv ->
311
Tvar (string_of_id x)
313
let f, cl = decompose_app t in
315
let r = global_of_constr f in
316
match tr_global env r with
317
| DeclType (id, k) ->
318
assert (k = List.length cl); (* since t:Set *)
319
Tid (id, List.map (tr_type tv env) cl)
326
(* we need to abstract some part of (f cl) *)
331
and make_term_abstraction tv env c =
332
let ty = Typing.type_of env Evd.empty c in
333
let id = new_abstraction () in
334
match tr_decl env id ty with
335
| DeclFun (id,_,_,_) as d ->
337
Hashtbl.find term_abstractions c
339
Hashtbl.add term_abstractions c id;
340
globals_stack := d :: !globals_stack;
346
(* translate a Coq declaration id:ty in a FOL declaration, that is either
347
- a type declaration : DeclType (id, n) where n:int is the type arity
348
- a function declaration : DeclFun (id, tl, t) ; that includes constants
349
- a predicate declaration : DeclPred (id, tl)
350
- an axiom : Axiom (id, p)
352
and tr_decl env id ty =
353
let tv, env, t = decomp_type_quantifiers env ty in
354
if is_Set t || is_Type t then
355
DeclType (id, List.length tv)
356
else if is_Prop t then
357
DeclPred (id, List.length tv, [])
359
let s = Typing.type_of env Evd.empty t in
361
Axiom (id, tr_formula tv [] env t)
363
let l, t = decompose_arrows t in
364
let l = List.map (tr_type tv env) l in
366
DeclPred(id, List.length tv, l)
368
let s = Typing.type_of env Evd.empty t in
369
if is_Set s || is_Type s then
370
DeclFun (id, List.length tv, l, tr_type tv env t)
374
(* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *)
375
and tr_global env r = match r with
383
let ty = Global.type_of_global r in
384
let id = rename_global r in
385
let d = tr_decl env id ty in
386
(* r can be already declared if it is a constructor *)
387
if not (mem_global r) then begin
388
add_global r (Gfo d);
389
globals_stack := d :: !globals_stack
391
begin try axiomatize_body env r id d with NotFO -> () end;
394
add_global r Gnot_fo;
397
and axiomatize_body env r id d = match r with
401
begin match (Global.lookup_constant c).const_body with
406
| DeclPred (id, _, []) ->
407
let tv, env, b = decomp_type_lambdas env b in
408
let value = tr_formula tv [] env b in
409
[id, Iff (Fatom (Pred (id, [])), value)]
410
| DeclFun (id, _, [], _) ->
411
let tv, env, b = decomp_type_lambdas env b in
412
let value = tr_term tv [] env b in
413
[id, Fatom (Eq (Fol.App (id, []), value))]
414
| DeclFun (id, _, l, _) | DeclPred (id, _, l) ->
415
(*Format.eprintf "axiomatize_body %S@." id;*)
416
let b = match kind_of_term b with
417
(* a single recursive function *)
418
| Fix (_, (_,_,[|b|])) ->
420
(* mutually recursive functions *)
421
| Fix ((_,i), (names,_,bodies)) ->
422
(* we only deal with named functions *)
424
let l = rec_names_for c names in
425
substl (List.rev_map mkConst l) bodies.(i)
432
let tv, env, b = decomp_type_lambdas env b in
433
let vars, t = decompose_lam b in
434
let n = List.length l in
435
let k = List.length vars in
437
let vars, env = coq_rename_vars env vars in
438
let t = substl (List.map mkVar vars) t in
439
let t, vars, env = eta_expanse t vars env (n-k) in
440
let vars = List.rev vars in
442
let vars = List.map (fun x -> string_of_id x) vars in
443
let fol_var x = Fol.App (x, []) in
444
let fol_vars = List.map fol_var vars in
445
let vars = List.combine vars l in
447
| DeclFun (_, _, _, ty) ->
448
begin match kind_of_term t with
449
| Case (ci, _, e, br) ->
450
equations_for_case env id vars tv bv ci e br
452
let t = tr_term tv bv env t in
454
add_proof (Fun_def (id, vars, ty, t))
456
let p = Fatom (Eq (App (id, fol_vars), t)) in
460
let value = tr_formula tv bv env t in
461
let p = Iff (Fatom (Pred (id, fol_vars)), value) in
468
| Axiom _ -> assert false)
470
let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in
471
globals_stack := axioms @ !globals_stack
476
iter_all_constructors i
478
let rc = global_of_constr c in
480
begin match tr_global env rc with
481
| DeclFun (_, _, [], _) -> ()
482
| DeclFun (idc, _, al, _) -> injection idc al
489
and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
490
| Var x when List.exists (fun (y, _) -> string_of_id x = y) vars ->
492
iter_all_constructors ci.ci_ind
495
let cjr = global_of_constr cj in
496
begin match tr_global env cjr with
497
| DeclFun (idc, _, l, _) ->
499
let rec_vars, b = decompose_lam b in
500
let rec_vars, env = coq_rename_vars env rec_vars in
501
let coq_rec_vars = List.map mkVar rec_vars in
502
let b = substl coq_rec_vars b in
503
let rec_vars = List.rev rec_vars in
504
let coq_rec_term = applist (cj, List.rev coq_rec_vars) in
505
let b = replace_vars [x, coq_rec_term] b in
506
let bv = bv @ rec_vars in
507
let rec_vars = List.map string_of_id rec_vars in
508
let fol_var x = Fol.App (x, []) in
509
let fol_rec_vars = List.map fol_var rec_vars in
510
let fol_rec_term = App (idc, fol_rec_vars) in
511
let rec_vars = List.combine rec_vars l in
512
let fol_vars = List.map fst vars in
513
let fol_vars = List.map fol_var fol_vars in
514
let fol_vars = List.map (fun y -> match y with
516
if id = string_of_id x
521
let vars = vars @ rec_vars in
522
let rec remove l e = match l with
524
| (y, t)::l' -> if y = string_of_id e then l'
525
else (y, t)::(remove l' e) in
526
let vars = remove vars x in
528
Fatom (Eq (App (id, fol_vars),
529
tr_term tv bv env b))
531
eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs
540
(* assumption: t:T:Set *)
541
and tr_term tv bv env t = match kind_of_term t with
542
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus ->
543
Plus (tr_term tv bv env a, tr_term tv bv env b)
544
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus ->
545
Moins (tr_term tv bv env a, tr_term tv bv env b)
546
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult ->
547
Mult (tr_term tv bv env a, tr_term tv bv env b)
548
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv ->
549
Div (tr_term tv bv env a, tr_term tv bv env b)
550
| Term.Var id when List.mem id bv ->
551
App (string_of_id id, [])
555
with NotArithConstant ->
556
let f, cl = decompose_app t in
558
let r = global_of_constr f in
559
match tr_global env r with
560
| DeclFun (s, k, _, _) ->
561
let cl = skip_k_args k cl in
562
Fol.App (s, List.map (tr_term tv bv env) cl)
568
| NotFO -> (* we need to abstract some part of (f cl) *)
569
let rec abstract app = function
571
Fol.App (make_term_abstraction tv env app, [])
574
let s = make_term_abstraction tv env app in
575
Fol.App (s, List.map (tr_term tv bv env) args)
577
abstract (applist (app, [x])) l
580
let app,l = match cl with
581
| x :: l -> applist (f, [x]), l | [] -> raise NotFO
586
and quantifiers n a b tv bv env =
587
let vars, env = coq_rename_vars env [n,a] in
588
let id = match vars with [x] -> x | _ -> assert false in
589
let b = subst1 (mkVar id) b in
590
let t = tr_type tv env a in
594
(* assumption: f is of type Prop *)
595
and tr_formula tv bv env f =
596
let c, args = decompose_app f in
597
match kind_of_term c, args with
599
Fatom (Pred (rename_global (VarRef id), []))
600
| _, [t;a;b] when c = build_coq_eq () ->
601
let ty = Typing.type_of env Evd.empty t in
602
if is_Set ty || is_Type ty then
603
let _ = tr_type tv env t in
604
Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b))
607
| _, [a;b] when c = Lazy.force coq_Zle ->
608
Fatom (Le (tr_term tv bv env a, tr_term tv bv env b))
609
| _, [a;b] when c = Lazy.force coq_Zlt ->
610
Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b))
611
| _, [a;b] when c = Lazy.force coq_Zge ->
612
Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b))
613
| _, [a;b] when c = Lazy.force coq_Zgt ->
614
Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b))
615
| _, [] when c = build_coq_False () ->
617
| _, [] when c = build_coq_True () ->
619
| _, [a] when c = build_coq_not () ->
620
Not (tr_formula tv bv env a)
621
| _, [a;b] when c = build_coq_and () ->
622
And (tr_formula tv bv env a, tr_formula tv bv env b)
623
| _, [a;b] when c = build_coq_or () ->
624
Or (tr_formula tv bv env a, tr_formula tv bv env b)
625
| _, [a;b] when c = Lazy.force coq_iff ->
626
Iff (tr_formula tv bv env a, tr_formula tv bv env b)
627
| Prod (n, a, b), _ ->
628
if is_imp_term f then
629
Imp (tr_formula tv bv env a, tr_formula tv bv env b)
631
let id, t, bv, env, b = quantifiers n a b tv bv env in
632
Forall (string_of_id id, t, tr_formula tv bv env b)
633
| _, [_; a] when c = build_coq_ex () ->
634
begin match kind_of_term a with
636
let id, t, bv, env, b = quantifiers n a b tv bv env in
637
Exists (string_of_id id, t, tr_formula tv bv env b)
639
(* unusual case of the shape (ex p) *)
640
raise NotFO (* TODO: we could eta-expanse *)
644
let r = global_of_constr c in
645
match tr_global env r with
646
| DeclPred (s, k, _) ->
647
let args = skip_k_args k args in
648
Fatom (Pred (s, List.map (tr_term tv bv env) args))
657
Hashtbl.clear locals;
658
let tr_one_hyp (id, ty) =
660
let s = rename_global (VarRef id) in
661
let d = tr_decl (pf_env gl) s ty in
662
Hashtbl.add locals id (Gfo d);
665
Hashtbl.add locals id Gnot_fo;
670
(fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc)
671
(pf_hyps_types gl) []
673
let c = tr_formula [] [] (pf_env gl) (pf_concl gl) in
674
let hyps = List.rev_append !globals_stack (List.rev hyps) in
678
type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy
680
let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
682
let sprintf = Format.sprintf
684
let file_contents f =
685
let buf = Buffer.create 1024 in
690
let s = input_line c in Buffer.add_string buf s;
691
Buffer.add_char buf '\n'
699
sprintf "(cannot open %s)" f
701
let timeout_sys_command cmd =
702
if !debug then Format.eprintf "command line: %s@." cmd;
703
let out = Filename.temp_file "out" "" in
704
let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
705
let ret = Sys.command cmd in
707
Format.eprintf "Output file %s:@.%s@." out (file_contents out);
710
let timeout_or_failure c cmd out =
715
(sprintf "command %s failed with output:\n%s " cmd (file_contents out))
717
let prelude_files = ref ([] : string list)
719
let set_prelude l = prelude_files := l
721
let (dp_prelude_obj,_) =
723
{(default_object "Dp_prelude") with
724
cache_function = (fun (_,x) -> set_prelude x);
725
load_function = (fun _ (_,x) -> set_prelude x);
726
export_function = (fun x -> Some x)}
728
let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
730
let why_files f = String.concat " " (!prelude_files @ [f])
732
let call_simplify fwhy =
734
sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy)
736
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
737
let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
739
sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out"
742
let out = Sys.command cmd in
744
if out = 0 then Valid None else if out = 1 then Invalid else Timeout
746
if not !debug then remove_files [fwhy; fsx];
750
let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
751
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
752
let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
753
let ftrace = Filename.temp_file "ergo_trace" "" in
756
sprintf "ergo -cctrace %s %s" ftrace fwhy
758
sprintf "ergo %s" fwhy
760
let ret,out = timeout_sys_command cmd in
763
timeout_or_failure ret cmd out
764
else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
765
Valid (if !trace then Some ftrace else None)
766
else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then
768
else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then
771
Failure ("command failed: " ^ cmd)
773
if not !debug then remove_files [fwhy; out];
776
let call_zenon fwhy =
778
sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy)
780
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
781
let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
782
let out = Filename.temp_file "dp_out" "" in
784
sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out
786
let c = Sys.command cmd in
787
if not !debug then remove_files [fwhy; fznn];
791
if c <> 0 then anomaly ("command failed: " ^ cmd);
792
if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then
793
error "Zenon failed";
794
let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in
795
if c = 0 then Valid (Some out) else Invalid
798
let call_yices fwhy =
800
sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
802
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
803
let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
805
sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out"
808
let out = Sys.command cmd in
810
if out = 0 then Valid None else if out = 1 then Invalid else Timeout
812
if not !debug then remove_files [fwhy; fsmt];
817
sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
819
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
820
let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
822
sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out"
825
let out = Sys.command cmd in
827
if out = 0 then Valid None else if out = 1 then Invalid else Timeout
829
if not !debug then remove_files [fwhy; fcvc];
832
let call_harvey fwhy =
834
sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
836
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
837
let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
838
let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in
839
if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed");
840
let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in
841
let outf = Filename.temp_file "rv" ".out" in
843
Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1"
851
sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
853
if Sys.command cmd = 0 then Valid None else Invalid
855
if not !debug then remove_files [fwhy; frv; outf];
859
let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in
860
if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
863
let ergo_proof_from_file f gl =
865
let buf = Buffer.create 1024 in
868
while true do Buffer.add_string buf (input_line c) done; assert false
873
let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in
874
let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in
877
let call_prover prover q =
878
let fwhy = Filename.temp_file "coq_dp" ".why" in
879
Dp_why.output_file fwhy q;
881
| Simplify -> call_simplify fwhy
882
| Ergo -> call_ergo fwhy
883
| Yices -> call_yices fwhy
884
| Zenon -> call_zenon fwhy
885
| CVCLite -> call_cvcl fwhy
886
| Harvey -> call_harvey fwhy
887
| Gwhy -> call_gwhy fwhy
890
Coqlib.check_required_library ["Coq";"ZArith";"ZArith"];
891
let concl_type = pf_type_of gl (pf_concl gl) in
892
if not (is_Prop concl_type) then error "Conclusion is not a Prop";
894
let q = tr_goal gl in
895
begin match call_prover prover q with
896
| Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
897
| Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
898
| Valid _ -> Tactics.admit_as_an_axiom gl
899
| Invalid -> error "Invalid"
900
| DontKnow -> error "Don't know"
901
| Timeout -> error "Timeout"
902
| Failure s -> error s
903
| NoAnswer -> Tacticals.tclIDTAC gl
906
error "Not a first order goal"
909
let simplify = tclTHEN intros (dp Simplify)
910
let ergo = tclTHEN intros (dp Ergo)
911
let yices = tclTHEN intros (dp Yices)
912
let cvc_lite = tclTHEN intros (dp CVCLite)
913
let harvey = dp Harvey
914
let zenon = tclTHEN intros (dp Zenon)
915
let gwhy = tclTHEN intros (dp Gwhy)
918
let env = Global.env () in
919
let one_hint (qid,r) =
920
if not (mem_global r) then begin
921
let ty = Global.type_of_global r in
922
let s = Typing.type_of env Evd.empty ty in
925
let id = rename_global r in
926
let tv, env, ty = decomp_type_quantifiers env ty in
927
let d = Axiom (id, tr_formula tv [] env ty) in
928
add_global r (Gfo d);
929
globals_stack := d :: !globals_stack
931
add_global r Gnot_fo;
934
str " ignored (not a first order proposition)")
936
add_global r Gnot_fo;
938
(pr_reference qid ++ str " ignored (not a proposition)")
942
List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
944
let (dp_hint_obj,_) =
946
{(default_object "Dp_hint") with
947
cache_function = (fun (_,l) -> dp_hint l);
948
load_function = (fun _ (_,l) -> dp_hint l);
949
export_function = (fun x -> Some x)}
951
let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
953
let dp_predefined qid s =
954
let r = Nametab.global qid in
955
let ty = Global.type_of_global r in
956
let env = Global.env () in
957
let id = rename_global r in
959
let d = match tr_decl env id ty with
960
| DeclType (_, n) -> DeclType (s, n)
961
| DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty)
962
| DeclPred (_, n, tyl) -> DeclPred (s, n, tyl)
966
| Axiom _ -> msg_warning (str " ignored (axiom)")
967
| d -> add_global r (Gfo d)
969
msg_warning (str " ignored (not a first order declaration)")
971
let (dp_predefined_obj,_) =
973
{(default_object "Dp_predefined") with
974
cache_function = (fun (_,(id,s)) -> dp_predefined id s);
975
load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
976
export_function = (fun x -> Some x)}
978
let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
980
let _ = declare_summary "Dp options"
982
(fun () -> !debug, !trace, !timeout, !prelude_files);
985
debug := d; trace := tr; timeout := tm; prelude_files := pr);
988
debug := false; trace := false; timeout := 10;
989
prelude_files := []);
990
survive_module = true;
991
survive_section = true }
added
removed
contrib/dp/dp.ml
