generalize builtin_arg_inj into builtin_arg_map

2 files changed, 10 insertions, 9 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 8adc92f9..afc9785e 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -1174,7 +1174,7 @@ Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval :=
     let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
     Stailcall sig svos sargs
   | Ibuiltin ef args res pc =>
-    let sargs := List.map (builtin_arg_inj (hsi_sreg_get prev)) args in
+    let sargs := List.map (builtin_arg_map (hsi_sreg_get prev)) args in
     Sbuiltin ef sargs res pc
   | Ireturn or => 
     let sor := SOME r <- or IN Some (hsi_sreg_get prev r) in
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v
index 81351f6a..5002b7c5 100644
--- a/kvx/lib/RTLpathSE_theory.v
+++ b/kvx/lib/RTLpathSE_theory.v
@@ -998,7 +998,8 @@ Inductive ssem pge (ge: RTL.genv) (sp:val) (st: sstate) stack f (rs0: regset) (m
      ssem pge ge sp st stack f rs0 m0 t s 
   .
 
-Fixpoint builtin_arg_inj (f: reg -> sval) (arg: builtin_arg reg) : builtin_arg sval :=
+(* NB: generic function that could be put into [AST] file *)
+Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
   match arg with
   | BA x => BA (f x)
   | BA_int n => BA_int n
@@ -1009,14 +1010,14 @@ Fixpoint builtin_arg_inj (f: reg -> sval) (arg: builtin_arg reg) : builtin_arg s
   | BA_addrstack ptr => BA_addrstack ptr
   | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr
   | BA_addrglobal id ptr => BA_addrglobal id ptr
-  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_inj f ba1) (builtin_arg_inj f ba2)
-  | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_inj f ba1) (builtin_arg_inj f ba2)
+  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2)
+  | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2)
   end.
 
 Lemma seval_builtin_arg_correct ge sp rs m rs0 m0 sreg: forall arg varg,
   (forall r, seval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
   eval_builtin_arg ge (fun r => rs # r) sp m arg varg ->
-  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_inj sreg arg) varg.
+  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg.
 Proof.
   induction arg.
   all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
@@ -1029,7 +1030,7 @@ Qed.
 Lemma seval_builtin_args_correct ge sp rs m rs0 m0 sreg args vargs:
   (forall r, seval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
   eval_builtin_args ge (fun r => rs # r) sp m args vargs ->
-  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_inj sreg) args) vargs.
+  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs.
 Proof.
   induction 2.
   - constructor.
@@ -1039,7 +1040,7 @@ Qed.
 
 Lemma seval_builtin_arg_complete ge sp rs m rs0 m0 sreg: forall arg varg,
   (forall r, seval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
-  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_inj sreg arg) varg ->
+  seval_builtin_arg ge sp m rs0 m0 (builtin_arg_map sreg arg) varg ->
   eval_builtin_arg ge (fun r => rs # r) sp m arg varg.
 Proof.
   induction arg.
@@ -1053,7 +1054,7 @@ Qed.
 
 Lemma seval_builtin_args_complete ge sp rs m rs0 m0 sreg: forall args vargs,
   (forall r, seval_sval ge sp (sreg r) rs0 m0 = Some rs # r) ->
-  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_inj sreg) args) vargs ->
+  seval_builtin_args ge sp m rs0 m0 (map (builtin_arg_map sreg) args) vargs ->
   eval_builtin_args ge (fun r => rs # r) sp m args vargs.
 Proof.
   induction args.
@@ -1075,7 +1076,7 @@ Definition sexec_final (i: instruction) (prev: sistate_local): sfval :=
     let sargs := list_sval_inj (List.map prev.(si_sreg) args) in
     Stailcall sig svos sargs
   | Ibuiltin ef args res pc =>
-    let sargs := List.map (builtin_arg_inj prev.(si_sreg)) args in
+    let sargs := List.map (builtin_arg_map prev.(si_sreg)) args in
     Sbuiltin ef sargs res pc
   | Ireturn or => 
     let sor := SOME r <- or IN Some (prev.(si_sreg) r) in