source: Deliverables/D2.3/8051-memoryspaces-branch/src/languages.mli @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 2.7 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
64    input AST from the (final) target AST. *)
65val annotate : ast -> ast -> ast
66
67(** [interpret ast] runs the program [ast] from the default initial
68    configuration. This interpretation may emit some cost labels. *)
69val interpret : ast -> CostLabel.t list
70
71(** {2 Serialization} *)
72
73(** [save filename input_ast] pretty prints [input_ast] in a fresh
74    file whose name is prefixed by [filename] and whose extension
75    is deduced from the language of the AST. *)
76val save : string -> ast -> unit
77
78(** [save_matita filename asts] pretty prints the first Clight AST in
79    [asts] in a fresh file whose name is prefixed by [filename] and whose
80    extension is .ma. *)
81val save_matita : string -> ast list -> unit
82
83(** [from_string s] parses [s] as an intermediate language name. *)
84val from_string : string -> name
85
86(** [to_string n] prints [n] as a string. *)
87val to_string   : name -> string
Note: See TracBrowser for help on using the repository browser.