summaryrefslogtreecommitdiff
path: root/backend/Linearize.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Linearize.v')
-rw-r--r--backend/Linearize.v16
1 files changed, 7 insertions, 9 deletions
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 636cb22..6fc8e48 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -198,17 +198,15 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code :=
(** Linearize a function body according to an enumeration of its nodes. *)
-Fixpoint linearize_body (f: LTL.function) (enum: list node)
- {struct enum} : code :=
- match enum with
- | nil => nil
- | pc :: rem =>
- match f.(LTL.fn_code)!pc with
- | None => linearize_body f rem
- | Some b => Llabel pc :: linearize_instr b (linearize_body f rem)
- end
+Definition linearize_node (f: LTL.function) (pc: node) (k: code) : code :=
+ match f.(LTL.fn_code)!pc with
+ | None => k
+ | Some b => Llabel pc :: linearize_instr b k
end.
+Definition linearize_body (f: LTL.function) (enum: list node) : code :=
+ list_fold_right (linearize_node f) enum nil.
+
(** * Entry points for code linearization *)
Definition transf_function (f: LTL.function) : res LTLin.function :=