Stream: Ltac2

Topic: writing efficient variant of `clear`


view this post on Zulip Jason Gross (Jul 23 2022 at 16:46):

I want a variant of Std.clear : ident list -> unit which is equivalent to progress (List.iter (fun id => try (Std.clear [id])) ids) (or it can iter on List.rev ids, whichever order Std.clear uses), except that I want it to only walk the context and goal a constant number of times. That is, performance should be at worst O((size of context and goal)ln(len(ids))+len(ids)\mathcal O((\text{size of context and goal}) \cdot \ln(\text{len}(\text{ids})) + \text{len}(\text{ids}), not O((size of context and goal)len(ids)\mathcal O((\text{size of context and goal}) \cdot \text{len}(\text{ids}). The obvious way to do this is something like:

  1. let ids_to_clear := hash set of ids
  2. walk the goal; for each ident id that shows up in the goal:
    a. if ids_to_clear is empty, bail early
    b. if id is in ids_to_clear, remove it

  3. let ids_to_avoid := ids_to_clear

  4. for each hypothesis h in the context, from bottom to top / inside to outside:
    a. if ids_to_avoid is empty, bail early
    b. if h is in ids_to_avoid, remove h from ids_to_avoid, continue to next iteration
    c. walk the body and type of h; for each ident id that shows up:
    i. if ids_to_avoid is empty, bail early
    ii. if id is in ids_to_avoid, remove it from both ids_to_clear and ids_to_avoid

  5. clear ids_to_clear, failing if ids_to_clear is empty

In English, this should first remove any ids that show up in the goal, incurring O((size of goal)(hash set lookup cost))\mathcal O((\text{size of goal})\cdot (\text{hash set lookup cost})) cost (and the lookup cost in the hash set should be at most O(ln(len(ids)))\mathcal O(\ln(\text{len}(\text{ids})))). Then it should traverse the context from bottom to top, removing any ids that show up in something not being cleared.

However, I'm concerned about the interpretation overhead of walking the goal and context in Ltac2 rather than OCaml (should I be?), and, moreover, I don't see any way to get a hashset of Ids without manually building it myself by converting ids to strings and hashing them myself, and this seems like it'd be pretty slow.

Any tips? / Can we get a hash set of ident primitively in Ltac2?

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 16:51):

can you be clearer about what the difference with the existing clear should be?

view this post on Zulip Jason Gross (Jul 23 2022 at 16:52):

clear H1 H2 fails if either H1 or H2 cannot be cleared without breaking typing. try clear H1 H2 will either clear all hypotheses, or none of them. I want a version that clears the maximal subset of the listed hypotheses, failing only if none of them can be cleared.

view this post on Zulip Jason Gross (Jul 23 2022 at 16:54):

(Hrm, I guess there's also the issue that it's hard to check whether or not the well-typedness of an evar relies on having a particular variable accessible... I guess there should be a separate pass that collects the evars, deduplicates them (is there a fast equality check on evar instances?), and does occurrence checks on clearing the relevant bits of the evar's instance? Is there even a way to get the type of an evar and the types of its instance in Ltac2?)

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:11):

if id is in ids_to_clear, remove it

remove it from ids_to_clear, not clear it, right?

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 17:11):

so if H2 depends on H1 or H1 depends on H2 and clear H1 H2 would succeed you want both cleared? so it can't be implemented as an iter on the input order or its reverse

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:12):

That's why 4 is looping on the context from bottom to top, right?

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:12):

Not that I get the invariant for ids_to_avoid

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 17:13):

I'm not looking at the bullet points, they don't matter

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:14):

ah, it's ids_to_clear intersected with the scope

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 17:14):

clear is implemented in ocaml, I don't know why you would want to implement the variant in ltac2

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:15):

in any case: yes, it can't iterate on hypotheses using the input order, it needs the context order

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:15):

(and indeed Jason was using context order)

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 17:16):

it seems like what you want is something like clear_variant ids := ltac1:(clear - (all variables - ids)) (pseudocode)

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 17:17):

ie Ltac2 clear_variant ids := Std.keep (List.filter (fun id => not (List.mem id ids)) (all_variables ()))

view this post on Zulip Gaëtan Gilbert (Jul 23 2022 at 17:18):

so you just need to implement all_variables and you're done

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:20):

(that) List.filter's still quadratic, so that still needs an actual hash?

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 17:22):

OTOH, all_variables () seems Control.hyps ()


Last updated: Jan 31 2023 at 11:01 UTC