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

(* TODO: consider making the typing stricter. *)

inductive expr : typ → Type[0] ≝
| Id : ∀t. ident → expr t
| Cst : ∀t. constant → expr t
| Op1 : ∀t,t'. unary_operation → expr t → expr t'
| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
| Ecost : ∀t. costlabel → expr t → expr t.

inductive stmt : Type[0] ≝
| St_skip : stmt
| St_assign : ∀t. ident → expr t → stmt
| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
(* ident for returned value, expression to identify fn, args. *)
| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
| St_seq : stmt → stmt → stmt
| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → 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 : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
| St_return : option (Σt. expr t) → stmt
| St_label : ident → stmt → stmt
| St_goto : ident → stmt
| St_cost : costlabel → stmt → stmt.

record internal_function : Type[0] ≝
{ f_return    : option typ
; f_params    : list (ident × typ)
; f_vars      : list (ident × typ)
; f_stacksize : nat
; f_body      : stmt
}.

definition Cminor_program ≝ program (fundef internal_function) unit.