whyml: simplify the e_arrow call

examples/use_api/use_api.ml

@@ -351,16 +351,12 @@ let d2 =
   let body =
     (* building expression "ref 0" *)
     let e =
-      (* recall that "ref" has type "(v:'a) -> ref 'a". We need to build an
-         instance of it *)
-      (* we first built a dummy effective parameter v of type int *)
-      let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "v") Mlw_ty.ity_int in
+      (* recall that "ref" has polymorphic type "(v:'a) -> ref 'a".
+         We need to build an instance of it *)
       (* we build "ref int" with a *fresh* region *)
       let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
-      (* we build the type "(v:int) -> ref <fresh region> int)" *)
-      let aty = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ity) in
       (* e1 : the appropriate instance of "ref" *)
-      let e1 = Mlw_expr.e_arrow ref_fun aty in
+      let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
       (* we apply it to 0 *)
       let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
       Mlw_expr.e_app e1 [c0]
@@ -375,9 +371,7 @@ let d2 =
     (* building expression "!x" *)
     let bang_x =
       (* recall that "!" as type "ref 'a -> 'a" *)
-      (* we build a dummy parameter r of the same type as x *)
-      let aty = Mlw_ty.vty_arrow [var_x] (Mlw_ty.VTvalue Mlw_ty.ity_int) in
-      let e1 = Mlw_expr.e_arrow get_fun aty in
+      let e1 = Mlw_expr.e_arrow get_fun [var_x.Mlw_ty.pv_ity] Mlw_ty.ity_int in
       Mlw_expr.e_app e1 [Mlw_expr.e_value var_x]
     in
     (* the complete body *)

src/jessie/ACSLtoWhy3.ml

@@ -192,24 +192,16 @@ let rec logic_type ty =
 let any _ty =
   Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0"))
 
-
 let mk_ref ty =
-    let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "a") ty in
-    let ity = Mlw_ty.ity_app_fresh ref_type [ty] in
-    let aty = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ity) in
-    Mlw_expr.e_arrow ref_fun aty
+    let ref_ty = Mlw_ty.ity_app_fresh ref_type [ty] in
+    Mlw_expr.e_arrow ref_fun [ty] ref_ty
 
 let mk_get ref_ty ty =
-    let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "r") ref_ty in
-    let aty = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ty) in
-    Mlw_expr.e_arrow get_fun aty
+    Mlw_expr.e_arrow get_fun [ref_ty] ty
 
 let mk_set ref_ty ty =
     (* (:=) has type (r:ref 'a) (v:'a) unit *)
-    let pv1 = Mlw_ty.create_pvsymbol (Ident.id_fresh "r") ref_ty in
-    let pv2 = Mlw_ty.create_pvsymbol (Ident.id_fresh "v") ty in
-    let aty = Mlw_ty.vty_arrow [pv1;pv2] (Mlw_ty.VTvalue Mlw_ty.ity_unit) in
-    Mlw_expr.e_arrow set_fun aty
+    Mlw_expr.e_arrow set_fun [ref_ty; ty] Mlw_ty.ity_unit
 
 
 

src/whyml/mlw_expr.ml

@@ -475,12 +475,22 @@ let e_value pv =
   let varm = add_pv_vars pv Mid.empty in
   mk_expr (Evalue pv) (VTvalue pv.pv_ity) pv.pv_ghost eff_empty varm
 
-let e_arrow ps aty =
+let e_arrow ps argl res =
   let varm = add_ps_vars ps Mid.empty in
-  let sbs = aty_vars_match ps.ps_subst ps.ps_aty aty in
+  let sbs = aty_vars_match ps.ps_subst ps.ps_aty argl res in
   let aty = aty_full_inst sbs ps.ps_aty in
   mk_expr (Earrow ps) (VTarrow aty) ps.ps_ghost eff_empty varm
 
+let e_arrow_aty ps aty =
+  let rec get_types argl a =
+    let add argl pv = pv.pv_ity :: argl in
+    let argl = List.fold_left add argl a.aty_args in
+    match a.aty_result with
+    | VTarrow a -> get_types argl a
+    | VTvalue v -> e_arrow ps (List.rev argl) v
+  in
+  get_types [] aty
+
 (* let-definitions *)
 
 let create_let_defn id e =
@@ -881,7 +891,7 @@ let ps_compat ps1 ps2 =
 
 let rec expr_subst psm e = e_label_copy e (match e.e_node with
   | Earrow ps when Mid.mem ps.ps_name psm ->
-      e_arrow (Mid.find ps.ps_name psm) (aty_of_expr e)
+      e_arrow_aty (Mid.find ps.ps_name psm) (aty_of_expr e)
   | Eapp (e,pv,_) ->
       e_app_real (expr_subst psm e) pv
   | Elet ({ let_sym = LetV pv ; let_expr = d }, e) ->

src/whyml/mlw_expr.mli

@@ -181,15 +181,14 @@ val e_label_add : label -> expr -> expr
 val e_label_copy : expr -> expr -> expr
 
 val e_value : pvsymbol -> expr
-val e_arrow : psymbol -> aty -> expr
-(** [e_arrow p ty] instantiates the program function symbol [p] into a
-    program expression having the given arrow type [ty], instantiating
-    appropriately the type variables and region variables. The
-    resulting expression can be applied to arguments using [e_app]
-    given below.
 
-    See also [examples/use_api/use_api.ml]
-*)
+val e_arrow : psymbol -> ity list -> ity -> expr
+(** [e_arrow p argl res] instantiates the program function symbol [p]
+    into a program expression having the given types of the arguments
+    and the result. The resulting expression can be applied to
+    arguments using [e_app] given below.
+
+    See also [examples/use_api/use_api.ml] *)
 
 exception ValueExpected of expr
 exception ArrowExpected of expr

src/whyml/mlw_ty.ml

@@ -873,19 +873,17 @@ let vty_arrow argl ?spec vty =
    the spec. In other words, only the type variables and regions in
    [aty_vars aty] are matched. The caller should supply a "freezing"
    substitution that covers all external type variables and regions. *)
