Merge branch 'master' of ssh://github.com/nwf/dyna into HEAD

.gitmodules

@@ -7,3 +7,6 @@
 [submodule "external/ekmett-trifecta"]
 	path = external/ekmett-trifecta
 	url = git://github.com/ekmett/trifecta.git
+[submodule "docs/sphinx/_themes/bootstrap"]
+	path = docs/sphinx/_themes/bootstrap
+	url = https://github.com/ryan-roemer/sphinx-bootstrap-theme.git

Makefile

@@ -6,27 +6,34 @@ all: deps build sphinxbuild
 
 .PHONY: $(VERFILE)
 $(VERFILE):
+	mkdir -p `dirname $@`
 	echo "Version: Dyna 0.4 pre-release" `git describe --all` > $@
 	echo "Build date:" `date` >> $@
 	echo "Commit: https://github.com/nwf/dyna/commit/"`git rev-parse HEAD` >> $@
 
+.PHONY: upstream
 upstream:
-	git submodule init
+	git submodule update --init
 	# git submodule update external/ekmett-parsers external/ekmett-trifecta
 	# cabal install --user --enable-tests --only-dependencies \
 	#  external/ekmett-parsers external/ekmett-trifecta .
 	# cabal install --user external/ekmett-parsers external/ekmett-trifecta
 
+.PHONY: deps
 deps:
 	alex --version 2>/dev/null >/dev/null || cabal install alex
 	happy --version 2>/dev/null >/dev/null || cabal install happy
 	cabal install --user --enable-tests --only-dependencies .
 
+.PHONY: build
 build: $(VERFILE)
-	cabal configure --user --enable-tests
+	cabal configure --user
 	cabal build
 
-test tests: build
+.PHONY: test tests
+test tests:
+	cabal configure --user --enable-tests
+	cabal build
 	dist/build/dyna-selftests/dyna-selftests
 	misc/dyna-doctest.py
 	# cabal test
