-- ** Inst Keys (§5.3.1, p94)
KI(..), KR(..), KRI, ENKRI,
-- ** Variables
- VV(..), VR(..),
+ VR(..),
-- * Context
-- ** Notes
-- ** Monad
SIMCT(..), runSIMCT,
-- *** And its context
- SIMCtx(..), emptySIMCtx,
+ SIMCtx(..), emptySIMCtx, allFreeSIMCtx,
-- ** Internal helper functions
- aliasX, aliasY,
+ e2x, q2y, aliasN, aliasV, aliasX, aliasY, kUpUniq,
)where
+import Control.Applicative (Applicative)
import Control.Exception(assert)
import Control.Lens
import Control.Monad
import Control.Monad.Error.Class
import Control.Monad.State
import Control.Monad.Trans.Either
-import Control.Monad.Trans.State
+-- import qualified Control.Monad.Trans.Maybe as CMTM
+import qualified Control.Monad.Trans.State as CMTS
+import qualified Control.Monad.Trans.Reader as CMTR
-- import Data.Function
-import qualified Data.Map as M
-import qualified Data.Traversable as T
+import qualified Data.Map as M
+import qualified Data.IntMap as IM
+import qualified Data.Traversable as T
-- import Data.Unique
import Dyna.Analysis.Mode.Execution.NamedInst
import Dyna.Analysis.Mode.Inst
+import qualified Dyna.Analysis.Mode.InstPretty as IP
import Dyna.Analysis.Mode.Unification
+import Dyna.Analysis.Mode.Uniq
import Dyna.Main.Exception
+import Dyna.Term.TTerm
import Dyna.XXX.DataUtils
import Dyna.XXX.MonadContext
-import qualified Debug.Trace as XT
-import qualified Text.PrettyPrint.Free as PP
+-- import qualified Debug.Trace as XT
+import qualified Text.PrettyPrint.Free as PP
------------------------------------------------------------------------}}}
-- Inst Types {{{
-- | An aliased variable, also known as an Inst Key. See §5.3.1, p94.
--
-- We use 'Int' internally for the moment
-newtype KI = KI { unKI :: Int } deriving (Eq,Num,Ord,Show)
+newtype KI = KI { unKI :: Int } deriving (Eq,Ord,Show)
--- | Key InstMap Values. These represent aliased bits of structure built up
+-- XXX Should probably track some notion of "display name" instead...
+instance PP.Pretty KI where
+ pretty (KI i) = (PP.text "_AK" PP.<> PP.pretty i)
+
+-- | Key Recursion. These represent aliased bits of structure built up
-- during analysis.
--
-- Periodically, we will attempt to collect structure that is no longer
-- | A defined inst (though filtered through the understanding that it
-- is aliased).
KRName n
- -- | An alias chain. It is safe to semiprune these as desired.
- | KRKey k
-- | An aliased inst ply, which recurses either as an (aliased) named inst
-- or as aliased structure.
- | KRInst (KRI f n k)
+ | KRStruct (KRI f n k)
+ -- | An alias chain. It is safe to semiprune these as desired.
+ | KRKey k
deriving (Eq,Ord,Show)
+instance (PP.Pretty 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 (KRKey k) = PP.pretty k
+
type KRI f n k = InstF f (Either n k)
-- | When the user looks up a key, they expect to get either a name or a ply
-- information about aliasing internal to the inst key map.
type ENKRI f n k = Either n (KRI f n k)
-------------------------------------------------------------------------}}}
--- Insts: Unaliased Insts {{{
-
-{-
--- | An unaliased variable. Again we use 'Int' internally for the moment.
-newtype UI = UI { unUI :: Int } deriving (Eq,Num,Ord,Show)
-
--- | Unaliased (User) InstMap Values. These represent unaliased structure
--- built up during analysis.
---
--- Note that Vars are defined to be acyclic (XXX again, no occurs check
--- right now)
-type UR f n k u = InstF f (VR n k u)
--}
-
------------------------------------------------------------------------}}}
-- Insts: Variables {{{
--- | An user variable.
-newtype VV = VV { unVV :: String } deriving (Eq,Ord,Show)
-
-- | Variables (and unaliased structure) bindings
data VR f n k =
-- | Defined named inst (unaliased)
| VRKey k
deriving (Eq,Ord,Show)
+instance (PP.Pretty 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 (VRKey k) = PP.pretty k
+
+-- | Widen from a more restrictive to less restrictive recursion type.
+e2x :: Either n k -> VR f n k
+e2x = either VRName VRKey
+
+-- | A shorthand which is useful in recursive traversals of 'KR's.
+q2y :: InstF f (Either n k) -> InstF f (VR f n k)
+q2y = fmap e2x
+
------------------------------------------------------------------------}}}
------------------------------------------------------------------------}}}
-- Context {{{
-- Context : Basics {{{
-- | Simplistic InstMap Context
-data SIMCtx f = SIMCtx { _simctx_next_k :: KI
- , _simctx_map_k :: M.Map KI (KR f (NIX f) KI)
- , _simctx_map_v :: M.Map VV (VR f (NIX f) KI)
+data SIMCtx f = SIMCtx { _simctx_next_ki_id :: Int
+ , _simctx_map_k :: IM.IntMap (KR f (NIX f) KI)
+ -- , _simctx_map_k_refs :: IM.IntMap [DVar]
+ , _simctx_map_v :: M.Map DVar (VR f (NIX f) KI)
}
deriving (Show)
$(makeLenses ''SIMCtx)
newtype SIMCT m f a = SIMCT { unSIMCT :: StateT (SIMCtx f) (EitherT UnifFail m) a }
- deriving (Monad,MonadFix)
+ deriving (Monad,MonadFix,Functor,Applicative)
instance (Monad m) => MonadError UnifFail (SIMCT m f) where
throwError e = SIMCT (lift (left e))
- catchError a f = SIMCT (liftCatch catchError (unSIMCT a) (unSIMCT . f))
+ catchError a f = SIMCT (CMTS.liftCatch catchError (unSIMCT a) (unSIMCT . f))
instance MonadIO m => MonadIO (SIMCT m f) where
liftIO m = SIMCT $ lift (liftIO m)
+instance (PP.Pretty f) => PP.Pretty (SIMCtx f) where
+ pretty (SIMCtx _ km vm) =
+ PP.vcat
+ [ PP.text "Unaliased variables:"
+ , PP.indent 2 $
+ PP.vcat $ flip map (M.toAscList vm)
+ $ \(v,vr) -> PP.pretty v
+ PP.<+> PP.text "=>"
+ PP.<+> PP.pretty vr
+ , PP.text "Aliased variables (_AK#):"
+ , PP.indent 2 $
+ PP.vcat $ flip map (IM.toAscList km)
+ $ \(k,kr) -> PP.pretty k
+ PP.<+> PP.text "=>"
+ PP.<+> PP.pretty kr
+ ]
+
{-
- XXX maybe
-}
emptySIMCtx :: SIMCtx f
-emptySIMCtx = SIMCtx 0 M.empty M.empty
+emptySIMCtx = SIMCtx 0 IM.empty {- IM.empty -} M.empty
+
+-- XXX make take S.Set DVar?
+allFreeSIMCtx :: [DVar] -> SIMCtx f
+allFreeSIMCtx fs = SIMCtx 0 IM.empty
+ $ M.fromList $ map (\x -> (x, VRStruct IFree)) fs
runSIMCT :: SIMCT m f a -> SIMCtx f -> m (Either UnifFail (a, SIMCtx f))
runSIMCT q x = runEitherT (runStateT (unSIMCT q) x)
key_canon :: MonadState (SIMCtx f) m => KI -> m KI
key_canon k = do
m <- use simctx_map_k
- let (k',m') = mapSemiprune isKey
- KRKey
- k
- m
+ let (k',m') = intmapSemiprune isKey
+ (KRKey . KI)
+ (unKI k)
+ m
simctx_map_k .= m'
- return k'
+ return (KI k')
where
- isKey (KRKey x) = Just x
- isKey _ = Nothing
+ isKey (KRKey (KI x)) = Just x
+ isKey _ = Nothing
key_lookup :: (MonadState (SIMCtx f) m, Show f)
=> KI
let r = maybe (dynacPanic $ PP.text "Key context miss:"
PP.<+> PP.text (show (k,ck)))
krenkri
- $ M.lookup ck m
- XT.traceShow ("KL",k,ck,r) $ return ()
+ $ IM.lookup (unKI ck) m
+ -- XT.traceShow ("KL",k,ck,r) $ return ()
return r
where
- krenkri (KRKey k') = error $ "Key context noncanonical: "
+ krenkri (KRKey k') = dynacPanicStr $ "Key context noncanonical: "
++ (show (k,k'))
krenkri (KRName n) = Left n
- krenkri (KRInst i) = Right i
+ krenkri (KRStruct i) = Right i
type instance MCVT (SIMCT m f) KI = ENKRI f (NIX f) KI
clookup = SIMCT . key_lookup
instance (Show f, Monad m) => MCD (SIMCT m f) KI where
- cdelete k = XT.traceShow ("KD",k) $ SIMCT $ do
+ cdelete k = {- XT.traceShow ("KD",k) $ -} SIMCT $ do
r <- key_lookup k
- simctx_map_k %= M.delete k
+ simctx_map_k %= IM.delete (unKI k)
return r
{-
instance (Show f, Monad m) => MCW (SIMCT m f) KI where
cassign v q = SIMCT $
- simctx_map_k %= M.insert v (either KRName KRInst q)
+ simctx_map_k %= M.insert v (either KRName KRStruct q)
-}
-instance (Show f, Monad m) => MCM (SIMCT m f) KI where
+
+-- XXX I am concerned about side-effects here: the onus is on the provided
+-- callback to manage side-effects within simctx_map_k, since we simply
+-- clobber its ck entry with the result. In principle, it might have
+-- changed between invocation and return; I'm asserting on this now, and
+-- we'll see if it trips. The Ord instance here is for exactly this assert,
+-- as it calls == on NIX, which calls 'nEq' which needs Ord f.
+instance (Show f, Ord f, Monad m) => MCM (SIMCT m f) KI where
cmerge f k v = SIMCT $ do
ck <- key_canon k
m <- use simctx_map_k
- maybe (assert (ck == k) $ error $ "Key context miss in merge: "
+ maybe (assert (ck == k) $ dynacPanicStr $ "Key context miss in merge: "
++ (show k))
(\v' -> do
merged <- unSIMCT $ f (krenkri v') v
- simctx_map_k .= M.insert ck (either KRName KRInst merged) m)
- $ M.lookup ck m
+ uses (simctx_map_k . at (unKI ck))
+ (flip assert () . (== Just v'))
+ simctx_map_k %= IM.insert (unKI ck)
+ (either KRName KRStruct merged))
+ $ IM.lookup (unKI ck) m
where
- krenkri (KRKey k') = error $ "Key context noncanonical in merge: "
+ krenkri (KRKey k') = dynacPanicStr $ "Key context noncanonical in merge: "
++ (show (k,k'))
krenkri (KRName n) = Left n
- krenkri (KRInst i) = Right i
+ krenkri (KRStruct i) = Right i
-type instance MCNC KI m = ()
+-- type instance MCNC KI m = ()
instance (Show f, Monad m) => MCN (SIMCT m f) KI where
- cnew lf f = do
- k <- lf $ SIMCT $ simctx_next_k <+= 1
- q <- f k
- lf $ SIMCT $ simctx_map_k %= M.insert k (either KRName KRInst q)
- return k
+ cnew f = do
+ k <- SIMCT $ simctx_next_ki_id <+= 1
+ q <- f (KI k)
+ SIMCT $ simctx_map_k %= IM.insert k (either KRName KRStruct q)
+ return (KI k)
instance (Show f, Monad m) => MCA (SIMCT m f) KI where
ccanon k = SIMCT $ key_canon k
vl <- key_lookup cl
vr <- key_lookup cr
vm <- unSIMCT $ f vl vr
- simctx_map_k %= M.insert cl (KRKey cr)
- simctx_map_k %= M.insert cr (either KRName KRInst vm)
+ simctx_map_k %= IM.insert (unKI cl) (KRKey cr)
+ simctx_map_k %= IM.insert (unKI cr) (either KRName KRStruct vm)
return cr
------------------------------------------------------------------------}}}
-- Context : Constructing Aliased Keys {{{
+aliasN :: forall f n k m .
+ (Monad m,
+ MCVT m k ~ ENKRI f n k,
+ MCN m k{-, MCNC k m -})
+ => n -> m k
+aliasN n = cnew $ const $ return $ Left n
+
aliasX :: forall f n k m .
(Monad m,
MCVT m k ~ ENKRI f n k,
- MCN m k, MCNC k m)
+ MCN m k{-, MCNC k m -})
=> VR f n k -> m k
-aliasX (VRName n) = cnew id $ const $ return $ Left n
+aliasX (VRName n) = aliasN n
aliasX (VRKey k) = return k
aliasX (VRStruct u) = aliasY u
aliasY :: forall f n k m .
(Monad m,
MCVT m k ~ ENKRI f n k,
- MCN m k, MCNC k m)
+ MCN m k{-, MCNC k m -})
=> InstF f (VR f n k) -> m k
aliasY u = T.sequence (fmap (liftM Right . aliasX) u)
- >>= cnew id . const . return . Right
+ >>= cnew . const . return . Right
+aliasV :: forall f n k m .
+ (Monad m,
+ MCVT m k ~ ENKRI f n k, MCN m k,
+ MCVT m DVar ~ VR f n k, MCR m DVar, MCW m DVar)
+ => DVar -> m k
+aliasV v = do
+ x <- clookup v
+ k <- aliasX x
+ cassign v $ VRKey k
+ return k
+
+kUpUniq :: (Ord f, n ~ NIX f, Monad m, MCVT m k ~ ENKRI f n k, MCM m k)
+ => Uniq -> k -> m k
+kUpUniq u0 k0 = cmerge go k0 u0 >> return k0
+ where
+ go (Left n) u = return $ Left $ nUpUniq u n
+ go a@(Right q) u = case iUniq q of
+ Nothing -> return a
+ Just u' | u' >= u -> return a
+ Just _ -> liftM Right $ (T.mapM (rec u) q)
+
+ rec u (Left n) = return $ Left $ nUpUniq u n
+ rec u (Right k) = kUpUniq u k >> return (Right k)
{-
-- | Called when we are moving a singleton alias key to unaliased structure.
-- Context : User Variables {{{
user_lookup :: (MonadState (SIMCtx f) m, Show f)
- => VV
+ => DVar
-> m (VR f (NIX f) KI)
user_lookup v = do
m <- use simctx_map_v
- r <- maybe (error $ "User variable context miss: " ++ (show v))
- return
- $ M.lookup v m
- XT.traceShow ("VL",v,r) $ return ()
+ let r = maybe (dynacPanicStr $ "User variable context miss: " ++ (show v))
+ id
+ $ M.lookup v m
+ -- XT.traceShow ("VL",v,r) $ return ()
return r
-type instance MCVT (SIMCT m f) VV = VR f (NIX f) KI
+type instance MCVT (SIMCT m f) DVar = VR f (NIX f) KI
-instance (Show f, Monad m) => MCR (SIMCT m f) VV where
+instance (Show f, Monad m) => MCR (SIMCT m f) DVar where
clookup = SIMCT . user_lookup
-instance (Show f, Monad m) => MCW (SIMCT m f) VV where
+instance (Show f, Monad m) => MCW (SIMCT m f) DVar where
cassign v w = SIMCT $ simctx_map_v %= M.insert v w
-instance (Show f, Monad m) => MCA (SIMCT m f) VV where
+instance (Show f, Monad m) => MCA (SIMCT m f) DVar where
ccanon x = return x
calias f l r = SIMCT $ do
simctx_map_v %= M.insert r x'
return l
+{-
+user_variable_death :: (MonadState (SIMCtx f) m, Show f) => DVar -> m ()
+user_variable_death v = do
+ m <- use simctx_map_v
+ let r = maybe (dynacPanicStr $ "Dying variable not in context: " ++ (show v))
+ id
+ $ M.lookup v m
+-}
+
+
+------------------------------------------------------------------------}}}
+-- Context : Transformers {{{
+
+-- These instances are used internally to allow us to wrap our workers with
+-- different utility parameters.
+
+type instance MCVT (CMTR.ReaderT r (SIMCT m f)) k = MCVT (SIMCT m f) k
+
+instance (MCA (SIMCT m f) k) => MCA (CMTR.ReaderT r (SIMCT m f)) k where
+ ccanon k = lift (ccanon k)
+
+ calias f k1 k2 = CMTR.ask >>= \e ->
+ lift (calias (\a b -> CMTR.runReaderT (f a b) e) k1 k2)
+
+instance (MCM (SIMCT m f) k) => MCM (CMTR.ReaderT r (SIMCT m f)) k where
+ cmerge f k v = CMTR.ask >>= \e ->
+ lift (cmerge (\a b -> CMTR.runReaderT (f a b) e) k v)
+
+instance (MCN (SIMCT m f) k) => MCN (CMTR.ReaderT r (SIMCT m f)) k where
+ cnew f = CMTR.ask >>= \e ->
+ lift (cnew (\a -> CMTR.runReaderT (f a) e))
+
+instance (MCR (SIMCT m f) k) => MCR (CMTR.ReaderT r (SIMCT m f)) k where
+ clookup k = lift (clookup k)
+
+instance (MCW (SIMCT m f) k) => MCW (CMTR.ReaderT r (SIMCT m f)) k where
+ cassign k v = lift (cassign k v)
+
------------------------------------------------------------------------}}}
------------------------------------------------------------------------}}}
-- Haddock Sections {{{
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
-module Dyna.Analysis.Mode.Execution.NoAliasContext (
+module Dyna.Analysis.Mode.Execution.ContextNoAlias (
-- * Inst Types
-- ** Naming Conventions
-- $naming
-- ** Variables
- VR(..), vrToNIX,
+ VR(..),
-- ** Monad
SIMCT(..), runSIMCT,
SIMCtx(..), emptySIMCtx, allFreeSIMCtx,
) where
+import Control.Applicative (Applicative)
-- import Control.Exception(assert)
import Control.Lens
-- import Control.Monad
pretty (VRName n) = PP.pretty n
pretty (VRStruct y) = IP.compactly PP.pretty PP.pretty y
+{-
-- This is used during rule analysis to capture the state of the binding
-- chart into the generated DOpAMine.
--
vrToNIX :: (Show f) => VR f (NIX f) -> NIX f
vrToNIX (VRName n) = n
vrToNIX (VRStruct i) = nHide $ fmap vrToNIX i
+-}
------------------------------------------------------------------------}}}
-- Context {{{
$(makeLenses ''SIMCtx)
newtype SIMCT m f a = SIMCT { unSIMCT :: StateT (SIMCtx f) (EitherT UnifFail m) a }
- deriving (Monad,MonadFix)
+ deriving (Monad,MonadFix,Functor,Applicative)
instance (Monad m) => MonadError UnifFail (SIMCT m f) where
throwError e = SIMCT (lift (left e))
emptySIMCtx :: SIMCtx f
emptySIMCtx = SIMCtx M.empty
+-- XXX make take S.Set DVar?
allFreeSIMCtx :: [DVar] -> SIMCtx f
allFreeSIMCtx fs = SIMCtx $ M.fromList $ map (\x -> (x, VRStruct IFree)) fs
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall #-}
-module Dyna.Analysis.Mode.Execution.Functions {-(
- -- * Named inst functions
- -- nWellFormed, nGround, nLeq, nLeqGLB, nSub, nSubGLB, nSubLUB,
+module Dyna.Analysis.Mode.Execution.Functions (
+ -- * Expansion
+ expandV, -- expandSharedV,
-- * Unification
- unifyVV, unifyUnaliasedNV,
+ unifyVV, unifyUnaliasedNV, unifyVF,
+ -- * Ordering
+ leqVV,
-- * Matching,
subVN,
-- * Modes
- doCall, mWellFormed
-)-} where
+ doCall,
+ -- * Misc
+ leqXX, -- leqMXX,
+) where
import Control.Applicative
-import Control.Exception
+-- import Control.Exception
import Control.Lens
import Control.Monad.Error.Class
-import Control.Monad.State
-import Control.Monad.Trans.Either
-import Control.Monad.Trans.RWS
+import Control.Monad.Reader
+-- import Control.Monad.Reader.Class
+-- import Control.Monad.State
+-- import Control.Monad.Trans.Either
+-- import Control.Monad.Trans.Maybe
+-- import Control.Monad.Trans.RWS
-- import Data.Functor.Identity
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 qualified Data.Maybe as MA
+-- import qualified Data.Set as S
+-- import qualified Data.Traversable as T
import Dyna.Analysis.Mode.Execution.Context
import Dyna.Analysis.Mode.Execution.NamedInst
import Dyna.Analysis.Mode.Inst
import Dyna.Analysis.Mode.Mode
import Dyna.Analysis.Mode.Unification
import Dyna.Analysis.Mode.Uniq
+import Dyna.Main.Exception
+import Dyna.Term.TTerm
+import Dyna.XXX.DataUtils
import Dyna.XXX.MonadContext
-import Dyna.XXX.MonadUtils
-import qualified Debug.Trace as XT
+-- import Dyna.XXX.MonadUtils
+
+-- import qualified Debug.Trace as XT
+ts :: Show a => a -> b -> b
+ts = const id -- XT.traceShow
------------------------------------------------------------------------}}}
--- Unification {{{
+-- Variable Expansion {{{
+
+type ExpC m f n k = (Ord f, Show f, Functor m,
+ Monad m,
+ MCVT m k ~ ENKRI f n k, MCR m k,
+ n ~ NIX f)
+
+-- | Deeply extract from the context as per definition 5.3.3, p95
+expandV :: (ExpC m f n k, MCVT m DVar ~ VR f n k, MCR m DVar)
+ => DVar -> m n
+expandV v = clookup v >>= \x ->
+ case x of
+ VRName n -> return n
+ VRStruct y -> expandY y
+ VRKey k -> clookup k
+ >>= either return (expandY . q2y)
+ where
+ expandY y = nDeep rec y
+ 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
--- | Constraints common to all unification functions
-type UnifCtxC m f n = (Ord f, Show f,
- Monad m, MonadError UnifFail m,
- n ~ NIX f)
+------------------------------------------------------------------------}}}
+-- Leq {{{
+
+type LeqC m f n k = (Ord f, Show f, Show k,
+ Monad m,
+ MCVT m k ~ ENKRI f n k, MCR m k,
+ n ~ NIX f)
+
+leqVV :: (LeqC m f n k,
+ MCVT m DVar ~ VR f n k, MCR m DVar)
+ => DVar -> DVar -> m Bool
+leqVV vl vr = do
+ xl <- clookup vl
+ xr <- clookup vr
+ leqXX xl xr
+
+-- | Compare two variable recursions, without write-back side-effects.
+--
+-- This is the direct lifting of NoContextFunctions.leqXX to the aliasing
+-- case. It is emphatically not definition 5.3.6, p96. (See 'leqMXX').
+--
+-- I am not sure this is useful, but it is written mostly as a warm-up.
+--
+-- XXX We should be testing that this is equivalent to expandV-ing both and
+-- calling nLeq, but that depends on us having the ability to generate
+-- interesting contexts.
+leqXX :: (LeqC m f n k)
+ => VR f n k -> VR f n k -> m Bool
+leqXX (VRName nl) (VRName nr) = leqNN nl nr
+leqXX (VRName nl) (VRStruct yr) = leqNY nl yr
+leqXX (VRName nl) (VRKey kr) = leqNK nl kr
+leqXX (VRStruct yl) (VRName nr) = leqYN yl nr
+leqXX (VRStruct yl) (VRStruct yr) = leqYY yl yr
+leqXX (VRStruct yl) (VRKey kr) = leqYK yl kr
+leqXX (VRKey kl) (VRName nr) = leqKN kl nr
+leqXX (VRKey kl) (VRStruct yr) = leqKY kl yr
+leqXX (VRKey kl) (VRKey kr) = leqKK kl kr
+
+leqKK :: (LeqC m f n k) => k -> k -> m Bool
+leqKK kl kr = do
+ el <- clookup kl
+ er <- clookup kr
+ case (el, er) of
+ (Left nl, Left nr) -> leqNN nl nr
+ (Left nl, Right qr) -> leqNQ nl qr
+ (Right ql, Left nr) -> leqQN ql nr
+ (Right ql, Right qr) -> leqQQ ql qr
+
+leqKN :: (LeqC m f n k) => k -> n -> m Bool
+leqKN kl nr = clookup kl >>= either (flip leqNN nr) (flip leqQN nr)
+
+leqNK :: (LeqC m f n k) => n -> k -> m Bool
+leqNK nl kr = clookup kr >>= either (leqNN nl) (leqNQ nl)
+
+leqKY :: (LeqC m f n k) => k -> InstF f (VR f n k) -> m Bool
+leqKY kl yr = clookup kl >>= either (flip leqNY yr) (flip leqQY yr)
+
+leqYK :: (LeqC m f n k) => InstF f (VR f n k) -> k -> m Bool
+leqYK yl kr = clookup kr >>= either (leqYN yl) (leqYQ yl)
+
+-- | Split J on right
+-- leqNJ :: (LeqC m f n k) => NIX f -> Either n k -> m Bool
+-- leqNJ nl = either (leqNN nl) (leqNK nl)
+
+-- leqXJ :: (LeqC m f n k) => VR f n k -> Either n k -> m Bool
+-- leqXJ xl jr = either (leqXX xl . VRName) (leqXX xl . VRKey) jr
+
+-- leqJI :: (LeqC m f n k) => Either n k -> InstF f n -> m Bool
+-- leqJI jl ir = either (\nl -> leqNN nl (nHide ir))
+-- (\kl -> leqKN kl (nHide ir))
+-- jl
+
+-- | Split J on left
+-- leqJN :: (LeqC m f n k) => Either n k -> n -> m Bool
+-- leqJN jl nr = either (flip leqNN nr) (flip leqKN nr) jl
+
+-- leqJX :: (LeqC m f n k) => Either n k -> VR f n k -> m Bool
+-- leqJX jl xr = either (flip leqXX xr . VRName) (flip leqXX xr . VRKey) jl
+
+-- leqJY :: (LeqC m f n k) => Either n k -> InstF f (VR f n k) -> m Bool
+-- leqJY jl yr = either (flip leqNY yr) (flip leqKY yr) jl
+
+-- | Induction hypothesis NY
+--
+-- Note that the induction on this branch is funny: if the 'InstF' is not
+-- recursive, we immediately bail out to name-on-name comparison with
+-- 'nShallow', rather than expanding the named inst with 'nExpose'. Since
+-- the right hand side is not getting smaller in such a case, the latter
+-- strategy would lead divergence.
+leqNY :: (LeqC m f n k) => n -> InstF f (VR f n k) -> m Bool
+leqNY nl (nShallow -> Just nr) = leqNN nl nr
+leqNY nl yr = iLeq_ leqNY leqNX (nExpose nl) yr
+
+-- | Induction hypothesis YN
+--
+-- Induction is similarly funny as in 'leqNY'
+leqYN :: (LeqC m f n k) => InstF f (VR f n k) -> n -> m Bool
+leqYN (nShallow -> Just nl) nr = leqNN nl nr
+leqYN yl nr = iLeq_ leqXI leqXN yl (nExpose nr)
--- | Constraints for unification on keyed insts
-type UnifCtxKC m f n k = (MCVT m k ~ ENKRI f n k, MCM m k)
+-- | Induction hypothesis YY
+leqYY :: (LeqC m f n k) => InstF f (VR f n k) -> InstF f (VR f n k) -> m Bool
+leqYY = iLeq_ leqXY leqXX
--- | Name-on-Name unification, which computes a new name for the result.
--- We assume that the sources will be updated by the caller, if
--- applicable (e.g. 'unifyNK').
-unifyNN :: UnifCtxC m f n
- => Bool -> n -> n -> m n
-unifyNN l a b =
- either throwError return $ (if l then nLeqGLBRL else nLeqGLBRD) a b
+-- | Repackage Y as X and invoke generic dispatch. Despite the growth of
+-- the RHS, this is guaranteed to then step to one of the induction
+-- hypotheses, which will reduce both sides.
+leqXY :: (LeqC m f n k) => VR f n k -> InstF f (VR f n k) -> m Bool
+leqXY xl yr = leqXX xl (VRStruct yr)
-unifyVV :: (UnifCtxC m f n, UnifCtxKC m f n k,
- MCVT m VV ~ VR f n k, MCA m VV)
- => Bool -> VV -> VV -> m VV
-unifyVV l vl vr = calias (unifyXX l) vl vr
+leqXI :: (LeqC m f n k) => VR f n k -> InstF f n -> m Bool
+leqXI xl ir = leqXX xl (VRName $ nHide ir)
--- |
---
--- Note that the caller is required to do whatever is necessary to ensure
--- that the resulting 'VR' is interpreted in an aliased context going
--- forward. That is, we expect to be called by 'calias'.
-unifyXX :: (UnifCtxC m f n, UnifCtxKC m f n k)
- => Bool -> VR f n k -> VR f n k -> m (VR f n k)
-unifyXX l (VRName na) (VRName nb) = liftM VRName $ unifyNN l na nb
-unifyXX l (VRName na) (VRKey kb) = liftM VRKey $ unifyNK l na kb
-unifyXX l (VRKey ka) (VRName nb) = liftM VRKey $ unifyNK l nb ka
+leqXN :: (LeqC m f n k) => VR f n k -> n -> m Bool
+leqXN xl nr = leqXX xl (VRName nr)
+
+-- leqXQ :: (LeqC m f n k) => VR f n k -> InstF f (Either n k) -> m Bool
+-- leqXQ xl qr = leqXX xl (VRStruct $ q2y qr)
+
+-- | Repackage N as X and invoke generic dispatch.
+leqNX :: (LeqC m f n k) => NIX f -> VR f n k -> m Bool
+leqNX nl xr = leqXX (VRName nl) xr
+-- | Repackage Q
+leqNQ :: (LeqC m f n k) => n -> InstF f (Either n k) -> m Bool
+leqNQ nl qr = leqNY nl (q2y qr)
+
+leqQN :: (LeqC m f n k) => InstF f (Either n k) -> n -> m Bool
+leqQN ql nr = leqYN (q2y ql) nr
+
+leqQY :: (LeqC m f n k) => InstF f (Either n k) -> InstF f (VR f n k) -> m Bool
+leqQY ql yr = leqYY (q2y ql) yr
+
+leqYQ :: (LeqC m f n k) => InstF f (VR f n k) -> InstF f (Either n k) -> m Bool
+leqYQ yl qr = leqYY yl (q2y qr)
+
+leqQQ :: (LeqC m f n k) => InstF f (Either n k) -> InstF f (Either n k) -> m Bool
+leqQQ ql qr = leqYY (q2y ql) (q2y qr)
+
+-- | Induction base case NN
+leqNN :: (Ord f, Monad m) => NIX f -> NIX f -> m Bool
+leqNN nl nr = return $ nLeq nl nr
+
+------------------------------------------------------------------------}}}
+-- LeqM {{{
{-
-unifyXX l (VRName na) (VRStruct ub) = do
- kb <- aliasY ub
- unifyNK l na kb
-unifyXX l (VRKey ka) (VRName nb) = unifyNK l nb ka
-unifyXX l (VRKey ka) (VRKey kb) = unifyKK l ka kb
-unifyXX l (VRKey ka) (VRStruct ub) = do
- kb <- aliasY ub
- unifyKK l ka kb
-unifyXX l (VRStruct ua) (VRName nb) = do
- ka <- aliasY ua
- unifyNK l nb ka
-unifyXX l (VRStruct ua) (VRKey kb) = do
- ka <- aliasY ua
- unifyKK l ka kb
-unifyXX l (VRStruct ua) (VRStruct ub) = do
- ka <- aliasY ua
- kb <- aliasY ub
- unifyKK l ka kb
--}
+type LeqMC m f n k = (Ord f, Show f, Show k,
+ Monad m,
+ MCVT m k ~ ENKRI f n k, MCR m k, MCM m k,
+ n ~ NIX f)
+
--- | Name-on-Key unification. This updates the key's bindings and leaves
--- the name alone (we assume that the source of the name will be updated
--- by the caller, if applicable)
+-- | Apply a leq constraint to the binding state
--
--- This function returns the key given as a convenient shorthand.
-unifyNK l n k = cmerge (unifyEE l UUnique) k (Left n) >> return k
-
--- | Unify two already-aliased bits of structure, returning an inst key
--- arbitrarily. Any additional aliases encountered will, of course,
--- also be updated as a result.
-unifyKK _ a b | a == b = return a
-unifyKK l a b = calias (unifyEE l UUnique) a b
-
--- | The guts of key-on-key unification; this expects to be called in a
--- context where the keys which produced the input will be suitably
--- rewritten (i.e. by 'calias' or 'cmerge')
-unifyEE :: forall f k m n .
- (UnifCtxC m f n, UnifCtxKC m f n k)
- => Bool
- -> Uniq
- -> ENKRI f n k
- -> ENKRI f n k
- -> m (ENKRI f n k)
-unifyEE l u (Left na) (Left nb) = liftM (Left . nUpUniq u) $ unifyNN l na nb
-unifyEE l u (Right ia) (Right ib) =
- either throwError (return . Right) =<<
- (if l then iLeqGLBRL_ else iLeqGLBRD_)
- (reUniqJ) (reUniqJ)
- (undefined)
- (undefined)
- (undefined)
- UUnique ia ib
-
-lsuQJ l u q (Left n) = unifyEE l u (Right q) (nExpose n)
-
-stepJ :: (n ~ NIX f, Monad m, MCVT m k ~ ENKRI f n k, MCR m k)
- => Either n k -> m (ENKRI f n k)
-stepJ (Left n) = return $ Left n
-stepJ (Right k) = either (return . Left) (return . Right) =<< clookup k
-
-reUniqJ :: (Ord f, n ~ NIX f, Monad m, MCVT m k ~ ENKRI f n k, MCM m k)
- => Uniq -> Either n k -> m (Either n k)
-reUniqJ u (Left n) = return (Left (nUpUniq u n))
-reUniqJ u0 (Right k) = cmerge mf k u0 >> return (Right k)
- where
- mf (Left n) u = return (Left (nUpUniq u n))
- mf (Right i) u = liftM Right $
- T.sequence $ over inst_rec (fmap (fmap (reUniqJ u)))
- $ over inst_uniq (max u) i
+-- See definition 5.3.6, p96
+--
+-- Notice that leqM is defined in terms of unification to handle aliasing.
+-- It further may fail if its second argument is an alias key while its
+-- first argument is not.
+--
+-- Annoyingly enough, the thesis is exceptionally unclear here; dealing with
+-- the alias case seems to require that we rely on the comutativity of ⋏ .
+
+leqMXX :: (LeqMC m f n k)
+ => VR f n k -> VR f n k -> MaybeT m Bool
+leqMXX (VRName nl) (VRName nr) = leqNN nl nr
+leqMXX (VRName nl) (VRStruct yr) = leqMNY nl yr
+leqMXX (VRName _ ) (VRKey _ ) = mzero
+leqMXX (VRStruct yl) (VRName nr) = leqMYN yl nr
+leqMXX (VRStruct yl) (VRStruct yr) = leqMYY yl yr
+leqMXX (VRStruct _ ) (VRKey _ ) = mzero
+leqMXX (VRKey kl) (VRName nr) = leqMKN kl nr
+leqMXX (VRKey kl) (VRStruct yr) = leqMKY kl yr
+-- leqMXX (VRKey kl) (VRKey kr) = leqMKK kl kr
+
+leqMKN :: (LeqMC m f n k) => VR f n k -> n -> MaybeT m Bool
+leqMKN kl nr = lift (cmerge unifyQN kl nr) >> return True
+
+leqMKY :: (LeqMC m f n k) => k -> InstF f (VR f n k) -> MaybeT m Bool
+leqMKY kl yr = lift (cmerge unifyQY kl yr) >> return True
+
+-- | Induction hypothesis NY
+leqMNY :: (LeqMC m f n k) => n -> InstF f (VR f n k) -> MaybeT m Bool
+leqMNY nl (nShallow -> Just nr) = leqNN nl nr
+leqMNY nl ir = iLeq_ leqMNY leqMNX (nExpose nl) ir
+
+-- | Induction hypothesis YN
+leqMYN :: (LeqMC m f n k) => InstF f (VR f n k) -> n -> MaybeT m Bool
+leqMYN (nShallow -> Just nl) nr = leqNN nl nr
+leqMYN yl nr = iLeq_ leqMXI leqMXN yl (nExpose nr)
+
+leqMXI :: (LeqMC m f n k) => VR f n k -> InstF f n -> MaybeT m Bool
+leqMXI xl ir = leqMXX xl (VRName $ nHide ir)
+
+-- | Induction hypothesis YY
+leqMYY :: (LeqMC m f n k)
+ => InstF f (VR f n k)
+ -> InstF f (VR f n k)
+ -> MaybeT m Bool
+leqMYY = iLeq_ leqMXY leqMXX
+
+leqMNX :: (LeqMC m f n k) => n -> VR f n k -> MaybeT m Bool
+leqMNX nl xr = leqMXX (VRName nl) xr
+
+leqMXN :: (LeqMC m f n k) => VR f n k -> n -> MaybeT m Bool
+leqMXN xl nr = leqMXX xl (VRName nr)
+
+-- | Repackage Y as X
+leqMXY :: (LeqMC m f n k) => VR f n k -> InstF f (VR f n k) -> MaybeT m Bool
+leqMXY xl yr = leqMXX xl (VRStruct yr)
+
+leqMQY :: (LeqMC m f n k) => InstF f (Either n k) -> InstF f (VR f n k) -> MaybeT m Bool
+leqMQY ql yr = leqMYY (q2y ql) yr
-{-
-{-
-unifyNE :: forall f k m n .
- ( Eq k, Ord f, Ord n, Show f, n ~ NIX f
- , Monad m, MCVT m k ~ ENKRI f n k, MCA m k, MCM m k )
- => Bool -> n -> ENKRI f n k ->
-}
+------------------------------------------------------------------------}}}
+-- Unification {{{
-unifyNK :: forall f k m n .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k)
- => Bool
- -> n
- -> k
- -> m k
-unifyNK l n k = cmerge (unifyEE l) k (Left n) >> return k
-
-unifyEE :: forall f k m n .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k)
- => Bool
- -> ENKRI f n k
- -> ENKRI f n k
- -> m (ENKRI f n k)
-unifyEE l (Left na) (Left nb) = liftM Left $ unifyNN l na nb
-unifyEE l (Left na) (Right qb) = do
- ia <- clookup na
- when (not l) $ semidet_clobbered_unify ia qb >>= flip when (fail "UEE NQ SCU")
- liftM Right $ iLeqGLB_ (return . Left) return
- (\n j -> unifyJJ l (Left n) j) ia qb
-unifyEE l (Right qa) (Left nb) = do
- ib <- clookup nb
- when (not l) $ semidet_clobbered_unify qa ib >>= flip when (fail "UEE QN SCU")
- liftM Right $ iLeqGLB_ return (return . Left)
- (\j n -> unifyJJ l j (Left n)) qa ib
-unifyEE l (Right qa) (Right qb) = liftM Right $ unifyQQ l qa qb
-
-unifyQQ :: forall f k m n .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k)
- => Bool
- -> KRI f n k
- -> KRI f n k
- -> m (KRI f n k)
-unifyQQ l qa qb = do
- when (not l) $ semidet_clobbered_unify qa qb >>= flip when (fail "UQQ QQ SCU")
- iLeqGLB_ return return (unifyJJ l) qa qb
-
-unifyJJ :: forall f k m n .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k)
- => Bool
- -> Either n k
- -> Either n k
- -> m (Either n k)
-unifyJJ l (Left na) (Left nb) = liftM Left $ unifyNN l na nb
-unifyJJ l (Left na) (Right kb) = liftM Right $ unifyNK l na kb
-unifyJJ l (Right ka) (Left nb) = liftM Right $ unifyNK l nb ka
-unifyJJ l (Right ka) (Right kb) = liftM Right $ unifyKK l ka kb
-
--- | Unify two already-aliased bits of structure, returning an inst key
--- arbitrarily. Any additional aliases will, of course, also be updated as
--- a result.
-unifyKK :: (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k)
- => Bool
- -> k
- -> k
- -> m k
-unifyKK _ a b | a == b = return a
-unifyKK l a b = XT.traceShow ("UKK",a,b) $ calias (unifyEE l) a b
-
--- | The core of unifyVV, this function operates on two user variable
--- bindings. When it encounters an unaliased reference it will promote
--- it to aliased and then continue unification, deleting the unaliased
--- inputs.
-unifyXX :: forall f k m n .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCD m k, MCM m k, MCN m k)
- => Bool
- -> VR f n k
- -> VR f n k
- -> m k
-unifyXX l (VRName na) (VRName nb) = unifyNN l na nb
- >>= cnew . const . return . Left
-unifyXX l (VRName na) (VRKey kb) = unifyNK l na kb
-unifyXX l (VRName na) (VRStruct ub) = do
- kb <- aliasY ub
- unifyNK l na kb
-unifyXX l (VRKey ka) (VRName nb) = unifyNK l nb ka
-unifyXX l (VRKey ka) (VRKey kb) = unifyKK l ka kb
-unifyXX l (VRKey ka) (VRStruct ub) = do
- kb <- aliasY ub
- unifyKK l ka kb
-unifyXX l (VRStruct ua) (VRName nb) = do
- ka <- aliasY ua
- unifyNK l nb ka
-unifyXX l (VRStruct ua) (VRKey kb) = do
- ka <- aliasY ua
- unifyKK l ka kb
-unifyXX l (VRStruct ua) (VRStruct ub) = do
- ka <- aliasY ua
- kb <- aliasY ub
- unifyKK l ka kb
+-- | Constraints common to all unification functions
+type UnifC m f n = (Ord f, Show f,
+ Monad m, MonadError UnifFail m,
+ MonadReader UnifParams m,
+ n ~ NIX f)
+
+-- | Constraints for unification on keyed insts
+type UnifKC m f n k = (Show k,
+ MCVT m k ~ ENKRI f n k, MCR m k,
+ MCA m k, MCM m k, MCN m k{-, MCNC k m-})
-- | Variable-on-variable unification. Ah, finally.
--
--
-- XXX We probably do not handle free-free unification correctly, in light
-- of §5.4.1. For the moment, I am skipping this.
-unifyVV :: forall f k m n v .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCD m k, MCM m k, MCN m k,
- MCVT m v ~ VR f n k, MCA m v)
- => (v -> Bool)
- -> v
- -> v
- -> m v
-unifyVV lf va vb =
- calias (\a' b' -> liftM VRKey $ unifyXX (lf va || lf vb) a' b') va vb
+unifyVV :: (UnifC m f n, UnifKC m f n k,
+ MCVT m DVar ~ VR f n k, MCA m DVar)
+ => DVar -> DVar -> m DVar
+unifyVV vl vr = calias (\a b -> liftM VRKey $ unifyXX UUnique a b) vl vr
+
+-- | Unaliased-ply unification. Notice that the result is always an alias
+-- key.
+unifyXX :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> VR f n k -> VR f n k -> m k
+unifyXX u xa xb = ts ("UXX",u,xa,xb) $ unifyXX_ u xa xb
+unifyXX_ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> VR f n k -> VR f n k -> m k
+unifyXX_ u (VRName na) (VRName nb) = unifyNN u na nb >>= aliasN
+unifyXX_ u (VRName na) (VRKey kb) = unifyKN u kb na
+unifyXX_ u (VRName na) (VRStruct yb) = aliasY yb >>= flip (unifyKN u) na
+unifyXX_ u (VRKey ka) (VRName nb) = unifyKN u ka nb
+unifyXX_ u (VRKey ka) (VRKey kb) = unifyKK u ka kb
+unifyXX_ u (VRKey ka) (VRStruct yb) = aliasY yb >>= unifyKK u ka
+unifyXX_ u (VRStruct ya) (VRName nb) = aliasY ya >>= flip (unifyKN u) nb
+unifyXX_ u (VRStruct ya) (VRKey kb) = aliasY ya >>= unifyKK u kb
+unifyXX_ u (VRStruct ya) (VRStruct yb) = aliasY ya >>= \ka ->
+ aliasY yb >>= unifyKK u ka
+
+-- | Aliased-ply unification.
+--
+-- Note that the caller is required to do whatever is necessary to ensure
+-- that the resulting 'KR' is interpreted in an aliased context going
+-- forward. That is, we expect to be called by 'calias'.
+unifyEE :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> ENKRI f n k -> ENKRI f n k -> m (ENKRI f n k)
+unifyEE u (Left na) (Left nb) = liftM Left $ unifyNN u na nb
+unifyEE u (Left na) (Right qb) = unifyNQ u na qb
+unifyEE u (Right qa) (Left nb) = unifyNQ u nb qa
+unifyEE u (Right qa) (Right qb) = liftM Right $ unifyQQ u qa qb
+
+unifyEQ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> ENKRI f n k -> KRI f n k -> m (ENKRI f n k)
+unifyEQ u (Left na) qb = unifyNQ u na qb
+unifyEQ u (Right qa) qb = liftM Right $ unifyQQ u qa qb
+
+unifyJJ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> Either n k -> Either n k -> m (Either n k)
+unifyJJ u (Left na) (Left nb) = liftM Left $ unifyNN u na nb
+unifyJJ u (Left na) (Right kb) = liftM Right $ unifyKN u kb na
+unifyJJ u (Right ka) (Left nb) = liftM Right $ unifyKN u ka nb
+unifyJJ u (Right ka) (Right kb) = liftM Right $ unifyKK u ka kb
+
+unifyJQ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> Either n k -> KRI f n k -> m (Either n k)
+unifyJQ u (Left na) qb = unifyNQ' u na qb
+unifyJQ u (Right ka) qb = unifyKQ u ka qb
+
+jUpUniq :: (UnifC m f n, UnifKC m f n k) => Uniq -> Either n k -> m (Either n k)
+jUpUniq u = either (return . Left . nUpUniq u) (liftM Right . kUpUniq u)
+
+unifyKK :: (UnifC m f n, UnifKC m f n k) => Uniq -> k -> k -> m k
+unifyKK u = calias (unifyEE u)
+
+unifyKN :: (UnifC m f n, UnifKC m f n k) => Uniq -> k -> n -> m k
+unifyKN u ka nb = do
+ ea <- clookup ka
+ ts ("UKN",u,ka,ea,nb) $ unifyKN_ u ka nb
+unifyKN_ :: (UnifC m f n, UnifKC m f n k) => Uniq -> k -> n -> m k
+unifyKN_ u ka nb = cmerge (\a b -> unifyEE u a (Left b)) ka nb >> return ka
+
+unifyKQ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> k -> KRI f n k -> m (Either n k)
+unifyKQ u ka qb = cmerge (\a b -> unifyEQ u a b) ka qb >> return (Right ka)
+
+-- | Induction hypothesis QN
+unifyNQ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> n -> KRI f n k -> m (ENKRI f n k)
+unifyNQ u na (nShallow -> Just nb) = liftM Left $ unifyNN u na nb
+unifyNQ u na qb = selUnifI >>= \f ->
+ f (\u' n' -> return $ Left $ nUpUniq u' n')
+ jUpUniq
+ (\u' q' n' -> unifyNQ' u' n' q')
+ (\u' i' j' -> either (liftM Left . unifyNN u' (nHide i'))
+ (liftM Right . flip (unifyKN u') (nHide i'))
+ j')
+ (\u' n' j' -> either (liftM Left . unifyNN u' n')
+ (liftM Right . flip (unifyKN u) n')
+ j')
+ u (nExpose na) qb
+ >>= either throwError (return . Right)
+
+unifyNQ' :: (UnifC m f n, UnifKC m f n k)
+ => Uniq -> n -> KRI f n k -> m (Either n k)
+unifyNQ' u n q = unifyNQ u n q
+ >>= either (return . Left)
+ (liftM Right . cnew . const . return . Right)
+
+-- | Induction hypothesis QQ
+unifyQQ :: (UnifC m f n, UnifKC m f n k)
+ => Uniq
+ -> KRI f n k
+ -> KRI f n k
+ -> m (KRI f n k)
+unifyQQ u ya yb = selUnifI >>= \f ->
+ f jUpUniq jUpUniq fJQ fJQ unifyJJ u ya yb
+ >>= either throwError return
+ where
+ fJQ u' q' j' = unifyJQ u' j' q'
+-- | Name-on-Name unification, which computes a new name for the result.
+-- We assume that the sources will be updated by the caller, if
+-- applicable (e.g. 'unifyNK').
+unifyNN :: UnifC m f n => Uniq -> n -> n -> m n
+unifyNN u a b = do
+ f <- selUnifN
+ either throwError (return . nUpUniq u) $ f a b
+
+-- | Select between two functions based on our unification parameters.
+selUnif_ :: (Monad m, MonadReader UnifParams m)
+ => a -> a -> m a
+selUnif_ l d = do
+ live <- view up_live
+ fake <- view up_fake
+ return $ if live && not fake then l else d
+
+-- | Select between two 'NIX' unifications based on unification parameters.
+selUnifN :: (Ord f, Show f,
+ Monad m, MonadReader UnifParams m)
+ => m (NIX f -> NIX f -> Either UnifFail (NIX f))
+selUnifN = selUnif_ nLeqGLBRL nLeqGLBRD
+
+selUnifI :: (Ord f,
+ Monad m, MonadReader UnifParams m)
+ => m (TyILeqGLB_ f m i i' o (m (Either UnifFail (InstF f o))))
+selUnifI = selUnif_ iLeqGLBRL_ iLeqGLBRD_
-- | Name-on-Variable unification. This should not be called on names
-- looked up from the context, as that would omit important updates to the
-- This function returns the variable given as a convenient shorthand.
--
-- Based on figure 5.7, p 104.
-unifyUnaliasedNV :: forall f k m n v .
- (Eq k, Ord f, Show k, n ~ NIX f,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k,
- MCVT m v ~ VR f n k, MCR m v, MCW m v)
- => Bool
- -> n
- -> v
- -> m v
-unifyUnaliasedNV l n0 v0 = do
+unifyUnaliasedNV :: forall f k m n .
+ (UnifC m f n, UnifKC m f n k, Applicative m,
+ MCVT m DVar ~ VR f n k, MCR m DVar, MCW m DVar)
+ => n
+ -> DVar
+ -> m DVar
+unifyUnaliasedNV n0 v0 = do
x0 <- clookup v0
- xu <- unifyNX n0 x0
+ xu <- naUnifyNX UUnique n0 x0
cassign v0 xu
return v0
where
- unifyNX :: n -> VR f n k -> m (VR f n k)
- unifyNX na (VRName nb) = liftM VRName $ unifyNN l na nb
- unifyNX na (VRKey kb) = liftM VRKey $ unifyNK l na kb
- unifyNX na (VRStruct ub) = liftM VRStruct $ unifyNY na ub
-
- unifyNY :: n -> InstF f (VR f n k) -> m (InstF f (VR f n k))
- unifyNY na ub = do
- ia <- clookup na
- when (not l) $ semidet_clobbered_unify ia ub >>= flip when (fail "UNU SCU")
- iLeqGLB_ (return . VRName) return unifyNX ia ub
--}
+ naUnifyNX :: Uniq -> n -> VR f n k -> m (VR f n k)
+ naUnifyNX u na (VRName nb) = liftM VRName $ unifyNN u na nb
+ naUnifyNX u na (VRKey kb) = liftM VRKey $ unifyKN u kb na
+ naUnifyNX u na (VRStruct ub) = naUnifyNY u na ub
+
+ -- Induction hypothesis NY
+ naUnifyNY :: Uniq -> n -> InstF f (VR f n k) -> m (VR f n k)
+ naUnifyNY u na (nShallow -> Just nb) = liftM VRName $ unifyNN u na nb
+ naUnifyNY u na yb = liftM VRStruct $
+ selUnifI >>= \f ->
+ f (\u' n' -> return $ VRName $ nUpUniq u' n')
+ xUpUniq
+ (\u' y' n' -> naUnifyNY u' n' y')
+ (\u' i' x' -> naUnifyNX u' (nHide i') x')
+ naUnifyNX
+ u (nExpose na) yb
+ >>= either throwError return
+
+ xUpUniq u (VRName n) = return $ VRName $ nUpUniq u n
+ xUpUniq u (VRKey k) = liftM VRKey $ kUpUniq u k
+ xUpUniq u (VRStruct y) = liftM VRStruct
+ $ liftM (over inst_uniq (max u))
+ $ inst_recps (xUpUniq u) y
+
+-- | Variable-on-Functor unification. In our case, since we walk over ANF,
+-- where every position has been given a name, we assume the outer functor
+-- recurses through a set of variables.
+--
+-- See definition 3.2.20, p53.
+unifyVF :: forall m m' f n k .
+ (Ord f, Monad m', m ~ SIMCT m' f, n ~ NIX f, Show f,
+ MCVT m k ~ ENKRI f n k,
+ MCVT m DVar ~ VR f n k)
+ => Bool -> (DVar -> m Bool) -> DVar -> f -> [DVar] -> m DVar
+unifyVF fake lf v f vs = do
+ vl <- lf v
+ vy <- clookup v
+ vys <- mapM clookup vs
+
+ let vvys = zip vs vys
+
+ -- Perform a dead unification of the variable's old inst and
+ -- bound(unique, f(...)). This gets us just the join on the lattice.
+ ki'' <- runReaderT (unifyXX UUnique vy (VRStruct $ IBound UUnique
+ (M.singleton f vys)
+ False))
+ (UnifParams False fake)
+
+ i'' <- clookup ki''
+
+ do
+ vy' <- expandV v
+ vys' <- mapM expandV vs
+ ts ("UVF1",i'',vy',vys') $ return ()
+
+ -- If we arrive here, unification was successful;
+ -- now, rip through the results and do the second unification pass.
+ (u,vks') <- case i'' of
+ Left n'' -> case nExpose n'' of
+ IBound u (M.toList -> [(f',ris)]) False | f == f' -> do
+ x <- go (\u_ n_ x_ -> unifyXX u_ (VRName n_) x_)
+ vl vvys u ris
+ return (u,x)
+ _ -> dynacPanicStr "unifyVF impossible NIX result"
+ Right (IBound u (M.toList -> [(f',ris)]) False) | f == f' -> do
+ x <- go (\u_ e_ x_ -> unifyXX u_ (e2x e_) x_)
+ vl vvys u ris
+ return (u,x)
+ _ -> dynacPanicStr "unifyVF impossible result"
+
+ -- And now one last unification
+ ki' <- runReaderT (unifyXX UUnique (VRKey ki'')
+ (VRStruct $ IBound u
+ (M.singleton f $ map VRKey vks')
+ False))
+ (UnifParams False fake)
+
+ cassign v (VRKey ki')
+ sequence_ $ zipWithTails (\v_ k_ -> cassign v_ (VRKey k_))
+ (\_ -> lenpanic)
+ (\_ -> lenpanic)
+ vs vks'
+
+ return v
+ where
+ go :: forall a b gm .
+ (gm ~ ReaderT UnifParams m)
+ => (Uniq -> a -> b -> gm k)
+ -> Bool -> [(DVar,b)] -> Uniq -> [a] -> m [k]
+ go uf vl vvys u ris = sequence $ zipWithTails
+ (\ri (v',oi) -> do
+ l <- lf v'
+ runReaderT (uf u ri oi)
+ (UnifParams (l && vl) fake))
+ (\_ -> lenpanic)
+ (\_ -> lenpanic)
+ ris vvys
+
+ lenpanic = dynacPanicStr "unifyVF length mismatch"
------------------------------------------------------------------------}}}
-- Matching {{{
+subVN :: forall f k m n .
+ (Ord f, Functor m, Monad m, n ~ NIX f, Show f,
+ MCVT m k ~ ENKRI f n k, MCR m k,
+ MCVT m DVar ~ VR f n k, MCR m DVar)
+ => DVar
+ -> n
+ -> m Bool
+subVN vl nr = expandV vl >>= \nl -> return $ nl `nSub` nr
+
{-
-subNN :: (Ord f, n ~ NI f, Monad m)
+ - An old version of matching that attempted to expand in place.
+ -
+type SubC m f n = (Ord f, Show f,
+ Monad m,
+ n ~ NIX f)
+
+-- | Constraints for unification on keyed insts
+type SubKC m f n k = (MCVT m k ~ ENKRI f n k, MCR m k)
+
+
+subNN :: (Ord f, n ~ NIX f, Monad m)
=> n -> n -> m Bool
-subNN a b = XT.traceShow ("SNN",a,b) $ return $ nSub a b
+subNN a b = return $ nSub a b
+
+subVN :: forall f k m n .
+ (SubC m f n, SubKC m f n k,
+ MCVT m DVar ~ VR f n k, MCR m DVar)
+ => DVar
+ -> n
+ -> m Bool
+subVN vl nr = do
+ xl <- clookup vl
+ case xl of
+ VRName nl -> subNN nl nr
+ VRKey kl -> undefined -- subKN uk n
+ VRStruct yl -> undefined -- subYN ui n
iCompare :: (Ord f, n ~ NI f)
=> (forall m' .
subNI :: forall f n m .
(Ord f, Show f, n ~ NI f, Monad m)
=> n -> InstF f n -> m Bool
-subNI n i = XT.traceShow ("SNI",n,i) $ do
+subNI n i = ts ("SNI",n,i) $ do
ni <- clookup n
return $ iCompare iSub_ ni i
(Ord f, n ~ NI f, Show f, Show k,
MCVT m k ~ ENKRI f n k, MCR m k)
=> KRI f n k -> InstF f n -> m Bool
-subQI q i = XT.traceShow ("SQI",q,i) $ iSub_ subJI subJN q i
+subQI q i = ts ("SQI",q,i) $ iSub_ subJI subJN q i
subQN :: forall f k m n .
(Ord f, n ~ NI f, Show f, Show k,
MCVT m k ~ ENKRI f n k, MCR m k)
=> KRI f n k -> n -> m Bool
-subQN q n = XT.traceShow ("SQN",q,n) $ do
+subQN q n = ts ("SQN",q,n) $ do
ni <- clookup n
subQI q ni
(Ord f, n ~ NI f, Show f, Show k,
MCVT m k ~ ENKRI f n k, MCR m k)
=> k -> n -> m Bool
-subKN k n = XT.traceShow ("SKN",k,n) $ do
+subKN k n = ts ("SKN",k,n) $ do
kq <- clookup k
(either subNN subQN kq) n
(Ord f, n ~ NI f, Show f, Show k,
MCVT m k ~ ENKRI f n k, MCR m k)
=> k -> InstF f n -> m Bool
-subKI k i = XT.traceShow ("SKI",k,i) $ do
+subKI k i = ts ("SKI",k,i) $ do
kq <- clookup k
(either subNI subQI kq) i
(Ord f, n ~ NI f, Show f, Show k,
MCVT m k ~ ENKRI f n k, MCR m k)
=> InstF f (VR f n k) -> InstF f n -> m Bool
-subYI y i = XT.traceShow ("SUI",y,i) $ do
+subYI y i = ts ("SUI",y,i) $ do
iSub_ subXI subXN y i
subXI :: forall f k m n .
(Ord f, n ~ NI f, Show f, Show k,
MCVT m k ~ ENKRI f n k, MCR m k)
=> VR f n k -> InstF f n -> m Bool
-subXI x i = XT.traceShow ("SXI",x,i) $ do
+subXI x i = ts ("SXI",x,i) $ do
case x of
VRName xn -> subNI xn i
VRKey xk -> subKI xk i
MCVT m n ~ InstF f n, MCR m n,
MCVT m k ~ ENKRI f n k, MCR m k)
=> VR f n k -> n -> m Bool
-subXN x n = XT.traceShow ("SXN",x,n) $ do
+subXN x n = ts ("SXN",x,n) $ do
case x of
VRName xn -> subNN xn n
VRKey xk -> subKN xk n
MCVT m n ~ InstF f n, MCR m n,
MCVT m k ~ ENKRI f n k, MCR m k)
=> InstF f (VR f n k) -> n -> m Bool
-subUN u n = XT.traceShow ("SUN",u,n) $ do
+subUN u n = ts ("SUN",u,n) $ do
ni <- clookup n
iSub_ subXI subXN u ni
-
-subVN :: forall f k m n v .
- (Ord n, Ord f, Show n, Show f, Show k, Show v,
- MCVT m n ~ InstF f n, MCR m n,
- MCVT m k ~ ENKRI f n k, MCR m k,
- MCVT m v ~ VR f n k, MCR m v)
- => v
- -> n
- -> m Bool
-subVN v n = XT.traceShow ("SVN",v,n) $ do
- vx <- clookup v
- case vx of
- VRName un -> subNN un n
- VRKey uk -> subKN uk n
- VRStruct ui -> subUN ui n
+-}
-- | Enact a particular call.
--
-- misread.
--
-- Based on Figure 5.7, p104
-doCall :: forall f k m n v .
- (Ord n, Ord f, Eq k,
- Show n, Show f, Show k, Show v,
- MonadPlus m, MonadFix m,
- MCVT m n ~ InstF f n, MCR m n, MCN m n,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k, MCR m k,
- MCVT m v ~ VR f n k, MCR m v, MCW m v)
- => (v -> Bool) -- Liveness predicate
- -> v -> [v] -- Call with these arguments
- -> QMode n -- Against this pattern
+doCall :: forall f k m m' n .
+ (m ~ SIMCT m' f, Monad m',
+ UnifC m f n, UnifKC m f n k)
+ => (DVar -> Bool) -- Liveness predicate
+ -> DVar -> [DVar] -- Call with these arguments
+ -> QMode n -- Against this pattern
-> m Bool
-doCall l r0 as0 (QMode cs0 (rmi,rmo)) = go (r0:as0) (rmi:map fst cs0)
+doCall l r0 as0 (QMode cs0 (rmi,rmo) _) = go (r0:as0) (rmi:map fst cs0)
where
go [] [] = goUnify as0 (rmo:map snd cs0)
- go (a:as) (c:cs) = andM (subVN a c) (go as cs)
+ go (a:as) (c:cs) = do
+ sub <- subVN a c
+ if sub
+ then go as cs
+ else throwError UFExDomain
go _ _ = return False
goUnify [] [] = return True
- goUnify (a:as) (c:cs) = unifyUnaliasedNV (l a) c a >> goUnify as cs
+ goUnify (a:as) (c:cs) = runReaderT (unifyUnaliasedNV c a)
+ (UnifParams (l a) True)
+ >> goUnify as cs
goUnify _ _ = return False
--}
------------------------------------------------------------------------}}}
-- Merging {{{
-- XXX Unimplemented
-
-------------------------------------------------------------------------}}}
--- Mode functions {{{
-
-{-
--- | Check that all names in a mode are indeed well-formed and that all
--- transitions are according to ≼.
-mWellFormed :: forall f . (Ord f) => QMode (NI f) -> Bool
-mWellFormed (QMode ats vm@(vti,vto)) =
- (all (nWellFormed UClobbered)
- $ vti:vto:concatMap (\(i,o) -> [i,o]) ats)
- &&
- (all (uncurry (flip nLeq)) $ vm:ats)
--}
-
-------------------------------------------------------------------------}}}
+-------------------------------------------------------------------------}}}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall #-}
-module Dyna.Analysis.Mode.Execution.NoAliasFunctions (
+module Dyna.Analysis.Mode.Execution.FunctionsNoAlias (
+ -- * Expansion
+ expandV,
-- * Unification
unifyVV, unifyVF, unifyUnaliasedNV,
-- * Matching,
-- import qualified Data.Maybe as MA
-- import qualified Data.Set as S
-- import qualified Data.Traversable as T
-import Dyna.Analysis.Mode.Execution.NoAliasContext
+import Dyna.Analysis.Mode.Execution.ContextNoAlias
import Dyna.Analysis.Mode.Execution.NamedInst
import Dyna.Analysis.Mode.Inst
import Dyna.Analysis.Mode.Mode
-- import Dyna.XXX.MonadUtils
-- import qualified Debug.Trace as XT
+------------------------------------------------------------------------}}}
+-- Variable Expansion {{{
+
+type ExpC m f n = (Ord f, Show f,
+ Monad m, Functor m,
+ n ~ NIX f)
+
+expandV :: (ExpC m f n, MCVT m DVar ~ VR f n, MCR m DVar)
+ => DVar -> m n
+expandV v = clookup v >>= \x -> case x of
+ VRName n -> return n
+ VRStruct y -> nDeep rec y
+ where
+ rec (VRName n) = return (Left n)
+ rec (VRStruct y) = return (Right y)
+
------------------------------------------------------------------------}}}
-- Leq {{{
module Dyna.Analysis.Mode.Execution.NamedInst (
-- * Datatype definition
NIX(..), NIXM,
- -- * Well-formedness predicates
- nWellFormedUniq, nWellFormedOC,
-- * Unary functions
- nNotEmpty, nGround, nUpUniq, nExpose, nHide, nShallow,
- -- * Unary functions on internals
+ -- ** Well-formedness predicates
+ nWellFormedUniq, nWellFormedOC,
+ -- ** Inquiries
+ nAllNotEmpty, nSomeNotEmpty, nGround, nUpUniq,
+ -- ** Construction
+ nHide, nShallow, nDeep,
+ -- ** Destruction
+ nExpose,
+ -- ** Internals
nPrune,
-- * Binary comparators
nCmp, nEq, nLeq, nSub,
-- Utilities {{{
-- | Throw exception if ever a NIX is not well formed
---
--- XXX Should attempt to do something with the 'NIX' passed in!
panicwf :: NIX f -> a
panicwf n = dynacPanic (text "NIX not well-formed"
`above` indent 2 (pretty n))
-- | 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).
---
--- Additionally, each position in the inst may have only one Uniq value
--- on any path that reaches it.
nWellFormedUniq :: forall f . (Show f) => Uniq -> NIX f -> Bool
nWellFormedUniq u0 n0@(NIX i0 m) = evalState (iWellFormed_ q u0 i0)
M.empty
do
cached <- gets (M.lookup a)
case cached of
- Nothing -> do
- id %= M.insert a u
- eml n0 (return . nWellFormedUniq u)
- (iWellFormed_ q u)
- m a
- Just u' -> return $ u == u'
+ Nothing -> rec
+ -- If we've been here before, it's OK if we are coming in
+ -- more uniquely. If we are coming in less uniquely (i.e.
+ -- with a greater Uniq), then we need to recurse through
+ -- this binding again.
+ Just u' -> orM1 (u <= u') rec
+ where
+ rec = do
+ id %= M.insert a u
+ eml n0 (return . nWellFormedUniq u)
+ (iWellFormed_ q u)
+ m a
-- | Check that a named inst is acyclic.
--
-- 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).
-nNotEmpty :: forall f . NIX f -> Bool
-nNotEmpty n0@(NIX i0 m0) = evalState (visit i0) S.empty
+nSomeNotEmpty :: forall f . NIX f -> Bool
+nSomeNotEmpty = fix (nNotEmpty_core orAny)
+ where orAny b bs = b `orM1` (anyM bs)
+
+-- | Like 'nNotEmpty' 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 `orM1` (anyM $ M.foldr (\fas a -> allM (map rec fas) : a) [] m)
-
- rec idx = do
- already <- gets (S.member idx)
- already `orM1` eml n0 (return . nNotEmpty)
- (\v -> modify (S.insert idx) >> visit v) m0 idx
-
+ 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)
-- | Increase the nonuniqueness of a particular named inst to at least the
-- given level.
--
--- This is equivalent to unification with 'IANy' at the given 'Uniq' level,
--- but may be slightly more efficient than actually performing that work.
+-- 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
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
+
+
------------------------------------------------------------------------}}}
-- Binary predicates {{{
InstF(..), inst_uniq, inst_rec, inst_recps,
iNotReached, iIsNotReached,
iUniq, iIsFree, iWellFormed_, iEq_, iGround_,
- iLeq_, iLeqGLB_,
+ iLeq_, iLeqGLB_, TyILeqGLB_,
iSub_, iSubGLB_, iSubLUB_,
) where
-- XXX Ought to assert that length is == length is'
{-# INLINABLE iLeq_ #-}
+-- | The type of iLeqGLB_, given a name so that we can reuse it elsewhere.
+--
+-- Note that not all parameters are free -- @r@ is typically @m' (InstF f
+-- i'')@ for some 'Monad' @m'@ built up in terms of @m@, but the lack of
+-- type lambdas forces us to resort to passing the whole type in.
+type TyILeqGLB_ f m i i' i'' r =
+ (Uniq -> i -> m i'') -- ^ Import left
+ -> (Uniq -> i' -> m i'') -- ^ Import right
+ -> (Uniq -> InstF f i' -> i -> m i'') -- ^ Lopsided merge left
+ -> (Uniq -> InstF f i -> i' -> m i'') -- ^ Lopsided merge right
+ -> (Uniq -> i -> i' -> m i'') -- ^ Simultaneous Merge
+ -> Uniq -- ^ Uniq of outer context
+ -> InstF f i -- ^ Left
+ -> InstF f i' -- ^ Right
+ -> r
+
+
-- | Compute the GLB under iLeq_ (⋏) at a particular uniqueness.
--
-- The uniqueness input is needed for the case when we unify with a free
-- tests that are restrictive but safe (such as shallow testing for free
-- variables).
-iLeqGLB_ :: (Monad m, Ord f)
- => (Uniq -> i -> m i'') -- ^ Import left
- -> (Uniq -> i' -> m i'') -- ^ Import right
- -> (Uniq -> InstF f i' -> i -> m i'') -- ^ Lopsided merge left
- -> (Uniq -> InstF f i -> i' -> m i'') -- ^ Lopsided merge right
- -> (Uniq -> i -> i' -> m i'') -- ^ Simultaneous Merge
- -> Uniq -- ^ Uniq of outer context
- -> InstF f i -- ^ Left
- -> InstF f i' -- ^ Right
- -> m (InstF f i'')
+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
-- | A Query Mode is a collection of instantiation transducers.
--
+-- Note that 'QMode's do not carry the name of the functor with which they
+-- are associated; that should be maintained elsewhere and probably passed
+-- around as a pair. (Or maybe we should revisit this decision, XXX)
+--
-- This is a surrogate for defn 3.1.10 (p34) which avoids the need to name
-- variables in a query. Many of the well-formedness conditions fall away,
-- but the subsumption test does not; see 'mWellFormed'
--
-- XXX In the same way that 'InstF' will need generalization when we replace
-- our mode system, so will this.
+--
+-- XXX This needs to addtionally indicate whether answers are concentrated
+-- or diffuse (and possibly diffuse with which aggregator, or aggregators if
+-- we want to go nuts -- consider @f(1) += ...@ @f(2) max= ...@ -- these
+-- heads do not unify but are subsumed by @f(free>>ground)@.), if they are
+-- returned in sorted order (but whose sorted order?), ...
data QMode n = QMode
{ _qmode_args :: [(n,n)]
, _qmode_result :: (n,n)
import Test.Framework
import qualified Dyna.Analysis.Mode.Selftest.NamedInst as NI
+import qualified Dyna.Analysis.Mode.Selftest.Contexts as C
-selftest = testGroup "Dyna.Analysis.Mode.Selftest" [ NI.selftest ]
+selftest :: Test
+selftest = testGroup "Dyna.Analysis.Mode.Selftest"
+ [ NI.selftest
+ , C.selftest
+ ]
--- /dev/null
+---------------------------------------------------------------------------
+-- | Tests for context and unification functions.
+
+-- Header material {{{
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Dyna.Analysis.Mode.Selftest.Contexts where
+
+import Control.Monad.Reader
+import Data.Functor.Identity
+import qualified Data.Map as M
+import qualified Dyna.Analysis.Mode.Execution.Context as CA
+import qualified Dyna.Analysis.Mode.Execution.ContextNoAlias as CNA
+import qualified Dyna.Analysis.Mode.Execution.Functions as FA
+import qualified Dyna.Analysis.Mode.Execution.FunctionsNoAlias as FNA
+import Dyna.Analysis.Mode.Execution.NamedInst
+import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Selftest.NamedInst
+import Dyna.Analysis.Mode.Selftest.Term
+import Dyna.Analysis.Mode.Unification
+import Dyna.Analysis.Mode.Uniq
+import qualified Test.Framework as TF
+import Test.Framework.Providers.QuickCheck2
+import Test.QuickCheck.Property as QCP
+import Test.Framework.TH
+
+------------------------------------------------------------------------}}}
+-- Utility Functions {{{
+
+
+unifProp filter test gold i1 i2 =
+ filter i1 && filter i2 QCP.==>
+ case (test i1 i2, gold i1 i2) of
+ (Left t , Left g ) -> t == g
+ (Right t, Right g) -> nEq t g
+ (_, _) -> False
+
+------------------------------------------------------------------------}}}
+-- Tests {{{
+
+prop_alias_unifyUnaliasedNV :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_alias_unifyUnaliasedNV = unifProp nWFN' alias_unifyUnaliasedNV nLeqGLBRL
+ where
+ alias_unifyUnaliasedNV n1 n2 =
+ fmap fst $ runIdentity
+ $ flip CA.runSIMCT (CA.allFreeSIMCtx [v])
+ $ flip runReaderT (UnifParams True False)
+ $ do
+ FA.unifyUnaliasedNV n1 v
+ FA.unifyUnaliasedNV n2 v
+ FA.expandV v
+ where v = "A"
+
+prop_alias_unify :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_alias_unify = unifProp nWFN' alias_unify nLeqGLBRL
+ where
+ alias_unify n1 n2 =
+ fmap fst $ runIdentity
+ $ flip CA.runSIMCT (CA.allFreeSIMCtx [vA,vB])
+ $ flip runReaderT (UnifParams True False)
+ $ do
+ FA.unifyUnaliasedNV n1 vA
+ FA.unifyUnaliasedNV n2 vB
+ FA.unifyVV vA vB
+ FA.expandV vA
+ where vA = "A"
+ vB = "B"
+
+
+-- | Check that a fake unifyVF ascribes to the lattice unification.
+--
+-- We cannot (easily) test real unifications as unifyVF makes a combination
+-- of dead and live unifications that do not map onto the lattice functions.
+prop_alias_unifyVF :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_alias_unifyVF = unifProp nWFN' alias_unifyVF gold
+
+gold n1 n2 = nLeqGLBRD n1 (nHide $ IBound UUnique
+ (M.singleton G [n2])
+ False)
+
+alias_unifyVF n1 n2 =
+ fmap fst $ runIdentity
+ $ flip CA.runSIMCT (CA.allFreeSIMCtx [vA,vB])
+ $ do
+ flip runReaderT (UnifParams True False) $ do
+ FA.unifyUnaliasedNV n1 vA
+ FA.unifyUnaliasedNV n2 vB
+ FA.unifyVF True (const $ return True) vA G [vB]
+ FA.expandV vA
+ where
+ vA = "A"
+ vB = "B"
+
+------------------------------------------------------------------------}}}
+-- Harness Toplevel {{{
+
+selftest :: TF.Test
+selftest = $(testGroupGenerator)
+
+main :: IO ()
+main = $(defaultMainGenerator)
+
+------------------------------------------------------------------------}}}
import Test.Framework.Providers.QuickCheck2
import Test.Framework.TH
import Test.QuickCheck
-import Test.QuickCheck.Property
+import Test.QuickCheck.Property as QCP
+import Test.SmallCheck as SC
+import Test.SmallCheck.Series as SCS
import qualified Debug.Trace as XT
-}
nWFU = nWellFormedUniq UUnique
+nWFN n = nWFU n && nSomeNotEmpty n
+nWFN' n = nWFU n && nAllNotEmpty n
+
+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.
-prop_nPrune_Eq :: Property
-prop_nPrune_Eq = forAll arbNIX (\i -> nWFU i ==> i `nEq` (nPrune i))
+prop_nPrune_Eq :: QCP.Property
+prop_nPrune_Eq = QCP.forAll (arbNIX UUnique) (\i -> nWFU i QCP.==> i `nEq` (nPrune i))
+
+-- | Check 'nMinimize'
+-- prop_nMinimize_Eq :: Bool -> QCP.Property
+-- prop_nMinimize_Eq b = QCP.forAll arbNIX
+-- (\i -> nWFU i QCP.==> i `nEq` (nMinimize b i))
-- | This property also checks that we don't generate crazy NIX
-- (such as we used to before the 'resize' call above in 'arbNIXME').
--
-- Notice that this holds regardless of the well-formedness requirements
-- on insts' recursion, since 'nEq' does not actually check them.
-prop_nEq_refl :: NIX TestFunct -> Property
+prop_nEq_refl :: NIX TestFunct -> QCP.Property
prop_nEq_refl i = property $ i `nEq` i
+{-
+scprop_nEq_refl :: (Monad m) => SC.Property m
+scprop_nEq_refl = SC.forAll $ \(i :: NIX TestFunct) -> i `nEq` i
+-}
+
-- XXX These tests are a little more time consuming and possibly not worth
-- the time to run all the time.
-prop_nLeq_refl :: NIX TestFunct -> Property
+prop_nLeq_refl :: NIX TestFunct -> QCP.Property
prop_nLeq_refl i = property $ i `nLeq` i
-prop_nLeq_asym :: NIX TestFunct -> NIX TestFunct -> Property
-prop_nLeq_asym i j = i `nLeq` j && j `nLeq` i ==> i `nEq` j
+prop_nLeq_asym :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_nLeq_asym i j = i `nLeq` j && j `nLeq` i QCP.==> i `nEq` j
-prop_nSub_refl :: NIX TestFunct -> Property
+prop_nSub_refl :: NIX TestFunct -> QCP.Property
prop_nSub_refl i = property $ i `nSub` i
-prop_nSub_asym :: NIX TestFunct -> NIX TestFunct -> Property
-prop_nSub_asym i j = i `nSub` j && j `nSub` i ==> i `nEq` j
+prop_nSub_asym :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_nSub_asym i j = i `nSub` j && j `nSub` i QCP.==> i `nEq` j
-- Check well-formedness of outputs of various binary functions
-prop_nLeqGLB_WF :: NIX TestFunct -> NIX TestFunct -> Property
-prop_nLeqGLB_WF i1 i2 = nWFU i1 && nWFU i2 ==> nWFU (nLeqGLB i1 i2)
+prop_nLeqGLB_WF :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_nLeqGLB_WF i1 i2 = nWFU i1 && nWFU i2 QCP.==> nWFU (nLeqGLB i1 i2)
-prop_nSubGLB_WF :: NIX TestFunct -> NIX TestFunct -> Property
-prop_nSubGLB_WF i1 i2 = nWFU i1 && nWFU i2 ==> nWFU (nSubGLB i1 i2)
+prop_nSubGLB_WF :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_nSubGLB_WF i1 i2 = nWFU i1 && nWFU i2 QCP.==> nWFU (nSubGLB i1 i2)
--- prop_nSubLUB_WF :: NIX TestFunct -> NIX TestFunct -> Property
+-- prop_nSubLUB_WF :: NIX TestFunct -> NIX TestFunct -> QCP.Property
-- prop_nSubLUB_WF i1 i2 = nWFU i1 && nWFU i2
--- ==> maybe True nWFU $ nSubLUB i1 i2
+-- QCP.==> maybe True nWFU $ nSubLUB i1 i2
-- Check edge-cases of various binary forms: given inputs ordered by their
-- lattice, these functions return something isomorphic to the appropriate
-- input.
-prop_nLeqGLB_Edge :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nLeqGLB_Edge :: NIX TestFunct -> NIX TestFunct -> QCP.Property
prop_nLeqGLB_Edge i1 i2 = i1 `nLeq` i2 && nWFU i1 && nWFU i2
- ==> nLeqGLB i1 i2 `nEq` i1
+ QCP.==> nLeqGLB i1 i2 `nEq` i1
-prop_nSubGLB_Edge :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nSubGLB_Edge :: NIX TestFunct -> NIX TestFunct -> QCP.Property
prop_nSubGLB_Edge i1 i2 = i1 `nSub` i2 && nWFU i1 && nWFU i2
- ==> nSubGLB i1 i2 `nEq` i1
+ QCP.==> nSubGLB i1 i2 `nEq` i1
--- prop_nSubLUB_Edge :: NIX TestFunct -> NIX TestFunct -> Property
+-- prop_nSubLUB_Edge :: NIX TestFunct -> NIX TestFunct -> QCP.Property
-- prop_nSubLUB_Edge i1 i2 = i1 `nSub` i2 && nWFU i1 && nWFU i2
--- ==> maybe False (nEq i2) $ nSubLUB i1 i2
+-- QCP.==> maybe False (nEq i2) $ nSubLUB i1 i2
-- Note that we return False above since the `nSub` constraint
-- should mean that nSubLUB is being called within its domain.
-- Check that the output of a binary function obeys the lattice ordering
-prop_nLeqGLB_is_LB :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nLeqGLB_is_LB :: NIX TestFunct -> NIX TestFunct -> QCP.Property
prop_nLeqGLB_is_LB i1 i2 = nWFU i1 && nWFU i2
- ==> let i = nLeqGLB i1 i2
+ QCP.==> let i = nLeqGLB i1 i2
in property $ i `nLeq` i1 && i `nLeq` i2
-prop_nLeqGLB_is_G :: NIX TestFunct -> NIX TestFunct -> NIX TestFunct -> Property
+prop_nLeqGLB_is_G :: NIX TestFunct -> NIX TestFunct -> NIX TestFunct -> QCP.Property
prop_nLeqGLB_is_G i1 i2 i3 = nWFU i1 && nWFU i2 && nWFU i3
- ==> let i = nLeqGLB i1 i2
- in i3 `nLeq` i1 && i3 `nLeq` i2 ==> property $ i3 `nLeq` i
+ QCP.==> let i = nLeqGLB i1 i2
+ in i3 `nLeq` i1 && i3 `nLeq` i2 QCP.==> property $ i3 `nLeq` i
-prop_nSubGLB_is_LB :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nSubGLB_is_LB :: NIX TestFunct -> NIX TestFunct -> QCP.Property
prop_nSubGLB_is_LB i1 i2 = nWFU i1 && nWFU i2
- ==> let i = nSubGLB i1 i2
+ QCP.==> let i = nSubGLB i1 i2
in property $ i `nSub` i1 && i `nSub` i2
-prop_nSubGLB_is_G :: NIX TestFunct -> NIX TestFunct -> NIX TestFunct -> Property
+prop_nSubGLB_is_G :: NIX TestFunct -> NIX TestFunct -> NIX TestFunct -> QCP.Property
prop_nSubGLB_is_G i1 i2 i3 = nWFU i1 && nWFU i2 && nWFU i3
- ==> let i = nSubGLB i1 i2
- in i3 `nSub` i1 && i3 `nSub` i2 ==> property $ i3 `nSub` i
+ QCP.==> let i = nSubGLB i1 i2
+ in i3 `nSub` i1 && i3 `nSub` i2 QCP.==> property $ i3 `nSub` i
-- prop_nSubLUB_is_UB :: NIX TestFunct -> NIX TestFunct -> Property
-- prop_nSubLUB_is_UB i1 i2 = nWFU i1 && nWFU i2
--- ==> maybe (property rejected)
+-- QCP.==> maybe (property rejected)
-- (\i -> property $ i1 `nSub` i && i2 `nSub` i)
-- $ nSubLUB i1 i2
-- tell us that we first check that the incoming variables are all ⊑ the
-- input half of the mode, then unify the input variables with the output
-- half of the mode. We know that the output half is ≼ the input half.
-prop_call_test_sufficient :: NIX TestFunct -> NIX TestFunct -> Property
-prop_call_test_sufficient i1 i2 = nWFU i1 && nWFU i2
- && nNotEmpty i1 && nNotEmpty i2
- && nSub i1 i2
- ==> nNotEmpty (nLeqGLB i1 i2)
+prop_call_test_sufficient :: NIX TestFunct -> NIX TestFunct -> QCP.Property
+prop_call_test_sufficient i1 i2 = nWFN i1 && nWFN i2 && nSub i1 i2
+ QCP.==> nWFN (nLeqGLB i1 i2)
selftest :: TF.Test
selftest = moreTries 10000 $ moreTests 400 $(testGroupGenerator)
+---------------------------------------------------------------------------
+-- | Test generators for Inst reasoning.
+
+-- Header material {{{
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Dyna.Analysis.Mode.Selftest.Term where
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.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
+
+------------------------------------------------------------------------}}}
+-- Misc {{{
+
+-- XXX Is this in the library anywhere?
+fe :: (Bounded a, Enum a) => [a]
+fe = enumFrom minBound
+
+-- XXX Goes upstream to quickcheck?
+arbitrarySetBEO :: forall a . (Bounded a, Enum a, Ord a) => Gen (S.Set a)
+arbitrarySetBEO = do
+ pres <- mapM (\_ -> arbitrary) (fe :: [a])
+ let mf = zipWith (\p f -> if p then Just f else Nothing) pres fe
+ return $ S.fromList $ MA.catMaybes mf
+
+-- XXX Goes upstream to smallcheck?
+serBoundedEnum :: forall a m . (Bounded a, Enum a, Monad m) => Series m a
+serBoundedEnum = foldr1 (\/) $ map cons0 fe
+
+-- XXX Goes upstream to smallcheck?
+serSetBEO :: forall a m . (Bounded a, Enum a, Ord a, Monad m) => Series m (S.Set a)
+serSetBEO = do
+ -- 'liftM not' needed so that we generate smaller sets first
+ pres <- mapM (\_ -> liftM not series) (fe :: [a])
+ let mf = zipWith (\p f -> if p then Just f else Nothing) pres fe
+ return $ S.fromList $ MA.catMaybes mf
+
+------------------------------------------------------------------------}}}
+-- Uniq {{{
-- XXX orphan instance
instance Arbitrary Uniq where arbitrary = arbitraryBoundedEnum
+-- XXX orphan instance
+instance (Monad m) => Serial m Uniq where series = serBoundedEnum
+
+arbUniq :: Uniq -> Gen Uniq
+arbUniq u = oneof $ map return [u..]
+
+------------------------------------------------------------------------}}}
+-- Closed-world functor {{{
+
+-- | The convention here is that these are F/0, G/1, H/2.
data TestFunct = F | G | H
deriving (Bounded,Enum,Eq,Ord,Show)
+genArgs :: (Monad m) => m i -> TestFunct -> m [i]
+genArgs _ F = return []
+genArgs g G = g >>= return . (\x -> [x])
+genArgs g H = do { i <- g; j <- g; return [i,j] }
+
+genFuncMap :: forall i m . (Monad m)
+ => m (S.Set TestFunct) -> m i -> m (M.Map TestFunct [i])
+genFuncMap stf gi = do
+ -- 'liftM S.toList' keeps us from generating lists containing
+ -- the same functor more than once.
+ fs :: [TestFunct] <- liftM S.toList stf
+ foldM (\m f -> genArgs gi f >>= return . flip (M.insert f) m)
+ M.empty
+ (L.nub fs)
+
+------------------------------------------------------------------------}}}
+-- Term: QuickCheck Generators {{{
+
instance Arbitrary TestFunct where arbitrary = arbitraryBoundedEnum
+instance Arbitrary (S.Set TestFunct) where arbitrary = arbitrarySetBEO
+
+-- | Generate an arbitrary, well-formed NIX at some uniqueness.
+arbNIX rootU = do
+ n <- sized (\s -> choose (1::Int,max 1 s)) -- How many plies?
+
+ let nl = [1..n]
-arbFuncMap :: forall i . Gen i -> Gen (M.Map TestFunct [i])
-arbFuncMap gi = do
- fs :: [TestFunct] <- arbitrary
- foldM (\m f -> genArgs f >>= return . flip (M.insert f) m) M.empty (L.nub fs)
+ uniqs <- vectorOf n (arbUniq rootU) -- Generate some uniques
+ -- that are all plausible
+ -- recursion candidates
+
+ let spares = zip [minBound.. ] [n+1 ..]
+
+ -- For each recursion site, pick a plausible recursor
+ let igen u = oneof $ map (return.snd) $ filter ((== u) . fst)
+ $ (zip uniqs nl ++ spares)
+
+ plies <- mapM (flip arbNIXME 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
where
- genArgs :: TestFunct -> Gen [i]
- genArgs F = pure []
- genArgs G = vectorOf 1 gi
- genArgs H = vectorOf 2 gi
-
-arbInstPly :: forall i . Gen i -> Gen (InstF TestFunct i)
-arbInstPly n = frequency [ (1,pure IFree)
- , (1,IAny <$> arbitrary)
- , (1,IUniv <$> arbitrary)
- , (3,IBound <$> arbitrary
- <*> sized (\s -> resize (s`div`2)
- $ arbFuncMap n)
- <*> arbitrary)
- ]
-
--- | Generate an Arbitrary 'NIXM' Entry (i.e. either a closed NIX automata
--- or a ply)
-arbNIXME :: forall f i . (f ~ TestFunct)
- => Gen i -> Gen (Either (NIX f) (InstF f i))
-arbNIXME igen = oneof [Left <$> sized (\s -> resize (s`div`2) arbitrary)
- ,Right <$> arbInstPly igen]
-
-arbNIX = do
+ arbInstPly :: forall i . Uniq -> (Uniq -> Gen i) -> Gen (InstF TestFunct i)
+ arbInstPly u n = frequency
+ [ (1,pure IFree)
+ , (1,IAny <$> arbUniq u)
+ , (1,IUniv <$> arbUniq u)
+ , (3,do
+ u' <- arbUniq u
+ IBound <$> pure u'
+ <*> sized (\s -> resize (s`div`2)
+ $ genFuncMap arbitrary (n u'))
+ <*> 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 = 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 (arbNIXME igen) -- Generate plies or recurse
+ plies <- vectorOf n (arbNIXMENWF igen) -- Generate plies or recurse
let m = M.fromList $ zip nl plies -- Make the map
- root <- arbInstPly igen -- The root
+ root <- arbInstPlyNWF igen -- The root
return $ NIX root m
+ where
+ arbInstPlyNWF :: forall i . Gen i -> Gen (InstF TestFunct i)
+ arbInstPlyNWF n = frequency
+ [ (1,pure IFree)
+ , (1,IAny <$> arbitrary)
+ , (1,IUniv <$> arbitrary)
+ , (3,IBound <$> arbitrary
+ <*> sized (\s -> resize (s`div`2)
+ $ 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
+ arbitrary = nPrune <$> arbNIX UUnique
shrink n@(NIX r m) = (MA.maybeToList noRecN) ++ subautomata
where
-- Pull out all the subautomata
subautomata = E.lefts (M.elems m)
+
+------------------------------------------------------------------------}}}
+-- Term: SmallCheck Generators {{{
+
+-- XXX These are buggy (they generate infinite, or at least "certainly too
+-- long" lists)
+
+{-
+instance (Monad m) => Serial m TestFunct where series = serBoundedEnum
+instance (Monad m) => Serial m (S.Set TestFunct) where series = serSetBEO
+
+serInstPly :: forall i m . (Monad m)
+ => Series m i
+ -> Series m (InstF TestFunct i)
+serInstPly n = cons0 IFree
+ \/ cons1 IAny
+ \/ cons1 IUniv
+ \/ (IBound <$> series
+ <*> genFuncMap series n
+ <*> series)
+
+serNIXME n = cons1 Left \/ (Right <$> serInstPly n)
+
+instance (Monad m) => Serial m (NIX TestFunct) where
+ series = do
+ SCS.Positive (n :: Int) <- series
+ let nl = [1..n]
+ let igen = generate (const nl)
+ plies <- mapM (\_ -> serNIXME igen) nl
+ let m = M.fromList $ zip nl plies
+ root <- serInstPly igen
+ return $ NIX root m
+-}
+
+------------------------------------------------------------------------}}}
-- The above fromJust calls are safe due to the 'iIsFree' guards.
{-# INLINABLE semidet_clobbered_unify #-}
-iLeqGLBRD_,iLeqGLBRL_
- :: (Monad m, Ord f)
- => (Uniq -> i -> m o)
- -> (Uniq -> i' -> m o)
- -> (Uniq -> InstF f i' -> i -> m o)
- -> (Uniq -> InstF f i -> i' -> m o)
- -> (Uniq -> i -> i' -> m o)
- -> Uniq
- -> InstF f i
- -> InstF f i'
- -> m (Either UnifFail (InstF f o))
+iLeqGLBRD_,iLeqGLBRL_ :: (Monad m, Ord f)
+ => TyILeqGLB_ f m i i' o (m (Either UnifFail (InstF f o)))
iLeqGLBRD_ il ir ml mr m u i1 i2 = do
io <- iLeqGLB_ il ir ml mr m u i1 i2
return $ if iIsNotReached io
import Dyna.Analysis.ANFPretty
import Dyna.Analysis.DOpAMine
import Dyna.Analysis.Mode
-import Dyna.Analysis.Mode.Execution.NoAliasContext
-import Dyna.Analysis.Mode.Execution.NoAliasFunctions
+import Dyna.Analysis.Mode.Execution.ContextNoAlias
+import Dyna.Analysis.Mode.Execution.FunctionsNoAlias
import Dyna.Term.TTerm
import Dyna.Term.Normalized
import Dyna.Main.Exception
(throwError UFExDomain))
(throwError UFExDomain)
-{-
- case i of
- NTVar v -> fup v (fup o (throwError UFExDomain)
-
--}
-
-- Structure building or unbuilding
--
-- XXX This ought to avail itself of unifyVF but doesn't.
mo = nHide (IUniv UShared)
unifyVU v = unifyUnaliasedNV mo v
mkMV v = do
- vi <- clookup v
- return $ MV v (vrToNIX vi) mo
+ vn <- expandV v
+ return $ MV v vn mo
ensureBound v = fgn v (throwError UFExDomain)
(return ())
-- representation of the term being updated, and
-- result variable.
-> SIMCtx DVar
- -- ^ Unbound variables in the rule
+ -- ^ Initial context (which must cover all the variables
+ -- in the given cruxes)
-> [(Cost, Actions fbs)]
-- ^ Plans and their costs
planner_ st sc cr mic ictx = runAgenda
---------------------------------------------------------------------------
-- | Class definitions for "context" monads.
+--
+-- This wants to be its own thing eventually.
-- Header material {{{
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
module Dyna.XXX.MonadContext(
- MCVT, MCA(..), MCD(..), MCF(..), MCM(..), MCNC, MCN(..), MCR(..), MCW(..),
+ MCVT, MCA(..), MCD(..), MCF(..), MCM(..), {- MCNC, -} MCN(..), MCR(..), MCW(..),
) where
-import GHC.Prim (Constraint)
+-- import GHC.Prim (Constraint)
-- import Control.Monad.Trans
-- import Control.Monad.Trans.Either
class (Monad m) => MCW m k where
cassign :: k -> MCVT m k -> m ()
--- | The monad @m@ is able to merge the assertion @k = v@ into
+-- | The monad @m@ is able to merge the assertion @k = b@ into
-- its context, provided a mechanism to merge values.
+--
+-- Note that this is intended for the case when @k@ and @b@ are
+-- distinct types! In the case where variable aliasing is desired,
+-- use the 'calias' method instead.
class (Monad m) => MCM m k where
cmerge :: (MCVT m k -> b -> m (MCVT m k))
-> k -> b -> m ()
class (Monad m) => MCD m k where
cdelete :: k -> m (MCVT m k)
-{-
+-- | The monad @m@ is able to fabricate new keys given a function
+-- which can produce a value from a key.
class (Monad m) => MCN m k where
- -- XXX OLD FORM cnew :: (MCVT m k) -> m k
cnew :: (k -> m (MCVT m k)) -> m k
--}
+{-
type family MCNC k (m' :: * -> *) :: Constraint
-- | The monad @m@ is able to fabricate new keys given a function
class (Monad m) => MCN m k where
cnew :: (Monad m', MCNC k m')
=> (forall a . m a -> m' a) -> (k -> m' (MCVT m k)) -> m' k
+-}
-- | The monad @m@ is able to generate new entities of type @k@.
class (Monad m) => MCF m k where
projects / dyna2 / commitdiff