Zulip Chat Archive

Stream: Is there code for X?

Topic: a mutable tactic


Kenny Lau (May 16 2020 at 07:42):

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 (May 16 2020 at 07:42):

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

Kenny Lau (May 16 2020 at 07:43):

I imagine I could start by inspect how random works

Kenny Lau (May 16 2020 at 07:44):

this behaviour is also acceptable:

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

Kenny Lau (May 16 2020 at 07:47):

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 (May 16 2020 at 07:48):

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 (May 16 2020 at 07:56):

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

Kenny Lau (May 16 2020 at 07:56):

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

Gabriel Ebner (May 16 2020 at 08:40):

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

Mario Carneiro (May 16 2020 at 08:47):

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

Kenny Lau (May 16 2020 at 09:58):

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 (May 16 2020 at 09:58):

this works perfectly

Kenny Lau (May 16 2020 at 09:58):

thanks to Mario

Kenny Lau (May 16 2020 at 10:07):

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

Kenny Lau (May 16 2020 at 10:07):

this doesn't survive <|>

Kenny Lau (May 16 2020 at 10:09):

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

Kenny Lau (May 16 2020 at 10:09):

this just gives 3 zeroes

Kenny Lau (May 16 2020 at 10:10):

maybe we really need to do some read/write?

Kenny Lau (May 16 2020 at 10:11):

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

Markus Himmel (May 16 2020 at 11:21):

Kenny Lau said:

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

Like tactic.unsafe_run_io?

Kenny Lau (May 16 2020 at 12:09):

seriously it takes more time to hack your kata

Kenny Lau (May 16 2020 at 12:09):

then is it still a hack?


Last updated: Dec 20 2023 at 11:08 UTC