From cb280b867e0990a6c8a4ac1043a74c4caf439632 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 7 Feb 2013 03:47:36 -0500 Subject: [PATCH] Some bits of Overton's mode system for Mercury The beginnings of a re-implementation of Mercury's mode system, as described in: 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. --- src/Dyna/Analysis/Mode/Det.hs | 40 ++++ src/Dyna/Analysis/Mode/Inst.hs | 326 +++++++++++++++++++++++++++++++++ src/Dyna/Analysis/Mode/Uniq.hs | 92 ++++++++++ 3 files changed, 458 insertions(+) create mode 100644 src/Dyna/Analysis/Mode/Det.hs create mode 100644 src/Dyna/Analysis/Mode/Inst.hs create mode 100644 src/Dyna/Analysis/Mode/Uniq.hs diff --git a/src/Dyna/Analysis/Mode/Det.hs b/src/Dyna/Analysis/Mode/Det.hs new file mode 100644 index 0000000..8c27f1b --- /dev/null +++ b/src/Dyna/Analysis/Mode/Det.hs @@ -0,0 +1,40 @@ +--------------------------------------------------------------------------- +-- | Reimplementation of the Mercury mode system (Determinism) +-- +-- This module contains the definitions of determinism and +-- primitive predicates defined by the thesis. + +-- Header material {{{ +{-# OPTIONS_GHC -Wall #-} +module Dyna.Analysis.Mode.Det(Det(..), detLt) where +------------------------------------------------------------------------}}} +-- Determinism {{{ + +-- | Mercury determinism (Table 2.2, p24) +-- +-- The 'Ord' instance is solely for internal use; for reasoning, use lattice +-- functions. +data Det = DetErroneous -- ^ At most zero results, and yet cannot fail + | DetFailure -- ^ Exactly zero results + | Det -- ^ Exactly one result + | DetSemi -- ^ Zero or one result + | DetMulti -- ^ At least one result + | DetNon -- ^ At least zero results + deriving (Eq, Ord, Show) + +-- | Determinism lattice transitive, non-reflexive partial ordering function +-- +-- Figure 2.4, p25 +detLt :: Det -> Det -> Bool +detLt DetErroneous b = b /= DetErroneous +detLt DetFailure DetSemi = True +detLt DetFailure DetNon = True +detLt Det DetSemi = True +detLt Det DetMulti = True +detLt Det DetNon = True +detLt DetSemi DetNon = True +detLt DetMulti DetNon = True +detLt _ _ = False +{-# INLINE detLt #-} + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs new file mode 100644 index 0000000..fc77bc4 --- /dev/null +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -0,0 +1,326 @@ +--------------------------------------------------------------------------- +-- | 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 + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Uniq.hs b/src/Dyna/Analysis/Mode/Uniq.hs new file mode 100644 index 0000000..84463ca --- /dev/null +++ b/src/Dyna/Analysis/Mode/Uniq.hs @@ -0,0 +1,92 @@ +--------------------------------------------------------------------------- +-- | 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) } +-} + +------------------------------------------------------------------------}}} -- 2.50.1