Module GlobalBounds

Require Import Errors.
Require Import RTL.
Require Import Registers.

Require Import RTLPaths.
Require Import Scope.
Require Import DLib.
Require Import LocalBounds.

Require Import String.
Require Import Maps.
Require Import RTLWfFunction.
Require Import SliceCFG.
Open Scope Z_scope.

Definition opt_error {A} (x:option A) (msg:String.string) : res A :=
  match x with
    | Some x => OK x
    | None => Error (MSG msg :: nil)
  end.

Fixpoint bound_rec (f:function) (fsc:Scope.family f) (exit_n:node) (reg_vint:reg)
  (fuel:nat) (sc:Scope.t)
  (acc:PTree.t Z) : res (PTree.t Z) :=
  match fuel with
    | O => Error (MSG ("bound_rec: not enough fuel") :: nil)
    | S fuel' =>
    let h := Scope.header fsc sc in
    if ptree_mem h acc then Error (MSG ("bound_rec assert false") :: nil)
    else
      if peq h f.(fn_entrypoint) then
        let acc' := PTree.set h 1 acc in
        let sons := Scope.sons sc in
        fold_left (fun eacc sc' =>
            do acc <- eacc;
              bound_rec f fsc exit_n reg_vint fuel' sc' acc) sons (OK acc')
      else
        let p_h := Scope.header fsc (Scope.parent fsc sc) in
        do slice <- slicer f fsc exit_n reg_vint h;
        let (tf,tfsc') := slice in
        let (tfsc,_) := tfsc' in
        match local_bound tf tfsc h with
          | OK local_bound_h =>
            do bound_p <- opt_error (PTree.get p_h acc) "bound_rec: parent not computed yet";
            let bound_h := (local_bound_h * bound_p)%Z in
            let acc' := PTree.set h bound_h acc in
            let sons := Scope.sons sc in
              fold_left (fun eacc sc' =>
                do acc <- eacc;
                  bound_rec f fsc exit_n reg_vint fuel' sc' acc) sons (OK acc')
          | Error _ => OK acc
        end
    end.

Definition bound (f:function) : res (node -> option Z) :=
  match Scope.build_family f with
    | Some fsc =>
      let main_sc := Scope.scope fsc f.(fn_entrypoint) in
      let all_sc := Scope.elements fsc in
      do (exit_n, reg_vint) <-check_wf f;
      do bound_headers <-
        bound_rec f fsc exit_n reg_vint (List.length all_sc) main_sc (PTree.empty _);
        OK (fun n =>
          let h := Scope.header fsc (Scope.scope fsc n) in
            PTree.get h bound_headers)
    | None => Error (MSG ("bound: build_scope failed ") :: nil)
end.

Fixpoint headers_rec (f:function) (fsc:Scope.family f) (fuel:nat) (sc:Scope.t)
  (acc:list node) : res (list node) :=
  match fuel with
    | O => Error (MSG ("headers_rec: not enough fuel") :: nil)
    | S fuel' =>
    let h := Scope.header fsc sc in
    if TheoryList.mem positive_eq_dec h acc then Error (MSG ("headers_rec assert false") :: nil)
    else
      let sons := Scope.sons sc in
      fold_left (fun eacc sc' =>
                   do acc <- eacc;
                 headers_rec f fsc fuel' sc' acc) sons (OK (h :: acc))
    end.

Definition headers (f:function) : res (list node) :=
  match Scope.build_family f with
    | Some fsc =>
      let main_sc := Scope.scope fsc f.(fn_entrypoint) in
      let all_sc := Scope.elements fsc in
      headers_rec f fsc (List.length all_sc) main_sc nil
    | None => Error (MSG ("headers: build_scope failed ") :: nil)
  end.