why3tac.ml4 49.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
IFDEF COQ84 THEN

open Libnames

let declare_summary name freeze unfreeze init =
  Summary.declare_summary name
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init; }

let body_of_constant _ c =
  if Reductionops.is_transparent (ConstKey c) then
    Declarations.body_of_constant (Global.lookup_constant c)
  else None

let get_transp_state _ =
  Conv_oracle.get_transp_state ()

let type_of_global = Global.type_of_global

MARCHE Claude's avatar
MARCHE Claude committed
43 44 45 46
let pf_type_of env t = Evd.empty, Tacmach.pf_type_of env t

let type_of env evd t = Evd.empty, Typing.type_of env evd t

47 48 49 50 51 52
let finite_ind v = v

let admit_as_an_axiom = Tactics.admit_as_an_axiom

let map_to_list = Util.array_map_to_list

53 54 55 56 57 58 59 60
let is_global c t =
  match c, kind_of_term t with
  | ConstRef c, Const c' -> eq_constant c c'
  | IndRef i, Ind i' -> eq_ind i i'
  | ConstructRef i, Construct i' -> eq_constructor i i'
  | VarRef id, Var id' -> id = id'
  | _ -> false

61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
ELSE

open Universes
open Globnames
open Vars
open Errors

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
    Declareops.body_of_constant Opaqueproof.empty_opaquetab (Global.lookup_constant c)
  else None

let get_transp_state env =
  Conv_oracle.get_transp_state (Environ.oracle env)

let type_of_global = Global.type_of_global_unsafe

MARCHE Claude's avatar
MARCHE Claude committed
84
let type_of = Typing.type_of
85

MARCHE Claude's avatar
MARCHE Claude committed
86
let pf_type_of = Tacmach.pf_type_of
87

88 89 90 91 92 93 94 95
let finite_ind v = v <> Decl_kinds.CoFinite

let pr_str = Pp.str

let pr_spc = Pp.spc

let pr_fnl = Pp.fnl

96
let admit_as_an_axiom = Tacticals.tclIDTAC
97 98 99 100 101

let map_to_list = CArray.map_to_list

let force x = x

102 103 104 105 106 107 108 109 110 111
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)

let is_global c t = is_global (Lazy.force c) t

112 113 114 115
DECLARE PLUGIN "why3tac"

END

116
module Why3tac = struct
117

118
open Why3
119
open Call_provers
120
open Whyconf
121 122
open Ty
open Term
123

124 125 126 127 128 129 130 131 132 133
let on_leaf_node node f =
  match node with
  | Lib.Leaf lobj -> f lobj
  | Lib.CompilingLibrary _
  | Lib.OpenedModule _
  | Lib.ClosedModule  _
  | Lib.OpenedSection _
  | Lib.ClosedSection _
  | Lib.FrozenState _ -> ()

134
let debug =
135
  try let _ = Sys.getenv "WHY3DEBUG" in true
136 137
  with Not_found -> false

138 139 140 141 142 143
let config =
  try
    Whyconf.read_config None
  with Whyconf.ConfigFailure(file, msg) ->
    error (file ^ ": " ^ msg)

144
let main = Whyconf.get_main config
145

146
let timelimit = timelimit main
147

148
let env = Env.create_env (loadpath main)
149

150 151
let provers = Hashtbl.create 17

152 153 154 155
let get_prover s =
  try
    Hashtbl.find provers s
  with Not_found ->
156 157 158 159 160 161 162 163 164 165 166
    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
167
    let drv = Driver.load_driver env cp.driver cp.extra_drivers in
168 169 170
    Hashtbl.add provers s (cp, drv);
    cp, drv

171
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
172
let print_tvm fmt m =
173 174 175
  Idmap.iter (fun id tv -> match tv with
    | None -> Format.fprintf fmt "%s->not FO@ " (string_of_id id)
    | Some tv -> Format.fprintf fmt "%s->%a@ "
176
                 (string_of_id id) Why3.Pretty.print_tv tv) m
