source: src/Cminor/syntax.ma @ 1139

Last change on this file since 1139 was 1139, checked in by campbell, 8 years ago

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 1.7 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
43definition Cminor_program ≝ program (fundef internal_function) (list init_data).
44
45definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.