whyml: constants and boolean operations

src/whyml/mlw_expr.ml

@@ -136,11 +136,13 @@ let ppat_plapp pls ppl vtv =
     ppat_vtv     = vtv;
     ppat_effect  = if vtv.vtv_ghost then eff_ghostify eff else eff; }
 
+let ity_of_ty_opt ty = ity_of_ty (Util.def_option ty_bool ty)
+
 let ppat_lapp ls ppl vtv =
   let pls = {
     pl_ls     = ls;
     pl_args   = List.map (fun ty -> vty_value (ity_of_ty ty)) ls.ls_args;
-    pl_value  = vty_value (ity_of_ty (Util.def_option ty_bool ls.ls_value));
+    pl_value  = vty_value (ity_of_ty_opt ls.ls_value);
     pl_effect = eff_empty; }
   in
   ppat_plapp pls ppl vtv
@@ -228,7 +230,7 @@ let make_ppattern pp vtv =
           ppat_vtv     = unmut vtv;
           ppat_effect  = if vtv.vtv_ghost then eff_ghostify eff else eff; }
     | PPlapp (ls,ppl) ->
-        let ity = ity_of_ty (Util.def_option ty_bool ls.ls_value) in
+        let ity = ity_of_ty_opt ls.ls_value in
         let sbs = ity_match ity_subst_empty ity vtv.vtv_ity in
         let mtch arg pp =
           let ity = ity_full_inst sbs (ity_of_ty arg) in
@@ -495,8 +497,7 @@ let on_value fn e = match e.e_node with
       let ld = create_let_defn (id_fresh "o") e in
       let pv = match ld.let_var with
         | LetA _ -> raise (ValueExpected e)
