source: Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli @ 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: 1.9 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(** Loop indices, to be identified with Clight identifiers *)
11module Index : sig
12        include StringSig.S
13end
14
15(** Simple expressions corresponding to loop tranformations. *)
16type sexpr
17
18val sexpr_id : sexpr
19
20module Indexing : sig
21        include Set.OrderedType
22        val empty : t
23end
24
25(** [sexpr_of i l] extracts the simple expression relative to [i] in [l].
26    It raises an [Invalid_argument] exception if [i] is not handled by [l] *)
27val sexpr_of : Index.t -> Indexing.t -> sexpr
28
29(** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 
30val compose_index : Index.t -> sexpr -> Indexing.t -> Indexing.t
31
32(** [compose_index l m] applies all the transformations in  [l] to [m] *)
33val compose_indexing : Indexing.t -> Indexing.t -> Indexing.t
34
35module IndexingSet : Set.S with type elt = Indexing.t
36
37type t = {
38        name : Atom.t;
39        i : Indexing.t
40}
41
42(** [string_of_cost_label t] converts an indexed label to a
43    string suitable for a label name in source.
44                [string_of_cost_label ~pretty:true t] prints a more readable form *)
45val string_of_cost_label : ?pretty : bool -> t -> string
46
47(** [fresh i u] creates a fresh label using [u] as name universe, inside
48    the indexing [i] (which represents the nested loops containing the label) *)
49val fresh : Indexing.t -> Atom.Gen.universe -> t
50
51module Set : Set.S with type elt = t
52module Map : Map.S with type key = t
53
54(** [indexings_of a s] produces the set of indexings of an atom [a] occurring
55    in the set of indexed labels [s]. *)
56val indexings_of : Atom.t -> Set.t -> IndexingSet.t
57
58(** [constant_map d x] produces a finite map which associates
59    [x] to every element of the set [d]. *)
60val constant_map : Set.t -> 'a -> 'a Map.t
61
Note: See TracBrowser for help on using the repository browser.