mlw_dty.ml 9.7 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2012                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Guillaume Melquiond                                                 *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* destructive types for program type inference *)

open Why3
24
open Util
25 26 27 28 29 30 31
open Ident
open Ty
open Term
open Ptree
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
32
open Mlw_module
33 34 35 36

type dity = dity_desc ref

and dity_desc = {
37
  uid : int;
38 39 40 41 42
  node: dity_node;
  ity : ity Lazy.t;
}

and dity_node =
43
  | Duvar of Ptree.ident (* user type variable *)
44
  | Dvar
Andrei Paskevich's avatar
Andrei Paskevich committed
45 46 47
  | Dskip of dity
  | Dits  of itysymbol * dity list * dreg list
  | Dts   of tysymbol  * dity list
48

49 50 51 52 53 54 55 56 57
and dreg = dreg_desc ref

and dreg_desc = {
  rid:   int;
  rity:  dity;
  ruser: bool;
  reg:   region Lazy.t;
}

58 59 60 61
let unique = let r = ref 0 in fun () -> incr r; !r

let create n l = ref { uid = unique (); node = n; ity = l }

62 63
let create_user_type_variable x =
  let id = id_user x.id x.id_loc in
64
  create (Duvar x) (lazy (ity_var (create_tvsymbol id)))
65 66 67

let create_type_variable () =
  let id = id_fresh "a" in
68
  create Dvar (lazy (ity_var (create_tvsymbol id)))
69 70 71

let ity_of_dity d = Lazy.force !d.ity

72 73
let reg_of_dreg d = Lazy.force !d.reg

Andrei Paskevich's avatar
Andrei Paskevich committed
74 75
let create_skip d = create (Dskip d) (lazy (ity_of_dity d))

76
let create_dreg ~user dity =
77 78 79
  ref { rid = unique (); rity = dity; ruser = user;
        reg = lazy (create_region (id_fresh "rho") (ity_of_dity dity)) }

80
let ts_app_real ts dl =
81
  create (Dts (ts, dl)) (lazy (ity_pur ts (List.map ity_of_dity dl)))
82

83 84 85 86 87 88 89 90 91
let its_app_real its dl rl =
  create (Dits (its, dl, rl))
    (lazy (ity_app its (List.map ity_of_dity dl) (List.map reg_of_dreg rl)))

let rec ity_inst_fresh ~user mv mr ity = match ity.ity_node with
  | Ityvar v ->
      mr, Mtv.find v mv
  | Itypur (s,tl) ->
      let mr,tl = Util.map_fold_left (ity_inst_fresh ~user mv) mr tl in
92
      mr, ts_app_real s tl
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
  | Ityapp (s,tl,rl) ->
      let mr,tl = Util.map_fold_left (ity_inst_fresh ~user mv) mr tl in
      let mr,rl = Util.map_fold_left (reg_refresh ~user mv) mr rl in
      mr, its_app_real s tl rl

and reg_refresh ~user mv mr r = match Mreg.find_opt r mr with
  | Some r ->
      mr, r
  | None ->
      let mr,ity = ity_inst_fresh ~user mv mr r.reg_ity in
      let reg = create_dreg ~user ity in
      Mreg.add r reg mr, reg

let its_app ~user s tl =
  let add m v t = Mtv.add v t m in
  let mv = try List.fold_left2 add Mtv.empty s.its_args tl
    with Invalid_argument _ ->
      raise (BadItyArity (s, List.length s.its_args, List.length tl))
  in
  match s.its_def with
  | Some ity ->
      snd (ity_inst_fresh ~user mv Mreg.empty ity)
  | None ->
      let _, rl =
        Util.map_fold_left (reg_refresh ~user mv) Mreg.empty s.its_regs in
      its_app_real s tl rl

let ts_app ts dl = match ts.ts_def with
  | Some ty ->
      let add m v t = Mtv.add v t m in
      let mv = try List.fold_left2 add Mtv.empty ts.ts_args dl
        with Invalid_argument _ ->
          raise (BadTypeArity (ts, List.length ts.ts_args, List.length dl)) in
      snd (ity_inst_fresh ~user:true mv Mreg.empty (ity_of_ty ty))
  | None ->
