whyml: applications (cont.)

src/whyml/mlw_expr.ml

@@ -297,6 +297,7 @@ exception ArrowExpected of expr
      Eapp pa pv [read ro]
    which is ok. If pa is computed before pv, then Eapp pa pv would
    violate the freshness of ro. *)
+
 let e_eapp e el =
   let rec app = function
     | [] -> e
@@ -317,11 +318,72 @@ let e_eapp e el =
               let pv = match ld.let_var with
                 | LetA _ -> raise (ValueExpected e)
                 | LetV pv -> pv in
-              left pv
+              e_let ld (left pv)
         end
   in
   app (List.rev el)
 
+let e_plapp pls el ity =
+  let rec app tl tvs regs ghost sbs vtvl argl =
+    match vtvl, argl with
+      | [],[] ->
+          let vtv = pls.pl_value in
+          let ghost = ghost || vtv.vtv_ghost in
+          let sbs = ity_match sbs vtv.vtv_ity ity in
+          let mut = Util.option_map (reg_full_inst sbs) vtv.vtv_mut in
+          let vty = VTvalue (vty_value ~ghost ?mut ity) in
+          let t = match pls.pl_ls.ls_value with
+            | Some _ -> fs_app pls.pl_ls tl (ty_of_ity ity)
+            | None   -> ps_app pls.pl_ls tl
+          in
+          ghost_effect { (e_dummy (Elogic t) vty) with
+            e_effect = eff_full_inst sbs pls.pl_effect;
+            e_tvs    = tvs;
+            e_regs   = regs; }
+      | [],_ | _,[] ->
+          raise (Term.BadArity
+            (pls.pl_ls, List.length pls.pl_args, List.length el))
+      | vtv::vtvl, ({ e_node = Elogic t } as e)::argl ->
+          let tvs = add_expr_tvs tvs e in
+          let regs = add_expr_regs regs e in
+          let evtv = match e.e_vty with
+            | VTvalue vtv -> vtv
+            | VTarrow _   -> assert false in
+          let ghost = ghost || (evtv.vtv_ghost && not vtv.vtv_ghost) in
+          let sbs = ity_match sbs vtv.vtv_ity evtv.vtv_ity in
+          app (t::tl) tvs regs ghost sbs vtvl argl
+      | vtv::vtvl, e::argl ->
+          let apply_to_pv pv =
+            let tl = t_var pv.pv_vs :: tl in
+            let tvs = add_pv_tvs tvs pv in
+            let regs = add_pv_regs regs pv in
+            let ghost = ghost || (pv.pv_vtv.vtv_ghost && not vtv.vtv_ghost) in
+            let sbs = ity_match sbs vtv.vtv_ity pv.pv_vtv.vtv_ity in
+            app tl tvs regs ghost sbs vtvl argl
+          in
+          begin match e.e_node with
+            | Evalue pv -> apply_to_pv pv
+            | _ ->
+                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 (apply_to_pv pv)
+          end
+  in
+  let vtvl = List.rev pls.pl_args in
+  let argl = List.rev el in
+  app [] Mid.empty Mid.empty false ity_subst_empty vtvl argl
+
+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_effect = eff_empty; }
+  in
+  e_plapp pls el ity
+
 (*
   - A "proper type" of a vty [v] is [v] with empty specification
     (effect/pre/post/xpost). Basically, it is formed from pv_ity's

src/whyml/mlw_expr.mli

@@ -165,6 +165,9 @@ val e_inst : psymbol -> ity_subst -> expr
    be restricted to type variables and regions (both top and subordinate)
    of ps_vta.vta_tvs/regs. *)
 
+exception ValueExpected of expr
+exception ArrowExpected of expr
+
 exception GhostWrite of expr * region
 exception GhostRaise of expr * xsymbol
 (* a ghost expression writes in a non-ghost region or raises an exception *)
@@ -173,6 +176,10 @@ val e_app : pasymbol -> pvsymbol -> expr
 
 val e_eapp : expr -> expr list -> expr
 
+val e_lapp : lsymbol -> expr list -> ity -> expr
+
+val e_plapp : plsymbol -> expr list -> ity -> expr
+
 val create_let_defn : preid -> expr -> let_defn
 
 exception StaleRegion of region * ident * expr

src/whyml/mlw_ty.ml

@@ -536,9 +536,17 @@ let vty_value ?(ghost=false) ?mut ity =
   }
 
 let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
+  (* mutable arguments are rejected outright *)
   if vtv.vtv_mut <> None then
-    Loc.errorm "Mutable arguments are not allowed in vty_arrow"
-  else {
+    Loc.errorm "Mutable arguments are not allowed in vty_arrow";
+  (* we accept a mutable vty_value for the result to simplify Mlw_expr,
+     but erase it in the signature: only projections return mutables *)
+  let vty = match vty with
+    | VTvalue ({ vtv_mut = Some r } as vtv) ->
+        let regs = Sreg.remove r vtv.vtv_regs in
+        VTvalue { vtv with vtv_mut = None ; vtv_regs = regs }
+    | _ -> vty
+  in {
     vta_arg    = vtv;
     vta_result = vty;
     vta_effect = effect;

src/whyml/mlw_ty.mli

@@ -143,6 +143,10 @@ val ity_equal_check : ity -> ity -> unit
 
 val ity_subst_union : ity_subst -> ity_subst -> ity_subst
 
+val ity_full_inst : ity_subst -> ity -> ity
+
+val reg_full_inst : ity_subst -> region -> region
+
 (* exception symbols *)
 type xsymbol = private {
   xs_name : ident;
@@ -175,6 +179,8 @@ val eff_assign : effect -> region -> ity -> effect
 
 val eff_remove_raise : effect -> xsymbol -> effect
 
+val eff_full_inst : ity_subst -> effect -> effect
+
 (** program types *)
 
 (* type of function arguments and values *)