lens >=4,
-- logict >=0.6,
parsers >=0.8.3,
+ prelude-extras >=0.3,
process >=1.1,
recursion-schemes >=3.0,
reducers >=3.0,
lens >=4,
-- logict >=0.6,
parsers >=0.8.3,
+ prelude-extras >=0.3,
process >=1.1,
QuickCheck >= 2.5,
recursion-schemes >=3.0,
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
------------------------------------------------------------------------}}}
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
''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.
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
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
---------------------------------------------------------------------------
-- | 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
{-# 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'.
-- 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)
-- 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)
-- 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)
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
+
+------------------------------------------------------------------------}}}
--- /dev/null
+-- | 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]
{-# 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
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))
------------------------------------------------------------------------}}}
$ 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 {{{
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)
------------------------------------------------------------------------}}}
-- 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
-- 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)
{-# 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)
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
-module Dyna.Analysis.Automata.Utilities where
+module Dyna.XXX.Automata.Utilities where
import Control.Arrow (first)
import Control.Lens
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 =
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.
+
------------------------------------------------------------------------}}}
projects / dyna2 / commitdiff