128
      ts_app_real ts dl
129

130 131 132
(* unification *)

let rec unify d1 d2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
133 134 135 136 137 138 139 140
  if !d1.uid <> !d2.uid then
  match !d1.node, !d2.node with
    | Dskip d1, _ ->
        unify d1 d2
    | _, Dskip d2 ->
        unify d1 d2
    | Dvar, Dvar ->
        d1 := !(create_skip d2)
141
    | Dvar, _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
142
        d1 := !d2
143 144
    | _, Dvar ->
        d2 := !d1
145
    | Duvar s1, Duvar s2 when s1.id = s2.id ->
Andrei Paskevich's avatar
Andrei Paskevich committed
146
        d1 := !d2
147 148 149 150
    | 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);
        List.iter2 unify dl1 dl2;
Andrei Paskevich's avatar
Andrei Paskevich committed
151 152
        List.iter2 unify_reg rl1 rl2;
        d1 := !d2
153
    | Dts (ts1, dl1), Dts (ts2, dl2) when ts_equal ts1 ts2 ->
154
        assert (List.length dl1 = List.length dl2);
Andrei Paskevich's avatar
Andrei Paskevich committed
155 156
        List.iter2 unify dl1 dl2;
        d1 := !d2
157 158 159
    | _ ->
        raise Exit

160 161
and unify_reg r1 r2 =
  if !r1.rid <> !r2.rid then
Andrei Paskevich's avatar
Andrei Paskevich committed
162 163 164 165 166 167 168 169
    if not !r1.ruser then begin
      unify !r1.rity !r2.rity;
      r1 := !r2
    end
    else if not !r2.ruser then begin
      unify !r1.rity !r2.rity;
      r2 := !r1
    end
170 171 172 173 174 175 176
    else begin (* two user regions *)
      if not (Lazy.lazy_is_val !r1.reg) then raise Exit;
      if not (Lazy.lazy_is_val !r2.reg) then raise Exit;
      if not (reg_equal (Lazy.force !r1.reg) (Lazy.force !r2.reg)) then
        raise Exit
    end

177 178 179 180
let unify d1 d2 =
  try unify d1 d2
  with Exit -> raise (TypeMismatch (ity_of_dity d1, ity_of_dity d2))

181 182 183 184
let ts_arrow =
  let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in
  Ty.create_tysymbol (Ident.id_fresh "arrow") v None

185 186 187 188 189 190
let rec vty_of_dity dity = match !dity.node with
  | Dts (ts, [d1; d2]) when ts_equal ts ts_arrow ->
      VTarrow (vty_arrow (vty_value (ity_of_dity d1)) (vty_of_dity d2))
  | _ ->
      VTvalue (vty_value (ity_of_dity dity))

191 192 193 194
type tvars = Sint.t (* a set of type variables *)
let empty_tvars = Sint.empty

let rec add_tvars tvs d = match !d.node with
195
  | Duvar _ | Dvar -> Sint.add !d.uid tvs
Andrei Paskevich's avatar
Andrei Paskevich committed
196
  | Dskip d -> add_tvars tvs d
197 198 199 200 201 202 203 204 205 206 207
  | Dits (_, dl, rl) ->
      let add_reg tvs r = add_tvars (Sint.add !r.rid tvs) !r.rity in
      List.fold_left add_reg (List.fold_left add_tvars tvs dl) rl
  | Dts (_, dl) -> List.fold_left add_tvars tvs dl

let specialize_scheme tvs dity =
  let hv = Hashtbl.create 17 in
  let huv = Hashtbl.create 17 in
  let hr = Hashtbl.create 17 in
  let rec specialize d = match !d.node with
    | Duvar _ | Dvar when Sint.mem !d.uid tvs -> d
Andrei Paskevich's avatar
Andrei Paskevich committed
208
    | Dskip d -> specialize d
209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232
    | Duvar id -> begin
        try Hashtbl.find huv id.id
        with Not_found ->
          let v = create_type_variable () in Hashtbl.add huv id.id v; v
      end
    | Dvar -> begin
        try Hashtbl.find hv !d.uid
        with Not_found ->
          let v = create_type_variable () in Hashtbl.add hv !d.uid v; v
      end
    | Dits (its, dl, rl) ->
        its_app_real its (List.map specialize dl) (List.map spec_reg rl)
    | Dts (ts, dl) -> ts_app_real ts (List.map specialize dl)
  and spec_reg r =
    if Sint.mem !r.rid tvs then r
    else if !r.ruser && Lazy.lazy_is_val !r.reg then r
    else
      try Hashtbl.find hr !r.rid
      with Not_found ->
        let v = create_dreg ~user:false (specialize !r.rity) in
        Hashtbl.add hr !r.rid v; v
  in
  specialize dity

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233 234 235 236 237 238 239 240 241 242 243
(* Specialization of symbols *)

let find_type_variable htv tv =
  try
    Htv.find htv tv
  with Not_found ->
    let dtv = create_type_variable () in
    Htv.add htv tv dtv;
    dtv

let rec dity_of_ity ~user htv hreg ity = match ity.ity_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
244 245 246 247
  | Ityvar tv ->
      assert (not user); find_type_variable htv tv
  | Itypur (ts, ityl) ->
      ts_app_real ts (List.map (dity_of_ity ~user htv hreg) ityl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
248 249 250 251 252 253 254 255 256 257 258 259 260
  | Ityapp (its, ityl, rl) ->
      its_app_real its (List.map (dity_of_ity ~user htv hreg) ityl)
        (List.map (dreg_of_reg ~user htv hreg) rl)

and dreg_of_reg ~user htv hreg r =
  try
    Hreg.find hreg r
  with Not_found ->
    let dreg = create_dreg ~user (dity_of_ity ~user htv hreg r.reg_ity) in
    Hreg.add hreg r dreg;
    dreg

let dity_of_vtv ~user htv hreg v = dity_of_ity ~user htv hreg v.vtv_ity
261

262
let specialize_vtvalue ~user vtv =
263
  let htv = Htv.create 17 in
264
  let hreg = Hreg.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265 266 267 268 269 270 271
  dity_of_vtv ~user htv hreg vtv

let specialize_pvsymbol pv =
  specialize_vtvalue ~user:true pv.pv_vtv

let make_arrow_type tyl ty =
  let arrow ty1 ty2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
272 273
    ts_app_real ts_arrow [ty1;ty2] in
(*
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
274
    create (Dts (ts_arrow, [ty1; ty2])) (lazy (invalid_arg "ity_of_dity")) in
Andrei Paskevich's avatar
Andrei Paskevich committed
275
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
276
  List.fold_right arrow tyl ty
277

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
278
let specialize_vtarrow vta =
279
  let htv = Htv.create 17 in
280
  let hreg = Hreg.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281 282 283 284 285 286 287
  let rec specialize a =
    let arg = dity_of_vtv ~user:false htv hreg a.vta_arg in
    let res = match a.vta_result with
      | VTvalue v -> dity_of_vtv ~user:false htv hreg v
      | VTarrow a1 -> specialize a1
    in
    make_arrow_type [arg] res
288
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289 290 291
  specialize vta

let specialize_psymbol ps = specialize_vtarrow ps.ps_vta
292 293 294

let specialize_plsymbol pls =
  let htv = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295 296 297
  let hreg = Hreg.create 17 in
  let args = List.map (dity_of_vtv ~user:false htv hreg) pls.pl_args in
  make_arrow_type args (dity_of_vtv ~user:false htv hreg pls.pl_value)
298

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
299
let dity_of_ty ~user htv hreg ty = dity_of_ity ~user htv hreg (ity_of_ty ty)
300 301 302

let specialize_lsymbol ls =
  let htv = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303
  let hreg = Hreg.create 17 in
304
  let ty = match ls.ls_value with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305 306
    | None -> dity_of_ity ~user:false htv hreg ity_bool
    | Some ty -> dity_of_ty ~user:false htv hreg ty
307
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
308 309
  let args = List.map (dity_of_ty ~user:false htv hreg) ls.ls_args in
  make_arrow_type args ty