From: Nathaniel Wesley Filardo Date: Fri, 12 Apr 2013 03:49:55 +0000 (-0400) Subject: Snapshot before more surgery X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=17a898082bc7c44d9341200dc2a70e9e5ff61c5e;p=dyna2 Snapshot before more surgery --- diff --git a/src/Dyna/Analysis/Mode/Execution/Base.hs b/src/Dyna/Analysis/Mode/Execution/Context.hs similarity index 66% rename from src/Dyna/Analysis/Mode/Execution/Base.hs rename to src/Dyna/Analysis/Mode/Execution/Context.hs index 535dd3e..8618aa8 100644 --- a/src/Dyna/Analysis/Mode/Execution/Base.hs +++ b/src/Dyna/Analysis/Mode/Execution/Context.hs @@ -5,6 +5,7 @@ -- fly. -- Header material {{{ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -16,17 +17,13 @@ {-# 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(..), @@ -40,53 +37,31 @@ module Dyna.Analysis.Mode.Execution.Base ( 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 _) = "" - -------------------------------------------------------------------------}}} -- Insts: Inst Keys (§5.3.1, p94) {{{ -- | An aliased variable, also known as an Inst Key. See §5.3.1, p94. @@ -128,6 +103,7 @@ 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) @@ -137,6 +113,7 @@ 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 {{{ @@ -145,11 +122,11 @@ type UR f n k u = InstF f (VR n k u) 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) @@ -158,62 +135,39 @@ data VR n k u = ------------------------------------------------------------------------}}} -- 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 {{{ @@ -233,11 +187,12 @@ key_canon k = do 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 () @@ -248,7 +203,7 @@ key_lookup k = do 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 @@ -281,10 +236,12 @@ instance (Show f, Monad m) => MCM (SIMCT m f) KI where 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 @@ -303,67 +260,24 @@ 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. @@ -396,16 +310,16 @@ unalias s k0 = do 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 @@ -413,7 +327,6 @@ instance (Show f, Monad m) => MCR (SIMCT m f) VV where 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 @@ -463,7 +376,7 @@ instance (Show f, Monad m) => MCA (SIMCT m f) VV where -- 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)@ -- @@ -477,13 +390,11 @@ instance (Show f, Monad m) => MCA (SIMCT m f) VV where -- -- * @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')@ ------------------------------------------------------------------------}}} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/Functions.hs b/src/Dyna/Analysis/Mode/Execution/Functions.hs index 4b4d221..ed72e7d 100644 --- a/src/Dyna/Analysis/Mode/Execution/Functions.hs +++ b/src/Dyna/Analysis/Mode/Execution/Functions.hs @@ -1,242 +1,168 @@ --------------------------------------------------------------------------- -- | 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 @@ -244,10 +170,8 @@ unifyNK :: forall f k m n . 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 @@ -266,10 +190,8 @@ unifyEE l (Right qa) (Left nb) = do 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 @@ -279,10 +201,8 @@ unifyQQ l qa qb = do 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 @@ -295,8 +215,7 @@ 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, 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 @@ -305,65 +224,49 @@ unifyKK :: (Eq k, Ord f, Ord n, MonadFix m, Show k, Show n, 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 @@ -379,121 +282,142 @@ unifyVV lf va vb = -- 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 @@ -517,31 +441,46 @@ subVN v n = XT.traceShow ("SVN",v,n) $ do -- 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) +-} + ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/NamedInst.hs b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs new file mode 100644 index 0000000..d10b5dc --- /dev/null +++ b/src/Dyna/Analysis/Mode/Execution/NamedInst.hs @@ -0,0 +1,507 @@ +--------------------------------------------------------------------------- +-- | 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)) +-} + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index cabd6e9..eb9658c 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -14,32 +14,38 @@ -- 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 {{{ @@ -87,7 +93,7 @@ data InstF f i = -- 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 @@ -99,7 +105,7 @@ data InstF f i = -- -- 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 @@ -110,26 +116,42 @@ data InstF f i = -- 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 {{{ @@ -152,13 +174,15 @@ inIGamma (RA r t) (IBound u ts) = r == uniqGamma u -- | 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 @@ -168,11 +192,11 @@ iWellFormed_ :: (Monad m) -> 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@. @@ -244,10 +268,10 @@ iLeq_ _ _ (IAny _) _ = return $ False 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 @@ -256,10 +280,20 @@ iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && u' <= u) $ -- 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 @@ -271,34 +305,42 @@ iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && u' <= u) $ -- 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 (⊑) @@ -326,10 +368,10 @@ iSub_ _ _ (IAny _) _ = return $ False 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 @@ -339,14 +381,24 @@ iSub_ _ q (IBound u m b) (IBound u' m' b') = andM1 (u <= u' && b <= b') $ {-# 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') @@ -354,15 +406,15 @@ iSubGLB_ _ _ _ (IAny u') (IUniv u) = return $ IUniv (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' @@ -377,37 +429,59 @@ iSubGLB_ _ _ q (IBound u m b) (IBound u' m' b') = do 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_ #-} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/InstSelftest.hs b/src/Dyna/Analysis/Mode/InstSelftest.hs deleted file mode 100644 index 56304a3..0000000 --- a/src/Dyna/Analysis/Mode/InstSelftest.hs +++ /dev/null @@ -1,82 +0,0 @@ ---------------------------------------------------------------------------- --- | 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) - diff --git a/src/Dyna/Analysis/Mode/Selftest.hs b/src/Dyna/Analysis/Mode/Selftest.hs new file mode 100644 index 0000000..3acccdd --- /dev/null +++ b/src/Dyna/Analysis/Mode/Selftest.hs @@ -0,0 +1,6 @@ +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 ] diff --git a/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs new file mode 100644 index 0000000..73ab6fd --- /dev/null +++ b/src/Dyna/Analysis/Mode/Selftest/NamedInst.hs @@ -0,0 +1,164 @@ +--------------------------------------------------------------------------- +-- | 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] diff --git a/src/Dyna/Analysis/Mode/Selftest/Term.hs b/src/Dyna/Analysis/Mode/Selftest/Term.hs new file mode 100644 index 0000000..954ead7 --- /dev/null +++ b/src/Dyna/Analysis/Mode/Selftest/Term.hs @@ -0,0 +1,43 @@ +{-# 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) + ] + + diff --git a/src/Dyna/Analysis/Mode/Unification.hs b/src/Dyna/Analysis/Mode/Unification.hs new file mode 100644 index 0000000..7ab6f01 --- /dev/null +++ b/src/Dyna/Analysis/Mode/Unification.hs @@ -0,0 +1,80 @@ +--------------------------------------------------------------------------- +-- | 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 + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Uniq.hs b/src/Dyna/Analysis/Mode/Uniq.hs index 84463ca..5b4c907 100644 --- a/src/Dyna/Analysis/Mode/Uniq.hs +++ b/src/Dyna/Analysis/Mode/Uniq.hs @@ -21,17 +21,37 @@ module Dyna.Analysis.Mode.Uniq(Uniq(..)) where -- 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) {- diff --git a/src/Dyna/XXX/TestFramework.hs b/src/Dyna/XXX/TestFramework.hs new file mode 100644 index 0000000..19a8c12 --- /dev/null +++ b/src/Dyna/XXX/TestFramework.hs @@ -0,0 +1,22 @@ +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 }