libencoding.ml 10.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
(*                                                                  *)
(*  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
(*                                                                  *)
10
(********************************************************************)
11 12 13 14 15

open Ident
open Ty
open Term
open Decl
16 17
open Theory

18
let debug = Debug.register_info_flag "encoding"
Andrei Paskevich's avatar
Andrei Paskevich committed
19
  ~desc:"Print@ debugging@ messages@ about@ polymorphism@ encoding."
20 21 22

(* meta to tag the protected types *)
let meta_kept = register_meta "encoding : kept" [MTty]
Andrei Paskevich's avatar
Andrei Paskevich committed
23
  ~desc:"Specify@ a@ type@ to@ keep@ during@ polymorphism@ encoding."
24

25 26 27 28 29 30
(* meta to tag the custom base type *)
let meta_base = register_meta_excl "encoding : base" [MTty]
  ~desc:"Specify@ the@ base@ type@ for@ monomorphic@ \
    polymorphism@ encoding@ (`int'@ or@ `real'@ only)."

(* sort symbol of the default base type *)
31 32
let ts_base = create_tysymbol (id_fresh "uni") [] None

33
(* default base type *)
34 35 36
let ty_base = ty_app ts_base []

(* ts_base declaration *)
37
let d_ts_base = create_ty_decl ts_base
38

39 40 41 42 43 44 45
(* sort symbol of (polymorphic) types *)
let ts_type = create_tysymbol (id_fresh "ty") [] None

(* sort of (polymorphic) types *)
let ty_type = ty_app ts_type []

(* ts_type declaration *)
46
let d_ts_type = create_ty_decl ts_type
47

48 49 50 51 52 53 54 55
(* add type args to the signature of a polymorphic lsymbol *)
let ls_extend = Wls.memoize 63 (fun ls ->
  if ls_equal ls ps_equ then ls else
  let tvs = ls_ty_freevars ls in
  if Stv.is_empty tvs then ls else
  let args = Stv.fold (fun _ l -> ty_type::l) tvs ls.ls_args in
  Term.create_lsymbol (id_clone ls.ls_name) args ls.ls_value)

56 57
(* function symbol mapping ty_type^n to ty_type *)
let ls_of_ts = Wts.memoize 63 (fun ts ->
58
  let args = List.map (Util.const ty_type) ts.ts_args in
59 60 61 62 63
  create_fsymbol (id_clone ts.ts_name) args ty_type)

(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
  | Tyvar tv ->
64
      Mtv.find tv tvmap
65
  | Tyapp (ts,tl) ->
66
      fs_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type
67

68
(* rewrite a closed formula modulo its free typevars *)
François Bobot's avatar
François Bobot committed
69
let type_close tvs fn f =
70
  let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
71 72 73
  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
74
  t_forall_close_simp vl [] (fn tvm f)
75

76
let t_type_close fn f =
77
  let tvs = t_ty_freevars Stv.empty f in
François Bobot's avatar
François Bobot committed
78 79
  type_close tvs fn f

80
(* convert a type declaration to a list of lsymbol declarations *)
81
let lsdecl_of_ts ts = create_param_decl (ls_of_ts ts)
82

83
(* convert a constant to a functional symbol of type ty_base *)
84
let ls_of_const =
85 86
  Hty.memo 3 (fun ty_base ->
  Hterm.memo 63 (fun t -> match t.t_node with
87
    | Tconst _ ->
88 89 90 91 92
        let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
        create_fsymbol (id_fresh s) [] ty_base
    | _ -> assert false))

let ls_of_const ty_base t = ls_of_const ty_base (t_label Slab.empty t)
93

94 95
(* unprotected and unprotecting idents *)

Andrei Paskevich's avatar
Andrei Paskevich committed
96 97
let unprotected_label = Ident.create_label "encoding : unprotected"
let unprotecting_label = Ident.create_label "encoding : unprotecting"
98

99 100
let id_unprotected n = id_fresh ~label:(Slab.singleton unprotected_label) n
let id_unprotecting n = id_fresh ~label:(Slab.singleton unprotecting_label) n
101

102 103
let is_protected_id id = not (Slab.mem unprotected_label id.id_label)
let is_protecting_id id = not (Slab.mem unprotecting_label id.id_label)
104 105 106 107 108

let is_protected_vs kept vs =
  is_protected_id vs.vs_name && Sty.mem vs.vs_ty kept

let is_protected_ls kept ls =
109
  is_protected_id ls.ls_name && Sty.mem (Opt.get ls.ls_value) kept
110

111 112
(* monomorphise modulo the set of kept types * and an lsymbol map *)

113 114 115
let vs_monomorph ty_base kept vs =
  if ty_equal vs.vs_ty ty_base || is_protected_vs kept vs
  then vs else create_vsymbol (id_clone vs.vs_name) ty_base
116

117 118
let t_monomorph ty_base kept lsmap consts vmap t =
  let rec t_mono vmap t = t_label_copy t (match t.t_node with
119 120
    | Tvar v ->
        Mvs.find v vmap
121 122
    | Tconst _ when ty_equal (t_type t) ty_base ||
                    Sty.mem  (t_type t) kept ->
123
        t
124
    | Tconst _ ->
125
        let ls = ls_of_const ty_base t in
126
        consts := Sls.add ls !consts;
127
        fs_app ls [] ty_base
128 129 130 131 132
    | Tapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
        t_equ (t_mono vmap t1) (t_mono vmap t2)
    | Tapp (ls,tl) ->
        let ls = lsmap ls in
        t_app ls (List.map (t_mono vmap) tl) ls.ls_value
133
    | Tif (f,t1,t2) ->
134
        t_if (t_mono vmap f) (t_mono vmap t1) (t_mono vmap t2)
135 136
    | Tlet (t1,b) ->
        let u,t2,close = t_open_bound_cb b in
137
        let v = vs_monomorph ty_base kept u in
138 139 140 141 142
        let t2 = t_mono (Mvs.add u (t_var v) vmap) t2 in
        t_let (t_mono vmap t1) (close v t2)
    | Tcase _ ->
        Printer.unsupportedTerm t "no match expressions at this point"
    | Teps b ->
143
        let u,f,close = t_open_bound_cb b in
144
        let v = vs_monomorph ty_base kept u in
145
        let f = t_mono (Mvs.add u (t_var v) vmap) f in
146
        t_eps (close v f)
147 148
    | Tquant (q,b) ->
        let ul,tl,f1,close = t_open_quant_cb b in
149
        let vl = List.map (vs_monomorph ty_base kept) ul in
150 151
        let add acc u v = Mvs.add u (t_var v) acc in
        let vmap = List.fold_left2 add vmap ul vl in
152 153
        let tl = tr_map (t_mono vmap) tl in
        t_quant q (close vl tl (t_mono vmap f1))
154
    | Tbinop (op,f1,f2) ->
155
        t_binary op (t_mono vmap f1) (t_mono vmap f2)
156
    | Tnot f1 ->
157
        t_not (t_mono vmap f1)
158 159
    | Ttrue | Tfalse -> t) in
  t_mono vmap t
160

161
let d_monomorph ty_base kept lsmap d =
162
  let consts = ref Sls.empty in
163
  let t_mono = t_monomorph ty_base kept lsmap consts in
164
  let dl = match d.d_node with
165 166 167 168 169 170 171 172 173
    | Dtype { ts_def = Some _ } -> []
    | Dtype ts when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> []
    | Dtype ts ->
        [create_ty_decl ts]
    | Ddata _ ->
        Printer.unsupportedDecl d "no algebraic types at this point"
    | Dparam ls ->
        let ls = if ls_equal ls ps_equ then ls else lsmap ls in
        [create_param_decl ls]
174 175
    | Dlogic ldl ->
        let conv (ls,ld) =
176 177
          let ls = if ls_equal ls ps_equ then ls else lsmap ls in
          let ul,e,close = open_ls_defn_cb ld in
178
          let vl = List.map (vs_monomorph ty_base kept) ul in
179 180 181
          let add acc u v = Mvs.add u (t_var v) acc in
          let vmap = List.fold_left2 add Mvs.empty ul vl in
          close ls vl (t_mono vmap e)
182 183
        in
        [create_logic_decl (List.map conv ldl)]
184
    | Dind (s, idl) ->
185
        let iconv (pr,f) = pr, t_mono Mvs.empty f in
186
        let conv (ls,il) = lsmap ls, List.map iconv il in
187
        [create_ind_decl s (List.map conv idl)]
188
    | Dprop (k,pr,f) ->
189
        [create_prop_decl k pr (t_mono Mvs.empty f)]
190
  in
191
  let add ls acc = create_param_decl ls :: acc in
192
  Sls.fold add !consts dl
193

194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
module OHTyl = Stdlib.OrderedHashedList(struct
  type t = ty
  let tag = ty_hash
end)

module Mtyl = Extmap.Make(OHTyl)

let ls_inst =
  (* FIXME? Skolem type constants are short-living but
      will stay in lsmap as long as the lsymbol is alive *)
  let lsmap = Wls.memoize 63 (fun _ -> ref Mtyl.empty) in
  fun ls tyl tyv ->
    let m = lsmap ls in
    let l = oty_cons tyl tyv in
    match Mtyl.find_opt l !m with
    | Some ls -> ls
    | None ->
        let nls = create_lsymbol (id_clone ls.ls_name) tyl tyv in
        m := Mtyl.add l nls !m;
        nls

215
let lsmap ty_base kept = Hls.memo 63 (fun ls ->
216 217 218 219 220 221 222 223
  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
  let ty_res = Opt.map pos ls.ls_value in
  if Opt.equal ty_equal ty_res ls.ls_value &&
     List.for_all2 ty_equal ty_arg ls.ls_args then ls
224
  else ls_inst ls ty_arg ty_res)
225 226 227

(* replace all non-kept types with ty_base *)
let monomorphise_task =
228 229 230 231 232 233 234 235 236
  Trans.on_meta_excl meta_base (fun base ->
  let ty_base, d_ts_base = match base with
    | Some [MAty ({ty_node = Tyapp (ts,[])} as ty)]
      when ts_equal ts ts_int || ts_equal ts ts_real ->
        ty, create_ty_decl ts
    | Some [MAty _] -> Loc.errorm
        "the \"enconding : base\" meta can only apply to `int' or `real'"
    | Some _ -> assert false
    | None -> ty_base, d_ts_base in
237 238
  Trans.on_tagged_ty meta_kept (fun kept ->
    let kept = Sty.add ty_type kept in
239 240 241
    let lsmap = lsmap ty_base kept in
    let decl = d_monomorph ty_base kept lsmap in
    Trans.decl decl (Task.add_decl None d_ts_base)))
242

243
(* replace type variables in a goal with fresh type constants *)
244 245 246
let ts_of_tv = Htv.memo 63 (fun tv ->
  create_tysymbol (id_clone tv.tv_name) [] None)

247 248 249 250
let monomorphise_goal = Trans.goal (fun pr f ->
  let stv = t_ty_freevars Stv.empty f in
  if Stv.is_empty stv then [create_prop_decl Pgoal pr f] else
  let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
251
    let ts = ts_of_tv tv in
252 253 254
    Mtv.add tv (ty_app ts []) mty, ts::ltv) stv (Mtv.empty,[]) in
  let f = t_ty_subst mty Mvs.empty f in
  List.fold_left
255
    (fun acc ts -> create_ty_decl ts :: acc)
256 257 258
    [create_prop_decl Pgoal pr f] ltv)

(* close by subtype the set of types tagged by meta_kept *)
259
let close_kept =
260 261 262
  Trans.on_tagged_ty meta_kept (fun kept ->
    let rec add acc ty = ty_fold add (Sty.add ty acc) ty in
    let kept' = Sty.fold (Util.flip add) kept kept in
263 264 265
    if kept == kept' then Trans.identity
    else
      let kept' = Sty.diff kept' kept in
266
      let fold ty acc = create_meta meta_kept [MAty ty] :: acc in
267
      Trans.add_tdecls (Sty.fold fold kept' []))
268

269
(* reconstruct a definition of an lsymbol or make a defining axiom *)
270 271 272 273 274 275
let defn_or_axiom ls f =
  match Decl.ls_defn_of_axiom f with
    | Some ld -> [create_logic_decl [ld]]
    | None ->
        let nm = ls.ls_name.id_string ^ "_def" in
        let pr = create_prsymbol (id_derive nm ls.ls_name) in
276
        [create_param_decl ls; create_prop_decl Paxiom pr f]