source: Deliverables/D2.2/8051/src/utilities/graphUtilities.mli @ 1580

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

implemented constant propagation in LTL
cleaned up translations in optimizations, a new module for translations is available

File size: 5.9 KB
Line 
1(** This module provides some general utilities for graph-like languages *)
2
3(** The module signature of graphs over which the functions will be defined *)
4module type GraphType = sig
5
6  (** The type of labels for nodes *)
7  type node
8
9  (** The type of statements of the language *)
10  type statement
11
12  (** Maps and sets over nodes *)
13  module NodeMap : Map.S with type key = node
14  module NodeSet : Set.S with type elt = node
15
16  (** The type of graphs of the language *)
17  type t = statement NodeMap.t
18
19  (** Successors are encoded in the statement. This function must
20      be able to extract them *)
21  val successors : statement -> node list
22
23  (** The skip/goto statement of the language *)
24  val skip : node -> statement
25
26  (** A function which replaces the successors of a statement with
27      the given nodes. It must not be defined in case of mismatch
28      between the provided successors and the ones allowed for the
29      statement. *)
30  val fill_succs : statement -> node list -> statement
31
32end
33
34(** This functor gives various helper functions over a single language *)
35module Util : functor (G : GraphType) -> sig
36
37  (** [compute_predecessor_lists g] gives a map mapping all the nodes
38      of [g] to the list of their predecessors. It is ensured that the
39      domain of the resulting map is equal to the one of [g]. Nodes with
40      no predecessors are mapped to empty lists. *)
41  val compute_predecessor_lists : G.t -> G.node list G.NodeMap.t
42
43  (** [dfs_fold f g entry init] computes [f ln sn (... (f l1 s1 init) ...)]
44      where [li, si] are nodes and statements of [g] in depth-first order,
45      starting with entry point [entry]. The order in which children are
46      explored is given by [G.successors]. Nodes that are unreachable from
47      [entry] are ignored.
48      @raises Invalid_argument if [entry] is not in [g]
49      @raises Not_found if a reachable node has successors outside of [g] *)
50  val dfs_fold :
51    (G.node -> G.statement -> 'a -> 'a) -> G.t -> G.node -> 'a -> 'a
52
53  (** [dfs_iter f g entry] iterates [f] over all [li, si]  nodes and statements
54      of [g] in depth-first order, starting with entry point [entry]. The order
55      in which children are explored is given by [G.successors]. Nodes that are
56      unreachable from [entry] are ignored.
57      @raises Invalid_argument if [entry] is not in [g]
58      @raises Not_found if a reachable node has successors outside of [g] *)
59  val dfs_iter :
60    (G.node -> G.statement -> unit) -> G.t -> G.node -> unit
61
62  (** [dead_code_elim g entry] gives back [g] where all nodes unreachable from
63      [entry] have been eliminated. *)
64  val dead_code_elim : G.t -> G.node -> G.t
65
66end
67
68(** This module provides a helper function to translate graphs between the
69    same or different languages. *)
70module Trans :
71  functor (Src : GraphType) ->
72    functor (Trg : GraphType with type node = Src.node) -> sig
73
74      type node = Src.node
75
76      (** [translate fresh f info g] translates [g] according to [f] using
77          [fresh] as node generating function and updating [info].
78
79          If [f x lbl stmt = (y, b)], then block [b] will replace [stmt] at
80          [lbl], with [lbl] itself as entry and the successors of [stmt] as
81          successors. [b]'s actual labels are ignored, but care must be taken
82          to end [b] with a statement that can have the same successors of
83          [stmt]. The ['a] parameter can be used to store global data that
84          needs to be used and/or updated during the translation (a typical
85          example are temporary variable declarations). *)
86      val translate : (unit -> node) ->
87        ('a -> node -> Src.statement -> 'a * Trg.statement list) ->
88        'a -> Src.t -> 'a * Trg.t
89
90  (** [translate_with_redirects] behaves like [translate], but is able to set
91      successors different than those of the starting statement. If
92      [f x lbl stmt = (y, b, None)], then the behaviour at [lbl] is the same
93      as for [translate]. If [f x lbl stmt = (y, b, Some succs)], then
94      [succs] will be used as successors to [b] instead. A typical example of
95      a use of this translation is for eliminating branchings that are known
96      to always take one route.
97      @see translate *)
98  val translate_with_redirects : (unit -> node) ->
99    ('a -> node -> Src.statement ->
100     'a * Trg.statement list * node list option) ->
101    'a -> Src.t -> 'a * Trg.t
102
103  (** [translate_pure] works like [ranslate], but accepts a translation
104      function that does not have an additional state. @see translate *)
105  val translate_pure : (unit -> node) ->
106    (node -> Src.statement -> Trg.statement list) -> Src.t -> Trg.t
107
108  (** [translate_pure_with_redirects] works like [ranslate_with_redirects],
109      but accepts a translationfunction that does not have an additional state.
110      @see translate_with_redirects
111      @see translate *)
112  val translate_pure_with_redirects : (unit -> node) ->
113    (node -> Src.statement -> Trg.statement list * node list option) ->
114    Src.t -> Trg.t
115
116
117  (** [translate' freshl freshr f u g] works like [translate] but uses lists
118      with binders as defined in BList. Each time a binder is encountered in
119      the translation of a statement, [freshr] is used incrementally (starting
120      from [u]) to generate an argument for the rest of the list of statements.
121      In this way the generation of (typically) fresh temporaries is left to
122      the final general function, while it can be encoded in place inside the
123      translation.
124      @see translate *)
125  val translate' : (unit -> node) -> ('u -> 'u * 'reg) ->
126    (node -> Src.statement -> (Trg.statement, 'reg) BList.t) ->
127    'u -> Src.t -> 'u * Trg.t
128
129  (** [translate_with_redirects'] is the analogous of [translate'] with
130      the possibility for redirection as in [translate_with_redirects].
131      @see translate'
132      @see translate_with_redirect *)
133  val translate_with_redirects' : (unit -> node) -> ('u -> 'u * 'reg) ->
134    (node -> Src.statement ->
135     (Trg.statement, 'reg) BList.t * node list option) ->
136    'u -> Src.t -> 'u * Trg.t
137
138end
Note: See TracBrowser for help on using the repository browser.