source: src/Cminor/syntax.ma @ 751

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

Initial version of the Cminor syntax and semantics.

File size: 1.5 KB
RevLine 
[751]1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4
5inductive expr : Type[0] ≝
6| Id : ident → expr
7| Cst : constant → expr
8| Op1 : unary_operation → expr → expr
9| Op2 : binary_operation → expr → expr → expr
10| Mem : memory_chunk → expr → expr
11| Cond : expr → expr → expr → expr
12| Ecost : costlabel → expr → expr.
13
14inductive stmt : Type[0] ≝
15| St_skip : stmt
16| St_assign : ident → expr → stmt
17| St_store : memory_chunk → expr → expr → stmt
18(* ident for returned value, expression to identify fn, args, signature. *)
19| St_call : option ident → expr → list expr → signature → stmt
20| St_tailcall : expr → list expr → signature → stmt
21| St_seq : stmt → stmt → stmt
22| St_ifthenelse : expr → stmt → stmt → stmt
23| St_loop : stmt → stmt
24| St_block : stmt → stmt
25| St_exit : nat → stmt
26(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
27| St_switch : expr → list (int × nat) → nat → stmt
28| St_return : option expr → stmt
29| St_label : ident → stmt → stmt
30| St_goto : ident → stmt
31| St_cost : costlabel → stmt → stmt.
32
33record internal_function : Type[0] ≝
34{ f_sig       : signature
35; f_params    : list ident
36; f_vars      : list ident
37; f_ptrs      : list ident
38; f_stacksize : nat
39; f_body      : stmt
40}.
41(* XXX: matita interpretations bug workaround *)
42definition f_stacksize : internal_function → nat ≝
43λf.match f with [ mk_internal_function _ _ _ _ s _ ⇒ s ].
44
45definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracBrowser for help on using the repository browser.