why3tac.ml 47 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Names
13
open Namegen
14
15
16
17
18
19
20
open Term
open Termops
open Tacmach
open Util
open Coqlib
open Hipattern
open Typing
21
22
open Libnames
open Declarations
23
open Pp
24

25
open Why3
26
open Call_provers
27
open Whyconf
28
29
open Ty
open Term
30

31
let debug =
32
  try let _ = Sys.getenv "WHY3DEBUG" in true
33
34
  with Not_found -> false

35
36
37
38
39
40
let config =
  try
    Whyconf.read_config None
  with Whyconf.ConfigFailure(file, msg) ->
    error (file ^ ": " ^ msg)

41
let main = Whyconf.get_main config
42

43
let timelimit = timelimit main
44

45
let env = Env.create_env (loadpath main)
46

47
48
let provers = Hashtbl.create 17

49
50
51
52
let get_prover s =
  try
    Hashtbl.find provers s
  with Not_found ->
53
54
55
56
57
58
59
60
61
62
63
    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
64
    let drv = Driver.load_driver env cp.driver cp.extra_drivers in
65
66
67
    Hashtbl.add provers s (cp, drv);
    cp, drv

68
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
69
let print_tvm fmt m =
70
71
72
  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@ "
73
                 (string_of_id id) Why3.Pretty.print_tv tv) m
74
let print_bv fmt m =
75
76
77
  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@ "
78
                 (string_of_id id) Why3.Pretty.print_vsty vs) m
79

80
81
82
83
84
85
86
87
88
89
90
91
92
(* 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"]]

93
let constant = gen_constant_in_modules "why" coq_modules
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

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")
123
let coq_Rinv = lazy (constant "Rinv")
124
125
126
127
128
129
let coq_Rminus = lazy (constant "Rminus")
let coq_Rdiv = lazy (constant "Rdiv")
let coq_powerRZ = lazy (constant "powerRZ")

let coq_iff = lazy (constant "iff")

130
131
let is_constant t c = try t = Lazy.force c with _ -> false

132
133
134
135
136
137
138
139
140
141
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)

142
143
144
145
146
147
(* 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 *)
148
(*
149
150
151
152
153
154
155
156
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)
157
*)
158

159
let coq_rename_var env na t =
160
161
162
163
164
165
  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)

166
(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
167
   identifiers n1...nk with the same path as c, if they exist; otherwise
168
   raises NotFO *)
169
170
171
let rec_names_for c =
  let mp,dp,_ = Names.repr_con c in
  array_map_to_list
