encoding_guard.ml 10.1 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.                           *)
(*                                                                  *)
(********************************************************************)
François Bobot's avatar
François Bobot committed
11 12 13 14 15

(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)


16
open Stdlib
François Bobot's avatar
François Bobot committed
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
open Ident
open Ty
open Term
open Decl
open Task
open Libencoding

(** module with printing functions *)
module Debug = struct
  let print_mtv vprinter fmter m =
    Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
      Pretty.print_tv key vprinter value) m

  (** utility to print a list of items *)
  let rec print_list printer fmter = function
    | [] -> Format.fprintf fmter ""
    | e::es -> if es = []
        then Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
        else Format.fprintf fmter "@[%a@], %a" printer e
        (print_list printer) es

  let debug x = Format.eprintf "%s@." x
end

(** {2 module to separate utilities from important functions} *)

module Transform = struct

45
  (** type_of *)
François Bobot's avatar
François Bobot committed
46 47 48 49
  let fs_type =
    let alpha = ty_var (create_tvsymbol (id_fresh "a")) in
    create_fsymbol (id_fresh "type_of") [alpha] ty_type

50
  let app_type t = fs_app fs_type [t] ty_type
François Bobot's avatar
François Bobot committed
51

52 53 54 55 56 57 58
  (** rewrite a closed formula modulo its free typevars
      using selection functions *)
  let rec extract_tvar acc t ty = match ty.ty_node with
    | Tyvar tvar when Mtv.mem tvar acc -> acc
    | Tyvar tvar -> Mtv.add tvar t acc
    | Tyapp (ts,tyl) ->
      let fold acc ls_select ty =
59
        extract_tvar acc (fs_app ls_select [t] ty_type) ty in
60 61 62
      List.fold_left2 fold acc (ls_selects_of_ts ts) tyl

  let type_close_select tvs ts fn f =
63
    let fold acc t = extract_tvar acc (app_type t) (t_type t) in
64
    let tvm = List.fold_left fold Mtv.empty ts in
65
    let tvs = Mtv.set_diff tvs tvm in
66 67 68 69 70
    let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
    let tvm' = Mtv.mapi (fun v () -> get_vs v) tvs in
    let vl = Mtv.values tvm' in
    let tvm' = Mtv.map t_var tvm' in
    let tvm = Mtv.union (fun _ _ _ -> assert false) tvm tvm' in
71
    t_forall_close_simp vl [] (fn tvm f)
72 73


74
  let type_variable_only_in_value lsymbol =
75
    let tvar_val = ty_freevars Stv.empty (Opt.get lsymbol.ls_value) in
76 77 78
    let tvar_arg = List.fold_left ty_freevars Stv.empty lsymbol.ls_args in
    Stv.diff tvar_val tvar_arg

François Bobot's avatar
François Bobot committed
79 80 81
  (** creates a new logic symbol, with a different type if the
  given symbol was polymorphic *)
  let findL = Wls.memoize 63 (fun lsymbol ->
82
    if lsymbol.ls_value = None then lsymbol else
83
    let new_ty = type_variable_only_in_value lsymbol in
François Bobot's avatar
François Bobot committed
84 85 86 87 88 89 90 91
    (* as many t as type vars *)
    if Stv.is_empty new_ty then lsymbol (* same type *) else
      let add _ acc = ty_type :: acc in
      let args = Stv.fold add new_ty lsymbol.ls_args in
      (* creates a new lsymbol with the same name but a different type *)
      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)

  (** {1 transformations} *)
92
    (** todo use callback for this one *)
93
  let rec f_open_all_quant q f = match f.t_node with
