Added qualified names to patches ("patch x.y.z with ...").

Fixed grammar for map patches (should start with "patch", not "map").
This commit is contained in:
Christian Rinderknecht 2019-03-20 09:45:32 +01:00
parent 60c23850bd
commit 563bc59285
No known key found for this signature in database
GPG Key ID: 9446816CFD267040
4 changed files with 58 additions and 66 deletions

38
AST.ml
View File

@ -331,9 +331,9 @@ and single_instr =
and map_patch = {
kwd_patch : kwd_patch;
map_name : variable;
path : path;
kwd_with : kwd_with;
delta : map_injection reg
map_inj : map_injection reg
}
and map_injection = {
@ -350,10 +350,10 @@ and binding = {
}
and record_patch = {
kwd_patch : kwd_patch;
record_name : variable;
kwd_with : kwd_with;
delta : record_injection reg
kwd_patch : kwd_patch;
path : path;
kwd_with : kwd_with;
record_inj : record_injection reg
}
and fail_instr = {
@ -625,11 +625,11 @@ and logic_expr_to_region = function
| CompExpr e -> comp_expr_to_region e
and bool_expr_to_region = function
Or {region; _}
| And {region; _}
| Not {region; _}
| False region
| True region -> region
Or {region; _}
| And {region; _}
| Not {region; _}
| False region
| True region -> region
and comp_expr_to_region = function
Lt {region; _}
@ -670,6 +670,10 @@ and record_expr_to_region = function
RecordInj {region; _}
| RecordProj {region; _} -> region
let path_to_region = function
Name var -> var.region
| RecordPath {region; _} -> region
let instr_to_region = function
Single Cond {region; _}
| Single Case {region; _}
@ -1182,18 +1186,18 @@ and print_field_path sequence =
print_nsepseq "." print_var sequence
and print_record_patch node =
let {kwd_patch; record_name; kwd_with; delta} = node in
let {kwd_patch; path; kwd_with; record_inj} = node in
print_token kwd_patch "patch";
print_var record_name;
print_path path;
print_token kwd_with "with";
print_record_injection delta
print_record_injection record_inj
and print_map_patch node =
let {kwd_patch; map_name; kwd_with; delta} = node in
let {kwd_patch; path; kwd_with; map_inj} = node in
print_token kwd_patch "patch";
print_var map_name;
print_path path;
print_token kwd_with "with";
print_map_injection delta
print_map_injection map_inj
and print_map_injection {value; _} =
let {opening; bindings; terminator; close} = value in

25
AST.mli
View File

@ -315,9 +315,9 @@ and single_instr =
and map_patch = {
kwd_patch : kwd_patch;
map_name : variable;
path : path;
kwd_with : kwd_with;
delta : map_injection reg
map_inj : map_injection reg
}
and map_injection = {
@ -334,10 +334,10 @@ and binding = {
}
and record_patch = {
kwd_patch : kwd_patch;
record_name : variable;
kwd_with : kwd_with;
delta : record_injection reg
kwd_patch : kwd_patch;
path : path;
kwd_with : kwd_with;
record_inj : record_injection reg
}
and fail_instr = {
@ -575,15 +575,12 @@ and list_pattern =
(* Projecting regions *)
val type_expr_to_region : type_expr -> Region.t
val expr_to_region : expr -> Region.t
val instr_to_region : instruction -> Region.t
val pattern_to_region : pattern -> Region.t
val type_expr_to_region : type_expr -> Region.t
val expr_to_region : expr -> Region.t
val instr_to_region : instruction -> Region.t
val pattern_to_region : pattern -> Region.t
val local_decl_to_region : local_decl -> Region.t
val path_to_region : path -> Region.t
(* Printing *)

View File

@ -126,7 +126,6 @@ sepseq(X,Sep):
%inline fun_name : Ident { $1 }
%inline field_name : Ident { $1 }
%inline record_name : Ident { $1 }
%inline map_name : Ident { $1 }
(* Main *)
@ -446,13 +445,13 @@ single_instr:
| map_patch { MapPatch $1 }
map_patch:
Map map_name With map_injection {
Patch path With map_injection {
let region = cover $1 $4.region in
let value = {
kwd_patch = $1;
map_name = $2;
kwd_with = $3;
delta = $4}
kwd_patch = $1;
path = $2;
kwd_with = $3;
map_inj = $4}
in {region; value}
}
@ -481,13 +480,13 @@ binding:
}
record_patch:
Patch record_name With record_injection {
Patch path With record_injection {
let region = cover $1 $4.region in
let value = {
kwd_patch = $1;
record_name = $2;
kwd_with = $3;
delta = $4}
kwd_patch = $1;
path = $2;
kwd_with = $3;
record_inj = $4}
in {region; value}
}
@ -769,21 +768,18 @@ core_expr:
map_expr:
map_selection { MapLookUp $1 }
path:
var { Name $1 }
| record_projection { RecordPath $1 }
map_selection:
map_name brackets(expr) {
let region = cover $1.region $2.region in
path brackets(expr) {
let region = cover (path_to_region $1) $2.region in
let value = {
path = Name $1;
path = $1;
index = $2}
in {region; value}
}
| record_projection brackets(expr) {
let region = cover $1.region $2.region in
let value = {
path = RecordPath $1;
index = $2}
in {region; value}
}
record_expr:
record_injection { RecordInj $1 }

View File

@ -16,12 +16,9 @@ entrypoint contribute (storage store : store;
fail "Deadline passed"
else
case store.backers[sender] of
None ->
patch store with
record
backers = add_binding ((sender, amount), store.backers)
end
| _ -> skip
None -> //store.backers[sender] := amount
patch store.backers with map sender -> amount end
| _ -> skip
end
end with (store, operations)
@ -33,8 +30,10 @@ entrypoint withdraw (storage store : store; const sender : address)
if now >= store.deadline then
if balance >= store.goal then
begin
patch store with record funded = True end;
operations := [Transfer (owner, balance)]
patch store with record funded = True end;
// patch store.funded with True end;
// store.funded := True;
operations := [Transfer (owner, balance)]
end
else fail "Below target"
else fail "Too soon"
@ -57,12 +56,8 @@ entrypoint claim (storage store : store; const sender : address)
fail "Cannot refund"
else
begin
amount := store.backers[sender];
patch store with
record
backers = remove_entry (sender, store.backers)
end;
operations := [Transfer (sender, amount)]
operations := [Transfer (sender, amount)];
// patch store.backers without key sender;
end
end
end with (store, operations)