why3tac.ml4 50.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11

12
open Names
13
open Namegen
14 15 16 17 18 19
open Term
open Termops
open Tacmach
open Util
open Coqlib
open Hipattern
20
open Declarations
21
open Pp
22 23 24
open Universes
open Globnames
open Vars
25 26

IFDEF COQ85 THEN
27
open Errors
28 29 30 31
ELSE
open CErrors
open Stdarg
END
32

Guillaume Melquiond's avatar
Guillaume Melquiond committed
33 34 35 36 37 38 39 40 41 42
IFDEF COQ87 THEN

module KVars = Vars
open EConstr
open EConstr.Vars
module Vars = KVars
open Ltac_plugin

END

43 44 45 46 47 48 49 50
let declare_summary name freeze unfreeze init =
  Summary.declare_summary name
    { Summary.freeze_function = (fun _ -> freeze ());
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init; }

let body_of_constant env c =
  if Reductionops.is_transparent env (ConstKey c) then
51 52 53 54
    let cb = Environ.lookup_constant c env in
    match cb.const_body with
    | Def _ -> Declareops.body_of_constant Opaqueproof.empty_opaquetab cb
    | _ -> None
55 56
  else None

57
let type_of = Typing.type_of
58

59 60 61 62 63 64 65 66 67 68
let finite_ind v = v <> Decl_kinds.CoFinite

let pr_str = Pp.str

let pr_spc = Pp.spc

let pr_fnl = Pp.fnl

let force x = x

69 70 71 72 73 74 75 76
let coq_reference t1 t2 =
  let th = lazy (coq_reference t1 t2) in
  fun x -> lazy (Lazy.force th x)

let find_reference t1 t2 =
  let th = lazy (find_reference t1 t2) in
  fun x -> lazy (Lazy.force th x)

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
IFDEF COQ85 THEN

let push_named = Environ.push_named
let betadeltaiota = Closure.betadeltaiota

module RedFlags = Closure.RedFlags

ELSE

let push_named (id, c, t) env =
  Environ.push_named
    (match c with
     | None -> Context.Named.Declaration.LocalAssum (id, t)
     | Some b -> Context.Named.Declaration.LocalDef (id, b, t))
    env

let pf_hyps gl =
  List.map (function
    | Context.Named.Declaration.LocalAssum (id, t) -> (id, None, t)
    | Context.Named.Declaration.LocalDef (id, b, t) -> (id, Some b, t))
    (pf_hyps gl)

let betadeltaiota = CClosure.all

module RedFlags = CClosure.RedFlags

END

105 106
DECLARE PLUGIN "why3tac"

Guillaume Melquiond's avatar
Guillaume Melquiond committed
107 108 109 110 111 112 113 114
IFDEF COQ87 THEN

let global_of_constr evd t = global_of_constr (to_constr evd t)
let type_of_global env c = of_constr (fst (Global.type_of_global_in_context env c))

ELSE

let kind _evd t = kind_of_term t
115
let is_global _evd c t = is_global c t
Guillaume Melquiond's avatar
Guillaume Melquiond committed
116 117 118 119 120 121 122 123 124 125 126 127 128
let is_Prop _evd t = is_Prop t
let is_Set _evd t = is_Set t
let is_Type _evd t = is_Type t
let to_constr _evd t = t
let of_constr t = t
let dependent _evd c t = dependent c t
let global_of_constr _evd t = global_of_constr t
let type_of_global _env c = Global.type_of_global_unsafe c
let is_imp_term _evd t = is_imp_term t
let decompose_app _evd t = decompose_app t

END

129
let is_global evd c t = is_global evd (Lazy.force c) t
130

131
module Why3tac = struct
132

133
open Why3
134
open Call_provers
135
open Whyconf
136 137
open Ty
open Term
138

139
let debug =
140
  try let _ = Sys.getenv "WHY3DEBUG" in true
141 142
  with Not_found -> false

143 144 145 146 147 148
let config =
  try
    Whyconf.read_config None
  with Whyconf.ConfigFailure(file, msg) ->
    error (file ^ ": " ^ msg)

149
let main = Whyconf.get_main config
150

151
let timelimit = timelimit main
152

153
let env = Env.create_env (loadpath main)
154

155 156
let provers = Hashtbl.create 17

157 158 159 160
let get_prover s =
  try
    Hashtbl.find provers s
  with Not_found ->
161 162 163 164 165 166 167 168 169 170 171
    let filter_prover = Whyconf.parse_filter_prover s in
    let cp = try Whyconf.filter_one_prover config filter_prover
      with Whyconf.ProverAmbiguity (wc,fp,provers) ->
        let provers = Mprover.filter (fun _ p -> not p.interactive) provers in
        if Mprover.is_num_elt 1 provers then
          snd (Mprover.choose provers)
        else if Mprover.is_empty provers then
          raise (Whyconf.ProverNotFound (wc,fp))
        else
          raise (Whyconf.ProverAmbiguity (wc,fp,provers))
    in
172
    let drv = Whyconf.load_driver main env cp.driver cp.extra_drivers in
173 174 175
    Hashtbl.add provers s (cp, drv);
    cp, drv

176
(* Coq constants *)
177

178 179 180 181 182 183 184 185 186 187
let coq_ref_BinInt = coq_reference "Why3" ["ZArith"; "BinInt"; "Z"]
let coq_Zplus = coq_ref_BinInt "add"
let coq_Zmult = coq_ref_BinInt "mul"
let coq_Zopp = coq_ref_BinInt "opp"
let coq_Zminus = coq_ref_BinInt "sub"
let coq_Zdiv = coq_ref_BinInt "div"
let coq_Zgt = coq_ref_BinInt "gt"
let coq_Zle = coq_ref_BinInt "le"
let coq_Zge = coq_ref_BinInt "ge"
let coq_Zlt = coq_ref_BinInt "lt"
188
let coq_ref_BinNums = coq_reference "Why3" ["Numbers"; "BinNums"]
189
let coq_Z = coq_ref_BinNums "Z"
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
let coq_Z0 = coq_ref_BinNums "Z0"
let coq_Zpos = coq_ref_BinNums "Zpos"
let coq_Zneg = coq_ref_BinNums "Zneg"
let coq_xH = coq_ref_BinNums "xH"
let coq_xI = coq_ref_BinNums "xI"
let coq_xO = coq_ref_BinNums "xO"

