Core_peval: also unfold stdlib proc bodies

Add a variant of the fun-body unfolder to work at the impure
expression level and unfold proc-body vals.

ocaml_frontend/rewriters/core_peval.ml

@@ -193,6 +193,20 @@ let rec select_case_pexpr loc_opt subst_sym pexpr = function
  end
  end
 
+let dest_specified p_e = match p_e with
+ | Pexpr (_, _, PEctor (Cspecified, [p_e2])) -> Some p_e2
+ | Pexpr (x, y, PEval (Vloaded (LVspecified z))) -> Some (Pexpr (x, y, PEval (Vobject z)))
+ | _ -> None
+
+let dest_ptr p_e = match p_e with
+ | Pexpr (_, _, PEval (Vobject (OVpointer ptr))) -> Some ptr
+ | _ -> None
+
+let known_fcall p_e =
+ Option.bind (dest_specified p_e)
+ (fun p_e -> Option.bind (dest_ptr p_e)
+ (fun ptr_e -> Impl_mem.case_ptrval ptr_e (fun _ -> None)
+ (fun opt_sym -> opt_sym) (fun _ _ -> None)))
 
 module Identity = struct
  type 'a t = 'a
@@ -454,7 +468,7 @@ let core_peval file : 'bty RW.rewriter =
  let to_unfold_funs =
  (* The list of stdlib functions to be unfolded (see PEcall) *)
  Pmap.filter stdlib_unfold_pred file.stdlib in
- 
+
  let to_unfold_impls =
  (* The list of impl-def functions to be unfolded (see PEcall) *)
  Pmap.filter impl_unfold_pred file.impl in
@@ -474,7 +488,15 @@ let core_peval file : 'bty RW.rewriter =
  | _ ->
  None
  end in
-
+
+ let check_unfold_proc sym =
+ begin match Pmap.lookup sym to_unfold_funs with
+ | Some (Proc (_, _, _, sym_bTys, e)) ->
+ Some (sym_bTys, e)
+ | _ -> None
+ end
+ in
+
  let open RW in {
  rw_pexpr=
  RW.RW begin fun _ (Pexpr (annots, bTy, pexpr_) as pexpr) ->
@@ -710,6 +732,32 @@ let core_peval file : 'bty RW.rewriter =
  , Identity.return )
  end
 
+ | Eccall (_, _, f_e, pes) ->
+ begin match known_fcall f_e with
+ (* unfold some calls to stdlib functions *)
+ | Some nm ->
+ begin match check_unfold_proc nm with
+ | Some (sym_bTys, body_e) ->
+ let pats =
+ List.map (fun (sym, bTy) ->
+ Core_aux.mk_sym_pat sym bTy
+ ) sym_bTys in
+ Update begin
+ match pes with
+ | [] ->
+ body_e
+ | _ ->
+ Core_aux.mk_let_e
+ (Core_aux.mk_tuple_pat pats)
+ (Core_aux.mk_tuple_pe pes)
+ body_e
+ end
+ | None ->
+ Traverse
+ end
+ | None ->
+ Traverse
+ end
 
 (*
  ChangeDoChildrenPost