dist/
examples/*.d
-examples/*.out
+examples/*.hist
examples/*.plan
+examples/*.plan.py
+examples/*.out
+
+docs/sphinx/_build
# -*- indent-tabs-mode:t; -*-
-all: deps build
+all: deps build sphinxbuild
upstream:
git submodule init
# cabal install --user external/ekmett-parsers external/ekmett-trifecta
deps:
- alex --version || cabal install alex
- happy --version || cabal install happy
+ alex --version >/dev/null || cabal install alex
+ happy --version >/dev/null || cabal install happy
cabal install --user --enable-tests --only-dependencies .
build:
# perfect, but it does OK.
HADDOCK_HTML ?= "../\\$$pkgid/html"
+.PHONY: haddock
haddock:
mkdir -p dist/alldoc
haddock --html -o dist/alldoc \
`runghc -imisc HaddockPaths "$(HADDOCK_HTML)"` \
`grep -ie '^\( \|\t\)*main-is:' dyna.cabal | sed -e "s/^.*Is: */src\//"`
+# Build our sphinx documentation
+.PHONY: sphinxbuild sphinxdoc
+sphinxbuild:
+ (cd docs/sphinx; make html)
+
+sphinxdoc: sphinxbuild
+ python -c 'import webbrowser; \
+ webbrowser.open("./docs/sphinx/_build/html/index.html")'
+
+doc: sphinxbuild haddock
+
# If the cabal file doesn't do the right thing, this tries to work through
# it all by hand. Blech! But it's better than nothing.
+.PHONY: ghcbuild
ghcbuild:
mkdir -p dist/build/dyna/
mkdir -p dist/build/dyna/dyna-tmp
# Every now and again we need to make a profiling build of some component
# of the tree. Set MAINMOD and MAINFILE and make this target.
+.PHONY: profbuild
profbuild:
mkdir -p dist/pb
ghc --make -isrc \
--- /dev/null
+# Makefile for Sphinx documentation
+#
+
+# You can set these variables from the command line.
+SPHINXOPTS =
+SPHINXBUILD = sphinx-build
+PAPER =
+BUILDDIR = _build
+
+# Internal variables.
+PAPEROPT_a4 = -D latex_paper_size=a4
+PAPEROPT_letter = -D latex_paper_size=letter
+ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
+# the i18n builder cannot share the environment and doctrees with the others
+I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
+
+.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest gettext
+
+help:
+ @echo "Please use \`make <target>' where <target> is one of"
+ @echo " html to make standalone HTML files"
+ @echo " dirhtml to make HTML files named index.html in directories"
+ @echo " singlehtml to make a single large HTML file"
+ @echo " pickle to make pickle files"
+ @echo " json to make JSON files"
+ @echo " htmlhelp to make HTML files and a HTML help project"
+ @echo " qthelp to make HTML files and a qthelp project"
+ @echo " devhelp to make HTML files and a Devhelp project"
+ @echo " epub to make an epub"
+ @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
+ @echo " latexpdf to make LaTeX files and run them through pdflatex"
+ @echo " text to make text files"
+ @echo " man to make manual pages"
+ @echo " texinfo to make Texinfo files"
+ @echo " info to make Texinfo files and run them through makeinfo"
+ @echo " gettext to make PO message catalogs"
+ @echo " changes to make an overview of all changed/added/deprecated items"
+ @echo " linkcheck to check all external links for integrity"
+ @echo " doctest to run all doctests embedded in the documentation (if enabled)"
+
+clean:
+ -rm -rf $(BUILDDIR)/*
+
+html:
+ $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
+ @echo
+ @echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
+
+dirhtml:
+ $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
+ @echo
+ @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
+
+singlehtml:
+ $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
+ @echo
+ @echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
+
+pickle:
+ $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
+ @echo
+ @echo "Build finished; now you can process the pickle files."
+
+json:
+ $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
+ @echo
+ @echo "Build finished; now you can process the JSON files."
+
+htmlhelp:
+ $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
+ @echo
+ @echo "Build finished; now you can run HTML Help Workshop with the" \
+ ".hhp project file in $(BUILDDIR)/htmlhelp."
+
+qthelp:
+ $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
+ @echo
+ @echo "Build finished; now you can run "qcollectiongenerator" with the" \
+ ".qhcp project file in $(BUILDDIR)/qthelp, like this:"
+ @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/Dyna.qhcp"
+ @echo "To view the help file:"
+ @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/Dyna.qhc"
+
+devhelp:
+ $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
+ @echo
+ @echo "Build finished."
+ @echo "To view the help file:"
+ @echo "# mkdir -p $$HOME/.local/share/devhelp/Dyna"
+ @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/Dyna"
+ @echo "# devhelp"
+
+epub:
+ $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
+ @echo
+ @echo "Build finished. The epub file is in $(BUILDDIR)/epub."
+
+latex:
+ $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
+ @echo
+ @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
+ @echo "Run \`make' in that directory to run these through (pdf)latex" \
+ "(use \`make latexpdf' here to do that automatically)."
+
+latexpdf:
+ $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
+ @echo "Running LaTeX files through pdflatex..."
+ $(MAKE) -C $(BUILDDIR)/latex all-pdf
+ @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
+
+text:
+ $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
+ @echo
+ @echo "Build finished. The text files are in $(BUILDDIR)/text."
+
+man:
+ $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
+ @echo
+ @echo "Build finished. The manual pages are in $(BUILDDIR)/man."
+
+texinfo:
+ $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
+ @echo
+ @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
+ @echo "Run \`make' in that directory to run these through makeinfo" \
+ "(use \`make info' here to do that automatically)."
+
+info:
+ $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
+ @echo "Running Texinfo files through makeinfo..."
+ make -C $(BUILDDIR)/texinfo info
+ @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
+
+gettext:
+ $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
+ @echo
+ @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
+
+changes:
+ $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
+ @echo
+ @echo "The overview file is in $(BUILDDIR)/changes."
+
+linkcheck:
+ $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
+ @echo
+ @echo "Link check complete; look for any errors in the above output " \
+ "or in $(BUILDDIR)/linkcheck/output.txt."
+
+doctest:
+ $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
+ @echo "Testing of doctests in the sources finished, look at the " \
+ "results in $(BUILDDIR)/doctest/output.txt."
--- /dev/null
+.. Bibliography
+
+Bibliography
+############
+
+.. [filardo-eisner-2012] Nathaniel W. Filardo and Jason Eisner.
+ :t:`A flexible solver for finite arithmetic circuits`.
+ ICLP LIPIcs, 2012.
+ http://cs.jhu.edu/~jason/papers/#filardo-eisner-2012-iclp
+
+.. [eisner-filardo-2011] Jason Eisner and Nathaniel W. Filardo.
+ :t:`Dyna: Extending Datalog for modern AI`.
+ Datalog Reloaded, 2011.
+ http://cs.jhu.edu/~jason/papers/#eisner-filardo-2011
+
+.. [goodrich-tamassia] Michael T. Goodrich and Roberto Tamassia.
+ :t:`Data Structures and Algorithms in Java`.
+ ISBN 978-0470383261.
+ 2010.
+
+.. [MercuryLang] http://www.mercurylang.org
--- /dev/null
+# -*- coding: utf-8 -*-
+#
+# Dyna documentation build configuration file, created by
+# sphinx-quickstart on Fri May 24 03:04:25 2013.
+#
+# This file is execfile()d with the current directory set to its containing dir.
+#
+# Note that not all possible configuration values are present in this
+# autogenerated file.
+#
+# All configuration values have a default; values that are commented out
+# serve to show the default.
+
+import sys, os, subprocess
+
+# If extensions (or modules to document with autodoc) are in another directory,
+# add these directories to sys.path here. If the directory is relative to the
+# documentation root, use os.path.abspath to make it absolute, like shown here.
+#sys.path.insert(0, os.path.abspath('.'))
+
+# -- General configuration -----------------------------------------------------
+
+# If your documentation needs a minimal Sphinx version, state it here.
+#needs_sphinx = '1.0'
+
+# Add any Sphinx extension module names here, as strings. They can be extensions
+# coming with Sphinx (named 'sphinx.ext.*') or your custom ones.
+extensions = [ 'sphinx.ext.todo'
+ , 'sphinx.ext.mathjax'
+ , 'sphinx.ext.graphviz'
+ , 'sphinx.ext.ifconfig'
+ , 'sphinx.ext.extlinks'
+ ]
+
+# Add any paths that contain templates here, relative to this directory.
+templates_path = []
+
+# The suffix of source filenames.
+source_suffix = '.rst'
+
+# The encoding of source files.
+#source_encoding = 'utf-8-sig'
+
+# The master toctree document.
+master_doc = 'index'
+
+# General information about the project.
+project = u'Dyna2'
+copyright = u'2013, Jason Eisner, Nathaniel Wesley Filardo, Tim Vieira, et al.'
+
+# The version info for the project you're documenting, acts as replacement for
+# |version| and |release|, also used in various other places throughout the
+# built documents.
+#
+# The short X.Y version.
+try:
+ version = subprocess.check_output(["../../dist/build/dyna/dyna"
+ ,"--version-number"])
+except:
+ version = "0.4" # XREF:VERSION
+
+# The full version, including alpha/beta/rc tags.
+release = version + ' git=' + subprocess.check_output(["git", "describe", "--always"])
+
+# The language for content autogenerated by Sphinx. Refer to documentation
+# for a list of supported languages.
+#language = None
+
+# There are two options for replacing |today|: either, you set today to some
+# non-false value, then it is used:
+#today = ''
+# Else, today_fmt is used as the format for a strftime call.
+#today_fmt = '%B %d, %Y'
+
+# List of patterns, relative to source directory, that match files and
+# directories to ignore when looking for source files.
+exclude_patterns = ['_build']
+
+# The reST default role (used for this markup: `text`) to use for all documents.
+#default_role = None
+
+# If true, '()' will be appended to :func: etc. cross-reference text.
+#add_function_parentheses = True
+
+# If true, the current module name will be prepended to all description
+# unit titles (such as .. function::).
+#add_module_names = True
+
+# If true, sectionauthor and moduleauthor directives will be shown in the
+# output. They are ignored by default.
+#show_authors = False
+
+# The name of the Pygments (syntax highlighting) style to use.
+pygments_style = 'sphinx'
+
+# A list of ignored prefixes for module index sorting.
+#modindex_common_prefix = []
+
+
+# -- Options for HTML output ---------------------------------------------------
+
+# The theme to use for HTML and HTML Help pages. See the documentation for
+# a list of builtin themes.
+html_theme = 'default'
+
+# Theme options are theme-specific and customize the look and feel of a theme
+# further. For a list of options available for each theme, see the
+# documentation.
+#html_theme_options = {}
+
+# Add any paths that contain custom themes here, relative to this directory.
+#html_theme_path = []
+
+# The name for this set of Sphinx documents. If None, it defaults to
+# "<project> v<release> documentation".
+#html_title = None
+
+# A shorter title for the navigation bar. Default is the same as html_title.
+#html_short_title = None
+
+# The name of an image file (relative to this directory) to place at the top
+# of the sidebar.
+#html_logo = None
+
+# The name of an image file (within the static path) to use as favicon of the
+# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
+# pixels large.
+#html_favicon = None
+
+# Add any paths that contain custom static files (such as style sheets) here,
+# relative to this directory. They are copied after the builtin static files,
+# so a file named "default.css" will overwrite the builtin "default.css".
+html_static_path = []
+
+# If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
+# using the given strftime format.
+#html_last_updated_fmt = '%b %d, %Y'
+
+# If true, SmartyPants will be used to convert quotes and dashes to
+# typographically correct entities.
+#html_use_smartypants = True
+
+# Custom sidebar templates, maps document names to template names.
+#html_sidebars = {}
+
+# Additional templates that should be rendered to pages, maps page names to
+# template names.
+#html_additional_pages = {}
+
+# If false, no module index is generated.
+#html_domain_indices = True
+
+# If false, no index is generated.
+#html_use_index = True
+
+# If true, the index is split into individual pages for each letter.
+#html_split_index = False
+
+# If true, links to the reST sources are added to the pages.
+#html_show_sourcelink = True
+
+# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
+#html_show_sphinx = True
+
+# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
+#html_show_copyright = True
+
+# If true, an OpenSearch description file will be output, and all pages will
+# contain a <link> tag referring to it. The value of this option must be the
+# base URL from which the finished HTML is served.
+#html_use_opensearch = ''
+
+# This is the file name suffix for HTML files (e.g. ".xhtml").
+#html_file_suffix = None
+
+# Output file base name for HTML help builder.
+htmlhelp_basename = 'Dynadoc'
+
+
+# -- Options for LaTeX output --------------------------------------------------
+
+latex_elements = {
+# The paper size ('letterpaper' or 'a4paper').
+#'papersize': 'letterpaper',
+
+# The font size ('10pt', '11pt' or '12pt').
+#'pointsize': '10pt',
+
+# Additional stuff for the LaTeX preamble.
+#'preamble': '',
+}
+
+# Grouping the document tree into LaTeX files. List of tuples
+# (source start file, target name, title, author, documentclass [howto/manual]).
+latex_documents = [
+ ('index', 'Dyna.tex', u'Dyna Documentation',
+ u'Jason Eisner, Nathaniel Wesley Filardo, Tim Vieira, et al.', 'manual'),
+]
+
+# The name of an image file (relative to this directory) to place at the top of
+# the title page.
+#latex_logo = None
+
+# For "manual" documents, if this is true, then toplevel headings are parts,
+# not chapters.
+#latex_use_parts = False
+
+# If true, show page references after internal links.
+#latex_show_pagerefs = False
+
+# If true, show URL addresses after external links.
+#latex_show_urls = False
+
+# Documents to append as an appendix to all manuals.
+#latex_appendices = []
+
+# If false, no module index is generated.
+#latex_domain_indices = True
+
+
+# -- Options for manual page output --------------------------------------------
+
+# One entry per manual page. List of tuples
+# (source start file, name, description, authors, manual section).
+man_pages = [
+ ('index', 'dyna', u'Dyna Documentation',
+ [u'Jason Eisner, Nathaniel Wesley Filardo, Tim Vieira, et al.'], 1)
+]
+
+# If true, show URL addresses after external links.
+#man_show_urls = False
+
+
+# -- Options for Texinfo output ------------------------------------------------
+
+# Grouping the document tree into Texinfo files. List of tuples
+# (source start file, target name, title, author,
+# dir menu entry, description, category)
+texinfo_documents = [
+ ('index', 'Dyna', u'Dyna Documentation',
+ u'Jason Eisner, Nathaniel Wesley Filardo, Tim Vieira, et al.',
+ 'Dyna',
+ u'Logic programming language',
+ 'Miscellaneous'),
+]
+
+# Documents to append as an appendix to all manuals.
+#texinfo_appendices = []
+
+# If false, no module index is generated.
+#texinfo_domain_indices = True
+
+# How to display URL addresses: 'footnote', 'no', or 'inline'.
+#texinfo_show_urls = 'footnote'
+
+# -- Miscellaneous Options -----------------------------------------------------
+
+# rst_prolog = ""
+
+extlinks = {'dynasrc': ('https://www.github.com/nwf/dyna/blob/master/%s',
+ 'file ' )
+ ,'githubbug': ("https://github.com/nwf/dyna/issues/%s",
+ 'issue ')
+ }
--- /dev/null
+.. Dyna2 documentation master file
+
+Welcome to Dyna2's documentation!
+=================================
+
+Dyna2 is an experimental new logic programming language developed at
+`Johns Hopkins University <http://www.jhu.edu>`_
+
+.. warning:: Please be advised that this documentation, the implementation,
+ and indeed the language itself are rapidly changing.
+
+.. warning:: Attempting to run Dyna programs may often crash our interpreter
+ or yield programs which run forever. (In the latter case, Control-C will
+ stop the program's execution.) If either of these things happen
+ unexpectedly, please contact a TA.
+
+Contents:
+
+.. toctree::
+ :maxdepth: 2
+
+ tutorial/index
+
+ spec/index
+
+ Bibliography <bib>
+
+Indices and tables
+==================
+
+* :ref:`genindex`
+* :ref:`search`
+
--- /dev/null
+.. Spec glossary
+ This file is enumerated in the toctree of spec/index.rst
+
+Specification Glossary
+######################
+
+.. glossary::
+
+ functor
+
+ The constructor of a term, such as ``path`` in ``path(1,2)``.
+
+ null
+
+ The value of items that have no rules contributing aggregands.
+ Null *annihilates* expressions (*e.g.* :math:`\mbox{null} + 2`
+ is :math:`\mbox{null}`) and is the *unit* of aggregations
+ (*e.g.* :math:`\sum\{\mbox{null}, 1, \mbox{null}, 2\}` is
+ just :math:`\sum\{1,2\}`).
--- /dev/null
+.. Specification index
+ This file is enumerated in the toctree directive of index.rst
+
+Specifications
+##############
+
+.. toctree::
+
+ pragmas
+ glossary
--- /dev/null
+.. Pragmas
+ This file documents the pragma assertions our pipeline understands.
+
+*******
+Pragmas
+*******
+
+Pragmas are used to pass a wide variety of information in to the system.
+They are visually separated by begining with ``:-``.
+
+######
+Syntax
+######
+
+Some pragmas alter the syntax of the language.
+
+.. index::
+ double: pragma; disposition
+
+.. _pragma_disposition:
+
+Disposition
+===========
+
+In Dyna source code, there are two different things that the term ``f(1,2)``
+could mean:
+
+* Construct the piece of data whose functor is ``f`` and has arguments
+ ``1`` and ``2``, as in ``f(A,B) = f(1,2)``, which unifies ``A`` with ``1``
+ and ``B`` with ``2``.
+
+* Compute the value of the ``f(1,2)`` item, as in ``f(1,2) + 3`` or
+ ``Y is f(1,2)``.
+
+It is always possible to explicitly specify which meaning to use, by use of
+the ``&`` and ``*`` operators (see :ref:`syntax-quote-eval`), but this would
+be tedious if it were the only solution. As such, we endow functors (of
+given arity) with *dispositions*, which indicate, by default, how they would
+like to treat their arguments.
+
+Dispositions are specified with the ``:-dispos`` pragma, thus::
+
+ :-dispos g(&). % g quotes its argument.
+ :-dispos '+'(*,*). % + evaluates both arguments.
+
+Now ``g(f(1,2)) + 1`` will pass the structure ``f(1,2)`` to the ``g``
+function and add ``1`` to the result. Note that dispositions take effect
+*while the program is being parsed*. That is, a program like::
+
+ :-dispos f(&).
+ goal += f(g(1)).
+ :-dispos f(*).
+ goal += f(g(2)).
+
+specifies that ``goal`` has two antecedents: the ``f`` images of ``g(1)``
+and the ``g`` image of ``2``.
+
+It is also possible to indicate that some terms should not be evaluated::
+
+ :-dispos &pair(*,*). % pair suppresses its own evaluation
+
+In the case of disagreements, like ``pair(1,2) + pair(3,4)``, the preference
+of the argument is honored.
+
+.. admonition:: Defaults
+
+ Absent any declarations, all functors are predisposed to evaluate their
+ arguments. Some functors (``pair/2``, ``true/0``, and ``false/0``)
+ suppress their own evaluation.
+
+More Detail
+-----------
+
+.. warning:: This section is probably relevant only if you are a developer
+ of the Dyna compiler.
+
+Requesting Evaluation
+^^^^^^^^^^^^^^^^^^^^^
+
+Just like it is possible to request that some functors not be evaluated even
+when in evaluation context, it is additionally possible for functors to
+request that they be evaluated even when the context is one of quotation::
+
+ :-dispos *f(*).
+
+The neutral position of specifying neither ``&`` nor ``*`` before a pragma
+is termed *inherit*, which means that the context or overrides apply. Under
+the defaults above, this is the default position for all functors.
+
+Disposition Defaults
+^^^^^^^^^^^^^^^^^^^^
+
+It is possible to override the defaults, as well; at least one of us has a
+stylistic preference for a more Prolog-styled structure-centric view of the
+universe. The pragma::
+
+ :-dispos_def prologish.
+
+will cause subsequent rules to behave as if all functors which start with an
+alphanumeric character had had ``:-dispos f(&,...,&)`` asserted, while all
+other functors had had ``:-dispos *f(*,...,*)``. There are, however, a few
+built-in overrides to this rule of thumb, giving alphabetic mathematical
+operators (*e.g.* ``abs``, ``exp``, ...) their functional meaning. See
+:dynasrc:`src/Dyna/Term/SurfaceSyntax.hs`
+
+The default default rules may be brought back in by either::
+
+ :-dispos_def dyna.
+ :-dispos_def.
+
+Note that when chaning defaults, any manually-speficied ``:-dispos``
+pragmas remain in effect.
+
+.. index::
+ double: pragma; operator
+
+.. _pragma_operator:
+
+Operators
+=========
+
+Dyna aims to have a rather flexible surface syntax; part of that goal is
+achieved by allowing the user to specify their own operators.
+
+As with :ref:`pragma_disposition`, these pragmas take effect
+*while the program is being parsed*.
+
+.. admonition:: bug
+
+ The ability to add and remove operators is not yet actually supported.
+
+Adding an operator
+------------------
+
+The ``:-oper add`` pragma takes three arguments: the fixity, priority, and
+lexeme that makes up the operator. Fixities are specified as ``pre``,
+``post`` or ``in``. Priorities are natural numbers, with higher numbers
+binding tighter. Lexemes are either bare words or singly-quoted functors.
+
+Examples::
+
+ :-oper add in 6 + .
+ :-oper add pre 9 - .
+
+Removing an operator
+--------------------
+
+The ``:-oper del`` pragma may be used to remove all previously added forms
+of a given operator.
+
+Defaults
+--------
+
+The default operator table is, hopefully, more or less what you might
+expect and follows the usual rules of arithmetic.
+
+.. admonition:: bug
+
+ For the moment, the source is the spec. See the source
+ :dynasrc:`src/Dyna/Term/SurfaceSyntax.hs` for full details.
+
+#########
+Execution
+#########
+
+On the other hand, some pragmas impact the execution of the system.
+
+.. index::
+ double: pragma; inst
+ double: pragma; mode
+
+.. _pragma_inst_mode:
+
+Insts and Modes
+===============
+
+Following the [MercuryLang]_ syntax, we allow the user to give names to
+instantiation states and modes::
+
+ :-inst name(args) == ... .
+ :-inst mode(args) == ... >> ... .
+
+.. index::
+ double: pragma; query mode
+ single: qmode
+
+.. _pragma_qmode:
+
+Query Modes
+===========
+
+A Query mode specifies that a particular backward-chaining operation is to
+be available to the system. These capture the change in instantiation
+state, determinism, and other properties of a query.
--- /dev/null
+.. Dijkstra tutorial page
+ This file is enumerated in the toctree of tutorial/index.rst
+
+.. index::
+ double: Shortest Path; Tutorial
+
+Shortest Path in a Graph
+************************
+
+We hope that Dyna offers the shortest ever shortest path program::
+
+ path(start) min= 0.
+ path(B) min= path(A) + edge(A,B).
+ goal min= path(end).
+
+This program already highlights one of the features of Dyna: the first rule
+and last rules are *dynamic*: the *value* of the ``start`` item determines
+which vertex in the graph is used as the start, and similarly the value of
+``end`` is used to select which vertex matters to ``goal``.
+
+This program is available in ``examples/dijkstra.dyna`` (or
+:dynasrc:`here <examples/dijkstra.dyna>`).
+
+Encoding the Input
+==================
+
+The following input graph is adapted from Goodrich & Tamassia's data
+structures textbook. It shows several available flights between U.S.
+airports, with their distances in miles. We would like to get from a
+friend's house, 10 miles from Boston (BOS), to our destination, 20 miles
+from Chicago (ORD).
+
+.. graphviz::
+
+ digraph foo {
+ graph[size="7,2",rankdir="LR"]
+
+ BOS -> JFK [label=187]
+ BOS -> MIA [label=1258]
+ JFK -> DFW [label=1391]
+ JFK -> SFO [label=2582]
+ JFK -> MIA [label=1090]
+ MIA -> DFW [label=1121]
+ MIA -> LAX [label=2342]
+ DFW -> ORD [label=802]
+ DFW -> LAX [label=1235]
+ ORD -> DFW [label=802]
+ LAX -> ORD [label=1749]
+
+ FriendHouse -> BOS [label=10]
+ ORD -> MyHouse [label=20]
+ }
+
+.. sidebar:: Shortest Paths
+
+ If we work things out by hand (or just ask Dyna) we will discover
+ that the shortest path to each node from "FriendHouse" is
+
+ .. rst-class:: center
+ ..
+
+ ============= =====
+ Destination Total
+ ============= =====
+ FriendHouse 0
+ BOS 10
+ JFK 197
+ MIA 1268
+ DFW 1588
+ ORD 2390
+ MyHouse 2410
+ SFO 2779
+ LAX 2823
+ ============= =====
+
+This is encoded into Dyna, using strings to identify vertices of the graph,
+thus::
+
+ edge("BOS","JFK") := 187.
+ edge("BOS","MIA") := 1258.
+ edge("JFK","DFW") := 1391.
+ edge("JFK","SFO") := 2582.
+ edge("JFK","MIA") := 1090.
+ edge("MIA","DFW") := 1121.
+ edge("MIA","LAX") := 2342.
+ edge("DFW","ORD") := 802.
+ edge("DFW","LAX") := 1235.
+ edge("ORD","DFW") := 802.
+ edge("LAX","ORD") := 1749.
+
+ edge("FriendHouse","BOS") := 10.
+ edge("ORD","MyHouse") := 20.
+
+``edge`` pairs that are not specified are said to be :term:`null`; that is,
+they have no value, and can be thought of as the identity of the aggregator
+``min=``, or :math:`+\infty`, meaning "You can't get there directly from
+here."
+
+And of course, we need to specify whence we come and where it is we would
+like to end up::
+
+ start := "FriendHouse".
+ end := "MyHouse".
+
+Run the program
+===============
+
+We can run this program in the interpreter::
+
+ ./dyna -i examples/dijkstra.dyna
+
+We are met with the conclusions, which include all the data we fed in as
+well as a pile of ``path`` assertions. Of course, that's not so useful,
+necessarily, so let's just ask for the answer::
+
+ :- query goal
+ out(0) := [(2410, {})]
+
+As we can see, the total weight of the shortest path is ``2410``. What
+happens, though, if we realize that we will be by the airport anyway? ::
+
+ :- start := "BOS".
+ =============
+ goal := 2400
+ out(0) := [(2400, {})]
+ path('BOS') := 0
+ path('DFW') := 1578
+ path('FriendHouse') := None
+ path('JFK') := 187
+ path('LAX') := 2813
+ path('MIA') := 1258
+ path('MyHouse') := 2400
+ path('ORD') := 2380
+ path('SFO') := 2769
+ start := 'BOS'
+
+And just like that, the total path weight from ``start`` to ``end`` is now
+``2400``. The system also tells us a number of potentially interesting
+things:
+
+* The system has in fact computed the revised ``path`` costs to each other
+ vertex.
+
+* There is no path from ``"BOS"`` to ``"FriendHouse"`` (thus ``None``).
+
+* A query we had made earlier has changed its answer.
+
+Explaining Answers
+==================
+
+.. admonition:: bug
+
+ We do not yet have a good mechanism implemented, though it's just a
+ matter of time. See :githubbug:`1`.
+
+Understanding The Program
+=========================
+
+Simply stated, this program looks for all paths from the vertex indicated by
+``start``. Formally, the technique currently used is called *agenda-driven
+semi-naive forward chaining* [#snfc]_ .
+
+Inference Rules
+---------------
+
+The first inference rule states that there is no distance on the degenerate
+path that does not go anywhere.::
+
+ path(start) min= 0.
+
+Alternatively, there is a path to vertex ``B`` if there is a path to some
+vertex ``A`` such that an edge connects ``A`` to ``B``.::
+
+ path(B) min= path(A) + edge(A,B).
+
+The final rule merely says that we are looking for the best path to the
+vertex indicated by ``end``.::
+
+ goal min= path(end).
+
+Inference Rules As Equations
+----------------------------
+
+But what are the ``min=`` and ``+`` doing? In fact, the inference rules are
+equations. They state how to find the values of all ``pathto`` and ``goal``
+items.
+
+Those items have values just like the ``hello``, ``world`` and ``goal``
+items in :doc:`the previous example <hello>`. But this program is more
+complicated. It involves lots of different ``pathto`` items for different
+airports, distinguished from one another by their arguments:
+``pathto("JFK")``, ``pathto("MyHouse")``, etc. These items may all have
+different values.
+
+Why These Particular Equations?
+-------------------------------
+
+Assuming that each ``edge``'s value represents its length in the input graph,
+the rules are carefully written so that ``pathto(V)``'s value will be the total
+length of the shortest path from the ``start`` vertex to vertex ``V``.
+
+In principle, there are several ways to get to ``V``: one can get there by
+an edge from ``start`` or an edge from some other ``U``. The ``min=``
+operator finds the minimum over all these possibilities. Think of it as
+keeping a running minimum (just as ``+=`` would keep a running total). In
+particular, ``pathto(V)`` is found as
+:math:`\mbox{min}(\mathtt{edge(start},V), \mbox{min}_U \mathtt{pathto}(U)+\mathtt{edge}(U,V))`
+which involves minimizing over all possible ``U``.
+
+If there are no paths to ``V``, then ``pathto(V)`` is a minimum over no
+lengths at all. Dyna specifies that items receiving no inputs take on the
+special value :term:`null`, which is the *identity* of every aggregator and
+a *zero* of every expression. Since we aggregate answers with ``min=``,
+:term:`null` approximates :math:`+\infty`.
+
+Endnotes
+========
+
+.. [#snfc] There are a multitude of inference algorithms for logic
+ programming. We would like to think that [filardo-eisner-2012]_ provides
+ a good overview as well as explaining the basics of what will become
+ Dyna 2's inference algorithm.
--- /dev/null
+.. Hello World tutorial page
+ This file is enumerated in the toctree of tutorial/index.rst
+
+.. index::
+ single: Tutorial; Hello World
+
+Hello World
+***********
+
+Welcome to the Dyna tutorial!
+
+It is traditional to start by writing and running a program that prints
+hello world. :ref:`Downlad Dyna </download>` and follow the instructions in
+``README.md`` to build it. Then, look at the file
+``examples/helloworld.dyna`` (or :dynasrc:`here <examples/helloworld.dyna>`).
+It should contain::
+
+ goal += hello*world. % an inference rule for deriving values
+ hello := 6. % some initial values
+ world := 7.
+
+This does not print hello world. It was the closest we could come. Dyna is a
+*pure* language. It focuses on computation, and sniffs haughtily at mundane
+concerns like input and output.
+
+Running Hello World
+===================
+
+After building Dyna, you may ask our interpreter to run ``helloworld`` by
+executing ::
+
+ ./dyna examples/helloworld.dyna
+
+At this point, you should see::
+
+ Charts
+ ============
+ goal/0
+ =================
+ goal := 42
+
+ hello/0
+ =================
+ hello := 6
+
+ world/0
+ =================
+ world := 7
+
+What has happened? Dyna has compiled and executed the program requested and
+printed out its conclusions. Notably, the item ``goal`` is seen to have
+value ``42``. Whenever the runtime prints all of its conclusions, they are
+organized by :term:`functor`
+
+The Interactive Interpreter
+===========================
+
+Dyna also comes with an :ref:`interactive interpreter </spec/repl>`. This
+mode allows you to
+
+* append new rules to the program and observe the consequences
+* make custom queries of the conclusions
+* visualize the information flow within the program
+
+To run a program interactively, add ``-i`` to the ``dyna`` command line::
+
+ ./dyna -i examples/helloworld.dyna
+
+In addition to the chart printout above, you will be greeted with the
+interpreter's prompt, ``:-``. Interactive help is available by typing
+``help`` at the prompt.
+
+Let's try adding a new rule to the program. Suppose that our goal is not
+merely to multiply ``hello`` by ``world`` but to additionally square
+``hello``. At the prompt, type::
+
+ goal += hello**2.
+
+The interpreter will respond with::
+
+ goal := 78
+
+Here you can see that ``goal``'s value has changed to be ``78``. But wait,
+is that right? We can check by typing at the prompt::
+
+ query hello**2
+
+.. admonition:: bug
+
+ The output for the query is not especially friendly. There's a
+ :githubbug:`bug <1>` filed about that and it's being worked on.
+
+If we modify one of the inputs ``hello`` or ``world``, by typing::
+
+ hello += 1.
+
+The interpreter will respond with::
+
+ goal := 120
+ hello := 8
+ out(3) := [(64, {})]
+
+So not only is it telling us that ``hello`` has changed, and that ``goal``
+now takes on a new value as a result, but it reminds us that the query we
+ran earlier also has a new value.
+
+At this point, we invite you to continue the tutorial by :doc:`finding the
+shortest path <dijkstra>`.
--- /dev/null
+.. Tutorial index
+ This file is enumerated in the toctree directive of /index.rst
+
+Tutorial
+########
+
+.. toctree::
+
+ hello
+ dijkstra
Name: dyna
+-- XREF:VERSION
Version: 0.4
Cabal-Version: >=1.14
Build-Type: Simple
-
% Dijkstra's algorithm for single-source shortest path
-path(start) min= 0 .
+path(start) min= 0.
path(B) min= path(A) + edge(A,B).
+goal min= path(end).
+
+edge("BOS","JFK") := 187.
+edge("BOS","MIA") := 1258.
+edge("JFK","DFW") := 1391.
+edge("JFK","SFO") := 2582.
+edge("JFK","MIA") := 1090.
+edge("MIA","DFW") := 1121.
+edge("MIA","LAX") := 2342.
+edge("DFW","ORD") := 802.
+edge("DFW","LAX") := 1235.
+edge("ORD","DFW") := 802.
+edge("LAX","ORD") := 1749.
-start := "a".
+edge("FriendHouse","BOS") := 10.
+edge("ORD","MyHouse") := 20.
-edge("a","b") := 1.
-edge("b","d") := 1.
-edge("a","d") := 3.
-edge("a","c") := 1.
-edge("c","d") := 2.
+start := "FriendHouse".
+end := "MyHouse".
-% Expected
-% path("a") = 0
-% path("b") = 1
-% path("c") = 1
-% path("d") = 2
+% This file is mentioned in the tutorial!
+% XREF:docs/sphinx/tutorial/dijkstra.rst
============
edge/2
=================
-edge('a','b') := 1
-edge('a','c') := 1
-edge('a','d') := 3
-edge('b','d') := 1
-edge('c','d') := 2
+edge('BOS','JFK') := 187
+edge('BOS','MIA') := 1258
+edge('DFW','LAX') := 1235
+edge('DFW','ORD') := 802
+edge('FriendHouse','BOS') := 10
+edge('JFK','DFW') := 1391
+edge('JFK','MIA') := 1090
+edge('JFK','SFO') := 2582
+edge('LAX','ORD') := 1749
+edge('MIA','DFW') := 1121
+edge('MIA','LAX') := 2342
+edge('ORD','DFW') := 802
+edge('ORD','MyHouse') := 20
+
+end/0
+=================
+end := 'MyHouse'
+
+goal/0
+=================
+goal := 2410
path/1
=================
-path('a') := 0
-path('b') := 1
-path('c') := 1
-path('d') := 2
+path('BOS') := 10
+path('DFW') := 1588
+path('FriendHouse') := 0
+path('JFK') := 197
+path('LAX') := 2823
+path('MIA') := 1268
+path('MyHouse') := 2410
+path('ORD') := 2390
+path('SFO') := 2779
start/0
=================
-start := 'a'
+start := 'FriendHouse'
--- /dev/null
+goal += hello*world. % an inference rule for deriving values
+hello := 6. % some initial values
+world := 7.
+
+% This file is mentioned in the tutorial!
+% XREF:docs/sphinx/tutorial/hello.rst
| QEHelpBackend
| QEHelpDump
| QEVersion
+ | QEVersionNumber
quickExit :: QuickExit -> IO ()
--- XXX
-quickExit QEBiblio = putStrLn "Bibliographic suggestions would appear here"
-quickExit QEHelp =
+quickExit QEBiblio = do
+ qeBanner "Recommended readings"
+ PPA.putDoc $ PPA.vcat
+ [ (PPA.<$>) (for PPA.green "users")
+ $ PPA.indent 2 $ PPA.vcat
+ [ "Documentation, including a tutorial,"
+ PPA.<+> "is available by running"
+ PPA.<+> PPA.white "make sphinxdoc"
+ PPA.<+> PPA.dot
+ ]
+ , (PPA.<$>) (for PPA.yellow "theoreticians and academics")
+ $ PPA.indent 2 $ PPA.vcat
+ [ "Several papers are available at"
+ PPA.<+> PPA.underline
+ "http://www.dyna.org/wiki/index.php?title=Publications"
+ PPA.<+> PPA.dot
+ ]
+ , (PPA.<$>) (for PPA.red "developers")
+ $ PPA.indent 2 $ PPA.vcat
+ [ "Source-based documentation can be built by"
+ PPA.<+> PPA.white "make haddock"
+ PPA.<+> PPA.dot
+ ]
+ , PPA.empty
+ ]
+ where
+ for c w = "For" PPA.<+> c w PPA.<> PPA.colon
+
+quickExit QEHelp = do
+ qeBanner "Help! I need somebody! Help! Not just anybody! Heeelp!"
+ putStrLn disclaimer
putStrLn (usageInfo h helpfulOptions)
where
+ disclaimer = "This version of Dyna2 represents a prototype!\n"
+ ++ "There are known inefficiencies and less-than-ideal code.\n"
+ ++ "We hope that you enjoy using it despite these woes! :)"
+
h = "\nUsage: dyna -B backend -o FILE.out FILE.dyna\n\nOption summary:"
quickExit QEHelpBackend = do
+ qeBanner "Backend information"
putDoc backendHelp
putStrLn ""
-quickExit QEHelpDump = putStrLn (usageInfo "\nDump options:" $ dumpOpts False)
-quickExit QEVersion = return ()
+quickExit QEHelpDump = do
+ qeBanner "Debugging dumps"
+ putStrLn (usageInfo "" $ dumpOpts False)
+quickExit QEVersion = putStrLn $ "Dyna " ++ version
+quickExit QEVersionNumber = putStrLn version
+
+version :: String
+version = "0.4" -- XREF:VERSION
+qeBanner :: String -> IO ()
+qeBanner s = putStrLn $ "Dyna " ++ version ++ ": " ++ s
data Opt = OptQE QuickExit
| OptBackend Backend
infoOpts :: [OptDescr Opt]
infoOpts =
[ Option ['V'] ["version"] (NoArg $ OptQE QEVersion) "display version and exit"
- -- This is an excellent idea we might consider, taken from the 'pi'
- -- program of http://www.ginac.de/CLN/
+
+ -- This is an excellent idea, taken from 'pi' at http://www.ginac.de/CLN/
, Option [] ["bibliography"] (NoArg $ OptQE QEBiblio) "relevant papers"
]
+-- | Miscellaneous options which the user probably does not care about
+unhelpfulOpts :: [OptDescr Opt]
+unhelpfulOpts =
+ [ Option [] ["version-number"] (NoArg $ OptQE QEVersionNumber)
+ "Display just the version number and exit"
+ ]
+
coreOpts :: [OptDescr Opt]
coreOpts =
[ Option ['B'] ["backend"] (ReqArg obe "BE")
allOptions :: [OptDescr Opt]
allOptions =
helpOpt : helpMoreOpts ++ infoOpts ++ coreOpts ++ (dumpOpts True)
+ ++ unhelpfulOpts
--- When the user has asked for help, what do they want to see?
+-- | When the user has asked for help, what do they want to see?
helpfulOptions :: [OptDescr Opt]
helpfulOptions = helpMoreOpts ++ infoOpts ++ coreOpts
case getOpt Permute allOptions argv of
(os,as,[]) -> case foldOpts os of
Left x -> do
- putStrLn "Dyna 0.4"
quickExit x
exitSuccess
Right f -> return $ (f defaultDynacConfig, as)
main :: IO ()
main = catches (getArgs >>= main_)
- [Handler printerr, Handler someExnPanic]
+ [Handler printerr, Handler exit, Handler someExnPanic]
where
printerr x = pe x >> exitFailure
hPutStrLn stderr ""
pe (Panic d) = panic d
+ exit ExitSuccess = return ()
+ exit (ExitFailure n) = panic $ "Haskell exit code: " <+> pretty n
+
someExnPanic (e :: SomeException) = panic $ "Uncaught Haskell exception:"
<+> text (show e)
-- rule index as an opaque token rather than something to be
-- interpreted. Eventually this will go away, when our
-- REPLs have captive compilers.
-
- -- | PMisc Term
- -- ^ Fall-back parser for :- lines.
+
+ {- --- | PMisc Term
+ -- ^ Fall-back parser for :- lines. -}
deriving (Eq,Show)
-
-- | The type of a parsed inst declaration
data ParsedInst = PIVar !B.ByteString
| PIInst !(InstF DFunct ParsedInst)
projects / dyna2 / commitdiff