whytac.ml 31.4 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

20 21 22 23 24 25 26 27 28
open Names
open Nameops
open Term
open Termops
open Tacmach
open Util
open Coqlib
open Hipattern
open Typing
29 30
open Libnames
open Declarations
31
open Pp
32 33 34

open Why
open Call_provers
35
open Whyconf
36 37
open Ty
open Term
38 39 40 41 42

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

43
let config = Whyconf.read_config None
44 45
let main = Whyconf.get_main config
let cprovers = Whyconf.get_provers config
46

47
let timelimit = main.timelimit
48

49
let env = Env.create_env (Lexer.retrieve main.loadpath)
50 51 52 53 54 55 56
    
let provers = Hashtbl.create 17

let get_prover s = 
  try 
    Hashtbl.find provers s 
  with Not_found -> 
57
    let cp = Util.Mstr.find s cprovers in
58 59 60 61
    let drv = Driver.load_driver env cp.driver in
    Hashtbl.add provers s (cp, drv);
    cp, drv

62 63 64 65 66 67 68 69
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
let print_tvm fmt m = 
  Idmap.iter (fun id tv -> Format.fprintf fmt "%s->%a@ " 
		 (string_of_id id) Why.Pretty.print_tv tv) m
let print_bv fmt m = 
  Idmap.iter (fun id vs -> Format.fprintf fmt "%s->%a@ " 
		 (string_of_id id) Why.Pretty.print_vsty vs) m

70 71 72 73 74 75 76 77 78 79 80 81 82
(* 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"]]

83
let constant = gen_constant_in_modules "why" coq_modules
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112

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")
113
let coq_Rinv = lazy (constant "Rinv")
114 115 116 117 118 119
let coq_Rminus = lazy (constant "Rminus")
let coq_Rdiv = lazy (constant "Rdiv")
let coq_powerRZ = lazy (constant "powerRZ")

let coq_iff = lazy (constant "iff")

120 121
let is_constant t c = try t = Lazy.force c with _ -> false

122 123 124 125 126 127
(* not first-order expressions *)
exception NotFO

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

128 129 130 131 132
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

133 134 135 136 137 138 139 140 141 142 143 144
(* 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)

145 146 147 148 149 150 151
let coq_rename_var env (na,t) =
  let avoid = ids_of_named_context (Environ.named_context env) in
  let id = next_name_away na avoid in
  id, Environ.push_named (id, None, t) env

let preid_of_id id = Ident.id_fresh (string_of_id id)

152 153 154 155 156 157 158 159 160 161
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for 
   identifiers n1...nk with the same path as c, if they exist; otherwise
   raises Not_found *)
