Added versions of the tranform_* functions in AST to work with functions

taking the ident as argument.

This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.

1 files changed, 1 insertions, 22 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 878c7e5d..bf7e4c3e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -713,26 +713,5 @@ let expand_fundef id = function
   | External ef ->
       Errors.OK (External ef)
 
-let rec transform_partial_prog transfun p =
-  match p with
-  | [] -> Errors.OK []
-  | (id,Gvar v)::l ->
-      (match transform_partial_prog transfun l with
-      | Errors.OK x -> Errors.OK ((id,Gvar v)::x)
-      | Errors.Error msg -> Errors.Error msg)
-  | (id,Gfun f)::l ->
-      (match transfun id f with
-      | Errors.OK tf ->
-          (match transform_partial_prog transfun l with
-          | Errors.OK x -> Errors.OK ((id,Gfun tf)::x)
-          | Errors.Error msg -> Errors.Error msg)
-      | Errors.Error msg ->
-          Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX
-          id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg))))
-
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  match transform_partial_prog expand_fundef p.prog_defs with
-  | Errors.OK x-> 
-      Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main =
-      p.prog_main }
-  | Errors.Error msg -> Errors.Error msg
+  AST.transform_partial_ident_program expand_fundef p