vericert.hls.PipelineOp

Definition div_pos (il: nat * list nat) x :=
  let (i, l) := il in
  match x with
  | RBop _ Odiv _ _ => (S i, i :: l)
  | RBop _ Odivu _ _ => (S i, i :: l)
  | RBop _ Omod _ _ => (S i, i :: l)
  | RBop _ Omodu _ _ => (S i, i :: l)
  | _ => (S i, l)
  end.

Definition div_pos_in_list (il: nat * list (nat * nat)) bb :=
  let (i, l) := il in
  let dp := snd (List.fold_left div_pos bb (0%nat, nil)) in
  (S i, (List.map (fun x => (i, x)) dp) ++ l).

Definition div_pos_in_block (il: nat * list (nat * nat * nat)) bb :=
  let (i, l) := il in
  let dp := snd (List.fold_left div_pos_in_list bb (0%nat, nil)) in
  (S i, (List.map (fun (yx : nat * nat) => let (y, x) := yx in (i, y, x)) dp) ++ l).

Definition find_divs (bb: bblock) :=
  snd (List.fold_left div_pos_in_block bb.(bb_body) (0%nat, nil)).

Fixpoint mapi' {A B: Type} (n: nat) (f: nat -> A -> B) (l: list A): list B :=
  match l with
  | nil => nil
  | a :: b => f n a :: mapi' (S n) f b
  end.

Definition mapi {A B: Type} := @mapi' A B 0.

Definition map_at {A: Type} (n: nat) (f: A -> A) (l: list A): list A :=
  mapi (fun i il =>
          if Nat.eqb n i
          then f il
          else il
       ) l.

Definition map_at_err {A: Type} (n: nat) (f: A -> A) (l: list A): option (list A) :=
  if (Datatypes.length l <=? n)%nat
  then None
  else Some (map_at n f l).