Ignore:
Timestamp:
Oct 5, 2011, 10:20:41 AM (8 years ago)
Author:
tranquil
Message:

Started branch of untrusted compiler with indexed labels

  • added indexing structure to CostLabel?
  • propagated changes to other modules
  • added indexing as parameter to labelling
  • loop indexes not implemented yet, so behaviour is still the same
Location:
Deliverables/D2.2/8051-indexed-labels-branch
Files:
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r486 r1291  
     1module Atom =
     2        struct
     3                include StringTools
     4        end
    15
    2 include StringTools
     6module StringMap = Map.Make(String)
     7
     8module Index =
     9        struct
     10                include StringTools
     11        end
     12
     13(** Simple expressions are for now affine maps of the form a*_+b *)
     14type sexpr =
     15    | Sexpr of int*int
     16
     17let sexpr_id = Sexpr(1, 0)
     18
     19let sexpr_of i l = snd (List.find (function (j, _) -> j = i) l)
     20
     21(** not using Map as insertion order matters *)
     22module Indexing =
     23        struct
     24                type t = (Index.t * sexpr) list
     25                let compare = compare (* built-in lexicographic order *)
     26                let empty = []
     27        end
     28
     29(* a*_+b is composed with c*_+d by substitution: *)
     30(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
     31let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
     32    Sexpr (a * c, b * c + d)
     33
     34(* i|-->e ° j|-->f = j|-->e°f   if i=j,  j|-->f otherwise *)
     35(* NB: if simple expressions are changed to more complex ones,*)
     36(* this must change *)
     37let compose_index_singl i1 s1 (i2,s2) =
     38    (i2, if i1 = i2 then compose_sexpr s1 s2 else s2)
     39
     40(* i|-->e ° I *)
     41let compose_index i s = List.map (compose_index_singl i s)
     42
     43(* I°J applies every mapping in I to every mapping in J *)
     44(* TODO: can we use the shape indexings have in actual usage? *)
     45let compose_indexing = List.fold_right (function (i,s) -> compose_index i s)
     46
     47
     48module IndexingSet = Set.Make(Indexing)
     49
     50
     51type t = {
     52    name : Atom.t;
     53    i : Indexing.t
     54}
     55
     56(* if [pretty] is false then a name suitable for labels is given*)
     57(* ('P' replaces '+') *)
     58let string_of_sexpr pretty id (Sexpr(a, b)) =
     59        let plus = if pretty then "+" else "P" in
     60  let a_id_s = if a = 1 then id else string_of_int a^id in
     61        let b_s = string_of_int b in
     62        if a = 0 then b_s else
     63        if b = 0 then a_id_s else a_id_s^plus^b_s
     64       
     65(* examples:*)
     66(* [pretty] true:  (0,i+1,2j+2)*)
     67(* [pretty] false: _0_iP1_2jP2 *)
     68let string_of_indexing pretty = function
     69        | [] -> ""
     70        | (i, s) :: l ->
     71                (* !!! assuming i starts with '_' which can be omitted !!! *)
     72                let i = String.sub i 1 (String.length i) in
     73                let left = if pretty then "(" else "_" in
     74                let right = if pretty then ")" else "" in
     75                let sep = if pretty then "," else "_" in
     76                let first = string_of_sexpr pretty i s in
     77                let f accu (j, t) = accu ^ sep ^ (string_of_sexpr pretty j t) in
     78                left ^ List.fold_left f first l ^ right
     79               
     80let string_of_cost_label ?(pretty = false) lab =
     81        lab.name ^ string_of_indexing pretty lab.i
     82
     83let fresh l universe =
     84        {name = Atom.Gen.fresh universe; i = l} 
     85
     86(* TODO: urgh. Necessary? *)
     87type aux_t = t
     88                                                       
     89(** labels are endowed with a lexicographical ordering *)
     90module T : Map.OrderedType with type t = aux_t =
     91    struct
     92        type t = aux_t
     93        let compare = compare (* uses the built-in lexicographical comparison *)
     94    end
     95
     96module Map = Map.Make(T)   
     97module Set = Set.Make(T)
     98(** [constant_map d x] produces a finite map which associates
     99    [x] to every element of the set [d]. *)
     100
     101let indexings_of atom s =
     102        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
     103        Set.fold f s IndexingSet.empty
    3104
    4105let constant_map d x =
    5106  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
     107       
     108        (**  **)
Note: See TracChangeset for help on using the changeset viewer.