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

Last change on this file since 1291 was 1291, checked in by tranquil, 8 years ago

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
File size: 3.0 KB
Line 
1module Atom =
2        struct
3                include StringTools
4        end
5
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
104
105let constant_map d x = 
106  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
107       
108        (**  **)
Note: See TracBrowser for help on using the repository browser.