Skip to content

Commit af479a3

Browse files
proux01proux01
authored
Merge pull request rocq-community#72 from coq-community/refine-docs
Refine documentation
2 parents d0df5b0 + 8016883 commit af479a3

File tree

5 files changed

+165
-94
lines changed

5 files changed

+165
-94
lines changed

‎.github/workflows/coq-action.yml renamed to ‎.github/workflows/docker-action.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
name: CI
1+
name: Docker CI
22

33
on:
44
push:

‎.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,3 +43,6 @@ _build
4343

4444
# coqpp generated file
4545
src/abstraction.ml
46+
47+
# lia cache
48+
.lia.cache

‎README.md

Lines changed: 62 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,17 @@
1+
<!---
2+
This file was generated from `meta.yml`, please do not edit manually.
3+
Follow the instructions on https://github.com/coq-community/templates to regenerate.
4+
--->
15
# Paramcoq
26

3-
[![CI][action-shield]][action-link]
7+
[![Docker CI][docker-action-shield]][docker-action-link]
48
[![Contributing][contributing-shield]][contributing-link]
59
[![Code of Conduct][conduct-shield]][conduct-link]
610
[![Zulip][zulip-shield]][zulip-link]
711
[![DOI][doi-shield]][doi-link]
812

9-
[action-shield]: https://github.com/coq-community/paramcoq/workflows/CI/badge.svg?branch=master
10-
[action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow%3ACI
13+
[docker-action-shield]: https://github.com/coq-community/paramcoq/workflows/Docker%20CI/badge.svg?branch=master
14+
[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI"
1115

1216
[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
1317
[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -22,8 +26,11 @@
2226
[doi-shield]: https://zenodo.org/badge/DOI/10.4230/LIPIcs.CSL.2012.399.svg
2327
[doi-link]: https://doi.org/10.4230/LIPIcs.CSL.2012.399
2428

25-
The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunk of standard library.
26-
29+
A Coq plugin providing commands for generating parametricity statements.
30+
Typical applications of such statements are in data refinement proofs.
31+
Note that the plugin is still in an experimental state - it is not very user
32+
friendly (lack of good error messages) and still contains bugs. But it
33+
is usable enough to "translate" a large chunk of the standard library.
2734

2835
## Meta
2936

@@ -37,9 +44,8 @@ The plugin is still in an experimental state. It is not very user friendly (lack
3744
- Matthieu Sozeau
3845
- Coq-community maintainer(s):
3946
- Pierre Roux ([**@proux01**](https://github.com/proux01))
40-
- License: [MIT](LICENSE)
41-
- Compatible Coq versions: The master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq.
42-
47+
- License: [MIT License](LICENSE)
48+
- Compatible Coq versions: The master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq
4349
- Additional dependencies: none
4450
- Coq namespace: `Param`
4551
- Related publication(s):
@@ -65,37 +71,57 @@ make install
6571
```
6672

6773

68-
Available commands
69-
------------------
70-
71-
The default arity is 2.
72-
73-
- Parametricity *ident* as *name* [arity *n*].
74-
75-
Declare the translation named *name* from the translation of the constant or inductive *ident*.
76-
77-
- Parametricity [Recursive] *ident* [arity *n*] [qualified].
78-
79-
The default name for the translation of the constant or inductive *ident* is automatically generated (from its unqualified name).
80-
You can use the `Recursive` option to recursively translate all the constants and inductives which are used by *ident*.
81-
You can use the `qualified` option to use a qualified default name for the translated constants and inductives. The default name then has the form `Module_o_Submodule_o_ident` if *ident* lies in the `Module.Submodule` namespace.
82-
83-
- Parametricity Translation *term* [as *name*] [arity *n*].
84-
85-
Define a new constant named *name* obtained by computing the parametricity translation of *term*.
86-
87-
- Parametricity Module *modulepath*.
74+
## Usage and Commands
8875

89-
Recursively translate everything in a module.
90-
91-
- Realizer *constant or variable* [as *name*] [arity *n*] := *term*.
76+
To load the plugin and make its commands available:
77+
```coq
78+
From Param Require Import Param.
79+
```
9280

93-
Declare *term* to be the translation of a constant.
94-
Useful to translate terms containing section variables, or axioms.
81+
The command scheme for named translations is:
82+
```
83+
Parametricity <ident> as <name> [arity <n>].
84+
```
85+
For example, the following command generates a translation named `my_param`
86+
of the constant or inductive `my_id` with arity 2 (the default):
87+
```coq
88+
Parametricity my_id as my_param.
89+
```
9590

96-
Note that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import `ProofIrrelevence`).
91+
The command scheme for automatically named translations is:
92+
```coq
93+
Parametricity [Recursive] <ident> [arity <n>] [qualified].
94+
```
95+
Such commands generate and name translations based on the given identifier.
96+
The `Recursive` option can be used to recursively translate all the constants
97+
and inductives which are used by the constant or inductive with the given
98+
identifier. The `qualified` option allows you to use a qualified default name
99+
for the translated constants and inductives. The default name then has the form
100+
`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the
101+
`Module.Submodule` namespace.
102+
103+
Instead of using identifiers, you can provide explicit terms to translate,
104+
according to the following command scheme:
105+
```coq
106+
Parametricity Translation <term> [as <name>] [arity <n>].
107+
```
108+
This defines a new constant containing the parametricity translation of
109+
the given term.
97110

98-
- [Global | Local] Parametricity Tactic := t.
111+
To recursively translate everything in a module:
112+
```coq
113+
Parametricity Module <module_path>.
114+
```
99115

100-
Use the tactic t to solve proof obligations generated by the `Parametricity` command.
116+
When translating terms containing section variables or axioms,
117+
it may be useful to declare a term to be the translation of a constant:
118+
```coq
119+
Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>.
120+
```
101121

122+
Note that translating a term or module may lead to proof obligations (for some
123+
fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to
124+
declare a tactic to solve such proof obligations:
125+
```coq
126+
[Global|Local] Parametricity Tactic := <tactic>.
127+
```

‎coq-paramcoq.opam

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,13 @@ license: "MIT"
99

1010
synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
1111
description: """
12-
The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunk of standard library.
13-
"""
12+
A Coq plugin providing commands for generating parametricity statements.
13+
Typical applications of such statements are in data refinement proofs.
14+
Note that the plugin is still in an experimental state - it is not very user
15+
friendly (lack of good error messages) and still contains bugs. But it
16+
is usable enough to "translate" a large chunk of the standard library."""
1417

15-
build: [make "-j%{jobs}%" ]
18+
build: [make "-j%{jobs}%"]
1619
install: [
1720
[make "install"]
1821
[make "-C" "test-suite" "examples"] {with-test}

‎meta.yml

Lines changed: 93 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -1,81 +1,120 @@
1+
---
12
fullname: Paramcoq
23
shortname: paramcoq
34
organization: coq-community
45
community: true
56
action: true
6-
synopsis: Plugin for generating parametricity statements to perform refinement proofs
7-
description: >
8-
The plugin is still in an experimental state. It is not very user
9-
friendly (lack of good error messages) and still contains bugs. But
10-
is useable enough to "translate" a large chunk of standard library.
7+
plugin: true
118
doi: 10.4230/LIPIcs.CSL.2012.399
9+
branch: master
10+
11+
synopsis: Plugin for generating parametricity statements to perform refinement proofs
12+
13+
description: |-
14+
A Coq plugin providing commands for generating parametricity statements.
15+
Typical applications of such statements are in data refinement proofs.
16+
Note that the plugin is still in an experimental state - it is not very user
17+
friendly (lack of good error messages) and still contains bugs. But it
18+
is usable enough to "translate" a large chunk of the standard library.
19+
1220
publications:
13-
- pub_title: Parametricity in an Impredicative Sort
14-
pub_url: https://hal.archives-ouvertes.fr/hal-00730913/
15-
pub_doi: 10.4230/LIPIcs.CSL.2012.399
21+
- pub_title: Parametricity in an Impredicative Sort
22+
pub_url: https://hal.archives-ouvertes.fr/hal-00730913/
23+
pub_doi: 10.4230/LIPIcs.CSL.2012.399
24+
1625
authors:
17-
- name: Chantal Keller
18-
initial: true
19-
- name: Marc Lasson
20-
initial: true
21-
- name: Abhishek Anand
22-
- name: Pierre Roux
23-
- name: Emilio Jesús Gallego Arias
24-
- name: Cyril Cohen
25-
- name: Matthieu Sozeau
26+
- name: Chantal Keller
27+
initial: true
28+
- name: Marc Lasson
29+
initial: true
30+
- name: Abhishek Anand
31+
- name: Pierre Roux
32+
- name: Emilio Jesús Gallego Arias
33+
- name: Cyril Cohen
34+
- name: Matthieu Sozeau
35+
2636
maintainers:
27-
- name: Pierre Roux
28-
nickname: proux01
37+
- name: Pierre Roux
38+
nickname: proux01
39+
2940
license:
30-
fullname: MIT
41+
fullname: MIT License
3142
identifier: MIT
43+
3244
supported_coq_versions:
33-
text: >
45+
text: >-
3446
The master branch tracks the development version of Coq, see
35-
releases for compatibility with released versions of Coq.
47+
releases for compatibility with released versions of Coq
3648
opam: '{= "dev" }'
37-
plugin: true
38-
categories:
39-
- name: 'Miscellaneous/Coq Extensions'
40-
keywords:
41-
- name: paramcoq
42-
- name: parametricity
43-
- name: ocaml module
44-
namespace: Param
45-
opam-file-maintainer: 'Pierre Roux <pierre.roux@onera.fr>'
46-
tested_coq_opam_versions:
47-
- version: 'dev'
48-
documentation: |
49-
Available commands
50-
------------------
51-
52-
The default arity is 2.
5349

54-
- Parametricity *ident* as *name* [arity *n*].
50+
categories:
51+
- name: 'Miscellaneous/Coq Extensions'
5552

56-
Declare the translation named *name* from the translation of the constant or inductive *ident*.
53+
keywords:
54+
- name: paramcoq
55+
- name: parametricity
56+
- name: ocaml module
5757

58-
- Parametricity [Recursive] *ident* [arity *n*] [qualified].
58+
namespace: Param
5959

60-
The default name for the translation of the constant or inductive *ident* is automatically generated (from its unqualified name).
61-
You can use the `Recursive` option to recursively translate all the constants and inductives which are used by *ident*.
62-
You can use the `qualified` option to use a qualified default name for the translated constants and inductives. The default name then has the form `Module_o_Submodule_o_ident` if *ident* lies in the `Module.Submodule` namespace.
60+
opam-file-maintainer: 'Pierre Roux <pierre.roux@onera.fr>'
6361

64-
- Parametricity Translation *term* [as *name*] [arity *n*].
62+
tested_coq_opam_versions:
63+
- version: 'dev'
6564

66-
Define a new constant named *name* obtained by computing the parametricity translation of *term*.
65+
documentation: |-
66+
## Usage and Commands
6767
68-
- Parametricity Module *modulepath*.
68+
To load the plugin and make its commands available:
69+
```coq
70+
From Param Require Import Param.
71+
```
6972
70-
Recursively translate everything in a module.
73+
The command scheme for named translations is:
74+
```
75+
Parametricity <ident> as <name> [arity <n>].
76+
```
77+
For example, the following command generates a translation named `my_param`
78+
of the constant or inductive `my_id` with arity 2 (the default):
79+
```coq
80+
Parametricity my_id as my_param.
81+
```
7182
72-
- Realizer *constant or variable* [as *name*] [arity *n*] := *term*.
83+
The command scheme for automatically named translations is:
84+
```coq
85+
Parametricity [Recursive] <ident> [arity <n>] [qualified].
86+
```
87+
Such commands generate and name translations based on the given identifier.
88+
The `Recursive` option can be used to recursively translate all the constants
89+
and inductives which are used by the constant or inductive with the given
90+
identifier. The `qualified` option allows you to use a qualified default name
91+
for the translated constants and inductives. The default name then has the form
92+
`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the
93+
`Module.Submodule` namespace.
7394
74-
Declare *term* to be the translation of a constant.
75-
Useful to translate terms containing section variables, or axioms.
95+
Instead of using identifiers, you can provide explicit terms to translate,
96+
according to the following command scheme:
97+
```coq
98+
Parametricity Translation <term> [as <name>] [arity <n>].
99+
```
100+
This defines a new constant containing the parametricity translation of
101+
the given term.
76102
77-
Note that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import `ProofIrrelevence`).
103+
To recursively translate everything in a module:
104+
```coq
105+
Parametricity Module <module_path>.
106+
```
78107
79-
- [Global | Local] Parametricity Tactic := t.
108+
When translating terms containing section variables or axioms,
109+
it may be useful to declare a term to be the translation of a constant:
110+
```coq
111+
Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>.
112+
```
80113
81-
Use the tactic t to solve proof obligations generated by the `Parametricity` command.
114+
Note that translating a term or module may lead to proof obligations (for some
115+
fixpoints and opaque terms if you did not import `ProofIrrelevence`). You can
116+
declare a tactic to solve such proof obligations:
117+
```coq
118+
[Global|Local] Parametricity Tactic := <tactic>.
119+
```
120+
---

0 commit comments

Comments
 (0)