Example of something ever so slightly slow in brazil

[JasonGross]

In case you're interested in where speed issues begin to crop up:

Definition Type := Universe f0.

(* sums *)
Parameter sum : Type -> Type -> Type.
Parameter inl : forall (A B : Type), A -> sum A B.
Parameter inr : forall (A B : Type), B -> sum A B.

Parameter sum_ind :
  forall (A B : Type) (P : sum A B -> Type), (forall (x : A), P (inl A B x)) -> (forall (x : B), P (inr A B x)) -> forall b : sum A B, P b.

Parameter sum_ind_inl :
  forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : A),
    sum_ind A B P IHinl IHinr (inl A B x) == (IHinl x).

Parameter sum_ind_inr :
  forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (x : B),
    sum_ind A B P IHinl IHinr (inr A B x) == (IHinr x).

Rewrite sum_ind_inl.
Rewrite sum_ind_inr.

Parameter sum_match_commutes :
  forall (A B : Type) (P : sum A B -> Type) (IHinl : forall (x : A), P (inl A B x)) (IHinr : forall (x : B), P (inr A B x)) (C : forall (x : sum A B), P x -> Type)
         (f : forall (x : sum A B) (p : P x), C x p)
         (x : sum A B),
    sum_ind A B (fun x : sum A B => C x (sum_ind A B P IHinl IHinr x))
            (fun (x : A) => equation sum_ind_inl in
                            (f (inl A B x) (IHinl x) :: C (inl A B x) (sum_ind A B P IHinl IHinr (inl A B x))))
            (fun (x : B) => equation sum_ind_inr in
                            (f (inr A B x) (IHinr x) :: C (inr A B x) (sum_ind A B P IHinl IHinr (inr A B x))))
            x
    == f x (sum_ind A B P IHinl IHinr x).


Definition sum_half_eta :=
  fun (A B : Type) (x : sum A B) =>
    sum_match_commutes A B (fun (x : sum A B) => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) (fun (x : sum A B) (_ : sum A B) => sum A B) (fun (x : sum A B) (_ : sum A B) => x) x
    :: sum_ind A B (fun _ : sum A B => sum A B) (fun x : A => inl A B x) (fun x : B => inr A B x) x == x.

Rewrite sum_half_eta.

(*********)

$ time ./brazil.byte examples/sum.br
...
real    0m1.560s
user    0m1.531s
sys     0m0.031s

$ time ./brazil.byte examples/sum.br
...
real    0m0.333s
user    0m0.311s
sys     0m0.000s

By contrast, timing the smoketest (only the typechecking, not compiling brazil and tt themselves) gives

real    0m0.152s
user    0m0.030s
sys     0m0.091s

on my machine.

[andrejbauer]

Yeah, there are several factors, Chris investigated, ranging from "Print.debug is slow even when not printing" to "those annotations on applications are really huge". We're probably going to do something about annotations so we only keep them when necessary.

[JasonGross]

Here's something even slower:

Definition Type := Universe f0.

Parameter sigma : forall (A : Type), (A -> Type) -> Type.

Parameter pair :
  forall (A : Type)
         (P : A -> Type)
         (a : A)
         (b : P a),
         sigma A P.

Parameter sigma_elim :
  forall (A : Type)
         (P : A -> Type)
         (u : sigma A P)
         (C : sigma A P -> Type),
         (forall (a : A) (b : P a), C (pair A P a b)) -> C u.

Parameter sigma_beta :
  forall (A : Type)
         (P : A -> Type)
         (a : A)
         (b : P a)
         (C : sigma A P -> Type)
         (f : forall (a : A) (b : P a), C (pair A P a b)),
         sigma_elim A P (pair A P a b) C f == f a b.

Parameter sigma_comm :
    forall (A : Type)
           (P : A -> Type)
           (Q : sigma A P -> Type)
           (q : forall (x : A) (p : P x), Q (pair A P x p))
           (R : forall (x : sigma A P), Q x -> Type)
           (f : forall (x : sigma A P) (q : Q x), R x q)
           (u : sigma A P),
  rewrite sigma_beta in
    sigma_elim A P u
               (fun (x : sigma A P) => R x (sigma_elim A P x Q (fun (x : A) (p : P x) => q x p)))
               (fun (x : A) (p : P x) => f (pair A P x p) (q x p) :: R (pair A P x p) (sigma_elim A P (pair A P x p) Q q))
      ==
    f u (sigma_elim A P u Q q).

