source: src/RTLabs/syntax.ma @ 1288

Last change on this file since 1288 was 1224, checked in by sacerdot, 8 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File size: 1.8 KB
Line 
1
2include "basics/logic.ma".
3
4include "common/AST.ma".
5include "common/CostLabel.ma".
6include "common/FrontEndOps.ma".
7include "common/Registers.ma".
8
9include "ASM/Vector.ma".
10include "common/Graphs.ma".
11
12inductive statement : Type[0] ≝
13| St_skip : label → statement
14| St_cost : costlabel → label → statement
15| St_const : register → constant → label → statement
16| St_op1 : unary_operation → register → register → label → statement (* destination source *)
17| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
18| St_load : memory_chunk → register → register → label → statement
19| St_store : memory_chunk → register → register → label → statement
20| St_call_id : ident → list register → option register → label → statement
21| St_call_ptr : register → list register → option register → label → statement
22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
24| St_cond : register → label → label → statement
25| St_jumptable : register → list label → statement
26| St_return : statement
27.
28
29record internal_function : Type[0] ≝
30{ f_labgen    : universe LabelTag
31; f_reggen    : universe RegisterTag
32; f_result    : option (register × typ)
33; f_params    : list (register × typ)
34; f_locals    : list (register × typ)
35; f_stacksize : nat
36; f_graph     : graph statement
37; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
38; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
39}.
40
41(* Note that the global variables will be initialised by the code in main
42   by this stage, so the only initialisation data is the amount of space to
43   allocate. *)
44
45definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.