From 2f1e02da9cd3c5e7f4bd87535ffac6decb9749a5 Mon Sep 17 00:00:00 2001 From: gares Date: Thu, 19 Sep 2024 13:51:27 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20LPCIC/co?= =?UTF-8?q?q-elpi@63623cfd725bf9048a2ae37cc4178cc23e249919=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- stlc.html | 2 +- tutorial_coq_elpi_HOAS.html | 58 ++++++++++++------------- tutorial_coq_elpi_command.html | 78 +++++++++++++++++----------------- tutorial_coq_elpi_tactic.html | 70 +++++++++++++++--------------- tutorial_elpi_lang.html | 34 +++++++-------- 5 files changed, 121 insertions(+), 121 deletions(-) diff --git a/stlc.html b/stlc.html index e037d8ed5..fcd2b2df5 100644 --- a/stlc.html +++ b/stlc.html @@ -133,7 +133,7 @@

stlc.html

File "coq-builtin.elpi", line 1547, column 0, character 63029:
coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,
coq.reduction.vm.norm T TY R
coq.reduction.vm.whd_all T TY R
File "coq-builtin.elpi", line 1554, column 0, character 63263:
get-option coq:redflags coq.redflags.all ⇒ 
coq.reduction.lazy.whd X Y
coq.reduction.lazy.whd_all X Y
File "coq-builtin.elpi", line 1671, column 0, character 67774:
coq.string->name S N
coq.id->name S N
-
File "coq-builtin.elpi", line 1772, column 0, character 71520:
coq.elpi.accumulate-clauses S N
[
C
]
coq.elpi.accumulate S N C
+
File "coq-builtin.elpi", line 1773, column 0, character 71548:
coq.elpi.accumulate-clauses S N
[
C
]
coq.elpi.accumulate S N C
File "elpi-builtin.elpi", line 9, column 0, character 89:
true
File "elpi-builtin.elpi", line 28, column 0, character 296:
A
(A ; 
_)
File "elpi-builtin.elpi", line 30, column 0, character 311:
B
(_ ; 
B)
diff --git a/tutorial_coq_elpi_HOAS.html b/tutorial_coq_elpi_HOAS.html index a86f64f1a..1c5884436 100644 --- a/tutorial_coq_elpi_HOAS.html +++ b/tutorial_coq_elpi_HOAS.html @@ -176,17 +176,17 @@

HOAS for Gallina

syntax tree of Coq terms.

Constructor global

-

Let's start with the gref data type (for global reference).

+

Let's start with the gref data type (for global reference).

 type const constant -> gref.
 type indt inductive -> gref.
 type indc constructor -> gref.
-

constant, inductive and constructor are Coq specific -data types that are opaque to Elpi. Still the gref data type lets you +

constant, inductive and constructor are Coq specific +data types that are opaque to Elpi. Still the gref data type lets you see what these names point to (a constant, and inductive type or a constructor).

-

The coq.locate API resolves a string to a gref.

+

The coq.locate API resolves a string to a gref.

An expression like indt «nat» is not a Coq term (or better a type) yet.

-

The global term constructor turns a gref into an -actual term.

+

The global term constructor turns a gref into an +actual term.

 type global gref -> term.

Constructors app and fun

-

The app term constructor takes a list of terms and builds +

The app term constructor takes a list of terms and builds the (n-ary) application. The first term is the head, while the others are the arguments.

For example app [global (indc «S»), global (indc «O»)] is @@ -235,30 +235,30 @@

Constructors "f" (const C), coq.env.const C (some Bo) _ -}}.
Query assignments:
Bo = fun `x` (global (indt «nat»)) c0 \ c0
C = «f»

The fun constructor carries a pretty printing hint `x`, +}}.

Query assignments:
Bo = fun `x` (global (indt «nat»)) c0 \ c0
C = «f»

The fun constructor carries a pretty printing hint `x`, the type of the bound variable nat and a function describing the body:

 type fun  name -> term -> (term -> term) -> term.

Note

-

name is just for pretty printing: in spite of carrying +

name is just for pretty printing: in spite of carrying a value in the Coq world, it has no content in Elpi (like the unit type)

-

Elpi terms of type name are just identifiers +

