include "common/FrontEndOps.ma".
include "common/CostLabel.ma".

inductive expr : Type[0] ≝
| Id : ident → expr
| Cst : constant → expr
| Op1 : unary_operation → expr → expr
| Op2 : binary_operation → expr → expr → expr
| Mem : memory_chunk → expr → expr
| Cond : expr → expr → expr → expr
| Ecost : costlabel → expr → expr.

inductive stmt : Type[0] ≝
| St_skip : stmt
| St_assign : ident → expr → stmt
| St_store : memory_chunk → expr → expr → stmt
(* ident for returned value, expression to identify fn, args, signature. *)
| St_call : option ident → expr → list expr → signature → stmt
| St_tailcall : expr → list expr → signature → stmt
| St_seq : stmt → stmt → stmt
| St_ifthenelse : expr → stmt → stmt → stmt
| St_loop : stmt → stmt
| St_block : stmt → stmt
| St_exit : nat → stmt
(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
| St_switch : expr → list (int × nat) → nat → stmt
| St_return : option expr → stmt
| St_label : ident → stmt → stmt
| St_goto : ident → stmt
| St_cost : costlabel → stmt → stmt.

record internal_function : Type[0] ≝
{ f_sig       : signature
; f_params    : list ident
; f_vars      : list ident
; f_ptrs      : list ident
; f_stacksize : nat
; f_body      : stmt
}.
(* XXX: matita interpretations bug workaround *)
definition f_stacksize : internal_function → nat ≝
λf.match f with [ mk_internal_function _ _ _ _ s _ ⇒ s ].

definition Cminor_program ≝ program (fundef internal_function) unit.