Commit df239061 authored by Andrei Paskevich's avatar Andrei Paskevich

WhymL: break and continue

Without an argument, break and continue refer to the innermost loop.
A label put over an expression sequence starting with a loop, can be
used as an optional argument for break and continue:

  label L in
  [ghost] ["tag"] [M.begin]
    while true do
      ...
      break L
      ...
    done;
    [...]
  [end] [: unit]

In the square brackets are listed the constructions allowed between
the label declaration and the loop expression.
parent 2f1058c9
......@@ -240,7 +240,6 @@ module NaturalMergesort
variant { n - !first_run }
label L in
let lo = ref 0 in
exception Break in try
while !lo < n - 1 do
invariant { 0 <= !lo <= n }
invariant { !first_run at L <= !first_run <= n }
......@@ -249,7 +248,7 @@ module NaturalMergesort
invariant { permut_all (a at L) a }
variant { n - !lo }
let mid = find_run a !lo in
if mid = n then begin if !lo = 0 then return; raise Break end;
if mid = n then begin if !lo = 0 then return; break end;
let hi = find_run a mid in
label M in
merge_using tmp a !lo mid hi;
......@@ -258,7 +257,6 @@ module NaturalMergesort
ghost if !lo = 0 then first_run := hi;
lo := hi;
done
with Break -> () end
done
......
......@@ -92,23 +92,23 @@ module Array
(0 <= i < ofs2 \/ ofs2 + len <= i < length a) -> a[i] = old a[i] }
ensures { forall i:int.
ofs2 <= i < ofs2 + len -> a[i] = old a[ofs1 + i - ofs2] }
= label Init in
=
if ofs1 <= ofs2 then (* from right to left *)
for k = len - 1 downto 0 do
invariant { forall i:int.
(0 <= i <= ofs2 + k \/ ofs2 + len <= i < length a) ->
a[i] = (a at Init)[i] }
a[i] = (old a)[i] }
invariant { forall i:int.
ofs2 + k < i < ofs2 + len -> a[i] = (a at Init)[ofs1 + i - ofs2] }
ofs2 + k < i < ofs2 + len -> a[i] = (old a)[ofs1 + i - ofs2] }
a[ofs2 + k] <- a[ofs1 + k]
done
else (* from left to right *)
for k = 0 to len - 1 do
invariant { forall i:int.
(0 <= i < ofs2 \/ ofs2 + k <= i < length a) ->
a[i] = (a at Init)[i] }
a[i] = (old a)[i] }
invariant { forall i:int.
ofs2 <= i < ofs2 + k -> a[i] = (a at Init)[ofs1 + i - ofs2] }
ofs2 <= i < ofs2 + k -> a[i] = (old a)[ofs1 + i - ofs2] }
a[ofs2 + k] <- a[ofs1 + k]
done
......
......@@ -29,7 +29,7 @@
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "return" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
)
"Minimal highlighting for Why3 mode")
......
......@@ -186,7 +186,9 @@ on linking described in file LICENSE.
<context id="meta-words" style-ref="keyword">
<keyword>any</keyword>
<keyword>begin</keyword>
<keyword>break</keyword>
<keyword>by</keyword>
<keyword>continue</keyword>
<keyword>do</keyword>
<keyword>done</keyword>
<keyword>downto</keyword>
......
......@@ -5,8 +5,8 @@
\lstdefinelanguage{why3}
{
basicstyle=\ttfamily,%
morekeywords=[1]{abstract,absurd,any,assert,assume,at,axiom,by,%
check,clone,coinductive,constant,diverges,do,done,downto,%
morekeywords=[1]{abstract,absurd,any,assert,assume,at,axiom,break,by,%
check,clone,coinductive,constant,continue,diverges,do,done,downto,%
else,end,ensures,exception,exists,export,false,for,forall,fun,%
function,ghost,goal,if,import,in,inductive,invariant,label,lemma,%
let,loop,match,meta,module,mutable,not,old,%
......
......@@ -91,7 +91,7 @@ syn keyword whyKeyword let meta
syn keyword whyKeyword not predicate so
syn keyword whyKeyword then type with
syn keyword whyKeyword abstract any
syn keyword whyKeyword abstract any break continue
syn keyword whyKeyword exception fun ghost label
syn keyword whyKeyword model mutable private
syn keyword whyKeyword raise rec return val while
......
......@@ -391,7 +391,6 @@ type dspec = ity -> dspec_final
clauses must have the type of the corresponding exception. *)
let old_mark = "'Old"
let old_mark_id = id_fresh old_mark
(** Expressions *)
......@@ -428,6 +427,7 @@ and dexpr_node =
| DEraise of dxsymbol * dexpr
| DEghost of dexpr
| DEexn of preid * dity * mask * dexpr
| DEoptexn of preid * dity * mask * dexpr
| DEassert of assertion_kind * term later
| DEpure of term later * dity
| DEvar_pure of string * dvty
......@@ -813,6 +813,9 @@ let dexpr ?loc node =
| DEtrue
| DEfalse ->
dvty_bool
| DEoptexn (_,dity,_,de) ->
dexpr_expected_type de dity;
[], dity
| DEcast (de,dity) ->
dexpr_expected_type de dity;
de.de_dvty
......@@ -1303,12 +1306,13 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
let ld, env = rec_defn uloc env drdf in
cexp uloc env de (LD (LS ld) :: lpl)
| DEexn (id,dity,mask,de) ->
let mask = if env.ghs then MaskGhost else mask in
let xs = create_xsymbol id ~mask (ity_of_dity dity) in
cexp uloc (add_xsymbol env xs) de (LD (LX xs) :: lpl)
| DEmark (id,de) ->
let env, old = add_label env id.pre_name in
cexp uloc env de (LD (LL old) :: lpl)
| DEvar_pure _ | DEpv_pure _
| DEvar_pure _ | DEpv_pure _ | DEoptexn _
| DEsym _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _
| DEassign _ | DEwhile _ | DEfor _ | DEtry _ | DEraise _ | DEassert _
| DEpure _ | DEabsurd | DEtrue | DEfalse -> assert false (* expr-only *)
......@@ -1460,8 +1464,17 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DEfalse ->
e_false
| DEexn (id,dity,mask,de) ->
let mask = if env.ghs then MaskGhost else mask in
let xs = create_xsymbol id ~mask (ity_of_dity dity) in
e_exn xs (expr uloc (add_xsymbol env xs) de)
| DEoptexn (id,dity,mask,de) ->
let mask = if env.ghs then MaskGhost else mask in
let xs = create_xsymbol id ~mask (ity_of_dity dity) in
let e = expr uloc (add_xsymbol env xs) de in
if not (Sxs.mem xs e.e_effect.eff_raises) then e else
let vl = vl_of_mask (id_fresh "r") mask xs.xs_ity in
let branches = Mxs.singleton xs (vl, e_of_vl vl) in
e_exn xs (e_try e ~case:false branches)
| DEmark (id,de) ->
let env, old = add_label env id.pre_name in
let put _ (ld,_) e = e_let ld e in
......@@ -1525,15 +1538,7 @@ and lambda uloc env pvl mask dsp dvl de =
let env = add_binders {env with ugh} pvl in
let preold = Mstr.find_opt old_mark env.old in
let env, old = add_label env old_mark in
let e = if pvl = [] then expr uloc env de else
let ity = ity_of_dity (dity_of_dvty de.de_dvty) in
let mask = if env.ghs then MaskGhost else mask in
let xs = create_xsymbol old_mark_id ~mask ity in
let e = expr uloc (add_xsymbol env xs) de in
if not (Sxs.mem xs e.e_effect.eff_raises) then e else
let vl = vl_of_mask (id_fresh "r") mask xs.xs_ity in
let branches = Mxs.singleton xs (vl, e_of_vl vl) in
e_exn xs (e_try e ~case:false branches) in
let e = expr uloc env de in
let dsp = get_later env dsp e.e_ity in
let dvl = get_later env dvl in
let dvl = rebase_variant env preold old dvl in
......
......@@ -58,12 +58,11 @@ type dbinder = preid option * ghost * dity
exception UnboundLabel of string
val old_mark : string
val old_mark_id : preid
val old_mark : string
type register_old = pvsymbol -> string -> pvsymbol
(** Program variables occurring under [old] or [at] are passed to
a registrar function. The label string must be ["0"] for [old]. *)
a registrar function. The label string must be ["'Old"] for [old]. *)
type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a
(** Specification terms are parsed and typechecked after the program
......@@ -121,6 +120,7 @@ and dexpr_node =
| DEraise of dxsymbol * dexpr
| DEghost of dexpr
| DEexn of preid * dity * mask * dexpr
| DEoptexn of preid * dity * mask * dexpr
| DEassert of assertion_kind * term later
| DEpure of term later * dity
| DEvar_pure of string * dvty
......
......@@ -26,10 +26,12 @@
[
"as", AS;
"axiom", AXIOM;
"break", BREAK;
"by", BY;
"clone", CLONE;
"coinductive", COINDUCTIVE;
"constant", CONSTANT;
"continue", CONTINUE;
"else", ELSE;
"end", END;
"epsilon", EPSILON;
......
......@@ -94,11 +94,9 @@
sp_diverge = s1.sp_diverge || s2.sp_diverge;
}
(* dead code
let add_init_mark e =
let init = { id_str = "Init"; id_lab = []; id_loc = e.expr_loc } in
{ e with expr_desc = Emark (init, e) }
*)
let break_id = "'Break"
let continue_id = "'Continue"
let return_id = "'Return"
let error_param loc =
Loc.errorm ~loc "cannot determine the type of the parameter"
......@@ -130,8 +128,8 @@
(* program keywords *)
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN BREAK CHECK
%token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
......@@ -675,11 +673,15 @@ kind:
rec_defn:
| ghost kind labels(lident_rich) binders ret_opt spec EQUAL spec seq_expr
{ $3, $1, $2, $4, fst $5, snd $5, spec_union $6 $8, $9 }
{ let id = mk_id return_id $startpos($7) $endpos($7) in
let e = { $9 with expr_desc = Eoptexn (id, snd $5, $9) } in
$3, $1, $2, $4, fst $5, snd $5, spec_union $6 $8, e }
fun_defn:
| binders ret_opt spec EQUAL spec seq_expr
{ Efun ($1, fst $2, snd $2, spec_union $3 $5, $6) }
{ let id = mk_id return_id $startpos($4) $endpos($4) in
let e = { $6 with expr_desc = Eoptexn (id, snd $2, $6) } in
Efun ($1, fst $2, snd $2, spec_union $3 $5, e) }
val_defn:
| params ret_opt spec
......@@ -801,7 +803,9 @@ single_expr_:
| LET REC with_list1(rec_defn) IN seq_expr
{ Erec ($3, $5) }
| FUN binders spec ARROW spec seq_expr
{ Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, $6) }
{ let id = mk_id return_id $startpos($4) $endpos($4) in
let e = { $6 with expr_desc = Eoptexn (id, Ity.MaskVisible, $6) } in
Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, e) }
| ANY return spec
{ Eany ([], Expr.RKnone, Some (fst $2), snd $2, $3) }
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
......@@ -815,12 +819,40 @@ single_expr_:
{ Eexn ($2, PTtuple [], Ity.MaskVisible, $4) }
| EXCEPTION labels(uident) return IN seq_expr
{ Eexn ($2, fst $3, snd $3, $5) }
| LABEL labels(uident) IN seq_expr
{ Emark ($2, $4) }
| LABEL id = labels(uident) IN e = seq_expr
{ let cont e =
let id = { id with id_str = id.id_str ^ continue_id } in
{ e with expr_desc = Eoptexn (id, Ity.MaskVisible, e) } in
let rec over_loop e = { e with expr_desc = over_loop_desc e }
and over_loop_desc e = match e.expr_desc with
| Escope (q, e1) -> Escope (q, over_loop e1)
| Enamed (l, e1) -> Enamed (l, over_loop e1)
| Ecast (e1, t) -> Ecast (over_loop e1, t)
| Eghost e1 -> Eghost (over_loop e1)
| Esequence (e1, e2) -> Esequence (over_loop e1, e2)
| Eoptexn (id, mask, e1) -> Eoptexn (id, mask, over_loop e1)
| Ewhile (e1, inv, var, e2) ->
let e = { e with expr_desc = Ewhile (e1, inv, var, cont e2) } in
let id = { id with id_str = id.id_str ^ break_id } in
Eoptexn (id, Ity.MaskVisible, e)
| Efor (id, ef, dir, et, inv, e1) ->
let e = { e with expr_desc = Efor (id,ef,dir,et,inv,cont e1) } in
let id = { id with id_str = id.id_str ^ break_id } in
Eoptexn (id, Ity.MaskVisible, e)
| d -> d in
Emark (id, over_loop e) }
| WHILE seq_expr DO loop_annotation seq_expr DONE
{ let inv, var = $4 in Ewhile ($2, inv, var, $5) }
{ let id_b = mk_id break_id $startpos($3) $endpos($3) in
let id_c = mk_id continue_id $startpos($3) $endpos($3) in
let e = { $5 with expr_desc = Eoptexn (id_c, Ity.MaskVisible, $5) } in
let e = mk_expr (Ewhile ($2, fst $4, snd $4, e)) $startpos $endpos in
Eoptexn (id_b, Ity.MaskVisible, e) }
| FOR lident_nq EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
{ Efor ($2, $4, $5, $6, $8, $9) }
{ let id_b = mk_id break_id $startpos($7) $endpos($7) in
let id_c = mk_id continue_id $startpos($7) $endpos($7) in
let e = { $9 with expr_desc = Eoptexn (id_c, Ity.MaskVisible, $9) } in
let e = mk_expr (Efor ($2, $4, $5, $6, $8, e)) $startpos $endpos in
Eoptexn (id_b, Ity.MaskVisible, e) }
| ABSURD
{ Eabsurd }
| RAISE uqualid expr_arg?
......@@ -828,7 +860,18 @@ single_expr_:
| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR
{ Eraise ($3, $4) }
| RETURN ioption(contract_expr)
{ Eraise (Qident (mk_id Dexpr.old_mark $startpos($1) $endpos($1)), $2) }
{ let id = mk_id return_id $startpos($1) $endpos($1) in
Eraise (Qident id, $2) }
| BREAK ioption(uident)
{ let id = match $2 with
| Some id -> { id with id_str = id.id_str ^ break_id }
| None -> mk_id break_id $startpos($1) $endpos($1) in
Eraise (Qident id, None) }
| CONTINUE ioption(uident)
{ let id = match $2 with
| Some id -> { id with id_str = id.id_str ^ continue_id }
| None -> mk_id continue_id $startpos($1) $endpos($1) in
Eraise (Qident id, None) }
| TRY seq_expr WITH bar_list1(exn_handler) END
{ Etry ($2, false, $4) }
| GHOST single_expr
......
......@@ -144,6 +144,7 @@ and expr_desc =
| Eidpur of qualid
| Eraise of qualid * expr option
| Eexn of ident * pty * Ity.mask * expr
| Eoptexn of ident * Ity.mask * expr
| Etry of expr * bool * (qualid * pattern option * expr) list
| Efor of ident * expr * Expr.for_direction * expr * invariant * expr
(* annotations *)
......
......@@ -711,8 +711,6 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let ds = dspec_no_variant muc sp in
let dity = dity_of_opt muc pty in
let denv = denv_add_args denv bl in
let denv = if bl = [] then denv else
denv_add_exn denv old_mark_id dity in
DEfun (bl, dity, msk, ds, dexpr muc denv e)
| Ptree.Eany (pl, kind, pty, msk, sp) ->
let pl = List.map (dparam muc) pl in
......@@ -809,9 +807,13 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
DEpure (get_term, denv_pure denv get_dty)
| Ptree.Eassert (ak, f) ->
DEassert (ak, dassert muc f)
| Ptree.Emark (id, e1) ->
| Ptree.Eoptexn (id, mask, e1) ->
let dity = dity_fresh () in
let id = create_user_id id in
DEmark (id, dexpr muc denv e1)
let denv = denv_add_exn denv id dity in
DEoptexn (id, dity, mask, dexpr muc denv e1)
| Ptree.Emark (id, e1) ->
DEmark (create_user_id id, dexpr muc denv e1)
| Ptree.Escope (q, e1) ->
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
......@@ -833,7 +835,6 @@ and drec_defn muc denv fdl =
let dity = dity_of_opt muc pty in
let pre denv =
let denv = denv_add_args denv bl in
let denv = denv_add_exn denv old_mark_id dity in
let dv = dvariant muc sp.sp_variant in
dspec muc sp, dv, dexpr muc denv e in
create_user_id id, gh, kind, bl, dity, msk, pre in
......
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