From 23230ca4faf2558a4dc06b1a4ecd26a69c44d26a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Aug 2021 14:41:56 +0200 Subject: [PATCH 1/9] wip --- .vscode/settings.json | 3 +- Makefile | 2 +- elpi/coq-lib.elpi | 11 ++-- elpi/elpi-reduction.elpi | 2 +- examples/tutorial_coq_elpi_HOAS.v | 89 +++++++++++++------------ examples/tutorial_coq_elpi_command.v | 83 ++++++++++++------------ examples/tutorial_coq_elpi_tactic.v | 97 ++++++++++++++-------------- examples/tutorial_style.rst | 58 +++++++++++++++++ 8 files changed, 205 insertions(+), 140 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 658ed59c4..2d71dd799 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -28,5 +28,6 @@ "**/Makefile.coq": true, "**/Makefile.coq.conf": true, "**/.merlin": true - } + }, + "restructuredtext.confPath": "${workspaceFolder}/alectryon/recipes/sphinx" } \ No newline at end of file diff --git a/Makefile b/Makefile index 82098fc70..e7a61a9d3 100644 --- a/Makefile +++ b/Makefile @@ -52,7 +52,7 @@ doc: $(DOCDEP) @echo "########################## generating doc ##########################" @mkdir -p doc @$(foreach tut,$(wildcard examples/tutorial*.v),\ - echo ALECTRYON $(tut); alectryon \ + echo ALECTRYON $(tut); alectryon/alectryon.py \ --frontend coq+rst \ --output-directory doc \ --sertop-arg=--topfile=Tutorial \ diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi index a9a9a499d..8dfb61953 100644 --- a/elpi/coq-lib.elpi +++ b/elpi/coq-lib.elpi @@ -102,9 +102,9 @@ coq.saturate Ty T O :- whd Ty [] (prod N Src Tgt) [], !, @pi-decl N Src x\ coq.saturate (Tgt x) R O. coq.saturate _ X X. -% copy can be used to perform a replacement, eg -% (copy (const "foo") (const "bar) :- !) => copy T T1 -% traverses T replacing foo with bar. +% [copy A B] can be used to perform a replacement, eg +% (copy (const "foo") (const "bar) :- !) => copy A B +% traverses A replacing foo with bar. pred copy i:term, o:term. :name "copy:start" copy X Y :- name X, !, X = Y, !. % avoid loading "copy x x" at binders @@ -488,12 +488,14 @@ coq.with-TC Class Instance->Clause Code :- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +pred coq.parse-attributes i:list attribute, i:list attribute-signature, o:list prop. + % Coq attribute parser, eg [#[attribute=value] Command] % % Usage: % main _ :- % attributes A, % fetch -% coq.parse-attributes A Spec Opts, % parse/validate +% coq.parse-attributes A Spec Opts, % parse/validate % Opts => (mycode, get-option "foo" V, mycode). % use % % where [Opts] is a list of clauses [get-option StringName Value], where value @@ -584,7 +586,6 @@ coq.typecheck-attribute N (oneof L) K _ (error Msg) :- std.fold S "" (s\ a\ calc (a ^ " " ^ s)) OneOf, Msg is "Attribute " ^ N ^ " takes one of " ^ OneOf ^ ", got: " ^ K. -pred coq.parse-attributes i:list attribute, i:list attribute-signature, o:list prop. coq.parse-attributes L S O :- std.map S (x\r\ r = supported-attribute x) CS, diff --git a/elpi/elpi-reduction.elpi b/elpi/elpi-reduction.elpi index 7f5485741..8932e9895 100644 --- a/elpi/elpi-reduction.elpi +++ b/elpi/elpi-reduction.elpi @@ -50,7 +50,7 @@ whd X C X C. % assert A reduces to a constructor whd-indc A GR KA :- whd A [] VA C, !, VA = global (indc GR), KA = C. -% asserts progress was made. TODO: optimization: get rid of = test +% [whd1 T R] asserts progress was made in reducing T to R. whd1 T R :- whd T [] HD ARGS, unwind HD ARGS R, diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 8861309d1..6425b0901 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -5,6 +5,8 @@ Tutorian on the HOAS for Coq terms :author: Enrico Tassi +.. include:: tutorial_style.rst + .. Elpi is an extension language that comes as a library to be embedded into host applications such as Coq. @@ -60,7 +62,7 @@ We defer to later quotations and antiquotations: syntactic features that let one write terms in Coq's native syntax. Here we focus on the abstract syntax tree. -Let's start with the "gref" data type (for global rerence). +Let's start with the :type:`gref` data type (for global rerence). .. code:: @@ -68,12 +70,12 @@ Let's start with the "gref" data type (for global rerence). 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 +:type:`constant`, :type:`inductive` and :type:`constructor` are Coq specific data +types that are opaque to Elpi. Still the :type:`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 name to a `gref`. +The :builtin:`coq.locate` API resolves a name to a :type:`gref`. |*) @@ -112,15 +114,17 @@ Elpi Query lp:{{ .. note:: `indt «nat»` is not a term (or better a type). - The `global` term constructor turns a `gref` into an actual `term`. + The :constructor:`global` term constructor turns a :type:`gref` into an + actual :type:`term`. .. code:: type global gref -> term. -.. note:: the `app` term constructor is taking a list of terms and building - - the application. `app [global (indc «S»), global (indc «O»)]` is +.. note:: the :constructor:`app` term constructor is taking a list of terms and building + the application. + + `app [global (indc «S»), global (indc «O»)]` is the representation of `1`. .. code:: @@ -142,17 +146,17 @@ Elpi Query lp:{{ (*| -The `fun` constructor carries a pretty printing hint ```x```, the type +The :constructor:`fun` constructor carries a pretty printing hint ```x```, the type of the bound variable `nat` and a function describing the body: .. code:: type fun name -> term -> (term -> term) -> term. -.. note:: name is just for pretty printing, in spite of carrying +.. note:: :type:`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 written between ````` (backticks). + Elpi terms of type :type:`name` are just identifiers written between ````` (backticks). .. coq:: @@ -162,11 +166,11 @@ of the bound variable `nat` and a function describing the body: }}. - 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``` + API such as :builtin:`coq.name-suffix` lets one craft a family of names starting + from one, eg ``coq.name-suffix `H` 1 N`` sets `N` to ```H1``` -The other binders `prod` (Coq's `forall`, AKA `Π`) and `let` are similar, -so let's rather focus on `fix` here. +The other binders :constructor:`prod` (Coq's `forall`, AKA `Π`) and :constructor:`let` are similar, +so let's rather focus on :constructor:`fix` here. |*) @@ -181,7 +185,7 @@ Check match 3 as w in nat return bool with 0 => true | S _ => false end. (*| -The `fix` constructor carries a pretty printing hint, the number of the +The :constructor:`fix` constructor carries a pretty printing hint, the number of the recursive argument (starting at 0), the type and finally the body where the recursive call is represented via a bound variable @@ -189,7 +193,7 @@ recursive call is represented via a bound variable type fix name -> int -> term -> (term -> term) -> term. -A `match` constructor carries the term being inspected, the return clause +A :constructor:`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 order of the constructors in the inductive type declaration. @@ -219,7 +223,7 @@ Elpi Query lp:{{ (*| -The last term constructor worth discussing is `sort`. +The last term constructor worth discussing is :constructor:`sort`. .. code:: @@ -228,7 +232,7 @@ The last term constructor worth discussing is `sort`. type prop universe. type typ univ -> universe. -The opaque `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. @@ -251,7 +255,8 @@ Elpi Query lp:{{ automatically and put Coq universe variables in place of Elpi's unification variables (`U` and `V` below). -Let's play a bit more with universe constraints using the `coq.typecheck` API: +Let's play a bit more with universe constraints using the +:builtin:`coq.typecheck` API: |*) @@ -379,7 +384,7 @@ feature introduced in Coq 8.10. Coqlib gives you an indirection between your code and the actual name of constants. -.. note:: the optional `@` to disable implicits. +.. note:: The optional `@` disables implicit arguments. |*) @@ -461,14 +466,15 @@ 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 following two predicates are used for that purpose: +The two predicates :builtin:`decl` and :builtin:`def` are used +for that purpose: .. code:: pred decl i:term, o:name, o:term. % Var Name Ty pred def i:term, o:name, o:term, o:term. % Var Name Ty Bo -where `def` is used to cross `let-in`. +where `def` is used to cross a `let`. |*) @@ -485,17 +491,15 @@ Elpi Query lp:{{ (*| -In order to ease this task, Coq-Elpi provides a few commodity macros in -`coq-builtin.elpi `_. - -For example: +In order to ease this task, Coq-Elpi provides a few commodity macros such as +`@pi-decl`: .. code:: macro @pi-decl N T F :- pi x\ decl x N T => F x. -Remember the precedence of lambda abstraction `x\` which lets you write the -following code without parentheses for `F`. +.. note:: the precedence of lambda abstraction `x\ ` lets you write the + following code without parentheses for `F`. |*) @@ -511,7 +515,9 @@ Elpi Query lp:{{ (*| -.. tip:: `@pi-decl N Ty x\ ` takes arguments in the same order of `fun` +.. tip:: `@pi-decl N Ty x\ ` takes arguments in the same order of :constructor:`fun` and + :constructor:`prod`, while + `@pi-def N Ty Bo x\ ` takes arguments in the same order of :constructor:`let`. ========================== Holes (implicit arguments) @@ -535,8 +541,8 @@ Elpi Query lp:{{ (*| -Before the call to coq.typecheck, coq.sigma.print prints nothing -interesting, while after the call it also prints the following +Before the call to :builtin:`coq.typecheck`, :builtin:`coq.sigma.print` +prints nothing interesting, while after the call it also prints the following syntactic constraint: .. code:: @@ -544,7 +550,7 @@ syntactic constraint: evar X0 (global (indt «nat»)) X0 /* suspended on X0 */ -which indicates that the hole `X0` is expected to have type nat. +which indicates that the hole `X0` is expected to have type `nat`. Now the bijective mapping from Coq evars to Elpi's unification variables is not empty anymore: @@ -638,7 +644,7 @@ does not work in all situations. In particular it only works for Elpi unification variables which are in the pattern fragment, which mean that they are applied only to distinct names (bound variables). -This is the case for all the {{ _ }} one uses inside quotations, for +This is the case for all the `{{ _ }}` one writes inside quotations, for example, but it is not hard to craft a term outside this fragment. In particular we can use Elpi's substitution (function application) to put an arbitrary term in place of a bound variable. @@ -680,7 +686,7 @@ 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 :macro:`@holes!` option. |*) @@ -699,15 +705,14 @@ Elpi Query lp:{{ (*| -Note that after the call to `coq.typecheck`, `X0`, is assigned with -`_\ X1`, that is, the offending argument has been pruned. +Note that after the call to :builtin:`coq.typecheck`, `X0` is assigned the term +`_\ X1`, that means that the offending argument has been pruned. -All APIs taking a term support this option which is documented in details -in `coq-builtin.elpi `_. +.. note:: All APIs taking a term support the :macro:`@holes!` option. -In addition to `@holes!` option, there is a class of APIs which can deal with +In addition to :macro:`@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 does with +"skeleton". A skeleton is not modified in place, as :builtin:`coq.typecheck` does with its first input, but is rather elaborated to a term related to it. In some sense APIs taking a skeleton are more powerful, because the can modify the structure of the term, eg. insert a coercions, but are less @@ -748,6 +753,4 @@ about or the one about `tactics `_. -.. include:: tutorial_style.rst - |*) \ No newline at end of file diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index 9ffca77d0..d6ed41d62 100644 --- a/examples/tutorial_coq_elpi_command.v +++ b/examples/tutorial_coq_elpi_command.v @@ -5,6 +5,8 @@ Tutorial on Coq commands :author: Enrico Tassi +.. include:: tutorial_style.rst + .. Elpi is an extension language that comes as a library to be embedded into host applications such as Coq. @@ -25,7 +27,6 @@ Tutorial on Coq commands "gares.coq-elpi-lang" extension. In CoqIDE please chose "coq-elpi" in Edit -> Preferences -> Colors. - This tutorial assumes the reader is familiar with Elpi and the HOAS representation of Coq terms; if it is not the case, please take a look at these other tutorials first: @@ -60,9 +61,9 @@ The program declaration is made of 3 parts. 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 `coq.say`) and data types (eg Coq terms) are loaded from +* APIs (eg :builtin:`coq.say`) and data types (eg Coq :type:`term` s) are loaded from `coq-builtin.elpi `_ -* some utilities, like `copy` or `whd1` are loaded from +* some utilities, like :lib:`copy` or :libred:`whd1` are loaded from `elpi-command-template.elpi `_ @@ -99,7 +100,7 @@ code if you are reading this online): Hello [str world!] The string `"world!"` we passed to the command is received by the code -as `(str "world!")`. Note that `coq.say` won't print quotes around strings. +as `(str "world!")`. Note that :builtin:`coq.say` won't print quotes around strings. ================= Command arguments @@ -161,8 +162,7 @@ the type of the record (which wa omitted) defaults to `Type` (for some level `X0`). Finally note the type of the second field sees `c0` (the value of the first field). -See the `argument` data type in -`coq-builtin.elpi `_. +See the :type:`argument` data type for a detailed decription of all the arguments a command can receive. ======================== @@ -191,8 +191,8 @@ Fail Elpi check_arg (1 = true). 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 `std.assert-ok!` combinator +The :builtin:`coq.typecheck` API has 3 arguments: a term, its type and a :stdtype:`diagnostic` +which can either be `ok` or `(error Message)`. The :stdlib:`assert-ok!` combinator checks if the diagnostic is `ok`, and if not it prints the error message and bails out. @@ -211,9 +211,10 @@ Check (1 = true). The command still fails even if we told Coq how to inject booleans values into the natural numbers. Indeed the Check commands works. -The `coq.typecheck` API modifies the term in place, it can assign +The call to :builtin:`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` +structure of the term. To do so, one has to use the +:builtin:`coq.elaborate-skeleton` API. |*) @@ -248,8 +249,8 @@ Example: 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 `coq.env.const` -for reading and `coq.env.add-const` for writing. +and are named after the global refence 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, it generates a term of type nat whose value is the number of constructors @@ -285,12 +286,12 @@ Fail Elpi constructors_num not_there bla. (*| The command starts by locating the first argument and asserting it points to -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) `std.assert!` aborts with the given error message. +an inductive type. This line is idiomatic: :builtin:`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`) :stdlib:`assert!` aborts with the given error message. -`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.indet-decl` lets +:builtin:`coq.env.indt` lets one access all the details of an inductive type, here +we just use the list of constructors. The twin API :builtin:`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. @@ -300,7 +301,7 @@ Then it crafts a natural number and declares a constant. Example: Abstracting an inductive ================================= -For the sake of introducing `copy`, the swiss army knife of λProlog, we +For the sake of introducing :lib:`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. @@ -359,10 +360,9 @@ Print tree'. As expected `tree'` as a parameter `A`. -Now lets focus on `copy`. The standard +Now lets focus on :lib:`copy`. The standard coq library (loaded by the command template) contains a definition of copy -for terms and declarations -`coq-lib.elpi `_. +for terms and declarations. An excerpt: @@ -374,7 +374,7 @@ An excerpt: copy T T1, pi x\ copy (F x) (F1 x). copy (app L) (app L1) :- !, std.map L copy L1. -Copy implements the identity: it builds, recursively, a copy of the first +`copy` implements the identity: it builds, recursively, a copy of the first term into the second argument. Unless one loads in the context a new clause, which takes precedence over the identity ones. Here we load @@ -389,20 +389,22 @@ which, at run time, looks like copy (app [global (indt «option»), global (indt «nat»)]) c0 and that clause masks the one for `app` when the sub-term being copied is -exactly (`option nat`). `copy-indt-decl` copies an inductive declaration and -calls `copy` on all the terms it contains (e.g. the type of the constructors). +exactly `option nat`. The API :lib:`copy-indt-decl` copies an inductive declaration +and calls `copy` on all the terms it contains (e.g. the type of the constructors). + +The :lib:`copy` predicate is very flexible, but sometimes one needs to collect +some data along the way. The sibling API :lib:`fold-map` lets one do that. -The `copy` predicate is very flexible, but sometimes one needs to collect -some data along the copy. The sibling `fold-map` lets one do that. An excerpt: +An excerpt: .. code:: 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 :lib:`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 :lib:`copy` to capture them. ==================================== @@ -420,7 +422,7 @@ and a Db can be later extended via `Elpi Accumulate`. A Db is pretty much like a regular program but can be shared among other programs *and* is accumulated by name. Moreover the Db and can be -extended by Elpi programs as well thanks to the API `coq.elpi.accumulate`. +extended by Elpi programs as well thanks to the API :builtin:`coq.elpi.accumulate`. Since is a Db is accumulated by name, each time a program runs, the currect contents of the Db are loaded, is usually just the type declaration @@ -435,8 +437,8 @@ Elpi Db age.db lp:{{ % We like Db names to end in a .db suffix % A typical Db is made of one main predicate pred age o:string, o:int. - % the Db is empty for now, we put a clause giving a descriptive error - % and we name that clause "age.fail". + % the Db is empty for now, we put a clause giving a + % descriptive error and we name that clause "age.fail". :name "age.fail" age Name _ :- coq.error "I don't know who" Name "is!". @@ -507,10 +509,9 @@ Elpi age "alice". Additions to a Db are Coq object, a bit like a Notation or a Type Class instance: these object live inside a Coq module (or a Coq file) and become active when that module is Imported. Hence deciding to which Coq module these -extra clauses belong is important and `coq.elpi.accumulate` provides a few +extra clauses belong is important and :builtin:`coq.elpi.accumulate` provides a few options to tune that (here we passed _, that uses the default setting). -All the options to `coq.elpi.accumulate` are described in coq-builtin.elpi, -as all other APIs. +See the :type:`scope` and :type:`clause` data types for more info. ===================== Attributes and Export @@ -541,8 +542,8 @@ location in the source file of the command. Then we find an attribute for the string `"33"`. Attributes are usually validated (parsed) and turned into regular options -using `coq.parse-attributes` (its implementation and documentation is in -coq-lib.elpi): +using :lib:`coq.parse-attributes` and a description of their types using +the :libtype:`attribute-type` data type: |*) @@ -599,7 +600,8 @@ Elpi Command go. Elpi Accumulate lp:{{ main [str Src, str "=>", str Tgt, str "/", str F] :- !, coq.say "going from" Src "to" Tgt "via" F. - main _ :- coq.error "Parse error! Use: go => / ". + main _ :- + coq.error "Parse error! Use: go => / ". }}. Elpi Typecheck. Elpi Export go. @@ -624,14 +626,11 @@ Fail bad 1. (*| -The command has indeed failed with message: -The elpi command bad failed without giving a specific error message. Please -report this inconvenience to the authors of the program. +You should use the :builtin:`coq.error` API the :stdlib:`assert!` family ones +to abort a program. Warnings can be reported using the :builtin:`coq.warning`. This is really the end, unless you want to learn more about writing `tactics `_ in Elpi, in that case look at that tutorial ;-) -.. include:: tutorial_style.rst - |*) \ No newline at end of file diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v index 9c4c5f654..fe74a58eb 100644 --- a/examples/tutorial_coq_elpi_tactic.v +++ b/examples/tutorial_coq_elpi_tactic.v @@ -5,6 +5,8 @@ Tutorial on Coq tactics :author: Enrico Tassi +.. include:: tutorial_style.rst + .. Elpi is an extension language that comes as a library to be embedded into host applications such as Coq. @@ -71,10 +73,10 @@ The tactic declaration is made of 3 parts. 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 `coq.say`) and data types (eg Coq terms) are loaded from +* APIs (eg :builtin:`coq.say`) and data types (eg Coq terms) are loaded from `coq-builtin.elpi `_ -* some utilities, like `copy` or `whd1` are loaded from - `elpi-tactic-template.elpi `_ +* some utilities, like :lib:`copy` or :libred:`whd1` are loaded from + `elpi-command-template.elpi `_ The second one `Elpi Accumulate ...` loads some extra code. @@ -95,8 +97,8 @@ 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 :builtin:`solve` which maps a :type:`goal` +into a list of :type:`sealed-goal` (representing subgoals). Tactics written in Elpi can be invoked by prefixing its name with `elpi`. @@ -143,7 +145,7 @@ The `_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 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 :builtin:`solve` predicate relates one goal to a list of subgoals, we implement our first tactic which blindly tries to solve the goal. |*) @@ -202,11 +204,11 @@ 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 tactics, in +There is a family of APIs named after :libtac:`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. +Usually a tactic builds a (possibly partial) term and calls :libtac:`refine` on it. Let's rewrite the `blind` tactic using this schema. @@ -279,16 +281,18 @@ The tactic `split` succeeds twice, stopping on the two identical goals `True` an the one which is an evar of type `Prop`. We then invoke `blind` on all goals. In the third case the type checking -constraint triggered by assigning `{{0}`} to `Proof` fails because -its type `{{nat}}` is not of sort `Prop`, so it backtracks and picks `{{I}}`. +constraint triggered by assigning `{{0}}` to `Trigger` fails because +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. -`coq.ltac.call` invokes an Ltac piece of code passing to it the desired +The API :libtac:`call`, in the `coq.ltac.` namespace, invokes some Ltac piece +of code passing to it the desired arguments. Then it builds the list of subgoals. -Here we pass an integer, passed to fail, and a term, passed to apply. +Here we pass an integer, which in turn is passed to `fail`, and a term, +which is turn is passed to `apply`. |*) @@ -339,16 +343,16 @@ The convention is that numbers like `1` are passed a `int `, identifiers or strings are passed as `str ` and terms have to be put between parentheses. -Remark that 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 `X0`. +.. important:: terms are received in raw format, eg before elaboration. + + Indeed the type argument to `eq` is a variable. + One can use APIs like :builtin:`coq.elaborate-skeleton` to infer holes like `X0`. -See the `argument` data type in -`coq-builtin.elpi `_. +See the :type:`argument` data type for a detailed decription of all the arguments a tactic can receive. -Now let's write a tactic which behave pretty much like the `refine` one -from Coq, but prints what it does. +Now let's write a tactic which behave pretty much like the :libtac:`refine` one +from Coq, but prints what it does using the API :builtin:`coq.term->string`. |*) @@ -419,13 +423,14 @@ Abort. (*| -============================ -Examples: assumption and set -============================ +================================ +Examples: `assumption` and `set` +================================ -A very simple tactic we can implement is assumption: we look up in the proof +A very simple tactic we can implement is `assumption`: we look up in the proof context for an hypothesis which unifies with the goal. -Recall that Ctx is made of decl and def clauses (here, for simplicity, we +Recall that `Ctx` is made of :builtin:`decl` and :builtin:`def` +clauses (here, for simplicity, we ignore the latter case). |*) @@ -454,7 +459,7 @@ 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 out tactic looking for an assumption which is unifiable with +Let's improve our tactic looking for an assumption which is unifiable with the goal, an not just alpha convertible |*) @@ -478,7 +483,7 @@ Qed. (*| -`refine` does unify the type of goal with the type of the term, hence we can +:libtac:`refine` does unify the type of goal with the type of the term, hence we can just write the follwing code, which is very close to our initial `blind` tactic, but it picks candidates from the context. @@ -503,9 +508,9 @@ Qed. (*| Now let's write a tactic which takes a term, possibly with holes, and -makes a let-int out of it, a bit like the `set` tactic. +makes a let-in out of it, a bit like the `set` tactic. -It will be the occasion to explain the `copy` utility. +It will be the occasion to explain the :lib:`copy` utility. |*) @@ -533,10 +538,7 @@ Abort. This first approximation only prints the term it found, or better the first intance of the given term. -Now lets focus on `copy`. The standard -Coq library `coq-lib.elpi `_. -(loaded by the command template) contains a definition of copy -for terms and declarations. An excerpt: +Now lets focus on :lib:`copy`. An excerpt: .. code:: @@ -560,7 +562,7 @@ which, at run time, looks like copy (app [global (indt «andn»), sort prop, sort prop, c0, X0 c0 c1]) c2 -and that clause masks the one for `app` when the sub-term being copied is +and that clause masks the one for :constructor:`app` when the sub-term being copied matches `(P /\ _)`. Now let's refine the tactic to build a let-in, and complain if the @@ -677,14 +679,14 @@ assigned to the trigger `X1` has to be elaborated to the final proof term `X0`, that should be a well typed term of type `x + 1 = 0`. This means that when an Elpi tactic assigns a value to `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. +it is currently implemented by calling the :builtin:`coq.elaborate-skeleton` API. Given this set up, it is impossible to use a term of the wrong type as a proof. Lets declare simle tactic that tries `0` and `I` as proof terms for a goal, without even looking at it. The refine utility simply assigns the trigger and then calls the -`coq.ltac.collect-goals` API on the elaborated proof term to get the list +:builtin:`coq.ltac.collect-goals` API on the elaborated proof term to get the list of sub goals Let's rewrite the split tactic using only low level operations. @@ -717,7 +719,7 @@ 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. -The `coq.ltac.collect-goals` API helps us to do this operation. +The :builtin:`coq.ltac.collect-goals` API helps us doing this. |*) @@ -742,15 +744,15 @@ Qed. (*| -At the light of that, refine is simply: +At the light of that, :libtac:`refine` is simply: .. code:: 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`. The only detail -we still have to explain is what exactly a `sealed-goal` is. A sealed goal +Now that we know the low level plumbing, we can use :libtac:`refine`. The only detail +we still have to explain is what exactly a :type:`sealed-goal` is. A sealed goal wraps into a single object all the proof variable and the assumptions about them, making this object easy (or better, sound) to pass around. More details in the next section. @@ -766,9 +768,9 @@ You can access this feature by using `all: tactic`: * 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 clause for -the `msolve` predicate. Since such tactic will need to manipulate multiple +the :builtin:`msolve` predicate. Since such 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 its proof context. +of :type:`sealed-goal`, a data type which seals a goal and its proof context. |*) @@ -807,10 +809,11 @@ the list itself. We see something like: (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` holds a regular goal, which in +:constructor:`nabla` binds all proof variables, then :constructor:`seal` +holds a regular goal, which in turn carries the context (the type of the proof variables). -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 :libtac:`open` utility, which postulates all proof variables using pi and loads the goal context using `=>`. @@ -880,7 +883,8 @@ the same hole. Indeed by solving one, we can also solve the other. On the notion of sealed-goal it is easy to define the usual LCF combinators, also known as Ltac tacticals. A few ones can be find in the -`elpi-ltac.elpi file `_. +`elpi-ltac.elpi file `_ +, see for example :libtac:`try`. As we hinted before, tactic arguments are attached to the goal, since they can mention proof variables. So the Ltac code @@ -935,8 +939,9 @@ a datum to be passed to what follows thenl [ open (tac1 Datum), open (tac2 Datum) ] -but the binder structure of `sealed-goal` would prevent `Datum` to mention +but the binder structure of :type:`sealed-goal` would prevent `Datum` to mention proof variables, that would otherwise escape the sealing. The utility +:libtac:`set-goal-arguments` .. code:: @@ -1010,6 +1015,4 @@ Print baz. That is all folks! -.. include:: tutorial_style.rst - |*) diff --git a/examples/tutorial_style.rst b/examples/tutorial_style.rst index 4590ab518..f0673de92 100644 --- a/examples/tutorial_style.rst +++ b/examples/tutorial_style.rst @@ -1,3 +1,53 @@ + +:alectryon/pygments/cmd: Elpi Command Tactic Program Accumulate Typecheck Export Db +:alectryon/pygments/tacn: elpi + +.. role:: elpi-api(ghref) + :pattern: ^(% \[$name|(external )?pred $name) + +.. role:: lib(elpi-api) + :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi + +.. role:: libred(elpi-api) + :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-reduction.elpi + +.. role:: libtac(elpi-api) + :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi + +.. role:: builtin(elpi-api) + :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + +.. role:: stdlib(elpi-api) + :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi + + +.. role:: elpi-type(ghref) + :pattern: ^(kind $name|typeabbrev $name) + +.. role:: type(elpi-type) + :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + +.. role:: libtype(elpi-type) + :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi + +.. role:: stdtype(elpi-type) + :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi + + +.. role:: elpi-constructor(ghref) + :pattern: ^type $name + +.. role:: constructor(elpi-constructor) + :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + + +.. role:: elpi-macro(ghref) + :pattern: ^macro $name + +.. role:: macro(elpi-macro) + :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + + .. raw:: html From 3888024fe9570bcd006fec008cb688e84990f576 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 Aug 2021 17:23:25 +0200 Subject: [PATCH 2/9] wip --- examples/tutorial_elpi_lang.v | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/examples/tutorial_elpi_lang.v b/examples/tutorial_elpi_lang.v index fde191f33..356af9466 100644 --- a/examples/tutorial_elpi_lang.v +++ b/examples/tutorial_elpi_lang.v @@ -5,6 +5,8 @@ Tutorial on the Elpi programming language :author: Enrico Tassi +.. include:: tutorial_style.rst + .. Elpi is an extension language that comes as a library to be embedded into host applications such as Coq. @@ -71,7 +73,7 @@ The next commands accumulates on top of the current `tutorial` program a predicate declaration for `age` and 3 clauses representing our knowledge about our terms. -Note that `int` is the primitive data type of integers. +Note that :stdtype:`int` is the primitive data type of integers. |*) @@ -130,7 +132,7 @@ Elpi Query lp:{{ (*| -Note that ``"strings"`` are also a primitive data type. +Note that :stdtype:`string` is also a primitive data type. `age` is said to be a relation (in contrast to a function), since it computes both ways: we can ask Elpi which person `P` is 23 years old. @@ -574,6 +576,7 @@ Elpi Query lp:{{ Let's run step by step this example. The clause for `fun` is used: + * `Ty` is assigned `arrow A1 B1` * a fresh constant `c1` is created by the `pi` construct * `of c1 A1` is added to the program by the `=>` construct, @@ -581,12 +584,14 @@ The clause for `fun` is used: Again, the clause for `fun` is used (since its variables are universally quantified, we use fresh `A2`, `B2`... this time): + * `B1` is assigned `arrow A2 B2` * a fresh `c2` is created by the `pi` construct * `of c2 A2` is added to the program by the `=>` construct, * the new query `of c1 B2` is run. The (hypotetical) clause `of c1 A1` is used: + * `B2` gets assigned to `A1` The value of `Ty` is hence `arr A1 (arr A2 A1)`, a good type @@ -889,8 +894,8 @@ Elpi Query lp:{{ X is 3 + 2, Y is "result " ^ "=", coq.say Y X }}. (*| Chaining "relations" can be painful, especially when -they look like functions. Here we use `std.append` -and `std.rev` as examples. +they look like functions. Here we use :stdlib:`append` +and :stdlib:`rev` from the `std.` namespace as examples. |*) @@ -927,11 +932,11 @@ Elpi Query lp:{{ (*| The two programs are equivalent, and indeed the latter is -elaborated into the former. Expressions between ``{`` and ``}`` are +elaborated into the former. Expressions between `{` and `}` are said to be spilled out and placed just before the predicate that contains them. -The `calc` predicate is just a wrapper around the infix `is` +The :stdlib:`calc` predicate is just a wrapper around the infix `is` |*) @@ -982,7 +987,7 @@ Elpi Query lp:{{ (*| The problem with `bad` is that `TMP` is fresh each time the clause -is used, but not every time the anonymous predicate passed to `std.map` +is used, but not every time the anonymous predicate passed to :stdlib:`map` is used. Technically `TMP` is quantified (allocated) where `L` and `Result` are. @@ -1103,7 +1108,8 @@ Elpi Program debug lp:{{ pred mypred i:int. - :if "DEBUG_MYPRED" mypred X :- + :if "DEBUG_MYPRED" + mypred X :- coq.say "calling mypred on " X, fail. mypred 0 :- coq.say "ok". @@ -1222,8 +1228,6 @@ the `Elpi home on github `_. Three more tutorials specific to Elpi as an extension language for Coq can be found in the `examples folder `_. -.. include:: tutorial_style.rst - |*) From b4c4b0c4405010a426af7fe98f4a3db9f84219e1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Aug 2021 10:52:31 +0200 Subject: [PATCH 3/9] cleanup --- examples/tutorial_coq_elpi_HOAS.v | 4 ++-- examples/tutorial_coq_elpi_tactic.v | 12 ++++++------ examples/tutorial_elpi_lang.v | 4 ++-- examples/tutorial_style.rst | 22 ++++++++++++---------- 4 files changed, 22 insertions(+), 20 deletions(-) diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 6425b0901..239a1db09 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -384,8 +384,6 @@ feature introduced in Coq 8.10. Coqlib gives you an indirection between your code and the actual name of constants. -.. note:: The optional `@` disables implicit arguments. - |*) Register Coq.Init.Datatypes.nat as my.N. @@ -398,6 +396,8 @@ Elpi Query lp:{{ }}. (*| + +.. note:: The (optional) `@` in `lib:@some.name` disables implicit arguments. The `{{:gref .. }}` quotation lets one the gref data type, instead of the term one. It supports `lib:` as well. diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v index fe74a58eb..9942c5632 100644 --- a/examples/tutorial_coq_elpi_tactic.v +++ b/examples/tutorial_coq_elpi_tactic.v @@ -287,7 +287,7 @@ 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 :libtac:`call`, in the `coq.ltac.` namespace, invokes some Ltac piece +The API :libtac:`coq.ltac.call` invokes some Ltac piece of code passing to it the desired arguments. Then it builds the list of subgoals. @@ -385,8 +385,8 @@ Abort. 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: +In particular elpi tacname accepts as arguments the following `bridges +for Ltac values `_ : * `ltac_string:(v)` (for `v` of type `string` or `ident`) * `ltac_int:(v)` (for `v` of type `int` or `integer`) @@ -598,7 +598,7 @@ Abort. (*| The new hole is annotated with a type. Here we use quotations to write -that term, but we could have used the commodity macro +that term, but we could have used the commodity :macro:`@cast` macro: .. code:: @@ -608,11 +608,11 @@ which unfolds to .. code:: - let _ (Tabs x) (Hole x) y\y + let `cast` (Tabs x) (Hole x) y\y which is how "type casts" are represented in the HOAS of terms. -For more example of (basic) tactics written in Elpi see the +For more examples of (basic) tactics written in Elpi see the `eltac app `_. diff --git a/examples/tutorial_elpi_lang.v b/examples/tutorial_elpi_lang.v index 356af9466..3fa90df6f 100644 --- a/examples/tutorial_elpi_lang.v +++ b/examples/tutorial_elpi_lang.v @@ -894,8 +894,8 @@ Elpi Query lp:{{ X is 3 + 2, Y is "result " ^ "=", coq.say Y X }}. (*| Chaining "relations" can be painful, especially when -they look like functions. Here we use :stdlib:`append` -and :stdlib:`rev` from the `std.` namespace as examples. +they look like functions. Here we use :stdlib:`std.append` +and :stdlib:`std.rev` as examples. |*) diff --git a/examples/tutorial_style.rst b/examples/tutorial_style.rst index f0673de92..39132c153 100644 --- a/examples/tutorial_style.rst +++ b/examples/tutorial_style.rst @@ -6,46 +6,48 @@ :pattern: ^(% \[$name|(external )?pred $name) .. role:: lib(elpi-api) - :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi + :src: LPCIC coq-elpi master elpi/coq-lib.elpi .. role:: libred(elpi-api) - :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-reduction.elpi + :src: LPCIC coq-elpi master elpi/elpi-reduction.elpi .. role:: libtac(elpi-api) - :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi + :mangle: name.replace('coq.ltac.','') + :src: LPCIC coq-elpi master elpi/elpi-ltac.elpi .. role:: builtin(elpi-api) - :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + :src: LPCIC coq-elpi master coq-builtin.elpi .. role:: stdlib(elpi-api) - :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi + :mangle: name.replace('std.','') + :src: LPCIC coq-elpi master elpi-builtin.elpi .. role:: elpi-type(ghref) :pattern: ^(kind $name|typeabbrev $name) .. role:: type(elpi-type) - :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + :src: LPCIC coq-elpi master coq-builtin.elpi .. role:: libtype(elpi-type) - :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi + :src: LPCIC coq-elpi master elpi/coq-lib.elpi .. role:: stdtype(elpi-type) - :src: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi + :src: LPCIC coq-elpi master elpi-builtin.elpi .. role:: elpi-constructor(ghref) :pattern: ^type $name .. role:: constructor(elpi-constructor) - :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + :src: LPCIC coq-elpi master coq-builtin.elpi .. role:: elpi-macro(ghref) :pattern: ^macro $name .. role:: macro(elpi-macro) - :src: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi + :src: LPCIC coq-elpi master coq-builtin.elpi .. raw:: html From cdb295a53aa7aac65c594b0d7b867171d51dc819 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Aug 2021 11:01:49 +0200 Subject: [PATCH 4/9] build the doc using my fork --- .github/workflows/doc.yml | 6 +++++- Makefile | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index 713bcabe6..54a5e4c44 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -36,7 +36,11 @@ jobs: - name: build doc run: | - stty cols 65 || true + git clone https://github.com/gares/alectryon -b ghref + mkdir alectryon/bin + (cd alectryon/bin; ln -s ../alectryon.py alectryon) + export PATH=$PWD/alectryon/bin:$PATH + stty cols 60 || true opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1 - name: deploy diff --git a/Makefile b/Makefile index e7a61a9d3..82098fc70 100644 --- a/Makefile +++ b/Makefile @@ -52,7 +52,7 @@ doc: $(DOCDEP) @echo "########################## generating doc ##########################" @mkdir -p doc @$(foreach tut,$(wildcard examples/tutorial*.v),\ - echo ALECTRYON $(tut); alectryon/alectryon.py \ + echo ALECTRYON $(tut); alectryon \ --frontend coq+rst \ --output-directory doc \ --sertop-arg=--topfile=Tutorial \ From 343a42651cd2cb41e9527f76196683411928ea56 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Aug 2021 13:11:59 +0200 Subject: [PATCH 5/9] typo --- examples/tutorial_coq_elpi_HOAS.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 239a1db09..66938980b 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -1,6 +1,6 @@ (*| -Tutorian on the HOAS for Coq terms +Tutorial on the HOAS for Coq terms ********************************** :author: Enrico Tassi From 3741a9de0974e31a69ff45155096fb351445988f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Aug 2021 13:12:03 +0200 Subject: [PATCH 6/9] colors --- examples/tutorial_style.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/tutorial_style.rst b/examples/tutorial_style.rst index 39132c153..35b9749f7 100644 --- a/examples/tutorial_style.rst +++ b/examples/tutorial_style.rst @@ -1,5 +1,5 @@ -:alectryon/pygments/cmd: Elpi Command Tactic Program Accumulate Typecheck Export Db +:alectryon/pygments/cmd: Elpi Command Tactic Program Accumulate Typecheck Export Db Query :alectryon/pygments/tacn: elpi .. role:: elpi-api(ghref) From f7b242e7999a9bfb1199d09b81ca15b28363e833 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Aug 2021 13:12:10 +0200 Subject: [PATCH 7/9] use VS style --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 82098fc70..89cc36243 100644 --- a/Makefile +++ b/Makefile @@ -55,7 +55,7 @@ doc: $(DOCDEP) echo ALECTRYON $(tut); alectryon \ --frontend coq+rst \ --output-directory doc \ - --sertop-arg=--topfile=Tutorial \ + --pygments-style vs \ -R theories elpi -Q src elpi \ $(tut) &&) true @cp stlc.html doc/ From a6ec4efb1871fb3e999b1b59824a53bd9a7cb4b2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Aug 2021 15:45:40 +0200 Subject: [PATCH 8/9] fixes --- examples/tutorial_coq_elpi_HOAS.v | 2 +- examples/tutorial_coq_elpi_command.v | 20 ++++++++++---------- examples/tutorial_style.rst | 6 ++++++ 3 files changed, 17 insertions(+), 11 deletions(-) diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 66938980b..80bee814d 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -459,7 +459,7 @@ Fail Elpi Query lp:{{ This fatal error says that `x` in `(Bo x)` is unknown to Coq. It is a variable postulated in Elpi, but it's type, `nat`, was lost. There -is nothing wrong per se in using `pi x\` as we did if we don't call Coq +is nothing wrong per se in using `pi x\ ` as we did if we don't call Coq APIs under it. But if we do, we have to record the type of `x` somewhere. In some sense Elpi's way of traversing a binder is similar to a Zipper. diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index d6ed41d62..7c059f905 100644 --- a/examples/tutorial_coq_elpi_command.v +++ b/examples/tutorial_coq_elpi_command.v @@ -262,16 +262,16 @@ Elpi Command constructors_num. Elpi Accumulate lp:{{ - pred int->nat i:int, o:term. - int->nat 0 {{ 0 }}. - int->nat N {{ S lp:X }} :- M is N - 1, int->nat M X. - - main [str IndName, str Name] :- - std.assert! (coq.locate IndName (indt GR)) "not an inductive type", - coq.env.indt GR _ _ _ _ Kn _, % the names of the constructors - std.length Kn N, % count them - int->nat N Nnat, % turn the integer into a nat - coq.env.add-const Name Nnat _ _ _. % save it +pred int->nat i:int, o:term. +int->nat 0 {{ 0 }}. +int->nat N {{ S lp:X }} :- M is N - 1, int->nat M X. + +main [str IndName, str Name] :- + std.assert! (coq.locate IndName (indt GR)) "not an inductive type", + coq.env.indt GR _ _ _ _ Kn _, % the names of the constructors + std.length Kn N, % count them + int->nat N Nnat, % turn the integer into a nat + coq.env.add-const Name Nnat _ _ _. % save it }}. Elpi Typecheck. diff --git a/examples/tutorial_style.rst b/examples/tutorial_style.rst index 35b9749f7..8589849c7 100644 --- a/examples/tutorial_style.rst +++ b/examples/tutorial_style.rst @@ -84,6 +84,12 @@ font-feature-settings: "XV00" 1; /* Use Coq ligatures when Iosevka is available */ line-height: initial; } + + .highlight .-ElpiFunction { color: #795E26 } + .highlight .-ElpiVariable { color: #0000ff } + .highlight .k-ElpiKeyword { color: #AF00DB } + .highlight .k-ElpiMode { color: #811f3f } + .highlight .m-ElpiInteger { color: #098658 } `; document.getElementsByTagName('head')[0].appendChild(style); From 2f74ca1af8a6c0ff57acef9154128eb50959023a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 21 Aug 2021 12:20:27 +0200 Subject: [PATCH 9/9] use my branch --- .github/workflows/doc.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index 54a5e4c44..d77d87dd3 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -36,7 +36,7 @@ jobs: - name: build doc run: | - git clone https://github.com/gares/alectryon -b ghref + git clone https://github.com/gares/alectryon -b pygments mkdir alectryon/bin (cd alectryon/bin; ln -s ../alectryon.py alectryon) export PATH=$PWD/alectryon/bin:$PATH