why3tac.ml4 48.8 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 20
open Term
open Termops
open Tacmach
open Util
open Coqlib
open Hipattern
open Typing
21
open Declarations
22
open Pp
23

24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
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

let finite_ind v = v

let admit_as_an_axiom = Tactics.admit_as_an_axiom

let map_to_list = Util.array_map_to_list

50 51 52 53 54 55 56 57
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

58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
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

let finite_ind v = v <> Decl_kinds.CoFinite

let pr_str = Pp.str

let pr_spc = Pp.spc

let pr_fnl = Pp.fnl

let admit_as_an_axiom = Proofview.V82.of_tactic Tactics.admit_as_an_axiom

let map_to_list = CArray.map_to_list

let force x = x

DECLARE PLUGIN "why3tac"

END

99
module Why3tac = struct
100

101
open Why3
102
open Call_provers
103
open Whyconf
104 105
open Ty
open Term
106

107 108 109 110 111 112 113 114 115 116
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 _ -> ()

117
let debug =
118
  try let _ = Sys.getenv "WHY3DEBUG" in true
119 120
  with Not_found -> false

121 122 123 124 125 126
let config =
  try
    Whyconf.read_config None
  with Whyconf.ConfigFailure(file, msg) ->
    error (file ^ ": " ^ msg)

127
let main = Whyconf.get_main config
128

129
let timelimit = timelimit main
130

131
let env = Env.create_env (loadpath main)
132

133 134
let provers = Hashtbl.create 17

135 136 137 138
let get_prover s =
  try
    Hashtbl.find provers s
  with Not_found ->
139 140 141 142 143 144 145 146 147 148 149
    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
150
    let drv = Driver.load_driver env cp.driver cp.extra_drivers in
151 152 153
    Hashtbl.add provers s (cp, drv);
    cp, drv

154
let print_constr fmt c = pp_with fmt (Termops.print_constr c)
155
let print_tvm fmt m =
156 157 158
  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@ "
159
                 (string_of_id id) Why3.Pretty.print_tv tv) m
160
let print_bv fmt m =
161 162 163
  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@ "
164
                 (string_of_id id) Why3.Pretty.print_vsty vs) m
165

166
(* Coq constants *)
167 168 169 170 171 172 173 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

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

213
let coq_WhyType =
214
  find_reference "Why3" ["Why3"; "BuiltIn"] "WhyType"
215 216

let rec is_WhyType c = match kind_of_term c with
217
  | App (f, [|_|]) -> is_global coq_WhyType f
218 219 220 221 222
  | Cast (c, _, _) -> is_WhyType c
  | _ -> false

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

223 224 225 226 227 228
(* 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 *)
229
(*
230 231 232 233 234 235 236 237
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)
238
*)
239

240
let coq_rename_var env na t =
241 242 243 244 245 246
  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)

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

262 263 264
(* 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 =
265 266 267 268 269
  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
270
    | Prod (n, a, t) when is_Set a || is_Type a ->
271 272 273 274 275 276 277 278
        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
279
    | _ ->
280
        (tvm, List.rev vars), env, t
281
  in
282
  loop env Idmap.empty [] t
283

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

304 305 306 307 308 309 310 311
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 []

312 313 314 315
let is_fo_kind ty =
  let _, ty = decompose_arrows ty in
  is_Set ty || is_Type ty

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

331
let rec skip_k_args k cl = match k, cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
332 333
  | [], _ -> cl
  | _ :: k, _ :: cl -> skip_k_args k cl
334 335
  | _, [] -> raise NotFO

336 337
(* Coq globals *)

338
(* Coq reference -> symbol *)
339
let global_ts = ref Refmap.empty
340 341
let global_ls = ref Refmap.empty

342 343
(* polymorphic arity (i.e. number of type variables) *)
let poly_arity = ref Mls.empty
344
let add_poly_arity ls n = poly_arity := Mls.add ls n !poly_arity
345 346
let get_poly_arity ls = assert (Mls.mem ls !poly_arity); Mls.find ls !poly_arity

347 348
(* ident -> decl *)
let global_decl = ref Ident.Mid.empty
349

350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
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 *)
367 368
let global_dep = ref Decl.Mdecl.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
369 370 371 372 373 374 375 376
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

377 378 379 380 381 382 383 384 385 386
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

387 388 389
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")
390 391

let why_constant_int dep s =
392
  task := Task.use_export !task (Lazy.force th_int);
393
  dep := { !dep with dep_use_int = true };
394
  Theory.ns_find_ls (Lazy.force th_int).Theory.th_export s
395 396

let why_constant_eucl dep s =
397
  task := Task.use_export !task (Lazy.force th_eucl);
