Skip to content

Commit 1f9b650

Browse files
dunnldunnl
committed
Squash artifact for JAR2024
1 parent f109980 commit 1f9b650

File tree

640 files changed

+292787
-69242
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

640 files changed

+292787
-69242
lines changed

‎.envrc

-1
This file was deleted.

‎.gitignore

+4-6
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,17 @@
11
.direnv/
2-
.#*
32
*.tmp
43
*.glob
54
*.vo*
65
*.aux
76
*.lia.cache
7+
Makefile.coq.local
88
Makefile.coq
99
Makefile.coq.conf
1010
.Makefile.coq.d
11-
html
11+
/html
12+
/html-alectryon
1213
# Emacs lock files
1314
.#*
1415
# Nix files
1516
result
16-
# Everything in the ~ignore/~ directory
17-
ignore/
18-
# Ignore result of building examples with alectryon
19-
html-examples/
17+
result-alectryon

‎Makefile

+55-31
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,61 @@
1-
COQDOC_EXTRA_DIR:=extra/CoqdocJS
2-
COQDOCFLAGS:= \
3-
--external 'http://ssr2.msr-inria.inria.fr/doc/ssreflect-1.5/' Ssreflect \
4-
--external 'http://ssr2.msr-inria.inria.fr/doc/mathcomp-1.5/' MathComp \
5-
--toc --toc-depth 2 --html --interpolate \
6-
--index indexpage --no-lib-name --parse-comments \
7-
--with-header $(COQDOC_EXTRA_DIR)/header.html --with-footer $(COQDOC_EXTRA_DIR)/footer.html
8-
export COQDOCFLAGS
9-
COQMAKEFILE:=Makefile.coq
10-
COQ_PROJ:=_CoqProject
11-
VS:=$(wildcard *.v)
12-
13-
all: html
14-
15-
clean: $(COQMAKEFILE)
16-
rm -fr html
17-
@$(MAKE) -f $(COQMAKEFILE) $@
18-
rm -f $(COQMAKEFILE)
1+
SHELL = bash
2+
COQ_MAKEFILE := Makefile.coq
3+
COQ_PROJ := _CoqProject
4+
COQ_VS := $(shell find Tealeaves/ -name "*.v")
5+
RM_ARTIFACTS := extra/remove_artifacts.sh
6+
export COQ_MAKEFILE
7+
8+
all: htmlpretty
9+
10+
# Generate Makefile.coq from _CoqProject and .v files
11+
# $(COQ_VS) forces regeneration whenever a .v has a more recent timestamp
12+
# $(COQ_PROJ) forces regeneration whenever a _CoqProject has a more recent timestamp
13+
$(COQ_MAKEFILE): $(COQ_PROJ) $(COQ_VS)
14+
@echo "Generating Makefile.coq" #with $(COQ_VS)"
15+
coq_makefile -f $(COQ_PROJ) -o $@
1916