let coq_ref_Rdefinitions = coq_reference "Why3" ["Reals"; "Rdefinitions"]
let coq_R = coq_ref_Rdefinitions "R"
let coq_R0 = coq_ref_Rdefinitions "R0"
let coq_R1 = coq_ref_Rdefinitions "R1"
let coq_Rgt = coq_ref_Rdefinitions "Rgt"
let coq_Rle = coq_ref_Rdefinitions "Rle"
let coq_Rge = coq_ref_Rdefinitions "Rge"
let coq_Rlt = coq_ref_Rdefinitions "Rlt"
let coq_Rplus = coq_ref_Rdefinitions "Rplus"
let coq_Rmult = coq_ref_Rdefinitions "Rmult"
let coq_Ropp = coq_ref_Rdefinitions "Ropp"
let coq_Rinv = coq_ref_Rdefinitions "Rinv"
let coq_Rminus = coq_ref_Rdefinitions "Rminus"
let coq_Rdiv = coq_ref_Rdefinitions "Rdiv"
let coq_powerRZ = coq_reference "Why3" ["Reals"; "Rfunctions"] "powerRZ"
212 213 214 215 216
IFDEF COQ87 THEN
let coq_IZR = coq_ref_Rdefinitions "IZR"
ELSE
let coq_IZR = coq_reference "Why3" ["Reals"; "Raxioms"] "IZR"
END
217 218 219 220 221 222 223 224 225 226

let coq_Logic = coq_reference "Why3" ["Init"; "Logic"]
let coq_False = coq_Logic "False"
let coq_True = coq_Logic "True"
let coq_eq = coq_Logic "eq"
let coq_not = coq_Logic "not"
let coq_and = coq_Logic "and"
let coq_or = coq_Logic "or"
let coq_ex = coq_Logic "ex"
let coq_iff = coq_Logic "iff"
227

228
let coq_WhyType =
229
  find_reference "Why3" ["Why3"; "BuiltIn"] "WhyType"
230

Guillaume Melquiond's avatar
Guillaume Melquiond committed
231 232 233
let rec is_WhyType evd c = match kind evd c with
  | App (f, [|_|]) -> is_global evd coq_WhyType f
  | Cast (c, _, _) -> is_WhyType evd c
234 235
  | _ -> false

Guillaume Melquiond's avatar
Guillaume Melquiond committed
236
let has_WhyType env evd c = is_WhyType evd (snd (type_of env evd c))
237

238 239 240 241 242 243
(* not first-order expressions *)
exception NotFO

(* 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 *)
244
(*
245 246 247 248 249 250 251 252
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)
253
*)
254

Guillaume Melquiond's avatar
Guillaume Melquiond committed
255
let coq_rename_var env evd na t =
256 257
  let avoid = ids_of_named_context (Environ.named_context env) in
  let id = next_name_away na avoid in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
258
  id, push_named (id, None, (to_constr evd t)) env
259 260 261

let preid_of_id id = Ident.id_fresh (string_of_id id)

262
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
263
   identifiers n1...nk with the same path as c, if they exist; otherwise
264
   raises NotFO *)
265 266
let rec_names_for c =
  let mp,dp,_ = Names.repr_con c in
267
  CArray.map_to_list
268 269
    (function
       | Name id ->
270
           let c' = Names.make_con mp dp (label_of_id id) in
271 272
           ignore
             (try Global.lookup_constant c' with Not_found -> raise NotFO);
273
           c'
274
       | Anonymous ->
275
           raise NotFO)
276

277 278
(* extract the prenex type quantifications i.e.
   type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
279
let decomp_type_quantifiers env evd t =
280 281 282 283
  let add m id =
    let tv = Ty.create_tvsymbol (preid_of_id id) in
    Idmap.add id (Some (Ty.ty_var tv)) m, tv
  in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
284 285 286
  let rec loop env tvm vars t = match kind evd t with
    | Prod (n, a, t) when is_Set evd a || is_Type evd a ->
        let n, env = coq_rename_var env evd n a in
287 288 289
        let t = subst1 (mkVar n) t in
        let tvm, tv = add tvm n in
        loop env tvm (tv :: vars) t
Guillaume Melquiond's avatar
Guillaume Melquiond committed
290 291
    | Prod (n, a, t) when is_WhyType evd a ->
        let n, env = coq_rename_var env evd n a in
292 293
        let t = subst1 (mkVar n) t in
        loop env tvm vars t
294
    | _ ->
295
        (tvm, List.rev vars), env, t
296
  in
297
  loop env Idmap.empty [] t
298

299 300
(* decomposes the first n type lambda abstractions correspondings to
   the list of type variables vars *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
301 302 303 304
let decomp_type_lambdas tvm env evd vars t =
  let rec loop tvm env vars t = match vars, kind evd t with
    | vars, Lambda (n, a, t) when is_WhyType evd a ->
        let id, env = coq_rename_var env evd n a in
305 306
        let t = subst1 (mkVar id) t in
        loop tvm env vars t
Guillaume Melquiond's avatar
Guillaume Melquiond committed
307 308
    | tv :: vars, Lambda (n, a, t) when is_Set evd a || is_Type evd a ->
        let id, env = coq_rename_var env evd n a in
309
        let t = subst1 (mkVar id) t in
310
        let tvm = Idmap.add id (Some (Ty.ty_var tv)) tvm in
311
        loop tvm env vars t
312 313
    | [], _ ->
        tvm, env, t
314
    | _ ->
315
        raise NotFO (*TODO: eta-expansion*)
316
  in
317
  loop tvm env vars t
318

Guillaume Melquiond's avatar
Guillaume Melquiond committed
319 320 321
let decompose_arrows evd =
  let rec arrows_rec l c = match kind evd c with
    | Prod (_,t,c) when not (dependent evd (mkRel 1) c) -> arrows_rec (t :: l) c
322 323 324 325 326
    | Cast (c,_,_) -> arrows_rec l c
    | _ -> List.rev l, c
  in
  arrows_rec []

Guillaume Melquiond's avatar
Guillaume Melquiond committed
327 328 329
let is_fo_kind evd ty =
  let _, ty = decompose_arrows evd ty in
  is_Set evd ty || is_Type evd ty
330

Guillaume Melquiond's avatar
Guillaume Melquiond committed
331 332
let decomp_lambdas _dep _tvm bv env evd vars t =
  let rec loop bv vsl env vars t = match vars, kind evd t with
333
    | [], _ ->
334
        (bv, List.rev vsl), env, t
335
    | ty :: vars, Lambda (n, a, t) ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
336
        let id, env = coq_rename_var env evd n a in
337 338
        let t = subst1 (mkVar id) t in
        let vs = create_vsymbol (preid_of_id id) ty in
339
        let bv = Idmap.add id (Some vs) bv in
340
        loop bv (vs :: vsl) env vars t
341
    | _ ->
342
        raise NotFO (*TODO: eta-expansion*)
343
  in
344
  loop bv [] env vars t
345

346
let rec skip_k_args k cl = match k, cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
347 348
  | [], _ -> cl
  | _ :: k, _ :: cl -> skip_k_args k cl
349 350
  | _, [] -> raise NotFO

351 352
(* Coq globals *)

353
(* Coq reference -> symbol *)
354
let global_ts = ref Refmap.empty
355 356
let global_ls = ref Refmap.empty

357 358
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
359
let add_poly_arity ls n = poly_arity := Mls.add ls n !poly_arity
360 361
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity

362 363
(* ident -> decl *)
let global_decl = ref Ident.Mid.empty
364

365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381
type dep = {
  dep_decls   : Decl.Sdecl.t;
  dep_use_int : bool;
  dep_use_eucl: bool;
  dep_use_real: bool;
}

let empty_dep =
  { dep_decls = Decl.Sdecl.empty;
    dep_use_int = false;
    dep_use_eucl = false;
    dep_use_real = false; }

let empty_dep () = ref empty_dep
let add_dep r v = r := { !r with dep_decls = Decl.Sdecl.add v !r.dep_decls }

(* dependencies: decl -> dep *)
382 383
let global_dep = ref Decl.Mdecl.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
384 385 386 387 388 389 390 391
let add_new_decl dep dep' decl =
  add_dep dep decl;
  Ident.Sid.iter
    (fun id ->
       global_decl := Ident.Mid.add id decl !global_decl)
    decl.Decl.d_news;
  global_dep := Decl.Mdecl.add decl dep' !global_dep

392 393 394 395 396 397 398 399 400 401
let print_dep fmt =
  let print1 d { dep_decls = 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

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

402 403 404
let th_int = lazy (Env.read_theory env ["int"] "Int")
let th_eucl = lazy (Env.read_theory env ["int"] "EuclideanDivision")
let th_real = lazy (Env.read_theory env ["real"] "Real")
405 406

let why_constant_int dep s =
407
  task := Task.use_export !task (Lazy.force th_int);
408
  dep := { !dep with dep_use_int = true };
409
  Theory.ns_find_ls (Lazy.force th_int).Theory.th_export s
410 411

let why_constant_eucl dep s =
412
  task := Task.use_export !task (Lazy.force th_eucl);
413
  dep := { !dep with dep_use_eucl = true };
414
  Theory.ns_find_ls (Lazy.force th_eucl).Theory.th_export s
415 416

let why_constant_real dep s =
417
  task := Task.use_export !task (Lazy.force th_real);
418
  dep := { !dep with dep_use_real = true };
419
  Theory.ns_find_ls (Lazy.force th_real).Theory.th_export s
420 421

let rec add_local_decls d =
422 423
  let id = Ident.Sid.choose d.Decl.d_news in
  if not (Ident.Mid.mem id (Task.task_known !task)) then begin
424
    assert (Decl.Mdecl.mem d !global_dep);
425
    let dep = Decl.Mdecl.find d !global_dep in
426
    Decl.Sdecl.iter add_local_decls dep.dep_decls;
427 428 429
    if dep.dep_use_int then task := Task.use_export !task (Lazy.force th_int);
    if dep.dep_use_eucl then task := Task.use_export !task (Lazy.force th_eucl);
    if dep.dep_use_real then task := Task.use_export !task (Lazy.force th_real);
430 431 432
    try
      task := Task.add_decl !task d
    with Decl.UnknownIdent id ->
433 434 435 436
      Format.eprintf "unknown ident %s@." id.Ident.id_string;
      Format.eprintf "  @[%a@]@.@." Pretty.print_decl d;
      Format.eprintf "task=@[%a@]@." Pretty.print_task !task;
      assert false
437 438
  end

439 440
(* synchronization *)
let () =
441 442 443 444 445 446 447 448 449 450 451 452
  declare_summary "Why globals"
    (fun () ->
     !global_ts, !global_ls, !poly_arity, !global_decl, !global_dep)
    (fun (ts,ls,pa,gdecl,gdep) ->
     global_ts := ts; global_ls := ls; poly_arity := pa;
     global_decl := gdecl; global_dep := gdep)
    (fun () ->
     global_ts := Refmap.empty;
     global_ls := Refmap.empty;
     poly_arity := Mls.empty;
     global_decl := Ident.Mid.empty;
     global_dep := Decl.Mdecl.empty)
453

454
let lookup_table table r = match Refmap.find r !table with
455 456 457
  | None -> raise NotFO
  | Some d -> d

458
let add_table table r v = table := Refmap.add r v !table
459

460 461 462 463 464 465 466 467
(* 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

Guillaume Melquiond's avatar
Guillaume Melquiond committed
468 469
let rec tr_positive evd p = match kind evd p with
  | Construct _ when is_global evd coq_xH p ->
470
      Big_int.unit_big_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
471
  | App (f, [|a|]) when is_global evd coq_xI f ->
472
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
473 474
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive evd a))
  | App (f, [|a|]) when is_global evd coq_xO f ->
475
      (* Mult (Cst 2, tr_positive a) *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
476
      Big_int.mult_big_int big_two (tr_positive evd a)
477
  | Cast (p, _, _) ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478
      tr_positive evd p
479 480 481
  | _ ->
      raise NotArithConstant

482
let const_of_big_int is_neg b =
Andrei Paskevich's avatar
Andrei Paskevich committed
483
  Term.t_const
484
    (Number.(ConstInt { ic_negative = is_neg ;
485
         ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
Clément Fumex's avatar
Clément Fumex committed
486
    ty_int
487

488
let const_of_big_int_real is_neg b =
489
  let s = Big_int.string_of_big_int b in
490 491 492 493
  Term.t_const
    (Number.(ConstReal { rc_negative = is_neg ;
                         rc_abs = real_const_dec s "0" None}))
    ty_real
494

495
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
496 497
let rec tr_arith_constant_IZR evd dep t = match kind evd t with
  | Construct _ when is_global evd coq_Z0 t ->
498 499
    Term.t_const (Number.(ConstReal { rc_negative = false ;
      rc_abs = real_const_dec "0" "0" None })) ty_real
500
  | App (f, [|a|]) when is_global evd coq_Zpos f ->
501
    const_of_big_int_real false (tr_positive evd a)
502
  | App (f, [|a|]) when is_global evd coq_Zneg f ->
503
    const_of_big_int_real true (tr_positive evd a)
504 505 506 507 508
  | Cast (t, _, _) ->
    tr_arith_constant_IZR evd dep t
  | _ ->
    raise NotArithConstant

Guillaume Melquiond's avatar
Guillaume Melquiond committed
509 510 511 512 513 514
let rec tr_arith_constant evd dep t = match kind evd t with
  | Construct _ when is_global evd coq_Z0 t -> Term.t_nat_const 0
  | App (f, [|a|]) when is_global evd coq_Zpos f ->
      const_of_big_int false (tr_positive evd a)
  | App (f, [|a|]) when is_global evd coq_Zneg f ->
      const_of_big_int true (tr_positive evd a)
515 516
  | App (f, [|a|]) when is_global evd coq_IZR f ->
      tr_arith_constant_IZR evd dep a
Guillaume Melquiond's avatar
Guillaume Melquiond committed
517
  | Const _ when is_global evd coq_R0 t ->
518 519
      Term.t_const (Number.(ConstReal { rc_negative = false ;
        rc_abs = real_const_dec "0" "0" None }))
Clément Fumex's avatar
Clément Fumex committed
520
        ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
521
  | Const _ when is_global evd coq_R1 t ->
522 523
      Term.t_const (Number.(ConstReal { rc_negative = false ;
        rc_abs = real_const_dec "1" "0" None}))
Clément Fumex's avatar
Clément Fumex committed
524
        ty_real
525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541
(*   | 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, _, _) ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
542
      tr_arith_constant evd dep t
543 544 545
  | _ ->
      raise NotArithConstant

546
let rec tr_type dep tvm env evd t =
547
  let t = Reductionops.clos_norm_flags
548
      (RedFlags.red_add_transparent
549
	 betadeltaiota (Conv_oracle.get_transp_state (Environ.oracle env)))
550
      env evd t in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
551
  if is_global evd coq_Z t then
552
    Ty.ty_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
553
  else if is_global evd coq_R t then
554
    Ty.ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
555
  else match kind evd t with
556
    | Var x when Idmap.mem x tvm ->
557 558 559 560
        begin match Idmap.find x tvm with
          | None -> raise NotFO
          | Some ty -> ty
        end
561
    | _ ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
562
        let f, cl = decompose_app evd t in
563
        begin try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
564
          let r = global_of_constr evd f in
565 566
          let ts = tr_task_ts dep env evd r in
          let cl = List.filter (fun c -> not (has_WhyType env evd c)) cl in
567 568
          assert (List.length ts.Ty.ts_args = List.length cl);
          (* since t:Set *)
569
          Ty.ty_app ts (List.map (tr_type dep tvm env evd) cl)
570 571 572 573 574 575 576
        with
          | Not_found ->
              raise NotFO
          | NotFO ->
              (* TODO: we need to abstract some part of (f cl) *)
              raise NotFO
        end
577

578
(* the type symbol for r *)
579 580
and tr_task_ts dep env evd r =
  let ts = tr_global_ts dep env evd r in
581 582 583 584
  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;
585
  ts
586 587

(* the type declaration for r *)
588
and tr_global_ts dep env evd (r : global_reference) =
589
  try
590 591 592 593 594
    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
595 596
  with Not_found ->
    add_table global_ts r None;
597
    let dep' = empty_dep () in
598
    match r with
599
      | VarRef id ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
600 601 602
          let ty = try type_of_global env r with Not_found -> raise NotFO in
          let (_,vars), _, t = decomp_type_quantifiers env evd ty in
          if not (is_Set evd t) && not (is_Type evd t) then raise NotFO;
603
          let id = preid_of_id id in
Clément Fumex's avatar
Clément Fumex committed
604
          let ts = Ty.create_tysymbol id vars NoDef in
605 606
          let decl = Decl.create_ty_decl ts in
          add_table global_ts r (Some ts);
Andrei Paskevich's avatar
Andrei Paskevich committed
607
          add_new_decl dep !dep' decl;
608
          ts
609
      | ConstructRef _ ->
610
          assert false
611
      | ConstRef c ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
612 613 614
          let ty = type_of_global env r in
          let (_,vars), _, t = decomp_type_quantifiers env evd ty in
          if not (is_Set evd t) && not (is_Type evd t) then raise NotFO;
615
          let id = preid_of_id (Nametab.basename_of_global r) in
616
          let ts = match body_of_constant env c with
617 618
            | Some b ->
                let b = force b in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
619
                let tvm, env, t = decomp_type_lambdas Idmap.empty env evd vars (of_constr b) in
Clément Fumex's avatar
Clément Fumex committed
620
                let def = Alias (tr_type dep' tvm env evd t) in
621 622 623
                Ty.create_tysymbol id vars def
                  (* FIXME: is it correct to use None when NotFO? *)
            | None ->
Clément Fumex's avatar
Clément Fumex committed
624
                Ty.create_tysymbol id vars NoDef
625
          in
626
          let decl = Decl.create_ty_decl ts in
627
          add_table global_ts r (Some ts);
Andrei Paskevich's avatar
Andrei Paskevich committed
628
          add_new_decl dep !dep' decl;
629
          ts
630
      | IndRef i ->
631 632 633 634
          let mib, _ = Global.lookup_inductive i in
          (* first, the inductive types *)
          let make_one_ts j _ = (* j-th inductive *)
            let r = IndRef (ith_mutual_inductive i j) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
635 636 637
            let ty = type_of_global env r in
            let (_,vars), _, t = decomp_type_quantifiers env evd ty in
            if not (is_Set evd t) && not (is_Type evd t) then raise NotFO;
638
            let id = preid_of_id (Nametab.basename_of_global r) in
Clément Fumex's avatar
Clément Fumex committed
639
            let ts = Ty.create_tysymbol id vars NoDef in
640 641 642 643 644 645 646 647
            add_table global_ts r (Some ts)
          in
          Array.iteri make_one_ts mib.mind_packets;
          (* second, the declarations with constructors *)
          let make_one j oib = (* j-th inductive *)
            let j = ith_mutual_inductive i j in
            let ts = lookup_table global_ts (IndRef j) in
            let tyj = Ty.ty_app ts (List.map Ty.ty_var ts.Ty.ts_args) in
648
            let constr = Array.length oib.mind_nf_lc in
649 650
            let mk_constructor k _tyk = (* k-th constructor *)
              let r = ConstructRef (j, k+1) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
651 652 653 654
              let ty = type_of_global env r in
              let (_,vars), env, t = decomp_type_quantifiers env evd ty in
              let l, c = decompose_arrows evd t in
              let tvm = match kind evd c with
655 656
                | App (_, v) ->
                    let v = Array.to_list v in
657
                    let no_whytype c = not (has_WhyType env evd c) in
658
                    let v = List.filter no_whytype v in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
659
                    let add v1 v2 tvm = match kind evd v1 with
660 661 662 663 664 665 666
                      | Var x1 ->
                          if Idmap.mem x1 tvm then raise NotFO;
                          let v2 = Some (Ty.ty_var v2) in
                          Idmap.add x1 v2 tvm
                      | _ -> raise NotFO (* GADT *)
                    in
                    List.fold_right2 add v ts.Ty.ts_args Idmap.empty
667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682
                | Ind _ -> Idmap.empty
                | Prod _ -> Idmap.empty
                (* ensured by Coq typing *)
                | CoFix _ -> assert false
                | Fix _ -> assert false
                | Case (_, _, _, _) -> assert false
                | Construct _ -> assert false
                | Const _ -> assert false
                | LetIn (_, _, _, _) -> assert false
                | Lambda (_, _, _) -> assert false
                | Cast (_, _, _) -> assert false
                | Sort _ -> assert false
                | Evar _ -> assert false
                | Meta _ -> assert false
                | Var _ -> assert false
                | Rel _ -> assert false
683
                | _ (* Proj *) -> assert false
684
              in
685
              let l = List.map (tr_type dep' tvm env evd) l in
686
              let id = preid_of_id (Nametab.basename_of_global r) in
687
              let ls = Term.create_fsymbol ~constr id l tyj in
688
              add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
689
              add_poly_arity ls vars;
690
              ls, List.map (fun _ -> None) ls.ls_args
691
            in
Andrei Paskevich's avatar
Andrei Paskevich committed
692 693 694 695
            let cl =
              try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
              with NotFO -> []
            in
696
            (j, oib), (ts, cl)
Andrei Paskevich's avatar
Andrei Paskevich committed
697 698 699
          in
          let dl = Array.mapi make_one mib.mind_packets in
          let dl = Array.to_list dl in
700 701 702 703 704 705
          let add ((j, oib), (ts, cl as d)) (tl, dl, sl) =
            if cl = [] then begin
              let sl = ref sl in
              for k = 0 to Array.length oib.mind_nf_lc - 1 do
                let r = ConstructRef (j, k+1) in
                try
706
                  make_one_ls dep' env evd r;
707 708 709 710
                  let ls = lookup_table global_ls r in
                  let d = Decl.create_param_decl ls in
                  sl := d :: !sl
                with NotFO ->
711
                  ()
712 713 714 715
              done;
              Decl.create_ty_decl ts :: tl, dl, !sl
            end else
              tl, d :: dl, sl
Andrei Paskevich's avatar
Andrei Paskevich committed
716
          in
717
          let tl, dl, sl = List.fold_right add dl ([], [], []) in
Andrei Paskevich's avatar
Andrei Paskevich committed
718 719
          let decl =
            if dl = [] then None else Some (Decl.create_data_decl dl)
720 721
          in
          (* Format.printf "decl = %a@." Pretty.print_decl decl; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
722 723
          List.iter (add_new_decl dep !dep') tl;
          List.iter (add_dep dep') tl;
724
          Opt.iter (add_new_decl dep !dep') decl;
725 726
          Opt.iter (add_dep dep') decl;
          List.iter (add_new_decl dep !dep') sl;
727
          lookup_table global_ts r
728

729
(* the function/predicate symbol for r *)
730 731
and tr_task_ls dep env evd r =
  let ls = tr_global_ls dep env evd r in
732 733 734 735
  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;
736
  ls
737

738
(* the function/predicate symbol declaration for r *)
739
and tr_global_ls dep env evd r =
740
  try
741 742 743 744 745
    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
746 747
  with Not_found ->
    add_table global_ls r None;
748
    let dep' = empty_dep () in
749
    (* type_of_global may fail on a local, higher-order variable *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
750 751 752 753
    let ty = try type_of_global env r with Not_found -> raise NotFO in
    let (tvm, _), env, t = decomp_type_quantifiers env evd ty in
    if is_Set evd t || is_Type evd t then raise NotFO;
    let _, t = decompose_arrows evd t in
754 755
    match r with
      | ConstructRef _ ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
756
          assert (not (is_Prop evd t)); (* is a proof *)
757
          let evd,s = type_of env evd t in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
758
          if not (is_Set evd s || is_Type evd s) then raise NotFO;
759
          ignore (tr_type dep' tvm env evd t);
760
          lookup_table global_ls r
761
      | ConstRef c ->
762
          let pl, d = decompose_definition dep' env evd c in
Andrei Paskevich's avatar
Andrei Paskevich committed
763
          List.iter (add_new_decl dep !dep') pl;
764
          List.iter (add_dep dep') pl;
765
          Opt.iter (add_new_decl dep !dep') d;
766
          lookup_table global_ls r
767
      | IndRef i ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
768
          assert (is_Prop evd t);
769
          let pl, d = decompose_inductive dep' env evd i in
Andrei Paskevich's avatar
Andrei Paskevich committed
770
          List.iter (add_new_decl dep !dep') pl;
771
          List.iter (add_dep dep') pl;
772
          Opt.iter (add_new_decl dep !dep') d;
773 774
          lookup_table global_ls r
      | VarRef _ ->
775
          make_one_ls dep' env evd r;
776 777
          let ls = lookup_table global_ls r in
          let decl = Decl.create_param_decl ls in
Andrei Paskevich's avatar
Andrei Paskevich committed
778
          add_new_decl dep !dep' decl;
779 780
          ls

781
and make_one_ls dep env evd r =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
782 783 784 785
  let ty = type_of_global env r in
  let (tvm, vars), env, t = decomp_type_quantifiers env evd ty in
  if is_Set evd t || is_Type evd t then raise NotFO;
  let l, t = decompose_arrows evd t in
786
  let args = List.map (tr_type dep tvm env evd) l in
787 788
  let ls =
    let id = preid_of_id (Nametab.basename_of_global r) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
789
    if is_Prop evd t then
790 791 792
        (* predicate definition *)
      create_lsymbol id args None
    else
793
      let evd,s = type_of env evd t in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
794
      if is_Set evd s || is_Type evd s then
795
          (* function definition *)
796
        let ty = tr_type dep tvm env evd t in
797 798 799 800 801
        create_lsymbol id args (Some ty)
      else
        raise NotFO
  in
  add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
802
  add_poly_arity ls vars
803

804
and decompose_definition dep env evd c =
805
  let dl = match body_of_constant env c with
806
    | None ->
807
        [ConstRef c, None]
808
    | Some b ->
809
        let b = force b in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
810
        let rec decomp vars t = match Constr.kind t with
811 812 813 814
          | Lambda (n, a, t) ->
              decomp ((n, a) :: vars) t
          | Fix (_, (names, _, bodies)) ->
              let lc = rec_names_for c names in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
815
              let l = List.rev_map Constr.mkConst lc in
816
              let n = List.length vars in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
817
              let db_vars = Array.init n (fun i -> Constr.mkRel (n - i)) in
818 819
              let l = List.map (fun t -> appvect (t, db_vars)) l in
              let bodies = Array.to_list bodies in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
820
              let bodies = List.map (Vars.substl l) bodies in
821
              let add_lambdas b =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
822
                List.fold_left (fun t (n,a) -> Constr.mkLambda (n,a,t)) b vars
823 824 825 826 827 828 829 830
              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
831
  in
832
  List.iter (fun (r, _) -> make_one_ls dep env evd r) dl;
833
  let make_one_decl (r, b) =
834 835 836
    let ls = lookup_table global_ls r in
    match b with
      | None ->
837
          assert false
838
      | Some b ->
839 840
          let tvs = List.fold_left Ty.ty_freevars Stv.empty
            (Ty.oty_cons ls.ls_args ls.ls_value) in
841 842
          let add tv tvm = Stdlib.Mstr.add tv.tv_name.Ident.id_string tv tvm in
          let tvm = Stv.fold add tvs Stdlib.Mstr.empty in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
843 844
          let ty = type_of_global env r in
          let (_, vars), env, _ = decomp_type_quantifiers env evd ty in
845
          let conv tv = Stdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
846
          let vars = List.map conv vars in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
847
          let tvm, env, b = decomp_type_lambdas Idmap.empty env evd vars (of_constr b) in
848
          let (bv, vsl), env, b =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
849
            decomp_lambdas dep tvm Idmap.empty env evd ls.ls_args b
850 851 852
          in
          begin match ls.ls_value with
            | None ->
853
                let b = tr_formula dep tvm bv env evd b in
854
                Decl.make_ls_defn ls vsl b
855
            | Some _ ->
856
                let b = tr_term dep tvm bv env evd b in
857
                Decl.make_ls_defn ls vsl b
858
          end
859
  in
860
  match dl with
861 862
    | [r, None] ->
        [Decl.create_param_decl (lookup_table global_ls r)], None
863
    | _ ->
864 865 866 867 868 869 870 871
        let add (r, _ as d) (pl, dl) =
          try
            pl, make_one_decl d :: dl
          with NotFO ->
            Decl.create_param_decl (lookup_table global_ls r) :: pl, dl
        in
        let pl, dl = List.fold_right add dl ([], []) in
        pl, if dl = [] then None else Some (Decl.create_logic_decl dl)
872

873
and decompose_inductive dep env evd i =
874 875 876
  let mib, _ = Global.lookup_inductive i in
  (* first, the inductive types *)
  let make_one_ls j _ = (* j-th inductive *)
877
    make_one_ls dep env evd (IndRef (ith_mutual_inductive i j))
878 879 880 881 882 883 884 885
  in
  Array.iteri make_one_ls mib.mind_packets;
  (* second, the inductive predicate declarations *)
  let make_one j oib = (* j-th inductive *)
    let j = ith_mutual_inductive i j in
    let ls = lookup_table global_ls (IndRef j) in
    let mk_constructor k _tyk = (* k-th constructor *)
      let r = ConstructRef (j, k+1) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
886 887
      let ty = type_of_global env r in
      let (_,vars), env, f = decomp_type_quantifiers env evd ty in
888 889
      let tvm =
        let add v1 v2 tvm =
890
          let v2 = Some (Ty.ty_var v2) in
891 892
          Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
893
        List.fold_right2 add vars (get_poly_arity ls) Idmap.empty
894
      in
895
      let f = tr_formula dep tvm Idmap.empty env evd f in
896 897 898 899
      let id = preid_of_id (Nametab.basename_of_global r) in
      let pr = Decl.create_prsymbol id in
      pr, f
    in
900 901 902 903
    let cl =
      try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
      with NotFO -> []
    in
904 905
    ls, cl
  in
906 907 908 909 910 911
  let dl = Array.mapi make_one mib.mind_packets in
  let dl = Array.to_list dl in
  let add (ls, cl as d) (pl, dl) =
    if cl = [] then Decl.create_param_decl ls :: pl, dl else pl, d :: dl
  in
  let pl, dl = List.fold_right add dl ([], []) in
912
  let s = if finite_ind mib.mind_finite then Decl.Ind else Decl.Coind in
913
  pl, if dl = [] then None else Some (Decl.create_ind_decl s dl)
914

915 916
(* translation of a Coq term
   assumption: t:T:Set *)
917
and tr_term dep tvm bv env evd t =
918
  try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
919 920
    tr_arith_constant evd dep t
  with NotArithConstant -> match kind evd t with
921
    (* binary operations on integers *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
922
    | App (c, [|a;b|]) when is_global evd coq_Zplus c ->
923
        let ls = why_constant_int dep ["infix +"] in
924
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
925
          Ty.ty_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
926
    | App (c, [|a;b|]) when is_global evd coq_Zminus c ->
927
        let ls = why_constant_int dep ["infix -"] in
928
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
929
          Ty.ty_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
930
    | App (c, [|a;b|]) when is_global evd coq_Zmult c ->
931
        let ls = why_constant_int dep ["infix *"] in
932
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
933
          Ty.ty_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
934
    | App (c, [|a;b|]) when is_global evd coq_Zdiv c ->
935
        let ls = why_constant_eucl dep ["div"] in
936
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
937
          Ty.ty_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
938
    | App (c, [|a|]) when is_global evd coq_Zopp c ->
939
        let ls = why_constant_int dep ["prefix -"] in
940
        Term.fs_app ls [tr_term dep tvm bv env evd a] Ty.ty_int
941
    (* binary operations on reals *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
942
    | App (c, [|a;b|]) when is_global evd coq_Rplus c ->
943
        let ls = why_constant_real dep ["infix +"] in
944
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
945
          Ty.ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
946
    | App (c, [|a;b|]) when is_global evd coq_Rminus c ->
947
        let ls = why_constant_real dep ["infix -"] in
948
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
949
          Ty.ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
950
    | App (c, [|a;b|]) when is_global evd coq_Rmult c ->
951
        let ls = why_constant_real dep ["infix *"] in
952
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
953
          Ty.ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
954
    | App (c, [|a;b|]) when is_global evd coq_Rdiv c ->
955
        let ls = why_constant_real dep ["infix /"] in
956
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
957
          Ty.ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
958
    | App (c, [|a|]) when is_global evd coq_Ropp c ->
959
        let ls = why_constant_real dep ["prefix -"] in
960
        Term.fs_app ls [tr_term dep tvm bv env evd a] Ty.ty_real
Guillaume Melquiond's avatar
Guillaume Melquiond committed
961
    | App (c, [|a|]) when is_global evd coq_Rinv c ->
962
        let ls = why_constant_real dep ["inv"] in
963
        Term.fs_app ls [tr_term dep tvm bv env evd a] Ty.ty_real
964
          (* first-order terms *)
965
    | Var id when Idmap.mem id bv ->
966 967 968 969 970
        let vs = match Idmap.find id bv with
          | None -> raise NotFO
          | Some vs -> vs
        in
        Term.t_var vs
971
    | Case (ci, _, e, br) ->
972 973 974
        let evd,ty = type_of env evd e in
        let ty = tr_type dep tvm env evd ty in
        let e = tr_term dep tvm bv env evd e in
975
        let branch j bj =
976
          let evd,tj = type_of env evd bj in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
977 978
          let (_,tvars), _, tj = decomp_type_quantifiers env evd tj in
          let tyl, _ = decompose_arrows evd tj in
979
          let tyl = List.map (tr_type dep tvm env evd) tyl in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
980 981
          let tvm, env, bj = decomp_type_lambdas tvm env evd tvars bj in
          let (bv, vars), env, bj = decomp_lambdas dep tvm bv env evd tyl bj in
982
          let cj = ith_constructor_of_inductive ci.ci_ind (j+1) in
983
          let ls = tr_global_ls dep env evd (ConstructRef cj) in
984 985
          if List.length vars <> List.length ls.ls_args then raise NotFO;
          let pat = pat_app ls (List.map pat_var vars) ty in
986
          t_close_branch pat (tr_term dep tvm bv env evd bj)
987
        in
988 989
        let evd,ty = type_of env evd t in
        let _ty = tr_type dep tvm env evd ty in
990
        t_case e (Array.to_list (Array.mapi branch br))
991
    | LetIn (x, e1, ty1, e2) ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
992
        if is_Prop evd ty1 || is_fo_kind evd ty1 then
993
          let e2 = subst1 e1 e2 in
994
          tr_term dep tvm bv env evd e2
995
        else begin
996
          let evd,s1 = type_of env evd ty1 in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
997
          if not (is_Set evd s1 || is_Type evd s1) then raise NotFO;
998 999 1000
          let t1 = tr_term dep tvm bv env evd e1 in
          let vs, _, bv, env, e2 = quantifiers x ty1 e2 dep tvm bv env evd in
          let t2 = tr_term dep tvm bv env evd e2 in
1001 1002 1003 1004 1005 1006 1007
          t_let_close vs t1 t2
        end
    | CoFix _ | Fix _ | Lambda _ | Prod _ | Sort _ | Evar _ | Meta _ ->
        raise NotFO
    | Rel _ ->
        assert false
    | Cast (t, _, _) ->
1008
        tr_term dep tvm bv env evd t
1009
    | Var _ | App _ | Construct _ | Ind _ | Const _ ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1010
        let f, cl = decompose_app evd t in
1011
        (* a local variable cannot be applied (not FO) *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1012
        begin match kind evd f with
1013 1014 1015
          | Var id when Idmap.mem id bv -> raise NotFO
          | _ -> ()
        end;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1016
        let r = try global_of_constr evd f with _ -> raise NotFO in
1017
        let ls = tr_task_ls dep env evd r in
1018 1019
        begin match ls.Term.ls_value with
          | Some _ ->
1020
              let cl = List.filter (fun c -> not (has_WhyType env evd c)) cl in
1021 1022
              let k = get_poly_arity ls in
              let cl = skip_k_args k cl in
1023 1024 1025
              let evd,ty = type_of env evd t in
              let ty = tr_type dep tvm env evd ty in
              Term.fs_app ls (List.map (tr_term dep tvm bv env evd) cl) ty
1026 1027 1028
          | None  ->
              raise NotFO
        end
1029
        (* TODO: we could abstract some part of (f cl) when not FO *)
1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044
(*               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 dep tvm 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 *)
1045 1046
  | _ (* Proj *) ->
      raise NotFO
1047

1048
and quantifiers n a b dep tvm bv env evd =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1049
  let id, env = coq_rename_var env evd n a in
1050
  let b = subst1 (mkVar id) b in
1051
  let t = tr_type dep tvm env evd a in
1052
  let vs = Term.create_vsymbol (preid_of_id id) t in
1053
  let bv = Idmap.add id (Some vs) bv in
1054 1055
  vs, t, bv, env, b

1056 1057
(* translation of a Coq formula
   assumption f:Prop *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1058 1059
and tr_formula dep tvm bv env evd f = match kind evd f with
  | App(c, [|t;a;b|]) when is_global evd coq_eq c ->
1060
      let evd,ty = type_of env evd t in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1061
      if not (is_Set evd ty || is_Type evd ty) then raise NotFO;
1062 1063
      let _ = tr_type dep tvm env evd t in
      Term.t_equ (tr_term dep tvm bv env evd a) (tr_term dep tvm bv env evd b)
1064
  (* comparisons on integers *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1065
  | App(c, [|a;b|]) when is_global evd coq_Zle c ->
1066
      let ls = why_constant_int dep ["infix <="] in
1067
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1068
  | App(c, [|a;b|]) when is_global evd coq_Zlt c ->
1069
      let ls = why_constant_int dep ["infix <"] in
1070
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1071
  | App(c, [|a;b|]) when is_global evd coq_Zge c ->
1072
      let ls = why_constant_int dep ["infix >="] in
1073
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1074
  | App(c, [|a;b|]) when is_global evd coq_Zgt c ->
1075
      let ls = why_constant_int dep ["infix >"] in
1076
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1077
  (* comparisons on reals *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1078
  | App(c, [|a;b|]) when is_global evd coq_Rle c ->
1079
      let ls = why_constant_real dep ["infix <="] in
1080
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1081
  | App(c, [|a;b|]) when is_global evd coq_Rlt c ->
1082
      let ls = why_constant_real dep ["infix <"] in
1083
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1084
  | App(c, [|a;b|]) when is_global evd coq_Rge c ->
1085
      let ls = why_constant_real dep ["infix >="] in
1086
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1087
  | App(c, [|a;b|]) when is_global evd coq_Rgt c ->
1088
      let ls = why_constant_real dep ["infix >"] in
1089
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1090
  (* propositional logic *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1091
  | _ when is_global evd coq_False f ->
1092
      Term.t_false
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1093
  | _ when is_global evd coq_True f ->
1094
      Term.t_true
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1095
  | App(c, [|a|]) when is_global evd coq_not c ->
1096
      Term.t_not (tr_formula dep tvm bv env evd a)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1097
  | App(c, [|a;b|]) when is_global evd coq_and c ->
1098
      Term.t_and (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1099
  | App(c, [|a;b|]) when is_global evd coq_or c ->
1100
      Term.t_or (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1101
  | App(c, [|a;b|]) when is_global evd coq_iff c ->
1102
      Term.t_iff (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
1103
  | Prod (n, a, b) ->
1104
      let evd,ty = type_of env evd a in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1105
      if is_imp_term evd f && is_Prop evd ty then
1106
        Term.t_implies
1107
          (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
1108
      else
1109 1110
        let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env evd in
        Term.t_forall_close [vs] [] (tr_formula dep tvm bv env evd b)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1111 1112
  | App(c, [|_; a|]) when is_global evd coq_ex c ->
      begin match kind evd a with
1113
        | Lambda(n, a, b) ->
1114 1115
            let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env evd in
            Term.t_exists_close [vs] [] (tr_formula dep tvm bv env evd b)
1116
        | _ ->
1117 1118
              (* unusual case of the shape (ex p) *)
              (* TODO: we could eta-expanse *)
1119 1120 1121
          raise NotFO
      end
  | Case (ci, _, e, br) ->
1122 1123 1124
      let evd,ty = type_of env evd e in
      let ty = tr_type dep tvm env evd ty in
      let t = tr_term dep tvm bv env evd e in
1125
      let branch j bj =
1126
        let evd,tj = type_of env evd bj in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1127 1128
        let (_,tvars), _, tj = decomp_type_quantifiers env evd tj in
        let tyl, _ = decompose_arrows evd tj in
1129
        let tyl = List.map (tr_type dep tvm env evd) tyl in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1130 1131
        let tvm, env, bj = decomp_type_lambdas tvm env evd tvars bj in
        let (bv, vars), env, bj = decomp_lambdas dep tvm bv env evd tyl bj in
1132
        let cj = ith_constructor_of_inductive ci.ci_ind (j+1) in
1133
        let ls = tr_global_ls dep env evd (ConstructRef cj) in
1134 1135
        if List.length vars <> List.length ls.ls_args then raise NotFO;
        let pat = pat_app ls (List.map pat_var vars) ty in
1136
        t_close_branch pat (tr_formula dep tvm bv env evd bj)
1137 1138 1139 1140 1141 1142 1143
      in
      t_case t (Array.to_list (Array.mapi branch br))
  | Var _ ->
      raise NotFO (* no propositional variables *)
  | CoFix _ | Fix _ | Lambda _ | Sort _ | Evar _ | Meta _ ->
      raise NotFO
  | LetIn (x, e1, ty1, e2) ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1144
      if is_Prop evd ty1 || is_Set evd ty1 || is_Type evd ty1 then
1145
        let e2 = subst1 e1 e2 in
1146
        tr_formula dep tvm bv env evd e2
1147
      else begin
1148
        let evd,s1 = type_of env evd ty1 in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1149
        if not (is_Set evd s1 || is_Type evd s1) then raise NotFO;
1150 1151 1152
        let t1 = tr_term dep tvm bv env evd e1 in
        let vs, _, bv, env, e2 = quantifiers x ty1 e2 dep tvm bv env evd in
        let f2 = tr_formula dep tvm bv env evd e2 in
1153 1154 1155 1156 1157
        t_let_close vs t1 f2
      end
  | Rel _ ->
      assert false (* quantified variables should be named at this point *)
  | Cast (c, _, _) ->
1158
      tr_formula dep tvm bv env evd c
1159
  | Construct _ | Ind _ | Const _ | App _ ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1160 1161
      let c, args = decompose_app evd f in
      let r = try global_of_constr evd c with _ -> raise NotFO in
1162
      let ls = tr_task_ls dep env evd r in
1163 1164
      begin match ls.Term.ls_value with
        | None ->
1165
            let args = List.filter (fun c -> not (has_WhyType env evd c)) args in
1166 1167
            let k = get_poly_arity ls in
            let args = skip_k_args k args in
1168
            Term.ps_app ls (List.map (tr_term dep tvm bv env evd) args)
1169 1170 1171
        | Some _ ->
          raise NotFO
      end
1172 1173
  | _ (* Proj *) ->
      raise NotFO
1174

1175 1176 1177 1178
let is_global_var id =
  try ignore (Environ.lookup_named id (Global.env ())); true
  with Not_found -> false

1179
let tr_goal gl evd =
1180
  let env = pf_env gl in
1181
  let dep = empty_dep () in
1182
  let rec tr_ctxt tvm bv = function
1183
    | [] ->
1184
        tr_formula dep tvm bv env evd (pf_concl gl)
1185 1186
    | (id, _, _) :: ctxt when is_global_var id ->
        tr_ctxt tvm bv ctxt
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1187
    | (id, None, ty) :: ctxt when is_Set evd ty || is_Type evd ty ->
1188
        let v = Ty.create_tvsymbol (preid_of_id id) in
1189 1190
        let tvm = Idmap.add id (Some (Ty.ty_var v)) tvm in
        tr_ctxt tvm bv ctxt
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1191
    | (id, None, ty) :: ctxt when is_fo_kind evd ty ->
1192
        let tvm = Idmap.add id None tvm in
1193
        tr_ctxt tvm bv ctxt
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1194
    | (id, None, ty) :: ctxt when is_WhyType evd ty ->
1195 1196
        let bv = Idmap.add id None bv in
        tr_ctxt tvm bv ctxt
1197
    | (id, None, ty) :: ctxt ->
1198
        let evd,t = type_of env evd ty in
1199
        begin try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1200
          if is_Set evd t || is_Type evd t then
1201
            let ty = tr_type dep tvm env evd ty in (* DO NOT INLINE! *)
1202
            let vs = Term.create_vsymbol (preid_of_id id) ty in
1203
            let bv = Idmap.add id (Some vs) bv in
1204
            Term.t_forall_close [vs] [] (tr_ctxt tvm bv ctxt)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1205
          else if is_Prop evd t then
1206
            let h = tr_formula dep tvm bv env evd ty in (* DO NOT INLINE! *)
1207