--- /dev/null
+---------------------------------------------------------------------------
+-- | Self-contained, recursive automata, parametric in ply functor.
+--
+-- 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
+-- API.
+
+-- Header material {{{
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Automata.Class where
+
+import qualified Data.Traversable as T
+
+------------------------------------------------------------------------}}}
+-- 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.
+type NonRec f = forall x . f x
+
+------------------------------------------------------------------------}}}
+-- Basic class definition {{{
+
+class Automata (a :: (* -> *) -> *) where
+ -- Construction
+
+ -- | An inverse (up to isomorphism) to 'autExpose'.
+ --
+ -- Note that this may not be efficient, so it should be used only as a
+ -- last resort.
+ autHide :: (T.Traversable f) => f (a f) -> a f
+
+ -- | This is most frequently used as a base case in a lopsided
+ -- inductive step, in which one side is known to be acyclic, but the other
+ -- may be cyclic. When we have reached the leaves of the former,
+ -- 'autShallow' will yield a trivial automata which may then be passed to
+ -- a binary automata function (e.g. 'autCmp') which will deal with cycles.
+ --
+ -- Parametricity ensures that this function has no access to any but the
+ -- top ply of its argument.
+ autShallow :: (T.Traversable f) => f x -> Maybe (a f)
+
+ -- Destruction
+
+ -- | Reveal the topmost ply of this automata.
+ --
+ -- Note that recursive use of this function may well diverge!
+ autExpose :: (Functor f) => a f -> f (a f)
+
+ -- Unary traversals
+
+ -- | Per-state rewriting function. Callback will be called at most once
+ -- for each state of the automata, and at least once for all reachable
+ -- states, but there may be equivalent states within as well (but see
+ -- 'autMinimize'). The callback has visibility into the states reachable
+ -- from the current position within the automata, but no cycle-breaking is
+ -- performed by the machinery, so careless use of this ability may
+ -- diverge; an 'Ord' instance is asserted for the recursion sites to help
+ -- mitigate this situation.
+ autAtEachState :: forall f .
+ (forall x . (Ord x) => (x -> f x) -> f x -> f x)
+ -> a f -> a f
+
+ -- | (Indexed) algebraic reduction of an automaton. Given a
+ -- cycle-breaking result (as a function of node identity)
+ -- and an algebraic interpretation of a single
+ -- state of the automaton (indexed, again, by node identity),
+ -- produce a result.
+ --
+ -- Note that cycles are only evaluated once: while a given spine is
+ -- active, all observations of that spine will yield the cycle-breaking
+ -- value; once a node is no longer on the active spine, observers will
+ -- observe its result. Results of this function are only well-defined
+ -- if the callbacks are invariant to node visit order subject to this
+ -- observation constraint.
+ --
+ -- Note that one should not expect to be able to fully reconstruct the
+ -- automata given only the observations made by this function, as the
+ -- states may have meaning internal to automata (e.g. interpreted subject
+ -- to equality constraints or just as regular structure).
+ autReduceIx :: forall f r x .
+ (T.Traversable f, Enum x, Ord x)
+ => (x -> r)
+ -> (x -> f r -> r)
+ -> a f -> r
+
+ -- | Non-indexed reduction. See 'autReduceIx'.
+ --
+ -- This could be written in terms of 'autReduceIx', but this may be
+ -- more efficient by not having to map state names.
+ autReduce :: forall f r .
+ (T.Traversable f)
+ => r
+ -> (f r -> r)
+ -> a f -> r
+
+ -- Binary traversals
+ --
+ -- XXX Possibly these want to be split out to an AutBin class, enabling us
+ -- to specify more than just the diagonals in the space of automata?
+
+ -- | Binary reducer; see 'autReduce' for overview.
+ --
+ -- The HOF here is given three callbacks, for both "in-phase" and
+ -- "out-of-phase" work; the former allows simultaneous descent into two
+ -- 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 ()))
+ => r
+ -> (forall x y m .
+ (Monad m)
+ => (x -> NonRec f -> m r)
+ -> (NonRec f -> y -> m r)
+ -> (x -> y -> m r)
+ -> f x -> f y -> m r)
+ -> a f -> a f -> r
+
+ -- | Total synchronous binary merge; @c@ records the type of top-down
+ -- context information needed for what is otherwise a bottom-up operation.
+ -- Since multiple paths may reach pairs of states, @c@ is used internally
+ -- 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 ()))
+ => (forall x y . f x -> f y -> c)
+ -> (forall x y z m .
+ (Monad m)
+ => (c -> x -> NonRec f -> m z)
+ -> (c -> NonRec f -> y -> m z)
+ -> (c -> x -> y -> m z)
+ -> c -> f x -> f y -> m (f z))
+ -> a f -> a f -> a f
+
+
+ -- | Partial synchronous binary merge.
+ --
+ -- 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 ()))
+ => (forall x y . f x -> f y -> c)
+ -> (forall x y z m .
+ (Monad m)
+ => (c -> x -> NonRec f -> m z)
+ -> (c -> NonRec f -> y -> m z)
+ -> (c -> x -> y -> m z)
+ -> c -> f x -> f y -> m (Either e (f z)))
+ -> a f -> a f -> Either e (a f)
+
+------------------------------------------------------------------------}}}
+-- Minimization class definition {{{
+
+class AutMinimize a where
+
+ -- | Automata minimization.
+ autMinimize :: (T.Traversable f, Ord (f Int)) => a f -> a f
+
+------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | An implementation of our automata using existentially-quantified maps
+
+-- Header material {{{
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Automata.NamedAut(NA(NA), naUnfold, naFromMap) where
+
+import Control.Applicative
+import Control.Lens
+import Control.Monad.Identity
+import Control.Monad.Trans.Either
+import Control.Monad.State
+import qualified Data.Foldable as F
+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.DataUtils (mapInOrCons)
+import Dyna.XXX.MonadUtils (incState, tryMapCache, trySetCache)
+
+------------------------------------------------------------------------}}}
+-- Definition {{{
+
+data NA f = forall a . (Ord a) => NA a (M.Map a (f a))
+
+------------------------------------------------------------------------}}}
+-- Internal utilities {{{
+
+naImport :: (T.Traversable f, Ord k, Functor m, Monad m)
+ => m a
+ -> (a -> f a -> m ())
+ -> (k -> f k)
+ -> k
+ -> a
+ -> m ()
+naImport nxt ins look r ir = do
+ _ <- flip runStateT M.empty $ go r ir
+ return ()
+ where
+ go k a = T.traverse rec (look k) >>= lift . ins a
+ rec = tryMapCache id (\_ -> lift nxt) go
+
+naPrune :: forall f . (F.Foldable f) => NA f -> NA f
+naPrune (NA a0 m0) = (NA a0 m')
+ where
+ m' = execState (go a0) M.empty
+ go a = tryMapCache id (\_ -> return af) (\_ _ -> F.mapM_ go af) a
+ where af = MA.fromJust $ m0 ^. at a
+
+naRelabel_ :: (Ord a, Enum o)
+ => M.Map a x
+ -> M.Map a o
+naRelabel_ m = flip evalState (toEnum 0) $ T.traverse (\_ -> incState id) m
+
+-- | Convert from whatever internal representation we're using for states
+-- to Int.
+naExposeAll :: (Functor f, Enum o, Ord o) => NA f -> (o, M.Map o (f o))
+naExposeAll (NA a0 m0) = let labels = naRelabel_ m0
+ relabel a = MA.fromJust $ labels ^. at a
+ in ( relabel a0
+ , fmap (fmap relabel)
+ $ M.mapKeysWith (error "NA relabel collision")
+ relabel m0)
+
+
+-- | Downcast away a forall.
+dc :: NonRec f -> f ()
+dc i = i
+
+------------------------------------------------------------------------}}}
+-- Unfolder {{{
+
+-- | Build an automata over the functor @f@ by unfolding. @r@ carries
+-- top-down information flow, while the user-specified 'Monad' @m@ may carry
+-- sideways state (that is, information dependent upon the unfolding order).
+-- @ix@ provides the internal label for the state being unfolded so that it
+-- may be referenced later (/e.g./ by first being stored in @m@ or @r@).
+--
+-- As a convenience, the unfolder is allowed to supply an entire (isolated)
+-- automata in liu of recursively descending.
+naUnfold :: forall f ix m r .
+ (Enum ix, Ord ix, Functor m, Monad m, Traversable f)
+ => (forall t . (MonadTrans t, Monad (t m))
+ => r -> ix -> t m (Either (NA f) (f (Either ix r))))
+ -> r -> m (NA f)
+naUnfold uf = liftM (\(r,(_,m)) -> NA r m)
+ . flip runStateT (toEnum 0,M.empty) . visit
+ where
+ visit r = do
+ i <- nxt
+ f <- uf r i
+ case f of
+ Right f' -> do
+ f'' <- T.mapM (either return visit) f'
+ ins i f''
+ Left (NA r' m') -> naImport nxt ins (MA.fromJust . (m' ^.) . at) r' i
+ return i
+
+ nxt = incState _1
+ ins k v = _2 . at k .= Just v
+{-# INLINABLE naUnfold #-}
+
+{-
+-- | Build an automata over the functor @f@ by unfolding. @t@ carries
+-- top-down information flow while @s@ carries sideways state (that is,
+-- information dependent upon the unfolding order). @ix@ provides the
+-- internal label for the state being unfolded.
+--
+-- One might use @s@ to carry a (partial) map from @t@ to @ix@ values,
+-- either for tying cyclic knots or to avoid re-unfolding structure. It may
+-- also be safe to ignore (just pass '()').
+naUnfold :: forall f ix m s t .
+ (Enum ix, Ord ix, Traversable f) =>
+ (t -> ix -> s -> (f (Either ix t), s)) -- ^ Unfolder step
+ -> t -- ^ Initial root
+ -> s -- ^ Initial flow state
+ -> NA f
+naUnfold uf t0 s0 = (\(r,(_,m,_)) -> NA r m)
+ $ flip runState (toEnum 0, M.empty, s0)
+ $ visit t0
+ where
+ visit t = do
+ i <- incState _1
+ (f,s') <- uses _3 (uf t i)
+ _3 .= s'
+ f' <- T.mapM (either return visit) f
+ _2 . at i .= Just f'
+ return i
+-}
+
+naFromMap :: forall f oix .
+ (T.Traversable f, Ord oix)
+ => M.Map oix (f oix) -> oix -> NA f
+naFromMap m0 a0 = flip evalState (M.empty :: M.Map oix Int) (naUnfold u a0)
+ where
+ u :: forall t m . (MonadTrans t, Monad (t m), MonadState (M.Map oix Int) m)
+ => oix -> Int -> t m (Either (NA f) (f (Either Int oix)))
+ u oix iix = do
+ lift (at oix .= Just iix)
+ liftM Right $ T.mapM relabel $ MA.fromJust (m0 ^. at oix)
+
+ relabel oix = lift (use (at oix)) >>= return . maybe (Right oix) (Left)
+{-# INLINABLE naFromMap #-}
+
+{-
+naFromAut :: forall a f x .
+ (Automata a, T.Traversable f, Enum x, Ord x)
+ => a f -> (x, M.Map x (f x))
+naFromAut = autReduceIx cyc rec
+ where
+ cyc x = (x,M.empty)
+ rec x fr = (x, M.insert x frx $ M.unions frms)
+ where
+ frx = fmap fst fr
+ frms = F.toList $ fmap snd fr
+{-# INLINABLE naFromAut #-}
+-}
+
+------------------------------------------------------------------------}}}
+-- Internal data types {{{
+
+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
+ }
+$(makeLenses ''NBinState)
+type NBSC m f c a b = (Monad m, MonadState (NBinState f c a b) m)
+
+iNBS :: forall (f :: * -> *) c a b. NBinState f c a b
+iNBS = NBS 0 M.empty M.empty M.empty M.empty
+
+data MinState a c = MS
+ { _ms_classes :: M.Map c [a]
+ , _ms_clinv :: M.Map a c
+ }
+ deriving (Show)
+$(makeLenses ''MinState)
+
+data MinSplitState f a c = MSS
+ { _mss_newcl :: M.Map (f c) [a] }
+ deriving (Show)
+$(makeLenses ''MinSplitState)
+
+------------------------------------------------------------------------}}}
+-- Automata instance {{{
+
+instance Automata NA where
+ autHide i0 = flip evalState (0::Int, M.empty) $ do
+ i0' <- T.traverse go i0
+ ra <- nxt
+ ins ra i0'
+ rm <- use _2
+ return (NA ra rm)
+ where
+ nxt = incState _1
+ ins k v = _2 . at k .= Just v
+
+ go (NA i' m') = do
+ i <- nxt
+ naImport nxt ins (MA.fromJust . (m' ^.) . at) i' i
+ return i
+
+ autShallow f = do
+ f' <- T.mapM (const mzero) f
+ return (NA () (M.fromList [((),f')]))
+ {-# INLINABLE autShallow #-}
+
+ autExpose (NA a0 m) = fmap (\a -> NA a m) $ MA.fromJust $ m ^. at a0
+ {-# INLINABLE autExpose #-}
+
+ autAtEachState q (NA a0 m0) = NA a0 (M.map q' m0)
+ where
+ q' = q (MA.fromJust . (m0 ^.) . at)
+ {-# INLINABLE autAtEachState #-}
+
+ autReduce cyc red (NA a0 m0) = evalState (q a0) M.empty
+ where
+ q a = do
+ _ <- tryMapCache id (\_ -> return cyc) miss a
+ liftM MA.fromJust $ use (at a)
+
+ miss a _ = do
+ fr <- T.mapM q (MA.fromJust $ m0 ^. at a)
+ let r = red fr
+ at a .= Just r
+ {-# INLINABLE autReduce #-}
+
+ autReduceIx cyc red (naExposeAll -> (a0,m0)) = evalState (q a0) M.empty
+ where
+ q a = do
+ _ <- tryMapCache id (return . cyc) miss a
+ liftM MA.fromJust $ use (at a)
+
+ miss a _ = do
+ fr <- T.mapM q (MA.fromJust $ m0 ^. at a)
+ let r = red a fr
+ at a .= Just r
+ {-# INLINABLE autReduceIx #-}
+
+ autBiReduce c q (NA la0 lm) (NA ra0 rm) =
+ evalState (qip la0 ra0) (S.empty, S.empty, S.empty)
+ where
+ qip l r = flip (trySetCache _1 c) (l,r) $ \_ -> do
+ let lf = MA.fromJust $ lm ^. at l
+ let rf = MA.fromJust $ rm ^. at r
+ q qopl qopr qip lf rf
+
+ qopl l r = flip (trySetCache _2 c) (l, dc r) $ \_ -> do
+ let lf = MA.fromJust $ lm ^. at l
+ q qopl qopr qip lf r
+
+ qopr l r = flip (trySetCache _3 c) (dc l, r) $ \_ -> do
+ let rf = MA.fromJust $ rm ^. at r
+ q qopl qopr qip l rf
+ {-# INLINABLE autBiReduce #-}
+
+ -- 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 ()))
+ => (forall x y . f x -> f y -> c)
+ -> (forall x y z m .
+ (Monad m)
+ => (c -> x -> NonRec f -> m z)
+ -> (c -> NonRec f -> y -> m z)
+ -> (c -> x -> y -> m z)
+ -> c -> f x -> f y -> m (f z))
+ -> NA f -> NA f -> NA f
+ autMerge ci f (NA (la0 :: la) lm) (NA (ra0 :: ra) rm) = evalState tlq iNBS
+ where
+ f' :: NBSC m f c la ra => c -> f la -> f ra -> m (f Int)
+ f' = f lsml lsmr merge
+
+ tlq = do
+ let lf :: f la = MA.fromJust $ lm ^. at la0
+ let rf :: f ra = MA.fromJust $ rm ^. at ra0
+ let ic = ci lf rf
+ ma <- merge ic la0 ra0
+ mm <- use nbs_ctx
+ return (NA ma mm)
+
+ -- These two are here so that the skolems remain local to this
+ -- defintion. It's a bit of a shame that the type system is
+ -- not willing to let these exist at higher scope.
+ nxt :: NBSC m f c la ra => m Int
+ nxt = incState nbs_next
+ ins k v = nbs_ctx . at k .= Just v
+
+ merge :: NBSC m f c la ra => c -> la -> ra -> m Int
+ merge c l r =
+ flip (tryMapCache nbs_cache_symm (\_ -> nxt)) (c,l,r) $ \_ a -> do
+ let lf = MA.fromJust $ lm ^. at l
+ let rf = MA.fromJust $ rm ^. at r
+ v <- f' c lf rf
+ ins a v
+
+ lsml :: NBSC m f c la ra => c -> la -> NonRec f -> m Int
+ lsml c l r =
+ flip (tryMapCache nbs_cache_lsml (\_ -> nxt)) (c,l,dc r) $ \_ a -> do
+ let lf = MA.fromJust $ lm ^. at l
+ v <- f' c lf r
+ ins a v
+
+ lsmr :: NBSC m f c la ra => c -> NonRec f -> ra -> m Int
+ lsmr c l r =
+ flip (tryMapCache nbs_cache_lsmr (\_ -> nxt)) (c,dc l,r) $ \_ a -> do
+ let rf = MA.fromJust $ rm ^. at r
+ v <- f' c l rf
+ ins a v
+ {-# INLINABLE autMerge #-}
+
+ autPMerge :: forall c e f .
+ (Ord c, Ord (f ()))
+ => (forall x y . f x -> f y -> c)
+ -> (forall x y z m .
+ (Monad m)
+ => (c -> x -> NonRec f -> m z)
+ -> (c -> NonRec f -> y -> m z)
+ -> (c -> x -> y -> m z)
+ -> c -> f x -> f y -> m (Either e (f z)))
+ -> NA f -> NA f -> Either e (NA f)
+ autPMerge ci f (NA (la0 :: la) lm) (NA (ra0 :: ra) rm) =
+ evalState (runEitherT tlq) iNBS
+ where
+ f' :: NBSC m f c la ra
+ => c -> f la -> f ra -> EitherT e m (Either e (f Int))
+ f' = f lsml lsmr merge
+
+ tlq = do
+ let lf :: f la = MA.fromJust $ lm ^. at la0
+ let rf :: f ra = MA.fromJust $ rm ^. at ra0
+ let ic = ci lf rf
+ ma <- merge ic la0 ra0
+ mm <- use nbs_ctx
+ return (NA ma mm)
+
+ -- These two are here so that the skolems remain local to this
+ -- defintion. It's a bit of a shame that the type system is
+ -- not willing to let these exist at higher scope.
+ nxt :: NBSC m f c la ra => m Int
+ nxt = incState nbs_next
+ ins k v = nbs_ctx . at k .= Just v
+
+ merge :: NBSC m f c la ra => c -> la -> ra -> EitherT e m Int
+ merge c l r =
+ flip (tryMapCache nbs_cache_symm (\_ -> nxt)) (c,l,r) $ \_ a -> do
+ let lf = MA.fromJust $ lm ^. at l
+ let rf = MA.fromJust $ rm ^. at r
+ m <- f' c lf rf
+ v <- hoistEither m
+ ins a v
+
+ lsml :: NBSC m f c la ra => c -> la -> NonRec f -> EitherT e m Int
+ lsml c l r =
+ flip (tryMapCache nbs_cache_lsml (\_ -> nxt)) (c,l,dc r) $ \_ a -> do
+ let lf = MA.fromJust $ lm ^. at l
+ m <- f' c lf r
+ v <- hoistEither m
+ ins a v
+
+ lsmr :: NBSC m f c la ra => c -> NonRec f -> ra -> EitherT e m Int
+ lsmr c l r =
+ flip (tryMapCache nbs_cache_lsmr (\_ -> nxt)) (c,dc l,r) $ \_ a -> do
+ let rf = MA.fromJust $ rm ^. at r
+ m <- f' c l rf
+ v <- hoistEither m
+ ins a v
+ {-# INLINABLE autPMerge #-}
+
+------------------------------------------------------------------------}}}
+-- AutMinimize instance {{{
+
+instance AutMinimize NA where
+
+ autMinimize (naPrune -> NA a0 m0) =
+ let ms = classifyUntil m0 (MS M.empty M.empty)
+ (mkClasses [M.keys m0])
+
+ msci = ms ^. ms_clinv
+
+ defn = \(a:_) -> fmap (\a' -> MA.fromJust $ msci ^. at a')
+ $ MA.fromJust $ m0 ^. at a
+ in NA ((MA.fromJust $ msci ^. at a0) :: Int)
+ (fmap defn $ ms ^. ms_classes)
+
+ where
+
+ -- Attempt to partition a class in the equivalence relationship. Evaluate
+ -- each contained state to see if they have become distinguished.
+ splitClasses :: forall f a c . (Ord c, Ord a, Traversable f, Ord (f c))
+ => M.Map a (f a)
+ -> MinState a c
+ -> [[a]]
+ splitClasses im ms =
+ concat $ flip map (M.keys $ ms ^. ms_classes)
+ $ \c -> (M.elems . _mss_newcl) $ flip execState (MSS M.empty)
+ $ forM_ (MA.fromJust $ (ms ^. ms_classes) ^. at c)
+ $ \a -> do
+ -- Look up the definition of this state in the original automata
+ -- so that we can sort it into mss_newcl appropriately
+ let ia :: f c
+ = runIdentity
+ $ traverse (pure . MA.fromJust . ((ms ^. ms_clinv) ^.) . at)
+ $ (MA.fromJust $ im ^. at a :: f a)
+ mss_newcl %= mapInOrCons ia a
+
+ mkClasses :: (Ord a, Enum c, Ord c) => [[a]] -> MinState a c
+ mkClasses = uncurry MS . go (toEnum 0) M.empty M.empty
+ where
+ go _ mc mi [] = (mc,mi)
+ go c mc mi ([]:xs) = c `seq` go (succ c) mc mi xs
+ go c mc mi ((a:as):xs) = go c (mapInOrCons c a mc) (M.insert a c mi) (as:xs)
+
+ classifyUntil :: forall a c f . (Ord a, Enum c, Ord c, Traversable f, Ord (f c))
+ => M.Map a (f a) -> MinState a c -> MinState a c -> MinState a c
+ classifyUntil im p p' =
+ if M.size (p ^. ms_classes) == M.size (p' ^. ms_classes)
+ then p'
+ else classifyUntil im p' (mkClasses $ splitClasses im p')
+
+------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | Utilities for automata library
+
+-- Header material {{{
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Dyna.Analysis.Automata.Utilities where
+
+import Control.Arrow (first)
+import Control.Lens
+import Control.Monad.State
+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.PPrint
+import Text.PrettyPrint.Free
+
+------------------------------------------------------------------------}}}
+-- Pretty Printing {{{
+
+autRender :: (T.Traversable f, Automata a)
+ => (f (Doc e) -> Doc e)
+ -> a f -> Doc e
+autRender f a =
+ let (r, defs) = autReduceIx
+ (\(x :: Int) -> (pan x, M.empty))
+ (\x fr -> let r = f $ fmap fst fr
+ ms = M.unions $ F.toList $ fmap snd fr
+ in (pan x, M.insert x r ms))
+ a
+ in r <+> "where" <+> valign (map defrow $ M.toList defs)
+ where
+ pan = angles . pretty
+ defrow (k,v) = pan k <+> equals <+> v
+
+------------------------------------------------------------------------}}}
| KRKey k
deriving (Eq,Ord,Show)
-instance (PP.Pretty f, PP.Pretty n, PP.Pretty k)
+instance (Show f, PP.Pretty n, PP.Pretty k)
=> PP.Pretty (KR f n k) where
pretty (KRName n) = PP.pretty n
- pretty (KRStruct e) = IP.compactly PP.pretty (either PP.pretty PP.pretty) e
+ pretty (KRStruct e) = IP.compactly (PP.text . show)
+ (either PP.pretty PP.pretty) e
pretty (KRKey k) = PP.pretty k
type KRI f n k = InstF f (Either n k)
| VRKey k
deriving (Eq,Ord,Show)
-instance (PP.Pretty f, PP.Pretty n, PP.Pretty k)
+instance (Show f, PP.Pretty n, PP.Pretty k)
=> PP.Pretty (VR f n k) where
pretty (VRName n) = PP.pretty n
- pretty (VRStruct y) = IP.compactly PP.pretty PP.pretty y
+ pretty (VRStruct y) = IP.compactly (PP.text . show) PP.pretty y
pretty (VRKey k) = PP.pretty k
-- | Widen from a more restrictive to less restrictive recursion type.
instance MonadIO m => MonadIO (SIMCT m f) where
liftIO m = SIMCT $ lift (liftIO m)
-instance (PP.Pretty f) => PP.Pretty (SIMCtx f) where
+instance (Show f, Ord f) => PP.Pretty (SIMCtx f) where
pretty (SIMCtx _ km vm) =
PP.vcat
[ PP.text "Unaliased variables:"
| VRStruct (InstF f (VR f n))
deriving (Eq,Ord,Show)
-instance (PP.Pretty f, PP.Pretty n) => PP.Pretty (VR f n) where
+instance (Show f, PP.Pretty n) => PP.Pretty (VR f n) where
pretty (VRName n) = PP.pretty n
- pretty (VRStruct y) = IP.compactly PP.pretty PP.pretty y
+ pretty (VRStruct y) = IP.compactly (PP.text . show) PP.pretty y
{-
-- This is used during rule analysis to capture the state of the binding
instance MonadIO m => MonadIO (SIMCT m f) where
liftIO m = SIMCT $ lift (liftIO m)
-instance (PP.Pretty f) => PP.Pretty (SIMCtx f) where
+instance (Show f, Ord f) => PP.Pretty (SIMCtx f) where
pretty (SIMCtx vm) = PP.vcat
$ flip map (M.toAscList vm)
$ \(v,vr) -> PP.pretty v
expandV v = clookup v >>= \x ->
case x of
VRName n -> return n
- VRStruct y -> expandY y
+ VRStruct _ -> expandX x
VRKey k -> clookup k
- >>= either return (expandY . q2y)
+ >>= either return (expandX . VRStruct . q2y)
where
- expandY y = nDeep rec y
+ expandX x = nDeep rec x
where
- rec (VRName n) = return (Left n)
- rec (VRStruct y') = return (Right y')
- rec (VRKey k) = do
- e <- clookup k
- either (return . Left) (return . Right . q2y) e
+ rec :: (MCR m k, MCVT m k ~ ENKRI f n k, MonadTrans t, Monad (t m))
+ => VR f n k
+ -> Int
+ -> t m (Either n (InstF f (Either a1 (VR f n k))))
+ rec (VRName n) _ = return (Left n)
+ rec (VRStruct y') _ = return (Right $ fmap Right y')
+ rec (VRKey k) _ = do
+ e <- lift (clookup k)
+ return $ either Left (Right . fmap Right . q2y) e
+
------------------------------------------------------------------------}}}
-- Leq {{{
=> DVar -> m n
expandV v = clookup v >>= \x -> case x of
VRName n -> return n
- VRStruct y -> nDeep rec y
+ VRStruct _ -> nDeep rec x
where
- rec (VRName n) = return (Left n)
- rec (VRStruct y) = return (Right y)
+ rec :: (MonadTrans t, Monad (t m))
+ => VR f n
+ -> Int
+ -> t m (Either n (InstF f (Either a1 (VR f n))))
+ rec (VRName n) _ = return (Left n)
+ rec (VRStruct y') _ = return (Right $ fmap Right y')
------------------------------------------------------------------------}}}
-- Leq {{{
---------------------------------------------------------------------------
--- | Self-contained, mu-recursive inst automata
---
--- XXX This could stand a good bit of refactoring out to being generic, but
--- I am writing it quickly in hopes of checking that it works before
--- investing too much more time.
+-- | Self-contained, mu-recursive inst automata, using the generic Automata
+-- framework.
-- Header material {{{
{-# LANGUAGE FlexibleContexts #-}
module Dyna.Analysis.Mode.Execution.NamedInst (
-- * Datatype definition
- NIX(..), NIXM,
+ NIX(..),
-- * Unary functions
-- ** Well-formedness predicates
- nWellFormedUniq, nWellFormedOC,
+ nWellFormedUniq,
-- ** Inquiries
nAllNotEmpty, nSomeNotEmpty, nGround,
-- ** Construction
- nHide, nShallow, nDeep,
+ nHide, nShallow, nDeep, nFromMap,
-- ** Destruction
nExpose,
- -- ** Internals
- nPrune,
-- ** Rewrites
- nUpUniq,
+ nUpUniq, nMinimize,
+ -- ** Display
+ renderNIX,
-- * Binary comparators
- nCmp, nEq, nLeq, nSub,
+ nEq, nLeq, nSub,
-- * Total binary functions
- nTBin, nLeqGLB, nSubGLB,
+ nLeqGLB, nSubGLB,
-- * Partial binary functions
- nPBin, nLeqGLBRD, nLeqGLBRL, -- nSubLUB,
+ nLeqGLBRD, nLeqGLBRL, -- nSubLUB,
-- * Mode functions
mWellFormed,
-
- -- * XXX
- eml,
) where
-import Control.Applicative
-import qualified Control.Arrow as A
import Control.Lens
--- import Control.Monad.Identity
+import Control.Monad.Identity
import Control.Monad.State
-import Control.Monad.Trans.Either
import qualified Data.Foldable as F
-import qualified Data.HashSet as H
import qualified Data.Map as M
-import qualified Data.Set as S
import qualified Data.Traversable as T
--- import qualified Debug.Trace as XT
+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.Main.Exception
--- import Dyna.XXX.DataUtils
-import Dyna.XXX.MonadUtils
--- import System.IO.Unsafe (unsafePerformIO)
-import System.Mem.StableName (makeStableName)
import Text.PrettyPrint.Free
------------------------------------------------------------------------}}}
-- Datatype definition {{{
--- | Each named position in a NIX automata either references another
--- closed term or an InstF ply which itself recurses as labels in this
--- automata.
---
--- Note that we are contractually obligated to keep NIX automata mutually
--- acyclic (i.e. all cycles must be confied within some NIX automata).
-type NIXM a f = M.Map a (Either (NIX f) (InstF f a))
-
--- | A closed, mu-recursive inst.
---
--- The existential captures a @Show f@ as well for use by 'panicwf' below.
--- This requires that all terms constructing NIXes afresh (e.g. 'nHide' and
--- 'nShallow') have a @Show f@ constraint, but means that we don't need to
--- annotate the whole universe. The trade-off, of course, is that we
--- potentially carry those dictionaries around at runtime.
---
--- The accessors and constructor is exported solely for the selftests'
--- benefits and SHOULD NOT be used elsewhere in the code!
-data NIX f = forall a . (Ord a,Show a,Show f) =>
- NIX
- {
- -- | The top InstF ply in this term.
- --
- -- Note that while we could, in theory, have used @:: a@ here,
- -- this would complicate the out-of-phase branch of comparison
- -- operators. Moreover, it's probably a good idea to use a ply
- -- at the top as it forces NIX to be productive and not just
- -- immediately alias another NIX via its map.
- nix_root :: InstF f a
- , nix_map :: NIXM a f
- }
+newtype NIX f = NIX { unNIX :: NA (InstF f) }
-- | Semantic, not structural, equality
instance (Ord f) => Eq (NIX f) where
n1 == n2 = nEq n1 n2
--- XXX This is hideously ugly, but we can clean it up later
-instance (Show f) => Show (NIX f) where
- show (NIX r m) = "(NIX ("++ (show r) ++ ") (" ++ (show m) ++ "))"
-
------------------------------------------------------------------------}}}
--- Utilities {{{
-
--- | Throw exception if ever a NIX is not well formed
-panicwf :: NIX f -> a
-panicwf n = dynacPanic (text "NIX not well-formed"
- `above` indent 2 (renderNIX n))
-
--- | Often we want to check a set cache for membership, returning true if
--- so, or assume this case and run some action to obtain a boolean. This is
--- used, for example, in cycle-breaking in backward chaining: we assume the
--- provability of our assumption and continue to look for a
--- counter-argument. Note that this is rather the opposite of most circular
--- systems!
-tsc :: (Ord e, MonadState s m)
- => Simple Lens s (S.Set e)
- -> e
- -> m Bool
- -> m Bool
-tsc l e miss = (uses l $ S.member e)
- `orM`
- (l %= S.insert e >> miss)
-
--- | Either of Maybe of Lookup. A common pattern found in implementation.
-eml :: (Ord k)
- => NIX f -- ^ For debugging
- -> (a -> c)
- -> (b -> c)
- -> M.Map k (Either a b)
- -> k
- -> c
-eml n al ar m x = either al ar (ml n m x)
-
--- | Our particular version of 'fromJust' which panics appropriately.
-ml :: (Ord k) => NIX f -> M.Map k b -> k -> b
-ml n m x = maybe (panicwf n) id (M.lookup x m)
+-- Pretty-printing {{{
-------------------------------------------------------------------------}}}
--- Pretty-printing core {{{
-
-renderNIX_ :: forall f e. (NIX f -> Doc e) -> NIX f -> Doc e
-renderNIX_ p (NIX r m) = align $
- ri r <> if M.null m
- then empty
- else line <> (indent 2 $
- text "where"
- <+> (align $ vsep $ map rme $ M.toList m))
- where
- -- render index
- rix = angles . text . show
-
- -- render map entry
- rme (k,v) = rix k <+> equals <+> either p ri v
-
- ri = IP.compactly (text . show) rix
-
--- | Print out a NIX just as it is. Notably, this is used by 'panicwf',
--- rather than the 'Pretty' instance, which, in order to be pretty, calls
--- 'nPrune'.
-renderNIX :: forall f e . NIX f -> Doc e
-renderNIX = fix renderNIX_
+-- | Render a NIX exactly as it stands (the 'Pretty' instance performs
+-- minimization first).
+renderNIX :: forall f e . (Show f) => NIX f -> Doc e
+renderNIX = autRender (IP.compactly (text.show) id) . unNIX
+
+-- | Pretty-printing minimizes automata first
+instance (Show f, Ord f) => Pretty (NIX f) where
+ pretty (nMinimize -> n) = renderNIX n
+
+instance (Show f, Ord f) => Show (NIX f) where
+ show = show . pretty
------------------------------------------------------------------------}}}
-- Unary predicates {{{
+-- | Check well-formedness of an inst at a given Uniq. All uniqueness
+-- annotations within the inst are required to be larger (i.e. less unique,
+-- more restrictive).
+
+-- XXX This formulation does not use iWellFormed_.
+-- XXX I'm not sure that it's correct, either. It has just enough hacks
+-- that I am uncomfortable.
+nWellFormedUniq :: forall f . Uniq -> NIX f -> Bool
+nWellFormedUniq u0 (NIX n) =
+ case autReduce (Just UClobbered) go n of
+ Nothing -> False
+ Just u -> u0 <= u
+ where
+ go fmu = let ufu = maybe UClobbered id $ iUniq fmu
+ mfu = T.sequence fmu
+ in mfu >>= \fu -> if ufu <= minimum (UClobbered : F.toList fu)
+ then Just ufu
+ else Nothing
+
+{-
-- | Check well-formedness of an inst at a given Uniq. All uniqueness
-- annotations within the inst are required to be larger (i.e. less unique,
-- more restrictive).
eml n0 (return . nWellFormedUniq u)
(iWellFormed_ q u)
m a
+-}
--- | Check that a named inst is acyclic.
---
--- Makes use of the 'StableName' functionality (and 'unsafePerformIO') to
--- ensure that the Haskell heap is acyclic. This is likely useful for
--- debugging nontermination of the compiler. There's nothing that can save
--- us from an evil NIX which generates additional NIXes on the fly, tho'.
---
-nWellFormedOC :: (Ord f) => NIX f -> IO ()
-nWellFormedOC n0 = evalStateT (go n0) H.empty
- where
- mksp x = x `seq` makeStableName x
-
- visit q i = F.mapM_ (F.mapM_ q) (i ^. inst_rec)
-
- go n@(NIX i m) = do
- sn <- liftIO $ mksp n
- vis <- get
- if sn `H.member` vis
- then dynacPanicStr "Named inst occurs check!"
- else do
- put (H.insert sn vis)
- evalStateT (visit q i) S.empty
- where
- q a = tsc id a
- (eml n0 (lift . go) (visit q) m a >> return True)
-- | Is a named inst ground?
--
-- (see def 3.2.17, p52), which includes everything from UUnique to
-- UClobbered. This may not be what you mean.
nGround :: forall f . NIX f -> Bool
-nGround n0@(NIX i0 m) = evalState (iGround_ q i0) S.empty
+nGround = autReduce True (runIdentity . iGround_ return) . unNIX
+
+nNotEmpty_ :: forall f .
+ ([Bool] -> Bool)
+ -> NIX f
+ -> Bool
+nNotEmpty_ disj = autReduce True (runIdentity . visit) . unNIX
where
- q a = tsc id a $ eml n0 (return . nGround) (iGround_ q) m a
+ visit IFree = return True
+ visit (IUniv _) = return True
+ visit (IAny _) = return True
+ visit (IBound _ m b) = return (disj (b:fmap and (F.toList m)))
+{-# INLINABLE nNotEmpty_ #-}
-- | Is there some term not ruled out by this inst?
--
-- This is mostly useful for the test harness, not actual reasoning, at
-- the moment, since we are not sufficiently precise (i.e. we will miss some
-- empty unification results).
+--
+-- Note in particular for InstF, the only non-accepting states are
+-- @IBound _ mempty False@; all the others include some term.
nSomeNotEmpty :: forall f . NIX f -> Bool
-nSomeNotEmpty = fix (nNotEmpty_core orAny)
- where orAny b bs = b `orM1` (anyM bs)
+nSomeNotEmpty = nNotEmpty_ or
+{-# INLINABLE nSomeNotEmpty #-}
--- | Like 'nNotEmpty' but conjunctive across choices -- that is, this
+-- | Like 'nSomeNotEmpty' but conjunctive across choices -- that is, this
-- requires that all possible branches of an automata are non-empty, rather
--- than 'nNotEmpty', which only checks that there is some reachable state in
--- the automata.
-nAllNotEmpty :: forall f . (Show f) => NIX f -> Bool
-nAllNotEmpty = fix (nNotEmpty_core andAll)
- where andAll b bs = b `andM1` (allM bs)
-
-
-
-nNotEmpty_core :: forall f .
- (forall m .
- (Monad m)
- => Bool
- -> [m Bool]
- -> m Bool)
- -> (NIX f -> Bool)
- -> NIX f -> Bool
-nNotEmpty_core disj self n0@(NIX i0 m0) = evalState (visit i0) S.empty
- where
- visit IFree = return True
- visit (IUniv _) = return True
- visit (IAny _) = return True
- visit (IBound _ m b) = b `disj` (M.foldr (\fas a -> allM (map rec fas) : a) [] m)
-
- rec idx = tsc id idx (eml n0 (return . self) visit m0 idx)
+-- than 'nSomeNotEmpty', which only checks that there is some input which
+-- is accepted by the automata.
+nAllNotEmpty :: forall f . NIX f -> Bool
+nAllNotEmpty = nNotEmpty_ and
+{-# INLINABLE nAllNotEmpty #-}
--- | Increase the nonuniqueness of a particular named inst to at least the
--- given level.
---
--- This would be equivalent to unification with 'IANy' at the given 'Uniq'
--- level, save that it leaves free variables untouched.
nUpUniq :: forall f . (Ord f) => Uniq -> NIX f -> NIX f
-{-
- - XXX The beginnings of a possibly more efficient implementation
-nUpUniq u0 n0@(NIX i0 m) = uncurry NIX $ runState (T.traverse visit i0) m
- where
- visit a = eml n0 (return . nUpUniq u0)
- (T.traverse visit (over inst_uniq (max u0)))
--}
-nUpUniq u0 n0@(NIX i0 m0) =
- maybe n0 (\u' -> if u' >= u0 then n0 else NIX i0' m0') (iUniq i0)
- where
- reuniq = over inst_uniq (max u0)
-
- m0' = M.map (nUpUniq u0 A.+++ reuniq) m0
- i0' = reuniq i0
+nUpUniq u0 = NIX . autAtEachState (\_ -> over inst_uniq (max u0)) . unNIX
{-# INLINABLE nUpUniq #-}
-- | Expose the root ply of a 'NIX' as an Inst which recurses as additional
--
-- Note that recursive use of this function may well diverge!
nExpose :: NIX f -> InstF f (NIX f)
-nExpose n@(NIX r m) = fmap (\a -> either id (\i -> NIX i m) (ml n m a)) r
+nExpose = fmap NIX . autExpose . unNIX
{-# INLINABLE nExpose #-}
--- | An inefficient \"inverse\" (up to isomorphism) of nExpose.
-nHide :: (Show f) => InstF f (NIX f) -> NIX f
-nHide i = uncurry NIX $ runState (T.mapM next i) M.empty
- where
- next n = do
- m <- get
- let n' = M.size m
- put (M.insert n' (Left n) m)
- return n'
-{-# INLINABLE nHide #-}
-
-nShallow :: (Show f) => InstF f a -> Maybe (NIX f)
-nShallow IFree = Just $ nHide $ IFree
-nShallow (IAny u) = Just $ nHide $ (IAny u)
-nShallow (IUniv u) = Just $ nHide $ (IUniv u)
-nShallow (IBound _ _ _) = Nothing
-{-# INLINABLE nShallow #-}
-
-nDeep :: (Show f, Monad m, Functor m)
- => (r -> m (Either (NIX f) (InstF f r)))
- -> InstF f r
- -> m (NIX f)
-nDeep rec root = liftM (\(nr,(_,nm)) -> NIX nr nm) $
- flip runStateT (0 :: Int, M.empty) $ inst_recps rec' root
- where
- rec' r = do
- a <- _1 <<%= (+(1 :: Int))
- rhs <- lift (rec r)
- rhs' <- either (return . Left) (liftM Right . inst_recps rec') rhs
- _2 %= M.insert a rhs'
- return a
+nHide :: InstF f (NIX f) -> NIX f
+nHide = NIX . autHide . fmap unNIX
+{-# INLinABLE nHide #-}
+nShallow :: (Show f) => InstF f x -> Maybe (NIX f)
+nShallow = fmap NIX . autShallow
+{-# INLINABLE nShallow #-}
+nDeep :: (Functor m, Monad m, Enum ix, Ord ix)
+ => (forall t . (MonadTrans t, Monad (t m))
+ => r -> ix -> t m (Either (NIX f) (InstF f (Either ix r))))
+ -> r -> m (NIX f)
+nDeep f r = liftM NIX $ naUnfold (\r' ix' -> liftM (left' unNIX) $ f r' ix') r
+{-# INLINABLE nDeep #-}
+
+nFromMap :: forall f oix.
+ Ord oix
+ => M.Map oix (InstF f oix) -- ^ recursion table
+ -> oix -- ^ root
+ -> NIX f
+nFromMap m r = NIX (naFromMap m r)
+{-# INLINABLE nFromMap #-}
------------------------------------------------------------------------}}}
-- Binary predicates {{{
-nCmp :: forall f .
- (Ord f)
- => (forall a b m .
- (Monad m)
- => (a -> (forall i_ . InstF f i_) -> m Bool)
- -> (a -> b -> m Bool)
- -> InstF f a -> InstF f b -> m Bool)
- -> NIX f -> NIX f -> Bool
-nCmp q l0@(NIX li0 lm) r0@(NIX ri0 rm) =
- evalState (q qop qip li0 ri0) (S.empty, S.empty)
- where
- -- Q In Phase
- qip l r = -- XT.traceShow ("NCMP QIP",l,r) $
- tsc _1 (l,r) $ do
- eli <- maybe (panicwf l0) return $ M.lookup l lm
- eri <- maybe (panicwf r0) return $ M.lookup r rm
- case (eli,eri) of
- (Left l', Left r') -> return $ nCmp q l' r'
- (Left l', Right r') -> return $ nCmp q l' (NIX r' rm)
- (Right l', Left r') -> return $ nCmp q (NIX l' lm) r'
- (Right l', Right r') -> q qop qip l' r'
-
- -- Q Out of Phase
- qop l ri = -- XT.traceShow ("NCMP QOP",l,ri) $
- tsc _2 (l,downcast ri)
- $ eml l0 (return . flip (nCmp q) (NIX ri rm))
- (flip (q qop qip) ri)
- lm l
-
- downcast :: (forall i_ . InstF f i_) -> InstF f ()
- downcast i = i
-
nEq, nLeq, nSub :: (Ord f) => NIX f -> NIX f -> Bool
-nEq = nCmp (\_ -> iEq_)
-nLeq = nCmp iLeq_
-nSub = nCmp iSub_
+nEq (NIX l) (NIX r) = autBiReduce True (\_ _ -> iEq_) l r
+nLeq (NIX l) (NIX r) = autBiReduce True (\x _ -> iLeq_ x) l r
+nSub (NIX l) (NIX r) = autBiReduce True (\x _ -> iSub_ x) l r
------------------------------------------------------------------------}}}
-- Binary functions {{{
-data NBinState a b f u = NBS { _nbs_next :: Int
- , _nbs_ctx :: NIXM Int f
- , _nbs_cache_symm :: M.Map (u,a,b) Int
- , _nbs_cache_lsml :: M.Map (u,InstF f b,a) Int
- , _nbs_cache_lsmr :: M.Map (u,InstF f a,b) Int
- }
-$(makeLenses ''NBinState)
-
-iNBS :: NBinState a b f u
-iNBS = NBS 0 M.empty M.empty M.empty M.empty
-
-
-nTBin :: forall f . (Ord f, Show f)
- => ( forall a b c m .
- (Monad m)
- => (Uniq -> a -> m c)
- -> (Uniq -> b -> m c)
- -> (Uniq -> (forall i_ . InstF f i_) -> a -> m c)
- -> (Uniq -> (forall i_ . InstF f i_) -> b -> m c)
- -> (Uniq -> a -> b -> m c)
- -> Uniq
- -> InstF f a -> InstF f b -> m (InstF f c))
- -> NIX f -> NIX f -> NIX f
-nTBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (tlq li0 ri0) iNBS
- where
- tlq l r = do
- ci <- f' S.empty UUnique l r
- ctx <- use nbs_ctx
- return $ nPrune $ NIX ci ctx
-
- f' sc = f (imp l0 lm) (imp r0 rm) (lsml sc) (lsmr sc) (merge sc)
-
- -- XXX import needs some caching, too.
-
- -- Occasionally, we need to "import" a term from one of the two inputs;
- -- this happens when we unify 'IBound' against 'IAny' or 'IUniv', for
- -- example.
- --
- -- To import the key x from the map m into our context,
- -- if it is a closed term, just return that
- -- otherwise, make it a closed term whose root is x and whose map is m
- imp n m u x =
- -- XT.traceShow ("NTB I",u,m,x)
- eml n return (return . flip NIX m) m x >>= new . Left . nUpUniq u
-
- new x = do
- k <- nbs_next <<%= (+1)
- nbs_ctx %= M.insert k x
- return k
-
- lsml sc u ir l = -- XT.traceShow ("NTB L",u,ir,l) $
- do
- cached <- uses nbs_cache_lsml $ M.lookup (u,ir,l)
- maybe merge' return cached
- where
- merge' = do
- k <- nbs_next <<%= (+1)
- nbs_cache_lsml %= M.insert (u,ir,l) k
- v <- eml r0
- (return . luu u . nTBin f (NIX ir rm))
- (\l' -> Right . over inst_uniq (max u) <$> f' (S.insert k sc) u l' ir)
- lm l
- nbs_ctx %= M.insert k v
- return k
-
- lsmr sc u il r = -- XT.traceShow ("NTB R",u,il,r) $
- do
- cached <- uses nbs_cache_lsmr $ M.lookup (u,il,r)
- maybe merge' return cached
- where
- merge' = do
- k <- nbs_next <<%= (+1)
- nbs_cache_lsmr %= M.insert (u,il,r) k
- v <- eml r0
- (return . luu u . nTBin f (NIX il lm))
- (\r' -> Right . over inst_uniq (max u) <$> f' (S.insert k sc) u il r')
- rm r
- nbs_ctx %= M.insert k v
- return k
-
- luu u = Left . nUpUniq u
-
- merge sc u l r = -- XT.traceShow ("NTB M",u,l,r) $
- do
- cached <- uses nbs_cache_symm $ M.lookup (u,l,r)
- maybe merge' return cached
- where
- merge' = do
- k <- nbs_next <<%= (+1)
- nbs_cache_symm %= M.insert (u,l,r) k
- eli <- maybe (panicwf l0) return $ M.lookup l lm
- eri <- maybe (panicwf r0) return $ M.lookup r rm
- v <- case (eli,eri) of
- (Left l', Left r') -> return $ luu u $ nTBin f l' r'
- (Left l', Right r') -> return $ luu u $ nTBin f l' (NIX r' rm)
- (Right l', Left r') -> return $ luu u $ nTBin f (NIX l' lm) r'
- (Right l', Right r') -> Right . over inst_uniq (max u)
- <$> f' (S.insert k sc) u l' r'
- nbs_ctx %= M.insert k v
- return k
-
--- | Total lattice functions
-nLeqGLB, nSubGLB :: forall f .
- (Ord f, Show f)
- => NIX f -> NIX f -> NIX f
-nLeqGLB = nTBin iLeqGLB_
-nSubGLB = nTBin (\_ _ fl fr fm _ -> iSubGLB_ (fl UUnique) (fr UUnique) (fm UUnique))
-
-nPBin :: forall e f .
- (Ord f, Show f)
- => ( forall a b c m .
- (Monad m, Show a, Show b, Show c)
- => (Uniq -> a -> m c)
- -> (Uniq -> b -> m c)
- -> (Uniq -> (forall i_ . InstF f i_) -> a -> m c)
- -> (Uniq -> (forall i_ . InstF f i_) -> b -> m c)
- -> (Uniq -> a -> b -> m c)
- -> Uniq
- -> InstF f a -> InstF f b -> m (Either e (InstF f c)))
- -> NIX f -> NIX f -> Either e (NIX f)
-nPBin f l0@(NIX li0 lm) r0@(NIX ri0 rm) = evalState (runEitherT (tlq li0 ri0)) iNBS
- where
- tlq l r = do
- ci <- f' S.empty UUnique l r
- ci' <- hoistEither ci
- ctx <- use nbs_ctx
- return $ nPrune $ NIX ci' ctx
-
- f' sc = f (imp l0 lm) (imp r0 rm) (lsml sc) (lsmr sc) (merge sc)
-
- luu u = Left . nUpUniq u
- mluu u r = luu u <$> hoistEither r
-
- -- Occasionally, we need to "import" a term from one of the two inputs;
- -- this happens when we unify 'IBound' against 'IAny' or 'IUniv', for
- -- example.
- --
- -- To import the key x from the map m into our context,
- -- if it is a closed term, just return that
- -- otherwise, make it a closed term whose root is x and whose map is m
- imp n m u x = {- XT.traceShow ("NPB I",m,u,x) $ -}
- new . luu u =<< eml n return (return . flip NIX m) m x
-
- new x = do
- k <- nbs_next <<%= (+1)
- nbs_ctx %= M.insert k x
- return k
-
- lsml sc u ir l = {- XT.traceShow ("NPB L",u,ir,l) $ -}
- do
- cached <- uses nbs_cache_lsml $ M.lookup (u,ir,l)
- maybe merge' return cached
- where
- merge' = do
- k <- nbs_next <<%= (+1)
- nbs_cache_lsml %= M.insert (u,ir,l) k
- v <- eml r0
- (mluu u . nPBin f (NIX ir rm))
- (\l' -> do
- l'' <- f' (S.insert k sc) u l' ir
- (Right . over inst_uniq (max u)) <$> hoistEither l'')
- lm l
- nbs_ctx %= M.insert k v
- return k
-
- lsmr sc u il r = {- XT.traceShow ("NPB R",u,il,r) $ -}
- do
- cached <- uses nbs_cache_lsmr $ M.lookup (u,il,r)
- maybe merge' return cached
- where
- merge' = do
- k <- nbs_next <<%= (+1)
- nbs_cache_lsmr %= M.insert (u,il,r) k
- v <- eml r0
- (mluu u . nPBin f (NIX il lm))
- (\r' -> do
- r'' <- f' (S.insert k sc) u il r'
- (Right . over inst_uniq (max u)) <$> hoistEither r'')
- rm r
- nbs_ctx %= M.insert k v
- return k
-
-
- merge sc u l r = {- XT.traceShow ("NPB M",u,l,r) $ -}
- do
- cached <- uses nbs_cache_symm $ M.lookup (u,l,r)
- maybe merge' return cached
- where
- merge' = do
- k <- nbs_next <<%= (+1)
- nbs_cache_symm %= M.insert (u,l,r) k
- eli <- maybe (panicwf l0) return $ M.lookup l lm
- eri <- maybe (panicwf r0) return $ M.lookup r rm
- v <- case (eli,eri) of
- (Left l', Left r') -> mluu u $ nPBin f l' r'
- (Left l', Right r') -> mluu u $ nPBin f l' (NIX r' rm)
- (Right l', Left r') -> mluu u $ nPBin f (NIX l' lm) r'
- (Right l', Right r') -> do
- m' <- f' (S.insert k sc) u l' r'
- (Right . over inst_uniq (max u))
- <$> hoistEither m'
- nbs_ctx %= M.insert k v
- return k
-
--- | Partial lattice functions. These raise unification failures if
--- the runtime would fail.
-nLeqGLBRD, nLeqGLBRL :: forall f .
- (Ord f, Show f)
- => NIX f -> NIX f -> Either UnifFail (NIX f)
-nLeqGLBRD = nPBin iLeqGLBRD_
-nLeqGLBRL = nPBin iLeqGLBRL_
-
{-
XXX BITROTTED; NOT YET -- need better understanding of the problem. The ⊔
its recursion in a way that is not painfully special-cased. At this instant
I have other things that can demand attention.
-
nSubLUB :: forall f . (Ord f, Show f) => NIX f -> NIX f -> Maybe (NIX f)
nSubLUB = nPBin (\il ir ll lr m -> iSubLUB_ il ir (ll UClobbered) (lr UClobbered) (m UClobbered))
-}
+ctxUniq :: InstF f a -> InstF f' a' -> Uniq
+ctxUniq x y = u x `max` u y
+ where
+ u = maybe UUnique id . iUniq
+
+-- XXX This may suggest that we could eliminate the "import" callbacks on
+-- iLeqGLB_ and friends now that we're not doing anything special with them.
+
+bendImpl :: forall f i i' i'' m r .
+ TyILeqGLB_ f m i i' i'' r
+ -> (Uniq -> i -> NonRec (InstF f) -> m i'')
+ -> (Uniq -> NonRec (InstF f) -> i' -> m i'')
+ -> (Uniq -> i -> i' -> m i'')
+ -> Uniq -> InstF f i -> InstF f i' -> r
+bendImpl x lsml lsmr merge = x impl impr lsml' lsmr merge
+ where
+ lsml' :: Uniq -> NonRec (InstF f) -> i -> m i''
+ lsml' u r l = lsml u l r
+
+ impl :: Uniq -> i -> m i''
+ impl u l = lsml u l IFree
+
+ impr :: Uniq -> i' -> m i''
+ impr u r = lsmr u IFree r
+
+nLeqGLB, nSubGLB :: forall f . (Ord f) => NIX f -> NIX f -> NIX f
+nLeqGLB (NIX l) (NIX r) = NIX $ autMerge ctxUniq (bendImpl iLeqGLB_) l r
+nSubGLB (NIX l) (NIX r) = NIX $ autMerge (\_ _ -> ()) go l r
+ where
+ go lsml lsmr merge () = iSubGLB_ (flip (lsml ())) (lsmr ()) (merge ())
+
+nLeqGLBRD, nLeqGLBRL :: (Ord f) => NIX f -> NIX f -> Either UnifFail (NIX f)
+nLeqGLBRD (NIX l) (NIX r) = fmap NIX $ autPMerge ctxUniq (bendImpl iLeqGLBRD_) l r
+nLeqGLBRL (NIX l) (NIX r) = fmap NIX $ autPMerge ctxUniq (bendImpl iLeqGLBRL_) l r
+
------------------------------------------------------------------------}}}
-- Mode functions {{{
------------------------------------------------------------------------}}}
-- Cleanup and minimization {{{
-nCrawl :: forall f .
- (forall a . Uniq -> InstF f a) -- ^ Replace free variables
- -> Uniq -- ^ Minimum uniqueness
- -> NIX f
- -> NIX f
-nCrawl fv u0 n0@(NIX i0 m) =
- let i0' = reall u0 i0 in NIX i0' $ execState (T.traverse (evac u0) i0') M.empty
- where
- reun = over inst_uniq (max u0)
-
- refv u IFree = fv u
- refv _ x = x
-
- reall u = reun . refv u
-
- evac u i = gets (M.lookup i) >>= maybe (go u i) (const $ return ())
-
- go u i = do
- let l = ml n0 m i
- case l of
- Left n -> id %= M.insert i (Left $ nCrawl fv u n)
- Right x -> do
- id %= M.insert i (Right $ reall u x)
- F.traverse_ (evac (maybe u (max u) $ iUniq x)) x
- return ()
-
--- | Prune the internals of a 'NIX'. This really ought not be needed, but
--- it's handy for test generation.
-nPrune :: forall f . NIX f -> NIX f
-nPrune = nCrawl (const IFree) UUnique
-
-------------------------------------------------------------------------}}}
--- Pretty-printing part 2 {{{
-
-instance Pretty (NIX f) where
- pretty (nPrune -> n) = renderNIX_ pretty n
+nMinimize :: (Ord f) => NIX f -> NIX f
+nMinimize = NIX . autMinimize . unNIX
------------------------------------------------------------------------}}}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall #-}
import Control.Applicative (Applicative)
import Control.Lens
--- import Control.Monad
+import Control.Monad
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 qualified Data.Set as S
+import Dyna.Analysis.Mode.Uniq
import Dyna.XXX.DataUtils as XDU
import Dyna.XXX.MonadUtils
-import Dyna.Analysis.Mode.Uniq
-
-- import qualified Debug.Trace as XT
------------------------------------------------------------------------}}}
-- | Extract the uniqueness from an inst.
--
-- Based on definition 3.2.13, p51 but see prose, p51, \"Note that there is
--- no uniqueness annotation on the free inst\".
+-- no uniqueness annotation on the free inst\". This is because we assume,
+-- during mode work, that we know where all the free variables are -- that
+-- is, they're either uniquely referenced in some automata or they are
+-- explicitly aliased.
iUniq :: InstF f i -> Maybe Uniq
-{-
-iUniq IFree = Nothing
-iUniq (IAny u) = Just u
-iUniq (IBound u _ _) = Just u
-iUniq (IUniv u) = Just u
--}
iUniq = (^? inst_uniq)
{-# INLINABLE iUniq #-}
-- variables).
iLeqGLB_ :: (Monad m, Ord f) => TyILeqGLB_ f m i i' i'' (m (InstF f i''))
-iLeqGLB_ _ r _ _ _ u IFree x = T.mapM (r u) x
-iLeqGLB_ l _ _ _ _ u x IFree = T.mapM (l u) x
+iLeqGLB_ _ r _ _ _ u IFree x = liftM (over inst_uniq (max u))
+ $ T.mapM (r u) x
+iLeqGLB_ l _ _ _ _ u x IFree = liftM (over inst_uniq (max u))
+ $ T.mapM (l u) x
iLeqGLB_ _ _ _ _ _ _ (IAny u) (IAny u') = return $ IAny (max u u')
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.Analysis.Mode.Execution.NamedInst
import Dyna.Analysis.Mode.Inst
import Dyna.Analysis.Mode.Selftest.Term
prop_arbNIX_is_WFU :: QCP.Property
prop_arbNIX_is_WFU = QCP.forAll (arbNIX UUnique) nWFU
--- | Check 'nPrune' using the separate 'arbNIX' generator, rather than
--- the 'Arbitrary' instance, which calls 'nPrune' internally.
+-- | Check 'nMinimize' using the separate 'arbNIX' generator, rather than
+-- the 'Arbitrary' instance, which calls 'nMinimize' internally.
prop_nPrune_Eq :: QCP.Property
-prop_nPrune_Eq = QCP.forAll (arbNIX UUnique) (\i -> nWFU i QCP.==> i `nEq` (nPrune i))
+prop_nPrune_Eq = QCP.forAll (arbNIX UUnique)
+ (\i -> nWFU i QCP.==> i `nEq` (nMinimize i))
-- | Check 'nMinimize'
-- prop_nMinimize_Eq :: Bool -> QCP.Property
selftest :: TF.Test
selftest = moreTries 5000 $(testGroupGenerator)
+
+main = TF.defaultMain [selftest]
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Dyna.Analysis.Mode.Selftest.Term where
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 Test.QuickCheck
import Test.SmallCheck as SC
import Test.SmallCheck.Series as SCS
+import qualified Text.PrettyPrint.Free as PP
------------------------------------------------------------------------}}}
-- Misc {{{
data TestFunct = F | G | H
deriving (Bounded,Enum,Eq,Ord,Show)
+instance PP.Pretty TestFunct where pretty = PP.text . show
+
genArgs :: (Monad m) => m i -> TestFunct -> m [i]
genArgs _ F = return []
genArgs g G = g >>= return . (\x -> [x])
instance Arbitrary (S.Set TestFunct) where arbitrary = arbitrarySetBEO
-- | Generate an arbitrary, well-formed NIX at some uniqueness.
+arbNIX :: Uniq -> Gen (NIX TestFunct)
arbNIX rootU = do
n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies?
let igen u = oneof $ map (return.snd) $ filter ((== u) . fst)
$ (zip uniqs nl ++ spares)
- plies <- mapM (flip arbNIXME igen) uniqs -- Generate plies or recurse
+ plies <- mapM (flip arbInstPly igen) uniqs -- Generate plies or recurse
let m = M.fromList (zip nl plies -- Make the map
- ++ map (\(_,i) -> (i,Right IFree)) spares)
- root <- arbInstPly rootU igen -- The root
- return $ NIX root m
+ ++ map (\(_,i) -> (i,IFree)) spares)
+ root <- choose (1,n)
+ return $ nFromMap m root
where
arbInstPly :: forall i . Uniq -> (Uniq -> Gen i) -> Gen (InstF TestFunct i)
arbInstPly u n = frequency
<*> arbitrary)
]
- arbNIXME :: forall f i . (f ~ TestFunct)
- => Uniq -> (Uniq -> Gen i) -> Gen (Either (NIX f) (InstF f i))
- arbNIXME u igen = oneof [Left <$> sized (\s -> resize (s`div`2) (arbNIX u))
- ,Right <$> arbInstPly u igen]
-
-
-- | The not-necessarily-well-formed variant
+arbNIXNWF :: Gen (NIX TestFunct)
arbNIXNWF = do
n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies?
let nl = [1..n]
let igen = choose (1::Int,n) -- Pick a ply
- plies <- vectorOf n (arbNIXMENWF igen) -- Generate plies or recurse
+ plies <- vectorOf n (arbInstPlyNWF igen) -- Generate plies or recurse
let m = M.fromList $ zip nl plies -- Make the map
- root <- arbInstPlyNWF igen -- The root
- return $ NIX root m
+ root <- choose (1,n)
+ return $ nFromMap m root
where
arbInstPlyNWF :: forall i . Gen i -> Gen (InstF TestFunct i)
arbInstPlyNWF n = frequency
$ genFuncMap arbitrary n)
<*> arbitrary)
]
-
- arbNIXMENWF :: forall f i . (f ~ TestFunct)
- => Gen i -> Gen (Either (NIX f) (InstF f i))
- arbNIXMENWF igen = oneof [Left <$> sized (\s -> resize (s`div`2) arbitrary)
- ,Right <$> arbInstPlyNWF igen]
-
instance Arbitrary (NIX TestFunct) where
- arbitrary = nPrune <$> arbNIX UUnique
+ arbitrary = liftM nMinimize $ arbNIX UUnique
+{-
shrink n@(NIX r m) = (MA.maybeToList noRecN) ++ subautomata
where
-- Replace all calls out to other automata with references to the root
-- Pull out all the subautomata
subautomata = E.lefts (M.elems m)
-
+-}
------------------------------------------------------------------------}}}
-- Term: SmallCheck Generators {{{
<+> c v vs
pdope_ _ (OPIter v vs _ DetNon (Just (PDBS c))) = do
- i <- incState
+ i <- incState id
return $ "for" <+> "d" <> pretty i
<> comma
<> piterate vs
-- XXX This works only for the special case at hand (thus the asserts)
pdope_ bc (OPIter o m f DetSemi Nothing) | (f,length m) `S.member` bc = do
- dookie <- incState
+ dookie <- incState id
return $
assert (iIsFree $ nExpose $ o^.mv_mi) $
assert (all (not . iIsFree . nExpose . _mv_mi) m) $
pdope_ bc (OPIter o m f _ Nothing) =
assert (not $ (f,length m) `S.member` bc) $ do
- i <- incState
+ i <- incState id
return $ let mo = m ++ [o] in
"for" <+> "d" <> pretty i <> "," <> piterate m <> comma <> (ground2underscore o)
<+> "in" <+> functorIndirect "chart" f m <> pslice mo <> colon
+{-# LANGUAGE Rank2Types #-}
+
module Dyna.XXX.MonadUtils(
-- * Data utilities generalizing 'Dyna.XXX.DataUtils'
mapForallM, mapExistsM, setForallM, setExistsM,
andM, andM1, orM, orM1, allM, anyM,
-- * MonadState utilities
bracketState, incState, readState,
+ -- * Monad cache utilities
+ trySetCache, tryMapCache,
) where
-- import Control.Applicative
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Map as M
+import Data.Monoid
import qualified Data.Set as S
andM :: Monad m => m Bool -> m Bool -> m Bool
andM x y = x >>= flip andM1 y
+{-# INLINABLE andM #-}
andM1 :: Monad m => Bool -> m Bool -> m Bool
andM1 False _ = return False
andM1 True x = x
+{-# INLINABLE andM1 #-}
orM :: Monad m => m Bool -> m Bool -> m Bool
orM x y = x >>= flip orM1 y
+{-# INLINABLE orM #-}
orM1 :: Monad m => Bool -> m Bool -> m Bool
orM1 True _ = return True
orM1 False x = x
+{-# INLINABLE orM1 #-}
allM :: Monad m => [m Bool] -> m Bool
allM = foldM andM1 True
+{-# INLINABLE allM #-}
anyM :: Monad m => [m Bool] -> m Bool
anyM = foldM orM1 False
+{-# INLINABLE anyM #-}
timesM :: Monad m => (a -> m a) -> Int -> a -> m a
timesM f = go
go n _ | n < 0 = error "timesM negative iteration count"
go 0 a = return a
go n a = f a >>= go (n-1)
+{-# INLINABLE timesM #-}
mapForallM, mapExistsM :: (Monad m)
=> (k -> v -> m Bool) -> M.Map k v -> m Bool
mapForallM p m = M.foldrWithKey (\k v -> (andM $ p k v)) (return True ) m
mapExistsM p m = M.foldrWithKey (\k v -> (orM $ p k v)) (return False) m
+{-# INLINABLE mapForallM #-}
+{-# INLINABLE mapExistsM #-}
setForallM, setExistsM :: (Monad m)
=> (e -> m Bool) -> S.Set e -> m Bool
setForallM p m = S.foldr (\e -> (andM $ p e)) (return True ) m
setExistsM p m = S.foldr (\e -> (orM $ p e)) (return False) m
+{-# INLINABLE setForallM #-}
+{-# INLINABLE setExistsM #-}
bracketState :: (MonadState s m) => s -> m t -> m (t, s)
bracketState bs m = do
s' <- get
put s
return (r, s')
+{-# INLINABLE bracketState #-}
-incState :: (Num a, MonadState a m) => m a
-incState = id <<%= (+1)
+-- | Increment a state field given its lens. Often you will just want to
+-- pass "id" or something similarly simple (frequently much shorter than
+-- the type given here!)
+incState :: (Enum a, MonadState s m)
+ => Overloading (->) (->) ((,) a) s s a a
+ -> m a
+incState = (<<%= succ)
+{-# INLINABLE incState #-}
readState :: (MonadState a m) => ReaderT a m b -> m b
readState x = get >>= runReaderT x
+{-# INLINABLE readState #-}
+
+-- | Often we want to check a set cache for membership, returning 'mempty'
+-- if so, or assume this case and run some action to obtain a result.
+--
+-- This is used, for example, in cycle-breaking in backward chaining, often,
+-- using 'True' for the cycle-break value, we assume the provability of our
+-- assumption and continue to look for a counter-argument. Note that this
+-- is rather the opposite of most circular systems, where 'False' would be
+-- the cycle-break value.
+trySetCache :: (Ord e, MonadState s m)
+ => Simple Lens s (S.Set e)
+ -> r
+ -> (e -> m r)
+ -> e
+ -> m r
+trySetCache l cyc miss e = do
+ h <- (uses l $ S.member e)
+ if h
+ then return cyc
+ else l %= S.insert e >> miss e
+{-# INLINABLE trySetCache #-}
+
+-- | Like 'trySetCache' but a version that actually, well, caches a value.
+-- This depends on us being able to store something into the map before
+-- actually recursing and does not update the map while recursing (the
+-- callbacks may of course do so at their own risk).
+tryMapCache :: (Ord e, MonadState s m)
+ => Simple Lens s (M.Map e a)
+ -> (e -> m a) -- On miss, construct @a@
+ -> (e -> a -> m ()) -- Now, given @a@, recurse
+ -> e
+ -> m a
+tryMapCache l mk rec e = use (l . at e) >>= maybe miss return
+ where
+ miss = mk e >>= \k -> (l . at e .= Just k) >> rec e k >> return k
+{-# INLINABLE tryMapCache #-}
projects / dyna2 / commitdiff