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

Last change on this file since 1584 was 1584, checked in by tranquil, 8 years ago
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
File size: 6.4 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
66  val replace : (unit -> G.node) ->
67    G.node -> G.statement list -> G.node list option -> G.t -> G.t
68
69  val replace' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
70    G.node -> (G.statement, 'r, 't) BList.t -> G.node list option ->
71    'u -> G.t -> 'u * G.t
72
73  val insert : (unit -> G.node) ->
74    G.node -> G.statement list -> G.t -> G.node * G.t
75
76  val insert' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
77    G.node -> (G.statement, 'r, 't) BList.t ->
78    'u -> G.t -> 'u * G.node * G.t
79
80
81end
82
83(** This module provides a helper function to translate graphs between the
84    same or different languages. *)
85module Trans :
86  functor (Src : GraphType) ->
87    functor (Trg : GraphType with type node = Src.node) -> sig
88
89      type node = Src.node
90
91      (** [translate fresh f info g] translates [g] according to [f] using
92          [fresh] as node generating function and updating [info].
93
94          If [f x lbl stmt = (y, b)], then block [b] will replace [stmt] at
95          [lbl], with [lbl] itself as entry and the successors of [stmt] as
96          successors. [b]'s actual labels are ignored, but care must be taken
97          to end [b] with a statement that can have the same successors of
98          [stmt]. The ['a] parameter can be used to store global data that
99          needs to be used and/or updated during the translation (a typical
100          example are temporary variable declarations). *)
101      val translate : (unit -> node) ->
102        ('a -> node -> Src.statement -> 'a * Trg.statement list) ->
103        'a -> Src.t -> 'a * Trg.t
104
105  (** [translate_with_redirects] behaves like [translate], but is able to set
106      successors different than those of the starting statement. If
107      [f x lbl stmt = (y, b, None)], then the behaviour at [lbl] is the same
108      as for [translate]. If [f x lbl stmt = (y, b, Some succs)], then
109      [succs] will be used as successors to [b] instead. A typical example of
110      a use of this translation is for eliminating branchings that are known
111      to always take one route.
112      @see translate *)
113  val translate_with_redirects : (unit -> node) ->
114    ('a -> node -> Src.statement ->
115     'a * Trg.statement list * node list option) ->
116    'a -> Src.t -> 'a * Trg.t
117
118  (** [translate_pure] works like [ranslate], but accepts a translation
119      function that does not have an additional state. @see translate *)
120  val translate_pure : (unit -> node) ->
121    (node -> Src.statement -> Trg.statement list) -> Src.t -> Trg.t
122
123  (** [translate_pure_with_redirects] works like [ranslate_with_redirects],
124      but accepts a translationfunction that does not have an additional state.
125      @see translate_with_redirects
126      @see translate *)
127  val translate_pure_with_redirects : (unit -> node) ->
128    (node -> Src.statement -> Trg.statement list * node list option) ->
129    Src.t -> Trg.t
130
131
132  (** [translate' freshl freshr f u g] works like [translate] but uses lists
133      with binders as defined in BList. Each time a binder is encountered in
134      the translation of a statement, [freshr] is used incrementally (starting
135      from [u]) to generate an argument for the rest of the list of statements.
136      In this way the generation of (typically) fresh temporaries is left to
137      the final general function, while it can be encoded in place inside the
138      translation.
139      @see translate *)
140  val translate' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
141    (node -> Src.statement -> (Trg.statement, 'reg, 't) BList.t) ->
142    'u -> Src.t -> 'u * Trg.t
143
144  (** [translate_with_redirects'] is the analogous of [translate'] with
145      the possibility for redirection as in [translate_with_redirects].
146      @see translate'
147      @see translate_with_redirect *)
148  val translate_with_redirects' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
149    (node -> Src.statement ->
150     (Trg.statement, 'reg, 't) BList.t * node list option) ->
151    'u -> Src.t -> 'u * Trg.t
152
153end
Note: See TracBrowser for help on using the repository browser.