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

Last change on this file since 1433 was 1433, checked in by tranquil, 8 years ago
  • added infrastructure to add same-language transformations along the compilation chain from command line options
  • started work on cost expression semplification
File size: 2.9 KB
Line 
1type cond =
2        | Ceq of int         (** index is equal to *)
3        | Cgeq of int        (** index is greater or equal to *)
4        | Cmod of int*int      (** index modulo equal to *)
5  | Cgeqmod of int*int*int (** index greater than and modulo equal to *)
6
7module CondSet = Set.Make(struct
8    type t = cond
9    let compare = compare
10end)
11
12open CostLabel
13
14   
15let cond_of_sexpr = function
16    | Sexpr(0, b) -> Ceq(b)
17    | Sexpr(1, b) -> Cgeq(b)
18    | Sexpr(a, b) when b < a -> Cmod(a, b)
19  | Sexpr(a, b) -> Cgeqmod(b, a, b mod a)
20
21type cost_expr =
22    | Exact of int
23    | Ternary of index * cond * cost_expr * cost_expr
24
25(* compute from the set [s] a the 3-uple [Some (h, s_h, s_rest)] where *)
26(* [h] is the head of first elements of [s], and [s] is the union of *)
27(* [{h :: tl | tl in s_h}] and [s_rest]. Gives [None] if either [s] is empty *)
28(* or it starts with an empty list. ([s] should contain lists with same length *)
29let heads_tails_of s =
30    if IndexingSet.is_empty s then None else
31    match IndexingSet.min_elt s with
32        | [] -> None
33        | head :: _ ->
34            let filter x = (List.hd x = head) in
35            let (s_head, s_rest) = IndexingSet.partition filter s in
36            let add_tail l = IndexingSet.add (List.tl l) in
37            let s_head = IndexingSet.fold add_tail s_head IndexingSet.empty in 
38            Some (head, s_head, s_rest) 
39
40let rec cost_mapping_ind atom ind (m : int Map.t) (s : IndexingSet.t) =
41    let lbl = {name = atom; i = ind} in
42    match heads_tails_of s with
43        | None when Map.mem lbl m-> Exact (Map.find lbl m)
44        | None -> Exact 0
45        | Some(h, s_head, s_rest) ->
46            let i = List.length ind in
47            let condition = cond_of_sexpr h in
48            let if_true = cost_mapping_ind atom (h :: ind) m s_head in
49            let if_false = cost_mapping_ind atom ind m s_rest in
50            Ternary(i, condition, if_true, if_false) 
51
52let indexing_sets_from_cost_mapping m =
53    let f k _ sets =
54        let s =
55            try
56                IndexingSet.add k.i (Atom.Map.find k.name sets)
57            with
58                | Not_found -> IndexingSet.singleton k.i in
59        Atom.Map.add k.name s sets in
60    Map.fold f m Atom.Map.empty
61   
62let cost_expr_mapping_of_cost_mapping m =
63    let sets = indexing_sets_from_cost_mapping m in
64    let f at s =
65         Atom.Map.add at (cost_mapping_ind at [] m s) in
66    Atom.Map.fold f sets Atom.Map.empty
67               
68
69let rec init_set f = function
70        | 0 -> CondSet.empty
71        | n -> CondSet.add (f (n-1)) (init_set f (n-1))
72
73let fill_ceq = init_set (fun x -> Ceq x)
74
75let fill_mod a = init_set (fun x -> Cmod (a, x))
76
77let fill_ceq_mod a b = init_set (fun x -> Ceq (a * x + b))
78 
79let cond_not = function
80        | Ceq k ->
81                CondSet.add (Cgeq (k+1)) (fill_ceq k)
82        | Cgeq k -> fill_ceq k
83        | Cmod (a, b) -> CondSet.remove (Cmod (a, b)) (fill_mod a a)
84        | Cgeqmod (k, a, b) ->
85                let non_mod = CondSet.remove (Cmod (a, b)) (fill_mod a a) in
86                CondSet.union (fill_ceq_mod a b (k / a)) non_mod
Note: See TracBrowser for help on using the repository browser.