From 24a79f904a3414cd9dd54f5ee9122e3828938ede Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 4 Mar 2015 12:52:23 +0100
Subject: [PATCH] Add xlang section with some basic structure
---
doc/index.rst | 2 +-
doc/xlang.rst | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 56 insertions(+), 1 deletion(-)
create mode 100644 doc/xlang.rst
diff --git a/doc/index.rst b/doc/index.rst
index 9ffe65702..bb9f64509 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -15,6 +15,7 @@ Contents:
installation
gettingstarted
purescala
+ xlang
verification
synthesis
repair
@@ -27,4 +28,3 @@ Indices and tables
* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`
-
diff --git a/doc/xlang.rst b/doc/xlang.rst
new file mode 100644
index 000000000..760afbb22
--- /dev/null
+++ b/doc/xlang.rst
@@ -0,0 +1,55 @@
+.. _xlang:
+
+XLang
+=====
+
+To complement the core PureScala language, the XLang module of Leon brings a
+few extensions to that core language.
+
+These extensions are kept as an optional feature, that needs to be explicitly
+enabled from the command line with the option ``--xlang``. If you do not specify
+the option, Leon will reject any program making use of an XLang feature.
+
+Technically, these extensions are implemented using a translation to PureScala.
+This means They are not implemented in the back-end solving system of Leon, but
+parsed in the the front-end and eliminate early during the Leon pipelining
+process.
+
+Imperative Code
+---------------
+
+XLang lets you introduce local variables in functions, and use Scala assignments
+syntax.
+
+.. code-block:: scala
+
+ def foo(x: Int): Int = {
+ var a = x
+ var b = 42
+ a = a + b
+ b = a
+ b
+ }
+
+The above example illustrates three new features introduced by XLang:
+
+1. Declaring a variable in a local scope
+
+2. Blocks of statement
+
+3. Assignment
+
+
+While loops
+
+Arrays
+
+Nested function closure on local variables.
+
+.. note::
+ some note comes here
+
+Epsilon
+-------
+
+
--
GitLab