source: src/Cminor/syntax.ma @ 1224

Last change on this file since 1224 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: 2.0 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4
5(* TODO: consider making the typing stricter. *)
6
7inductive expr : typ → Type[0] ≝
8| Id : ∀t. ident → expr t
9| Cst : ∀t. constant → expr t
10| Op1 : ∀t,t'. unary_operation → expr t → expr t'
11| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
12| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
13| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
14| Ecost : ∀t. costlabel → expr t → expr t.
15
16inductive stmt : Type[0] ≝
17| St_skip : stmt
18| St_assign : ∀t. ident → expr t → stmt
19| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
20(* ident for returned value, expression to identify fn, args. *)
21| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
22| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
23| St_seq : stmt → stmt → stmt
24| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
25| St_loop : stmt → stmt
26| St_block : stmt → stmt
27| St_exit : nat → stmt
28(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
30| St_return : option (Σt. expr t) → stmt
31| St_label : ident → stmt → stmt
32| St_goto : ident → stmt
33| St_cost : costlabel → stmt → stmt.
34
35record internal_function : Type[0] ≝
36{ f_return    : option typ
37; f_params    : list (ident × typ)
38; f_vars      : list (ident × typ)
39; f_stacksize : nat
40; f_body      : stmt
41}.
42
43(* We define two closely related versions of Cminor, the first with the original
44   initialisation data for global variables, and the second where the code is
45   responsible for initialisation and we only give the size of each variable. *)
46
47definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
48
49definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.