Commit 4fd8b24d authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: change the syntax of "abstract"

The old syntax:   abstract expr [spec]...

The semicolon binds more loosely than "abstract" and
the specification clauses are optional, so that
"abstract e1; e2" is the same as "(abstract e1); e2"
and "abstract e1; e2; ensures {...}" is a syntax error.

The new syntax:   abstract [spec]... expr end

This allows to put sequences of expressions under "abstract"
without ambiguity and moves the specification clauses to the
beginning. In other words, "abstract" becomes a "begin" with
a specification attached. The spec-at-the-top is consistent
with the syntax of functions and the whole seems to be more
natural for the intented use of "abstract" (a logical cut).
parent e66e2a3f
......@@ -144,7 +144,7 @@ module HashtblImpl
ensures { forall k': key. k' <> k ->
Map.get h.view k' = Map.get (old h.view) k' }
=
abstract (if h.size = length h.data then resize h);
abstract if h.size = length h.data then resize h end;
remove h k;
let i = bucket k (length h.data) in
h.data[i] <- Cons (k, v) h.data[i];
......
......@@ -192,6 +192,7 @@ on linking described in file LICENSE.
<keyword>if</keyword>
<keyword>in</keyword>
<keyword>let</keyword>
<keyword>loop</keyword>
<keyword>match</keyword>
<keyword>raise</keyword>
<keyword>rec</keyword>
......
......@@ -58,6 +58,7 @@ syn keyword whyTodo contained TODO FIXME XXX NOTE
" Blocks
" FIXME? match and try should detect the absence of "with" ?
syn region whyEnd matchgroup=whyKeyword start="\<begin\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<abstract\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<match\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<loop\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region whyEnd matchgroup=whyKeyword start="\<try\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
......@@ -90,7 +91,7 @@ syn keyword whyKeyword let meta
syn keyword whyKeyword not predicate
syn keyword whyKeyword then type with
syn keyword whyKeyword abstract any
syn keyword whyKeyword any
syn keyword whyKeyword exception fun ghost
syn keyword whyKeyword model mutable private
syn keyword whyKeyword raise rec val while
......@@ -139,7 +140,7 @@ syn sync maxlines=500
syn sync match whyDoSync grouphere whyDo "\<do\>"
syn sync match whyDoSync groupthere whyDo "\<done\>"
syn sync match whyEndSync grouphere whyEnd "\<\(begin\|match\|loop\|try\)\>"
syn sync match whyEndSync grouphere whyEnd "\<\(begin\|abstract\|match\|loop\|try\)\>"
syn sync match whyEndSync groupthere whyEnd "\<end\>"
syn sync match whyTheorySync grouphere whyTheory "\<theory\>"
......
......@@ -205,8 +205,6 @@ end
%right SEMICOLON
%nonassoc prec_no_else
%nonassoc DOT ELSE GHOST
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES DIVERGES VARIANT
%nonassoc prec_named
%nonassoc COLON
......@@ -1273,8 +1271,8 @@ expr:
{ mk_expr (Eany $2) }
| GHOST expr
{ mk_expr (Eghost $2) }
| ABSTRACT expr spec
{ mk_expr (Eabstract($2, $3)) }
| ABSTRACT spec final_expr END
{ mk_expr (Eabstract($3, $2)) }
| label expr %prec prec_named
{ mk_expr (Enamed ($1, $2)) }
;
......@@ -1400,8 +1398,8 @@ type_invariant:
;
spec:
| /* epsilon */ %prec prec_no_spec { empty_spec }
| single_spec spec { spec_union $1 $2 }
| /* epsilon */ { empty_spec }
| single_spec spec { spec_union $1 $2 }
;
single_spec:
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment