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

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

34
open Why3
35
open Call_provers
36
open Whyconf
37 38
open Ty
open Term
39

40
let debug =
41
  try let _ = Sys.getenv "WHY3DEBUG" in true
42 43
  with Not_found -> false

44 45 46 47 48 49 50 51 52
let config =
  try
    let _ = Sys.getenv "WHY3NOCONFIG" in
    Whyconf.default_config ""
  with Not_found -> try
    Whyconf.read_config None
  with Whyconf.ConfigFailure(file, msg) ->
    error (file ^ ": " ^ msg)

53
let main = Whyconf.get_main config
54

55
let timelimit = timelimit main
56

57
let env = Env.create_env (loadpath main)
58

59 60
let provers = Hashtbl.create 17

61 62 63 64
let get_prover s =
  try
    Hashtbl.find provers s
  with Not_found ->
65 66 67 68 69 70 71 72 73 74 75
    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
76
    let drv = Driver.load_driver env cp.driver cp.extra_drivers in
77 78 79
    Hashtbl.add provers s (cp, drv);
    cp, drv

80
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
81
let print_tvm fmt m =
82 83 84
  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@ "
85
                 (string_of_id id) Why3.Pretty.print_tv tv) m
86
let print_bv fmt m =
87 88 89
  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@ "
90
                 (string_of_id id) Why3.Pretty.print_vsty vs) m
91

92 93 94 95 96 97 98 99 100 101 102 103 104
(* Coq constants *)
let logic_dir = ["Coq";"Logic";"Decidable"]

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

105
let constant = gen_constant_in_modules "why" coq_modules
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134

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

let coq_R = lazy (constant "R")
let coq_R0 = lazy (constant "R0")
let coq_R1 = lazy (constant "R1")
let coq_Rgt = lazy (constant "Rgt")
let coq_Rle = lazy (constant "Rle")
let coq_Rge = lazy (constant "Rge")
let coq_Rlt = lazy (constant "Rlt")
let coq_Rplus = lazy (constant "Rplus")
let coq_Rmult = lazy (constant "Rmult")
let coq_Ropp = lazy (constant "Ropp")
135
let coq_Rinv = lazy (constant "Rinv")
136 137 138 139 140 141
let coq_Rminus = lazy (constant "Rminus")
let coq_Rdiv = lazy (constant "Rdiv")
let coq_powerRZ = lazy (constant "powerRZ")

let coq_iff = lazy (constant "iff")

142 143
let is_constant t c = try t = Lazy.force c with _ -> false

144 145 146 147 148 149 150 151 152 153
let coq_WhyType =
  lazy (gen_constant_in_modules "why" [["Why3"; "BuiltIn"]] "WhyType")

let rec is_WhyType c = match kind_of_term c with
  | App (f, [|_|]) -> is_constant f coq_WhyType
  | Cast (c, _, _) -> is_WhyType c
  | _ -> false

let has_WhyType env c = is_WhyType (type_of env Evd.empty c)

154 155 156 157 158 159
(* 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 *)
160
(*
161 162 163 164 165 166 167 168
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)
169
*)
170

171
let coq_rename_var env na t =
172 173 174 175 176 177
  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)

178
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
179
   identifiers n1...nk with the same path as c, if they exist; otherwise
180
   raises NotFO *)
181 182 183
let rec_names_for c =
  let mp,dp,_ = Names.repr_con c in
  array_map_to_list