-        | LetV pv -> pv
-      in
+        | LetV pv -> pv in
       e_let ld (fn pv)
 
 (* We adopt right-to-left evaluation order so that expression
@@ -519,6 +520,10 @@ let on_value fn e = match e.e_node with
 
 let e_app = List.fold_left (fun e -> on_value (e_app_real e))
 
+let vtv_of_expr e = match e.e_vty with
+  | VTvalue vtv -> vtv
+  | VTarrow _ -> raise (ValueExpected e)
+
 let e_plapp pls el ity =
   let rec app tl vars ghost eff sbs vtvl argl =
     match vtvl, argl with
@@ -544,10 +549,8 @@ let e_plapp pls el ity =
       | vtv::vtvl, ({ e_node = Elogic t } as e)::argl ->
           let t = match t.t_ty with
             | Some _ -> t
-            | None -> t_if t t_bool_true t_bool_false in
-          let evtv = match e.e_vty with
-            | VTvalue vtv -> vtv
-            | VTarrow _   -> assert false in
+            | None -> t_if_simp t t_bool_true t_bool_false in
+          let evtv = vtv_of_expr e in
           let ghost = ghost || (evtv.vtv_ghost && not vtv.vtv_ghost) in
           let eff = eff_union eff e.e_effect in
           let sbs = ity_match sbs vtv.vtv_ity evtv.vtv_ity in
@@ -569,15 +572,11 @@ let e_lapp ls el ity =
   let pls = {
     pl_ls     = ls;
     pl_args   = List.map (fun ty -> vty_value (ity_of_ty ty)) ls.ls_args;
-    pl_value  = vty_value (ity_of_ty (Util.def_option ty_bool ls.ls_value));
+    pl_value  = vty_value (ity_of_ty_opt ls.ls_value);
     pl_effect = eff_empty; }
   in
   e_plapp pls el ity
 
-let vtv_of_expr e = match e.e_vty with
-  | VTvalue vtv -> vtv
-  | VTarrow _ -> raise (ValueExpected e)
-
 let e_if_real pv e1 e2 =
   let vtv1 = vtv_of_expr e1 in
   let vtv2 = vtv_of_expr e2 in
@@ -675,6 +674,57 @@ let e_any ee ity =
   let vars = List.fold_right add_e_vars ee.aeff_writes vars in
   mk_expr (Eany ee) (VTvalue (vty_value ity)) eff vars
 
+let e_const t =
+  let vtv = vty_value (ity_of_ty_opt t.t_ty) in
+  mk_expr (Elogic t) (VTvalue vtv) eff_empty Mid.empty
+
+let e_int_const s = e_const (t_int_const s)
+let e_real_const rc = e_const (t_real_const rc)
+let e_const c = e_const (t_const c)
+
+(* FIXME? Should we rather use boolean constants here? *)
+let e_true =
+  mk_expr (Elogic t_true) (VTvalue (vty_value ity_bool)) eff_empty Mid.empty
+
+let e_false =
+  mk_expr (Elogic t_false) (VTvalue (vty_value ity_bool)) eff_empty Mid.empty
+
+let on_fmla fn e = match e.e_node with
+  | Elogic ({ t_ty = None } as f) -> fn e f
+  | Elogic t -> fn e (t_equ_simp t t_bool_true)
+  | Evalue pv -> fn e (t_equ_simp (t_var pv.pv_vs) t_bool_true)
+  | _ ->
+      let ld = create_let_defn (id_fresh "o") e in
+      let pv = match ld.let_var with
+        | LetA _ -> raise (ValueExpected e)
+        | LetV pv -> pv in
+      e_let ld (fn (e_value pv) (t_equ_simp (t_var pv.pv_vs) t_bool_true))
+
+let e_not e =
+  on_fmla (fun e f ->
+    let vtv = vtv_of_expr e in
+    ity_equal_check vtv.vtv_ity ity_bool;
+    let vty = VTvalue (vty_value ~ghost:vtv.vtv_ghost ity_bool) in
+    mk_expr (Elogic (t_not f)) vty e.e_effect e.e_vars) e
+
+let e_binop op e1 e2 =
+  on_fmla (fun e2 f2 -> on_fmla (fun e1 f1 ->
+    let vtv1 = vtv_of_expr e1 in
+    let vtv2 = vtv_of_expr e2 in
+    ity_equal_check vtv1.vtv_ity ity_bool;
+    ity_equal_check vtv2.vtv_ity ity_bool;
+    let vars = add_e_vars e1 e2.e_vars in
+    let eff = eff_union e1.e_effect e2.e_effect in
+    let ghost = vtv1.vtv_ghost || vtv2.vtv_ghost in
+    let vty = VTvalue (vty_value ~ghost ity_bool) in
+    mk_expr (Elogic (t_binary op f1 f2)) vty eff vars) e1) e2
+
+let e_lazy_and e1 e2 =
+  if eff_is_empty e2.e_effect then e_binop Tand e1 e2 else e_if e1 e2 e_false
+
+let e_lazy_or e1 e2 =
+  if eff_is_empty e2.e_effect then e_binop Tor e1 e2 else e_if e1 e_true e2
+
 (* Compute the fixpoint on recursive definitions *)
 
 let vars_equal vs1 vs2 =

src/whyml/mlw_expr.mli

@@ -213,11 +213,17 @@ val e_case : expr -> (ppattern * expr) list -> expr
 exception Immutable of expr
 
 val e_assign : expr -> expr -> expr
-
 val e_ghost : expr -> expr
-
 val e_any : any_effect -> ity -> expr
 
+val e_const : constant -> expr
+val e_int_const : string -> expr
+val e_real_const : real_constant -> expr
+
+val e_lazy_and : expr -> expr -> expr
+val e_lazy_or : expr -> expr -> expr
+val e_not : expr -> expr
+
 (* TODO: when should we check for escaping identifiers (regions?)
    in pre/post/xpost/effects? Here or in WP? *)
 

src/whyml/mlw_ty.ml

@@ -496,6 +496,15 @@ let eff_empty = {
   eff_resets = Mreg.empty;
 }
 
+let eff_is_empty e =
+  Sreg.is_empty e.eff_reads &&
+  Sreg.is_empty e.eff_writes &&
+  Sexn.is_empty e.eff_raises &&
+  Sreg.is_empty e.eff_ghostr &&
+  Sreg.is_empty e.eff_ghostw &&
+  Sexn.is_empty e.eff_ghostx &&
+  Mreg.is_empty e.eff_resets
+
 let join_reset _key v1 v2 =
   Some (if option_eq reg_equal v1 v2 then v1 else None)
 

src/whyml/mlw_ty.mli

@@ -212,6 +212,8 @@ val eff_full_inst : ity_subst -> effect -> effect
 
 val eff_filter : varset -> effect -> effect
 
+val eff_is_empty : effect -> bool
+
 (** program types *)
 
 (* type of function arguments and values *)

src/whyml/mlw_typing.ml

@@ -126,8 +126,10 @@ let rec dity_of_pty ~user denv = function
 
 (** Typing program expressions *)
 
-let dity_unit = ts_app (ts_tuple 0) []
+let dity_int  = ts_app ts_int []
+let dity_real = ts_app ts_real []
 let dity_bool = ts_app ts_bool []
+let dity_unit = ts_app (ts_tuple 0) []
 
 let expected_type e dity =
   unify e.dexpr_type dity
@@ -345,22 +347,30 @@ and dexpr_desc ~userloc denv loc = function
       let res = dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl) in
       mk_let ~loc ~userloc e1 res
   | Ptree.Eassign (e1, q, e2) ->
