source: Deliverables/D3.3/Cminor-experiment/syntax.ma @ 796

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

Update experimental version of Cminor semantics.

File size: 1.8 KB
Line 
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 Fin : nat → Type[0] ≝
15| FO : ∀n. Fin (S n)
16| FS : ∀n. Fin n → Fin (S n).
17
18inductive stmt : ∀blockdepth:nat. Type[0] ≝
19| St_skip : ∀n. stmt n
20| St_assign : ident → expr → ∀n. stmt n
21| St_store : memory_chunk → expr → expr → ∀n. stmt n
22(* ident for returned value, expression to identify fn, args, signature. *)
23| St_call : option ident → expr → list expr → signature → ∀n. stmt n
24| St_tailcall : expr → list expr → signature → ∀n. stmt n
25| St_seq : ∀n. stmt n → stmt n → stmt n
26| St_ifthenelse : expr → ∀n. stmt n → stmt n → stmt n
27| St_loop : ∀n. stmt n → stmt n
28| St_block : ∀n. stmt (S n) → stmt n
29| St_exit : ∀n. Fin n → stmt n
30(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
31| St_switch : expr → ∀n. list (int × (Fin n)) → Fin n → stmt n
32| St_return : option expr → ∀n. stmt n
33| St_label : ident → ∀n. stmt n → stmt n
34| St_goto : ident → ∀n. stmt n
35| St_cost : costlabel → ∀n. stmt n → stmt n.
36
37record internal_function : Type[0] ≝
38{ f_sig       : signature
39; f_params    : list ident
40; f_vars      : list ident
41; f_ptrs      : list ident
42; f_stacksize : nat
43; f_body      : stmt O
44}.
45(* XXX: matita interpretations bug workaround *)
46definition f_stacksize : internal_function → nat ≝
47λf.match f with [ mk_internal_function _ _ _ _ s _ ⇒ s ].
48
49definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracBrowser for help on using the repository browser.