Stream: Ltac2

Topic: writing efficient variant of `clear`

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 $\mathcal O((\text{size of context and goal}) \cdot \ln(\text{len}(\text{ids})) + \text{len}(\text{ids})$, not $\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 $\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 $\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?

Gaëtan Gilbert (Jul 23 2022 at 16:51):

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

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.

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

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?

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

Paolo Giarrusso (Jul 23 2022 at 17:12):

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

Paolo Giarrusso (Jul 23 2022 at 17:12):

Not that I get the invariant for ids_to_avoid

Gaëtan Gilbert (Jul 23 2022 at 17:13):

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

Paolo Giarrusso (Jul 23 2022 at 17:14):

ah, it's ids_to_clear intersected with the scope

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

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

Paolo Giarrusso (Jul 23 2022 at 17:15):

(and indeed Jason was using context order)

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)

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

Gaëtan Gilbert (Jul 23 2022 at 17:18):

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

Paolo Giarrusso (Jul 23 2022 at 17:20):

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

Paolo Giarrusso (Jul 23 2022 at 17:22):

OTOH, all_variables () seems Control.hyps ()

Last updated: Oct 13 2024 at 01:02 UTC