From 8d2796e9401c0ba18852685f9810e8f3fe54c039 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Tue, 13 Nov 2012 23:23:29 -0500 Subject: [PATCH] Begin transcoding Overton's thesis --- dyna.cabal | 13 +-- src/Dyna/Analysis/Mode.hs | 174 ++++++++++++++++++++++++++++++++++++++ src/Dyna/Term/TTerm.hs | 2 +- src/Dyna/XXX/DataUtils.hs | 20 +++++ 4 files changed, 202 insertions(+), 7 deletions(-) create mode 100644 src/Dyna/Analysis/Mode.hs create mode 100644 src/Dyna/XXX/DataUtils.hs diff --git a/dyna.cabal b/dyna.cabal index 858f9e0..5bc6bb1 100644 --- a/dyna.cabal +++ b/dyna.cabal @@ -1,5 +1,3 @@ ----------------------------------------------------------------- - Name: dyna Version: 0.4 Cabal-Version: >=1.14 @@ -19,6 +17,10 @@ Description: A weighted logic programming language for dynamic include memoization, both forward- and backward-chaining, and namespace modularity. +source-repository head + type: git + location: git://github.com/nwf/dyna.git + Library Default-Language: Haskell2010 Hs-Source-Dirs: src @@ -27,6 +29,7 @@ Library Exposed-Modules: Dyna.Analysis.NormalizeParse, + Dyna.Analysis.Mode, Dyna.BackendK3.AST, Dyna.BackendK3.Automation, Dyna.BackendK3.Render, @@ -71,6 +74,7 @@ Executable drepl semigroups >=0.8, tagged >= 0.4.4, trifecta >=0.90, + unification-fd, unordered-containers>=0.2, utf8-string >=0.3, wl-pprint-extras >=3.0 @@ -101,6 +105,7 @@ Test-suite dyna-selftests test-framework-hunit >=0.2, test-framework-th >=0.2, trifecta >=0.90, + unification-fd, unordered-containers>=0.2, utf8-string >=0.3, wl-pprint-extras >=3.0 @@ -108,7 +113,3 @@ Test-suite dyna-selftests Other-Modules: Dyna.BackendK3.Examples Main-Is: Dyna/Test/Main.hs - - ----------------------------------------------------------------- ------------------------------------------------------------ fin. diff --git a/src/Dyna/Analysis/Mode.hs b/src/Dyna/Analysis/Mode.hs new file mode 100644 index 0000000..3c1a02c --- /dev/null +++ b/src/Dyna/Analysis/Mode.hs @@ -0,0 +1,174 @@ +--------------------------------------------------------------------------- +-- | 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. +-- + +-- 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 + + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/Term/TTerm.hs b/src/Dyna/Term/TTerm.hs index 9257f0e..ba73738 100644 --- a/src/Dyna/Term/TTerm.hs +++ b/src/Dyna/Term/TTerm.hs @@ -1,5 +1,5 @@ --------------------------------------------------------------------------- --- | Very, very basic representation of terms. +-- | Very, very basic (Trivial, even) representation of terms. -- -- XXX This isn't going to be sufficient when we start doing more -- complicated things, but it suffices for now? diff --git a/src/Dyna/XXX/DataUtils.hs b/src/Dyna/XXX/DataUtils.hs new file mode 100644 index 0000000..1c83689 --- /dev/null +++ b/src/Dyna/XXX/DataUtils.hs @@ -0,0 +1,20 @@ +module Dyna.XXX.DataUtils ( + -- * 'Data.Map' utilities + -- ** Quantification + mapExists, mapForall, + -- * 'Data.Set' utilities + -- ** Quantification + setExists, setForall + +) where + +import qualified Data.Map as M +import qualified Data.Set as S + +mapForall, mapExists :: (k -> v -> Bool) -> M.Map k v -> Bool +mapForall p m = M.foldrWithKey (\k v -> (&& p k v)) True m +mapExists p m = M.foldrWithKey (\k v -> (|| p k v)) False m + +setForall, setExists :: (a -> Bool) -> S.Set a -> Bool +setForall p s = S.fold (\e -> (&& p e)) True s +setExists p s = S.fold (\e -> (|| p e)) False s -- 2.50.1