Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

mlw_dty.ml 12.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-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 13 14 15 16 17 18 19 20 21

(* destructive types for program type inference *)

open Ident
open Ty
open Term
open Ptree
open Mlw_ty
open Mlw_ty.T
open Mlw_expr

Andrei Paskevich's avatar
Andrei Paskevich committed
22 23
type dity =
  | Dvar  of dvar ref
24
  | Duvar of tvsymbol * (* opaque *) bool
Andrei Paskevich's avatar
Andrei Paskevich committed
25 26
  | Dits  of itysymbol * dity list * dreg list
  | Dts   of tysymbol  * dity list
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30 31 32 33 34 35 36
and dvar =
  | Dtvs  of tvsymbol
  | Dval  of dity

and dreg =
  | Rreg  of region * dity
  | Rvar  of rvar ref

and rvar =
37
  | Rtvs  of tvsymbol * dity
Andrei Paskevich's avatar
Andrei Paskevich committed
38 39
  | Rval  of dreg

40 41
let create_user_type_variable x op =
  Duvar (Typing.create_user_tv x.id, op)
42 43

let create_type_variable () =
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  Dvar (ref (Dtvs (create_tvsymbol (id_fresh "a"))))
Andrei Paskevich's avatar
Andrei Paskevich committed
45

46
let create_dreg dity =
47
  Rvar (ref (Rtvs (create_tvsymbol (id_fresh "rho"), dity)))
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49
let ts_app_real ts dl = Dts (ts, dl)
50

Andrei Paskevich's avatar
Andrei Paskevich committed
51
let its_app_real its dl rl = Dits (its, dl, rl)
52

53
let rec ity_inst_fresh mv mr ity = match ity.ity_node with
54 55 56
  | Ityvar v ->
      mr, Mtv.find v mv
  | Itypur (s,tl) ->
57
      let mr,tl = Lists.map_fold_left (ity_inst_fresh mv) mr tl in
58
      mr, ts_app_real s tl
59
  | Ityapp (s,tl,rl) ->
60 61
      let mr,tl = Lists.map_fold_left (ity_inst_fresh mv) mr tl in
      let mr,rl = Lists.map_fold_left (reg_refresh mv) mr rl in
62 63
      mr, its_app_real s tl rl

64
and reg_refresh mv mr r = match Mreg.find_opt r mr with
65 66 67
  | Some r ->
      mr, r
  | None ->
68 69
      let mr,ity = ity_inst_fresh mv mr r.reg_ity in
      let reg = create_dreg ity in
70 71
      Mreg.add r reg mr, reg

72 73 74
let its_app s dl =
  let mv = try List.fold_right2 Mtv.add s.its_ts.ts_args dl Mtv.empty with
    | Invalid_argument _ -> raise (BadItyArity (s, List.length dl)) in
75 76
  match s.its_def with
  | Some ity ->
77
      snd (ity_inst_fresh mv Mreg.empty ity)
78
  | None ->
79
      let _,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
80 81 82 83 84 85
      its_app_real s dl rl

let ts_app s dl =
  let mv = try List.fold_right2 Mtv.add s.ts_args dl Mtv.empty with
    | Invalid_argument _ -> raise (BadTypeArity (s, List.length dl)) in
  match s.ts_def with
86
  | Some ty ->
87
      snd (ity_inst_fresh mv Mreg.empty (ity_of_ty ty))
88
  | None ->
89
      ts_app_real s dl
90

91 92 93 94 95 96 97
let rec dity_refresh = function
  | Dvar { contents = Dtvs _ } as dity -> dity
  | Dvar { contents = Dval dty } -> dity_refresh dty
  | Duvar _ as dity -> dity
  | Dits (its,dl,_) -> its_app its (List.map dity_refresh dl)
  | Dts (ts,dl) -> ts_app_real ts (List.map dity_refresh dl)

