Commit 6d269278 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: polymorphic recursion (EXPERIMENTAL)

parent 8ad5eebf
......@@ -40,9 +40,6 @@ and rvar =
let create_user_type_variable x op =
Duvar (Typing.create_user_tv x.id, op)
let create_type_variable () =
Dvar (ref (Dtvs (create_tvsymbol (id_fresh "a"))))
let create_dreg dity =
Rvar (ref (Rtvs (create_tvsymbol (id_fresh "rho"), dity)))
......@@ -88,13 +85,6 @@ let ts_app s dl =
| None ->
ts_app_real s dl
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)
let rec opaque_tvs acc = function
| Dvar { contents = Dtvs _ } -> acc
| Dvar { contents = Dval dty } -> opaque_tvs acc dty
......@@ -104,29 +94,27 @@ let rec opaque_tvs acc = function
(* 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
let rec ity_of_dity = function
| Dvar { contents = Dtvs _ } ->
Loc.errorm "undefined type variable"
| 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
| Rvar ({ contents = Rtvs (tv,dty) } as r) ->
let reg = create_region (id_clone tv.tv_name) (ity_of_dity dty) in
r := Rval (Rreg (reg,dty));
reg
| Rvar { contents = Rval dreg } ->
reg_of_dreg dreg
(* unification *)
......@@ -136,69 +124,105 @@ let rec occur_check tv = function
| Dvar { contents = Dtvs tv' } | Duvar (tv',_) ->
if tv_equal tv tv' then raise Exit
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
| Rvar { contents = Rtvs (tv',dity) } ->
if tv_equal tv tv' then raise Exit;
occur_check_reg tv dity
| Rreg _ -> ()
in
List.iter (occur_check_reg tv) dl;
List.iter check rl
| Dts (_,dl) ->
List.iter (occur_check_reg tv) dl
let rec unify ~weak d1 d2 = match d1,d2 with
let rec unify d1 d2 = match d1,d2 with
| Dvar { contents = Dval d1 }, d2
| d1, Dvar { contents = Dval d2 } ->
unify ~weak d1 d2
unify d1 d2
| Dvar { contents = Dtvs tv1 },
Dvar { contents = Dtvs tv2 } when tv_equal tv1 tv2 ->
()
| 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 ~weak) dl1 dl2;
if not weak then 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 ~weak) dl1 dl2
occur_check tv d;
r := Dval d
| Duvar (tv1,_), Duvar (tv2,_) when tv_equal tv1 tv2 ->
()
| Dits (its1,dl1,_), Dits (its2,dl2,_) when its_equal its1 its2 ->
List.iter2 unify dl1 dl2
| Dts (ts1,dl1), Dts (ts2,dl2) when ts_equal ts1 ts2 ->
List.iter2 unify dl1 dl2
| _ -> raise Exit
and unify_reg r1 r2 =
let rec dity_of_reg = function
| Rvar { contents = Rval r } -> dity_of_reg r
| Rvar { contents = Rtvs (_,dity) }
| Rreg (_,dity) -> dity
in
match r1,r2 with
| Rvar { contents = Rval r1 }, r2
| r1, Rvar { contents = Rval r2 } ->
unify_reg r1 r2
| Rvar { contents = Rtvs (tv1,_) },
Rvar { contents = Rtvs (tv2,_) } when tv_equal tv1 tv2 ->
()
| Rvar ({ contents = Rtvs (tv,rd) } as r), d
| d, Rvar ({ contents = Rtvs (tv,rd) } as r) ->
let dity = dity_of_reg d in
occur_check_reg tv dity;
unify ~weak:false rd dity;
r := Rval d
| Rreg (reg1,_), Rreg (reg2,_) when reg_equal reg1 reg2 -> ()
| _ -> raise Exit
exception DTypeMismatch of dity * dity
let unify d1 d2 =
try unify d1 d2 with Exit -> raise (DTypeMismatch (d1,d2))
(** Reunify regions *)
let dtvs_queue : dvar ref Queue.t = Queue.create ()
let create_type_variable () =
let r = ref (Dtvs (create_tvsymbol (id_fresh "a"))) in
Queue.add r dtvs_queue;
Dvar r
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)
let refresh_dtvs () =
let refr r = match !r with
| Dval dty -> r := Dval (dity_refresh dty)
| Dtvs _ -> () in
Queue.iter refr dtvs_queue;
Queue.clear dtvs_queue
let unify_queue : (dity * dity) Queue.t = Queue.create ()
let unify ?(weak=false) d1 d2 =
try unify ~weak d1 d2 with Exit -> raise (DTypeMismatch (d1,d2))
unify d1 d2;
if not weak then Queue.add (d1,d2) unify_queue
let rec reunify d1 d2 = match d1,d2 with
| Dvar { contents = Dval d1 }, d2
| d1, Dvar { contents = Dval d2 } ->
reunify d1 d2
| Dvar { contents = Dtvs tv1 }, Dvar { contents = Dtvs tv2 }
| Duvar (tv1,_), Duvar (tv2,_) ->
assert (tv_equal tv1 tv2)
| Dits (its1,dl1,rl1), Dits (its2,dl2,rl2) ->
assert (its_equal its1 its2);
List.iter2 reunify dl1 dl2;
List.iter2 unify_reg rl1 rl2
| Dts (ts1,dl1), Dts (ts2,dl2) ->
assert (ts_equal ts1 ts2);
List.iter2 reunify dl1 dl2
| _ -> assert false
and unify_reg r1 r2 = match r1,r2 with
| Rvar { contents = Rval r1 }, r2
| r1, Rvar { contents = Rval r2 } ->
unify_reg r1 r2
| Rvar { contents = Rtvs (tv1,_) },
Rvar { contents = Rtvs (tv2,_) } when tv_equal tv1 tv2 ->
()
| Rvar ({ contents = Rtvs (_,d1) } as r),
(Rvar { contents = Rtvs (_,d2) } as d)
| Rvar ({ contents = Rtvs (_,d1) } as r), (Rreg (_,d2) as d)
| (Rreg (_,d1) as d), Rvar ({ contents = Rtvs (_,d2) } as r) ->
reunify d1 d2;
r := Rval d
| Rreg _, Rreg _ -> ()
(* we don't check whether the regions are the same,
because we won't have a good location for the error.
Let the core API raise the exception later. *)
let reunify_regs () =
Queue.iter (fun (d1,d2) -> reunify d1 d2) unify_queue;
Queue.clear unify_queue
let ity_of_dity dity =
if not (Queue.is_empty unify_queue) then begin
refresh_dtvs ();
reunify_regs ()
end;
ity_of_dity dity
(** Arrow types *)
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
......@@ -218,46 +242,38 @@ let empty_tvars = []
let add_dity tvs dity = dity :: tvs
let add_dvty tvs (argl,res) = res :: List.rev_append argl tvs
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
let tv_in_tvars tv tvs =
try List.iter (occur_check tv) tvs; false with Exit -> true
let reg_in_tvars tv tvs =
try List.iter (occur_check_reg tv) tvs; false with Exit -> true
let specialize_scheme tvs (argl,res) =
let htvs = Htv.create 17 in
let hreg = Htv.create 17 in
let rec specialize = function
| Dvar { contents = Dval d } -> specialize d
| Dvar { contents = Dval d } ->
specialize d
| Dvar { contents = Dtvs tv } | Duvar (tv,_) as d ->
if tv_in_tvars 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
(* can't use d directly, might differ in regions *)
if tv_in_tvars tv tvs then unify ~weak:true v d;
Htv.add htvs tv v;
v
end
| Dits (its, dl, rl) ->
| Dits (its,dl,rl) ->
its_app_real its (List.map specialize dl) (List.map spec_reg rl)
| Dts (ts, dl) ->
| Dts (ts,dl) ->
ts_app_real ts (List.map specialize dl)
and spec_reg r = match r with
| Rvar { contents = Rval r } -> spec_reg r
and spec_reg = function
| Rvar { contents = Rval r } ->
spec_reg r
| Rvar { contents = Rtvs (tv,dity) } ->
if reg_in_tvars tv tvs then r else
begin try Htv.find hreg tv with Not_found ->
let v = create_dreg (specialize dity) in
Htv.add hreg tv v; v
Htv.add hreg tv v;
v
end
| Rreg _ -> r
| Rreg _ as r ->
r
in
List.map specialize argl, specialize res
......
......@@ -27,15 +27,12 @@ type tvars (* a set of type variables *)
val empty_tvars: tvars
val add_dity: tvars -> dity -> tvars
val add_dvty: tvars -> dvty -> tvars
val add_dvty_vars: tvars -> dvty -> tvars (* add only variables *)
val create_type_variable: unit -> dity
val create_user_type_variable: Ptree.ident -> (* opaque *) bool -> dity
val its_app: itysymbol -> dity list -> dity
val ts_app: tysymbol -> dity list -> dity
val dity_refresh: dity -> dity (* refresh regions *)
val opaque_tvs: Stv.t -> dity -> Stv.t
val is_chainable: dvty -> bool (* non-bool * non-bool -> bool *)
......@@ -46,7 +43,7 @@ val unify: ?weak:bool -> dity -> dity -> unit
(* when [weak] is true, don't unify regions *)
val ity_of_dity: dity -> ity
(* only use once unification is done *)
(* only use once all unification is done *)
val specialize_scheme: tvars -> dvty -> dvty
......
......@@ -175,15 +175,15 @@ let rec extract_labels labs loc e = match e.Ptree.expr_desc with
labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
| e -> labs, loc, e
let rec find_top_pty e = match e.Ptree.expr_desc with
| Ptree.Enamed (_, e) -> find_top_pty e
| Ptree.Ecast (_, pty) -> Some pty
| _ -> None
(* Hack alert. Since the result type in "let [rec] fn x y : ty = ..."
is moved to Ecast and then usually lost in destructive unification,
we try to preserve opacity annotations by moving them to binders. *)
let pass_opacity (e,_) bl =
let rec find e = match e.Ptree.expr_desc with
| Ptree.Ecast (_, pty) -> Some pty
| Ptree.Enamed (_, e) -> find e
| _ -> None in
match find e with
let pass_opacity (e,_) bl = match find_top_pty e with
| Some pty ->
let ht = Hstr.create 3 in
let rec fill = function
......@@ -277,6 +277,12 @@ let add_mono id dvty denv =
let locals = Mstr.add id.id (None, dvty) denv.locals in
{ denv with locals = locals; tvars = add_dvty denv.tvars dvty }
let add_rec_mono id dvty denv =
(* fix type variables but not regions *)
let tvars = add_dvty denv.tvars dvty in
let locals = Mstr.add id.id (Some tvars, dvty) denv.locals in
{ denv with locals = locals; tvars = tvars }
let add_var id dity denv = add_mono id ([],dity) denv
let specialize_qualid uc p = match uc_find_ps uc p with
......@@ -698,224 +704,37 @@ and de_desc denv loc = function
and dletrec ~top denv fdl =
(* add all functions into the environment *)
let add_one denv (_,id,_,bl,_) =
let argl = List.map (fun _ -> create_type_variable ()) bl in
let dvty = argl, create_type_variable () in
add_mono id dvty denv, dvty in
let add_one denv (_,id,_,bl,tr) =
let _,argl,tyl = dbinders denv (pass_opacity tr bl) in
let rpty = find_top_pty (fst tr) in
let dvty = tyl, match rpty with
| Some pty -> dity_of_pty denv pty
| None -> create_type_variable () in
let check (_,_,_,apty) = apty = None in
let denv = if rpty = None || List.exists check bl
then add_rec_mono id dvty denv
else add_poly id dvty denv in
denv, (argl, dvty) in
let denv, dvtyl = Lists.map_fold_left add_one denv fdl in
(* then unify the binders *)
let bind_one (_,_,_,bl,tr) (argl,res) =
let denv,bl,tyl = dbinders denv (pass_opacity tr bl) in
List.iter2 unify argl tyl;
denv,bl,tyl,res in
let denvl = List.map2 bind_one fdl dvtyl in
(* then type-check the bodies *)
let type_one (loc,id,gh,_,tr) (denv,bl,tyl,tyv) =
let type_one (loc,id,gh,bl,tr) (argl,((tyl,tyv) as dvty)) =
let add denv (_,id,_,_) dity = match id with
| Some id -> add_var id dity denv
| None -> denv in
let denv = List.fold_left2 add denv bl tyl in
let id, gh = add_lemma_label ~top id gh in
let tr, (argl, res) = dtriple denv tr in
if argl <> [] then errorm ~loc
let tr, (badl, res) = dtriple denv tr in
if badl <> [] then errorm ~loc
"The body of a recursive function must be a first-order value";
unify_loc unify loc tyv res;
id, gh, (tyl, tyv), bl, tr in
List.map2 type_one fdl denvl
id, gh, dvty, argl, tr in
List.map2 type_one fdl dvtyl
and dtriple denv (e, sp) =
let e = dexpr denv e in
let sp = dspec denv.uc sp in
(e, sp), e.de_type
(** stage 1.5 *)
(* After the stage 1, we know precisely the types of all binders
and program expressions. However, the regions in recursive functions
might be over-unified, since we do not support recursive polymorphism.
For example, the letrec below will require that a and b share the region.
let rec main a b : int = if !a = 0 then main b a else 5
To avoid this, we retype the whole dexpr generated at the stage 1.
Every binder keeps its previous type with all regions refreshed.
Every non-arrow expression keeps its previous type modulo regions.
When we type-check recursive functions, we add them to the denv
as polymorphic, but freeze every type variable. In other words,
only regions are specialized during recursive calls. *)
let add_preid id dity denv =
add_var (mk_id (Ident.preid_name id) Loc.dummy_position) dity denv
let rec rpattern denv pp dity = match pp with
| PPwild -> denv
| PPvar id -> add_preid id dity denv
| PPlapp (ls, ppl) -> rpat_app denv (specialize_lsymbol ls) ppl dity
| PPpapp (pl, ppl) -> rpat_app denv (specialize_plsymbol pl) ppl dity
| PPor (pp1, pp2) -> rpattern (rpattern denv pp1 dity) pp2 dity
| PPas (pp1, id) -> add_preid id dity (rpattern denv pp1 dity)
and rpat_app denv (argl,res) ppl dity =
unify res dity;
List.fold_left2 rpattern denv ppl argl
let rbinders denv bl =
let rbinder (id,gh,dity) (denv,bl,tyl) =
let dity = dity_refresh dity in
add_var id dity denv, (id,gh,dity)::bl, dity::tyl in
List.fold_right rbinder bl (denv,[],[])
let rec rtype_c denv (tyv, sp) =
let tyv, dvty = rtype_v denv tyv in (tyv, sp), dvty
and rtype_v denv = function
| DSpecV dity ->
let dity = dity_refresh dity in
DSpecV dity, ([],dity)
| DSpecA (bl,tyc) ->
let denv,bl,tyl = rbinders denv bl in
let tyc,(argl,res) = rtype_c denv tyc in
DSpecA (bl,tyc), (tyl @ argl,res)
let rec rexpr denv ({ de_type = (argl,res) } as de) =
let desc, dvty = re_desc denv de in
let de = { de with de_desc = desc; de_type = dvty } in
if argl = [] then expected_type ~weak:true de (dity_refresh res);
de
and re_desc denv de = match de.de_desc with
| DElocal x as d ->
let dvty = match Mstr.find x denv.locals with
| Some tvs, dvty -> specialize_scheme tvs dvty
| None, dvty -> dvty in
d, dvty
| DEglobal_pv pv as d -> d, ([],specialize_pvsymbol pv)
| DEglobal_ps ps as d -> d, specialize_psymbol ps
| DEglobal_pl pl as d -> d, specialize_plsymbol pl
| DEglobal_ls ls as d -> d, specialize_lsymbol ls
| DEconstant _ as d -> d, de.de_type
| DEapply (e1, el) ->
let e1 = rexpr denv e1 in
let el = List.map (rexpr denv) el in
de_app de.de_loc e1 el
| DEfun (bl, (e1, sp)) ->
let denv, bl, tyl = rbinders denv bl in
let e1 = rexpr denv e1 in
let argl, res = e1.de_type in
DEfun (bl, (e1, sp)), (tyl @ argl, res)
| DElet (id, gh, e1, e2) ->
let e1 = rexpr denv e1 in
let denv = match e1.de_desc with
| DEfun _ -> add_poly id e1.de_type denv
| _ -> add_mono id e1.de_type denv in
let e2 = rexpr denv e2 in
DElet (id, gh, e1, e2), e2.de_type
| DEletrec (fdl, e1) ->
let fdl = rletrec denv fdl in
let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
let denv = List.fold_left add_one denv fdl in
let e1 = rexpr denv e1 in
DEletrec (fdl, e1), e1.de_type
| DEassign (pl, e1, e2) ->
let e1 = rexpr denv e1 in
let e2 = rexpr denv e2 in
(* no need to weakly reunify e1.pl with e2,
since both dexprs retain their "pure" types *)
DEassign (pl, e1, e2), ([], dity_unit)
| DEif (e1, e2, e3) ->
let e1 = rexpr denv e1 in
expected_type e1 dity_bool;
let e2 = rexpr denv e2 in
let e3 = rexpr denv e3 in
let res = create_type_variable () in
expected_type e2 res;
expected_type e3 res;
DEif (e1, e2, e3), e2.de_type
| DElazy (op, e1, e2) ->
let e1 = rexpr denv e1 in
let e2 = rexpr denv e2 in
expected_type e1 dity_bool;
expected_type e2 dity_bool;
DElazy (op, e1, e2), ([], dity_bool)
| DEnot e1 ->
let e1 = rexpr denv e1 in
expected_type e1 dity_bool;
DEnot e1, ([], dity_bool)
| DEmatch (e1, bl) ->
let e1 = rexpr denv e1 in
let res = create_type_variable () in
let ety = create_type_variable () in
expected_type e1 ety;
let branch (pp,e) =
let denv = rpattern denv pp ety in
let e = rexpr denv e in
expected_type e res;
pp, e in
DEmatch (e1, List.map branch bl), ([], res)
| DEraise (xs, e1) ->
let e1 = rexpr denv e1 in
expected_type e1 (specialize_xsymbol xs);
DEraise (xs, e1), ([], create_type_variable ())
| DEtry (e1, cl) ->
let res = create_type_variable () in
let e1 = rexpr denv e1 in
expected_type e1 res;
let branch (xs, pp, e) =
let ety = specialize_xsymbol xs in
let denv = rpattern denv pp ety in
let e = rexpr denv e in
expected_type e res;
xs, pp, e in
DEtry (e1, List.map branch cl), e1.de_type
| DEabsurd as d ->
d, ([], create_type_variable ())
| DEassert _ as d ->
d, ([], dity_unit)
| DEabstract (e1, sp) ->
let e1 = rexpr denv e1 in
DEabstract (e1, sp), e1.de_type
| DEmark (id, e1) ->
let e1 = rexpr denv e1 in
DEmark (id, e1), e1.de_type
| DEghost e1 ->
let e1 = rexpr denv e1 in
DEghost e1, e1.de_type
| DEany tyc ->
let tyc, dvty = rtype_c denv tyc in
DEany tyc, dvty
| DEloop (var, inv, e1) ->
let e1 = rexpr denv e1 in
expected_type e1 dity_unit;
DEloop (var, inv, e1), e1.de_type
| DEfor (id, efrom, dir, eto, inv, e1) ->
let efrom = rexpr denv efrom in
let eto = rexpr denv eto in
let denv = add_var id dity_int denv in
let e1 = rexpr denv e1 in
expected_type efrom dity_int;
expected_type eto dity_int;
expected_type e1 dity_unit;
DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
and rletrec denv fdl =
(* add all functions into the environment *)
let add_one denv (id,_,(argl,res),_,_) =
let dvty = List.map dity_refresh argl, dity_refresh res in
let tvars = add_dvty_vars denv.tvars dvty in
let locals = Mstr.add id.id (Some tvars, dvty) denv.locals in
{ denv with locals = locals; tvars = tvars } in
let denv = List.fold_left add_one denv fdl in
(* then type-check the bodies *)
let type_one (id,gh,_,bl,(e,sp)) =
let denv,bl,tyl = rbinders denv bl in
let e = rexpr denv e in
let argl, tyv = e.de_type in
assert (argl = []);
id, gh, (tyl, tyv), bl, (e, sp) in
List.map type_one fdl
let dexpr denv e =
rexpr denv (dexpr denv e)
let dletrec ~top denv fdl =
rletrec denv (dletrec ~top denv fdl)