source: Deliverables/D2.2/8051-memoryspaces-branch/src/languages.mli @ 1328

(** This module defines the intermediate languages. 

    This is a dispatching module that is aware of the whole
    compilation chain. It can also be used as an homogeneous way to
    deal with the intermediate languages functionalities.
*)


type name = 
  | Clight
  | Cminor
  | RTLabs
  | RTL
  | ERTL
  | LTL
  | LIN
  | ASM

(** {2 Abstract syntax trees} *)

(** The types of abstract syntax trees of each language. *)
type ast = 
  | AstClight of Clight.program
  | AstCminor of Cminor.program
  | AstRTLabs of RTLabs.program
  | AstRTL    of RTL.program
  | AstERTL   of ERTL.program
  | AstLTL    of LTL.program
  | AstLIN    of LIN.program
  | AstASM    of ASM.program

(** [language_of_ast ast] returns the programming language of the 
    abstract syntax tree [ast]. *)
val language_of_ast : ast -> name

(** [parse name] returns the parsing function of the language
    [name]. *)
val parse : name -> (string -> ast) 

(** {2 Compilation} *)

(** [compile debug l1 l2] returns the compilation function that
    translates the language [l1] to the language [l2]. This may be the
    composition of several compilation functions. If [debug] is
    [true], all the intermediate programs are inserted in the
    output. *)
val compile : bool -> name -> name -> (ast -> ast list)

(** {2 Annotation} 

    Labelling consists in the insertion of so-called "cost labels" 
    which are useful control points in order to compute costs.

    The annotation process first computes cost of constant-time
    execution path starting from each cost label on the lowest-level
    language. Then, it instruments the (high-level) source code with
    these computed costs.
*)

(** [labelize ast] inserts cost labels in the program [ast]. *)
val labelize : ast -> ast

(** [annotate input_ast target_ast] inserts cost annotations into the
    input AST from the (final) target AST. *)
val annotate : ast -> ast -> ast

(** [interpret ast] runs the program [ast] from the default initial
    configuration. This interpretation may emit some cost labels. *)
val interpret : ast -> CostLabel.t list

(** {2 Serialization} *)

(** [save filename input_ast] pretty prints [input_ast] in a fresh
    file whose name is prefixed by [filename] and whose extension
    is deduced from the language of the AST. *)
val save : string -> ast -> unit

(** [save_matita filename asts] pretty prints the first Clight AST in
    [asts] in a fresh file whose name is prefixed by [filename] and whose
    extension is .ma. *)
val save_matita : string -> ast list -> unit

(** [from_string s] parses [s] as an intermediate language name. *)
val from_string : string -> name

(** [to_string n] prints [n] as a string. *)
val to_string   : name -> string