diff --git a/.gitmodules b/.gitmodules index a2431b8..cab8fd7 100644 --- a/.gitmodules +++ b/.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 diff --git a/Makefile b/Makefile index 7905e45..00b356c 100644 --- a/Makefile +++ b/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" diff --git a/docs/sphinx/_themes/bootstrap b/docs/sphinx/_themes/bootstrap new file mode 160000 index 0000000..71d6ae5 --- /dev/null +++ b/docs/sphinx/_themes/bootstrap @@ -0,0 +1 @@ +Subproject commit 71d6ae5999333f256e69a760a81bc844342dbd2e diff --git a/docs/sphinx/conf.py b/docs/sphinx/conf.py index 05278bb..0247cee 100644 --- a/docs/sphinx/conf.py +++ b/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 # " v documentation". diff --git a/docs/sphinx/spec/index.rst b/docs/sphinx/spec/index.rst index 6892ae4..f106425 100644 --- a/docs/sphinx/spec/index.rst +++ b/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 diff --git a/docs/sphinx/spec/type-system.rst b/docs/sphinx/spec/type-system.rst new file mode 100644 index 0000000..6c85f96 --- /dev/null +++ b/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 +============= + + diff --git a/dyna.cabal b/dyna.cabal index 721ad53..aec6a05 100644 --- a/dyna.cabal +++ b/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, diff --git a/misc/dyna-doctest.py b/misc/dyna-doctest.py old mode 100644 new mode 100755 diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs index 189d9d4..aeaef4e 100644 --- a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs +++ b/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 ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index eb33a0e..129f9d5 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/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. diff --git a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs index bcf7ddf..4bf8c77 100644 --- a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs +++ b/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 diff --git a/src/Dyna/Analysis/Mode/Selftest/Term.hs b/src/Dyna/Analysis/Mode/Selftest/Term.hs index ac3700f..f0e3f24 100644 --- a/src/Dyna/Analysis/Mode/Selftest/Term.hs +++ b/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 diff --git a/src/Dyna/Backend/Python/utils.py b/src/Dyna/Backend/Python/utils.py index 648b45c..0b5b2ea 100644 --- a/src/Dyna/Backend/Python/utils.py +++ b/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: diff --git a/src/Dyna/Analysis/Automata/Class.hs b/src/Dyna/XXX/Automata/Class.hs similarity index 81% rename from src/Dyna/Analysis/Automata/Class.hs rename to src/Dyna/XXX/Automata/Class.hs index fffb53d..277358e 100644 --- a/src/Dyna/Analysis/Automata/Class.hs +++ b/src/Dyna/XXX/Automata/Class.hs @@ -1,6 +1,12 @@ --------------------------------------------------------------------------- -- | Self-contained, recursive automata, parametric in ply functor. -- +-- Automata parameterised by functor F can be expected to behave as maps +-- from labels to F-structure over labels. That is, they are labeled +-- descriptions of fixed points of F. This interface hides the actual +-- labeling strategy in use inside an automaton from the user of the +-- representation. +-- -- Note that particular automata implementations (instances) may have an API -- that goes (well) beyond what's available here. In particular, it is -- expected that non-trivial construction is beyond the scope of this common @@ -12,22 +18,27 @@ {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wall #-} -module Dyna.Analysis.Automata.Class where +module Dyna.XXX.Automata.Class where import qualified Data.Traversable as T +import qualified Prelude.Extras as PE ------------------------------------------------------------------------}}} -- Utility type definitions {{{ -- | An alias for universal quantification forcing a non-recursive ply of @f@: --- since there is no defined data of fully polymorphic type, any recursive --- positions in @f@ must not contain data. +-- since there is no defined data of fully polymorphic type, this rules out +-- the use of recursive branches of @f@ (except with 'undefined'). type NonRec f = forall x . f x ------------------------------------------------------------------------}}} -- Basic class definition {{{ -class Automata (a :: (* -> *) -> *) where +-- | The class of a representations of an automata. The functions here are +-- not the user-friendly operations like @intersect@ and @union@ but are +-- rather designed to provide a reasonably abstract view of the internals of +-- any backing store for automata. +class AutomataRepr (a :: (* -> *) -> *) where -- Construction -- | An inverse (up to isomorphism) to 'autExpose'. @@ -112,7 +123,7 @@ class Automata (a :: (* -> *) -> *) where -- states, while the others allow the merge to remain at a leaf state in -- one automata while descending the other. autBiReduce :: forall f r . - (Ord (f ())) + (PE.Ord1 f) => r -> (forall x y m . (Monad m) @@ -128,7 +139,7 @@ class Automata (a :: (* -> *) -> *) where -- as part of the index -- that is, a given pair of states may be -- given to the callback repeatedly at differing @c@ values. autMerge :: forall c f . - (Ord c, Ord (f ())) + (Ord c, PE.Ord1 f) => (forall x y . f x -> f y -> c) -> (forall x y z m . (Monad m) @@ -144,7 +155,7 @@ class Automata (a :: (* -> *) -> *) where -- Note that the callbacks are total (monadic) functions: failure is -- handled internally to @m@ and may short-circuit. autPMerge :: forall c e f . - (Ord c, Ord (f ())) + (Ord c, PE.Ord1 f) => (forall x y . f x -> f y -> c) -> (forall x y z m . (Monad m) @@ -163,3 +174,16 @@ class AutMinimize a where autMinimize :: (T.Traversable f, Ord (f Int)) => a f -> a f ------------------------------------------------------------------------}}} +-- Functor recursor class definition {{{ + +-- XXX Future Work. +-- +-- Sometimes, there's really only one set of operations we'd like to support +-- on the structure @f@. In that case, we can specify the recursors all at +-- once and have a simpler library of operations which use the appropriate +-- recursor. This simpler library will have things like 'union', +-- 'intersection', 'isEmpty', 'isUniversal', etc. + +-- class AutStruct (f :: * -> *) where + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/XXX/Automata/Examples.hs b/src/Dyna/XXX/Automata/Examples.hs new file mode 100644 index 0000000..fef59da --- /dev/null +++ b/src/Dyna/XXX/Automata/Examples.hs @@ -0,0 +1,9 @@ +-- | Deterministic string automata: each (state, symbol) pair transitions +-- uniquely to a new state. +data DFAF alphabet state = M.Map alphabet state + +-- | An example for describing non-deterministic string automata: each +-- (state,symbol) pair transitions to a set of possible successor states. +-- This formulation does not allow for \epsilon edges but requires that we +-- compute epsilon closure of the transition relation. +data NFAF alphabet state = M.Map alphabet [state] diff --git a/src/Dyna/Analysis/Automata/NamedAut.hs b/src/Dyna/XXX/Automata/NamedAut.hs similarity index 94% rename from src/Dyna/Analysis/Automata/NamedAut.hs rename to src/Dyna/XXX/Automata/NamedAut.hs index f7147e1..0fef9a1 100644 --- a/src/Dyna/Analysis/Automata/NamedAut.hs +++ b/src/Dyna/XXX/Automata/NamedAut.hs @@ -14,7 +14,7 @@ {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wall #-} -module Dyna.Analysis.Automata.NamedAut(NA(NA), naUnfold, naFromMap) where +module Dyna.XXX.Automata.NamedAut(NA(NA), naUnfold, naFromMap) where import Control.Applicative import Control.Lens @@ -26,13 +26,16 @@ 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.XXX.Automata.Class import Dyna.XXX.DataUtils (mapInOrCons) import Dyna.XXX.MonadUtils (incState, tryMapCache, trySetCache) +import qualified Prelude.Extras as PE ------------------------------------------------------------------------}}} -- Definition {{{ +-- | A single-accepting-state automaton representation, using an existential +-- for state labels. data NA f = forall a . (Ord a) => NA a (M.Map a (f a)) ------------------------------------------------------------------------}}} @@ -74,10 +77,17 @@ naExposeAll (NA a0 m0) = let labels = naRelabel_ m0 $ M.mapKeysWith (error "NA relabel collision") relabel m0) +newtype DC f = DC (f ()) +instance (PE.Eq1 f) => Eq (DC f) where + (DC l) == (DC r) = l PE.==# r +instance (PE.Ord1 f) => Ord (DC f) where + (DC l) `compare` (DC r) = l `PE.compare1` r --- | Downcast away a forall. -dc :: NonRec f -> f () -dc i = i +-- | Downcast away a forall. The instances above convert our 'PE.Ord1' +-- requirements into the traditional 'Ord' and 'Eq' for 'f ()'. This serves +-- to hide the use of '()' from the consumer code. +dc :: NonRec f -> DC f +dc i = DC i ------------------------------------------------------------------------}}} -- Unfolder {{{ @@ -174,8 +184,8 @@ naFromAut = autReduceIx cyc rec data NBinState f c a b = NBS { _nbs_next :: Int , _nbs_ctx :: M.Map Int (f Int) , _nbs_cache_symm :: M.Map (c,a ,b ) Int - , _nbs_cache_lsml :: M.Map (c,a ,f ()) Int - , _nbs_cache_lsmr :: M.Map (c,f (),b ) Int + , _nbs_cache_lsml :: M.Map (c,a ,DC f) Int + , _nbs_cache_lsmr :: M.Map (c,DC f,b ) Int } $(makeLenses ''NBinState) type NBSC m f c a b = (Monad m, MonadState (NBinState f c a b) m) @@ -198,7 +208,7 @@ $(makeLenses ''MinSplitState) ------------------------------------------------------------------------}}} -- Automata instance {{{ -instance Automata NA where +instance AutomataRepr NA where autHide i0 = flip evalState (0::Int, M.empty) $ do i0' <- T.traverse go i0 ra <- nxt @@ -271,7 +281,7 @@ instance Automata NA where -- While unusual, we need this instance type declaration to introduce -- scoped type variables for us to hold on to down below. Oy! autMerge :: forall c f . - (Ord c, Ord (f ())) + (Ord c, PE.Ord1 f) => (forall x y . f x -> f y -> c) -> (forall x y z m . (Monad m) @@ -324,7 +334,7 @@ instance Automata NA where {-# INLINABLE autMerge #-} autPMerge :: forall c e f . - (Ord c, Ord (f ())) + (Ord c, PE.Ord1 f) => (forall x y . f x -> f y -> c) -> (forall x y z m . (Monad m) diff --git a/src/Dyna/Analysis/Automata/Utilities.hs b/src/Dyna/XXX/Automata/Utilities.hs similarity index 71% rename from src/Dyna/Analysis/Automata/Utilities.hs rename to src/Dyna/XXX/Automata/Utilities.hs index 28a93b3..4713995 100644 --- a/src/Dyna/Analysis/Automata/Utilities.hs +++ b/src/Dyna/XXX/Automata/Utilities.hs @@ -6,7 +6,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -module Dyna.Analysis.Automata.Utilities where +module Dyna.XXX.Automata.Utilities where import Control.Arrow (first) import Control.Lens @@ -15,15 +15,18 @@ import qualified Data.Foldable as F import qualified Data.Traversable as T import qualified Data.Map as M import qualified Data.Maybe as MA -import Dyna.Analysis.Automata.Class -import Dyna.Analysis.Automata.NamedAut +import Dyna.XXX.Automata.Class +import Dyna.XXX.Automata.NamedAut import Dyna.XXX.PPrint import Text.PrettyPrint.Free ------------------------------------------------------------------------}}} -- Pretty Printing {{{ -autRender :: (T.Traversable f, Automata a) +-- | Given a ply-by-ply rendering function, render an automaton. The +-- callback should not inspect or manipulate the @Doc e@ in a ply in order +-- to be a faithful printout of the automaton. +autRender :: (T.Traversable f, AutomataRepr a) => (f (Doc e) -> Doc e) -> a f -> Doc e autRender f a = @@ -38,4 +41,8 @@ autRender f a = pan = angles . pretty defrow (k,v) = pan k <+> equals <+> v +-- XXX Maybe we should consider a version which does not reveal state labels +-- for non-recursive terms. "<0> where <0> = U@sh" is a lot more verbose +-- than "U@sh", even if more standardized. + ------------------------------------------------------------------------}}}