-      let fl = { expr_desc = Eident q ; expr_loc = loc } in
-      let e1 = { expr_desc = Eapply (fl,e1) ; expr_loc = loc } in
+      let fl = { expr_desc = Eident q; expr_loc = loc } in
+      let e1 = { expr_desc = Eapply (fl,e1); expr_loc = loc } in
       let e1 = dexpr ~userloc denv e1 in
       let e2 = dexpr ~userloc denv e2 in
       expected_type e2 e1.dexpr_type;
       DEassign (e1, e2), dity_unit
-  | Ptree.Econstant _c ->
-      assert false (*TODO*)
+  | Ptree.Econstant (ConstInt _ as c) ->
+      DEconstant c, dity_int
+  | Ptree.Econstant (ConstReal _ as c) ->
+      DEconstant c, dity_real
+  | Ptree.Enot e1 ->
+      let e1 = dexpr ~userloc denv e1 in
+      expected_type e1 dity_bool;
+      DEnot e1, dity_bool
+  | Ptree.Elazy (op, e1, e2) ->
+      let e1 = dexpr ~userloc denv e1 in
+      let e2 = dexpr ~userloc denv e2 in
+      expected_type e1 dity_bool;
+      expected_type e2 dity_bool;
+      DElazy (op, e1, e2), dity_bool
   | Ptree.Eletrec (_rdl, _e1) ->
       assert false (*TODO*)
   | Ptree.Eloop (_ann, _e1) ->
       assert false (*TODO*)
-  | Ptree.Elazy (_lazy_op, _e1, _e2) ->
-      assert false (*TODO*)
-  | Ptree.Enot (_e1) ->
-      assert false (*TODO*)
   | Ptree.Ematch (_e1, _bl) ->
       assert false (*TODO*)
   | Ptree.Eabsurd ->
@@ -434,6 +444,14 @@ let rec expr locals de = match de.dexpr_desc with
       e_if (expr locals de1) (expr locals de2) (expr locals de3)
   | DEassign (de1, de2) ->
       e_assign (expr locals de1) (expr locals de2)
+  | DEconstant c ->
+      e_const c
+  | DElazy (LazyAnd, de1, de2) ->
+      e_lazy_and (expr locals de1) (expr locals de2)
+  | DElazy (LazyOr, de1, de2) ->
+      e_lazy_or (expr locals de1) (expr locals de2)
+  | DEnot de1 ->
+      e_not (expr locals de1)
   | _ ->
       assert false (*TODO*)