Commit 811ab575 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: ghost variables, functions, and expressions

parent 57635caf
......@@ -167,6 +167,13 @@ end
let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }
let effect_union e1 e2 =
let { pe_reads = r1; pe_writes = w1; pe_raises = x1 } = e1 in
let { pe_reads = r2; pe_writes = w2; pe_raises = x2 } = e2 in
{ pe_reads = r1 @ r2; pe_writes = w1 @ w2; pe_raises = x1 @ x2 }
let effect_exprs ghost l = List.map (fun x -> (ghost, x)) l
let type_c p ty ef q =
{ pc_result_type = ty;
pc_effect = ef;
......@@ -245,7 +252,7 @@ end
%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
%nonassoc DOT ELSE
%nonassoc DOT ELSE GHOST
%nonassoc prec_named
%nonassoc COLON
......@@ -1053,17 +1060,16 @@ program_decl:
{ Dlogic $1 }
| use_clone
{ Duseclone $1 }
| LET lident_rich_pgm labels list1_type_v_binder opt_cast EQUAL triple
{ Dlet (add_lab $2 $3, mk_expr_i 7 (Efun ($4, cast_body $5 $7))) }
| LET lident_rich_pgm labels EQUAL FUN list1_type_v_binder ARROW triple
{ Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET ghost lident_rich_pgm labels list1_type_v_binder opt_cast EQUAL triple
{ Dlet (add_lab $3 $4, $2, mk_expr_i 8 (Efun ($5, cast_body $6 $8))) }
| LET ghost lident_rich_pgm labels EQUAL FUN list1_type_v_binder ARROW triple
{ Dlet (add_lab $3 $4, $2, mk_expr_i 9 (Efun ($7, $9))) }
| LET REC list1_recfun_sep_and
{ Dletrec $3 }
| VAL lident_rich_pgm labels COLON type_v
{ Dparam (add_lab $2 $3, $5) }
| VAL lident_rich_pgm labels list1_type_v_param COLON type_c
{ let tv = Tarrow ($4, $6) in
Dparam (add_lab $2 $3, tv) }
| VAL ghost lident_rich_pgm labels COLON type_v
{ Dparam (add_lab $3 $4, $2, $6) }
| VAL ghost lident_rich_pgm labels list1_type_v_param COLON type_c
{ Dparam (add_lab $3 $4, $2, Tarrow ($5, $7)) }
| EXCEPTION uident labels
{ Dexn (add_lab $2 $3, None) }
| EXCEPTION uident labels primitive_type
......@@ -1099,8 +1105,9 @@ list1_recfun_sep_and:
;
recfun:
| lident_rich_pgm labels list1_type_v_binder opt_cast opt_variant EQUAL triple
{ add_lab $1 $2, $3, $5, cast_body $4 $7 }
| ghost lident_rich_pgm labels list1_type_v_binder
opt_cast opt_variant EQUAL triple
{ add_lab $2 $3, $1, $4, $6, cast_body $5 $8 }
;
expr:
......@@ -1152,10 +1159,16 @@ expr:
{ mk_expr (Elazy (LazyOr, $1, $3)) }
| LET pattern EQUAL expr IN expr
{ match $2.pat_desc with
| PPpvar id -> mk_expr (Elet (id, $4, $6))
| _ -> mk_expr (Ematch ($4, [$2, $6])) }
| PPpvar id -> mk_expr (Elet (id, false, $4, $6))
| _ -> mk_expr (Ematch ($4, [$2, $6])) }
| LET GHOST pattern EQUAL expr IN expr
{ match $3.pat_desc with
| PPpvar id -> mk_expr (Elet (id, true, $5, $7))
| _ -> Loc.errorm ~loc:(floc_i 3) "`ghost' cannot come before a pattern" }
| LET lident labels list1_type_v_binder EQUAL triple IN expr
{ mk_expr (Elet (add_lab $2 $3, mk_expr_i 6 (Efun ($4, $6)), $8)) }
{ mk_expr (Elet (add_lab $2 $3, false, mk_expr_i 6 (Efun ($4, $6)), $8)) }
| LET GHOST lident labels list1_type_v_binder EQUAL triple IN expr
{ mk_expr (Elet (add_lab $3 $4, true, mk_expr_i 7 (Efun ($5, $7)), $9)) }
| LET REC list1_recfun_sep_and IN expr
{ mk_expr (Eletrec ($3, $5)) }
| FUN list1_type_v_binder ARROW triple
......@@ -1190,6 +1203,8 @@ expr:
{ mk_expr (Etry ($2, $5)) }
| ANY simple_type_c
{ mk_expr (Eany $2) }
| GHOST expr
{ mk_expr (Eghost $2) }
| ABSTRACT expr post
{ mk_expr (Eabstract($2, $3)) }
| label expr %prec prec_named
......@@ -1309,17 +1324,17 @@ list1_type_v_param:
;
type_v_binder:
| lident labels
{ [add_lab $1 $2, None] }
| ghost lident labels
{ [add_lab $2 $3, $1, None] }
| type_v_param
{ $1 }
;
type_v_param:
| LEFTPAR RIGHTPAR
{ [id_anonymous (), Some (ty_unit ())] }
| LEFTPAR lidents_lab COLON primitive_type RIGHTPAR
{ List.map (fun i -> (i, Some $4)) $2 }
{ [id_anonymous (), false, Some (ty_unit ())] }
| LEFTPAR ghost lidents_lab COLON primitive_type RIGHTPAR
{ List.map (fun i -> (i, $2, Some $5)) $3 }
;
lidents_lab:
......@@ -1335,9 +1350,13 @@ type_v:
arrow_type_v:
| primitive_type ARROW type_c
{ Tarrow ([id_anonymous (), Some $1], $3) }
{ Tarrow ([id_anonymous (), false, Some $1], $3) }
| GHOST primitive_type ARROW type_c
{ Tarrow ([id_anonymous (), true, Some $2], $4) }
| lident labels COLON primitive_type ARROW type_c
{ Tarrow ([add_lab $1 $2, Some $4], $6) }
{ Tarrow ([add_lab $1 $2, false, Some $4], $6) }
| GHOST lident labels COLON primitive_type ARROW type_c
{ Tarrow ([add_lab $2 $3, true, Some $5], $7) }
/* TODO: we could alllow lidents instead, e.g. x y : int -> ... */
/*{ Tarrow (List.map (fun x -> x, Some $3) $1, $5) }*/
;
......@@ -1392,23 +1411,23 @@ post_exn:
;
effects:
| opt_reads opt_writes opt_raises
{ { pe_reads = $1; pe_writes = $2; pe_raises = $3 } }
| /* epsilon */ { empty_effect }
| effect effects { effect_union $1 $2 }
;
opt_reads:
| /* epsilon */ { [] }
| READS list1_lexpr_arg { $2 }
;
opt_writes:
| /* epsilon */ { [] }
| WRITES list1_lexpr_arg { $2 }
;
opt_raises:
| /* epsilon */ { [] }
| RAISES list1_uqualid { $2 }
effect:
| READS list1_lexpr_arg
{ { pe_reads = effect_exprs false $2; pe_writes = []; pe_raises = [] } }
| WRITES list1_lexpr_arg
{ { pe_writes = effect_exprs false $2; pe_reads = []; pe_raises = [] } }
| RAISES list1_uqualid
{ { pe_raises = effect_exprs false $2; pe_writes = []; pe_reads = [] } }
| GHOST READS list1_lexpr_arg
{ { pe_reads = effect_exprs true $3; pe_writes = []; pe_raises = [] } }
| GHOST WRITES list1_lexpr_arg
{ { pe_writes = effect_exprs true $3; pe_reads = []; pe_raises = [] } }
| GHOST RAISES list1_uqualid
{ { pe_raises = effect_exprs true $3; pe_writes = []; pe_reads = [] } }
;
opt_variant:
......@@ -1427,6 +1446,11 @@ list1_uqualid:
| uqualid list1_uqualid { $1 :: $2 }
;
ghost:
| /* epsilon */ { false }
| GHOST { true }
;
/*
Local Variables:
compile-command: "unset LANG; make -C ../.."
......
......@@ -186,17 +186,19 @@ type loop_annotation = {
type for_direction = To | Downto
type ghost = bool
type effect = {
pe_reads : lexpr list;
pe_writes : lexpr list;
pe_raises : qualid list;
pe_reads : (ghost * lexpr) list;
pe_writes : (ghost * lexpr) list;
pe_raises : (ghost * qualid) list;
}
type pre = lexpr
type post = lexpr * (qualid * lexpr) list
type binder = ident * pty option
type binder = ident * ghost * pty option
type type_v =
| Tpure of pty
......@@ -219,8 +221,9 @@ and expr_desc =
| Eident of qualid
| Eapply of expr * expr
| Efun of binder list * triple
| Elet of ident * expr * expr
| Eletrec of (ident * binder list * variant option * triple) list * expr
| Elet of ident * ghost * expr * expr
| Eletrec of
(ident * ghost * binder list * variant option * triple) list * expr
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eupdate of expr * (qualid * expr) list
......@@ -241,19 +244,18 @@ and expr_desc =
| Emark of ident * expr
| Ecast of expr * pty
| Eany of type_c
| Eghost of expr
| Eabstract of expr * post
| Enamed of label * expr
(* TODO: ghost *)
and triple = pre * expr * post
type program_decl =
| Dlet of ident * expr
| Dletrec of (ident * binder list * variant option * triple) list
| Dlet of ident * ghost * expr
| Dletrec of (ident * ghost * binder list * variant option * triple) list
| Dlogic of decl
| Duseclone of use_clone
| Dparam of ident * type_v
| Dparam of ident * ghost * type_v
| Dexn of ident * pty option
(* modules *)
| Duse of qualid * bool option * (*as:*) string option
......
......@@ -248,12 +248,17 @@ let dexception uc qid =
print_dty ty;
r
let no_ghost gh =
if gh then errorm "ghost types are not supported in this version of WhyML"
let eff_no_ghost l = List.map (fun (gh,x) -> no_ghost gh; x) l
let dueffect env e =
{ du_reads = e.Ptree.pe_reads;
du_writes = e.Ptree.pe_writes;
{ du_reads = eff_no_ghost e.Ptree.pe_reads;
du_writes = eff_no_ghost e.Ptree.pe_writes;
du_raises =
List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
e.Ptree.pe_raises; }
(eff_no_ghost e.Ptree.pe_raises); }
let dpost uc (q, ql) =
let dexn (id, l) = let s, _, _ = dexception uc id in s, l in
......@@ -309,7 +314,8 @@ and dutype_c env c =
duc_post = dpost env.uc c.Ptree.pc_post;
}
and dubinder env ({id=x; id_loc=loc} as id, v) =
and dubinder env ({id=x; id_loc=loc} as id, gh, v) =
no_ghost gh;
let ty = match v with
| Some v -> dtype ~user:true env v
| None -> create_type_var loc
......@@ -480,7 +486,8 @@ and dexpr_desc ~ghost ~userloc env loc = function
let tyl = List.map (fun (_,ty) -> ty) bl in
let ty = dcurrying tyl e.dexpr_type in
DEfun (bl, t), ty
| Ptree.Elet (x, e1, e2) ->
| Ptree.Elet (x, gh, e1, e2) ->
no_ghost gh;
let e1 = dexpr ~ghost ~userloc env e1 in
let ty1 = e1.dexpr_type in
let env = add_local env x.id ty1 in
......@@ -716,12 +723,16 @@ and dexpr_desc ~ghost ~userloc env loc = function
let e1 = dexpr ~ghost ~userloc env e1 in
let q = dpost env.uc q in
DEabstract(e1, q), e1.dexpr_type
| Ptree.Eghost _ ->
no_ghost true;
assert false
| Ptree.Enamed _ ->
assert false
and dletrec ~ghost ~userloc env dl =
(* add all functions into environment *)
let add_one env (id, bl, var, t) =
let add_one env (id, gh, bl, var, t) =
no_ghost gh;
let ty = create_type_var id.id_loc in
let env = add_local_top env id.id ty in
env, ((id, ty), bl, var, t)
......@@ -1560,7 +1571,7 @@ let rec is_pure_expr e =
| Elocal _ | Elogic _ -> true
| Eif (e1, e2, e3) -> is_pure_expr e1 && is_pure_expr e2 && is_pure_expr e3
| Elet (_, e1, e2) -> is_pure_expr e1 && is_pure_expr e2
| Eabstract (e1, _)
| Eabstract (e1, _)
| Emark (_, e1) -> is_pure_expr e1
| Eany c -> E.no_side_effect c.c_effect
| Eassert _ | Etry _ | Efor _ | Eraise _ | Ematch _
......@@ -2295,7 +2306,8 @@ let find_module penv lmod q id = match q with
(* env = to retrieve theories and modules from the loadpath
lmod = local modules *)
let rec decl ~wp env ltm lmod uc = function
| Ptree.Dlet (id, e) ->
| Ptree.Dlet (id, gh, e) ->
no_ghost gh;
let denv = create_denv uc in
let e = dexpr ~ghost:false ~userloc:None denv e in
let e = iexpr (create_ienv denv) e in
......@@ -2334,7 +2346,8 @@ let rec decl ~wp env ltm lmod uc = function
let d = Dletrec dl in
let uc = add_decl d uc in
if wp then Pgm_wp.decl uc d else uc
| Ptree.Dparam (id, tyv) ->
| Ptree.Dparam (id, gh, tyv) ->
no_ghost gh;
let loc = id.id_loc in
let denv = create_denv uc in
let tyv = dutype_v denv tyv in
......
......@@ -75,7 +75,7 @@ and dexpr_desc =
| DEglobal_ls of Term.lsymbol
| DEapply of dexpr * dexpr list
| DEfun of dlambda
| DElet of ident * dexpr * dexpr
| DElet of ident * ghost * dexpr * dexpr
| DEletrec of drecfun list * dexpr
| DEassign of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
......@@ -92,6 +92,6 @@ and dexpr_desc =
| DEghost of dexpr
| DEany of dtype_c
and drecfun = ident * dity * dlambda
and drecfun = ident * ghost * dity * dlambda
and dlambda = dbinder list * dvariant list * dpre * dexpr * dpost * dxpost
......@@ -668,6 +668,10 @@ let vtv_unmut vtv =
if vtv.vtv_mut = None then vtv else
vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity
let vty_ghost = function
| VTvalue vtv -> vtv.vtv_ghost
| VTarrow vta -> vta.vta_ghost
let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
(* mutable arguments are rejected outright *)
if vtv.vtv_mut <> None then
......@@ -681,14 +685,10 @@ let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
vta_arg = vtv;
vta_result = vty;
vta_effect = effect;
vta_ghost = ghost;
vta_ghost = ghost || vty_ghost vty;
vta_vars = vty_vars vtv.vtv_vars vty;
}
let vty_ghost = function
| VTvalue vtv -> vtv.vtv_ghost
| VTarrow vta -> vta.vta_ghost
let vtv_ghostify vtv = { vtv with vtv_ghost = true }
let vta_ghostify vta = { vta with vta_ghost = true }
......
This diff is collapsed.
......@@ -19,7 +19,7 @@ module N
type tree 'a = Node 'a (forest 'a) | Leaf
with forest 'a = Cons (tree 'a) (forest 'a) | Nil
type ref 'b = {| (* ghost *) mutable contents : 'b |}
type ref 'b = {| ghost mutable contents : 'b |}
type myrec 'a = {| f1 : int ; ghost f2 : tree 'a |}
......@@ -29,7 +29,7 @@ module N
let create_dref i = {| dcontents = {| contents = i |} |}
let foo (x : ref int) (y : ref int) =
let ghost foo (x : ref int) (y : ref int) =
x.contents <- 1;
y.contents <- 2
......@@ -40,16 +40,16 @@ module N
{} unit writes gr { gr.contents = (old gr.contents) + 4 }
let test () =
let ghost test () =
foo gr {| contents = 4 |}
let myfun r = { r = r }
let ghost myfun r = { r = r }
'L:
let rec on_tree t = { true } match t with
let rec ghost on_tree t = { true } match t with
| Node {| contents = v |} f -> v + on_forest f
| Leaf -> raise (Exit Leaf)
end { at r 'L = t }
with on_forest f = match f with
with ghost on_forest f = match f with
| Cons t f -> let ee = Leaf in on_tree t + on_forest f + on_tree ee
| Nil -> 1
end
......
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