184 185
    (function
       | Name id ->
186
           let c' = Names.make_con mp dp (label_of_id id) in
187 188
           ignore
             (try Global.lookup_constant c' with Not_found -> raise NotFO);
189
           c'
190
       | Anonymous ->
191
           raise NotFO)
192

193 194 195
(* 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 =
196 197 198 199 200
  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
201
    | Prod (n, a, t) when is_Set a || is_Type a ->
202 203 204 205 206 207 208 209
        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
210
    | _ ->
211
        (tvm, List.rev vars), env, t
212
  in
213
  loop env Idmap.empty [] t
214

215 216
(* 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
217
let decomp_type_lambdas tvm env vars t =
218
  let rec loop tvm env vars t = match vars, kind_of_term t with
219 220 221 222
    | 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
223
    | tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
224
        let id, env = coq_rename_var env n a in
225
        let t = subst1 (mkVar id) t in
226
        let tvm = Idmap.add id (Some (Ty.ty_var tv)) tvm in
227
        loop tvm env vars t
228 229
    | [], _ ->
        tvm, env, t
230
    | _ ->
231
        raise NotFO (*TODO: eta-expansion*)
232
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233
  loop tvm env vars t
234

235 236 237 238 239 240 241 242
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 []

243 244 245 246
let is_fo_kind ty =
  let _, ty = decompose_arrows ty in
  is_Set ty || is_Type ty

247
let decomp_lambdas _dep _tvm bv env vars t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248
  let rec loop bv vsl env vars t = match vars, kind_of_term t with
249
    | [], _ ->
250
        (bv, List.rev vsl), env, t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251
    | ty :: vars, Lambda (n, a, t) ->
252
        let id, env = coq_rename_var env n a in
253 254
        let t = subst1 (mkVar id) t in
        let vs = create_vsymbol (preid_of_id id) ty in
255
        let bv = Idmap.add id (Some vs) bv in
256
        loop bv (vs :: vsl) env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257
    | _ ->
258
        raise NotFO (*TODO: eta-expansion*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259
  in
260
  loop bv [] env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261

262
let rec skip_k_args k cl = match k, cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
263 264
  | [], _ -> cl
  | _ :: k, _ :: cl -> skip_k_args k cl
265 266
  | _, [] -> raise NotFO

267 268
(* Coq globals *)

269
(* Coq reference -> symbol *)
270
let global_ts = ref Refmap.empty
271 272
let global_ls = ref Refmap.empty

273 274
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
275
let add_poly_arity ls n = poly_arity := Mls.add ls n !poly_arity
276 277
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity

278 279
(* ident -> decl *)
let global_decl = ref Ident.Mid.empty
280

281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297
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 *)
298 299
let global_dep = ref Decl.Mdecl.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
300 301 302 303 304 305 306 307
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

308 309 310 311 312 313 314 315 316 317
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

318 319 320
let th_int = lazy (Env.find_theory env ["int"] "Int")
let th_eucl = lazy (Env.find_theory env ["int"] "EuclideanDivision")
let th_real = lazy (Env.find_theory env ["real"] "Real")
321 322

let why_constant_int dep s =
323
  task := Task.use_export !task (Lazy.force th_int);
324
  dep := { !dep with dep_use_int = true };
325
  Theory.ns_find_ls (Lazy.force th_int).Theory.th_export s
326 327

let why_constant_eucl dep s =
328
  task := Task.use_export !task (Lazy.force th_eucl);
329
  dep := { !dep with dep_use_eucl = true };
330
  Theory.ns_find_ls (Lazy.force th_eucl).Theory.th_export s
331 332

let why_constant_real dep s =
333
  task := Task.use_export !task (Lazy.force th_real);
334
  dep := { !dep with dep_use_real = true };
335
  Theory.ns_find_ls (Lazy.force th_real).Theory.th_export s
336 337

let rec add_local_decls d =
338 339
  let id = Ident.Sid.choose d.Decl.d_news in
  if not (Ident.Mid.mem id (Task.task_known !task)) then begin
340
    assert (Decl.Mdecl.mem d !global_dep);
341
    let dep = Decl.Mdecl.find d !global_dep in
342
    Decl.Sdecl.iter add_local_decls dep.dep_decls;
343 344 345
    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);
346 347 348
    try
      task := Task.add_decl !task d
    with Decl.UnknownIdent id ->
349 350 351 352
      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
353 354
  end

355 356 357
(* synchronization *)
let () =
  Summary.declare_summary "Why globals"
358
    { Summary.freeze_function =
359 360
        (fun () ->
           !global_ts, !global_ls, !poly_arity, !global_decl, !global_dep);
361
      Summary.unfreeze_function =
362 363 364
        (fun (ts,ls,pa,gdecl,gdep) ->
           global_ts := ts; global_ls := ls; poly_arity := pa;
           global_decl := gdecl; global_dep := gdep);
365
      Summary.init_function =
366 367 368 369 370 371
        (fun () ->
           global_ts := Refmap.empty;
           global_ls := Refmap.empty;
           poly_arity := Mls.empty;
           global_decl := Ident.Mid.empty;
           global_dep := Decl.Mdecl.empty);
372 373
      (* Summary.survive_module = true; *)
      (* Summary.survive_section = true; *)
374
    }
375

376
let lookup_table table r = match Refmap.find r !table with
377 378 379
  | None -> raise NotFO
  | Some d -> d

380
let add_table table r v = table := Refmap.add r v !table
381

382 383 384 385 386 387 388 389 390
(* 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
391
  | Construct _ when is_constant p coq_xH ->
392
      Big_int.unit_big_int
393
  | App (f, [|a|]) when is_constant f coq_xI ->
394
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
395
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
396
  | App (f, [|a|]) when is_constant f coq_xO ->
397
      (* Mult (Cst 2, tr_positive a) *)
398 399 400 401 402 403 404
      Big_int.mult_big_int big_two (tr_positive a)
  | Cast (p, _, _) ->
      tr_positive p
  | _ ->
      raise NotArithConstant

let const_of_big_int b = Term.t_int_const (Big_int.string_of_big_int b)
405

406 407
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant t = match kind_of_term t with
408
  | Construct _ when is_constant t coq_Z0 ->
409
      Term.t_int_const "0"
410
  | App (f, [|a|]) when is_constant f coq_Zpos ->
411
      const_of_big_int (tr_positive a)
412
  | App (f, [|a|]) when is_constant f coq_Zneg ->
413
      const_of_big_int (Big_int.minus_big_int (tr_positive a))
414
  | Const _ when is_constant t coq_R0 ->
415
      Term.t_real_const (Term.RConstDecimal ("0", "0", None))
416
  | Const _ when is_constant t coq_R1 ->
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
      Term.t_real_const (Term.RConstDecimal ("1", "0", None))
(*   | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(*       let ta = tr_arith_constant a in *)
(*       let tb = tr_arith_constant b in *)
(*       begin match ta,tb with *)
(*         | RCst na, RCst nb -> RCst (Big_int.add_big_int na nb) *)
(*         | _ -> raise NotArithConstant *)
(*       end *)
(*   | App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> *)
(*       let ta = tr_arith_constant a in *)
(*       let tb = tr_arith_constant b in *)
(*       begin match ta,tb with *)
(*         | RCst na, RCst nb -> RCst (Big_int.mult_big_int na nb) *)
(*         | _ -> raise NotArithConstant *)
(*       end *)
(*   | App (f, [|a;b|]) when f = Lazy.force coq_powerRZ -> *)
(*       tr_powerRZ a b *)
  | Cast (t, _, _) ->
      tr_arith_constant t
  | _ ->
      raise NotArithConstant

439
let rec tr_type dep tvm env t =
440
  let t = Reductionops.nf_betadeltaiota env Evd.empty t in
441
  if is_constant t coq_Z then
442
    Ty.ty_int
443
  else if is_constant t coq_R then
444 445
    Ty.ty_real
  else match kind_of_term t with
446
    | Var x when Idmap.mem x tvm ->
447 448 449 450
        begin match Idmap.find x tvm with
          | None -> raise NotFO
          | Some ty -> ty
        end
451
    | _ ->
452 453 454 455
        let f, cl = decompose_app t in
        begin try
          let r = global_of_constr f in
          let ts = tr_task_ts dep env r in
456
          let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
457 458
          assert (List.length ts.Ty.ts_args = List.length cl);
          (* since t:Set *)
459 460 461 462 463 464 465 466
          Ty.ty_app ts (List.map (tr_type dep tvm env) cl)
        with
          | Not_found ->
              raise NotFO
          | NotFO ->
              (* TODO: we need to abstract some part of (f cl) *)
              raise NotFO
        end
467

468
(* the type symbol for r *)
469
and tr_task_ts dep env r =
470
  let ts = tr_global_ts dep env r in
471 472 473 474
  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;
475
  ts
476 477

(* the type declaration for r *)
478
and tr_global_ts dep env r =
479
  try
480 481 482 483 484
    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
485 486
  with Not_found ->
    add_table global_ts r None;
487
    let dep' = empty_dep () in
488
    match r with
489
      | VarRef id ->
490
          let ty = try Global.type_of_global r with Not_found -> raise NotFO in
491 492 493 494 495 496
          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
497
          add_new_decl dep !dep' decl;
498
          ts
499
      | ConstructRef _ ->
500
          assert false
501
      | ConstRef c ->
502 503 504
          let ty = Global.type_of_global r in
          let (_,vars), _, t = decomp_type_quantifiers env ty in
          if not (is_Set t) && not (is_Type t) then raise NotFO;
505
          let id = preid_of_id (Nametab.basename_of_global r) in
Claude Marche's avatar
Claude Marche committed
506
          let ts = match CoqCompat.body_of_constant (Global.lookup_constant c) with
507 508 509 510 511 512 513 514 515
            | Some b ->
                let b = force b in
                let tvm, env, t = decomp_type_lambdas Idmap.empty env vars b in
                let def = Some (tr_type dep' tvm env t) in
                Ty.create_tysymbol id vars def
                  (* FIXME: is it correct to use None when NotFO? *)
            | None ->
                Ty.create_tysymbol id vars None
          in
516
          let decl = Decl.create_ty_decl ts in
517
          add_table global_ts r (Some ts);
Andrei Paskevich's avatar
Andrei Paskevich committed
518
          add_new_decl dep !dep' decl;
519
          ts
520
      | IndRef i ->
521 522 523 524 525 526 527
          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
            let ty = Global.type_of_global r in
            let (_,vars), _, t = decomp_type_quantifiers env ty in
            if not (is_Set t) && not (is_Type t) then raise NotFO;
528
            let id = preid_of_id (Nametab.basename_of_global r) in
529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
            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
            let mk_constructor k _tyk = (* k-th constructor *)
              let r = ConstructRef (j, k+1) in
              let ty = Global.type_of_global r in
              let (_,vars), env, t = decomp_type_quantifiers env ty in
              let tvm =
                let add v1 v2 tvm =
544
                  let v2 = Some (Ty.ty_var v2) in
545 546 547 548 549 550
                  Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
                in
                List.fold_right2 add vars ts.Ty.ts_args Idmap.empty
              in
              let l, _ = decompose_arrows t in
              let l = List.map (tr_type dep' tvm env) l in
551
              let id = preid_of_id (Nametab.basename_of_global r) in
552 553
              let ls = Term.create_lsymbol id l (Some tyj) in
              add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
554
              add_poly_arity ls vars;
555
              ls, List.map (fun _ -> None) ls.ls_args
556
            in
Andrei Paskevich's avatar
Andrei Paskevich committed
557 558 559 560 561 562 563 564 565 566 567 568 569 570
            let cl =
              try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
              with NotFO -> []
            in
            ts, cl
          in
          let dl = Array.mapi make_one mib.mind_packets in
          let dl = Array.to_list dl in
          let add (ts, cl as d) (tl, dl) =
            if cl = [] then Decl.create_ty_decl ts :: tl, dl else tl, d :: dl
          in
          let tl, dl = List.fold_right add dl ([], []) in
          let decl =
            if dl = [] then None else Some (Decl.create_data_decl dl)
571 572
          in
          (* Format.printf "decl = %a@." Pretty.print_decl decl; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
573 574 575
          List.iter (add_new_decl dep !dep') tl;
          List.iter (add_dep dep') tl;
          Util.option_iter (add_new_decl dep !dep') decl;
576
          lookup_table global_ts r
577

578
(* the function/predicate symbol for r *)
579
and tr_task_ls dep env r =
580
  let ls = tr_global_ls dep env r in
581 582 583 584
  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;
585
  ls
586

587
(* the function/predicate symbol declaration for r *)
588
and tr_global_ls dep env r =
589
  try
590 591 592 593 594
    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
595 596
  with Not_found ->
    add_table global_ls r None;
597
    let dep' = empty_dep () in
598 599
    (* type_of_global may fail on a local, higher-order variable *)
    let ty = try Global.type_of_global r with Not_found -> raise NotFO in
600
    let (tvm, _), env, t = decomp_type_quantifiers env ty in
601
    if is_Set t || is_Type t then raise NotFO;
602
    let _, t = decompose_arrows t in
603 604
    match r with
      | ConstructRef _ ->
605
          assert (not (is_Prop t)); (* is a proof *)
606 607 608 609
          let s = type_of env Evd.empty t in
          if not (is_Set s || is_Type s) then raise NotFO;
          ignore (tr_type dep' tvm env t);
          lookup_table global_ls r
610
      | ConstRef c ->
611
          let pl, d = decompose_definition dep' env c in
Andrei Paskevich's avatar
Andrei Paskevich committed
612
          List.iter (add_new_decl dep !dep') pl;
613
          List.iter (add_dep dep') pl;
Andrei Paskevich's avatar
Andrei Paskevich committed
614
          Util.option_iter (add_new_decl dep !dep') d;
615
          lookup_table global_ls r
616 617
      | IndRef i ->
          assert (is_Prop t);
618
          let pl, d = decompose_inductive dep' env i in
Andrei Paskevich's avatar
Andrei Paskevich committed
619
          List.iter (add_new_decl dep !dep') pl;
620
          List.iter (add_dep dep') pl;
Andrei Paskevich's avatar
Andrei Paskevich committed
621
          Util.option_iter (add_new_decl dep !dep') d;
622 623 624 625 626
          lookup_table global_ls r
      | VarRef _ ->
          make_one_ls dep' env r;
          let ls = lookup_table global_ls r in
          let decl = Decl.create_param_decl ls in
Andrei Paskevich's avatar
Andrei Paskevich committed
627
          add_new_decl dep !dep' decl;
628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650
          ls

and make_one_ls dep env r =
  let ty = Global.type_of_global r in
  let (tvm, vars), env, t = decomp_type_quantifiers env ty in
  if is_Set t || is_Type t then raise NotFO;
  let l, t = decompose_arrows t in
  let args = List.map (tr_type dep tvm env) l in
  let ls =
    let id = preid_of_id (Nametab.basename_of_global r) in
    if is_Prop t then
        (* predicate definition *)
      create_lsymbol id args None
    else
      let s = type_of env Evd.empty t in
      if is_Set s || is_Type s then
          (* function definition *)
        let ty = tr_type dep tvm env t in
        create_lsymbol id args (Some ty)
      else
        raise NotFO
  in
  add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
651
  add_poly_arity ls vars
652

653
and decompose_definition dep env c =
Claude Marche's avatar
Claude Marche committed
654
  let dl = match CoqCompat.body_of_constant (Global.lookup_constant c) with
655
    | None ->
656
        [ConstRef c, None]
657
    | Some b ->
658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679
        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
680
  in
681
  List.iter (fun (r, _) -> make_one_ls dep env r) dl;
682
  let make_one_decl (r, b) =
683 684 685
    let ls = lookup_table global_ls r in
    match b with
      | None ->
686
          assert false
687
      | Some b ->
688 689 690 691
          let tvs = List.fold_left Ty.ty_freevars Stv.empty
            (Ty.oty_cons ls.ls_args ls.ls_value) in
          let add tv tvm = Util.Mstr.add tv.tv_name.Ident.id_string tv tvm in
          let tvm = Stv.fold add tvs Util.Mstr.empty in
692
          let ty = Global.type_of_global r in
693 694 695
          let (_, vars), env, _ = decomp_type_quantifiers env ty in
          let conv tv = Util.Mstr.find tv.tv_name.Ident.id_string tvm in
          let vars = List.map conv vars in
696 697
          let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
          let (bv, vsl), env, b =
698
            decomp_lambdas dep tvm Idmap.empty env ls.ls_args b
699 700 701 702
          in
          begin match ls.ls_value with
            | None ->
                let b = tr_formula dep tvm bv env b in
703
                Decl.make_ls_defn ls vsl b
704 705
            | Some _ ->
                let b = tr_term dep tvm bv env b in
706
                Decl.make_ls_defn ls vsl b
707
          end
708
  in
709
  match dl with
710 711
    | [r, None] ->
        [Decl.create_param_decl (lookup_table global_ls r)], None
712
    | _ ->
713 714 715 716 717 718 719 720
        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)
721

722 723 724 725
and decompose_inductive dep env i =
  let mib, _ = Global.lookup_inductive i in
  (* first, the inductive types *)
  let make_one_ls j _ = (* j-th inductive *)
Andrei Paskevich's avatar
Andrei Paskevich committed
726
    make_one_ls dep env (IndRef (ith_mutual_inductive i j))
727 728 729 730 731 732 733 734 735 736 737 738
  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
      let ty = Global.type_of_global r in
      let (_,vars), env, f = decomp_type_quantifiers env ty in
      let tvm =
        let add v1 v2 tvm =
739
          let v2 = Some (Ty.ty_var v2) in
740 741
          Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
742
        List.fold_right2 add vars (get_poly_arity ls) Idmap.empty
743 744 745 746 747 748
      in
      let f = tr_formula dep tvm Idmap.empty env f in
      let id = preid_of_id (Nametab.basename_of_global r) in
      let pr = Decl.create_prsymbol id in
      pr, f
    in
749 750 751 752
    let cl =
      try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
      with NotFO -> []
    in
753 754
    ls, cl
  in
755 756 757 758 759 760
  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
761 762
  let s = if mib.mind_finite then Decl.Ind else Decl.Coind in
  pl, if dl = [] then None else Some (Decl.create_ind_decl s dl)
763

764 765
(* translation of a Coq term
   assumption: t:T:Set *)
766
and tr_term dep tvm bv env t =
767 768 769
  try
    tr_arith_constant t
  with NotArithConstant -> match kind_of_term t with
770
    (* binary operations on integers *)
771
    | App (c, [|a;b|]) when is_constant c coq_Zplus ->
772
        let ls = why_constant_int dep ["infix +"] in
773
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
774
          Ty.ty_int
775
    | App (c, [|a;b|]) when is_constant c coq_Zminus ->
776
        let ls = why_constant_int dep ["infix -"] in
777
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
778
          Ty.ty_int
779
    | App (c, [|a;b|]) when is_constant c coq_Zmult ->
780
        let ls = why_constant_int dep ["infix *"] in
781
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
782
          Ty.ty_int
783
    | App (c, [|a;b|]) when is_constant c coq_Zdiv ->
784
        let ls = why_constant_eucl dep ["div"] in
785
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
786
          Ty.ty_int
787
    | App (c, [|a|]) when is_constant c coq_Zopp ->
788
        let ls = why_constant_int dep ["prefix -"] in
789
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_int
790
    (* binary operations on reals *)
791
    | App (c, [|a;b|]) when is_constant c coq_Rplus ->
792
        let ls = why_constant_real dep ["infix +"] in
793
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
794
          Ty.ty_real
795
    | App (c, [|a;b|]) when is_constant c coq_Rminus ->
796
        let ls = why_constant_real dep ["infix -"] in
797
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
798
          Ty.ty_real
799
    | App (c, [|a;b|]) when is_constant c coq_Rmult ->
800
        let ls = why_constant_real dep ["infix *"] in
801
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
802
          Ty.ty_real
803
    | App (c, [|a;b|]) when is_constant c coq_Rdiv ->
804
        let ls = why_constant_real dep ["infix /"] in
805
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
806
          Ty.ty_real
807
    | App (c, [|a|]) when is_constant c coq_Ropp ->
808
        let ls = why_constant_real dep ["prefix -"] in
809
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
810
    | App (c, [|a|]) when is_constant c coq_Rinv ->
811
        let ls = why_constant_real dep ["inv"] in
812
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
813
          (* first-order terms *)
814
    | Var id when Idmap.mem id bv ->
815 816 817 818 819
        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
820
    | Case (ci, _, e, br) ->
821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839
        let ty = type_of env Evd.empty e in
        let ty = tr_type dep tvm env ty in
        let e = tr_term dep tvm bv env e in
        let branch j bj =
          let tj = type_of env Evd.empty bj in
          let (_,tvars), _, tj = decomp_type_quantifiers env tj in
          let tyl, _ = decompose_arrows tj in
          let tyl = List.map (tr_type dep tvm env) tyl in
          let tvm, env, bj = decomp_type_lambdas tvm env tvars bj in
          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
          let ls = tr_global_ls dep env (ConstructRef cj) in
          if List.length vars <> List.length ls.ls_args then raise NotFO;
          let pat = pat_app ls (List.map pat_var vars) ty in
          t_close_branch pat (tr_term dep tvm bv env bj)
        in
        let ty = type_of env Evd.empty t in
        let _ty = tr_type dep tvm env ty in
        t_case e (Array.to_list (Array.mapi branch br))
840
    | LetIn (x, e1, ty1, e2) ->
841