encoding_instantiate.ml 18.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
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 Stdlib
13 14 15 16 17 18 19
open Ident
open Ty
open Term
open Theory
open Task
open Decl

20
exception TooMuchInstantiation of int
21
let max_instantiation = 512 (* 7 ** 3 = 343 *)
22 23 24 25 26 27 28

let () = Exn_printer.register (fun fmt exn ->
  match exn with
    | TooMuchInstantiation i -> Format.fprintf fmt
      "encoding_instantiate : %i instantiation to create, it is limited to %i"
      i max_instantiation
    | _ -> raise exn)
29

30
(* Ce type est utiliser pour indiquer un alpha *)
31
let tv_dumb = create_tvsymbol (id_fresh "instantiate_alpha")
32 33
let ty_dumb = ty_var tv_dumb

34 35 36
(* TODO : transmettre les tags des logiques polymorphe vers les logiques
   instantié. Un tag sur un logique polymorphe doit être un tag sur toute
   la famille de fonctions *)
37

38
module OHTyl = OrderedHashedList(struct
Andrei Paskevich's avatar
Andrei Paskevich committed
39 40 41 42
  type t = ty
  let tag = ty_hash
end)

43 44
module Mtyl = Extmap.Make(OHTyl)
module Htyl = Exthtbl.Make(OHTyl)
45 46

