--- /dev/null
+---------------------------------------------------------------------------
+-- | Reimplementation of the Mercury mode system (Inst)
+--
+-- This module contains the definitions of instantiation states and the
+-- primitive predicates on insts. For clarity and flexibility of
+-- implementation, many of these primitive predicates are parameterized on
+-- some 'Monad' and defined in terms of open recursion. This leaves it to
+-- 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.
+
+-- Header material {{{
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -Wall #-}
+module Dyna.Analysis.Mode.Inst(
+ InstF(..),
+ iNotReached, iIsNotReached,
+ iUniq, iWellFormed_, iGround_, iSub_, iSubGLB_, iLeq_, iLeqGLB_,
+) where
+
+-- import Control.Monad
+import qualified Data.Foldable as F
+import qualified Data.Traversable as T
+import qualified Data.Map as M
+-- import qualified Data.Set as S
+import Dyna.XXX.MonadUtils
+
+import Dyna.Analysis.Mode.Uniq
+
+------------------------------------------------------------------------}}}
+-- Instantiation States {{{
+
+-- | Instantiation states, parametric in Prolog functor @f@ with open
+-- recursion through @i@.
+--
+-- We differ from the thesis and the mercury implementation (see prose, p60,
+-- \"Obviously, it is not...\") in the use of open recursion rather than a
+-- @defined_inst@ branch in the @InstF@. Rather, we use a disjunctive @i@.
+-- Similarly, we use our disjunctive @i@ rather than a separate @alias@
+-- constructor (see figure 5.3, p94).
+--
+-- It's also worth pointing out, while here, that the mode system is
+-- concerned only with actual data, not types. There is clearly some
+-- overlap with a type system, and we may wish to investigate adding typing
+-- information to this system rather than brew an entirely separate type
+-- system (XXX). In particular, the importance here is that 'IBound' and
+-- 'IUniv' should be viewed as intersected with the type information, if
+-- any.
+--
+-- Based on figure 5.3, p94 (but see figure 3.17, p50, for easier cases)
+--
+-- The 'Ord' instance is solely for internal use; for reasoning, use lattice
+-- functions.
+data InstF f i =
+ -- | An unbound inst.
+ --
+ -- If you like a machine-core representation-centric view of
+ -- the universe, such a thing is a pointer whose own space has
+ -- been allocated already but is not pointing to anything yet.
+ -- Rules which bind free variables engage in allocation and
+ -- fill in these holes.
+ 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.
+ --
+ -- Note that we are saying nothing about the possible data
+ -- bound by this variable; that would be the job of the type
+ -- system.
+ | IAny !Uniq
+
+ -- | A bound inst. More specifically, a disjunction of
+ -- possible binding states: it's guaranteed to be one of these
+ -- functors and its associated insts.
+ --
+ -- Note that defition 3.2.11 (p50) requires that the
+ -- uniqueness of the inner Insts be below by <=
+ -- (see the 'iWellformed' predicate below)
+ --
+ -- The Bool field, which is an extension from the thesis,
+ -- indicates the possibility that this inst is
+ -- bound to a base-case of the term universe.
+ --
+ -- XXX It's possible that we would want a @[TBaseSkolem]@
+ -- field for tracking which base-cases, or even a @[TBase]@
+ -- field for recording possible actual base-cases, too,
+ -- but one thing at a time.
+ --
+ -- Definition 3.2.18, p52:
+ -- @not_reached(u) === IBound u M.empty False@.
+ -- @not_reached === not_reached(UUnique)@.
+ | IBound !Uniq
+ !(M.Map f [i])
+ !Bool
+
+ -- | This one is not in the thesis exposition but is used during
+ -- computation to represent the entire universe of ground
+ -- terms. See prose, p63, \"For efficiency, we treat ground...\".
+ --
+ -- Defninition 3.2.17, p52 is thus rewritten:
+ -- @ground(u) === IUniv u@.
+ | IUniv !Uniq
+
+ -- XXX Mercury has a concept of \"higher-order modes\", which we
+ -- do not yet support (though there is grumbling about it in
+ -- the background). See 3.2.4 p55 et seq.
+
+ deriving (Eq, F.Foldable, Functor, Ord, Show, T.Traversable)
+
+------------------------------------------------------------------------}}}
+-- Instantiation States: Unary predicates {{{
+
+{-
+-- | 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, p51
+inIGamma :: RA (UTerm (RTerm f) v) -> Inst f -> Bool
+inIGamma _ IFree = True
+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.
+--
+-- Based on definition 3.2.13, p51 but see prose, p51, \"Note that there is
+-- no uniqueness annotation on the free inst\" -- we choose to make that
+-- explicit here.
+iUniq :: InstF f i -> Uniq
+iUniq IFree = UUnique
+iUniq (IAny u) = u
+iUniq (IBound u _ _) = u
+iUniq (IUniv u) = u
+{-# INLINE iUniq #-}
+
+-- | Check that an instantiation state is well-formed as per defintion
+-- 3.2.11, p50.
+iWellFormed_ :: (Monad m)
+ => (Uniq -> i -> m Bool)
+ -> Uniq -> InstF f i
+ -> m Bool
+iWellFormed_ _ _ IFree = return True
+iWellFormed_ _ u' (IAny u) = return $ u <= u'
+iWellFormed_ q u' (IBound u b _) = if u <= u'
+ then mfmamm (q u) b
+ else return False
+iWellFormed_ _ u' (IUniv u) = return $ u <= u'
+-- iWellFormed_ _ u' (INotReached u) = return $ u <= u'
+{-# INLINE iWellFormed_ #-}
+
+-- | Is an instantiation ground?
+--
+-- Surrogate for definition 3.2.17, p52
+iGround_ :: (Monad m) => (i -> m Bool) -> InstF f i -> m Bool
+iGround_ q (IBound UUnique b _) = mfmamm q b
+iGround_ _ (IUniv _) = return True
+iGround_ _ _ = return False
+
+------------------------------------------------------------------------}}}
+-- Instantiation States: Binary predicates {{{
+
+-- | Instantiatedness partial order with uniqueness
+--
+-- IAny `iLeq` IAny is declared (prose, p46, \"We allow...\") to be unsafe
+-- in general but safe for reasoning about forward execution (recall defn
+-- 3.1.10, p34). XXX I do not understand.
+--
+-- Definition 3.2.14, p51
+iLeq_ :: (Eq f, Monad m)
+ => (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
+iLeq_ _ _ (IAny _) _ = return $ False
+iLeq_ _ _ (IUniv u) (IAny u') = return $ u' <= u
+iLeq_ _ _ (IUniv u) (IUniv u') = return $ u' <= u
+iLeq_ _ _ (IUniv _) _ = return $ False
+iLeq_ q _ (IBound u b _) r@(IAny u') = andM1 (u' <= u) $
+ mfmamm (flip q r) b
+iLeq_ q _ (IBound u b _) r@(IUniv u') = andM1 (u' <= u) $
+ mfmamm (flip q r) b
+iLeq_ _ q (IBound u b _) (IBound u' b' _) = andM1 (u' <= u) $
+ mapForallM (\f is -> mapExistsM (\f' is' -> andM1 (f == f') $
+ allM $ zipWith q is is'
+ ) b'
+ ) b
+ -- 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_ #-}
+
+
+-- | Compute the GLB under iLeq_
+iLeqGLB_ :: (Monad m, Ord f)
+ => (i -> i -> m i)
+ -> InstF f i
+ -> InstF f i
+ -> m (InstF f i)
+iLeqGLB_ _ IFree x = return x
+iLeqGLB_ _ x IFree = return x
+
+iLeqGLB_ _ (IAny u) (IAny u') = return $ IAny (max u u')
+
+iLeqGLB_ _ (IAny u') (IUniv u) = return $ IUniv (max u u')
+iLeqGLB_ _ (IUniv u) (IAny u') = return $ IUniv (max u u')
+iLeqGLB_ _ (IUniv u) (IUniv u') = return $ IUniv (max u u')
+
+iLeqGLB_ _ (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_ _ (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_ 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
+
+-- | Matches partial order with uniqueness
+--
+-- Definition 3.2.15, p51
+iSub_ :: (Eq f, Monad m)
+ => (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
+iSub_ _ _ (IAny u) (IAny u') = return $ u <= u'
+iSub_ _ _ (IAny _) _ = return $ False
+iSub_ _ _ (IUniv u) (IAny u') = return $ u <= u'
+iSub_ _ _ (IUniv u) (IUniv u') = return $ u <= u'
+iSub_ _ _ (IUniv _) _ = return $ False
+iSub_ q _ (IBound u b _) r@(IAny u') = andM1 (u <= u') $
+ mfmamm (flip q r) b
+iSub_ q _ (IBound u b _) r@(IUniv u') = andM1 (u <= u') $
+ mfmamm (flip q r) b
+iSub_ _ q (IBound u b _) (IBound u' b' _) = andM1 (u <= u') $
+ mapForallM (\f is -> mapExistsM (\f' is' -> andM1 (f == f') $
+ allM $ zipWith q is is'
+ ) b'
+ ) b
+ -- 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
+
+-- | Compute the GLB under iSub_
+iSubGLB_ :: (Ord f, Monad m)
+ => (i -> i -> m i)
+ -> InstF f i -> InstF f i -> m (Maybe (InstF f i))
+iSubGLB_ _ IFree IFree = return $ Just IFree
+iSubGLB_ _ IFree _ = return $ Nothing
+iSubGLB_ _ _ IFree = return $ Nothing
+
+iSubGLB_ _ (IAny u) (IAny u') = return $ Just $ IAny (min u u')
+
+iSubGLB_ _ (IAny u') (IUniv u) = return $ Just $ IUniv (min u u')
+iSubGLB_ _ (IUniv u) (IAny u') = return $ Just $ IUniv (min u u')
+iSubGLB_ _ (IUniv u) (IUniv u') = return $ Just $ IUniv (min u u')
+
+iSubGLB_ _ (IBound u m b) (IAny u') = return $ Just $ IBound (min u u') m b
+iSubGLB_ _ (IAny u') (IBound u m b) = return $ Just $ IBound (min u u') m b
+
+iSubGLB_ _ (IBound u m b) (IUniv u') = return $ Just $ IBound (min u u') m b
+iSubGLB_ _ (IUniv u') (IBound u m b) = return $ Just $ IBound (min u u') m b
+
+iSubGLB_ q (IBound u m b) (IBound u' m' b') = do
+ m'' <- mergeBoundLB q m m'
+ return $! Just $! IBound (min u u') m'' (b && b')
+
+-- iSubGLB_ _ a@(INotReached _) _ = return $ Just a
+-- iSubGLB_ _ _ a@(INotReached _) = return $ Just a
+-- iSubGLB_ _ _ _ = return $ Nothing
+
+------------------------------------------------------------------------}}}
+-- Instantiation States: Utility Functions {{{
+
+iNotReached :: Uniq -> InstF f i
+iNotReached u = IBound u M.empty False
+
+iIsNotReached :: InstF f i -> Bool
+iIsNotReached (IBound _ m False) = M.null m
+iIsNotReached _ = False
+
+-- | A common pattern we encounter in unary predicates, so let's just pull
+-- it out.
+mfmamm :: Monad m => (a -> m Bool) -> M.Map k [a] -> m Bool
+mfmamm f = mapForallM (\_ -> allM . map f)
+
+-- | Compute the lower bound of two guts of IBound constructors.
+mergeBoundLB :: (Monad m, Ord f)
+ => (i -> i -> m i)
+ -> M.Map f [i] -> M.Map f [i] -> m (M.Map f [i])
+mergeBoundLB q lm rm = M.foldrWithKey fold (return M.empty)
+ $ M.intersectionWith (,) lm rm
+ where
+ fold f (lis,ris) mm = do
+ m <- mm
+ is <- sequence $ zipWith q lis ris
+ return $ M.insert f is m
+
+------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- | Reimplementation of the Mercury mode system (Uniqueness)
+--
+-- This module contains the definitions of uniqueness annotations and
+-- primitive predicates defined by the thesis.
+--
+-- Much of the material here is not actually needed (and thus commented out
+-- and probably a little stale) but is used in the mathematical machinery of
+-- the thesis; it was implemented during a sort of rote transcription and
+-- may prove useful for testing later.
+
+-- Header material {{{
+{-# OPTIONS_GHC -Wall #-}
+module Dyna.Analysis.Mode.Uniq(Uniq(..)) where
+------------------------------------------------------------------------}}}
+-- Uniqueness Annotations {{{
+
+-- | Mercury uniqueness annotations (figure 3.15, p48)
+--
+-- Ord instance is ⊴ from definition 3.2.10 (p48). Intuitively, if u1 <=
+-- u2, then it is safe to use u1 in a context expecting u2.
+--
+-- The Mostly variants are intended (see p26) to handle trailing (i.e. undo
+-- logs). See also the discussion on p48
+data Uniq = UUnique
+ -- ^ All references are known to the mode analysis system.
+ --
+ -- In a system without alias tracking, this more obviously
+ -- means \"unique reference\" (see prose, p90, \"This is a
+ -- subtle change in what we mean by unique.\").
+ | UMostlyUnique
+ | UShared
+ | UMostlyClobbered
+ | UClobbered
+ deriving (Bounded, Enum, Eq, Ord, Show)
+
+{-
+-- | Reference counts are bounded below by 0 or 1.
+--
+-- Figure 3.16, p49
+data URCL = Urcl0 | Urcl1 deriving (Bounded,Enum,Eq,Ord,Show)
+
+-- | Reference counts are bounded above by 1 or infinity.
+--
+-- Figure 3.16, p49
+data URCH = Urch1 | UrchI deriving (Bounded,Enum,Eq,Ord,Show)
+type URCC = (URCL, URCH)
+newtype URC = URC (URCC, URCC) deriving (Eq,Show)
+
+-- | Uniqueness concretization function
+--
+-- A section of 'uniqAlpha'.
+--
+-- Figure 3.16, p49
+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, p49
+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
+--
+-- p49
+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
+-}
+
+------------------------------------------------------------------------}}}
+-- Reference-count-Annotated Terms {{{
+
+{-
+data RA t = RA URC t
+ deriving (Eq{-F.Foldable-},Functor,Show{-,T.Traversable-})
+
+newtype RTerm f t = RTerm { rterm :: TermF f (RA t) }
+-}
+
+------------------------------------------------------------------------}}}
projects / dyna2 / commitdiff