why3tac.ml4 49.5 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 102 103 104 105

let map_to_list = CArray.map_to_list

let force x = x

DECLARE PLUGIN "why3tac"

END

106
module Why3tac = struct
107

108
open Why3
109
open Call_provers
110
open Whyconf
111 112
open Ty
open Term
113

114 115 116 117 118 119 120 121 122 123
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 _ -> ()

124
let debug =
125
  try let _ = Sys.getenv "WHY3DEBUG" in true
126 127
  with Not_found -> false

128 129 130 131 132 133
let config =
  try
    Whyconf.read_config None
  with Whyconf.ConfigFailure(file, msg) ->
    error (file ^ ": " ^ msg)

134
let main = Whyconf.get_main config
135

136
let timelimit = timelimit main
137

138
let env = Env.create_env (loadpath main)
139

140 141
let provers = Hashtbl.create 17

142 143 144 145
let get_prover s =
  try
    Hashtbl.find provers s
  with Not_found ->
146 147 148 149 150 151 152 153 154 155 156
    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
157
    let drv = Driver.load_driver env cp.driver cp.extra_drivers in
158 159 160
    Hashtbl.add provers s (cp, drv);
    cp, drv

161
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
162
let print_tvm fmt m =
163 164 165
  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@ "
166
                 (string_of_id id) Why3.Pretty.print_tv tv) m
167
let print_bv fmt m =
168 169 170
  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@ "
171
                 (string_of_id id) Why3.Pretty.print_vsty vs) m
172

173
(* Coq constants *)
174 175 176 177 178 179 180 181 182 183 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

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

220
let coq_WhyType =
221
  find_reference "Why3" ["Why3"; "BuiltIn"] "WhyType"
222 223

let rec is_WhyType c = match kind_of_term c with
224
  | App (f, [|_|]) -> is_global coq_WhyType f
225 226 227
  | Cast (c, _, _) -> is_WhyType c
  | _ -> false

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

230 231 232 233 234 235
(* 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 *)
236
(*
237 238 239 240 241 242 243 244
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)
245
*)
246

247
let coq_rename_var env na t =
248 249 250 251 252 253
  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)

254
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
255
   identifiers n1...nk with the same path as c, if they exist; otherwise
256
   raises NotFO *)
257 258
let rec_names_for c =
  let mp,dp,_ = Names.repr_con c in
259
  map_to_list
