programs: fixed typing error messages; more tests

parent 24626f5d
module M
use import module stdlib.Ref
parameter f : x:int -> {} unit writes a {}
end
module M
use import module stdlib.Ref
parameter f : x:int -> {} unit writes x {}
end
module M
use import module stdlib.Ref
parameter a : int
parameter f : x:int -> {} unit writes a {}
end
module M
use import module stdlib.Ref
parameter foo : int -> int
parameter f : x:int -> {} unit writes foo {}
end
......@@ -195,6 +195,12 @@ let check_mutable_type loc dty = match view_dty dty with
"this expression has type %a, but is expected to have a mutable type"
print_dty dty
let check_mutable_dtype_v loc = function
| DTpure dty -> check_mutable_type loc dty
| DTarrow _ ->
errorm ~loc
"this expression is a function, but is expected to have a mutable type"
let dreference env = function
| Qident id when Mstr.mem id.id env.locals ->
(* local variable *)
......@@ -204,9 +210,12 @@ let dreference env = function
| qid ->
let loc = Typing.qloc qid in
let sl = Typing.string_list_of_qualid [] qid in
let s, _ty = specialize_global loc sl env.uc in
(* TODO check_reference_type env.uc loc ty; *)
DRglobal s
try
let s, ty = specialize_global loc sl env.uc in
check_mutable_dtype_v loc ty;
DRglobal s
with Not_found ->
errorm ~loc "unbound variable %a" print_qualid qid
let dexception uc qid =
let sl = Typing.string_list_of_qualid [] qid in
......
theory A
type t
end
module P
use import module A
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
logic c : int
parameter foo : int -> int
parameter f : x:int -> {} unit writes x {}
let foo (t : array int) =
{ length t >= 1 && t[0] = 1 }
t[0 <- 1];
t[0] + 3
{ result = 3 }
let g (y:int) =
y
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