Module CtypingC

Require Import String.
Require Import CoqlibC Maps Integers Floats Errors.
Require Import AST Linking.
Require Import Values Memory Globalenvs Events.
Require Import CtypesC Cop Csyntax Csem ValuesC.
Require Import sflib.
newly added *
Require Export Ctyping.
Require Import Skeleton.

Local Open Scope error_monad_scope.

Set Implicit Arguments.

Inductive typify_c (v: val) (ty: type): val -> Prop :=
| typify_c_ok
    (WT: wt_retval v ty):
    typify_c v ty v
| typify_c_no
    (NWT: ~ wt_retval v ty):
    typify_c v ty Vundef.

Lemma typify_c_dtm
      v ty tv0 tv1
      (TY0: typify_c v ty tv0)
      (TY1: typify_c v ty tv1):
    tv0 = tv1.
Proof.
inv TY0; inv TY1; des; ss. Qed.

Lemma typify_c_ex: forall v ty,
  exists tv, <<TYP: typify_c v ty tv>>.
Proof.
  i. destruct (classic (wt_retval v ty)).
  - esplits; econs 1; eauto.
  - esplits; econs 2; eauto.
Qed.

Lemma typify_c_spec
      v ty tv
      (TY: typify_c v ty tv):
    <<WT: wt_retval tv ty>>.
Proof.
  inv TY; des; ss. split.
  - econs.
  - reflexivity.
Qed.

Lemma wt_initial_frame
      (cp: Csyntax.program) fptr vs_arg m
      targs tres cconv
      (ge: genv)
      (INT: exists fd, Genv.find_funct ge fptr = Some (Internal fd))
      (WTLOCALS:
         forall fd, Genv.find_funct ge fptr = Some (Internal fd) ->
         Forall (fun t : type => wt_type ge t) (map snd (fn_params fd ++ fn_vars fd)))
      (WTARGS: Forall2 val_casted vs_arg (typelist_to_listtype targs))
      (NVOID: Forall (fun ty : type => ty <> Tvoid) (typelist_to_listtype targs)):
    wt_state cp ge (Csem.Callstate fptr (Tfunction targs tres cconv) vs_arg Kstop m).
Proof.
  des. econs; et; ss.
  - econs; et.
  - ii. exfalso. eapply EXT; et.
Qed.

Lemma wt_val_has_type
      v ty
      (WT: wt_val v ty)
      (NVOID: ty <> Tvoid):
    <<TY: Val.has_type v ty.(typ_of_type)>>.
Proof.
inv WT; ss. Qed.

Lemma wt_retval_has_type
      v ty
      (WT: wt_retval v ty):
    <<TY: Val.has_type v ty.(typ_of_type)>>.
Proof.
inv WT; ss. inv WTV; ss. erewrite NVOID; ss. Qed.

Lemma typify_inject
      v_src ty tv_src v_tgt j
      (TYP: typify_c v_src ty tv_src)
      (INJ: Val.inject j v_src v_tgt):
    <<INJ: Val.inject j tv_src (typify v_tgt (typ_of_type ty))>>.
Proof.
  inv TYP.
  - exploit wt_retval_has_type; eauto. i; des. unfold typify. des_ifs. inv INJ; ss.
  - ss.
Qed.