Add rewriting step for moving execute clauses into auxiliary functions

For example, generates an auxiliary function execute_ADD (rs, rt, rd) for the
clause execute (ADD (rs,rt,rd)) = ...

Without this rewriting, the execute function easily becomes too large to be
handled by Isabelle (e.g., for CHERI-MIPS; for MIPS alone, it seems to be just
about small enough).

This used to be implemented in the pretty-printer, but that code was commented
out recently in order to support a recursive execute function for RISC-V
compressed instructions.

1 files changed, 0 insertions, 65 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 4bb3b553..d347c1bd 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1213,71 +1213,6 @@ let doc_mutrec_lem = function
 let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
-  (* TODO: Move splitting of execute function to the rewriter *)
-  (*| FCL_aux (FCL_Funcl(id,_),_) :: _
-    when string_of_id id = "execute" (*|| string_of_id id = "initial_analysis"*) ->
-    let (_,auxiliary_functions,clauses) =
-      List.fold_left
-        (fun (already_used_fnames,auxiliary_functions,clauses) funcl ->
-          match funcl with
-          | FCL_aux (FCL_Funcl (Id_aux (Id _,l),pexp),annot) ->
-             let pat,guard,exp,(pexp_l,_) = destruct_pexp pexp in
-             let _ = match guard with
-               | None -> ()
-               | _ ->
-                  raise (Reporting_basic.err_unreachable pexp_l
-                           "guarded pattern expression should have been rewritten before pretty-printing")
-             in
-             let ctor, l, argspat, pannot = (match pat with
-               | P_aux (P_app (Id_aux (Id ctor,l),argspat),pannot) ->
-                 (ctor, l, argspat, pannot)
-               | P_aux (P_id (Id_aux (Id ctor,l)), pannot) ->
-                 (ctor, l, [], pannot)
-               | _ ->
-                 raise (Reporting_basic.err_unreachable l
-                   "unsupported parameter pattern in function clause")) in
-             let rec pick_name_not_clashing_with already_used candidate =
-               if StringSet.mem candidate already_used then
-                 pick_name_not_clashing_with already_used (candidate ^ "'")
-               else candidate in
-             let unit_pat = P_aux (P_lit (mk_lit L_unit), (l, Some (Env.empty, unit_typ, no_effect))) in
-             let aux_fname = pick_name_not_clashing_with already_used_fnames (string_of_id id ^ "_" ^ ctor) in
-             let aux_args = if argspat = [] then unit_pat else P_aux (P_tup argspat,pannot) in
-             let already_used_fnames = StringSet.add aux_fname already_used_fnames in
-             let fcl = FCL_aux (FCL_Funcl (Id_aux (Id aux_fname,l),
-                                           Pat_aux (Pat_exp (aux_args,exp),(pexp_l,None)))
-                                  ,annot) in
-             let auxiliary_functions =
-                auxiliary_functions ^^ hardline ^^ hardline ^^
-                  doc_fundef_lem (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
-             (* Bind complex patterns to names so that we can pass them to the
-                auxiliary function *)
-             let name_pat idx (P_aux (p,a)) = match p with
-               | P_as (pat,_) -> P_aux (p,a) (* already named *)
-               | P_lit _ -> P_aux (p,a) (* no need to name a literal *)
-               | P_id _ -> P_aux (p,a) (* no need to name an identifier *)
-               | _ -> P_aux (P_as (P_aux (p,a), Id_aux (Id ("arg" ^ string_of_int idx),l)),a) in
-             let named_argspat = List.mapi name_pat argspat in
-             let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
-             let named_args = if argspat = [] then [unit_pat] else named_argspat in
-             let doc_arg idx (P_aux (p,(l,a))) = match p with
-               | P_as (pat,id) -> doc_id_lem id
-               | P_lit lit -> doc_lit_lem lit
-               | P_id id -> doc_id_lem id
-               | _ -> string ("arg" ^ string_of_int idx) in
-             let clauses =
-               clauses ^^ (break 1) ^^
-                 (separate space
-                    [pipe;doc_pat_lem empty_ctxt false named_pat;arrow;
-                     string aux_fname;
-                     separate space (List.mapi doc_arg named_args)]) in
-             (already_used_fnames,auxiliary_functions,clauses)
-        ) (StringSet.empty,empty,empty) fcls in
-
-    auxiliary_functions ^^ hardline ^^ hardline ^^
-    (prefix 2 1)
-      ((separate space) [string "let" ^^ doc_rec_lem false r ^^ doc_id_lem id;equals;string "function"])
-      (clauses ^/^ string "end")*)
   | FCL_aux (FCL_Funcl(id,_),annot) :: _
     when not (Env.is_extern id (env_of_annot annot) "lem") ->
     string "let" ^^ (doc_rec_lem (List.length fcls > 1) r) ^^ (doc_fundef_rhs_lem fd)