From: Nathaniel Wesley Filardo Date: Wed, 5 Jun 2013 05:06:45 +0000 (-0400) Subject: New documentation and cleanups X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=1c8b95fb245917f8329a24596db48d3ed18ca1f0;p=dyna2 New documentation and cleanups Notably, add docs/sphinx for our prose documentation and several corresponding Makefile targets. --- diff --git a/.gitignore b/.gitignore index a17f27d..26624b4 100644 --- a/.gitignore +++ b/.gitignore @@ -4,5 +4,9 @@ dist/ examples/*.d -examples/*.out +examples/*.hist examples/*.plan +examples/*.plan.py +examples/*.out + +docs/sphinx/_build diff --git a/Makefile b/Makefile index 594cd87..398eb8c 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ # -*- indent-tabs-mode:t; -*- -all: deps build +all: deps build sphinxbuild upstream: git submodule init @@ -10,8 +10,8 @@ upstream: # 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: @@ -39,6 +39,7 @@ run-parser: # perfect, but it does OK. HADDOCK_HTML ?= "../\\$$pkgid/html" +.PHONY: haddock haddock: mkdir -p dist/alldoc haddock --html -o dist/alldoc \ @@ -47,8 +48,20 @@ haddock: `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 @@ -66,6 +79,7 @@ ghcbuild: # 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 \ diff --git a/docs/sphinx/Makefile b/docs/sphinx/Makefile new file mode 100644 index 0000000..7786914 --- /dev/null +++ b/docs/sphinx/Makefile @@ -0,0 +1,153 @@ +# 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 ' where 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." diff --git a/docs/sphinx/bib.rst b/docs/sphinx/bib.rst new file mode 100644 index 0000000..a417290 --- /dev/null +++ b/docs/sphinx/bib.rst @@ -0,0 +1,21 @@ +.. 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 diff --git a/docs/sphinx/conf.py b/docs/sphinx/conf.py new file mode 100644 index 0000000..22aeb35 --- /dev/null +++ b/docs/sphinx/conf.py @@ -0,0 +1,264 @@ +# -*- 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 +# " v 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 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 ') + } diff --git a/docs/sphinx/index.rst b/docs/sphinx/index.rst new file mode 100644 index 0000000..3349c8b --- /dev/null +++ b/docs/sphinx/index.rst @@ -0,0 +1,33 @@ +.. Dyna2 documentation master file + +Welcome to Dyna2's documentation! +================================= + +Dyna2 is an experimental new logic programming language developed at +`Johns Hopkins University `_ + +.. 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 + +Indices and tables +================== + +* :ref:`genindex` +* :ref:`search` + diff --git a/docs/sphinx/spec/glossary.rst b/docs/sphinx/spec/glossary.rst new file mode 100644 index 0000000..c08f965 --- /dev/null +++ b/docs/sphinx/spec/glossary.rst @@ -0,0 +1,19 @@ +.. 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\}`). diff --git a/docs/sphinx/spec/index.rst b/docs/sphinx/spec/index.rst new file mode 100644 index 0000000..1016b73 --- /dev/null +++ b/docs/sphinx/spec/index.rst @@ -0,0 +1,10 @@ +.. Specification index + This file is enumerated in the toctree directive of index.rst + +Specifications +############## + +.. toctree:: + + pragmas + glossary diff --git a/docs/sphinx/spec/pragmas.rst b/docs/sphinx/spec/pragmas.rst new file mode 100644 index 0000000..fadbb1b --- /dev/null +++ b/docs/sphinx/spec/pragmas.rst @@ -0,0 +1,194 @@ +.. 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. diff --git a/docs/sphinx/tutorial/dijkstra.rst b/docs/sphinx/tutorial/dijkstra.rst new file mode 100644 index 0000000..d3d3d5b --- /dev/null +++ b/docs/sphinx/tutorial/dijkstra.rst @@ -0,0 +1,222 @@ +.. 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 `). + +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 `. 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. diff --git a/docs/sphinx/tutorial/hello.rst b/docs/sphinx/tutorial/hello.rst new file mode 100644 index 0000000..012fe3e --- /dev/null +++ b/docs/sphinx/tutorial/hello.rst @@ -0,0 +1,108 @@ +.. 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 ` and follow the instructions in +``README.md`` to build it. Then, look at the file +``examples/helloworld.dyna`` (or :dynasrc:`here `). +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 `. 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 `. diff --git a/docs/sphinx/tutorial/index.rst b/docs/sphinx/tutorial/index.rst new file mode 100644 index 0000000..bfd017d --- /dev/null +++ b/docs/sphinx/tutorial/index.rst @@ -0,0 +1,10 @@ +.. Tutorial index + This file is enumerated in the toctree directive of /index.rst + +Tutorial +######## + +.. toctree:: + + hello + dijkstra diff --git a/dyna.cabal b/dyna.cabal index 91469fa..704e399 100644 --- a/dyna.cabal +++ b/dyna.cabal @@ -1,4 +1,5 @@ Name: dyna +-- XREF:VERSION Version: 0.4 Cabal-Version: >=1.14 Build-Type: Simple diff --git a/examples/dijkstra.dyna b/examples/dijkstra.dyna index 8952c29..3d9d70c 100644 --- a/examples/dijkstra.dyna +++ b/examples/dijkstra.dyna @@ -1,18 +1,25 @@ - % 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 diff --git a/examples/expected/dijkstra.py.out b/examples/expected/dijkstra.py.out index 397415a..562a7a8 100644 --- a/examples/expected/dijkstra.py.out +++ b/examples/expected/dijkstra.py.out @@ -3,20 +3,41 @@ Charts ============ 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' diff --git a/examples/helloworld.dyna b/examples/helloworld.dyna new file mode 100644 index 0000000..76ca087 --- /dev/null +++ b/examples/helloworld.dyna @@ -0,0 +1,6 @@ +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 diff --git a/src/Dyna/Main/Driver.hs b/src/Dyna/Main/Driver.hs index d477a2a..2bc3ad3 100644 --- a/src/Dyna/Main/Driver.hs +++ b/src/Dyna/Main/Driver.hs @@ -114,20 +114,62 @@ data QuickExit = QEBiblio | 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 @@ -146,11 +188,18 @@ helpMoreOpts = 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") @@ -165,8 +214,9 @@ coreOpts = 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 @@ -175,7 +225,6 @@ procArgs argv = do 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) @@ -316,7 +365,7 @@ main_ argv = do main :: IO () main = catches (getArgs >>= main_) - [Handler printerr, Handler someExnPanic] + [Handler printerr, Handler exit, Handler someExnPanic] where printerr x = pe x >> exitFailure @@ -336,6 +385,9 @@ main = catches (getArgs >>= main_) 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) diff --git a/src/Dyna/ParserHS/Parser.hs b/src/Dyna/ParserHS/Parser.hs index 1f9ef78..1a12beb 100644 --- a/src/Dyna/ParserHS/Parser.hs +++ b/src/Dyna/ParserHS/Parser.hs @@ -144,12 +144,11 @@ data Pragma = PDispos SelfDispos B.ByteString [ArgDispos] -- 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)