text:
Require Import HoTT.
Require Import heterogeneous_equality.

(** The type of paths over path defined as an inductive type.
    The goal is to represent paths in dependent families.
 *)
Inductive path_over {A : Type} (C : A -> Type)
  : forall {a₁ a₂ : A} (p : a₁ = a₂) (c₁ : C a₁) (c₂ : C a₂), Type
  := path_over_id : forall {a : A} (c : C a), path_over C idpath c c.

Arguments path_over_id {A C a} c.

(** Alternatively, we can define it using path induction. *)
Definition path_over_pi
           {A : Type} (C : A -> Type)
           {a₁ a₂ : A} (p : a₁ = a₂)
  : forall (c₁ : C a₁) (c₂ : C a₂), Type
  := match p with
     | idpath => fun c₁ c₂ => c₁ = c₂
     end.

Section equivalences.
  (** Paths in dependent families are equivalent to heterogeneous equalities. *)
  Definition path_over_to_heq
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : path_over C p c₁ c₂)
    : heq (ap C p) c₁ c₂
    := match q with
       | path_over_id _ _ => heq_refl _
       end.

  Definition heq_to_path_over
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : heq (ap C p) c₁ c₂)
    : path_over C p c₁ c₂.
  Proof.
    induction p ; cbn in *.
    exact (transport (path_over C idpath c₁) (heq_to_heq_pi q) (path_over_id _)).
  Defined.

  Global Instance path_over_to_heq_isequiv
         {A : Type} {C : A -> Type}
         {a₁ a₂ : A} {p : a₁ = a₂}
         {c₁ : C a₁} {c₂ : C a₂}
    : IsEquiv (@path_over_to_heq A C a₁ a₂ p c₁ c₂).
  Proof.
    simple refine (isequiv_adjointify _ (@heq_to_path_over A C a₁ a₂ p c₁ c₂) _ _).
    - intros x ; induction p ; cbn in *.
      refine (_ @ eissect heq_to_heq_pi x).
      induction (heq_to_heq_pi x).
      reflexivity.
    - intros x ; induction x.
      reflexivity.
  Defined.

  (** Also, paths in path families are equivalent to paths in both [C a₁]. *)
  Definition path_over_to_path
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : path_over C p c₁ c₂)
    : transport C p c₁ = c₂
    := match q with
       | path_over_id _ _ => idpath
       end.

  Definition path_to_path_over
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : transport C p c₁ = c₂)
    : path_over C p c₁ c₂.
  Proof.
    induction p.
    exact (transport (path_over C idpath c₁) q (path_over_id _)).
  Defined.

  Global Instance path_over_to_path_is_equiv
         {A : Type} {C : A -> Type}
         {a₁ a₂ : A} {p : a₁ = a₂}
         {c₁ : C a₁} {c₂ : C a₂}
    : IsEquiv (@path_over_to_path A C a₁ a₂ p c₁ c₂).
  Proof.
    simple refine (isequiv_adjointify _ (@path_to_path_over A C a₁ a₂ p c₁ c₂) _ _).
    - intros q ; induction p, q ; cbn in *.
      reflexivity.
    - intros x ; induction x.
      reflexivity.
  Defined.

  (** Also, paths in path families are equivalent to paths in both [C a₂]. *)
  Definition path_over_to_path_V
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : path_over C p c₁ c₂)
    : c₁ = transport C p^ c₂
    := match q with
       | path_over_id _ _ => idpath
       end.

  Definition path_V_to_path_over
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : c₁ = transport C p^ c₂)
    : path_over C p c₁ c₂.
  Proof.
    induction p.
    exact (transport (path_over C idpath c₁) q (path_over_id _)).
  Defined.

  Global Instance path_over_to_path_V_is_equiv
         {A : Type} {C : A -> Type}
         {a₁ a₂ : A} {p : a₁ = a₂}
         {c₁ : C a₁} {c₂ : C a₂}
    : IsEquiv (@path_over_to_path_V A C a₁ a₂ p c₁ c₂).
  Proof.
    simple refine (isequiv_adjointify _ (@path_V_to_path_over A C a₁ a₂ p c₁ c₂) _ _).
    - intros q ; induction p ; cbn in * ; induction q.
      reflexivity.
    - intros x ; induction x.
      reflexivity.
  Defined.

  (** The definitions of paths in dependent families using inductive types and path induction, are equivalent. *)
  Definition path_over_to_path_over_pi
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : path_over C p c₁ c₂)
    : path_over_pi C p c₁ c₂
    := match q with
       | path_over_id _ _ => idpath
       end.

  Definition path_over_pi_to_path_over
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C a₁} {c₂ : C a₂}
             (q : path_over_pi C p c₁ c₂)
    : path_over C p c₁ c₂.
  Proof.
    induction p ; cbn in *.
    exact (transport (path_over C 1 c₁) q (path_over_id _)).
  Defined.

  Global Instance path_over_to_path_over_pi_is_equiv
         {A : Type} {C : A -> Type}
         {a₁ a₂ : A} {p : a₁ = a₂}
         {c₁ : C a₁} {c₂ : C a₂}
    : IsEquiv (@path_over_to_path_over_pi A C a₁ a₂ p c₁ c₂).
  Proof.
    simple refine (isequiv_adjointify _ (@path_over_pi_to_path_over A C a₁ a₂ p c₁ c₂) _ _).
    - intros x.
      induction p, x.
      reflexivity.
    - intros x ; induction x.
      reflexivity.
  Defined.
End equivalences.

Section operations.
  (** Dependent maps can be applied to paths.
      This gives a path in a dependent family.
   *)
  Definition apd_po
             {A : Type} {C : A -> Type}
             (f : forall (a : A), C a)
             {a₁ a₂ : A} (p : a₁ = a₂)
    : path_over C p (f a₁) (f a₂)
    := match p with
       | idpath => path_over_id _
       end.

  (** A path in a dependent family gives a path in a sigma type. *)
  Definition path_prod_po
             {A : Type} {C : A -> Type}
             {a₁ a₂ : A} (p : a₁ = a₂)
             {c₁ : C a₁} {c₂ : C a₂}
             (q : path_over C p c₁ c₂)
    : (a₁;c₁) = (a₂;c₂)
    := match q with
       | path_over_id _ _ => idpath
       end.

  (** If we look at a path over the identity path, then it is just a path in a certain fiber. *)
  Definition path_over_single_fiber
             {A : Type} {C : A -> Type}
             {a : A}
             {c₁ : C a} {c₂ : C a}
             (q : path_over C idpath c₁ c₂)
    : c₁ = c₂
    := path_over_to_path q.

  Global Instance path_over_single_fiber_is_equiv
         {A : Type} {C : A -> Type}
         {a : A}
         {c₁ : C a} {c₂ : C a}
    : IsEquiv (@path_over_single_fiber A C a c₁ c₂)
    := _.

  (** If the fiber is constant, then it is just a path in that fiber. *)
  Definition path_over_const
             {A C : Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ c₂ : C}
             (q : path_over (fun _ => C) p c₁ c₂)
    : c₁ = c₂
    := match q with
       | path_over_id _ _ => idpath
       end.

  Definition const_path_over
             {A C : Type}
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ c₂ : C}
             (q : c₁ = c₂)
    : path_over (fun _ => C) p c₁ c₂
    := match p, q with
       | idpath, idpath => path_over_id _
       end.

  Global Instance path_over_const_isequiv
         {A C : Type}
         {a₁ a₂ : A} {p : a₁ = a₂}
         {c₁ c₂ : C}
    : IsEquiv (@path_over_const A C a₁ a₂ p c₁ c₂).
  Proof.
    simple refine (isequiv_adjointify _ (@const_path_over A C a₁ a₂ p c₁ c₂) _ _).
    - intros q ; induction p, q.
      reflexivity.
    - intros q ; induction q.
      reflexivity.
  Defined.

  (** Composing the fibration with a map [f] gives a path over [ap f p]. *)
  Definition path_over_compose
             {A B : Type} {C : B -> Type} (f : A -> B)
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C (f a₁)} {c₂ : C (f a₂)}
             (q : path_over (C o f) p c₁ c₂)
    : path_over C (ap f p) c₁ c₂
    := match q with
       | path_over_id _ _ => path_over_id _
       end.

  Definition compose_path_over
             {A B : Type} {C : B -> Type} (f : A -> B)
             {a₁ a₂ : A} {p : a₁ = a₂}
             {c₁ : C (f a₁)} {c₂ : C (f a₂)}
             (q : path_over C (ap f p) c₁ c₂)
    : path_over (C o f) p c₁ c₂.
  Proof.
    induction p ; cbn in *.
    exact (transport (path_over _ idpath c₁) (path_over_to_path q) (path_over_id c₁)).
  Defined.

  Global Instance path_over_compose_isequiv
         {A B : Type} {C : B -> Type} (f : A -> B)
         {a₁ a₂ : A} {p : a₁ = a₂}
         {c₁ : C (f a₁)} {c₂ : C (f a₂)}
    : IsEquiv (@path_over_compose A B C f a₁ a₂ p c₁ c₂).
  Proof.
    simple refine (isequiv_adjointify _ (@compose_path_over A B C f a₁ a₂ p c₁ c₂) _ _).
    - intros x ; induction p ; cbn in *.
      refine (_ @ eissect path_over_to_path x).
      induction (path_over_to_path x).
      reflexivity.
    - intros q ; induction q.
      reflexivity.
  Defined.