177
let print_bv fmt m =
178 179 180
  Idmap.iter (fun id vs -> match vs with
    | None -> Format.fprintf fmt "%s->not FO@ " (string_of_id id)
    | Some vs -> Format.fprintf fmt "%s->%a@ "
181
                 (string_of_id id) Why3.Pretty.print_vsty vs) m
182

183
(* Coq constants *)
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228

let coq_ref_BinInt = coq_reference "Why3" ["ZArith"; "BinInt"]
let coq_Z = coq_ref_BinInt "Z"
let coq_Zplus = coq_ref_BinInt "Zplus"
let coq_Zmult = coq_ref_BinInt "Zmult"
let coq_Zopp = coq_ref_BinInt "Zopp"
let coq_Zminus = coq_ref_BinInt "Zminus"
let coq_Zdiv = coq_reference "Why3" ["ZArith"; "Zdiv"] "Zdiv"
let coq_Zgt = coq_ref_BinInt "Zgt"
let coq_Zle = coq_ref_BinInt "Zle"
let coq_Zge = coq_ref_BinInt "Zge"
let coq_Zlt = coq_ref_BinInt "Zlt"
let coq_ref_BinNums = coq_reference "Why3" ["Numbers"; "BinNums"]
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"

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"
229

230
let coq_WhyType =
231
  find_reference "Why3" ["Why3"; "BuiltIn"] "WhyType"
232 233

let rec is_WhyType c = match kind_of_term c with
234
  | App (f, [|_|]) -> is_global coq_WhyType f
235 236 237
  | Cast (c, _, _) -> is_WhyType c
  | _ -> false

MARCHE Claude's avatar
MARCHE Claude committed
238
let has_WhyType env evd c = is_WhyType (snd (type_of env evd c))
239

240 241 242 243 244 245
(* 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 *)
246
(*
247 248 249 250 251 252 253 254
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)
255
*)
256

257
let coq_rename_var env na t =
258 259 260 261 262 263
  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)

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

279 280 281
(* 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 =
282 283 284 285 286
  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
  let rec loop env tvm vars t = match kind_of_term t with
287
    | Prod (n, a, t) when is_Set a || is_Type a ->
288 289 290 291 292 293 294 295
        let n, env = coq_rename_var env n a in
        let t = subst1 (mkVar n) t in
        let tvm, tv = add tvm n in
        loop env tvm (tv :: vars) t
    | Prod (n, a, t) when is_WhyType a ->
        let n, env = coq_rename_var env n a in
        let t = subst1 (mkVar n) t in
        loop env tvm vars t
296
    | _ ->
297
        (tvm, List.rev vars), env, t
298
  in
299
  loop env Idmap.empty [] t
300

301 302
(* 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
303
let decomp_type_lambdas tvm env vars t =
304
  let rec loop tvm env vars t = match vars, kind_of_term t with
305 306 307 308
    | vars, Lambda (n, a, t) when is_WhyType a ->
        let id, env = coq_rename_var env n a in
        let t = subst1 (mkVar id) t in
        loop tvm env vars t
309
    | tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
310
        let id, env = coq_rename_var env n a in
311
        let t = subst1 (mkVar id) t in
312
        let tvm = Idmap.add id (Some (Ty.ty_var tv)) tvm in
313
        loop tvm env vars t
314 315
    | [], _ ->
        tvm, env, t
316
    | _ ->
317
        raise NotFO (*TODO: eta-expansion*)
318
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
319
  loop tvm env vars t
320

321 322 323 324 325 326 327 328
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 []

329 330 331 332
let is_fo_kind ty =
  let _, ty = decompose_arrows ty in
  is_Set ty || is_Type ty

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

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

353 354
(* Coq globals *)

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

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

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

367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
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 *)
384 385
let global_dep = ref Decl.Mdecl.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
386 387 388 389 390 391 392 393
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

394 395 396 397 398 399 400 401 402 403
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

404 405 406
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")
407 408

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

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

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

let rec add_local_decls d =
424 425
  let id = Ident.Sid.choose d.Decl.d_news in
  if not (Ident.Mid.mem id (Task.task_known !task)) then begin
426
    assert (Decl.Mdecl.mem d !global_dep);
427
    let dep = Decl.Mdecl.find d !global_dep in
428
    Decl.Sdecl.iter add_local_decls dep.dep_decls;
429 430 431
    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);
