Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Kernel conversion should provide a way of sharing conversions and not just reductions #16606

Open
JasonGross opened this issue Oct 4, 2022 · 7 comments
Open

Kernel conversion should provide a way of sharing conversions and not just reductions #16606

JasonGross opened this issue Oct 4, 2022 · 7 comments
Labels
kind: performance Improvements to performance and efficiency. part: kernel

Comments

@JasonGross
Copy link
Member

JasonGross commented Oct 4, 2022 •
edited

Description of the problem

It seems that kernel conversion does not share conversion of let-binders with other terms. This is relevant at mit-plv/fiat-crypto#1358 (comment), where we have kernel conversion (Qed) taking about 50 minutes. Here is a simplified version that I believe is representative of the sort of conversion problem we're facing:

Require Import Coq.ZArith.ZArith.
Set Debug "Cbv".
Definition Z_div_eucl_unfolded := Eval cbv in Z.div_eucl.
(* Take output, run through `grep -o 'Unfolding [^ ]*$' | grep -o '[^ ]*$' | sort | uniq` *)
Strategy -10 [Coq.Init.Datatypes.CompOpp
Coq.PArith.BinPos.Pos.add
Coq.PArith.BinPos.Pos.compare
Coq.PArith.BinPos.Pos.compare_cont
Coq.PArith.BinPos.Pos.mul
Coq.PArith.BinPos.Pos.pred_double
Coq.PArith.BinPos.Pos.succ
Coq.ZArith.BinInt.Z.add
Coq.ZArith.BinInt.Z.compare
Coq.ZArith.BinInt.Z.div_eucl
Coq.ZArith.BinInt.Z.double
Coq.ZArith.BinInt.Z.leb
Coq.ZArith.BinInt.Z.ltb
Coq.ZArith.BinInt.Z.mul
Coq.ZArith.BinInt.Z.opp
Coq.ZArith.BinInt.Z.pos_div_eucl
Coq.ZArith.BinInt.Z.pos_sub
Coq.ZArith.BinInt.Z.pred_double
Coq.ZArith.BinInt.Z.sub
Coq.ZArith.BinInt.Z.succ_double].
Strategy -10 [Z_div_eucl_unfolded].
Set Debug "-Cbv".
Fixpoint dupT (n : nat) (A : Set) : Set
  := match n with O => unit | S n => A * dupT n A end.
Fixpoint dup {A : Set} (n : nat) (a : A) : dupT n A :=
  match n with O => tt | S n => (a, dup n a) end.
Definition mk_unif1' (n : nat) : Prop
  := Eval cbv beta iota delta [dupT dup] in
    (let x := Z_div_eucl_unfolded in dup n x)
    = (dup n Z.div_eucl).
Definition mk_unif2' (n : nat) : Prop
  := Eval cbv beta iota delta [dupT dup] in
    (let x := Z.div_eucl in dup n x)
    = (dup n Z.div_eucl).
Definition mk_unif3' (n : nat) : Prop
  := Eval cbv beta iota delta [dupT dup Z_div_eucl_unfolded] in
    (dup n Z_div_eucl_unfolded)
    = (dup n Z_div_eucl_unfolded).
Definition mk_unif4' (n : nat) : Prop
  := Eval cbv beta iota delta [dupT dup Z_div_eucl_unfolded] in
    (let x := Z_div_eucl_unfolded in dup n x)
    = (dup n Z_div_eucl_unfolded).