260 261
    (function
       | Name id ->
262
           let c' = Names.make_con mp dp (label_of_id id) in
263 264
           ignore
             (try Global.lookup_constant c' with Not_found -> raise NotFO);
265
           c'
266
       | Anonymous ->
267
           raise NotFO)
268

269 270 271
(* 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 =
272 273 274 275 276
  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
277
    | Prod (n, a, t) when is_Set a || is_Type a ->
278 279 280 281 282 283 284 285
        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
286
    | _ ->
287
        (tvm, List.rev vars), env, t
288
  in
289
  loop env Idmap.empty [] t
290

291 292
(* 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
293
let decomp_type_lambdas tvm env vars t =
294
  let rec loop tvm env vars t = match vars, kind_of_term t with
295 296 297 298
    | 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
299
    | tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
300
        let id, env = coq_rename_var env n a in
301
        let t = subst1 (mkVar id) t in
302
        let tvm = Idmap.add id (Some (Ty.ty_var tv)) tvm in
303
        loop tvm env vars t
304 305
    | [], _ ->
        tvm, env, t
306
    | _ ->
307
        raise NotFO (*TODO: eta-expansion*)
308
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
309
  loop tvm env vars t
310

311 312 313 314 315 316 317 318
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 []

319 320 321 322
let is_fo_kind ty =
  let _, ty = decompose_arrows ty in
  is_Set ty || is_Type ty

323
let decomp_lambdas _dep _tvm bv env vars t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
  let rec loop bv vsl env vars t = match vars, kind_of_term t with
325
    | [], _ ->
326
        (bv, List.rev vsl), env, t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
327
    | ty :: vars, Lambda (n, a, t) ->
328
        let id, env = coq_rename_var env n a in
329 330
        let t = subst1 (mkVar id) t in
        let vs = create_vsymbol (preid_of_id id) ty in
331
        let bv = Idmap.add id (Some vs) bv in
332
        loop bv (vs :: vsl) env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
    | _ ->
334
        raise NotFO (*TODO: eta-expansion*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335
  in
336
  loop bv [] env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337

338
let rec skip_k_args k cl = match k, cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
339 340
  | [], _ -> cl
  | _ :: k, _ :: cl -> skip_k_args k cl
341 342
  | _, [] -> raise NotFO

343 344
(* Coq globals *)

345
(* Coq reference -> symbol *)
346
let global_ts = ref Refmap.empty
347 348
let global_ls = ref Refmap.empty

349 350
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
351
let add_poly_arity ls n = poly_arity := Mls.add ls n !poly_arity
352 353
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity

354 355
(* ident -> decl *)
let global_decl = ref Ident.Mid.empty
356

357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
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 *)
374 375
let global_dep = ref Decl.Mdecl.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
376 377 378 379 380 381 382 383
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

384 385 386 387 388 389 390 391 392 393
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

394 395 396
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")
397 398

let why_constant_int dep s =
399
  task := Task.use_export !task (Lazy.force th_int);
400
  dep := { !dep with dep_use_int = true };
401
  Theory.ns_find_ls (Lazy.force th_int).Theory.th_export s
402 403

let why_constant_eucl dep s =
404
  task := Task.use_export !task (Lazy.force th_eucl);
405
  dep := { !dep with dep_use_eucl = true };
406
  Theory.ns_find_ls (Lazy.force th_eucl).Theory.th_export s
407 408

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

let rec add_local_decls d =
414 415
  let id = Ident.Sid.choose d.Decl.d_news in
  if not (Ident.Mid.mem id (Task.task_known !task)) then begin
416
    assert (Decl.Mdecl.mem d !global_dep);
417
    let dep = Decl.Mdecl.find d !global_dep in
418
    Decl.Sdecl.iter add_local_decls dep.dep_decls;
419 420 421
    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);
422 423 424
    try
      task := Task.add_decl !task d
    with Decl.UnknownIdent id ->
425 426 427 428
      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
429 430
  end

431 432
(* synchronization *)
let () =
433 434 435 436 437 438 439 440 441 442 443 444
  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)
445

446
let lookup_table table r = match Refmap.find r !table with
447 448 449
  | None -> raise NotFO
  | Some d -> d

450
let add_table table r v = table := Refmap.add r v !table
451

452 453 454 455 456 457 458 459 460
(* 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
461
  | Construct _ when is_global coq_xH p ->
462
      Big_int.unit_big_int
463
  | App (f, [|a|]) when is_global coq_xI f ->
464
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
465
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
466
  | App (f, [|a|]) when is_global coq_xO f ->
467
      (* Mult (Cst 2, tr_positive a) *)
468 469 470 471 472 473
      Big_int.mult_big_int big_two (tr_positive a)
  | Cast (p, _, _) ->
      tr_positive p
  | _ ->
      raise NotArithConstant

Andrei Paskevich's avatar
Andrei Paskevich committed
474 475
let const_of_big_int b =
  Term.t_const
476
    (Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
477

478
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
479
let rec tr_arith_constant dep t = match kind_of_term t with
480 481
  | Construct _ when is_global coq_Z0 t -> Term.t_nat_const 0
  | App (f, [|a|]) when is_global coq_Zpos f ->
482
      const_of_big_int (tr_positive a)
483
  | App (f, [|a|]) when is_global coq_Zneg f ->
484 485 486
      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
487
  | Const _ when is_global coq_R0 t ->
488
      Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
489
  | Const _ when is_global coq_R1 t ->
490
      Term.t_const (Number.ConstReal (Number.real_const_dec "1" "0" None))
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507
(*   | 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, _, _) ->
508
      tr_arith_constant dep t
509 510 511
  | _ ->
      raise NotArithConstant

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

544
(* the type symbol for r *)
MARCHE Claude's avatar
MARCHE Claude committed
545 546
and tr_task_ts dep env evd r =
  let ts = tr_global_ts dep env evd r in
547 548 549 550
  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;
551
  ts
552 553

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

696
(* the function/predicate symbol for r *)
MARCHE Claude's avatar
MARCHE Claude committed
697 698
and tr_task_ls dep env evd r =
  let ls = tr_global_ls dep env evd r in
699 700 701 702
  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;
703
  ls
704

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

MARCHE Claude's avatar
MARCHE Claude committed
748
and make_one_ls dep env evd r =
749
  let ty = type_of_global r in
750 751 752
  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
753
  let args = List.map (tr_type dep tvm env evd) l in
754 755 756 757 758 759
  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
760
      let evd,s = type_of env evd t in
761 762
      if is_Set s || is_Type s then
          (* function definition *)
MARCHE Claude's avatar
MARCHE Claude committed
763
        let ty = tr_type dep tvm env evd t in
764 765 766 767 768
        create_lsymbol id args (Some ty)
      else
        raise NotFO
  in
  add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
769
  add_poly_arity ls vars
770

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

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

882 883
(* translation of a Coq term
   assumption: t:T:Set *)
MARCHE Claude's avatar
MARCHE Claude committed
884
and tr_term dep tvm bv env evd t =
885
  try
886
    tr_arith_constant dep t
887
  with NotArithConstant -> match kind_of_term t with
888
    (* binary operations on integers *)
889
    | App (c, [|a;b|]) when is_global coq_Zplus c ->
890
        let ls = why_constant_int dep ["infix +"] in
MARCHE Claude's avatar
MARCHE Claude committed
891
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
892
          Ty.ty_int
893
    | App (c, [|a;b|]) when is_global coq_Zminus c ->
894
        let ls = why_constant_int dep ["infix -"] in
MARCHE Claude's avatar
MARCHE Claude committed
895
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
896
          Ty.ty_int
897
    | App (c, [|a;b|]) when is_global coq_Zmult c ->
898
        let ls = why_constant_int dep ["infix *"] in
MARCHE Claude's avatar
MARCHE Claude committed
899
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
900
          Ty.ty_int
901
    | App (c, [|a;b|]) when is_global coq_Zdiv c ->
902
        let ls = why_constant_eucl dep ["div"] in
MARCHE Claude's avatar
MARCHE Claude committed
903
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
904
          Ty.ty_int
905
    | App (c, [|a|]) when is_global coq_Zopp c ->
906
        let ls = why_constant_int dep ["prefix -"] in
MARCHE Claude's avatar
MARCHE Claude committed
907
        Term.fs_app ls [tr_term dep tvm bv env evd a] Ty.ty_int
908
    (* binary operations on reals *)
909
    | App (c, [|a;b|]) when is_global coq_Rplus c ->
910
        let ls = why_constant_real dep ["infix +"] in
MARCHE Claude's avatar
MARCHE Claude committed
911
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
912
          Ty.ty_real
913
    | App (c, [|a;b|]) when is_global coq_Rminus c ->
914
        let ls = why_constant_real dep ["infix -"] in
MARCHE Claude's avatar
MARCHE Claude committed
915
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
916
          Ty.ty_real
917
    | App (c, [|a;b|]) when is_global coq_Rmult c ->
918
        let ls = why_constant_real dep ["infix *"] in
MARCHE Claude's avatar
MARCHE Claude committed
919
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
920
          Ty.ty_real
921
    | App (c, [|a;b|]) when is_global coq_Rdiv c ->
922
        let ls = why_constant_real dep ["infix /"] in
MARCHE Claude's avatar
MARCHE Claude committed
923
        Term.fs_app ls [tr_term dep tvm bv env evd a; tr_term dep tvm bv env evd b]
924
          Ty.ty_real
925
    | App (c, [|a|]) when is_global coq_Ropp c ->
926
        let ls = why_constant_real dep ["prefix -"] in
MARCHE Claude's avatar
MARCHE Claude committed
927
        Term.fs_app ls [tr_term dep tvm bv env evd a] Ty.ty_real