source: Deliverables/D2.2/8051/src/LTL/LTLToLINI.mli @ 818

Last change on this file since 818 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 1.8 KB
Line 
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
10module 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
43end) : 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
56end
57
Note: See TracBrowser for help on using the repository browser.