source: Deliverables/D2.2/8051/src/languages.mli @ 619

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

Update of D2.2 from Paris.

File size: 3.0 KB
Line 
1(** This module defines the intermediate languages.
2
3    This is a dispatching module that is aware of the whole
4    compilation chain. It can also be used as an homogeneous way to
5    deal with the intermediate languages functionalities.
6*)
7
8
9type name = 
10  | Clight
11  | Cminor
12  | RTLabs
13  | RTL
14  | ERTL
15  | LTL
16  | LIN
17  | ASM
18
19(** {2 Abstract syntax trees} *)
20
21(** The types of abstract syntax trees of each language. *)
22type ast = 
23  | AstClight of Clight.program
24  | AstCminor of Cminor.program
25  | AstRTLabs of RTLabs.program
26  | AstRTL    of RTL.program
27  | AstERTL   of ERTL.program
28  | AstLTL    of LTL.program
29  | AstLIN    of LIN.program
30  | AstASM    of ASM.program
31
32(** [language_of_ast ast] returns the programming language of the
33    abstract syntax tree [ast]. *)
34val language_of_ast : ast -> name
35
36(** [parse name] returns the parsing function of the language
37    [name]. *)
38val parse : name -> (string -> ast) 
39
40(** {2 Compilation} *)
41
42(** [compile debug l1 l2] returns the compilation function that
43    translates the language [l1] to the language [l2]. This may be the
44    composition of several compilation functions. If [debug] is
45    [true], all the intermediate programs are inserted in the
46    output. *)
47val compile : bool -> name -> name -> (ast -> ast list)
48
49(** {2 Annotation}
50
51    Labelling consists in the insertion of so-called "cost labels"
52    which are useful control points in order to compute costs.
53
54    The annotation process first computes cost of constant-time
55    execution path starting from each cost label on the lowest-level
56    language. Then, it instruments the (high-level) source code with
57    these computed costs.
58*)
59
60(** [labelize ast] inserts cost labels in the program [ast]. *)
61val labelize : ast -> ast
62
63(** [annotate input_ast target_ast] inserts cost annotations into the input AST
64    from the (final) target AST. It also returns the name of the cost increment
65    function *)
66val annotate : ast -> ast -> (ast * string)
67
68(** [interpret print_result ast] runs the program [ast] from the default initial
69    configuration. This interpretation may emit some cost labels. If
70    [print_result] is [true], then the result of the interpretations is
71    output. *)
72val interpret : bool -> ast -> AST.trace
73
74(** {2 Serialization} *)
75
76(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
77    whose name is prefixed by [filename] and whose extension is deduced from the
78    language of the AST. If [exact_output] is false then the written file will
79    be fresh. *)
80val save : bool -> string -> ast -> unit
81
82(** [save_cost_incr filename cost_incr] prints the name of the cost increment
83    function [cost_incr] in the file prefixed by [filename] and extended with
84    ".cost". If the file already exists, it is overwritten. *)
85val save_cost_incr : string -> string -> unit
86
87(** [from_string s] parses [s] as an intermediate language name. *)
88val from_string : string -> name
89
90(** [to_string n] prints [n] as a string. *)
91val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.