Zulip Chat Archive

Stream: general

Topic: meta timeout


view this post on Zulip Patrick Massot (Aug 12 2018 at 23:47):

I'm still playing with Lean introspection, but I can't sort declarations in order to print first axioms, then constants, then definition, and then theorems. I try

meta def declaration_kind_nb : declaration  
| (ax _ _ _) := 1
| (cnst _ _ _ _) := 2
| (defn _ _ _ _ _ _) := 3
| (thm _ _ _ _) := 4

meta def declaration_compare (d d' : declaration) := declaration_kind_nb d  declaration_kind_nb d'

meta instance : decidable_rel declaration_compare :=
by tauto

meta def sort_env : tactic unit :=
do curr_env  get_env,
   let decls := curr_env.fold [] list.cons,
   trace ((list.merge_sort declaration_compare decls).map (to_string  to_name))

and get either determistic timeout or worse (excessive memory consumption, segfault...)

view this post on Zulip Simon Hudon (Aug 12 2018 at 23:56):

What if you print only the length of the resulting list?

view this post on Zulip Mario Carneiro (Aug 12 2018 at 23:56):

this works for me:

meta instance : decidable_rel declaration_compare :=
λ _ _, nat.decidable_le _ _

meta def sort_env : tactic unit :=
do curr_env ← get_env,
   let decls := curr_env.fold [] list.cons,
   (list.merge_sort declaration_compare decls).mmap' (trace ∘ to_name)

run_cmd sort_env

view this post on Zulip Mario Carneiro (Aug 12 2018 at 23:57):

the problem is that the format instance for list string involves a recursion, so it is very deeply nested and hits the recursion limit

view this post on Zulip Mario Carneiro (Aug 12 2018 at 23:57):

(this is why TCO is important in functional programming languages)

view this post on Zulip Patrick Massot (Aug 12 2018 at 23:58):

Thanks!

view this post on Zulip Patrick Massot (Aug 13 2018 at 00:00):

Is there a more natural way to do define that comparison function?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 00:03):

Not particularly; you could do a cases on both and return true or false in each case

view this post on Zulip Patrick Massot (Aug 13 2018 at 00:04):

This was my original plan, but I decided there were too many cases

view this post on Zulip Mario Carneiro (Aug 13 2018 at 00:05):

this is a legitimate way to cut down the number of cases from O(n^2) to O(n)

view this post on Zulip Mario Carneiro (Aug 13 2018 at 00:06):

I wish there was a built in (autogenerated) T.discr function that returns the discriminant of the type, which is basically this

view this post on Zulip Mario Carneiro (Aug 13 2018 at 00:07):

it has an O(1) implementation, since this is the tag on the vm object


Last updated: May 13 2021 at 20:13 UTC