ghostify ghost arguments

src/whyml/mlw_expr.ml

@@ -705,6 +705,8 @@ let e_plapp pls el ity =
             | 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
+          if vtv.vtv_ghost && not evtv.vtv_ghost then
+            Loc.errorm "non-ghost value passed as a ghost argument";
           let eff = eff_union eff e.e_effect in
           let sbs = ity_match sbs vtv.vtv_ity evtv.vtv_ity in
           app (t::tl) (add_e_vars e varm) ghost eff sbs vtvl argl
@@ -716,6 +718,8 @@ let e_plapp pls el ity =
             let sbs = ity_match sbs vtv.vtv_ity pv.pv_vtv.vtv_ity in
             app (t::tl) (add_pv_vars pv varm) ghost eff sbs vtvl argl
           in
+          if vtv.vtv_ghost && not (vty_ghost e.e_vty) then
+            Loc.errorm "non-ghost value passed as a ghost argument";
           on_value apply_to_pv e
   in
   let vtvl = List.rev pls.pl_args in

src/whyml/mlw_ty.ml

@@ -999,6 +999,8 @@ let vta_app vta pv =
     | vty -> vty in
   let result = vty_subst vta.vta_result in
   let spec = spec_subst sbs vta.vta_spec in
+  if not vtv.vtv_ghost && arg.pv_vtv.vtv_ghost then
+    Loc.errorm "non-ghost value passed as a ghost argument";
   let ghost = vta.vta_ghost || (vtv.vtv_ghost && not arg.pv_vtv.vtv_ghost) in
   if rest = [] then spec, (if ghost then vty_ghostify result else result)
   else spec_empty ty_unit, VTarrow (vty_arrow_unsafe rest ~ghost ~spec result)

src/whyml/mlw_typing.ml

@@ -950,6 +950,22 @@ let vty_ghostify gh vty =
 let e_ghostify gh e =
   if gh && not (vty_ghost e.e_vty) then e_ghost e else e
 
+let e_app_gh e el =
+  let rec decomp = function
+    | VTvalue _ -> []
+    | VTarrow a -> a.vta_args @ decomp a.vta_result in
+  let rec ghostify = function
+    | _, [] -> []
+    | [], _ -> assert false
+    | pv :: pvl, e :: el ->
+        e_ghostify pv.pv_vtv.vtv_ghost e :: ghostify (pvl, el)
+  in
+  e_app e (ghostify (decomp e.e_vty, el))
+
+let e_plapp_gh pl el ity =
+  let ghostify vtv e = e_ghostify vtv.vtv_ghost e in
+  e_plapp pl (List.map2 ghostify pl.pl_args el) ity
+
 let rec expr lenv de =
   let loc = de.de_loc in
   let e = Loc.try3 loc expr_desc lenv loc de in
@@ -1019,9 +1035,9 @@ and expr_desc lenv loc de = match de.de_desc with
   | DEapply (de1, del) ->
       let el = List.map (expr lenv) del in
       begin match de1.de_desc with
-        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity (snd de.de_type))
-        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity (snd de.de_type))
-        | _               -> e_app (expr lenv de1) el
+        | DEglobal_pl pls -> e_plapp_gh pls el (ity_of_dity (snd de.de_type))
+        | DEglobal_ls ls  -> e_lapp ls el (ity_of_dity (snd de.de_type))
+        | _               -> e_app_gh (expr lenv de1) el
       end
   | DEglobal_pv pv ->
       e_value pv