From e510593b9bef4e6a917b3c63bfcec1e362568b31 Mon Sep 17 00:00:00 2001 From: wdeweijer Date: Wed, 17 Jul 2024 19:25:18 +0200 Subject: [PATCH] Fix typos and broken links in tutorials --- examples/tutorial_coq_elpi_HOAS.v | 8 +++--- examples/tutorial_coq_elpi_command.v | 14 +++++----- examples/tutorial_coq_elpi_tactic.v | 40 ++++++++++++++-------------- examples/tutorial_elpi_lang.v | 22 +++++++-------- 4 files changed, 42 insertions(+), 42 deletions(-) diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 1c92d9462..8ce682784 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -20,7 +20,7 @@ Tutorial on the HOAS for Coq terms evars in the Coq jargon). This software, "coq-elpi", is a Coq plugin embedding Elpi and - exposing to the extension language Coq spefic data types (e.g. terms) + exposing to the extension language Coq specific data types (e.g. terms) and API (e.g. to declare a new inductive type). In order to get proper syntax highlighting using VSCode please install the @@ -52,7 +52,7 @@ Elpi Command tutorial_HOAS. (* .none *) (*| The full syntax of Coq terms can be found in -`coq-builtin.elpi `_ +`coq-builtin.elpi `_ together with a detailed documentation of the encoding of contexts and the APIs one can use to interact with Coq. This tutorial, and the two more that focus on commands and tactics, are a gentle introduction to all that. @@ -65,7 +65,7 @@ syntax tree of Coq terms. Constructor :e:`global` ----------------------- -Let's start with the :type:`gref` data type (for global rerence). +Let's start with the :type:`gref` data type (for global reference). .. code:: elpi @@ -382,7 +382,7 @@ Elpi Query lp:{{ It is quite frequent to put Coq variables in the scope of an Elpi unification variable, and this can be done by simply writing -`lp:(X a b)` which is a shorhand for `lp:{{ X {{ a }} {{ b }} }}`. +`lp:(X a b)` which is a shorthand for `lp:{{ X {{ a }} {{ b }} }}`. .. warning:: writing `lp:X a b` (without parentheses) would result in a Coq application, not an Elpi one diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index 42256a037..98ab50093 100644 --- a/examples/tutorial_coq_elpi_command.v +++ b/examples/tutorial_coq_elpi_command.v @@ -20,7 +20,7 @@ Tutorial on Coq commands evars in the Coq jargon). This software, "coq-elpi", is a Coq plugin embedding Elpi and - exposing to the extension language Coq spefic data types (e.g. terms) + exposing to the extension language Coq specific data types (e.g. terms) and API (e.g. to declare a new inductive type). In order to get proper syntax highlighting using VSCode please install the @@ -63,7 +63,7 @@ The first one `Elpi Command hello.` sets the current program to hello. Since it is declared as a `Command` some code is loaded automatically: * APIs (eg :builtin:`coq.say`) and data types (eg Coq :type:`term` s) are loaded from - `coq-builtin.elpi `_ + `coq-builtin.elpi `_ * some utilities, like :lib:`copy` or :libred:`whd1` are loaded from `elpi-command-template.elpi `_ @@ -168,7 +168,7 @@ Finally note that the type of the second field sees :e:`c0` (the value of the first field). See the :type:`argument` data type -for a detailed decription of all the arguments a command can receive. +for a detailed description of all the arguments a command can receive. ------------------------ Processing raw arguments @@ -179,7 +179,7 @@ so that no elaboration has been performed. This can be achieved by using the `#[arguments(raw)]` attributed when the command is declared. -Then, thre are two ways to process term arguments: +Then, there are two ways to process term arguments: typechecking and elaboration. |*) @@ -267,7 +267,7 @@ 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 refence they manipulate, eg :builtin:`coq.env.const` +and are named after the global reference they manipulate, eg :builtin:`coq.env.const` for reading and :builtin:`coq.env.add-const` for writing. Here we implement a little command that given an inductive type name @@ -612,7 +612,7 @@ Elpi Accumulate lp:{{ The first attribute, :e:`elpi.loc` is always present and corresponds to the location in the source file of the command. Then we find an attribute for -:e:`"this"` holding the emptry string and an attribute for :e:`"more.stuff"` holding +:e:`"this"` holding the empty string and an attribute for :e:`"more.stuff"` holding the string :e:`"33"`. Attributes are usually validated (parsed) and turned into regular options @@ -699,7 +699,7 @@ Fail Go nowhere. (* .fails *) Reporting errors ---------------- -Last, (good) Elpi programs should fail reporting intellegible error messages, +Last, (good) Elpi programs should fail reporting intelligible error messages, as the previous one. |*) diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v index ec1e31767..57f057ed1 100644 --- a/examples/tutorial_coq_elpi_tactic.v +++ b/examples/tutorial_coq_elpi_tactic.v @@ -20,7 +20,7 @@ Tutorial on Coq tactics evars in the Coq jargon). This software, "coq-elpi", is a Coq plugin embedding Elpi and - exposing to the extension language Coq spefic data types (e.g. terms) + exposing to the extension language Coq specific data types (e.g. terms) and API (e.g. to declare a new inductive type). In order to get proper syntax highlighting using VSCode please install the @@ -74,7 +74,7 @@ The first one `Elpi Tactic show.` sets the current program to `show`. Since it is declared as a `Tactic` some code is loaded automatically: * APIs (eg :builtin:`coq.say`) and data types (eg Coq :type:`term` s) are loaded from - `coq-builtin.elpi `_ + `coq-builtin.elpi `_ * some utilities, like :lib:`copy` or :libred:`whd1` are loaded from `elpi-command-template.elpi `_ @@ -112,7 +112,7 @@ Abort. In the Elpi code up there :e:`Proof` is the hole for the current goal, :e:`Type` the statement to be proved and :e:`Ctx` the proof context (the list of -hypotheses). Since we don't assign :e:`Proof` the tactic makes no progess. +hypotheses). Since we don't assign :e:`Proof` the tactic makes no progress. Elpi prints somethinglike this: .. mquote:: .s(elpi).msg{Goal:*X0 c0 c1*} @@ -135,7 +135,7 @@ the variable has :e:`c0` and :e:`c1` in scope (the proof term can use them). Finally we see the type of the goal `x + 1 = y`. The :e:`_Trigger` component, which we did not print, is a variable that, when -assigned, trigger the elaboration of its value against the type of the goal +assigned, triggers the elaboration of its value against the type of the goal and obtains a value for :e:`Proof` this way. Keeping in mind that the :builtin:`solve` predicate relates one goal to a list of @@ -225,7 +225,7 @@ the statement features an explicit conjunction. |*) -About conj. (* remak the implicit arguments *) +About conj. (* remark the implicit arguments *) Elpi Tactic split. Elpi Accumulate lp:{{ @@ -236,8 +236,8 @@ Elpi Accumulate lp:{{ solve _ _ :- % This signals a failure in the Ltac model. A failure - % in Elpi, that is no more cluases to try, is a fatal - % error that cannot be catch by Ltac combinators like repeat. + % in Elpi, that is no more clauses to try, is a fatal + % error that cannot be caught by Ltac combinators like repeat. coq.ltac.fail _ "not a conjunction". }}. Elpi Typecheck. @@ -245,7 +245,7 @@ Elpi Typecheck. Lemma test_split : exists t : Prop, True /\ True /\ t. Proof. (* .in *) eexists. -repeat elpi split. (* The failure is catched by Ltac's repeat *) +repeat elpi split. (* The failure is caught by Ltac's repeat *) (* Remark that the last goal is left untouched, since it did not match the pattern {{ _ /\ _ }}. *) all: elpi blind. @@ -269,7 +269,7 @@ 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, -which is turn is passed to `apply`. +which in turn is passed to `apply`. |*) @@ -327,7 +327,7 @@ have to be put between parentheses. :e:`X0`. See the :type:`argument` data type -for a detailed decription of all the arguments a tactic can receive. +for a detailed description of all the arguments a tactic can receive. Now let's write a tactic which behaves pretty much like the :libtac:`refine` one from Coq, but prints what it does using the API :builtin:`coq.term->string`. @@ -368,7 +368,7 @@ It is customary to use the Tactic Notation command to attach a nicer syntax to Elpi tactics. In particular `elpi tacname` accepts as arguments the following `bridges -for Ltac values `_ : +for Ltac values `_ : * `ltac_string:(v)` (for `v` of type `string` or `ident`) * `ltac_int:(v)` (for `v` of type `int` or `integer`) @@ -410,16 +410,16 @@ Failure ======== The :builtin:`coq.error` aborts the execution of both -Elpi and any enclosing LTac context. This failure cannot be catched -by LTac. +Elpi and any enclosing Ltac context. This failure cannot be caught +by Ltac. On the contrary the :builtin:`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 +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, :builtin:`coq.error`. -The flag `@ltacfail! N` can be set to alter this behavior and turn erros into +The flag `@ltacfail! N` can be set to alter this behavior and turn errors into calls to `coq.ltac.fail N`. |*) @@ -485,8 +485,8 @@ As we hinted before, Elpi's equality is alpha equivalence. In the second goal the assumption has type `Q` but the goal has type `id Q` which is convertible (unifiable, for Coq's unification) to `Q`. -Let's improve our tactic looking for an assumption which is unifiable with -the goal, an not just alpha convertible. The :builtin:`coq.unify-leq` +Let's improve our tactic by looking for an assumption which is unifiable with +the goal, and not just alpha convertible. The :builtin:`coq.unify-leq` calls Coq's unification for types (on which cumulativity applies, hence the `-leq` suffix). The :stdlib:`std.mem` utility, thanks to backtracking, eventually finds an hypothesis that satisfies the following predicate @@ -571,7 +571,7 @@ Abort. (*| This first approximation only prints the term it found, or better the first -intance of the given term. +instance of the given term. Now lets focus on :lib:`copy`. An excerpt: @@ -904,7 +904,7 @@ tactic, here the precise type definition: typeabbrev tactic (sealed-goal -> (list sealed-goal -> prop)). -A few tacticals can be fond in the +A few tacticals can be found in the `elpi-ltac.elpi file `_. For example this is the code of :libtac:`try`: diff --git a/examples/tutorial_elpi_lang.v b/examples/tutorial_elpi_lang.v index 2fcb6b2b1..3fc5c79a2 100644 --- a/examples/tutorial_elpi_lang.v +++ b/examples/tutorial_elpi_lang.v @@ -185,7 +185,7 @@ hence unification succeeds. See also the `Wikipedia page on Unification `_. -Since the first part of the query is succesful the rest of +Since the first part of the query is successful the rest of the query is run: the value of :e:`P` is printed as well as the :e:`"is 23 years old"` string. @@ -232,7 +232,7 @@ but the third one has no solution, so unification fails. Backtracking ------------ -When failure occurs all assignements are undone (i.e. :e:`P` is unset again) +When failure occurs all assignments are undone (i.e. :e:`P` is unset again) and the next rule in the program is tried. This operation is called *backtracking*. @@ -248,7 +248,7 @@ This one also fails. The unification problem for the last rule is: age P 20 = age alice 20 -This one works, and the assigment :e:`P = alice` is kept as the result +This one works, and the assignment :e:`P = alice` is kept as the result of the first part of the query. Then :e:`P` is printed and the program ends. @@ -293,7 +293,7 @@ Elpi Query lp:{{ The :e:`not(P)` predicate tries to solve the query :e:`P`: it fails if :e:`P` succeeds, and succeeds if :e:`P` fails. In any case no trace is left - of the computation for :e:`P`. E.g. :e:`not(X = 1, 2 < 1)` suceeds, but + of the computation for :e:`P`. E.g. :e:`not(X = 1, 2 < 1)` succeeds, but the assignment for :e:`X` is undone. See also the section about the `foundations`_ of λProlog. @@ -562,7 +562,7 @@ Elpi Bound Steps 0. :e:`pi x\ ` and :e:`=>` ----------------------- -We have seen how to implement subtitution using the binders of λProlog. +We have seen how to implement substitution using the binders of λProlog. More often than not we need to move under binders rather than remove them by substituting some term in place of the bound variable. @@ -653,7 +653,7 @@ universally quantified, we use :e:`A2`, :e:`B2`... this time): * the :e:`=>` connective adds the rule :e:`of c2 A2` the program * the new query :e:`of c1 B2` is run. -The (hypotetical) rule :e:`of c1 A1` is used: +The (hypothetical) rule :e:`of c1 A1` is used: * unification assigns :e:`A1` to :e:`B2` @@ -686,7 +686,7 @@ First, the rule for elpi:`fun` is selected: Then it's the turn of typing the application: -* the query :e:`of c1 (arr A2 B2)` assignes to :e:`A1` the +* the query :e:`of c1 (arr A2 B2)` assigns to :e:`A1` the value :e:`arr A2 B2`. This means that the hypothetical rule is now :e:`of c1 (arr A2 B2)`. * the query :e:`of c1 A2` fails because the unification @@ -915,7 +915,7 @@ Elpi Query lp:{{ sum X (s z) (s (s z)), (X = z ; X = s z) }}. (*| -In this example the computation suspends, then makes progess, +In this example the computation suspends, then makes progress, then suspends again... |*) @@ -1296,7 +1296,7 @@ Debugging ========= The most sophisticated debugging feature can be used via -the Visual Sudio Code extension ``gares.elpi-lang`` and its +the Visual Studio Code extension ``gares.elpi-lang`` and its ``Elpi Tracer`` tab. --------------- @@ -1328,7 +1328,7 @@ the load icon, in the upper right corner of the Elpi Tracer panel. the extension settings in order to get a correct display. The trace browser displays, on the left column, a list of cards corresponding -to a step perfoemd by the interpreter. The right side of the +to a step performed by the interpreter. The right side of the panel gives more details about the selected step. In the image below one can see the goal, the rule being applied, the assignments performed by the unification of the rule's head with the goal, the subgoals generated. @@ -1539,7 +1539,7 @@ fails, because :e:`X` cannot be at the same time 3 and 9. Initially asserting that 3 (the value hold by :e:`X`) is equal to 9. The second call to :e:`is` does not change the value carried by :e:`X`! -Unification, and hence the :e:`=` pradicate, plays two roles. +Unification, and hence the :e:`=` predicate, plays two roles. When :e:`X` is unset, :e:`X = v` sets the variable. When :e:`X` is set to :e:`u`, :e:`X = v` checks if the value of :e:`X` is equal to :e:`u`: it is equivalent to :e:`u = v`.