From e5f9a7feca641e31831718432ea19b71308ce036 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 9 Oct 2023 16:12:38 +0200
Subject: [PATCH] example: abstract holes (#514)

example: abstract holes
---
 README.md                    |   2 +
 _CoqProject.examples         |   1 +
 examples/example_abs_evars.v | 117 +++++++++++++++++++++++++++++++++++
 3 files changed, 120 insertions(+)
 create mode 100644 examples/example_abs_evars.v

diff --git a/README.md b/README.md
index 92869edfa..1b48bc400 100644
--- a/README.md
+++ b/README.md
@@ -130,6 +130,8 @@ and `ocaml-lsp-server` (version 1.15).
   simple tactics by using (proof) terms and the elaborator of Coq
 - [generalize](examples/example_generalize.v) show how to abstract
   subterms out (one way to skin the cat, there are many)
+- [abs_evars](examples/example_abs_evars.v) show how to close a term
+  containing holes (evars) with binders
 - [record import](examples/example_import_projections.v) gives short names
   to record projections applied to the given record instance.
 - [reduction surgery](examples/example_reduction_surgery.v) implements
diff --git a/_CoqProject.examples b/_CoqProject.examples
index e927100fb..9a8173fb8 100644
--- a/_CoqProject.examples
+++ b/_CoqProject.examples
@@ -21,3 +21,4 @@ examples/example_fuzzer.v
 examples/example_generalize.v
 examples/example_import_projections.v
 examples/example_reduction_surgery.v
+examples/example_abs_evars.v
diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v
new file mode 100644
index 000000000..f9879ee37
--- /dev/null
+++ b/examples/example_abs_evars.v
@@ -0,0 +1,117 @@
+From elpi Require Import elpi.
+
+(** Closing a term with holes with binders *)
+
+(*
+
+The operation consists in replacing all occurrences of the same hole
+in a term by a bound variable.
+
+We first traverse the term and count how many distinct hole are there
+and replace them by a placeholder to be later abstracted.
+Once we know how many binders we need, we generate the spine of binders
+and replace the placeholders by the bound variables.
+
+This example is interesting because it uses the constraint store
+to attach data to holes, in particular if the hole has been seen before,
+and to attach to each hole a unique number.
+
+*)
+
+Elpi Tactic abs_evars.
+Elpi Accumulate lp:{{
+
+% we add a new constructor to terms to represent terms to be abstracted
+type abs int -> term.
+
+% bind back abstracted subterms
+pred bind i:int, i:int, i:term, o:term.
+bind I M T T1 :- M > I, !,
+  T1 = {{ forall x, lp:(B x) }},   
+  N is I + 1,
+  pi x\                           % we allocate the fresh symbol for (abs M)
+    (copy (abs N) x :- !) =>      % we schedule the replacement (abs M) -> x
+    bind N M T (B x).
+bind M M T T1 :- copy T T1.         % we perform all the replacements
+
+% for a term with M holes, returns a term with M variables to fill these holes
+% the clause see is only generated for a term if it hasn't been seen before
+% the term might need to be typechecked first or main generates extra holes for the
+% type of the parameters
+pred abs-evars i:term, o:term, o:int.
+abs-evars T1 T3 M :- std.do! [
+  % we put (abs N) in place of each occurrence of the same hole
+  (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen? T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, seen! T M) =>
+  (pi T N M \ fold-map T N (abs M) N :- var T, seen? T M, !) =>
+    fold-map T1 0 T2 M,
+  % we abstract M holes (M abs nodes)
+  bind 0 M T2 T3,
+  % cleanup constraint store
+  purge-seen!,
+].
+
+% all constraints are also on _ so that they share
+% a variable with the constraint to purge the store
+
+% we query if the hole was seen before, and if so
+% we fetch its number
+pred seen? i:term, o:int.
+seen? X Y :- declare_constraint (seen? X Y) [X,_].  
+
+% we declare it is now seen and label it with a number
+pred seen! i:term, i:int.
+seen! X Y :- declare_constraint (seen! X Y) [X,_].
+
+% to empty the store
+pred purge-seen!.
+purge-seen! :- declare_constraint purge-seen! [_].
+
+constraint seen? seen! purge-seen!  {
+  % a succesful query, give the label back via M
+  rule (seen! X N) \ (seen? X M) <=> (M = N).
+  % an unsuccesful query
+  rule             \ (seen? X _) <=> false.
+
+  rule purge-seen! \ (seen! _ _).
+  rule \ purge-seen!.
+}
+
+% if we pass an argument this is what we use to refine the goal
+solve (goal _ _ _ _ [trm T] as G) GL :-
+  std.assert-ok! (coq.elaborate-ty-skeleton T _ T1) "illtyped",
+  std.assert! (abs-evars T1 ClosedT1 _) "closure fails",
+  refine ClosedT1 G GL.
+
+% if we pass no argument, then we abstract the goal.
+% the first subgoal is a proof of the abstracted goal, while
+% the other goals are for the abstracted premises
+solve (goal _ _ T _ [] as G) GL :-
+  std.assert! (abs-evars T ClosedT N) "closure fails",
+  coq.mk-app {{ (fun x : lp:ClosedT => x) _ }} {coq.mk-n-holes N} R,
+refine R G GL.
+
+}}.
+Elpi Typecheck.
+Elpi Export abs_evars.
+
+Fail Lemma test : forall x, x = x.
+Lemma test : abs_evars (forall x, x = x).
+intros t x; reflexivity.
+Abort.
+
+Lemma test : abs_evars (forall x y, x = y).
+intros t x y; symmetry.
+Abort.
+
+Lemma test : True.
+assert (abs_evars (tt = _)) as H.
+  intro x; destruct x; reflexivity.
+Abort.
+
+Lemma test : exists x, x = tt.
+econstructor.
+(* it is silly, but shows the code above performs the abstraction *)
+elpi abs_evars.
+  now intros [].
+exact tt.
+Qed.