From f41cdc3c72385983e00d91655090d256efedca2c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Oct 2023 15:57:36 +0200 Subject: [PATCH 1/5] 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 483769296..389dc81dc 100644 --- a/README.md +++ b/README.md @@ -126,6 +126,8 @@ all the dependencies installed first (see [coq-elpi.opam](coq-elpi.opam)). 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..f02177fca --- /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 replacing 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 in interesting because it uses the constraint store +to attach data to holes, in particular if the hole has been seen before, +and if so, and 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, + std.spy (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. From 489f888584706dcb3af4c3f4c67ab9b86405c43b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Oct 2023 16:10:30 +0200 Subject: [PATCH 2/5] Update examples/example_abs_evars.v --- examples/example_abs_evars.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v index f02177fca..f37f0eb70 100644 --- a/examples/example_abs_evars.v +++ b/examples/example_abs_evars.v @@ -88,7 +88,7 @@ solve (goal _ _ _ _ [trm T] as G) GL :- 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, - std.spy (refine R G GL). +refine R G GL. }}. Elpi Typecheck. From 2306bfd84b92924d7da6483e108322c4b4c8b5db Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Oct 2023 16:11:13 +0200 Subject: [PATCH 3/5] Update examples/example_abs_evars.v --- examples/example_abs_evars.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v index f37f0eb70..b9ffa72d9 100644 --- a/examples/example_abs_evars.v +++ b/examples/example_abs_evars.v @@ -8,7 +8,7 @@ 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 replacing them by a placeholder to be later abstracted. +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. From e5dc83383364a01fb48c55125c8ca63f3a6c46f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Oct 2023 16:11:34 +0200 Subject: [PATCH 4/5] Update examples/example_abs_evars.v --- examples/example_abs_evars.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v index b9ffa72d9..a4f9940a9 100644 --- a/examples/example_abs_evars.v +++ b/examples/example_abs_evars.v @@ -12,7 +12,7 @@ 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 in interesting because it uses the constraint store +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 if so, and attach to each hole a unique number. From d882ffb8256a5bb36e63228a11d6cee7b1854a60 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Oct 2023 16:12:12 +0200 Subject: [PATCH 5/5] Update examples/example_abs_evars.v --- examples/example_abs_evars.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v index a4f9940a9..f9879ee37 100644 --- a/examples/example_abs_evars.v +++ b/examples/example_abs_evars.v @@ -14,7 +14,7 @@ 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 if so, and attach to each hole a unique number. +and to attach to each hole a unique number. *)