Section variable leak

[Tragicus]

It is possible to make clauses using section variables survive the end of the section, contrary to what is stated in the documentation of coq.elpi.accumulate.

From elpi Require Import elpi.

Elpi Command cmd.
Elpi Db db lp:{{
pred db? o:term.
}}.

Elpi Accumulate Db db.

#[synterp]
Elpi Accumulate cmd lp:{{
main _ :-
  coq.env.begin-section "Dummy",
  coq.env.end-section.
}}.
Elpi Accumulate cmd lp:{{
main _ :-
  coq.env.begin-section "Dummy",
  coq.env.add-section-variable "T" _ {{ Type }} T,
  coq.elpi.accumulate _ "db" (clause _ _ (db? (global (const T)))),
  coq.env.end-section.
}}.

Elpi cmd.

Section Dummy.
Variable (T U : Type).

Elpi Query cmd lp:{{
db? {{ T }}.
}}.

Fail Elpi Query cmd lp:{{
db? {{ U }}.
}}.

End Dummy.

[gares]

Arrghhh!

[gares]

The bug must be here:

coq-elpi/src/rocq_elpi_HOAS.ml

Lines 548 to 558 in b1933bc

	let collect_term_variables ~depth t =
	let rec aux ~depth acc t =
	match E.look ~depth t with
	| E.CData c when isconstant c ->
	begin match constantout c with
	| Variable id -> id :: acc
	| _ -> acc
	end
	| x -> fold_elpi_term aux acc ~depth x
	in
	aux ~depth [] t

coq-elpi/src/rocq_elpi_utils.ml

Lines 300 to 308 in b1933bc

	let fold_elpi_term f acc ~depth t =
	let module E = Elpi.API.RawData in
	match t with
	| E.Const _ | E.Nil | E.CData _ -> acc
	| E.App (_, x, xs) -> List.fold_left (f ~depth) (f ~depth acc x) xs
	| E.Cons (x, xs) -> f ~depth (f ~depth acc x) xs
	| E.Builtin (_, xs) -> List.fold_left (f ~depth) acc xs
	| E.Lam x -> f ~depth:(depth + 1) acc x
	| E.UnifVar (_, xs) -> List.fold_left (f ~depth) acc xs

[gares]

Oh... now I see the bug. The problem is that the section is closed while the program runs, but clauses are accumulated after the facts. One should check if their vs are still there, else discard them.