## Stream: general

### Topic: meta timeout

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

#### Simon Hudon (Aug 12 2018 at 23:56):

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

#### 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


#### 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

#### Mario Carneiro (Aug 12 2018 at 23:57):

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

Thanks!

#### Patrick Massot (Aug 13 2018 at 00:00):

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

#### 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

#### Patrick Massot (Aug 13 2018 at 00:04):

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

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

#### 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

#### 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: Dec 20 2023 at 11:08 UTC