source: src/Cminor/syntax.ma @ 1147

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

Remove some obsolete commented out code, update a couple of comments.

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.