include "Clight/toCminor.ma".
include "Clight/Cexec.ma".
include "Clight/abstract.ma".
include "Cminor/abstract.ma".
include "Clight/frontend_misc.ma".
include "Clight/memoryInjections.ma".


lemma translate_notbool_to_cminor :
  ∀t,sg,arg.
  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
*
[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
| #structname #fieldspec | #unionname #fieldspec | #id ]
normalize in match (typ_of_type ?);
#sg #arg #cmop
whd in ⊢ (??%% → ?); #Heq destruct (Heq)
cases arg
[ | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp ]
#res
whd in ⊢ ((??%?) → ?);
#Heq
[ 6,11,12: | *: destruct (Heq) ]
[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
     #H normalize nodelta #Heq destruct
     whd in match (eval_unop ????);
     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
] qed.

lemma translate_notint_to_cminor :
  ∀t,t',arg.
  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
  ∀res. sem_unary_operation Onotint arg t = Some ? res →
        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
#ty *
[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
#sz #sg #arg #cmop
whd in match (translate_unop ???);
@(match typ_eq (ASTint sz sg) (typ_of_type ty)
  with
  [ inl H ⇒ ?
  | inr H ⇒ ? ])
normalize nodelta
[ 2: #Heq destruct ]
lapply H -H
lapply cmop -cmop
cases ty
[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
| #structname #fieldspec | #unionname #fieldspec | #id ]
normalize nodelta
#cmop normalize in match (typ_of_type ?); #H destruct
#H' normalize in H';
destruct (H')
#res
whd in match (sem_unary_operation ???);
cases arg
[ | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp ]
whd in match (sem_notint ?);
#H destruct (H) @refl
qed.


lemma translate_negint_to_cminor :
  ∀t,t',arg.
  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
  ∀res. sem_unary_operation Oneg arg t = Some ? res →
        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
#ty *
[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
#sz #sg #arg #cmop
whd in match (translate_unop ???);
@(match typ_eq (ASTint sz sg) (typ_of_type ty)
  with
  [ inl H ⇒ ?
  | inr H ⇒ ? ])
normalize nodelta
[ 2: #Heq destruct ]
lapply H -H
lapply cmop -cmop
cases ty
[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
| #structname #fieldspec | #unionname #fieldspec | #id ]
normalize nodelta
#cmop normalize in match (typ_of_type ?); #H destruct
#H' normalize in H';
destruct (H')
#res
whd in match (sem_unary_operation ???);
cases arg
[ | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp
| | #vsz #vi | | #vp ]
whd in match (sem_neg ??);
#H destruct (H)
whd in match (eval_unop ????);
cases (eq_intsize sz' vsz) in H; normalize nodelta
#H destruct @refl
qed.


lemma translate_unop :
  ∀ty,sg,op,cmop.
  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
#ty #sg * #cmop #Htranslate #arg
[ @translate_notbool_to_cminor assumption
| @translate_notint_to_cminor assumption
| @translate_negint_to_cminor assumption ]
qed.


lemma classify_add_inversion :
  ∀ty1,ty2. 
    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
    (classify_add ty1 ty2 = add_default ty1 ty2).
#ty1 #ty2
cases (classify_add ty1 ty2)
[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
| #tya #tyb %2 @refl ]
qed.

lemma classify_sub_inversion :
  ∀ty1,ty2.
    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_ii sz sg) ∨
    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_pi n ty' sz sg) ∨
    (∃ty1',ty2',n1,n2. ty1 = ptr_type ty1' n1 ∧ ty2 = ptr_type ty2' n2 ∧ classify_sub ty1 ty2 ≃ sub_case_pp n1 n2 ty1' ty2') ∨
    (classify_sub ty1 ty2 = sub_default ty1 ty2).
#ty1 #ty2
cases (classify_sub ty1 ty2)
[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
| #n1 #n2 #t1 #t2 %1 %2 %{t1} %{t2} %{n1} %{n2} @conj try @conj try @refl @refl_jmeq
| #tya #tyb %2 @refl ]
qed.

lemma classify_aop_inversion :
  ∀ty1,ty2. 
    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
    classify_aop ty1 ty2 = aop_default ty1 ty2.
#ty1 #ty2
cases (classify_aop ty1 ty2)
[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
| #ty #ty' %2 @refl ]
qed.


lemma complete_cmp_inversion : 
  ∀ty:type.
  ∀e:expr (ASTint I8 Unsigned).
  ∀r:expr (typ_of_type ty).
   complete_cmp ty e = return r → 
   ∃sz,sg. ty = Tint sz sg ∧ 
           r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
*
[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
| #structname #fieldspec | #unionname #fieldspec | #id ]
#e whd in match (typ_of_type ?);
#r whd in ⊢ ((??%%) → ?);
#H destruct
%{sz} %{sg} @conj try @refl @refl_jmeq
qed.


lemma pointer_translation_eq_block :
  ∀E,p1,p2,p1',p2'.
  pointer_translation p1 E = Some ? p1' →
  pointer_translation p2 E = Some ? p2' →
  eq_block (pblock p1) (pblock p2) = true → 
  eq_block (pblock p1') (pblock p2') = true.
#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
#H1 #H2 #Heq_block
lapply (eq_block_to_refl … Heq_block) #H destruct (H)
lapply H1 lapply H2 -H1 -H2
whd in ⊢ ((??%?) → (??%?) → ?);
cases (E b2) normalize nodelta
[ #Habsurd destruct ]
* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
@eq_block_b_b
qed.