source: Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml @ 1328

module Atom =
        struct
                include StringTools
        end

module StringMap = Map.Make(String)

(** Simple expressions are for now affine maps of the form a*_+b *)
type sexpr =
    | Sexpr of int*int

let sexpr_id = Sexpr(1, 0)

let const_sexpr n = Sexpr(0, n)

type index = int

let make_id prefix depth = prefix ^ string_of_int depth

type indexing = sexpr list

type const_indexing = int array

(** [enter_loop n indexing] is used to update indexing when one is entering a
    loop indexed by [n].
                The function recycles the same constant indexing *)
let rec enter_loop n indexing = match n with
        | None -> ()
        | Some x -> try indexing.(x) <- 0 with | _ -> assert false

(** [enter_loop n indexing] is used to update indexing when one is continuing a
    loop indexed by [n]. *)
let rec continue_loop n indexing = match n with
        | None -> ()
        | Some x -> try indexing.(x) <- indexing.(x) + 1 with | _ -> assert false

let sexpr_of i l = 
    try
        List.nth l i
    with
                        | Failure _
      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"

let empty_indexing = []

let add_id_indexing ind = sexpr_id :: ind

(* a*_+b is composed with c*_+d by substitution: *)
(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
    Sexpr (a * c, b * c + d)
                
let ev_sexpr i (Sexpr(a, b)) = a*i+b

(* i|-->e ° I *)
let rec compose_index i s l = match i, l with
        | 0, s' :: l' -> compose_sexpr s s' :: l'
        | x, s' :: l' -> compose_index (i-1) s l'
        | _ -> l 


(* I°J applies every mapping in I to every mapping in J *)
let rec compose_indexing m n = match m, n with
        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
        | _ -> n  

let rec compose_const_indexing_i i c = function
        | [] -> []
        | s :: l ->
                try
                  const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l
                with
                        | Invalid_argument _ -> assert false

module IndexingSet = Set.Make(struct
    type t = indexing
                let compare = compare
        end)

type t = {
    name : Atom.t;
    i : indexing
}

let apply_const_indexing c lbl =
    {lbl with i = compose_const_indexing_i 0 c lbl.i}


(* if [pretty] is false then a name suitable for labels is given*)
(* ('P' replaces '+') *)
let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
        let plus = if pretty then "+" else "P" in
        let id = prefix ^ string_of_int i in
  let a_id_s = if a = 1 then id else string_of_int a ^ id in
        let b_s = string_of_int b in
        if a = 0 then b_s else
        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
        
(* examples:*)
(* [pretty] true:  (0,i1+1,2i2+2)*)
(* [pretty] false: _0_i1P1_2i2P2 *)
let rec string_of_indexing_tl pretty prefix i = function
        | [] -> if pretty then ")" else ""
        | hd :: tl ->
                let sep = if pretty then "," else "_" in
                let str = string_of_sexpr pretty prefix i hd in
                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl

let string_of_indexing pretty prefix = function
        | [] -> ""
        | hd :: tl ->
                let start = if pretty then "(" else "_" in
    let str = string_of_sexpr pretty prefix 0 hd in
                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
                
let string_of_cost_label ?(pretty = false) lab =
        lab.name ^ string_of_indexing pretty "i" lab.i

let fresh l universe =
        {name = Atom.Gen.fresh universe; i = l}  

(* TODO: urgh. Necessary? *)
type aux_t = t
                                                        
(** labels are endowed with a lexicographical ordering *)
module T : Map.OrderedType with type t = aux_t =
    struct
        type t = aux_t
        let compare = compare (* uses the built-in lexicographical comparison *) 
    end

module Map = Map.Make(T)   
module Set = Set.Make(T) 
(** [constant_map d x] produces a finite map which associates 
    [x] to every element of the set [d]. *)

let indexings_of atom s =
        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
        Set.fold f s IndexingSet.empty

let constant_map d x = 
  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
        
        (**  **)