help with `has_to_pexpr`

Stream: general

[Scott Morrison]

I'm not sure how to construct has_to_pexpr instances, and there are few useful examples around. In particular, I'd like to make the following work:

import tactic

open tactic

meta instance nat_pexpr : has_to_pexpr ℕ := ⟨pexpr.of_expr ∘ λ n, reflect n⟩
meta instance int_pexpr : has_to_pexpr ℤ := ⟨pexpr.of_expr ∘ λ n, reflect n⟩

meta def turkle (p : ℕ) : tactic unit :=
do M ← to_expr ``(2^%%p - 1 : ℤ) >>= eval_expr ℤ,
   t ← to_expr ``(2^%%p - 1 = %%M),
   v ← to_expr ``(by norm_num : 2^%%p - 1 = %%M),
   assertv `w t v,
   skip

example : true :=
begin
  turkle 5,
  -- This produces `w : 2^5 - 1 = int.of_nat 31`,
  -- but I want:
  guard_hyp w := 2^5 - 1 = (31 : ℤ),
  trivial,
end

[Scott Morrison]

I guess this is the int_pexpr instance's fault, but I don't know what to replace it with.

[Scott Morrison]

Oh... maybe I undestand. I just have to calculate the binary digits of my integer, and build the pexpr out of bit0 and bit1 directly? (And put in a negative sign if the integer is negative...)

[Scott Morrison]

Does this exist somewhere already? It seems like the sort of thing that someone would have wanted before me.

[Scott Morrison]

Alternatively, adding `[simp at w] at the end of turkle achieves the desired result, so I'm going to leave this for now.

[Reid Barton]

Presumably whatever is building int.of_nat 31 already knows how to do the bit0/bit1 part.

[Simon Hudon]

You may want to look at the has_reflect instance for nat. I believe that's where the bit0 / bit1 logic is. My guess is that has_reflect on int is done by pattern matching on the int, reflecting the nat and then applying the constructor. Instead, you can treat the int as a number in its own right and do the binary division and add a minus when necessary

[Mario Carneiro]

the eval_expr on the first line is completely unnecessary, just do let M := 2^p-1