I removed the annotation for the variable that iterates over collections.
for x in set s block { ... } // now for x : t in set s block { ... } // before
This commit is contained in:
parent
8d3fbf73f9
commit
02f58ee212
@ -432,8 +432,6 @@ and for_collect = {
|
|||||||
kwd_for : kwd_for;
|
kwd_for : kwd_for;
|
||||||
var : variable;
|
var : variable;
|
||||||
bind_to : (arrow * variable) option;
|
bind_to : (arrow * variable) option;
|
||||||
colon : colon;
|
|
||||||
elt_type : type_expr;
|
|
||||||
kwd_in : kwd_in;
|
kwd_in : kwd_in;
|
||||||
collection : collection;
|
collection : collection;
|
||||||
expr : expr;
|
expr : expr;
|
||||||
|
@ -422,8 +422,6 @@ and for_collect = {
|
|||||||
kwd_for : kwd_for;
|
kwd_for : kwd_for;
|
||||||
var : variable;
|
var : variable;
|
||||||
bind_to : (arrow * variable) option;
|
bind_to : (arrow * variable) option;
|
||||||
colon : colon;
|
|
||||||
elt_type : type_expr;
|
|
||||||
kwd_in : kwd_in;
|
kwd_in : kwd_in;
|
||||||
collection : collection;
|
collection : collection;
|
||||||
expr : expr;
|
expr : expr;
|
||||||
|
@ -647,19 +647,17 @@ for_loop:
|
|||||||
block = $5}
|
block = $5}
|
||||||
in For (ForInt {region; value})
|
in For (ForInt {region; value})
|
||||||
}
|
}
|
||||||
| For var option(arrow_clause) COLON type_expr
|
| For var option(arrow_clause)
|
||||||
In collection expr block {
|
In collection expr block {
|
||||||
let region = cover $1 $9.region in
|
let region = cover $1 $7.region in
|
||||||
let value = {
|
let value = {
|
||||||
kwd_for = $1;
|
kwd_for = $1;
|
||||||
var = $2;
|
var = $2;
|
||||||
bind_to = $3;
|
bind_to = $3;
|
||||||
colon = $4;
|
kwd_in = $4;
|
||||||
elt_type = $5;
|
collection = $5;
|
||||||
kwd_in = $6;
|
expr = $6;
|
||||||
collection = $7;
|
block = $7}
|
||||||
expr = $8;
|
|
||||||
block = $9}
|
|
||||||
in For (ForCollect {region; value})}
|
in For (ForCollect {region; value})}
|
||||||
|
|
||||||
collection:
|
collection:
|
||||||
|
@ -359,13 +359,11 @@ and print_var_assign buffer {value; _} =
|
|||||||
print_expr buffer expr
|
print_expr buffer expr
|
||||||
|
|
||||||
and print_for_collect buffer ({value; _} : for_collect reg) =
|
and print_for_collect buffer ({value; _} : for_collect reg) =
|
||||||
let {kwd_for; var; bind_to; colon; elt_type;
|
let {kwd_for; var; bind_to;
|
||||||
kwd_in; collection; expr; block} = value in
|
kwd_in; collection; expr; block} = value in
|
||||||
print_token buffer kwd_for "for";
|
print_token buffer kwd_for "for";
|
||||||
print_var buffer var;
|
print_var buffer var;
|
||||||
print_bind_to buffer bind_to;
|
print_bind_to buffer bind_to;
|
||||||
print_token buffer colon ":";
|
|
||||||
print_type_expr buffer elt_type;
|
|
||||||
print_token buffer kwd_in "in";
|
print_token buffer kwd_in "in";
|
||||||
print_collection buffer collection;
|
print_collection buffer collection;
|
||||||
print_expr buffer expr;
|
print_expr buffer expr;
|
||||||
@ -1221,23 +1219,19 @@ and pp_var_assign buffer ~pad:(_,pc) asgn =
|
|||||||
|
|
||||||
and pp_for_collect buffer ~pad:(_,pc) collect =
|
and pp_for_collect buffer ~pad:(_,pc) collect =
|
||||||
let () =
|
let () =
|
||||||
let pad = mk_pad 4 0 pc in
|
let pad = mk_pad 3 0 pc in
|
||||||
match collect.bind_to with
|
match collect.bind_to with
|
||||||
None ->
|
None ->
|
||||||
pp_ident buffer ~pad collect.var
|
pp_ident buffer ~pad collect.var
|
||||||
| Some (_, var) ->
|
| Some (_, var) ->
|
||||||
pp_var_binding buffer ~pad (collect.var, var) in
|
pp_var_binding buffer ~pad (collect.var, var) in
|
||||||
let () =
|
let () =
|
||||||
let _, pc as pad = mk_pad 4 1 pc in
|
let _, pc as pad = mk_pad 3 1 pc in
|
||||||
pp_node buffer ~pad "<element type>";
|
|
||||||
pp_type_expr buffer ~pad:(mk_pad 1 0 pc) collect.elt_type in
|
|
||||||
let () =
|
|
||||||
let _, pc as pad = mk_pad 4 2 pc in
|
|
||||||
pp_node buffer ~pad "<collection>";
|
pp_node buffer ~pad "<collection>";
|
||||||
pp_collection buffer ~pad:(mk_pad 2 0 pc) collect.collection;
|
pp_collection buffer ~pad:(mk_pad 2 0 pc) collect.collection;
|
||||||
pp_expr buffer ~pad:(mk_pad 1 0 pc) collect.expr in
|
pp_expr buffer ~pad:(mk_pad 1 0 pc) collect.expr in
|
||||||
let () =
|
let () =
|
||||||
let pad = mk_pad 4 3 pc in
|
let pad = mk_pad 3 2 pc in
|
||||||
let statements = collect.block.value.statements in
|
let statements = collect.block.value.statements in
|
||||||
pp_node buffer ~pad "<statements>";
|
pp_node buffer ~pad "<statements>";
|
||||||
pp_statements buffer ~pad statements
|
pp_statements buffer ~pad statements
|
||||||
|
@ -2,17 +2,17 @@
|
|||||||
|
|
||||||
function counter (var n : nat) : nat is block {
|
function counter (var n : nat) : nat is block {
|
||||||
var i : nat := 0n ;
|
var i : nat := 0n ;
|
||||||
while (i < n) block {
|
while i < n block {
|
||||||
i := i + 1n ;
|
i := i + 1n;
|
||||||
}
|
}
|
||||||
} with i
|
} with i
|
||||||
|
|
||||||
function while_sum (var n : nat) : nat is block {
|
function while_sum (var n : nat) : nat is block {
|
||||||
var i : nat := 0n ;
|
var i : nat := 0n ;
|
||||||
var r : nat := 0n ;
|
var r : nat := 0n ;
|
||||||
while (i < n) block {
|
while i < n block {
|
||||||
i := i + 1n ;
|
i := i + 1n;
|
||||||
r := r + i ;
|
r := r + i;
|
||||||
}
|
}
|
||||||
} with r
|
} with r
|
||||||
|
|
||||||
@ -20,26 +20,26 @@ function for_sum (var n : nat) : int is block {
|
|||||||
var acc : int := 0 ;
|
var acc : int := 0 ;
|
||||||
for i := 1 to int(n)
|
for i := 1 to int(n)
|
||||||
begin
|
begin
|
||||||
acc := acc + i ;
|
acc := acc + i;
|
||||||
end
|
end
|
||||||
} with acc
|
} with acc
|
||||||
|
|
||||||
function for_collection_list (var nee : unit) : (int * string) is block {
|
function for_collection_list (var nee : unit) : (int * string) is block {
|
||||||
var acc : int := 0 ;
|
var acc : int := 0;
|
||||||
var st : string := "to" ;
|
var st : string := "to";
|
||||||
var mylist : list(int) := list 1 ; 1 ; 1 end ;
|
var mylist : list(int) := list 1; 1; 1 end;
|
||||||
for x : int in list mylist
|
for x in list mylist
|
||||||
begin
|
begin
|
||||||
acc := acc + x ;
|
acc := acc + x;
|
||||||
st := st^"to" ;
|
st := st ^ "to";
|
||||||
end
|
end
|
||||||
} with (acc, st)
|
} with (acc, st)
|
||||||
|
|
||||||
function for_collection_set (var nee : unit) : (int * string) is block {
|
function for_collection_set (var nee : unit) : (int * string) is block {
|
||||||
var acc : int := 0 ;
|
var acc : int := 0;
|
||||||
var st : string := "to" ;
|
var st : string := "to";
|
||||||
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
var myset : set(int) := set 1; 2; 3 end;
|
||||||
for x : int in set myset
|
for x in set myset
|
||||||
begin
|
begin
|
||||||
acc := acc + x ;
|
acc := acc + x ;
|
||||||
st := st^"to" ;
|
st := st^"to" ;
|
||||||
@ -50,15 +50,15 @@ function for_collection_if_and_local_var (var nee : unit) : int is block {
|
|||||||
var acc : int := 0 ;
|
var acc : int := 0 ;
|
||||||
const theone : int = 1 ;
|
const theone : int = 1 ;
|
||||||
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
||||||
for x : int in set myset
|
for x in set myset
|
||||||
begin
|
begin
|
||||||
const thetwo : int = 2 ;
|
const thetwo : int = 2 ;
|
||||||
if (x=theone) then
|
if x=theone then
|
||||||
acc := acc + x ;
|
acc := acc + x
|
||||||
else if (x=thetwo) then
|
else if x=thetwo then
|
||||||
acc := acc + thetwo ;
|
acc := acc + thetwo;
|
||||||
else
|
else
|
||||||
acc := acc + 10 ;
|
acc := acc + 10;
|
||||||
end
|
end
|
||||||
} with acc
|
} with acc
|
||||||
|
|
||||||
@ -66,73 +66,71 @@ function for_collection_rhs_capture (var nee : unit) : int is block {
|
|||||||
var acc : int := 0 ;
|
var acc : int := 0 ;
|
||||||
const mybigint : int = 1000 ;
|
const mybigint : int = 1000 ;
|
||||||
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
||||||
for x : int in set myset
|
for x in set myset
|
||||||
begin
|
begin
|
||||||
if (x=1) then
|
if x=1 then acc := acc + mybigint;
|
||||||
acc := acc + mybigint ;
|
else acc := acc + 10;
|
||||||
else
|
|
||||||
acc := acc + 10 ;
|
|
||||||
end
|
end
|
||||||
} with acc
|
} with acc
|
||||||
|
|
||||||
function for_collection_proc_call (var nee : unit) : int is block {
|
function for_collection_proc_call (var nee : unit) : int is block {
|
||||||
var acc : int := 0 ;
|
var acc : int := 0 ;
|
||||||
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
||||||
for x : int in set myset
|
for x in set myset
|
||||||
begin
|
begin
|
||||||
if (x=1) then
|
if x=1 then
|
||||||
acc := acc + for_collection_rhs_capture(unit) ;
|
acc := acc + for_collection_rhs_capture(unit);
|
||||||
else
|
else
|
||||||
acc := acc + 10 ;
|
acc := acc + 10;
|
||||||
end
|
end
|
||||||
} with acc
|
} with acc
|
||||||
|
|
||||||
function for_collection_comp_with_acc (var nee : unit) : int is block {
|
function for_collection_comp_with_acc (var nee : unit) : int is block {
|
||||||
var myint : int := 0 ;
|
var myint : int := 0 ;
|
||||||
var mylist : list(int) := list 1 ; 10 ; 15 end;
|
var mylist : list(int) := list 1 ; 10 ; 15 end;
|
||||||
for x : int in list mylist
|
for x in list mylist
|
||||||
begin
|
begin
|
||||||
if (x < myint) then skip ;
|
if x < myint then skip;
|
||||||
else myint := myint + 10 ;
|
else myint := myint + 10
|
||||||
end
|
end
|
||||||
} with myint
|
} with myint
|
||||||
|
|
||||||
function for_collection_with_patches (var nee : unit) : map(string,int) is block {
|
function for_collection_with_patches (var nee : unit) : map(string,int) is block {
|
||||||
var myint : int := 12 ;
|
var myint : int := 12 ;
|
||||||
var mylist : list(string) := list "I" ; "am" ; "foo" end;
|
var mylist : list(string) := list "I"; "am"; "foo" end;
|
||||||
var mymap : map(string,int) := map end;
|
var mymap : map(string,int) := map end;
|
||||||
for x : string in list mylist
|
for x in list mylist
|
||||||
begin
|
begin
|
||||||
patch mymap with map [ x -> myint ];
|
patch mymap with map [x -> myint];
|
||||||
end
|
end
|
||||||
} with mymap
|
} with mymap
|
||||||
|
|
||||||
function for_collection_empty (var nee : unit) : int is block {
|
function for_collection_empty (var nee : unit) : int is block {
|
||||||
var acc : int := 0 ;
|
var acc : int := 0 ;
|
||||||
var myset : set(int) := set 1 ; 2 ; 3 end ;
|
var myset : set(int) := set 1; 2; 3 end;
|
||||||
for x : int in set myset
|
for x in set myset
|
||||||
begin
|
begin
|
||||||
skip ;
|
skip
|
||||||
end
|
end
|
||||||
} with acc
|
} with acc
|
||||||
|
|
||||||
function for_collection_map_kv (var nee : unit) : (int * string) is block {
|
function for_collection_map_kv (var nee : unit) : (int * string) is block {
|
||||||
var acc : int := 0 ;
|
var acc : int := 0;
|
||||||
var st : string := "" ;
|
var st : string := "";
|
||||||
var mymap : map(string,int) := map "1" -> 1 ; "2" -> 2 ; "3" -> 3 end ;
|
var mymap : map(string,int) := map "1" -> 1; "2" -> 2; "3" -> 3 end;
|
||||||
for k -> v : (string * int) in map mymap
|
for k -> v in map mymap
|
||||||
begin
|
begin
|
||||||
acc := acc + v ;
|
acc := acc + v;
|
||||||
st := st^k ;
|
st := st ^ k;
|
||||||
end
|
end
|
||||||
} with (acc, st)
|
} with (acc, st)
|
||||||
|
|
||||||
function for_collection_map_k (var nee : unit) : string is block {
|
function for_collection_map_k (var nee : unit) : string is block {
|
||||||
var st : string := "" ;
|
var st : string := "" ;
|
||||||
var mymap : map(string,int) := map "1" -> 1 ; "2" -> 2 ; "3" -> 3 end ;
|
var mymap : map(string,int) := map "1" -> 1 ; "2" -> 2 ; "3" -> 3 end ;
|
||||||
for k : string in map mymap
|
for k in map mymap
|
||||||
begin
|
begin
|
||||||
st := st^k ;
|
st := st ^ k;
|
||||||
end
|
end
|
||||||
} with st
|
} with st
|
||||||
|
|
||||||
@ -152,5 +150,5 @@ function for_collection_map_k (var nee : unit) : string is block {
|
|||||||
// } with (myint,myst)
|
// } with (myint,myst)
|
||||||
|
|
||||||
function dummy (const n : nat) : nat is block {
|
function dummy (const n : nat) : nat is block {
|
||||||
while (False) block { skip }
|
while False block { skip }
|
||||||
} with n
|
} with n
|
||||||
|
Loading…
Reference in New Issue
Block a user