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 Fin : nat → Type[0] ≝
| FO : ∀n. Fin (S n)
| FS : ∀n. Fin n → Fin (S n).

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

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 O
}.
(* 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.