meta timeout

Stream: general

[Patrick Massot]

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...)

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

Thanks!

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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