From 3ad171796d1d250ad3769472a8940c064dea4a62 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 28 Feb 2013 23:48:29 -0500 Subject: [PATCH] Checkpoint effort on the Mercury mode system --- dyna.cabal | 14 + src/Dyna/Analysis/Mode.hs | 438 +++++++++++----- src/Dyna/Analysis/Mode/Det.hs | 10 +- src/Dyna/Analysis/Mode/Execution/Base.hs | 479 ++++++++++++++++++ src/Dyna/Analysis/Mode/Execution/Functions.hs | 344 +++++++++++++ src/Dyna/Analysis/Mode/Inst.hs | 234 +++++---- src/Dyna/Analysis/Mode/InstMap.hs | 71 +++ src/Dyna/Analysis/Mode/InstSelftest.hs | 82 +++ src/Dyna/Main/TestsDriver.hs | 20 +- src/Dyna/XXX/MonadContext.hs | 49 ++ src/Dyna/XXX/MonadUtils.hs | 22 +- 11 files changed, 1497 insertions(+), 266 deletions(-) create mode 100644 src/Dyna/Analysis/Mode/Execution/Base.hs create mode 100644 src/Dyna/Analysis/Mode/Execution/Functions.hs create mode 100644 src/Dyna/Analysis/Mode/InstMap.hs create mode 100644 src/Dyna/Analysis/Mode/InstSelftest.hs create mode 100644 src/Dyna/XXX/MonadContext.hs diff --git a/dyna.cabal b/dyna.cabal index 442b372..2f69428 100644 --- a/dyna.cabal +++ b/dyna.cabal @@ -45,11 +45,14 @@ Library 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, @@ -71,11 +74,14 @@ Executable drepl 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, @@ -100,11 +106,14 @@ Executable dyna 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, @@ -130,16 +139,21 @@ Test-suite dyna-selftests 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, diff --git a/src/Dyna/Analysis/Mode.hs b/src/Dyna/Analysis/Mode.hs index 3c1a02c..b87e724 100644 --- a/src/Dyna/Analysis/Mode.hs +++ b/src/Dyna/Analysis/Mode.hs @@ -1,174 +1,334 @@ --------------------------------------------------------------------------- --- | 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. -- +-- +-- 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 +-} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Det.hs b/src/Dyna/Analysis/Mode/Det.hs index 8c27f1b..993cd32 100644 --- a/src/Dyna/Analysis/Mode/Det.hs +++ b/src/Dyna/Analysis/Mode/Det.hs @@ -6,7 +6,7 @@ -- Header material {{{ {-# OPTIONS_GHC -Wall #-} -module Dyna.Analysis.Mode.Det(Det(..), detLt) where +module Dyna.Analysis.Mode.Det(Det(..), detLt, detLe) where ------------------------------------------------------------------------}}} -- Determinism {{{ @@ -35,6 +35,12 @@ detLt Det DetNon = True 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 #-} ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/Base.hs b/src/Dyna/Analysis/Mode/Execution/Base.hs new file mode 100644 index 0000000..0280388 --- /dev/null +++ b/src/Dyna/Analysis/Mode/Execution/Base.hs @@ -0,0 +1,479 @@ +--------------------------------------------------------------------------- +-- | 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 _) = "" + +------------------------------------------------------------------------}}} +-- 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' + +------------------------------------------------------------------------}}} +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Execution/Functions.hs b/src/Dyna/Analysis/Mode/Execution/Functions.hs new file mode 100644 index 0000000..83a202e --- /dev/null +++ b/src/Dyna/Analysis/Mode/Execution/Functions.hs @@ -0,0 +1,344 @@ +--------------------------------------------------------------------------- +-- | 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 + + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/Inst.hs b/src/Dyna/Analysis/Mode/Inst.hs index 79f1512..fa2a8c6 100644 --- a/src/Dyna/Analysis/Mode/Inst.hs +++ b/src/Dyna/Analysis/Mode/Inst.hs @@ -8,6 +8,13 @@ -- 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 #-} @@ -18,7 +25,7 @@ module Dyna.Analysis.Mode.Inst( InstF(..), iNotReached, iIsNotReached, - iUniq, iWellFormed_, iEq_, iGround_, + iUniq, iIsFree, iWellFormed_, iEq_, iGround_, iLeq_, iLeqGLB_, iSub_, iSubGLB_, iSubLUB_, ) where @@ -57,7 +64,7 @@ import Dyna.Analysis.Mode.Uniq -- -- 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 @@ -65,14 +72,17 @@ data InstF f i = -- 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 @@ -83,9 +93,13 @@ data InstF f i = -- 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 @@ -132,7 +146,7 @@ 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. @@ -145,7 +159,7 @@ iUniq IFree = UUnique 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. @@ -159,8 +173,12 @@ 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_ #-} +{-# INLINABLE iWellFormed_ #-} + +-- | Compare with 'IFree' without imposing @Eq i@. +iIsFree :: InstF f i -> Bool +iIsFree IFree = True +iIsFree _ = False -- | Is an instantiation ground? -- @@ -169,14 +187,15 @@ 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 +{-# 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 @@ -197,6 +216,7 @@ iEq_ q (IBound u b c) (IBound u' b' c') Just is' -> allM $ zipWith q is is' iEq_ _ (IBound _ _ _) (IBound _ _ _) | otherwise = return False +{-# INLINABLE iEq_ #-} -- | Instantiatedness partial order with uniqueness (≼) -- @@ -214,9 +234,9 @@ iEq_ _ (IBound _ _ _) (IBound _ _ _) -- -- 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 @@ -234,44 +254,52 @@ iLeq_ _ q (IBound u m b) (IBound u' m' b') = andM1 (b <= b' && 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 (⊑) -- @@ -284,13 +312,12 @@ iLeqGLB_ q (IBound u m b) (IBound u' m' b') = do -- 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 @@ -309,31 +336,35 @@ iSub_ _ q (IBound u m b) (IBound u' m' b') = andM1 (u <= u' && b <= b') $ 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 @@ -344,10 +375,7 @@ iSubGLB_ q (IBound u m b) (IBound u' m' b') = do -- 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_ (⊔) -- @@ -356,28 +384,31 @@ iSubGLB_ q (IBound u m b) (IBound u' m' b') = do -- 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 {{{ @@ -386,11 +417,13 @@ iSubLUB_ q (IBound u m b) (IBound u' m' b') = do -- 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 @@ -402,17 +435,20 @@ mfmamm f = mapForallM (\_ -> allM . map f) -- | 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 ------------------------------------------------------------------------}}} diff --git a/src/Dyna/Analysis/Mode/InstMap.hs b/src/Dyna/Analysis/Mode/InstMap.hs new file mode 100644 index 0000000..96e4e99 --- /dev/null +++ b/src/Dyna/Analysis/Mode/InstMap.hs @@ -0,0 +1,71 @@ +--------------------------------------------------------------------------- +-- | 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) + diff --git a/src/Dyna/Analysis/Mode/InstSelftest.hs b/src/Dyna/Analysis/Mode/InstSelftest.hs new file mode 100644 index 0000000..56304a3 --- /dev/null +++ b/src/Dyna/Analysis/Mode/InstSelftest.hs @@ -0,0 +1,82 @@ +--------------------------------------------------------------------------- +-- | Reimplementation of the Mercury mode system +-- +-- This module implements some basic self-test functionality for the insts +-- predicates in 'Dyna.Analysis.Mode.Insts'. + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE UndecidableInstances #-} + +module Dyna.Analysis.Mode.InstSelftest where + +import Control.Applicative +import Control.Monad +import Control.Monad.Trans.Maybe +import Data.Functor.Identity +import qualified Data.Map as M +import Dyna.Analysis.Mode.Inst +import Dyna.Analysis.Mode.Uniq +import qualified Test.Framework as TF +import Test.Framework.Providers.QuickCheck2 +import Test.Framework.TH +import Test.QuickCheck + +newtype Fix f = In { out :: f (Fix f) } +deriving instance (Eq (f (Fix f))) => Eq (Fix f) +deriving instance (Show (f (Fix f))) => Show (Fix f) +deriving instance (Ord f, Arbitrary f) => Arbitrary (Fix (InstF f)) + +instance Arbitrary Uniq where arbitrary = arbitraryBoundedEnum +instance (Ord f, Arbitrary f, Arbitrary i) => Arbitrary (InstF f i) where + arbitrary = frequency [ (1,pure IFree) + , (1,IAny <$> arbitrary) + , (1,IUniv <$> arbitrary) + , (3,IBound <$> arbitrary + <*> sized (\s -> resize (s`div`2) + (M.fromList <$> arbitrary)) + <*> arbitrary) + ] + + +q1 f = \x y -> f (\a ob -> q1 f a (In ob)) + (\a b -> q1 f a b) + (out x) (out y) + +qtb f = \x y -> In <$> f (\a b -> qtb f a b) (out x) (out y) + +qpb :: (Monad m, ff ~ Fix f, fff ~ f ff) + => ((ff -> ff -> MaybeT m ff) + -> fff -> fff -> MaybeT m (Maybe fff)) + -> ff -> ff -> m (Maybe ff) +qpb f x y = runMaybeT $ q x y + where q a b = maybe mzero (return . In) =<< f q (out a) (out b) + +qdLeq a b = runIdentity $ q1 iLeq_ a b +qdLeqGLB a b = runIdentity $ qtb (iLeqGLB_ return return) a b +qdSub a b = runIdentity $ q1 iSub_ a b +qdSubGLB a b = runIdentity $ qtb (iSubGLB_ return return) a b +qdSubLUB a b = runIdentity $ qpb (iSubLUB_ return return) a b + +prop_iLeq_GLB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property +prop_iLeq_GLB i1 i2 = i1 `qdLeq` i2 + ==> qdLeqGLB i1 i2 == i1 + +prop_iSub_GLB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property +prop_iSub_GLB i1 i2 = i1 `qdSub` i2 + ==> qdSubGLB i1 i2 == i1 + +prop_iSub_LUB :: Fix (InstF Bool) -> Fix (InstF Bool) -> Property +prop_iSub_LUB i1 i2 = i1 `qdSub` i2 + ==> qdSubLUB i1 i2 == (Just i2) + +selftest :: TF.Test +selftest = $(testGroupGenerator) + +main :: IO () +main = $(defaultMainGenerator) + diff --git a/src/Dyna/Main/TestsDriver.hs b/src/Dyna/Main/TestsDriver.hs index f3fbef3..98dcd5e 100644 --- a/src/Dyna/Main/TestsDriver.hs +++ b/src/Dyna/Main/TestsDriver.hs @@ -1,20 +1,28 @@ --- 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 + } diff --git a/src/Dyna/XXX/MonadContext.hs b/src/Dyna/XXX/MonadContext.hs new file mode 100644 index 0000000..96215e3 --- /dev/null +++ b/src/Dyna/XXX/MonadContext.hs @@ -0,0 +1,49 @@ +--------------------------------------------------------------------------- +-- | 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 diff --git a/src/Dyna/XXX/MonadUtils.hs b/src/Dyna/XXX/MonadUtils.hs index f6ab533..b0faf11 100644 --- a/src/Dyna/XXX/MonadUtils.hs +++ b/src/Dyna/XXX/MonadUtils.hs @@ -1,7 +1,3 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE MultiParamTypeClasses #-} - module Dyna.XXX.MonadUtils( -- * Data utilities generalizing 'Dyna.XXX.DataUtils' mapForallM, mapExistsM, setForallM, setExistsM, @@ -9,11 +5,10 @@ module Dyna.XXX.MonadUtils( 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 @@ -59,17 +54,4 @@ bracketState bs m = do 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) -- 2.50.1