172
173
    (function
       | Name id ->
174
           let c' = Names.make_con mp dp (label_of_id id) in
175
176
           ignore
             (try Global.lookup_constant c' with Not_found -> raise NotFO);
177
           c'
178
       | Anonymous ->
179
           raise NotFO)
180

181
182
183
(* extract the prenex type quantifications i.e.
   type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
let decomp_type_quantifiers env t =
184
185
186
187
188
  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
189
    | Prod (n, a, t) when is_Set a || is_Type a ->
190
191
192
193
194
195
196
197
        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
198
    | _ ->
199
        (tvm, List.rev vars), env, t
200
  in
201
  loop env Idmap.empty [] t
202

203
204
(* 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
205
let decomp_type_lambdas tvm env vars t =
206
  let rec loop tvm env vars t = match vars, kind_of_term t with
207
208
209
210
    | 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
211
    | tv :: vars, Lambda (n, a, t) when is_Set a || is_Type a ->
212
        let id, env = coq_rename_var env n a in
213
        let t = subst1 (mkVar id) t in
214
        let tvm = Idmap.add id (Some (Ty.ty_var tv)) tvm in
215
        loop tvm env vars t
216
217
    | [], _ ->
        tvm, env, t
218
    | _ ->
219
        raise NotFO (*TODO: eta-expansion*)
220
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221
  loop tvm env vars t
222

223
224
225
226
227
228
229
230
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 []

231
232
233
234
let is_fo_kind ty =
  let _, ty = decompose_arrows ty in
  is_Set ty || is_Type ty

235
let decomp_lambdas _dep _tvm bv env vars t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
236
  let rec loop bv vsl env vars t = match vars, kind_of_term t with
237
    | [], _ ->
238
        (bv, List.rev vsl), env, t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239
    | ty :: vars, Lambda (n, a, t) ->
240
        let id, env = coq_rename_var env n a in
241
242
        let t = subst1 (mkVar id) t in
        let vs = create_vsymbol (preid_of_id id) ty in
243
        let bv = Idmap.add id (Some vs) bv in
244
        loop bv (vs :: vsl) env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245
    | _ ->
246
        raise NotFO (*TODO: eta-expansion*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247
  in
248
  loop bv [] env vars t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249

250
let rec skip_k_args k cl = match k, cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
251
252
  | [], _ -> cl
  | _ :: k, _ :: cl -> skip_k_args k cl
253
254
  | _, [] -> raise NotFO

255
256
(* Coq globals *)

257
(* Coq reference -> symbol *)
258
let global_ts = ref Refmap.empty
259
260
let global_ls = ref Refmap.empty

261
262
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
263
let add_poly_arity ls n = poly_arity := Mls.add ls n !poly_arity
264
265
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity

266
267
(* ident -> decl *)
let global_decl = ref Ident.Mid.empty
268

269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
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 *)
286
287
let global_dep = ref Decl.Mdecl.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
288
289
290
291
292
293
294
295
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

296
297
298
299
300
301
302
303
304
305
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

306
307
308
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")
309
310

let why_constant_int dep s =
311
  task := Task.use_export !task (Lazy.force th_int);
312
  dep := { !dep with dep_use_int = true };
313
  Theory.ns_find_ls (Lazy.force th_int).Theory.th_export s
314
315

let why_constant_eucl dep s =
316
  task := Task.use_export !task (Lazy.force th_eucl);
317
  dep := { !dep with dep_use_eucl = true };
318
  Theory.ns_find_ls (Lazy.force th_eucl).Theory.th_export s
319
320

let why_constant_real dep s =
321
  task := Task.use_export !task (Lazy.force th_real);
322
  dep := { !dep with dep_use_real = true };
323
  Theory.ns_find_ls (Lazy.force th_real).Theory.th_export s
324
325

let rec add_local_decls d =
326
327
  let id = Ident.Sid.choose d.Decl.d_news in
  if not (Ident.Mid.mem id (Task.task_known !task)) then begin
328
    assert (Decl.Mdecl.mem d !global_dep);
329
    let dep = Decl.Mdecl.find d !global_dep in
330
    Decl.Sdecl.iter add_local_decls dep.dep_decls;
331
332
333
    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);
334
335
336
    try
      task := Task.add_decl !task d
    with Decl.UnknownIdent id ->
337
338
339
340
      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
341
342
  end

343
344
345
(* synchronization *)
let () =
  Summary.declare_summary "Why globals"
346
    { Summary.freeze_function =
347
348
        (fun () ->
           !global_ts, !global_ls, !poly_arity, !global_decl, !global_dep);
349
      Summary.unfreeze_function =
350
351
352
        (fun (ts,ls,pa,gdecl,gdep) ->
           global_ts := ts; global_ls := ls; poly_arity := pa;
           global_decl := gdecl; global_dep := gdep);
353
      Summary.init_function =
354
355
356
357
358
359
        (fun () ->
           global_ts := Refmap.empty;
           global_ls := Refmap.empty;
           poly_arity := Mls.empty;
           global_decl := Ident.Mid.empty;
           global_dep := Decl.Mdecl.empty);
360
361
      (* Summary.survive_module = true; *)
      (* Summary.survive_section = true; *)
362
    }
363

364
let lookup_table table r = match Refmap.find r !table with
365
366
367
  | None -> raise NotFO
  | Some d -> d

368
let add_table table r v = table := Refmap.add r v !table
369

370
371
372
373
374
375
376
377
378
(* 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
379
  | Construct _ when is_constant p coq_xH ->
380
      Big_int.unit_big_int
381
  | App (f, [|a|]) when is_constant f coq_xI ->
382
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
383
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
384
  | App (f, [|a|]) when is_constant f coq_xO ->
385
      (* Mult (Cst 2, tr_positive a) *)
386
387
388
389
390
391
      Big_int.mult_big_int big_two (tr_positive a)
  | Cast (p, _, _) ->
      tr_positive p
  | _ ->
      raise NotArithConstant

Andrei Paskevich's avatar
Andrei Paskevich committed
392
393
let const_of_big_int b =
  Term.t_const
394
    (Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
395

396
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
397
let rec tr_arith_constant dep t = match kind_of_term t with
398
  | Construct _ when is_constant t coq_Z0 -> Term.t_nat_const 0
399
  | App (f, [|a|]) when is_constant f coq_Zpos ->
400
      const_of_big_int (tr_positive a)
401
  | App (f, [|a|]) when is_constant f coq_Zneg ->
402
403
404
      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
405
  | Const _ when is_constant t coq_R0 ->
406
      Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
407
  | Const _ when is_constant t coq_R1 ->
408
      Term.t_const (Number.ConstReal (Number.real_const_dec "1" "0" None))
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
(*   | 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, _, _) ->
426
      tr_arith_constant dep t
427
428
429
  | _ ->
      raise NotArithConstant

430
let body_of_constant c =
431
432
433
434
  if Reductionops.is_transparent (ConstKey c) then
    CoqCompat.body_of_constant (Global.lookup_constant c)
  else None

435
let rec tr_type dep tvm env t =
436
437
438
439
  let t = Reductionops.clos_norm_flags
      (Closure.RedFlags.red_add_transparent
	 Closure.betadeltaiota (Conv_oracle.get_transp_state()))
      env Evd.empty t in
440
  if is_constant t coq_Z then
441
    Ty.ty_int
442
  else if is_constant t coq_R then
443
444
    Ty.ty_real
  else match kind_of_term t with
445
    | Var x when Idmap.mem x tvm ->
446
447
448
449
        begin match Idmap.find x tvm with
          | None -> raise NotFO
          | Some ty -> ty
        end
450
    | _ ->
451
452
453
454
        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
455
          let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
456
457
          assert (List.length ts.Ty.ts_args = List.length cl);
          (* since t:Set *)
458
459
460
461
462
463
464
465
          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
466

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

(* the type declaration for r *)
477
and tr_global_ts dep env r =
478
  try
479
480
481
482
483
    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
484
485
  with Not_found ->
    add_table global_ts r None;
486
    let dep' = empty_dep () in
487
    match r with
488
      | VarRef id ->
489
          let ty = try Global.type_of_global r with Not_found -> raise NotFO in
490
491
492
493
494
495
          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
496
          add_new_decl dep !dep' decl;
497
          ts
498
      | ConstructRef _ ->
499
          assert false
500
      | ConstRef c ->
501
502
503
          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;
504
          let id = preid_of_id (Nametab.basename_of_global r) in
505
          let ts = match body_of_constant c with
506
507
508
509
510
511
512
513
514
            | 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
515
          let decl = Decl.create_ty_decl ts in
516
          add_table global_ts r (Some ts);
Andrei Paskevich's avatar
Andrei Paskevich committed
517
          add_new_decl dep !dep' decl;
518
          ts
519
      | IndRef i ->
520
521
522
523
524
525
526
          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;
527
            let id = preid_of_id (Nametab.basename_of_global r) in
528
529
530
531
532
533
534
535
536
            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
537
538
            let opaque = Ty.Stv.of_list ts.Ty.ts_args in
            let constr = Array.length oib.mind_nf_lc in
539
540
541
542
            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
543
544
545
546
              let l, c = decompose_arrows t in
              let tvm = match kind_of_term c with
                | App (_, v) ->
                    let v = Array.to_list v in
547
548
                    let no_whytype c = not (has_WhyType env c) in
                    let v = List.filter no_whytype v in
549
550
551
552
553
554
555
556
                    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
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
                | 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
573
574
              in
              let l = List.map (tr_type dep' tvm env) l in
575
              let id = preid_of_id (Nametab.basename_of_global r) in
576
              let ls = Term.create_fsymbol ~opaque ~constr id l tyj in
577
              add_table global_ls r (Some ls);
Andrei Paskevich's avatar
Andrei Paskevich committed
578
              add_poly_arity ls vars;
579
              ls, List.map (fun _ -> None) ls.ls_args
580
            in
Andrei Paskevich's avatar
Andrei Paskevich committed
581
582
583
584
            let cl =
              try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
              with NotFO -> []
            in
585
            (j, oib), (ts, cl)
Andrei Paskevich's avatar
Andrei Paskevich committed
586
587
588
          in
          let dl = Array.mapi make_one mib.mind_packets in
          let dl = Array.to_list dl in
589
590
591
592
593
594
595
596
597
598
599
          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
                  make_one_ls dep' env r;
                  let ls = lookup_table global_ls r in
                  let d = Decl.create_param_decl ls in
                  sl := d :: !sl
                with NotFO ->
600
                  ()
601
602
603
604
              done;
              Decl.create_ty_decl ts :: tl, dl, !sl
            end else
              tl, d :: dl, sl
Andrei Paskevich's avatar
Andrei Paskevich committed
605
          in
606
          let tl, dl, sl = List.fold_right add dl ([], [], []) in
Andrei Paskevich's avatar
Andrei Paskevich committed
607
608
          let decl =
            if dl = [] then None else Some (Decl.create_data_decl dl)
609
610
          in
          (* Format.printf "decl = %a@." Pretty.print_decl decl; *)
Andrei Paskevich's avatar
Andrei Paskevich committed
611
612
          List.iter (add_new_decl dep !dep') tl;
          List.iter (add_dep dep') tl;
613
          Opt.iter (add_new_decl dep !dep') decl;
614
615
          Opt.iter (add_dep dep') decl;
          List.iter (add_new_decl dep !dep') sl;
616
          lookup_table global_ts r
617

618
(* the function/predicate symbol for r *)
619
and tr_task_ls dep env r =
620
  let ls = tr_global_ls dep env r in
621
622
623
624
  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;
625
  ls
626

627
(* the function/predicate symbol declaration for r *)
628
and tr_global_ls dep env r =
629
  try
630
631
632
633
634
    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
635
636
  with Not_found ->
    add_table global_ls r None;
637
    let dep' = empty_dep () in
638
639
    (* 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
640
    let (tvm, _), env, t = decomp_type_quantifiers env ty in
641
    if is_Set t || is_Type t then raise NotFO;
642
    let _, t = decompose_arrows t in
643
644
    match r with
      | ConstructRef _ ->
645
          assert (not (is_Prop t)); (* is a proof *)
646
647
648
649
          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
650
      | ConstRef c ->
651
          let pl, d = decompose_definition dep' env c in
Andrei Paskevich's avatar
Andrei Paskevich committed
652
          List.iter (add_new_decl dep !dep') pl;
653
          List.iter (add_dep dep') pl;
654
          Opt.iter (add_new_decl dep !dep') d;
655
          lookup_table global_ls r
656
657
      | IndRef i ->
          assert (is_Prop t);
658
          let pl, d = decompose_inductive dep' env i in
Andrei Paskevich's avatar
Andrei Paskevich committed
659
          List.iter (add_new_decl dep !dep') pl;
660
          List.iter (add_dep dep') pl;
661
          Opt.iter (add_new_decl dep !dep') d;
662
663
664
665
666
          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
667
          add_new_decl dep !dep' decl;
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
          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
691
  add_poly_arity ls vars
692

693
and decompose_definition dep env c =
694
  let dl = match body_of_constant c with
695
    | None ->
696
        [ConstRef c, None]
697
    | Some b ->
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
        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
720
  in
721
  List.iter (fun (r, _) -> make_one_ls dep env r) dl;
722
  let make_one_decl (r, b) =
723
724
725
    let ls = lookup_table global_ls r in
    match b with
      | None ->
726
          assert false
727
      | Some b ->
728
729
          let tvs = List.fold_left Ty.ty_freevars Stv.empty
            (Ty.oty_cons ls.ls_args ls.ls_value) in
730
731
          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
732
          let ty = Global.type_of_global r in
733
          let (_, vars), env, _ = decomp_type_quantifiers env ty in
734
          let conv tv = Stdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
735
          let vars = List.map conv vars in
736
737
          let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
          let (bv, vsl), env, b =
738
            decomp_lambdas dep tvm Idmap.empty env ls.ls_args b
739
740
741
742
          in
          begin match ls.ls_value with
            | None ->
                let b = tr_formula dep tvm bv env b in
743
                Decl.make_ls_defn ls vsl b
744
745
            | Some _ ->
                let b = tr_term dep tvm bv env b in
746
                Decl.make_ls_defn ls vsl b
747
          end
748
  in
749
  match dl with
750
751
    | [r, None] ->
        [Decl.create_param_decl (lookup_table global_ls r)], None
752
    | _ ->
753
754
755
756
757
758
759
760
        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)
761

762
763
764
765
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
766
    make_one_ls dep env (IndRef (ith_mutual_inductive i j))
767
768
769
770
771
772
773
774
775
776
777
778
  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 =
779
          let v2 = Some (Ty.ty_var v2) in
780
781
          Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
782
        List.fold_right2 add vars (get_poly_arity ls) Idmap.empty
783
784
785
786
787
788
      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
789
790
791
792
    let cl =
      try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
      with NotFO -> []
    in
793
794
    ls, cl
  in
795
796
797
798
799
800
  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
801
802
  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)
803

804
805
(* translation of a Coq term
   assumption: t:T:Set *)
806
and tr_term dep tvm bv env t =
807
  try
808
    tr_arith_constant dep t
809
  with NotArithConstant -> match kind_of_term t with
810
    (* binary operations on integers *)
811
    | App (c, [|a;b|]) when is_constant c coq_Zplus ->
812
        let ls = why_constant_int dep ["infix +"] in
813
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
814
          Ty.ty_int
815
    | App (c, [|a;b|]) when is_constant c coq_Zminus ->
816
        let ls = why_constant_int dep ["infix -"] in
817
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
818
          Ty.ty_int
819
    | App (c, [|a;b|]) when is_constant c coq_Zmult ->
820
        let ls = why_constant_int dep ["infix *"] in
821
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
822
          Ty.ty_int
823
    | App (c, [|a;b|]) when is_constant c coq_Zdiv ->
824
        let ls = why_constant_eucl dep ["div"] in
825
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
826
          Ty.ty_int
827
    | App (c, [|a|]) when is_constant c coq_Zopp ->
828
        let ls = why_constant_int dep ["prefix -"] in
829
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_int
830
    (* binary operations on reals *)
831
    | App (c, [|a;b|]) when is_constant c coq_Rplus ->
832
        let ls = why_constant_real dep ["infix +"] in
833
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
834
          Ty.ty_real
835
    | App (c, [|a;b|]) when is_constant c coq_Rminus ->
836
        let ls = why_constant_real dep ["infix -"] in
837
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
838
          Ty.ty_real
839
    | App (c, [|a;b|]) when is_constant c coq_Rmult ->
840
        let ls = why_constant_real dep ["infix *"] in
841
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
842
          Ty.ty_real
843
    | App (c, [|a;b|]) when is_constant c coq_Rdiv ->
844
        let ls = why_constant_real dep ["infix /"] in
845
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
846
          Ty.ty_real
847
    | App (c, [|a|]) when is_constant c coq_Ropp ->
848
        let ls = why_constant_real dep ["prefix -"] in
849
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
850
    | App (c, [|a|]) when is_constant c coq_Rinv ->
851
        let ls = why_constant_real dep ["inv"] in
852
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
853
          (* first-order terms *)
854
    | Var id when Idmap.mem id bv ->
855
856
857
858
859
        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
860
    | Case (ci, _, e, br) ->
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
        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))
880
    | LetIn (x, e1, ty1, e2) ->
881
        if is_Prop ty1 || is_fo_kind ty1 then
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
          let e2 = subst1 e1 e2 in
          tr_term dep tvm bv env e2
        else begin
          let s1 = type_of env Evd.empty ty1 in
          if not (is_Set s1 || is_Type s1) then raise NotFO;
          let t1 = tr_term dep tvm bv env e1 in
          let vs, _, bv, env, e2 = quantifiers x ty1 e2 dep tvm bv env in
          let t2 = tr_term dep tvm bv env e2 in
          t_let_close vs t1 t2
        end
    | CoFix _ | Fix _ | Lambda _ | Prod _ | Sort _ | Evar _ | Meta _ ->
        raise NotFO
    | Rel _ ->
        assert false
    | Cast (t, _, _) ->
        tr_term dep tvm bv env t
898
    | Var _ | App _ | Construct _ | Ind _ | Const _ ->
899
        let f, cl = decompose_app t in
900
901
902
903
904
        (* 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;
905
        let r = try global_of_constr f with _ -> raise NotFO in
906
907
908
        let ls = tr_task_ls dep env r in
        begin match ls.Term.ls_value with
          | Some _ ->
909
              let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
910
911
912
913
              let k = get_poly_arity ls in
              let cl = skip_k_args k cl in
              let ty = type_of env Evd.empty t in
              let ty = tr_type dep tvm env ty in
914
              Term.fs_app ls (List.map (tr_term dep tvm bv env) cl) ty
915
916
917
          | None  ->
              raise NotFO
        end
918
        (* TODO: we could abstract some part of (f cl) when not FO *)
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
(*               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 *)
934

935
and quantifiers n a b dep tvm bv env =
936
  let id, env = coq_rename_var env n a in
937
  let b = subst1 (mkVar id) b in
938
  let t = tr_type dep tvm env a in
939
  let vs = Term.create_vsymbol (preid_of_id id) t in
940
  let bv = Idmap.add id (Some vs) bv in