Module CopC

Require Import CoqlibC.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Ctypes.
Require Archi.
newly added *
Require Export Cop.
Require Import sflib.
Require Conventions1.


Inductive typecheck (vs: list val) (tys: typelist): Prop :=
| typecheck_intro
    (TYP: Forall2 (val_casted) vs (typelist_to_listtype tys))
    (NVOID: Forall (fun ty => ty <> Tvoid) (typelist_to_listtype tys))
    (SZ: 4 * Conventions1.size_arguments_64 (typlist_of_typelist tys) 0 0 0 <= Ptrofs.max_unsigned).

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

Lemma val_casted_has_type_list
      vs tys
      (WT: Forall2 val_casted vs (typelist_to_listtype tys))
      (NVOID: Forall (fun ty => ty <> Tvoid) (typelist_to_listtype tys)):
    Val.has_type_list vs (typlist_of_typelist tys).
Proof.
  ginduction vs; destruct tys; ii; ss; inv WT; inv NVOID; ii; ss.
  esplits; eauto.
  eapply val_casted_has_type; eauto.
Qed.

Lemma typlist_of_typelist_eq: forall itys,
    typlist_of_typelist (type_of_params itys) = (map typ_of_type (map snd itys)).
Proof.
i. ginduction itys; ii; ss; des_ifs; ss. f_equal. ss. Qed.

Lemma typelist_to_listtype_length: forall itys,
    length (typelist_to_listtype (type_of_params itys)) = length (map typ_of_type (map snd itys)).
Proof.
i. ginduction itys; ii; ss; des_ifs; ss. xomega. Qed.