98 99 100 101 102 103 104
let rec opaque_tvs acc = function
  | Dvar { contents = Dtvs _ } -> acc
  | Dvar { contents = Dval dty } -> opaque_tvs acc dty
  | Duvar (tv,true) -> Stv.add tv acc
  | Duvar (_,false) -> acc
  | Dits (_,dl,_) | Dts (_,dl) -> List.fold_left opaque_tvs acc dl

105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
(* create ity *)

let ity_of_dity dity =
  let rec get_ity = function
    | Dvar { contents = Dtvs _ } ->
        Loc.errorm "undefined type variable"
    | Dvar { contents = Dval dty } ->
        get_ity dty
    | Duvar (tv,_) ->
        ity_var tv
    | Dits (its,dl,rl) ->
        ity_app its (List.map get_ity dl) (List.map get_reg rl)
    | Dts (ts,dl) ->
        ity_pur ts (List.map get_ity dl)
  and get_reg = function
    | Rreg (r,_) ->
        r
    | Rvar ({ contents = Rtvs (tv,dty) } as r) ->
        let reg = create_region (id_clone tv.tv_name) (get_ity dty) in
        r := Rval (Rreg (reg,dty));
        reg
    | Rvar { contents = Rval dreg } ->
        get_reg dreg
  in
  get_ity dity

131 132
(* unification *)

Andrei Paskevich's avatar
Andrei Paskevich committed
133 134 135
let rec occur_check tv = function
  | Dvar { contents = Dval d } -> occur_check tv d
  | Dits (_,dl,_) | Dts (_,dl) -> List.iter (occur_check tv) dl
136
  | Dvar { contents = Dtvs tv' } | Duvar (tv',_) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
137
      if tv_equal tv tv' then raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
138

Andrei Paskevich's avatar
Andrei Paskevich committed
139 140 141 142 143 144
let rec occur_check_reg tv = function
  | Dvar { contents = Dval d } -> occur_check_reg tv d
  | Dvar { contents = Dtvs _ } | Duvar _ -> ()
  | Dits (_,dl,rl) ->
      let rec check = function
        | Rvar { contents = Rval dreg } -> check dreg
