source: src/Cminor/syntax.ma @ 950

Last change on this file since 950 was 886, checked in by campbell, 10 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.