ghc-prim >= 0.3,
HUnit >=1.2,
mtl >=2.1,
+ lens >=3.8,
parsers >=0.5,
+ recursion-schemes >=3.0,
reducers >=3.0,
semigroups >=0.8,
tagged >= 0.4.4,
template-haskell,
+ transformers >= 0.3,
trifecta >= 1.0,
unification-fd,
unordered-containers>=0.2,
containers >=0.4,
haskeline >=0.6,
mtl >=2.1,
+ lens >=3.8,
parsers >=0.5,
process >=1.1,
+ recursion-schemes >=3.0,
reducers >=3.0,
semigroups >=0.8,
tagged >= 0.4.4,
+ transformers >= 0.3,
trifecta >= 1.0,
unification-fd,
unordered-containers>=0.2,
haskeline >=0.6,
HUnit >=1.2,
mtl >=2.1,
+ lens >=3.8,
parsers >=0.5,
process >=1.1,
+ recursion-schemes >=3.0,
reducers >=3.0,
semigroups >=0.8,
tagged >= 0.4.4,
+ transformers >= 0.3,
trifecta >= 1.0,
unification-fd,
unordered-containers>=0.2,
ghc-prim >= 0.3,
HUnit >=1.2,
mtl >=2.1,
+ lens >=3.8,
parsers >=0.5,
process >=1.1,
+ QuickCheck >= 2.5,
+ recursion-schemes >=3.0,
reducers >=3.0,
semigroups >=0.8,
tagged >= 0.4.4,
template-haskell,
test-framework >=0.6,
test-framework-hunit >=0.2,
+ test-framework-quickcheck2 >=0.3,
test-framework-th >=0.2,
test-framework-golden >= 1.1,
+ transformers >= 0.3,
trifecta >= 1.0,
unification-fd,
unordered-containers>=0.2,
---------------------------------------------------------------------------
--- | Reimplementation of the Mercury mode system, following David Overton's
--- 2003 Ph.D. thesis.
+-- | Reimplementation of the Mercury mode system
--
--- David Overton. Precise and expressive mode systems for typed logic
--- programming languages.
+-- For this module and all modules under Dyna.Analysis.Mode, we are
+-- incredibly indebted to David Overton and the Mercury Prolog system:
+-- David Overton. Precise and Expressive Mode Systems for Typed Logic
+-- Programming Languages. University of Melbourne, Department of Computer
+-- Science and Software Engineering. Ph.D. thesis. December, 2003.
-- <http://www.mercury.csse.unimelb.edu.au/information/papers.html#dmo-thesis>
+--
+-- The sub-modules have been organized in an effort to be as transparently
+-- ascriptive to the thesis as possible. This module is primarily concerned
+-- with execution details which are not part of the thesis exposition,
+-- primarily by running computable algorithms over the regular trees of the
+-- thesis.
+
+-- XXX This file is, at this point, mostly detritus from development and
+-- will be cleaned up real soon now.
-- Header material {{{
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wall #-}
module Dyna.Analysis.Mode(
- -- * Uniqueness annotations
- Uniq(..),
- -- ** Reference counts
- URCL(..), URCH(..), URC(..), uniqGamma, uniqAlpha, uniqLeq,
- -- * Instantiation States
- Inst(..), iUniq, iWellFormed, iLeq, iSub, iGround
+
+ iuWellFormed, iuCompare, iuLeq, iuSub,
+ -- * Instantiation Key Maps
+ -- InstKeyMap(..), InstKeyVal(..),
+ -- * Instantiation contexts
+ -- IMLookup(..), IMAssign(..),
+ -- * Modes
+ -- Mode(..), -- mWellFormed,
+
+ module Dyna.Analysis.Mode.Det,
+ module Dyna.Analysis.Mode.Uniq,
+ module Dyna.Analysis.Mode.Inst,
+ -- module Dyna.Analysis.Mode.InstMap,
+ module Dyna.Analysis.Mode.Execution.Base,
+ module Dyna.Analysis.Mode.Execution.Functions,
) where
-import Control.Unification
-import qualified Data.Foldable as F
-import qualified Data.Map as M
-import qualified Data.Traversable as T
-import Dyna.Term.TTerm
+import Control.Applicative
+import Control.Exception(assert)
+import Control.Lens
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Trans.Maybe
+import qualified Data.Foldable as F
+import qualified Data.Map as M
+import qualified Data.Set as S
+import qualified Data.Traversable as T
+import Dyna.Analysis.Mode.Execution.Base
+import Dyna.Analysis.Mode.Execution.Functions
+import Dyna.Analysis.Mode.Det
+import Dyna.Analysis.Mode.Inst
+-- import Dyna.Analysis.Mode.InstMap
+import Dyna.Analysis.Mode.Uniq
import Dyna.XXX.DataUtils
+import Dyna.XXX.MonadContext
+import Dyna.XXX.MonadUtils
------------------------------------------------------------------------}}}
--- Uniqueness Modes {{{
+-- Instantiation contexts {{{
--- | Mercury uniqueness annotations (figure 3.15, page 48)
-data Uniq = UUnique
- | UMostlyUnique
- | UShared
- | UMostlyClobbered
- | UClobbered
- deriving (Eq, Ord, Show)
+{-
+class (Monad m, Ord v) => IMLookup m f v | m -> f v where
+ vlookup :: v -> m (InstF f v)
--- | Reference counts are bounded below by 0 or 1.
---
--- Figure 3.16, page 49
-data URCL = Urcl0 | Urcl1 deriving (Eq,Ord,Show)
+class (Monad m, Ord v, IMLookup m f v) => IMAssign m f v where
+ vassign :: v -> InstF f v -> m ()
+-}
--- | Reference counts are bounded above by 1 or infinity.
+{-
+-- | Very often we need to recurse through the variable context and stop as
+-- soon as we loop. (Since variables may well be knot-tied to support
+-- mu-recursive types, for example.)
--
--- Figure 3.16, page 49
-data URCH = Urch1 | UrchI deriving (Eq,Ord,Show)
-type URCC = (URCL, URCH)
-newtype URC = URC (URCC, URCC) deriving (Eq,Show)
+-- The folder is applicative
+ctxRecurse :: (Ord v, Ord a, IMLookup m f v)
+ => (a -> InstF f v -> Either [(v,a)] r) -- ^ Single step
+ -> (r -> m r -> m r) -- ^ Folder
+ -> r -- ^ Zero answer
+ -> r -- ^ Cycle answer
+ -> a -> InstF f v -> m r
+ctxRecurse step fold zr cr = go S.empty
+ where
+ go stk a i = case step a i of
+ Left is -> foldM (fold_ stk) zr is
+ Right r -> return r
--- | Uniqueness concretization function
---
--- A section of 'uniqAlpha'.
---
--- Figure 3.16, page 49
-uniqGamma :: Uniq -> URC
-uniqGamma UClobbered = URC ((Urcl0, UrchI), (Urcl0, UrchI))
-uniqGamma UMostlyClobbered = URC ((Urcl0, UrchI), (Urcl1, UrchI))
-uniqGamma UShared = URC ((Urcl1, UrchI), (Urcl1, UrchI))
-uniqGamma UMostlyUnique = URC ((Urcl1, Urch1), (Urcl1, UrchI))
-uniqGamma UUnique = URC ((Urcl1, Urch1), (Urcl1, Urch1))
-
--- | Uniqueness abstraction function
---
--- A retraction of 'uniqGamma'.
---
--- Figure 3.16, page 49
-uniqAlpha :: URC -> Uniq
-uniqAlpha (URC ((Urcl0, _ ), (Urcl0, _ ))) = UClobbered
-uniqAlpha (URC ((Urcl0, _ ), _ )) = UMostlyClobbered
-uniqAlpha (URC ((Urcl1, Urch1), (Urcl1, Urch1))) = UUnique
-uniqAlpha (URC ((Urcl1, Urch1), _ )) = UMostlyUnique
-uniqAlpha (URC (_ , _ )) = UShared
-
--- | Partial ordering on uniqueness
---
--- page 49
-uniqLeq :: URC -> URC -> Bool
-uniqLeq (URC (f, b)) (URC (f', b')) = f `ci` f' && b `ci` b'
- where ci (la, ua) (lb, ub) = lb <= la && ua <= ub
+ fold_ stk r (v,a) = if S.member (v,a) stk
+ then fold r (return cr)
+ else fold r $ do
+ i <- vlookup v
+ go (S.insert (v,a) stk) a i
+-}
------------------------------------------------------------------------}}}
--- Reference-count-Annotated Terms {{{
+-- Instantiation operations {{{
+
+
+iuWellFormed :: forall f i m v .
+ (MCVT m i ~ (InstF f i), MCR m i, Ord i,
+ MCVT m v ~ (Either i (InstF f (Either v i))), MCR m v, Ord v)
+ => Uniq -> v -> m Bool
+iuWellFormed u0 v0 = evalStateT (q u0 v0) S.empty
+ where
+ qe u (Left v) = q u v
+ qe u (Right i) = lift $ nWellFormed u i
+
+ q :: Uniq -> v -> StateT (S.Set v) m Bool
+ q u vu = do
+ looped <- gets $ S.member vu
+ if looped
+ then return False
+ else do
+ modify $ S.insert vu
+ i <- lift $ clookup vu
+ case i of
+ Left vi -> lift $ nWellFormed u vi
+ Right i' -> iWellFormed_ qe u i'
+
+
+iuCompare :: forall eiv f i ir m tm v .
+ (MCVT m i ~ InstF f i, MCR m i, Ord i, Ord f,
+ MCVT m v ~ Either i ir, MCR m v, Ord v,
+ tm ~ StateT (S.Set (eiv,ir), S.Set (eiv,eiv)) m,
+ ir ~ InstF f eiv,
+ eiv ~ Either i v)
+ => ( forall m' . (Monad m')
+ => (eiv -> ir -> m' Bool)
+ -> (eiv -> eiv -> m' Bool)
+ -> ir -> ir -> m' Bool)
+ -> v -> v -> m Bool
+iuCompare cmp i0 j0 = evalStateT (qb (Right i0) (Right j0)) (S.empty, S.empty)
+ where
+ rq = cmp qa qb
+
+ ll :: eiv -> tm ir
+ ll = either (liftM (fmap Left) . lift . clookup) lq
+ where
+ lq x = do
+ x' <- lift $ clookup x
+ either (liftM (fmap Left) . lift . clookup) return x'
+
+ qa (v :: eiv) j = do
+ already <- gets $ S.member (v,j) . fst
+ if already
+ then return True
+ else do
+ modify $ over _1 (S.insert (v,j))
+ i <- ll v
+ rq i j
+ -- XXX? qb vi vj | vi == vj = return True
+ qb (vi :: eiv) (vj :: eiv) = do
+ already <- gets $ S.member (vi,vj) . snd
+ if already
+ then return True
+ else do
+ modify $ over _2 (S.insert (vi,vj))
+ i <- ll vi
+ j <- ll vj
+ rq i j
+
+iuLeq, iuSub :: forall f i v m .
+ (Ord i, Ord f, Ord v, Monad m,
+ MCVT m i ~ InstF f i, MCR m i,
+ MCVT m v ~ Either i (InstF f (Either i v)), MCR m v)
+ => v -> v -> m Bool
+iuLeq = iuCompare iLeq_
+iuSub = iuCompare iSub_
-data RA t = RA URC t
- deriving (Eq,F.Foldable,Functor,Show,T.Traversable)
-newtype RTerm f t = RTerm { rterm :: TermF f (RA t) }
------------------------------------------------------------------------}}}
--- Instantiation States {{{
+-- Instantiation Maps {{{
+
+{-
+chkial m = goV S.empty S.empty
+ where
+ goV vis stk v = case M.lookup v m of
+ Just i -> go vis stk i
+ Nothing -> Left v
+
+ goI vis stk (IAlias v) =
+ case () of
+ _ | v `S.member` stk -> Left v -- ERR: cycle
+ _ | v `S.member` vis -> Right vis -- OK: already cleared
+ _ -> goV (S.insert v vis) (S.insert v stk) -- WORK: chase cycle
+ goI vis _ _ = Right vis -- OK: Productive step
+
+-- | Test the well-formedness of an 'InstMap' and return a witness variable
+-- that is problematic, if any.
+imWellFormed :: InstMap f v -> Maybe v
+imWellFormed IMNotReached = Nothing
+imWellFormed (IM m) = foldr checker S.empty (M.keys m)
--- | Instantiation states, parametric in functor @f@.
---
--- figure 3.17, page 50
-data Inst f = IFree
- | IAny Uniq
- | IBound Uniq (M.Map f [Inst f])
- deriving (Eq, Ord, Show)
+
+go S.empty S.empty (M.keys m)
+ where
+ go _ _ [] = Nothing
+ go vis as (v:vs) =
+ if v `S.elem` vis
+ then go vis S.empty vs -- Been here and it's OK
+ else case M.lookup v m of
+ Nothing -> Just v -- Whoop, that's bad.
+ Just i -> check vs vis as i
+-}
{-
--- | Test if a term is in the set generated by the inst concretization
--- function.
---
--- Use as @term `inIGamma` inst@.
---
--- Surrogate for definition 3.2.12, page 51
-inIGamma :: RA (UTerm (RTerm f) v) -> Inst f -> Bool
-inIGamma _ IFree = True
-inIGamma (RA r _) (IAny u) = r == uniqGamma u
-inIGamma (RA r t) (IBound u ts) = r == uniqGamma u
- && undefined -- XXX
+refineIM_ v i i' m s =
+ case i `iLeqGLB_` i' of
+ Nothing -> IMNotReached (M.delete v m) (S.insert v s)
+ -- XXX Just (INotReached _) -> IMNotReached (M.delete v m) (S.insert v s)
+ Just iglb -> IM (M.insert v iglb m)
+
+refineIM :: (Ord v, Eq f) => v -> InstF f i -> InstMap f v i -> InstMap f v i
+refineIM v i (IM m) =
+ let i0 = maybe IFree id $ M.lookup v m in
+ assert (i `iLeq_` i0) $ refineIM_ v i i0 m S.empty
+refineIM v _ im@(IMNotReached _ s) | v `S.member` s = im
+refineIM v i (IMNotReached m s) =
+ let i0 = maybe IFree id $ M.lookup v m in
+ assert (i `iLeq_` i0) $ refineIM_ v i i0 m s
-}
--- | Uniqueness function
---
--- definition 3.2.13, page 51
-iUniq :: Inst f -> Maybe Uniq
-iUniq (IAny u) = Just $ u
-iUniq (IBound u _) = Just $ u
-iUniq IFree = Nothing
-
--- | Check that an instantiation state is well-formed as per defintion
--- 3.2.11, page 50.
---
--- XXX This ought to be enforced statically!
-iWellFormed :: Uniq -> Inst f -> Bool
-iWellFormed _ IFree = True
-iWellFormed u' (IAny u) = u <= u'
-iWellFormed u' (IBound u b) = u <= u'
- && mapForall (const $ all (iWellFormed u)) b
-
--- | Instantiatedness partial order with uniqueness
---
--- Definition 3.2.14, page 51
-iLeq :: (Eq f) => Inst f -> Inst f -> Bool
-iLeq _ IFree = True
-iLeq (IAny u) (IAny u') = u' <= u
-iLeq (IBound u b) r@(IAny u') = u' <= u &&
- mapForall (\_ is -> all (flip iLeq r) is) b
-iLeq (IBound u b) (IBound u' b') = u' <= u &&
- mapForall (\f is -> mapExists (\f' is' -> f == f' &&
- and (zipWith iLeq is is')
- ) b'
- ) b
-iLeq _ _ = False
-
--- | Matches partial order with uniqueness
---
--- Definition 3.2.15, page 51
-iSub :: (Eq f) => Inst f -> Inst f -> Bool
-iSub IFree IFree = True
-iSub (IBound _ b) IFree = b == M.empty -- not_reached(u)
-iSub (IAny u) (IAny u') = u <= u'
-iSub (IBound u b) r@(IAny u') = u <= u' &&
- mapForall (\_ is -> all (flip iSub r) is) b
-iSub (IBound u b) (IBound u' b') = u <= u' &&
- mapForall (\f is -> mapExists (\f' is' -> f == f' &&
- and (zipWith iSub is is')
- ) b'
- ) b
-iSub _ _ = False
-
--- | Is an instantiation ground?
+
+{-
+instance (Monad m, Ord v) => IMLookup (StateT (InstMap f v v) m) f v where
+ vlookup v = get >>= return . imLookup v
+-}
+
+
+------------------------------------------------------------------------}}}
+-- Instantiation Key Maps {{{
+
+{-
+-- | An instantiation key map is the representation of the prolog abstract
+-- machine's binding patterns. That is, it maps every prolog variable @u@
+-- to another variable or an Inst, which in turn recurses to contain either
+-- prolog variables or defined (possibly recursive)
+newtype InstKeyMap f u v = IKM { unIKM :: M.Map u (InstKeyVal f u v) }
+
+data InstKeyVal f u v = IKVUser u
+ | IKVName v
+ | IKVInst (InstF f (Either u v))
+
+class (Monad m, Ord u) => IKMLookup m f u v | m -> f u v where
+ ulookup :: u -> m (InstKeyVal f u v)
+
+class (Monad m, Ord u, IKMLookup m f u v) => IKMAssign m f u v where
+ uassign :: u -> InstKeyVal f u v -> m ()
+
+ikmSemiprune :: (Ord u, MonadState (InstKeyMap f u v) m) => u -> m u
+ikmSemiprune u = do
+ m <- gets unIKM
+ let (u', m') = mapSemiprune q IKVUser u m
+ put (IKM m')
+ return u'
+ where q (IKVUser u') = Just u'
+ q _ = Nothing
+
+instance (Monad m, Ord u) => IKMLookup (StateT (InstKeyMap f u v) m) f u v where
+ ulookup u = do
+ u' <- ikmSemiprune u
+ m' <- get
+ case M.lookup u' (unIKM m') of
+ Just (IKVUser u'') | u' == u'' -> do
+ put $ IKM $ M.insert u' (IKVInst IFree) (unIKM m')
+ return (IKVUser u')
+ Just (IKVUser _) -> error "ikmSemiprune bug"
+ Just i -> return i
+ Nothing -> error "ulookup XXX" -- XXX
+
+{-
+instance (Monad m, Ord u) => IKMAssign (StateT (InstKeyMap f u v) m) f u v where
+ uassign u ikv = modify (IKM . M.insert u ikv . unIKM)
+-}
+
+{-
+abstract_unify :: InstKeyMap f u v -> u -> u -> Maybe (InstKeyMap f u v)
+abstract_unify ikm u1 u2 =
+ u1' <- ikmSemiprune u1 ikm
+ u2' <- ikmSemiprune u2 ikm
+ abstract_unify_core ikm'' u1' u2'
+
+abstract_unify_core :: InstKeyMap f u v -> InstKeyVal f u v -> InstKeyVal f u v -> Maybe (InstKeyMap f u v)
+abstract_unify_core = undefined
+-}
+
+-}
+
+------------------------------------------------------------------------}}}
+-- Abstract Interpretation {{{
+
+
+
+
+------------------------------------------------------------------------}}}
+-- Mode {{{
+
+-- XXX While this type works fine for the thesis, for us it's a little bit
+-- of bad news: we need to have both of these maps in scope as we go about
+-- reasoning. That means we're going to need to freshen these into our
+-- current global store and do operations there. It may not be so bad, but
+-- this also kind of sucks.
--
--- Surrogate for definition 3.2.17, page 52
-iGround :: Inst f -> Bool
-iGround (IBound UUnique b) = mapForall (\_ -> all iGround) b
-iGround _ = False
+-- It's also another argument in favor of some later attempt to have the
+-- scope maps canonicalize themselves as we go.
+-- | Mode
+--
+-- Definition 3.1.10, p34
+-- data Mode f v i = Mode { m_ini :: InstMap f v i
+-- , m_fin :: InstMap f v i}
+{-
+-- | Well-formedness condition on modes. Definition 3.1.10, p35
+mWellFormedV :: (MCR m v (InstF f v), Ord f, Ord v) => Mode f v v -> m Bool
+mWellFormedV (Mode {m_init = mi, m_fin = mf}) =
+ let kmi = imKeys mi
+ in andM1 (kmi == (imKeys mf)) $
+ setForallM (\v -> imLookup v mf `iLeq` imLookup v mi) kmi
+-}
------------------------------------------------------------------------}}}
-- Header material {{{
{-# OPTIONS_GHC -Wall #-}
-module Dyna.Analysis.Mode.Det(Det(..), detLt) where
+module Dyna.Analysis.Mode.Det(Det(..), detLt, detLe) where
------------------------------------------------------------------------}}}
-- Determinism {{{
detLt DetSemi DetNon = True
detLt DetMulti DetNon = True
detLt _ _ = False
-{-# INLINE detLt #-}
+{-# INLINABLE detLt #-}
+
+-- | Determinism lattice transitive, reflexive partial ordering function
+detLe :: Det -> Det -> Bool
+detLe a b | a == b = True
+detLe a b = detLt a b
+{-# INLINABLE detLe #-}
------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | Basics of actually running the mode system reasoner.
+
+-- XXX when we need to consider expand_shared, we will also do that on the
+-- fly.
+
+-- Header material {{{
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Mode.Execution.Base (
+ -- * Inst Types
+ -- ** Naming Conventions
+ -- $naming
+
+ -- ** Named Insts
+ NI(..), di_unique, di_inst,
+ -- ** Inst Keys (§5.3.1, p94)
+ KI(..), KR(..), KRI, ENKRI,
+ -- ** Unaliased Insts
+ UI(..), UR,
+ -- ** Variables
+ VV(..), VR(..),
+
+ -- * Context
+ -- ** Notes
+ -- $context
+
+ -- ** Monad
+ SIMCT(..), runSIMCT,
+ -- *** And its context
+ SIMCtx(..), emptySIMCtx,
+
+ -- ** Internal helper functions
+ aliasW,
+)where
+
+import Control.Exception(assert)
+import Control.Lens
+import Control.Monad
+import Control.Monad.State
+import Data.Function
+import qualified Data.Map as M
+import qualified Data.Traversable as T
+import Data.Unique
+import Dyna.Analysis.Mode.Inst
+import Dyna.XXX.DataUtils
+import Dyna.XXX.MonadContext
+import qualified Debug.Trace as XT
+
+------------------------------------------------------------------------}}}
+-- 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 { _di_unique :: Unique
+ , _di_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 _di_unique
+
+instance Show (NI f) where
+ show (NI u _) = "<NI h=" ++ (show $ hashUnique u) ++ ">"
+
+------------------------------------------------------------------------}}}
+-- Insts: Inst Keys (§5.3.1, p94) {{{
+
+-- | An aliased variable, also known as an Inst Key. See §5.3.1, p94.
+--
+-- We use 'Int' internally for the moment
+newtype KI = KI { unKI :: Int } deriving (Eq,Num,Ord,Show)
+
+-- | Key InstMap Values. These represent aliased bits of structure built up
+-- during analysis.
+--
+-- Periodically, we will attempt to collect structure that is no longer
+-- aliased and move it back to the un-aliased map. As long as something is
+-- in here, however, the interpretation should be that it is certainly
+-- aliased.
+--
+-- Inst Keys are defined to be acyclic (though we really should be running
+-- an occurs check during analysis XXX)
+--
+-- See thesis, section 5.3.1
+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)
+ deriving (Eq,Ord,Show)
+
+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
+-- of an inst which appropriately recurses ('KRI'). Using this rather than
+-- 'KR' directly in our (e.g.) 'MCR' instance ensures that we cannot leak
+-- 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 n k u =
+ -- | Defined named inst (unaliased)
+ VRName n
+ -- | Unaliased structure
+ | VRStruct u
+ -- | Aliased structure
+ | VRKey k
+ deriving (Eq,Ord,Show)
+
+------------------------------------------------------------------------}}}
+------------------------------------------------------------------------}}}
+-- Context {{{
+-- Context : Basics {{{
+data SIMCtx f = SIMCtx { {- _simctx_next_iv :: NI
+ , _simctx_map_iv :: InstMap f NI NI
+ , -}
+ _simctx_next_k :: KI
+ , _simctx_next_u :: UI
+
+ , _simctx_map_k :: M.Map KI (KR f (NI f) KI)
+ , _simctx_map_u :: M.Map UI (UR f (NI f) KI UI)
+ , _simctx_map_v :: M.Map VV (VR (NI f) KI UI)
+ }
+ deriving (Show)
+$(makeLenses ''SIMCtx)
+
+newtype SIMCT m f a = SIMCT { unSIMCT :: StateT (SIMCtx f) 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) => 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
+
+{-
+-- 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
+
+instance (Monad m) => MCW (SIMCT m f) NI (InstF f NI) where
+ cassign v b = SIMCT $ simctx_map_iv %= (imAssign v b)
+
+instance (Monad m) => MCF (SIMCT m f) NI where
+ cfresh = SIMCT $ do
+ x <- simctx_next_iv <+= 1
+ return x
+-}
+
+------------------------------------------------------------------------}}}
+-- Context : Aliased Keys {{{
+
+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
+ simctx_map_k .= m'
+ return k'
+ where
+ isKey (KRKey x) = Just x
+ isKey _ = Nothing
+
+key_lookup :: (MonadState (SIMCtx f) m, Show f)
+ => KI
+ -> m (ENKRI f (NI 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)))
+ krenkri
+ $ M.lookup ck m
+ XT.traceShow ("KL",k,ck,r) $ return ()
+ return r
+ where
+ krenkri (KRKey k') = error $ "User context noncanonical: "
+ ++ (show (k,k'))
+ krenkri (KRName n) = Left n
+ krenkri (KRInst i) = Right i
+
+type instance MCVT (SIMCT m f) KI = ENKRI f (NI f) KI
+
+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
+ r <- key_lookup k
+ simctx_map_k %= M.delete 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)
+-}
+
+instance (Show f, Monad m) => MCM (SIMCT m f) KI where
+ cmerge f k v = SIMCT $ do
+ ck <- key_canon k
+ m <- use simctx_map_k
+ mm <- maybe (assert (ck == k) $
+ return $ M.insert k (either KRName KRInst v) m)
+ (\v' -> do
+ merged <- unSIMCT $ f (krenkri v') v
+ return $ M.insert ck (either KRName KRInst merged) m)
+ $ M.lookup ck m
+ simctx_map_k .= mm
+ where
+ krenkri (KRKey k') = error $ "User context noncanonical in merge: "
+ ++ (show (k,k'))
+ krenkri (KRName n) = Left n
+ krenkri (KRInst i) = Right i
+
+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)
+ return k
+
+instance (Show f, Monad m) => MCA (SIMCT m f) KI where
+ ccanon k = SIMCT $ key_canon k
+
+ -- Since everything in this table is already aliased, just do the merge
+ -- and make one arbitrarily point at the other.
+ calias f l r = SIMCT $ do
+ cl <- key_canon l
+ cr <- key_canon r
+ 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)
+ 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
+
+-- | Move an unaliased structure to the aliased table
+aliasW :: forall f n k u 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
+
+aliasX :: forall f n k u 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
+
+{-
+-- | Called when we are moving a singleton alias key to unaliased structure.
+unalias :: forall f n k u m .
+ (Monad m,
+ MCVT m u ~ UR f n k u,
+ MCR m u, MCN m u,
+ MCVT m k ~ ENKRI f n k,
+ MCR m k, MCD m k)
+ => (k -> m Bool)
+ -> k
+ -> m (Either n u)
+unalias s k0 = do
+ lk <- cdelete k0
+ case lk of
+ Left n -> return $ Left n
+ Right r -> liftM Right $ T.sequence (fmap move r) >>= cnew
+ where
+ move :: Either n k -> m (VR n k u)
+ move (Left n) = return $ VRName n
+ move (Right k) = do
+ also <- s k
+ if also
+ then liftM (either VRName VRStruct) $ unalias s k
+ else return $ VRKey k
+-}
+
+------------------------------------------------------------------------}}}
+-- Context : User Variables {{{
+
+user_lookup :: (MonadState (SIMCtx f) m, Show f)
+ => VV
+ -> m (VR (NI f) KI UI)
+user_lookup v = do
+ m <- use simctx_map_v
+ r <- maybe (error $ "Unaliased 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
+
+instance (Show f, Monad m) => MCR (SIMCT m f) VV where
+ clookup = SIMCT . user_lookup
+
+instance (Show f, Monad m) => MCW (SIMCT m f) VV where
+ cassign v w = SIMCT $ simctx_map_v %= M.insert v w
+
+
+instance (Show f, Monad m) => MCA (SIMCT m f) VV where
+ ccanon x = return x
+
+ calias f l r = SIMCT $ do
+ vl <- user_lookup l
+ vr <- user_lookup r
+ x <- unSIMCT $ f vl vr >>= aliasX
+ let x' = VRKey x
+ simctx_map_v %= M.insert l x'
+ simctx_map_v %= M.insert r x'
+ return l
+
+------------------------------------------------------------------------}}}
+------------------------------------------------------------------------}}}
+-- Haddock Sections {{{
+-- Contexts {{{
+
+-- $context
+--
+-- We track three sorts of things in our context:
+--
+-- 1. Inst Keys, which are handles to aliased bits of structure. An Inst
+-- Key handle 'KI' binds a 'KR'.
+--
+-- 2. Unaliased structure handles. Such a handle 'UI' binds a 'UR',
+-- which is exactly a ply of an inst which recurses as a named inst, a
+-- key, or another bit of unaliased structure.
+--
+-- 3. User variables, which again are bound to either a named inst, a
+-- key, or another bit of unaliased structure.
+--
+-- XXX The context implementation given here is not ideal, but it is
+-- hopefully viable.
+--
+-- Rather than follow a strict interpretation of the thesis, which uses
+-- expand/2 and expand'/2 to eliminate user variables (``inst keys''), we
+-- implicitly do the expansion at the points where it becomes necessary
+-- during comparison.
+
+------------------------------------------------------------------------}}}
+-- Notes on Naming Conventions {{{
+
+-- $naming
+-- NAMING CONVENTIONS
+--
+-- We have a lot of types flying around, so let's get a shorthand for some
+-- of them. Despite the proliferation, much of the implementation is
+-- type-directed, so it's not so bad.
+--
+-- * @N@ -- 'NI'
+--
+-- * @I@ -- @'InstF' f ('NI' f)@
+--
+-- * @K@ -- 'KI'
+--
+-- * @R@ -- 'KR'
+--
+-- * @Q@ -- 'KRI' (i.e. @'InstF' f ('Either' ('NI' f) 'KI')@)
+--
+-- * @E@ -- 'ENKRI' (i.e. @'Either' n ('InstF' f ('Either' ('NI' f) 'KI'))@
+--
+-- * @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'
+
+------------------------------------------------------------------------}}}
+------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | Execution-oriented aspects of functions we might actually want to
+-- call during mode analysis.
+--
+
+-- Header material {{{
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wall #-}
+
+module Dyna.Analysis.Mode.Execution.Functions(
+ -- * Named inst functions
+ nWellFormed, nGround, nLeq, nLeqGLB, nSub, nSubGLB, nSubLUB,
+ -- * Unification
+ unifyVV,
+ -- * Matching
+) where
+
+import Control.Lens
+import Control.Monad.State
+import Control.Monad.Trans.Maybe
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Dyna.Analysis.Mode.Execution.Base
+import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Uniq
+import Dyna.XXX.MonadContext
+import qualified Debug.Trace as XT
+
+------------------------------------------------------------------------}}}
+-- Named inst functions {{{
+
+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)
+
+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 = evalStateT (qb i0 j0) (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
+
+
+
+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 :: (MonadFix m, Ord n, MCVT m n ~ InstF f n, MCR m n, MCN m n, Ord f)
+ => 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')
+
+-- | 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)
+ => 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
+
+-- | 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)
+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)
+ => 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, 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)
+ => 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, 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)
+ => 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, 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)
+ => 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, 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, 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
+
+-- | 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 ~ InstF f (VR n k u), MCD m u, MCR m u)
+ => Bool -> u -> u -> m k
+unifyUU _ a b | a == b = cdelete a >>= aliasW
+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)
+ => Bool
+ -> VR n k u
+ -> VR n k u
+ -> m k
+unifyXX l (VRName na) (VRName nb) = unifyNN l na nb >>= cnew . Left
+unifyXX l (VRName na) (VRKey kb) = unifyNK l na kb
+unifyXX l (VRName na) (VRStruct ub) = do
+ kb <- cdelete ub >>= aliasW
+ 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
+ unifyKK l ka kb
+unifyXX l (VRStruct ua) (VRName nb) = do
+ ka <- cdelete ua >>= aliasW
+ unifyNK l nb ka
+unifyXX l (VRStruct ua) (VRKey kb) = do
+ ka <- cdelete ua >>= aliasW
+ unifyKK l ka kb
+unifyXX l (VRStruct ua) (VRStruct ub) = unifyUU l ua ub
+
+-- | Variable-on-variable unification. Ah, finally.
+unifyVV :: 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, 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)
+ => v
+ -> v
+ -> m v
+unifyVV va vb = calias (\a' b' -> liftM VRKey $ unifyXX True {- XXX -} a' b') va vb
+
+
+------------------------------------------------------------------------}}}
-- the outer 'Monad' to deal with (or not, if termination isn't important ;)
-- ) a lot of technicalities that would obscure the exposition of the
-- thesis' material.
+--
+-- The thesis has one big datatype for all branches of Inst, with
+-- restrictions that some branches may not be used in certain places.
+-- 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'.
-- Header material {{{
{-# LANGUAGE DeriveFoldable #-}
module Dyna.Analysis.Mode.Inst(
InstF(..),
iNotReached, iIsNotReached,
- iUniq, iWellFormed_, iEq_, iGround_,
+ iUniq, iIsFree, iWellFormed_, iEq_, iGround_,
iLeq_, iLeqGLB_,
iSub_, iSubGLB_, iSubLUB_,
) where
--
-- The 'Ord' instance is solely for internal use; for reasoning, use lattice
-- functions.
-data InstF f i =
+data InstF f i =
-- | An unbound inst.
--
-- If you like a machine-core representation-centric view of
-- been allocated already but is not pointing to anything yet.
-- Rules which bind free variables engage in allocation and
-- fill in these holes.
+ --
+ -- XXX a boolean flag is introduced in §5.4.1, p103; that
+ -- is not yet plumbed through here.
IFree
-- | A possibly-bound inst. We have lost track of whether or
- -- not the given variable is free. We may not pass such a
- -- thing to a predicate expecting a bound variable, and any
- -- predicate expecting a free variable must be prepared to
- -- check and engage in unification, rather than allocation,
- -- with the possible (partial) structure bound here.
+ -- not the given variable is free. Note that this has runtime
+ -- implications: we actively need a bit of data to indicate
+ -- whether this value is bound or free, so that we may
+ -- dynamically dispatch. That has implications for any call
+ -- whose mode results in the creation of an 'IAny' inst.
--
-- Note that we are saying nothing about the possible data
-- bound by this variable; that would be the job of the type
-- possible binding states: it's guaranteed to be one of these
-- functors and its associated insts.
--
+ -- The thesis uses sets inside bound, but has the caveat that
+ -- a function symbol may occur at most once (defn 3.1.2, p31),
+ -- which justifies our use of 'M.Map' here.
+ --
-- 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
inIGamma _ IBoundUniverse = True
inIGamma (RA r _) (IAny u) = r == uniqGamma u
inIGamma (RA r t) (IBound u ts) = r == uniqGamma u
- && undefined -- XXX
+ && ...
-}
-- | Extract the uniqueness from an inst.
iUniq (IAny u) = u
iUniq (IBound u _ _) = u
iUniq (IUniv u) = u
-{-# INLINE iUniq #-}
+{-# INLINABLE iUniq #-}
-- | Check that an instantiation state is well-formed as per defintion
-- 3.2.11, p50.
then mfmamm (q u) b
else return False
iWellFormed_ _ u' (IUniv u) = return $ u <= u'
--- iWellFormed_ _ u' (INotReached u) = return $ u <= u'
-{-# INLINE iWellFormed_ #-}
+{-# INLINABLE iWellFormed_ #-}
+
+-- | Compare with 'IFree' without imposing @Eq i@.
+iIsFree :: InstF f i -> Bool
+iIsFree IFree = True
+iIsFree _ = False
-- | Is an instantiation ground?
--
iGround_ q (IBound UUnique b _) = mfmamm q b
iGround_ _ (IUniv _) = return True
iGround_ _ _ = return False
+{-# INLINABLE iGround_ #-}
------------------------------------------------------------------------}}}
-- Instantiation States: Binary predicates {{{
-- | Equality of two insts
iEq_ :: (Ord f, Monad m)
- => (i -> i -> m Bool)
- -> InstF f i -> InstF f i -> m Bool
+ => (i -> i' -> m Bool)
+ -> InstF f i -> InstF f i' -> m Bool
iEq_ _ IFree IFree = return $ True
iEq_ _ _ IFree = return $ False
iEq_ _ IFree _ = return $ False
Just is' -> allM $ zipWith q is is'
iEq_ _ (IBound _ _ _) (IBound _ _ _)
| otherwise = return False
+{-# INLINABLE iEq_ #-}
-- | Instantiatedness partial order with uniqueness (≼)
--
--
-- Definition 3.2.14, p51 (see also definitions 3.1.4 (p32) and 3.2.5 (p46))
iLeq_ :: (Ord f, Monad m)
- => (i -> InstF f i -> m Bool)
- -> (i -> i -> m Bool)
- -> InstF f i -> InstF f i -> m Bool
+ => (i -> InstF f i' -> m Bool)
+ -> (i -> i' -> m Bool)
+ -> InstF f i -> InstF f i' -> m Bool
iLeq_ _ _ _ IFree = return $ True
iLeq_ _ _ IFree _ = return $ False
iLeq_ _ _ (IAny u) (IAny u') = return $ u' <= u
Nothing -> return False
Just is' -> allM $ zipWithTails q crf crf is is'
-- XXX Ought to assert that length is == length is'
-{-
-iLeq_ _ (INotReached u) (IAny u') = return $ u' <= u
-iLeq_ _ (INotReached u) (IUniv u') = return $ u' <= u
-iLeq_ _ (INotReached u) (INotReached u') = return $ u' <= u
--}
-{-# INLINE iLeq_ #-}
-
+{-# INLINABLE iLeq_ #-}
-- | Compute the GLB under iLeq_ (⋏)
--
-- Since iLeq (≼) is a lattice, this is a total function.
+--
+-- 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
+-- is that, because we do not know the type information, we are viewing
+-- insts as intersected with the type system, so we cannot actually know
+-- when we might have hit notreached (we have one-sided error, but we want
+-- to know the other side, as it were). Instead, we'll use some surrogate
+-- tests that are restrictive but safe (such as shallow testing for free
+-- variables).
+
iLeqGLB_ :: (Monad m, Ord f)
- => (i -> i -> m i)
- -> InstF f i
+ => (i -> m i'')
+ -> (i' -> m i'')
+ -> (i -> i' -> m i'')
-> InstF f i
- -> m (InstF f i)
-iLeqGLB_ _ IFree x = return x
-iLeqGLB_ _ x IFree = return x
+ -> InstF f i'
+ -> 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) (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_ _ _ _ (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_ _ (IBound u m b) (IAny u') = return $ IBound (max u u') m b
-iLeqGLB_ _ (IAny u') (IBound u m b) = return $ IBound (max u u') m b
+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_ _ (IBound u m b) (IUniv u') = return $ IBound (max u u') m b
-iLeqGLB_ _ (IUniv u') (IBound u m b) = return $ IBound (max u u') m b
+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
+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_ _ a@(INotReached _) _ = return $ Just a
--- iLeqGLB_ _ _ a@(INotReached _) = return $ Just a
+{-# INLINABLE iLeqGLB_ #-}
-- | Matches partial order with uniqueness (⊑)
--
-- Definition 3.2.15, p51 (see also definitions 3.1.11 (p35) and 3.2.7
-- (p46))
iSub_ :: (Ord f, Monad m)
- => (i -> InstF f i -> m Bool)
- -> (i -> i -> m Bool)
- -> InstF f i
+ => (i -> InstF f i' -> m Bool)
+ -> (i -> i' -> m Bool)
-> InstF f i
+ -> InstF f i'
-> m Bool
iSub_ _ _ IFree IFree = return $ True
--- iSub_ _ (INotReached _) IFree = return $ True
iSub_ _ _ x@(IBound _ _ _) IFree | iIsNotReached x = return $ True
iSub_ _ _ IFree _ = return $ False
iSub_ _ _ _ IFree = return $ False
Nothing -> return False
Just is' -> allM $ zipWithTails q crf crf is is'
-- XXX Ought to assert that length is == length is'
--- iSub_ _ (INotReached u) (IAny u') = return $ u <= u'
--- iSub_ _ (INotReached u) (IUniv u') = return $ u <= u'
--- iSub_ _ _ _ = return $ False
+{-# INLINABLE iSub_ #-}
-- | Compute the GLB under iSub_ (⊓)
iSubGLB_ :: (Ord f, Monad m)
- => (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)
-
-iSubGLB_ _ (IAny u) (IAny u') = return $ IAny (min u u')
-
-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_ _ (IBound u m b) (IAny u') = return $ IBound (min u u') m b
-iSubGLB_ _ (IAny u') (IBound u m b) = return $ IBound (min u u') m b
-
-iSubGLB_ _ (IBound u m b) (IUniv u') = return $ IBound (min u u') m b
-iSubGLB_ _ (IUniv u') (IBound u m b) = return $ IBound (min u u') m b
-
-iSubGLB_ q (IBound u m b) (IBound u' m' b') = do
+ => (i -> m 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)
+
+iSubGLB_ _ _ _ (IAny u) (IAny u') = return $ IAny (min u u')
+
+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) (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_ _ _ q (IBound u m b) (IBound u' m' b') = do
let u'' = min u u'
-- NOTE: I was briefly concerned that we would have to pass u'' down
-- through q, but since the well-formedness criteria may be assumed to
-- part.
m'' <- mergeBoundLB q m m'
return $ IBound u'' m'' (b && b')
-
--- iSubGLB_ _ a@(INotReached _) _ = return $ Just a
--- iSubGLB_ _ _ a@(INotReached _) = return $ Just a
--- iSubGLB_ _ _ _ = return $ Nothing
+{-# INLINABLE iSubGLB_ #-}
-- | Compute the LUB under iSub_ (⊔)
--
-- 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 -> 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_ q (IBound u m b) (IBound u' m' b') = do
- m'' <- mergeBoundUB q m m'
+ => (i -> m i'')
+ -> (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')
+{-# INLINABLE iSubLUB_ #-}
------------------------------------------------------------------------}}}
-- Instantiation States: Utility Functions {{{
-- the empty set of (non-ground) terms.
iNotReached :: Uniq -> InstF f i
iNotReached u = IBound u M.empty False
+{-# INLINABLE iNotReached #-}
-- | Indicator function for 'iNotReached'
iIsNotReached :: InstF f i -> Bool
iIsNotReached (IBound _ m False) = M.null m
iIsNotReached _ = False
+{-# INLINABLE iIsNotReached #-}
crf :: (Monad m) => a -> m Bool
crf = const $ return False
-- | Compute the lower bound of two guts of IBound constructors.
mergeBoundLB :: (Monad m, Ord f)
- => (i -> i -> m a)
- -> M.Map f [i] -> M.Map f [i] -> m (M.Map f [a])
+ => (i -> i' -> m a)
+ -> M.Map f [i] -> M.Map f [i'] -> m (M.Map f [a])
mergeBoundLB q lm rm = T.sequence $ M.intersectionWith (\a b -> sequence $ zipWith q a b) lm rm
-- | Compute the upper bound of two guts of IBound constructors.
mergeBoundUB :: (Monad m, Ord f)
- => (i -> i -> m i)
- -> M.Map f [i] -> M.Map f [i] -> m (M.Map f [i])
-mergeBoundUB q lm rm = T.sequence
+ => (i -> i' -> m i'')
+ -> (i -> m i'')
+ -> (i' -> m i'')
+ -> M.Map f [i] -> M.Map f [i'] -> m (M.Map f [i''])
+mergeBoundUB q l r lm rm = T.sequence
$ M.mergeWithKey (\_ a b -> Just $ sequence $ zipWith q a b)
- (fmap return) (fmap return)
+ (fmap (T.mapM l))
+ (fmap (T.mapM r))
lm rm
------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | Reimplementation of the Mercury mode system (Inst)
+--
+-- This module contains the functionality for InstMaps, which are maps from
+-- keys to openly-recursive InstF plys.
+--
+-- XXX This module is likely junk given the current implementation effort,
+-- but is here for completeness. It may go away later.
+
+module Dyna.Analysis.Mode.InstMap where
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Dyna.Analysis.Mode.Uniq
+import Dyna.Analysis.Mode.Inst
+
+-- | Options for a user variable binding
+data UVarF f i u =
+ -- | Another user variable; we use this instead of the @alias()@
+ -- construction of the thesis. Note that user-variable bindings are
+ -- required to be in the least fixed point (unlike inst bindings).
+ VUser u
+ -- | An Inst key.
+ | VIVar i
+ -- | An 'InstF' ply, which may recurse as either a user var @u@ or
+ -- an inst key @i@.
+ | VInst (InstF f (Either u i))
+
+-- | An InstMap tells us how to interpret variables @v@ used in our insts,
+-- which recurse as @i@.
+--
+-- The intent is that @v@ is a projection of @i@, possibly @i@ itself.
+data InstMap f v i =
+ -- | As soon as /any/ 'Inst' in the map becomes @not_reached@
+ -- (see the commentary on 'IBound'), the entire system configuration is
+ -- not reachable.
+ --
+ -- This carries a map of non-@not_reached@ variables and a set of
+ -- @not_reached@ values, which must be nonempty.
+ IMNotReached (M.Map v (InstF f i)) (S.Set v)
+
+ -- | Most of the time, however, the system state is reachable.
+ --
+ -- As a result of 'IMNotReached' there is an invariant on the map here,
+ -- coded as 'imWellFormed', which is that every 'IBound' constructor in
+ -- the map actually has at least one possible disjunct.
+ | IM (M.Map v (InstF f i))
+ deriving (Show)
+
+-- | The empty 'InstMap'
+imEmpty :: InstMap f v i
+imEmpty = IM M.empty
+
+-- | The variables explicitly known about in this map
+imKeys :: (Ord v) => InstMap f v i -> S.Set v
+imKeys (IM m) = M.keysSet m
+imKeys (IMNotReached m s) = S.union s (M.keysSet m)
+
+-- | Fetch the binding of a variable
+imLookup :: (Ord v, Show v) => v -> InstMap f v i -> InstF f i
+imLookup v (IM m) = maybe (error $ "InstMap miss: " ++ (show v)) id
+ $ M.lookup v m
+imLookup _ (IMNotReached _ _) = (iNotReached UUnique)
+
+-- | Assign and manage the notreached invariant
+imAssign :: (Ord v) => v -> InstF f i -> InstMap f v i -> InstMap f v i
+imAssign v i (IMNotReached m s) | iIsNotReached i = IMNotReached m (S.insert v s)
+imAssign v i (IMNotReached m s) = IMNotReached (M.insert v i m) s
+imAssign v i (IM m) | iIsNotReached i = IMNotReached m (S.singleton v)
+imAssign v i (IM m) = IM (M.insert v i m)
+
--- /dev/null
+---------------------------------------------------------------------------
+-- | Reimplementation of the Mercury mode system
+--
+-- This module implements some basic self-test functionality for the insts
+-- predicates in 'Dyna.Analysis.Mode.Insts'.
+
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Dyna.Analysis.Mode.InstSelftest where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Trans.Maybe
+import Data.Functor.Identity
+import qualified Data.Map as M
+import Dyna.Analysis.Mode.Inst
+import Dyna.Analysis.Mode.Uniq
+import qualified Test.Framework as TF
+import Test.Framework.Providers.QuickCheck2
+import Test.Framework.TH
+import Test.QuickCheck
+
+newtype Fix f = In { out :: f (Fix f) }
+deriving instance (Eq (f (Fix f))) => Eq (Fix f)
+deriving instance (Show (f (Fix f))) => Show (Fix f)
+deriving instance (Ord f, Arbitrary f) => Arbitrary (Fix (InstF f))
+
+instance Arbitrary Uniq where arbitrary = arbitraryBoundedEnum
+instance (Ord f, Arbitrary f, Arbitrary i) => Arbitrary (InstF f i) where
+ arbitrary = frequency [ (1,pure IFree)
+ , (1,IAny <$> arbitrary)
+ , (1,IUniv <$> arbitrary)
+ , (3,IBound <$> arbitrary
+ <*> sized (\s -> resize (s`div`2)
+ (M.fromList <$> arbitrary))
+ <*> arbitrary)
+ ]
+
+
+q1 f = \x y -> f (\a ob -> q1 f a (In ob))
+ (\a b -> q1 f a b)
+ (out x) (out y)
+
+qtb f = \x y -> In <$> f (\a b -> qtb f a b) (out x) (out y)
+
+qpb :: (Monad m, ff ~ Fix f, fff ~ f ff)
+ => ((ff -> ff -> MaybeT m ff)
+ -> fff -> fff -> MaybeT m (Maybe fff))
+ -> ff -> ff -> m (Maybe ff)
+qpb f x y = runMaybeT $ q x y
+ where q a b = maybe mzero (return . In) =<< f q (out a) (out b)
+
+qdLeq a b = runIdentity $ q1 iLeq_ a b
+qdLeqGLB a b = runIdentity $ qtb (iLeqGLB_ return return) a b
+qdSub a b = runIdentity $ q1 iSub_ a b
+qdSubGLB a b = runIdentity $ qtb (iSubGLB_ return return) a b
+qdSubLUB a b = runIdentity $ qpb (iSubLUB_ return return) a b
+
+prop_iLeq_GLB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property
+prop_iLeq_GLB i1 i2 = i1 `qdLeq` i2
+ ==> qdLeqGLB i1 i2 == i1
+
+prop_iSub_GLB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property
+prop_iSub_GLB i1 i2 = i1 `qdSub` i2
+ ==> qdSubGLB i1 i2 == i1
+
+prop_iSub_LUB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property
+prop_iSub_LUB i1 i2 = i1 `qdSub` i2
+ ==> qdSubLUB i1 i2 == (Just i2)
+
+selftest :: TF.Test
+selftest = $(testGroupGenerator)
+
+main :: IO ()
+main = $(defaultMainGenerator)
+
--- Bring together all of our test suites
-
+-- | Bring together all of our test suites
module Dyna.Main.TestsDriver where
+import Data.Monoid
import Test.Framework
+import qualified Dyna.Analysis.Mode.InstSelftest as DAMI
-- import qualified Dyna.Backend.K3.Selftest as DBK3S
-import qualified Dyna.Backend.Python.Selftest as DBPS
-import qualified Dyna.ParserHS.Selftest as DPHS
-import qualified Dyna.XXX.TrifectaTests as DXT
+import qualified Dyna.Backend.Python.Selftest as DBPS
+import qualified Dyna.ParserHS.Selftest as DPHS
+import qualified Dyna.XXX.TrifectaTests as DXT
main :: IO ()
main = defaultMain
[DPHS.selftest
, DXT.selftest
+ , moreTries 2000 $ DAMI.selftest
-- XXX Until this is meaningful...
-- ,DBK3S.selftest
- , DBPS.selftest
+ ,DBPS.selftest
]
+
+moreTries :: Int -> Test -> Test
+moreTries n = plusTestOptions
+ $ mempty
+ { topt_maximum_unsuitable_generated_tests = Just n
+ }
--- /dev/null
+---------------------------------------------------------------------------
+-- | Class definitions for "context" monads.
+
+-- Header material {{{
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+module Dyna.XXX.MonadContext(
+ MCVT, MCA(..), MCD(..), MCF(..), MCM(..), MCN(..), MCR(..), MCW(..),
+) where
+
+type family MCVT (m :: * -> *) (k :: *) :: *
+
+-- | The monad @m@ has a readable context of type @k -> v@
+class (Monad m) => MCR m k where
+ clookup :: k -> m (MCVT m k)
+
+-- | The monad @m@ has a writeable context of type @k -> v@
+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
+-- its context, provided a mechanism to merge values, if necessary.
+class (Monad m) => MCM m k where
+ cmerge :: (MCVT m k -> MCVT m k -> m (MCVT m k)) -> k -> (MCVT m k) -> m ()
+
+-- | It is possible to delete keys of type @k@ from the context @m@.
+class (Monad m) => MCD m k where
+ cdelete :: k -> m (MCVT m k)
+
+-- | The monad @m@ is able to fabricate new keys given only a value.
+-- This is likely especially useful when @m@ is 'MonadFix'.
+class (Monad m) => MCN m k where
+ cnew :: (MCVT m k) -> m k
+
+-- | The monad @m@ is able to generate new entities of type @k@.
+class (Monad m) => MCF m k where
+ cfresh :: m k
+
+-- | The monad @m@ understands variable aliasing.
+class (Monad m) => MCA m k where
+ -- | Canonicalize a key by semipruning
+ ccanon :: k -> m k
+
+ -- | Arbitrarily alias these two keys, given a mechanism to merge
+ -- their values. Returns some name for the resulting aliased
+ -- object (which need not be either of the inputs, if they
+ -- themselves were aliased, for example).
+ calias :: (MCVT m k -> MCVT m k -> m (MCVT m k)) -> k -> k -> m k
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-
module Dyna.XXX.MonadUtils(
-- * Data utilities generalizing 'Dyna.XXX.DataUtils'
mapForallM, mapExistsM, setForallM, setExistsM,
andM, andM1, orM, orM1, allM, anyM,
-- * MonadState utilities
bracketState, incState,
- -- * Context classes
- MCR(..), MCW(..), MCF(..),
) where
import Control.Applicative
+import Control.Lens
import Control.Monad.State
import qualified Data.Map as M
import qualified Data.Set as S
return (r, bs)
incState :: (Num a, MonadState a m) => m a
-incState = do
- s <- get
- put $! (s+1)
- return s
-
--- | Assert the the monad @m@ has a readable context of type @k -> v@
-class (Monad m) => MCR m k v | m k -> v where
- clookup :: k -> m v
-
-class (MCR m k v) => MCW m k v | m k -> v where
- cassign :: k -> v -> m ()
-
-class (Monad m) => MCF m k where
- cfresh :: m k
+incState = id <<%= (+1)
projects / dyna2 / commitdiff