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