programs: simplification of universal quantifications in WPs

bench/bench

@@ -143,13 +143,13 @@ programs bench/programs/good
 programs examples/programs
 echo ""
 
-echo "=== Checking valid goals ==="
-valid_goals bench/valid
-echo ""
-
 echo "=== VC generation on good programs ==="
 pgml_options=
 programs bench/programs/good
 programs examples/programs
 echo ""
 
+echo "=== Checking valid goals ==="
+valid_goals bench/valid
+echo ""
+

bench/programs/good/list.mlw

@@ -4,16 +4,6 @@ module M
   use import list.List
   use import list.Length
 
-  (*
-  let rec length_ (l : list 'a) variant { length l } = 
-    {}
-    match l with
-    | Nil -> 0
-    | Cons _ r -> 1 + length_ r
-    end
-    { result = length l }
-  *)
-
   let rec append (l1 : list 'a) (l2 : list 'a) variant { length l1 } =
     { }
     match l1 with
@@ -25,7 +15,7 @@ module M
 end
 
 (*
-Local Variables: 
+Local Variables:
 compile-command: "unset LANG; make -C ../../.. bench/programs/good/list"
-End: 
+End:
 *)

bench/programs/good/recfun.mlw

 module M
 
-use import int.Int
-use import module ref.Ref
+  use import int.Int
+  use import module ref.Ref
 
-(** Recursive functions *)
+  (** Recursive functions *)
 
-(** 1. Pure function *)
+  (** 1. Pure function *)
 
-let rec f1 (x:int) : int variant { x } =
-  { x >= 0 } (if x > 0 then (f1 (x-1)) else x) { result = 0 }
+  let rec f1 (x:int) : int variant { x } =
+    { x >= 0 } (if x > 0 then (f1 (x-1)) else x) { result = 0 }
 
-(** 2. With effects but no argument *)
+  (** 2. With effects but no argument *)
 
-parameter x : ref int
+  parameter x : ref int
 
-let rec f2 (u:unit) : unit variant { !x } =
-  { !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
+  let rec f2 (u:unit) : unit variant { !x } =
+    { !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
 
-(** 3. With effects and a pure argument *)
+  (** 3. With effects and a pure argument *)
 
-let rec f3 (a:int) : unit variant { a } =
-  { a >= 0 }
-  if a > 0 then begin x := !x + 1; (f3 (a-1)) end
-  { !x = old !x + a }
+  let rec f3 (a:int) : unit variant { a } =
+    { a >= 0 }
+    if a > 0 then begin x := !x + 1; (f3 (a-1)) end
+    { !x = old !x + a }
 
-(** 4. With effects and a reference as argument *)
+  (** 4. With effects and a reference as argument *)
 
-let rec f4 (a:ref int) : unit variant { !a } =
-  { !a >= 0 }
-  if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
-  { !x = old !x + old !a }
+  let rec f4 (a:ref int) : unit variant { !a } =
+    { !a >= 0 }
+    if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
+    { !x = old !x + old !a }
 
-(** 5. The acid test:
-       partial application of a recursive function with effects *)
+  (** 5. The acid test:
+         partial application of a recursive function with effects *)
 
-let rec f5 (a b:ref int) variant { !a } =
-  { !a >= 0 }
-  if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
-  { result = old !a + old !b }
+  let rec f5 (a b:ref int) variant { !a } =
+    { !a >= 0 }
+    if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
+    { result = old !a + old !b }
 
-let test_f5 () =
-  { !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
+  let test_f5 () =
+    { !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
 
-end
+  end
 
 (*
 Local Variables:

src/programs/pgm_typing.ml

@@ -1578,6 +1578,7 @@ and letrec gl env dl = (* : env * recfun list *)
       let c = Mvs.find i.i_impure m in
       let c = match decvar, var with
 	| Some phi0, Some (_, phi, r) ->
+	    let _, phi = term_effect E.empty phi in
 	    let decphi = match r with
 	      | None -> (* 0 <= phi0 and phi < phi0 *)
 		  t_and (ps_app (find_ls ~pure:true gl "infix <=")

src/programs/pgm_wp.ml

@@ -65,7 +65,24 @@ let is_arrow_ty ty = match ty.ty_node with
   | Tyapp (ts, _) -> ts_equal ts ts_arrow
   | _ -> false
 
-let wp_forall v f =
+let rec wp_forall env v f =
+  let kn = get_known (pure_uc env) in
+  let ty = v.vs_ty in
+  let cl = match ty.ty_node with
+    | Tyapp (ts, _) -> find_constructors kn ts
+    | _ -> []
+  in
+  match cl with
+    | [ls] ->
+	let s = ty_match Mtv.empty (of_option ls.ls_value) ty in
+	let mk_v ty = create_vsymbol (id_fresh "x") (ty_inst s ty) in
+	let vl = List.map mk_v ls.ls_args in
+	let t = fs_app ls (List.map t_var vl) ty in
+	List.fold_right (wp_forall env) vl (t_let_close_simp v t f)
+    | _ ->
+	t_forall_close_simp [v] [] f
+
+let wp_forall env v f =
   if is_arrow_ty v.vs_ty then f else
   (* if t_occurs_single v f then t_forall_close_simp [v] [] f else f *)
   match f.t_node with
@@ -77,7 +94,7 @@ let wp_forall v f =
       when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
         t_let_close_simp v r (t_implies_simp g h)
     | _ when t_occurs_single v f ->
-        t_forall_close_simp [v] [] f
+        wp_forall env v f
     | _ ->
         f
 
@@ -87,11 +104,11 @@ let fresh_label env =
   let ty = ty_app (find_ts ~pure:true env "label_") [] in
   create_vsymbol (id_fresh "label") ty
 
-let wp_binder x f = match x.pv_tv with
-  | Tpure _ -> wp_forall x.pv_pure f
+let wp_binder env x f = match x.pv_tv with
+  | Tpure _ -> wp_forall env x.pv_pure f
   | Tarrow _ -> f
 
-let wp_binders = List.fold_right wp_binder
+let wp_binders env = List.fold_right (wp_binder env)
 
 let add_binder x rm =
   let add r rm =
@@ -152,7 +169,7 @@ let find_constructor env ts =
   | [ls] -> ls
   | _ -> assert false
 
-let wp_close rm ef f =
+let wp_close kn rm ef f =
   let sreg = ef.E.writes in
   let sreg =
     Spv.fold (fun pv s -> Sreg.union pv.pv_regions s)
@@ -165,7 +182,7 @@ let wp_close rm ef f =
     in
     Sreg.fold add sreg Spv.empty
   in
-  let quantify_v v f = wp_forall v.pv_pure f in
+  let quantify_v v f = wp_forall kn v.pv_pure f in
   Spv.fold quantify_v vars f
 
 (* quantify over all references in ef
@@ -238,7 +255,7 @@ let quantify env rm ef f =
     t_let_close v' updatev f
   in
   let f = Mpv.fold quantify_v' vv' f in
-  let quantify_r _ r' f = wp_forall r' f in
+  let quantify_r _ r' f = wp_forall env r' f in
   Mreg.fold quantify_r mreg f
 
 (* let quantify ?(all=false) env rm ef f = *)
@@ -256,7 +273,7 @@ let abstract_wp env rm 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 (R.Rlocal v) v' f) *)
       | Some v ->
-	  wp_forall v f
+	  wp_forall env v f
       | None ->
 	  f
     in
@@ -537,7 +554,7 @@ and wp_desc env rm e q = match e.expr_desc with
 	(quantify env rm e.expr_effect
 	   (wp_and ~sym:true
 	      (wp_expl "for loop preservation"
-		(wp_forall x.pv_pure
+		(wp_forall env x.pv_pure
 	         (wp_implies
 		    (wp_and (ps_app le [t_var v1.pv_pure; t_var x.pv_pure])
 		            (ps_app le [t_var x.pv_pure;  t_var v2.pv_pure]))
@@ -576,8 +593,8 @@ and wp_triple env rm bl (p, e, q) =
   in
   let f = wp_expr env rm e q in
   let f = wp_implies p f in
-  let f = wp_close rm e.expr_effect f in
-  wp_binders bl f
+  let f = wp_close env rm e.expr_effect f in
+  wp_binders env bl f
 
 and wp_recfun env rm (_, bl, _var, t) =
   wp_triple env rm bl t

tests/test-pgm-jcf.mlw

@@ -5,7 +5,7 @@ module M
 
   parameter x : ref int
 
-  let rec f2 () : unit = {  } x := 1; f2 () {  }
+  let rec f2 () : unit variant { !x } = x := !x - 1; f2 ()
 
 end