programs: constants in abstract types

parent 3919a48a
......@@ -285,8 +285,11 @@ and wp_desc env e q = match e.expr_desc with
| Elocal v ->
let (res, q), _ = q in
f_subst (subst1 res (t_var v.pv_vs)) q
| Eglobal _ ->
| Eglobal s when is_arrow_ty s.p_ty ->
let (_, q), _ = q in q
| Eglobal s ->
let (v, q), _ = q in
f_subst_single v (t_app_infer s.p_ls []) q
| Efun (bl, t) ->
let (_, q), _ = q in
let f = wp_triple env t in
......
......@@ -5,18 +5,23 @@ module P
use import module stdlib.Ref
use import module stdlib.Array
parameter x : ghost int
parameter c : ghost int
let gid (x:int) = {} ghost x { result=x }
axiom a : c = 1
let gid (x:int) = {} ghost (c + x) { result=c+x }
(* FIXME *)
(* let gid (x:int) = {} (x, ghost x) { let a,b = result in a=x and b=x } *)
(* FIXME : make c a first parameter of gid => then to type gid c y inside
ghost we should not insert unghost *)
let g (x : int) (y : ghost int) =
let z = ghost (1 + gid y) in
assert { z = 1 + y };
assert { z = 2 + y };
x + 1
(* FIXME *)
(* let gid (x:int) = {} (x, ghost_ x) { let a,b = result in a=x and b=x } *)
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