From 1b5b148b2f9d312634b159025f787b4d7a3f59af Mon Sep 17 00:00:00 2001 From: Mysaa Date: Mon, 28 Aug 2023 17:43:21 +0200 Subject: [PATCH] Added appendix code generation --- Makefile | 15 ++++++++++++--- ZOL2.lagda | 2 +- report/CodeIndex.html | 21 +++++++++++++++++++++ report/M1Report.tex | 7 ++++--- report/header.tex | 1 + 5 files changed, 39 insertions(+), 7 deletions(-) create mode 100644 report/CodeIndex.html diff --git a/Makefile b/Makefile index 43ea719..a211748 100644 --- a/Makefile +++ b/Makefile @@ -11,9 +11,13 @@ all: report/build/M1Report.pdf latex/%.tex: %.lagda agda --latex --allow-unsolved-metas $< cp latex/agda.sty report/agda.sty +html/%.html: %.lagda + agda --html --allow-unsolved-metas $< +html/%.html: %.agda + agda --html --allow-unsolved-metas $< -report/build/M1Report.pdf: agda-tex-FFOL agda-tex-FIni agda-tex-ZOL - $(cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report") +report/build/M1Report.pdf: agda-tex agda-html report/M1Report.tex report/header.tex report/Bilibibio.bib + cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report" agda-tex: latex/ZOL2.tex latex/ZOLInitial.tex latex/ZOLCompleteness.tex latex/IFOL2.tex latex/IFOLInitial.tex latex/IFOLInitial.tex latex/FFOL.tex latex/FFOLInitial.tex mkdir -p report/agda @@ -26,6 +30,11 @@ agda-tex: latex/ZOL2.tex latex/ZOLInitial.tex latex/ZOLCompleteness.tex latex/IF $(call split,"latex/FFOL.tex","report/agda/FFOL-",".tex") $(call split,"latex/FFOLInitial.tex","report/agda/FFOL-I-",".tex") +agda-html: report/CodeIndex.html html/PropUtil.html html/ListUtil.html html/ZOL2.html html/ZOLInitial.html html/ZOLCompleteness.html html/IFOL2.html html/IFOLInitial.html html/IFOLCompleteness.html html/FFOL.html html/FFOLInitial.html + mkdir -p html/ + cp report/CodeIndex.html html/ + cd html; ebook-convert CodeIndex.html Code.pdf --base-font-size=8 --margin-bottom=3 --margin-top=3 --paper-size=a4 --language=en --authors="Samy Avrillon" --toc-filter=".*" + .PHONY: clean agda-tex agda-tex-FFOL agda-tex-ZOL agda-tex-FIni clean: - rm -fr *.agdai report/agda latex report/build + rm -fr *.agdai report/agda latex report/build html html2 diff --git a/ZOL2.lagda b/ZOL2.lagda index 1ac55d1..ac565c0 100644 --- a/ZOL2.lagda +++ b/ZOL2.lagda @@ -1,4 +1,4 @@ -\begin{code}[hide] +\begin{code} {-# OPTIONS --prop --rewriting #-} open import PropUtil diff --git a/report/CodeIndex.html b/report/CodeIndex.html new file mode 100644 index 0000000..5dc74d5 --- /dev/null +++ b/report/CodeIndex.html @@ -0,0 +1,21 @@ + + + + + ZOL2 + + + +
    +
  1. PropUtil
    2. +
  2. ListUtil
    3. +
  3. ZOL
    4. +
  4. ZOLInitial
    5. +
  5. ZOLCompleteness
    6. +
  6. IFOL
    7. +
  7. IFOLInitial
    8. +
  8. IFOLCompleteness
    9. +
  9. FFOL
    10. +
  10. FFOLInitial
    11. +
+ diff --git a/report/M1Report.tex b/report/M1Report.tex index a3908a2..503073a 100644 --- a/report/M1Report.tex +++ b/report/M1Report.tex @@ -122,7 +122,7 @@ What will be the use of these morphisms? One thing we want to do is to find the \emph{initial} model, or \emph{syntax} for this class of models. It means that we want to find a model from which, for any model $M$, there exists one and only one morphism from this model to $M$. We can also call the syntax the \emph{minimal model}, as it is the model that contains just the objects something needs to be a model of Propositional Logic. - Mathematically, this model is really easy to find. We only have to take all the sorts defined in the GAT and apply a quotient by every equation of the GAT. But this is not very interesting, as the defined model would not be \emph{strict}, i.e. all equations will not be definitional. Having only strict definitions for objects allows us to study completeness while removing a lot of transport issues that make the transport hell far bigger in the completeness proof. Transport Hell will be explained in \autoref{sec:transport-hell}. + Mathematically, this model is really easy to find. We only have to take all the sorts defined in the GAT and apply a quotient by every equation of the GAT. But this is not very interesting, as the defined model would not be \emph{strict}, i.e. all equations will not be definitional. Having only strict definitions for objects allows us to study completeness while removing a lot of transport issues that make the transport hell far bigger in the completeness proof. Transport hell will be explained in \autoref{sec:transport-hell}. So we have three things to do : \begin{enumerate} @@ -170,9 +170,9 @@ And we now have a working model for Propositional Logic. We can implement our previously defined record and all the equations can be directly understood by Agda (\AgdaInductiveConstructor{refl} is enough proof). - I won't dive into the construction of the initial morphism and the proof that it is unique, because it is a bit ugly because of some \emph{transport hell} (see \autoref{sec:transport-hell} for an explanation of the issue). + I won't dive into the construction of the initial morphism and the proof that it is unique, since it is a bit ugly because of some \emph{transport hell} (see \autoref{sec:transport-hell} for an explanation of the issue). - Still, below is the construction of the \AgdaField{Con} and \AgdaField{For} mappings, as they show the basic idea of the construction. The idea is simple, we pattern-match against the datatype definition of our Sort in our syntax, and for each constructor, we call the corresponding one in the algebra. + Still, below is the construction of the \AgdaField{Con} and \AgdaField{For} mappings, as they show the basic idea of the construction. The idea is simple, we pattern-match against the datatype definition of our sort in our syntax, and for each constructor, we call the corresponding one in the algebra. And the uniqueness proof is pretty simple again because you only need to prove that the \AgdaDatatype{Con} and \AgdaDatatype{For} mappings are unique, because the other ones are in \AgdaPrimitive{Prop}, so they are automatically unique. And to prove the unicity, you split again on the sort's datatype, and for each constructor, you use the fact that a morphism preserves constructors, and you have a nice proof by recursion (except it's ugly because of transport hell). @@ -595,5 +595,6 @@ \appendixpage \section{Agda Code} + The Agda code has been written to A4 paper and is given in the next pages \end{document} diff --git a/report/header.tex b/report/header.tex index 7915f63..87e5bfe 100644 --- a/report/header.tex +++ b/report/header.tex @@ -34,6 +34,7 @@ \usepackage{minitoc} \usepackage{mathtools} \usepackage{textgreek} +\usepackage{pdfpages} \usepackage[textheight=0.75\paperheight]{geometry}