source: src/Cminor/syntax.ma @ 898

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

Put types into parameter and variable lists in Cminor.
Temporarily breaks translation to RTLabs.

File size: 1.6 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 (int × 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) unit.
Note: See TracBrowser for help on using the repository browser.