94 95
    | Tquant (q', f) when q' = q ->
      let vl, tr, f = t_open_quant f in
96 97 98 99 100 101 102 103
      begin match tr with
        | [] ->
          let vl', tr, f = f_open_all_quant q f in
          vl@vl', tr, f
        | _ -> vl, tr, f
      end
    | _ -> [], [], f

François Bobot's avatar
François Bobot committed
104 105 106 107 108

  (** translation of terms *)
  let rec term_transform kept varM t =
    match t.t_node with
      (* first case : predicate are not translated *)
109
    | Tapp(p,terms) when t.t_ty = None ->
François Bobot's avatar
François Bobot committed
110
      let terms = List.map (term_transform kept varM) terms in
111
      ps_app (findL p) terms
112 113 114
    | Tapp(f,terms) ->
      let terms = args_transform kept varM f terms (t_type t) in
      t_app (findL f) terms t.t_ty
115
    | Tquant(q,_) ->
116 117
      let vsl,trl,fmla = f_open_all_quant q t in
      let fmla = term_transform kept varM fmla in
118
      let fmla2 = guard q kept varM fmla vsl in
François Bobot's avatar
François Bobot committed
119
        (* TODO : how to modify the triggers? *)
120
      let trl = tr_map (term_transform kept varM) trl in
121
      t_quant q (t_close_quant vsl trl fmla2)
122 123
    | _ -> (* default case : traverse *)
      t_map (term_transform kept varM) t
François Bobot's avatar
François Bobot committed
124

125 126
  and guard q kept varM fmla vsl =
    let aux fmla vs =
127
      if Libencoding.is_protected_vs kept vs then fmla else
128
        let g = t_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
129
        match q with
130 131
          | Tforall -> t_implies g fmla
          | Texists -> t_and g fmla in
132 133
    List.fold_left aux fmla vsl

134
  and args_transform kept varM lsymbol args ty =
François Bobot's avatar
François Bobot committed
135
    (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
136
    let tv_to_ty = ty_match Mtv.empty (Opt.get lsymbol.ls_value) ty in
137
    let new_ty = type_variable_only_in_value lsymbol in
138
    let tv_to_ty = Mtv.set_inter tv_to_ty new_ty in
François Bobot's avatar
François Bobot committed
139 140 141 142 143 144
    (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
    let args = List.map (term_transform kept varM) args in
    (* fresh args to be added at the beginning of the list of arguments *)
    let add _ ty acc = term_of_ty varM ty :: acc in
    Mtv.fold add tv_to_ty args

145
  and f_type_close_select kept f' =
146
    let tvs = t_ty_freevars Stv.empty f' in
147
    let trans fn acc f = match f.t_node with
148
      | Tquant(Tforall as q,_) -> (* Exists same thing? *)
149
        let vsl,trl,fmla = f_open_all_quant q f in
150 151 152 153 154
        let add acc vs = (t_var vs)::acc in
        let acc = List.fold_left add acc vsl in
        let fn varM f =
          let fmla2 = guard q kept varM f vsl in
          (* TODO : how to modify the triggers? *)
155
          let trl = tr_map (term_transform kept varM) trl in
156
          fn varM (t_quant q (t_close_quant vsl trl fmla2))
157
        in
158
        let fn varM f = fn varM (term_transform kept varM f) in
159 160
        type_close_select tvs acc fn fmla
      | _ ->
161
        let fn varM f = fn varM (term_transform kept varM f) in
162 163 164
        type_close_select tvs acc fn f in
    trans (fun _ f -> f) [] f'

François Bobot's avatar
François Bobot committed
165 166 167
  let logic_guard kept acc lsymbol =
    match lsymbol.ls_value with
      | None -> acc
168
      | Some _ when Libencoding.is_protected_ls kept lsymbol -> acc
François Bobot's avatar
François Bobot committed
169
      | Some ty_val ->
170 171 172
        let v_id = if Libencoding.is_protecting_id lsymbol.ls_name
          then id_fresh "x" else Libencoding.id_unprotected "j" in
        let varl = List.map (create_vsymbol v_id) lsymbol.ls_args in
François Bobot's avatar
François Bobot committed
173 174
        let trans varM () =
          let terms = List.map t_var varl in
175
          let terms = args_transform kept varM lsymbol terms ty_val in
François Bobot's avatar
François Bobot committed
176
          let fmla =
177
            t_equ (app_type (fs_app (findL lsymbol) terms ty_val))
François Bobot's avatar
François Bobot committed
178 179
              (term_of_ty varM ty_val) in
          let guard fmla vs =
180
            if Libencoding.is_protected_vs kept vs then fmla else
181 182
              let g = t_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
              t_implies g fmla in
François Bobot's avatar
François Bobot committed
183
          let fmla = List.fold_left guard fmla varl in
184
          t_forall_close_simp varl [] fmla
François Bobot's avatar
François Bobot committed
185
        in
186 187 188
        let stv = ls_ty_freevars lsymbol in
        let tl = List.rev_map (t_var) varl in
        let fmla = type_close_select stv tl trans () in
François Bobot's avatar
François Bobot committed
189 190 191
        Decl.create_prop_decl Paxiom
          (create_prsymbol (id_clone lsymbol.ls_name)) fmla::acc

192 193 194
  let param_transform kept ls =
    Decl.create_param_decl (findL ls) :: logic_guard kept [] ls

195
  let logic_transform kept d = function
196
    | [ls,ld] when not (Sid.mem ls.ls_name d.d_syms) ->
197 198 199 200
        let f = f_type_close_select kept (ls_defn_axiom ld) in
        Libencoding.defn_or_axiom (findL ls) f @ logic_guard kept [] ls
    | _ -> Printer.unsupportedDecl d
        "Recursively-defined symbols are not supported, run eliminate_recursion"
François Bobot's avatar
François Bobot committed
201 202

  (** transform an inductive declaration *)
203
  let ind_transform kept s idl =
204
    let iconv (pr,f) = pr, f_type_close_select kept f in
François Bobot's avatar
François Bobot committed
205
    let conv (ls,il) = findL ls, List.map iconv il in
206
    [Decl.create_ind_decl s (List.map conv idl)]
François Bobot's avatar
François Bobot committed
207 208 209

  (** transforms a proposition into another (mostly a substitution) *)
  let prop_transform kept (prop_kind, prop_name, f) =
210
    let quantified_fmla = f_type_close_select kept f in
François Bobot's avatar
François Bobot committed
211 212 213 214 215 216 217
    [Decl.create_prop_decl prop_kind prop_name quantified_fmla]

end

(** {2 main part} *)

let decl kept d = match d.d_node with
218 219 220 221 222 223
  | Dtype { ts_def = Some _ } -> []
  | Dtype ts -> d :: Libencoding.lsdecl_of_ts_select ts
  | Ddata _ -> Printer.unsupportedDecl d
      "Algebraic and recursively-defined types are \
            not supported, run eliminate_algebraic"
  | Dparam ls -> Transform.param_transform kept ls
224
  | Dlogic ldl -> Transform.logic_transform kept d ldl
225
  | Dind (s, idl) -> Transform.ind_transform kept s idl
François Bobot's avatar
François Bobot committed
226 227 228 229 230
  | Dprop prop -> Transform.prop_transform kept prop

let empty_th =
  let task = use_export None Theory.builtin_theory in
  let task = Task.add_decl task d_ts_type in
231 232
  let task = Task.add_param_decl task ls_int_of_ty in
  let task = Task.add_param_decl task Transform.fs_type in
François Bobot's avatar
François Bobot committed
233 234 235
  task

let guard =
236
  Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
François Bobot's avatar
François Bobot committed
237 238 239 240
    Trans.decl (decl kept) empty_th)

(** {2 monomorphise task } *)

241
open Libencoding
François Bobot's avatar
François Bobot committed
242

243
let lsmap kept = Wls.memoize 63 (fun ls ->
244 245 246 247 248
  let prot_arg = is_protecting_id ls.ls_name in
  let prot_val = is_protected_id ls.ls_name in
  let neg ty = if prot_arg && Sty.mem ty kept then ty else ty_base in
  let pos ty = if prot_val && Sty.mem ty kept then ty else ty_base in
  let ty_arg = List.map neg ls.ls_args in
249 250
  let ty_res = Opt.map pos ls.ls_value in
  if Opt.equal ty_equal ty_res ls.ls_value &&
François Bobot's avatar
François Bobot committed
251 252 253
     List.for_all2 ty_equal ty_arg ls.ls_args then ls
  else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)

254
let monomorph = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
François Bobot's avatar
François Bobot committed
255
  let kept = Sty.add ty_type kept in
256
  let decl = d_monomorph kept (lsmap kept) in
François Bobot's avatar
François Bobot committed
257 258
  Trans.decl decl (Task.add_decl None d_ts_base))

259
let () = Hstr.replace Encoding.ft_enco_poly "guard"
François Bobot's avatar
François Bobot committed
260
    (fun _ -> Trans.compose guard monomorph)