Commit 3c7026a2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

admit formulas in Elogic

parent 00091957
......@@ -1056,8 +1056,7 @@ expr:
| expr EQUAL expr
{ mk_infix $1 "=" $3 }
| expr LTGT expr
{ let t = mk_infix $1 "=" $3 in
mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = floc () } [t]) }
{ mk_expr (Enot (mk_infix $1 "=" $3)) }
| expr LARROW expr
{ match $1.expr_desc with
| Eapply (e11, e12) -> begin match e11.expr_desc with
......@@ -1081,7 +1080,7 @@ expr:
| expr OP4 expr
{ mk_infix $1 $2 $3 }
| NOT expr %prec prec_prefix_op
{ mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = floc () } [$2]) }
{ mk_expr (Enot $2) }
| prefix_op expr %prec prec_prefix_op
{ mk_prefix $1 $2 }
| expr_arg list1_expr_arg %prec prec_app
......
......@@ -221,6 +221,7 @@ and expr_desc =
| Eif of expr * expr * expr
| Eloop of loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Enot of expr
| Ematch of expr * (pattern * expr) list
| Eabsurd
| Eraise of qualid * expr option
......
......@@ -93,6 +93,7 @@ and dexpr_desc =
| DEif of dexpr * dexpr * dexpr
| DEloop of dloop_annotation * dexpr
| DElazy of lazy_op * dexpr * dexpr
| DEnot of dexpr
| DEmatch of dexpr * (Denv.dpattern * dexpr) list
| DEabsurd
| DEraise of esymbol * dexpr option
......@@ -192,6 +193,7 @@ and iexpr_desc =
| IEif of iexpr * iexpr * iexpr
| IEloop of loop_annotation * iexpr
| IElazy of lazy_op * iexpr * iexpr
| IEnot of iexpr
| IEmatch of ivsymbol * (ipattern * iexpr) list
| IEabsurd
| IEraise of esymbol * iexpr option
......
......@@ -87,9 +87,10 @@ let find_ls ~pure uc s =
(* TODO: improve efficiency *)
let dty_bool uc = tyapp (find_ts ~pure:true uc "bool") []
let dty_int _uc = tyapp Ty.ts_int []
let dty_unit _uc = tyapp (ts_tuple 0) []
let dty_mark _uc = tyapp ts_mark []
let dty_int = tyapp Ty.ts_int []
let dty_unit = tyapp (Ty.ts_tuple 0) []
let dty_mark = tyapp ts_mark []
(* note: local variables are simultaneously in locals (to type programs)
and in denv (to type logic elements) *)
......@@ -444,6 +445,10 @@ and dexpr_desc ~ghost ~userloc env loc = function
let e2 = dexpr ~ghost ~userloc env e2 in
expected_type e2 (dty_bool env.uc);
DElazy (op, e1, e2), dty_bool env.uc
| Ptree.Enot e1 ->
let e1 = dexpr ~ghost ~userloc env e1 in
expected_type e1 (dty_bool env.uc);
DEnot e1, dty_bool env.uc
| Ptree.Eapply (e1, e2) ->
let e1 = dexpr ~ghost ~userloc env e1 in
(* let ghost = ghost || is_ps_ghost e1 in *)
......@@ -590,13 +595,13 @@ and dexpr_desc ~ghost ~userloc env loc = function
try mutable_field mt.mt_effect i
with Not_found -> errorm ~loc "not a mutable field"
in
DEassign (e1, ls, j, e2), dty_unit env.uc
DEassign (e1, ls, j, e2), dty_unit
| None ->
errorm ~loc "unbound record field %a" print_qualid q
end
| Ptree.Esequence (e1, e2) ->
let e1 = dexpr ~ghost ~userloc env e1 in
expected_type e1 (dty_unit env.uc);
expected_type e1 dty_unit;
let e2 = dexpr ~ghost ~userloc env e2 in
DEsequence (e1, e2), e2.dexpr_type
| Ptree.Eif (e1, e2, e3) ->
......@@ -608,8 +613,8 @@ and dexpr_desc ~ghost ~userloc env loc = function
DEif (e1, e2, e3), e2.dexpr_type
| Ptree.Eloop (a, e1) ->
let e1 = dexpr ~ghost ~userloc env e1 in
expected_type e1 (dty_unit env.uc);
DEloop (dloop_annotation env a, e1), dty_unit env.uc
expected_type e1 dty_unit;
DEloop (dloop_annotation env a, e1), dty_unit
| Ptree.Ematch (e1, bl) ->
let e1 = dexpr ~ghost ~userloc env e1 in
let ty1 = e1.dexpr_type in
......@@ -668,20 +673,19 @@ and dexpr_desc ~ghost ~userloc env loc = function
DEtry (e1, List.map handler hl), e1.dexpr_type
| Ptree.Efor (x, e1, d, e2, inv, e3) ->
let e1 = dexpr ~ghost ~userloc env e1 in
expected_type e1 (dty_int env.uc);
expected_type e1 dty_int;
let e2 = dexpr ~ghost ~userloc env e2 in
expected_type e2 (dty_int env.uc);
let env = add_local env x.id (dty_int env.uc) in
expected_type e2 dty_int;
let env = add_local env x.id dty_int in
let e3 = dexpr ~ghost ~userloc env e3 in
expected_type e3 (dty_unit env.uc);
DEfor (x, e1, d, e2, inv, e3), dty_unit env.uc
expected_type e3 dty_unit;
DEfor (x, e1, d, e2, inv, e3), dty_unit
| Ptree.Eassert (k, le) ->
DEassert (k, le), dty_unit env.uc
DEassert (k, le), dty_unit
| Ptree.Emark ({id=s}, e1) ->
if Typing.mem_var s env.denv then
errorm ~loc "clash with previous mark %s" s;
let ty = dty_mark env.uc in
let env = { env with denv = add_pure_var s ty env.denv } in
let env = { env with denv = add_pure_var s dty_mark env.denv } in
let e1 = dexpr ~ghost ~userloc env e1 in
DEmark (s, e1), e1.dexpr_type
| Ptree.Ecast (e1, ty) ->
......@@ -972,23 +976,23 @@ let rec purify_itype_v = function
(List.map (fun (v,_) -> v.i_impure.vs_ty) bl)
(purify_itype_v c.ic_result_type)
let rec iutype_v gl env = function
let rec iutype_v env = function
| DUTpure ty ->
ITpure (Denv.ty_of_dty ty)
| DUTarrow (bl, c) ->
let env, bl = map_fold_left (iubinder gl) env bl in
ITarrow (bl, iutype_c gl env c)
let env, bl = map_fold_left iubinder env bl in
ITarrow (bl, iutype_c env c)
and iutype_c gl env c =
let tyv = iutype_v gl env c.duc_result_type in
and iutype_c env c =
let tyv = iutype_v env c.duc_result_type in
let ty = purify_itype_v tyv in
{ ic_result_type = tyv;
ic_effect = iueffect env c.duc_effect;
ic_pre = ifmla env c.duc_pre;
ic_post = iupost env ty c.duc_post; }
and iubinder gl env (x, ty, tyv) =
let tyv = iutype_v gl env tyv in
and iubinder env (x, ty, tyv) =
let tyv = iutype_v env tyv in
let ty = Denv.ty_of_dty ty in
let env, v = iadd_local env (id_user x.id x.id_loc) ty in
env, (v, tyv)
......@@ -996,11 +1000,6 @@ and iubinder gl env (x, ty, tyv) =
let mk_iexpr loc ty d =
{ iexpr_desc = d; iexpr_loc = loc; iexpr_lab = []; iexpr_type = ty }
let mk_t_if gl f =
let ty = ty_app (find_ts ~pure:true gl "bool") [] in
t_if f (fs_app (find_ls ~pure:true gl "True") [] ty)
(fs_app (find_ls ~pure:true gl "False") [] ty)
(* apply ls to a list of expressions, introducing let's if necessary
ls [e1; e2; ...; en]
......@@ -1011,15 +1010,14 @@ let mk_t_if gl f =
let xn = en in
ls(x1,x2,...,xn)
*)
let make_logic_app gl loc ty ls el =
let make_logic_app loc ty ls el =
let rec make lvars gvars args = function
| [] ->
begin match ls.ls_value with
| Some _ ->
let t = fs_app ls (List.rev args) (purify ty) in
IElogic (t, lvars, gvars)
IElogic (fs_app ls (List.rev args) (purify ty), lvars, gvars)
| None ->
IElogic (mk_t_if gl (ps_app ls (List.rev args)), lvars, gvars)
IElogic (ps_app ls (List.rev args), lvars, gvars)
end
| ({ iexpr_desc = IElogic (t, lvt, gvt) }, _, _) :: r ->
make (Svs.union lvars lvt) (Spv.union gvars gvt) (t :: args) r
......@@ -1039,7 +1037,7 @@ let make_logic_app gl loc ty ls el =
f [e1; e2; ...; en]
-> let x1 = e1 in ... let xn = en in (...((f x1) x2)... xn)
*)
let make_app _gl loc ty f el =
let make_app loc ty f el =
let mk_iexpr loc lab ty d =
let ie = mk_iexpr loc ty d in
{ ie with iexpr_lab = lab }
......@@ -1164,13 +1162,13 @@ let drown_lab d e =
(* [iexpr] translates dexpr into iexpr
[env : vsymbol Mstr.t] maps strings to vsymbols for local variables *)
let rec iexpr gl env e =
let rec iexpr env e =
let ty = Denv.ty_of_dty e.dexpr_type in
let d = iexpr_desc gl env e.dexpr_loc ty e.dexpr_desc in
let d = iexpr_desc env e.dexpr_loc ty e.dexpr_desc in
drown_lab e { iexpr_desc = d; iexpr_type = ty;
iexpr_loc = e.dexpr_loc; iexpr_lab = [] }
and iexpr_desc gl env loc ty = function
and iexpr_desc env loc ty = function
| DEconstant c ->
IElogic (t_const c, Svs.empty, Spv.empty)
| DElocal (x, _) ->
......@@ -1184,41 +1182,41 @@ and iexpr_desc gl env loc ty = function
| [], Some _ ->
IElogic (fs_app ls [] (purify ty), Svs.empty, Spv.empty)
| [], None ->
IElogic (mk_t_if gl (ps_app ls []), Svs.empty, Spv.empty)
IElogic (ps_app ls [], Svs.empty, Spv.empty)
| al, _ ->
errorm ~loc "function symbol %s is expecting %d arguments"
ls.ls_name.id_string (List.length al)
end
| DEapply (e1, e2) ->
let f, args = decompose_app gl env e1 [iexpr gl env e2, ty, []] in
let f, args = decompose_app env e1 [iexpr env e2, ty, []] in
begin match f.dexpr_desc with
| DElogic ls ->
let n = List.length ls.ls_args in
if List.length args <> n then
errorm ~loc "function symbol %s is expecting %d arguments"
ls.ls_name.id_string n;
make_logic_app gl loc ty ls args
make_logic_app loc ty ls args
| _ ->
let f = iexpr gl env f in
let e = make_app gl loc ty f args in
let f = iexpr env f in
let e = make_app loc ty f args in
e.iexpr_desc
end
| DEfun (bl, e1) ->
let env, bl = map_fold_left (iubinder gl) env bl in
IEfun (bl, itriple gl env e1)
let env, bl = map_fold_left iubinder env bl in
IEfun (bl, itriple env e1)
| DElet (x, e1, e2) ->
let e1 = iexpr gl env e1 in
let e1 = iexpr env e1 in
let env, v = iadd_local env (id_user x.id x.id_loc) e1.iexpr_type in
IElet (v, e1, iexpr gl env e2)
IElet (v, e1, iexpr env e2)
| DEletrec (dl, e1) ->
let env, dl = iletrec gl env dl in
let e1 = iexpr gl env e1 in
let env, dl = iletrec env dl in
let e1 = iexpr env e1 in
IEletrec (dl, e1)
| DEassign (e1, ls, j, e2) ->
(* e1.f <- e2 is syntactic sugar for
let x1 = e1 in let x2 = e2 in any {} writes f { x1.f = x2 } *)
let e1 = iexpr gl env e1 in
let e2 = iexpr gl env e2 in
let e1 = iexpr env e1 in
let e2 = iexpr env e2 in
let x1 = create_ivsymbol (id_fresh "x") e1.iexpr_type in
let x2 = create_ivsymbol (id_fresh "x") e2.iexpr_type in
let r = match e1.iexpr_type.ty_node with
......@@ -1244,9 +1242,9 @@ and iexpr_desc gl env loc ty = function
IEany c))))
| DEsequence (e1, e2) ->
let vs = create_ivsymbol (id_fresh "_") (ty_app (ts_tuple 0) []) in
IElet (vs, iexpr gl env e1, iexpr gl env e2)
IElet (vs, iexpr env e1, iexpr env e2)
| DEif (e1, e2, e3) ->
IEif (iexpr gl env e1, iexpr gl env e2, iexpr gl env e3)
IEif (iexpr env e1, iexpr env e2, iexpr env e3)
| DEloop (la, e1) ->
let la =
{ loop_invariant =
......@@ -1254,16 +1252,18 @@ and iexpr_desc gl env loc ty = function
loop_variant =
option_map (ivariant env) la.dloop_variant; }
in
IEloop (la, iexpr gl env e1)
IEloop (la, iexpr env e1)
| DElazy (op, e1, e2) ->
IElazy (op, iexpr gl env e1, iexpr gl env e2)
IElazy (op, iexpr env e1, iexpr env e2)
| DEnot e1 ->
IEnot (iexpr env e1)
| DEmatch (e1, bl) ->
let e1 = iexpr gl env e1 in
let e1 = iexpr env e1 in
let branch (p, e) =
let envi = Mstr.map (fun v -> v.i_impure) env.i_impures in
let _, p = Denv.pattern envi p in
let env, p = ipattern env p in
(p, iexpr gl env e)
(p, iexpr env e)
in
let bl = List.map branch bl in
let v = create_ivsymbol (id_user "x" loc) e1.iexpr_type in
......@@ -1271,7 +1271,7 @@ and iexpr_desc gl env loc ty = function
| DEabsurd ->
IEabsurd
| DEraise (ls, e) ->
IEraise (ls, option_map (iexpr gl env) e)
IEraise (ls, option_map (iexpr env) e)
| DEtry (e, hl) ->
let handler (ls, x, h) =
let x, env = match x with
......@@ -1282,17 +1282,17 @@ and iexpr_desc gl env loc ty = function
| None ->
None, env
in
(ls, x, iexpr gl env h)
(ls, x, iexpr env h)
in
IEtry (iexpr gl env e, List.map handler hl)
IEtry (iexpr env e, List.map handler hl)
| DEfor (x, e1, d, e2, inv, e3) ->
List.iter
(fun s -> ignore (find_int_ls ~loc env.i_uc s)) ["infix <"; "infix +"];
let e1 = iexpr gl env e1 in
let e2 = iexpr gl env e2 in
let e1 = iexpr env e1 in
let e2 = iexpr env e2 in
let env, vx = iadd_local env (id_user x.id x.id_loc) e1.iexpr_type in
let inv = option_map (ifmla env) inv in
let e3 = iexpr gl env e3 in
let e3 = iexpr env e3 in
let v1 = create_ivsymbol (id_user "for_start" loc) e1.iexpr_type in
let v2 = create_ivsymbol (id_user "for_end" loc) e2.iexpr_type in
IElet (v1, e1, mk_iexpr loc ty (
......@@ -1303,20 +1303,20 @@ and iexpr_desc gl env loc ty = function
IEassert (k, f)
| DEmark (s, e1) ->
let env, v = iadd_local env (id_fresh s) ty_mark in
IEmark (v.i_impure, iexpr gl env e1)
IEmark (v.i_impure, iexpr env e1)
| DEany c ->
let c = iutype_c gl env c in
let c = iutype_c env c in
IEany c
and decompose_app gl env e args = match e.dexpr_desc with
and decompose_app env e args = match e.dexpr_desc with
| DEapply (e1, e2) ->
let lab = e.dexpr_lab in
let ty = Denv.ty_of_dty e.dexpr_type in
decompose_app gl env e1 ((iexpr gl env e2, ty, lab) :: args)
decompose_app env e1 ((iexpr env e2, ty, lab) :: args)
| _ ->
e, args
and iletrec gl env dl =
and iletrec env dl =
(* add all functions into env, and compute local env *)
let step1 env ((x, dty), bl, var, t) =
let ty = Denv.ty_of_dty dty in
......@@ -1326,9 +1326,9 @@ and iletrec gl env dl =
let env, dl = map_fold_left step1 env dl in
(* then translate variants and bodies *)
let step2 (v, bl, var, (_,_,_ as t)) =
let env, bl = map_fold_left (iubinder gl) env bl in
let env, bl = map_fold_left iubinder env bl in
let var = option_map (ivariant env) var in
let t = itriple gl env t in
let t = itriple env t in
let var, t = match var with
| None ->
None, t
......@@ -1374,9 +1374,9 @@ and iletrec gl env dl =
end;
env, dl
and itriple gl env (p, e, q) =
and itriple env (p, e, q) =
let p = ifmla env p in
let e = iexpr gl env e in
let e = iexpr env e in
let ty = e.iexpr_type in
let q = iupost env ty q in
(p, e, q)
......@@ -1691,6 +1691,13 @@ and expr_desc gl env loc ty = function
Eif (e1, mk_true loc gl, e2)
in
d, tpure ty, ef
| IEnot e1 ->
let e1 = expr gl env e1 in
let ls = find_ls ~pure:true gl "notb" in
let v1 = create_pvsymbol_v (id_fresh "lazy") (tpure ty) in
let t = fs_app ls [t_var v1.pv_pure] ty in
let d = Elet (v1, e1, mk_simple_expr loc ty (Elogic t)) in
d, tpure ty, e1.expr_effect
| IEmatch (i, bl) ->
let v = Mvs.find i.i_impure env in
let branch ef (p, e) =
......@@ -2252,7 +2259,7 @@ let rec decl ~wp env penv ltm lmod uc = function
| Ptree.Dlet (id, e) ->
let denv = create_denv uc in
let e = dexpr ~ghost:false ~userloc:None denv e in
let e = iexpr uc (create_ienv denv) e in
let e = iexpr (create_ienv denv) e in
let e = expr uc Mvs.empty e in
check_region_vars ();
if Debug.test_flag debug then
......@@ -2267,7 +2274,7 @@ let rec decl ~wp env penv ltm lmod uc = function
| Ptree.Dletrec dl ->
let denv = create_denv uc in
let _, dl = dletrec ~ghost:false ~userloc:None denv dl in
let _, dl = iletrec uc (create_ienv denv) dl in
let _, dl = iletrec (create_ienv denv) dl in
let _, dl = letrec uc Mvs.empty dl in
check_region_vars ();
let one uc (v, _, _, _ as d) =
......@@ -2290,7 +2297,7 @@ let rec decl ~wp env penv ltm lmod uc = function
let loc = id.id_loc in
let denv = create_denv uc in
let tyv = dutype_v denv tyv in
let tyv = iutype_v uc (create_ienv denv) tyv in
let tyv = iutype_v (create_ienv denv) tyv in
let tyv = type_v Mvs.empty tyv in
if cannot_be_generalized tyv then errorm ~loc "cannot be generalized";
if Debug.test_flag debug then
......
......@@ -411,14 +411,10 @@ let well_founded_rel = function
(* Recursive computation of the weakest precondition *)
let t_True env =
fs_app (find_ls ~pure:true env "True") []
(ty_app (find_ts ~pure:true env "bool") [])
(*
let add_expl msg f =
t_label_add Split_goal.stop_split (t_label_add ("expl:"^msg) f)
*)
let ty_bool env = ty_app (find_ts ~pure:true env "bool") []
let t_True env = fs_app (find_ls ~pure:true env "True") [] (ty_bool env)
let t_False env = fs_app (find_ls ~pure:true env "False") [] (ty_bool env)
let mk_t_if env f = t_if f (t_True env) (t_False env)
(*
env : module_uc
......@@ -430,7 +426,6 @@ let rec wp_expr env rm e q =
let q = post_map (old_mark lab) q in
let f = wp_desc env rm e q in
let f = erase_mark lab f in
(* let f = wp_label e f in *)
if Debug.test_flag debug then begin
eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Pgm_pretty.print_expr e;
eprintf "@[<hov 2>q = %a@]@\n" Pretty.print_term (snd (fst q));
......@@ -441,7 +436,9 @@ let rec wp_expr env rm e q =
and wp_desc env rm e q = match e.expr_desc with
| Elogic t ->
let (v, q), _ = q in
t_subst_single v (wp_label e t) q
let t = wp_label e t in
let t = if t.t_ty = None then mk_t_if env t else t in
t_subst_single v t q
| Elocal pv ->
let (v, q), _ = q in
t_subst_single v (wp_label e (t_var pv.pv_pure)) q
......@@ -654,34 +651,44 @@ let wp_rec env (_,_,_,ef as def) =
let f = wp_recfun env rm def in
wp_close rm ef f
let rec t_btop env t = match t.t_node with
| Tif (f,t1,t2) -> let f = f_btop env f in
t_label t.t_label (t_if_simp f (t_btop env t1) (t_btop env t2))
| Tapp (ls, [t1;t2]) when ls_equal ls (find_ls ~pure:true env "andb") ->
t_label t.t_label (t_and_simp (t_btop env t1) (t_btop env t2))
| Tapp (ls, [t1;t2]) when ls_equal ls (find_ls ~pure:true env "orb") ->
t_label t.t_label (t_or_simp (t_btop env t1) (t_btop env t2))
| Tapp (ls, [t1]) when ls_equal ls (find_ls ~pure:true env "notb") ->
t_label t.t_label (t_not_simp (t_btop env t1))
| Tapp (ls, []) when ls_equal ls (find_ls ~pure:true env "True") ->
t_label t.t_label t_true
| Tapp (ls, []) when ls_equal ls (find_ls ~pure:true env "False") ->
t_label t.t_label t_false
| _ ->
t_equ (f_btop env t) (t_True env)
and f_btop env f = match f.t_node with
| Tapp (ls, [{t_ty = Some {ty_node = Tyapp (ts, [])}} as l; r])
when ls_equal ls ps_equ && ts_equal ts (find_ts ~pure:true env "bool") ->
t_label_copy f (t_iff_simp (t_btop env l) (t_btop env r))
| _ -> t_map (f_btop env) f
let bool_to_prop env f =
let ts_bool = find_ts ~pure:true env "bool" in
let ls_andb = find_ls ~pure:true env "andb" in
let ls_orb = find_ls ~pure:true env "orb" in
let ls_notb = find_ls ~pure:true env "notb" in
let ls_True = find_ls ~pure:true env "True" in
let ls_False = find_ls ~pure:true env "False" in
let t_True = fs_app ls_True [] (ty_app ts_bool []) in
let rec t_btop t = t_label ?loc:t.t_loc t.t_label (* t_label_copy? *)
(match t.t_node with
| Tif (f,t1,t2) ->
t_if_simp (f_btop f) (t_btop t1) (t_btop t2)
| Tapp (ls, [t1;t2]) when ls_equal ls ls_andb ->
t_and_simp (t_btop t1) (t_btop t2)
| Tapp (ls, [t1;t2]) when ls_equal ls ls_orb ->
t_or_simp (t_btop t1) (t_btop t2)
| Tapp (ls, [t1]) when ls_equal ls ls_notb ->
t_not_simp (t_btop t1)
| Tapp (ls, []) when ls_equal ls ls_True ->
t_true
| Tapp (ls, []) when ls_equal ls ls_False ->
t_false
| _ ->
t_equ (f_btop t) t_True)
and f_btop f = match f.t_node with
| Tapp (ls, [{t_ty = Some {ty_node = Tyapp (ts, [])}} as l; r])
when ls_equal ls ps_equ && ts_equal ts ts_bool ->
t_label_copy f (t_iff_simp (t_btop l) (t_btop r))
| _ -> t_map f_btop f
in
f_btop f
let add_wp_decl ps f uc =
let name = ps.ps_pure.ls_name in
let s = "WP_" ^ name.id_string in
let label = ["expl:" ^ name.id_string] in
let id = id_fresh ~label ?loc:name.id_loc s in
let f = f_btop uc f in
let f = bool_to_prop uc f in
let km = get_known (pure_uc uc) in
let f = eval_match ~inline:inline_nonrec_linear km f in
(* printf "wp: f=%a@." print_term f; *)
......
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