programs: loops, exceptions (in progress)

src/programs/pgm_itree.ml

@@ -63,7 +63,7 @@ and expr_desc =
 
   | Esequence of expr * expr
   | Eif of expr * expr * expr
-  | Ewhile of expr * loop_annotation * expr
+  | Eloop of loop_annotation * expr
   | Elazy of lazy_op * expr * expr
   | Ematch of expr list * (Term.pattern list * expr) list
   | Eskip 

src/programs/pgm_parser.mly

@@ -71,6 +71,7 @@
   let id_unit () = { id = "unit"; id_loc = loc () }
   let id_result () = { id = "result"; id_loc = loc () }
   let id_anonymous () = { id = "_"; id_loc = loc () }
+  let exit_exn () = { id = "%Exit"; id_loc = loc () }
 
   let id_wf_lt_int () = Qident { id = "wf_lt_int"; id_loc = loc () }
 
@@ -290,7 +291,13 @@ expr:
 | LABEL uident COLON expr
    { mk_expr (Elabel ($2, $4)) }
 | WHILE expr DO loop_annotation expr DONE
-   { mk_expr (Ewhile ($2, $4, $5)) }
+   { mk_expr 
+       (Etry 
+	  (mk_expr
+	     (Eloop ($4, 
+		     mk_expr (Eif ($2, $5,
+				   mk_expr (Eraise (exit_exn (), None)))))),
+	   [exit_exn (), None, mk_expr Eskip])) }
 | ABSURD
    { mk_expr Eabsurd }
 | expr COLON simple_pure_type

src/programs/pgm_ptree.ml

@@ -81,7 +81,7 @@ and expr_desc =
   (* control *)
   | Esequence of expr * expr
   | Eif of expr * expr * expr
-  | Ewhile of expr * loop_annotation * expr
+  | Eloop of loop_annotation * expr
   | Elazy of lazy_op * expr * expr
   | Ematch of expr list * (Ptree.pattern list * expr) list
   | Eskip 

src/programs/pgm_ttree.ml

@@ -85,7 +85,7 @@ and dexpr_desc =
 
   | DEsequence of dexpr * dexpr
   | DEif of dexpr * dexpr * dexpr
-  | DEwhile of dexpr *  dloop_annotation * dexpr
+  | DEloop of dloop_annotation * dexpr
   | DElazy of lazy_op * dexpr * dexpr
   | DEmatch of dexpr list * (Typing.dpattern list * dexpr) list
   | DEskip
@@ -140,7 +140,7 @@ and expr_desc =
 
   | Esequence of expr * expr
   | Eif of expr * expr * expr
-  | Ewhile of expr * loop_annotation * expr
+  | Eloop of loop_annotation * expr
   | Elazy of lazy_op * expr * expr
   | Ematch of expr list * (Term.pattern list * expr) list
   | Eskip 

src/programs/pgm_types.ml

@@ -34,11 +34,14 @@ type env = {
   globals : type_v Mls.t;
   locals  : type_v Mvs.t;
   ts_arrow: tysymbol;
+  ts_bool : tysymbol;
   ts_label: tysymbol;
   ts_ref: tysymbol;
+  ts_unit : tysymbol;
   ls_at : lsymbol;
   ls_bang : lsymbol;
   ls_old : lsymbol;
+  ls_True : lsymbol;
 }
 
 let find_ts uc = ns_find_ts (get_namespace uc)
@@ -65,6 +68,12 @@ let ls_assign = memo_ls
      let a = ty_var (create_tvsymbol (id_fresh "a")) in
      create_lsymbol (id_fresh "infix :=") [ty_app ts_ref [a]; a] (Some ty_unit))
 
+let ls_Exit = memo_ls
+  (fun uc _ ->
+     let ty_exn = ty_app (find_ts uc ["exn"]) [] in
+     create_lsymbol (id_fresh "%Exit") [] (Some ty_exn))
+     
+
 let v_result ty = create_vsymbol (id_fresh "result") ty
 
 let add_type_v_ref uc m =
@@ -103,12 +112,15 @@ let empty_env uc = {
   locals = Mvs.empty;
   (* types *)
   ts_arrow = find_ts uc ["arrow"];
+  ts_bool  = find_ts uc ["bool"];
   ts_label = find_ts uc ["label"];
   ts_ref   = find_ts uc ["ref"];
+  ts_unit  = find_ts uc ["unit"];
   (* functions *)
   ls_at    = find_ls uc ["at"];
   ls_bang  = find_ls uc ["prefix !"];
   ls_old   = find_ls uc ["old"];
+  ls_True  = find_ls uc ["True"];
 }    
 
 let add_local x v env = { env with locals = Mvs.add x v env.locals }
