Commit 79923ded authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: make the ref type built-in and handle the "ref" keyword

parent 137d4d2c
......@@ -8,7 +8,6 @@ prelude "#include <assert.h>"
module ref.Ref
syntax type ref "%1"
syntax val ref "%1"
syntax val (!_) "%1"
syntax converter (!_) "%1"
syntax val (:=) "%1 = %2"
......
......@@ -51,7 +51,6 @@ end
module ref.Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
......
......@@ -71,7 +71,6 @@ end
module ref.Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
......
......@@ -25,7 +25,7 @@
(defconst why3-font-lock-keywords-1
(list
`(,(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" "partial" "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)
`(,(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" "partial" "raise" "ref" "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")
......
......@@ -209,6 +209,7 @@ on linking described in file LICENSE.
<keyword>match</keyword>
<keyword>not</keyword>
<keyword>raise</keyword>
<keyword>ref</keyword>
<keyword>rec</keyword>
<keyword>return</keyword>
<keyword>so</keyword>
......
......@@ -10,7 +10,7 @@ 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,%
predicate,private,pure,raise,raises,reads,rec,requires,result,return,%
predicate,private,pure,raise,raises,reads,rec,ref,requires,result,return,%
returns,scope,so,then,theory,to,true,try,type,use,val,variant,while,%
with,writes},%
string=[b]",%
......
......@@ -94,7 +94,7 @@ syn keyword whyKeyword then type with
syn keyword whyKeyword abstract any break continue
syn keyword whyKeyword exception fun ghost label
syn keyword whyKeyword model mutable partial private
syn keyword whyKeyword raise rec return val while
syn keyword whyKeyword raise rec ref return val while
syn keyword whyBoolean true false
......
......@@ -156,6 +156,8 @@ module Print = struct
(print_list comma (print_expr info)) tl
| _, None, [t1] when isfield ->
fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
| _, None, [t1] when rs_equal rs rs_ref_cons ->
fprintf fmt "@[<hov 2>ref %a@]" (print_expr ~paren:true info) t1
| _, None, tl when isconstructor () -> let pjl = get_record info rs in
begin match pjl, tl with
| [], [] ->
......
......@@ -766,6 +766,8 @@ module MLToC = struct
let n = Number.compute_int_constant ic in
let e = C.(Econst (Cint (BigInt.to_string n))) in
([], return_or_expr env e)
| Eapp (rs, [e]) when rs_equal rs Pmodule.rs_ref_cons ->
expr info env e
| Eapp (rs, el) ->
Debug.dprintf debug_c_extraction "call to %s@." rs.rs_name.id_string;
if is_rs_tuple rs && env.computes_return_value
......
......@@ -372,7 +372,7 @@ let e_attr_copy { e_attrs = attrs; e_loc = loc } e =
let loc = if e.e_loc = None then loc else e.e_loc in
{ e with e_attrs = attrs; e_loc = loc }
let proxy_attr = create_attribute "whyml_proxy_symbol"
let proxy_attr = create_attribute "mlw:proxy_symbol"
let proxy_attrs = Sattr.singleton proxy_attr
let rec e_attr_push ?loc l e = match e.e_node with
......
......@@ -507,7 +507,8 @@ let built_in_modules =
] ;
["ref"],"Ref",
[], (* ? *)
["ref", exec_ref_make ;
["mk ref", exec_ref_make ;
"contents", exec_ref_get ;
Ident.op_prefix "!", exec_ref_get;
Ident.op_infix ":=", exec_ref_set;
] ;
......
......@@ -344,6 +344,8 @@ module Print = struct
fprintf fmt "@[(%a)@]" (print_list comma (print_expr info)) tl
| _, None, [t1] when isfield ->
fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
| _, None, [t1] when rs_equal rs rs_ref_cons ->
fprintf fmt "@[<hov 2>ref %a@]" (print_expr ~paren:true info) t1
| _, None, tl when isconstructor () ->
let pjl = get_record info rs in
begin match pjl, tl with
......
......@@ -71,6 +71,12 @@ let same_overload r1 r2 =
| FixedRes t1, FixedRes t2 -> ity_equal t1 t2
| _ -> false (* two NoOver's are not the same *)
let ref_attr = Ident.create_attribute "mlw:reference_var"
let has_ref s =
let has v = Sattr.mem ref_attr v.pv_vs.vs_name.id_attrs in
List.exists has s.rs_cty.cty_args
exception IncompatibleNotation of string
let merge_ps chk x vo vn =
......@@ -87,12 +93,14 @@ let merge_ps chk x vo vn =
(* but we can merge two compatible symbols *)
| RS r1, RS r2 ->
if rs_equal r1 r2 then vo else
if has_ref r1 || has_ref r2 then vn else
if not (same_overload r1 r2) then vn else
if ity_equal (fsty r1) (fsty r2) then vn else
OO (Srs.add r2 (Srs.singleton r1))
(* or add a compatible symbol to notation *)
| OO s1, RS r2 ->
if Srs.mem r2 s1 then vo else
if has_ref r2 then vn else
let r1 = Srs.choose s1 in
if not (same_overload r1 r2) then vn else
let ty = fsty r2 in
......@@ -398,6 +406,26 @@ let unit_module =
let td = create_alias_decl (id_fresh "unit") [] ity_unit in
close_module (List.fold_left add uc (create_type_decl [td]))
let itd_ref =
let tv = create_tvsymbol (id_fresh "a") in
let attrs = Sattr.singleton (create_attribute "model_trace:") in
let pj = create_pvsymbol (id_fresh ~attrs "contents") (ity_var tv) in
create_plain_record_decl ~priv:false ~mut:true (id_fresh "ref")
[tv] [true, pj] [] []
let its_ref = itd_ref.itd_its
let rs_ref_cons = List.hd itd_ref.itd_constructors
let rs_ref_proj = List.hd itd_ref.itd_fields
let ts_ref = its_ref.its_ts
let ls_ref_cons = ls_of_rs rs_ref_cons
let ls_ref_proj = ls_of_rs rs_ref_proj
let ref_module =
let add uc d = add_pdecl_raw ~warn:false uc d in
let uc = empty_module dummy_env (id_fresh "Ref") ["why3";"Ref"] in
close_module (List.fold_left add uc (create_type_decl [itd_ref]))
let create_module env ?(path=[]) n =
let m = empty_module env n path in
let m = use_export m builtin_module in
......@@ -408,6 +436,8 @@ let create_module env ?(path=[]) n =
let add_use uc d = Sid.fold (fun id uc ->
if id_equal id ts_func.ts_name then
use_export uc highord_module
else if id_equal id ts_ref.ts_name then
use_export uc ref_module
else match is_ts_tuple_id id with
| Some n -> use_export uc (tuple_module n)
| None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc
......@@ -1187,6 +1217,7 @@ end)
let mlw_language_builtin =
let builtin s =
if s = unit_module.mod_theory.th_name.id_string then unit_module else
if s = ref_module.mod_theory.th_name.id_string then ref_module else
if s = builtin_theory.th_name.id_string then builtin_module else
if s = highord_theory.th_name.id_string then highord_module else
if s = bool_theory.th_name.id_string then bool_module else
......
......@@ -48,6 +48,8 @@ type overload =
val overload_of_rs : rsymbol -> overload
val ref_attr : Ident.attribute
exception IncompatibleNotation of string
(** {2 Module} *)
......@@ -138,6 +140,14 @@ val bool_module : pmodule
val unit_module : pmodule
val highord_module : pmodule
val tuple_module : int -> pmodule
val ref_module : pmodule
val its_ref : itysymbol
val ts_ref : tysymbol
val rs_ref_cons : rsymbol
val rs_ref_proj : rsymbol
val ls_ref_cons : lsymbol
val ls_ref_proj : lsymbol
(** {2 WhyML language} *)
......
......@@ -85,6 +85,7 @@
"raises", RAISES;
"reads", READS;
"rec", REC;
"ref", REF;
"requires", REQUIRES;
"return", RETURN;
"returns", RETURNS;
......@@ -222,6 +223,8 @@ rule token = parse
{ DOT }
| ".."
{ DOTDOT }
| "&"
{ AMP }
| "|"
{ BAR }
| "<"
......
......@@ -166,6 +166,18 @@
let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
[mk_t (Tattr (ATstr we_attr, p))]
let set_ref id =
List.iter (function
| ATstr a when Ident.attr_equal a Pmodule.ref_attr ->
Loc.errorm ~loc:id.id_loc "this variable is already a reference"
| _ -> ()) id.id_ats;
{ id with id_ats = ATstr Pmodule.ref_attr :: id.id_ats }
let set_ref_opt loc r = function
| id when not r -> id
| Some id -> Some (set_ref id)
| None -> Loc.errorm ~loc "anonymous parameters cannot be references"
let error_param loc =
Loc.errorm ~loc "cannot determine the type of the parameter"
......@@ -208,13 +220,13 @@
%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 PARTIAL
%token PRIVATE PURE RAISE RAISES READS REC REQUIRES
%token PRIVATE PURE RAISE RAISES READS REF REC REQUIRES
%token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
(* symbols *)
%token AND ARROW
%token BAR
%token AMP BAR
%token COLON COMMA
%token DOT DOTDOT EQUAL LT GT LTGT MINUS
%token LEFTPAR LEFTSQ
......@@ -493,10 +505,12 @@ ind_case:
ty:
| ty_arg { $1 }
| REF ty_arg+ { PTref $2 }
| lqualid ty_arg+ { PTtyapp ($1, $2) }
| ty ARROW ty { PTarrow ($1, $3) }
ty_arg:
| REF { PTref [] }
| lqualid { PTtyapp ($1, []) }
| quote_lident { PTtyvar $1 }
| uqualid DOT ty_block { PTscope ($1, $3) }
......@@ -524,7 +538,7 @@ params: param* { List.concat $1 }
binders: binder+ { List.concat $1 }
param:
| anon_binder
| special_binder
{ error_param (floc $startpos $endpos) }
| lident_nq attr+
{ error_param (floc $startpos $endpos) }
......@@ -533,18 +547,20 @@ param:
| LEFTPAR GHOST ty RIGHTPAR
{ [floc $startpos $endpos, None, true, $3] }
| LEFTPAR binder_vars_rest RIGHTPAR
{ match $2 with [l,_] -> error_param l
{ match snd $2 with [l,_] -> error_param l
| _ -> error_loc (floc $startpos($3) $endpos($3)) }
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
{ match $3 with [l,_] -> error_param l
{ match snd $3 with [l,_] -> error_param l
| _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
{ List.map (fun (l,i) -> l, i, false, $3) $2 }
{ let r = fst $2 in let ty = if r then PTref [$3] else $3 in
List.map (fun (l,i) -> l, set_ref_opt l r i, false, ty) (snd $2) }
| LEFTPAR GHOST binder_vars cast RIGHTPAR
{ List.map (fun (l,i) -> l, i, true, $4) $3 }
{ let r = fst $3 in let ty = if r then PTref [$4] else $4 in
List.map (fun (l,i) -> l, set_ref_opt l r i, true, ty) (snd $3) }
binder:
| anon_binder
| special_binder
{ let l,i = $1 in [l, i, false, None] }
| lident_nq attr+
{ [floc $startpos $endpos, Some (add_attr $1 $2), false, None] }
......@@ -552,39 +568,49 @@ binder:
{ match $1 with
| PTtyapp (Qident id, [])
| PTparen (PTtyapp (Qident id, [])) ->
[floc $startpos $endpos, Some id, false, None]
| _ -> [floc $startpos $endpos, None, false, Some $1] }
[floc $startpos $endpos, Some id, false, None]
| PTparen (PTref [PTtyapp (Qident id, [])]) ->
let id = set_ref id in
[floc $startpos $endpos, Some id, false, None]
| _ -> [floc $startpos $endpos, None, false, Some $1] }
| LEFTPAR GHOST ty RIGHTPAR
{ match $3 with
| PTtyapp (Qident id, []) ->
[floc $startpos $endpos, Some id, true, None]
| _ -> [floc $startpos $endpos, None, true, Some $3] }
[floc $startpos $endpos, Some id, true, None]
| PTref [PTtyapp (Qident id, [])] ->
let id = set_ref id in
[floc $startpos $endpos, Some id, true, None]
| _ -> [floc $startpos $endpos, None, true, Some $3] }
| LEFTPAR binder_vars_rest RIGHTPAR
{ match $2 with [l,i] -> [l, i, false, None]
{ match snd $2 with [l,i] -> [l, set_ref_opt l (fst $2) i, false, None]
| _ -> error_loc (floc $startpos($3) $endpos($3)) }
| LEFTPAR GHOST binder_vars_rest RIGHTPAR
{ match $3 with [l,i] -> [l, i, true, None]
{ match snd $3 with [l,i] -> [l, set_ref_opt l (fst $3) i, true, None]
| _ -> error_loc (floc $startpos($4) $endpos($4)) }
| LEFTPAR binder_vars cast RIGHTPAR
{ List.map (fun (l,i) -> l, i, false, Some $3) $2 }
{ let r = fst $2 in let ty = if r then PTref [$3] else $3 in
List.map (fun (l,i) -> l, set_ref_opt l r i, false, Some ty) (snd $2) }
| LEFTPAR GHOST binder_vars cast RIGHTPAR
{ List.map (fun (l,i) -> l, i, true, Some $4) $3 }
{ let r = fst $3 in let ty = if r then PTref [$4] else $4 in
List.map (fun (l,i) -> l, set_ref_opt l r i, true, Some ty) (snd $3) }
binder_vars:
| binder_vars_head { List.rev $1 }
| binder_vars_head { fst $1, match snd $1 with
| [] -> Loc.error ~loc:(floc $startpos $endpos) Error
| bl -> List.rev bl }
| binder_vars_rest { $1 }
binder_vars_rest:
| binder_vars_head attr+ binder_var*
{ List.rev_append (match $1 with
{ let l2 = floc $startpos($2) $endpos($2) in
fst $1, List.rev_append (match snd $1 with
| (l, Some id) :: bl ->
let l2 = floc $startpos($2) $endpos($2) in
(Loc.join l l2, Some (add_attr id $2)) :: bl
| _ -> assert false) $3 }
| binder_vars_head anon_binder binder_var*
{ List.rev_append $1 ($2 :: $3) }
| anon_binder binder_var*
{ $1 :: $2 }
| _ -> Loc.error ~loc:l2 Error) $3 }
| binder_vars_head special_binder binder_var*
{ fst $1, List.rev_append (snd $1) ($2 :: $3) }
| special_binder binder_var*
{ false, $1 :: $2 }
binder_vars_head:
| ty {
......@@ -593,15 +619,18 @@ binder_vars_head:
| PTtyapp (Qident id, []) -> of_id id :: acc
| _ -> Loc.error ~loc:(floc $startpos $endpos) Error in
match $1 with
| PTtyapp (Qident id, l) -> List.fold_left push [of_id id] l
| PTtyapp (Qident id, l) ->
false, List.fold_left push [of_id id] l
| PTref l -> true, List.fold_left push [] l
| _ -> Loc.error ~loc:(floc $startpos $endpos) Error }
binder_var:
| attrs(lident_nq) { floc $startpos $endpos, Some $1 }
| anon_binder { $1 }
| special_binder { $1 }
anon_binder:
| UNDERSCORE { floc $startpos $endpos, None }
special_binder:
| UNDERSCORE { floc $startpos $endpos, None }
| AMP attrs(lident_nq) { floc $startpos $endpos, Some (set_ref $2) }
(* Logical terms *)
......@@ -924,6 +953,10 @@ single_expr_:
{ Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
| LET ghost kind attrs(lident_op_nq) mk_expr(fun_defn) IN seq_expr
{ Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
| LET ghost REF attrs(lident_nq) EQUAL seq_expr IN seq_expr
{ let rf = mk_expr Eref $startpos($3) $endpos($3) in
let ee = { $6 with expr_desc = Eapply (rf, $6) } in
Elet (set_ref $4, ghost $2, Expr.RKnone, apply_partial $2 ee, $8) }
| LET REC with_list1(rec_defn) IN seq_expr
{ Erec ($3, $5) }
| FUN binders spec ARROW spec seq_expr
......@@ -1024,6 +1057,7 @@ expr_dot: e = mk_expr(expr_dot_) { e }
expr_arg_:
| qualid { Eident $1 }
| numeral { Econst $1 }
| REF { Eref }
| TRUE { Etrue }
| FALSE { Efalse }
| o = oppref ; a = expr_arg { Eidapp (Qident o, [a]) }
......@@ -1225,6 +1259,8 @@ pat_uni_:
pat_arg_:
| UNDERSCORE { Pwild }
| AMP attrs(lident_nq) { Pvar (add_model_trace_attr
(set_ref $2)) }
| attrs(lident_nq) { Pvar (add_model_trace_attr $1) }
| uqualid { Papp ($1,[]) }
| uqualid DOT mk_pat(pat_block_) { Pscope ($1,$3) }
......@@ -1327,6 +1363,8 @@ sident:
| lident { $1 }
| uident { $1 }
| STRING { mk_id $1 $startpos $endpos }
| REF { mk_id "ref" $startpos $endpos }
(* TODO: we can add other keywords and save on quotes *)
quote_lident:
| QUOTE_LIDENT { mk_id $1 $startpos $endpos }
......@@ -1427,13 +1465,17 @@ semicolon_list1(X):
located(X): X { $1, $startpos, $endpos }
(* Parsing of a list of qualified identifiers for the ITP *)
qualid_extended:
| qualid { $1 }
| REF { Qident (mk_id "ref" $startpos $endpos) }
qualid_eof:
| qualid EOF { $1 }
| qualid_extended EOF { $1 }
qualid_comma_list_eof:
| comma_list1(qualid) EOF { $1 }
| comma_list1(qualid_extended) EOF { $1 }
ident_comma_list_eof:
| comma_list1(ident) EOF { $1 }
......
......@@ -31,6 +31,7 @@ type pty =
| PTtyvar of ident
| PTtyapp of qualid * pty list
| PTtuple of pty list
| PTref of pty list
| PTarrow of pty * pty
| PTscope of qualid * pty
| PTparen of pty
......@@ -120,6 +121,7 @@ type expr = {
}
and expr_desc =
| Eref
| Etrue
| Efalse
| Econst of Number.constant
......
......@@ -118,6 +118,8 @@ let rec ty_of_pty ns = function
| PTtuple tyl ->
let s = its_tuple (List.length tyl) in
ty_app s.its_ts (List.map (ty_of_pty ns) tyl)
| PTref tyl ->
ty_app ts_ref (List.map (ty_of_pty ns) tyl)
| PTarrow (ty1, ty2) ->
ty_func (ty_of_pty ns ty1) (ty_of_pty ns ty2)
| PTscope (q, ty) ->
......@@ -438,6 +440,8 @@ let rec ity_of_pty muc = function
Loc.try3 ~loc:(qloc q) ity_app s tyl []
| PTtuple tyl ->
ity_tuple (List.map (ity_of_pty muc) tyl)
| PTref tyl ->
ity_app its_ref (List.map (ity_of_pty muc) tyl) []
| PTarrow (ty1, ty2) ->
ity_func (ity_of_pty muc ty1) (ity_of_pty muc ty2)
| PTpure ty ->
......@@ -809,6 +813,8 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let dty = if Mts.is_empty muc.muc_theory.uc_floats
then dity_real else dity_fresh () in
DEconst(c, dty)
| Ptree.Eref ->
DEsym (RS rs_ref_cons)
| Ptree.Erecord fl ->
let ls_of_rs rs = match rs.rs_logic with
| RLls ls -> ls | _ -> assert false in
......@@ -1153,6 +1159,7 @@ let add_types muc tdl =
find_itysymbol muc q in
Loc.try3 ~loc:(qloc q) ity_app s (List.map (down muc) tyl) []
| PTtuple tyl -> ity_tuple (List.map (down muc) tyl)
| PTref tyl -> ity_app its_ref (List.map (down muc) tyl) []
| PTarrow (ty1,ty2) -> ity_func (down muc ty1) (down muc ty2)
| PTpure ty -> ity_purify (down muc ty)
| PTscope (q,ty) ->
......
......@@ -13,13 +13,9 @@
module Ref
type ref 'a = { mutable contents [@model_trace:] : 'a }
use export why3.Ref.Ref
function (!) (x: ref 'a) : 'a = x.contents
let ref (v: 'a) ensures { result = { contents = v } } = { contents = v }
let (!) (r:ref 'a) ensures { result = !r } = r.contents
let function (!) (r: ref 'a) = r.contents
let (:=) (r:ref 'a) (v:'a) ensures { !r = v } = r.contents <- v
......
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