Commit 729322d4 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: WP for function application (still in progress)

parent ed8085c2
......@@ -60,6 +60,8 @@ module Reference = struct
| Rlocal _, Rglobal _ -> -1
| Rglobal _, Rlocal _ -> 1
let equal r1 r2 = compare r1 r2 = 0
end
module Sref = Set.Make(Reference)
......@@ -84,6 +86,14 @@ let union t1 t2 =
writes = Sref.union t1.writes t2.writes;
raises = E.union t1.raises t2.raises; }
let subst vs r t =
let add1 r' s = match r' with
| Rlocal vs' when vs_equal vs' vs -> Sref.add r s
| _ -> Sref.add r' s
in
let apply s = Sref.fold add1 s Sref.empty in
{ reads = apply t.reads; writes = apply t.writes; raises = t.raises }
open Format
open Pp
open Pretty
......
......@@ -45,5 +45,7 @@ val add_raise : lsymbol -> t -> t
val union : t -> t -> t
val subst : vsymbol -> reference -> t -> t
val print_reference : Format.formatter -> reference -> unit
val print : Format.formatter -> t -> unit
......@@ -143,25 +143,7 @@ let type_c_of_type_v env = function
c_pre = f_true;
c_post = (v_result ty, f_true), []; }
let rec subst_type_c ts s c =
{ c_result_type = subst_type_v ts s c.c_result_type;
c_effect = c.c_effect;
c_pre = f_ty_subst ts s c.c_pre;
c_post = subst_post ts s c.c_post; }
and subst_type_v ts s = function
| Tpure ty ->
Tpure (ty_inst ts ty)
| Tarrow (bl, c) ->
let s, bl = Util.map_fold_left (binder ts) s bl in
Tarrow (bl, subst_type_c ts s c)
and binder ts s (vs, v) =
let v = subst_type_v ts s v in
let s, vs = subst_var ts s vs in
s, (vs, v)
and subst_var ts s vs =
let rec subst_var ts s vs =
let ty' = ty_inst ts vs.vs_ty in
if ty_equal ty' vs.vs_ty then
s, vs
......@@ -177,18 +159,44 @@ and subst_post ts s ((v, q), ql) =
in
vq, List.map handler ql
let rec subst_type_c ef ts s c =
{ c_result_type = subst_type_v ef ts s c.c_result_type;
c_effect = ef c.c_effect;
c_pre = f_ty_subst ts s c.c_pre;
c_post = subst_post ts s c.c_post; }
and subst_type_v ef ts s = function
| Tpure ty ->
Tpure (ty_inst ts ty)
| Tarrow (bl, c) ->
let s, bl = Util.map_fold_left (binder ef ts) s bl in
Tarrow (bl, subst_type_c ef ts s c)
and binder ef ts s (vs, v) =
let v = subst_type_v ef ts s v in
let s, vs = subst_var ts s vs in
s, (vs, v)
let subst1 vs1 vs2 = Mvs.add vs1 (t_var vs2) Mvs.empty
let apply_type_v env v vs = match v with
| Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify env.uc tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
subst_type_c ts (subst1 x vs) c
subst_type_c (fun e -> e) ts (subst1 x vs) c
| Tarrow ([], _) | Tpure _ ->
assert false
let apply_type_v_ref env v r =
assert false (*TODO*)
let apply_type_v_ref env v r = match r, v with
| E.Rlocal vs as r, Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify env.uc tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
let ef = E.subst x r in
subst_type_c ef ts (subst1 x vs) c
| E.Rglobal _, Tarrow ((_x, _tyx) :: _bl, _c) ->
assert false (*TODO*)
| _ ->
assert false
(* pretty-printers *)
......@@ -217,8 +225,13 @@ and print_type_c fmt c =
and print_binder fmt (x, v) =
fprintf fmt "(%a:%a)" print_vs x print_type_v v
let apply_type_v env v vs =
eprintf "apply_type_v: v=%a vs=%a@." print_type_v v print_vs vs;
apply_type_v env v vs
(* let apply_type_v env v vs = *)
(* eprintf "apply_type_v: v=%a vs=%a@." print_type_v v print_vs vs; *)
(* apply_type_v env v vs *)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
......@@ -408,10 +408,9 @@ and dexpr_desc env loc = function
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, lexpr le), dty_unit env.genv
| Pgm_ptree.Elabel ({id=l}, e1) ->
let s = "label " ^ l in
| Pgm_ptree.Elabel ({id=s}, e1) ->
if Typing.mem_var s env.denv then
errorm ~loc "clash with previous label %s" l;
errorm ~loc "clash with previous label %s" s;
let ty = dty_label env.genv in
let env = { env with denv = Typing.add_var s ty env.denv } in
let e1 = dexpr env e1 in
......@@ -750,9 +749,9 @@ let rec print_expr fmt e = match e.expr_desc with
| Eglobal ls ->
fprintf fmt "<global %a>" print_ls ls
| Eapply (e, vs) ->
fprintf fmt "@[(%a %a)@]" print_expr e print_vs vs
fprintf fmt "@[((%a) %a)@]" print_expr e print_vs vs
| Eapply_ref (e, r) ->
fprintf fmt "@[(%a <ref %a>)@]" print_expr e print_reference r
fprintf fmt "@[((%a) <ref %a>)@]" print_expr e print_reference r
| Efun (_, (_,e,_)) ->
fprintf fmt "@[fun _ ->@ %a@]" print_expr e
| Elet (v, e1, e2) ->
......
......@@ -58,6 +58,13 @@ let post_effect env ef ((_,q),ql) =
let add_binder env (x, v) = add_local x v env
let add_binders = List.fold_left add_binder
let make_apply loc e1 ty c =
let x = create_vsymbol (id_fresh "f") e1.expr_type in
let v = c.c_result_type and ef = c.c_effect in
let any_c = { expr_desc = Eany c; expr_type = ty;
expr_type_v = v; expr_effect = ef; expr_loc = loc } in
Elet (x, e1, any_c), v, ef
let rec expr env e =
let ty = e.Pgm_ttree.expr_type in
let loc = e.Pgm_ttree.expr_loc in
......@@ -65,7 +72,7 @@ let rec expr env e =
{ expr_desc = d; expr_type = ty;
expr_type_v = v; expr_effect = ef; expr_loc = loc }
and expr_desc env _loc ty = function
and expr_desc env loc ty = function
| Pgm_ttree.Elogic t ->
let ef = term_effect env E.empty t in
Elogic t, Tpure ty, ef
......@@ -78,12 +85,11 @@ and expr_desc env _loc ty = function
| Pgm_ttree.Eapply (e1, vs) ->
let e1 = expr env e1 in
let c = apply_type_v env e1.expr_type_v vs in
Eany c, c.c_result_type, c.c_effect
(* TODO: do not forget about e1 *)
make_apply loc e1 ty c
| Pgm_ttree.Eapply_ref (e1, r) ->
let e1 = expr env e1 in
let c = apply_type_v_ref env e1.expr_type_v r in
Eany c, c.c_result_type, c.c_effect
make_apply loc e1 ty c
| Pgm_ttree.Efun (bl, t) ->
let env = add_binders env bl in
let t, c = triple env t in
......@@ -200,6 +206,7 @@ and unref_term env r v t = match t.t_node with
(* quantify over all references in ef *)
let quantify env ef f =
(* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
let quantify1 r f =
let ty = unref_ty env (E.type_of_reference r) in
let v = create_vsymbol (id_clone (E.name_of_reference r)) ty in
......@@ -289,6 +296,10 @@ and wp_desc env e q = match e.expr_desc with
| Elogic t ->
let (v, q), _ = q in
f_let v t q
| Elocal _ ->
assert false (*TODO*)
| Eglobal _ ->
assert false (*TODO*)
| Efun (bl, t) ->
let (_, q), _ = q in
let f = wp_triple env t in
......@@ -299,6 +310,8 @@ and wp_desc env e q = match e.expr_desc with
let q1 = result, f_subst (subst1 x result) w2 in
let q1 = saturate_post e1.expr_effect q1 q in
wp_expr env e1 q1
| Eletrec _ ->
assert false (*TODO*)
| Esequence (e1, e2) ->
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
......
......@@ -14,11 +14,19 @@ parameter r : int ref
parameter write : v:int -> {} unit writes r { !r = v }
let ff () =
{ true }
(fun x -> {x=0} x+42 { result=42 }) 0
{ result=40+2 }
(*
let ff () =
{ !r >= 0 }
!r + 2
{ !r = 44 }
let x = ref 2 in
imp_sub r x;
!r
{ result = 42 }
*)
(*
Local Variables:
......
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