whytac.ml 16.8 KB
Newer Older
1

2
3
4
5
6
7
8
9
10
open Names
open Nameops
open Term
open Termops
open Tacmach
open Util
open Coqlib
open Hipattern
open Typing
11
12
open Libnames
open Declarations
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

open Why
open Call_provers

let debug = 
  try let _ = Sys.getenv "WHYDEBUG" in true
  with Not_found -> false

let loadpath = 
  try Str.split (Str.regexp ":") (Sys.getenv "WHYLOADPATH")
  with Not_found -> ["theories"]

let env = Env.create_env (Typing.retrieve loadpath)
    
let timeout = 
  try int_of_string (Sys.getenv "WHYTIMEOUT")
  with Not_found -> 2

let drv =
  let filename = 
    try Sys.getenv "WHYDRIVER" with Not_found -> "drivers/alt_ergo.drv"
  in
  Driver.load_driver filename env

(* Coq constants *)
let logic_dir = ["Coq";"Logic";"Decidable"]

let coq_modules =
  init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
    @ [["Coq"; "ZArith"; "BinInt"];
       ["Coq"; "Reals"; "Rdefinitions"];
       ["Coq"; "Reals"; "Raxioms";];
       ["Coq"; "Reals"; "Rbasic_fun";];
       ["Coq"; "Reals"; "R_sqrt";];
       ["Coq"; "Reals"; "Rfunctions";]]
    @ [["Coq"; "omega"; "OmegaLemmas"]]

50
let constant = gen_constant_in_modules "why" coq_modules
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

let coq_Z = lazy (constant "Z")
let coq_Zplus = lazy (constant "Zplus")
let coq_Zmult = lazy (constant "Zmult")
let coq_Zopp = lazy (constant "Zopp")
let coq_Zminus = lazy (constant "Zminus")
let coq_Zdiv = lazy (constant "Zdiv")
let coq_Zs = lazy (constant "Zs")
let coq_Zgt = lazy (constant "Zgt")
let coq_Zle = lazy (constant "Zle")
let coq_Zge = lazy (constant "Zge")
let coq_Zlt = lazy (constant "Zlt")
let coq_Z0 = lazy (constant "Z0")
let coq_Zpos = lazy (constant "Zpos")
let coq_Zneg = lazy (constant "Zneg")
let coq_xH = lazy (constant "xH")
let coq_xI = lazy (constant "xI")
let coq_xO = lazy (constant "xO")

let coq_R = lazy (constant "R")
let coq_R0 = lazy (constant "R0")
let coq_R1 = lazy (constant "R1")
let coq_Rgt = lazy (constant "Rgt")
let coq_Rle = lazy (constant "Rle")
let coq_Rge = lazy (constant "Rge")
let coq_Rlt = lazy (constant "Rlt")
let coq_Rplus = lazy (constant "Rplus")
let coq_Rmult = lazy (constant "Rmult")
let coq_Ropp = lazy (constant "Ropp")
80
let coq_Rinv = lazy (constant "Rinv")
81
82
83
84
85
86
let coq_Rminus = lazy (constant "Rminus")
let coq_Rdiv = lazy (constant "Rdiv")
let coq_powerRZ = lazy (constant "powerRZ")

let coq_iff = lazy (constant "iff")

87
88
let is_constant t c = try t = Lazy.force c with _ -> false

89
90
91
92
93
94
(* not first-order expressions *)
exception NotFO

(* the task under construction *)
let task = ref None 

95
96
97
98
99
let why_constant path t s =
  let th = Env.find_theory env path t in
  task := Task.use_export !task th;
  Theory.ns_find_ls th.Theory.th_export s

100
101
102
103
104
105
106
107
108
109
110
111
(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
   env names, and returns the new variables together with the new
   environment *)
let coq_rename_vars env vars =
  let avoid = ref (ids_of_named_context (Environ.named_context env)) in
  List.fold_right
    (fun (na,t) (newvars, newenv) ->
       let id = next_name_away na !avoid in
       avoid := id :: !avoid;
       id :: newvars, Environ.push_named (id, None, t) newenv)
    vars ([],env)

