programs: fixed capture bug in program types

parent 747bc5fe
{
use import int.Gcd
use import int.ComputerDivision
}
let rec gcd u v variant { v } =
{ u >= 0 and v >= 0 }
if v = 0 then
u
else
gcd v (mod u v)
{ gcd u v result }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/gcd"
End:
*)
......@@ -47,7 +47,7 @@
}
{
(* use import int.ComputerDivision *)
use import int.ComputerDivision
}
let rec sd n =
......
......@@ -94,9 +94,9 @@ let equal t1 t2 =
let no_side_effect t =
Sref.is_empty t.writes && Sls.is_empty t.raises
let subst vs r t =
let subst m t =
let add1 r' s = match r' with
| Rlocal vs' when vs_equal vs' vs -> Sref.add r s
| Rlocal vs' -> Sref.add (try Mvs.find vs' m with Not_found -> r') s
| _ -> Sref.add r' s
in
let apply s = Sref.fold add1 s Sref.empty in
......
......@@ -54,7 +54,7 @@ val equal : t -> t -> bool
val no_side_effect : t -> bool
val subst : vsymbol -> reference -> t -> t
val subst : reference Mvs.t -> t -> t
val occur : reference -> t -> bool
......
......@@ -31,7 +31,6 @@ and type_c =
and binder = Term.vsymbol * type_v
(* environments *)
type env = {
......@@ -212,7 +211,7 @@ and subst_post ts s ((v, q), 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_effect = E.subst ef c.c_effect;
c_pre = f_ty_subst ts s c.c_pre;
c_post = subst_post ts s c.c_post; }
......@@ -228,13 +227,30 @@ and binder ef ts s (vs, v) =
let s, vs = subst_var ts s vs in
s, (vs, v)
let tpure ty = Tpure ty
let tarrow bl c = match bl with
| [] ->
invalid_arg "tarrow"
| _ ->
let rename (e, s) (vs, v) =
let vs' = create_vsymbol (id_clone vs.vs_name) vs.vs_ty in
let v' = subst_type_v e Mtv.empty s v in
let e' = Mvs.add vs (E.Rlocal vs') e in
let s' = Mvs.add vs (t_var vs') s in
(e', s'), (vs', v')
in
let (e, s), bl' = Util.map_fold_left rename (Mvs.empty, Mvs.empty) bl in
Tarrow (bl', subst_type_c e Mtv.empty s c)
let subst1 vs1 t2 = Mvs.add vs1 t2 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 tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
subst_type_c (fun e -> e) ts (subst1 x (t_var vs)) c
subst_type_c Mvs.empty ts (subst1 x (t_var vs)) c
| Tarrow ([], _) | Tpure _ ->
assert false
......@@ -242,13 +258,13 @@ 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 tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
let ef = E.subst x r in
let ef = Mvs.add x r Mvs.empty in
subst_type_c ef ts (subst1 x (t_var vs)) c
| E.Rglobal ls as r, Tarrow ((x, tyx) :: bl, c) ->
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
let ts = ty_match Mtv.empty (purify env tyx) ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
let ef = E.subst x r in
let ef = Mvs.add x r Mvs.empty in
subst_type_c ef ts (subst1 x (t_app ls [] ty)) c
| _ ->
assert false
......
......@@ -19,7 +19,7 @@ type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v =
type type_v = private
| Tpure of Ty.ty
| Tarrow of binder list * type_c
......@@ -31,6 +31,9 @@ and type_c =
and binder = Term.vsymbol * type_v
val tpure : Ty.ty -> type_v
val tarrow : binder list -> type_c -> type_v
(* environments *)
type env = private {
......
......@@ -528,10 +528,10 @@ let variant loc env (t, ps) =
let rec type_v gl env = function
| DTpure ty ->
Tpure (Denv.ty_of_dty ty)
tpure (Denv.ty_of_dty ty)
| DTarrow (bl, c) ->
let env, bl = map_fold_left (binder gl) env bl in
Tarrow (bl, type_c gl env c)
tarrow bl (type_c gl env c)
and type_c gl env c =
let tyv = type_v gl env c.dc_result_type in
......@@ -823,9 +823,9 @@ let add_binders = List.fold_left add_binder
let rec add_local_pat env p = match p.pat_node with
| Term.Pwild -> env
| Term.Pvar x -> add_local x (Tpure p.pat_ty) env
| Term.Pvar x -> add_local x (tpure p.pat_ty) env
| Term.Papp (_, pl) -> List.fold_left add_local_pat env pl
| Term.Pas (p, x) -> add_local_pat (add_local x (Tpure p.pat_ty) env) p
| Term.Pas (p, x) -> add_local_pat (add_local x (tpure p.pat_ty) env) p
| Term.Por (p, _) -> add_local_pat env p
let make_apply loc e1 ty c =
......@@ -860,14 +860,14 @@ let rec is_pure_expr e =
| Eglobal _ | Eabsurd -> false (* TODO: improve *)
let mk_expr loc ty ef d =
{ expr_desc = d; expr_type = ty; expr_type_v = Tpure ty;
{ expr_desc = d; expr_type = ty; expr_type_v = tpure ty;
expr_effect = ef; expr_loc = loc }
let mk_simple_expr loc ty d = mk_expr loc ty E.empty d
let mk_bool_constant loc gl ls =
let ty = ty_app gl.ts_bool [] in
{ expr_desc = Elogic (t_app ls [] ty); expr_type = ty; expr_type_v = Tpure ty;
{ expr_desc = Elogic (t_app ls [] ty); expr_type = ty; expr_type_v = tpure ty;
expr_effect = E.empty; expr_loc = loc }
let mk_false loc gl = mk_bool_constant loc gl gl.ls_False
......@@ -899,7 +899,7 @@ let rec expr gl env e =
and expr_desc gl env loc ty = function
| IElogic t ->
let ef = term_effect gl E.empty t in
Elogic t, Tpure ty, ef
Elogic t, tpure ty, ef
| IElocal (vs, _) ->
let tyv = Mvs.find vs env in
Elocal vs, tyv, E.empty
......@@ -919,7 +919,7 @@ and expr_desc gl env loc ty = function
| IEfun (bl, t) ->
let env = add_binders env bl in
let t, c = triple gl env t in
Efun (bl, t), Tarrow (bl, c), E.empty
Efun (bl, t), tarrow bl c, E.empty
| IElet (v, e1, e2) ->
let e1 = expr gl env e1 in
let env = add_local v e1.expr_type_v env in
......@@ -978,7 +978,7 @@ and expr_desc gl env loc ty = function
| Pgm_ptree.LazyOr ->
Eif (e1, mk_true loc gl, e2)
in
d, Tpure ty, ef
d, tpure ty, ef
| IEmatch (v, bl) ->
if is_reference_type gl v.vs_ty then
errorm ~loc "cannot match over a reference";
......@@ -989,14 +989,14 @@ and expr_desc gl env loc ty = function
ef, (p, e)
in
let ef, bl = map_fold_left branch E.empty bl in
Ematch (v, bl), Tpure ty, ef
Ematch (v, bl), tpure ty, ef
| IEabsurd ->
Eabsurd, Tpure ty, E.empty
Eabsurd, tpure ty, E.empty
| IEraise (x, e1) ->
let e1 = option_map (expr gl env) e1 in
let ef = match e1 with Some e1 -> e1.expr_effect | None -> E.empty in
let ef = E.add_raise x ef in
Eraise (x, e1), Tpure ty, ef
Eraise (x, e1), tpure ty, ef
| IEtry (e1, hl) ->
let e1 = expr gl env e1 in
let ef = e1.expr_effect in
......@@ -1004,7 +1004,7 @@ and expr_desc gl env loc ty = function
if not (Sls.mem x ef.E.raises) && !exn_check then
errorm ~loc "exception %a cannot be raised" print_ls x;
let env = match x.ls_args, v with
| [ty], Some v -> add_local v (Tpure ty) env
| [ty], Some v -> add_local v (tpure ty) env
| [], None -> env
| _ -> assert false
in
......@@ -1012,11 +1012,11 @@ and expr_desc gl env loc ty = function
in
let hl = List.map handler hl in
let ef = List.fold_left (fun e (x,_,_) -> E.remove_raise x e) ef hl in
Etry (e1, hl), Tpure ty, ef
Etry (e1, hl), tpure ty, ef
| IEassert (k, f) ->
let ef = fmla_effect gl E.empty f in
Eassert (k, f), Tpure ty, ef
Eassert (k, f), tpure ty, ef
| IElabel (lab, e1) ->
let e1 = expr gl env e1 in
Elabel (lab, e1), e1.expr_type_v, e1.expr_effect
......@@ -1048,7 +1048,7 @@ and letrec gl env dl = (* : env * recfun list *)
| _ ->
c
in
add_local v (Tarrow (bl, c)) env
add_local v (tarrow bl c) env
in
List.fold_left add1 env dl
in
......@@ -1072,7 +1072,7 @@ and letrec gl env dl = (* : env * recfun list *)
let add_empty_effect m (v, bl, _, (p, _, q)) =
let tyl, ty = uncurrying gl v.vs_ty in
assert (List.length bl = List.length tyl);
let c = { c_result_type = Tpure ty;
let c = { c_result_type = tpure ty;
c_pre = p; c_effect = E.empty; c_post = q; }
in
Mvs.add v c m
......
(* test file *)
theory S
theory Test
use import int.Int
logic p int
goal G : forall x:int. (p 1 \/ p 2) -> p 3
......
let test (x : ref int) =
{}
let z = ref 0 in
if !x >= 0 then ref !x else z
{ !result >= 0 }
{
use import int.Gcd
use import int.ComputerDivision
}
let f () =
let r = test (ref (-2)) in
assert { !r >= 0 };
r := 1;
assert { !r > 0 }
let foo () =
let x = ref 0 in
x := 1;
assert { !x = 1 };
x := !x + 1;
assert { !x > 1 }
let rec gcd u v variant { v } =
{ u >= 0 and v >= 0 }
if v = 0 then
u
else
gcd v (mod u v)
{ gcd u v result }
(*
Local Variables:
......
......@@ -220,7 +220,7 @@ theory BitVector
axiom Lsr_nth_high:
forall b:bv,n s:int. n+s >= size -> nth (lsr b s) n = False
(* arithmetic shift left *)
(* arithmetic shift right *)
logic asr bv int : bv
axiom Asr_nth_low:
......
......@@ -153,3 +153,37 @@ theory NumOf
logic num_of (a b : int) : int = N.num_of () a b
end
(* number theory *)
theory Divisibility
use import Int
logic divides (a b : int) = exists q : int. b = q * a
end
theory Gcd
use import Int
use import Divisibility
logic gcd (a b g : int) =
divides g a and
divides g b and
forall x : int. divides x a -> divides x b -> divides x g
lemma Gcd_sym : forall a b g : int. gcd a b g -> gcd b a g
lemma Gcd_0 : forall a : int. gcd a 0 a
lemma Gcd_euclid : forall a b q g : int. gcd a (b - q * a) g -> gcd a b g
end
(*
Local Variables:
compile-command: "../bin/why.opt int.why"
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