From 81146486d887d4156f73fe336d6c189ef4304f7b Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabriel@motacilla.home>
Date: Sat, 23 Oct 2021 10:07:30 +0200
Subject: [PATCH] documentation

---
 docs/Makefile      |  2 +-
 docs/main.adoc     | 41 +++++++++++++++++++++++++++++++++++++----
 encoding/README.md |  5 -----
 3 files changed, 38 insertions(+), 10 deletions(-)
 delete mode 100644 encoding/README.md

diff --git a/docs/Makefile b/docs/Makefile
index 31c7025..01bc88f 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -3,7 +3,7 @@ all: main.html
 .SUFFIXES: .adoc .html
 
 .adoc.html:
-	asciidoc $<
+	asciidoc -a mathjax $<
 
 .PHONY: clobber
 clobber:
diff --git a/docs/main.adoc b/docs/main.adoc
index ccbe314..6a321dd 100644
--- a/docs/main.adoc
+++ b/docs/main.adoc
@@ -1,4 +1,4 @@
-// vim: set syntax=asciidoc textwidth=70:
+// vim: set syntax=asciidoc textwidth=70 expandtab ts=2 sw=2:
 = Translating PVS to Dedukti with Personoj =
 Gabriel Hondet <gabriel.hondet@inria.fr>
 v1.0, October 2021
@@ -43,7 +43,7 @@ checking terms becomes decidable.
 PVS-Cert has been encoded in
 link:https://github.com/Deducteam/lambdpi[lambdapi], an extension of
 Dedukti with meta-variables. This encoding is described
-link:https://arxiv.org/abs/2010.16115[there].
+link:https://hal.inria.fr/hal-03279766[there].
 The encoding of PVS-Core is work in progress. In particular, encoding
 implicit predicate subtyping requires some procedure to make it
 explicit. Personoj provides the encodings that can be used by lambdapi
@@ -52,8 +52,10 @@ type check them.
 
 == How to translate and X-check PVS files? ==
 
-This section can be seen as a tutorial. It explains step by step how
-to translate theories from PVS to lambdapi files.
+We call translation of a PVS file the process of creating a file in
+the syntax of lambdapi (suffixed by +.lp+) from a PVS specification
+(suffixed by +.pvs+). Cross-checking a PVS file consists in type
+checking its translation.
 
 IMPORTANT: this document is focused on the translation of the standard
 library of PVS called _Prelude_. Its management is a bit particular
@@ -176,3 +178,34 @@ translated yet.
 
 TIP: if the translation fails, ensure that +$PVSPATH+ and
 +$PERSONOJPATH+ are correctly set up.
+
+== Implementation details ==
+
+=== Encoding ===
+
+The encoding is a set of lambdapi files in +encoding/+ that define
+axioms allowing to type check PVS terms and propositions.
+
++lhol.lp+ ::
+  Simple Type theory expressed as a PTS commonly named λHOL
++pvs_cert.lp+ ::
+  Explicit predicate subtyping
++tuple.lp+ ::
+  Non dependents tuples. Can also be seen as a non dependent version
+  of link:https://doi.org/10.1016/0890-5401(91)90066-B[de Bruijn
+  telescopes].
++logical.lp+ ::
+  Locical connectives
++eqtup.lp+ ::
+  Uncurried equality and disequality, latexmath:[$eq (t, u)$]
++coercions.lp+ ::
+  Define coercions to implement implicit predicate subtyping
++extra+ ::
+  More definitions and tools
+  +arity-tools.lp+ :::
+    An encoding of natural numbers used in data structures (they are
+    not the natural numbers used in PVS)
++alt+ ::
+  Alternate definitions
++examples+ ::
+  Some example specification
diff --git a/encoding/README.md b/encoding/README.md
deleted file mode 100644
index b34e343..0000000
--- a/encoding/README.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# Personoj encoding
-
-- `extra/`: files that are not needed for PVS but may be useful to develop in
-  PVS' theory
-- `examples/`: examples of PVS developments in lambadpi
-- 
GitLab