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