let rec_names_for c =
  let mp,dp,_ = Names.repr_con c in
  array_map_to_list
    (function 
       | Name id -> 
	   let c' = Names.make_con mp dp (label_of_id id) in
	   ignore (Global.lookup_constant c');
162
	   (* msgnl (Printer.pr_constr (mkConst c')); *)
163 164 165 166
	   c'
       | Anonymous ->
	   raise Not_found)

167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
(* 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
	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

184 185
(* decomposes the first n type lambda abstractions correspondings to
   the list of type variables vars *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
186
let decomp_type_lambdas tvm env vars t =
187 188 189 190 191 192 193 194 195 196 197
  let rec loop tvm env vars t = match vars, kind_of_term t with
    | [], _ -> 
	tvm, env, t
    | tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
	let id, env = coq_rename_var env (n, a) in
	let t = subst1 (mkVar id) t in
	let tvm = Idmap.add id tv tvm in
	loop tvm env vars t
    | _ ->
	assert false (*TODO: eta-expansion*)
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198
  loop tvm env vars t
199

200 201 202 203 204 205 206 207
let decompose_arrows =
  let rec arrows_rec l c = match kind_of_term c with
    | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
    | Cast (c,_,_) -> arrows_rec l c
    | _ -> List.rev l, c
  in
  arrows_rec []

208
let decomp_lambdas _dep _tvm bv env vars t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
209 210 211 212 213 214 215 216 217 218 219 220
  let rec loop bv vsl env vars t = match vars, kind_of_term t with
    | [], _ -> 
	(bv, List.rev vsl), env, t
    | ty :: vars, Lambda (n, a, t) ->
	let id, env = coq_rename_var env (n, a) in
	let t = subst1 (mkVar id) t in
	let vs = create_vsymbol (preid_of_id id) ty in
	let bv = Idmap.add id vs bv in
	loop bv (vs :: vsl) env vars t
    | _ ->
	assert false (*TODO: eta-expansion*)
  in
221
  loop bv [] env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
222 223 224



225 226 227 228 229
let rec skip_k_args k cl = match k, cl with
  | 0, _ -> cl
  | _, _ :: cl -> skip_k_args (k-1) cl
  | _, [] -> raise NotFO

230 231
(* Coq globals *)

232
(* Coq reference -> symbol *)
233
let global_ts = ref Refmap.empty 
234 235
let global_ls = ref Refmap.empty

236 237 238 239 240
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
let add_poly_arith ls n = poly_arity := Mls.add ls n !poly_arity
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity

241 242
(* ident -> decl *)
let global_decl = ref Ident.Mid.empty
243

244 245 246 247 248 249 250 251
(* dependencies: decl -> decl list *)
let global_dep = ref Decl.Mdecl.empty

let local_decl = ref Decl.Sdecl.empty

let rec add_local_decls d =
  if not (Decl.Sdecl.mem d !local_decl) then begin
    local_decl := Decl.Sdecl.add d !local_decl;
252
    assert (Decl.Mdecl.mem d !global_dep);
253 254
    let dep = Decl.Mdecl.find d !global_dep in
    Decl.Sdecl.iter add_local_decls dep;
255 256 257 258
    try
      task := Task.add_decl !task d
    with Decl.UnknownIdent id ->
      Format.eprintf "unknown ident %s@." id.Ident.id_string; exit 42
259 260 261 262
  end

let empty_dep () = ref Decl.Sdecl.empty
let add_dep r v = r := Decl.Sdecl.add v !r
263

264 265 266 267 268 269 270
let print_dep fmt =
  let print1 d dl = 
    Format.fprintf fmt "@[%a -> @[%a@]@]@\n" Pretty.print_decl d
      (Pp.print_list Pp.newline Pretty.print_decl) (Decl.Sdecl.elements dl)
  in
  Decl.Mdecl.iter print1 !global_dep

271 272 273 274
(* synchronization *)
let () =
  Summary.declare_summary "Why globals"
    { Summary.freeze_function = 
275 276
	(fun () -> 
	   !global_ts, !global_ls, !poly_arity, !global_decl, !global_dep);
277
      Summary.unfreeze_function = 
278 279 280
	(fun (ts,ls,pa,gdecl,gdep) -> 
	   global_ts := ts; global_ls := ls; poly_arity := pa;
	   global_decl := gdecl; global_dep := gdep);
281
      Summary.init_function = 
282 283 284 285 286 287
	(fun () -> 
	   global_ts := Refmap.empty;
	   global_ls := Refmap.empty;
	   poly_arity := Mls.empty;
	   global_decl := Ident.Mid.empty;
	   global_dep := Decl.Mdecl.empty);
288 289 290
      Summary.survive_module = true;
      Summary.survive_section = true;
    }
291

292
let lookup_table table r = match Refmap.find r !table with
293 294 295
  | None -> raise NotFO
  | Some d -> d

296
let add_table table r v = table := Refmap.add r v !table
297

298 299 300 301 302 303 304 305 306
(* 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
307
  | Construct _ when is_constant p coq_xH ->
308
      Big_int.unit_big_int
309
  | App (f, [|a|]) when is_constant f coq_xI ->
310
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
311
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
312
  | App (f, [|a|]) when is_constant f coq_xO ->
313
      (* Mult (Cst 2, tr_positive a) *)
314 315 316 317 318 319 320 321 322 323
      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
324
  | Construct _ when is_constant t coq_Z0 ->
325
      Term.t_int_const "0"
326
  | App (f, [|a|]) when is_constant f coq_Zpos ->
327
      const_of_big_int (tr_positive a)
328
  | App (f, [|a|]) when is_constant f coq_Zneg ->
329
      const_of_big_int (Big_int.minus_big_int (tr_positive a))
330
  | Const _ when is_constant t coq_R0 ->
331
      Term.t_real_const (Term.RConstDecimal ("0", "0", None))
332
  | Const _ when is_constant t coq_R1 ->
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
      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

355
let rec tr_type dep tvm env t =
356
  let t = Reductionops.nf_betadeltaiota env Evd.empty t in
357
  if is_constant t coq_Z then
358
    Ty.ty_int
359
  else if is_constant t coq_R then
360 361
    Ty.ty_real
  else match kind_of_term t with
362 363
    | Var x when Idmap.mem x tvm ->
	Ty.ty_var (Idmap.find x tvm)
364
    | _ ->
365 366 367
	let f, cl = decompose_app t in
	begin try
	  let r = global_of_constr f in
368
	  let ts = tr_task_ts dep env r in
369
	  assert (List.length ts.Ty.ts_args = List.length cl); (* since t:Set *)
370
	  Ty.ty_app ts (List.map (tr_type dep tvm env) cl)
371 372
	with
	  | Not_found ->
373
	      raise NotFO
374 375 376 377 378
	  | NotFO ->
	      (* TODO: we need to abstract some part of (f cl) *)
	      raise NotFO
	end

379 380
(* the type symbol for r *)
and tr_task_ts dep env r = 
381
  let ts = tr_global_ts dep env r in
382 383 384 385
  if Ident.Mid.mem ts.ts_name !global_decl then begin
    let d = Ident.Mid.find ts.ts_name !global_decl in
    add_local_decls d
  end;
386
  ts
387 388 389 390

(* the type declaration for r *)
and tr_global_ts dep env r =   
  try
391 392 393 394 395
    let ts = lookup_table global_ts r in
    begin try
      let d = Ident.Mid.find ts.ts_name !global_decl in add_dep dep d
    with Not_found -> () end;
    ts
396 397
  with Not_found ->
    add_table global_ts r None;
398
    let dep' = empty_dep () in
399
    match r with
400
      | VarRef _id ->
401 402 403 404 405
	  assert false (*TODO*)
      | ConstructRef _ ->
	  assert false
      | ConstRef c -> 
	  let ty = Global.type_of_global r in
406
	  let (_,vars), _, t = decomp_type_quantifiers env ty in
407 408 409 410 411
	  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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
		let tvm, env, t = decomp_type_lambdas Idmap.empty env vars b in
413
		let def = Some (tr_type dep' tvm env t) in
414
		Ty.create_tysymbol id vars def
415
		  (* FIXME: is it correct to use None when NotFO? *)
416
	    | None -> 
417
		Ty.create_tysymbol id vars None
418
	  in
419
	  let decl = Decl.create_ty_decl [ts, Decl.Tabstract] in
420 421 422 423 424
	  add_dep dep decl;
	  add_table global_ts r (Some ts);
	  global_decl := Ident.Mid.add ts.ts_name decl !global_decl;
	  global_dep := Decl.Mdecl.add decl !dep' !global_dep;
	  ts
425
      | IndRef i ->
426
	  let all_ids = ref [] in
427
	  let mib, _ = Global.lookup_inductive i in
428 429
	  (* first, the inductive types *)
	  let make_one_ts j _ = (* j-th inductive *)
430 431
	    let r = IndRef (ith_mutual_inductive i j) in
	    let ty = Global.type_of_global r in
432
	    let (_,vars), _, t = decomp_type_quantifiers env ty in
433 434
	    if not (is_Set t) && not (is_Type t) then raise NotFO;
	    let id = preid_of_id (Nametab.id_of_global r) in
435
	    let ts = Ty.create_tysymbol id vars None in
436
	    all_ids := ts.ts_name :: !all_ids;
437
	    add_table global_ts r (Some ts)
438 439
	  in
	  Array.iteri make_one_ts mib.mind_packets;
440 441 442
	  (* second, the declarations with constructors *)
	  let make_one j oib = (* j-th inductive *)
	    let j = ith_mutual_inductive i j in
443
	    let ts = lookup_table global_ts (IndRef j) in
444
	    let tyj = Ty.ty_app ts (List.map Ty.ty_var ts.Ty.ts_args) in
MARCHE Claude's avatar
MARCHE Claude committed
445
	    let mk_constructor k _tyk = (* k-th constructor *)
446 447
	      let r = ConstructRef (j, k+1) in
	      let ty = Global.type_of_global r in
448 449 450
	      let (_,vars), env, t = decomp_type_quantifiers env ty in
	      let tvm =
		let add v1 v2 tvm = 
451
		  Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
452 453
		in
		List.fold_right2 add vars ts.Ty.ts_args Idmap.empty
454 455
	      in
	      let l, _ = decompose_arrows t in
456
	      let l = List.map (tr_type dep' tvm env) l in
457
	      let id = preid_of_id (Nametab.id_of_global r) in
458
	      let ls = Term.create_lsymbol id l (Some tyj) in
459 460
	      all_ids := ls.Term.ls_name :: !all_ids;
	      add_table global_ls r (Some ls);
461
	      add_poly_arith ls (List.length vars);
462
	      ls
463 464
	    in
	    let ls = Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc) in
465 466 467 468
	    ts, Decl.Talgebraic ls
	  in
	  let decl = Array.mapi make_one mib.mind_packets in
	  let decl = Array.to_list decl in
469
	  let decl = Decl.create_ty_decl decl in
470 471
	  (* Format.printf "decl = %a@." Pretty.print_decl decl; *)
	  add_dep dep decl;
472
	  List.iter 
473 474 475 476 477
	    (fun id -> 
	       global_decl := Ident.Mid.add id decl !global_decl)
	    !all_ids;
	  global_dep := Decl.Mdecl.add decl !dep' !global_dep;
	  lookup_table global_ts r
478

479
(* the function/predicate symbol for r *)
480
and tr_task_ls dep env r = 
481
  let ls = tr_global_ls dep env r in
482 483 484 485
  if Ident.Mid.mem ls.ls_name !global_decl then begin
    let d = Ident.Mid.find ls.ls_name !global_decl in
    add_local_decls d
  end;
486
  ls
487

488
(* the function/predicate symbol declaration for r *)
489
and tr_global_ls dep env r =
490
  try
491 492 493 494 495
    let ls = lookup_table global_ls r in
    begin try
      let d = Ident.Mid.find ls.ls_name !global_decl in add_dep dep d
    with Not_found -> () end;
    ls
496 497
  with Not_found ->
    add_table global_ls r None;
498 499
    let dep' = empty_dep () in
    let ty = Global.type_of_global r in
500
    let (tvm, _), env, t = decomp_type_quantifiers env ty in
501
    if is_Set t || is_Type t then raise NotFO;
502
    let _, t = decompose_arrows t in
503 504 505 506 507 508 509 510
    match r with
      | ConstructRef _ ->
	  if is_Prop t then raise NotFO; (*TODO? *)
	  let s = type_of env Evd.empty t in
	  if not (is_Set s || is_Type s) then raise NotFO;
	  ignore (tr_type dep' tvm env t);
	  lookup_table global_ls r
      | ConstRef c ->
511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587
	  let ld = decompose_definition dep' env c in
(* 	  let ld = match defl with *)
(* 	    | [] -> *)
(* 		[make_def_decl dep env r None] *)
(* 	    | _ -> *)
(* 		List.map (fun (r, t) -> make_def_decl dep env r (Some t)) defl *)
(* 	  in *)
	  let decl = Decl.create_logic_decl ld in
	  add_dep dep decl;
	  List.iter
	    (fun (ls, _) -> 
	       global_decl := Ident.Mid.add ls.ls_name decl !global_decl)
	    ld;
	  global_dep := Decl.Mdecl.add decl !dep' !global_dep;
	  lookup_table global_ls r
      | VarRef _ | IndRef _ ->
	  raise NotFO

and decompose_definition dep env c = 
  let dl = match (Global.lookup_constant c).const_body with
    | None ->
	[ConstRef c, None]
    | Some b ->
	let b = force b in
	let rec decomp vars t = match kind_of_term t with
	  | Lambda (n, a, t) ->
	      decomp ((n, a) :: vars) t
	  | Fix (_, (names, _, bodies)) ->
	      let lc = rec_names_for c names in
	      let l = List.rev_map mkConst lc in
	      let n = List.length vars in
	      let db_vars = Array.init n (fun i -> mkRel (n - i)) in
	      let l = List.map (fun t -> appvect (t, db_vars)) l in
	      let bodies = Array.to_list bodies in
	      let bodies = List.map (substl l) bodies in
	      let add_lambdas b = 
		List.fold_left (fun t (n,a) -> mkLambda (n,a,t)) b vars 
	      in
	      let bodies = List.map add_lambdas bodies in
	      List.fold_right2 
		(fun c b acc -> (ConstRef c, Some b) :: acc) lc bodies []
	  | _ ->
	      [ConstRef c, Some b]
	in
	decomp [] b
  in
  let make_one_ls r =
    let ty = Global.type_of_global r in
    let (tvm, vars), env, t = decomp_type_quantifiers env ty in
    if is_Set t || is_Type t then raise NotFO;
    let l, t = decompose_arrows t in
    let args = List.map (tr_type dep tvm env) l in
    let ls = 
      let id = preid_of_id (Nametab.id_of_global r) in
      if is_Prop t then 
	(* predicate definition *)
	create_lsymbol id args None
      else
	let s = type_of env Evd.empty t in
	if is_Set s || is_Type s then 
	  (* function definition *)
	  let ty = tr_type dep tvm env t in
	  create_lsymbol id args (Some ty)
	else
	  raise NotFO
    in
    add_table global_ls r (Some ls);
    add_poly_arith ls (List.length vars)
  in
  List.iter (fun (r, _) -> make_one_ls r) dl;
  let make_one_decl (r, b) = 
    let ls = lookup_table global_ls r in
    match b with
      | None ->
	  ls, None
      | Some b ->
	  let ty = Global.type_of_global r in
588 589 590
	  let (tvm, vars), env, ty = decomp_type_quantifiers env ty in
	  let tyl, _ = decompose_arrows ty in
	  let tyl = List.map (tr_type dep tvm env) tyl in
591 592
	  let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
	  let (bv, vsl), env, b = 
593
	    decomp_lambdas dep tvm Idmap.empty env tyl b 
594
	  in
595 596 597 598 599 600 601 602 603 604 605 606
	  begin match ls.ls_value with
	    | None -> 
		let b = tr_formula dep tvm bv env b in
		Decl.make_ps_defn ls vsl b
	    | Some _ ->
		let b = tr_term dep tvm bv env b in
		Decl.make_fs_defn ls vsl b
	  end
  in
  List.map make_one_decl dl

(***
607 608 609 610
	  (* is it defined? *)
	  let ld = match (Global.lookup_constant c).const_body with
	    | Some b ->
		let b = force b in
611 612 613 614 615 616 617 618 619
		let b = match kind_of_term b with
		  (* a single recursive function *)
		  | Fix (_, (_,_,[|b|])) -> 
		      subst1 (mkConst c) b
		  | Fix ((_,_i), (_names,_,_bodies)) ->
		      assert false (*TODO*)
		  | _ -> 
		      b
		in
620
***)
621

622 623
(* translation of a Coq term
   assumption: t:T:Set *)
624
and tr_term dep tvm bv env t =
625 626 627
  try
    tr_arith_constant t
  with NotArithConstant -> match kind_of_term t with
628
    (* binary operations on integers *)
629 630
    | App (c, [|a;b|]) when is_constant c coq_Zplus ->
	let ls = why_constant ["int"] "Int" ["infix +"] in
631
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
632
	  Ty.ty_int
633 634
    | App (c, [|a;b|]) when is_constant c coq_Zminus ->
	let ls = why_constant ["int"] "Int" ["infix -"] in
635
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
636
	  Ty.ty_int
637 638
    | App (c, [|a;b|]) when is_constant c coq_Zmult ->
	let ls = why_constant ["int"] "Int" ["infix *"] in
639
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
640
	  Ty.ty_int
641 642
    | App (c, [|a;b|]) when is_constant c coq_Zdiv ->
	let ls = why_constant ["int"] "EuclideanDivision" ["div"] in
643
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
644
	  Ty.ty_int
645 646
    | App (c, [|a|]) when is_constant c coq_Zopp ->
	let ls = why_constant ["int"] "Int" ["prefix -"] in
647 648
	Term.t_app ls [tr_term dep tvm bv env a] Ty.ty_int
    (* binary operations on reals *)
649 650
    | App (c, [|a;b|]) when is_constant c coq_Rplus ->
	let ls = why_constant ["real"] "Real" ["infix +"] in
651
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
652
	  Ty.ty_real
653 654
    | App (c, [|a;b|]) when is_constant c coq_Rminus ->
	let ls = why_constant ["real"] "Real" ["infix -"] in
655
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
656
	  Ty.ty_real
657 658
    | App (c, [|a;b|]) when is_constant c coq_Rmult ->
	let ls = why_constant ["real"] "Real" ["infix *"] in
659
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
660
	  Ty.ty_real
661 662
    | App (c, [|a;b|]) when is_constant c coq_Rdiv ->
	let ls = why_constant ["real"] "Real" ["infix /"] in
663
	Term.t_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b] 
664
	  Ty.ty_real
665 666
    | App (c, [|a|]) when is_constant c coq_Ropp ->
	let ls = why_constant ["real"] "Real" ["prefix -"] in
667
	Term.t_app ls [tr_term dep tvm bv env a] Ty.ty_real
668 669
    | App (c, [|a|]) when is_constant c coq_Rinv ->
	let ls = why_constant ["real"] "Real" ["inv"] in
670
	Term.t_app ls [tr_term dep tvm bv env a] Ty.ty_real
671
	  (* first-order terms *)
672 673
    | Var id when Idmap.mem id bv ->
	Term.t_var (Idmap.find id bv)
674 675 676
    | Var id ->
	Format.eprintf "tr_term: unbound variable %s@." (string_of_id id);
	exit 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
677 678 679 680 681 682 683 684 685 686
    | Case (ci, _, e, br) ->
	let ty = type_of env Evd.empty e in
	let ty = tr_type dep tvm env ty in
	let e = tr_term dep tvm bv env e in
	let branch j bj =
	  let tj = type_of env Evd.empty bj in
	  let (_,tvars), _, tj = decomp_type_quantifiers env tj in
	  let tyl, _ = decompose_arrows tj in
	  let tyl = List.map (tr_type dep tvm env) tyl in
	  let tvm, env, bj = decomp_type_lambdas tvm env tvars bj in
687
	  let (bv, vars), env, bj = decomp_lambdas dep tvm bv env tyl bj in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
688 689 690 691
	  let cj = ith_constructor_of_inductive ci.ci_ind (j+1) in
	  let ls = tr_global_ls dep env (ConstructRef cj) in
	  if List.length vars <> List.length ls.ls_args then raise NotFO;
	  let pat = pat_app ls (List.map pat_var vars) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
692
	  t_close_branch pat (tr_term dep tvm bv env bj)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
693 694
	in
	let ty = type_of env Evd.empty t in
695
	let _ty = tr_type dep tvm env ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
696
	t_case e (Array.to_list (Array.mapi branch br))
697
    | _ ->
698
	let f, cl = decompose_app t in
699 700 701
	let r = global_of_constr f in
	let ls = tr_task_ls dep env r in
	begin match ls.Term.ls_value with
702 703
	  | Some _ ->
	      let k = get_poly_arity ls in
704
	      let cl = skip_k_args k cl in
705 706
	      let ty = type_of env Evd.empty t in
	      let ty = tr_type dep tvm env ty in
707 708 709 710 711
	      Term.t_app ls (List.map (tr_term dep tvm bv env) cl) ty
	  | None  ->
	      raise NotFO
	end
        (* TODO: we could abstract some part of (f cl) when not FO *)
712 713 714 715 716 717
(* 	      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 *)
718
(* 	  	      Fol.App (s, List.map (tr_term dep tvm bv env) args) *)
719 720 721 722 723 724 725 726 727
(* 	  	    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 *)
	  
728
and quantifiers n a b dep tvm bv env =
729 730 731
  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
732
  let t = tr_type dep tvm env a in
733
  let vs = Term.create_vsymbol (preid_of_id id) t in
734 735 736
  let bv = Idmap.add id vs bv in
  vs, t, bv, env, b

737 738
(* translation of a Coq formula
   assumption f:Prop *)
739
and tr_formula dep tvm bv env f =
740 741
  let c, args = decompose_app f in
  match kind_of_term c, args with
742 743
      (*
	| Var id, [] ->
744
	Fatom (Pred (rename_global (VarRef id), []))
745
      *)
746 747 748
    | _, [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
749 750
	  let _ = tr_type dep tvm env t in
	  Term.f_equ (tr_term dep tvm bv env a) (tr_term dep tvm bv env b)
751 752
	else
	  raise NotFO
753
    (* comparisons on integers *)
754 755
    | _, [a;b] when is_constant c coq_Zle ->
	let ls = why_constant ["int"] "Int" ["infix <="] in
756
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
757 758
    | _, [a;b] when is_constant c coq_Zlt ->
	let ls = why_constant ["int"] "Int" ["infix <"] in
759
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
760 761
    | _, [a;b] when is_constant c coq_Zge ->
	let ls = why_constant ["int"] "Int" ["infix >="] in
762
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
763 764
    | _, [a;b] when is_constant c coq_Zgt ->
	let ls = why_constant ["int"] "Int" ["infix >"] in
765 766
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
    (* comparisons on reals *)
767 768
    | _, [a;b] when is_constant c coq_Rle ->
	let ls = why_constant ["real"] "Real" ["infix <="] in
769
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
770 771
    | _, [a;b] when is_constant c coq_Rlt ->
	let ls = why_constant ["real"] "Real" ["infix <"] in
772
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
773 774
    | _, [a;b] when is_constant c coq_Rge ->
	let ls = why_constant ["real"] "Real" ["infix >="] in
775
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
776 777
    | _, [a;b] when is_constant c coq_Rgt ->
	let ls = why_constant ["real"] "Real" ["infix >"] in
778 779
	Term.f_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
    (* propositional logic *)
780 781 782 783 784
    | _, [] when c = build_coq_False () ->
	Term.f_false
    | _, [] when c = build_coq_True () ->
	Term.f_true
    | _, [a] when c = build_coq_not () ->
785
	Term.f_not (tr_formula dep tvm bv env a)
786
    | _, [a;b] when c = build_coq_and () ->
787
	Term.f_and (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
788
    | _, [a;b] when c = build_coq_or () ->
789
	Term.f_or (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
790
    | _, [a;b] when c = Lazy.force coq_iff ->
791
	Term.f_iff (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
792 793
    | Prod (n, a, b), _ ->
	if is_imp_term f && is_Prop (type_of env Evd.empty a) then
794
	  Term.f_implies 
795
	    (tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
796
	else
797
	  let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env in
Andrei Paskevich's avatar
Andrei Paskevich committed
798
	  Term.f_forall_close [vs] [] (tr_formula dep tvm bv env b)
799 800 801
    | _, [_; a] when c = build_coq_ex () ->
	begin match kind_of_term a with
	  | Lambda(n, a, b) ->
802
	      let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env in
Andrei Paskevich's avatar
Andrei Paskevich committed
803
	      Term.f_exists_close [vs] [] (tr_formula dep tvm bv env b)
804 805
	  | _ ->
	      (* unusual case of the shape (ex p) *)
806 807
	      (* TODO: we could eta-expanse *)
	      raise NotFO 
808
	end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
809 810 811 812 813 814 815 816 817 818
    | Case (ci, _, e, br), [] ->
	let ty = type_of env Evd.empty e in
	let ty = tr_type dep tvm env ty in
	let t = tr_term dep tvm bv env e in
	let branch j bj =
	  let tj = type_of env Evd.empty bj in
	  let (_,tvars), _, tj = decomp_type_quantifiers env tj in
	  let tyl, _ = decompose_arrows tj in
	  let tyl = List.map (tr_type dep tvm env) tyl in
	  let tvm, env, bj = decomp_type_lambdas tvm env tvars bj in
819
	  let (bv, vars), env, bj = decomp_lambdas dep tvm bv env tyl bj in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
820 821 822 823
	  let cj = ith_constructor_of_inductive ci.ci_ind (j+1) in
	  let ls = tr_global_ls dep env (ConstructRef cj) in
	  if List.length vars <> List.length ls.ls_args then raise NotFO;
	  let pat = pat_app ls (List.map pat_var vars) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
824
	  f_close_branch pat (tr_formula dep tvm bv env bj)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
825
	in
826
	f_case t (Array.to_list (Array.mapi branch br))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
827 828
    | Case _, _ :: _ ->
	raise NotFO (* TODO: we could possibly swap case and application *)
829
    | _ ->
830
	let r = global_of_constr c in (*TODO: may fail *)
831 832 833
	let ls = tr_task_ls dep env r in
	begin match ls.Term.ls_value with
	  | None ->
834
	      let k = get_poly_arity ls in
835 836 837 838 839
	      let args = skip_k_args k args in
	      Term.f_app ls (List.map (tr_term dep tvm bv env) args)
	  | Some _ ->
	      raise NotFO
	end
840 841

let tr_goal gl =
842
  local_decl := Decl.Sdecl.empty;
843
  let env = pf_env gl in
844
  let dep = empty_dep () in
845
  let rec tr_ctxt tvm bv = function
846
    | [] ->
847
	tr_formula dep tvm bv env (pf_concl gl) 
848 849
    | (id, None, ty) :: ctxt when is_Set ty || is_Type ty ->
	let v = Ty.create_tvsymbol (preid_of_id id) in
850 851
	let tvm = Idmap.add id v tvm in
	tr_ctxt tvm bv ctxt
852 853 854 855
    | (id, None, ty) :: ctxt ->
	let t = type_of env Evd.empty ty in
	begin try
	  if is_Set t || is_Type t then
856
	    let ty = tr_type dep tvm env ty in (* DO NOT INLINE! *)
857 858
	    let vs = Term.create_vsymbol (preid_of_id id) ty in
	    let bv = Idmap.add id vs bv in
Andrei Paskevich's avatar
Andrei Paskevich committed
859
	    Term.f_forall_close [vs] [] (tr_ctxt tvm bv ctxt)
860
	  else if is_Prop t then 
861 862
	    let h = tr_formula dep tvm bv env ty in (* DO NOT INLINE! *)
	    Term.f_implies h (tr_ctxt tvm bv ctxt)
863 864 865
	  else 
	    raise NotFO
	with NotFO -> 
866
	  tr_ctxt tvm bv ctxt
867 868 869 870 871 872
	end
    | (id, Some d, ty) :: ctxt -> 
	(* local definition -> let or skip *)
	let t = type_of env Evd.empty ty in
	begin try
	  if not (is_Set t || is_Type t) then raise NotFO;
873 874
	  let d = tr_term dep tvm bv env d in
	  let ty = tr_type dep tvm env ty in
875 876
	  let vs = Term.create_vsymbol (preid_of_id id) ty in
	  let bv = Idmap.add id vs bv in
Andrei Paskevich's avatar
Andrei Paskevich committed
877
	  Term.f_let_close vs d (tr_ctxt tvm bv ctxt)
878
	with NotFO -> 
879
	  tr_ctxt tvm bv ctxt
880
	end
881
  in
882 883 884 885 886
  let f = tr_ctxt Idmap.empty Idmap.empty (List.rev (pf_hyps gl)) in
  let pr = Decl.create_prsymbol (Ident.id_fresh "goal") in
  if debug then Format.printf "---@\n%a@\n---@." Pretty.print_fmla f;
  task := Task.add_prop_decl !task Decl.Pgoal pr f

887
let () = Printexc.record_backtrace true
888

889
let whytac s gl =
890
  (* print_dep Format.err_formatter; *)
891 892 893 894 895
  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;
896 897
    let cp, drv = get_prover s in
    let command = cp.command in
898
    if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
899
    if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
900
    let res = Driver.prove_task ~command ~timelimit drv !task () in
901 902 903 904 905 906 907
    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 -> 
908
	  error ("Prover failure\n" ^ res.pr_output ^ "\n")
909 910 911 912 913 914 915
  with 
    | NotFO ->
	error "Not a first order goal"
    | e ->
	Printexc.print_backtrace stderr;
	raise e
	
916 917 918 919


(*
Local Variables:
920
compile-command: "unset LANG; make -C ../.. src/coq-plugin/whytac.cmxs"
921 922
End:
*)