Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (9 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

Location:
Deliverables/D2.2/8051/src/common
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/common/costLabel.ml

    r486 r1542  
     1module Atom =
     2  struct
     3    include StringTools
     4  end
    15
    2 include StringTools
     6module StringMap = Map.Make(String)
     7
     8(** Simple expressions are for now affine maps of the form a*_+b *)
     9type sexpr =
     10    | Sexpr of int*int
     11
     12let is_const_sexpr (Sexpr(a, _)) = (a = 0)
     13
     14let sexpr_id = Sexpr(1, 0)
     15
     16let const_sexpr n = Sexpr(0, n)
     17
     18type index = int
     19
     20let make_id prefix depth = prefix ^ string_of_int depth
     21
     22type indexing = sexpr list
     23
     24type const_indexing = int ExtArray.t
     25
     26let const_ind_iter = ExtArray.iter
     27
     28let curr_const_ind = function
     29    | hd :: _ -> hd
     30    | _ -> invalid_arg "curr_const_ind applied to non-empty list"
     31
     32let init_const_indexing () = ExtArray.make ~buff:1 0 0
     33
     34let enter_loop_single indexing n = ExtArray.set indexing n 0
     35
     36let continue_loop_single indexing n =
     37  try
     38    ExtArray.set indexing n (ExtArray.get indexing n + 1)
     39  with | _ ->
     40    invalid_arg "uninitialized loop index"
     41
     42let curr_ind = function
     43    | hd :: _ -> hd
     44    | _ -> invalid_arg "non-empty indexing stack"
     45
     46let enter_loop inds = enter_loop_single (curr_ind inds)
     47
     48let continue_loop inds = continue_loop_single (curr_ind inds)
     49
     50let enter_loop_opt indexing = Option.iter (enter_loop indexing)
     51
     52let continue_loop_opt indexing = Option.iter (continue_loop indexing)
     53
     54let new_const_ind inds = init_const_indexing () :: inds
     55
     56let forget_const_ind = function
     57        | _ :: inds -> inds
     58        | _ -> invalid_arg "non-empty indexing stack"
     59
     60let sexpr_of i l =
     61    try
     62        List.nth l i
     63    with
     64                        | Failure _
     65      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
     66
     67let empty_indexing = []
     68
     69let add_id_indexing ind = sexpr_id :: ind
     70
     71(* a*_+b is composed with c*_+d by substitution: *)
     72(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
     73let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
     74    Sexpr (a * c, b * c + d)
     75               
     76let ev_sexpr i (Sexpr(a, b)) = a*i+b
     77
     78(* i|-->e ° I *)
     79let rec compose_index_indexing i s l = match i, l with
     80        | 0, s' :: l' -> compose_sexpr s s' :: l'
     81        | x, s' :: l' -> s' :: compose_index_indexing (i-1) s l'
     82        | _ -> l
     83
     84
     85(* I°J applies every mapping in I to every mapping in J *)
     86let rec compose_indexing m n = match m, n with
     87        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
     88        | _ -> n 
     89
     90let rec compose_const_indexing_i i c = function
     91        | [] -> []
     92        | s :: l ->
     93                let head =
     94                        (* if s is constant leave it be. In particular, avoid raising the error *)
     95                        if is_const_sexpr s then s else
     96                        try
     97                          const_sexpr (ev_sexpr (ExtArray.get c i) s)
     98                        with
     99                                | Invalid_argument _ ->
     100                                        invalid_arg "constant indexing not enough to be applied" in
     101          head :: compose_const_indexing_i (i+1) c l
     102
     103module IndexingSet = Set.Make(struct
     104    type t = indexing
     105                let compare = compare
     106        end)
     107
     108type t = {
     109    name : Atom.t;
     110    i : indexing
     111}
     112
     113let comp_index i s lbl =
     114        {lbl with i = compose_index_indexing i s lbl.i}
     115
     116let ev_indexing c lbl =
     117    {lbl with i = compose_const_indexing_i 0 c lbl.i}
     118
     119
     120(* if [pretty] is false then a name suitable for labels is given*)
     121(* ('P' replaces '+') *)
     122let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
     123        let plus = if pretty then "+" else "P" in
     124        let id = prefix ^ string_of_int i in
     125  let a_id_s = if a = 1 then id else string_of_int a ^ id in
     126        let b_s = string_of_int b in
     127        if a = 0 then b_s else
     128        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
     129       
     130(* examples:*)
     131(* [pretty] true:  (0,i1+1,2i2+2)*)
     132(* [pretty] false: _0_i1P1_2i2P2 *)
     133let rec string_of_indexing_tl pretty prefix i = function
     134        | [] -> if pretty then ")" else ""
     135        | hd :: tl ->
     136                let sep = if pretty then "," else "_" in
     137                let str = string_of_sexpr pretty prefix i hd in
     138                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
     139
     140let string_of_indexing pretty prefix = function
     141        | [] -> ""
     142        | hd :: tl ->
     143                let start = if pretty then "(" else "_" in
     144    let str = string_of_sexpr pretty prefix 0 hd in
     145                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
     146               
     147let string_of_cost_label ?(pretty = false) lab =
     148        lab.name ^ string_of_indexing pretty "i" lab.i
     149
     150let fresh l universe =
     151        {name = Atom.Gen.fresh universe; i = l} 
     152
     153(* TODO: urgh. Necessary? *)
     154type aux_t = t
     155                                                       
     156(** labels are endowed with a lexicographical ordering *)
     157module T : Map.OrderedType with type t = aux_t =
     158    struct
     159        type t = aux_t
     160        let compare = compare (* uses the built-in lexicographical comparison *)
     161    end
     162
     163module Map = Map.Make(T)   
     164module Set = Set.Make(T)
     165(** [constant_map d x] produces a finite map which associates
     166    [x] to every element of the set [d]. *)
     167
     168let indexings_of atom s =
     169        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
     170        Set.fold f s IndexingSet.empty
    3171
    4172let constant_map d x =
  • Deliverables/D2.2/8051/src/common/costLabel.mli

    r486 r1542  
    11
    2 (** This module provides functions to manipulate and create fresh cost
     2(** This module provides functions to manipulate and create indexed cost
    33    labels. *)
    44
    5 include StringSig.S
     5(** [Atom] provides functions for cost atoms, the root of indexed costs *)
     6module Atom : sig
     7  include StringSig.S
     8end
     9
     10(** Simple expressions corresponding to loop tranformations.
     11    TODO: abstract or not? *)
     12type sexpr = Sexpr of int*int
     13
     14(** The identity simple expression, used in initialization. *)
     15val sexpr_id : sexpr
     16
     17(** Indexes are identified with (single-entry) loop depths. *)
     18type index = int
     19
     20(** [make_id prefix index] produces an identifier out of a
     21    prefix and a loop depth. *)
     22val make_id : string -> index -> string
     23
     24type indexing = sexpr list
     25
     26(** The type of constant indexings, to be used by interpreations *)
     27type const_indexing
     28
     29(** [const_ind_iter f c] iterates [f] over the values of indexes in c *)
     30val const_ind_iter : (int -> unit) -> const_indexing -> unit
     31
     32(** This is equivalent to [List.hd], but raises
     33    [Invalid_argument "non-empty indexing stack"] if argument is empty *)
     34val curr_const_ind : const_indexing list -> const_indexing
     35
     36(** [enter_loop inds n] is used to update the indexing stack [ind] when one
     37    is entering a loop indexed by [n]. Raises [Invalid_argument
     38    "non-empty indexing stack"] if [inds] is empty. *)
     39val enter_loop : const_indexing list -> index -> unit
     40
     41(** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does
     42    nothing in case of [None].
     43    @see enter_loop *)
     44val enter_loop_opt : const_indexing list -> index option -> unit
     45
     46(** [continue_loop inds n] is used to update the indexing stack [inds] when
     47    one is continuing a loop indexed by [n].
     48    @raise [Invalid_argument "non-empty indexing stack"] if [inds] is empty.
     49    @raise [Invalid_argument "uninitialized loop index"] if the head of
     50    [inds] has no value for [index]. *)
     51val continue_loop : const_indexing list -> index -> unit
     52
     53(** [continue_loop_opt inds (Some n)] behaves like [continue_loop inds n], and
     54    does nothing in case of [None].
     55    @see continue_loop *)
     56val continue_loop_opt : const_indexing list -> index option -> unit
     57
     58(** [new_const_ind inds] pushes a new empty constant indexing on top of the
     59    stack [inds]. *)
     60val new_const_ind : const_indexing list -> const_indexing list
     61
     62(** [forget_const_ind inds] pops and discards the top constant indexing from the
     63    stack [inds].  Raises [Invalid_argument "non-empty indexing stack"] if
     64    [inds] is empty. *)
     65val forget_const_ind : const_indexing list -> const_indexing list
     66
     67(** [empty_indexing] is the empty indexing *)
     68val empty_indexing : indexing
     69
     70(** [add_id_indexing ind] adds an identity mapping in front of ind **)
     71val add_id_indexing : indexing -> indexing
     72
     73module IndexingSet : Set.S with type elt = indexing
     74
     75type t = {
     76  name : Atom.t;
     77  i : indexing
     78}
     79
     80(** [comp_index i s lbl] gives back the label [lbl] where index [i] is remapped
     81    to the simple expression [s]. *)
     82val comp_index : index -> sexpr -> t -> t
     83
     84(** [ev_indexing ind lbl] returns [lbl] where its indexing has been
     85    evaluated in the constant indexing [ind].
     86    @raise  Invalid_argument "constant indexing not enough to be applied" if
     87    [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *)
     88val ev_indexing : const_indexing -> t -> t
     89
     90(** [string_of_cost_label pref t] converts an indexed label to a
     91    string suitable for a label name in C source.
     92    [string_of_cost_label ~pretty:true t] prints a more readable form *)
     93val string_of_cost_label : ?pretty : bool -> t -> string
     94
     95(** [fresh i u] creates a fresh label using [u] as name universe, inside
     96    the indexing [i] (which represents the nested loops containing the label) *)
     97val fresh : indexing -> Atom.Gen.universe -> t
     98
     99module Set : Set.S with type elt = t
     100module Map : Map.S with type key = t
     101
     102(** [indexings_of a s] produces the set of indexings of an atom [a] occurring
     103    in the set of indexed labels [s]. *)
     104val indexings_of : Atom.t -> Set.t -> IndexingSet.t
    6105
    7106(** [constant_map d x] produces a finite map which associates
  • Deliverables/D2.2/8051/src/common/label.ml

    r486 r1542  
    11
    22include StringTools
     3
     4module ImpMap = struct
     5
     6  type key =
     7      Map.key
     8 
     9  type 'data t =
     10      'data Map.t ref
     11     
     12  let create () =
     13    ref Map.empty
     14
     15  let clear t =
     16    t := Map.empty
     17   
     18  let add k d t =
     19    t := Map.add k d !t
     20
     21  let find k t =
     22    Map.find k !t
     23
     24  let iter f t =
     25    Map.iter f !t
     26
     27end
  • Deliverables/D2.2/8051/src/common/label.mli

    r486 r1542  
    44
    55include StringSig.S
     6
     7(** Imperative label maps for use with Fix *)
     8module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t)
Note: See TracChangeset for help on using the changeset viewer.