Merge pull request #669 from wdeweijer/master

Fix typos and broken links in tutorials

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 <https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi>`_
+`coq-builtin.elpi <https://github.com/LPCIC/coq-elpi/blob/master/builtin-doc/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

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 <https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi>`_
+  `coq-builtin.elpi <https://github.com/LPCIC/coq-elpi/blob/master/builtin-doc/coq-builtin.elpi>`_
 * some utilities, like :lib:`copy` or :libred:`whd1` are loaded from
   `elpi-command-template.elpi <https://github.com/LPCIC/coq-elpi/blob/master/elpi/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.
 
 |*)

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 <https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi>`_
+  `coq-builtin.elpi <https://github.com/LPCIC/coq-elpi/blob/master/builtin-doc/coq-builtin.elpi>`_
 * some utilities, like :lib:`copy` or :libred:`whd1` are loaded from
   `elpi-command-template.elpi <https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-tactic-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,16 +236,16 @@ 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.
 
 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 <https://coq.inria.fr/doc/proof-engine/ltac.html#syntactic-values>`_ :
+for Ltac values <https://coq.inria.fr/doc/master/refman/proof-engine/ltac.html#syntactic-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 <https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi>`_.
 For example this is the code of :libtac:`try`:
 

examples/tutorial_elpi_lang.v

@@ -185,7 +185,7 @@ hence unification succeeds.
 
 See also the `Wikipedia page on Unification <https://en.wikipedia.org/wiki/Unification_(computer_science)#Syntactic_unification_of_first-order_terms>`_.
 
-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`.