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
}.

(* We define two closely related versions of Cminor, the first with the original
   initialisation data for global variables, and the second where the code is
   responsible for initialisation and we only give the size of each variable. *)

definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).

definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.