programs: fixed bug in WP

drivers/alt_ergo.drv

@@ -22,7 +22,7 @@ transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
 transformation "simplify_formula"
-transformation "simplify_trivial_quantification"
+(*transformation "simplify_trivial_quantification"*)
 
 theory BuiltIn
   syntax type int "int"

src/programs/pgm_effect.ml

@@ -60,8 +60,6 @@ module Reference = struct
     | Rlocal _, Rglobal _ -> -1
     | Rglobal _, Rlocal _ -> 1
 
-  let equal r1 r2 = compare r1 r2 = 0
-
 end
 
 module Sref = Set.Make(Reference)

src/programs/pgm_types.ml

@@ -177,13 +177,13 @@ and binder ef ts s (vs, v) =
   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 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.uc 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 vs) c
+      subst_type_c (fun e -> e) ts (subst1 x (t_var vs)) c
   | Tarrow ([], _) | Tpure _ -> 
       assert false
 
@@ -192,9 +192,13 @@ let apply_type_v_ref env v r = match r, v with
       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*)
+      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.uc tyx) 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 (t_app ls [] ty)) c
   | _ ->
       assert false
 

src/programs/pgm_types.mli

@@ -62,9 +62,9 @@ val v_result : ty -> vsymbol
 
 val post_map : (fmla -> fmla) -> post -> post
 
-val subst1 : vsymbol -> vsymbol -> term Mvs.t
+val subst1 : vsymbol -> term -> term Mvs.t
 
 (* pretty-printers *)
 
 val print_type_v : Format.formatter -> type_v -> unit
-
+val print_post   : Format.formatter -> post   -> unit

src/programs/pgm_typing.ml

@@ -757,6 +757,10 @@ let rec print_expr fmt e = match e.expr_desc with
   | Elet (v, e1, e2) ->
       fprintf fmt "@[let %a = %a in@ %a@]" print_vs v
 	print_expr e1 print_expr e2
+
+  | Esequence (e1, e2) ->
+      fprintf fmt "@[%a;@\n%a@]" print_expr e1 print_expr e2
+
   | _ ->
       fprintf fmt "<other>"
 
@@ -866,13 +870,13 @@ End:
 (* 
 TODO:
 
-- use a pure structure for globals
-
 - mutually recursive functions: allow order relation to be specified only once
 
 - exhaustivity of pattern-matching (in WP?)
 
 - do not add global references into the theory (add_global_if_pure)
 
+- ML-like polymorphism
+
 - ghost / effects
 *)

src/programs/pgm_wp.ml

@@ -25,6 +25,7 @@ open Ty
 open Term
 open Decl
 open Theory
+open Pretty
 open Pgm_ttree
 open Pgm_itree
 open Pgm_typing
@@ -194,8 +195,8 @@ let rec unref env r v f =
   f_map (unref_term env r v) (unref env r v) f
 
 and unref_term env r v t = match t.t_node with
-  | Tapp (ls, [t]) when ls_equal ls env.ls_bang ->
-      let rt = reference_of_term t in
+  | Tapp (ls, [u]) when ls_equal ls env.ls_bang ->
+      let rt = reference_of_term u in
       if E.ref_equal rt r then t_var v else t
   | Tapp (ls, _) when ls_equal ls env.ls_old ->
       assert false
@@ -210,7 +211,8 @@ let quantify env ef 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
-    wp_forall [v] [] (unref env r v f)
+    let f = unref env r v f in
+    wp_forall [v] [] f
   in
   let s = E.Sref.union ef.E.reads ef.E.writes in
   E.Sref.fold quantify1 s f
@@ -224,7 +226,7 @@ let abstract_wp env ef (q',ql') (q,ql) =
 	  let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in
 	  wp_forall [v'] [] (unref env (E.Rlocal v) v' f)
       | Some v -> 
-	  wp_forall [v] [] f 
+	  wp_forall [v] [] f
       | None -> 
 	  f 
     in
@@ -233,7 +235,7 @@ let abstract_wp env ef (q',ql') (q,ql) =
   let quantify_h (e',(x',f')) (e,(x,f)) =
     assert (ls_equal e' e);
     let res, f' = match x', x with
-      | Some v', Some v -> Some v, f_subst (subst1 v' v) f'
+      | Some v', Some v -> Some v, f_subst (subst1 v' (t_var v)) f'
       | None, None -> None, f'
       | _ -> assert false
     in
@@ -241,7 +243,7 @@ let abstract_wp env ef (q',ql') (q,ql) =
   in
   let f = 
     let res, f = q and res', f' = q' in
-    let f' = f_subst (subst1 res' res) f' in
+    let f' = f_subst (subst1 res' (t_var res)) f' in
     quantify_res f' f (Some res)
   in
   wp_ands (f :: List.map2 quantify_h ql' ql)
@@ -286,6 +288,8 @@ let saturate_post ef q (_, ql) =
 (* Recursive computation of the weakest precondition *)
 
 let rec wp_expr env e q = 
+(*   if !debug then  *)
+(*     eprintf "@[wp_expr: q=%a@]@." Pretty.print_fmla (snd (fst q)); *)
   let lab = fresh_label env in
   let q = post_map (old_label env lab) q in
   let f = wp_desc env e q in
@@ -299,7 +303,8 @@ and wp_desc env e q = match e.expr_desc with
   | Elocal _ ->
       assert false (*TODO*)
   | Eglobal _ ->
-      assert false (*TODO*)
+      let (_, q), _ = q in 
+      q
   | Efun (bl, t) ->
       let (_, q), _ = q in
       let f = wp_triple env t in
@@ -307,7 +312,7 @@ and wp_desc env e q = match e.expr_desc with
   | Elet (x, e1, e2) ->
       let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
       let result = v_result e1.expr_type in
-      let q1 = result, f_subst (subst1 x result) w2 in
+      let q1 = result, f_subst (subst1 x (t_var result)) w2 in
       let q1 = saturate_post e1.expr_effect q1 q in
       wp_expr env e1 q1
   | Eletrec _ ->

tests/test-jcf.why

@@ -9,6 +9,11 @@ theory Test
   goal G : 3.14 = 3.15
 end
 
+theory Test2
+  use export list.List
+  goal G : let x = Nil in let t = (Cons(1, x), Cons(3.14, x)) in t=t
+end
+
 
 (*
 Local Variables: 

tests/test-pgm-jcf.mlw

@@ -14,19 +14,18 @@ parameter r : int ref
 
 parameter write : v:int -> {} unit writes r { !r = v }
 
-let ff () =
+let apply_fun () =
   { true } 
   (fun x -> {x=0} x+42 { result=42 }) 0
   { result=40+2 }
 
-(*
+
 let ff () = 
-  { !r = 44 } 
-  let x = ref 2 in
+  { !r = 44 }
+  let x = ref 2 in 
   imp_sub r x;
   !r
   { result = 42 }
-*)
 
 (*
 Local Variables: