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

Last change on this file since 1310 was 1310, checked in by tranquil, 9 years ago
  • finished changes on annotator
  • implementing indexes in interpreter
File size: 4.4 KB
Line 
1module Atom =
2        struct
3                include StringTools
4        end
5
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 sexpr_id = Sexpr(1, 0)
13
14type index = int
15
16let make_id prefix depth = prefix ^ string_of_int depth
17
18type indexing = sexpr list
19
20type const_indexing = int ref list
21
22(** [enter_loop n indexing] is used to update indexing when one is entering a
23    loop indexed by [n].
24                The function recycles the same constant indexing *)
25let rec enter_loop n indexing = match n, indexing with
26        | None, _ -> indexing (* entering a multi-entry loop *)
27        | Some 0, [] -> [ref 0] (* entering a single entry loop, current depth *)
28        | Some 0, hd :: tl -> hd := 0; indexing (* as above, reusing slot *) 
29        | Some x, hd :: tl -> hd :: enter_loop (Some (x-1)) tl (* lower depth *)
30        | Some x, [] -> assert false(* means I'm entering a single entry loop *)
31                                    (* without having entered the one containing it *)       
32
33(** [enter_loop n indexing] is used to update indexing when one is continuing a
34    loop indexed by [n]. *)
35let rec continue_loop n indexing = match n, indexing with
36        | None, _ -> indexing (* continuing a multi-entry loop *)
37        | Some 0, hd :: tl -> hd := !hd + 1; indexing (* incrementing index *) 
38        | Some x, hd :: tl -> hd :: continue_loop (Some (x-1)) tl (* lower depth *)
39        | Some _, [] -> assert false (* means I'm continuing a single entry loop *)
40                                     (* without having entered it *)       
41
42let sexpr_of i l = 
43    try
44        List.nth l i
45    with
46                        | Failure _
47      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
48
49let rec id_indexing = function
50        | 0 -> []
51        | n -> sexpr_id :: id_indexing (n-1)
52
53(* a*_+b is composed with c*_+d by substitution: *)
54(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
55let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
56    Sexpr (a * c, b * c + d)
57               
58let ev_sexpr i (Sexpr(a, b)) = a*i+b
59
60(* i|-->e ° I *)
61let rec compose_index i s l = match i, l with
62        | 0, s' :: l' -> compose_sexpr s s' :: l'
63        | x, s' :: l' -> compose_index (i-1) s l'
64        | _ -> l
65
66
67(* I°J applies every mapping in I to every mapping in J *)
68let rec compose_indexing m n = match m, n with
69        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
70        | _ -> n 
71
72let rec compose_const_indexing c m = match c, m with
73        | i1 :: l1, s2 :: l2 -> ev_sexpr !i1 s2 :: compose_const_indexing l1 l2
74        | _, [] -> [] (* that's ok as current indexings will not be shrinked *)
75        | [], _ -> assert false (* means an indexed label is not in the right ctx *) 
76
77module IndexingSet = Set.Make(struct
78    type t = indexing
79                let compare = compare
80        end)
81
82
83type t = {
84    name : Atom.t;
85    i : indexing
86}
87
88
89(* if [pretty] is false then a name suitable for labels is given*)
90(* ('P' replaces '+') *)
91let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
92        let plus = if pretty then "+" else "P" in
93        let id = prefix ^ string_of_int i in
94  let a_id_s = if a = 1 then id else string_of_int a ^ id in
95        let b_s = string_of_int b in
96        if a = 0 then b_s else
97        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
98       
99(* examples:*)
100(* [pretty] true:  (0,i1+1,2i2+2)*)
101(* [pretty] false: _0_i1P1_2i2P2 *)
102let rec string_of_indexing_tl pretty prefix i = function
103        | [] -> if pretty then ")" else ""
104        | hd :: tl ->
105                let sep = if pretty then "," else "_" in
106                let str = string_of_sexpr pretty prefix i hd in
107                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
108
109let string_of_indexing pretty prefix = function
110        | [] -> ""
111        | hd :: tl ->
112                let start = if pretty then "(" else "_" in
113    let str = string_of_sexpr pretty prefix 0 hd in
114                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
115               
116let string_of_cost_label ?(pretty = false) lab =
117        lab.name ^ string_of_indexing pretty "i" lab.i
118
119let fresh l universe =
120        {name = Atom.Gen.fresh universe; i = l} 
121
122(* TODO: urgh. Necessary? *)
123type aux_t = t
124                                                       
125(** labels are endowed with a lexicographical ordering *)
126module T : Map.OrderedType with type t = aux_t =
127    struct
128        type t = aux_t
129        let compare = compare (* uses the built-in lexicographical comparison *) 
130    end
131
132module Map = Map.Make(T)   
133module Set = Set.Make(T) 
134(** [constant_map d x] produces a finite map which associates
135    [x] to every element of the set [d]. *)
136
137let indexings_of atom s =
138        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
139        Set.fold f s IndexingSet.empty
140
141let constant_map d x = 
142  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
143       
144        (**  **)
Note: See TracBrowser for help on using the repository browser.