From e5d3e35ef9183a23eb10b6291feefe6f0584bb6a Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr> Date: Fri, 18 Mar 2011 17:59:16 +0100 Subject: [PATCH] fixed label precedence in programs --- src/parser/parser.pre.mly | 3 ++- src/programs/TODO | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/parser/parser.pre.mly b/src/parser/parser.pre.mly index f9b9c8b209..6f8d1627b9 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 ee63550c8c..bbb1a4ca85 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) -- GitLab