398
  dep := { !dep with dep_use_eucl = true };
399
  Theory.ns_find_ls (Lazy.force th_eucl).Theory.th_export s
400 401

let why_constant_real dep s =
402
  task := Task.use_export !task (Lazy.force th_real);
403
  dep := { !dep with dep_use_real = true };
404
  Theory.ns_find_ls (Lazy.force th_real).Theory.th_export s
405 406

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

424 425
(* synchronization *)
let () =
426 427 428 429 430 431 432 433 434 435 436 437
  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)
438

439
let lookup_table table r = match Refmap.find r !table with
440 441 442
  | None -> raise NotFO
  | Some d -> d

443
let add_table table r v = table := Refmap.add r v !table
444

445 446 447 448 449 450 451 452 453
(* 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
454
  | Construct _ when is_global coq_xH p ->
455
      Big_int.unit_big_int
456
  | App (f, [|a|]) when is_global coq_xI f ->
457
      (* Plus (Mult (Cst 2, tr_positive a), Cst 1) *)
458
      Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a))
459
  | App (f, [|a|]) when is_global coq_xO f ->
460
      (* Mult (Cst 2, tr_positive a) *)
461 462 463 464 465 466
      Big_int.mult_big_int big_two (tr_positive a)
  | Cast (p, _, _) ->
      tr_positive p
  | _ ->
      raise NotArithConstant

Andrei Paskevich's avatar
Andrei Paskevich committed
467 468
let const_of_big_int b =
  Term.t_const
469
    (Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
470

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

505
let rec tr_type dep tvm env t =
506 507
  let t = Reductionops.clos_norm_flags
      (Closure.RedFlags.red_add_transparent
508
	 Closure.betadeltaiota (get_transp_state env))
509
      env Evd.empty t in
510
  if is_global coq_Z t then
511
    Ty.ty_int
512
  else if is_global coq_R t then
513 514
    Ty.ty_real
  else match kind_of_term t with
515
    | Var x when Idmap.mem x tvm ->
516 517 518 519
        begin match Idmap.find x tvm with
          | None -> raise NotFO
          | Some ty -> ty
        end
520
    | _ ->
521 522 523 524
        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
525
          let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
526 527
          assert (List.length ts.Ty.ts_args = List.length cl);
          (* since t:Set *)
528 529 530 531 532 533 534 535
          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
536

537
(* the type symbol for r *)
538
and tr_task_ts dep env r =
539
  let ts = tr_global_ts dep env r in
540 541 542 543
  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;
544
  ts
545 546

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

688
(* the function/predicate symbol for r *)
689
and tr_task_ls dep env r =
690
  let ls = tr_global_ls dep env r in
691 692 693 694
  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;
695
  ls
696

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

and make_one_ls dep env r =
741
  let ty = type_of_global r in
742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760
  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
761
  add_poly_arity ls vars
762

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

832 833 834 835
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
836
    make_one_ls dep env (IndRef (ith_mutual_inductive i j))
837 838 839 840 841 842 843 844
  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
845
      let ty = type_of_global r in
846 847 848
      let (_,vars), env, f = decomp_type_quantifiers env ty in
      let tvm =
        let add v1 v2 tvm =
849
          let v2 = Some (Ty.ty_var v2) in
850 851
          Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
852
        List.fold_right2 add vars (get_poly_arity ls) Idmap.empty
853 854 855 856 857 858
      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
859 860 861 862
    let cl =
      try Array.to_list (Array.mapi mk_constructor oib.mind_nf_lc)
      with NotFO -> []
    in
863 864
    ls, cl
  in
865 866 867 868 869 870
  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
871
  let s = if finite_ind mib.mind_finite then Decl.Ind else Decl.Coind in
872
  pl, if dl = [] then None else Some (Decl.create_ind_decl s dl)
873

874 875
(* translation of a Coq term
   assumption: t:T:Set *)
876
and tr_term dep tvm bv env t =
877
  try
878
    tr_arith_constant dep t
879
  with NotArithConstant -> match kind_of_term t with
880
    (* binary operations on integers *)
881
    | App (c, [|a;b|]) when is_global coq_Zplus c ->
882
        let ls = why_constant_int dep ["infix +"] in
883
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
884
          Ty.ty_int
885
    | App (c, [|a;b|]) when is_global coq_Zminus c ->
886
        let ls = why_constant_int dep ["infix -"] in
887
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
888
          Ty.ty_int
889
    | App (c, [|a;b|]) when is_global coq_Zmult c ->
890
        let ls = why_constant_int dep ["infix *"] in
891
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
892
          Ty.ty_int
893
    | App (c, [|a;b|]) when is_global coq_Zdiv c ->
894
        let ls = why_constant_eucl dep ["div"] in
895
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
896
          Ty.ty_int
897
    | App (c, [|a|]) when is_global coq_Zopp c ->
898
        let ls = why_constant_int dep ["prefix -"] in
899
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_int
900
    (* binary operations on reals *)
901
    | App (c, [|a;b|]) when is_global coq_Rplus c ->
902
        let ls = why_constant_real dep ["infix +"] in
903
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
904
          Ty.ty_real
905
    | App (c, [|a;b|]) when is_global coq_Rminus c ->
906
        let ls = why_constant_real dep ["infix -"] in
907
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
908
          Ty.ty_real
909
    | App (c, [|a;b|]) when is_global coq_Rmult c ->
910
        let ls = why_constant_real dep ["infix *"] in
911
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
912
          Ty.ty_real
913
    | App (c, [|a;b|]) when is_global coq_Rdiv c ->
914
        let ls = why_constant_real dep ["infix /"] in
915
        Term.fs_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
916
          Ty.ty_real
917
    | App (c, [|a|]) when is_global coq_Ropp c ->
918
        let ls = why_constant_real dep ["prefix -"] in
919
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
920
    | App (c, [|a|]) when is_global coq_Rinv c ->
921
        let ls = why_constant_real dep ["inv"] in
922
        Term.fs_app ls [tr_term dep tvm bv env a] Ty.ty_real
923
          (* first-order terms *)
924
    | Var id when Idmap.mem id bv ->
925 926 927 928 929
        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
930
    | Case (ci, _, e, br) ->
931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949
        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))
950
    | LetIn (x, e1, ty1, e2) ->
951
        if is_Prop ty1 || is_fo_kind ty1 then
952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967
          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
968
    | Var _ | App _ | Construct _ | Ind _ | Const _ ->
969
        let f, cl = decompose_app t in
970 971 972 973 974
        (* 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;
975
        let r = try global_of_constr f with _ -> raise NotFO in
976 977 978
        let ls = tr_task_ls dep env r in
        begin match ls.Term.ls_value with
          | Some _ ->
979
              let cl = List.filter (fun c -> not (has_WhyType env c)) cl in
980 981 982 983
              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
984
              Term.fs_app ls (List.map (tr_term dep tvm bv env) cl) ty
985 986 987
          | None  ->
              raise NotFO
        end
988
        (* TODO: we could abstract some part of (f cl) when not FO *)
989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003
(*               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 *)
1004

1005
and quantifiers n a b dep tvm bv env =
1006
  let id, env = coq_rename_var env n a in
1007
  let b = subst1 (mkVar id) b in
1008
  let t = tr_type dep tvm env a in
1009
  let vs = Term.create_vsymbol (preid_of_id id) t in
1010
  let bv = Idmap.add id (Some vs) bv in
1011 1012
  vs, t, bv, env, b

1013 1014
(* translation of a Coq formula
   assumption f:Prop *)
1015
and tr_formula dep tvm bv env f = match kind_of_term f with
1016
  | App(c, [|t;a;b|]) when is_global coq_eq c ->
1017 1018 1019 1020 1021
      let ty = type_of env Evd.empty t in
      if not (is_Set ty || is_Type ty) then raise NotFO;
      let _ = tr_type dep tvm env t in
      Term.t_equ (tr_term dep tvm bv env a) (tr_term dep tvm bv env b)
  (* comparisons on integers *)
1022
  | App(c, [|a;b|]) when is_global coq_Zle c ->
1023
      let ls = why_constant_int dep ["infix <="] in
1024
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
1025
  | App(c, [|a;b|]) when is_global coq_Zlt c ->
1026
      let ls = why_constant_int dep ["infix <"] in
1027
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
1028
  | App(c, [|a;b|]) when is_global coq_Zge c ->
1029
      let ls = why_constant_int dep ["infix >="] in
1030
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
1031
  | App(c, [|a;b|]) when is_global coq_Zgt c ->
1032
      let ls = why_constant_int dep ["infix >"] in
1033 1034
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
  (* comparisons on reals *)
1035
  | App(c, [|a;b|]) when is_global coq_Rle c ->
1036
      let ls = why_constant_real dep ["infix <="] in
1037
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
1038
  | App(c, [|a;b|]) when is_global coq_Rlt c ->
1039
      let ls = why_constant_real dep ["infix <"] in
1040
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]
1041
  | App(c, [|a;b|]) when is_global coq_Rge c ->
1042
      let ls = why_constant_real dep ["infix >="] in
1043
      Term.ps_app ls [tr_term dep tvm bv env a; tr_term dep tvm bv env b]