Notation mk_unif1_gen mk_unif n := (match n%nat return _ with n' => ltac:(let n' := (eval cbv in n') in let v := (eval cbv beta iota delta [mk_unif] in (mk_unif n')) in exact v) end) (only parsing).
Notation mk_unif1 n := (mk_unif1_gen mk_unif1' n) (only parsing).
Notation mk_unif2 n := (mk_unif1_gen mk_unif2' n) (only parsing).
Notation mk_unif3 n := (mk_unif1_gen mk_unif3' n) (only parsing).
Notation mk_unif4 n := (mk_unif1_gen mk_unif4' n) (only parsing).
Ltac mk_unif1 n := constr:(mk_unif1 n).
Ltac mk_unif2 n := constr:(mk_unif2 n).
Ltac mk_unif3 n := constr:(mk_unif3 n).
Ltac mk_unif4 n := constr:(mk_unif4 n).
Ltac check_time mk_unif n :=
  lazymatch n with
  | O => idtac
  | S ?n'
    => check_time mk_unif n';
       idtac "n:" n;
       let ty := mk_unif n in
       let __ := constr:(ltac:(time reflexivity) : ty) in
       idtac
  end.
Ltac check_time1 n := check_time ltac:(mk_unif1) n.
Ltac check_time2 n := check_time ltac:(mk_unif2) n.
Ltac check_time3 n := check_time ltac:(mk_unif3) n.
Ltac check_time4 n := check_time ltac:(mk_unif4) n.
Timing info 
Goal True.
  check_time1 50.
  (*
n: 1
Tactic call ran for 0.008 secs (0.008u,0.s) (success)
n: 2
Tactic call ran for 0.015 secs (0.015u,0.s) (success)
n: 3
Tactic call ran for 0.038 secs (0.038u,0.s) (success)
n: 4
Tactic call ran for 0.049 secs (0.049u,0.s) (success)
n: 5
Tactic call ran for 0.036 secs (0.035u,0.s) (success)
n: 6
Tactic call ran for 0.057 secs (0.057u,0.s) (success)
n: 7
Tactic call ran for 0.104 secs (0.104u,0.s) (success)
n: 8
Tactic call ran for 0.086 secs (0.085u,0.s) (success)
n: 9
Tactic call ran for 0.087 secs (0.078u,0.008s) (success)
n: 10
Tactic call ran for 0.092 secs (0.092u,0.s) (success)
n: 11
Tactic call ran for 0.102 secs (0.102u,0.s) (success)
n: 12
Tactic call ran for 0.094 secs (0.094u,0.s) (success)
n: 13
Tactic call ran for 0.129 secs (0.129u,0.s) (success)
n: 14
Tactic call ran for 0.126 secs (0.126u,0.s) (success)
n: 15
Tactic call ran for 0.118 secs (0.118u,0.s) (success)
n: 16
Tactic call ran for 0.125 secs (0.125u,0.s) (success)
n: 17
Tactic call ran for 0.13 secs (0.13u,0.s) (success)
n: 18
Tactic call ran for 0.141 secs (0.141u,0.s) (success)
n: 19
Tactic call ran for 0.141 secs (0.141u,0.s) (success)
n: 20
Tactic call ran for 0.159 secs (0.158u,0.s) (success)
n: 21
Tactic call ran for 0.294 secs (0.294u,0.s) (success)
n: 22
Tactic call ran for 0.214 secs (0.214u,0.s) (success)
n: 23
Tactic call ran for 0.197 secs (0.197u,0.s) (success)
n: 24
Tactic call ran for 0.19 secs (0.19u,0.s) (success)
n: 25
Tactic call ran for 0.201 secs (0.2u,0.s) (success)
n: 26
Tactic call ran for 0.203 secs (0.203u,0.s) (success)
n: 27
Tactic call ran for 0.257 secs (0.257u,0.s) (success)
n: 28
Tactic call ran for 0.221 secs (0.221u,0.s) (success)
n: 29
Tactic call ran for 0.243 secs (0.243u,0.s) (success)
n: 30
Tactic call ran for 0.277 secs (0.277u,0.s) (success)
n: 31
Tactic call ran for 0.272 secs (0.272u,0.s) (success)
n: 32
Tactic call ran for 0.315 secs (0.315u,0.s) (success)
n: 33
Tactic call ran for 0.3 secs (0.3u,0.s) (success)
n: 34
Tactic call ran for 0.304 secs (0.304u,0.s) (success)
n: 35
Tactic call ran for 0.308 secs (0.308u,0.s) (success)
n: 36
Tactic call ran for 0.36 secs (0.36u,0.s) (success)
n: 37
Tactic call ran for 0.327 secs (0.327u,0.s) (success)
n: 38
Tactic call ran for 0.32 secs (0.32u,0.s) (success)
n: 39
Tactic call ran for 0.352 secs (0.352u,0.s) (success)
n: 40
Tactic call ran for 0.348 secs (0.348u,0.s) (success)
n: 41
Tactic call ran for 0.351 secs (0.351u,0.s) (success)
n: 42
Tactic call ran for 0.363 secs (0.363u,0.s) (success)
n: 43
Tactic call ran for 0.407 secs (0.406u,0.s) (success)
n: 44
Tactic call ran for 0.391 secs (0.391u,0.s) (success)
n: 45
Tactic call ran for 0.415 secs (0.415u,0.s) (success)
n: 46
Tactic call ran for 0.447 secs (0.447u,0.s) (success)
n: 47
Tactic call ran for 0.453 secs (0.453u,0.s) (success)
n: 48
Tactic call ran for 0.458 secs (0.458u,0.s) (success)
n: 49
Tactic call ran for 0.465 secs (0.465u,0.s) (success)
n: 50
Tactic call ran for 0.463 secs (0.463u,0.s) (success)
   *)
  check_time2 50.
  (* n: 1
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 2
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 3
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 4
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 5
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 6
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 7
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 8
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 9
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 10
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 11
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 12
Tactic call ran for 0. secs (0.u,0.s) (success)
n: 13
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
n: 14
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
n: 15
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 16
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
n: 17
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 18
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 19
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 20
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 21
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 22
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
n: 23
Tactic call ran for 0.003 secs (0.003u,0.s) (success)
n: 24
Tactic call ran for 0.004 secs (0.004u,0.s) (success)
n: 25
Tactic call ran for 0.004 secs (0.004u,0.s) (success)
n: 26
Tactic call ran for 0.004 secs (0.004u,0.s) (success)
n: 27
Tactic call ran for 0.004 secs (0.004u,0.s) (success)
n: 28
Tactic call ran for 0.005 secs (0.005u,0.s) (success)
n: 29
Tactic call ran for 0.004 secs (0.004u,0.s) (success)
n: 30
Tactic call ran for 0.007 secs (0.007u,0.s) (success)
n: 31
Tactic call ran for 0.005 secs (0.005u,0.s) (success)
n: 32
Tactic call ran for 0.005 secs (0.005u,0.s) (success)
n: 33
Tactic call ran for 0.006 secs (0.006u,0.s) (success)
n: 34
Tactic call ran for 0.006 secs (0.006u,0.s) (success)
n: 35
Tactic call ran for 0.006 secs (0.006u,0.s) (success)
n: 36
Tactic call ran for 0.019 secs (0.009u,0.009s) (success)
n: 37
Tactic call ran for 0.007 secs (0.007u,0.s) (success)
n: 38
Tactic call ran for 0.007 secs (0.007u,0.s) (success)
n: 39
Tactic call ran for 0.008 secs (0.008u,0.s) (success)
n: 40
Tactic call ran for 0.019 secs (0.019u,0.s) (success)
n: 41
Tactic call ran for 0.009 secs (0.009u,0.s) (success)
n: 42
Tactic call ran for 0.009 secs (0.009u,0.s) (success)
n: 43
Tactic call ran for 0.01 secs (0.01u,0.s) (success)
n: 44
Tactic call ran for 0.023 secs (0.023u,0.s) (success)
n: 45
Tactic call ran for 0.01 secs (0.01u,0.s) (success)
n: 46
Tactic call ran for 0.011 secs (0.011u,0.s) (success)
n: 47
Tactic call ran for 0.024 secs (0.024u,0.s) (success)
n: 48
Tactic call ran for 0.012 secs (0.012u,0.s) (success)
n: 49
Tactic call ran for 0.013 secs (0.013u,0.s) (success)
n: 50
Tactic call ran for 0.013 secs (0.013u,0.s) (success)
*)
  check_time3 30.
  (* n: 1
Tactic call ran for 0.035 secs (0.035u,0.s) (success)
n: 2
Tactic call ran for 0.105 secs (0.105u,0.s) (success)
n: 3
Tactic call ran for 0.19 secs (0.18u,0.01s) (success)
n: 4
Tactic call ran for 0.203 secs (0.183u,0.019s) (success)
n: 5
Tactic call ran for 0.26 secs (0.26u,0.s) (success)
n: 6
Tactic call ran for 0.325 secs (0.305u,0.02s) (success)
n: 7
Tactic call ran for 0.347 secs (0.327u,0.02s) (success)
n: 8
Tactic call ran for 0.409 secs (0.399u,0.009s) (success)
n: 9
Tactic call ran for 0.459 secs (0.459u,0.s) (success)
n: 10
Tactic call ran for 0.508 secs (0.488u,0.019s) (success)
n: 11
Tactic call ran for 0.548 secs (0.529u,0.019s) (success)
n: 12
Tactic call ran for 0.546 secs (0.506u,0.039s) (success)
n: 13
Tactic call ran for 0.572 secs (0.552u,0.02s) (success)
n: 14
Tactic call ran for 0.619 secs (0.569u,0.05s) (success)
n: 15
Tactic call ran for 0.716 secs (0.686u,0.029s) (success)
n: 16
Tactic call ran for 0.768 secs (0.768u,0.s) (success)
n: 17
Tactic call ran for 0.766 secs (0.766u,0.s) (success)
n: 18
Tactic call ran for 0.809 secs (0.809u,0.s) (success)
n: 19
Tactic call ran for 0.895 secs (0.895u,0.s) (success)
n: 20
Tactic call ran for 0.983 secs (0.963u,0.02s) (success)
n: 21
Tactic call ran for 1.014 secs (0.954u,0.059s) (success)
n: 22
Tactic call ran for 1.048 secs (0.968u,0.08s) (success)
n: 23
Tactic call ran for 1.168 secs (1.078u,0.09s) (success)
n: 24
Tactic call ran for 1.108 secs (1.098u,0.009s) (success)
n: 25
Tactic call ran for 2.966 secs (2.966u,0.s) (success)
n: 26
Tactic call ran for 1.237 secs (1.237u,0.s) (success)
n: 27
Tactic call ran for 1.241 secs (1.241u,0.s) (success)
n: 28
Tactic call ran for 1.339 secs (1.339u,0.s) (success)
n: 29
Tactic call ran for 1.304 secs (1.304u,0.s) (success)
n: 30
Tactic call ran for 1.228 secs (1.228u,0.s) (success)
*)
  check_time4 30.
  (*
  n: 1
Tactic call ran for 0.056 secs (0.056u,0.s) (success)
n: 2
Tactic call ran for 0.1 secs (0.1u,0.s) (success)
n: 3
Tactic call ran for 0.179 secs (0.179u,0.s) (success)
n: 4
Tactic call ran for 0.229 secs (0.219u,0.01s) (success)
n: 5
Tactic call ran for 0.218 secs (0.208u,0.009s) (success)
n: 6
Tactic call ran for 0.312 secs (0.312u,0.s) (success)
n: 7
Tactic call ran for 0.385 secs (0.375u,0.009s) (success)
n: 8
Tactic call ran for 0.373 secs (0.353u,0.02s) (success)
n: 9
Tactic call ran for 0.431 secs (0.421u,0.009s) (success)
n: 10
Tactic call ran for 0.425 secs (0.415u,0.009s) (success)
n: 11
Tactic call ran for 0.481 secs (0.461u,0.02s) (success)
n: 12
Tactic call ran for 0.619 secs (0.619u,0.s) (success)
n: 13
Tactic call ran for 0.542 secs (0.532u,0.01s) (success)
n: 14
Tactic call ran for 0.683 secs (0.673u,0.009s) (success)
n: 15
Tactic call ran for 0.674 secs (0.664u,0.01s) (success)
n: 16
Tactic call ran for 0.835 secs (0.795u,0.04s) (success)
n: 17
Tactic call ran for 0.815 secs (0.775u,0.04s) (success)
n: 18
Tactic call ran for 0.861 secs (0.861u,0.s) (success)
n: 19
Tactic call ran for 0.861 secs (0.861u,0.s) (success)
n: 20
Tactic call ran for 0.884 secs (0.864u,0.02s) (success)
n: 21
Tactic call ran for 0.931 secs (0.881u,0.049s) (success)
n: 22
Tactic call ran for 0.966 secs (0.906u,0.059s) (success)
n: 23
Tactic call ran for 0.996 secs (0.916u,0.08s) (success)
n: 24
Tactic call ran for 1.53 secs (1.53u,0.s) (success)
n: 25
Tactic call ran for 1.24 secs (1.19u,0.05s) (success)
n: 26
Tactic call ran for 1.313 secs (1.283u,0.03s) (success)
n: 27
Tactic call ran for 1.315 secs (1.215u,0.099s) (success)
n: 28
Tactic call ran for 1.356 secs (1.266u,0.09s) (success)
n: 29
Tactic call ran for 1.341 secs (1.231u,0.11s) (success)
n: 30
Tactic call ran for 1.399 secs (1.319u,0.08s) (success)
*)
Abort.

Here's a slightly less simplified version, that is more accurate to the problem we're dealing with:

Inductive type := BASE | UNIT | PROD (A B : type).
Fixpoint denoteT (t : type) : Set
  := match t with
     | UNIT => unit
     | BASE => Z -> Z -> Z * Z
     | PROD A B => denoteT A * denoteT B
     end.
Inductive expr : type -> Set :=
| Z_DIV_EUCL : expr BASE
| PAIR {A B} : expr A -> expr B -> expr (PROD A B)
| TT : expr UNIT
.
Definition denote
  := Eval cbv delta [Z_div_eucl_unfolded] in
    fix denote {t} (e : expr t) : denoteT t
    := match e with
       | Z_DIV_EUCL => Z_div_eucl_unfolded
       | PAIR x y => (denote x, denote y)
       | TT => tt
       end.
Strategy -1000 [denoteT denote].
Fixpoint DUPT (n : nat) (A : type) : type
  := match n with O => UNIT | S n => PROD A (DUPT n A) end.
Fixpoint DUP {A : type} (n : nat) (a : expr A) : expr (DUPT n A) :=
  match n with O => TT | S n => PAIR a (DUP n a) end.
Definition MK_UNIF_L (n : nat)
  := Eval cbv beta iota delta [DUPT DUP dup dupT] in
    denote (let x := Z_DIV_EUCL in DUP n x).
Definition MK_UNIF_R (n : nat)
  := Eval cbv beta iota delta [DUPT DUP dup dupT] in
    (dup n Z.div_eucl).
Notation MK_UNIF n := (match n%nat return _ with n' => ltac:(let n' := (eval cbv in n') in let v := (eval cbv beta iota delta [MK_UNIF_L MK_UNIF_R denoteT] in (MK_UNIF_L n' = MK_UNIF_R n')) in exact v) end) (only parsing).
Ltac MK_UNIF n := constr:(MK_UNIF n).
Ltac CHECK_TIME n := check_time ltac:(MK_UNIF) n.
Timing info 
Goal True.
  CHECK_TIME 40.
  (* n: 1
Tactic call ran for 0.008 secs (0.008u,0.s) (success)
n: 2
Tactic call ran for 0.017 secs (0.017u,0.s) (success)
n: 3
Tactic call ran for 0.031 secs (0.031u,0.s) (success)
n: 4
Tactic call ran for 0.038 secs (0.038u,0.s) (success)
n: 5
Tactic call ran for 0.043 secs (0.043u,0.s) (success)
n: 6
Tactic call ran for 0.045 secs (0.045u,0.s) (success)
n: 7
Tactic call ran for 0.053 secs (0.053u,0.s) (success)
n: 8
Tactic call ran for 0.072 secs (0.072u,0.s) (success)
n: 9
Tactic call ran for 0.075 secs (0.075u,0.s) (success)
n: 10
Tactic call ran for 0.077 secs (0.077u,0.s) (success)
n: 11
Tactic call ran for 0.096 secs (0.096u,0.s) (success)
n: 12
Tactic call ran for 0.103 secs (0.103u,0.s) (success)
n: 13
Tactic call ran for 0.11 secs (0.11u,0.s) (success)
n: 14
Tactic call ran for 0.119 secs (0.119u,0.s) (success)
n: 15
Tactic call ran for 0.133 secs (0.133u,0.s) (success)
n: 16
Tactic call ran for 0.148 secs (0.148u,0.s) (success)
n: 17
Tactic call ran for 0.17 secs (0.17u,0.s) (success)
n: 18
Tactic call ran for 0.162 secs (0.162u,0.s) (success)
n: 19
Tactic call ran for 0.18 secs (0.18u,0.s) (success)
n: 20
Tactic call ran for 0.2 secs (0.2u,0.s) (success)
n: 21
Tactic call ran for 0.22 secs (0.22u,0.s) (success)
n: 22
Tactic call ran for 0.208 secs (0.208u,0.s) (success)
n: 23
Tactic call ran for 0.222 secs (0.222u,0.s) (success)
n: 24
Tactic call ran for 0.218 secs (0.218u,0.s) (success)
n: 25
Tactic call ran for 0.223 secs (0.223u,0.s) (success)
n: 26
Tactic call ran for 0.247 secs (0.247u,0.s) (success)
n: 27
Tactic call ran for 0.233 secs (0.233u,0.s) (success)
n: 28
Tactic call ran for 0.287 secs (0.287u,0.s) (success)
n: 29
Tactic call ran for 0.317 secs (0.317u,0.s) (success)
n: 30
Tactic call ran for 0.284 secs (0.284u,0.s) (success)
n: 31
Tactic call ran for 0.294 secs (0.294u,0.s) (success)
n: 32
Tactic call ran for 0.319 secs (0.319u,0.s) (success)
n: 33
Tactic call ran for 0.308 secs (0.308u,0.s) (success)
n: 34
Tactic call ran for 0.336 secs (0.336u,0.s) (success)
n: 35
Tactic call ran for 0.34 secs (0.34u,0.s) (success)
n: 36
Tactic call ran for 0.358 secs (0.358u,0.s) (success)
n: 37
Tactic call ran for 0.35 secs (0.35u,0.s) (success)
n: 38
Tactic call ran for 0.348 secs (0.348u,0.s) (success)
n: 39
Tactic call ran for 0.39 secs (0.39u,0.s) (success)
n: 40
Tactic call ran for 0.38 secs (0.38u,0.s) (success)
   *)
Abort.

Note that in this version, we have control over Z.div_eucl and how we're managing let binders in let x := Z_DIV_EUCL in DUP n x, but don't have much control over how denote gives us Z_div_eucl_unfolded nor the contents of Z_div_eucl_unfolded nor (the unfolded) DUP, dup, etc. So we could, e.g., mark denote as an identifier whose conversions should be cached, or wrap cache_this around Z_DIV_EUCL or around the uses of the let-bound x, or around Z.div_eucl in dup n Z.div_eucl, but we can't really insert "cache this" in the middle of denote at only the Z_DIV_EUCL branch.

Coq Version

8.17+alpha
@JasonGross JasonGross added kind: performance Improvements to performance and efficiency. part: kernel labels Oct 4, 2022
@JasonGross JasonGross mentioned this issue Oct 4, 2022
Closed
@ppedrot
Copy link
Member

ppedrot commented Oct 4, 2022

AFAICT, what takes time on your example is not conversion, it's just all the reductions and normalization performed by the pretyping algorithm. In particular, we call nf_evars on the resulting term which is huge.

@JasonGross
Copy link
Member Author

Surely the CHECK_TIME example with denote is not spending much time in pretyping? What's the huge term there?

@JasonGross
Copy link
Member Author

If we look only at the time it takes to execute abstract, which presumably is not about pretyping (right?), we see that changing the definition of denote from using Z_div_eucl_unfolded to using Z.div_eucl (this change does not show up anywhere in the initial nor final term, I believe), we get a 10x speedup in abstract:

code and timing 
Require Import Coq.ZArith.ZArith.
Set Debug "Cbv".
Definition Z_div_eucl_unfolded := Eval cbv in Z.div_eucl.
(* Take output, run through `grep -o 'Unfolding [^ ]*$' | grep -o '[^ ]*$' | sort | uniq` *)
Strategy -10 [Coq.Init.Datatypes.CompOpp
Coq.PArith.BinPos.Pos.add
Coq.PArith.BinPos.Pos.compare
Coq.PArith.BinPos.Pos.compare_cont
Coq.PArith.BinPos.Pos.mul
Coq.PArith.BinPos.Pos.pred_double
Coq.PArith.BinPos.Pos.succ
Coq.ZArith.BinInt.Z.add
Coq.ZArith.BinInt.Z.compare
Coq.ZArith.BinInt.Z.div_eucl
Coq.ZArith.BinInt.Z.double
Coq.ZArith.BinInt.Z.leb
Coq.ZArith.BinInt.Z.ltb
Coq.ZArith.BinInt.Z.mul
Coq.ZArith.BinInt.Z.opp
Coq.ZArith.BinInt.Z.pos_div_eucl
Coq.ZArith.BinInt.Z.pos_sub
Coq.ZArith.BinInt.Z.pred_double
Coq.ZArith.BinInt.Z.sub
Coq.ZArith.BinInt.Z.succ_double].
Strategy -10 [Z_div_eucl_unfolded].
Set Debug "-Cbv".

Fixpoint dupT (n : nat) (A : Set) : Set
  := match n with O => unit | S n => A * dupT n A end.
Fixpoint dup {A : Set} (n : nat) (a : A) : dupT n A :=
  match n with O => tt | S n => (a, dup n a) end.


Inductive type := BASE | UNIT | PROD (A B : type).
Fixpoint denoteT (t : type) : Set
  := match t with
     | UNIT => unit
     | BASE => Z -> Z -> Z * Z
     | PROD A B => denoteT A * denoteT B
     end.
Inductive expr : type -> Set :=
| Z_DIV_EUCL : expr BASE
| PAIR {A B} : expr A -> expr B -> expr (PROD A B)
| TT : expr UNIT
.
Definition denote
  := Eval cbv delta [Z_div_eucl_unfolded] in
    fix denote {t} (e : expr t) : denoteT t
    := match e with
       | Z_DIV_EUCL => Z_div_eucl_unfolded
       | PAIR x y => (denote x, denote y)
       | TT => tt
       end.
Definition denote'
  := fix denote' {t} (e : expr t) : denoteT t
    := match e with
       | Z_DIV_EUCL => Z.div_eucl
       | PAIR x y => (denote' x, denote' y)
       | TT => tt
       end.
Strategy -1000 [denoteT denote denote'].
Fixpoint DUPT (n : nat) (A : type) : type
  := match n with O => UNIT | S n => PROD A (DUPT n A) end.
Fixpoint DUP {A : type} (n : nat) (a : expr A) : expr (DUPT n A) :=
  match n with O => TT | S n => PAIR a (DUP n a) end.
Definition MK_UNIF_L (n : nat)
  := Eval cbv beta iota delta [DUPT DUP] in
    denote (let x := Z_DIV_EUCL in DUP n x).
Definition MK_UNIF_L' (n : nat)
  := Eval cbv beta iota delta [DUPT DUP] in
    denote' (let x := Z_DIV_EUCL in DUP n x).
Definition MK_UNIF_R (n : nat)
  := Eval cbv beta iota delta [DUPT DUP dup dupT] in
    (dup n Z.div_eucl).
Notation MK_UNIF n := (match n%nat return _ with n' => ltac:(let n' := (eval cbv in n') in let v := (eval cbv beta iota delta [MK_UNIF_L MK_UNIF_R denoteT] in (MK_UNIF_L n' = MK_UNIF_R n')) in exact v) end) (only parsing).
Notation MK_UNIF' n := (match n%nat return _ with n' => ltac:(let n' := (eval cbv in n') in let v := (eval cbv beta iota delta [MK_UNIF_L' MK_UNIF_R denoteT] in (MK_UNIF_L' n' = MK_UNIF_R n')) in exact v) end) (only parsing).
Ltac check_time mk_unif n :=
  lazymatch n with
  | O => idtac
  | S ?n'
    => check_time mk_unif n';
       idtac "n:" n;
       let ty := mk_unif n in
       let __ := constr:(ltac:(cut True; [ intros _; abstract (cut True; [ intros _; time "reflexivity" reflexivity | restart_timer; exact I ]) | finish_timing ( "Tactic call abstract" ); exact I ]) : ty) in
       idtac
  end.
Ltac MK_UNIF n := constr:(MK_UNIF n).
Ltac MK_UNIF' n := constr:(MK_UNIF' n).
Ltac CHECK_TIME n := check_time ltac:(MK_UNIF) n.
Ltac CHECK_TIME' n := check_time ltac:(MK_UNIF') n.
Goal True.
  CHECK_TIME 50.
  (* n: 1
Tactic call reflexivity ran for 0.009 secs (0.009u,0.s) (success)
Tactic call abstract ran for 0.009 secs (0.009u,0.s)
n: 2
Tactic call reflexivity ran for 0.024 secs (0.024u,0.s) (success)
Tactic call abstract ran for 0.018 secs (0.018u,0.s)
n: 3
Tactic call reflexivity ran for 0.047 secs (0.047u,0.s) (success)
Tactic call abstract ran for 0.025 secs (0.025u,0.s)
n: 4
Tactic call reflexivity ran for 0.04 secs (0.04u,0.s) (success)
Tactic call abstract ran for 0.049 secs (0.049u,0.s)
n: 5
Tactic call reflexivity ran for 0.114 secs (0.114u,0.s) (success)
Tactic call abstract ran for 0.052 secs (0.052u,0.s)
n: 6
Tactic call reflexivity ran for 0.116 secs (0.116u,0.s) (success)
Tactic call abstract ran for 0.08 secs (0.08u,0.s)
n: 7
Tactic call reflexivity ran for 0.069 secs (0.069u,0.s) (success)
Tactic call abstract ran for 0.058 secs (0.058u,0.s)
n: 8
Tactic call reflexivity ran for 0.094 secs (0.094u,0.s) (success)
Tactic call abstract ran for 0.099 secs (0.099u,0.s)
n: 9
Tactic call reflexivity ran for 0.086 secs (0.086u,0.s) (success)
Tactic call abstract ran for 0.077 secs (0.077u,0.s)
n: 10
Tactic call reflexivity ran for 0.097 secs (0.097u,0.s) (success)
Tactic call abstract ran for 0.085 secs (0.085u,0.s)
n: 11
Tactic call reflexivity ran for 0.108 secs (0.108u,0.s) (success)
Tactic call abstract ran for 0.091 secs (0.091u,0.s)
n: 12
Tactic call reflexivity ran for 0.125 secs (0.125u,0.s) (success)
Tactic call abstract ran for 0.119 secs (0.119u,0.s)
n: 13
Tactic call reflexivity ran for 0.149 secs (0.149u,0.s) (success)
Tactic call abstract ran for 0.116 secs (0.116u,0.s)
n: 14
Tactic call reflexivity ran for 0.134 secs (0.134u,0.s) (success)
Tactic call abstract ran for 0.117 secs (0.117u,0.s)
n: 15
Tactic call reflexivity ran for 0.149 secs (0.149u,0.s) (success)
Tactic call abstract ran for 0.134 secs (0.134u,0.s)
n: 16
Tactic call reflexivity ran for 0.153 secs (0.153u,0.s) (success)
Tactic call abstract ran for 0.135 secs (0.135u,0.s)
n: 17
Tactic call reflexivity ran for 0.192 secs (0.192u,0.s) (success)
Tactic call abstract ran for 0.174 secs (0.174u,0.s)
n: 18
Tactic call reflexivity ran for 0.181 secs (0.181u,0.s) (success)
Tactic call abstract ran for 0.168 secs (0.168u,0.s)
n: 19
Tactic call reflexivity ran for 0.195 secs (0.195u,0.s) (success)
Tactic call abstract ran for 0.17 secs (0.17u,0.s)
n: 20
Tactic call reflexivity ran for 0.201 secs (0.201u,0.s) (success)
Tactic call abstract ran for 0.205 secs (0.205u,0.s)
n: 21
Tactic call reflexivity ran for 0.254 secs (0.254u,0.s) (success)
Tactic call abstract ran for 0.205 secs (0.205u,0.s)
n: 22
Tactic call reflexivity ran for 0.215 secs (0.215u,0.s) (success)
Tactic call abstract ran for 0.19 secs (0.19u,0.s)
n: 23
Tactic call reflexivity ran for 0.226 secs (0.226u,0.s) (success)
Tactic call abstract ran for 0.224 secs (0.224u,0.s)
n: 24
Tactic call reflexivity ran for 0.242 secs (0.242u,0.s) (success)
Tactic call abstract ran for 0.209 secs (0.209u,0.s)
n: 25
Tactic call reflexivity ran for 0.231 secs (0.231u,0.s) (success)
Tactic call abstract ran for 0.236 secs (0.236u,0.s)
n: 26
Tactic call reflexivity ran for 0.273 secs (0.273u,0.s) (success)
Tactic call abstract ran for 0.252 secs (0.252u,0.s)
n: 27
Tactic call reflexivity ran for 0.259 secs (0.259u,0.s) (success)
Tactic call abstract ran for 0.286 secs (0.286u,0.s)
n: 28
Tactic call reflexivity ran for 0.434 secs (0.417u,0.017s) (success)
Tactic call abstract ran for 0.346 secs (0.346u,0.s)
n: 29
Tactic call reflexivity ran for 0.371 secs (0.371u,0.s) (success)
Tactic call abstract ran for 0.423 secs (0.423u,0.s)
n: 30
Tactic call reflexivity ran for 0.561 secs (0.531u,0.029s) (success)
Tactic call abstract ran for 0.404 secs (0.384u,0.02s)
n: 31
Tactic call reflexivity ran for 0.433 secs (0.433u,0.s) (success)
Tactic call abstract ran for 0.382 secs (0.382u,0.s)
n: 32
Tactic call reflexivity ran for 0.411 secs (0.411u,0.s) (success)
Tactic call abstract ran for 0.409 secs (0.399u,0.009s)
n: 33
Tactic call reflexivity ran for 0.426 secs (0.426u,0.s) (success)
Tactic call abstract ran for 0.363 secs (0.363u,0.s)
n: 34
Tactic call reflexivity ran for 0.395 secs (0.395u,0.s) (success)
Tactic call abstract ran for 0.441 secs (0.441u,0.s)
n: 35
Tactic call reflexivity ran for 0.507 secs (0.507u,0.s) (success)
Tactic call abstract ran for 0.375 secs (0.375u,0.s)
n: 36
Tactic call reflexivity ran for 0.463 secs (0.463u,0.s) (success)
Tactic call abstract ran for 0.696 secs (0.696u,0.s)
n: 37
Tactic call reflexivity ran for 0.455 secs (0.445u,0.009s) (success)
Tactic call abstract ran for 0.391 secs (0.391u,0.s)
n: 38
Tactic call reflexivity ran for 0.384 secs (0.384u,0.s) (success)
Tactic call abstract ran for 0.34 secs (0.34u,0.s)
n: 39
Tactic call reflexivity ran for 0.396 secs (0.396u,0.s) (success)
Tactic call abstract ran for 0.385 secs (0.375u,0.009s)
n: 40
Tactic call reflexivity ran for 0.39 secs (0.39u,0.s) (success)
Tactic call abstract ran for 0.457 secs (0.457u,0.s)
n: 41
Tactic call reflexivity ran for 0.473 secs (0.473u,0.s) (success)
Tactic call abstract ran for 0.371 secs (0.371u,0.s)
n: 42
Tactic call reflexivity ran for 0.409 secs (0.409u,0.s) (success)
Tactic call abstract ran for 0.409 secs (0.409u,0.s)
n: 43
Tactic call reflexivity ran for 0.453 secs (0.453u,0.s) (success)
Tactic call abstract ran for 0.39 secs (0.39u,0.s)
n: 44
Tactic call reflexivity ran for 0.482 secs (0.482u,0.s) (success)
Tactic call abstract ran for 0.383 secs (0.383u,0.s)
n: 45
Tactic call reflexivity ran for 0.438 secs (0.438u,0.s) (success)
Tactic call abstract ran for 0.44 secs (0.44u,0.s)
n: 46
Tactic call reflexivity ran for 0.527 secs (0.527u,0.s) (success)
Tactic call abstract ran for 0.577 secs (0.577u,0.s)
n: 47
Tactic call reflexivity ran for 0.519 secs (0.519u,0.s) (success)
Tactic call abstract ran for 0.417 secs (0.417u,0.s)
n: 48
Tactic call reflexivity ran for 0.508 secs (0.508u,0.s) (success)
Tactic call abstract ran for 0.419 secs (0.419u,0.s)
n: 49
Tactic call reflexivity ran for 0.482 secs (0.482u,0.s) (success)
Tactic call abstract ran for 0.514 secs (0.475u,0.039s)
n: 50
Tactic call reflexivity ran for 0.572 secs (0.532u,0.04s) (success)
Tactic call abstract ran for 0.573 secs (0.533u,0.04s)
   *)
  CHECK_TIME' 50.
  (* n: 1
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0. secs (0.u,0.s)
n: 2
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0. secs (0.u,0.s)
n: 3
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0. secs (0.u,0.s)
n: 4
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0. secs (0.u,0.s)
n: 5
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0. secs (0.u,0.s)
n: 6
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0.001 secs (0.001u,0.s)
n: 7
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.002 secs (0.002u,0.s)
n: 8
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0.002 secs (0.002u,0.s)
n: 9
Tactic call reflexivity ran for 0. secs (0.u,0.s) (success)
Tactic call abstract ran for 0.002 secs (0.002u,0.s)
n: 10
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.003 secs (0.003u,0.s)
n: 11
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.003 secs (0.003u,0.s)
n: 12
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.005 secs (0.005u,0.s)
n: 13
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.004 secs (0.004u,0.s)
n: 14
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.005 secs (0.005u,0.s)
n: 15
Tactic call reflexivity ran for 0.001 secs (0.001u,0.s) (success)
Tactic call abstract ran for 0.004 secs (0.004u,0.s)
n: 16
Tactic call reflexivity ran for 0.003 secs (0.003u,0.s) (success)
Tactic call abstract ran for 0.006 secs (0.006u,0.s)
n: 17
Tactic call reflexivity ran for 0.002 secs (0.002u,0.s) (success)
Tactic call abstract ran for 0.007 secs (0.007u,0.s)
n: 18
Tactic call reflexivity ran for 0.002 secs (0.002u,0.s) (success)
Tactic call abstract ran for 0.008 secs (0.008u,0.s)
n: 19
Tactic call reflexivity ran for 0.002 secs (0.002u,0.s) (success)
Tactic call abstract ran for 0.031 secs (0.011u,0.02s)
n: 20
Tactic call reflexivity ran for 0.002 secs (0.002u,0.s) (success)
Tactic call abstract ran for 0.008 secs (0.008u,0.s)
n: 21
Tactic call reflexivity ran for 0.004 secs (0.004u,0.s) (success)
Tactic call abstract ran for 0.009 secs (0.009u,0.s)
n: 22
Tactic call reflexivity ran for 0.003 secs (0.003u,0.s) (success)
Tactic call abstract ran for 0.011 secs (0.011u,0.s)
n: 23
Tactic call reflexivity ran for 0.003 secs (0.003u,0.s) (success)
Tactic call abstract ran for 0.013 secs (0.013u,0.s)
n: 24
Tactic call reflexivity ran for 0.006 secs (0.006u,0.s) (success)
Tactic call abstract ran for 0.01 secs (0.01u,0.s)
n: 25
Tactic call reflexivity ran for 0.005 secs (0.005u,0.s) (success)
Tactic call abstract ran for 0.014 secs (0.014u,0.s)
n: 26
Tactic call reflexivity ran for 0.007 secs (0.007u,0.s) (success)
Tactic call abstract ran for 0.013 secs (0.013u,0.s)
n: 27
Tactic call reflexivity ran for 0.019 secs (0.009u,0.01s) (success)
Tactic call abstract ran for 0.016 secs (0.016u,0.s)
n: 28
Tactic call reflexivity ran for 0.007 secs (0.007u,0.s) (success)
Tactic call abstract ran for 0.016 secs (0.016u,0.s)
n: 29
Tactic call reflexivity ran for 0.007 secs (0.007u,0.s) (success)
Tactic call abstract ran for 0.018 secs (0.018u,0.s)
n: 30
Tactic call reflexivity ran for 0.006 secs (0.006u,0.s) (success)
Tactic call abstract ran for 0.02 secs (0.02u,0.s)
n: 31
Tactic call reflexivity ran for 0.007 secs (0.007u,0.s) (success)
Tactic call abstract ran for 0.019 secs (0.019u,0.s)
n: 32
Tactic call reflexivity ran for 0.025 secs (0.015u,0.009s) (success)
Tactic call abstract ran for 0.02 secs (0.02u,0.s)
n: 33
Tactic call reflexivity ran for 0.009 secs (0.009u,0.s) (success)
Tactic call abstract ran for 0.023 secs (0.023u,0.s)
n: 34
Tactic call reflexivity ran for 0.008 secs (0.008u,0.s) (success)
Tactic call abstract ran for 0.025 secs (0.025u,0.s)
n: 35
Tactic call reflexivity ran for 0.01 secs (0.01u,0.s) (success)
Tactic call abstract ran for 0.024 secs (0.024u,0.s)
n: 36
Tactic call reflexivity ran for 0.024 secs (0.014u,0.009s) (success)
Tactic call abstract ran for 0.026 secs (0.026u,0.s)
n: 37
Tactic call reflexivity ran for 0.012 secs (0.012u,0.s) (success)
Tactic call abstract ran for 0.028 secs (0.028u,0.s)
n: 38
Tactic call reflexivity ran for 0.012 secs (0.012u,0.s) (success)
Tactic call abstract ran for 0.029 secs (0.029u,0.s)
n: 39
Tactic call reflexivity ran for 0.03 secs (0.02u,0.009s) (success)
Tactic call abstract ran for 0.033 secs (0.033u,0.s)
n: 40
Tactic call reflexivity ran for 0.015 secs (0.015u,0.s) (success)
Tactic call abstract ran for 0.039 secs (0.039u,0.s)
n: 41
Tactic call reflexivity ran for 0.017 secs (0.017u,0.s) (success)
Tactic call abstract ran for 0.049 secs (0.049u,0.s)
n: 42
Tactic call reflexivity ran for 0.04 secs (0.02u,0.019s) (success)
Tactic call abstract ran for 0.048 secs (0.048u,0.s)
n: 43
Tactic call reflexivity ran for 0.022 secs (0.022u,0.s) (success)
Tactic call abstract ran for 0.044 secs (0.043u,0.s)
n: 44
Tactic call reflexivity ran for 0.015 secs (0.015u,0.s) (success)
Tactic call abstract ran for 0.071 secs (0.051u,0.019s)
n: 45
Tactic call reflexivity ran for 0.018 secs (0.018u,0.s) (success)
Tactic call abstract ran for 0.042 secs (0.042u,0.s)
n: 46
Tactic call reflexivity ran for 0.016 secs (0.016u,0.s) (success)
Tactic call abstract ran for 0.072 secs (0.052u,0.019s)
n: 47
Tactic call reflexivity ran for 0.016 secs (0.016u,0.s) (success)
Tactic call abstract ran for 0.047 secs (0.047u,0.s)
n: 48
Tactic call reflexivity ran for 0.018 secs (0.018u,0.s) (success)
Tactic call abstract ran for 0.09 secs (0.049u,0.04s)
n: 49
Tactic call reflexivity ran for 0.02 secs (0.02u,0.s) (success)
Tactic call abstract ran for 0.048 secs (0.048u,0.s)
n: 50
Tactic call reflexivity ran for 0.018 secs (0.018u,0.s) (success)
Tactic call abstract ran for 0.069 secs (0.049u,0.019s)
*)
Abort.

@ppedrot
Copy link
Member

ppedrot commented Oct 4, 2022

In your first example, ty in check_time is bound to a huge term in cases 3 and 4. What exactly are you expecting?

@JasonGross
Copy link
Member Author

I created cases 3 and 4 because I don't fully understand the perfomance behavior of this part of Coq. I'm most interested in the performance of abstract in CHECK_TIME. I'm expecting that there should be a way to make the linear factor in CHECK_TIME and CHECK_TIME' be the same, with only a constant overhead from checking Z.div_eucl against Z_div_eucl_unfolded once. If you want to bench the real example that I'm looking at, I can point you at it

@ppedrot
Copy link
Member

ppedrot commented Oct 4, 2022

OK, so basically you'd like some form of caching of conversion problems, because you'd like to leverage the fact that Coq has already checked that SOMEBIGTERM ≡ Constant. Not sure how to do that efficiently, because on your examples you'd have to recognize these big terms when there is no reason a priori that it's going to be worthwhile to check you've seen them already. Not completely crazy, but I really don't see how you could do that in general.

@JasonGross
Copy link
Member Author

@ppedrot Do we need to recognize the big terms, or just the constants? What about having the ability to add constants to a whitelist so that all conversion problems where either side is the application of a whitelisted constant to one or more other constants gets cached? Then I would either add denote to the whitelist, or else I'd add Z.div_eucl to the whitelist.

Alternatively, there could be a whitelist of constants c such that when facing conversion problems of the form App c args1 = App c args2, the immediate subproblems that arise from converting args1 with args2 get cached. (Importantly, this should happen before attempting to unfold c, even if the strategy level of c is negative.) (I think this form is actually better.) Then I could have denote insert whitelisted identity functions at every node, have reification strip off these functions, and insert them in the term being reified at select places. That is, I could do something like

Require Import Coq.ZArith.ZArith.
Definition Z_div_eucl_unfolded := Eval cbv in Z.div_eucl.
Definition whitelisted_id {A} (x : A) := x.
Fixpoint dupT (n : nat) (A : Set) : Set
  := match n with O => unit | S n => A * dupT n A end.
Fixpoint dup {A : Set} (n : nat) (a : A) : dupT n A :=
  match n with O => tt | S n => (a, dup n a) end.
Inductive type := BASE | UNIT | PROD (A B : type).
Fixpoint denoteT (t : type) : Set
  := match t with
     | UNIT => unit
     | BASE => Z -> Z -> Z * Z
     | PROD A B => denoteT A * denoteT B
     end.
Inductive expr : type -> Set :=
| Z_DIV_EUCL : expr BASE
| PAIR {A B} : expr A -> expr B -> expr (PROD A B)
| TT : expr UNIT
.
Definition denote'
  := Eval cbv delta [Z_div_eucl_unfolded] in
    fix denote {t} (e : expr t) : denoteT t
    := match e with
       | Z_DIV_EUCL => Z_div_eucl_unfolded
       | PAIR x y => (whitelisted_id denote x, whitelisted_id denote y)
       | TT => tt
       end.
Definition denote {t} (e : expr t) := whitelisted_id (denote' e).
Strategy -1000 [denoteT denote denote' whitelisted_id].
Fixpoint DUPT (n : nat) (A : type) : type
  := match n with O => UNIT | S n => PROD A (DUPT n A) end.
Fixpoint DUP {A : type} (n : nat) (a : expr A) : expr (DUPT n A) :=
  match n with O => TT | S n => PAIR a (DUP n a) end.
Definition MK_UNIF_L (n : nat)
  := Eval cbv beta iota delta [DUPT DUP dup dupT] in
    denote (let x := Z_DIV_EUCL in DUP n x).
Definition MK_UNIF_R (n : nat)
  := Eval cbv beta iota delta [DUPT DUP dup dupT] in
    (dup n (whitelisted_id Z.div_eucl)).
Notation MK_UNIF n := (match n%nat return _ with n' => ltac:(let n' := (eval cbv in n') in let v := (eval cbv beta iota delta [MK_UNIF_L MK_UNIF_R denoteT] in (MK_UNIF_L n' = MK_UNIF_R n')) in exact v) end) (only parsing).
Ltac MK_UNIF n := constr:(MK_UNIF n).

What do you think?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: performance Improvements to performance and efficiency. part: kernel
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @ppedrot