Definition sigma_half_eta :=
  fun (A : Type)
      (P : A -> Type)
      (u : sigma A P) =>
    sigma_comm A P (fun (_ : sigma A P) => sigma A P) (pair A P) (fun (_ : sigma A P) (_ : sigma A P) => sigma A P) (fun (x : sigma A P) (_ : sigma A P) => x) u
    :: sigma_elim A P u (fun (_ : sigma A P) => sigma A P)
         (fun (a : A) (b : P a) => pair A P a b)
       ==
       u.

Rewrite sigma_beta.

Definition fst :=
  fun (A : Type) (P : A -> Type) (u : sigma A P) =>
    sigma_elim A P u (fun (_ : sigma  A P) => A) (fun (a : A) (_ : P a) => a).

Definition snd :=
  fun (A : Type) (P : A -> Type) (u : sigma A P) =>
    sigma_elim
      A P u
      (fun (u : sigma A P) => P (fst A P u))
      (fun (a : A) (b : P a) => b).

(*match u as u' with (a; b) => (fun u p => (fst p; snd p)) (a; b) end == match u with (a; b) => (a; b) end
match u as u' with (a; b) => (fun u p => (fst p; snd p)) (a; b) end == match u with (a; b) => (a; b) end
(fun u p => (fst p; snd p)) u ... == match u with (a; b) => (a; b) end
(fst u; snd u) == (fun u p => p) u (match u with (a; b) => (a; b) end)
(fst u; snd u) == match u with (a; b) => (a; b) end
(fst u; snd u) == u*)

Definition sigma_half_eta_with_dummy_unit := fun _ : unit => sigma_half_eta.

Definition sigma_eta :=
  fun (A : Type)
      (P : A -> Type)
      (u : sigma A P)
  =>
    rewrite (fun (a : A) (b : P a) => sigma_beta A P a b (fun (_ : sigma A P) => A) (fun (a : A) (_ : P a) => a) :: (fst A P (pair A P a b) == a)) in
    (fun term : sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => (fun (u : sigma A P) (p : sigma A P) => pair A P (fst A P p) (snd A P p)) (pair A P a b) (pair A P a b))
                == u
     => rewrite sigma_comm A P (fun (_ : sigma A P) => sigma A P) (pair A P) (fun (_ : sigma A P) (_ : sigma A P) => sigma A P) (fun (_ : sigma A P) (x : sigma A P) => pair A P (fst A P x) (snd A P x)) u in
        term :: (fun (u : sigma A P) (p : sigma A P) => pair A P (fst A P p) (snd A P p)) u (sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b))
                 == u)  (* (fun u p => (fst p; snd p)) u (match u with (a; b) => (a; b) end) == u *)
     ((((fun dummy : unit =>
         rewrite sigma_half_eta_with_dummy_unit dummy A P u in
         refl u
         :: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P a b)
            == u) ()) (* match u with (a; b) => (a; b) end == u *)
        :: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => pair A P (fst A P (pair A P a b)) (snd A P (pair A P a b)))
          == u)       (* match u with (a; b) => (fst (a; b); snd (a; b)) end == u *)
      :: sigma_elim A P u (fun (_ : sigma A P) => sigma A P) (fun (a : A) (b : P a) => (fun (u : sigma A P) (p : sigma A P) => pair A P (fst A P p) (snd A P p)) (pair A P a b) (pair A P a b))
          == u)       (* match u with (a; b) => (fun u p => (fst p; snd p)) (a; b) (a; b) end == u *).

$ time ./brazil.native examples/slow.br
...
real    0m12.768s
user    0m12.671s
sys     0m0.031s

This is probably huge annotations?

[christopherastone]

It turned out to be too painful to get rid of the big annotations, but I made some other speed improvements which speeds up the sum example by a factor of 3 or so.

Unfortunately, along the way the pattern-matching code was rewritten yet again (to be much less ad-hoc), and Brazil no longer can type check the second example.

[JasonGross]

Do you have a sense of what broke the second example?

[christopherastone]

Generally, I'm asusming a rewrite is no longer applying, because the system is being (unintentionally) less-aggressive about reducing subterms during matching, or because it's being (intentionally) more careful about checking that the type of the hint matches the type of the term. Or for some other reason.

There's quite a lot of debugging output, so I haven't yet tracked down exactly where the problem lies.

[JasonGross]

#28 is a smaller example.