@@ -52,9 +59,6 @@ clean:
 veryclean: clean
 	rm -rf dist/*
 
-run-parser:
-	ghci -isrc Dyna.ParserHS.Parser
-
 # Cabal's haddock integration is sort of sad; since I want to have
 # everything we use in one place, run haddock by hand.  This still isn't
 # perfect, but it does OK.
@@ -72,7 +76,7 @@ haddock:
 # Build our sphinx documentation
 .PHONY: sphinxbuild sphinxdoc
 sphinxbuild:
-	(cd docs/sphinx; make html)
+	which sphinx-build >/dev/null && (cd docs/sphinx; make html)
 
 sphinxdoc: sphinxbuild
 	python -m webbrowser "./docs/sphinx/_build/html/index.html"

docs/sphinx/conf.py

@@ -63,7 +63,7 @@
 
 # The full version, including alpha/beta/rc tags.
 try:
-  release = version + ' git=' + subprocess.check_output(["git", "describe", "--always"])
+  release = version + ' git=' + subprocess.check_output(["git", "describe", "--always"]).strip()
 except subprocess.CalledProcessError:
   release = version + ' gitless'
 
@@ -117,7 +117,7 @@
 #html_theme_options = {}
 
 # Add any paths that contain custom themes here, relative to this directory.
-#html_theme_path = []
+html_theme_path = [ '_themes/bootstrap' ]
 
 # The name for this set of Sphinx documents.  If None, it defaults to
 # "<project> v<release> documentation".

docs/sphinx/spec/index.rst

@@ -391,25 +391,9 @@ Non-ground terms
 Types
 =====
 
-Type declarations
------------------
-
-.. todo:: old design at http://www.dyna.org/wiki/index.php?title=Term#Union_types
-
-Typed variables
----------------
-
-Co-inductive types
-------------------
-
-.. todo:: how do we deal with types for varargs and keyword args?
-
-Possible future extensions
---------------------------
-Guarded types?  Nonlinear types?  Parametric types?
+.. todo::
 
-Type coercion
-=============
+   Discussion moved to :doc:`/spec/type-system`
 
 
 Unification

docs/sphinx/spec/type-system.rst

@@ -0,0 +1,104 @@
+.. -*- compile-command: "make -C .. html" -*-
+.. Type system specification
+
+.. todo:: This really is just an outline.
+
+
+####################
+  Dyna Type System
+####################
+
+Dyna uses a ``set-theoretic`` type system: abstractly, a type is simply a
+set of ground terms and all operations of the type system are defined in
+terms of operations on sets.  In practice, our system may be instantiated
+with any *computable description* of sets closed under the requisite
+operations.
+
+Type Roles
+----------
+
+In a pure Dyna (one without foreign primops) we could say that *every* term
+is an item and that every query is therefore supported, but might fail.
+However, efficient use of foreign primops forces us to constrain the
+system's actions: some primops are only capable of working with certain
+terms (e.g. ``sqrt`` only knows how to operate on numbers, not strings).
+
+Type checking
+-------------
+
+Type checking enforces that every term construction and evaluation obeys any
+type restrictions (though it does not guarantee executability of a rule --
+that falls to the mode system).  That is, we assume that we have an *upper
+bounds* on the types of terms and items available in the program, and we
+would like to ensure that every rule's implied upper bound is non-empty.
+This upper-bound is computed by simply intersecting upper-bounds of each
+construction and evaluation in a rule.
+
+However, in addition, our type checking algorithm imposes constraints in an
+effort to catch situations which are likely to be unintentional errors.  We
+try to model an intuitive understanding of information flow, akin to those
+in more traditional programming langues, even though our system can execute
+things "out of order."  In this intuitive model (which is not necessarily
+indicitative of the evaluation order planned by the compiler), information
+flows between sub-expressions in a left-to-right, innermost-out order: in
+``f(X), g(X)``, the ``f`` subgoal grounds ``X`` (if it is not already) and
+``g`` must be prepared to handle that ground form; the same is true in
+``h(f(X),g(X))``.
+
+More formally, when a rule is de-sugared, we preserve the left-to-right DFS
+order of sub-expressions.  Any type annotations in the head of the rule also
+become sub-expressions and are placed at the front of this order.  Starting
+from the assumption that all variables range over all terms, the type
+checker then traverses sub-expressions in order, intersecting the current
+context with the term and, if evaluated, item types for the subgoal under
+consideration.  Only variables *first-mentioned* in this subgoal are
+permitted to have a narrower type after intersection; if this check fails,
+type checking aborts.  If ever the type context implies an empty set of
+results, type checking aborts.
+
+Type declarations
+-----------------
+
+.. todo:: old design at http://www.dyna.org/wiki/index.php?title=Term#Union_types
+
+Typed variables
+---------------
+
+Type inference
+--------------
+
+The other source of constraints on types comes from an inference pass, which
+attempts to fill in declarations not given.
+
+Our inference algorithm, like the type checking algorithm, is set-theoretic
+and therefore parameterized by a representation of sets.  Inference is
+further parametric in a union-semilattice of types, which we will call
+"natural" types.  The set of "natural" types is likely to include types like
+
+* Numeric families, like ``:int`` and ``:float``, and other primitive
+  families like ``:string``.
+
+* The Herbrand universe of Dyna functors over natural types, each as an
+  element of the lattice.
+
+* The set of all ground terms.
+
+Type inference proceeds inflationarily, beginning with the assumption that
+*only* pre-declared (including primitive) types exist.  It then runs a
+variant of type-checking...
+
+.. todo:: 
+
+Co-inductive types
+------------------
+
+.. todo:: how do we deal with types for varargs and keyword args?
+
+Possible future extensions
+--------------------------
+Guarded types?  Nonlinear types?  Parametric types?
+
+Type coercion
+=============
+
+

dyna.cabal

@@ -106,13 +106,13 @@ Executable dyna
                         charset >=0.3,
                         containers >=0.4,
                         either >= 3.4,
-                        haskeline >=0.6,
                         ghc-prim,
                         HUnit >=1.2,
                         mtl >=2.1,
                         lens >=4,
                         -- logict >=0.6,
                         parsers >=0.8.3,
+                        prelude-extras >=0.3,
                         process >=1.1,
                         recursion-schemes >=3.0,
                         reducers >=3.0,
@@ -148,6 +148,7 @@ Test-suite dyna-selftests
                         lens >=4,
                         -- logict >=0.6,
                         parsers >=0.8.3,
+                        prelude-extras >=0.3,
                         process >=1.1,
                         QuickCheck >= 2.5,
                         recursion-schemes >=3.0,

src/Dyna/Analysis/Mode/Execution/NamedInst.hs

@@ -45,14 +45,14 @@ import           Control.Monad.State
 import qualified Data.Foldable                     as F
 import qualified Data.Map                          as M
 import qualified Data.Traversable                  as T
-import           Dyna.Analysis.Automata.Class
-import           Dyna.Analysis.Automata.NamedAut
-import           Dyna.Analysis.Automata.Utilities
 import           Dyna.Analysis.Mode.Inst
 import qualified Dyna.Analysis.Mode.InstPretty     as IP
 import           Dyna.Analysis.Mode.Mode
 import           Dyna.Analysis.Mode.Unification
 import           Dyna.Analysis.Mode.Uniq
+import           Dyna.XXX.Automata.Class
+import           Dyna.XXX.Automata.NamedAut
+import           Dyna.XXX.Automata.Utilities
 import           Text.PrettyPrint.Free
 
 ------------------------------------------------------------------------}}}

src/Dyna/Analysis/Mode/Inst.hs

@@ -45,6 +45,7 @@ import qualified Data.Maybe               as MA
 import           Dyna.Analysis.Mode.Uniq
 import           Dyna.XXX.DataUtils       as XDU
 import           Dyna.XXX.MonadUtils
+import qualified Prelude.Extras           as PE
 
 -- import qualified Debug.Trace                       as XT
 
@@ -154,6 +155,11 @@ $(makeLensesFor [("_inst_uniq","inst_uniq")
                 ''InstF)
 -- Note that makeLensesFor creates INLINE pragmas for its lenses, too. :)
 
+instance (Eq f) => PE.Eq1 (InstF f)
+-- | For the automata library's consumption; for reasoning, use lattice
+-- functions.
+instance (Ord f) => PE.Ord1 (InstF f)
+
 -- | Traverse all of the recursion points @a@, rather than the @M.Map f [a]@
 -- structure itself.  This provides a more robust interface to term
 -- recursion, but of course loses information about disjunctions.

src/Dyna/Analysis/Mode/Selftest/NamedInst.hs

@@ -23,8 +23,8 @@ import qualified Data.Map                  as M
 import qualified Data.Maybe                as MA
 import qualified Data.Set                  as S
 import qualified Data.Traversable          as T
-import           Dyna.Analysis.Automata.Class
-import           Dyna.Analysis.Automata.Utilities
+import           Dyna.XXX.Automata.Class
+import           Dyna.XXX.Automata.Utilities
 import           Dyna.Analysis.Mode.Execution.NamedInst
 import           Dyna.Analysis.Mode.Inst
 import           Dyna.Analysis.Mode.Selftest.Term

src/Dyna/Analysis/Mode/Selftest/Term.hs

@@ -18,11 +18,11 @@ import qualified Data.List                 as L
 import qualified Data.Map                  as M
 import qualified Data.Maybe                as MA
 import qualified Data.Set                  as S
-import           Dyna.Analysis.Automata.Class
-import           Dyna.Analysis.Automata.Utilities
 import           Dyna.Analysis.Mode.Inst
 import           Dyna.Analysis.Mode.Uniq
 import           Dyna.Analysis.Mode.Execution.NamedInst
+import           Dyna.XXX.Automata.Class
+import           Dyna.XXX.Automata.Utilities
 import           Test.QuickCheck
 import           Test.SmallCheck           as SC
 import           Test.SmallCheck.Series    as SCS

src/Dyna/Backend/Python/utils.py

@@ -261,9 +261,17 @@ def span_to_src(span, src=None):
     Utility for retrieving source code for Parsec error message (there is
     nothing specific about rules)
     """
-
-    [(filename, bl, bc, el, ec)] = re.findall(r'(.*):(\d+):(\d+)-\1:(\d+):(\d+)', span)
-
+
+    # look for intervals like `filename:3:1-filename:3:6`
+    lines = re.findall(r'(.*):(\d+):(\d+)-\1:(\d+):(\d+)', span)
+    if lines:
+        [(filename, bl, bc, el, ec)] = lines
+    else:
+        # look for point-like errors as in `filename:3:1`
+        [(filename, bl, bc)] = re.findall(r'(.*):(\d+):(\d+)', span)
+        el = bl
+        ec = bc
+
     (bl, bc, el, ec) = map(int, [bl, bc, el, ec])
 
     if not src: