--- /dev/null
+---------------------------------------------------------------------------
+-- | Reimplementation of the Mercury mode system, following David Overton's
+-- 2003 Ph.D. thesis.
+--
+-- David Overton. Precise and expressive mode systems for typed logic
+-- programming languages.
+-- <http://www.mercury.csse.unimelb.edu.au/information/papers.html#dmo-thesis>
+
+-- Header material {{{
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TypeFamilies #-}
+module Dyna.Analysis.Mode(
+ -- * Uniqueness annotations
+ Uniq(..),
+ -- ** Reference counts
+ URCL(..), URCH(..), URC(..), uniqGamma, uniqAlpha, uniqLeq,
+ -- * Instantiation States
+ Inst(..), iUniq, iWellFormed, iLeq, iSub, iGround
+) 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 Dyna.XXX.DataUtils
+
+------------------------------------------------------------------------}}}
+-- Uniqueness Modes {{{
+
+-- | Mercury uniqueness annotations (figure 3.15, page 48)
+data Uniq = UUnique
+ | UMostlyUnique
+ | UShared
+ | UMostlyClobbered
+ | UClobbered
+ deriving (Eq, Ord, Show)
+
+-- | Reference counts are bounded below by 0 or 1.
+--
+-- Figure 3.16, page 49
+data URCL = Urcl0 | Urcl1 deriving (Eq,Ord,Show)
+
+-- | Reference counts are bounded above by 1 or infinity.
+--
+-- 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)
+
+-- | 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
+
+------------------------------------------------------------------------}}}
+-- 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) }
+
+------------------------------------------------------------------------}}}
+-- Instantiation States {{{
+
+-- | 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)
+
+{-
+-- | 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
+-}
+
+-- | 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?
+--
+-- Surrogate for definition 3.2.17, page 52
+iGround :: Inst f -> Bool
+iGround (IBound UUnique b) = mapForall (\_ -> all iGround) b
+iGround _ = False
+
+
+------------------------------------------------------------------------}}}
projects / dyna2 / commitdiff