Commit b8fb2e85 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: "alias { t1 with t2, t3 with t4 }" annotation

Forces aliasing between the arguments, external reads and the
result (denoted "result"). Cannot be used for exceptional results.
Currently, is only used for "any" and "val", and is silently ignored
otherwise.
parent 4a48a9ee
......@@ -69,6 +69,7 @@ let empty_spec = {
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
......
......@@ -39,8 +39,9 @@
let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
let empty_spec = {
sp_pre = []; sp_post = []; sp_xpost = [];
sp_reads = []; sp_writes = []; sp_variant = [];
sp_pre = []; sp_post = []; sp_xpost = [];
sp_reads = []; sp_writes = []; sp_alias = [];
sp_variant = [];
sp_checkrw = false; sp_diverge = false;
}
......@@ -50,6 +51,7 @@
sp_xpost = s1.sp_xpost @ s2.sp_xpost;
sp_reads = s1.sp_reads @ s2.sp_reads;
sp_writes = s1.sp_writes @ s2.sp_writes;
sp_alias = s1.sp_alias @ s2.sp_alias;
sp_variant = variant_union s1.sp_variant s2.sp_variant;
sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
sp_diverge = s1.sp_diverge || s2.sp_diverge;
......
......@@ -28,7 +28,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . 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 '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "alias" "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" "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")
......
......@@ -216,6 +216,7 @@ on linking described in file LICENSE.
</context>
<context id="spec" style-ref="spec-keyword">
<keyword>absurd</keyword>
<keyword>alias</keyword>
<keyword>assert</keyword>
<keyword>assume</keyword>
<keyword>at</keyword>
......
......@@ -5,7 +5,7 @@
\lstdefinelanguage{why3}
{
basicstyle=\ttfamily,%
morekeywords=[1]{abstract,absurd,any,assert,assume,at,axiom,break,by,%
morekeywords=[1]{abstract,absurd,alias,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,%
......
......@@ -101,7 +101,7 @@ syn keyword whyBoolean true false
syn keyword whyType bool int list map option real
syn keyword whyType array ref unit
syn keyword whySpec absurd assert assume check diverges ensures invariant
syn keyword whySpec absurd alias assert assume check diverges ensures invariant
syn keyword whySpec pure raises reads requires returns variant writes at old
syn match whyConstructor "(\s*)"
......
......@@ -24,6 +24,7 @@
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[
"alias", ALIAS;
"as", AS;
"axiom", AXIOM;
"break", BREAK;
......
......@@ -78,6 +78,7 @@
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
......@@ -89,6 +90,7 @@
sp_xpost = s1.sp_xpost @ s2.sp_xpost;
sp_reads = s1.sp_reads @ s2.sp_reads;
sp_writes = s1.sp_writes @ s2.sp_writes;
sp_alias = s1.sp_alias @ s2.sp_alias;
sp_variant = variant_union s1.sp_variant s2.sp_variant;
sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
sp_diverge = s1.sp_diverge || s2.sp_diverge;
......@@ -128,7 +130,7 @@
(* program keywords *)
%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN BREAK CHECK
%token ABSTRACT ABSURD ALIAS 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
......@@ -159,7 +161,7 @@
%nonassoc prec_no_else
%nonassoc DOT ELSE RETURN
%nonassoc prec_no_spec
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES DIVERGES VARIANT
%nonassoc REQUIRES ENSURES RETURNS RAISES READS WRITES ALIAS DIVERGES VARIANT
%nonassoc below_LARROW
%nonassoc LARROW
%nonassoc below_COMMA
......@@ -998,6 +1000,8 @@ single_spec:
{ { empty_spec with sp_reads = $3; sp_checkrw = true } }
| WRITES LEFTBRC comma_list0(single_term) RIGHTBRC
{ { empty_spec with sp_writes = $3; sp_checkrw = true } }
| ALIAS LEFTBRC comma_list0(alias) RIGHTBRC
{ { empty_spec with sp_alias = $3; sp_checkrw = true } }
| RAISES LEFTBRC comma_list1(xsymbol) RIGHTBRC
{ { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
| DIVERGES
......@@ -1005,6 +1009,9 @@ single_spec:
| variant
{ { empty_spec with sp_variant = $1 } }
alias:
| term WITH term { $1, $3 }
ensures:
| term
{ let id = mk_id "result" $startpos $endpos in
......@@ -1162,10 +1169,11 @@ lident_rich:
lident_op_id:
| LEFTPAR lident_op RIGHTPAR { mk_id $2 $startpos($2) $endpos($2) }
| LEFTPAR_STAR_RIGHTPAR
{ (* parentheses are removed from the location *)
let s = let s = $startpos in { s with pos_cnum = s.pos_cnum + 1 } in
let e = let e = $endpos in { e with pos_cnum = e.pos_cnum - 1 } in
mk_id (infix "*") s e }
{ (* parentheses are removed from the location *)
let s = $startpos and e = $endpos in
let s = { s with Lexing.pos_cnum = s.Lexing.pos_cnum + 1 } in
let e = { e with Lexing.pos_cnum = e.Lexing.pos_cnum - 1 } in
mk_id (infix "*") s e }
lident_op:
| op_symbol { infix $1 }
......
......@@ -103,6 +103,7 @@ type spec = {
sp_xpost : xpost list;
sp_reads : qualid list;
sp_writes : term list;
sp_alias : (term * term) list;
sp_variant : variant;
sp_checkrw : bool;
sp_diverge : bool;
......
......@@ -624,6 +624,48 @@ let local_kind = function
| RKfunc | RKpred -> RKlocal
| k -> k
let rec eff_dterm muc denv {term_desc = desc; term_loc = loc} =
let expr_app loc e el =
List.fold_left (fun e1 e2 ->
DEapp (Dexpr.dexpr ~loc e1, e2)) e el
in
let qualid_app loc q el =
let e = try DEsym (find_prog_symbol muc q) with
| _ -> DEls_pure (find_lsymbol muc.muc_theory q, false) in
expr_app loc e el
in
let qualid_app loc q el = match q with
| Qident {id_str = n} ->
(match denv_get_opt denv n with
| Some d -> expr_app loc d el
| None -> qualid_app loc q el)
| _ -> qualid_app loc q el
in
Dexpr.dexpr ~loc (match desc with
| Ptree.Tident q ->
qualid_app loc q []
| Ptree.Tidapp (q, [e1]) ->
qualid_app loc q [eff_dterm muc denv e1]
| Ptree.Tapply (e1, e2) ->
DEapp (eff_dterm muc denv e1, eff_dterm muc denv e2)
| Ptree.Tscope (q, e1) ->
let muc = open_scope muc "dummy" in
let muc = import_scope muc (string_list_of_qualid q) in
DElabel (eff_dterm muc denv e1, Slab.empty)
| Ptree.Tnamed (Lpos uloc, e1) ->
DEuloc (eff_dterm muc denv e1, uloc)
| Ptree.Tnamed (Lstr lab, e1) ->
DElabel (eff_dterm muc denv e1, Slab.singleton lab)
| Ptree.Tcast (e1, pty) ->
let d1 = eff_dterm muc denv e1 in
DEcast (d1, dity_of_pty muc pty)
| Ptree.Tat _ -> Loc.errorm ~loc "`at' and `old' cannot be used here"
| Ptree.Tidapp _ | Ptree.Tconst _ | Ptree.Tinfix _ | Ptree.Tinnfix _
| Ptree.Ttuple _ | Ptree.Tlet _ | Ptree.Tmatch _ | Ptree.Tif _
| Ptree.Ttrue | Ptree.Tfalse | Ptree.Tnot _ | Ptree.Tbinop _ | Ptree.Tbinnop _
| Ptree.Tquant _ | Ptree.Trecord _ | Ptree.Tupdate _ ->
Loc.errorm ~loc "unsupported effect expression")
let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let expr_app loc e el =
List.fold_left (fun e1 e2 ->
......@@ -747,7 +789,18 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| RKlemma, None -> ity_unit
| RKpred, None -> ity_bool
| _ -> Loc.errorm ~loc "cannot determine the type of the result" in
DEany (pl, dity_of_ity ity, msk, ds)
let dity = dity_of_ity ity in
let res = Some (id_fresh "result"), false, dity in
let denv = denv_add_args denv (res::pl) in
let add_alias (t1, t2) =
let bty = dity_fresh () in
let dt1 = eff_dterm muc denv t1 in
let dt2 = eff_dterm muc denv t2 in
ignore (Dexpr.dexpr ~loc:t1.term_loc (DEcast (dt1, bty)));
ignore (Dexpr.dexpr ~loc:t2.term_loc (DEcast (dt2, bty)));
in
List.iter add_alias sp.sp_alias;
DEany (pl, dity, msk, ds)
| Ptree.Ematch (e1, bl) ->
let e1 = dexpr muc denv e1 in
let branch (pp, e) =
......
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