a mutable tactic

Stream: Is there code for X?

[Kenny Lau]

is it possible to write a tactic:

meta def increment : tactic unit :=

such that every time I do #eval by increment it prints 0 and then 1 and then 2 etc?

[Kenny Lau]

#eval by increment -- 0
#eval by increment -- 1
#eval by increment -- 2

[Kenny Lau]

I imagine I could start by inspect how random works

[Kenny Lau]

this behaviour is also acceptable:

#eval by {increment, increment, increment} -- 0 \n 1 \n 2

[Kenny Lau]

Kenny Lau said:

I imagine I could start by inspect how random works

welp I'm out of luck as I've hit the constant wall

[Kenny Lau]

I imagine I could also use the help of an outside file, if I've resolved the issue of not being able to open files

[Kenny Lau]

it doesn't have to go on forever, e.g. by reading a file that basically contains 0\n1\n2\n3\n4

[Kenny Lau]

then it's basically "read the next line" tactic

[Gabriel Ebner]

You could use user_attribute to set (and modify) an attribute on the increment declaration.

[Mario Carneiro]

is there an approach with less performance cost than this? Particularly when the object being stored is large

[Kenny Lau]

meta def hack : list expr :=
[`(42), `(57)]

@[user_attribute]
meta def incr_attr : user_attribute unit ℕ :=
{ name   := `incrementer,
  descr  := "incrementer",
  parser := pure 0 }

open tactic
meta def increment : tactic unit :=
do n ← incr_attr.get_param `increment <|> pure 0,
  e ← hack.nth (n % 2),
  tactic.exact e,
  incr_attr.set `increment (n+1) tt

def test0 : ℕ := by increment
def test1 : ℕ := by increment
def test2 : ℕ := by increment
def test3 : ℕ := by increment
#print test0 -- 42
#print test1 -- 57
#print test2 -- 42
#print test3 -- 57

[Kenny Lau]

this works perfectly

[Kenny Lau]

thanks to Mario

[Kenny Lau]

@Mario Carneiro is there a way to change the environment permanently?

[Kenny Lau]

this doesn't survive <|>

[Kenny Lau]

lemma test : true :=
by rw [by increment] <|> rw [by increment] <|> rw [by increment]

[Kenny Lau]

this just gives 3 zeroes

[Kenny Lau]

maybe we really need to do some read/write?

[Kenny Lau]

but then we would need some way to pass from io to tactic

[Markus Himmel]

Kenny Lau said:

but then we would need some way to pass from io to tactic

Like tactic.unsafe_run_io?

[Kenny Lau]

seriously it takes more time to hack your kata

[Kenny Lau]

then is it still a hack?