Module SSAfastliveprecompute

Require Import Time.
Require Import Maps.

Require Import SSAfastliveprecomputeRT.
Require Import SSAfastliveprecomputeTT.

Local Open Scope string_scope.
Local Open Scope positive_scope.

Definition precompute_r_t g u dom_pre :=
  let '(r, c, t_up, back) := time (Some "precompute_r_t ") "precompute_r_t_up " (fun _ => precompute_r_t_up g u dom_pre) tt in
  let pre u :=
    match r ! u with
    | None => 1
    | Some (n, _) => n
    end
  in
  let t := time (Some "precompute_r_t ") "precompute_t_from_t_up " (fun _ => precompute_t_from_t_up dom_pre pre t_up back) tt in
  (r, c, t, back).