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 *) |
---|
4 | module 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 | |
---|
32 | end |
---|
33 | |
---|
34 | (** This functor gives various helper functions over a single language *) |
---|
35 | module 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 | end |
---|
67 | |
---|
68 | (** This module provides a helper function to translate graphs between the |
---|
69 | same or different languages. *) |
---|
70 | module 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 | |
---|
138 | end |
---|