Write up new normalization details

While here, permute the directory structure of docs/sphinx slightly.

diff --git a/docs/sphinx/conf.py b/docs/sphinx/conf.py
index 468ffa4079b57c31c4b02ae9d331784712c17769..851e3993c8375a79b93af2db6db7cd32126ccb9a 100644 (file)
--- a/docs/sphinx/conf.py
+++ b/docs/sphinx/conf.py
@@ -260,8 +260,6 @@ texinfo_documents = [
 
 # rst_prolog = ""
 
-extlinks = {'dynasrc': ('https://www.github.com/nwf/dyna/blob/master/%s',
-                        'file ' )
-           ,'githubbug': ("https://github.com/nwf/dyna/issues/%s",
-                        'issue ')
+extlinks = {'dynasrc': ('https://www.github.com/nwf/dyna/blob/master/%s', '')
+           ,'githubbug': ("https://github.com/nwf/dyna/issues/%s", 'issue ')
            }

diff --git a/docs/sphinx/index.rst b/docs/sphinx/index.rst
index 3349c8b463546721bc743d48557dd4d27d572420..81bbe05e061bf4aa325b953e191e1c04941b1744 100644 (file)
--- a/docs/sphinx/index.rst
+++ b/docs/sphinx/index.rst
@@ -21,6 +21,8 @@ Contents:
 
    tutorial/index
 
+   manual/index
+
    spec/index
 
    Bibliography <bib>

diff --git a/docs/sphinx/manual/index.rst b/docs/sphinx/manual/index.rst
new file mode 100644 (file)
index 0000000..4f3dfa5
--- /dev/null
+++ b/docs/sphinx/manual/index.rst
@@ -0,0 +1,9 @@
+.. Manual index
+   This file is enumerated in the toctree directive of index.rst
+
+User Manual
+###########
+
+.. toctree::
+
+   pragmas

diff --git a/docs/sphinx/spec/pragmas.rst b/docs/sphinx/manual/pragmas.rst
similarity index 98%
rename from docs/sphinx/spec/pragmas.rst
rename to docs/sphinx/manual/pragmas.rst
index fadbb1b85b7d4c32d801b5b76211f063178c8592..e7d3095ae0ddefd56c027822d9ab5685a90f04cc 100644 (file)
--- a/docs/sphinx/spec/pragmas.rst
+++ b/docs/sphinx/manual/pragmas.rst
@@ -156,7 +156,7 @@ expect and follows the usual rules of arithmetic.
 
 .. admonition:: bug
 
-   For the moment, the source is the spec.  See the source
+   For the moment, the source is the spec.  See the source in
    :dynasrc:`src/Dyna/Term/SurfaceSyntax.hs` for full details.
 
 #########

diff --git a/docs/sphinx/spec/index.rst b/docs/sphinx/spec/index.rst
index 1016b73ffa42071bf0b5cf5cd8025511872dfd79..dbe48a7906bbd0f1b7cf5e084532c57b8eb12d8a 100644 (file)
--- a/docs/sphinx/spec/index.rst
+++ b/docs/sphinx/spec/index.rst
@@ -6,5 +6,5 @@ Specifications
 
 .. toctree::
 
-   pragmas
+   syntax
    glossary

diff --git a/docs/sphinx/spec/syntax.rst b/docs/sphinx/spec/syntax.rst
new file mode 100644 (file)
index 0000000..8541cab
--- /dev/null
+++ b/docs/sphinx/spec/syntax.rst
@@ -0,0 +1,86 @@
+.. Syntax
+
+******
+Syntax
+******
+
+This chapter defines Dyna's concrete syntax.
+
+.. index::
+   single: quotation and evaluation
+   single: syntax; quotation and evaluation
+
+.. _syntax-quote-eval:
+
+#############
+Quote vs Eval
+#############
+
+.. sidebar:: Relevant source files:
+   
+   * :dynasrc:`src/Dyna/Analysis/ANF.hs`
+   * :dynasrc:`src/Dyna/Term/SurfaceSyntax.hs`
+
+Dyna's syntax has both *nested terms* (also called *recursive terms*) and
+*in-place evaluation*.  (Recall the discussion in
+:ref:`pragma_disposition`.)  Managing the details in a way that is (ideally)
+not too surprising to users requires some technical complexity.
+
+Since this all takes place at parse time, the most upon which we can really
+expect to key our decisions is the term's functor and arity.  Each
+(functor,arity) pair may specify
+
+* A :term:`self disposition`, which may be one of ``evaluate``, ``quote``,
+  or ``inherit``.  No functors in Dyna (by default) use ``evaluate``; it is
+  offered to facilitate the development of more Prolog-like syntaxes.
+
+* For each argument, a :term:`argument disposition` which may be either
+  ``evaluate`` or ``quote``.
+
+Additionally, there are two explicit operators defined in the language:
+
+.. index::
+   single: operators; quote.
+   single: operators; evaluate.
+
+* A quotation operator, prefix unary ``&``.
+
+* An evaluation operator, prefix unary ``*``.
+
+When attempting to understand a term in a Dyna program, one must keep track
+of:
+
+* The argument disposition of the location where it occurs.  Functors
+  specify this as per above; an aggregator will always place its head in a
+  quoted context and its body in an evaluation context.
+
+* The number of ``*`` operators seen between the functor's argument position
+  and the functor of the inner term.
+
+* Whether or not the sequence of quotation and evaluation operators ends
+  with a quotation operator.  Note that only the right end matters; that is,
+  ``*&*&`` has the same effect as ``**&``.
+
+* The self disposition of the inner functor.
+
+The interpretation is then the first matching row in this table:
+
+======== ============== ======= ========= ==================================
+Context  Eval Operators Quoted? Self             Effect
+======== ============== ======= ========= ==================================
+Any      0              Yes     Any       Quotation (explicit at site)
+Any      0              No      Quote     Quotation (implicit from self)
+Any      0              No      Evaluate  Evaluation (implicit from self)
+Quote    0              No      Inherit   Quotation (implicit from context)
+Evaluate 0              No      Inherit   Evaluation (implicit from context)
+Any      :math:`n > 0`  Yes     Any       :math:`n`-chained evaluation
+Any      :math:`n > 0`  No      Evaluate  :math:`(n+1)`-chained evaluation
+Any      :math:`n > 0`  No      Any       :math:`n`-chained evaluation
+======== ============== ======= ========= ==================================
+
+Where, by ":math:`n`-chained evaluation", we mean one evaluation of the term
+at hand, and then :math:`n-1`
+:term:`indirect evaluations <indirect evaluation>` where the :term:`value`
+is fed through the :term:`chart` to obtain the next value.  The last of
+these is taken to be the value of the chain as a whole.  See
+:ref:`spec-indirect-evaluation` for more details.