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

Last change on this file since 1319 was 1319, checked in by tranquil, 9 years ago

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
File size: 2.0 KB
Line 
1
2(** This module provides functions to manipulate and create indexed cost
3    labels. *)
4               
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: leave it abstract or not? *)
12type sexpr
13
14val sexpr_id : sexpr
15
16(* trying a nameless approach *)
17type index = int
18
19val make_id : string -> index -> string
20
21type indexing = sexpr list
22
23type const_indexing = int array
24
25(** [enter_loop n indexing] is used to update indexing when one is entering a
26    loop indexed by [n].
27        The function recycles the same constant indexing *)
28val enter_loop : index option -> const_indexing -> unit
29
30(** [continue_loop n indexing] is used to update indexing when one is continuing a
31    loop indexed by [n]. *)
32val continue_loop : index option -> const_indexing -> unit
33
34(** [empty_indexing] generates an empty indexing *) 
35val empty_indexing : indexing
36
37(** [add_id_indexing ind] adds an identity mapping in front of ind **)
38val add_id_indexing : indexing -> indexing
39
40module IndexingSet : Set.S with type elt = indexing
41
42type t = {
43        name : Atom.t;
44        i : indexing
45}
46
47val apply_const_indexing : const_indexing -> t -> t
48
49
50(** [string_of_cost_label pref t] converts an indexed label to a
51    string suitable for a label name in source
52                [string_of_cost_label ~pretty:true t] prints a more readable form *)
53val string_of_cost_label : ?pretty : bool -> t -> string
54
55(** [fresh i u] creates a fresh label using [u] as name universe, inside
56    the indexing [i] (which represents the nested loops containing the label) *)
57val fresh : indexing -> Atom.Gen.universe -> t
58
59module Set : Set.S with type elt = t
60module Map : Map.S with type key = t
61
62(** [indexings_of a s] produces the set of indexings of an atom [a] occurring
63    in the set of indexed labels [s]. *)
64val indexings_of : Atom.t -> Set.t -> IndexingSet.t
65
66(** [constant_map d x] produces a finite map which associates
67    [x] to every element of the set [d]. *)
68val constant_map : Set.t -> 'a -> 'a Map.t
69
Note: See TracBrowser for help on using the repository browser.