112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
(* extract the prenex type quantifications i.e.
   type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
let decomp_type_quantifiers env t =
  let rec loop vars t = match kind_of_term t with
    | Prod (n, a, t) when is_Set a || is_Type a -> 
	loop ((n,a) :: vars) t
    | _ -> 
	let vars, env = coq_rename_vars env vars in
	let t = substl (List.map mkVar vars) t in
	List.rev vars, env, t
  in
  loop [] t

let preid_of_id id = Ident.id_fresh (string_of_id id)

(* same thing with lambda binders (for axiomatize body) *)
let decomp_type_lambdas env t =
  let rec loop vars t = match kind_of_term t with
    | Lambda (n, a, t) when is_Set a || is_Type a ->
	loop ((n,a) :: vars) t
    | _ ->
	let vars, env = coq_rename_vars env vars in
	let t = substl (List.map mkVar vars) t in
	let add m id = 
	  let tv = Ty.create_tvsymbol (preid_of_id id) in
	  Idmap.add id tv m, tv 
	in
	Util.map_fold_left add Idmap.empty vars, env, t
  in
  loop [] t

(* Coq globals *)

let global_ts = ref Refmap.empty 
(* let global_ls = ref Refmap.empty  *)

let lookup_global table r = match Refmap.find r !table with
  | None -> raise NotFO
  | Some d -> d

let add_global table r v = table := Refmap.add r v !table

154
155
156
157
158
159
160
161
162
(* Arithmetic constants *)

exception NotArithConstant

(* translates a closed Coq term p:positive into a FOL term of type int *)

let big_two = Big_int.succ_big_int Big_int.unit_big_int

let rec tr_positive p = match kind_of_term p with
163
  | Construct _ when is_constant p coq_xH ->
164
      Big_int.unit_big_int
165
  | App (f, [|a|]) when is_constant f coq_xI ->
166
167
168
169
(*
      Plus (Mult (Cst 2, tr_positive a), Cst 1)
*)
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
170
  | App (f, [|a|]) when is_constant f coq_xO ->
171
172
173
174
175
176
177
178
179
180
181
182
183
(*
      Mult (Cst 2, tr_positive a)
*)
      Big_int.mult_big_int big_two (tr_positive a)
  | Cast (p, _, _) ->
      tr_positive p
  | _ ->
      raise NotArithConstant

let const_of_big_int b = Term.t_int_const (Big_int.string_of_big_int b)
  
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant t = match kind_of_term t with
184
  | Construct _ when is_constant t coq_Z0 ->
185
      Term.t_int_const "0"
186
  | App (f, [|a|]) when is_constant f coq_Zpos ->
187
      const_of_big_int (tr_positive a)
188
  | App (f, [|a|]) when is_constant f coq_Zneg ->
189
      const_of_big_int (Big_int.minus_big_int (tr_positive a))
190
  | Const _ when is_constant t coq_R0 ->
191
      Term.t_real_const (Term.RConstDecimal ("0", "0", None))
192
  | Const _ when is_constant t coq_R1 ->
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
      Term.t_real_const (Term.RConstDecimal ("1", "0", None))
(*   | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(*       let ta = tr_arith_constant a in *)
(*       let tb = tr_arith_constant b in *)
(*       begin match ta,tb with *)
(*         | RCst na, RCst nb -> RCst (Big_int.add_big_int na nb) *)
(*         | _ -> raise NotArithConstant *)
(*       end *)
(*   | App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> *)
(*       let ta = tr_arith_constant a in *)
(*       let tb = tr_arith_constant b in *)
(*       begin match ta,tb with *)
(*         | RCst na, RCst nb -> RCst (Big_int.mult_big_int na nb) *)
(*         | _ -> raise NotArithConstant *)
(*       end *)
(*   | App (f, [|a;b|]) when f = Lazy.force coq_powerRZ -> *)
(*       tr_powerRZ a b *)
  | Cast (t, _, _) ->
      tr_arith_constant t
  | _ ->
      raise NotArithConstant

let rec tr_type tv env t =
  let t = Reductionops.nf_betadeltaiota env Evd.empty t in
217
  if is_constant t coq_Z then
218
    Ty.ty_int
219
  else if is_constant t coq_R then
220
221
222
223
224
    Ty.ty_real
  else match kind_of_term t with
    | Var x when Idmap.mem x tv ->
	Ty.ty_var (Idmap.find x tv)
    | _ ->
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
	let f, cl = decompose_app t in
	begin try
	  let r = global_of_constr f in
	  let ts = tr_global_ts env r in
	  assert (List.length ts.Ty.ts_args = List.length cl); (* since t:Set *)
	  Ty.ty_app ts (List.map (tr_type tv env) cl)
	with
	  | Not_found ->
	      assert false (* raise NotFO ??? *)
	  | NotFO ->
	      (* TODO: we need to abstract some part of (f cl) *)
	      raise NotFO
	end

and tr_global_ts env r = 
  try
    lookup_global global_ts r
  with Not_found -> 
    add_global global_ts r None;
    match r with
      | VarRef id ->
	  assert false (*TODO*)
      | ConstructRef _ ->
	  assert false
      | ConstRef c -> 
	  let ty = Global.type_of_global r in
	  let tv, _, t = decomp_type_quantifiers env ty in
	  if not (is_Set t) && not (is_Type t) then raise NotFO;
	  let id = preid_of_id (Nametab.id_of_global r) in
	  let ts = match (Global.lookup_constant c).const_body with
	    | Some b ->
		let b = force b in
		let (tv, vars), env, t = decomp_type_lambdas env b in
		let def = Some (tr_type tv env t) in
259
		Ty.create_tysymbol id vars def
260
261
262
263
264
265
266
267
268
269
270
		(* FIXME: is it correct to use None when NotFO? *)
	    | None -> 
		let tv = 
		  List.map (fun x -> Ty.create_tvsymbol (preid_of_id x)) tv 
		in
		Ty.create_tysymbol id tv None
	  in
	  add_global global_ts r (Some ts);
	  task := Task.add_ty_decl !task [ts, Decl.Tabstract];
	  ts
      | IndRef i ->
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
	  Format.eprintf "ici@.";
	  let mib, _ = Global.lookup_inductive i in
	  let make_one_ts j _ =
	    let r = IndRef (ith_mutual_inductive i j) in
	    let ty = Global.type_of_global r in
	    let tv, _, t = decomp_type_quantifiers env ty in
	    if not (is_Set t) && not (is_Type t) then raise NotFO;
	    let id = preid_of_id (Nametab.id_of_global r) in
	    let tv = 
	      List.map (fun x -> Ty.create_tvsymbol (preid_of_id x)) tv 
	    in
	    let ts = Ty.create_tysymbol id tv None in
	    add_global global_ts r (Some ts)
	  in
	  Array.iteri make_one_ts mib.mind_packets;
	  let make_one j ib = 
	    let ls = [] in
	    let r = IndRef (ith_mutual_inductive i j) in
	    let ts = lookup_global global_ts r in
	    ts, Decl.Talgebraic ls
	  in
	  let decl = Array.mapi make_one mib.mind_packets in
	  let decl = Array.to_list decl in
	  task := Task.add_ty_decl !task decl;
	  lookup_global global_ts r
296
297
298
299
300
301

(* assumption: t:T:Set *)
and tr_term tv bv env t =
  try
    tr_arith_constant t
  with NotArithConstant -> match kind_of_term t with
302
      (* binary operations on integers *)
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
    | App (c, [|a;b|]) when is_constant c coq_Zplus ->
	let ls = why_constant ["int"] "Int" ["infix +"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
    | App (c, [|a;b|]) when is_constant c coq_Zminus ->
	let ls = why_constant ["int"] "Int" ["infix -"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
    | App (c, [|a;b|]) when is_constant c coq_Zmult ->
	let ls = why_constant ["int"] "Int" ["infix *"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
    | App (c, [|a;b|]) when is_constant c coq_Zdiv ->
	let ls = why_constant ["int"] "EuclideanDivision" ["div"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
    | App (c, [|a|]) when is_constant c coq_Zopp ->
	let ls = why_constant ["int"] "Int" ["prefix -"] in
	Term.t_app ls [tr_term tv bv env a] Ty.ty_int
318
	  (* binary operations on reals *)
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
    | App (c, [|a;b|]) when is_constant c coq_Rplus ->
	let ls = why_constant ["real"] "Real" ["infix +"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
    | App (c, [|a;b|]) when is_constant c coq_Rminus ->
	let ls = why_constant ["real"] "Real" ["infix -"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
    | App (c, [|a;b|]) when is_constant c coq_Rmult ->
	let ls = why_constant ["real"] "Real" ["infix *"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
    | App (c, [|a;b|]) when is_constant c coq_Rdiv ->
	let ls = why_constant ["real"] "Real" ["infix /"] in
	Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
    | App (c, [|a|]) when is_constant c coq_Ropp ->
	let ls = why_constant ["real"] "Real" ["prefix -"] in
	Term.t_app ls [tr_term tv bv env a] Ty.ty_real
    | App (c, [|a|]) when is_constant c coq_Rinv ->
	let ls = why_constant ["real"] "Real" ["inv"] in
	Term.t_app ls [tr_term tv bv env a] Ty.ty_real
337
	  (* first-order terms *)
338
339
340
341
    | Var id when Idmap.mem id bv ->
	Term.t_var (Idmap.find id bv)
    | _ ->
	assert false (*TODO*)
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
	  (* 	let f, cl = decompose_app t in *)
	  (* 	begin try *)
	  (* 	  let r = global_of_constr f in *)
	  (* 	  match tr_global env r with *)
	  (* 	    | DeclFun (s, k, _, _) -> *)
	  (* 		let cl = skip_k_args k cl in *)
	  (* 		Fol.App (s, List.map (tr_term tv bv env) cl) *)
	  (* 	    | _ -> *)
	  (* 		raise NotFO *)
	  (* 	with *)
	  (* 	  | Not_found -> *)
	  (* 	      raise NotFO *)
	  (* 	  | NotFO -> (\* we need to abstract some part of (f cl) *\) *)
	  (* 	      let rec abstract app = function *)
	  (* 		| [] -> *)
	  (* 		    Fol.App (make_term_abstraction tv env app, []) *)
	  (* 		| x :: l as args -> *)
	  (* 		    begin try *)
	  (* 		      let s = make_term_abstraction tv env app in *)
	  (* 		      Fol.App (s, List.map (tr_term tv bv env) args) *)
	  (* 		    with NotFO -> *)
	  (* 		      abstract (applist (app, [x])) l *)
	  (* 		    end *)
	  (* 	      in *)
	  (* 	      let app,l = match cl with *)
	  (* 		| x :: l -> applist (f, [x]), l | [] -> raise NotFO *)
	  (* 	      in *)
	  (* 	      abstract app l *)
	  (* 	end *)
371
372
373
374
375
376

and quantifiers n a b tv bv env =
  let vars, env = coq_rename_vars env [n,a] in
  let id = match vars with [x] -> x | _ -> assert false in
  let b = subst1 (mkVar id) b in
  let t = tr_type tv env a in
377
  let vs = Term.create_vsymbol (preid_of_id id) t in
378
379
380
381
382
383
  let bv = Idmap.add id vs bv in
  vs, t, bv, env, b

and tr_formula tv bv env f =
  let c, args = decompose_app f in
  match kind_of_term c, args with
384
385
      (*
	| Var id, [] ->
386
	Fatom (Pred (rename_global (VarRef id), []))
387
      *)
388
389
390
391
392
393
394
    | _, [t;a;b] when c = build_coq_eq () ->
	let ty = type_of env Evd.empty t in
	if is_Set ty || is_Type ty then
	  let _ = tr_type tv env t in
	  Term.f_equ (tr_term tv bv env a) (tr_term tv bv env b)
	else
	  raise NotFO
395
	    (* comparisons on integers *)
396
397
398
399
400
401
402
403
404
405
406
407
    | _, [a;b] when is_constant c coq_Zle ->
	let ls = why_constant ["int"] "Int" ["infix <="] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
    | _, [a;b] when is_constant c coq_Zlt ->
	let ls = why_constant ["int"] "Int" ["infix <"] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
    | _, [a;b] when is_constant c coq_Zge ->
	let ls = why_constant ["int"] "Int" ["infix >="] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
    | _, [a;b] when is_constant c coq_Zgt ->
	let ls = why_constant ["int"] "Int" ["infix >"] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
408
	  (* comparisons on reals *)
409
410
411
412
413
414
415
416
417
418
419
420
    | _, [a;b] when is_constant c coq_Rle ->
	let ls = why_constant ["real"] "Real" ["infix <="] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
    | _, [a;b] when is_constant c coq_Rlt ->
	let ls = why_constant ["real"] "Real" ["infix <"] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
    | _, [a;b] when is_constant c coq_Rge ->
	let ls = why_constant ["real"] "Real" ["infix >="] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
    | _, [a;b] when is_constant c coq_Rgt ->
	let ls = why_constant ["real"] "Real" ["infix >"] in
	Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
421
	  (* propositional logic *)
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
    | _, [] when c = build_coq_False () ->
	Term.f_false
    | _, [] when c = build_coq_True () ->
	Term.f_true
    | _, [a] when c = build_coq_not () ->
	Term.f_not (tr_formula tv bv env a)
    | _, [a;b] when c = build_coq_and () ->
	Term.f_and (tr_formula tv bv env a) (tr_formula tv bv env b)
    | _, [a;b] when c = build_coq_or () ->
	Term.f_or (tr_formula tv bv env a) (tr_formula tv bv env b)
    | _, [a;b] when c = Lazy.force coq_iff ->
	Term.f_iff (tr_formula tv bv env a) (tr_formula tv bv env b)
    | Prod (n, a, b), _ ->
	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
	  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
	      Term.f_exists [vs] [] (tr_formula tv bv env b)
	  | _ ->
	      (* unusual case of the shape (ex p) *)
	      raise NotFO (* TODO: we could eta-expanse *)
	end
449
450
451
452
453
	  (*
	    | _ ->
	    begin try
	    let r = global_of_constr c in
	    match tr_global env r with
454
	    | DeclPred (s, k, _) ->
455
456
	    let args = skip_k_args k args in
	    Fatom (Pred (s, List.map (tr_term tv bv env) args))
457
	    | _ ->
458
459
460
461
462
	    raise NotFO
	    with Not_found ->
	    raise NotFO
	    end
	  *)
463
464
465
466
467
    | _ -> assert false (*TODO*)

let tr_goal gl =
  let f = tr_formula Idmap.empty Idmap.empty (pf_env gl) (pf_concl gl) in
  let pr = Decl.create_prsymbol (Ident.id_fresh "goal") in
468
  if debug then Format.printf "---@\n%a@\n---@." Pretty.print_fmla f;
469
  task := Task.add_prop_decl !task Decl.Pgoal pr f
470
471

let whytac gl =
472
473
474
475
476
  let concl_type = pf_type_of gl (pf_concl gl) in
  if not (is_Prop concl_type) then error "Conclusion is not a Prop";
  task := Task.use_export None Theory.builtin_theory;
  try
    tr_goal gl;
477
    if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
478
    if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
479
480
481
482
483
484
485
486
487
488
489
490
    let res = Driver.call_prover ~debug ~timeout drv !task in
    match res.pr_answer with
      | Valid -> Tactics.admit_as_an_axiom gl
      | Invalid -> error "Invalid"
      | Unknown s -> error ("Don't know: " ^ s)
      | Failure s -> error ("Failure: " ^ s)
      | Timeout -> error "Timeout"
      | HighFailure -> 
	  error ("Prover failure\n" ^ res.pr_stdout ^ "\n" ^ res.pr_stderr)
  with NotFO ->
    error "Not a first order goal"

491
492
493
494
495

let _ =
  Tacinterp.overwriting_add_tactic "Why" (fun _ -> whytac);
  Egrammar.extend_tactic_grammar "Why" [[Egrammar.TacTerm "why"]]

496
497
498
499
500
501

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. coq-plugin-opt-yes"
End:
*)