Module ASTC

copied && added "C" *
Require Import String.
Require Import CoqlibC Maps Errors Integers Floats.
Require Archi.

newly added *
Require Export AST.
Require Import Errors.
Require Import sflib.

Set Implicit Arguments.

Generalizable Variables F.

Lemma prog_defmap_spec
      F V (p: program F V) id:
    In id p.(prog_defs_names) <-> exists g, p.(prog_defmap) ! id = Some g.
Proof.
  split; ii.
  - exploit prog_defmap_dom; eauto.
  - des. exploit in_prog_defmap; eauto. i.
    clear - H0. destruct p; ss. u. apply in_map_iff. esplits; eauto. ss.
Qed.

Lemma prog_defmap_image
      F V (p : AST.program F V) id g
      (GET: (prog_defmap p) ! id = Some g):
    <<IN: In id (prog_defs_names p)>>.
Proof.
eapply prog_defmap_spec; et. Qed.


Lemma prog_defmap_update_snd
      X Y (f: X -> Y) (defs: list (positive * X)) id:
    (PTree_Properties.of_list (map (update_snd f) defs)) ! id =
    option_map f ((PTree_Properties.of_list defs) ! id).
Proof.
  unfold PTree_Properties.of_list.
  rewrite <- ! fold_left_rev_right in *. rewrite <- map_rev. unfold PTree.elt.
  abstr (rev defs) xs. clear_tac. generalize id.
  induction xs; ii; try rewrite PTree.gempty in *; ss.
  { unfold option_map. rewrite PTree.gempty in *; ss. }
  destruct a; ss.
  rewrite PTree.gsspec. des_ifs.
  { unfold option_map. rewrite PTree.gsspec. des_ifs. }
  rewrite IHxs. rewrite PTree.gsspec. des_ifs.
Qed.

Class HasExternal (X: Type): Type := {
  is_external: X -> bool;
}.




Section FUNCTIONS.

  Definition is_external_fd F (f: fundef F): bool :=
    match f with
    | External ef => is_external_ef ef
    | _ => false
    end.

  Lemma transf_fundef_is_external
        A B (transf: A -> B) f
        (ISEXT: is_external_fd (transf_fundef transf f)):
      <<ISEXT: is_external_fd f>>.
Proof.
compute in ISEXT. des_ifs. Qed.

  Lemma transf_fundef_external
        A B (transf: A -> B) f ef
        (EXT: (transf_fundef transf f) = External ef):
      f = External ef.
Proof.
compute in EXT. des_ifs. Qed.

  Lemma transf_partial_fundef_is_external_fd
        A B (transf_partial: A -> res B) f tf
        (TRANSF: (transf_partial_fundef transf_partial f) = OK tf)
        (ISEXT: is_external_fd tf):
      <<ISEXT: is_external_fd f>>.
Proof.
compute in ISEXT. des_ifs. compute in TRANSF. des_ifs. Qed.

  Lemma transf_partial_fundef_external
        A B (transf_partial: A -> res B) f ef
        (TRANSF: (transf_partial_fundef transf_partial f) = OK (External ef)):
      <<ISEXT: f = External ef>>.
Proof.
compute in TRANSF. des_ifs. Qed.

  Definition is_dtm_ef (ef: external_function): bool :=
    match ef with
    | EF_external _ _
    | EF_builtin _ _
    | EF_runtime _ _
    | EF_inline_asm _ _ _ => false
    | _ => true
    end.

  Definition is_dtm_fd F (fd: AST.fundef F): bool :=
    match fd with
    | External ef => is_dtm_ef ef
    | _ => true
    end.

End FUNCTIONS.

Definition is_external_gd `{HasExternal F} V (gd: globdef F V): bool :=
  match gd with
  | Gfun fd => is_external fd
  | Gvar _ => false
  end.

Arguments is_external_fd {F}.
Arguments is_external_gd {_} {_} {V}.
Hint Unfold is_external_gd is_external_fd.

Global Instance external_function_HasExternal: HasExternal external_function :=
  Build_HasExternal is_external_ef.
Global Instance fundef_HasExternal {F}: HasExternal (AST.fundef F) :=
  Build_HasExternal is_external_fd.
Global Instance globdef_HasExternal `{HasExternal F} {V}: HasExternal (globdef F V) :=
  Build_HasExternal is_external_gd.









Section PROGRAMS.

  Variable F V: Type.
  Variable p: program F V.

  Definition good_prog (p: program F V): Prop :=
    incl p.(prog_public) p.(prog_defs_names).

  Definition defs: ident -> bool := fun id => In_dec ident_eq id p.(prog_defs_names).
  Check (defs: ident -> Prop).
  Definition defs_old: ident -> Prop := fun id => exists gd, p.(prog_defmap)!id = Some gd.
  Goal defs <1= defs_old.
Proof.
    ii. exploit prog_defmap_dom; eauto. inv PR.
    unfold defs in *. des_sumbool; ss.
  Qed.

  Definition privs: ident -> bool :=
    fun id => andb (<<DEFS: defs id>>) (<<PRIVS: negb (In_dec ident_eq id p.(prog_public))>>).
  Definition privs_old: ident -> Prop :=
    <<DEFS: defs_old>> /1\ <<PRIVS: (fun id => ~ In id p.(prog_public))>>.

  Lemma privs_defs_old: <<LE: (privs_old <1= defs_old)>>.
Proof.
ii. inv PR. eauto. Qed.

End PROGRAMS.

Lemma defs_prog_defmap
      F V (prog: AST.program F V):
    forall id, (exists gd, (prog_defmap prog) ! id = Some gd) <-> defs prog id.
Proof.
  ii. etrans.
  { symmetry. eapply prog_defmap_spec. }
  unfold defs, prog_defs_names. split; i; des; des_sumbool; ss.
Qed.




Section PROGRAMS2.

  Context `{HasExternal F} {V: Type}.
  Variable p: program F V.

  Definition internals: ident -> bool :=
    fun id => match p.(prog_defmap)!id with
              | Some gd => negb (is_external gd)
              | None => false
              end.

  Definition internals': ident -> bool :=
    fun id => is_some
                (List.find (fun idg => andb (ident_eq id idg.(fst)) (is_external idg.(snd))) p.(prog_defs)).

End PROGRAMS2.

Hint Unfold defs privs internals.
Hint Unfold defs_old privs_old internals'.

Lemma internals_defs
      `{HasExternal F} V
      (p: AST.program F V):
    p.(internals) <1= p.(defs).
Proof.
  u. ii. des_sumbool. eapply prog_defmap_spec. des_ifs; et.
Qed.


Lemma chunk_type_chunk: forall ty,
    (type_of_chunk (chunk_of_type ty)) = ty.
Proof.
destruct ty; ss. Qed.