From 94be155e6543a64310e5903d1c55335e16303c75 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 4 Jul 2023 11:34:07 +0200
Subject: [PATCH] [doc] Structure for interpretation reference

---
 doc/contributing.rst   |  9 ++++++
 doc/interpretation.rst | 73 ++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 79 insertions(+), 3 deletions(-)

diff --git a/doc/contributing.rst b/doc/contributing.rst
index 9f46da7..2b2ad72 100644
--- a/doc/contributing.rst
+++ b/doc/contributing.rst
@@ -32,6 +32,14 @@ The root of the repository has the following folders:
 Setting up a development environment
 ************************************
 
+With an Opam switch
+-------------------
+
+Need to download `ocaml language server <https://github.com/ocaml/ocaml-lsp>`_, `ocamlformat <https://github.com/ocaml-ppx/ocamlformat>`_ v0.25.1 and
+`ocp-indent <https://github.com/OCamlPro/ocp-indent>`_.
+
+With nix-shell
+--------------
 TODO
 
 .. index:: Prover;prover
@@ -44,4 +52,5 @@ Some possible topics for opening a MR are:
 
 * support for a new prover
 * enhancing the support for an existing prover
+* new proof strategies
 * bug fixes
diff --git a/doc/interpretation.rst b/doc/interpretation.rst
index 8cdfbc4..5958f01 100644
--- a/doc/interpretation.rst
+++ b/doc/interpretation.rst
@@ -6,13 +6,80 @@ The CAISAR modelling language
 Origin: WhyML
 -------------
 
+CAISAR heavily relies on Why3 and uses the WhyML as a basis.
+A reference of WhyML is available on the original `Why3
+manual <https://why3.lri.fr/doc/syntaxref.html>`_.
+
+However, because Why3 aims to verify a whole range of programs, it cannot
+specialize on a particular program structure.
+For further background the paper [F2013]_ from one of Why3's
+original author details the rationale and tradeoff involved
+in WhyML design and implementation. To quote them, "[they] have come up with logic of compromise".
+
+As CAISAR focuses on artificial intelligence systems, it can
+make some additional assumptions on the nature of the
+inputs, program and users, among the following
+
+* users will have a basic background on linear algebra, and
+  expect CAISAR to reflect this
+
+* inputs will mostly be multidimensional vectors (machine
+  learning community coined the term "tensor" as well) of
+  floating point values, strings, ints or chars
+
+* the program control flow will mostly be composed of a lot
+  real or floating-point arithmetic operations: there is no
+  loop with runtime invariant, nor conditional
+
+With those constraints in mind, CAISAR provides several
+extensions to WhyML, that we detail here. They can be used
+directly in any WhyML provided by CAISAR.
+
+Those extensions will be "interpreted".
+Roughly speaking, during the translation from "pure" WhyML
+logic to actual inputs to provers, some symbols will be
+replaced with other values.
+
 Built-ins
 ---------
 
+.. index:: Interpretation; interpretation
+
 Available under ``stdlib/interpretation.mlw``.
 
 Several theories available to use in any property file.
 
-* Vector
-* NeuralNetwork
-* Dataset
+TODO: a custom css class with function name, type and
+description?
+
+
+Vector
+******
+
+Functions
+~~~~~~~~~
+
+Predicates
+~~~~~~~~~~
+
+NeuralNetwork
+*************
+
+Functions
+~~~~~~~~~
+
+Predicates
+~~~~~~~~~~
+
+Dataset
+*******
+
+Functions
+~~~~~~~~~
+
+Predicates
+~~~~~~~~~~
+
+.. [F2013] Jean-Christophe Filiâtre, *One Logic to Use Them All*,
+   CADE 24 - the 24th International Conference on
+   Automated Deduction
-- 
GitLab