From 9bde0f01fcfe9ae1b3d7a5bc5ebb0d8fc29acb25 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Sat, 1 Mar 2014 21:19:03 -0500 Subject: [PATCH] Move automata library --- dyna.cabal | 2 + src/Dyna/Analysis/Mode/Execution/NamedInst.hs | 6 +-- src/Dyna/Analysis/Mode/Inst.hs | 6 +++ src/Dyna/Analysis/Mode/Selftest/NamedInst.hs | 4 +- src/Dyna/Analysis/Mode/Selftest/Term.hs | 4 +- src/Dyna/{Analysis => XXX}/Automata/Class.hs | 38 +++++++++++++++---- src/Dyna/XXX/Automata/Examples.hs | 9 +++++ .../{Analysis => XXX}/Automata/NamedAut.hs | 30 ++++++++++----- .../{Analysis => XXX}/Automata/Utilities.hs | 15 ++++++-- 9 files changed, 86 insertions(+), 28 deletions(-) rename src/Dyna/{Analysis => XXX}/Automata/Class.hs (81%) create mode 100644 src/Dyna/XXX/Automata/Examples.hs rename src/Dyna/{Analysis => XXX}/Automata/NamedAut.hs (94%) rename src/Dyna/{Analysis => XXX}/Automata/Utilities.hs (71%) diff --git a/dyna.cabal b/dyna.cabal index 721ad53..4e3235b 100644 --- a/dyna.cabal +++ b/dyna.cabal @@ -113,6 +113,7 @@ Executable dyna 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 +149,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/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/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. + ------------------------------------------------------------------------}}} -- 2.50.1