@@ -202,6 +214,20 @@ let apply_type_v_ref env v r = match r, v with
   | _ ->
       assert false
 
+let rec eq_type_v v1 v2 = match v1, v2 with
+  | Tpure ty1, Tpure ty2 ->
+      ty_equal ty1 ty2
+  | Tarrow _, Tarrow _ ->
+      false (* TODO? *)
+  | _ ->
+      assert false
+
+let t_True env =
+  t_app env.ls_True [] (ty_app env.ts_bool [])
+
+let type_v_unit env =
+  Tpure (ty_app env.ts_unit [])
+
 (* pretty-printers *)
 
 open Pp

src/programs/pgm_types.mli

@@ -35,15 +35,23 @@ type env = private {
   locals  : type_v Mvs.t;
   (* predefined symbols *)
   ts_arrow: tysymbol;
+  ts_bool : tysymbol;
   ts_label: tysymbol;
   ts_ref  : tysymbol;
+  ts_unit : tysymbol;
   ls_at   : lsymbol;
   ls_bang : lsymbol;
   ls_old  : lsymbol;
+  ls_True : lsymbol;
 }
 
 val ls_ref    : theory_uc -> lsymbol (* ref: 'a -> 'a ref *)
 val ls_assign : theory_uc -> lsymbol (* := : 'a ref -> 'a -> unit *)
+val ls_Exit   : theory_uc -> lsymbol
+
+val t_True : env -> term
+
+val type_v_unit : env -> type_v
 
 val purify : theory_uc -> type_v -> ty
 
@@ -64,6 +72,8 @@ val post_map : (fmla -> fmla) -> post -> post
 
 val subst1 : vsymbol -> term -> term Mvs.t
 
+val eq_type_v : type_v -> type_v -> bool
+
 (* pretty-printers *)
 
 val print_type_v : Format.formatter -> type_v -> unit

src/programs/pgm_typing.ml

@@ -95,7 +95,9 @@ let create_genv uc = {
     Mstr.add "ref" (ls_ref uc)
     (Mstr.add "infix :=" (ls_assign uc) 
     Mstr.empty);
-  exceptions = Mstr.empty;
+  exceptions = 
+    Mstr.add "%Exit" (ls_Exit uc)
+    Mstr.empty;
   ts_bool = ns_find_ts (get_namespace uc) ["bool"];
   ts_unit = ns_find_ts (get_namespace uc) ["unit"];
   ts_ref  = ns_find_ts (get_namespace uc) ["ref"];
@@ -336,12 +338,10 @@ and dexpr_desc env loc = function
       let e3 = dexpr env e3 in
       expected_type e3 e2.dexpr_type;
       DEif (e1, e2, e3), e2.dexpr_type
-  | Pgm_ptree.Ewhile (e1, a, e2) ->
+  | Pgm_ptree.Eloop (a, e1) ->
       let e1 = dexpr env e1 in
-      expected_type e1 (dty_bool env.genv);
-      let e2 = dexpr env e2 in
-      expected_type e2 (dty_unit env.genv);
-      DEwhile (e1, dloop_annotation env.genv.uc a, e2), (dty_unit env.genv)
+      expected_type e1 (dty_unit env.genv);
+      DEloop (dloop_annotation env.genv.uc a, e1), (dty_unit env.genv)
   | Pgm_ptree.Elazy (op, e1, e2) ->
       let e1 = dexpr env e1 in
       expected_type e1 (dty_bool env.genv);
@@ -634,14 +634,14 @@ and expr_desc gl env denv loc ty = function
       Esequence (expr gl env e1, expr gl env e2)
   | DEif (e1, e2, e3) ->
       Eif (expr gl env e1, expr gl env e2, expr gl env e3)
-  | DEwhile (e1, la, e2) ->
+  | DEloop (la, e1) ->
       let la = 
 	{ loop_invariant = 
 	    option_map (Typing.type_fmla denv env) la.dloop_invariant;
 	  loop_variant   = 
 	    option_map (variant denv env) la.dloop_variant; }
       in
-      Ewhile (expr gl env e1, la, expr gl env e2)
+      Eloop (la, expr gl env e1)
   | DElazy (op, e1, e2) ->
       Elazy (op, expr gl env e1, expr gl env e2)
   | DEmatch (el, bl) ->
@@ -876,7 +876,9 @@ TODO:
 
 - do not add global references into the theory (add_global_if_pure)
 
-- ML-like polymorphism
+- polymorphic let?
+
+- ghost
 
-- ghost / effects
+- move effect inference here (from pgm_wp), as phase 3
 *)

