include "common/FrontEndOps.ma".
include "common/CostLabel.ma".
include "basics/lists/list.ma".

inductive expr : typ → Type[0] ≝
| Id : ∀t. ident → expr t
| Cst : ∀t. constant t → expr t
| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
| Mem : ∀t,r. 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.

(* Assert a predicate on every variable or parameter identifier. *)
let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
match e with
[ Id t i ⇒ P i t
| Cst _ _ ⇒ True
| Op1 _ _ _ e ⇒ expr_vars ? e P
| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
| Mem _ _ e ⇒ expr_vars ? e P
| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
| Ecost _ _ e ⇒ expr_vars ? e P
].

lemma expr_vars_mp : ∀t,e,P,Q.
  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
#t0 #e elim e normalize /3/ 
[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
  % /3/
| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
] qed.

axiom Label : String.

inductive stmt : Type[0] ≝
| St_skip : stmt
| St_assign : ∀t. ident → expr t → stmt
| St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
(* ident for returned value, expression to identify fn, args. *)
| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
(* We don't use these at the moment, and they're getting in the way.
| 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 : identifier Label → stmt → stmt
| St_goto : identifier Label → stmt
| St_cost : costlabel → stmt → stmt.

let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
match s with
[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
| St_loop s' ⇒ P s ∧ stmt_P P s'
| St_block s' ⇒ P s ∧ stmt_P P s'
| St_label _ s' ⇒ P s ∧ stmt_P P s'
| St_cost _ s' ⇒ P s ∧ stmt_P P s'
| _ ⇒ P s
].

lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
#P * normalize /2/
[ #s1 #s2 * * /2/
| #sz #sg #e #s1 #s2 * * /2/ 
| 3,4: #s * /2/
| 5,6: #i #s normalize * /2/
] qed.

(* Assert a predicate on every variable or parameter identifier. *)
definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
λP,s.
match s with
[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
| St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
(*
| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
*)
| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
| St_switch _ _ e _ _ ⇒ expr_vars ? e P
| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
| _ ⇒ True
].

definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
λP,s.
match s with
[ St_label l _ ⇒ P l
| St_goto l ⇒ P l
| _ ⇒ True
].

lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
#P #Q #H #s elim s /2/
[ #s1 #s2 #H1 #H2 normalize * * /4/
| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
| #s #H * /5/
| #s #H * /5/
| #l #s #H * /5/
| #l #s #H * /5/
] qed.

lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
#P #Q #H #s elim s normalize
[ //
| #t #id #e * /4/
| #t #r #e1 #e2 * /4/
| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] 
(*
| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
*)
| #s1 #s2 #H1 #H2 * /3/
| #sz #sg #e #s1 #s2 #H1 #H2 /5/
| 7,8: #s #H1 #H2 /2/
| //
| /5/
| * normalize [ // | *; normalize /3/ ]
| /2/
| //
| /2/
] qed.

lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
#P #Q #H #s elim s normalize /2/ qed.

(* Get labels from a Cminor statement. *)
let rec labels_of (s:stmt) : list (identifier Label) ≝
match s with
[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
| St_loop s ⇒ labels_of s
| St_block s ⇒ labels_of s
| St_label l s ⇒ l::(labels_of s)
| St_cost _ s ⇒ labels_of s
| _ ⇒ [ ]
].

record internal_function : Type[0] ≝
{ f_return    : option typ
; f_params    : list (ident × typ)
; f_vars      : list (ident × typ)
; f_distinct  : distinct_env … (f_params @ f_vars)
; f_stacksize : nat
; f_body      : stmt
     (* Ensure that variables appear in the params and vars list with the
        correct typ; and that all goto labels used are declared. *)
; f_inv       : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧
                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
}.

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