20-
html: $(COQMAKEFILE) $(VS)
21-
rm -fr html
22-
@$(MAKE) -f $(COQMAKEFILE) $@
23-
cp $(COQDOC_EXTRA_DIR)/resources/* html
17+
$(COQ_VS):
18+
@echo "This statement shouldn't be reached, but was reached via $@"
2419

25-
#alectryon: $(COQMAKEFILE) $(COQMF_VFILES)
26-
# rm -fr html-alectryon
27-
# alectryon --output-directory html-alectryon $(COQMF_VFILES)
20+
# html: Generate Coqdocs
21+
# gallinahtml: Generate Coqdocs without proofs
22+
# html-pretty: Generate Coqdocs with CoqdocJS
23+
# alectryon: Generate HTML with Alectryon
24+
html gallinahtml htmlpretty alectryon: $(COQ_MAKEFILE)
25+
$(MAKE) -f $(COQ_MAKEFILE) $@
2826

29-
$(COQMAKEFILE): $(COQ_PROJ) $(VS)
30-
coq_makefile -f $(COQ_PROJ) -o $@
27+
# Any target not matched above will be passed to Makefile.coq
28+
%: $(COQ_MAKEFILE) force
29+
@echo "'%' pattern target running for target \"$@\""
30+
$(MAKE) -f $(COQ_MAKEFILE) $@
31+
32+
# Supress Makefile's auto-rebuilding target
33+
# # https://stackoverflow.com/questions/67251937/makefile-match-anything-rule-picks-up-makefile-target
34+
Makefile: ;
35+
36+
# Placeholder if we wanted to generate _CoqProject
37+
$(COQ_PROJ): ;
38+
39+
install-examples:
40+
cp html-examples/* ${out} -r
41+
42+
# The last command requires GNU find and deletes empty directories
43+
# under Tealeaves/
44+
clean: $(COQ_MAKEFILE)
45+
$(MAKE) -f $(COQ_MAKEFILE) $@
46+
rm -f $(COQ_MAKEFILE)
47+
$(RM_ARTIFACTS)
48+
find Tealeaves/ . -type d -empty -delete
49+
50+
clean-html:
51+
rm -fr html
3152

32-
%: $(COQMAKEFILE) force
33-
@$(MAKE) -f $(COQMAKEFILE) $@
53+
clean-all: clean clean-html
3454

35-
force $(COQ_PROJ) $(VS): ;
55+
# Warning: this interactively destroys all files not under version
56+
# control
57+
clean-repo: clean
58+
git clean -xdi -e Makefile.coq.conf -e Makefile.coq.local -e ".*"
3659

37-
.PHONY: clean all force
60+
force: ;
61+
.PHONY: clean all force clean-repo examples-html install-examples

‎Makefile.coq.local

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
include extra/Makefile.alectryon
2+
include extra/Makefile.htmlpretty

‎Makefile.examples

-13
This file was deleted.

‎README.md

+7-39
Original file line numberDiff line numberDiff line change
@@ -7,49 +7,17 @@ Tealeaves is a Coq framework for proving theorems about syntax abstractly, i.e.
77
## How to build Tealeaves
88
System requirements:
99
- `make` (see [GNU Make](https://www.gnu.org/software/make/))
10-
- An installation of Coq >= 8.13 (see the Coq [downloads page](https://coq.inria.fr/download)).
10+
- [Autosubst](https://github.com/coq-community/autosubst/tree/master)
11+
- An installation of [Coq](https://coq.inria.fr/download). This branch has been tested with Coq 8.16.
1112

1213
Compilation instructions:
1314
- Run `make` in the top-level directory
1415
- Run `make clean` to remove all build artifacts (including compiled files) and start over
16+
- By default `make` generates Coqdocs under `html`
17+
- Run `make alectryon` (if Alectryon is installed) to generate documents under `html-alectryon/`
1518

16-
We have tested with Coq 8.13, but other versions may work too. We observe a compilation time of approximately 4-5 minutes on a typical desktop computer. On multicore systems you may want to use the `-j` flag to use several build threads. We have sometimes observed that `-j` leads to cryptic build errors. The solution to these is simply to re-run the build command again.
19+
## Documentation
1720

18-
Tealeaves is built with the [coq_makefile](https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile), which is distributed with Coq itself. This utility generates a customized Makefile to build a Coq project. For simplicity, we provide a top-level `Makefile` which will call `coq_makefile` for you, and then recursively call `make` on the generated Makefile, so that you should not have to do anything except call `make` once in the top-level directory.
21+
Coqdocs are found under [/docs/html/toc.html](/docs/html/toc.html)
1922

20-
## Generating the documentation
21-
22-
Pretty-printed HTML documentation is generated by default in the `html/` directory.
23-
24-
## Module organization
25-
26-
### Typeclasses
27-
Classes of "structured" functors (like monads, decorated monads, traversable functors, etc.) are found in under `Tealeaves/Classes`. The internal implementation of Tealeaves uses an *algebraic* rather than *Kleisli-style* implementation of our typeclasses, so that operations like `bind` are derived rather than taken as primitive. For example, decorated monads are defined [here](https://github.com/dunnl/tealeaves/blob/master/Tealeaves/Classes/DecoratedMonad.v) as monads equipped with a "decoration" operation. Their equivalent Kleisli presentation is derived [here](https://github.com/dunnl/tealeaves/blob/master/Tealeaves/Classes/DecoratedMonad.v#L200) in the same file. A characterization of decorated functors as comodules of the reader/writer bimonad is found [here](https://github.com/dunnl/tealeaves/blob/master/Tealeaves/Theory/Decorated.v).
28-
29-
### The locally nameless backend
30-
Our locally nameless backend library is formalized under the `LN/` directory. The operations (opening, closing, local closure, etc) are defined [here](https://github.com/dunnl/tealeaves/blob/master/LN/Operations.v). Various lemmas about these operations, proved polymorphically over a decorated traversable monad `T`, are proved [here](https://github.com/dunnl/tealeaves/blob/master/LN/Theory.v).
31-
32-
### Simply typed lambda calculus
33-
Our formalization of STLC is under the `STLC/` directory. A formalization of STLC's syntax as a DTM is found [here](https://github.com/dunnl/tealeaves/blob/master/STLC/Language.v). Basic metatheory such as a progress theorem are proved [here](https://github.com/dunnl/tealeaves/blob/master/STLC/Theory.v).
34-
35-
### Multisorted
36-
Our multisorted classes live under `Multisorted/`. Our extension of the locally nameless backend lives under `LN/Multisorted/.` SystemF lives under `SystemF`.
37-
38-
## Typeclasses hierarchy
39-
![Tealeaves typeclass hierarchy](/images/cube.svg)
40-
41-
| **Tealeaves Typeclasses** | Functor | Monad |
42-
|---------------------------|-------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------|
43-
| Plain | [Classes/Functor.v](/Tealeaves/Classes/Functor.v) | [Algebraic](/Tealeaves/Classes/Algebraic/Monad.v) / [Kleisli](/Tealeaves/Classes/Kleisli/Monad.v) |
44-
| Decorated | [Algebraic](/Tealeaves/Classes/Algebraic/Decorated/Functor.v) / [Kleisli](/Tealeaves/Classes/Kleisli/Decorated/Functor.v) | [Algebraic](/Tealeaves/Classes/Algebraic/Decorated/Monad.v) / [Kleisli](/Tealeaves/Classes/Kleisli/Decorated/Monad.v) |
45-
| Traversable | [Algebraic](/Tealeaves/Classes/Algebraic/Traversable/Functor.v) / [Kleisli](/Tealeaves/Classes/Kleisli/Traversable/Functor.v) | [Algebraic](/Tealeaves/Classes/Algebraic/Traversable/Monad.v) / [Kleisli](/Tealeaves/Classes/Kleisli/Traversable/Monad.v) |
46-
| Decorated+Traversable | [Algebraic](/Tealeaves/Classes/Algebraic/DT/Functor.v) / [Kleisli](/Tealeaves/Classes/Kleisli/DT/Functor.v) | [Algebraic](/Tealeaves/Classes/Algebraic/DT/Monad.v) / [Kleisli](/Tealeaves/Classes/Kleisli/DT/Monad.v) |
47-
48-
## Other notes
49-
50-
### Axioms used in Tealeaves
51-
Tealeaves currently uses two axioms commonly used in Coq formalizations, which have been proven (on paper) to be equi-consistent with Coq itself. They are the following.
52-
- [Propositional extensionality](https://coq.github.io/doc/v8.12/stdlib/Coq.Logic.PropExtensionality.html#propositional_extensionality), which says that equivalent propositions (`P <-> Q`) are propositionally equal (`P = Q`)
53-
- [Functional extensionality](https://coq.inria.fr/library/Coq.Logic.FunctionalExtensionality.html#functional_extensionality), which is the statement `forall x, f x = g x -> f = g`.
54-
55-
There axioms are assumed [here](https://github.com/dunnl/tealeaves/blob/1e69a99b9376506c5c28c243112e74c9282535aa/Tealeaves/Util/Prelude.v#L6). They are a convenience to use Coq's rewriting features. In principle one can eliminate these at the cost of ``setoid hell'' (see [this question](https://stackoverflow.com/questions/65493694/why-do-calculus-of-construction-based-languages-use-setoids-so-much) on StackOverflow).
23+
Alectryon files are found under [/docs/html-alectryon/](/docs/html-alectryon/)

‎Tealeaves/Adapters/CategoricalToKleisli/DecoratedFunctor.v

+98
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
From Tealeaves Require Import
2+
Classes.Categorical.DecoratedFunctor
3+
Classes.Kleisli.DecoratedFunctor.
4+
5+
#[local] Generalizable Variables E F.
6+
7+
#[local] Arguments map F%function_scope {Map} {A B}%type_scope f%function_scope _.
8+
#[local] Arguments dec {E}%type_scope F%function_scope {Decorate} {A}%type_scope _.
9+
#[local] Arguments extract W%function_scope {Extract} {A}%type_scope _.
10+
11+
Import Product.Notations.
12+
13+
(** * Algebraic decorated functor to Kleisli decorated functor *)
14+
(******************************************************************************)
15+
16+
(** ** Kleisli laws for <<fmapd>> *)
17+
(******************************************************************************)
18+
Module ToKleisli.
19+
20+
Section operation.
21+
22+
Context
23+
(E : Type)
24+
(F : Type -> Type)
25+
`{Map F} `{Decorate E F}.
26+
27+
#[export] Instance Mapd_dec : Mapd E F :=
28+
fun A B (f : E * A -> B) => map F f ∘ dec F.
29+
30+
End operation.
31+
32+
Import Comonad.Notations.
33+
Import Comonad.ToKleisli.
34+
35+
Section with_functor.
36+
37+
Context
38+
(F : Type -> Type)
39+
`{Classes.Categorical.DecoratedFunctor.DecoratedFunctor E F}.
40+
41+
Theorem mapd_id {A} : @mapd E F _ A A (extract (E ×)) = @id (F A).
42+
Proof.
43+
introv. unfold_ops @Mapd_dec.
44+
apply (dfun_dec_extract).
45+
Qed.
46+
47+
Theorem mapd_mapd (A B C : Type) (g : E * B -> C) (f : E * A -> B) :
48+
@mapd E F _ B C g ∘ @mapd E F _ A B f = @mapd E F _ A C (kc4 g f).
49+
Proof.
50+
unfold_ops @Mapd_dec.
51+
reassociate <- on left.
52+
reassociate -> near (map F f).
53+
rewrite <- (natural (G := F ○ prod E)).
54+
reassociate <- on left.
55+
unfold transparent tcs.
56+
rewrite (fun_map_map (F := F)).
57+
reassociate -> on left.
58+
rewrite (dfun_dec_dec).
59+
reassociate <- on left.
60+
rewrite (fun_map_map (F := F)).
61+
repeat fequal.
62+
ext [e a].
63+
reflexivity.
64+
Qed.
65+
66+
#[export] Instance DecoratedFunctor: Kleisli.DecoratedFunctor.DecoratedFunctor E F :=
67+
{| dfun_mapd1 := @mapd_id;
68+
dfun_mapd2 := @mapd_mapd
69+
|}.
70+
71+
End with_functor.
72+
73+
End ToKleisli.
74+
75+
(** * Miscellaneous properties of decorated functors *)
76+
(******************************************************************************)
77+
Section DecoratedFunctor_misc.
78+
79+
Context
80+
(T : Type -> Type)
81+
`{Categorical.DecoratedFunctor.DecoratedFunctor E T}.
82+
83+
Theorem cobind_dec {A B} : forall (f : E * A -> B),
84+
map T (cobind (W := (E ×)) f) ∘ dec T = dec T ∘ map T f ∘ dec T.
85+
Proof.
86+
intros.
87+
unfold_ops @Cobind_reader.
88+
rewrite <- (natural (ϕ := @dec E T _)).
89+
unfold_ops @Map_compose.
90+
reassociate ->.
91+
rewrite (dfun_dec_dec (E := E) (F := T)).
92+
reassociate <-.
93+
rewrite (fun_map_map (F := T)).
94+
fequal. fequal.
95+
now ext [e a].
96+
Qed.
97+
98+
End DecoratedFunctor_misc.

0 commit comments

Comments
 (0)