145
        | Rvar { contents = Rtvs (tv',dity) } ->
Andrei Paskevich's avatar
Andrei Paskevich committed
146 147
            if tv_equal tv tv' then raise Exit;
            occur_check_reg tv dity
Andrei Paskevich's avatar
Andrei Paskevich committed
148
        | Rreg _ -> ()
Andrei Paskevich's avatar
Andrei Paskevich committed
149 150 151 152 153 154
      in
      List.iter (occur_check_reg tv) dl;
      List.iter check rl
  | Dts (_,dl) ->
      List.iter (occur_check_reg tv) dl

155
let rec unify ~weak d1 d2 = match d1,d2 with
Andrei Paskevich's avatar
Andrei Paskevich committed
156 157
  | Dvar { contents = Dval d1 }, d2
  | d1, Dvar { contents = Dval d2 } ->
158
      unify ~weak d1 d2
Andrei Paskevich's avatar
Andrei Paskevich committed
159 160 161
  | Dvar { contents = Dtvs tv1 },
    Dvar { contents = Dtvs tv2 } when tv_equal tv1 tv2 ->
      ()
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163 164
  | Dvar ({ contents = Dtvs tv } as r), d
  | d, Dvar ({ contents = Dtvs tv } as r) ->
      occur_check tv d; r := Dval d
165
  | Duvar (tv1,_), Duvar (tv2,_) when tv_equal tv1 tv2 -> ()
Andrei Paskevich's avatar
Andrei Paskevich committed
166 167 168
  | Dits (its1, dl1, rl1), Dits (its2, dl2, rl2) when its_equal its1 its2 ->
      assert (List.length rl1 = List.length rl2);
      assert (List.length dl1 = List.length dl2);
169 170
      List.iter2 (unify ~weak) dl1 dl2;
      if not weak then List.iter2 unify_reg rl1 rl2
Andrei Paskevich's avatar
Andrei Paskevich committed
171 172
  | Dts (ts1, dl1), Dts (ts2, dl2) when ts_equal ts1 ts2 ->
      assert (List.length dl1 = List.length dl2);
173
      List.iter2 (unify ~weak) dl1 dl2
Andrei Paskevich's avatar
Andrei Paskevich committed
174
  | _ -> raise Exit
175

176
and unify_reg r1 r2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
177 178
  let rec dity_of_reg = function
    | Rvar { contents = Rval r } -> dity_of_reg r
179
    | Rvar { contents = Rtvs (_,dity) }
180
    | Rreg (_,dity) -> dity
Andrei Paskevich's avatar
Andrei Paskevich committed
181 182 183
  in
  match r1,r2 with
    | Rvar { contents = Rval r1 }, r2
Andrei Paskevich's avatar
Andrei Paskevich committed
184 185
    | r1, Rvar { contents = Rval r2 } ->
        unify_reg r1 r2
186 187
    | Rvar { contents = Rtvs (tv1,_) },
      Rvar { contents = Rtvs (tv2,_) } when tv_equal tv1 tv2 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
188
        ()
189 190
    | Rvar ({ contents = Rtvs (tv,rd) } as r), d
    | d, Rvar ({ contents = Rtvs (tv,rd) } as r) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
191 192
        let dity = dity_of_reg d in
        occur_check_reg tv dity;
193
        unify ~weak:false rd dity;
Andrei Paskevich's avatar
Andrei Paskevich committed
194 195 196
        r := Rval d
    | Rreg (reg1,_), Rreg (reg2,_) when reg_equal reg1 reg2 -> ()
    | _ -> raise Exit
197

Andrei Paskevich's avatar
Andrei Paskevich committed
198 199
exception DTypeMismatch of dity * dity

200
let unify ~weak d1 d2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
201
  try unify ~weak d1 d2 with Exit -> raise (DTypeMismatch (d1,d2))
202

203 204
let unify_weak d1 d2 = unify ~weak:true d1 d2
let unify d1 d2 = unify ~weak:false d1 d2
205

206
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
207

208 209 210 211 212 213 214 215 216
let is_chainable dvty =
  let rec is_bool = function
    | Dvar { contents = Dval dty } -> is_bool dty
    | Dts (ts,_) -> ts_equal ts ts_bool
    | _ -> false in
  match dvty with
    | [t1;t2],t -> is_bool t && not (is_bool t1) && not (is_bool t2)
    | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
217
type tvars = dity list
218

Andrei Paskevich's avatar
Andrei Paskevich committed
219
let empty_tvars = []
Andrei Paskevich's avatar
Andrei Paskevich committed
220

221 222
let add_dity tvs dity = dity :: tvs
let add_dvty tvs (argl,res) = res :: List.rev_append argl tvs
Andrei Paskevich's avatar
Andrei Paskevich committed
223

224 225 226 227 228 229 230 231 232 233
let rec add_dity_vars tvs = function
  | Dvar { contents = Dtvs _ } as dity -> dity :: tvs
  | Dvar { contents = Dval dity } -> add_dity_vars tvs dity
  | Duvar _ as dity -> dity :: tvs
  | Dits (_,dl,_)
  | Dts (_,dl) -> List.fold_left add_dity_vars tvs dl

let add_dvty_vars tvs (argl,res) =
  add_dity_vars (List.fold_left add_dity_vars tvs argl) res

Andrei Paskevich's avatar
Andrei Paskevich committed
234 235
let tv_in_tvars tv tvs =
  try List.iter (occur_check tv) tvs; false with Exit -> true
236

Andrei Paskevich's avatar
Andrei Paskevich committed
237 238
let reg_in_tvars tv tvs =
  try List.iter (occur_check_reg tv) tvs; false with Exit -> true
239

240
let specialize_scheme tvs (argl,res) =
Andrei Paskevich's avatar
Andrei Paskevich committed
241 242 243 244
  let htvs = Htv.create 17 in
  let hreg = Htv.create 17 in
  let rec specialize = function
    | Dvar { contents = Dval d } -> specialize d
245
    | Dvar { contents = Dtvs tv } | Duvar (tv,_) as d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
246
        if tv_in_tvars tv tvs then d else
Andrei Paskevich's avatar
Andrei Paskevich committed
247 248 249 250
        begin try Htv.find htvs tv with Not_found ->
          let v = create_type_variable () in
          Htv.add htvs tv v; v
        end
251 252
    | Dits (its, dl, rl) ->
        its_app_real its (List.map specialize dl) (List.map spec_reg rl)
Andrei Paskevich's avatar
Andrei Paskevich committed
253 254
    | Dts (ts, dl) ->
        ts_app_real ts (List.map specialize dl)
255
  and spec_reg r = match r with
Andrei Paskevich's avatar
Andrei Paskevich committed
256
    | Rvar { contents = Rval r } -> spec_reg r
257
    | Rvar { contents = Rtvs (tv,dity) } ->
Andrei Paskevich's avatar
Andrei Paskevich committed
258
        if reg_in_tvars tv tvs then r else
Andrei Paskevich's avatar
Andrei Paskevich committed
259
        begin try Htv.find hreg tv with Not_found ->
260
          let v = create_dreg (specialize dity) in
Andrei Paskevich's avatar
Andrei Paskevich committed
261 262
          Htv.add hreg tv v; v
        end
263
    | Rreg _ -> r
264
  in
265
  List.map specialize argl, specialize res
266

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267 268
(* Specialization of symbols *)

269
let rec dity_of_ity htv hreg vars ity = match ity.ity_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
270
  | Ityvar tv ->
271
      assert (not (Stv.mem tv vars.vars_tv));
Andrei Paskevich's avatar
Andrei Paskevich committed
272 273 274 275 276
      begin try Htv.find htv tv with Not_found ->
        let dtv = create_type_variable () in
        Htv.add htv tv dtv;
        dtv
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
277
  | Itypur (ts, ityl) ->
278
      ts_app_real ts (List.map (dity_of_ity htv hreg vars) ityl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279
  | Ityapp (its, ityl, rl) ->
280 281
      its_app_real its (List.map (dity_of_ity htv hreg vars) ityl)
        (List.map (dreg_of_reg htv hreg vars) rl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282

283
and dreg_of_reg htv hreg vars r =
Andrei Paskevich's avatar
Andrei Paskevich committed
284
  try Hreg.find hreg r with Not_found ->
285 286
  let dity = dity_of_ity htv hreg vars r.reg_ity in
  let dreg = if reg_occurs r vars then Rreg (r,dity)
287
    else create_dreg dity in
Andrei Paskevich's avatar
Andrei Paskevich committed
288 289
  Hreg.add hreg r dreg;
  dreg
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290

291
let specialize_ity ity =
292
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
293
  dity_of_ity htv hreg ity.ity_vars ity
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
294

295
let specialize_pvsymbol pv = specialize_ity pv.pv_ity
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
296

297
let specialize_xsymbol xs = specialize_ity xs.xs_ity
Andrei Paskevich's avatar
Andrei Paskevich committed
298

299
let specialize_arrow vars aty =
300
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
301
  let conv pv = dity_of_ity htv hreg vars pv.pv_ity in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
302
  let rec specialize a =
303 304
    let argl = List.map conv a.aty_args in
    let narg,res = match a.aty_result with
305
      | VTvalue v -> [], dity_of_ity htv hreg vars v
306
      | VTarrow a -> specialize a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307
    in
308
    argl @ narg, res
309
  in
310
  specialize aty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
311

312
let specialize_psymbol ps =
313
  specialize_arrow ps.ps_vars ps.ps_aty
314 315

let specialize_plsymbol pls =
316
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
317
  let conv fd = dity_of_ity htv hreg vars_empty fd.fd_ity in
318
  List.map conv pls.pl_args, conv pls.pl_value
319

320
let dity_of_ty htv hreg vars ty =
321 322 323 324 325 326
  let rec pure ty = match ty.ty_node with
    | Tyapp (ts,tl) ->
        begin try ignore (restore_its ts); false
        with Not_found -> List.for_all pure tl end
    | Tyvar _ -> true in
  if not (pure ty) then raise Exit;
327
  dity_of_ity htv hreg vars (ity_of_ty ty)
328 329

let specialize_lsymbol ls =
330 331
  let htv = Htv.create 3 and hreg = Hreg.create 3 in
  let conv ty = dity_of_ty htv hreg vars_empty ty in
332
  let ty = Opt.get_def ty_bool ls.ls_value in
333
  List.map conv ls.ls_args, conv ty
Andrei Paskevich's avatar
Andrei Paskevich committed
334

335 336 337 338 339
let specialize_lsymbol ls =
  try specialize_lsymbol ls with Exit ->
    Loc.errorm "Function symbol `%a' can only be used in specification"
      Pretty.print_ls ls

Andrei Paskevich's avatar
Andrei Paskevich committed
340 341 342 343 344 345 346 347 348
(* Pretty-printing *)

let debug_print_reg_types = Debug.register_info_flag "print_reg_types"
  ~desc:"Print@ types@ of@ regions@ (mutable@ fields)."

let print_dity fmt dity =
  let protect_on x s = if x then "(" ^^ s ^^ ")" else s in
  let rec print_dity inn fmt = function
    | Dvar { contents = Dtvs tv }
349
    | Duvar (tv,_) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
        Pretty.print_tv fmt tv
    | Dvar { contents = Dval dty } ->
        print_dity inn fmt dty
    | Dts (ts,tl) when is_ts_tuple ts ->
        Format.fprintf fmt "(%a)"
          (Pp.print_list Pp.comma (print_dity false)) tl
    | Dts (ts,[]) ->
        Pretty.print_ts fmt ts
    | Dts (ts,tl) ->
        Format.fprintf fmt (protect_on inn "%a@ %a")
          Pretty.print_ts ts (Pp.print_list Pp.space (print_dity true)) tl
    | Dits (its,[],rl) ->
        Format.fprintf fmt (protect_on inn "%a@ <%a>")
          Mlw_pretty.print_its its (Pp.print_list Pp.comma print_dreg) rl
    | Dits (its,tl,rl) ->
        Format.fprintf fmt (protect_on inn "%a@ <%a>@ %a")
          Mlw_pretty.print_its its (Pp.print_list Pp.comma print_dreg) rl
          (Pp.print_list Pp.space (print_dity true)) tl
  and print_dreg fmt = function
    | Rreg (r,_) when Debug.test_flag debug_print_reg_types ->
        Format.fprintf fmt "@[%a:@,%a@]" Mlw_pretty.print_reg r
          Mlw_pretty.print_ity r.reg_ity
    | Rreg (r,_) ->
        Mlw_pretty.print_reg fmt r
374
    | Rvar { contents = Rtvs (tv,dity) }
Andrei Paskevich's avatar
Andrei Paskevich committed
375 376 377 378
      when Debug.test_flag debug_print_reg_types ->
        let r = create_region (id_clone tv.tv_name) Mlw_ty.ity_unit in
        Format.fprintf fmt "@[%a:@,%a@]" Mlw_pretty.print_reg r
          (print_dity false) dity
379
    | Rvar { contents = Rtvs (tv,_) } ->
Andrei Paskevich's avatar
Andrei Paskevich committed
380 381 382 383 384 385 386 387 388 389 390 391 392 393
        let r = create_region (id_clone tv.tv_name) Mlw_ty.ity_unit in
        Mlw_pretty.print_reg fmt r
    | Rvar { contents = Rval dreg } ->
        print_dreg fmt dreg
  in
  print_dity false fmt dity

let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | DTypeMismatch (t1,t2) ->
      Format.fprintf fmt "Type mismatch between %a and %a"
        print_dity t1 print_dity t2
  | _ -> raise exn
  end