source: src/Cminor/syntax.ma @ 955

Last change on this file since 955 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
RevLine 
[751]1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4
[880]5(* TODO: consider making the typing stricter. *)
[751]6
[880]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'
[881]12| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
[880]13| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
14| Ecost : ∀t. costlabel → expr t → expr t.
15
[751]16inductive stmt : Type[0] ≝
17| St_skip : stmt
[880]18| St_assign : ∀t. ident → expr t → stmt
[881]19| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
[816]20(* ident for returned value, expression to identify fn, args. *)
[880]21| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
22| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
[751]23| St_seq : stmt → stmt → stmt
[880]24| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
[751]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 *)
[880]29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
30| St_return : option (Σt. expr t) → stmt
[751]31| St_label : ident → stmt → stmt
32| St_goto : ident → stmt
33| St_cost : costlabel → stmt → stmt.
34
35record internal_function : Type[0] ≝
[886]36{ f_return    : option typ
37; f_params    : list (ident × typ)
38; f_vars      : list (ident × typ)
[751]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.