End operations.

author: nmvdw

repo: Three-HITs

save_path: github-repos/coq/nmvdw-Three-HITs


text:
From Undecidability.L Require Export LTactics LTerm Functions.Encoding Tactics.Lbeta_nonrefl.
Import L_Notations.

(* * First Fixed Point Theorem *)

Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t == t.
Proof.
  intros cls_s.
  pose (A := lam (s (#0 #0))).
  pose (t := A A).
  exists t. split;[subst t A;Lproc|].
  symmetry. cbv. now redStep.
Qed.

(* * Second Fixed Point Theorem *)

Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (enc t) == t.
Proof.
  intros cls_s.
  pose (A := lam(s ((ext app) #0 ((ext term_enc) #0)))).
  pose (t := A (ext A)).
  exists t. split;[subst t A;Lproc|].
  symmetry. change (enc t) with (ext t).
  unfold t. unfold A at 1.
  redSteps. now Lsimpl.
Qed.

Goal exists t, closed t /\ t == (enc t).
Proof.
  destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]]. Lproc.
  exists t.
  split. Lproc. rewrite <- A at 1. clear A. unfold I. now Lsimpl.
Qed.

author: uds-psl

repo: coq-synthetic-incompleteness


text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(**
   natZ.
   Some lemmas about inject_nat, absolu and the relation between
   Z and nat in general.

   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import ZArith.
Require Import EqNat.

Require Import lemmas.

Lemma abs_opp : forall x : Z, Zabs_nat x = Zabs_nat (- x).
Proof.
   simple induction x.
   simpl in |- *. reflexivity.
   simpl in |- *. reflexivity.
   simpl in |- *. reflexivity.
Qed.

Lemma inj_abs_pos : forall x : Z, (x >= 0)%Z -> Z_of_nat (Zabs_nat x) = x.
Proof.
   simple induction x.
   reflexivity.
   intros. simpl in |- *.
   induction  p as [p Hrecp| p Hrecp| ].
   rewrite BinInt.Zpos_xI.
   rewrite <- Hrecp.
   replace (nat_of_P (xI p)) with (S (2 * nat_of_P p)).
   rewrite Znat.inj_S.
   rewrite Znat.inj_mult.
   rewrite Hrecp.
   simpl in |- *.
   reflexivity.
   apply Zle_ge. apply Zorder.Zle_0_pos.
   replace 2 with (nat_of_P 2).
   rewrite <- nat_of_P_mult_morphism.
   simpl in |- *.
   rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ.
   rewrite P_of_succ_nat_o_nat_of_P_eq_succ.
   simpl in |- *.
   reflexivity.
   simpl in |- *.
   reflexivity.
   apply Zle_ge. apply Zorder.Zle_0_pos.
   rewrite BinInt.Zpos_xO.
   rewrite <- Hrecp.
   replace (nat_of_P (xO p)) with (2 * nat_of_P p).
   rewrite Znat.inj_mult.
   rewrite Hrecp.
   simpl in |- *.
   reflexivity.
   apply Zle_ge. apply Zorder.Zle_0_pos.
   replace 2 with (nat_of_P 2).
   rewrite <- nat_of_P_mult_morphism.
   simpl in |- *.
   reflexivity.
   simpl in |- *.
   reflexivity.
   apply Zle_ge.
   apply Zorder.Zle_0_pos.
   reflexivity.
   intros.
   elim H.
   simpl in |- *.
   reflexivity.
Qed.

Lemma inj_abs_neg :
 forall x : Z, (x < 0)%Z -> Z_of_nat (Zabs_nat x) = (- x)%Z.
Proof.
   intros.
   rewrite abs_opp.
   apply inj_abs_pos.
   apply Zle_ge.
   apply Zplus_le_reg_l with x.
   rewrite <- Zplus_0_r_reverse.
   rewrite Zplus_opp_r.
   apply Zlt_le_weak.
   assumption.
Qed.

Lemma abs_inj : forall n : nat, Zabs_nat (Z_of_nat n) = n.
Proof.
   simple induction n.
   simpl in |- *. reflexivity.
   intros m IH.
   rewrite <- IH. simpl in |- *.
   rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
   reflexivity.
Qed.

Lemma abs_mult : forall x y : Z, Zabs_nat (x * y) = Zabs_nat x * Zabs_nat y.
Proof.
   simple induction x.
   simpl in |- *. intro. reflexivity.
   intro.
   simple induction y.
   simpl in |- *.
   rewrite <- mult_n_O.
   reflexivity.
   intro.
   simpl in |- *.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
   simpl in |- *.
   intro.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
   intro.
   simple induction y.
   simpl in |- *.
   rewrite <- mult_n_O.
   reflexivity.
   intro.
   unfold Zabs_nat in |- *.
   simpl in |- *.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
   intro.
   unfold Zabs_nat in |- *.
   simpl in |- *.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
Qed.

Lemma isnat_inj_abs :
 forall (x : Z) (n : nat), x = Z_of_nat n -> n = Zabs_nat x.
Proof.
   intros.
   rewrite H.
   rewrite abs_inj.
   reflexivity.
Qed.

Lemma isnat_abs_inj :
 forall (x : Z) (n : nat), (0 <= x)%Z -> n = Zabs_nat x -> x = Z_of_nat n.
Proof.
   intros.
   rewrite H0.
   rewrite inj_abs_pos.
   reflexivity.
   apply Zle_ge.
   assumption.
Qed.

Lemma isnat_plus : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x + y)%Z.
Proof.
   simple induction x. simpl in |- *. intros. assumption.
   intro. simple induction y. simpl in |- *. intros. assumption.
   simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
   intros. unfold Zle in H0. elim H0. simpl in |- *. reflexivity.
   intros. unfold Zle in H. elim H. simpl in |- *. reflexivity.
Qed.

Lemma isnat_mult : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * y)%Z.
Proof.
   simple induction x.
   simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
   intro. simple induction y. simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
   simpl in |- *. intros. unfold Zle in |- *. simpl in |- *. discriminate.
   intros. unfold Zle in H0. elim H0. simpl in |- *. reflexivity.
   intros. unfold Zle in H. elim H. simpl in |- *. reflexivity.
Qed.

Lemma lezle :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Zabs_nat x <= Zabs_nat y.
Proof.
   intros.
   elim (le_or_lt (Zabs_nat x) (Zabs_nat y)).
   intros. assumption.
   intros. elim (Zlt_not_le y x).
   rewrite <- (inj_abs_pos x).
   rewrite <- (inj_abs_pos y).
   apply Znat.inj_lt. assumption.
   apply Zle_ge. assumption.
   apply Zle_ge. assumption.
   assumption.
Qed.

Lemma gtzgt :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x > y)%Z -> Zabs_nat x > Zabs_nat y.
Proof.
   intros.
   elim (le_or_lt (Zabs_nat x) (Zabs_nat y)).
   intros.
   elim (Zle_not_lt x y).
   rewrite <- (inj_abs_pos x).
   rewrite <- (inj_abs_pos y).
   apply Znat.inj_le. assumption.
   apply Zle_ge. assumption.
   apply Zle_ge. assumption.
   apply Zgt_lt. assumption.
   unfold gt in |- *. intro. assumption.
Qed.

Lemma ltzlt :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Zabs_nat x < Zabs_nat y.
Proof.
   intros.
   change (Zabs_nat y > Zabs_nat x) in |- *.
   apply gtzgt. assumption. assumption.
   apply Zlt_gt. assumption.
Qed.

Lemma abs_plus_pos :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> Zabs_nat (x + y) = Zabs_nat x + Zabs_nat y.
Proof.
   simple induction x.
   simpl in |- *.
   intros.
   reflexivity.
   intro.
   simple induction y.
   simpl in |- *.
   rewrite <- plus_n_O.
   intros.
   reflexivity.
   simpl in |- *.
   intros.
   apply nat_of_P_plus_morphism.
   intros.
   unfold Zle in H0.
   simpl in H0.
   elim H0.
   reflexivity.
   intros.
   unfold Zle in H.
   simpl in H.
   elim H.
   reflexivity.
Qed.

Lemma abs_minus_pos :
 forall x y : Z,
 (0 <= x)%Z ->
 (0 <= y)%Z -> (x >= y)%Z -> Zabs_nat (x - y) = Zabs_nat x - Zabs_nat y.
Proof.
   intros.
   elim (Z_of_nat_complete x).
   intros nx Hx.
   elim (Z_of_nat_complete y).
   intros ny Hy.
   elim (Z_of_nat_complete (x - y)).
   intros d Hd.
   rewrite Hx.
   rewrite Hy.
   rewrite <- Znat.inj_minus1.
   rewrite abs_inj.
   rewrite abs_inj.
   rewrite abs_inj.
   reflexivity.
   rewrite (isnat_inj_abs x nx).
   rewrite (isnat_inj_abs y ny).
   apply lezle.
   assumption.
   assumption.
   apply Zge_le.
   assumption.
   assumption.
   assumption.
   unfold Zminus in |- *.
   apply Zle_left.
   apply Zge_le.
   assumption.
   assumption.
   assumption.
Qed.

Lemma abs_pred_pos :
 forall x : Z, (0 < x)%Z -> pred (Zabs_nat x) = Zabs_nat (x - 1).
Proof.
   intros.
   rewrite abs_minus_pos.
   replace (Zabs_nat 1) with 1.
   rewrite predminus1.
   reflexivity.
   reflexivity.
   apply Zlt_le_weak.
   assumption.
   unfold Zle in |- *.
   simpl in |- *.
   discriminate.
   apply Zle_ge.
   change (Zsucc 0 <= x)%Z in |- *.
   apply Zlt_le_succ.
   assumption.
Qed.

Lemma abs_neq_lt : forall x : Z, x <> 0%Z -> 0 < Zabs_nat x.
Proof.
   simple induction x.
   intro. elim H. reflexivity.
   intros. change (Zabs_nat 0 < Zabs_nat (Zpos p)) in |- *. apply ltzlt.
   unfold Zle in |- *. simpl in |- *. discriminate.
   unfold Zle in |- *. simpl in |- *. discriminate.
   unfold Zlt in |- *. simpl in |- *. reflexivity.
   intros. change (Zabs_nat 0 < Zabs_nat (Zpos p)) in |- *. apply ltzlt.
   unfold Zle in |- *. simpl in |- *. discriminate.
   unfold Zle in |- *. simpl in |- *. discriminate.
   unfold Zlt in |- *. simpl in |- *. reflexivity.
Qed.

Lemma nat_ge_0 : forall n : nat, (Z_of_nat n >= 0)%Z.
Proof.
   simple induction n.
   simpl in |- *. unfold Zge in |- *. simpl in |- *. discriminate.
   intros m IHm.
   change (Z_of_nat (S m) >= Z_of_nat 0)%Z in |- *.
   apply Znat.inj_ge. unfold ge in |- *.
   apply le_O_n.
Qed.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
From Hammer Require Import Hammer.

Require Import OrderedType.
From compcert Require Import Coqlib.
From compcert Require Import Maps.
From compcert Require Import Ordered.
From compcert Require Import AST.
From compcert Require Import Values.
From compcert Require Export Machregs.

Inductive slot: Type :=
| Local
| Incoming
| Outgoing.

Lemma slot_eq: forall (p q: slot), {p = q} + {p <> q}.
Proof. hammer_hook "Locations" "Locations.slot_eq".
decide equality.
Defined.

Open Scope Z_scope.

Definition typesize (ty: typ) : Z :=
match ty with
| Tint => 1
| Tlong => 2
| Tfloat => 2
| Tsingle => 1
| Tany32 => 1
| Tany64 => 2
end.

Lemma typesize_pos:
forall (ty: typ), typesize ty > 0.
Proof. hammer_hook "Locations" "Locations.typesize_pos".
destruct ty; compute; auto.
Qed.

Definition typealign (ty: typ) : Z :=
match ty with
| Tint => 1
| Tlong => 2
| Tfloat => 1
| Tsingle => 1
| Tany32 => 1
| Tany64 => 1
end.

Lemma typealign_pos:
forall (ty: typ), typealign ty > 0.
Proof. hammer_hook "Locations" "Locations.typealign_pos".
destruct ty; compute; auto.
Qed.

Lemma typealign_typesize:
forall (ty: typ), (typealign ty | typesize ty).
Proof. hammer_hook "Locations" "Locations.typealign_typesize".
intros. exists (typesize ty / typealign ty); destruct ty; reflexivity.
Qed.

Inductive loc : Type :=
| R (r: mreg)
| S (sl: slot) (pos: Z) (ty: typ).

Module Loc.

Definition type (l: loc) : typ :=
match l with
| R r => mreg_type r
| S sl pos ty => ty
end.

Lemma eq: forall (p q: loc), {p = q} + {p <> q}.
Proof. hammer_hook "Locations" "Locations.Loc.eq".
decide equality.
apply mreg_eq.
apply typ_eq.
apply zeq.
apply slot_eq.
Defined.

Definition diff (l1 l2: loc) : Prop :=
match l1, l2 with
| R r1, R r2 =>
r1 <> r2
| S s1 d1 t1, S s2 d2 t2 =>
s1 <> s2 \/ d1 + typesize t1 <= d2 \/ d2 + typesize t2 <= d1
| _, _ =>
True
end.

Lemma same_not_diff:
forall l, ~(diff l l).
Proof. hammer_hook "Locations" "Locations.Loc.same_not_diff".
destruct l; unfold diff; auto.
red; intros. destruct H; auto. generalize (typesize_pos ty); omega.
Qed.

Lemma diff_not_eq:
forall l1 l2, diff l1 l2 -> l1 <> l2.
Proof. hammer_hook "Locations" "Locations.Loc.diff_not_eq".
unfold not; intros. subst l2. elim (same_not_diff l1 H).
Qed.

Lemma diff_sym:
forall l1 l2, diff l1 l2 -> diff l2 l1.
Proof. hammer_hook "Locations" "Locations.Loc.diff_sym".
destruct l1; destruct l2; unfold diff; auto.
intuition.
Qed.

Definition diff_dec (l1 l2: loc) : { Loc.diff l1 l2 } + { ~Loc.diff l1 l2 }.
Proof. hammer_hook "Locations" "Locations.Loc.diff_dec".
intros. destruct l1; destruct l2; simpl.
- destruct (mreg_eq r r0). right; tauto. left; auto.
- left; auto.
- left; auto.
- destruct (slot_eq sl sl0).
destruct (zle (pos + typesize ty) pos0).
left; auto.
destruct (zle (pos0 + typesize ty0) pos).
left; auto.
right; red; intros [P | [P | P]]. congruence. omega. omega.
left; auto.
Defined.

Fixpoint notin (l: loc) (ll: list loc) {struct ll} : Prop :=
match ll with
| nil => True
| l1 :: ls => diff l l1 /\ notin l ls
end.

Lemma notin_iff:
forall l ll, notin l ll <-> (forall l', In l' ll -> Loc.diff l l').
Proof. hammer_hook "Locations" "Locations.Loc.notin_iff".
induction ll; simpl.
tauto.
rewrite IHll. intuition. subst a. auto.
Qed.

Lemma notin_not_in:
forall l ll, notin l ll -> ~(In l ll).
Proof. hammer_hook "Locations" "Locations.Loc.notin_not_in".
intros; red; intros. rewrite notin_iff in H.
elim (diff_not_eq l l); auto.
Qed.

Lemma notin_dec (l: loc) (ll: list loc) : {notin l ll} + {~notin l ll}.
Proof. hammer_hook "Locations" "Locations.Loc.notin_dec".
induction ll; simpl.
left; auto.
destruct (diff_dec l a).
destruct IHll.
left; auto.
right; tauto.
right; tauto.
Defined.

Definition disjoint (l1 l2: list loc) : Prop :=
forall x1 x2, In x1 l1 -> In x2 l2 -> diff x1 x2.

Lemma disjoint_cons_left:
forall a l1 l2,
disjoint (a :: l1) l2 -> disjoint l1 l2.
Proof. hammer_hook "Locations" "Locations.Loc.disjoint_cons_left".
unfold disjoint; intros. auto with coqlib.
Qed.
Lemma disjoint_cons_right:
forall a l1 l2,
disjoint l1 (a :: l2) -> disjoint l1 l2.
Proof. hammer_hook "Locations" "Locations.Loc.disjoint_cons_right".
unfold disjoint; intros. auto with coqlib.
Qed.

Lemma disjoint_sym:
forall l1 l2, disjoint l1 l2 -> disjoint l2 l1.
Proof. hammer_hook "Locations" "Locations.Loc.disjoint_sym".
unfold disjoint; intros. apply diff_sym; auto.
Qed.

Lemma in_notin_diff:
forall l1 l2 ll, notin l1 ll -> In l2 ll -> diff l1 l2.
Proof. hammer_hook "Locations" "Locations.Loc.in_notin_diff".
intros. rewrite notin_iff in H. auto.
Qed.

Lemma notin_disjoint:
forall l1 l2,
(forall x, In x l1 -> notin x l2) -> disjoint l1 l2.
Proof. hammer_hook "Locations" "Locations.Loc.notin_disjoint".
intros; red; intros. exploit H; eauto. rewrite notin_iff; intros. auto.
Qed.

Lemma disjoint_notin:
forall l1 l2 x, disjoint l1 l2 -> In x l1 -> notin x l2.
Proof. hammer_hook "Locations" "Locations.Loc.disjoint_notin".
intros; rewrite notin_iff; intros. red in H. auto.
Qed.

Inductive norepet : list loc -> Prop :=
| norepet_nil:
norepet nil
| norepet_cons:
forall hd tl, notin hd tl -> norepet tl -> norepet (hd :: tl).

Lemma norepet_dec (ll: list loc) : {norepet ll} + {~norepet ll}.
Proof. hammer_hook "Locations" "Locations.Loc.norepet_dec".
induction ll.
left; constructor.
destruct (notin_dec a ll).
destruct IHll.
left; constructor; auto.
right; red; intros P; inv P; contradiction.
right; red; intros P; inv P; contradiction.
Defined.

Definition no_overlap (l1 l2 : list loc) :=
forall r, In r l1 -> forall s, In s l2 ->  r = s \/ Loc.diff r s.

End Loc.

Set Implicit Arguments.

Module Locmap.

Definition t := loc -> val.

Definition init (x: val) : t := fun (_: loc) => x.

Definition get (l: loc) (m: t) : val := m l.

Definition set (l: loc) (v: val) (m: t) : t :=
fun (p: loc) =>
if Loc.eq l p then
match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end
else if Loc.diff_dec l p then
m p
else Vundef.

Lemma gss: forall l v m,
(set l v m) l =
match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end.
Proof. hammer_hook "Locations" "Locations.Locmap.gss".
intros. unfold set. apply dec_eq_true.
Qed.

Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v.
Proof. hammer_hook "Locations" "Locations.Locmap.gss_reg".
intros. unfold set. rewrite dec_eq_true. auto.
Qed.

Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v.
Proof. hammer_hook "Locations" "Locations.Locmap.gss_typed".
intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto.
Qed.

Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p.
Proof. hammer_hook "Locations" "Locations.Locmap.gso".
intros. unfold set. destruct (Loc.eq l p).
subst p. elim (Loc.same_not_diff _ H).
destruct (Loc.diff_dec l p).
auto.
contradiction.
Qed.

Fixpoint undef (ll: list loc) (m: t) {struct ll} : t :=
match ll with
| nil => m
| l1 :: ll' => undef ll' (set l1 Vundef m)
end.

Lemma guo: forall ll l m, Loc.notin l ll -> (undef ll m) l = m l.
Proof. hammer_hook "Locations" "Locations.Locmap.guo".
induction ll; simpl; intros. auto.
destruct H. rewrite IHll; auto. apply gso. apply Loc.diff_sym; auto.
Qed.

Lemma gus: forall ll l m, In l ll -> (undef ll m) l = Vundef.
Proof. hammer_hook "Locations" "Locations.Locmap.gus".
assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef).
induction ll; simpl; intros. auto. apply IHll.
unfold set. destruct (Loc.eq a l).
destruct a. auto. destruct ty; reflexivity.
destruct (Loc.diff_dec a l); auto.
induction ll; simpl; intros. contradiction.
destruct H. apply P. subst a. apply gss_typed. exact I.
auto.
Qed.

Definition getpair (p: rpair loc) (m: t) : val :=
match p with
| One l => m l
| Twolong l1 l2 => Val.longofwords (m l1) (m l2)
end.

Definition setpair (p: rpair mreg) (v: val) (m: t) : t :=
match p with
| One r => set (R r) v m
| Twolong hi lo => set (R lo) (Val.loword  v) (set (R hi) (Val.hiword v) m)
end.

Lemma getpair_exten:
forall p ls1 ls2,
(forall l, In l (regs_of_rpair p) -> ls2 l = ls1 l) ->
getpair p ls2 = getpair p ls1.
Proof. hammer_hook "Locations" "Locations.Locmap.getpair_exten".
intros. destruct p; simpl.
apply H; simpl; auto.
f_equal; apply H; simpl; auto.
Qed.

Lemma gpo:
forall p v m l,
forall_rpair (fun r => Loc.diff l (R r)) p -> setpair p v m l = m l.
Proof. hammer_hook "Locations" "Locations.Locmap.gpo".
intros; destruct p; simpl in *.
- apply gso. apply Loc.diff_sym; auto.
- destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto.
Qed.

Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t :=
match res with
| BR r => set (R r) v m
| BR_none => m
| BR_splitlong hi lo =>
setres lo (Val.loword v) (setres hi (Val.hiword v) m)
end.

End Locmap.

Module IndexedTyp <: INDEXED_TYPE.
Definition t := typ.
Definition index (x: t) :=
match x with
| Tany32 => 1%positive
| Tint => 2%positive
| Tsingle => 3%positive
| Tany64 => 4%positive
| Tfloat => 5%positive
| Tlong => 6%positive
end.
Lemma index_inj: forall x y, index x = index y -> x = y.
Proof. hammer_hook "Locations" "Locations.IndexedTyp.index_inj". destruct x; destruct y; simpl; congruence. Qed.
Definition eq := typ_eq.
End IndexedTyp.

Module OrderedTyp := OrderedIndexed(IndexedTyp).

Module IndexedSlot <: INDEXED_TYPE.
Definition t := slot.
Definition index (x: t) :=
match x with Local => 1%positive | Incoming => 2%positive | Outgoing => 3%positive end.
Lemma index_inj: forall x y, index x = index y -> x = y.
Proof. hammer_hook "Locations" "Locations.IndexedSlot.index_inj". destruct x; destruct y; simpl; congruence. Qed.
Definition eq := slot_eq.
End IndexedSlot.

Module OrderedSlot := OrderedIndexed(IndexedSlot).

Module OrderedLoc <: OrderedType.
Definition t := loc.
Definition eq (x y: t) := x = y.
Definition lt (x y: t) :=
match x, y with
| R r1, R r2 => Plt (IndexedMreg.index r1) (IndexedMreg.index r2)
| R _, S _ _ _ => True
| S _ _ _, R _ => False
| S sl1 ofs1 ty1, S sl2 ofs2 ty2 =>
OrderedSlot.lt sl1 sl2 \/ (sl1 = sl2 /\
(ofs1 < ofs2 \/ (ofs1 = ofs2 /\ OrderedTyp.lt ty1 ty2)))
end.
Lemma eq_refl : forall x : t, eq x x.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.eq_refl". exact ((@eq_refl t)). Qed.
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.eq_sym". exact ((@eq_sym t)). Qed.
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.eq_trans". exact ((@eq_trans t)). Qed.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.lt_trans".
unfold lt; intros.
destruct x; destruct y; destruct z; try tauto.
eapply Plt_trans; eauto.
destruct H.
destruct H0. left; eapply OrderedSlot.lt_trans; eauto.
destruct H0. subst sl0. auto.
destruct H. subst sl.
destruct H0. auto.
destruct H.
right.  split. auto.
intuition.
right; split. congruence. eapply OrderedTyp.lt_trans; eauto.
Qed.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.lt_not_eq".
unfold lt, eq; intros; red; intros. subst y.
destruct x.
eelim Plt_strict; eauto.
destruct H. eelim OrderedSlot.lt_not_eq; eauto. red; auto.
destruct H. destruct H0. omega.
destruct H0. eelim OrderedTyp.lt_not_eq; eauto. red; auto.
Qed.
Definition compare : forall x y : t, Compare lt eq x y.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.compare".
intros. destruct x; destruct y.
- destruct (OrderedPositive.compare (IndexedMreg.index r) (IndexedMreg.index r0)).
+ apply LT. red. auto.
+ apply EQ. red. f_equal. apply IndexedMreg.index_inj. auto.
+ apply GT. red. auto.
- apply LT. red; auto.
- apply GT. red; auto.
- destruct (OrderedSlot.compare sl sl0).
+ apply LT. red; auto.
+ destruct (OrderedZ.compare pos pos0).
* apply LT. red. auto.
* destruct (OrderedTyp.compare ty ty0).
apply LT. red; auto.
apply EQ. red; red in e; red in e0; red in e1. congruence.
apply GT. red; auto.
* apply GT. red. auto.
+ apply GT. red; auto.
Defined.
Definition eq_dec := Loc.eq.

Definition diff_low_bound (l: loc) : loc :=
match l with
| R mr => l
| S sl ofs ty => S sl (ofs - 1) Tany64
end.

Definition diff_high_bound (l: loc) : loc :=
match l with
| R mr => l
| S sl ofs ty => S sl (ofs + typesize ty - 1) Tlong
end.

Lemma outside_interval_diff:
forall l l', lt l' (diff_low_bound l) \/ lt (diff_high_bound l) l' -> Loc.diff l l'.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.outside_interval_diff".
intros.
destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto.
- assert (IndexedMreg.index mr <> IndexedMreg.index mr').
{ destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. }
congruence.
- assert (RANGE: forall ty, 1 <= typesize ty <= 2).
{ intros; unfold typesize. destruct ty0; omega.  }
destruct H.
+ destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto.
destruct H. right.
destruct H0. right. generalize (RANGE ty'); omega.
destruct H0.
assert (ty' = Tint \/ ty' = Tsingle \/ ty' = Tany32).
{ unfold OrderedTyp.lt in H1. destruct ty'; auto; compute in H1; congruence. }
right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; omega.
+ destruct H. left. apply OrderedSlot.lt_not_eq; auto.
destruct H. right.
destruct H0. left; omega.
destruct H0. exfalso. destruct ty'; compute in H1; congruence.
Qed.

Lemma diff_outside_interval:
forall l l', Loc.diff l l' -> lt l' (diff_low_bound l) \/ lt (diff_high_bound l) l'.
Proof. hammer_hook "Locations" "Locations.OrderedLoc.diff_outside_interval".
intros.
destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto.
- unfold Plt, Pos.lt. destruct (Pos.compare (IndexedMreg.index mr) (IndexedMreg.index mr')) eqn:C.
elim H. apply IndexedMreg.index_inj. apply Pos.compare_eq_iff. auto.
auto.
rewrite Pos.compare_antisym. rewrite C. auto.
- destruct (OrderedSlot.compare sl sl'); auto.
destruct H. contradiction.
destruct H.
right; right; split; auto. left; omega.
left; right; split; auto.
assert (EITHER: typesize ty' = 1 /\ OrderedTyp.lt ty' Tany64 \/ typesize ty' = 2).
{ destruct ty'; compute; auto. }
destruct (zlt ofs' (ofs - 1)). left; auto.
destruct EITHER as [[P Q] | P].
right; split; auto. omega.
left; omega.
Qed.

End OrderedLoc.

author: lukaszcz

repo: coqhammer-eval


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** RTL function inlining *)

Require Import Coqlib Wfsimpl Maps Errors Integers.
Require Import AST Linking.
Require Import Op Registers RTL.

(** ** Environment of inlinable functions *)

(** We maintain a mapping from function names to their definitions.
  In this mapping, we only include internal functions that are eligible for
  inlining, as determined by the external heuristic
  [should_inline]. *)

Definition funenv : Type := PTree.t function.

Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv.

Parameter should_inline: ident -> function -> bool.

Definition add_globdef (fenv: funenv) (idg: ident * option (globdef fundef unit)) : funenv :=
  match idg with
  | (id, Some (Gfun (Internal f))) =>
      if should_inline id f
      then PTree.set id f fenv
      else PTree.remove id fenv
  | (id, _) =>
      PTree.remove id fenv
  end.

Definition funenv_program (p: program) : funenv :=
  List.fold_left add_globdef p.(prog_defs) (PTree.empty function).

(** State monad *)

(** To construct incrementally the CFG of a function after inlining,
  we use a state monad similar to that used in module [RTLgen].
  It records the current state of the CFG, plus counters to generate
  fresh pseudo-registers and fresh CFG nodes.  It also records the
  stack size needed for the inlined function. *)

Record state : Type := mkstate {
  st_nextreg: positive;                 (**r last used pseudo-register *)
  st_nextnode: positive;                (**r last used CFG node *)
  st_code: code;                        (**r current CFG  *)
  st_stksize: Z                         (**r current stack size *)
}.

(** Monotone evolution of the state. *)

Inductive sincr (s1 s2: state) : Prop :=
  Sincr (NEXTREG: Ple s1.(st_nextreg) s2.(st_nextreg))
        (NEXTNODE: Ple s1.(st_nextnode) s2.(st_nextnode))
        (STKSIZE: s1.(st_stksize) <= s2.(st_stksize)).

Remark sincr_refl: forall s, sincr s s.
Proof.
  intros; constructor; xomega.
Qed.

Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3.
Proof.
  intros. inv H; inv H0. constructor; xomega.
Qed.

(** Dependently-typed state monad, ensuring that the final state is
  greater or equal (in the sense of predicate [sincr] above) than
  the initial state. *)

Inductive res {A: Type} {s: state}: Type := R (x: A) (s': state) (I: sincr s s').

Definition mon (A: Type) : Type := forall (s: state), @res A s.

(** Operations on this monad. *)

Definition ret {A: Type} (x: A): mon A :=
  fun s => R x s (sincr_refl s).

Definition bind {A B: Type} (x: mon A) (f: A -> mon B): mon B :=
  fun s1 => match x s1 with R vx s2 I1 =>
              match f vx s2 with R vy s3 I2 =>
                R vy s3 (sincr_trans s1 s2 s3 I1 I2)
              end
            end.

Notation "'do' X <- A ; B" := (bind A (fun X => B))
   (at level 200, X ident, A at level 100, B at level 200).

Definition initstate :=
  mkstate 1%positive 1%positive (PTree.empty instruction) 0.

Program Definition set_instr (pc: node) (i: instruction): mon unit :=
  fun s =>
    R tt
      (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize))
      _.
Next Obligation.
  intros; constructor; simpl; xomega.
Qed.

Program Definition add_instr (i: instruction): mon node :=
  fun s =>
    let pc := s.(st_nextnode) in
    R pc
      (mkstate s.(st_nextreg) (Psucc pc) (PTree.set pc i s.(st_code)) s.(st_stksize))
      _.
Next Obligation.
  intros; constructor; simpl; xomega.
Qed.

Program Definition reserve_nodes (numnodes: positive): mon positive :=
  fun s =>
    R s.(st_nextnode)
      (mkstate s.(st_nextreg) (Pplus s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize))
      _.
Next Obligation.
  intros; constructor; simpl; xomega.
Qed.

Program Definition reserve_regs (numregs: positive): mon positive :=
  fun s =>
    R s.(st_nextreg)
      (mkstate (Pplus s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize))
      _.
Next Obligation.
  intros; constructor; simpl; xomega.
Qed.

Program Definition request_stack (sz: Z): mon unit :=
  fun s =>
    R tt
      (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Zmax s.(st_stksize) sz))
      _.
Next Obligation.
  intros; constructor; simpl; xomega.
Qed.

Program Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit :=
  fun s =>
    R tt
      (PTree.fold (fun s1 k v => match f k v s1 return _ with R _ s2 _ => s2 end) t s)
      _.
Next Obligation.
  apply PTree_Properties.fold_rec.
  auto.
  apply sincr_refl.
  intros. destruct (f k v a). eapply sincr_trans; eauto.
Qed.

(** ** Inlining contexts *)

(** A context describes how to insert the CFG for a source function into
  the CFG for the function after inlining:
- a source instruction at PC [n] is relocated to PC [n + ctx.(dpc)];
- all pseudo-registers of this instruction are shifted by [ctx.(dreg)];
- all stack references are shifted by [ctx.(dstk)];
- "return" instructions are transformed into "return" or "move" instructions
  as governed by [ctx.(retinfo)].
*)

Record context: Type := mkcontext {
  dpc: positive;                        (**r offset for PCs *)
  dreg: positive;                       (**r offset for pseudo-regs *)
  dstk: Z;                              (**r offset for stack references *)
  mreg: positive;                       (**r max pseudo-reg number *)
  mstk: Z;                              (**r original stack block size *)
  retinfo: option(node * reg)           (**r where to branch on return *)
                                        (**r and deposit return value *)
}.

(** The following functions "shift" (relocate) PCs, registers, operations, etc. *)

Definition shiftpos (p amount: positive) := Ppred (Pplus p amount).

Definition spc (ctx: context) (pc: node) := shiftpos pc ctx.(dpc).

Definition sreg (ctx: context) (r: reg) := shiftpos r ctx.(dreg).

Definition sregs (ctx: context) (rl: list reg) := List.map (sreg ctx) rl.

Definition sros (ctx: context) (ros: reg + ident) := sum_left_map (sreg ctx) ros.

Definition sop (ctx: context) (op: operation) :=
  shift_stack_operation ctx.(dstk) op.

Definition saddr (ctx: context) (addr: addressing) :=
  shift_stack_addressing ctx.(dstk) addr.

Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg :=
  match a with
  | BA x => BA (sreg ctx x)
  | BA_loadstack chunk ofs => BA_loadstack chunk (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk)))
  | BA_addrstack ofs => BA_addrstack (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk)))
  | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
  | BA_addptr a1 a2 => BA_addptr (sbuiltinarg ctx a1) (sbuiltinarg ctx a2)
  | _ => a
  end.

Definition sbuiltinres (ctx: context) (a: builtin_res reg) : builtin_res reg :=
  match a with
  | BR x => BR (sreg ctx x)
  | _    => BR_none
  end.

(** The initial context, used to copy the CFG of a toplevel function. *)

Definition initcontext (dpc dreg nreg: positive) (sz: Z) :=
  {| dpc := dpc;
     dreg := dreg;
     dstk := 0;
     mreg := nreg;
     mstk := Zmax sz 0;
     retinfo := None |}.

(** The context used to inline a call to another function. *)

Definition min_alignment (sz: Z) :=
  if zle sz 1 then 1
  else if zle sz 2 then 2
  else if zle sz 4 then 4 else 8.

Definition callcontext (ctx: context)
                      (dpc dreg nreg: positive) (sz: Z)
                      (retpc: node) (retreg: reg) :=
  {| dpc := dpc;
     dreg := dreg;
     dstk := align (ctx.(dstk) + ctx.(mstk)) (min_alignment sz);
     mreg := nreg;
     mstk := Zmax sz 0;
     retinfo := Some (spc ctx retpc, sreg ctx retreg) |}.

(** The context used to inline a tail call to another function. *)

Definition tailcontext (ctx: context) (dpc dreg nreg: positive) (sz: Z) :=
  {| dpc := dpc;
     dreg := dreg;
     dstk := align ctx.(dstk) (min_alignment sz);
     mreg := nreg;
     mstk := Zmax sz 0;
     retinfo := ctx.(retinfo) |}.

(** ** Recursive expansion and copying of a CFG *)

(** Insert "move" instructions to copy the arguments of an inlined
    function into its parameters. *)

Fixpoint add_moves (srcs dsts: list reg) (succ: node): mon node :=
  match srcs, dsts with
  | s1 :: sl, d1 :: dl =>
      do n <- add_instr (Iop Omove (s1 :: nil) d1 succ);
      add_moves sl dl n
  | _, _ =>
      ret succ
  end.

(** To prevent infinite inlining of a recursive function, when we
  inline the body of a function [f], this function is removed from the
  environment of inlinable functions and therefore becomes ineligible
  for inlining.  This decreases the size (number of entries) of the
  environment and guarantees termination.  Inlining is, therefore,
  presented as a well-founded recursion over the size of the environment. *)

Section EXPAND_CFG.

Variable fenv: funenv.

(** The [rec] parameter is the recursor: [rec fenv' P ctx f] copies
  the body of function [f], with inline expansion within, as governed
  by context [ctx].  It can only be called for function environments
  [fenv'] strictly smaller than the current environment [fenv]. *)

Variable rec: forall fenv', (size_fenv fenv' < size_fenv fenv)%nat -> context -> function -> mon unit.

(** Given a register-or-symbol [ros], can we inline the corresponding call? *)

Inductive inline_decision (ros: reg + ident) : Type :=
  | Cannot_inline
  | Can_inline (id: ident) (f: function) (P: ros = inr reg id) (Q: fenv!id = Some f).

Program Definition can_inline (ros: reg + ident): inline_decision ros :=
  match ros with
  | inl r => Cannot_inline _
  | inr id => match fenv!id with Some f => Can_inline _ id f _ _ | None => Cannot_inline _ end
  end.

(** Inlining of a call to function [f].  An appropriate context is
  created, then the CFG of [f] is recursively copied, then moves
  are inserted to copy the arguments of the call to the parameters of [f]. *)

Definition inline_function (ctx: context) (id: ident) (f: function)
                           (P: PTree.get id fenv = Some f)
                           (args: list reg)
                           (retpc: node) (retreg: reg) : mon node :=
  let npc := max_pc_function f in
  let nreg := max_reg_function f in
  do dpc <- reserve_nodes npc;
  do dreg <- reserve_regs nreg;
  let ctx' := callcontext ctx dpc dreg nreg f.(fn_stacksize) retpc retreg in
  do x <- rec (PTree.remove id fenv) (PTree_Properties.cardinal_remove P) ctx' f;
  add_moves (sregs ctx args) (sregs ctx' f.(fn_params)) (spc ctx' f.(fn_entrypoint)).

(** Inlining of a tail call to function [f].  Similar to [inline_function],
  but the new context is different. *)

Definition inline_tail_function (ctx: context) (id: ident) (f: function)
                               (P: PTree.get id fenv = Some f)
                               (args: list reg): mon node :=
  let npc := max_pc_function f in
  let nreg := max_reg_function f in
  do dpc <- reserve_nodes npc;
  do dreg <- reserve_regs nreg;
  let ctx' := tailcontext ctx dpc dreg nreg f.(fn_stacksize) in
  do x <- rec (PTree.remove id fenv) (PTree_Properties.cardinal_remove P) ctx' f;
  add_moves (sregs ctx args) (sregs ctx' f.(fn_params)) (spc ctx' f.(fn_entrypoint)).

(** The instruction generated for a [Ireturn] instruction found in an
  inlined function body. *)

Definition inline_return (ctx: context) (or: option reg) (retinfo: node * reg) :=
  match retinfo, or with
  | (retpc, retreg), Some r => Iop Omove (sreg ctx r :: nil) retreg retpc
  | (retpc, retreg), None   => Inop retpc
  end.

(** Expansion and copying of an instruction.  For most instructions,
  its registers and successor PC are shifted as per the context [ctx],
  then the instruction is inserted in the final CFG at its final position
  [spc ctx pc].

  [Icall] instructions are either replaced by a "goto" to the expansion
  of the called function, or shifted as described above.

  [Itailcall] instructions are similar, with one additional case.  If
  the [Itailcall] occurs in the body of an inlined function, and
  cannot be inlined itself, it must be turned into an [Icall]
  instruction that branches to the return point of the inlined
  function.

  Finally, [Ireturn] instructions within an inlined function are
  turned into a "move" or "goto" that stores the result, if any,
  into the destination register, then branches back to the successor
  of the inlined call. *)

Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit :=
  match i with
  | Inop s =>
      set_instr (spc ctx pc) (Inop (spc ctx s))
  | Iop op args res s =>
      set_instr (spc ctx pc)
                (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s))
  | Iload chunk addr args dst s =>
      set_instr (spc ctx pc)
                (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s))
  | Istore chunk addr args src s =>
      set_instr (spc ctx pc)
                (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s))
  | Icall sg ros args res s =>
      match can_inline ros with
      | Cannot_inline =>
          set_instr (spc ctx pc)
                    (Icall sg (sros ctx ros) (sregs ctx args) (sreg ctx res) (spc ctx s))
      | Can_inline id f P Q =>
          do n <- inline_function ctx id f Q args s res;
          set_instr (spc ctx pc) (Inop n)
      end
  | Itailcall sg ros args =>
      match can_inline ros with
      | Cannot_inline =>
          match ctx.(retinfo) with
          | None =>
              set_instr (spc ctx pc)
                        (Itailcall sg (sros ctx ros) (sregs ctx args))
          | Some(rpc, rreg) =>
              set_instr (spc ctx pc)
                        (Icall sg (sros ctx ros) (sregs ctx args) rreg rpc)
          end
      | Can_inline id f P Q =>
          do n <- inline_tail_function ctx id f Q args;
          set_instr (spc ctx pc) (Inop n)
      end
  | Ibuiltin ef args res s =>
      set_instr (spc ctx pc)
                (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (spc ctx s))
  | Icond cond args s1 s2 =>
      set_instr (spc ctx pc)
                (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2))
  | Ijumptable r tbl =>
      set_instr (spc ctx pc)
                (Ijumptable (sreg ctx r) (List.map (spc ctx) tbl))
  | Ireturn or =>
      match ctx.(retinfo) with
      | None =>
          set_instr (spc ctx pc) (Ireturn (option_map (sreg ctx) or))
      | Some rinfo =>
          set_instr (spc ctx pc) (inline_return ctx or rinfo)
      end
  end.

(** The expansion of a function [f] iteratively expands all its
  instructions, after recording how much stack it needs. *)

Definition expand_cfg_rec (ctx: context) (f: function): mon unit :=
  do x <- request_stack (ctx.(dstk) + ctx.(mstk));
  ptree_mfold (expand_instr ctx) f.(fn_code).

End EXPAND_CFG.

(** Here we "tie the knot" of the recursion, taking the fixpoint
  of [expand_cfg_rec]. *)

Definition expand_cfg := Fixm size_fenv expand_cfg_rec.

(** Start of the recursion: copy and inline function [f] in the
  initial context. *)

Definition expand_function (fenv: funenv) (f: function): mon context :=
  let npc := max_pc_function f in
  let nreg := max_reg_function f in
  do dpc <- reserve_nodes npc;
  do dreg <- reserve_regs nreg;
  let ctx := initcontext dpc dreg nreg f.(fn_stacksize) in
  do x <- expand_cfg fenv ctx f;
  ret ctx.

(** ** Inlining in functions and whole programs. *)

Local Open Scope string_scope.

(** Inlining can increase the size of the function's stack block.  We must
  make sure that the new size does not exceed [Ptrofs.max_unsigned], otherwise
  address computations within the stack would overflow and produce incorrect
  results. *)

Definition transf_function (fenv: funenv) (f: function) : Errors.res function :=
  let '(R ctx s _) := expand_function fenv f initstate in
  if zlt s.(st_stksize) Ptrofs.max_unsigned then
    OK (mkfunction f.(fn_sig)
                   (sregs ctx f.(fn_params))
                   s.(st_stksize)
                   s.(st_code)
                   (spc ctx f.(fn_entrypoint)))
  else
    Error(msg "Inlining: stack too big").

Definition transf_fundef (fenv: funenv) (fd: fundef) : Errors.res fundef :=
  AST.transf_partial_fundef (transf_function fenv) fd.

Definition transf_program (p: program): Errors.res program :=
  let fenv := funenv_program p in
  AST.transform_partial_program (transf_fundef fenv) p.

author: CertiKOS


text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************)
(*           The Calculus of Inductive Constructions            *)
(*                       COQ v5.10                              *)
(*                                                              *)
(* Laurent Arditi.  Laboratoire I3S. CNRS ura 1376.             *)
(* Universite de Nice - Sophia Antipolis                        *)
(* arditi@unice.fr, http://wwwi3s.unice.fr/~arditi/lolo.html    *)
(*                                                              *)
(* date: may 1995                                               *)
(* file: Bool_compl.v                                           *)
(* contents: additional lemmas about bool, definition of xor,   *)
(* bool_to_nat and if_then_else                                 *)
(****************************************************************)

Require Export Bool.

(****************************************************************)
Lemma neg_eq : forall a b : bool, negb a = negb b -> a = b.
simple induction a; simple induction b; auto.
Qed. Hint Resolve neg_eq.

Lemma false_to_true : false = negb true.
auto.
Qed.

Lemma true_to_false : true = negb false.
auto.
Qed.

Definition xorb (b1 b2 : bool) : bool := b1 && negb b2 || negb b1 && b2.

Lemma xorb_b_b : forall b : bool, xorb b b = false.
simple induction b; auto.
Qed. Hint Resolve xorb_b_b.

Lemma xorb_b_false : forall b : bool, xorb b false = b.
simple induction b; auto.
Qed. Hint Resolve xorb_b_false.

Lemma xorb_b_true : forall b : bool, xorb b true = negb b.
simple induction b; auto.
Qed. Hint Resolve xorb_b_true.

(****************************************************************)
Definition bool_to_nat (b : bool) :=
  match b with
  | true => 1
  | false => 0
  end.

Lemma bool_to_nat_all :
 forall b : bool, bool_to_nat b = 0 \/ bool_to_nat b = 1.
simple induction b; auto.
Qed. Hint Resolve bool_to_nat_all.

(*
Lemma bool_to_nat_negb : (b:bool)
	(bool_to_nat (negb b))=(minus (S O) (bool_to_nat b)).
Induction b;Auto.
Qed. Hints Resolve bool_to_nat_negb.
*)

(****************************************************************)
(* Conditionnelle polymorphique: le test est un booleen,        *)
(* les clauses d'un type quelconque (le meme pour les 2 clauses *)

Definition If (T : Set) (b : bool) (x y : T) :=
  match b with
  | true => x
  | false => y
  end.

Lemma If_neg :
 forall (T : Set) (b : bool) (x y : T), If T (negb b) x y = If T b y x.
simple induction b; simpl in |- *; trivial.
Qed. Hint Resolve If_neg.

Lemma If_eq : forall (T : Set) (b : bool) (x : T), If T b x x = x.
simple induction b; simpl in |- *; trivial.
Qed. Hint Resolve If_eq.

Lemma IfIf :
 forall (T : Set) (b1 b2 : bool) (x x' y y' : T),
 If T b1 (If T b2 x y) (If T b2 x' y') =
 If T b2 (If T b1 x x') (If T b1 y y').
simple induction b2; auto.
Qed.

Lemma If_cond_true :
 forall (T : Set) (a : bool) (x y : T), x <> y -> If T a x y = x -> a = true.
unfold not in |- *. simple induction a; auto.
Qed.

Lemma If_cond_false :
 forall (T : Set) (a : bool) (x y : T), x <> y -> If T a x y = y -> a = false.
unfold not in |- *. simple induction a. simpl in |- *. intros. absurd (x = y). auto.
exact H0. auto.
Qed.

Lemma F_If :
 forall (T T' : Set) (a : bool) (x y : T) (F : T -> T'),
 F (If T a x y) = If T' a (F x) (F y).
simple induction a; auto.
Qed. Hint Resolve F_If.

author: coq-contribs

repo: circuits

save_path: github-repos/coq/coq-contribs-circuits


text:
From Cat Require Import Cat.
From Cat.Universal Require Import Initial Terminal Product Coproduct Exponential.
From Cat.Instances Require Import Discrete FunCat.

Set Implicit Arguments.

#[export]
Instance CAT_init : Cat := Discrete Empty_set.

#[refine]
#[export]
Instance CAT_create (X : Cat) : Functor CAT_init X :=
{
  fob := fun e => match e with end;
  fmap := fun e _ _ => match e with end
}.
Proof.
  all: easy.
Defined.

#[refine]
#[export]
Instance HasInit_CAT : HasInit CAT :=
{
  init := CAT_init;
  create := CAT_create
}.
Proof.
  intros X F G; cbn in *.
  now exists (fun e : Empty_set => match e with end).
Defined.

#[export]
Instance HasStrictInit_CAT : HasStrictInit CAT.
Proof.
  intros C F.
  exists (create C); split; cycle 1.
  - apply equiv_initial.
  - unshelve esplit; cbn in *.
    + now intros A; destruct (fob F A).
    + now intros A B G; cbn; destruct (fob F A).
Defined.

#[export]
Instance CAT_term : Cat := Discrete unit.

#[refine]
#[export]
Instance CAT_delete (X : Cat) : Functor X CAT_term :=
{
  fob := fun _ => tt;
}.
Proof.
  all: easy.
Defined.

#[refine]
#[export]
Instance HasTerm_CAT : HasTerm CAT :=
{
  term := CAT_term;
  delete := CAT_delete;
}.
Proof.
  cbn; intros X F G.
  assert (Heq : forall H : Hom X CAT_term, H == CAT_delete X).
  {
    intros H.
    unshelve esplit.
    - now cbn; intros A; destruct (fob H A).
    - now cbn; intros A B f; apply Eqdep_dec.UIP_refl_unit.
  }
  now rewrite (Heq F), (Heq G).
Defined.

#[refine]
#[export]
Instance CAT_outl (X Y : Cat) : Functor (CAT_product X Y) X :=
{
  fob := fst;
  fmap := fun _ _ => fst
}.
Proof.
  - now proper.
  - easy.
  - easy.
Defined.

#[refine]
#[export]
Instance CAT_outr (X Y : Cat) : Functor (CAT_product X Y) Y :=
{
  fob := snd;
  fmap := fun _ _ => snd
}.
Proof.
  - now proper.
  - easy.
  - easy.
Defined.

#[refine]
#[export]
Instance CAT_fpair
  (X Y A : Cat) (F : Functor A X) (G : Functor A Y) : Functor A (CAT_product X Y) :=
{
  fob := fun X : Ob A => (fob F X, fob G X);
  fmap := fun _ _ f => (fmap F f, fmap G f)
}.
Proof.
  - now proper.
  - now cbn; intros; rewrite !fmap_comp.
  - now cbn; intros; rewrite !fmap_id.
Defined.

Lemma CAT_fpair_unique :
  forall (X C D : Cat) (F : @Hom CAT X C) (G : @Hom CAT X D) (FG : @Hom CAT X (CAT_product C D)),
    F == FG .> CAT_outl C D -> G == FG .> CAT_outr C D -> CAT_fpair F G == FG.
Proof.
  intros X C D F G FG [p q] [r s].
  unshelve esplit; cbn in *; intros.
  - apply eq_prod_intro; cbn; [apply p | apply r].
  - apply eq_prod_intro.
    + rewrite <- q; clear q s.
      generalize (p A), (p B), (r A), (r B).
      destruct (fob FG A), (fob FG B); cbn.
      now intros [] [] [] []; cbn.
    + rewrite <- s; clear q s.
      generalize (p A), (p B), (r A), (r B).
      destruct (fob FG A), (fob FG B); cbn.
      now intros [] [] [] []; cbn.
Qed.

#[refine]
#[export]
Instance HasProducts_CAT : HasProducts CAT :=
{
  product := CAT_product;
  outl := CAT_outl;
  outr := CAT_outr;
  fpair := CAT_fpair
}.
Proof.
  intros C D; split; intros X F G.
  - now exists (fun _ => eq_refl); cbn.
  - now exists (fun _ => eq_refl); cbn.
  - intros Hl Hr.
    transitivity (CAT_fpair (F .> CAT_outl C D) (F .> CAT_outr C D)).
    + now symmetry; apply CAT_fpair_unique.
    + now apply CAT_fpair_unique.
Defined.

Definition CoprodCatHom {C D : Cat} (X Y : Ob C + Ob D) : Type :=
match X, Y with
| inl X', inl Y' => Hom X' Y'
| inr X', inr Y' => Hom X' Y'
| _     , _      => Empty_set
end.

#[refine]
#[export]
Instance CoprodCatSetoid {C D : Cat} (X Y : Ob C + Ob D) : Setoid (CoprodCatHom X Y) :=
{
  equiv :=
    match X, Y with
    | inl X', inl Y' => fun f g => f == g
    | inr X', inr Y' => fun f g => f == g
    | _     , _      => fun _ _ => False
    end;
}.
Proof.
  destruct X as [X' | X'], Y as [Y' | Y']; cbn.
  + now apply HomSetoid.
  + easy.
  + easy.
  + now apply HomSetoid.
Defined.

#[refine]
#[export]
Instance CAT_coproduct (C : Cat) (D : Cat) : Cat :=
{
  Ob := Ob C + Ob D;
  Hom := CoprodCatHom;
  HomSetoid := CoprodCatSetoid;
  id := fun A : Ob C + Ob D =>
    match A with
    | inl A' => id A'
    | inr A' => id A'
    end;
  comp := fun A B C =>
    match A, B, C with
    | inl A', inl B', inl C' => fun f g => f .> g
    | inr A', inr B', inr C' => fun f g => f .> g
    | _     , _     , _      => ltac:(easy)
    end;
}.
Proof.
  - now intros [X | X] [Y | Y] [Z | Z]; cbn; proper.
  - now intros [X | X] [Y | Y] [Z | Z] [W | W] *; cbn.
  - now intros [X | X] [Y | Y]; cbn.
  - now intros [X | X] [Y | Y]; cbn.
Defined.

#[refine]
#[export]
Instance CAT_finl (X Y : Cat) : Functor X (CAT_coproduct X Y) :=
{
  fob := inl;
  fmap := fun _ _ f => f
}.
Proof.
  all: easy.
Defined.

#[refine]
#[export]
Instance CAT_finr (X Y : Cat) : Functor Y (CAT_coproduct X Y) :=
{
  fob := inr;
  fmap := fun _ _ f => f
}.
Proof.
  all: easy.
Defined.

#[refine]
#[export]
Instance CAT_copair
  (C D E : Cat) (F : Functor C E) (G : Functor D E) : Functor (CAT_coproduct C D) E :=
{
  fob := fun X : Ob C + Ob D =>
    match X with
    | inl X' => fob F X'
    | inr X' => fob G X'
    end;
  fmap := fun A B =>
    match A, B with
    | inl A', inl B' => fun f => fmap F f
    | inr A', inr B' => fun f => fmap G f
    | _     , _      => ltac:(easy)
    end;
}.
Proof.
  - intros [A | A] [B | B] f g Heq; cbn; [| easy | easy |].
    + now rewrite Heq.
    + now rewrite Heq.
  - intros [X | X] [Y | Y] [Z | Z] f g; cbn in *; try easy.
    + now rewrite fmap_comp.
    + now rewrite fmap_comp.
  - now intros [X | X]; cbn in *; rewrite fmap_id.
Defined.

#[refine]
#[export]
Instance HasCoproducts_CAT : HasCoproducts CAT :=
{
  coproduct := CAT_coproduct;
  finl := CAT_finl;
  finr := CAT_finr;
  copair := CAT_copair
}.
Proof.
  intros C D; split; cbn; intros P' F G.
  - now exists (fun _ => eq_refl).
  - now exists (fun _ => eq_refl).
  - intros [p q] [r s].
    unshelve esplit.
    + now intros [A | A]; [apply p | apply r].
    + now intros [A | A] [B | B] H; [apply q | | | apply s].
Defined.

#[refine]
#[export]
Instance HasExponentials_CAT : HasExponentials CAT :=
{
  exponential := @FunCat;
}.
Proof.
  - cbn; intros C D.
    unshelve esplit with (fob := fun '(F, X) => fob F X).
    + intros [F X] [G Y] [f g]; cbn in *.
      exact (component f X .> fmap G g).
    + intros [F X] [G Y] [α f] [β g] [H1 H2]; cbn in *.
      now rewrite H1, H2.
    + intros [F X] [G Y] [H Z] [[α H1] f] [[β H2] g]; cbn in *.
      now rewrite comp_assoc, H2, fmap_comp, !comp_assoc, <- H2.
    + now intros [F X]; cbn; rewrite fmap_id, comp_id_l.
  - cbn; intros D E C.
    intros [fob fmap prp pcmp pid].
    unshelve esplit; cbn in *.
    + intro X. unshelve esplit with (fob := fun d => fob (X, d)).
      * intros A B f.
Abort.

author: wkolowski

repo: CoqCat

save_path: github-repos/coq/wkolowski-CoqCat