-let rec aty_vars_match s a1 a2 =
+let rec aty_vars_match s a argl res =
   let rec match_args s l1 l2 = match l1, l2 with
-    | [],[] -> s, a1.aty_result, a2.aty_result
-    | [], _ -> s, a1.aty_result, VTarrow { a2 with aty_args = l2 }
-    | _, [] -> s, VTarrow { a1 with aty_args = l1 }, a2.aty_result
-    | {pv_ity = v1}::l1, {pv_ity = v2}::l2 ->
-        match_args (ity_match s v1 v2) l1 l2
-  in
-  let s, vty1, vty2 = match_args s a1.aty_args a2.aty_args in
-  match vty1, vty2 with
-  | VTarrow a1, VTarrow a2 -> aty_vars_match s a1 a2
-  | VTvalue v1, VTvalue v2 -> ity_match s v1 v2
-  | _ -> invalid_arg "Mlw_ty.aty_vars_match"
+    | v1::l1, v2::l2 -> match_args (ity_match s v1.pv_ity v2) l1 l2
+    | [], l -> s, l
+    | _, [] -> invalid_arg "Mlw_ty.aty_vars_match" in
+  let s, argl = match_args s a.aty_args argl in
+  match a.aty_result, argl with
+  | VTvalue v, [] -> ity_match s v res
+  | VTvalue _, _
+  | VTarrow _, [] -> invalid_arg "Mlw_ty.aty_vars_match"
+  | VTarrow a, _  -> aty_vars_match s a argl res
 
 (* the substitution must cover not only [aty_vars aty] but
    also every type variable and every region in [aty_spec] *)

src/whyml/mlw_ty.mli

@@ -295,7 +295,7 @@ val vty_arrow : pvsymbol list -> ?spec:spec -> vty -> aty
    the spec. In other words, only the type variables and regions in
    [aty_vars aty] are matched. The caller should supply a "freezing"
    substitution that covers all external type variables and regions. *)
-val aty_vars_match : ity_subst -> aty -> aty -> ity_subst
+val aty_vars_match : ity_subst -> aty -> ity list -> ity -> ity_subst
 
 (* the substitution must cover not only [aty_vars aty] but
    also every type variable and every region in [aty_spec] *)

src/whyml/mlw_typing.ml

@@ -1214,6 +1214,9 @@ let e_plapp_gh pl el ity =
   let ghostify fd e = e_ghostify fd.fd_ghost e in
   e_plapp pl (List.map2 ghostify pl.pl_args el) ity
 
+let e_arrow_dity ps (argl,res) =
+  e_arrow ps (List.map ity_of_dity argl) (ity_of_dity res)
+
 let rec expr lenv de =
   let loc = de.de_loc in
   let e = Loc.try3 loc expr_desc lenv loc de in
@@ -1224,11 +1227,7 @@ and expr_desc lenv loc de = match de.de_desc with
       assert (Mstr.mem x lenv.let_vars);
       begin match Mstr.find x lenv.let_vars with
       | LetV pv -> e_value pv
-      | LetA ps ->
-          begin match vty_of_dvty de.de_type with
-            | VTarrow aty -> e_arrow ps aty
-            | VTvalue _ -> assert false
-          end
+      | LetA ps -> e_arrow_dity ps de.de_type
       end
   | DElet (x, gh, { de_desc = DEfun (bl, tr) }, de2) ->
       let fd = expr_fun lenv x gh bl tr in
@@ -1238,13 +1237,13 @@ and expr_desc lenv loc de = match de.de_desc with
   | DEfun (bl, tr) ->
       let x = mk_id "fn" loc in
       let fd = expr_fun lenv x false bl tr in
-      let e2 = e_arrow fd.fun_ps fd.fun_ps.ps_aty in
+      let e2 = e_arrow_dity fd.fun_ps de.de_type in
       e_rec [fd] e2
   (* FIXME? (ghost "lab" fun x -> ...) loses the label "lab" *)
   | DEghost { de_desc = DEfun (bl, tr) } ->
       let x = mk_id "fn" loc in
       let fd = expr_fun lenv x true bl tr in
-      let e2 = e_arrow fd.fun_ps fd.fun_ps.ps_aty in
+      let e2 = e_arrow_dity fd.fun_ps de.de_type in
       e_rec [fd] e2
   | DElet (x, gh, de1, de2) ->
       let e1 = e_ghostify gh (expr lenv de1) in
@@ -1290,10 +1289,7 @@ and expr_desc lenv loc de = match de.de_desc with
   | DEglobal_pv pv ->
       e_value pv
   | DEglobal_ps ps ->
-      begin match vty_of_dvty de.de_type with
-        | VTarrow aty -> e_arrow ps aty
-        | VTvalue _ -> assert false
-      end
+      e_arrow_dity ps de.de_type
   | DEglobal_pl pl ->
       e_plapp pl [] (ity_of_dity (snd de.de_type))
   | DEglobal_ls ls ->