Zulip Chat Archive

Stream: Is there code for X?

Topic: a mutable tactic


view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 16 2020 at 07:42):

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

view this post on Zulip Kenny Lau (May 16 2020 at 07:43):

I imagine I could start by inspect how random works

view this post on Zulip Kenny Lau (May 16 2020 at 07:44):

this behaviour is also acceptable:

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 16 2020 at 07:56):

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

view this post on Zulip Gabriel Ebner (May 16 2020 at 08:40):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 16 2020 at 09:58):

this works perfectly

view this post on Zulip Kenny Lau (May 16 2020 at 09:58):

thanks to Mario

view this post on Zulip Kenny Lau (May 16 2020 at 10:07):

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

view this post on Zulip Kenny Lau (May 16 2020 at 10:07):

this doesn't survive <|>

view this post on Zulip Kenny Lau (May 16 2020 at 10:09):

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

view this post on Zulip Kenny Lau (May 16 2020 at 10:09):

this just gives 3 zeroes

view this post on Zulip Kenny Lau (May 16 2020 at 10:10):

maybe we really need to do some read/write?

view this post on Zulip Kenny Lau (May 16 2020 at 10:11):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 16 2020 at 12:09):

seriously it takes more time to hack your kata

view this post on Zulip Kenny Lau (May 16 2020 at 12:09):

then is it still a hack?


Last updated: May 07 2021 at 21:10 UTC