]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/LTL/LTLToLINI.mli
Package description and copyright added.
[pkg-cerco/acc.git] / src / LTL / LTLToLINI.mli
1
2 (** This module is the central part of the translation of [LTL]
3     programs into [LIN] programs. *)
4
5 (* Adapted from Pottier's PP compiler *)
6
7 (* The functor [Visit] implements the core of the translation of
8    [LTL] to [LIN]. *)
9
10 module Visit (S : sig
11
12   (* [fetch l] is the statement found at label [l] in the source
13      program. *)
14
15   val fetch: Label.t -> LTL.statement
16
17   (* [translate_statement stmt] translates the [LTL] statement [stmt] to
18      a [LIN] statement. [LTL] statements that have one explicit
19      successor are turned into [LIN] statements with an implicit
20      successor. [LTL] statements that have two explicit successors
21      are turned into [LIN] statements where the first successor is
22      explicit and the second successor is implicit. *)
23
24   val translate_statement: LTL.statement -> LIN.statement
25
26   (* [generate stmt] generates statement [stmt]. Statements are
27      generated sequentially. *)
28
29   val generate: LIN.statement -> unit
30
31   (* [require l] records the fact that the label [l] should explicitly
32      exist in the [LIN] program. It must be used whenever a [LIN]
33      branch statement is issued. *)
34
35   val require: Label.t -> unit
36
37   (* [mark l] marks the label [l]. [marked l] tells whether [l] is
38      marked. *)
39
40   val mark: Label.t -> unit
41   val marked: Label.t -> bool
42
43 end) : sig
44
45   (* [visit] implements a depth-first traversal of the control flow graph,
46      generating statements as new nodes are being discovered.
47
48      If label [l] has already been discovered, then [visit l] issues
49      an [St_goto] statement towards [l]. If [l] has not been
50      discovered yet, [visit l] marks [l] as discovered, issues an
51      [St_label] statement, translates the statement found at [l] in
52      the source program, and visits its successors. *)
53
54   val visit: Label.t -> unit
55
56 end
57