src/programs/pgm_wp.ml

@@ -109,10 +109,27 @@ and expr_desc env loc ty = function
       let e2 = expr env e2 in
       let ef = E.union e1.expr_effect e2.expr_effect in
       Esequence (e1, e2), e2.expr_type_v, ef
-  | Pgm_ttree.Eif _ ->
-      assert false (*TODO*)
-  | Pgm_ttree.Ewhile _ ->
-      assert false (*TODO*)
+  | Pgm_ttree.Eif (e1, e2, e3) ->
+      let e1 = expr env e1 in
+      let e2 = expr env e2 in
+      let e3 = expr env e3 in
+      let ef = E.union e1.expr_effect e2.expr_effect in
+      let ef = E.union ef             e3.expr_effect in
+      if not (eq_type_v e2.expr_type_v e3.expr_type_v) then
+	errorm ~loc "cannot branch on functions";
+      Eif (e1, e2, e3), e2.expr_type_v, ef
+  | Pgm_ttree.Eloop (a, e1) ->
+      let e1 = expr env e1 in
+      let ef = e1.expr_effect in
+      let ef = match a.loop_invariant with
+	| Some f -> fmla_effect env ef f
+	| None -> ef
+      in
+      let ef = match a.loop_variant with
+	| Some (t, _) -> term_effect env ef t
+	| None -> ef
+      in
+      Eloop (a, e1), type_v_unit env, ef
   | Pgm_ttree.Elazy _ ->
       assert false (*TODO*)
   | Pgm_ttree.Ematch _ ->
@@ -121,10 +138,14 @@ and expr_desc env loc ty = function
       Eskip, Tpure ty, E.empty
   | Pgm_ttree.Eabsurd ->
       assert false (*TODO*)
-  | Pgm_ttree.Eraise _ ->
-      assert false (*TODO*)
-  | Pgm_ttree.Etry _ ->
-      assert false (*TODO*)
+  | Pgm_ttree.Eraise (x, e1) ->
+      let e1 = option_map (expr 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
+  | Pgm_ttree.Etry (_e1, _hl) ->
+      assert false (* TODO *)
+      (*Etry (e1, hl), Tpure ty, ef*)
 
   | Pgm_ttree.Eassert (k, f) ->
       let ef = fmla_effect env E.empty f in
@@ -338,9 +359,17 @@ and wp_desc env e q = match e.expr_desc with
       let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
       let q1 = saturate_post e1.expr_effect (v_result e1.expr_type, w2) q in
       wp_expr env e1 q1
-  | Eif _ ->
-      assert false (*TODO*)
-  | Ewhile _ ->
+  | Eif (e1, e2, e3) ->
+      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
+      let w3 = wp_expr env e3 (filter_post e3.expr_effect q) in
+      let q1 = (* if result=True then w2 else w3 *)
+	let res = v_result e1.expr_type in
+	let test = f_equ (t_var res) (t_True env) in
+	let q1 = f_if test w2 w3 in
+	saturate_post e1.expr_effect (res, q1) q
+      in
+      wp_expr env e1 q1
+  | Eloop _ ->
       assert false (*TODO*)
   | Elazy _ ->
       assert false (*TODO*)

tests/test-pgm-jcf.mlw

@@ -14,6 +14,13 @@ parameter r : int ref
 
 parameter write : v:int -> {} unit writes r { !r = v }
 
+let test () =
+  {} 
+  while !r <= 100 do
+    r := !r + 1
+  done
+  { !r = 100 }
+
 let apply_fun () =
   { true } 
   (fun x -> {x=0} x+42 { result=42 }) 0

theories/programs.why

@@ -10,6 +10,13 @@ theory Prelude
   logic ge_bool('a, 'a) : bool
   logic gt_bool('a, 'a) : bool
 
+  axiom Eq_bool_def : forall x,y:'a.  eq_bool(x,y)=True <-> x= y
+  axiom Ne_bool_def : forall x,y:'a.  ne_bool(x,y)=True <-> x<>y
+  axiom Le_bool_def : forall x,y:int. le_bool(x,y)=True <-> x<=y
+  axiom Lt_bool_def : forall x,y:int. lt_bool(x,y)=True <-> x< y
+  axiom Ge_bool_def : forall x,y:int. ge_bool(x,y)=True <-> x>=y
+  axiom Gt_bool_def : forall x,y:int. gt_bool(x,y)=True <-> x> y
+
   use export unit.Unit
   logic ignore('a) : unit