Commit 6cfcbf82 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: typing

parent 5006540b
......@@ -31,58 +31,62 @@ open Mlw_ty.T
open Mlw_expr
open Mlw_module
type dity = dity_desc ref
and dity_desc = {
uid : int;
node: dity_node;
ity : ity Lazy.t;
}
and dity_node =
| Duvar of Ptree.ident (* user type variable *)
| Dvar
| Dskip of dity
let create_user_tv =
let hs = Hashtbl.create 17 in
fun s -> try Hashtbl.find hs s with Not_found ->
let tv = create_tvsymbol (id_fresh s) in
Hashtbl.add hs s tv;
tv
type dity =
| Dvar of dvar ref
| Duvar of tvsymbol
| Dits of itysymbol * dity list * dreg list
| Dts of tysymbol * dity list
and dreg = dreg_desc ref
and dreg_desc = {
rid: int;
rity: dity;
ruser: bool;
reg: region Lazy.t;
}
let unique = let r = ref 0 in fun () -> incr r; !r
let create n l = ref { uid = unique (); node = n; ity = l }
and dvar =
| Dtvs of tvsymbol
| Dval of dity
and dreg =
| Rreg of region * dity
| Rureg of tvsymbol * dity * region Lazy.t
| Rvar of rvar ref
and rvar =
| Rtvs of tvsymbol * dity * region Lazy.t
| Rval of dreg
let rec ity_of_dity = function
| Dvar { contents = Dtvs tv } -> ity_var tv
| Dvar { contents = Dval dty } -> ity_of_dity dty
| Duvar tv -> ity_var tv
| Dits (its,dl,rl) ->
ity_app its (List.map ity_of_dity dl) (List.map reg_of_dreg rl)
| Dts (ts,dl) ->
ity_pur ts (List.map ity_of_dity dl)
and reg_of_dreg = function
| Rreg (r,_) -> r
| Rureg (_,_,r)
| Rvar { contents = Rtvs (_,_,r) } -> Lazy.force r
| Rvar { contents = Rval dreg } -> reg_of_dreg dreg
let create_user_type_variable x =
let id = id_user x.id x.id_loc in
create (Duvar x) (lazy (ity_var (create_tvsymbol id)))
Duvar (create_user_tv x.id)
let create_type_variable () =
let id = id_fresh "a" in
create Dvar (lazy (ity_var (create_tvsymbol id)))
let ity_of_dity d = Lazy.force !d.ity
let reg_of_dreg d = Lazy.force !d.reg
let create_skip d = create (Dskip d) (lazy (ity_of_dity d))
Dvar (ref (Dtvs (create_tvsymbol (id_fresh "a"))))
let create_dreg ~user dity =
ref { rid = unique (); rity = dity; ruser = user;
reg = lazy (create_region (id_fresh "rho") (ity_of_dity dity)) }
let id = id_fresh (if user then "urho" else "rho") in
let tv = create_tvsymbol id in
let reg = lazy (create_region id (ity_of_dity dity)) in
if user then Rureg (tv,dity,reg) else Rvar (ref (Rtvs (tv,dity,reg)))
let ts_app_real ts dl =
create (Dts (ts, dl)) (lazy (ity_pur ts (List.map ity_of_dity dl)))
let ts_app_real ts dl = Dts (ts, dl)
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 its_app_real its dl rl = Dits (its, dl, rl)
let rec ity_inst_fresh ~user mv mr ity = match ity.ity_node with
| Ityvar v ->
......@@ -129,50 +133,45 @@ let ts_app ts dl = match ts.ts_def with
(* unification *)
let rec unify d1 d2 =
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)
| Dvar, _ ->
d1 := !d2
| _, Dvar ->
d2 := !d1
| Duvar s1, Duvar s2 when s1.id = s2.id ->
d1 := !d2
| 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;
List.iter2 unify_reg rl1 rl2;
d1 := !d2
| Dts (ts1, dl1), Dts (ts2, dl2) when ts_equal ts1 ts2 ->
assert (List.length dl1 = List.length dl2);
List.iter2 unify dl1 dl2;
d1 := !d2
| _ ->
raise Exit
let rec occur_check tv = function
| Dvar { contents = Dval d } -> occur_check tv d
| Dvar { contents = Dtvs tv' } -> if tv_equal tv tv' then raise Exit
| Dits (_,dl,_) | Dts (_,dl) -> List.iter (occur_check tv) dl
| Duvar _ -> ()
let rec unify d1 d2 = match d1,d2 with
| Dvar { contents = Dval d1 }, d2
| d1, Dvar { contents = Dval d2 } ->
unify d1 d2
| Dvar ({ contents = Dtvs tv } as r), d
| d, Dvar ({ contents = Dtvs tv } as r) ->
occur_check tv d; r := Dval d
| Duvar tv1, Duvar tv2 when tv_equal tv1 tv2 -> ()
| 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;
List.iter2 unify_reg rl1 rl2
| Dts (ts1, dl1), Dts (ts2, dl2) when ts_equal ts1 ts2 ->
assert (List.length dl1 = List.length dl2);
List.iter2 unify dl1 dl2
| _ -> raise Exit
and unify_reg r1 r2 =
if !r1.rid <> !r2.rid then
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
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
let rec dity_of_reg = function
| Rvar { contents = Rval r } -> dity_of_reg r
| Rvar { contents = Rtvs (_,dity,_) }
| Rureg (_,dity,_) | Rreg (_,dity) -> dity
in
match r1,r2 with
| Rvar { contents = Rval r1 }, r2
| r1, Rvar { contents = Rval r2 } -> unify_reg r1 r2
| Rvar r, d | d, Rvar r ->
unify (dity_of_reg r1) (dity_of_reg r2);
r := Rval d
| Rureg (tv1,_,_), Rureg (tv2,_,_) when tv_equal tv1 tv2 -> ()
| Rreg (reg1,_), Rreg (reg2,_) when reg_equal reg1 reg2 -> ()
| _ -> raise Exit
let unify d1 d2 =
try unify d1 d2
......@@ -182,67 +181,67 @@ 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
let rec vty_of_dity dity = match !dity.node with
let rec vty_of_dity = function
| Dts (ts, [d1; d2]) when ts_equal ts ts_arrow ->
VTarrow (vty_arrow (vty_value (ity_of_dity d1)) (vty_of_dity d2))
| _ ->
| dity ->
VTvalue (vty_value (ity_of_dity dity))
type tvars = Sint.t (* a set of type variables *)
let empty_tvars = Sint.empty
type tvars = Stv.t (* a set of type variables *)
let empty_tvars = Stv.empty
let rec add_tvars tvs = function
| Dvar { contents = Dval d } -> add_tvars tvs d
| Dvar { contents = Dtvs tv } | Duvar tv -> Stv.add tv tvs
| Dits (_,dl,rl) ->
List.fold_left add_tvars_reg (List.fold_left add_tvars tvs dl) rl
| Dts (_, dl) ->
List.fold_left add_tvars tvs dl
let rec add_tvars tvs d = match !d.node with
| Duvar _ | Dvar -> Sint.add !d.uid tvs
| Dskip d -> add_tvars tvs d
| 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
and add_tvars_reg tvs = function
| Rvar { contents = Rval r } -> add_tvars_reg tvs r
| Rvar { contents = Rtvs (tv,dity,_) }
| Rureg (tv,dity,_) -> add_tvars (Stv.add tv tvs) dity
| Rreg _ -> tvs
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
| Dskip d -> specialize d
| 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
let htvs = Htv.create 17 in
let hreg = Htv.create 17 in
let rec specialize = function
| Dvar { contents = Dval d } -> specialize d
| Dvar { contents = Dtvs tv } | Duvar tv as d ->
if Stv.mem tv tvs then d else
begin try Htv.find htvs tv with Not_found ->
let v = create_type_variable () in
Htv.add htvs tv 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
| Dts (ts, dl) ->
ts_app_real ts (List.map specialize dl)
and spec_reg = function
| Rvar { contents = Rval r } -> spec_reg r
| Rvar { contents = Rtvs (tv,dity,_) }
| Rureg (tv,dity,_) as r ->
if Stv.mem tv tvs then r else
begin try Htv.find hreg tv with Not_found ->
let v = create_dreg ~user:false (specialize dity) in
Htv.add hreg tv v; v
end
| Rreg _ as r -> r
in
specialize dity
(* 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
| Ityvar tv ->
assert (not user); find_type_variable htv tv
assert (not user);
begin try Htv.find htv tv with Not_found ->
let dtv = create_type_variable () in
Htv.add htv tv dtv;
dtv
end
| Itypur (ts, ityl) ->
ts_app_real ts (List.map (dity_of_ity ~user htv hreg) ityl)
| Ityapp (its, ityl, rl) ->
......@@ -250,12 +249,10 @@ let rec dity_of_ity ~user htv hreg ity = match ity.ity_node with
(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
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
......@@ -268,11 +265,7 @@ let specialize_pvsymbol pv =
specialize_vtvalue ~user:true pv.pv_vtv
let make_arrow_type tyl ty =
let arrow ty1 ty2 =
ts_app_real ts_arrow [ty1;ty2] in
(*
create (Dts (ts_arrow, [ty1; ty2])) (lazy (invalid_arg "ity_of_dity")) in
*)
let arrow ty1 ty2 = ts_app_real ts_arrow [ty1;ty2] in
List.fold_right arrow tyl ty
let specialize_vtarrow vta =
......
......@@ -292,7 +292,7 @@ and expr_fun locals x bl (_, e1, _) =
l_expr = e1;
l_post = create_post res1 t_true; (* TODO *)
l_xpost = Mexn.empty; (* TODO *)
} in
} in
create_fun_defn (id_user x) lam
(** Type declaration *)
......
......@@ -16,14 +16,17 @@ module N
use import M
goal G1: f 41 = 42
type unit = ()
type tree 'a = Node 'a (forest 'a) | Leaf
with forest 'a = Cons (tree 'a) (forest 'a) | Nil
type ref 'b = {| ghost mutable contents : 'b |}
function id (tree 'c) : (tree 'c)
let h (x : tree 'd) = ((id x) : tree 'd)
let h x =
let bang y = y.contents in
let z = bang x + zero in
Node x Nil
end
(*
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment