Maps and sets defined by extension are now general expressions.
They used to be allowed only as initial values in declarations. This new syntax enables idioms like if set ["John"; "Paul"] contains x then ... else
This commit is contained in:
parent
f9ffc7b8e7
commit
45a26826ca
14
Parser.mly
14
Parser.mly
@ -417,10 +417,6 @@ unqualified_decl(OP):
|
|||||||
opt_type = $3};
|
opt_type = $3};
|
||||||
rpar = Region.ghost}
|
rpar = Region.ghost}
|
||||||
in EConstr (NoneExpr {region; value})
|
in EConstr (NoneExpr {region; value})
|
||||||
| `EMap inj ->
|
|
||||||
EMap (MapInj inj)
|
|
||||||
| `ESet inj ->
|
|
||||||
ESet (SetInj inj)
|
|
||||||
in $1, $2, $3, $4, init, $6, stop
|
in $1, $2, $3, $4, init, $6, stop
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -457,12 +453,9 @@ var_decl:
|
|||||||
}
|
}
|
||||||
|
|
||||||
extended_expr:
|
extended_expr:
|
||||||
expr { {region = expr_to_region $1;
|
expr { {region = expr_to_region $1; value = `Expr $1} }
|
||||||
value = `Expr $1} }
|
|
||||||
| Nil { {region = $1; value = `EList $1} }
|
| Nil { {region = $1; value = `EList $1} }
|
||||||
| C_None { {region = $1; value = `ENone $1} }
|
| C_None { {region = $1; value = `ENone $1} }
|
||||||
| map_injection { {region = $1.region; value = `EMap $1} }
|
|
||||||
| set_injection { {region = $1.region; value = `ESet $1} }
|
|
||||||
|
|
||||||
instruction:
|
instruction:
|
||||||
single_instr { Single $1 }
|
single_instr { Single $1 }
|
||||||
@ -936,6 +929,7 @@ core_expr:
|
|||||||
| none_expr { EConstr (NoneExpr $1) }
|
| none_expr { EConstr (NoneExpr $1) }
|
||||||
| fun_call { ECall $1 }
|
| fun_call { ECall $1 }
|
||||||
| map_expr { EMap $1 }
|
| map_expr { EMap $1 }
|
||||||
|
| set_expr { ESet $1 }
|
||||||
| record_expr { ERecord $1 }
|
| record_expr { ERecord $1 }
|
||||||
| projection { EProj $1 }
|
| projection { EProj $1 }
|
||||||
| Constr arguments {
|
| Constr arguments {
|
||||||
@ -947,8 +941,12 @@ core_expr:
|
|||||||
EConstr (SomeApp {region; value = $1,$2})
|
EConstr (SomeApp {region; value = $1,$2})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
set_expr:
|
||||||
|
set_injection { SetInj $1 }
|
||||||
|
|
||||||
map_expr:
|
map_expr:
|
||||||
map_lookup { MapLookUp $1 }
|
map_lookup { MapLookUp $1 }
|
||||||
|
| map_injection { MapInj $1 }
|
||||||
|
|
||||||
map_lookup:
|
map_lookup:
|
||||||
path brackets(expr) {
|
path brackets(expr) {
|
||||||
|
@ -28,6 +28,7 @@ entrypoint withdraw (storage store : store; const sender : address)
|
|||||||
: store * list (operation) is
|
: store * list (operation) is
|
||||||
var operations : list (operation) := list end
|
var operations : list (operation) := list end
|
||||||
begin
|
begin
|
||||||
|
// if set ["a"; "b"] contains x then skip else skip;
|
||||||
if sender = owner then
|
if sender = owner then
|
||||||
if now (Unit) >= store.deadline then
|
if now (Unit) >= store.deadline then
|
||||||
if balance >= store.goal then {
|
if balance >= store.goal then {
|
||||||
|
Loading…
Reference in New Issue
Block a user