Elpi terms of type name are just identifiers written between ` (backticks).

Query assignments:
B = X0
T = X1

API such as coq.name-suffix lets one craft a family of +}}.

Query assignments:
B = X0
T = X1

API such as coq.name-suffix lets one craft a family of names starting from one, eg coq.name-suffix `H` 1 N sets N to `H1`.

Constructors fix and match

-

The other binders prod (Coq's forall, AKA Π) and let are similar, -so let's rather focus on fix here.

+

The other binders prod (Coq's forall, AKA Π) and let are similar, +so let's rather focus on fix here.

The fix constructor carries a pretty printing hint, + app [global (indc «S»), app [c0, c3, c2]]]

C = «Nat.add»

The fix constructor carries a pretty printing hint, the number of the recursive argument (starting at 0), the type of the recursive function and finally the body where the recursive call is represented via a bound variable

 type fix   name -> int -> term -> (term -> term) -> term.
-

A match constructor carries the term being inspected, +

A match constructor carries the term being inspected, the return clause and a list of branches. Each branch is a Coq function expecting in input the arguments of the corresponding constructor. The order follows the @@ -311,13 +311,13 @@

Constructors global (indc «O»)]) c4 \ app [c1, c2]

Constructor sort

-

The last term constructor worth discussing is sort.

+

The last term constructor worth discussing is sort.

 type sort  universe -> term.
 type prop universe.
 type typ univ -> universe.
-

The opaque type univ is a universe level variable. Elpi holds a store of +

The opaque type univ is a universe level variable. Elpi holds a store of constraints among these variables and provides APIs named coq.univ.* to impose constraints.

Let's play a bit more with universe constraints using the -coq.typecheck API:

+coq.typecheck API:

The diagnostic data type is used by coq.typecheck to +

The diagnostic data type is used by coq.typecheck to tell if the term is well typed. The constructor ok signals success, while error carries an error message. In case of success universe constraints are added to the store.

@@ -588,7 +588,7 @@

The context

In some sense Elpi's way of traversing a binder is similar to a Zipper. The context of Elpi must record the part of the Zipper context that is relevant for binders.

-

The two predicates decl and def are used +

The two predicates decl and def are used for that purpose:

 pred decl i:term, o:name, o:term.         % Var Name Ty
@@ -636,9 +636,9 @@ 
The context

   app [global (indc «S»), global (indc «O»)]]
Ty = global (indt «nat»)

Tip

-

@pi-decl N Ty x\ takes arguments in the same order of fun and -prod, while -@pi-def N Ty Bo x\ takes arguments in the same order of let.

+

@pi-decl N Ty x\ takes arguments in the same order of fun and +prod, while +@pi-def N Ty Bo x\ takes arguments in the same order of let.

@@ -685,7 +685,7 @@

The context

α7 := Type WEAK CONSTRAINTS: -

Before the call to coq.typecheck, coq.sigma.print +

Before the call to coq.typecheck, coq.sigma.print prints nothing interesting, while after the call it also prints the following syntactic constraint:

evar (X1) (global (indt «nat»)) (X1)  /* suspended on X1 */

which indicates that the hole X1 is linked to a Coq evar @@ -833,7 +833,7 @@

Outside the pattern fragment< to be a special dummy constant, to be turned into an actual hole on the fly when needed.

This use case is perfectly legitimate and is supported by all APIs taking -terms in input thanks to the @holes! option.

+terms in input thanks to the @holes! option.

Note that after the call to coq.typecheck, X0 is assigned the +

Note that after the call to coq.typecheck, X0 is assigned the term _\ X1, that means that the offending argument has been pruned (discarded).

Note

-

All APIs taking a term support the @holes! option.

+

All APIs taking a term support the @holes! option.

-

In addition to the @holes! option, there is a class of APIs which can +

In addition to the @holes! option, there is a class of APIs which can deal with terms outside the pattern fragment. These APIs take in input a term -skeleton. A skeleton is not modified in place, as coq.typecheck +skeleton. A skeleton is not modified in place, as coq.typecheck does with its first argument, but is rather elaborated to a term related to it.

In some sense APIs taking a skeleton are more powerful, because they can modify the structure of the term, eg. insert a coercions, but are less diff --git a/tutorial_coq_elpi_command.html b/tutorial_coq_elpi_command.html index 5336267c3..64d102900 100644 --- a/tutorial_coq_elpi_command.html +++ b/tutorial_coq_elpi_command.html @@ -187,9 +187,9 @@

Defining commands

The first one Elpi Command hello. sets the current program to hello. Since it is declared as a Command some code is loaded automatically:

The second one Elpi Accumulate ... loads some extra code. @@ -214,7 +214,7 @@

Defining commands

as (str "world!").

Note

-

coq.say won't print quotes around strings

+

coq.say won't print quotes around strings

@@ -263,7 +263,7 @@

Command arguments

the type of the record (which was omitted) defaults to Type. Finally note that the type of the second field sees c0 (the value of the first field).

-

See the argument data type +

See the argument data type for a detailed description of all the arguments a command can receive.

Processing raw arguments

@@ -296,9 +296,9 @@

Processing raw arguments

"true" : "bool" The 3rd term has type "bool" which should be a subtype of "nat".

The command check_arg receives a term T and type checks it, then it prints the term and its type.

-

The coq.typecheck API has 3 arguments: a term, its type and a -diagnostic which can either be ok or (error Message). -The assert-ok! combinator checks if the diagnostic is ok, +

The coq.typecheck API has 3 arguments: a term, its type and a +diagnostic which can either be ok or (error Message). +The assert-ok! combinator checks if the diagnostic is ok, and if not it prints the error message and bails out.

The first invocation succeeds while the second one fails and prints the type checking error (given by Coq) following the string passed to @@ -314,10 +314,10 @@

Processing raw arguments

1 = true : Prop

The command still fails even if we told Coq how to inject booleans values into the natural numbers. Indeed the Check commands works.

-

The call to coq.typecheck modifies the term in place, it can assign +

The call to coq.typecheck modifies the term in place, it can assign implicit arguments (like the type parameter of eq) but it cannot modify the structure of the term. To do so, one has to use the -coq.elaborate-skeleton API.

+coq.elaborate-skeleton API.

#[arguments(raw)]
 Elpi Command elaborate_arg.
 Elpi Accumulate lp:{{
@@ -355,8 +355,8 @@ 
Examples

 
Synthesizing a term

 
Synthesizing a term typically involves reading an existing declaration
 and writing a new one. The relevant APIs are in the coq.env.* namespace
-and are named after the global reference they manipulate, eg coq.env.const
-for reading and coq.env.add-const for writing.

+and are named after the global reference they manipulate, eg coq.env.const
+for reading and coq.env.add-const for writing.

 
Here we implement a little command that given an inductive type name
 generates a term of type nat whose value is the number of constructors
 of the given inductive type.

@@ -388,20 +388,20 @@ 
Synthesizing a term

 
 
not an inductive type: coq.locate plus (indt X0)

 
Global reference not found: not_there

The command starts by locating the first argument and asserting it points to -an inductive type. This line is idiomatic: coq.locate aborts if +an inductive type. This line is idiomatic: coq.locate aborts if the string cannot be located, and if it relates it to a gref which is not -indt (for example const plus) assert! aborts with the given +indt (for example const plus) assert! aborts with the given error message.

-

coq.env.indt lets one access all the details of an inductive type, +

coq.env.indt lets one access all the details of an inductive type, here we just use the list of constructors. -The twin API coq.env.indt-decl lets +The twin API coq.env.indt-decl lets one access the declaration of the inductive in HOAS form, which might be easier to manipulate in other situations, like the next example.

Then the program crafts a natural number and declares a constant for it.

Abstracting an inductive

-

For the sake of introducing copy, the swiss army knife of λProlog, we +

For the sake of introducing copy, the swiss army knife of λProlog, we write a command which takes an inductive type declaration and builds a new one abstracting the former one on a given term. The new inductive has a parameter in place of the occurrences of that term.

@@ -458,7 +458,7 @@

Abstracting an inductive

Arguments tree' A%type_scope Arguments leaf' A%type_scope Arguments node' A%type_scope _ _ _

As expected tree' has a parameter A.

-

Now let's focus on copy. The standard +

Now let's focus on copy. The standard coq library (loaded by the command template) contains a definition of copy for terms and declarations.

An excerpt:

@@ -480,19 +480,19 @@

Abstracting an inductive

copy (app [global (indt «option»), global (indt «nat»)]) c0

and that rule masks the one for app when the sub-term being copied is -exactly option nat. The API copy-indt-decl copies an inductive +exactly option nat. The API copy-indt-decl copies an inductive declaration and calls copy on all the terms it contains (e.g. the type of the constructors).

-

The copy predicate is very flexible, but sometimes one needs to collect -some data along the way. The sibling API fold-map lets one do that.

+

The copy predicate is very flexible, but sometimes one needs to collect +some data along the way. The sibling API fold-map lets one do that.

An excerpt:

 fold-map (fun N T F) A (fun N T1 F1) A2 :-
   fold-map T A T1 A1, pi x\ fold-map (F x) A1 (F1 x) A2.
-

For example one can use fold-map to collect into a list all the occurrences +

For example one can use fold-map to collect into a list all the occurrences of inductive type constructors in a given term, then use the list to postulate -the right number of binders for them, and finally use copy to capture them.

+the right number of binders for them, and finally use copy to capture them.

@@ -505,7 +505,7 @@

Using DBs to store data across ca Since is a Db is accumulated when a program runs the current contents of the Db are used. Moreover the Db can be extended by Elpi programs themselves -thanks to the API coq.elpi.accumulate, enabling code to save a state +thanks to the API coq.elpi.accumulate, enabling code to save a state which is then visible at subsequent runs.

The initial contents of a Db, some code in the example above, is usually just the type declaration for the predicates part of the Db, @@ -546,7 +546,7 @@

Using DBs to store data across ca
bob is 24 years old

Extending data bases this way is fine, but requires the user of our command to be familiar with Elpi's syntax, which is not very nice. Instead, -we can write a new program that uses the coq.elpi.accumulate API +we can write a new program that uses the coq.elpi.accumulate API to extend the Db.

Elpi Command set_age.
 Elpi Accumulate Db age.db.
@@ -564,9 +564,9 @@ 
Using DBs to store data across ca
 instance: these object live inside a Coq module (or a Coq file) and become
 active when that module is Imported.

 
Deciding to which Coq module these
-extra rules belong is important and coq.elpi.accumulate provides
+extra rules belong is important and coq.elpi.accumulate provides
 a few options to tune that. Here we passed _, that uses the default
-setting. See the scope and clause data types for more info.

+setting. See the scope and clause data types for more info.

 

 
Inspecting a Db

 
So far we did query a Db but sometimes one needs to inspect the whole
@@ -587,11 +587,11 @@ 
Using DBs to store data across ca
 
 }}.
 Elpi Typecheck.
-
bob is 24 years old
alice is 21 years old

The std.findall predicate gathers in a list all solutions to -a query, while std.forall iterates a predicate over a list. -It is important to notice that coq.error is a fatal error which +

bob is 24 years old
alice is 21 years old

The std.findall predicate gathers in a list all solutions to +a query, while std.forall iterates a predicate over a list. +It is important to notice that coq.error is a fatal error which aborts an Elpi program. Here we shadow the catch all clause with a regular -failure so that std.findall can complete to list all the results.

+failure so that std.findall can complete to list all the results.

@@ -620,8 +620,8 @@

Attributes

"this" holding the empty string and an attribute for "more.stuff" holding the string "33".

Attributes are usually validated (parsed) and turned into regular options -using coq.parse-attributes and a description of their types using -the attribute-type data type:

+using coq.parse-attributes and a description of their types using +the attribute-type data type:

Elpi Command parse_attr.
 Elpi Accumulate lp:{{
 
@@ -694,10 +694,10 @@ 
Reporting errors

 error:

 
The elpi tactic/command bad failed without giving a
 specific error message. Please report this
-inconvenience to the authors of the program.
You should use the coq.error API or the assert! one
-to abort a program. There is a dedicated coq.ltac.fail API to abort
+inconvenience to the authors of the program.

You should use the coq.error API or the assert! one +to abort a program. There is a dedicated coq.ltac.fail API to abort tactics.

-

Warnings can be reported using the coq.warning which lets you +

Warnings can be reported using the coq.warning which lets you pick a name and category. In turn these can be used to disable or make fatal your warnings (as any other Coq warning).

@@ -822,13 +822,13 @@

Parsing and Execution

}}. Elpi Typecheck. -
The module is «tutorial_coq_elpi_command.Module51»

If the only data to be passed to the interp phase is the list of +

The module is «tutorial_coq_elpi_command.Module33»

If the only data to be passed to the interp phase is the list of synterp actions, then a few APIs can come in handy. -The synterp phase has access to the API coq.synterp-actions +The synterp phase has access to the API coq.synterp-actions that lists the actions performed so far. The interp phase can use -coq.replay-synterp-action and coq.next-synterp-action to +coq.replay-synterp-action and coq.next-synterp-action to replay an action or peek the next one to be performed.

-

An excerpt of the synterp-action.

+

An excerpt of the synterp-action.

 % Action executed during the parsing phase (aka synterp)
 kind synterp-action type.
diff --git a/tutorial_coq_elpi_tactic.html b/tutorial_coq_elpi_tactic.html
index d7b9c8046..e7c5d666d 100644
--- a/tutorial_coq_elpi_tactic.html
+++ b/tutorial_coq_elpi_tactic.html
@@ -193,9 +193,9 @@ 
Defining tactics

 
The first one Elpi Tactic show. sets the current program to show.
 Since it is declared as a Tactic some code is loaded automatically:

 
 
The second one Elpi Accumulate ... loads some extra code.
@@ -214,8 +214,8 @@ 
Defining tactics

 code does not contain the most frequent kind of mistakes. This command
 considers some mistakes minor and only warns about them. You can
 pass -w +elpi.typecheck to coqc to turn these warnings into errors.

-
The entry point for tactics is called solve which maps a goal
-into a list of sealed-goal (representing subgoals).

+
The entry point for tactics is called solve which maps a goal
+into a list of sealed-goal (representing subgoals).

 
Tactics written in Elpi can be invoked by prefixing its name with elpi.

 
x, y: nat
x + 1 = y

 
Goal: 
@@ -251,7 +251,7 @@ 
Defining tactics

 
The _Trigger component, which we did not print, is a variable that, when
 assigned, triggers the elaboration of its value against the type of the goal
 and obtains a value for Proof this way.

-
Keeping in mind that the solve predicate relates one goal to a list of
+
Keeping in mind that the solve predicate relates one goal to a list of
 subgoals, we implement our first tactic which blindly tries to solve the goal.

 
Elpi Tactic blind.
 Elpi Accumulate lp:{{
@@ -277,12 +277,12 @@ 
Integration with Ltac

 
For a simple tactic like blind the list of subgoals is easy to write, since
 it is empty, but in general one should collect all the holes in
 the value of Proof (the checked proof term) and build goals out of them.

-
There is a family of APIs named after refine, the mother of all
+
There is a family of APIs named after refine, the mother of all
 tactics, in 
 elpi-ltac.elpi
 which does this job for you.

 
Usually a tactic builds a (possibly partial) term and calls
-refine on it.

+refine on it.

 
Let's rewrite the blind tactic using this schema.

 
Elpi Tactic blind2.
 Elpi Accumulate lp:{{
@@ -347,7 +347,7 @@ 
Integration with Ltac

 its type nat is not of sort Prop, so it backtracks and picks {{I}}.

 
Another common way to build an Elpi tactic is to synthesize a term and
 then call some Ltac piece of code finishing the work.

-
The API coq.ltac.call invokes some Ltac piece
+
The API coq.ltac.call invokes some Ltac piece
 of code passing to it the desired
 arguments. Then it builds the list of subgoals.

 
Here we pass an integer, which in turn is passed to fail, and a term,
@@ -395,13 +395,13 @@ 
Arguments and Tactic Notation
 
Important

 
terms are received in raw format, eg before elaboration

 
Indeed the type argument to eq is a variable.
-One can use APIs like coq.elaborate-skeleton to infer holes like
+One can use APIs like coq.elaborate-skeleton to infer holes like
 X0.

 

-
See the argument data type
+
See the argument data type
 for a detailed description of all the arguments a tactic can receive.

-
Now let's write a tactic which behaves pretty much like the refine
-one from Coq, but prints what it does using the API coq.term->string.

+
Now let's write a tactic which behaves pretty much like the refine
+one from Coq, but prints what it does using the API coq.term->string.

 
Elpi Tactic refine.
 Elpi Accumulate lp:{{
   solve (goal _ _ Ty _ [trm S] as G) GL :-
@@ -463,14 +463,14 @@ 
Ltac arguments to Elpi arguments<
 

 

 
Failure

-
The coq.error aborts the execution of both
+
The coq.error aborts the execution of both
 Elpi and any enclosing Ltac context. This failure cannot be caught
 by Ltac.

-
On the contrary the coq.ltac.fail builtin can be used to
+
On the contrary the coq.ltac.fail builtin can be used to
 abort the execution of Elpi code in such a way that Ltac can catch it.
 This API takes an integer akin to Ltac's fail depth together with
 the error message to be displayed to the user.

-
Library functions of the assert! family call, by default, coq.error.
+
Library functions of the assert! family call, by default, coq.error.
 The flag @ltacfail! N can be set to alter this behavior and turn errors into
 calls to coq.ltac.fail N.

 
Elpi Tactic abort.
@@ -499,7 +499,7 @@ 
Examples

 
Let's code assumption in Elpi

 
assumption is a very simple tactic: we look up in the proof
 context for an hypothesis which unifies with the goal.
-Recall that Ctx is made of decl and def
+Recall that Ctx is made of decl and def
 (here, for simplicity, we ignore the latter case).

 
Elpi Tactic assumption.
 Elpi Accumulate lp:{{
@@ -521,9 +521,9 @@ 
Let's code Q but the goal has type id Q which is
 convertible (unifiable, for Coq's unification) to Q.

 
Let's improve our tactic by looking for an assumption which is unifiable with
-the goal, and not just alpha convertible. The coq.unify-leq
+the goal, and not just alpha convertible. The coq.unify-leq
 calls Coq's unification for types (on which cumulativity applies, hence the
--leq suffix). The std.mem utility, thanks to backtracking,
+-leq suffix). The std.mem utility, thanks to backtracking,
 eventually finds an hypothesis that satisfies the following predicate
 (ie unifies with the goal).

 
Elpi Tactic assumption2.
@@ -541,7 +541,7 @@ 
Let's code Proof.
 
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
id Q

 all: elpi assumption2.
-Qed.
refine does unify the type of goal with the type of the term,
+Qed.
refine does unify the type of goal with the type of the term,
 hence we can simplify the code further. We obtain a
 tactic very similar to our initial blind tactic, which picks
 candidates from the context rather than from the program itself.

@@ -564,7 +564,7 @@ 
Let's code Let's code set in Elpi

 
The set tactic takes a term, possibly with holes, and
 makes a let-in out of it.

-
It gives us the occasion to explain the copy utility.

+
It gives us the occasion to explain the copy utility.

 
Elpi Tactic find.
 Elpi Accumulate lp:{{
 
@@ -584,7 +584,7 @@ 
Let's code 
found P /\ P
P, Q: Prop
P /\ P \/ P /\ Q

 Abort.
This first approximation only prints the term it found, or better the first
 instance of the given term.

-
Now lets focus on copy. An excerpt:

+
Now lets focus on copy. An excerpt:

 
 copy X X :- name X.     % checks X is a bound variable
 copy (global _ as C) C.
@@ -602,7 +602,7 @@ 
Let's code 
 copy (app [global (indt «andn»), sort prop, sort prop, c0, X0 c0 c1]) c2
 

-
and that rule masks the one for app when the 
+
and that rule masks the one for app when the 
 sub-term being copied matches (P /\ _). The first time this rule
 is used X0 is assigned, making the rule represent the term (P /\ P).

 
Now let's refine the tactic to build a let-in, and complain if the
@@ -719,9 +719,9 @@ 
Let's code X1 some procedure to
 turn that value into X0 is triggered. That procedure is called
 elaboration and it is currently implemented by calling the
-coq.elaborate-skeleton API.

+coq.elaborate-skeleton API.

 
Given this set up, it is impossible to use a term of the wrong type as a
-Proof. Let's rewrite the split tactic without using refine.

+Proof. Let's rewrite the split tactic without using refine.

 
Elpi Tactic split_ll.
 Elpi Accumulate lp:{{
   solve (goal Ctx Trigger {{ lp:A /\ lp:B }} Proof []) GL :- !,
@@ -743,7 +743,7 @@ 
Let's code Qed.
Crafting by hand the list of subgoal is not easy.
 In particular here we did not set up the new trigger for Pa and Pb,
 nor seal the goals appropriately (we did not bind proof variables).

-
The coq.ltac.collect-goals API helps us doing this.

+
The coq.ltac.collect-goals API helps us doing this.

 
Elpi Tactic split_ll_bis.
 Elpi Accumulate lp:{{
   solve (goal Ctx Trigger {{ lp:A /\ lp:B }} Proof []) GL :- !,
@@ -764,14 +764,14 @@ 
Let's code 
True /\ True /\ ?t

 
True
True
?t

 all: elpi blind.
-Qed.
At the light of that, refine is simply:

+Qed.
At the light of that, refine is simply:

 
 refine T (goal _ RawEv _ Ev _) GS :-
   RawEv = T, coq.ltac.collect-goals Ev GS _.
 

-
Now that we know the low level plumbing, we can use refine ;-)

+
Now that we know the low level plumbing, we can use refine ;-)

 
The only detail we still have to explain is what exactly a
-sealed-goal is. A sealed goal wraps into a single object all
+sealed-goal is. A sealed goal wraps into a single object all
 the proof variables and the assumptions about them, making this object easy
 (or better, sound) to pass around.

 

@@ -783,9 +783,9 @@ 
multi-goal tactics

 
  • if the tactic is a multi-goal one, it will receive all goals
    • 
 
 
    In Elpi you can implement a multi-goal tactic by providing a rule for
-the msolve predicate. Since such a tactic will need to manipulate
+the msolve predicate. Since such a tactic will need to manipulate
 multiple goals, potentially living in different proof context, it receives
-a list of sealed-goal, a data type which seals a goal and
+a list of sealed-goal, a data type which seals a goal and
 its proof context.
    
 
    Elpi Tactic ngoals.
 Elpi Accumulate lp:{{
@@ -821,9 +821,9 @@ 
    multi-goal tactics
    
   nabla c1 \
    seal
     (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X2 c0 c1) c1 
-      (X3 c0 c1) [])]
    nabla binds all proof variables, then seal
+      (X3 c0 c1) [])]
    nabla binds all proof variables, then seal
 holds a regular goal, which in turn carries the proof context.
    
-
    In order to operate inside a goal one can use the coq.ltac.open utility,
+
    In order to operate inside a goal one can use the coq.ltac.open utility,
 which postulates all proof variables using pi x\  and loads the proof
 context using =>.
    
 
    Operating on multiple goals at the same time is doable, but not easy.
@@ -896,7 +896,7 @@ 
    LCF tacticals

    A few tacticals can be found in the elpi-ltac.elpi file. -For example this is the code of try:

    +For example this is the code of try:

     pred try i:tactic, i:sealed-goal, o:list sealed-goal.
 try T G GS :- T G GS.
@@ -949,9 +949,9 @@ 
    Setting arguments for a tactic
 thenl [ open (tac1 Datum), open (tac2 Datum) ]
    -

    but the binder structure of sealed-goal would prevent Datum +

    but the binder structure of sealed-goal would prevent Datum to mention proof variables, that would otherwise escape the sealing.

    -

    The utility set-goal-arguments:

    +

    The utility set-goal-arguments:

     coq.ltac.set-goal-arguments Args G G1 G1wArgs
    diff --git a/tutorial_elpi_lang.html b/tutorial_elpi_lang.html index 8737a7679..659659365 100644 --- a/tutorial_elpi_lang.html +++ b/tutorial_elpi_lang.html @@ -218,8 +218,8 @@

    Logic programming

    is a mode declaration, which we will explain later (ignore it for now).

    Note

    -

    int is the built-in data type of integers

    -

    Integers come with usual arithmetic operators, see the calc built-in.

    +

    int is the built-in data type of integers

    +

    Integers come with usual arithmetic operators, see the calc built-in.

    In order to run our program we have to write a query, i.e. a predicate expression containing variables such as:

    @@ -247,14 +247,14 @@

    Logic programming

    age alice A, coq.say "The age of alice is" A -}}.
    The age of alice is 20
    Query assignments:
    A = 20

    coq.say is a built-in predicate provided by Coq-Elpi which +}}.

    The age of alice is 20
    Query assignments:
    A = 20

    coq.say is a built-in predicate provided by Coq-Elpi which prints its arguments. You can look at the output buffer of Coq to see the value for A or hover or toggle the little bubble after }}. if you are reading the tutorial with a web browser.

    Note

    -

    string is a built-in data type

    +

    string is a built-in data type

    Strings are delimited by double quotes and \ is the escape symbol.

    The predicate age represents a relation (in contrast to a function) @@ -872,8 +872,8 @@

    Constraint Handling Rules

    Spilling (relation composition)

    Chaining "relations" can be painful, especially when -they look like functions. Here we use std.append -and std.rev to build a palindrome:

    +they look like functions. Here we use std.append +and std.rev to build a palindrome:

    Elpi Program function lp:{{
 
 pred make-palindrome i:list A, o:list A.
@@ -926,20 +926,20 @@ 
    Spilling (relation composition)<
 
    
 
    APIs for built-in data
    
 
    Functions about built-in data types are available via the
-calc predicate or its infix version is. Example:
    
+calc predicate or its infix version is. Example:
    
 
    result = 5
    Query assignments:
    X = result =
    Y = 5
    The calc predicate works nicely with spilling:
    
+}}.
    result = 5
    Query assignments:
    X = result =
    Y = 5

    The calc predicate works nicely with spilling:

    result = 5
    Query assignments:
    Spilled_1 = 5

    Allocation of variables

    The language let's one use λ-abstraction also to write anonymous rules but one has to be wary of where variables are bound (allocated really).

    -

    In our example we use the higher order predicate std.map:

    +

    In our example we use the higher order predicate std.map:

     pred std.map i:list A, i:(A -> B -> prop), o:list B.
    @@ -983,7 +983,7 @@

    Allocation of variables

    good2 [1,2,3] R3 }}.
    Query assignments:
    R1 = X0
    R2 = [2, 3, 4]
    R3 = [2, 3, 4]

    The problem with bad is that TMP is fresh each time the rule -is used, but not every time the anonymous rule passed to map +is used, but not every time the anonymous rule passed to map is used. Technically TMP is quantified (allocated) where L and Result are.

    There are two ways to quantify TMP correctly, that is inside the @@ -1156,7 +1156,7 @@

    Trace browser

    of (fun c0 \ fun c1 \ c0) X0
    rid:0 step:2 gid:7 user:rule = backchain
    rid:0 step:2 gid:7 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, character 459: -
    }}} -> (0.001s)
    select 3 {{{ +
    }}} -> (0.000s)
    select 3 {{{
    rid:0 step:2 gid:7 user:rule:backchain:try = File "(stdin)", line 15, column 3, character 459: (of (fun A0) (arr A1 A2)) :- ( pi (c0 \ @@ -1221,7 +1221,7 @@

    Trace browser

    (of c0 X1) :- .
    rid:0 step:8 gid:0 user:assign = X1 := X4
    rid:0 step:8 gid:14 user:rule:backchain = success -
    }}} -> (0.000s)
    run 9 {{{ +
    }}} -> (0.002s)
    run 9 {{{
    rid:0 step:9 gid:8 user:curgoal = coq.say coq.say (arr X4 (arr X3 X4))
    rid:0 step:9 gid:8 user:rule = builtin @@ -1295,7 +1295,7 @@

    Trace browser

    of c0 (arr X3^1 X2)
    rid:1 step:6 gid:21 user:rule = backchain
    rid:1 step:6 gid:21 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: -
    }}} -> (0.000s)
    select 5 {{{ +
    }}} -> (0.001s)
    select 5 {{{
    rid:1 step:6 gid:21 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: (of c0 X1) :- .
    rid:1 step:6 gid:0 user:assign:expand = X3^1 := X4 c0 @@ -1314,7 +1314,7 @@

    Trace browser

    rid:1 step:7 gid:22 user:backchain:fail-to = unify X5 with arr X5 X2
    }}} -> (0.000s)
    select 7 {{{
    rid:1 step:7 gid:22 user:rule:backchain = fail -
    }}} -> (0.002s)
    The elpi tactic/command stlc failed without giving a +
    }}} -> (0.000s)
    The elpi tactic/command stlc failed without giving a specific error message. Please report this inconvenience to the authors of the program.

    The trace can be limited to a range of steps. Look at the numbers run HERE {{{.

    @@ -1470,7 +1470,7 @@

    Precedence of }}.
    Query assignments:
    A = X0
    B = X0
    C = X0

    Backtracking

    -

    Backtracking can lead to weird execution traces. The std.do! predicate +

    Backtracking can lead to weird execution traces. The std.do! predicate should be used to write non-backtracking code.

     pred not-a-backtracking-one.
@@ -1483,8 +1483,8 @@ 
    Backtracking
    
 
    In the example above once condition holds we start a sequence of
 steps which we will not reconsider. Locally, backtracking is still
 available, e.g. between generate and test.
-See also the std.spy-do! predicate which prints each and every step,
-and the std.spy one which can be used to spy on a single one.
    
+See also the std.spy-do! predicate which prints each and every step,
+and the std.spy one which can be used to spy on a single one.