-- fly.
-- Header material {{{
+{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
-module Dyna.Analysis.Mode.Execution.Base (
+module Dyna.Analysis.Mode.Execution.Context (
-- * Inst Types
-- ** Naming Conventions
-- $naming
- -- ** Named Insts
- NI(..), ni_unique, ni_inst,
-- ** Inst Keys (§5.3.1, p94)
KI(..), KR(..), KRI, ENKRI,
- -- ** Unaliased Insts
- UI(..), UR,
-- ** Variables
VV(..), VR(..),
SIMCtx(..), emptySIMCtx,
-- ** Internal helper functions
- aliasW,
+ aliasX, aliasY,
)where
import Control.Exception(assert)
import Control.Lens
import Control.Monad
+import Control.Monad.Error.Class
import Control.Monad.State
-import Data.Function
+import Control.Monad.Trans.Either
+import Control.Monad.Trans.State
+-- import Data.Function
import qualified Data.Map as M
import qualified Data.Traversable as T
-import Data.Unique
+-- import Data.Unique
+import Dyna.Analysis.Mode.Execution.NamedInst
import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Unification
+import Dyna.Main.Exception
import Dyna.XXX.DataUtils
import Dyna.XXX.MonadContext
import qualified Debug.Trace as XT
+import qualified Text.PrettyPrint.Free as PP
------------------------------------------------------------------------}}}
-- Inst Types {{{
--- Insts: Named Insts {{{
-
--- | A named inst. These are used when we need recursive Insts. Notice
--- that they are only permitted to recurse as themselves. See prose, p60.
---
--- Our implementation relies on globally unique keys created by the runtime
--- system and the use of laziness to tie the knot. This allows them to be
--- garbage collected when no longer used and means that we do not have to
--- carry around another map in our context.
---
--- Despite this, we continue to provide 'MCR' and 'MCN' instances for named
--- insts, just for uniformity of calling code and ease of changing the
--- underlying representation.
-data NI f = NI { _ni_unique :: Unique
- , _ni_inst :: InstF f (NI f)
- }
-$(makeLenses ''NI)
-
--- | The 'Eq' instance here is for exact object equality.
-instance Eq (NI f) where
- (NI a _) == (NI b _) = a == b
-
-instance Ord (NI f) where
- compare = on compare _ni_unique
-
-instance Show (NI f) where
- show (NI u _) = "<NI h=" ++ (show $ hashUnique u) ++ ">"
-
-------------------------------------------------------------------------}}}
-- Insts: Inst Keys (§5.3.1, p94) {{{
-- | An aliased variable, also known as an Inst Key. See §5.3.1, p94.
------------------------------------------------------------------------}}}
-- Insts: Unaliased Insts {{{
+{-
-- | An unaliased variable. Again we use 'Int' internally for the moment.
newtype UI = UI { unUI :: Int } deriving (Eq,Num,Ord,Show)
-- 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 {{{
newtype VV = VV { unVV :: String } deriving (Eq,Ord,Show)
-- | Variables (and unaliased structure) bindings
-data VR n k u =
+data VR f n k =
-- | Defined named inst (unaliased)
VRName n
-- | Unaliased structure
- | VRStruct u
+ | VRStruct (InstF f (VR f n k))
-- | Aliased structure
| VRKey k
deriving (Eq,Ord,Show)
------------------------------------------------------------------------}}}
-- Context {{{
-- Context : Basics {{{
-data SIMCtx f = SIMCtx { {- _simctx_next_iv :: NI
- , _simctx_map_iv :: InstMap f NI NI
- , -}
- _simctx_next_k :: KI
- , _simctx_next_u :: UI
-
- , _simctx_map_k :: M.Map KI (KR f (NI f) KI)
- , _simctx_map_u :: M.Map UI (UR f (NI f) KI UI)
- , _simctx_map_v :: M.Map VV (VR (NI f) KI UI)
+
+-- | 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)
}
deriving (Show)
$(makeLenses ''SIMCtx)
-newtype SIMCT m f a = SIMCT { unSIMCT :: StateT (SIMCtx f) m a }
+newtype SIMCT m f a = SIMCT { unSIMCT :: StateT (SIMCtx f) (EitherT UnifFail m) a }
deriving (Monad,MonadFix)
-emptySIMCtx :: SIMCtx f
-emptySIMCtx = SIMCtx 0 0 M.empty M.empty M.empty
-
-runSIMCT :: SIMCT m f a -> SIMCtx f -> m (a, SIMCtx f)
-runSIMCT q x = runStateT (unSIMCT q) x
-
-------------------------------------------------------------------------}}}
--- Context : Named Insts {{{
-
-type instance MCVT (SIMCT m f) (NI f) = InstF f (NI f)
+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))
-instance (Monad m) => MCR (SIMCT m f) (NI f) where
- clookup (NI _ v) = SIMCT $ return v
-
-instance (MonadIO m) => MCN (SIMCT m f) (NI f) where
- cnew v = SIMCT $ do
- nu <- liftIO $ newUnique
- return $ NI nu v
+instance MonadIO m => MonadIO (SIMCT m f) where
+ liftIO m = SIMCT $ lift (liftIO m)
{-
--- For the old NI definition, which required another map; kept in case we
--- like that better. A little stale.
-
-instance (Monad m) => MCR (SIMCT m f) NI (InstF f NI) where
- clookup v = SIMCT $ get >>= return . imLookup v . view simctx_map_iv
-
-instance (Monad m) => MCN (SIMCT m f) NI (InstF f NI) where
- cnew v = SIMCT $ do
- k <- simctx_next_iv <+= 1
- simctx_map_iv %= imAssign k v
- return k
+ - XXX maybe
+
+instance (Monad m) => MonadState (SIMCtx f) (SIMCT m f) where
+ get = SIMCT get
+ put = SIMCT . get
+ state = SIMCT . state
+-}
-instance (Monad m) => MCW (SIMCT m f) NI (InstF f NI) where
- cassign v b = SIMCT $ simctx_map_iv %= (imAssign v b)
+emptySIMCtx :: SIMCtx f
+emptySIMCtx = SIMCtx 0 M.empty M.empty
-instance (Monad m) => MCF (SIMCT m f) NI where
- cfresh = SIMCT $ do
- x <- simctx_next_iv <+= 1
- return x
--}
+runSIMCT :: SIMCT m f a -> SIMCtx f -> m (Either UnifFail (a, SIMCtx f))
+runSIMCT q x = runEitherT (runStateT (unSIMCT q) x)
------------------------------------------------------------------------}}}
-- Context : Aliased Keys {{{
key_lookup :: (MonadState (SIMCtx f) m, Show f)
=> KI
- -> m (ENKRI f (NI f) KI)
+ -> m (ENKRI f (NIX f) KI)
key_lookup k = do
ck <- key_canon k
m <- use simctx_map_k
- let r = maybe (error $ "Key context miss: " ++ (show (k,ck)))
+ 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 ()
krenkri (KRName n) = Left n
krenkri (KRInst i) = Right i
-type instance MCVT (SIMCT m f) KI = ENKRI f (NI f) KI
+type instance MCVT (SIMCT m f) KI = ENKRI f (NIX f) KI
instance (Show f, Monad m) => MCR (SIMCT m f) KI where
clookup = SIMCT . key_lookup
krenkri (KRName n) = Left n
krenkri (KRInst i) = Right i
+type instance MCNC KI m = ()
instance (Show f, Monad m) => MCN (SIMCT m f) KI where
- cnew q = SIMCT $ do
- k <- simctx_next_k <+= 1
- simctx_map_k %= M.insert k (either KRName KRInst q)
+ 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
instance (Show f, Monad m) => MCA (SIMCT m f) KI where
return cr
------------------------------------------------------------------------}}}
--- Context : Unaliased {{{
-
-unaliased_lookup :: (MonadState (SIMCtx f) m, Show f)
- => UI
- -> m (UR f (NI f) KI UI)
-unaliased_lookup v = do
- m <- use simctx_map_u
- r <- maybe (error $ "Unaliased context miss: " ++ (show v))
- return
- $ M.lookup v m
- return r
-
-type instance MCVT (SIMCT m f) UI = UR f (NI f) KI UI
-
-instance (Show f, Monad m) => MCR (SIMCT m f) UI where
- clookup k = SIMCT $ do
- r <- unaliased_lookup k
- XT.traceShow ("UL",k) $ return r
-
-instance (Show f, Monad m) => MCW (SIMCT m f) UI where
- cassign v w = SIMCT $ simctx_map_u %= M.insert v w
-
-instance (Show f, Monad m) => MCD (SIMCT m f) UI where
- cdelete k = SIMCT $ do
- r <- unaliased_lookup k
- simctx_map_u %= M.delete k
- XT.traceShow ("UD",k,r) $ return r
-
-{-
-instance (Show f, Monad m) => MCM (SIMCT m f) UI where
- cmerge f k v = SIMCT $ do
- m <- use simctx_map_u
- maybe (error $ "User context miss in merge: " ++ (show k))
- (\v' -> do
- merged <- unSIMCT $ f v' v
- simctx_map_u .= M.insert k merged m)
- $ M.lookup k m
--}
+-- Context : Constructing Aliased Keys {{{
--- | Move an unaliased structure to the aliased table
-aliasW :: forall f n k u m .
+aliasX :: forall f n k m .
(Monad m,
- MCVT m u ~ UR f n k u,
- MCR m u, MCD m u,
MCVT m k ~ ENKRI f n k,
- MCN m k)
- => UR f n k u
- -> m k
-aliasW x = T.sequence (fmap (liftM Right . aliasX) x) >>= cnew . Right
+ MCN m k, MCNC k m)
+ => VR f n k -> m k
+aliasX (VRName n) = cnew id $ const $ return $ Left n
+aliasX (VRKey k) = return k
+aliasX (VRStruct u) = aliasY u
-aliasX :: forall f n k u m .
+aliasY :: forall f n k m .
(Monad m,
- MCVT m u ~ UR f n k u,
- MCR m u, MCD m u,
MCVT m k ~ ENKRI f n k,
- MCN m k)
- => VR n k u -> m k
-aliasX (VRName n) = cnew (Left n)
-aliasX (VRKey k) = return k
-aliasX (VRStruct u) = cdelete u >>= T.sequence . fmap (liftM Right . aliasX)
- >>= cnew . Right
+ 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
{-
-- | Called when we are moving a singleton alias key to unaliased structure.
user_lookup :: (MonadState (SIMCtx f) m, Show f)
=> VV
- -> m (VR (NI f) KI UI)
+ -> m (VR f (NIX f) KI)
user_lookup v = do
m <- use simctx_map_v
- r <- maybe (error $ "Unaliased context miss: " ++ (show v))
+ r <- maybe (error $ "User variable context miss: " ++ (show v))
return
$ M.lookup v m
XT.traceShow ("VL",v,r) $ return ()
return r
-type instance MCVT (SIMCT m f) VV = VR (NI f) KI UI
+type instance MCVT (SIMCT m f) VV = VR f (NIX f) KI
instance (Show f, Monad m) => MCR (SIMCT m f) VV where
clookup = SIMCT . user_lookup
instance (Show f, Monad m) => MCW (SIMCT m f) VV where
cassign v w = SIMCT $ simctx_map_v %= M.insert v w
-
instance (Show f, Monad m) => MCA (SIMCT m f) VV where
ccanon x = return x
-- of them. Despite the proliferation, much of the implementation is
-- type-directed, so it's not so bad.
--
--- * @N@ -- 'NI'
+-- * @N@ -- 'NIX' f
--
-- * @I@ -- @'InstF' f ('NI' f)@
--
--
-- * @J@ -- @'Either' ('NI' f) 'KI'@
--
--- * @U@ -- 'UI'
---
--- * @W@ -- 'UR' (i.e. @'InstF' f ('VR' ('NI' f) 'KI' 'UI')@)
---
-- * @V@ -- 'VV'
--
--- * @X@ -- 'VR' 'NI' 'KI' 'UI'
+-- * @X@ -- 'VR' f 'NI' 'KI'
+--
+-- * @Y@ -- @InstF f (VR f 'NI' 'KI')@
------------------------------------------------------------------------}}}
------------------------------------------------------------------------}}}
---------------------------------------------------------------------------
-- | Execution-oriented aspects of functions we might actually want to
-- call during mode analysis.
---
-- Header material {{{
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
-module Dyna.Analysis.Mode.Execution.Functions(
+module Dyna.Analysis.Mode.Execution.Functions {-(
-- * Named inst functions
- nWellFormed, nGround, nLeq, nLeqGLB, nSub, nSubGLB, nSubLUB,
+ -- nWellFormed, nGround, nLeq, nLeqGLB, nSub, nSubGLB, nSubLUB,
-- * Unification
- unifyVV, unifyNV,
+ unifyVV, unifyUnaliasedNV,
-- * Matching,
subVN,
- -- * Calls
- doCall,
-) where
+ -- * Modes
+ doCall, mWellFormed
+)-} where
+import Control.Applicative
+import Control.Exception
import Control.Lens
+import Control.Monad.Error.Class
import Control.Monad.State
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Either
+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 Dyna.Analysis.Mode.Execution.Base
+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.XXX.MonadContext
import Dyna.XXX.MonadUtils
import qualified Debug.Trace as XT
-------------------------------------------------------------------------}}}
--- Named inst functions {{{
-
--- These functions all use StateT transformers to handle cyclic reasoning.
---
--- XXX It is possible that we will be hitting some of these tests often and
--- should do some form of caching in our contexts.
-
-nWellFormed :: forall f m n .
- (MCVT m n ~ InstF f n, MCR m n, Ord n)
- => Uniq
- -> n
- -> m Bool
-nWellFormed u0 i0 = evalStateT (q u0 i0) S.empty
- where
- q u v = do
- already <- gets $ S.member (u,v)
- if already
- then return True
- else do
- modify $ S.insert (u,v)
- i <- lift $ clookup v
- iWellFormed_ q u (i :: InstF f n)
-
-nGround :: forall f m n .
- (MCVT m n ~ InstF f n, MCR m n, Ord n)
- => n -> m Bool
-nGround i0 = evalStateT (q i0) S.empty
- where
- q v = do
- already <- gets $ S.member v
- if already
- then return True
- else do
- modify $ S.insert v
- i <- lift $ clookup v
- iGround_ q (i :: InstF f n)
-
-tieKnotCompare :: (MCVT m n ~ InstF f n, MCR m n, Ord n, Ord f)
- => (forall m' .
- (Monad m')
- => (n -> InstF f n -> m' Bool)
- -> (n -> n -> m' Bool)
- -> InstF f n -> InstF f n -> m' Bool)
- -> (forall t .
- (MonadTrans t, Monad (t m))
- => (n -> InstF f n -> t m Bool)
- -> (n -> n -> t m Bool)
- -> t m Bool)
- -> m Bool
-tieKnotCompare cmp start = evalStateT (start qa qb) (S.empty, S.empty)
- where
- qa v j = do
- already <- gets $ S.member (v,j) . fst
- if already
- then return True
- else do
- modify $ over _1 (S.insert (v,j))
- i <- lift $ clookup v
- cmp qa qb i j
- -- XXX? qb vi vj | vi == vj = return True
- qb vi vj = do
- already <- gets $ S.member (vi,vj) . snd
- if already
- then return True
- else do
- modify $ over _2 (S.insert (vi,vj))
- i <- lift $ clookup vi
- j <- lift $ clookup vj
- cmp qa qb i j
-
-
-nCompare :: (MCVT m n ~ InstF f n, MCR m n, Ord n, Ord f --,
- -- m' ~ StateT (S.Set (v,InstF f v), S.Set (v,v)) m
- )
- => (forall m' .
- (Monad m')
- => (n -> InstF f n -> m' Bool)
- -> (n -> n -> m' Bool)
- -> InstF f n -> InstF f n -> m' Bool)
- -> n -> n -> m Bool
-nCompare cmp i0 j0 = tieKnotCompare cmp (\_ qb -> qb i0 j0)
-
-nLeq, nSub :: forall f n m .
- (Ord f, Ord n, MCVT m n ~ InstF f n, MCR m n)
- => n -> n -> m Bool
-nLeq = nCompare iLeq_ {- :: (Monad m')
- => (n -> InstF f n -> m' Bool)
- -> (n -> n -> m' Bool)
- -> InstF f n -> InstF f n -> m' Bool) -}
-
-nSub = nCompare iSub_ {- :: (Monad m')
- => (n -> InstF f n -> m' Bool)
- -> (n -> n -> m' Bool)
- -> InstF f n -> InstF f n -> m' Bool) -}
-
-nTotalBin :: forall f m m' t n .
- (Ord n, MonadFix m,
- MCVT m n ~ t, MCR m n, MCN m n,
- m' ~ StateT (M.Map (n, n) n) m, t ~ InstF f n)
- => ((n -> n -> m' n)
- -> t -> t -> m' t)
- -> n -> n -> m n
-nTotalBin f i0 j0 = evalStateT (q i0 j0) M.empty
- where
- q ni nj | ni == nj = return ni
- q ni nj = do
- cached <- gets $ M.lookup (ni,nj)
- case cached of
- Just i -> return i
- Nothing -> do
- (_,nk) <- mfix $ \(~(k,_)) -> do
- nk <- lift $ cnew k
- modify $ M.insert (ni,nj) nk
- i <- lift $ clookup ni
- j <- lift $ clookup nj
- k' <- f q i (j :: t)
- return (k',nk)
- return nk
-
-nLeqGLB, nSubGLB :: (Ord f, Ord n,
- MonadFix m, MCVT m n ~ InstF f n, MCR m n, MCN m n)
- => n -> n -> m n
-nLeqGLB = nTotalBin (iLeqGLB_ return return)
-nSubGLB = nTotalBin (iSubGLB_ return return)
-
-nSubLUB :: forall f n m .
- (MonadFix m, Ord f, Ord n,
- MCVT m n ~ InstF f n, MCR m n, MCN m n, MCF m n, Show n)
- => n -> n -> m (Maybe n)
-nSubLUB i0 j0 = evalStateT (runMaybeT (q i0 j0)) M.empty
- where
- q ni nj | ni == nj = return ni
- q ni nj = do
- -- XT.traceShow ("Q ENT",ni,nj) $ return ()
- cache <- gets $ M.lookup (ni,nj)
- case cache of
- Just k -> return k
- Nothing -> do
- (_,nk) <- mfix $ \(~(k,_)) -> do
- nk <- lift $ lift $ cnew k
- modify $ M.insert (ni,nj) nk
- i <- lift $ lift $ clookup ni
- j <- lift $ lift $ clookup nj
- mk <- iSubLUB_ return return q i (j :: InstF f n)
- maybe mzero (\k' -> return (k',nk)) mk
- return nk
-
------------------------------------------------------------------------}}}
-- Unification {{{
--- | This predicate is used to ensure that we reject any attempt at
--- unification which could fail (i.e. is semidet, or, possibly better
--- phrased, must traverse the structure of its argument) and may reference
--- clobbered state.
---
--- In words, a unification can enter its arguments whenever
--- 1. both inputs are not free variables (a free variable turns
--- unification into assignment; two makes it aliasing)
--- 2. either input represents more than one possible term
---
--- The thesis will invoke this function (or rather, its negation) to allow a
--- /dead/ unification to succeed. Live unifications are probably (yes? XXX?)
--- permitted because it's always possible (if unlikely) that some predicate
--- can run with a clobbered input, and if not, we'll fail at that point.
--- A semidet unification, on the other hand, cannot run with a clobbered
--- input.
---
--- Definition 3.2.19, p53
---
--- XXX In contrast to the thesis, we ignore the size of the sets represented
--- by the insts we are given, which makes this test wider, and therefore the
--- set of unifications we will accept smaller.
---
-semidet_clobbered_unify :: (Monad m) => InstF f i -> InstF f i' -> m Bool
-semidet_clobbered_unify i i' = return $
- (not $ iIsFree i)
- && (not $ iIsFree i')
- && (UMostlyClobbered <= iUniq i || UMostlyClobbered <= iUniq i')
+-- | Constraints common to all unification functions
+type UnifCtxC m f n = (Ord f, Show f,
+ Monad m, MonadError UnifFail m,
+ n ~ NIX f)
+
+-- | Constraints for unification on keyed insts
+type UnifCtxKC m f n k = (MCVT m k ~ ENKRI f n k, MCM m k)
-- | 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.
-unifyNN :: (Ord n, Ord f, Show n,
- MonadFix m,
- MCVT m n ~ InstF f n, MCR m n, MCN m n)
+-- applicable (e.g. 'unifyNK').
+unifyNN :: UnifCtxC m f n
=> Bool -> n -> n -> m n
-unifyNN l a b = XT.traceShow ("UNN",a,b) $ do
- when (not l) $ do
- ia <- clookup a
- ib <- clookup b
- semidet_clobbered_unify ia ib >>= flip when (fail "UNN SCU")
- nLeqGLB a b
+unifyNN l a b =
+ either throwError return $ (if l then nLeqGLBRL else nLeqGLBRD) a b
+
+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
+
+-- |
+--
+-- 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
+
+
+{-
+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
+-}
-- | 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)
--
-- 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
+
+{-
+{-
+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 ->
+-}
+
+
unifyNK :: forall f k m n .
- (Eq k, Ord f, Ord n, Show n, Show k,
- MonadFix m,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k,
- MCVT m n ~ InstF f n, MCR m n, MCN 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
unifyNK l n k = cmerge (unifyEE l) k (Left n) >> return k
unifyEE :: forall f k m n .
- (Eq k, Ord f, Ord n, Show n, Show k,
- MonadFix m,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k,
- MCVT m n ~ InstF f n, MCR m n, MCN 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
unifyEE l (Right qa) (Right qb) = liftM Right $ unifyQQ l qa qb
unifyQQ :: forall f k m n .
- (Eq k, Ord f, Ord n, Show n, Show k,
- MonadFix m,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k,
- MCVT m n ~ InstF f n, MCR m n, MCN 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
iLeqGLB_ return return (unifyJJ l) qa qb
unifyJJ :: forall f k m n .
- (Eq k, Ord f, Ord n, Show n, Show k,
- MonadFix m,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k,
- MCVT m n ~ InstF f n, MCR m n, MCN 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
-- | 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, Ord n, MonadFix m, Show k, Show n,
- MCVT m n ~ InstF f n, MCR m n, MCN m n,
+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
unifyKK _ a b | a == b = return a
unifyKK l a b = XT.traceShow ("UKK",a,b) $ calias (unifyEE l) a b
--- | Unify two previously unaliased bits of structure into an aliased piece
--- of structure.
---
--- Deletes inputs from unaliased table.
-unifyUU :: (Eq u, Eq k, Ord f, Ord n, MonadFix m, Show k, Show n,
- MCVT m n ~ InstF f n, MCR m n, MCN m n,
- MCVT m k ~ ENKRI f n k, MCA m k, MCD m k, MCM m k, MCN m k,
- MCVT m u ~ UR f n k u, MCD m u, MCR m u)
- => Bool -> u -> u -> m k
-unifyUU _ a b | a == b = cdelete a >>= aliasW -- XXX probably should be error
-unifyUU l a b = do
- ka <- cdelete a >>= aliasW
- kb <- cdelete b >>= aliasW
- unifyKK l ka kb
-
-- | 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 u .
- (Eq k, Eq u, Ord f, Ord n, Show n, Show k,
- MonadFix m,
- MCVT m k ~ ENKRI f n k, MCA m k, MCD m k, MCM m k, MCN m k,
- MCVT m n ~ InstF f n, MCN m n, MCR m n,
- MCVT m u ~ UR f n k u, MCD m u, MCR m u)
+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 n k u
- -> VR n k u
+ -> VR f n k
+ -> VR f n k
-> m k
-unifyXX l (VRName na) (VRName nb) = unifyNN l na nb >>= cnew . Left
+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 <- cdelete ub >>= aliasW
+ 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 <- cdelete ub >>= aliasW
+ kb <- aliasY ub
unifyKK l ka kb
unifyXX l (VRStruct ua) (VRName nb) = do
- ka <- cdelete ua >>= aliasW
+ ka <- aliasY ua
unifyNK l nb ka
unifyXX l (VRStruct ua) (VRKey kb) = do
- ka <- cdelete ua >>= aliasW
+ ka <- aliasY ua
+ unifyKK l ka kb
+unifyXX l (VRStruct ua) (VRStruct ub) = do
+ ka <- aliasY ua
+ kb <- aliasY ub
unifyKK l ka kb
-unifyXX l (VRStruct ua) (VRStruct ub) = unifyUU l ua ub
-
-- | Variable-on-variable unification. Ah, finally.
--
+-- Based on figure 5.7, p 104.
+--
-- 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 u v .
- (Eq k, Eq u, Ord f, Ord n, Show n, Show k,
- MonadFix m,
+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 n ~ InstF f n, MCN m n, MCR m n,
- MCVT m u ~ UR f n k u, MCD m u, MCR m u,
- MCVT m v ~ VR n k u, MCA m v)
+ MCVT m v ~ VR f n k, MCA m v)
=> (v -> Bool)
-> v
-> v
-- predicate mode.
--
-- This function returns the variable given as a convenient shorthand.
-unifyNV :: forall f k m n u v .
- (Eq k, Eq u, Ord f, Ord n, Show n, Show k,
- MonadFix m,
- MCVT m k ~ ENKRI f n k, MCA m k, MCM m k,
- MCVT m n ~ InstF f n, MCN m n, MCR m n,
- MCVT m u ~ UR f n k u, MCR m u, MCW m u,
- MCVT m v ~ VR n k u, MCR m v, MCW m v)
- => Bool
- -> n
- -> v
- -> m v
-unifyNV l n0 v0 = do
+--
+-- 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
x0 <- clookup v0
xu <- unifyNX n0 x0
cassign v0 xu
return v0
where
- unifyNX :: n -> VR n k u -> m (VR n k u)
+ 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 $ unifyNU na ub
-
- unifyNU :: n -> u -> m u
- unifyNU na ub = do
- wb <- clookup ub
- wu <- unifyNW na wb
- cassign ub wu
- return ub
+ unifyNX na (VRStruct ub) = liftM VRStruct $ unifyNY na ub
- unifyNW :: n -> UR f n k u -> m (UR f n k u)
- unifyNW na ub = do
+ 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
-
+-}
------------------------------------------------------------------------}}}
-- Matching {{{
-subNN :: (Ord f, Ord n, Show n, MCVT m n ~ InstF f n, MCR m n)
+{-
+subNN :: (Ord f, n ~ NI f, Monad m)
=> n -> n -> m Bool
-subNN a b = XT.traceShow ("SNN",a,b) $ nSub a b
+subNN a b = XT.traceShow ("SNN",a,b) $ return $ nSub a b
-iCompare :: (MCVT m n ~ InstF f n, MCR m n, Ord n, Ord f --,
- -- m' ~ StateT (S.Set (v,InstF f v), S.Set (v,v)) m
- )
+iCompare :: (Ord f, n ~ NI f)
=> (forall m' .
(Monad m')
=> (n -> InstF f n -> m' Bool)
-> (n -> n -> m' Bool)
-> InstF f n -> InstF f n -> m' Bool)
- -> InstF f n -> InstF f n -> m Bool
+ -> InstF f n -> InstF f n -> Bool
iCompare cmp i0 j0 = tieKnotCompare cmp (\qa qb -> cmp qa qb i0 j0)
+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
ni <- clookup n
- iCompare iSub_ ni i
+ return $ iCompare iSub_ ni i
+subJN :: forall f k m n .
+ (Ord f, n ~ NI f, Show f, Show k,
+ MCVT m k ~ ENKRI f n k, MCR m k)
+ => Either n k -> n -> m Bool
subJN j = either subNN subKN j
+subJI :: forall f k m n .
+ (Ord f, n ~ NI f, Show f, Show k,
+ MCVT m k ~ ENKRI f n k, MCR m k)
+ => Either n k -> InstF f n -> m Bool
subJI j = either subNI subKI j
+subQI :: 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 -> InstF f n -> m Bool
subQI q i = XT.traceShow ("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
ni <- clookup n
- iSub_ subJI subJN q ni
+ subQI q ni
+subKN :: forall f k m n .
+ (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
kq <- clookup k
(either subNN subQN kq) n
+subKI :: forall f k m 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
kq <- clookup k
(either subNI subQI kq) i
-subUI u i = XT.traceShow ("SUI",u,i) $ do
- uw <- clookup u
- iSub_ subXI subXN uw i
-
+subYI :: forall f k m n .
+ (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
+ 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
case x of
VRName xn -> subNI xn i
VRKey xk -> subKI xk i
- VRStruct xu -> subUI xu i
+ VRStruct xy -> subYI xy i
-subXN :: forall f k m n u .
- (Ord n, Ord f, MonadFix m, Show n, Show f, Show k, Show u,
+subXN :: forall f k m n .
+ (Ord n, Ord f, Show n, Show f, Show k,
MCVT m n ~ InstF f n, MCR m n,
- MCVT m k ~ ENKRI f n k, MCR m k,
- MCVT m u ~ UR f n k u, MCR m u)
- => VR n k u -> n -> m Bool
+ 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
case x of
VRName xn -> subNN xn n
VRKey xk -> subKN xk n
VRStruct xu -> subUN xu n
-subUN :: forall f k m n u .
- (Ord n, Ord f, MonadFix m, Show n, Show f, Show k, Show u,
+subUN :: forall f k m n .
+ (Ord n, Ord f, Show n, Show f, Show k,
MCVT m n ~ InstF f n, MCR m n,
- MCVT m k ~ ENKRI f n k, MCR m k,
- MCVT m u ~ UR f n k u, MCR m u)
- => u -> n -> m Bool
+ 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
- uw <- clookup u
ni <- clookup n
- iSub_ subXI subXN uw ni
+ iSub_ subXI subXN u ni
-subVN :: forall f k m n u v .
- (Ord n, Ord f, MonadFix m, Show n, Show f, Show k, Show u, Show v,
+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 u ~ UR f n k u, MCR m u,
- MCVT m v ~ VR n k u, MCR m v)
+ MCVT m v ~ VR f n k, MCR m v)
=> v
-> n
-> m Bool
-- misread.
--
-- Based on Figure 5.7, p104
-doCall :: forall f k m n u v .
- (Ord n, Ord f, Eq u, Eq k,
- Show n, Show f, Show k, Show u, Show v,
- MonadFix m,
+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 u ~ UR f n k u, MCR m u, MCW m u,
- MCVT m v ~ VR n k u, MCR m v, MCW m v)
+ MCVT m v ~ VR f n k, MCR m v, MCW m v)
=> (v -> Bool) -- Liveness predicate
- -> [v] -- Call with these arguments
- -> [(n, n)] -- Against this pattern
+ -> v -> [v] -- Call with these arguments
+ -> QMode n -- Against this pattern
-> m Bool
-doCall l as0 cs0 = go as0 (map fst cs0)
+doCall l r0 as0 (QMode cs0 (rmi,rmo)) = go (r0:as0) (rmi:map fst cs0)
where
- go [] [] = goUnify as0 (map snd cs0)
+ go [] [] = goUnify as0 (rmo:map snd cs0)
go (a:as) (c:cs) = andM (subVN a c) (go as cs)
go _ _ = return False
goUnify [] [] = return True
- goUnify (a:as) (c:cs) = unifyNV (l a) c a >> goUnify as cs
+ goUnify (a:as) (c:cs) = unifyUnaliasedNV (l a) c a >> 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)
+-}
+
------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | 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.
+
+-- Header material {{{
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Mode.Execution.NamedInst (
+ -- * Datatype definition
+ NIX(..), NIXM,
+ -- * Well-formedness predicates
+ nWellFormedUniq, nWellFormedOC,
+ -- * Unary functions
+ nGround, nUpUniq, nPrune, nExpose, nHide,
+ -- * Binary comparators
+ nCmp, nEq, nLeq, nSub,
+ -- * Total binary functions
+ nTBin, nLeqGLB, nSubGLB,
+ -- * Partial binary functions
+ nPBin, nLeqGLBRD, nLeqGLBRL, -- nSubLUB,
+) where
+
+import Control.Applicative
+-- import qualified Control.Arrow as A
+import Control.Lens
+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 Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Unification
+import Dyna.Analysis.Mode.Uniq
+import Dyna.Main.Exception
+import Dyna.XXX.MonadUtils
+
+-- import qualified Debug.Trace as XT
+
+import System.IO.Unsafe (unsafePerformIO)
+import System.Mem.StableName (makeStableName)
+
+------------------------------------------------------------------------}}}
+-- 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 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) =>
+ 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
+ }
+
+-- 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
+--
+-- XXX Should attempt to do something with the 'NIX' passed in!
+panicwf :: NIX f -> a
+panicwf _ = dynacPanicStr "NIX not well formed"
+
+-- | 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 :: (Monad m, Ord k)
+ => NIX f -- ^ For debugging
+ -> (a -> m c)
+ -> (b -> m c)
+ -> M.Map k (Either a b)
+ -> k
+ -> m 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)
+
+------------------------------------------------------------------------}}}
+-- 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).
+--
+-- 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
+ where
+ q u a = -- XT.traceShow ("NWFU Q",u,a,ml n0 m a) $
+ 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'
+
+-- | 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 :: forall f . (Ord f) => NIX f -> ()
+nWellFormedOC = go H.empty
+ where
+ mksp x = x `seq` unsafePerformIO (makeStableName x)
+
+ visit q i = F.mapM_ (F.mapM_ q) (i ^. inst_rec)
+
+ go vis n0@(NIX i m) =
+ let sn0 = mksp n0
+ in if sn0 `H.member` vis
+ then dynacPanicStr "Named inst occurs check!"
+ else evalState (visit (q vis) i) S.empty
+ where
+ q v a = tsc id a
+ (eml n0 (return . go v) (visit (q v)) m a >> return True)
+
+nGround :: forall f . NIX f -> Bool
+nGround n0@(NIX i0 m) = evalState (iGround_ q i0) S.empty
+ where
+ q a = tsc id a $ eml n0 (return . nGround) (iGround_ q) m a
+ {-
+ q (Left a) = return $ nGround a
+ q (Right a) = tsc id a $ ml n0 m a >>= iGround_ q
+ -}
+
+-- | Prune the internals of a 'NIX'. This really ought not be needed, but
+-- it's handy for test generation.
+
+nCrawl :: forall f . (Ord 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 ()
+
+
+nPrune :: forall f . (Ord f) => NIX f -> NIX f
+nPrune = nCrawl (const IFree) UUnique
+
+nUpUniq :: forall f . (Ord f) => Uniq -> NIX f -> NIX f
+nUpUniq = nCrawl (const IFree)
+{-
+-- | Increase the nonuniqueness of a particular named inst to at least the
+-- given level.
+nUpUniq :: forall f . Uniq -> NIX f -> NIX f
+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)
+{-
+ reuniq (IFree ) = IFree
+ reuniq i@(IUniv u' ) = if u' >= u0 then i else IUniv u0
+ reuniq i@(IAny u' ) = if u' >= u0 then i else IAny u0
+ reuniq i@(IBound u' im ib) = if u' >= u0 then i else IBound u0 im ib
+-}
+
+ m0' = M.map (nUpUniq u0 A.+++ reuniq) m0
+ i0' = reuniq i0
+-}
+
+-- | Expose the root ply of a 'NIX' as an Inst which recurses as additional
+-- 'NIX' elements.
+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
+{-# INLINABLE nExpose #-}
+
+-- | An inefficient \"inverse\" of nExpose.
+nHide :: 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 #-}
+
+------------------------------------------------------------------------}}}
+-- Binary predicates {{{
+
+nCmp :: forall f . (Ord f, Show f)
+ => (forall a b m .
+ (Monad m)
+ => (a -> InstF f b -> 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,ri) $ eml l0 (return . flip (nCmp q) (NIX ri rm))
+ (flip (q qop qip) ri)
+ lm l
+
+nEq, nLeq, nSub :: (Ord f, Show f) => NIX f -> NIX f -> Bool
+nEq = nCmp (\_ -> iEq_)
+nLeq = nCmp iLeq_
+nSub = nCmp iSub_
+
+------------------------------------------------------------------------}}}
+-- Binary functions {{{
+
+data NBinState a b f = NBS { _nbs_next :: Int
+ , _nbs_ctx :: NIXM Int f
+ , _nbs_cache_symm :: M.Map (Uniq,a,b) Int
+ , _nbs_cache_lsml :: M.Map (Uniq,InstF f b,a) Int
+ , _nbs_cache_lsmr :: M.Map (Uniq,InstF f a,b) Int
+ }
+$(makeLenses ''NBinState)
+
+iNBS :: NBinState a b f
+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 -> InstF f b -> a -> m c)
+ -> (Uniq -> InstF f a -> 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
+
+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 -> InstF f b -> a -> m c)
+ -> (Uniq -> InstF f a -> 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
+
+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 ⊔
+function is particularly interesting and it is not yet clear how to define
+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))
+-}
+
+------------------------------------------------------------------------}}}
-- Because I think it will be easier to understand in the long run, I have
-- opted to avoid that -- the InstF functor contains only those constructors
-- necessary for building plies of an actual inst. The other (co)products
--- needed at runtime may be found in 'Dyna.Analysis.Mode.ExecutionTypes'.
+-- needed at runtime may be found in 'Dyna.Analysis.Mode.Execution.Base'.
-- Header material {{{
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall #-}
module Dyna.Analysis.Mode.Inst(
- InstF(..),
+ InstF(..), inst_uniq, inst_rec,
iNotReached, iIsNotReached,
iUniq, iIsFree, iWellFormed_, iEq_, iGround_,
iLeq_, iLeqGLB_,
iSub_, iSubGLB_, iSubLUB_,
) where
+import Control.Lens
-- 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.XXX.DataUtils as XDU
import Dyna.XXX.MonadUtils
import Dyna.Analysis.Mode.Uniq
+-- import qualified Debug.Trace as XT
+
------------------------------------------------------------------------}}}
-- Instantiation States {{{
-- Note that we are saying nothing about the possible data
-- bound by this variable; that would be the job of the type
-- system.
- | IAny !Uniq
+ | IAny { _inst_uniq :: !Uniq }
-- | A bound inst. More specifically, a disjunction of
-- possible binding states: it's guaranteed to be one of these
--
-- Note that defition 3.2.11 (p50) requires that the
-- uniqueness of the inner Insts be below by <=
- -- (see the 'iWellformed_' predicate below)
+ -- (see the 'iWellFormed_' predicate below)
--
-- The Bool field, which is an extension from the thesis,
-- indicates the possibility that this inst is
-- field for recording possible actual base-cases, too,
-- but one thing at a time.
--
- -- Definition 3.2.18, p52:
- -- @not_reached(u) === IBound u M.empty False@.
- -- @not_reached === not_reached(UUnique)@.
- | IBound !Uniq
- !(M.Map f [i])
- !Bool
+ -- XXX The thesis uses lists, of course, for each functor's arguments. We
+ -- are going to want to change that once we have a better understanding of
+ -- our term layer. (That is, we should make InstF parametric in its
+ -- choice of container of arguments, or we could existentially hide the
+ -- container by converting InstF into a GADT. I think either option is
+ -- acceptable.)
+ --
+ -- Definition 3.2.18, p52, is now:
+ --
+ -- * @not_reached(u) === IBound u M.empty False@.
+ --
+ -- * @not_reached === not_reached(UUnique)@.
+ | IBound { _inst_uniq :: !Uniq
+ , _inst_rec :: !(M.Map f [i])
+ , _inst_base :: !Bool
+ }
-- | This one is not in the thesis exposition but is used during
-- computation to represent the entire universe of ground
-- terms. See prose, p63, \"For efficiency, we treat ground...\".
--
- -- Defninition 3.2.17, p52 is thus rewritten:
- -- @ground(u) === IUniv u@.
- | IUniv !Uniq
+ -- Defninition 3.2.17, p52 is thus rewritten: @ground(u) === IUniv u@.
+ | IUniv { _inst_uniq :: !Uniq }
-- XXX Mercury has a concept of \"higher-order modes\", which we
-- do not yet support (though there is grumbling about it in
-- the background). See 3.2.4 p55 et seq.
deriving (Eq, F.Foldable, Functor, Ord, Show, T.Traversable)
+-- $(makePrisms ''InstF)
+$(makeLensesFor [("_inst_uniq","inst_uniq")
+ ,("_inst_rec","inst_rec")
+ ]
+ ''InstF)
+
+-- XXX class (Pretty f, Pretty i) => Pretty (InstF f i) where
------------------------------------------------------------------------}}}
-- Instantiation States: Unary predicates {{{
-- | 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\" -- we choose to make that
--- explicit here.
-iUniq :: InstF f i -> Uniq
-iUniq IFree = UUnique
-iUniq (IAny u) = u
-iUniq (IBound u _ _) = u
-iUniq (IUniv u) = u
+-- no uniqueness annotation on the free inst\".
+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 #-}
-- | Check that an instantiation state is well-formed as per defintion
-> Uniq -> InstF f i
-> m Bool
iWellFormed_ _ _ IFree = return True
-iWellFormed_ _ u' (IAny u) = return $ u <= u'
-iWellFormed_ q u' (IBound u b _) = if u <= u'
- then mfmamm (q u) b
+iWellFormed_ _ u (IAny u') = return $ u <= u'
+iWellFormed_ q u (IBound u' b _) = if u <= u'
+ then mfmamm (q u') b
else return False
-iWellFormed_ _ u' (IUniv u) = return $ u <= u'
+iWellFormed_ _ u (IUniv u') = return $ u <= u'
{-# INLINABLE iWellFormed_ #-}
-- | Compare with 'IFree' without imposing @Eq i@.
iLeq_ _ _ (IUniv u) (IAny u') = return $ u' <= u
iLeq_ _ _ (IUniv u) (IUniv u') = return $ u' <= u
iLeq_ _ _ (IUniv _) _ = return $ False
-iLeq_ q _ (IBound u b _) r@(IAny u') = andM1 (u' <= u) $
- mfmamm (flip q r) b
-iLeq_ q _ (IBound u b _) r@(IUniv u') = andM1 (u' <= u) $
- mfmamm (flip q r) b
+iLeq_ q _ (IBound u b _) (IAny u') = andM1 (u' <= u) $
+ mfmamm (\x -> q x (IAny u')) b
+iLeq_ q _ (IBound u b _) (IUniv u') = andM1 (u' <= u) $
+ mfmamm (\x -> q x (IUniv u')) b
iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && u' <= u) $
flip mapForallM m $
\f is -> case M.lookup f m' of
-- XXX Ought to assert that length is == length is'
{-# INLINABLE iLeq_ #-}
--- | Compute the GLB under iLeq_ (⋏)
+-- | Compute the GLB under iLeq_ (⋏) at a particular uniqueness.
+--
+-- The uniqueness input is needed for the case when we unify with a free
+-- variable deep within a structure. It should be UUnique at the root of
+-- a unification.
--
-- Since iLeq (≼) is a lattice, this is a total function.
--
+-- Notice that the \"import\" and \"merge\" callbacks take a 'Uniq'
+-- argument; this 'Uniq' must be ≼ the uniqueness of the returned @i''@
+-- inst in order for the produced inst to be well-formed. It is impossible,
+-- due to open recursion, for this function to engage in the necessary
+-- rewrites itself.
+--
-- XXX Unlike the thesis exposition, but like the Mercury implementation, we
-- might consider an alternative version of this function that returned not
-- only the result of unification, but the determinism as well. The problem
-- variables).
iLeqGLB_ :: (Monad m, Ord f)
- => (i -> m i'')
- -> (i' -> m i'')
- -> (i -> i' -> m i'')
- -> InstF f i
- -> InstF f i'
+ => (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_ _ r _ IFree x = T.mapM r x
-iLeqGLB_ l _ _ x IFree = T.mapM l x
-
-iLeqGLB_ _ _ _ (IAny u) (IAny u') = return $ IAny (max u u')
-
-iLeqGLB_ _ _ _ (IAny u') (IUniv u) = return $ IUniv (max u u')
-iLeqGLB_ _ _ _ (IUniv u) (IAny u') = return $ IUniv (max u u')
-iLeqGLB_ _ _ _ (IUniv u) (IUniv u') = return $ IUniv (max u u')
-
-iLeqGLB_ l _ _ (IBound u m b) (IAny u') = (return . flip (IBound (max u u')) b)
- =<< T.mapM (T.mapM l) m
-iLeqGLB_ _ r _ (IAny u') (IBound u m b) = (return . flip (IBound (max u u')) b)
- =<< T.mapM (T.mapM r) m
-
-iLeqGLB_ l _ _ (IBound u m b) (IUniv u') = (return . flip (IBound (max u u')) b)
- =<< T.mapM (T.mapM l) m
-iLeqGLB_ _ r _ (IUniv u') (IBound u m b) = (return . flip (IBound (max u u')) b)
- =<< T.mapM (T.mapM r) m
-
-iLeqGLB_ _ _ q (IBound u m b) (IBound u' m' b') = do
- m'' <- mergeBoundLB q m m'
- return $! IBound (max u u') m'' (b && b')
+iLeqGLB_ _ r _ _ _ u IFree x = T.mapM (r u) x
+iLeqGLB_ l _ _ _ _ u x IFree = T.mapM (l u) x
+
+iLeqGLB_ _ _ _ _ _ _ (IAny u) (IAny u') = return $ IAny (max u u')
+
+iLeqGLB_ _ _ _ _ _ _ (IAny u') (IUniv u) = return $ IUniv (max u u')
+iLeqGLB_ _ _ _ _ _ _ (IUniv u) (IAny u') = return $ IUniv (max u u')
+iLeqGLB_ _ _ _ _ _ _ (IUniv u) (IUniv u') = return $ IUniv (max u u')
+
+iLeqGLB_ _ _ l _ _ _ (IBound u m b) (IAny u') =
+ let v = max u u'
+ in return . flip (IBound v) b =<< T.mapM (T.mapM (l v $ IAny v)) m
+iLeqGLB_ _ _ _ r _ _ (IAny u') (IBound u m b) =
+ let v = max u u'
+ in return . flip (IBound v) b =<< T.mapM (T.mapM (r v $ IAny v)) m
+
+iLeqGLB_ _ _ l _ _ _ (IBound u m b) (IUniv u') =
+ let v = max u u'
+ in return . flip (IBound v) b =<< T.mapM (T.mapM (l v $ IUniv v)) m
+iLeqGLB_ _ _ _ r _ _ (IUniv u') (IBound u m b) =
+ let v = max u u'
+ in return . flip (IBound v) b =<< T.mapM (T.mapM (r v $ IUniv v)) m
+
+iLeqGLB_ _ _ _ _ q _ (IBound u m b) (IBound u' m' b') = do
+ let v = max u u'
+ m'' <- mergeBoundLB (q v) m m'
+ return $! IBound v m'' (b && b')
{-# INLINABLE iLeqGLB_ #-}
-- | Matches partial order with uniqueness (⊑)
iSub_ _ _ (IUniv u) (IAny u') = return $ u <= u'
iSub_ _ _ (IUniv u) (IUniv u') = return $ u <= u'
iSub_ _ _ (IUniv _) _ = return $ False
-iSub_ q _ (IBound u b _) r@(IAny u') = andM1 (u <= u') $
- mfmamm (flip q r) b
-iSub_ q _ (IBound u b _) r@(IUniv u') = andM1 (u <= u') $
- mfmamm (flip q r) b
+iSub_ q _ (IBound u b _) (IAny u') = andM1 (u <= u') $
+ mfmamm (\x -> q x (IAny u')) b
+iSub_ q _ (IBound u b _) (IUniv u') = andM1 (u <= u') $
+ mfmamm (\x -> q x (IUniv u')) b
iSub_ _ q (IBound u m b) (IBound u' m' b') = andM1 (u <= u' && b <= b') $
flip mapForallM m $
\f is -> case M.lookup f m' of
{-# INLINABLE iSub_ #-}
-- | Compute the GLB under iSub_ (⊓)
+--
+-- Unlike 'iLeqGLB_', the \"lopsided merge\" callbacks do not need 'Uniq'
+-- inputs, as the uniqueness merge operation here is 'min' and 'Uniq' is
+-- required to be nondecreasing as we recurse through a term.
+-- Note further the lack of \"import\" callbacks: since the only relations
+-- on 'IFree' are with 'IFree' or 'iNotReached', there is no recursion to be
+-- done.
iSubGLB_ :: (Ord f, Monad m)
- => (i -> m i'')
- -> (i' -> m i'')
+ => (InstF f i' -> i -> m i'')
+ -> (InstF f i -> i' -> m i'')
-> (i -> i' -> m i'')
-> InstF f i -> InstF f i' -> m (InstF f i'')
iSubGLB_ _ _ _ IFree IFree = return $ IFree
-iSubGLB_ _ _ _ IFree b = return $ iNotReached (iUniq b)
-iSubGLB_ _ _ _ a IFree = return $ iNotReached (iUniq a)
+ -- The 'fromJust' calls here are safe since it is guaranteed by the
+ -- above match that iUniq is being called on something that is not
+ -- 'IFree' and is therefore within its domain.
+iSubGLB_ _ _ _ IFree b = return $ iNotReached (MA.fromJust $ iUniq b)
+iSubGLB_ _ _ _ a IFree = return $ iNotReached (MA.fromJust $ iUniq a)
iSubGLB_ _ _ _ (IAny u) (IAny u') = return $ IAny (min u u')
iSubGLB_ _ _ _ (IUniv u) (IAny u') = return $ IUniv (min u u')
iSubGLB_ _ _ _ (IUniv u) (IUniv u') = return $ IUniv (min u u')
-iSubGLB_ l _ _ (IBound u m b) (IAny u') = (return . flip (IBound (min u u')) b)
- =<< T.mapM (T.mapM l) m
-iSubGLB_ _ r _ (IAny u') (IBound u m b) = (return . flip (IBound (min u u')) b)
- =<< T.mapM (T.mapM r) m
+iSubGLB_ l _ _ (IBound u m b) r@(IAny u') = (return . flip (IBound (min u u')) b)
+ =<< T.mapM (T.mapM (l r)) m
+iSubGLB_ _ r _ l@(IAny u') (IBound u m b) = (return . flip (IBound (min u u')) b)
+ =<< T.mapM (T.mapM (r l)) m
-iSubGLB_ l _ _ (IBound u m b) (IUniv u') = (return . flip (IBound (min u u')) b)
- =<< T.mapM (T.mapM l) m
-iSubGLB_ _ r _ (IUniv u') (IBound u m b) = (return . flip (IBound (min u u')) b)
- =<< T.mapM (T.mapM r) m
+iSubGLB_ l _ _ (IBound u m b) r@(IUniv u') = (return . flip (IBound (min u u')) b)
+ =<< T.mapM (T.mapM (l r)) m
+iSubGLB_ _ r _ l@(IUniv u') (IBound u m b) = (return . flip (IBound (min u u')) b)
+ =<< T.mapM (T.mapM (r l)) m
iSubGLB_ _ _ q (IBound u m b) (IBound u' m' b') = do
let u'' = min u u'
return $ IBound u'' m'' (b && b')
{-# INLINABLE iSubGLB_ #-}
+maxuniq :: forall a m t t' .
+ (Monad m, F.Foldable t, F.Foldable t')
+ => (a -> m Uniq) -> Uniq -> t (t' a) -> m Uniq
+
+maxuniq q0 = go (go q0 UUnique)
+ where go q = F.foldrM (\i u -> q i >>= return . max u)
+
-- | Compute the LUB under iSub_ (⊔)
--
-- Since 'iSub_' is not a full lattice, this is a partial function (thus
-- 'Maybe'). Note, however, that the recursion is defined to be total --
-- thus it is the responsibility of the outer 'Monad' to bail out if any
-- call to 'iSubGLB_' yields 'Nothing'.
-iSubLUB_ :: (Ord f, Monad m)
- => (i -> m i'')
- -> (i' -> m i'')
+--
+-- Unlike the other calls, this one needs \"find the maximum 'Uniq' in an
+-- Inst\" callbacks for its lop-sided merge cases. These callbacks should
+-- abort if they encounter free variables, in keeping with the defintion of
+-- ⊑ .
+iSubLUB_ :: (Ord f, Monad m, Show i, Show i', Show i'', Show f)
+ => (i -> m Uniq)
+ -> (i' -> m Uniq)
+ -> (Uniq -> i -> m i'')
+ -> (Uniq -> i' -> m i'')
-> (i -> i' -> m i'')
-> InstF f i -> InstF f i' -> m (Maybe (InstF f i''))
-iSubLUB_ _ _ _ IFree IFree = return $ Just IFree
-iSubLUB_ _ _ _ IFree b | iIsNotReached b = return $ Just IFree
-iSubLUB_ _ _ _ a IFree | iIsNotReached a = return $ Just IFree
-iSubLUB_ _ _ _ IFree _ = return $ Nothing
-iSubLUB_ _ _ _ _ IFree = return $ Nothing
-
-iSubLUB_ _ _ _ (IAny u) (IAny u') = return $ Just $ IAny (max u u')
-iSubLUB_ _ _ _ (IAny u') (IUniv u) = return $ Just $ IAny (max u u')
-iSubLUB_ _ _ _ (IUniv u) (IAny u') = return $ Just $ IAny (max u u')
-iSubLUB_ _ _ _ (IUniv u) (IUniv u') = return $ Just $ IUniv (max u u')
-
-iSubLUB_ _ _ _ (IBound u _ _) (IAny u') = return $ Just $ IAny (max u u')
-iSubLUB_ _ _ _ (IAny u') (IBound u _ _) = return $ Just $ IAny (max u u')
-
-iSubLUB_ _ _ _ (IBound u _ _) (IUniv u') = return $ Just $ IUniv (max u u')
-iSubLUB_ _ _ _ (IUniv u') (IBound u _ _) = return $ Just $ IUniv (max u u')
-
-iSubLUB_ l r q (IBound u m b) (IBound u' m' b') = do
- m'' <- mergeBoundUB q l r m m'
- return $! Just $! IBound (max u u') m'' (b || b')
+iSubLUB_ _ _ _ _ _ IFree IFree = return $ Just IFree
+iSubLUB_ _ _ _ _ _ IFree b | iIsNotReached b = return $ Just IFree
+iSubLUB_ _ _ _ _ _ a IFree | iIsNotReached a = return $ Just IFree
+iSubLUB_ _ _ _ _ _ IFree _ = return $ Nothing
+iSubLUB_ _ _ _ _ _ _ IFree = return $ Nothing
+
+iSubLUB_ _ _ _ _ _ (IAny u) (IAny u') = return $ Just $ IAny (max u u')
+iSubLUB_ _ _ _ _ _ (IAny u') (IUniv u) = return $ Just $ IAny (max u u')
+iSubLUB_ _ _ _ _ _ (IUniv u) (IAny u') = return $ Just $ IAny (max u u')
+iSubLUB_ _ _ _ _ _ (IUniv u) (IUniv u') = return $ Just $ IUniv (max u u')
+
+iSubLUB_ l _ _ _ _ (IBound u m _) (IAny u') = do
+ lu <- maxuniq l u m
+ return (Just $ IAny (max lu u'))
+iSubLUB_ _ r _ _ _ (IAny u') (IBound u m _) = do
+ ru <- maxuniq r u m
+ return (Just $ IAny (max ru u'))
+iSubLUB_ l _ _ _ _ (IBound u m _) (IUniv u') = do
+ lu <- maxuniq l u m
+ return (Just $ IUniv (max lu u'))
+iSubLUB_ _ r _ _ _ (IUniv u') (IBound u m _) = do
+ ru <- maxuniq r u m
+ return (Just $ IUniv (max ru u'))
+
+iSubLUB_ _ _ l r q (IBound u m b) (IBound u' m' b') = do
+ let v = max u u'
+ m'' <- mergeBoundUB q (l v) (r v) m m'
+ return $! Just $! IBound v m'' (b || b')
{-# INLINABLE iSubLUB_ #-}
------------------------------------------------------------------------}}}
+++ /dev/null
----------------------------------------------------------------------------
--- | Reimplementation of the Mercury mode system
---
--- This module implements some basic self-test functionality for the insts
--- predicates in 'Dyna.Analysis.Mode.Insts'.
-
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module Dyna.Analysis.Mode.InstSelftest where
-
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Trans.Maybe
-import Data.Functor.Identity
-import qualified Data.Map as M
-import Dyna.Analysis.Mode.Inst
-import Dyna.Analysis.Mode.Uniq
-import qualified Test.Framework as TF
-import Test.Framework.Providers.QuickCheck2
-import Test.Framework.TH
-import Test.QuickCheck
-
-newtype Fix f = In { out :: f (Fix f) }
-deriving instance (Eq (f (Fix f))) => Eq (Fix f)
-deriving instance (Show (f (Fix f))) => Show (Fix f)
-deriving instance (Ord f, Arbitrary f) => Arbitrary (Fix (InstF f))
-
-instance Arbitrary Uniq where arbitrary = arbitraryBoundedEnum
-instance (Ord f, Arbitrary f, Arbitrary i) => Arbitrary (InstF f i) where
- arbitrary = frequency [ (1,pure IFree)
- , (1,IAny <$> arbitrary)
- , (1,IUniv <$> arbitrary)
- , (3,IBound <$> arbitrary
- <*> sized (\s -> resize (s`div`2)
- (M.fromList <$> arbitrary))
- <*> arbitrary)
- ]
-
-
-q1 f = \x y -> f (\a ob -> q1 f a (In ob))
- (\a b -> q1 f a b)
- (out x) (out y)
-
-qtb f = \x y -> In <$> f (\a b -> qtb f a b) (out x) (out y)
-
-qpb :: (Monad m, ff ~ Fix f, fff ~ f ff)
- => ((ff -> ff -> MaybeT m ff)
- -> fff -> fff -> MaybeT m (Maybe fff))
- -> ff -> ff -> m (Maybe ff)
-qpb f x y = runMaybeT $ q x y
- where q a b = maybe mzero (return . In) =<< f q (out a) (out b)
-
-qdLeq a b = runIdentity $ q1 iLeq_ a b
-qdLeqGLB a b = runIdentity $ qtb (iLeqGLB_ return return) a b
-qdSub a b = runIdentity $ q1 iSub_ a b
-qdSubGLB a b = runIdentity $ qtb (iSubGLB_ return return) a b
-qdSubLUB a b = runIdentity $ qpb (iSubLUB_ return return) a b
-
-prop_iLeq_GLB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property
-prop_iLeq_GLB i1 i2 = i1 `qdLeq` i2
- ==> qdLeqGLB i1 i2 == i1
-
-prop_iSub_GLB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property
-prop_iSub_GLB i1 i2 = i1 `qdSub` i2
- ==> qdSubGLB i1 i2 == i1
-
-prop_iSub_LUB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property
-prop_iSub_LUB i1 i2 = i1 `qdSub` i2
- ==> qdSubLUB i1 i2 == (Just i2)
-
-selftest :: TF.Test
-selftest = $(testGroupGenerator)
-
-main :: IO ()
-main = $(defaultMainGenerator)
-
--- /dev/null
+module Dyna.Analysis.Mode.Selftest where
+
+import Test.Framework
+import qualified Dyna.Analysis.Mode.Selftest.NamedInst as NI
+
+selftest = testGroup "Dyna.Analysis.Mode.Selftest" [ NI.selftest ]
--- /dev/null
+---------------------------------------------------------------------------
+-- | Reimplementation of the Mercury mode system
+--
+-- This module implements some basic self-test functionality for the insts
+-- predicates in 'Dyna.Analysis.Mode.Insts' using the execution machinery
+-- in 'Dyna.Analysis.Mode.Execution.NamedInsts'.
+
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Dyna.Analysis.Mode.Selftest.NamedInst where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Trans.Maybe
+import Data.Functor.Identity
+import qualified Data.Either as E
+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 qualified Data.Traversable as T
+import Dyna.Analysis.Mode.Execution.NamedInst
+import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Selftest.Term
+import Dyna.Analysis.Mode.Uniq
+import Dyna.XXX.TestFramework
+import qualified Test.Framework as TF
+import Test.Framework.Providers.QuickCheck2
+import Test.Framework.TH
+import Test.QuickCheck
+import Test.QuickCheck.Property
+
+import qualified Debug.Trace as XT
+
+fromList :: Ord k => [(k,v)] -> M.Map k v
+fromList = M.fromList
+
+-- | Generate an Arbitrary 'NIXM' Entry (i.e. either a closed NIX automata
+-- or
+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
+ 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
+ let m = M.fromList $ zip nl plies -- Make the map
+ root <- arbInstPly igen -- The root
+ return $ NIX root m
+
+instance Arbitrary (NIX TestFunct) where
+ arbitrary = nPrune <$> arbNIX
+
+ shrink n@(NIX r m) = (MA.maybeToList noRecN) ++ subautomata
+ where
+ -- Replace all calls out to other automata with references to the root
+ noRecN = if null (E.lefts $ M.elems m) then Nothing else Just $ NIX r m'
+ where m' = M.map (either (const $ Right r) Right) m
+
+ -- Pull out all the subautomata
+ subautomata = E.lefts (M.elems m)
+
+nWFU = nWellFormedUniq UUnique
+
+-- | 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))
+
+-- | 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 i = property $ 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 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_nSub_refl :: NIX TestFunct -> 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
+
+-- 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_nSubGLB_WF :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nSubGLB_WF i1 i2 = nWFU i1 && nWFU i2 ==> nWFU (nSubGLB i1 i2)
+
+-- prop_nSubLUB_WF :: NIX TestFunct -> NIX TestFunct -> Property
+-- prop_nSubLUB_WF i1 i2 = nWFU i1 && nWFU i2
+-- ==> 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 i1 i2 = i1 `nLeq` i2 && nWFU i1 && nWFU i2
+ ==> nLeqGLB i1 i2 `nEq` i1
+
+prop_nSubGLB_Edge :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nSubGLB_Edge i1 i2 = i1 `nSub` i2 && nWFU i1 && nWFU i2
+ ==> nSubGLB i1 i2 `nEq` i1
+
+-- prop_nSubLUB_Edge :: NIX TestFunct -> NIX TestFunct -> Property
+-- prop_nSubLUB_Edge i1 i2 = i1 `nSub` i2 && nWFU i1 && nWFU i2
+-- ==> 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 i1 i2 = nWFU i1 && nWFU i2
+ ==> 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 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
+
+
+prop_nSubGLB_is_LB :: NIX TestFunct -> NIX TestFunct -> Property
+prop_nSubGLB_is_LB i1 i2 = nWFU i1 && nWFU i2
+ ==> 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 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
+
+-- prop_nSubLUB_is_UB :: NIX TestFunct -> NIX TestFunct -> Property
+-- prop_nSubLUB_is_UB i1 i2 = nWFU i1 && nWFU i2
+-- ==> maybe (property rejected)
+-- (\i -> property $ i1 `nSub` i && i2 `nSub` i)
+-- $ nSubLUB i1 i2
+
+
+selftest :: TF.Test
+selftest = moreTries 10000 $ moreTests 400 $(testGroupGenerator)
+
+main :: IO ()
+main = TF.defaultMain [selftest]
--- /dev/null
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Dyna.Analysis.Mode.Selftest.Term where
+
+import Control.Applicative
+import Control.Monad
+import qualified Data.List as L
+import qualified Data.Map as M
+import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Uniq
+import Test.QuickCheck
+
+-- XXX orphan instance
+instance Arbitrary Uniq where arbitrary = arbitraryBoundedEnum
+
+data TestFunct = F | G | H
+ deriving (Bounded,Enum,Eq,Ord,Show)
+
+instance Arbitrary TestFunct where arbitrary = arbitraryBoundedEnum
+
+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)
+ 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)
+ ]
+
+
--- /dev/null
+---------------------------------------------------------------------------
+-- | Wrappers around 'InstF' primitives that are useful during unification.
+
+-- Header material {{{
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Mode.Unification {-(
+)-} where
+
+import qualified Data.Maybe as MA
+import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Uniq
+-- import qualified Debug.Trace as XT
+
+------------------------------------------------------------------------}}}
+-- Unification Failure Flavors {{{
+
+data UnifFail =
+ UFSemiClob -- ^ see 'semidet_clobbered_unify'
+ | UFNotReach -- ^ Some nested unification satisfies 'iNotReached'
+ | UFExDomain -- ^ A partial function was applied outside its domain
+
+------------------------------------------------------------------------}}}
+-- Unification {{{
+
+-- | This predicate is used to ensure that we reject any attempt at
+-- unification which could fail (i.e. is semidet, or, possibly better
+-- phrased, must traverse the structure of its argument) and may reference
+-- clobbered state.
+--
+-- In words, a unification can enter its arguments whenever
+-- 1. both inputs are not free variables (a free variable turns
+-- unification into assignment; two makes it aliasing)
+-- 2. either input represents more than one possible term
+
+-- The thesis will invoke this function (or rather, its negation) to allow a
+-- /dead/ unification (i.e., one in which one of the two variables is not
+-- live going forward) to succeed. Live unifications are probably (yes?
+-- XXX?) permitted because it's always possible (if unlikely) that some
+-- predicate can run with a clobbered input, and if not, we'll fail at that
+-- point. A semidet unification, on the other hand, cannot run with a
+-- clobbered input.
+
+-- Definition 3.2.19, p53
+--
+-- XXX In contrast to the thesis, we ignore the size of the sets represented
+-- by the insts we are given, which makes this test wider, and therefore the
+-- set of unifications we will accept smaller.
+--
+semidet_clobbered_unify :: (Monad m) => InstF f i -> InstF f i' -> m Bool
+semidet_clobbered_unify i i' = return $
+ (not $ iIsFree i)
+ && (not $ iIsFree i')
+ && ( UMostlyClobbered <= MA.fromJust (iUniq i )
+ || UMostlyClobbered <= MA.fromJust (iUniq i'))
+ -- The above fromJust calls are safe due to the 'iIsFree' guards.
+
+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_ il ir ml mr m u i1 i2 = do
+ io <- iLeqGLB_ il ir ml mr m u i1 i2
+ return $ if iIsNotReached io
+ then Left UFNotReach
+ else Right io
+iLeqGLBRL_ il ir ml mr m u i1 i2 = do
+ scu <- semidet_clobbered_unify i1 i2
+ if scu
+ then return (Left UFSemiClob)
+ else iLeqGLBRD_ il ir ml mr m u i1 i2
+
+------------------------------------------------------------------------}}}
-- u2, then it is safe to use u1 in a context expecting u2.
--
-- The Mostly variants are intended (see p26) to handle trailing (i.e. undo
--- logs). See also the discussion on p48
+-- logs). See also the discussion on p48.
data Uniq = UUnique
-- ^ All references are known to the mode analysis system.
--
+ -- The system is permitted to issue both reads and untrailed
+ -- writes.
+ --
-- In a system without alias tracking, this more obviously
-- means \"unique reference\" (see prose, p90, \"This is a
-- subtle change in what we mean by unique.\").
| UMostlyUnique
+ -- ^ All references are known, but the value is used on
+ -- backtracking.
+ --
+ -- The system is permitted to issue reads and writes, but
+ -- all writes must be trailed or otherwise inverted.
| UShared
+ -- ^ This position may be reached by multiple paths.
+ --
+ -- The system may read, but may not write to this location.
| UMostlyClobbered
+ -- ^ This location has been clobbered but it is available
+ -- for backtracking.
+ --
+ -- The system may not read from this location.
| UClobbered
+ -- ^ This location has been clobbered and is unavailable
+ -- even in the trail.
+ --
+ -- The system may issue neither reads nor writes to this
+ -- location.
deriving (Bounded, Enum, Eq, Ord, Show)
{-
--- /dev/null
+module Dyna.XXX.TestFramework where
+
+import Data.Monoid
+import Test.Framework
+
+moreTests :: Int -> Test -> Test
+moreTests n = plusTestOptions
+ $ mempty
+ { topt_maximum_generated_tests = Just n
+ }
+
+
+moreTries :: Int -> Test -> Test
+moreTries n = plusTestOptions
+ $ mempty
+ { topt_maximum_unsuitable_generated_tests = Just n
+ }
+
+withTimeout :: Int -> Test -> Test
+withTimeout n = plusTestOptions
+ $ mempty
+ { topt_timeout = Just $ Just n }
projects / dyna2 / commitdiff