programs: fixed typing bug

parent 32772a8c
......@@ -34,15 +34,13 @@ let rec f4 (a:ref int) : unit variant { a } =
(** 5. The acid test:
partial application of a recursive function with effects *)
(* FIXME
let rec f5 (a b:ref int) variant { a } =
{ a >= 0 }
if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
{ result = old a + old b }
let test_f5 () =
{ x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
*)
{ x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old x }
end
......
......@@ -260,14 +260,15 @@ end = struct
| Tpure ty ->
Tpure (ty_inst ts ty)
| Tarrow (bl, c) ->
let s, bl = Util.map_fold_left (subst_binder ef ts) s bl in
let (ef, s), bl = Util.map_fold_left (subst_binder ts) (ef, s) bl in
Tarrow (bl, subst_type_c ef ts s c)
and subst_binder ef ts s pv =
and subst_binder ts (ef, s) pv =
let v' = subst_type_v ef ts s pv.pv_tv in
let s, vs' = subst_var ts s pv.pv_vs in
let pv' = create_pvsymbol (id_clone pv.pv_name) ~vs:vs' v' in
s, pv'
let ef' = Mpv.add pv (R.Rlocal pv') ef in
(ef', s), pv'
let tpure ty = Tpure ty
......
......@@ -130,6 +130,8 @@ and R : sig
val name_of : t -> ident
val print : Format.formatter -> t -> unit
end
and Sref : sig include Set.S with type elt = R.t end
and Mref : sig include Map.S with type key = R.t end
......
......@@ -1176,7 +1176,10 @@ and expr_desc gl env loc ty = function
let r = reference env r in
if occur_type_v r e1.expr_type_v then
errorm ~loc "this application would create an alias";
(* printf "e1 : %a@." print_type_v e1.expr_type_v; *)
(* printf "r = %a@." R.print r; *)
let c = apply_type_v_ref e1.expr_type_v r in
(* printf "c = %a@." print_type_c c; *)
make_apply loc e1 ty c
| IEfun (bl, t) ->
let env, bl = add_binders env bl in
......
......@@ -6,7 +6,9 @@ module P
let f1 () (a : ref int) = !a
let f2 (a : ref int) = f1 () a
parameter r : ref int
let f2 () = f1 () r
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