432 433 434
    try
      task := Task.add_decl !task d
    with Decl.UnknownIdent id ->
435 436 437 438
      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
439 440
  end

441 442
(* synchronization *)
let () =
443 444 445 446 447 448 449 450 451 452 453 454
  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)
455

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

460
let add_table table r v = table := Refmap.add r v !table
461

462 463 464 465 466 467 468 469 470
(* 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
471
  | Construct _ when is_global coq_xH p ->
472
      Big_int.unit_big_int
473
  | App (f, [|a|]) when is_global coq_xI f ->
474
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
475
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
476
  | App (f, [|a|]) when is_global coq_xO f ->
477
      (* Mult (Cst 2, tr_positive a) *)
478 479 480 481 482 483
      Big_int.mult_big_int big_two (tr_positive a)
  | Cast (p, _, _) ->
      tr_positive p
  | _ ->
      raise NotArithConstant

Andrei Paskevich's avatar
Andrei Paskevich committed
484 485
let const_of_big_int b =
  Term.t_const
486
    (Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
487

488
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
489
let rec tr_arith_constant dep t = match kind_of_term t with
490 491
  | Construct _ when is_global coq_Z0 t -> Term.t_nat_const 0
  | App (f, [|a|]) when is_global coq_Zpos f ->
492
      const_of_big_int (tr_positive a)
493
  | App (f, [|a|]) when is_global coq_Zneg f ->
494 495 496
      let t = const_of_big_int (tr_positive a) in
      let fs = why_constant_int dep ["prefix -"] in
      Term.fs_app fs [t] Ty.ty_int
497
  | Const _ when is_global coq_R0 t ->
498
      Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
499
  | Const _ when is_global coq_R1 t ->
500
      Term.t_const (Number.ConstReal (Number.real_const_dec "1" "0" None))
501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517
(*   | 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, _, _) ->
518
      tr_arith_constant dep t
519 520 521
  | _ ->
      raise NotArithConstant

MARCHE Claude's avatar
MARCHE Claude committed
522
let rec tr_type dep tvm env evd t =
523 524
  let t = Reductionops.clos_norm_flags
      (Closure.RedFlags.red_add_transparent
525
	 Closure.betadeltaiota (get_transp_state env))
MARCHE Claude's avatar
MARCHE Claude committed
526
      env evd t in
527
  if is_global coq_Z t then
528
    Ty.ty_int
529
  else if is_global coq_R t then
530 531
    Ty.ty_real
  else match kind_of_term t with
532
    | Var x when Idmap.mem x tvm ->
533 534 535 536
        begin match Idmap.find x tvm with
          | None -> raise NotFO
          | Some ty -> ty
        end
537
    | _ ->
538 539 540
        let f, cl = decompose_app t in
        begin try
          let r = global_of_constr f in
MARCHE Claude's avatar
MARCHE Claude committed
541 542
          let ts = tr_task_ts dep env evd r in
          let cl = List.filter (fun c -> not (has_WhyType env evd c)) cl in
543 544
          assert (List.length ts.Ty.ts_args = List.length cl);
          (* since t:Set *)
MARCHE Claude's avatar
MARCHE Claude committed
545
          Ty.ty_app ts (List.map (tr_type dep tvm env evd) cl)
546 547 548 549 550 551 552
        with
          | Not_found ->
              raise NotFO
          | NotFO ->
              (* TODO: we need to abstract some part of (f cl) *)
              raise NotFO
        end
553

554
(* the type symbol for r *)
MARCHE Claude's avatar
MARCHE Claude committed
555 556
and tr_task_ts dep env evd r =
  let ts = tr_global_ts dep env evd r in
557 558 559 560
  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;
561
  ts
562 563

(* the type declaration for r *)
MARCHE Claude's avatar
MARCHE Claude committed
564
and tr_global_ts dep env evd (r : global_reference) =
565
  try
566 567 568 569 570
    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
571 572
  with Not_found ->
    add_table global_ts r None;
573
    let dep' = empty_dep () in
574
    match r with
575
      | VarRef id ->
576
          let ty = try type_of_global r with Not_found -> raise NotFO in
577 578 579 580 581 582
          let (_,vars), _, t = decomp_type_quantifiers env ty in
          if not (is_Set t) && not (is_Type t) then raise NotFO;
          let id = preid_of_id id in
          let ts = Ty.create_tysymbol id vars None in
          let decl = Decl.create_ty_decl ts in
          add_table global_ts r (Some ts);
Andrei Paskevich's avatar
Andrei Paskevich committed
583
          add_new_decl dep !dep' decl;
584
          ts
585
      | ConstructRef _ ->
586
          assert false
587
      | ConstRef c ->
588
          let ty = type_of_global r in
589 590
          let (_,vars), _, t = decomp_type_quantifiers env ty in
          if not (is_Set t) && not (is_Type t) then raise NotFO;
591
          let id = preid_of_id (Nametab.basename_of_global r) in
592
          let ts = match body_of_constant env c with
593 594 595
            | Some b ->
                let b = force b in
                let tvm, env, t = decomp_type_lambdas Idmap.empty env vars b in
MARCHE Claude's avatar
MARCHE Claude committed
596
                let def = Some (tr_type dep' tvm env evd t) in
597 598 599 600 601
                Ty.create_tysymbol id vars def
                  (* FIXME: is it correct to use None when NotFO? *)
            | None ->
                Ty.create_tysymbol id vars None
          in
602
          let decl = Decl.create_ty_decl ts in
603
          add_table global_ts r (Some ts);
Andrei Paskevich's avatar
Andrei Paskevich committed
604
          add_new_decl dep !dep' decl;
605
          ts
606
      | IndRef i ->
607 608 609 610
          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
611
            let ty = type_of_global r in
612 613
            let (_,vars), _, t = decomp_type_quantifiers env ty in
            if not (is_Set t) && not (is_Type t) then raise NotFO;
614
            let id = preid_of_id (Nametab.basename_of_global r) in
615 616 617 618 619 620 621 622 623
            let ts = Ty.create_tysymbol id vars None in
            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
624 625
            let opaque = Ty.Stv.of_list ts.Ty.ts_args in
            let constr = Array.length oib.mind_nf_lc in
626 627
            let mk_constructor k _tyk = (* k-th constructor *)
              let r = ConstructRef (j, k+1) in
628
              let ty = type_of_global r in
629
              let (_,vars), env, t = decomp_type_quantifiers env ty in
630 631 632 633
              let l, c = decompose_arrows t in
              let tvm = match kind_of_term c with
                | App (_, v) ->
                    let v = Array.to_list v in
MARCHE Claude's avatar
MARCHE Claude committed
634
                    let no_whytype c = not (has_WhyType env evd c) in
635
                    let v = List.filter no_whytype v in
636 637 638 639 640 641 642 643
                    let add v1 v2 tvm = match kind_of_term v1 with
                      | 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
644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
                | 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
660
                | _ (* Proj *) -> assert false
661
              in
MARCHE Claude's avatar
MARCHE Claude committed
662
              let l = List.map (tr_type dep' tvm env evd) l in
663
              let id = preid_of_id (Nametab.basename_of_global r) in
664
              let ls = Term.create_fsymbol ~opaque ~constr id l tyj in
665
              add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
666
              add_poly_arity ls vars;
667
              ls, List.map (fun _ -> None) ls.ls_args
668
            in
Andrei Paskevich's avatar
Andrei Paskevich committed
669 670 671 672
            let cl =
              try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
              with NotFO -> []
            in
673
            (j, oib), (ts, cl)
Andrei Paskevich's avatar
Andrei Paskevich committed
674 675 676
          in
          let dl = Array.mapi make_one mib.mind_packets in
          let dl = Array.to_list dl in
677 678 679 680 681 682
          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
MARCHE Claude's avatar
MARCHE Claude committed
683
                  make_one_ls dep' env evd r;
684 685 686 687
                  let ls = lookup_table global_ls r in
                  let d = Decl.create_param_decl ls in
                  sl := d :: !sl
                with NotFO ->
688
                  ()
689 690 691 692
              done;
              Decl.create_ty_decl ts :: tl, dl, !sl
            end else
              tl, d :: dl, sl
Andrei Paskevich's avatar
Andrei Paskevich committed
693
          in
694
          let tl, dl, sl = List.fold_right add dl ([], [], []) in
Andrei Paskevich's avatar
Andrei Paskevich committed
695 696
          let decl =
            if dl = [] then None else Some (Decl.create_data_decl dl)
697 698
          in
          (* Format.printf "decl = %a@." Pretty.print_decl decl; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
699 700
          List.iter (add_new_decl dep !dep') tl;
          List.iter (add_dep dep') tl;
701
          Opt.iter (add_new_decl dep !dep') decl;
702 703
          Opt.iter (add_dep dep') decl;
          List.iter (add_new_decl dep !dep') sl;
704
          lookup_table global_ts r
705

706
(* the function/predicate symbol for r *)
MARCHE Claude's avatar
MARCHE Claude committed
707 708
and tr_task_ls dep env evd r =
  let ls = tr_global_ls dep env evd r in
709 710 711 712
  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;
713
  ls
714

715
(* the function/predicate symbol declaration for r *)
MARCHE Claude's avatar
MARCHE Claude committed
716
and tr_global_ls dep env evd r =
717
  try
718 719 720 721 722
    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
723 724
  with Not_found ->
    add_table global_ls r None;
725
    let dep' = empty_dep () in
726
    (* type_of_global may fail on a local, higher-order variable *)
727
    let ty = try type_of_global r with Not_found -> raise NotFO in
728
    let (tvm, _), env, t = decomp_type_quantifiers env ty in
729
    if is_Set t || is_Type t then raise NotFO;
730
    let _, t = decompose_arrows t in
731 732
    match r with
      | ConstructRef _ ->
733
          assert (not (is_Prop t)); (* is a proof *)
MARCHE Claude's avatar
MARCHE Claude committed
734
          let evd,s = type_of env evd t in
735
          if not (is_Set s || is_Type s) then raise NotFO;
MARCHE Claude's avatar
MARCHE Claude committed
736
          ignore (tr_type dep' tvm env evd t);
737
          lookup_table global_ls r
738
      | ConstRef c ->
MARCHE Claude's avatar
MARCHE Claude committed
739
          let pl, d = decompose_definition dep' env evd c in
Andrei Paskevich's avatar
Andrei Paskevich committed
740
          List.iter (add_new_decl dep !dep') pl;
741
          List.iter (add_dep dep') pl;
742
          Opt.iter (add_new_decl dep !dep') d;
743
          lookup_table global_ls r
744 745
      | IndRef i ->
          assert (is_Prop t);
MARCHE Claude's avatar
MARCHE Claude committed
746
          let pl, d = decompose_inductive dep' env evd i in
Andrei Paskevich's avatar
Andrei Paskevich committed
747
          List.iter (add_new_decl dep !dep') pl;
748
          List.iter (add_dep dep') pl;
749
          Opt.iter (add_new_decl dep !dep') d;
750 751
          lookup_table global_ls r
      | VarRef _ ->
MARCHE Claude's avatar
MARCHE Claude committed
752
          make_one_ls dep' env evd r;
753 754
          let ls = lookup_table global_ls r in
          let decl = Decl.create_param_decl ls in
Andrei Paskevich's avatar
Andrei Paskevich committed
755
          add_new_decl dep !dep' decl;
756 757
          ls

MARCHE Claude's avatar
MARCHE Claude committed
758
and make_one_ls dep env evd r =
759
  let ty = type_of_global r in
760 761 762
  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
MARCHE Claude's avatar
MARCHE Claude committed
763
  let args = List.map (tr_type dep tvm env evd) l in
764 765 766 767 768 769
  let ls =
    let id = preid_of_id (Nametab.basename_of_global r) in
    if is_Prop t then
        (* predicate definition *)
      create_lsymbol id args None
    else
MARCHE Claude's avatar
MARCHE Claude committed
770
      let evd,s = type_of env evd t in
771 772
      if is_Set s || is_Type s then
          (* function definition *)
MARCHE Claude's avatar
MARCHE Claude committed
773
        let ty = tr_type dep tvm env evd t in
774 775 776 777 778
        create_lsymbol id args (Some ty)
      else
        raise NotFO
  in
  add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
779
  add_poly_arity ls vars
780

MARCHE Claude's avatar
MARCHE Claude committed
781
and decompose_definition dep env evd c =
782
  let dl = match body_of_constant env c with
783
    | None ->
784
        [ConstRef c, None]
785
    | Some b ->
786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807
        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
808
  in
MARCHE Claude's avatar
MARCHE Claude committed
809
  List.iter (fun (r, _) -> make_one_ls dep env evd r) dl;
810
  let make_one_decl (r, b) =
811 812 813
    let ls = lookup_table global_ls r in
    match b with
      | None ->
814
          assert false
815
      | Some b ->
816 817
          let tvs = List.fold_left Ty.ty_freevars Stv.empty
            (Ty.oty_cons ls.ls_args ls.ls_value) in
818 819
          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
820
          let ty = type_of_global r in
821
          let (_, vars), env, _ = decomp_type_quantifiers env ty in
822
          let conv tv = Stdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
823
          let vars = List.map conv vars in
824 825
          let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
          let (bv, vsl), env, b =
826
            decomp_lambdas dep tvm Idmap.empty env ls.ls_args b
827 828 829
          in
          begin match ls.ls_value with
            | None ->
MARCHE Claude's avatar
MARCHE Claude committed
830
                let b = tr_formula dep tvm bv env evd b in
831
                Decl.make_ls_defn ls vsl b
832
            | Some _ ->
MARCHE Claude's avatar
MARCHE Claude committed
833
                let b = tr_term dep tvm bv env evd b in
834
                Decl.make_ls_defn ls vsl b
835
          end
836
  in
837
  match dl with
838 839
    | [r, None] ->
        [Decl.create_param_decl (lookup_table global_ls r)], None
840
    | _ ->
841 842 843 844 845 846 847 848
        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)
849

MARCHE Claude's avatar
MARCHE Claude committed
850
and decompose_inductive dep env evd i =
851 852 853
  let mib, _ = Global.lookup_inductive i in
  (* first, the inductive types *)
  let make_one_ls j _ = (* j-th inductive *)
MARCHE Claude's avatar
MARCHE Claude committed
854
    make_one_ls dep env evd (IndRef (ith_mutual_inductive i j))
855 856 857 858 859 860 861 862
  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
863
      let ty = type_of_global r in
864 865 866
      let (_,vars), env, f = decomp_type_quantifiers env ty in
      let tvm =
        let add v1 v2 tvm =
867
          let v2 = Some (Ty.ty_var v2) in
868 869
          Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
870
        List.fold_right2 add vars (get_poly_arity ls) Idmap.empty
871
      in
MARCHE Claude's avatar
MARCHE Claude committed
872
      let f = tr_formula dep tvm Idmap.empty env evd f in
873 874 875 876
      let id = preid_of_id (Nametab.basename_of_global r) in
      let pr = Decl.create_prsymbol id in
      pr, f
    in
877 878 879 880
    let cl =
      try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
      with NotFO -> []
    in
881 882
    ls, cl
  in
883 884 885 886 887 888
  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
889
  let s = if finite_ind mib.mind_finite then Decl.Ind else Decl.Coind in
890
  pl, if dl = [] then None else Some (Decl.create_ind_decl s dl)
891

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

MARCHE Claude's avatar
MARCHE Claude committed
1025
and quantifiers n a b dep tvm bv env evd =
1026
  let id, env = coq_rename_var env n a in
1027
  let b = subst1 (mkVar id) b in
MARCHE Claude's avatar
MARCHE Claude committed
1028
  let t = tr_type dep tvm env evd a in
1029
  let vs = Term.create_vsymbol (preid_of_id id) t in
1030
  let bv = Idmap.add id (Some vs) bv in
1031 1032
  vs, t, bv, env, b

1033 1034
(* translation of a Coq formula
   assumption f:Prop *)
MARCHE Claude's avatar
MARCHE Claude committed
1035
and tr_formula dep tvm bv env evd f = match kind_of_term f with
1036
  | App(c, [|t;a;b|]) when is_global coq_eq c ->
MARCHE Claude's avatar
MARCHE Claude committed
1037
      let evd,ty = type_of env evd t in
1038
      if not (is_Set ty || is_Type ty) then raise NotFO;
MARCHE Claude's avatar
MARCHE Claude committed
1039 1040
      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)
1041
  (* comparisons on integers *)
1042
  | App(c, [|a;b|]) when is_global coq_Zle c ->
1043
      let ls = why_constant_int dep ["infix <="] in
MARCHE Claude's avatar
MARCHE Claude committed
1044
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1045
  | App(c, [|a;b|]) when is_global coq_Zlt c ->
1046
      let ls = why_constant_int dep ["infix <"] in
MARCHE Claude's avatar
MARCHE Claude committed
1047
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1048
  | App(c, [|a;b|]) when is_global coq_Zge c ->
1049
      let ls = why_constant_int dep ["infix >="] in
MARCHE Claude's avatar
MARCHE Claude committed
1050
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1051
  | App(c, [|a;b|]) when is_global coq_Zgt c ->
1052
      let ls = why_constant_int dep ["infix >"] in
MARCHE Claude's avatar
MARCHE Claude committed
1053
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1054
  (* comparisons on reals *)
1055
  | App(c, [|a;b|]) when is_global coq_Rle c ->
1056
      let ls = why_constant_real dep ["infix <="] in
MARCHE Claude's avatar
MARCHE Claude committed
1057
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1058
  | App(c, [|a;b|]) when is_global coq_Rlt c ->
1059
      let ls = why_constant_real dep ["infix <"] in
MARCHE Claude's avatar
MARCHE Claude committed
1060
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1061
  | App(c, [|a;b|]) when is_global coq_Rge c ->
1062
      let ls = why_constant_real dep ["infix >="] in
MARCHE Claude's avatar
MARCHE Claude committed
1063
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1064
  | App(c, [|a;b|]) when is_global coq_Rgt c ->
1065
      let ls = why_constant_real dep ["infix >"] in
MARCHE Claude's avatar
MARCHE Claude committed
1066
      Term.ps_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
1067
  (* propositional logic *)
1068
  | _ when is_global coq_False f ->
1069
      Term.t_false
1070
  | _ when is_global coq_True f ->
1071
      Term.t_true
1072
  | App(c, [|a|]) when is_global coq_not c ->
MARCHE Claude's avatar
MARCHE Claude committed
1073
      Term.t_not (tr_formula dep tvm bv env evd a)
1074
  | App(c, [|a;b|]) when is_global coq_and c ->
MARCHE Claude's avatar
MARCHE Claude committed
1075
      Term.t_and (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
1076
  | App(c, [|a;b|]) when is_global coq_or c ->
MARCHE Claude's avatar
MARCHE Claude committed
1077
      Term.t_or (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
1078
  | App(c, [|a;b|]) when is_global coq_iff c ->
MARCHE Claude's avatar
MARCHE Claude committed
1079
      Term.t_iff (tr_formula dep tvm bv env evd a) (tr_formula dep tvm bv env evd b)
1080
  | Prod (n, a, b) ->