datafix 0.0.0.1 → 0.0.0.2

raw patch · 17 files changed

+779/−513 lines, 17 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• datafix.cabal +19/−7
• examples/Analyses/AdHocStrAnal.hs +113/−113
• examples/Analyses/StrAnal/Analysis.hs +1/−1
• examples/Analyses/Templates/LetDn.hs +21/−10
• src/Datafix.hs +6/−2
• src/Datafix/Common.hs +183/−0
• src/Datafix/Denotational.hs +73/−0
• src/Datafix/Description.hs +0/−248
• src/Datafix/Entailments.hs +46/−0
• src/Datafix/Explicit.hs +126/−0
• src/Datafix/NodeAllocator.hs +1/−1
• src/Datafix/ProblemBuilder.hs +15/−8
• src/Datafix/Utils/Constraints.hs +62/−0
• src/Datafix/Worklist.hs +5/−3
• src/Datafix/Worklist/Denotational.hs +47/−0
• src/Datafix/Worklist/Internal.hs +54/−120

@@ -0,0 +1,7 @@+# Change log++`datafix` follows the [PVP][1].+The change log is available [on GitHub][2].++[1]: https://pvp.haskell.org/+[2]: https://github.com/sgraf812/datafix/releases

@@ -1,22 +1,29 @@ name:                datafix-version:             0.0.0.1+version:             0.0.0.2 synopsis:            Fixing data-flow problems-description:         Fixing data-flow problems in expression trees+description:         Fixing data-flow problems in expression trees.+                     This should be useful if you want to write optimizations+                     for your favorite programming language. +                     See the Tutorial module for an introduction. After that,+                     you might want to take a look at the `examples/` folder+                     in the [repository](https://github.com/sgraf812/datafix/tree/master/examples).+ license:             ISC license-file:        LICENSE author:              Sebastian Graf maintainer:          sgraf1337@gmail.com-copyright:           © 2017 Sebastian Graf+copyright:           © 2018 Sebastian Graf homepage:            https://github.com/sgraf812/datafix bug-reports:         https://github.com/sgraf812/datafix/issues  category:            Compiler build-type:          Custom stability:           alpha (experimental)-cabal-version:       >=1.24+cabal-version:       1.24  extra-source-files:+  CHANGELOG.md   README.md   stack.yaml   exprs/const.hs@@ -45,18 +52,23 @@   ghc-options:       -Wall   hs-source-dirs:    src   exposed-modules:   Datafix-                     Datafix.Tutorial-                     Datafix.Description+                     Datafix.Common+                     Datafix.Denotational+                     Datafix.Explicit                      Datafix.MonoMap                      Datafix.NodeAllocator                      Datafix.ProblemBuilder+                     Datafix.Tutorial+                     Datafix.Utils.Constraints                      Datafix.Utils.TypeLevel                      Datafix.Worklist+                     Datafix.Worklist.Denotational                      Datafix.Worklist.Graph                      Datafix.Worklist.Graph.Dense                      Datafix.Worklist.Graph.Sparse                      Datafix.Worklist.Internal   other-modules:+                     Datafix.Entailments                      Datafix.Utils.GrowableVector                      Datafix.IntArgsMonoMap                      Datafix.IntArgsMonoSet@@ -133,7 +145,7 @@ benchmark benchmarks   type:              exitcode-stdio-1.0   default-language:  Haskell2010-  ghc-options:       -Wall -O2 -threaded -rtsopts -with-rtsopts=-N+  ghc-options:       -Wall -threaded -rtsopts -with-rtsopts=-N   hs-source-dirs:    bench examples   main-is:           Main.hs   other-modules:     Sum

@@ -1,113 +1,113 @@-module Analyses.AdHocStrAnal (analyse) where
-
-import           Algebra.Lattice
-import           Analyses.StrAnal.Arity
-import           Analyses.StrAnal.Strictness
-
-import           CoreSyn
-import           Id
-import           Var
-import           VarEnv
-
-analyse :: CoreExpr -> StrLattice
-analyse e = analExpr emptyVarEnv e 0
-
-applyWhen :: Bool -> (a -> a) -> a -> a
-applyWhen True f  = f
-applyWhen False _ = id
-
-analExpr :: VarEnv StrType -> CoreExpr -> Arity -> StrLattice
-analExpr env expr arity =
-  case expr of
-    Lit _       -> emptyStrLattice
-    Type _      -> emptyStrLattice
-    -- Coercions are irrelevant to Strictness Analysis:
-    -- 'emptyStrLattice' is already the 'top' element,
-    -- so it's a safe approximation.
-    Coercion _ -> emptyStrLattice
-    Tick _ e    -> analExpr env e arity
-    Cast e _ -> analExpr env e arity
-    App f a ->
-      let
-        StrLattice (fTy, fAnns) = analExpr env f (arity + 1)
-        (argStr, fTy') = overArgs unconsArgStr fTy
-        argArity =
-          case argStr of
-            -- It's unfortunate that we don't have the type available to
-            -- trim this... But it doesn't hurt either.
-            HyperStrict -> Arity maxBound
-            Lazy        -> 0
-            Strict n    -> n
-        StrLattice (aTy, aAnns) = analExpr env a argArity
-      in mkStrLattice (aTy `bothStrType` fTy') (fAnns \/ aAnns)
-    Var id_
-      | isLocalId id_ ->
-          let
-            rhsType = case lookupVarEnv env id_ of
-              Just ty
-                -- 'ty' is a safe approximation for a call with 'idArity' at
-                -- minimum.
-                -- Note that 'Arity' is 'Op' ordered.
-                | arity <= Arity (idArity id_) -> ty
-              _ -> emptyStrType
-          in mkStrLattice (unitStrType id_ (Strict arity) `bothStrType` rhsType) emptyAnnotations
-      | otherwise -> emptyStrLattice
-    Lam id_ body
-      | isTyVar id_ -> analExpr env body arity
-      | otherwise ->
-          let
-            StrLattice (ty1, anns) = analExpr env body (0 /\ (arity-1))
-            (argStr, ty2) = peelFV id_ ty1
-            anns' = annotate id_ argStr anns
-            ty3 = modifyArgs (consArgStr argStr) ty2
-            ty4 = applyWhen (arity == 0) lazifyStrType ty3
-          in mkStrLattice ty4 anns'
-    Case scrut bndr _ alts ->
-      let
-        transferAlt (_, bndrs, alt) =
-          peelAndAnnotateFVs bndrs (analExpr env alt arity)
-        StrLattice (altTy, altAnns) =
-          peelAndAnnotateFV bndr . joins . map transferAlt $ alts
-        StrLattice (scrutTy, scrutAnns) = analExpr env scrut 0
-      in mkStrLattice (scrutTy `bothStrType` altTy) (scrutAnns \/ altAnns)
-    Let bind body ->
-      let
-        -- we assume a single call with `idArity` for our approximation
-        (rhsAnns, env') = case bind of
-          NonRec id_ rhs
-            | StrLattice (ty, anns) <- analExpr env rhs (Arity (idArity id_))
-            -> (anns, extendVarEnv env id_ ty)
-          Rec binds  -> fixBinds env binds
-        bodyLatt = analExpr env' body arity
-        StrLattice (bodyTy, bodyAnns) = peelAndAnnotateFVs (bindersOf bind) bodyLatt
-      in mkStrLattice bodyTy (bodyAnns \/ rhsAnns)
-
-fixBinds :: VarEnv StrType -> [(Id, CoreExpr)] -> (Annotations, VarEnv StrType)
-fixBinds env binds = mergeWithLatts stableLatts
-  where
-    mergeWithLatts :: [StrLattice] -> (Annotations, VarEnv StrType)
-    mergeWithLatts latts = foldr merger (emptyAnnotations, env) (zip binds latts)
-
-    merger :: ((Id, CoreExpr), StrLattice) -> (Annotations, VarEnv StrType) -> (Annotations, VarEnv StrType)
-    merger ((id_, _), StrLattice (ty, anns)) (restAnns, env') =
-      (restAnns \/ anns, extendVarEnv env' id_ ty)
-
-    latts0 :: [StrLattice]
-    latts0 = map (const bottom) binds
-
-    approximations :: [[StrLattice]]
-    approximations = iterate (iter . snd . mergeWithLatts) latts0
-
-    stable :: ([StrLattice], [StrLattice]) -> Bool
-    stable (old, new) = map strType old == map strType new
-
-    stableLatts :: [StrLattice]
-    stableLatts = snd . head . filter stable $ zip approximations (tail approximations)
-
-    iter env' = snd (foldr iterBind (env', []) binds)
-
-    iterBind (id_, rhs) (env', latts) =
-      let
-        latt = analExpr env' rhs (Arity (idArity id_))
-        env'' = extendVarEnv env' id_ (strType latt)
-      in (env'', latt:latts)
+module Analyses.AdHocStrAnal (analyse) where++import           Algebra.Lattice+import           Analyses.StrAnal.Arity+import           Analyses.StrAnal.Strictness++import           CoreSyn+import           Id+import           Var+import           VarEnv++analyse :: CoreExpr -> StrLattice+analyse e = analExpr emptyVarEnv e 0++applyWhen :: Bool -> (a -> a) -> a -> a+applyWhen True f  = f+applyWhen False _ = id++analExpr :: VarEnv StrType -> CoreExpr -> Arity -> StrLattice+analExpr env expr arity =+  case expr of+    Lit _       -> emptyStrLattice+    Type _      -> emptyStrLattice+    -- Coercions are irrelevant to Strictness Analysis:+    -- 'emptyStrLattice' is already the 'top' element,+    -- so it's a safe approximation.+    Coercion _ -> emptyStrLattice+    Tick _ e    -> analExpr env e arity+    Cast e _ -> analExpr env e arity+    App f a ->+      let+        StrLattice (fTy, fAnns) = analExpr env f (arity + 1)+        (argStr, fTy') = overArgs unconsArgStr fTy+        argArity =+          case argStr of+            -- It's unfortunate that we don't have the type available to+            -- trim this... But it doesn't hurt either.+            HyperStrict -> Arity maxBound+            Lazy        -> 0+            Strict n    -> n+        StrLattice (aTy, aAnns) = analExpr env a argArity+      in mkStrLattice (aTy `bothStrType` fTy') (fAnns \/ aAnns)+    Var id_+      | isLocalId id_ ->+          let+            rhsType = case lookupVarEnv env id_ of+              Just ty+                -- 'ty' is a safe approximation for a call with 'idArity' at+                -- minimum.+                -- Note that 'Arity' is 'Op' ordered.+                | arity <= Arity (idArity id_) -> ty+              _ -> emptyStrType+          in mkStrLattice (unitStrType id_ (Strict arity) `bothStrType` rhsType) emptyAnnotations+      | otherwise -> emptyStrLattice+    Lam id_ body+      | isTyVar id_ -> analExpr env body arity+      | otherwise ->+          let+            StrLattice (ty1, anns) = analExpr env body (0 /\ (arity-1))+            (argStr, ty2) = peelFV id_ ty1+            anns' = annotate id_ argStr anns+            ty3 = modifyArgs (consArgStr argStr) ty2+            ty4 = applyWhen (arity == 0) lazifyStrType ty3+          in mkStrLattice ty4 anns'+    Case scrut bndr _ alts ->+      let+        transferAlt (_, bndrs, alt) =+          peelAndAnnotateFVs bndrs (analExpr env alt arity)+        StrLattice (altTy, altAnns) =+          peelAndAnnotateFV bndr . joins . map transferAlt $ alts+        StrLattice (scrutTy, scrutAnns) = analExpr env scrut 0+      in mkStrLattice (scrutTy `bothStrType` altTy) (scrutAnns \/ altAnns)+    Let bind body ->+      let+        -- we assume a single call with `idArity` for our approximation+        (rhsAnns, env') = case bind of+          NonRec id_ rhs+            | StrLattice (ty, anns) <- analExpr env rhs (Arity (idArity id_))+            -> (anns, extendVarEnv env id_ ty)+          Rec binds  -> fixBinds env binds+        bodyLatt = analExpr env' body arity+        StrLattice (bodyTy, bodyAnns) = peelAndAnnotateFVs (bindersOf bind) bodyLatt+      in mkStrLattice bodyTy (bodyAnns \/ rhsAnns)++fixBinds :: VarEnv StrType -> [(Id, CoreExpr)] -> (Annotations, VarEnv StrType)+fixBinds env binds = mergeWithLatts stableLatts+  where+    mergeWithLatts :: [StrLattice] -> (Annotations, VarEnv StrType)+    mergeWithLatts latts = foldr merger (emptyAnnotations, env) (zip binds latts)++    merger :: ((Id, CoreExpr), StrLattice) -> (Annotations, VarEnv StrType) -> (Annotations, VarEnv StrType)+    merger ((id_, _), StrLattice (ty, anns)) (restAnns, env') =+      (restAnns \/ anns, extendVarEnv env' id_ ty)++    latts0 :: [StrLattice]+    latts0 = map (const bottom) binds++    approximations :: [[StrLattice]]+    approximations = iterate (iter . snd . mergeWithLatts) latts0++    stable :: ([StrLattice], [StrLattice]) -> Bool+    stable (old, new) = map strType old == map strType new++    stableLatts :: [StrLattice]+    stableLatts = snd . head . filter stable $ zip approximations (tail approximations)++    iter env' = snd (foldr iterBind (env', []) binds)++    iterBind (id_, rhs) (env', latts) =+      let+        latt = analExpr env' rhs (Arity (idArity id_))+        env'' = extendVarEnv env' id_ (strType latt)+      in (env'', latt:latts)

@@ -24,7 +24,7 @@ import           VarEnv  analyse :: CoreExpr -> StrLattice-analyse expr = evalDenotation (buildDenotation transferFunctionAlg expr) NeverAbort 0+analyse expr = evalDenotation (buildDenotation transferFunctionAlg expr) NeverAbort (0 :: Arity)  applyWhen :: Bool -> (a -> a) -> a -> a applyWhen True f  = f

@@ -76,20 +76,31 @@ -- lead to non-structural recursion, so termination isn't obvious and -- demands some confidence in domain theory by the programmer. buildDenotation-  :: forall m-   . MonadDependency m-  => Eq (ReturnType (Domain m))-  => Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool)-  => TransferAlgebra (Domain m)+  :: forall domain+   . Eq (ReturnType domain)+  => Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)+  => TransferAlgebra domain   -> CoreExpr-  -> ProblemBuilder m (TF m)-buildDenotation alg' = buildExpr emptyVarEnv+  -> Denotation domain+buildDenotation = buildDenotation'++-- This brings in the scope the existentially quantified 'MonadDatafix'. Too+-- bad that we have no big lambda so that this is necessary.+buildDenotation'+  :: forall m domain+   . MonadDatafix m+  => domain ~ Domain (DepM m)+  => Eq (ReturnType domain)+  => TransferAlgebra domain+  -> CoreExpr+  -> m (TF (DepM m))+buildDenotation' alg' = buildExpr emptyVarEnv   where-    alg = alg' (Proxy :: Proxy m) (Proxy :: Proxy (Domain m))+    alg = alg' (Proxy :: Proxy (DepM m)) (Proxy :: Proxy domain)     buildExpr-      :: VarEnv (TF m)+      :: VarEnv (TF (DepM m))       -> CoreExpr-      -> ProblemBuilder m (TF m)+      -> m (TF (DepM m))     buildExpr env expr =       case expr of         Lit lit -> pure (alg env (LitF lit))

@@ -15,7 +15,9 @@ -- Look at "Datafix.Tutorial" for a tour guided by use cases.  module Datafix-  ( module Datafix.Description+  ( module Datafix.Common+  , module Datafix.Denotational+  , module Datafix.Explicit   , module Datafix.NodeAllocator   , module Datafix.ProblemBuilder   , Datafix.MonoMap.MonoMap@@ -23,7 +25,9 @@   , module Datafix.Worklist   ) where -import           Datafix.Description+import           Datafix.Common+import           Datafix.Denotational+import           Datafix.Explicit import           Datafix.MonoMap import           Datafix.NodeAllocator import           Datafix.ProblemBuilder

@@ -0,0 +1,183 @@+{-# LANGUAGE AllowAmbiguousTypes     #-}+{-# LANGUAGE ConstraintKinds         #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE TypeFamilies            #-}+{-# LANGUAGE UndecidableInstances    #-}+{-# LANGUAGE UndecidableSuperClasses #-}++-- |+-- Module      :  Datafix.Common+-- Copyright   :  (c) Sebastian Graf 2018+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- Common definitions for defining data-flow problems, defining infrastructure+-- around the notion of 'Domain'.++module Datafix.Common+  ( LiftedFunc+  , ChangeDetector+  , eqChangeDetector+  , alwaysChangeDetector+  , MonadDomain (..)+  , Datafixable+  ) where++import           Algebra.Lattice+import           Datafix.MonoMap+import           Datafix.Utils.Constraints+import           Datafix.Utils.TypeLevel++-- $setup+-- >>> :set -XTypeFamilies+-- >>> :set -XScopedTypeVariables+--++-- | Data-flow problems denote 'Node's in the data-flow graph+-- by monotone transfer functions.+--+-- This type alias alone carries no semantic meaning.+-- However, it is instructive to see some examples of how+-- this alias reduces to a normal form:+--+-- @+--   LiftedFunc Int m ~ m Int+--   LiftedFunc (Bool -> Int) m ~ Bool -> m Int+--   LiftedFunc (a -> b -> Int) m ~ a -> b -> m Int+--   LiftedFunc (a -> b -> c -> Int) m ~ a -> b -> c -> m Int+-- @+--+-- @m@ will generally be an instance of 'MonadDependency' and the type alias+-- effectively wraps @m@ around @domain@'s return type.+-- The result is a function that produces its return value while+-- potentially triggering side-effects in @m@, which amounts to+-- depending on 'LiftedFunc's of other 'Node's for the+-- 'MonadDependency' case.+type LiftedFunc domain m+  = Arrows (ParamTypes domain) (m (ReturnType domain))++-- | A function that checks points of some function with type 'domain' for changes.+-- If this returns 'True', the point of the function is assumed to have changed.+--+-- An example is worth a thousand words, especially because of the type-level hackery:+--+-- >>> cd = (\a b -> even a /= even b) :: ChangeDetector Int+--+-- This checks the parity for changes in the abstract domain of integers.+-- Integers of the same parity are considered unchanged.+--+-- >>> cd 4 5+-- True+-- >>> cd 7 13+-- False+--+-- Now a (quite bogus) pointwise example:+--+-- >>> cd = (\x fx gx -> x + abs fx /= x + abs gx) :: ChangeDetector (Int -> Int)+-- >>> cd 1 (-1) 1+-- False+-- >>> cd 15 1 2+-- True+-- >>> cd 13 35 (-35)+-- False+--+-- This would consider functions @id@ and @negate@ unchanged, so the sequence+-- @iterate negate :: Int -> Int@ would be regarded immediately as convergent:+--+-- >>> f x = iterate negate x !! 0+-- >>> let g x = iterate negate x !! 1+-- >>> cd 123 (f 123) (g 123)+-- False+type ChangeDetector domain+  = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)++-- | A 'ChangeDetector' that delegates to the 'Eq' instance of the+-- node values.+eqChangeDetector+  :: forall domain+   . Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)+  => Eq (ReturnType domain)+  => ChangeDetector domain+eqChangeDetector =+  currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $+    const (/=)+{-# INLINE eqChangeDetector #-}++-- | A 'ChangeDetector' that always returns 'True'.+--+-- Use this when recomputing a node is cheaper than actually testing for the change.+-- Beware of cycles in the resulting dependency graph, though!+alwaysChangeDetector+  :: forall domain+   . Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)+  => ChangeDetector domain+alwaysChangeDetector =+  currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $+    \_ _ _ -> True+{-# INLINE alwaysChangeDetector #-}++-- | A monad with an associated 'Domain'. This class exists mostly to share the+-- associated type-class between 'MonadDependency' and 'MonadDatafix'.+--+-- Also it implies that @m@ satisfies 'Datafixable', which is common enough+class (Monad m, Datafixable (Domain m)) => MonadDomain m where+  -- | The abstract domain in which nodes of the data-flow graph are denoted.+  -- When this reduces to a function, then all functions of this domain+  -- are assumed to be monotone wrt. the (at least) partial order of all occuring+  -- types!+  --+  -- If you can't guarantee monotonicity, try to pull non-monotone arguments+  -- into 'Node's.+  type Domain m :: *++-- | A constraint synonym for constraints the 'domain' has to suffice.+--+-- This is actually a lot less scary than you might think.+-- Assuming we got [quantified class constraints](http://i.cs.hku.hk/~bruno/papers/hs2017.pdf)+-- instead of hackery from the [@constraints@ package](https://hackage.haskell.org/package/constraints-0.10/docs/Data-Constraint-Forall.html#t:ForallF),+-- @Datafixable@ is a specialized version of this:+--+-- @+-- type Datafixable domain =+--   ( forall r. Currying (ParamTypes domain) r+--   , MonoMapKey (Products (ParamTypes domain))+--   , BoundedJoinSemiLattice (ReturnType domain)+--   )+-- @+--+-- Now, let's assume a concrete @domain ~ String -> Bool -> Int@, so that+-- @'ParamTypes' (String -> Bool -> Int)@ expands to the type-level list @'[String, Bool]@+-- and @'Products' '[String, Bool]@ reduces to @(String, Bool)@.+--+-- Then this constraint makes sure we are able to+--+--  1.  Curry the domain of @String -> Bool -> r@ for all @r@ to e.g. @(String, Bool) -> r@.+--      See 'Currying'. This constraint should always be discharged automatically by the+--      type-checker as soon as 'ParamTypes' and 'ReturnTypes' reduce for the 'Domain' argument,+--      which happens when the concrete @'MonadDependency' m@ is known.+--+--  2.  We want to use a [monotone](https://en.wikipedia.org/wiki/Monotonic_function)+--      map of @(String, Bool)@ to @Int@ (the @ReturnType domain@). This is+--      ensured by the @'MonoMapKey' (String, Bool)@ constraint.+--+--      This constraint has to be discharged manually, but should amount to a+--      single line of boiler-plate in most cases, see 'MonoMapKey'.+--+--      Note that the monotonicity requirement means we have to pull non-monotone+--      arguments in @Domain m@ into the 'Node' portion of the 'DataFlowProblem'.+--+--  3.  For fixed-point iteration to work at all, the values which we iterate+--      naturally have to be instances of 'BoundedJoinSemiLattice'.+--      That type-class allows us to start iteration from a most-optimistic 'bottom'+--      value and successively iterate towards a conservative approximation using+--      the '(\/)' operator.+type Datafixable domain =+  ( Forall (Currying (ParamTypes domain))+  , MonoMapKey (Products (ParamTypes domain))+  , BoundedJoinSemiLattice (ReturnType domain)+  )

@@ -0,0 +1,73 @@+{-# LANGUAGE AllowAmbiguousTypes     #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE TypeFamilies            #-}+{-# LANGUAGE UndecidableInstances    #-}+{-# LANGUAGE UndecidableSuperClasses #-}++-- |+-- Module      :  Datafix.Denotational+-- Copyright   :  (c) Sebastian Graf 2018+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- Provides an alternative method (to 'MonadDependency'/"Datafix.Explicit")+-- of formulating data-flow problems as a 'Denotation' built in the context of+-- 'MonadDatafix'. This offers better usability for defining static analyses,+-- as the problem of allocating nodes in the data-flow graph is abstracted from+-- the user.++module Datafix.Denotational+  ( MonadDatafix (..)+  , datafixEq+  , Denotation+  ) where++import           Datafix.Common+import           Datafix.Entailments+import           Datafix.Utils.Constraints+import           Datafix.Utils.TypeLevel++-- | Builds on an associated 'DepM' that is a 'MonadDomain' (like any+-- 'MonadDependency') by providing a way to track dependencies without explicit+-- 'Node' management. Essentially, this allows to specify a build plan for a+-- 'DataFlowProblem' through calls to 'datafix' in analogy to 'fix' or 'mfix'.+class (Monad m, MonadDomain (DepM m)) => MonadDatafix m where+  -- | The monad in which data dependencies are expressed.+  -- Can and will be instantiated to some 'MonadDependency', if you choose+  -- to go through 'ProblemBuilder'.+  type DepM m :: * -> *+  -- | This is the closest we can get to an actual fixed-point combinator.+  --+  -- We need to provide a 'ChangeDetector' for detecting the fixed-point as+  -- well as a function to be iterated. In addition to returning a better+  -- approximation of itself in terms of itself, it can return an arbitrary+  -- value of type @a@. Because the iterated function might want to 'datafix'+  -- additional times (think of nested let bindings), the return values are+  -- wrapped in @m@.+  --+  -- Finally, the arbitrary @a@ value is returned, in analogy to @a@ in+  -- @'Control.Monad.Fix.mfix' :: MonadFix m => (a -> m a) -> m a@.+  datafix+    :: dom ~ Domain (DepM m)+    => ChangeDetector dom+    -> (LiftedFunc dom (DepM m) -> m (a, LiftedFunc dom (DepM m)))+    -> m a++-- | Shorthand that partially applies 'datafix' to an 'eqChangeDetector'.+datafixEq+  :: forall m dom a+   . MonadDatafix m+  => dom ~ Domain (DepM m)+  => Eq (ReturnType dom)+  => (LiftedFunc dom (DepM m) -> m (a, LiftedFunc dom (DepM m)))+  -> m a+datafixEq = datafix @m (eqChangeDetector @dom) \\ cdInst @dom++-- | A denotation of some syntactic entity in a semantic @domain@, built in a+-- some 'MonadDatafix' context.+type Denotation dom+  =  forall m. (MonadDatafix m, dom ~ Domain (DepM m)) => m (LiftedFunc dom (DepM m))

@@ -1,248 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes    #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE MultiParamTypeClasses  #-}-{-# LANGUAGE ScopedTypeVariables    #-}-{-# LANGUAGE TypeApplications       #-}-{-# LANGUAGE TypeFamilies           #-}---- |--- Module      :  Datafix.Description--- Copyright   :  (c) Sebastian Graf 2018--- License     :  ISC--- Maintainer  :  sgraf1337@gmail.com--- Portability :  portable------ Primitives for describing a [data-flow problem](https://en.wikipedia.org/wiki/Data-flow_analysis) in a declarative manner.------ Import this module transitively through "Datafix" and get access to "Datafix.Worklist" for functions that compute solutions to your 'DataFlowProblem's.--module Datafix.Description-  ( Node (..)-  , LiftedFunc-  , ChangeDetector-  , DataFlowProblem (..)-  , MonadDependency (..)-  , MonadDatafix (..)-  , datafixEq-  , eqChangeDetector-  , alwaysChangeDetector-  ) where--import           Datafix.Utils.TypeLevel---- $setup--- >>> :set -XTypeFamilies--- >>> :set -XScopedTypeVariables--- >>> import Data.Proxy------- | This is the type we use to index nodes in the data-flow graph.------ The connection between syntactic things (e.g. 'Id's) and 'Node's is--- made implicitly in code in analysis templates through an appropriate--- allocation mechanism as in 'NodeAllocator'.-newtype Node-  = Node { unwrapNode :: Int }-  deriving (Eq, Ord, Show)---- | A function that checks points of some function with type 'domain' for changes.--- If this returns 'True', the point of the function is assumed to have changed.------ An example is worth a thousand words, especially because of the type-level hackery:------ >>> cd = (\a b -> even a /= even b) :: ChangeDetector Int------ This checks the parity for changes in the abstract domain of integers.--- Integers of the same parity are considered unchanged.------ >>> cd 4 5--- True--- >>> cd 7 13--- False------ Now a (quite bogus) pointwise example:------ >>> cd = (\x fx gx -> x + abs fx /= x + abs gx) :: ChangeDetector (Int -> Int)--- >>> cd 1 (-1) 1--- False--- >>> cd 15 1 2--- True--- >>> cd 13 35 (-35)--- False------ This would consider functions @id@ and @negate@ unchanged, so the sequence--- @iterate negate :: Int -> Int@ would be regarded immediately as convergent:------ >>> f x = iterate negate x !! 0--- >>> let g x = iterate negate x !! 1--- >>> cd 123 (f 123) (g 123)--- False-type ChangeDetector domain-  = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)---- | Data-flow problems denote 'Node's in the data-flow graph--- by monotone transfer functions.------ This type alias alone carries no semantic meaning.--- However, it is instructive to see some examples of how--- this alias reduces to a normal form:------ @---   LiftedFunc Int m ~ m Int---   LiftedFunc (Bool -> Int) m ~ Bool -> m Int---   LiftedFunc (a -> b -> Int) m ~ a -> b -> m Int---   LiftedFunc (a -> b -> c -> Int) m ~ a -> b -> c -> m Int--- @------ @m@ will generally be an instance of 'MonadDependency' and the type alias--- effectively wraps @m@ around @domain@'s return type.--- The result is a function that produces its return value while--- potentially triggering side-effects in @m@, which amounts to--- depending on 'LiftedFunc's of other 'Node's for the--- 'MonadDependency' case.-type LiftedFunc domain m-  = Arrows (ParamTypes domain) (m (ReturnType domain))---- | Models a data-flow problem, where each 'Node' is mapped to--- its denoting 'LiftedFunc' and a means to detect when--- the iterated transfer function reached a fixed-point through--- a 'ChangeDetector'.-data DataFlowProblem m-  = DFP-  { dfpTransfer     :: !(Node -> LiftedFunc (Domain m) m)-  -- ^ A transfer function per each 'Node' of the modeled data-flow problem.-  , dfpDetectChange :: !(Node -> ChangeDetector (Domain m))-  -- ^ A 'ChangeDetector' for each 'Node' of the modeled data-flow problem.-  -- In the simplest case, this just delegates to an 'Eq' instance.-  }---- | A monad with a single impure primitive 'dependOn' that expresses--- a dependency on a 'Node' of a data-flow graph.------ The associated 'Domain' type is the abstract domain in which--- we denote 'Node's.------ Think of it like memoization on steroids.--- You can represent dynamic programs with this quite easily:------ >>> :{---   transferFib :: forall m . (MonadDependency m, Domain m ~ Int) => Node -> LiftedFunc Int m---   transferFib (Node 0) = return 0---   transferFib (Node 1) = return 1---   transferFib (Node n) = (+) <$> dependOn @m (Node (n-1)) <*> dependOn @m (Node (n-2))---   -- sparing the negative n error case--- :}------ We can construct a description of a 'DataFlowProblem' with this @transferFib@ function:------ >>> :{---   dataFlowProblem :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m---   dataFlowProblem = DFP transferFib (const (eqChangeDetector @(Domain m)))--- :}------ We regard the ordinary @fib@ function a solution to the recurrence modeled by @transferFib@:------ >>> :{---   fib :: Int -> Int---   fib 0 = 0---   fib 1 = 1---   fib n = fib (n-1) + fib (n - 2)--- :}------ E.g., under the assumption of @fib@ being total (which is true on the domain of natural numbers),--- it computes the same results as the least /fixed-point/ of the series of iterations--- of the transfer function @transferFib@.------ Ostensibly, the nth iteration of @transferFib@ substitutes each @dependOn@--- with @transferFib@ repeatedly for n times and finally substitutes all--- remaining @dependOn@s with a call to 'error'.------ Computing a solution by /fixed-point iteration/ in a declarative manner is the--- purpose of this library. There potentially are different approaches to--- computing a solution, but in "Datafix.Worklist" we offer an approach--- based on a worklist algorithm, trying to find a smart order in which--- nodes in the data-flow graph are reiterated.------ The concrete MonadDependency depends on the solution algorithm, which--- is in fact the reason why there is no satisfying data type in this module:--- We are only concerned with /declaring/ data-flow problems here.------ The distinguishing feature of data-flow graphs is that they are not--- necessarily acyclic (data-flow graphs of dynamic programs always are!),--- but [under certain conditions](https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem)--- even have solutions when there are cycles.------ Cycles occur commonly in data-flow problems of static analyses for--- programming languages, introduced through loops or recursive functions.--- Thus, this library mostly aims at making the life of compiler writers--- easier.-class Monad m => MonadDependency m where-  type Domain m :: *-  -- ^ The abstract domain in which 'Node's of the data-flow graph are denoted.-  -- When this is a synonym for a function, then all functions of this domain-  -- are assumed to be monotone wrt. the (at least) partial order of all occuring-  -- types!-  ---  -- If you can't guarantee monotonicity, try to pull non-monotone arguments-  -- into 'Node's.-  dependOn :: Node -> LiftedFunc (Domain m) m-  -- ^ Expresses a dependency on a node of the data-flow graph, thus-  -- introducing a way of trackable recursion. That's similar-  -- to how you would use 'Data.Function.fix' to abstract over recursion.---- | Builds on 'MonadDependency' by providing a way to track dependencies--- without explicit 'Node' management. Essentially, this allows to specify--- a build plan for a 'DataFlowProblem' through calls to 'datafix' in--- analogy to 'fix' or 'mfix'.-class (MonadDependency mdep, Monad mdat) => MonadDatafix mdep mdat | mdat -> mdep where-  -- | This is the closest we can get to an actual fixed-point combinator.-  ---  -- We need to provide a 'ChangeDetector' for detecting the fixed-point as-  -- well as a function to be iterated. In addition to returning a better-  -- approximation of itself in terms of itself, it can return an arbitrary-  -- value of type @a@. Because the iterated function might want to 'datafix'-  -- additional times (think of nested let bindings), the return values are-  -- wrapped in @mdat@.-  ---  -- Finally, the arbitrary @a@ value is returned, in analogy to @a@ in-  -- @mfix :: MonadFix m => (a -> m a) -> m a@.-  datafix-    :: ChangeDetector (Domain mdep)-    -> (LiftedFunc (Domain mdep) mdep -> mdat (a, LiftedFunc (Domain mdep) mdep))-    -> mdat a---- | Shorthand that partially applies 'datafix' to an 'eqChangeDetector'.-datafixEq-  :: forall mdep mdat a-   . MonadDatafix mdep mdat-  => Currying (ParamTypes (Domain mdep)) (ReturnType (Domain mdep) -> ReturnType (Domain mdep) -> Bool)-  => Eq (ReturnType (Domain mdep))-  => (LiftedFunc (Domain mdep) mdep -> mdat (a, LiftedFunc (Domain mdep) mdep))-  -> mdat a-datafixEq = datafix @mdep @mdat (eqChangeDetector @(Domain mdep))---- | A 'ChangeDetector' that delegates to the 'Eq' instance of the--- node values.-eqChangeDetector-  :: forall domain-   . Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)-  => Eq (ReturnType domain)-  => ChangeDetector domain-eqChangeDetector =-  currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $-    const (/=)-{-# INLINE eqChangeDetector #-}---- | A 'ChangeDetector' that always returns 'True'.------ Use this when recomputing a node is cheaper than actually testing for the change.--- Beware of cycles in the resulting dependency graph, though!-alwaysChangeDetector-  :: forall domain-   . Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)-  => ChangeDetector domain-alwaysChangeDetector =-  currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain -> Bool) $-    \_ _ _ -> True-{-# INLINE alwaysChangeDetector #-}

@@ -0,0 +1,46 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeOperators       #-}++-- |+-- Module      :  Datafix.Entailments+-- Copyright   :  (c) Sebastian Graf 2018+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- A bunch of helpful auxiliary entailments for 'Currying' that are recurring+-- throughout the code base.++module Datafix.Entailments+  ( cdInst+  , lfInst+  , afInst+  , idInst+  ) where++import           Datafix.Utils.Constraints+import           Datafix.Utils.TypeLevel++-- | 'Currying' entailment for 'ChangeDetector's.+cdInst+  :: Forall (Currying (ParamTypes domain))+  :- Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)+cdInst = inst++-- | 'Currying' entailment for 'LiftedFunc's.+lfInst+  :: Forall (Currying (ParamTypes domain))+  :- Currying (ParamTypes domain) (m (ReturnType domain))+lfInst = inst++-- | 'Currying' entailment for abortion functions.+afInst+  :: Forall (Currying (ParamTypes domain))+  :- Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain)+afInst = inst++-- | 'Currying' entailment for pure functions.+idInst+  :: Forall (Currying (ParamTypes domain))+  :- Currying (ParamTypes domain) (ReturnType domain)+idInst = inst

@@ -0,0 +1,126 @@+{-# LANGUAGE AllowAmbiguousTypes     #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeFamilies            #-}+{-# LANGUAGE UndecidableInstances    #-}+{-# LANGUAGE UndecidableSuperClasses #-}++-- |+-- Module      :  Datafix.Explicit+-- Copyright   :  (c) Sebastian Graf 2018+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- Primitives for describing a [data-flow problem](https://en.wikipedia.org/wiki/Data-flow_analysis) in a declarative manner.+-- This module requires you to manage assignment of 'Node's in the data-flow+-- graph to denotations by hand. If you're looking for a safer+-- approach suited for static analysis, have a look at "Datafix.Denotational".+--+-- Import this module transitively through "Datafix" and get access to+-- "Datafix.Worklist" for functions that compute solutions to your+-- 'DataFlowProblem's.++module Datafix.Explicit+  ( Node (..)+  , DataFlowProblem (..)+  , MonadDependency (..)+  ) where++import           Datafix.Common++-- $setup+-- >>> :set -XTypeFamilies+-- >>> :set -XScopedTypeVariables+-- >>> import Data.Proxy+--++-- | This is the type we use to index nodes in the data-flow graph.+--+-- The connection between syntactic things (e.g. 'Id's) and 'Node's is+-- made implicitly in code in analysis templates through an appropriate+-- allocation mechanism as in 'NodeAllocator'.+newtype Node+  = Node { unwrapNode :: Int }+  deriving (Eq, Ord, Show)++-- | Models a data-flow problem, where each 'Node' is mapped to+-- its denoting 'LiftedFunc' and a means to detect when+-- the iterated transfer function reached a fixed-point through+-- a 'ChangeDetector'.+data DataFlowProblem m+  = DFP+  { dfpTransfer     :: !(Node -> LiftedFunc (Domain m) m)+  -- ^ A transfer function per each 'Node' of the modeled data-flow problem.+  , dfpDetectChange :: !(Node -> ChangeDetector (Domain m))+  -- ^ A 'ChangeDetector' for each 'Node' of the modeled data-flow problem.+  -- In the simplest case, this just delegates to an 'Eq' instance.+  }++-- | A monad with a single impure primitive 'dependOn' that expresses+-- a dependency on a 'Node' of a data-flow graph.+--+-- The associated 'Domain' type is the abstract domain in which+-- we denote 'Node's.+--+-- Think of it like memoization on steroids.+-- You can represent dynamic programs with this quite easily:+--+-- >>> :{+--   transferFib :: forall m . (MonadDependency m, Domain m ~ Int) => Node -> LiftedFunc Int m+--   transferFib (Node 0) = return 0+--   transferFib (Node 1) = return 1+--   transferFib (Node n) = (+) <$> dependOn @m (Node (n-1)) <*> dependOn @m (Node (n-2))+--   -- sparing the negative n error case+-- :}+--+-- We can construct a description of a 'DataFlowProblem' with this @transferFib@ function:+--+-- >>> :{+--   dataFlowProblem :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m+--   dataFlowProblem = DFP transferFib (const (eqChangeDetector @(Domain m)))+-- :}+--+-- We regard the ordinary @fib@ function a solution to the recurrence modeled by @transferFib@:+--+-- >>> :{+--   fib :: Int -> Int+--   fib 0 = 0+--   fib 1 = 1+--   fib n = fib (n-1) + fib (n - 2)+-- :}+--+-- E.g., under the assumption of @fib@ being total (which is true on the domain of natural numbers),+-- it computes the same results as the least /fixed-point/ of the series of iterations+-- of the transfer function @transferFib@.+--+-- Ostensibly, the nth iteration of @transferFib@ substitutes each @dependOn@+-- with @transferFib@ repeatedly for n times and finally substitutes all+-- remaining @dependOn@s with a call to 'error'.+--+-- Computing a solution by /fixed-point iteration/ in a declarative manner is the+-- purpose of this library. There potentially are different approaches to+-- computing a solution, but in "Datafix.Worklist" we offer an approach+-- based on a worklist algorithm, trying to find a smart order in which+-- nodes in the data-flow graph are reiterated.+--+-- The concrete MonadDependency depends on the solution algorithm, which+-- is in fact the reason why there is no satisfying data type in this module:+-- We are only concerned with /declaring/ data-flow problems here.+--+-- The distinguishing feature of data-flow graphs is that they are not+-- necessarily acyclic (data-flow graphs of dynamic programs always are!),+-- but [under certain conditions](https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem)+-- even have solutions when there are cycles.+--+-- Cycles occur commonly in data-flow problems of static analyses for+-- programming languages, introduced through loops or recursive functions.+-- Thus, this library mostly aims at making the life of compiler writers+-- easier.+class MonadDomain m => MonadDependency m where+  dependOn :: Node -> LiftedFunc (Domain m) m+  -- ^ Expresses a dependency on a node of the data-flow graph, thus+  -- introducing a way of trackable recursion. That's similar+  -- to how you would use 'Data.Function.fix' to abstract over recursion.

@@ -22,7 +22,7 @@ import           Control.Monad.Trans.Class import           Control.Monad.Trans.State.Strict import           Data.Primitive.Array-import           Datafix.Description+import           Datafix.Explicit import           Datafix.Utils.GrowableVector     (GrowableVector) import qualified Datafix.Utils.GrowableVector     as GV import           System.IO.Unsafe                 (unsafePerformIO)

@@ -2,6 +2,7 @@ {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE RankNTypes                 #-} {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE TypeApplications           #-} {-# LANGUAGE TypeFamilies               #-}@@ -13,7 +14,10 @@ -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable ----- Offers an instance for 'MonadDatafix' based on 'NodeAllocator'.+-- Builds a 'DataFlowProblem' for a 'Denotation'al formulation in terms of+-- 'MonadDatafix'. Effectively reduces descriptions from "Datafix.Denotational"+-- to ones from "Datafix.Explicit", so that solvers such as "Datafix.Worklist"+-- only have to provide an interpreter for 'MonadDependency'.  module Datafix.ProblemBuilder   ( ProblemBuilder@@ -21,9 +25,12 @@   ) where  import           Data.Primitive.Array-import           Datafix.Description+import           Datafix.Common+import           Datafix.Denotational+import           Datafix.Entailments+import           Datafix.Explicit import           Datafix.NodeAllocator-import           Datafix.Utils.TypeLevel+import           Datafix.Utils.Constraints  -- | Constructs a build plan for a 'DataFlowProblem' by tracking allocation of -- 'Node's mapping to 'ChangeDetector's and transfer functions.@@ -31,7 +38,8 @@   = ProblemBuilder { unwrapProblemBuilder :: NodeAllocator (ChangeDetector (Domain m), LiftedFunc (Domain m) m) a }   deriving (Functor, Applicative, Monad) -instance MonadDependency m => MonadDatafix m (ProblemBuilder m) where+instance MonadDependency m => MonadDatafix (ProblemBuilder m) where+  type DepM (ProblemBuilder m) = m   datafix cd func = ProblemBuilder $ allocateNode $ \node -> do     let deref = dependOn @m node     (ret, transfer) <- unwrapProblemBuilder (func deref)@@ -45,12 +53,11 @@ buildProblem   :: forall m    . MonadDependency m-  => Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool)-  => ProblemBuilder m (LiftedFunc (Domain m) m)+  => Denotation (Domain m)   -> (Node, Node, DataFlowProblem m) buildProblem buildDenotation = (root, Node (sizeofArray arr - 1), prob)   where     prob = DFP (snd . indexArray arr . unwrapNode) (fst . indexArray arr . unwrapNode)     (root, arr) = runAllocator $ allocateNode $ \root_ -> do-      denotation <- unwrapProblemBuilder buildDenotation-      return (root_, (alwaysChangeDetector @(Domain m), denotation))+      denotation <- unwrapProblemBuilder (buildDenotation @(ProblemBuilder m))+      return (root_, (alwaysChangeDetector @(Domain m) \\ cdInst @(Domain m), denotation))

@@ -0,0 +1,62 @@+{-# LANGUAGE ConstraintKinds         #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeFamilies            #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE UndecidableInstances    #-}+{-# LANGUAGE UndecidableSuperClasses #-}++-- |+-- Module      :  Datafix.Utils.Constraints+-- Copyright   :  (c) Sebastian Graf 2018+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- Universally quantified constraints, until we have -XQuantifiedConstraints.++module Datafix.Utils.Constraints+  ( Dict (..)+  , (:-) (..)+  , (\\)+  , Forall+  , inst+  ) where++import           Data.Kind+import           Unsafe.Coerce (unsafeCoerce)++data Dict :: Constraint -> Type where+  Dict :: c => Dict c++newtype a :- b = Sub (a => Dict b)++infixl 1 \\ -- required comment++-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@+(\\) :: a => (b => r) -> (a :- b) -> r+r \\ Sub Dict = r++-- The `Skolem` type family represents skolem variables; do not export!+-- If GHC supports it, these might be made closed with no instances.++type family Skolem (p :: k -> Constraint) :: k++-- The outer `Forall` type family prevents GHC from giving a spurious+-- superclass cycle error.+-- The inner `Forall_` class prevents the skolem from leaking to the user,+-- which would be disastrous.++-- | A representation of the quantified constraint @forall a. p a@.+type family Forall (p :: k -> Constraint) :: Constraint+type instance Forall p = Forall_ p+class p (Skolem p) => Forall_ (p :: k -> Constraint)+instance p (Skolem p) => Forall_ (p :: k -> Constraint)++inst :: forall p a . Forall p :- p a+inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p))

@@ -7,14 +7,16 @@ -- -- This module provides the 'Impl.solveProblem' function, which solves the description of a -- 'Datafix.Description.DataFlowProblem' by employing a worklist algorithm.+-- There's also an interpreter for 'Denotation'al problems in the form of+-- 'Denotational.evalDenotation'.  module Datafix.Worklist   ( Impl.DependencyM-  , Impl.Datafixable   , Impl.Density (..)   , Impl.IterationBound (..)   , Impl.solveProblem-  , Impl.evalDenotation+  , Denotational.evalDenotation   ) where -import qualified Datafix.Worklist.Internal as Impl+import qualified Datafix.Worklist.Denotational as Denotational+import qualified Datafix.Worklist.Internal     as Impl

@@ -0,0 +1,47 @@+{-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}++-- |+-- Module      :  Datafix.Worklist.Denotational+-- Copyright   :  (c) Sebastian Graf 2018+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- Bridges the "Datafix.Worklist" solver for 'DataFlowProblem's ('solveProblem')+-- with the "Datafix.Denotational" approach, using 'MonadDatafix' to describe+-- a 'Denotation'.++module Datafix.Worklist.Denotational+  ( evalDenotation+  ) where++import           Datafix.Common+import           Datafix.Denotational+import           Datafix.ProblemBuilder+import           Datafix.Worklist.Internal++-- | @evalDenotation denot ib@ returns a value in @domain@ that is described by+-- the denotation @denot@.+--+-- It does so by building up the 'DataFlowProblem' corresponding to @denot@+-- and solving the resulting problem with 'solveProblem', the documentation of+-- which describes in detail how to arrive at a stable denotation and what+-- the 'IterationBound' @ib@ is for.+evalDenotation+  :: Datafixable domain+  => Denotation domain+  -- ^ A build plan for computing the denotation, possibly involving+  -- fixed-point iteration factored through calls to 'datafix'.+  -> IterationBound domain+  -- ^ Whether the solution algorithm should respect a maximum bound on the+  -- number of iterations per point. Pass 'NeverAbort' if you don't care.+  -> domain+evalDenotation denot ib = solveProblem prob (Dense max_) ib root+  where+    (root, max_, prob) = buildProblem denot+{-# INLINE evalDenotation #-}

@@ -33,12 +33,14 @@ import           Data.Maybe                       (fromMaybe, listToMaybe,                                                    mapMaybe) import           Data.Type.Equality-import           Datafix.Description              hiding (dependOn)-import qualified Datafix.Description+import           Datafix.Common+import           Datafix.Entailments+import           Datafix.Explicit                 hiding (dependOn)+import qualified Datafix.Explicit import           Datafix.IntArgsMonoSet           (IntArgsMonoSet) import qualified Datafix.IntArgsMonoSet           as IntArgsMonoSet import           Datafix.MonoMap                  (MonoMapKey)-import           Datafix.ProblemBuilder+import           Datafix.Utils.Constraints import           Datafix.Utils.TypeLevel import           Datafix.Worklist.Graph           (GraphRef, PointInfo (..)) import qualified Datafix.Worklist.Graph           as Graph@@ -58,9 +60,9 @@   --   -- This ultimately leaks badly into the exported interface in 'solveProblem':   -- Since we can't have universally quantified instance contexts (yet!), we can' write-  -- @(forall s. Datafixable (DependencyM s graph domain)) => (forall s. DataFlowProblem (DependencyM s graph domain)) -> ...@+  -- @(forall s. Datafixable domain => (forall s. DataFlowProblem (DependencyM s graph domain)) -> ...@   -- and have to instead have the isomorphic-  -- @(forall s r. (Datafixable (DependencyM s graph domain) => r) -> r) -> (forall s. DataFlowProblem (DependencyM s graph domain)) -> ...@+  -- @(forall s r. (Datafixable domain => r) -> r) -> (forall s. DataFlowProblem (DependencyM s graph domain)) -> ...@   -- and urge all call sites to pass a meaningless 'id' parameter.   --   -- Also, this means more explicit type signatures as we have to make clear to@@ -109,64 +111,13 @@     <*> newIORef unstable_ {-# INLINE initialEnv #-} --- | A constraint synonym for the constraints 'm' and its associated--- 'Domain' have to suffice.------ This is actually a lot less scary than you might think.--- Assuming we got [quantified class constraints](http://i.cs.hku.hk/~bruno/papers/hs2017.pdf),--- @Datafixable@ is a specialized version of this:------ @--- type Datafixable m =---   ( forall r. Currying (ParamTypes (Domain m)) r---   , MonoMapKey (Products (ParamTypes (Domain m)))---   , BoundedJoinSemiLattice (ReturnType (Domain m))---   )--- @------ Now, let's assume a concrete @Domain m ~ String -> Bool -> Int@, so that--- @'ParamTypes' (String -> Bool -> Int)@ expands to the type-level list @'[String, Bool]@--- and @'Products' '[String, Bool]@ reduces to @(String, Bool)@.------ Then this constraint makes sure we are able to------  1.  Curry the domain of @String -> Bool -> r@ for all @r@ to e.g. @(String, Bool) -> r@.---      See 'Currying'. This constraint should always be discharged automatically by the---      type-checker as soon as 'ParamTypes' and 'ReturnTypes' reduce for the 'Domain' argument,---      which happens when the concrete @'MonadDependency' m@ is known.------      (Actually, we do this for multiple concrete @r@ because of the missing---      support for quantified class constraints)------  2.  We want to use a [monotone](https://en.wikipedia.org/wiki/Monotonic_function)---      map of @(String, Bool)@ to @Int@ (the @ReturnType (Domain m)@). This is---      ensured by the @'MonoMapKey' (String, Bool)@ constraint.------      This constraint has to be discharged manually, but should amount to a---      single line of boiler-plate in most cases, see 'MonoMapKey'.------      Note that the monotonicity requirement means we have to pull non-monotone---      arguments in @Domain m@ into the 'Node' portion of the 'DataFlowProblem'.------  3.  For fixed-point iteration to work at all, the values which we iterate---      naturally have to be instances of 'BoundedJoinSemiLattice'.---      That type-class allows us to start iteration from a most-optimistic 'bottom'---      value and successively iterate towards a conservative approximation using---      the '(\/)' operator.-type Datafixable m =-  ( Currying (ParamTypes (Domain m)) (ReturnType (Domain m))-  , Currying (ParamTypes (Domain m)) (m (ReturnType (Domain m)))-  , Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool)-  , Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m))-  , MonoMapKey (Products (ParamTypes (Domain m)))-  , BoundedJoinSemiLattice (ReturnType (Domain m))-  )+-- | The 'Domain' is extracted from a type parameter.+instance Datafixable domain => MonadDomain (DependencyM graph domain) where+  type Domain (DependencyM graph domain) = domain  -- | This allows us to solve @MonadDependency m => DataFlowProblem m@ descriptions -- with 'solveProblem'.--- The 'Domain' is extracted from a type parameter.-instance (Datafixable (DependencyM graph domain), GraphRef graph) => MonadDependency (DependencyM graph domain) where-  type Domain (DependencyM graph domain) = domain+instance (Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) where   dependOn = dependOn @domain @graph   {-# INLINE dependOn #-} @@ -282,7 +233,7 @@ {-# INLINE highestPriorityUnstableNode #-}  withCall-  :: Datafixable (DependencyM graph domain)+  :: Datafixable domain   => Int   -> Products (ParamTypes domain)   -> ReaderT (Env graph domain) IO a@@ -314,13 +265,15 @@   => cod ~ ReturnType domain   => depm ~ DependencyM graph domain   => GraphRef graph-  => Datafixable depm+  => Datafixable domain   => Int -> Products dom -> ReaderT (Env graph domain) IO cod recompute node args = withCall node args $ do   prob <- asks problem   let node' = Node node   let DM iterate' = uncurrys @dom @(depm cod) (dfpTransfer prob node') args+                  \\ lfInst @domain @depm   let detectChange' = uncurrys @dom @(cod -> cod -> Bool) (dfpDetectChange prob node') args+                    \\ cdInst @domain   -- We need to access the graph at three different points in time:   --   --    1. before the call to 'iterate', to access 'iterations', but only if abortion is required@@ -336,7 +289,7 @@     Just preInfo <- lift (withReaderT graph (Graph.lookup node args))     guard (iterations preInfo >= n)     Just oldVal <- return (value preInfo)-    return (uncurrys @dom @(cod -> cod) abort args oldVal)+    return (uncurrys @dom @(cod -> cod) abort args oldVal \\ afInst @domain)   -- For the 'Nothing' case, we proceed by iterating the transfer function.   newVal <- maybe iterate' return maybeAbortedVal   -- When abortion is required, 'iterate'' is not called and@@ -362,37 +315,40 @@ {-# INLINE recompute #-}  dependOn-  :: forall domain graph-   . Datafixable (DependencyM graph domain)+  :: forall domain graph depm+   . depm ~ DependencyM graph domain+  => Datafixable domain   => GraphRef graph-  => Node -> LiftedFunc domain (DependencyM graph domain)-dependOn (Node node) = currys @(ParamTypes domain) @(DependencyM graph domain (ReturnType domain)) impl-  where-    impl args = DM $ do-      cycleDetected <- IntArgsMonoSet.member node args <$> asks callStack-      isStable <- zoomUnstable $-        not . IntArgsMonoSet.member node args <$> get-      maybePointInfo <- withReaderT graph (Graph.lookup node args)-      zoomReferencedPoints (modify' (IntArgsMonoSet.insert node args))-      case maybePointInfo >>= value of-        -- 'value' can only be 'Nothing' if there was a 'cycleDetected':-        -- Otherwise, the node wasn't part of the call stack and thus will either-        -- have a 'value' assigned or will not have been discovered at all.-        Nothing | cycleDetected ->-          -- Somewhere in an outer activation record we already compute this one.-          -- We don't recurse again and just return an optimistic approximation,-          -- such as 'bottom'.-          -- Otherwise, 'recompute' will immediately add a 'PointInfo' before-          -- any calls to 'dependOn' for a cycle to even be possible.-          optimisticApproximation node args-        Just val | isStable || cycleDetected ->-          -- No brainer-          return val-        maybeVal ->-          -- No cycle && (unstable || undiscovered). Apply one of the schemes-          -- outlined in-          -- https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like-          scheme2 maybeVal node args+  => Node -> LiftedFunc domain depm+dependOn (Node node) =+  currys @(ParamTypes domain) @(depm (ReturnType domain)) impl+    \\ lfInst @domain @(DependencyM graph domain)+    where+      impl args = DM $ do+        cycleDetected <- IntArgsMonoSet.member node args <$> asks callStack+        isStable <- zoomUnstable $+          not . IntArgsMonoSet.member node args <$> get+        maybePointInfo <- withReaderT graph (Graph.lookup node args)+        zoomReferencedPoints (modify' (IntArgsMonoSet.insert node args))+        case maybePointInfo >>= value of+          -- 'value' can only be 'Nothing' if there was a 'cycleDetected':+          -- Otherwise, the node wasn't part of the call stack and thus will either+          -- have a 'value' assigned or will not have been discovered at all.+          Nothing | cycleDetected ->+            -- Somewhere in an outer activation record we already compute this one.+            -- We don't recurse again and just return an optimistic approximation,+            -- such as 'bottom'.+            -- Otherwise, 'recompute' will immediately add a 'PointInfo' before+            -- any calls to 'dependOn' for a cycle to even be possible.+            optimisticApproximation node args+          Just val | isStable || cycleDetected ->+            -- No brainer+            return val+          maybeVal ->+            -- No cycle && (unstable || undiscovered). Apply one of the schemes+            -- outlined in+            -- https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like+            scheme2 maybeVal node args {-# INLINE dependOn #-}  -- | Compute an optimistic approximation for a point of a given node that is@@ -404,7 +360,7 @@ -- that are lower bounds to the current point. optimisticApproximation   :: GraphRef graph-  => Datafixable (DependencyM graph domain)+  => Datafixable domain   => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain) optimisticApproximation node args = do   points <- withReaderT graph (Graph.lookupLT node args)@@ -415,7 +371,7 @@  scheme1, scheme2   :: GraphRef graph-  => Datafixable (DependencyM graph domain)+  => Datafixable domain   => Maybe (ReturnType domain)   -> Int   -> Products (ParamTypes domain)@@ -474,7 +430,7 @@ -- fixed-point has been reached. work   :: GraphRef graph-  => Datafixable (DependencyM graph domain)+  => Datafixable domain   => ReaderT (Env graph domain) IO () work = whileJust_ highestPriorityUnstableNode (uncurry recompute) {-# INLINE work #-}@@ -499,7 +455,7 @@ solveProblem   :: forall domain graph    . GraphRef graph-  => Datafixable (DependencyM graph domain)+  => Datafixable domain   => DataFlowProblem (DependencyM graph domain)   -- ^ The description of the @DataFlowProblem@ to solve.   -> Density graph@@ -516,7 +472,7 @@   -- you specified via the @DataFlowProblem@.   -> domain solveProblem prob density ib (Node node) =-  castWith arrowsAxiom (currys @(ParamTypes domain) @(ReturnType domain) impl)+  castWith arrowsAxiom (currys @(ParamTypes domain) @(ReturnType domain) impl \\ idInst @domain)     where       impl         = fromMaybe (error "Broken invariant: The root node has no value")@@ -531,25 +487,3 @@         env <- initialEnv (IntArgsMonoSet.singleton node args) prob ib newGraphRef         runReaderT (work >> withReaderT graph (Graph.lookup node args)) env {-# INLINE solveProblem #-}---- | @evalDenotation denot ib@ returns a value in @domain@ that is described by--- the denotation @denot@.------ It does so by building up the 'DataFlowProblem' corresponding to @denot@--- and solving the resulting problem with 'solveProblem', the documentation of--- which describes in detail how to arrive at a stable denotation and what--- the 'IterationBound' @ib@ is for.-evalDenotation-  :: forall domain-   . Datafixable (DependencyM DenseGraph.Ref domain)-  => ProblemBuilder (DependencyM DenseGraph.Ref domain) (LiftedFunc domain (DependencyM DenseGraph.Ref domain))-  -- ^ A build plan for computing the denotation, possibly involving-  -- fixed-point iteration factored through calls to 'datafix'.-  -> IterationBound domain-  -- ^ Whether the solution algorithm should respect a maximum bound on the-  -- number of iterations per point. Pass 'NeverAbort' if you don't care.-  -> domain-evalDenotation denot ib = solveProblem prob (Dense max_) ib root-  where-    (root, max_, prob) = buildProblem denot-{-# INLINE evalDenotation #-}