encoding_twin.ml 4.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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
open Ident
open Ty
open Term
open Decl

18
let make_pont = Wty.memoize 3 (fun ty ->
19 20 21 22 23 24 25 26
  let t2tb =
    let t2tb_name = "t2tb" in
    let t2tb_id = Libencoding.id_unprotected t2tb_name in
    create_fsymbol t2tb_id [ty] ty in
  let tb2t =
    let tb2t_name = "tb2t" in
    let tb2t_id = Libencoding.id_unprotecting tb2t_name in
    create_fsymbol tb2t_id [ty] ty in
27 28
  let t2tb_def = create_param_decl t2tb in
  let tb2t_def = create_param_decl tb2t in
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
  let bridge_l =
    let x_vs = create_vsymbol (id_fresh "i") ty in
    let x_t = t_var x_vs in
    let t2tb_x = fs_app t2tb [x_t] ty in
    let tb2t_t2tb_x = fs_app tb2t [t2tb_x] ty in
    let eq = t_equ tb2t_t2tb_x x_t in
    let ax = t_forall_close [x_vs] [[t2tb_x]] eq in
    let pr = create_prsymbol (id_fresh "BridgeL") in
    create_prop_decl Paxiom pr ax in
  let bridge_r =
    let x_vs = create_vsymbol (Libencoding.id_unprotected "j") ty in
    let x_t = t_var x_vs in
    let tb2t_x = fs_app tb2t [x_t] ty in
    let t2tb_tb2t_x = fs_app t2tb [tb2t_x] ty in
    let eq = t_equ t2tb_tb2t_x x_t in
    let ax = t_forall_close [x_vs] [[t2tb_tb2t_x]] eq in
    let pr = create_prsymbol (id_fresh "BridgeR") in
    create_prop_decl Paxiom pr ax in
47
  t2tb, tb2t, [t2tb_def; tb2t_def; bridge_l; bridge_r])
Andrei Paskevich's avatar
Andrei Paskevich committed
48 49

let seen = Hty.create 7
50 51

let add_decls tenv decls =
Andrei Paskevich's avatar
Andrei Paskevich committed
52 53 54 55 56
  let add ty () decls =
    let _,_,defs = Mty.find ty tenv in
    List.append defs decls in
  let decls = Hty.fold add seen decls in
  Hty.clear seen;
57 58 59 60 61 62
  decls

let conv_arg tenv t aty =
  let tty = t_type t in
  if ty_equal tty aty then t else
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
63 64
    let t2tb,tb2t,_ = Mty.find tty tenv in
    Hty.replace seen tty ();
65 66 67 68 69 70 71
    match t.t_node with
      | Tapp (fs,[t]) when ls_equal fs tb2t -> t
      | _ -> fs_app t2tb [t] tty
  with Not_found -> t

let conv_app tenv fs tl tty =
  let t = fs_app fs tl tty in
72
  let vty = Opt.get fs.ls_value in
73 74
  if ty_equal tty vty then t else
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
75 76
    let _,tb2t,_ = Mty.find tty tenv in
    Hty.replace seen tty ();
77 78 79 80 81 82 83
    fs_app tb2t [t] tty
  with Not_found -> t

(* FIXME? in quantifiers we might generate triggers
   with unnecessary bridge functions over them *)
let rec rewrite tenv t = match t.t_node with
  | Tapp (ls,[t1;t2]) when ls_equal ls ps_equ ->
84
      t_label_copy t (t_equ (rewrite tenv t1) (rewrite tenv t2))
85 86 87
  | Tapp (ls,tl) ->
      let tl = List.map (rewrite tenv) tl in
      let tl = List.map2 (conv_arg tenv) tl ls.ls_args in
88 89
      if t.t_ty = None then t_label_copy t (ps_app ls tl)
      else t_label_copy t (conv_app tenv ls tl (t_type t))
90 91 92
  | _ -> t_map (rewrite tenv) t

let decl tenv d = match d.d_node with
93 94
  | Dtype _ | Dparam _ -> [d]
  | Ddata _ -> Printer.unsupportedDecl d
95 96
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
97
  | Dlogic [ls,ld] when not (Sid.mem ls.ls_name d.d_syms) ->
98 99 100 101 102 103 104 105 106 107 108 109 110 111
      let f = rewrite tenv (ls_defn_axiom ld) in
      Libencoding.defn_or_axiom ls f
  | Dlogic _ -> Printer.unsupportedDecl d
      "Recursively defined symbols are not supported, run eliminate_recursion"
  | Dind _ -> Printer.unsupportedDecl d
      "Inductive predicates are not supported, run eliminate_inductive"
  | Dprop (k,pr,f) ->
      [create_prop_decl k pr (rewrite tenv f)]

let decl tenv d =
  let decls = decl tenv d in
  add_decls tenv decls

let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
112
  Trans.decl (decl (Mty.mapi (fun ty () -> make_pont ty) s)) None)
113

114
let () = Hstr.replace Encoding.ft_enco_kept "twin" (Util.const t)