Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

fields can be omitted in effect expressions when not ambiguous

parent 084f446e
module M
parameter f : x:int -> {} unit writes 1 {}
end
module M
parameter f : x:int -> {} unit writes x {}
end
module M
type t = {| mutable a : int; mutable b : int |}
parameter f : x:t -> {} unit writes x {}
end
......@@ -3,7 +3,7 @@ module M
use import int.Int
use import module stdlib.Ref
parameter incr : x:ref int -> { } unit writes x.contents { x = old x + 1 }
parameter incr : x:ref int -> { } unit writes x { x = old x + 1 }
parameter x : ref int
......
......@@ -8,7 +8,7 @@ parameter t : ref int
parameter m : a:int -> b:int ->
{ }
unit reads t.contents raises Exception
unit reads t raises Exception
{ true } | Exception -> { true }
let test () =
......
......@@ -7,7 +7,7 @@ module M
parameter r : ref int
parameter f1 : y:int ->
{} unit writes r.contents { q1 r (old r) y }
{} unit writes r { q1 r (old r) y }
let g1 () = {} f1 !r { q1 r (old r) (old r) }
......@@ -15,7 +15,7 @@ module M
logic q int int int
parameter f : t:ref int -> x:int ->
{} unit writes t.contents { q t (old t) x }
{} unit writes t { q t (old t) x }
let g (t:ref int) =
{}
......
......@@ -49,7 +49,7 @@ let p11a () = {} let a = (fsucc 1) in a + a { result = 4 }
(* function with a post-condition and side-effects *)
parameter incrx : unit -> { } unit writes x.contents { x = (old x) + 1 }
parameter incrx : unit -> { } unit writes x { x = (old x) + 1 }
let p12 () = { x = 0 } incrx () { x = 1 }
......@@ -59,7 +59,7 @@ let p13a () = {} incrx (incrx ()) { x = (old x) + 2 }
(* function with side-effects, result and post-condition *)
parameter incrx2 : unit -> { } int writes x.contents { x = old x + 1 and result = x }
parameter incrx2 : unit -> { } int writes x { x = old x + 1 and result = x }
let p14 () = { x = 0 } incrx2 () { result = 1 }
......
......@@ -10,7 +10,7 @@ module M
parameter set_and_test_zero :
v:int ->
{}
bool writes x.contents
bool writes x
{ x = v and if result=True then x = 0 else x <> 0 }
let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
......@@ -18,7 +18,7 @@ module M
parameter set_and_test_nzero :
v:int ->
{}
bool writes x.contents
bool writes x
{ x = v and if result=True then x <> 0 else x = 0 }
let p2 (y:ref int) =
......
......@@ -5,7 +5,7 @@ use import module stdlib.Ref
parameter x : ref int
parameter f : unit -> { } unit writes x.contents { x = 1 - old x }
parameter f : unit -> { } unit writes x { x = 1 - old x }
let p () =
begin
......
......@@ -714,7 +714,7 @@ let rec type_effect_term env { pp_loc = loc; pp_desc = d } = match d with
| _ ->
errorm ~loc "unsupported effect syntax"
let iuregion env { pp_loc = loc; pp_desc = d } = match d with
let iuregion env ({ pp_loc = loc; pp_desc = d } as t) = match d with
| PPapp (f, [t]) ->
let th = effect_uc env.i_uc in
let ls, _, _ = Typing.specialize_lsymbol f th in
......@@ -742,7 +742,24 @@ let iuregion env { pp_loc = loc; pp_desc = d } = match d with
errorm ~loc "not a record field"
end
| _ ->
errorm ~loc "unsupported effect syntax"
let ty = type_effect_term env t in
let not_mutable () = errorm ~loc
"this expression has type %a,@ but is expected to have a mutable type@]"
Pretty.print_ty ty
in
begin match ty.ty_node with
| Ty.Tyapp (ts, tyl) ->
let mt = get_mtsymbol ts in
let n = mt.mt_regions in
if n = 0 then not_mutable ();
if n > 1 then errorm ~loc
"ambiguous effect term (more than one region)";
let r = regions_tyapp ts mt.mt_regions tyl in
List.nth r 0
| _ ->
not_mutable ()
end
(***
| Qident id when Mstr.mem id.id env.locals ->
(* local variable *)
......
......@@ -6,7 +6,7 @@ module TestRef
let f1 (x : ref int) (y : ref int) =
{}
x := !x + 1;
x := 1;
y := 2
{ x = 1 and y = 2 }
......@@ -20,7 +20,7 @@ module TestRef
parameter a : ref int
parameter havoc : unit -> {} unit writes a.contents {a=1}
parameter havoc : unit -> {} unit writes a {a=1}
let foo () = { a=0 } havoc(); 1 { a=1 and result=1 }
......@@ -31,8 +31,14 @@ module TestRef
provoque "undefined type variable" (la rgion)
problme : comment faire l'infrence du type de n
*)
type t2 = {| mutable fa : int; mutable fb : int |}
parameter ft2 : x:t2 -> {} unit writes x.fa x.fb {}
end
(***
module Array
type t
......@@ -43,8 +49,6 @@ module Array
end
(***
module TestArray
use import int.Int
......
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