type tenv =
47 48 49
  | Complete (* The transformation keep the polymorphism *)
  | Incomplete (* The environnement when the transformation isn't complete*)

50

51
(* A type is projected on term or type depending
52
   of its color (green part,red part, black part) *)
53
type tty =
54
  | Tyterm of ty
55 56
  | Tyty of ty

57
(* dead code
58
let print_tty fmt = function
59
  | Tyterm ty -> Format.fprintf fmt "(Tyterm %a)" Pretty.print_ty ty
60
  | Tyty ty -> Format.fprintf fmt "(Tyty %a)" Pretty.print_ty ty
61
*)
62

63 64
(* It can be backprojected to type, ty_dumb is like a bottom type it
   never appear in final formulas *)
65 66 67 68 69
let reduce_to_type = function
  | Tyty ty -> ty
  | Tyterm _ -> ty_dumb


70 71 72 73 74 75 76 77 78 79 80 81 82 83
let reduce_to_real = function
  | Tyty ty | Tyterm ty -> ty

(* let reduce_to_pos tenv = function *)
(*   | Tyty ty -> ty *)
(*   | Tyterm _ -> match tenv with  *)
(*       | Incomplete -> assert false (\* All is type in this mode *\) *)
(*       | Tenv tenv -> tenv.undeco *)

(* let reduce_to_neg tenv = function *)
(*   | Tyty ty -> ty *)
(*   | Tyterm _ -> match tenv with  *)
(*       | Incomplete -> assert false (\* All is type in this mode *\) *)
(*       | Tenv tenv -> tenv.deco *)
84

85
(* The environnement of the transformation between two decl (* unmutable *) *)
86 87 88
type env = {
  etenv : tenv;
  ekeep : Sty.t;
89
  prop_toremove : ty Mtv.t Mpr.t;
90 91
  eprojty : ty Mty.t;
  edefined_lsymbol : lsymbol Mtyl.t Mls.t;
92
  edefined_tsymbol : tysymbol Mtyl.t Mts.t;
93 94
}

95
(* dead code
96
type auto_clone = task -> tenv -> Sty.t -> task * env
97
*)
98

99
(* The environnement of the transformation during
100
   the transformation of a formula *)
101 102 103 104 105
type menv = {
  tenv : tenv;
  keep : Sty.t;
  mutable projty : ty Mty.t;
  mutable defined_lsymbol : lsymbol Mtyl.t Mls.t;
106
  mutable defined_tsymbol : tysymbol Mtyl.t Mts.t;
107 108 109 110
  mutable undef_lsymbol : Sls.t;
  mutable undef_tsymbol : Sts.t;
}

111
let _print_env fmt menv =
112
  Format.fprintf fmt "defined_lsymbol (%a)@."
113
    (Pp.print_iter2 Mls.iter Pp.semi Pp.comma Pretty.print_ls
114 115 116 117
       (Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
          (Pp.print_list Pp.space Pretty.print_ty)
          Pretty.print_ls)) menv.defined_lsymbol;
  Format.fprintf fmt "defined_tsymbol (%a)@."
118
    (Pp.print_iter2 Mts.iter Pp.semi Pp.comma Pretty.print_ts
119 120
       (Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
          (Pp.print_list Pp.space Pretty.print_ty)
121
          Pretty.print_ts)) menv.defined_tsymbol
122

123
type _tvar = ty Mtv.t
124

125
let projty menv tvar ty =
126 127
  let rec aux ty =
    match ty.ty_node with
128
      | Tyvar _ -> Tyterm ty
129 130 131 132 133
      | Tyapp (ts,tyl) ->
        try
          Tyty (Mty.find ty menv.projty)
        with Not_found ->
          match menv.tenv with
134
            | Incomplete ->
135
              (* In this configuration there is no term representing type,
136
                 all type are a type or are in the black part
137
                 (the or is not a xor)*)
138 139 140 141
              (* let preid = id_clone ts.ts_name in *)
              (* let ts = create_tysymbol preid [] None (\*Some ty*\) in *)
              (* let tty = ty_app ts [] in *)
              let tty = ty in
142 143 144 145 146
              menv.projty <- Mty.add ty tty menv.projty;
              menv.undef_tsymbol <- Sts.add ts menv.undef_tsymbol;
              (*Format.eprintf "projty : ts : %a env : %a@." Pretty.print_ts ts
              print_env menv;*)
              Tyty tty
147
            | Complete ->
148 149
              let tyl = List.map aux tyl in
              let tyl_red = List.map reduce_to_type tyl in
150
              let tys =
151 152 153 154 155 156 157
                try
                  Mtyl.find tyl_red (Mts.find ts menv.defined_tsymbol)
                with Not_found ->
                  let insts = try Mts.find ts menv.defined_tsymbol
                    with Not_found -> Mtyl.empty in
                  let args = List.fold_left (fun acc e ->
                    match e with
158
                      | Tyterm _ -> (create_tvsymbol (id_fresh "a"))::acc
159
                      | Tyty _ -> acc) [] tyl in
160 161
                  let tys = if List.length args = List.length ts.ts_args
                    then ts
162 163
                    else create_tysymbol (id_clone ts.ts_name) args None in
                  let insts = Mtyl.add tyl_red tys insts in
164 165
                  menv.defined_tsymbol <-
                    Mts.add ts insts menv.defined_tsymbol;
166 167
                  menv.undef_tsymbol <- Sts.add tys menv.undef_tsymbol;
                  tys in
168 169
              let args = List.rev (List.fold_left (fun acc e ->
                match e with
170
                  | Tyterm ty -> ty::acc
171
                  | Tyty _ -> acc) [] tyl) in
172 173
              Tyterm (ty_app tys args) in
  let ty = ty_inst tvar ty in
174 175
  aux ty

176 177 178 179 180 181 182 183 184
let projty_real menv tvar ty = reduce_to_real (projty menv tvar ty)

(* let reduce_to_default menv d = function *)
(*   | Tyty ty -> ty *)
(*   | Tyterm ty -> match menv.tenv with *)
(*       | Incomplete -> ty *)
(*       | Complete -> projty menv Mtv.empty d *)


185
let reduce_to_default menv tvar d ty =
186
  match projty menv tvar ty with
187
    | Tyty _ -> (*keep the term unfolded *) ty_inst tvar ty
188 189
    | Tyterm _ -> ty_var d

190 191 192 193 194
(* Weakmemo only on the symbols *)
let clone_lsymbol_memo =
  let clone_lsymbol p =
    let h = Htyl.create 7 in
    fun arg result ->
195
      let key = (Opt.fold (fun arg r -> r::arg) arg result) in
196 197 198 199 200 201 202 203
      try
        Htyl.find h key
      with Not_found ->
        let p = create_lsymbol (id_clone p.ls_name) arg result in
        Htyl.add h key p;
        p in
  Wls.memoize 7 clone_lsymbol

204 205 206
let find_logic menv tvar p tyl ret =
  if ls_equal p ps_equ then p else begin
    let inst = ls_app_inst p tyl ret in
207 208 209
     (* Format.eprintf "inst : %a@." *)
     (*   (Pp.print_iter2 Mtv.iter Pp.comma Pp.space Pp.nothing *)
     (*      Pretty.print_ty) inst; *)
210 211
    let inst = Mtv.mapi (reduce_to_default menv tvar) inst in
    let inst_l = Mtv.fold (fun _ v acc -> v::acc) inst [] in
212 213
    (* Format.eprintf "p : %a | arg : %a| tyl = %a | inst_l : %a@." *)
    (*   Pretty.print_ls p *)
214
    (*   (Pp.print_list Pp.comma Pretty.print_ty) p.ls_args *)
215 216 217
    (*   (Pp.print_list Pp.comma Pretty.print_ty) *)
    (*   (List.map (fun t -> (projty_real menv tvar t.t_ty)) tyl) *)
    (*   (Pp.print_list Pp.comma Pretty.print_ty) inst_l; *)
218 219
      try
      let insts = Mls.find p menv.defined_lsymbol in
220
      Mtyl.find inst_l insts
221
    with Not_found ->
222
      let insts =
223 224 225 226
        try
          Mls.find p menv.defined_lsymbol
        with Not_found ->
          Mtyl.empty in
227
      (* proj fold the types previously kept unfold in inst *)
228 229 230
      let proj ty = reduce_to_real (projty menv Mtv.empty ty) in
      let arg = List.map (ty_inst inst) p.ls_args in
      let arg = List.map proj arg in
231 232
      let result = Opt.map (ty_inst inst) p.ls_value in
      let result = Opt.map proj result in
233 234 235
      (* Format.eprintf "arg : %a ; result : %a@." *)
      (*   (Pp.print_list Pp.comma Pretty.print_ty) arg *)
      (*   (Pp.print_option Pretty.print_ty) result; *)
236
      let ls = if List.for_all2 ty_equal arg p.ls_args &&
237
          Opt.equal ty_equal result p.ls_value
238
        then p else clone_lsymbol_memo p arg result in
239 240 241
      let insts = Mtyl.add inst_l ls insts in
      menv.defined_lsymbol <- Mls.add p insts menv.defined_lsymbol;
      menv.undef_lsymbol <- Sls.add ls menv.undef_lsymbol;
242
      (* Format.eprintf "fl : env : %a  p : %a | inst : %a@." *)
243 244 245 246 247 248 249 250 251 252 253 254 255
      (*   print_env menv *)
      (*   Pretty.print_ls p *)
      (*   (Pp.print_list Pp.comma Pretty.print_ty) inst_l; *)
      ls
  end


(* let deco_res menv t ty = *)
(*   match ty with *)
(*     | Tyty _ -> t *)
(*     | Tyterm tyterm -> *)
(*       match menv.tenv with *)
(*         | Incomplete -> assert false *)
256
(*         | Tenv tenv -> fs_app tenv.sort [tyterm;t] tenv.deco *)
257 258 259 260

(* let sort_app tenv ty t = *)
(*   match tenv with *)
(*     | Incomplete -> assert false *)
261
(*     | Tenv tenv -> fs_app tenv.sort [ty;t] tenv.deco    *)
262 263 264


let conv_vs menv tvar vsvar vs =
265 266 267 268
  let ty = projty_real menv tvar vs.vs_ty in
  let vs' = if ty_equal ty vs.vs_ty then vs else
      create_vsymbol (id_clone vs.vs_name) ty in
  Mvs.add vs (t_var vs') vsvar,vs'
269

270
(* The convertion of term and formula *)
271
let rec rewrite_term menv tvar vsvar t =
272 273
  let fnT = rewrite_term menv tvar in
  let fnF = rewrite_fmla menv tvar in
274
  (* Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t; *)
275
  let t = match t.t_node with
276 277
    | Tconst _ -> t
    | Tvar x -> Mvs.find x vsvar
278
    | Tapp(p,tl) ->
279
      let tl' = List.map (fnT vsvar) tl in
280
      let p = find_logic menv tvar p tl t.t_ty in
281
      fs_app p tl' (projty_real menv tvar (t_type t))
282 283
    | Tif(f, t1, t2) ->
      t_if (fnF vsvar f) (fnT vsvar t1) (fnT vsvar t2)
284
    | Tlet (t1, b) -> let u,t2,cb = t_open_bound_cb b in
285
      let (vsvar',u) = conv_vs menv tvar vsvar u in
286 287
      let t1 = fnT vsvar t1 in let t2 = fnT vsvar' t2 in
      t_let t1 (cb u t2)
288
    | Tcase _ | Teps _ ->
289
      Printer.unsupportedTerm t
290
        "Encoding instantiate : I can't encode this term"
291
    | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
292
  in
293 294 295
  (* Format.eprintf "@[<hov 2>Term : => %a : %a@\n@?" *)
  (*   Pretty.print_term t Pretty.print_ty t.t_ty; *)
  t
296

297
and rewrite_fmla menv tvar vsvar f =
298 299
  let fnT = rewrite_term menv tvar in
  let fnF = rewrite_fmla menv tvar in
300
  (* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
301 302
  match f.t_node with
    | Tapp(p, tl) ->
303
      let tl' = List.map (fnT vsvar) tl in
304
      let p = find_logic menv tvar p tl None in
305
      ps_app p tl'
306 307
    | Tquant(q, b) ->
      let vl, tl, f1, cb = t_open_quant_cb b in
308
      let vsvar,vl = Lists.map_fold_left (conv_vs menv tvar) vsvar vl in
309 310 311

      let f1 = fnF vsvar f1 in
      (* Ici un trigger qui ne match pas assez de variables
312
         peut être généré *)
313
      let tl = TermTF.tr_map (fnT vsvar) (fnF vsvar) tl in
314
      t_quant q (cb vl tl f1)
315
    | Tlet (t1, b) -> let u,f2,cb = t_open_bound_cb b in
316
      let (vsvar',u) = conv_vs menv tvar vsvar u in
317
      let t1 = fnT vsvar t1 and f2 = fnF vsvar' f2 in
318 319
      (* Format.eprintf "u.vs_ty : %a == t1.t_ty : %a@." *)
      (*    Pretty.print_ty u.vs_ty Pretty.print_ty t1.t_ty; *)
320
      ty_equal_check u.vs_ty (t_type t1);
321
      t_let t1 (cb u f2)
322
    | _ -> TermTF.t_map (fun _ -> assert false) (fnF vsvar) f
323

324
(* Generation of all the possible instantiation of a formula *)
325 326
let gen_tvar env ts =
  let aux tv tvarl =
327
    let gen tvar ty = Mtv.add tv ty tvar in
328
    let tvarl' = List.fold_left (fun acc tvar ->
329 330
      Sty.fold (fun ty acc -> gen tvar ty :: acc) env.ekeep acc) [] tvarl in
    match env.etenv with
331 332 333
      | Incomplete -> tvarl'
      | Complete ->
        let gen acc tvar = (Mtv.add tv (ty_var tv) tvar)::acc in
334
        List.fold_left gen tvarl' tvarl in
335
  Stv.fold aux ts [Mtv.empty]
336 337

(*
338
let ty_args_from_tty =
339 340 341
  List.fold_left (fun acc e ->
    match e with
      | Tyterm _ -> tenv.ty::acc
342
      | Tyty _ -> acc) []
343 344 345

let conv_to_tty env ts tyl proj_ty =
  let ty = ty_app ts tyl in
346
  if Sty.mem ty env.keep
347 348 349 350 351 352 353 354
  then (assert (Mty.mem ty proj_ty); proj_ty)
  else let args = ty_args_from_tty tyl in
*)

let ty_quant =
  let rec add_vs s ty = match ty.ty_node with
    | Tyvar vs -> Stv.add vs s
    | _ -> ty_fold add_vs s ty in
355
  t_ty_fold add_vs Stv.empty
356

357 358
let add_decl_ud menv task =
  let task = Sts.fold
359
    (fun ts task -> add_ty_decl task ts)
360 361
    menv.undef_tsymbol task in
  let task = Sls.fold
362
    (fun ls task -> add_param_decl task ls)
363 364 365 366
    menv.undef_lsymbol task in
  task


367
(* The Core of the transformation *)
368
let fold_map task_hd ((env:env),task) =
369
  match task_hd.task_decl.td_node with
370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401
    | Use _ | Clone _ -> env,add_tdecl task task_hd.task_decl
    | Meta(meta,ml) ->
      begin try
        let menv =  {
          tenv = env.etenv;
          keep = env.ekeep;
          projty = env.eprojty;
          defined_lsymbol = env.edefined_lsymbol;
          defined_tsymbol = env.edefined_tsymbol;
          undef_lsymbol = Sls.empty;
          undef_tsymbol = Sts.empty;
        } in
        let map = function
          | MAty ty -> MAty (projty_real menv Mtv.empty ty)
          (* | MAts {ts_name = name; ts_args = []; ts_def = Some ty} -> *)
          (*   MAts (conv_ts tenv ud name ty) *)
          (* | MAts {ts_args = []; ts_def = None} as x -> x *)
          | MAts _ -> raise Exit
          | MAls _ -> raise Exit
          | MApr _ -> raise Exit
          | MAstr _ as s -> s
          | MAint _ as i -> i in
        let arg = (List.map map ml) in
        let task = add_meta (add_decl_ud menv task) meta arg in
        {env with edefined_lsymbol = menv.defined_lsymbol;
          edefined_tsymbol = menv.defined_tsymbol;
          eprojty = menv.projty;
        }, task
      with
        | Printer.UnsupportedType _
        | Exit -> env,add_tdecl task task_hd.task_decl
      end
402
    | Decl d -> match d.d_node with
403
    | Dtype _ -> (env,task)
404
    (* Nothing here since the type kept are already defined and the other
405
       will be lazily defined *)
406
    | Ddata _ -> Printer.unsupportedDecl
407 408
        d "encoding_decorate : I can work only on abstract\
            type which are not in recursive bloc."
409 410 411 412 413
    | Dparam _ ->
        (* Noting here since the logics are lazily defined *)
        (env,task)
    | Dlogic _ -> Printer.unsupportedDecl
        d "encoding_decorate : I can't encode definition. \
414
Perhaps you could use eliminate_definition"
415
    | Dind _ -> Printer.unsupportedDecl
416 417 418 419 420 421
        d "encoding_decorate : I can't work on inductive"
        (* let fn (pr,f) = pr, fnF f in *)
        (* let fn (ps,l) = ps, List.map fn l in *)
        (* [create_ind_decl (List.map fn l)] *)
    | Dprop (k,pr,f) ->
      let tvl = ty_quant f in
422
      assert (k <> Pgoal || Ty.Stv.is_empty tvl);
423 424
      let tvarl = gen_tvar env tvl in
      let tvarl_len = List.length tvarl in
425 426
      if tvarl_len > max_instantiation then
        raise (TooMuchInstantiation tvarl_len);
427 428 429 430 431 432 433 434 435
      let menv =  {
        tenv = env.etenv;
        keep = env.ekeep;
        projty = env.eprojty;
        defined_lsymbol = env.edefined_lsymbol;
        defined_tsymbol = env.edefined_tsymbol;
        undef_lsymbol = Sls.empty;
        undef_tsymbol = Sts.empty;
      } in
436
      let conv_f task tvar =
437 438 439 440 441
        if begin
          try (Mtv.equal ty_equal) tvar (Mpr.find pr env.prop_toremove)
          with Not_found -> false end
        then task
        else
442
        (* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
443
        (*   (t_ty_subst tvar Mvs.empty f) *)
444
        (*   print_env menv; *)
445
        let f = rewrite_fmla menv tvar Mvs.empty f in
446 447
        (* Format.eprintf "f : %a@. env : %a@." Pretty.print_fmla f *)
        (*   print_env menv; *)
448 449
        let pr =
          if tvarl_len = 1 then pr
450
          else create_prsymbol (id_clone pr.pr_name) in
451 452 453 454 455
        (* Format.eprintf "undef ls : %a, ts : %a@." *)
        (*   (Pp.print_iter1 Sls.iter Pp.comma Pretty.print_ls) *)
        (*   menv.undef_lsymbol *)
        (*   (Pp.print_iter1 Sts.iter Pp.comma Pretty.print_ts) *)
        (*   menv.undef_tsymbol; *)
456
        let task = add_decl_ud menv task in
457 458 459 460 461 462 463 464 465 466
        let task = add_prop_decl task k pr f in
        task
      in
      {env with edefined_lsymbol = menv.defined_lsymbol;
        edefined_tsymbol = menv.defined_tsymbol;
        eprojty = menv.projty;
      },
      List.fold_left conv_f task tvarl


467
let _monomorphise_goal =
468
  Trans.goal (fun pr f ->
469
    let stv = ty_quant f in
470
    let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
471 472
      let ts = create_tysymbol (id_clone tv.tv_name) [] None in
      Mtv.add tv (ty_app ts []) mty,ts::ltv) stv (Mtv.empty,[]) in
473
    let f = t_ty_subst mty Mvs.empty f in
474 475
    let acc = [create_prop_decl Pgoal pr f] in
    let acc = List.fold_left
476
      (fun acc ts -> (create_ty_decl ts) :: acc)
477 478 479
      acc ltv in
    acc)

480

481
(* Some general env creation function *)
François Bobot's avatar
François Bobot committed
482 483
let create_env task tenv keep =
  let projty = Sty.fold (fun ty ty_ty ->
484
    Mty.add ty ty ty_ty)
485
    keep Mty.empty in
François Bobot's avatar
François Bobot committed
486
  let task = Sty.fold (fun ty task ->
487
    let add_ts task ts = add_ty_decl task ts in
488 489
    let task = ty_s_fold add_ts task ty in
    task (* the meta is yet here *)) keep task in
François Bobot's avatar
François Bobot committed
490
  task,{
491
    etenv = tenv;
492
    ekeep = keep;
493
    prop_toremove = Mpr.empty;
494 495 496 497 498
    eprojty = projty;
    edefined_lsymbol = Mls.empty;
    edefined_tsymbol = Mts.empty
  }

499
(* This one take use the tag but also all the type which appear in the goal *)
500
let _is_ty_mono ~only_mono ty =
501 502 503 504 505 506 507 508
  try
    let rec check () ty = match ty.ty_node with
      | Tyvar _ -> raise Exit
      | Tyapp _ -> ty_fold check () ty in
    check () ty;
    true
  with Exit when not only_mono -> false

509

510
let create_trans_complete kept complete =
511
  let task = use_export None builtin_theory in
512
  let init_task,env = create_env task complete kept in
513 514
  Trans.fold_map fold_map env init_task

515
let encoding_instantiate complete =
516
  Trans.compose Libencoding.close_kept
517
  (Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
518
    create_trans_complete kept complete))
519

520
let () = Hstr.replace Encoding.ft_enco_kept "instantiate"
521
  (Util.const (encoding_instantiate Incomplete))
522

523
let () = Hstr.replace Encoding.ft_enco_kept "instantiate_complete"
524
  (Util.const (encoding_instantiate Complete))
525 526 527 528 529 530

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)