I added set definitions by extension.
For example: const bar : set (int) = set 1; 1+1; f(3); end
This commit is contained in:
parent
1e65c63d99
commit
f6dbd9d601
67
AST.ml
67
AST.ml
@ -63,6 +63,7 @@ type kwd_patch = Region.t
|
|||||||
type kwd_procedure = Region.t
|
type kwd_procedure = Region.t
|
||||||
type kwd_record = Region.t
|
type kwd_record = Region.t
|
||||||
type kwd_remove = Region.t
|
type kwd_remove = Region.t
|
||||||
|
type kwd_set = Region.t
|
||||||
type kwd_skip = Region.t
|
type kwd_skip = Region.t
|
||||||
type kwd_step = Region.t
|
type kwd_step = Region.t
|
||||||
type kwd_storage = Region.t
|
type kwd_storage = Region.t
|
||||||
@ -121,6 +122,7 @@ type fun_name = string reg
|
|||||||
type type_name = string reg
|
type type_name = string reg
|
||||||
type field_name = string reg
|
type field_name = string reg
|
||||||
type map_name = string reg
|
type map_name = string reg
|
||||||
|
type set_name = string reg
|
||||||
type constr = string reg
|
type constr = string reg
|
||||||
|
|
||||||
(* Parentheses *)
|
(* Parentheses *)
|
||||||
@ -470,6 +472,16 @@ and expr =
|
|||||||
| ETuple of tuple
|
| ETuple of tuple
|
||||||
| EPar of expr par reg
|
| EPar of expr par reg
|
||||||
|
|
||||||
|
and set_expr =
|
||||||
|
SetInj of set_injection reg
|
||||||
|
|
||||||
|
and set_injection = {
|
||||||
|
opening : kwd_set;
|
||||||
|
elements : (expr, semi) nsepseq;
|
||||||
|
terminator : semi option;
|
||||||
|
close : kwd_end
|
||||||
|
}
|
||||||
|
|
||||||
and map_expr =
|
and map_expr =
|
||||||
MapLookUp of map_lookup reg
|
MapLookUp of map_lookup reg
|
||||||
| MapInj of map_injection reg
|
| MapInj of map_injection reg
|
||||||
@ -531,10 +543,6 @@ and list_expr =
|
|||||||
| List of (expr, comma) nsepseq brackets reg
|
| List of (expr, comma) nsepseq brackets reg
|
||||||
| EmptyList of empty_list reg
|
| EmptyList of empty_list reg
|
||||||
|
|
||||||
and set_expr =
|
|
||||||
Set of (expr, comma) nsepseq braces reg
|
|
||||||
| EmptySet of empty_set reg
|
|
||||||
|
|
||||||
and constr_expr =
|
and constr_expr =
|
||||||
SomeApp of (c_Some * arguments) reg
|
SomeApp of (c_Some * arguments) reg
|
||||||
| NoneExpr of none_expr reg
|
| NoneExpr of none_expr reg
|
||||||
@ -574,15 +582,6 @@ and typed_empty_list = {
|
|||||||
list_type : type_expr
|
list_type : type_expr
|
||||||
}
|
}
|
||||||
|
|
||||||
and empty_set = typed_empty_set par
|
|
||||||
|
|
||||||
and typed_empty_set = {
|
|
||||||
lbrace : lbrace;
|
|
||||||
rbrace : rbrace;
|
|
||||||
colon : colon;
|
|
||||||
set_type : type_expr
|
|
||||||
}
|
|
||||||
|
|
||||||
and none_expr = typed_none_expr par
|
and none_expr = typed_none_expr par
|
||||||
|
|
||||||
and typed_none_expr = {
|
and typed_none_expr = {
|
||||||
@ -648,6 +647,9 @@ and map_expr_to_region = function
|
|||||||
MapLookUp {region; _}
|
MapLookUp {region; _}
|
||||||
| MapInj {region; _} -> region
|
| MapInj {region; _} -> region
|
||||||
|
|
||||||
|
and set_expr_to_region = function
|
||||||
|
SetInj {region; _} -> region
|
||||||
|
|
||||||
and logic_expr_to_region = function
|
and logic_expr_to_region = function
|
||||||
BoolExpr e -> bool_expr_to_region e
|
BoolExpr e -> bool_expr_to_region e
|
||||||
| CompExpr e -> comp_expr_to_region e
|
| CompExpr e -> comp_expr_to_region e
|
||||||
@ -685,10 +687,6 @@ and list_expr_to_region = function
|
|||||||
| List {region; _}
|
| List {region; _}
|
||||||
| EmptyList {region; _} -> region
|
| EmptyList {region; _} -> region
|
||||||
|
|
||||||
and set_expr_to_region = function
|
|
||||||
Set {region; _}
|
|
||||||
| EmptySet {region; _} -> region
|
|
||||||
|
|
||||||
and constr_expr_to_region = function
|
and constr_expr_to_region = function
|
||||||
NoneExpr {region; _}
|
NoneExpr {region; _}
|
||||||
| ConstrApp {region; _}
|
| ConstrApp {region; _}
|
||||||
@ -1138,8 +1136,10 @@ and print_expr = function
|
|||||||
|
|
||||||
and print_map_expr = function
|
and print_map_expr = function
|
||||||
MapLookUp {value; _} -> print_map_lookup value
|
MapLookUp {value; _} -> print_map_lookup value
|
||||||
| MapInj inj ->
|
| MapInj inj -> print_map_injection inj
|
||||||
print_map_injection inj
|
|
||||||
|
and print_set_expr = function
|
||||||
|
SetInj inj -> print_set_injection inj
|
||||||
|
|
||||||
and print_map_lookup {path; index} =
|
and print_map_lookup {path; index} =
|
||||||
let {lbracket; inside; rbracket} = index.value in
|
let {lbracket; inside; rbracket} = index.value in
|
||||||
@ -1206,10 +1206,6 @@ and print_list_expr = function
|
|||||||
| List e -> print_list e
|
| List e -> print_list e
|
||||||
| EmptyList e -> print_empty_list e
|
| EmptyList e -> print_empty_list e
|
||||||
|
|
||||||
and print_set_expr = function
|
|
||||||
Set e -> print_set e
|
|
||||||
| EmptySet e -> print_empty_set e
|
|
||||||
|
|
||||||
and print_constr_expr = function
|
and print_constr_expr = function
|
||||||
SomeApp e -> print_some_app e
|
SomeApp e -> print_some_app e
|
||||||
| NoneExpr e -> print_none_expr e
|
| NoneExpr e -> print_none_expr e
|
||||||
@ -1265,11 +1261,18 @@ and print_map_remove node =
|
|||||||
|
|
||||||
and print_map_injection {value; _} =
|
and print_map_injection {value; _} =
|
||||||
let {opening; bindings; terminator; close} = value in
|
let {opening; bindings; terminator; close} = value in
|
||||||
print_token opening "record";
|
print_token opening "map";
|
||||||
print_nsepseq ";" print_binding bindings;
|
print_nsepseq ";" print_binding bindings;
|
||||||
print_terminator terminator;
|
print_terminator terminator;
|
||||||
print_token close "end"
|
print_token close "end"
|
||||||
|
|
||||||
|
and print_set_injection {value; _} =
|
||||||
|
let {opening; elements; terminator; close} = value in
|
||||||
|
print_token opening "set";
|
||||||
|
print_nsepseq ";" print_expr elements;
|
||||||
|
print_terminator terminator;
|
||||||
|
print_token close "end"
|
||||||
|
|
||||||
and print_binding {value; _} =
|
and print_binding {value; _} =
|
||||||
let {source; arrow; image} = value in
|
let {source; arrow; image} = value in
|
||||||
print_expr source;
|
print_expr source;
|
||||||
@ -1298,22 +1301,6 @@ and print_empty_list {value; _} =
|
|||||||
print_type_expr list_type;
|
print_type_expr list_type;
|
||||||
print_token rpar ")"
|
print_token rpar ")"
|
||||||
|
|
||||||
and print_set {value; _} =
|
|
||||||
let {lbrace; inside; rbrace} = value in
|
|
||||||
print_token lbrace "{";
|
|
||||||
print_nsepseq "," print_expr inside;
|
|
||||||
print_token rbrace "}"
|
|
||||||
|
|
||||||
and print_empty_set {value; _} =
|
|
||||||
let {lpar; inside; rpar} = value in
|
|
||||||
let {lbrace; rbrace; colon; set_type} = inside in
|
|
||||||
print_token lpar "(";
|
|
||||||
print_token lbrace "{";
|
|
||||||
print_token rbrace "}";
|
|
||||||
print_token colon ":";
|
|
||||||
print_type_expr set_type;
|
|
||||||
print_token rpar ")"
|
|
||||||
|
|
||||||
and print_none_expr {value; _} =
|
and print_none_expr {value; _} =
|
||||||
let {lpar; inside; rpar} = value in
|
let {lpar; inside; rpar} = value in
|
||||||
let {c_None; colon; opt_type} = inside in
|
let {c_None; colon; opt_type} = inside in
|
||||||
|
25
AST.mli
25
AST.mli
@ -47,6 +47,7 @@ type kwd_patch = Region.t
|
|||||||
type kwd_procedure = Region.t
|
type kwd_procedure = Region.t
|
||||||
type kwd_record = Region.t
|
type kwd_record = Region.t
|
||||||
type kwd_remove = Region.t
|
type kwd_remove = Region.t
|
||||||
|
type kwd_set = Region.t
|
||||||
type kwd_skip = Region.t
|
type kwd_skip = Region.t
|
||||||
type kwd_step = Region.t
|
type kwd_step = Region.t
|
||||||
type kwd_storage = Region.t
|
type kwd_storage = Region.t
|
||||||
@ -105,6 +106,7 @@ type fun_name = string reg
|
|||||||
type type_name = string reg
|
type type_name = string reg
|
||||||
type field_name = string reg
|
type field_name = string reg
|
||||||
type map_name = string reg
|
type map_name = string reg
|
||||||
|
type set_name = string reg
|
||||||
type constr = string reg
|
type constr = string reg
|
||||||
|
|
||||||
(* Parentheses *)
|
(* Parentheses *)
|
||||||
@ -454,6 +456,16 @@ and expr =
|
|||||||
| ETuple of tuple
|
| ETuple of tuple
|
||||||
| EPar of expr par reg
|
| EPar of expr par reg
|
||||||
|
|
||||||
|
and set_expr =
|
||||||
|
SetInj of set_injection reg
|
||||||
|
|
||||||
|
and set_injection = {
|
||||||
|
opening : kwd_set;
|
||||||
|
elements : (expr, semi) nsepseq;
|
||||||
|
terminator : semi option;
|
||||||
|
close : kwd_end
|
||||||
|
}
|
||||||
|
|
||||||
and map_expr =
|
and map_expr =
|
||||||
MapLookUp of map_lookup reg
|
MapLookUp of map_lookup reg
|
||||||
| MapInj of map_injection reg
|
| MapInj of map_injection reg
|
||||||
@ -515,10 +527,6 @@ and list_expr =
|
|||||||
| List of (expr, comma) nsepseq brackets reg
|
| List of (expr, comma) nsepseq brackets reg
|
||||||
| EmptyList of empty_list reg
|
| EmptyList of empty_list reg
|
||||||
|
|
||||||
and set_expr =
|
|
||||||
Set of (expr, comma) nsepseq braces reg
|
|
||||||
| EmptySet of empty_set reg
|
|
||||||
|
|
||||||
and constr_expr =
|
and constr_expr =
|
||||||
SomeApp of (c_Some * arguments) reg
|
SomeApp of (c_Some * arguments) reg
|
||||||
| NoneExpr of none_expr reg
|
| NoneExpr of none_expr reg
|
||||||
@ -558,15 +566,6 @@ and typed_empty_list = {
|
|||||||
list_type : type_expr
|
list_type : type_expr
|
||||||
}
|
}
|
||||||
|
|
||||||
and empty_set = typed_empty_set par
|
|
||||||
|
|
||||||
and typed_empty_set = {
|
|
||||||
lbrace : lbrace;
|
|
||||||
rbrace : rbrace;
|
|
||||||
colon : colon;
|
|
||||||
set_type : type_expr
|
|
||||||
}
|
|
||||||
|
|
||||||
and none_expr = typed_none_expr par
|
and none_expr = typed_none_expr par
|
||||||
|
|
||||||
and typed_none_expr = {
|
and typed_none_expr = {
|
||||||
|
@ -89,6 +89,7 @@ type t =
|
|||||||
| Procedure of Region.t (* "procedure" *)
|
| Procedure of Region.t (* "procedure" *)
|
||||||
| Record of Region.t (* "record" *)
|
| Record of Region.t (* "record" *)
|
||||||
| Remove of Region.t (* "remove" *)
|
| Remove of Region.t (* "remove" *)
|
||||||
|
| Set of Region.t (* "set" *)
|
||||||
| Skip of Region.t (* "skip" *)
|
| Skip of Region.t (* "skip" *)
|
||||||
| Step of Region.t (* "step" *)
|
| Step of Region.t (* "step" *)
|
||||||
| Storage of Region.t (* "storage" *)
|
| Storage of Region.t (* "storage" *)
|
||||||
|
@ -88,6 +88,7 @@ type t =
|
|||||||
| Procedure of Region.t (* "procedure" *)
|
| Procedure of Region.t (* "procedure" *)
|
||||||
| Record of Region.t (* "record" *)
|
| Record of Region.t (* "record" *)
|
||||||
| Remove of Region.t (* "remove" *)
|
| Remove of Region.t (* "remove" *)
|
||||||
|
| Set of Region.t (* "set" *)
|
||||||
| Skip of Region.t (* "skip" *)
|
| Skip of Region.t (* "skip" *)
|
||||||
| Step of Region.t (* "step" *)
|
| Step of Region.t (* "step" *)
|
||||||
| Storage of Region.t (* "storage" *)
|
| Storage of Region.t (* "storage" *)
|
||||||
@ -210,6 +211,7 @@ let proj_token = function
|
|||||||
| Procedure region -> region, "Procedure"
|
| Procedure region -> region, "Procedure"
|
||||||
| Record region -> region, "Record"
|
| Record region -> region, "Record"
|
||||||
| Remove region -> region, "Remove"
|
| Remove region -> region, "Remove"
|
||||||
|
| Set region -> region, "Set"
|
||||||
| Skip region -> region, "Skip"
|
| Skip region -> region, "Skip"
|
||||||
| Step region -> region, "Step"
|
| Step region -> region, "Step"
|
||||||
| Storage region -> region, "Storage"
|
| Storage region -> region, "Storage"
|
||||||
@ -298,6 +300,7 @@ let to_lexeme = function
|
|||||||
| Procedure _ -> "procedure"
|
| Procedure _ -> "procedure"
|
||||||
| Record _ -> "record"
|
| Record _ -> "record"
|
||||||
| Remove _ -> "remove"
|
| Remove _ -> "remove"
|
||||||
|
| Set _ -> "set"
|
||||||
| Skip _ -> "skip"
|
| Skip _ -> "skip"
|
||||||
| Step _ -> "step"
|
| Step _ -> "step"
|
||||||
| Storage _ -> "storage"
|
| Storage _ -> "storage"
|
||||||
@ -355,6 +358,7 @@ let keywords = [
|
|||||||
(fun reg -> Procedure reg);
|
(fun reg -> Procedure reg);
|
||||||
(fun reg -> Record reg);
|
(fun reg -> Record reg);
|
||||||
(fun reg -> Remove reg);
|
(fun reg -> Remove reg);
|
||||||
|
(fun reg -> Set reg);
|
||||||
(fun reg -> Skip reg);
|
(fun reg -> Skip reg);
|
||||||
(fun reg -> Step reg);
|
(fun reg -> Step reg);
|
||||||
(fun reg -> Storage reg);
|
(fun reg -> Storage reg);
|
||||||
@ -580,6 +584,7 @@ let is_kwd = function
|
|||||||
| Procedure _
|
| Procedure _
|
||||||
| Record _
|
| Record _
|
||||||
| Remove _
|
| Remove _
|
||||||
|
| Set _
|
||||||
| Skip _
|
| Skip _
|
||||||
| Step _
|
| Step _
|
||||||
| Storage _
|
| Storage _
|
||||||
|
@ -67,6 +67,7 @@
|
|||||||
%token <Region.t> Procedure (* "procedure" *)
|
%token <Region.t> Procedure (* "procedure" *)
|
||||||
%token <Region.t> Record (* "record" *)
|
%token <Region.t> Record (* "record" *)
|
||||||
%token <Region.t> Remove (* "remove" *)
|
%token <Region.t> Remove (* "remove" *)
|
||||||
|
%token <Region.t> Set (* "set" *)
|
||||||
%token <Region.t> Skip (* "skip" *)
|
%token <Region.t> Skip (* "skip" *)
|
||||||
%token <Region.t> Step (* "step" *)
|
%token <Region.t> Step (* "step" *)
|
||||||
%token <Region.t> Storage (* "storage" *)
|
%token <Region.t> Storage (* "storage" *)
|
||||||
|
44
Parser.mly
44
Parser.mly
@ -177,8 +177,15 @@ core_type:
|
|||||||
}
|
}
|
||||||
| Map type_tuple {
|
| Map type_tuple {
|
||||||
let region = cover $1 $2.region in
|
let region = cover $1 $2.region in
|
||||||
let value = {value="map"; region=$1}
|
let type_constr = {value="map"; region=$1}
|
||||||
in TApp {region; value = value, $2}
|
in TApp {region; value = type_constr, $2}
|
||||||
|
}
|
||||||
|
| Set par(type_expr) {
|
||||||
|
let total = cover $1 $2.region in
|
||||||
|
let type_constr = {value="set"; region=$1} in
|
||||||
|
let {region; value = {lpar; inside; rpar}} = $2 in
|
||||||
|
let tuple = {region; value={lpar; inside=inside,[]; rpar}}
|
||||||
|
in TApp {region=total; value = type_constr, tuple}
|
||||||
}
|
}
|
||||||
| par(type_expr) {
|
| par(type_expr) {
|
||||||
TPar $1
|
TPar $1
|
||||||
@ -405,7 +412,9 @@ unqualified_decl(OP):
|
|||||||
rpar = Region.ghost}
|
rpar = Region.ghost}
|
||||||
in EConstr (NoneExpr {region; value})
|
in EConstr (NoneExpr {region; value})
|
||||||
| `EMap inj ->
|
| `EMap inj ->
|
||||||
EMap (MapInj 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
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -448,6 +457,7 @@ extended_expr:
|
|||||||
value = `EList ($1,$2)} }
|
value = `EList ($1,$2)} }
|
||||||
| C_None { {region = $1; value = `ENone $1} }
|
| C_None { {region = $1; value = `ENone $1} }
|
||||||
| map_injection { {region = $1.region; value = `EMap $1} }
|
| map_injection { {region = $1.region; value = `EMap $1} }
|
||||||
|
| set_injection { {region = $1.region; value = `ESet $1} }
|
||||||
|
|
||||||
|
|
||||||
instruction:
|
instruction:
|
||||||
@ -489,6 +499,18 @@ map_patch:
|
|||||||
in {region; value}
|
in {region; value}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
set_injection:
|
||||||
|
Set series(expr) {
|
||||||
|
let first, (others, terminator, close) = $2 in
|
||||||
|
let region = cover $1 close
|
||||||
|
and value = {
|
||||||
|
opening = $1;
|
||||||
|
elements = first, others;
|
||||||
|
terminator;
|
||||||
|
close}
|
||||||
|
in {region; value}
|
||||||
|
}
|
||||||
|
|
||||||
map_injection:
|
map_injection:
|
||||||
Map series(binding) {
|
Map series(binding) {
|
||||||
let first, (others, terminator, close) = $2 in
|
let first, (others, terminator, close) = $2 in
|
||||||
@ -797,8 +819,6 @@ core_expr:
|
|||||||
| tuple { ETuple $1 }
|
| tuple { ETuple $1 }
|
||||||
| list_expr { EList (List $1) }
|
| list_expr { EList (List $1) }
|
||||||
| empty_list { EList (EmptyList $1) }
|
| empty_list { EList (EmptyList $1) }
|
||||||
| set_expr { ESet (Set $1) }
|
|
||||||
| empty_set { ESet (EmptySet $1) }
|
|
||||||
| 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 }
|
||||||
@ -891,20 +911,6 @@ typed_empty_list:
|
|||||||
list_type = $4}
|
list_type = $4}
|
||||||
}
|
}
|
||||||
|
|
||||||
set_expr:
|
|
||||||
braces(nsepseq(expr,COMMA)) { $1 }
|
|
||||||
|
|
||||||
empty_set:
|
|
||||||
par(typed_empty_set) { $1 }
|
|
||||||
|
|
||||||
typed_empty_set:
|
|
||||||
LBRACE RBRACE COLON type_expr {
|
|
||||||
{lbrace = $1;
|
|
||||||
rbrace = $2;
|
|
||||||
colon = $3;
|
|
||||||
set_type = $4}
|
|
||||||
}
|
|
||||||
|
|
||||||
none_expr:
|
none_expr:
|
||||||
par(typed_none_expr) { $1 }
|
par(typed_none_expr) { $1 }
|
||||||
|
|
||||||
|
@ -6,7 +6,8 @@ type store is
|
|||||||
funded : bool;
|
funded : bool;
|
||||||
end
|
end
|
||||||
|
|
||||||
const foo : store = map "X" -> 10; "Y" -> 11 end
|
const foo : map (string, nat) = map "X" -> 10; "Y" -> 11 end
|
||||||
|
const bar : set (int) = set 1; 1+1; f(3); end
|
||||||
|
|
||||||
entrypoint contribute (storage store : store;
|
entrypoint contribute (storage store : store;
|
||||||
const sender : address;
|
const sender : address;
|
||||||
|
Loading…
Reference in New Issue
Block a user