source: src/Cminor/Cminor_syntax.ma @ 3041

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. expr ASTptr → 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.

inductive stmt : Type[0] ≝
| St_skip : stmt
| St_assign : ∀t. ident → expr t → stmt
| St_store : ∀t. expr ASTptr → expr t → stmt
(* ident for returned value, expression to identify fn, args. *)
| St_call : option (ident × typ) → expr ASTptr → list (𝚺t. expr t) → stmt
(* We don't use these at the moment, and they're getting in the way.
| St_tailcall : expr ASTptr → list (𝚺t. expr t) → stmt
*)
| St_seq : stmt → stmt → stmt
| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
| St_return : option (𝚺t. expr t) → stmt
| St_label : identifier Label → stmt → stmt
| St_goto : identifier Label → stmt
| St_cost : costlabel → stmt → stmt.

(* Apply a predicate to every statement.  Be careful with grouping so that the
   local application is the first conjunct, and substatements the second. *)

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_label _ s' ⇒ P s ∧ stmt_P P s'
| St_cost _ s' ⇒ P s ∧ stmt_P P s'
| _ ⇒ P s ∧ True
].

lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
#P * normalize * /3 by proj1/
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_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 /6 by proj1, proj2, conj/
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 #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/
| * 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_label l s ⇒ l::(labels_of s)
| St_cost _ s ⇒ labels_of s
| _ ⇒ [ ]
].

inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝
| rettyp_none : rettyp_match (None ?) (None ?)
| rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭).

record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ {
  cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s;
  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s;
  cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe
                               | _ ⇒ True ]
}.

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 (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) 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.