(* PREAMBLE *)

From compcert.cfrontend Require Csyntax Csem.
From compcert.lib Require Coqlib.

From trancert.analysis Require Function.
From trancert.lib Require List.

Import lib.All Csyntax Csem List Coqlib common.AST cfrontend.Ctypes analysis.Function Decidability.

Local Notation program := Csyntax.program.
Local Notation type := Ctypes.type.
Local Notation ident := AST.ident.
Local Notation fundef := Csyntax.fundef.
Local Notation globvar := (AST.globvar type).
Local Notation gdef := (AST.globdef (Ctypes.fundef function) type ).
Local Notation Internal := Ctypes.Internal.

(** *Properties of [program] *)

(** Conversion between [Ctypes.prog_defs] and [AST.prog_defs]. *)
Lemma ctypes_to_ast_prog_defs:
  forall (p:program), Ctypes.prog_defs p = AST.prog_defs (Ctypes.program_of_program p).
Proof. intros []; auto. Defined.


(** * Well-formedness of AST*)

(** CompCert has an unverified parser which is not formalized in Coq.
    The type of AST yielded by the parser allows for construction of such trees that
    are never produced by the parser (but might occur as a result of reductions). In
    this file we formalize the constraints on the AST that we require in our proofs
    and provide computable functions to verify them; this way we can validate the
    AST before doing refactoring and fail if the constraints are not satisfied.
 *)



Section DistinctIdentifiers.

  (** **Distinct Identifiers *)

  (** In [program], all identifiers are distinct. This is not enforced by construction, but parser works this way. *)

  (** In our proofs we rely on this fact, so as a part of code transformation we
      will validate this property and fail if it does not hold. *)
  Definition program_idents_wf (p:Csyntax.program) : Prop :=
    list_norepet (List.map fst (Ctypes.prog_defs p)) .

  Theorem program_idents_wf_dec (p: Csyntax.program) :
    { program_idents_wf p } +  { ~ program_idents_wf p }.
  Proof.
    apply list_norepet_dec. apply peq.
  Defined.

End DistinctIdentifiers.


Section ProgramWF.

  (** * Program well-formedness *)

  (** In this section we collect everything we know about parser output. *)

  Inductive globdef_wf : globdef (Csyntax.fundef) type -> Prop :=
  | gdwf_var:
      forall v, globdef_wf  (Gvar v)

  | gdwf_fundef :
      forall f, fundef_wf f -> globdef_wf (Gfun f)
  .

  Theorem globdef_wf_dec :
    forall g, dec (globdef_wf g).
  Proof.
    destruct g; try solve [repeat constructor].
    destruct (fundef_wf_dec f).
    {
      repeat constructor; assumption.
    }
    {
      constructor 2. contradict n. inversion n. assumption.
    }
  Defined.

  Record program_wf (p:Csyntax.program) : Prop :=
    {
    pwf_idents: program_idents_wf p ;
    pwf_defs:   Forall (skip1 globdef_wf) (Ctypes.prog_defs p)
    } .


  Theorem program_wf_dec :
    forall p, dec (program_wf p).
  Proof.
    assert (H:forall e : ident * globdef Csyntax.fundef type, dec (skip1 globdef_wf e)).
    {
      clear.
      intros e.
      destruct e.
      simpl in *.
      destruct (globdef_wf_dec g).
      {
        constructor 1.
        assumption.
      }
      {
        constructor 2.
        contradict n. assumption.
      }
    }

    intros p.
    destruct (program_idents_wf_dec p), p;
      destruct (Forall_decidability (skip1 globdef_wf) H prog_defs);
      try solve [constructor 1; constructor; auto
                |
                constructor 2; contradict n; inv n; auto
                ].
  Defined.

(** ** Identifiers in a well-formed program *)

  Import Globalenvs.Genv.

Definition def_id (p: program) (def: AST.globdef _ _) (id:AST.ident): Prop :=
  In (id, def) (Ctypes.prog_defs p).

Definition fundef_id (p: program) (f: fundef) (id:AST.ident): Prop :=
  def_id p (AST.Gfun f) id.

Definition fun_id (p: Csyntax.program) (f: function) (id:AST.ident): Prop :=
  fundef_id p (Ctypes.Internal f) id.

Definition genv_def_id (ge:genv) def (id: AST.ident): Prop :=
  exists b, (genv_defs ge) ! b = Some def /\ (genv_symb ge) ! id = Some b.


Definition genv_fundef_id (ge:genv) (f: fundef) (id: AST.ident): Prop :=
  genv_def_id ge (AST.Gfun f) id.

Theorem fundef_id_inj :
  forall f1 f2 p i,
    program_wf p ->
    fundef_id p f1 i ->
    fundef_id p f2 i -> f1 = f2.
Proof.
  unfold fundef_id, def_id; intros.
  inv H.
  unfold program_idents_wf in *.
  eapply in_norepet_unique2 in H0; eauto.
  decomp.
  rewrite -> H in *.
  apply in_app in H1.
  decomp.
  - apply (in_map fst) in H1. contradiction.
  - destruct H1; last by  apply (in_map fst) in H1.
      by inv H1.
Qed.

Theorem fun_id_inj :
  forall f1 f2 p i,
    program_wf p ->
    fun_id p f1 i ->
    fun_id p f2 i -> f1 = f2.
Proof.
  move => ? ? ? ? Hwf H1 H2.
  by move: (fundef_id_inj _ _ _ _ Hwf H1 H2); inversion 1.
Qed.

Section Genv.
  Import Globalenvs.Genv.

  Theorem prog_def_id_genv:
    forall (p:Csyntax.program),
      list_norepet (AST.prog_defs_names (Ctypes.program_of_program p)) ->
      forall def id, (def_id p def id <-> genv_def_id (Csem.globalenv p) def id).
  Proof.
    split; unfold fundef_id, def_id, genv_fundef_id, genv_def_id.
    {
      move: ctypes_to_ast_prog_defs -> =>
      /AST.prog_defmap_norepet /Globalenvs.Genv.find_def_symbol.
      unfold find_symbol, find_def.
      intros (b & Hsym & Hdef) =>//.
      change (Csyntax.fundef) with (Ctypes.fundef function) in *.
      eauto.
    }
    {
      intros (b & Hsym & Hdef) =>//.
      change (Csyntax.fundef) with (Ctypes.fundef function) in *.
      simpl in *.
      move: ctypes_to_ast_prog_defs -> .
      eapply AST.in_prog_defmap.
      apply find_def_symbol; eauto.
    }
  Qed.

  Theorem prog_fundef_id_genv:
    forall (p:Csyntax.program),
      list_norepet (AST.prog_defs_names (Ctypes.program_of_program p)) ->
      (forall f id, fundef_id p f id <-> genv_fundef_id (Csem.globalenv p) f id).
  Proof.
    split; by apply prog_def_id_genv.
  Qed.

  Lemma fundef_id_exists:
    forall (p:program) fd vf,
      program_wf p ->
      let ge := Csem.globalenv p in
      (forall b def, (genv_defs ge) ! b = Some def -> exists i : positive, (genv_symb ge) ! i = Some b) ->
      find_funct ge vf = Some fd -> exists fdfid, fundef_id p fd fdfid.
  Proof.
    intros. 
    assert (exists fdfid, genv_fundef_id (Csem.globalenv p) fd fdfid) as (fdfid & Hfdfid).
    {
      unfold find_funct, find_funct_ptr, find_symbol, find_def, genv_fundef_id, genv_def_id in *.
      intros.
      repeat option_cases.
      subst.
      autoinj.
      edestruct H0 as (i & Hsymb); eauto.
    }
    exists fdfid.
    apply prog_fundef_id_genv; auto.
    by inv H.
  Qed.

End Genv.
End ProgramWF.



(* Section DistinctFunctions. *)

(*   (** * Distinct global identifiers *) *)

(*   (** This is not a well-formed-ness condition, but a condition required to *)
(*   conduct some proofs. If functions are not distinct we can not differentiate *)
(*   between them once their identifiers are lost -- e.g. in continuations. *) *)

(*   Definition distinct_functions (p: program) : Prop := *)
(*     forall (i j:ident) f, *)
(*       In (i, Gfun f) (prog_defs p) -> *)
(*       In (j, Gfun f) (prog_defs p) -> *)
(*       i = j . *)

(*   (** *)
(*      Suppose [program_idents_wf p] holds. Let us construct an initial global *)
(*      environment [ge] from it. If [genv_defs ge] holds a definition by an *)
(*      address [b], then there exists a symbol [id] that is mapped to this *)
(*      address. *)
(*   *) *)

  Import Globalenvs Genv.
  Import compcert.lib.Maps Maps.PTree common.Values.

  Theorem symb_exists:
    forall (b:block) (p:program) def,
      let ge := Genv.globalenv p in

      program_idents_wf p ->

      (genv_defs ge) ! b = Some def ->
      exists id, (genv_symb ge) ! id = Some b.
  Proof.
    unfold globalenv,program_idents_wf.
    intros b [] def Hidents Hget =>//=.
    pose (P := fun ge => get b (genv_defs ge) = Some def -> exists id, get id (genv_symb ge) = Some b).
    assert (REC: forall l ge,
               list_norepet (List.map fst l) ->
               (forall i, In i (List.map fst l) -> get i (genv_symb ge) = None) ->
               P ge ->
               P (add_globals ge l)).
    {
      elim =>//=. 
      intros [] l IHl ge. inversion 1 => Hcond HP Hdef.
      apply IHl; auto.
      - move => i Hget'  //=.
        move: gsspec ->; simpl in *; subst.
        erewrite Hcond; eauto.
        destruct (peq _ _); [subst; contradiction| auto].
      - red. red in HP.
        simpl in *.
        move: gsspec =>->.
        destruct (peq _ _).
        + inversion 1. subst.
          exists p. apply gss.
        + move => /HP. intros [id Hid].
          exists id. rewrite gsspec.
          destruct (peq _ _ ); auto.
          subst.
          erewrite Hcond in Hid; [discriminate| eauto 2].
    }
    apply REC; eauto.
    - by intros; apply gempty.
    - by red; rewrite gempty.
  Qed.

  Lemma wf_globalenv_ident:
    forall p id g,
      program_idents_wf p ->
      In (id, g) (prog_defs p) ->
      exists b, find_symbol (globalenv p) id = Some b /\ find_def (globalenv p) b = Some g.
  Proof.
    intros p id g H H0.
    unfold program_idents_wf  in *.
    rewrite ctypes_to_ast_prog_defs in H.
    exploit AST.prog_defmap_norepet; eauto.
    by move / find_def_symbol.
  Qed.

  (* Theorem fundef_id_unique: *)
  (*   forall f i1 i2 p, *)
  (*     program_wf p -> *)
  (*     distinct_functions p -> *)
  (*     fundef_id p f i1 -> fundef_id p f i2 -> i1 = i2. *)
  (* Proof. by intros; eauto. Qed. *)


