diff --git a/src/parser/parser.pre.mly b/src/parser/parser.pre.mly index f9b9c8b20993a8f8d22776dabfce89e977a75353..6f8d1627b9629bb6b21d3bb9fbbac57495d90c77 100644 --- a/src/parser/parser.pre.mly +++ b/src/parser/parser.pre.mly @@ -190,6 +190,7 @@ /* Precedences */ +%nonassoc prec_label %nonassoc prec_post %nonassoc BAR @@ -1073,7 +1074,7 @@ expr: { mk_expr (Ematch ($2, $5)) } | MATCH expr COMMA list1_expr_sep_comma WITH bar_ program_match_cases END { mk_expr (Ematch (mk_expr (Etuple ($2::$4)), $7)) } -| LABEL uident COLON expr +| LABEL uident COLON expr %prec prec_label { mk_expr (Elabel ($2, $4)) } | LOOP loop_annotation expr END { mk_expr (Eloop ($2, $3)) } diff --git a/src/programs/TODO b/src/programs/TODO index ee63550c8c5942d3e344036889a65af2b25963b3..bbb1a4ca85a567f686549c3b0770eb55b03d34ab 100644 --- a/src/programs/TODO +++ b/src/programs/TODO @@ -1,4 +1,6 @@ +o automatically add a label pre_f at entrance of each function f + o use of old in loop invariant should be reported as an error (correctly) o what about pervasives old, at, label, unit = () @@ -7,8 +9,6 @@ o what about pervasives old, at, label, unit = () o fmla_effect -o fixed precedence of label (label L: e) wrt sequence (e ; e) - o model types (abstract but not mutable) abstract types (no model)