datafix (empty) → 0.0.0.1
raw patch · 45 files changed
+4675/−0 lines, 45 filesdep +Cabaldep +Globdep +QuickCheckbuild-type:Customsetup-changed
Dependencies added: Cabal, Glob, QuickCheck, base, cabal-toolkit, containers, criterion, datafix, deepseq, directory, doctest, filepath, ghc, ghc-paths, lattices, pomaps, primitive, tasty, tasty-hunit, tasty-smallcheck, text, transformers, turtle, vector
Files
- LICENSE +13/−0
- README.md +6/−0
- Setup.hs +2/−0
- bench/Main.hs +130/−0
- datafix.cabal +168/−0
- examples/Analyses/AdHocStrAnal.hs +113/−0
- examples/Analyses/StrAnal.hs +5/−0
- examples/Analyses/StrAnal/Analysis.hs +115/−0
- examples/Analyses/StrAnal/Arity.hs +69/−0
- examples/Analyses/StrAnal/Strictness.hs +284/−0
- examples/Analyses/Syntax/CoreSynF.hs +45/−0
- examples/Analyses/Syntax/MkCoreFromFile.hs +79/−0
- examples/Analyses/Syntax/MkCoreHelpers.hs +53/−0
- examples/Analyses/Templates/LetDn.hs +154/−0
- examples/Fac.hs +21/−0
- examples/Fib.hs +24/−0
- examples/Mutual.hs +29/−0
- examples/Sum.hs +17/−0
- exprs/const.hs +5/−0
- exprs/findLT.hs +13/−0
- exprs/kahan.hs +56/−0
- exprs/lambda.hs +261/−0
- exprs/sieve.hs +44/−0
- lattices/Algebra/Lattice.hs +477/−0
- src/Datafix.hs +31/−0
- src/Datafix/Description.hs +248/−0
- src/Datafix/IntArgsMonoMap.hs +109/−0
- src/Datafix/IntArgsMonoSet.hs +50/−0
- src/Datafix/MonoMap.hs +132/−0
- src/Datafix/NodeAllocator.hs +60/−0
- src/Datafix/ProblemBuilder.hs +56/−0
- src/Datafix/Tutorial.hs +270/−0
- src/Datafix/Utils/GrowableVector.hs +68/−0
- src/Datafix/Utils/TypeLevel.hs +164/−0
- src/Datafix/Worklist.hs +20/−0
- src/Datafix/Worklist/Graph.hs +69/−0
- src/Datafix/Worklist/Graph/Dense.hs +90/−0
- src/Datafix/Worklist/Graph/Sparse.hs +90/−0
- src/Datafix/Worklist/Internal.hs +555/−0
- stack.yaml +64/−0
- tests/Critical.hs +81/−0
- tests/Main.hs +20/−0
- tests/StrAnal.hs +253/−0
- tests/Trivial.hs +57/−0
- tests/doctest.hs +5/−0
+ LICENSE view
@@ -0,0 +1,13 @@+Copyright (c) 2017, Sebastian Graf++Permission to use, copy, modify, and/or distribute this software for any+purpose with or without fee is hereby granted, provided that the above+copyright notice and this permission notice appear in all copies.++THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ README.md view
@@ -0,0 +1,6 @@+`datafix` [](https://travis-ci.org/sgraf812/datafix) [](https://hackage.haskell.org/package/datafix)+==========++Library for separating specification of a data-flow problem from computing its solution.++See the haddocks in `Datafix.Tutorial` for an introduction and the `examples/` folder for more advanced material.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple.Toolkit+main = defaultMainWithBuildInfo
+ bench/Main.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE FlexibleInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++import Algebra.Lattice+import Control.DeepSeq+import Criterion+import Criterion.Main+import Datafix+import Datafix.Worklist (Density (..),+ IterationBound (..),+ solveProblem)+import Datafix.Worklist.Graph (GraphRef)+import Numeric.Natural++import qualified Analyses.AdHocStrAnal as AdHocStrAnal+import qualified Analyses.StrAnal as StrAnal+import Analyses.StrAnal.Strictness+import Analyses.Syntax.MkCoreFromFile (compileCoreExpr)+import Analyses.Syntax.MkCoreHelpers+import Sum++import CoreSeq (seqExpr)+import CoreSyn+import CoreTidy (tidyExpr)+import Id+import VarEnv (emptyTidyEnv)++instance JoinSemiLattice Natural where+ (\/) = max++instance BoundedJoinSemiLattice Natural where+ bottom = 0++-- | For 'Criterion.env'.+instance NFData CoreExpr where+ rnf = seqExpr++fixSum :: GraphRef graph => (Node -> Density graph) -> Int -> Natural+fixSum density n = solveProblem sumProblem (density (Node n)) NeverAbort (Node n)++main :: IO ()+main = defaultMain+ [ bgroup "sum" $ map sumGroup [100, 1000, 10000]+ , bgroup "stranal"+ [ strAnalGroup "simpleRecursive1" simpleRecursive1+ , strAnalGroup "nestedRecursive1" nestedRecursive1+ , strAnalFileGroup "exprs/const.hs"+ , strAnalFileGroup "exprs/findLT.hs"+ , strAnalFileGroup "exprs/kahan.hs"+ , strAnalFileGroup "exprs/sieve.hs"+ , strAnalFileGroup "exprs/lambda.hs"+ ]+ ] where+ sumGroup n =+ bgroup (show n)+ [ bench "baseline" (whnf (\n' -> sum [1..n']) n)+ , bench "sparse" (whnf (fixSum (const Sparse)) n)+ , bench "dense" (whnf (fixSum Dense) n)+ ]+ strAnalGroup descr e =+ bgroup descr+ [ bench "baseline" (whnf (seqStrLattice . AdHocStrAnal.analyse) e)+ , bench "datafix" (whnf (seqStrLattice . StrAnal.analyse) e)+ ]+ strAnalFileGroup file =+ env (compileCoreExpr file) $ \e ->+ bgroup file+ [ bench "baseline" (whnf (seqStrLattice . AdHocStrAnal.analyse) e)+ , bench "datafix" (whnf (seqStrLattice . StrAnal.analyse) e)+ ]+++seqStrLattice :: StrLattice -> ()+seqStrLattice l = strType l `seq` annotations l `seq` ()++x, x1, x2, z, b, b1, b2, f, g :: Id+[x, x1, x2, z, b, b1, b2, f, g] = mkTestIds+ [ ("x", int)+ , ("x1", int)+ , ("x2", int)+ , ("z", int)+ , ("b", bool)+ , ("b1", bool)+ , ("b2", bool)+ , ("f", bool2int2int)+ , ("g", bool2int2int)+ ]+++-- | @+-- let f b x =+-- if b+-- then f b z+-- else z+-- in f False 1+-- @+simpleRecursive1 :: CoreExpr+simpleRecursive1 = tidyExpr emptyTidyEnv $+ letrec+ f (lam b $ lam x $+ ite (var b)+ (var f $$ var b $$ var z)+ (var z))+ (var f $$ boolLit False $$ intLit 1)+++-- | @+-- let f b1 x1 =+-- let g b2 x2 =+-- if b2+-- then g b2 z+-- else f b2 x2+-- in if b1+-- then g b1 x1+-- else z+-- in f False 1+-- @+nestedRecursive1 :: CoreExpr+nestedRecursive1 = tidyExpr emptyTidyEnv $+ letrec+ f (lam b1 $ lam x1 $+ letrec+ g (lam b2 $ lam x2 $+ ite (var b2)+ (var g $$ var b2 $$ var z)+ (var f $$ var b2 $$ var x2))+ (ite (var b)+ (var g $$ var b1 $$ var x1)+ (var z)))+ (var f $$ boolLit False $$ intLit 1)
+ datafix.cabal view
@@ -0,0 +1,168 @@+name: datafix+version: 0.0.0.1+synopsis: Fixing data-flow problems+description: Fixing data-flow problems in expression trees++license: ISC+license-file: LICENSE+author: Sebastian Graf+maintainer: sgraf1337@gmail.com+copyright: © 2017 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++extra-source-files:+ README.md+ stack.yaml+ exprs/const.hs+ exprs/findLT.hs+ exprs/kahan.hs+ exprs/lambda.hs+ exprs/sieve.hs++source-repository head+ type: git+ location: https://github.com/sgraf812/datafix++flag no-lattices+ description: Don't depend on the lattices package.+ default: False++custom-setup+ setup-depends:+ base+ , Cabal+ -- let cabal-toolkit choose the right Cabal and base versions+ , cabal-toolkit >= 0.0.4++library+ default-language: Haskell2010+ ghc-options: -Wall+ hs-source-dirs: src+ exposed-modules: Datafix+ Datafix.Tutorial+ Datafix.Description+ Datafix.MonoMap+ Datafix.NodeAllocator+ Datafix.ProblemBuilder+ Datafix.Utils.TypeLevel+ Datafix.Worklist+ Datafix.Worklist.Graph+ Datafix.Worklist.Graph.Dense+ Datafix.Worklist.Graph.Sparse+ Datafix.Worklist.Internal+ other-modules:+ Datafix.Utils.GrowableVector+ Datafix.IntArgsMonoMap+ Datafix.IntArgsMonoSet+ build-depends: base >= 4.8 && < 5+ , containers >= 0.5 && < 0.6+ , transformers < 0.6+ -- Just Data.Vector.Mutable, which has been there for ages+ , vector < 0.13+ -- Data.Primitive.Array.sizeofArray was introduced in 0.6.2.0+ , primitive >= 0.6.2.0 && < 0.7+ -- has not reached the first major version, so quite unstable+ , pomaps >= 0.0.0.2 && < 0.0.1.0+ if !flag(no-lattices)+ build-depends: lattices < 2+ if flag(no-lattices)+ hs-source-dirs: lattices+ exposed-modules: Algebra.Lattice++test-suite tests+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+ hs-source-dirs: tests examples+ main-is: Main.hs+ other-modules: Analyses.AdHocStrAnal+ Analyses.StrAnal+ Analyses.StrAnal.Analysis+ Analyses.StrAnal.Arity+ Analyses.StrAnal.Strictness+ Analyses.Syntax.CoreSynF+ Analyses.Syntax.MkCoreHelpers+ Analyses.Syntax.MkCoreFromFile+ Analyses.Templates.LetDn+ Fib+ Fac+ Mutual+ Critical+ Trivial+ StrAnal+ build-depends: base >= 4.8 && < 5+ -- let cabal-toolkit choose the Cabal version+ , Cabal+ , cabal-toolkit == 0.0.4+ , tasty >= 0.11+ , tasty-hunit >= 0.9+ , tasty-smallcheck >= 0.8+ , containers+ , primitive+ , transformers < 0.6+ , datafix+ , ghc+ , ghc-paths+ , directory+ , filepath+ , turtle+ , text+ if !flag(no-lattices)+ build-depends: lattices < 2+ if flag(no-lattices)+ build-depends: pomaps >= 0.0.0.2 && < 0.0.1.0++test-suite doctests+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+ hs-source-dirs: tests+ main-is: doctest.hs+ build-depends: base >= 4.8 && < 5+ , doctest >=0.10+ , Glob >= 0.7+ , QuickCheck >= 2.5+ , datafix++benchmark benchmarks+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ ghc-options: -Wall -O2 -threaded -rtsopts -with-rtsopts=-N+ hs-source-dirs: bench examples+ main-is: Main.hs+ other-modules: Sum+ Analyses.AdHocStrAnal+ Analyses.StrAnal+ Analyses.StrAnal.Analysis+ Analyses.StrAnal.Arity+ Analyses.StrAnal.Strictness+ Analyses.Syntax.CoreSynF+ Analyses.Syntax.MkCoreHelpers+ Analyses.Syntax.MkCoreFromFile+ Analyses.Templates.LetDn+ build-depends: base >= 4.8 && < 5+ -- let cabal-toolkit choose the Cabal version+ , Cabal+ , cabal-toolkit == 0.0.4+ , criterion >= 1.1+ , deepseq+ , containers+ , primitive+ , transformers < 0.6+ , datafix + , ghc+ , ghc-paths+ , directory+ , filepath+ , turtle+ , text+ if !flag(no-lattices)+ build-depends: lattices < 2+ if flag(no-lattices)+ build-depends: pomaps >= 0.0.0.2 && < 0.0.1.0
+ examples/Analyses/AdHocStrAnal.hs view
@@ -0,0 +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)
+ examples/Analyses/StrAnal.hs view
@@ -0,0 +1,5 @@+module Analyses.StrAnal+ ( Impl.analyse+ ) where++import qualified Analyses.StrAnal.Analysis as Impl
+ examples/Analyses/StrAnal/Analysis.hs view
@@ -0,0 +1,115 @@+{-# LANGUAGE ScopedTypeVariables #-}+-- This is so that the specialisation of transferFunctionAlg gets inlined.+{-# OPTIONS_GHC -funfolding-creation-threshold=999999 #-}+--{-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}++-- | This module defines a strictness analysis in the style of GHC's+-- projection-based backwards analysis by defining a 'transferFunctionAlg'+-- that is passed on to @Analyses.Templates.LetDn.'buildProblem'@,+-- yielding a 'DataFlowProblem' to be solved by @Datafix.'solveProblem'@.+module Analyses.StrAnal.Analysis (analyse) where++import Algebra.Lattice+import Analyses.StrAnal.Arity+import Analyses.StrAnal.Strictness+import Analyses.Syntax.CoreSynF+import Analyses.Templates.LetDn+import Control.Monad (foldM)+import Datafix.Worklist (IterationBound (..),+ evalDenotation)++import CoreSyn+import Id+import Var+import VarEnv++analyse :: CoreExpr -> StrLattice+analyse expr = evalDenotation (buildDenotation transferFunctionAlg expr) NeverAbort 0++applyWhen :: Bool -> (a -> a) -> a -> a+applyWhen True f = f+applyWhen False _ = id++-- | This specifies the strictness as a 'TransferAlgebra'. Note the absence+-- of any recursion! That's all abstracted into+-- @Analyses.Tempaltes.LetDn.'buildProblem'@, so that this function definition+-- is completely compositional: It is only concerned with peeling off a single+-- layer of the 'CoreExprF' and interpret that in terms of the+-- transfer function over the @Arity -> StrLattice@ 'Domain'.+--+-- Because there is no explicit fixpointing going on, the resulting analysis+-- logic is clear and to the point.+transferFunctionAlg :: TransferAlgebra (Arity -> StrLattice)+transferFunctionAlg _ _ env expr arity =+ case expr of+ LitF _ -> pure emptyStrLattice+ TypeF _ -> pure emptyStrLattice+ -- Coercions are irrelevant to Strictness Analysis:+ -- 'emptyStrLattice' is already the 'top' element,+ -- so it's a safe approximation.+ CoercionF _ -> pure emptyStrLattice+ TickF _ e -> e arity+ CastF e _ -> e arity+ AppF f a -> do+ StrLattice (fTy, fAnns) <- f (arity + 1)+ let (argStr, fTy') = overArgs unconsArgStr fTy+ let 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) <- a argArity+ pure (mkStrLattice (aTy `bothStrType` fTy') (fAnns \/ aAnns))+ VarF id_+ | isLocalId id_ -> do+ rhsType <- case lookupVarEnv env id_ of+ Just denotation -> strType <$> denotation arity+ Nothing -> pure emptyStrType+ pure (mkStrLattice (unitStrType id_ (Strict arity) `bothStrType` rhsType) emptyAnnotations)+ | otherwise -> pure emptyStrLattice+ LamF id_ body+ | isTyVar id_ -> body arity+ | otherwise -> do+ StrLattice (ty1, anns) <- body (0 /\ (arity-1))+ let (argStr, ty2) = peelFV id_ ty1+ let anns' = annotate id_ argStr anns+ let ty3 = modifyArgs (consArgStr argStr) ty2+ let ty4 = applyWhen (arity == 0) lazifyStrType ty3+ pure (mkStrLattice ty4 anns')+ CaseF scrut bndr _ alts -> do+ let transferAlt (_, bndrs, transfer) = do+ latt <- transfer arity+ pure (peelAndAnnotateFVs bndrs latt)+ StrLattice (altTy, altAnns) <-+ peelAndAnnotateFV bndr . joins <$> mapM transferAlt alts+ StrLattice (scrutTy, scrutAnns) <- scrut 0+ pure (mkStrLattice (scrutTy `bothStrType` altTy) (scrutAnns \/ altAnns))+ LetF bind body -> do+ let transferBinder (StrLattice (ty, anns)) (id_, transfer) = do+ -- We do this only for annotations.+ -- Strictness on free variables was unleashed+ -- at call sites, now we only have to+ -- 'transfer' with the minimum incoming arity.+ -- Well, actually the minimum possible arity+ -- for which we annotate is 'idArity'.+ -- This is OK as long as the function is only+ -- called through the wrapper and as long as+ -- this wrapper is only inlined when fully+ -- saturated.+ -- Otherwise, to account for unsaturated calls,+ -- we'd always have to assume incoming arity 0+ -- for annotations, which wouldn't allow us to+ -- unbox any arguments.+ let (str, ty') = peelFV id_ ty+ let anns' = annotate id_ str anns+ let oldArity = Arity (idArity id_)+ let safeArity+ | Strict n <- str = n+ | otherwise = 0+ let annotationArity = oldArity /\ safeArity+ StrLattice (_, rhsAnns) <- transfer annotationArity+ pure (mkStrLattice ty' (anns' \/ rhsAnns))+ latt <- body arity+ foldM transferBinder latt (flattenBindsF [bind])
+ examples/Analyses/StrAnal/Arity.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeFamilies #-}++module Analyses.StrAnal.Arity where++import Algebra.Lattice+import Algebra.PartialOrd+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap+import Data.Maybe (maybeToList)+import Data.Ord (Down (..))+import GHC.Exts (coerce)++import Datafix.MonoMap++-- | Arity is totally ordered, but with the order turned+-- upside down. E.g., 'Arity 0' is the figurative 'top'+-- element and the instance for 'JoinSemiLattice' will+-- return the minimum of the two arities.+--+-- This corresponds to the intuition that more incoming+-- arguments is more valuable information to the analysis.+newtype Arity+ = Arity Int+ deriving (Eq, Num)++instance Show Arity where+ show (Arity i) = show i++instance Ord Arity where+ compare (Arity a) (Arity b) = compare (Down a) (Down b)++instance PartialOrd Arity where+ leq a b = a <= b++instance JoinSemiLattice Arity where+ Arity a \/ Arity b = Arity (min a b)++instance MeetSemiLattice Arity where+ Arity a /\ Arity b = Arity (max a b)++newtype ArityMap v+ = ArityMap (IntMap v)+ deriving (Eq, Show, Foldable)++-- | This can use an efficient 'IntMap' representation instead of the default+-- implementation using 'POMap'.+--+-- We must be careful with the 'Op' ordering, though.+instance MonoMapKey Arity where+ type MonoMap Arity = ArityMap+ empty = ArityMap IntMap.empty+ singleton (Arity n) v = ArityMap (IntMap.singleton n v)+ insert (Arity n) v (ArityMap m) = ArityMap (IntMap.insert n v m)+ delete (Arity n) (ArityMap m) = ArityMap (IntMap.delete n m)+ lookup (Arity n) (ArityMap m) = IntMap.lookup n m+ -- using GT here!+ lookupLT (Arity n) (ArityMap m) = coerce (maybeToList (IntMap.lookupGT n m))+ -- maxview!+ lookupMin (ArityMap m) = coerce (maybeToList (fst <$> IntMap.maxViewWithKey m))+ difference (ArityMap a) (ArityMap b) = ArityMap (IntMap.difference a b)+ keys (ArityMap m) = coerce (IntMap.keys m)+ insertWith f (Arity n) v (ArityMap m) = ArityMap (IntMap.insertWith f n v m)+ insertLookupWithKey f (Arity n) v (ArityMap m) =+ coerce (IntMap.insertLookupWithKey (coerce f) n v m)+ updateLookupWithKey f (Arity n) (ArityMap m) =+ coerce (IntMap.updateLookupWithKey (coerce f) n m)+ alter f (Arity n) (ArityMap m) = ArityMap (IntMap.alter (coerce f) n m)+ adjust f (Arity n) (ArityMap m) = ArityMap (IntMap.adjust (coerce f) n m)
+ examples/Analyses/StrAnal/Strictness.hs view
@@ -0,0 +1,284 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Analyses.StrAnal.Strictness where++import Algebra.Lattice+import Data.IntMap.Strict (IntMap)+import Data.Maybe (fromMaybe)+import Unsafe.Coerce (unsafeCoerce)++import Analyses.StrAnal.Arity++import Coercion+import Id+import UniqFM+import VarEnv++instance Show v => Show (UniqFM v) where+ -- I'd rather use coerce or the UFM constructor, but+ -- that isn't exported.+ show env = show (unsafeCoerce env :: IntMap v)+++-- | Captures lower bounds on evaluation cardinality of some variable.+-- E.g.: Is this variable evaluated at least once, and if so, what is the+-- maximum number of arguments it was surely applied to?+data Strictness+ = Lazy -- ^ Evaluated lazily (possibly not evaluated at all)+ | Strict Arity -- ^ Evaluated strictly (>= 1), called with n args+ | HyperStrict -- ^ Fully evaluated, a call with maximum arity+ deriving Eq++instance Show Strictness where+ show Lazy = "L"+ show (Strict n) = "S(" ++ show n ++ ")"+ show HyperStrict = "B"++instance JoinSemiLattice Strictness where+ Lazy \/ _ = Lazy+ _ \/ Lazy = Lazy+ HyperStrict \/ s = s+ s \/ HyperStrict = s+ Strict n \/ Strict m = Strict (n \/ m)++instance BoundedJoinSemiLattice Strictness where+ bottom = HyperStrict++instance MeetSemiLattice Strictness where+ HyperStrict /\ _ = HyperStrict+ _ /\ HyperStrict = HyperStrict+ Lazy /\ s = s+ s /\ Lazy = s+ Strict n /\ Strict m = Strict (n /\ m)++instance BoundedMeetSemiLattice Strictness where+ top = Lazy++-- | Captures certain divergence through 'Diverges', which allows+-- to assume a 'defaultStr' of 'HyperStrict'.+data Termination+ = Diverges -- ^ Denotes certain divergence+ | Dunno -- ^ Possibly terminates+ deriving (Eq, Show)++instance JoinSemiLattice Termination where+ Diverges \/ t = t+ t \/ Diverges = t+ _ \/ _ = Dunno++instance BoundedJoinSemiLattice Termination where+ bottom = Diverges++instance MeetSemiLattice Termination where+ Diverges /\ _ = Diverges+ _ /\ Diverges = Diverges+ _ /\ _ = Dunno++instance BoundedMeetSemiLattice Termination where+ top = Dunno++-- | In the case of divergence, we want to assume+-- an optimistic 'HyperStrict' strictness for any variables+-- not present in the 'StrEnv'.+-- Otherwise, those variables are possible absent and thus used+-- lazily.+defaultStr :: Termination -> Strictness+defaultStr Dunno = Lazy+defaultStr Diverges = HyperStrict++-- | Tracks strictness on free variables of a possibly diverging+-- expression.+data StrEnv+ = StrEnv !(VarEnv Strictness) !Termination+ deriving (Eq, Show)++instance JoinSemiLattice StrEnv where+ (StrEnv a t1) \/ (StrEnv b t2) =+ StrEnv (plusVarEnv_CD (\/) a (defaultStr t1) b (defaultStr t2)) (t1 \/ t2)++instance BoundedJoinSemiLattice StrEnv where+ bottom = StrEnv emptyVarEnv Diverges++instance MeetSemiLattice StrEnv where+ (StrEnv a t1) /\ (StrEnv b t2) =+ StrEnv (plusVarEnv_CD (/\) a (defaultStr t1) b (defaultStr t2)) (t1 /\ t2)++instance BoundedMeetSemiLattice StrEnv where+ top = StrEnv emptyVarEnv Dunno++unitStrEnv :: Var -> Strictness -> StrEnv+unitStrEnv id_ str = StrEnv (unitVarEnv id_ str) Dunno++peelStrEnv :: Id -> StrEnv -> (Strictness, StrEnv)+peelStrEnv id_ (StrEnv env t) =+ (fromMaybe (defaultStr t) (lookupVarEnv env id_), StrEnv (delVarEnv env id_) t)++peelFV :: Id -> StrType -> (Strictness, StrType)+peelFV id_ ty =+ let (str, fvs') = peelStrEnv id_ (fvs ty)+ in (str, ty { fvs = fvs' })++lazifyStrEnv :: StrEnv -> StrEnv+lazifyStrEnv _ = top++data ArgStr+ = BottomArgStr+ | TopArgStr+ | ConsArgStr !Strictness !ArgStr+ deriving Eq++instance Show ArgStr where+ show argStr = "[" ++ impl argStr ++ "]"+ where+ impl BottomArgStr = "B,B.."+ impl TopArgStr = "L,L.."+ impl (ConsArgStr str args') = show str ++ "," ++ impl args'++instance JoinSemiLattice ArgStr where+ BottomArgStr \/ s = s+ s \/ BottomArgStr = s+ TopArgStr \/ _ = TopArgStr+ _ \/ TopArgStr = TopArgStr+ (ConsArgStr s1 a1) \/ (ConsArgStr s2 a2) = ConsArgStr (s1 \/ s2) (a1 \/ a2)++instance BoundedJoinSemiLattice ArgStr where+ bottom = BottomArgStr++-- | This instance doesn't make a lot of sense semantically,+-- but it's the dual to the 'JoinSemiLattice' instance.+-- We mostly need this for 'top'.+instance MeetSemiLattice ArgStr where+ BottomArgStr /\ _ = BottomArgStr+ _ /\ BottomArgStr = BottomArgStr+ TopArgStr /\ s = s+ s /\ TopArgStr = s+ (ConsArgStr s1 a1) /\ (ConsArgStr s2 a2) = ConsArgStr (s1 /\ s2) (a1 /\ a2)++instance BoundedMeetSemiLattice ArgStr where+ top = TopArgStr++consArgStr :: Strictness -> ArgStr -> ArgStr+consArgStr Lazy TopArgStr = TopArgStr+consArgStr HyperStrict BottomArgStr = BottomArgStr+consArgStr s a = ConsArgStr s a++unconsArgStr :: ArgStr -> (Strictness, ArgStr)+unconsArgStr BottomArgStr = (bottom, BottomArgStr)+unconsArgStr TopArgStr = (top, TopArgStr)+unconsArgStr (ConsArgStr s a) = (s, a)++data StrType+ = StrType+ { fvs :: !StrEnv+ , args :: !ArgStr+ } deriving (Eq, Show)++instance JoinSemiLattice StrType where+ (StrType fvs1 args1) \/ (StrType fvs2 args2) =+ StrType (fvs1 \/ fvs2) (args1 \/ args2)++instance BoundedJoinSemiLattice StrType where+ bottom = StrType bottom bottom++-- | This instance doesn't make a lot of sense semantically,+-- but it's the dual to the 'JoinSemiLattice' instance.+-- We mostly need this for 'top'.+instance MeetSemiLattice StrType where+ (StrType fvs1 args1) /\ (StrType fvs2 args2) =+ StrType (fvs1 /\ fvs2) (args1 /\ args2)++instance BoundedMeetSemiLattice StrType where+ top = StrType top top++overFVs :: (StrEnv -> (a, StrEnv)) -> StrType -> (a, StrType)+overFVs f ty =+ let (a, fvs') = f (fvs ty)+ in (a, ty { fvs = fvs' })++overArgs :: (ArgStr -> (a, ArgStr)) -> StrType -> (a, StrType)+overArgs f ty =+ let (a, args') = f (args ty)+ in (a, ty { args = args' })++modifyArgs :: (ArgStr -> ArgStr) -> StrType -> StrType+modifyArgs f = snd . overArgs (\a -> ((), f a))++emptyStrType :: StrType+emptyStrType = top++unitStrType :: Id -> Strictness -> StrType+unitStrType id_ str = StrType (unitStrEnv id_ str) top++-- | Sequential composition, or Par or both.+-- This is right biased, meaning that it will return the+-- argument strictness of the right argument.+bothStrType :: StrType -> StrType -> StrType+bothStrType (StrType fvs1 _) (StrType fvs2 args2) =+ StrType (fvs1 /\ fvs2) args2++lazifyStrType :: StrType -> StrType+lazifyStrType ty = StrType fvs' (args ty)+ -- Doesn't change argument strictness, but+ -- it shouldn't actually matter.+ -- Anyway, ArgStr always corresponds to a+ -- single incoming call.+ where+ fvs' = lazifyStrEnv (fvs ty)++-- | Tracks annotations in the syntax tree.+-- Has an instance of 'JoinSemiLattice', but+-- really doesn't allow overwriting annotations.+newtype Annotations+ = Ann (VarEnv Strictness)+ deriving (Eq, Show)++emptyAnnotations :: Annotations+emptyAnnotations = Ann emptyVarEnv++instance JoinSemiLattice Annotations where+ (Ann a) \/ (Ann b) = Ann $ plusVarEnv_C (\/) a b++instance BoundedJoinSemiLattice Annotations where+ bottom = emptyAnnotations++overwriteError :: (Show a, Show b) => a -> b -> c+overwriteError old new =+ error $+ "Should never overwrite an annotation. Old: "+ ++ show old ++ ", New: "+ ++ show new++annotate :: Id -> Strictness -> Annotations -> Annotations+annotate id_ str (Ann anns) = Ann (extendVarEnv_C overwriteError anns id_ str)++lookupAnnotation :: Id -> Annotations -> Maybe Strictness+lookupAnnotation id_ (Ann env) = lookupVarEnv env id_++newtype StrLattice+ = StrLattice (StrType, Annotations)+ deriving (Eq, Show, JoinSemiLattice, BoundedJoinSemiLattice)++mkStrLattice :: StrType -> Annotations -> StrLattice+mkStrLattice ty ann = StrLattice (ty, ann)++emptyStrLattice :: StrLattice+emptyStrLattice = mkStrLattice emptyStrType emptyAnnotations++strType :: StrLattice -> StrType+strType (StrLattice (ty, _)) = ty++annotations :: StrLattice -> Annotations+annotations (StrLattice (_, anns)) = anns++peelAndAnnotateFV :: Id -> StrLattice -> StrLattice+peelAndAnnotateFV id_ (StrLattice (ty, anns)) =+ let (str, ty') = peelFV id_ ty+ anns' = annotate id_ str anns+ in mkStrLattice ty' anns'++peelAndAnnotateFVs :: [Id] -> StrLattice -> StrLattice+peelAndAnnotateFVs ids latt = foldr peelAndAnnotateFV latt ids
+ examples/Analyses/Syntax/CoreSynF.hs view
@@ -0,0 +1,45 @@+module Analyses.Syntax.CoreSynF where++import Coercion+import CoreSyn+import Id+import Literal+import Type+import Unsafe.Coerce (unsafeCoerce)++newtype Fix f+ = In { out :: f (Fix f) }++type AltF b a = (AltCon, [b], a)++data BindF b a+ = NonRecF b a+ | RecF [(b, a)]++flattenBindsF :: [BindF b a] -> [(b, a)]+flattenBindsF = concatMap impl+ where+ impl (NonRecF b a) = [(b, a)]+ impl (RecF bs) = bs++data ExprF b a+ = VarF Id+ | LitF Literal+ | AppF a a+ | LamF b a+ | LetF (BindF b a) a+ | CaseF a b Type [AltF b a]+ | CastF a Coercion+ | TickF (Tickish Id) a+ | TypeF Type+ | CoercionF Coercion++type CoreExprF+ = ExprF CoreBndr++-- | 'unsafeCoerce' mostly because I'm too lazy to write the boilerplate.+fromCoreExpr :: CoreExpr -> Fix CoreExprF+fromCoreExpr = unsafeCoerce++toCoreExpr :: CoreExpr -> Fix CoreExprF+toCoreExpr = unsafeCoerce
+ examples/Analyses/Syntax/MkCoreFromFile.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}++-- | This whole module is basically a huge hack that+-- compiles a haskell module and returns the expression+-- bound to the top-level, non-recursive `expr` binding.+module Analyses.Syntax.MkCoreFromFile where++import Control.Monad.IO.Class+import Data.Maybe (fromMaybe)+import Data.Monoid (First (..))+import qualified Data.Text as Text+import Distribution.Simple.LocalBuildInfo+import Distribution.Simple.Toolkit (getGHCPackageDBFlags,+ localBuildInfoQ)+import Prelude hiding (FilePath)+import qualified Prelude+import System.Directory (canonicalizePath)+import System.FilePath (splitSearchPath)+import Turtle++import CoreSyn+import CoreTidy (tidyExpr)+import DynFlags+import GHC+import qualified GHC.Paths+import Id+import Name+import Packages+import VarEnv (emptyTidyEnv)++findTopLevelDecl :: String -> CoreProgram -> Maybe CoreExpr+findTopLevelDecl occ = getFirst . foldMap (First . findName)+ where+ findName (NonRec id_ rhs)+ | occNameString (occName (idName id_)) == occ+ = Just rhs+ findName _ = Nothing+++compileCoreExpr :: Prelude.FilePath -> IO CoreExpr+compileCoreExpr modulePath = runGhc (Just GHC.Paths.libdir) $ do+ -- Don't generate any artifacts+ _ <- getSessionDynFlags >>= setSessionDynFlags . (\df -> df { hscTarget = HscNothing })+ -- Set up the package database++ addPkgDbs $(localBuildInfoQ)+ m <- liftIO (canonicalizePath modulePath) >>= compileToCoreModule+ pure $+ tidyExpr emptyTidyEnv+ -- . pprTraceIt "expr"+ . fromMaybe (error "Could not find top-level non-recursive binding `expr`")+ . findTopLevelDecl "expr"+ . cm_binds+ $ m+++stackPkgDbs :: MonadIO m => m (Maybe [Prelude.FilePath])+stackPkgDbs = do+ (ec, paths) <- procStrict "stack" ["path", "--ghc-package-path"] mempty+ if ec == ExitSuccess+ then pure (Just (splitSearchPath (Text.unpack paths)))+ else pure Nothing+++-- | Add a list of package databases to the Ghc monad.+addPkgDbs :: (MonadIO m, GhcMonad m) => LocalBuildInfo -> m ()+addPkgDbs lbi = do+ dfs <- getSessionDynFlags+ let pkgs = getGHCPackageDBFlags lbi+#if MIN_VERSION_Cabal(2,0,0)+ let dfs' = dfs { packageDBFlags = pkgs }+#else+ let dfs' = dfs { extraPkgConfs = (pkgs ++) . extraPkgConfs dfs }+#endif+ _ <- setSessionDynFlags dfs'+ _ <- liftIO $ initPackages dfs'+ return ()
+ examples/Analyses/Syntax/MkCoreHelpers.hs view
@@ -0,0 +1,53 @@+module Analyses.Syntax.MkCoreHelpers where++import CoreSyn+import FastString+import Id+import Literal+import MkCore+import Type+import TysWiredIn+import Unique++mkTestId :: Int -> String -> Type -> Id+mkTestId i s = mkSysLocal (mkFastString s) (mkBuiltinUnique i)++mkTestIds :: [(String, Type)] -> [Id]+mkTestIds = zipWith (\i (s, t) -> mkTestId i s t) [0..]++int :: Type+int = intTy++bool :: Type+bool = boolTy++int2int :: Type+int2int = mkFunTys [int] int++int2int2int :: Type+int2int2int = mkFunTys [int, int] int++bool2int2int :: Type+bool2int2int = mkFunTys [bool, int] int++letrec :: Id -> CoreExpr -> CoreExpr -> CoreExpr+letrec id_ rhs = mkCoreLet (Rec [(id_, rhs)])++lam :: Id -> CoreExpr -> CoreExpr+lam = Lam++var :: Id -> CoreExpr+var = Var++ite :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr+ite = mkIfThenElse++($$) :: CoreExpr -> CoreExpr -> CoreExpr+f $$ a = App f a++intLit :: Integer -> CoreExpr+intLit i = Lit (mkLitInteger i int)++boolLit :: Bool -> CoreExpr+boolLit True = Var trueDataConId+boolLit False = Var falseDataConId
+ examples/Analyses/Templates/LetDn.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fexpose-all-unfoldings #-}++-- | This module provides a template for backward analyses in the style of+-- GHC's projection-based strictness analysis. Defining property is the way+-- in which let-bindings are handled: Strictness types are unleashed at call+-- sites depending on incoming argument strictness.+--+-- The idea is that users of this module only need to provide a+-- 'TransferAlgebra' for 'buildProblem' to get a specification for the desired+-- data-flow problem. Remarkably, 'buildProblem' completely abstracts away+-- recursive bindings: The passed 'TransferAlgebra' is non-recursive and thus+-- doesn't need to do any allocation of 'Node's or calls to 'dependOn'.+-- As a result, 'TransferAlgebra's operate in a clean @forall m. Monad m@+-- constraint, guaranteeing purity.++module Analyses.Templates.LetDn+ ( TransferAlgebra+ , buildDenotation+ ) where++import Data.Proxy (Proxy (..))++import Analyses.Syntax.CoreSynF+import Datafix++import CoreSyn+import VarEnv++-- | A 'TransferAlgebra' for a given @lattice@ interprets a single layer of+-- 'CoreExprF' in terms of a 'LiftedFunc lattice m', for any possible+-- @'Monad' m@. It has access to a 'VarEnv' of transfer functions for every+-- free variable in the expression in order to do so.+--+-- The suffix @Algebra@ is inspired by recursion schemes. 'TransferAlgebra's+-- are <F-algebras https://en.wikipedia.org/wiki/F-algebra>, where the+-- /base functor/ is 'CoreExprF' and the /carrier/ is a transfer function of+-- type 'LiftedFunc lattice m'.+--+-- By the same analogy, 'buildDenotation' is the associated recursion scheme.+--+-- To recover general recursion, it's still possible to implement a paramorphic+-- variant of 'buildDenotation' that feeds what would be a R-'TransferAlgebra'.+type TransferAlgebra lattice+ = forall m+ . Monad m+ => Proxy m+ -> Proxy lattice+ -> VarEnv (LiftedFunc lattice m)+ -> CoreExprF (LiftedFunc lattice m)+ -> LiftedFunc lattice m++type TF m = LiftedFunc (Domain m) m++-- | Given a 'TransferAlgebra', this function takes care of building a+-- 'DataFlowProblem' for 'CoreExpr's.+-- It allocates 'Node's and ties knots for recursive bindings+-- through calls to 'dependOn'. These are then hidden in a 'VarEnv'+-- and passed on to the 'TransferAlgebra', which can stay completely+-- agnostic of node allocation and 'MonadDependency' this way.+--+-- It returns the root 'Node', denoting the passed expression, and the maximum+-- allocated 'Node', which allows to configure 'solveProblem' with a dense+-- 'GraphRef'. The final return value is the 'DataFlowProblem' reflecting+-- the analysis specified by the 'TransferAlgebra' applied to the given+-- 'CoreExpr'.+--+-- Continuing the recursion schemes analogy from 'TransferAlgebra',+-- 'buildProblem' is a recursion scheme. Applying it to a 'TransferAlgebra'+-- yields a catamorphism. It is special in that recursive let-bindings+-- 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)+ -> CoreExpr+ -> ProblemBuilder m (TF m)+buildDenotation alg' = buildExpr emptyVarEnv+ where+ alg = alg' (Proxy :: Proxy m) (Proxy :: Proxy (Domain m))+ buildExpr+ :: VarEnv (TF m)+ -> CoreExpr+ -> ProblemBuilder m (TF m)+ buildExpr env expr =+ case expr of+ Lit lit -> pure (alg env (LitF lit))+ Var id_ -> pure (alg env (VarF id_))+ Type ty -> pure (alg env (TypeF ty))+ Coercion co -> pure (alg env (CoercionF co))+ Cast e co -> do+ transferE <- buildExpr env e+ pure (alg env (CastF transferE co))+ Tick t e -> do+ transferE <- buildExpr env e+ pure (alg env (TickF t transferE))+ App f a -> do+ transferF <- buildExpr env f+ transferA <- buildExpr env a+ pure (alg env (AppF transferF transferA))+ Lam id_ body -> do+ transferBody <- buildExpr env body+ pure (alg env (LamF id_ transferBody))+ Case scrut bndr ty alts -> do+ transferScrut <- buildExpr env scrut+ transferAlts <- mapM (buildAlt env) alts+ pure (alg env (CaseF transferScrut bndr ty transferAlts))+ Let bind body -> do+ (env', transferredBind) <- datafixBindingGroup env bind+ transferBody <- buildExpr env' body+ -- Note that we pass the old env to 'alg'.+ -- 'alg' should use 'transferredBind' for+ -- annotated RHSs.+ pure (alg env (LetF transferredBind transferBody))+ {-# INLINE buildExpr #-}++ buildAlt env (con, bndrs, e) = do+ transferE <- buildExpr env e+ pure (con, bndrs, transferE)+ {-# INLINE buildAlt #-}++ mapBinders f env bind = do+ let binders = flattenBinds [bind]+ (env', transferredBinds) <- f env binders+ case bind of+ Rec{} -> pure (env', RecF transferredBinds)+ NonRec{}+ | [(id_, transferRHS)] <- transferredBinds+ -> pure (env', NonRecF id_ transferRHS)+ _ -> error "NonRec, but multiple transferredBinds"+ {-# INLINE mapBinders #-}+++ datafixBindingGroup = mapBinders impl+ where+ impl env binders =+ case binders of+ [] -> pure (env, [])+ ((id_, rhs):binders') ->+ datafixEq $ \self -> do+ let env' = extendVarEnv env id_ self+ (env'', transferredBind) <- impl env' binders'+ transferRHS <- buildExpr env' rhs+ pure ((env'', (id_, self):transferredBind), transferRHS)+ {-# INLINE datafixBindingGroup #-}+{-# INLINE buildDenotation #-}
+ examples/Fac.hs view
@@ -0,0 +1,21 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Fac where++import Datafix+import Numeric.Natural++facProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+facProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+ where+ transfer :: Node -> LiftedFunc Natural m+ transfer (Node 0) = return 1+ transfer (Node 1) = return 1+ transfer (Node n) = do+ a <- dependOn @m (Node (n-1))+ return (fromIntegral n * a)++fac :: Int -> Natural+fac n = product [1..fromIntegral n]
+ examples/Fib.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Fib where++import Datafix+import Numeric.Natural++fibProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+fibProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+ where+ transfer :: Node -> LiftedFunc Natural m+ transfer (Node 0) = return 0+ transfer (Node 1) = return 1+ transfer (Node n) = do+ a <- dependOn @m (Node (n-1))+ b <- dependOn @m (Node (n-2))+ return (a + b)++fib :: Int -> Natural+fib 0 = 0+fib 1 = 1+fib n = fib (n-1) + fib (n-2)
+ examples/Mutual.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Mutual where++import Datafix+import Numeric.Natural++-- | A 'DataFlowProblem' with two nodes, mutually depending on another, like+--+-- @+-- a = b + 1+-- b = min a 10+-- @+--+-- After a few bounces, this will reach a stable state where the first node+-- has value 11 and the other has value 10.+mutualRecursiveProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+mutualRecursiveProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+ where+ transfer :: Node -> LiftedFunc Natural m+ transfer (Node 0) = do+ b <- dependOn @m (Node 1)+ return (b + 1)+ transfer (Node 1) = do+ a <- dependOn @m (Node 0)+ return (min 10 a) -- So the overall fixpoint of this is 10+ transfer (Node _) = error "Invalid node"
+ examples/Sum.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Sum where++import Datafix+import Numeric.Natural++sumProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+sumProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+ where+ transfer :: Node -> LiftedFunc Natural m+ transfer (Node 0) = return 0+ transfer (Node n) = do+ a <- dependOn @m (Node (n-1))+ return (fromIntegral n + a)
+ exprs/const.hs view
@@ -0,0 +1,5 @@+module Expr where++expr a b = const a b+ where+ const a b = a
+ exprs/findLT.hs view
@@ -0,0 +1,13 @@+module Expr where++expr :: Int -> [Int] -> Maybe Int+expr a b = findLT a b+ where+ findLT _ [] = Nothing+ findLT n (x:xs)+ | x < n = findLTJust n x xs+ | otherwise = findLT n xs+ findLTJust n m [] = Just m+ findLTJust n m (x:xs)+ | x < n && x > m = findLTJust n m xs+ | otherwise = findLTJust n x xs
+ exprs/kahan.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE FlexibleContexts #-}+-- Inferred type for 'inner' has a constraint (MArray (STUArray s) Double m)+-- An alternative fix (better, but less faithful to backward perf comparison)+-- would be MonoLocalBinds++-- | Implementation of Kahan summation algorithm that tests+-- performance of tight loops involving unboxed arrays and floating+-- point arithmetic.+module Expr where++import Control.Monad.ST+import Data.Array.Base+import Data.Array.ST+import Data.Bits+import Data.Word+import System.Environment++type Vec s = STUArray s Int Double++expr :: Int -> Vec s -> Vec s -> ST s ()+expr a b c = kahan a b c+ where+ vdim :: Int+ vdim = 100++ prng :: Word -> Word+ prng w = w'+ where+ w1 = w `xor` (w `shiftL` 13)+ w2 = w1 `xor` (w1 `shiftR` 7)+ w' = w2 `xor` (w2 `shiftL` 17)++ kahan :: Int -> Vec s -> Vec s -> ST s ()+ kahan vnum s c = do+ let inner w j+ | j < vdim = do+ cj <- unsafeRead c j+ sj <- unsafeRead s j+ let y = fromIntegral w - cj+ t = sj + y+ w' = prng w+ unsafeWrite c j ((t-sj)-y)+ unsafeWrite s j t+ inner w' (j+1)+ | otherwise = return ()++ outer i | i <= vnum = inner (fromIntegral i) 0 >> outer (i+1)+ | otherwise = return ()+ outer 1++ calc :: Int -> ST s (Vec s)+ calc vnum = do+ s <- newArray (0,vdim-1) 0+ c <- newArray (0,vdim-1) 0+ kahan vnum s c+ return s
+ exprs/lambda.hs view
@@ -0,0 +1,261 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Expr where++-- From Mark: marku@cs.waikato.ac.nz [Nov 2001]+-- This program contrasts the cost of direct and+-- state-monadic style of computation.++-- Experiments with Higher-Order mappings over terms.+-- Speed comparisons of passing environments in a monad, versus explicitly.+--+-- With Hugs98 Feb 2001: (K reductions/ K cells)+-- N mainSimple mainMonad+-- Redns Cells Redns Cells+-- 10 4.7 8 15 28+-- 20 16.0 27 49 92+-- 30 33.5 57 102 192+-- 40 58 98 175 329+-- 50 89 150 268 502+-- 80 221 373 664 1242+-- 160 865 1456 2582 4826+-- 320 3419 5754 10181 19021+--+-- With GHC 5.00.1+-- N mainSimple mainMonad+-- secs Kbytes secs Kbytes+-- 100 0.02 1180 0.08 8213+-- 200 0.080 4529 0.30 31997+-- 400 0.310 17850 1.36 126333+-- 800 1.54 70928 6.6 502096+-- 1 1600 7.66 282833 34.6 2001963+-- 2 1600 28.76 1725128 1 with newtype+-- 3 1600 28.1 1694119 2 + eval covers ALL cases+-- 4 1600 28.5 1742828 3 + recursion calls eval+-- 5 1600 7.13 282832 1 with no Add typechecks+--+-- Conclusion: mainMonad is about 4 times slower than mainSimple+-- and about 7 times more memory.+--++import System.Environment++import Control.Monad.Trans.State.Strict+import Data.Functor.Identity++----------------------------------------------------------------------+-- A directly recursive Eval, with explicit environment+----------------------------------------------------------------------+-- A trivial monad so that we can use monad syntax.+newtype Id a = Id (Identity a)+ deriving (Applicative, Functor, Monad)++instance Show a => Show (Id a) where+ show (Id i) = show (runIdentity i)+++data Term+ = Var String+ | Con Int+ | Incr+ | Add Term Term+ | Lam String Term+ | App Term Term+ | IfZero Term Term Term+ -- the following terms are used internally+ | Thunk Term Env -- a closure+ deriving (Eq,Read,Show)++type Env = [(String,Term)]+-----------------------------------------------------------------+-- This class extends Monad to have the standard features+-- we expect while evaluating/manipulating expressions.+----------------------------------------------------+class (Monad m) => EvalEnvMonad m where+ incr :: m () -- example of a state update function+ -- these defines the traversal!+ traverseTerm :: Term -> m Term+ --traversePred :: Pred -> m Pred+ lookupVar :: String -> m Term+ pushVar :: String -> Term -> m a -> m a+ currEnv :: m Env -- returns the current environment+ withEnv :: Env -> m a -> m a -- uses the given environment+ pushVar v t m = do env <- currEnv; withEnv ((v,t):env) m++instance EvalEnvMonad (State Env) where+ incr = return ()+ traverseTerm = undefined -- eval+ lookupVar v = do+ env <- get+ return $ lookup2 env+ where+ lookup2 env = maybe (error ("undefined var: " ++ v)) id (lookup v env)+ currEnv = get+ withEnv tmp m = return (evalState m tmp)++expr :: IO ()+expr = do { mainSimple ; mainMonad }+ where+ mainSimple =+ do args <- getArgs+ if null args+ then putStrLn "Args: number-to-sum-up-to"+ else putStrLn (show (simpleEval [] (App sum0 (Con (read(head args))))))++ mainMonad =+ do args <- getArgs+ if null args+ then putStrLn "Args: number-to-sum-up-to"+ else (ev (App sum0 (Con (read(head args))))) >> return ()+++ ------------------------------------------------------------+ -- Data structures+ ------------------------------------------------------------+ --instance Show (a -> b) where+ -- show f = "<function>"++ ----------------------------------------------------------------------+ -- Evaluate a term+ ----------------------------------------------------------------------+ ev :: Term -> IO (Env,Term)+ ev t =+ do let (t2, env) = runState (traverseTerm t :: State Env Term) []+ putStrLn (pp t2 ++ " " ++ ppenv env)+ return (env,t2)+++++ eval :: (EvalEnvMonad m) => Term -> m Term+ eval (Var x) =+ do e <- currEnv+ t <- lookupVar x+ traverseTerm t+ eval (Add u v) =+ do {Con u' <- traverseTerm u;+ Con v' <- traverseTerm v;+ return (Con (u'+v'))}+ eval (Thunk t e) =+ withEnv e (traverseTerm t)+ eval f@(Lam x b) =+ do env <- currEnv+ return (Thunk f env) -- return a closure!+ eval (App u v) =+ do {u' <- traverseTerm u;+ -- call-by-name, so we do not evaluate the argument v+ apply u' v+ }+ eval (IfZero c a b) =+ do {val <- traverseTerm c;+ if val == Con 0+ then traverseTerm a+ else traverseTerm b}+ eval (Con i) = return (Con i)+ eval (Incr) = incr >> return (Con 0)++ --apply :: Term -> Term -> StateMonad2 Term+ apply (Thunk (Lam x b) e) a =+ do orig <- currEnv+ withEnv e (pushVar x (Thunk a orig) (traverseTerm b))+ apply a b = fail ("bad application: " ++ pp a +++ " [ " ++ pp b ++ " ].")+++++ simpleEval :: Env -> Term -> Id Term+ simpleEval env (Var v) =+ simpleEval env (maybe (error ("undefined var: " ++ v)) id (lookup v env))+ simpleEval env e@(Con _) =+ return e+ simpleEval env e@Incr =+ return (Con 0)+ simpleEval env (Add u v) =+ do {Con u' <- simpleEval env u;+ Con v' <- simpleEval env v;+ return (Con (u' + v'))}+ where+ addCons (Con a) (Con b) = return (Con (a+b))+ addCons (Con _) b = fail ("type error in second arg of Add: " ++ pp b)+ addCons a (Con _) = fail ("type error in first arg of Add: " ++ pp a)+ simpleEval env f@(Lam x b) =+ return (Thunk f env) -- return a closure!+ simpleEval env (App u v) =+ do {u' <- simpleEval env u;+ -- call-by-name, so we do not evaluate the argument v+ simpleApply env u' v+ }+ simpleEval env (IfZero c a b) =+ do {val <- simpleEval env c;+ if val == Con 0+ then simpleEval env a+ else simpleEval env b}+ simpleEval env (Thunk t e) =+ simpleEval e t++ simpleApply :: Env -> Term -> Term -> Id Term+ simpleApply env (Thunk (Lam x b) e) a =+ simpleEval env2 b+ where+ env2 = (x, Thunk a env) : e+ simpleApply env a b = fail ("bad application: " ++ pp a +++ " [ " ++ pp b ++ " ].")++ ------------------------------------------------------------+ -- Utility functions for printing terms and envs.+ ------------------------------------------------------------+ ppenv env = "[" ++ concatMap (\(v,t) -> v ++ "=" ++ pp t ++ ", ") env ++ "]"+++ pp :: Term -> String+ pp = ppn 0++ -- Precedences:+ -- 0 = Lam and If (contents never bracketed)+ -- 1 = Add+ -- 2 = App+ -- 3 = atomic and bracketed things+ ppn :: Int -> Term -> String+ ppn _ (Var v) = v+ ppn _ (Con i) = show i+ ppn _ (Incr) = "INCR"+ ppn n (Lam v t) = bracket n 0 ("@" ++ v ++ ". " ++ ppn (-1) t)+ ppn n (Add a b) = bracket n 1 (ppn 1 a ++ " + " ++ ppn 1 b)+ ppn n (App a b) = bracket n 2 (ppn 2 a ++ " " ++ ppn 2 b)+ ppn n (IfZero c a b) = bracket n 0+ ("IF " ++ ppn 0 c ++ " THEN " ++ ppn 0 a ++ " ELSE " ++ ppn 0 b)+ ppn n (Thunk t e) = bracket n 0 (ppn 3 t ++ "::" ++ ppenv e)++ bracket outer this t | this <= outer = "(" ++ t ++ ")"+ | otherwise = t+++ ------------------------------------------------------------+ -- Test Data+ ------------------------------------------------------------+ x = (Var "x")+ y = (Var "y")+ a1 = (Lam "x" (Add (Var "x") (Con 1)))+ aa = (Lam "x" (Add (Var "x") (Var "x")))++ -- These should all return 1+ iftrue = (IfZero (Con 0) (Con 1) (Con 2))+ iffalse = (IfZero (Con 1) (Con 2) (Con 1))++ -- This function sums all the numbers from 0 upto its argument.+ sum0 :: Term+ sum0 = (App fix partialSum0)+ partialSum0 = (Lam "sum"+ (Lam "n"+ (IfZero (Var "n")+ (Con 0)+ (Add (Var "n") (App (Var "sum") nMinus1)))))+ nMinus1 = (Add (Var "n") (Con (-1)))++ lfxx :: Term+ lfxx = (Lam "x" (App (Var "F") (App (Var "x") (Var "x"))))++ -- This is the fix point combinator: Y+ fix :: Term+ fix = (Lam "F" (App lfxx lfxx))
+ exprs/sieve.hs view
@@ -0,0 +1,44 @@+-- Mark II lazy wheel-sieve.+-- Colin Runciman (colin@cs.york.ac.uk); March 1996.+-- See article "Lazy wheel sieves and spirals of primes" (to appear, JFP).+module Expr where++data Wheel = Wheel Int [Int] [Int]++expr :: [Int]+expr = primes+ where+ primes :: [Int]+ primes = spiral wheels primes squares++ spiral (Wheel s ms ns:ws) ps qs =+ foldr turn0 (roll s) ns+ where+ roll o = foldr (turn o) (foldr (turn o) (roll (o+s)) ns) ms+ turn0 n rs =+ if n<q then n:rs else sp+ turn o n rs =+ let n' = o+n in+ if n'==2 || n'<q then n':rs else dropWhile (<n') sp+ sp = spiral ws (tail ps) (tail qs)+ q = head qs++ squares :: [Int]+ squares = [p*p | p <- primes]++ wheels :: [Wheel]+ wheels = Wheel 1 [1] [] :+ zipWith3 nextSize wheels primes squares++ nextSize (Wheel s ms ns) p q =+ Wheel (s*p) ms' ns'+ where+ (xs, ns') = span (<=q) (foldr turn0 (roll (p-1) s) ns)+ ms' = foldr turn0 xs ms+ roll 0 _ = []+ roll t o = foldr (turn o) (foldr (turn o) (roll (t-1) (o+s)) ns) ms+ turn0 n rs =+ if n`mod`p>0 then n:rs else rs+ turn o n rs =+ let n' = o+n in+ if n'`mod`p>0 then n':rs else rs
+ lattices/Algebra/Lattice.hs view
@@ -0,0 +1,477 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE Safe #-}+#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709+{-# OPTIONS_GHC -fno-warn-amp #-}+#endif+----------------------------------------------------------------------------+-- |+-- Module : Algebra.Lattice+-- Copyright : (C) 2010-2015 Maximilian Bolingbroke+-- License : BSD-3-Clause (see the file LICENSE)+--+-- Maintainer : Oleg Grenrus <oleg.grenrus@iki.fi>+--+-- In mathematics, a lattice is a partially ordered set in which every+-- two elements have a unique supremum (also called a least upper bound+-- or @join@) and a unique infimum (also called a greatest lower bound or+-- @meet@).+--+-- In this module lattices are defined using 'meet' and 'join' operators,+-- as it's constructive one.+--+----------------------------------------------------------------------------+module Algebra.Lattice (+ -- * Unbounded lattices+ JoinSemiLattice(..), MeetSemiLattice(..), Lattice,+ joinLeq, meetLeq,++ -- * Bounded lattices+ BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice,+ joins, meets,+ fromBool,++ -- * Monoid wrappers+ Meet(..), Join(..),++ -- * Fixed points of chains in lattices+ lfp, lfpFrom, unsafeLfp,+ gfp, gfpFrom, unsafeGfp,+ ) where++import qualified Algebra.PartialOrd as PO++import Control.Monad.Zip (MonadZip (..))+import Data.Data (Data, Typeable)+import Data.Proxy (Proxy (..))+import Data.Semigroup (All (..), Any (..), Endo (..),+ Semigroup (..))+import Data.Void (Void)+import GHC.Generics (Generic)++import qualified Data.IntMap as IM+import qualified Data.IntSet as IS+import qualified Data.Map as M+import qualified Data.Set as S++import Control.Applicative (Const (..))+import Data.Functor.Identity (Identity (..))++infixr 6 /\ -- This comment needed because of CPP+infixr 5 \/++-- | A algebraic structure with element joins: <http://en.wikipedia.org/wiki/Semilattice>+--+-- > Associativity: x \/ (y \/ z) == (x \/ y) \/ z+-- > Commutativity: x \/ y == y \/ x+-- > Idempotency: x \/ x == x+class JoinSemiLattice a where+ (\/) :: a -> a -> a+ (\/) = join++ join :: a -> a -> a+ join = (\/)++#if __GLASGOW_HASKELL__ >= 707+ {-# MINIMAL (\/) | join #-}+#endif+{-# DEPRECATED join "Use '\\/' infix operator" #-}++-- | The partial ordering induced by the join-semilattice structure+joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool+joinLeq x y = (x \/ y) == y++-- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice>+--+-- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z+-- > Commutativity: x /\ y == y /\ x+-- > Idempotency: x /\ x == x+class MeetSemiLattice a where+ (/\) :: a -> a -> a+ (/\) = meet++ meet :: a -> a -> a+ meet = (/\)++#if __GLASGOW_HASKELL__ >= 707+ {-# MINIMAL (/\) | meet #-}+#endif+{-# DEPRECATED meet "Use '/\\' infix operator" #-}++-- | The partial ordering induced by the meet-semilattice structure+meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool+meetLeq x y = (x /\ y) == x++++-- | The combination of two semi lattices makes a lattice if the absorption law holds:+-- see <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)>+--+-- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a+class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where++-- | A join-semilattice with some element |bottom| that \/ approaches.+--+-- > Identity: x \/ bottom == x+class JoinSemiLattice a => BoundedJoinSemiLattice a where+ bottom :: a++-- | The join of a list of join-semilattice elements+joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a+joins = getJoin . foldMap Join++-- | A meet-semilattice with some element |top| that /\ approaches.+--+-- > Identity: x /\ top == x+class MeetSemiLattice a => BoundedMeetSemiLattice a where+ top :: a++-- | The meet of a list of meet-semilattice elements+meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a+meets = getMeet . foldMap Meet++-- | Lattices with both bounds+class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where++-- | 'True' to 'top' and 'False' to 'bottom'+fromBool :: BoundedLattice a => Bool -> a+fromBool True = top+fromBool False = bottom++--+-- Sets+--++instance Ord a => JoinSemiLattice (S.Set a) where+ (\/) = S.union++instance Ord a => MeetSemiLattice (S.Set a) where+ (/\) = S.intersection++instance Ord a => Lattice (S.Set a) where++instance Ord a => BoundedJoinSemiLattice (S.Set a) where+ bottom = S.empty++--+-- IntSets+--++instance JoinSemiLattice IS.IntSet where+ (\/) = IS.union++instance MeetSemiLattice IS.IntSet where+ (/\) = IS.intersection++instance Lattice IS.IntSet++instance BoundedJoinSemiLattice IS.IntSet where+ bottom = IS.empty++--+-- Maps+--++instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where+ (\/) = M.unionWith (\/)++instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where+ (/\) = M.intersectionWith (/\)++instance (Ord k, Lattice v) => Lattice (M.Map k v) where++instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where+ bottom = M.empty++--+-- IntMaps+--++instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where+ (\/) = IM.unionWith (\/)++instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where+ bottom = IM.empty++instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where+ (/\) = IM.intersectionWith (/\)++instance Lattice v => Lattice (IM.IntMap v)++--+-- Functions+--++instance JoinSemiLattice v => JoinSemiLattice (k -> v) where+ f \/ g = \x -> f x \/ g x++instance MeetSemiLattice v => MeetSemiLattice (k -> v) where+ f /\ g = \x -> f x /\ g x++instance Lattice v => Lattice (k -> v) where++instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where+ bottom = const bottom++instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where+ top = const top++instance BoundedLattice v => BoundedLattice (k -> v) where++-- Unit+instance JoinSemiLattice () where+ _ \/ _ = ()++instance BoundedJoinSemiLattice () where+ bottom = ()++instance MeetSemiLattice () where+ _ /\ _ = ()++instance BoundedMeetSemiLattice () where+ top = ()++instance Lattice () where+instance BoundedLattice () where++--+-- Tuples+--++instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where+ (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2)++instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where+ (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2)++instance (Lattice a, Lattice b) => Lattice (a, b) where++instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where+ bottom = (bottom, bottom)++instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where+ top = (top, top)++instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where++--+-- Bools+--++instance JoinSemiLattice Bool where+ (\/) = (||)++instance MeetSemiLattice Bool where+ (/\) = (&&)++instance Lattice Bool where++instance BoundedJoinSemiLattice Bool where+ bottom = False++instance BoundedMeetSemiLattice Bool where+ top = True++instance BoundedLattice Bool where++--- Monoids++-- | Monoid wrapper for JoinSemiLattice+newtype Join a = Join { getJoin :: a }+ deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic)++instance JoinSemiLattice a => Semigroup (Join a) where+ Join a <> Join b = Join (a \/ b)++instance BoundedJoinSemiLattice a => Monoid (Join a) where+ mempty = Join bottom+ Join a `mappend` Join b = Join (a \/ b)++instance Functor Join where+ fmap f (Join x) = Join (f x)++instance Applicative Join where+ pure = Join+ Join f <*> Join x = Join (f x)+ _ *> x = x++instance Monad Join where+ return = pure+ Join m >>= f = f m+ (>>) = (*>)++instance MonadZip Join where+ mzip (Join x) (Join y) = Join (x, y)++-- | Monoid wrapper for MeetSemiLattice+newtype Meet a = Meet { getMeet :: a }+ deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic)++instance MeetSemiLattice a => Semigroup (Meet a) where+ Meet a <> Meet b = Meet (a /\ b)++instance BoundedMeetSemiLattice a => Monoid (Meet a) where+ mempty = Meet top+ Meet a `mappend` Meet b = Meet (a /\ b)++instance Functor Meet where+ fmap f (Meet x) = Meet (f x)++instance Applicative Meet where+ pure = Meet+ Meet f <*> Meet x = Meet (f x)+ _ *> x = x++instance Monad Meet where+ return = pure+ Meet m >>= f = f m+ (>>) = (*>)++instance MonadZip Meet where+ mzip (Meet x) (Meet y) = Meet (x, y)++-- All+instance JoinSemiLattice All where+ All a \/ All b = All $ a \/ b++instance BoundedJoinSemiLattice All where+ bottom = All False++instance MeetSemiLattice All where+ All a /\ All b = All $ a /\ b++instance BoundedMeetSemiLattice All where+ top = All True++instance Lattice All where+instance BoundedLattice All where++-- Any+instance JoinSemiLattice Any where+ Any a \/ Any b = Any $ a \/ b++instance BoundedJoinSemiLattice Any where+ bottom = Any False++instance MeetSemiLattice Any where+ Any a /\ Any b = Any $ a /\ b++instance BoundedMeetSemiLattice Any where+ top = Any True++instance Lattice Any where+instance BoundedLattice Any where++-- Endo+instance JoinSemiLattice a => JoinSemiLattice (Endo a) where+ Endo a \/ Endo b = Endo $ a \/ b++instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where+ bottom = Endo bottom++instance MeetSemiLattice a => MeetSemiLattice (Endo a) where+ Endo a /\ Endo b = Endo $ a /\ b++instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where+ top = Endo top++instance Lattice a => Lattice (Endo a) where+instance BoundedLattice a => BoundedLattice (Endo a) where++-- Proxy+instance JoinSemiLattice (Proxy a) where+ _ \/ _ = Proxy++instance BoundedJoinSemiLattice (Proxy a) where+ bottom = Proxy++instance MeetSemiLattice (Proxy a) where+ _ /\ _ = Proxy++instance BoundedMeetSemiLattice (Proxy a) where+ top = Proxy++instance Lattice (Proxy a) where+instance BoundedLattice (Proxy a) where++#if MIN_VERSION_base(4,8,0)+-- Identity+instance JoinSemiLattice a => JoinSemiLattice (Identity a) where+ Identity a \/ Identity b = Identity (a \/ b)++instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where+ bottom = Identity bottom++instance MeetSemiLattice a => MeetSemiLattice (Identity a) where+ Identity a /\ Identity b = Identity (a /\ b)++instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where+ top = Identity top++instance Lattice a => Lattice (Identity a) where+instance BoundedLattice a => BoundedLattice (Identity a) where+#endif++-- Const+instance JoinSemiLattice a => JoinSemiLattice (Const a b) where+ Const a \/ Const b = Const (a \/ b)++instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where+ bottom = Const bottom++instance MeetSemiLattice a => MeetSemiLattice (Const a b) where+ Const a /\ Const b = Const (a /\ b)++instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where+ top = Const top++instance Lattice a => Lattice (Const a b) where+instance BoundedLattice a => BoundedLattice (Const a b) where++-- Void+instance JoinSemiLattice Void where+ a \/ _ = a++instance MeetSemiLattice Void where+ a /\ _ = a++instance Lattice Void where++-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.+-- Assumes that the function is monotone and does not check if that is correct.+{-# INLINE unsafeLfp #-}+unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a+unsafeLfp = PO.unsafeLfpFrom bottom++-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.+-- Forces the function to be monotone.+{-# INLINE lfp #-}+lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a+lfp = lfpFrom bottom++-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.+-- Forces the function to be monotone.+{-# INLINE lfpFrom #-}+lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a+lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x \/ x)+++-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.+-- Assumes that the function is antinone and does not check if that is correct.+{-# INLINE unsafeGfp #-}+unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a+unsafeGfp = PO.unsafeGfpFrom top++-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.+-- Forces the function to be antinone.+{-# INLINE gfp #-}+gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a+gfp = gfpFrom top++-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.+-- Forces the function to be antinone.+{-# INLINE gfpFrom #-}+gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a+gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x /\ x)
+ src/Datafix.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++-- |+-- Module : Datafix+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- This is the top-level, import-all, kitchen sink module.+--+-- Look at "Datafix.Tutorial" for a tour guided by use cases.++module Datafix+ ( module Datafix.Description+ , module Datafix.NodeAllocator+ , module Datafix.ProblemBuilder+ , Datafix.MonoMap.MonoMap+ , module Datafix.Utils.TypeLevel+ , module Datafix.Worklist+ ) where++import Datafix.Description+import Datafix.MonoMap+import Datafix.NodeAllocator+import Datafix.ProblemBuilder+import Datafix.Utils.TypeLevel+import Datafix.Worklist
+ src/Datafix/Description.hs view
@@ -0,0 +1,248 @@+{-# 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 #-}
+ src/Datafix/IntArgsMonoMap.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Datafix.IntArgsMonoMap+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Composes 'IntMap' with a 'MonoMap'.++module Datafix.IntArgsMonoMap where++import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap+import Data.Maybe (maybeToList)+import Datafix.MonoMap (MonoMap, MonoMapKey)+import qualified Datafix.MonoMap as MonoMap+import GHC.Exts (coerce)++newtype IntArgsMonoMap k v+ = Map (IntMap (MonoMap k v))++deriving instance Eq (MonoMap k v) => Eq (IntArgsMonoMap k v)+deriving instance Show (MonoMap k v) => Show (IntArgsMonoMap k v)++nothingIfEmpty :: MonoMapKey k => MonoMap k v -> Maybe (MonoMap k v)+nothingIfEmpty m+ | null m = Nothing+ | otherwise = Just m++empty :: IntArgsMonoMap k v+empty = Map IntMap.empty++singleton :: MonoMapKey k => Int -> k -> v -> IntArgsMonoMap k v+singleton i k v = Map (IntMap.singleton i (MonoMap.singleton k v))++insert :: MonoMapKey k => Int -> k -> v -> IntArgsMonoMap k v -> IntArgsMonoMap k v+insert i k v (Map m) =+ Map (IntMap.insertWith (const (MonoMap.insert k v)) i (MonoMap.singleton k v) m)++delete :: MonoMapKey k => Int -> k -> IntArgsMonoMap k v -> IntArgsMonoMap k v+delete i k (Map m) = Map (IntMap.update f i m)+ where+ f monoMap = nothingIfEmpty (MonoMap.delete k monoMap)++lookup :: MonoMapKey k => Int -> k -> IntArgsMonoMap k v -> Maybe v+lookup i k (Map m) = IntMap.lookup i m >>= MonoMap.lookup k++difference :: MonoMapKey k => IntArgsMonoMap k a -> IntArgsMonoMap k b -> IntArgsMonoMap k a+difference (Map ma) (Map mb) = Map (IntMap.differenceWith f ma mb)+ where+ f a b = nothingIfEmpty (MonoMap.difference a b)++-- | Highest priority node and lowest element of the domain `k` first.+highestPriorityNodes :: MonoMapKey k => IntArgsMonoMap k v -> [(Int, k)]+highestPriorityNodes (Map m) = maybeToList (IntMap.maxViewWithKey m) >>= viewIntoMonoMap+ where+ viewIntoMonoMap ((i, monoMap), _) = pairUp i <$> MonoMap.lookupMin monoMap+ pairUp i (k, _) = (i, k)++keys :: MonoMapKey k => IntArgsMonoMap k v -> [(Int, k)]+keys (Map m) = IntMap.foldrWithKey f [] m+ where+ f i monoMap ks = map ((,) i) (MonoMap.keys monoMap) ++ ks++insertLookupWithKey+ :: MonoMapKey k+ => (Int -> k -> v -> v -> v)+ -> Int+ -> k+ -> v+ -> IntArgsMonoMap k v+ -> (Maybe v, IntArgsMonoMap k v)+insertLookupWithKey f i k v (Map m) = coerce (IntMap.alterF alterMonoMap i m)+ where+ alterMonoMap Nothing = (Nothing, Just (MonoMap.singleton k v))+ alterMonoMap (Just monoMap) = Just <$> MonoMap.insertLookupWithKey (f i) k v monoMap++insertWith+ :: MonoMapKey k+ => (v -> v -> v)+ -> Int+ -> k+ -> v+ -> IntArgsMonoMap k v+ -> IntArgsMonoMap k v+insertWith f i k v (Map m) = Map $+ IntMap.insertWith (const $ MonoMap.insertWith f k v) i (MonoMap.singleton k v) m++updateLookupWithKey+ :: MonoMapKey k+ => (Int -> k -> v -> Maybe v)+ -> Int+ -> k+ -> IntArgsMonoMap k v+ -> (Maybe v, IntArgsMonoMap k v)+updateLookupWithKey f i k (Map m) = coerce (IntMap.alterF alterMonoMap i m)+ where+ alterMonoMap Nothing = (Nothing, Nothing)+ alterMonoMap (Just monoMap) = nothingIfEmpty <$> MonoMap.updateLookupWithKey (f i) k monoMap++adjust :: MonoMapKey k => (v -> v) -> Int -> k -> IntArgsMonoMap k v -> IntArgsMonoMap k v+adjust f i k (Map m) = Map (IntMap.adjust (MonoMap.adjust f k) i m)++lookupLT :: MonoMapKey k => Int -> k -> IntArgsMonoMap k v -> [(k, v)]+lookupLT i k (Map m) = maybe [] (MonoMap.lookupLT k) (IntMap.lookup i m)
+ src/Datafix/IntArgsMonoSet.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Datafix.IntArgsMonoSet+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Wraps an 'IntArgsMonoMap' into an 'IntArgsMonoSet'.++module Datafix.IntArgsMonoSet where++import Data.Maybe (isJust)+import Datafix.IntArgsMonoMap (IntArgsMonoMap)+import qualified Datafix.IntArgsMonoMap as Map+import Datafix.MonoMap (MonoMap, MonoMapKey)+import GHC.Exts (coerce)++newtype IntArgsMonoSet k+ = Set (IntArgsMonoMap k ())++deriving instance Eq (MonoMap k ()) => Eq (IntArgsMonoSet k)+deriving instance Show (MonoMap k ()) => Show (IntArgsMonoSet k)++empty :: IntArgsMonoSet k+empty = Set Map.empty++singleton :: MonoMapKey k => Int -> k -> IntArgsMonoSet k+singleton i k = Set (Map.singleton i k ())++insert :: MonoMapKey k => Int -> k -> IntArgsMonoSet k -> IntArgsMonoSet k+insert i k = coerce (Map.insert i k ())++delete :: MonoMapKey k => Int -> k -> IntArgsMonoSet k -> IntArgsMonoSet k+delete i k (Set m) = Set (Map.delete i k m)++member :: MonoMapKey k => Int -> k -> IntArgsMonoSet k -> Bool+member i k (Set m) = isJust (Map.lookup i k m)++difference :: MonoMapKey k => IntArgsMonoSet k -> IntArgsMonoSet k -> IntArgsMonoSet k+difference (Set a) (Set b) = Set (Map.difference a b)++toList :: MonoMapKey k => IntArgsMonoSet k -> [(Int, k)]+toList (Set m) = Map.keys m++highestPriorityNodes :: MonoMapKey k => IntArgsMonoSet k -> [(Int, k)]+highestPriorityNodes (Set m) = Map.highestPriorityNodes m
+ src/Datafix/MonoMap.hs view
@@ -0,0 +1,132 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeFamilyDependencies #-}++-- |+-- Module : Datafix.MonoMap+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- A uniform interface for ordered maps that can be used to model+-- monotone functions.++module Datafix.MonoMap where++import Algebra.PartialOrd+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap+import Data.Maybe (maybeToList)+import Data.POMap.Strict (POMap)+import qualified Data.POMap.Strict as POMap++-- | Chooses an appropriate 'MonoMap' for a given key type.+--+-- @MonoMap@s should all be ordered maps, which feature+-- efficient variants of the 'lookupLT' and 'lookupMin' combinators.+-- This unifies "Data.Maybe", "Data.IntMap.Strict", "Data.Map.Strict" and "Data.POMap.Strict"+-- under a common type class, for which instances can delegate to the+-- most efficient variant available.+--+-- Because of 'lookupLT', this class lends itself well to approximating+-- monotone functions.+--+-- The default implementation delegates to 'POMap', so when there is no+-- specially crafted map data-structure for your key type, all you need to do+-- is to make sure it satisfies 'PartialOrd'. Then you can do+--+-- >>> import Data.IntSet+-- >>> instance MonoMapKey IntSet+--+-- to make use of the default implementation.+class Foldable (MonoMap k) => MonoMapKey k where+ type MonoMap k = (r :: * -> *) | r -> k+ -- ^ The particular ordered map implementation to use for the key type 'k'.+ type MonoMap k = POMap k+ -- ^ The default implementation delegates to 'POMap'.+ empty :: MonoMap k v+ default empty :: (MonoMap k v ~ POMap k v) => MonoMap k v+ empty = POMap.empty+ singleton :: k -> v -> MonoMap k v+ default singleton :: (MonoMap k v ~ POMap k v) => k -> v -> MonoMap k v+ singleton = POMap.singleton+ insert :: k -> v -> MonoMap k v -> MonoMap k v+ default insert :: (MonoMap k v ~ POMap k v, PartialOrd k) => k -> v -> MonoMap k v -> MonoMap k v+ insert = POMap.insert+ delete :: k -> MonoMap k v -> MonoMap k v+ default delete :: (MonoMap k v ~ POMap k v, PartialOrd k) => k -> MonoMap k v -> MonoMap k v+ delete = POMap.delete+ lookup :: k -> MonoMap k v -> Maybe v+ default lookup :: (MonoMap k v ~ POMap k v, PartialOrd k) => k -> MonoMap k v -> Maybe v+ lookup = POMap.lookup+ lookupLT :: k -> MonoMap k v -> [(k, v)]+ -- ^ Key point of this interface! Note that it returns a list of+ -- lower bounds, to account for the 'PartialOrd' case.+ default lookupLT :: (MonoMap k v ~ POMap k v, PartialOrd k) => k -> MonoMap k v -> [(k, v)]+ lookupLT = POMap.lookupLT+ lookupMin :: MonoMap k v -> [(k, v)]+ default lookupMin :: (MonoMap k v ~ POMap k v, PartialOrd k) => MonoMap k v -> [(k, v)]+ lookupMin = POMap.lookupMin+ difference :: MonoMap k a -> MonoMap k b -> MonoMap k a+ default difference :: (MonoMap k a ~ POMap k a, MonoMap k b ~ POMap k b, PartialOrd k) => MonoMap k a -> MonoMap k b -> MonoMap k a+ difference = POMap.difference+ keys :: MonoMap k a -> [k]+ default keys :: MonoMap k v ~ POMap k v => MonoMap k v -> [k]+ keys = POMap.keys+ insertWith :: (v -> v -> v) -> k -> v -> MonoMap k v -> MonoMap k v+ default insertWith :: (MonoMap k v ~ POMap k v, PartialOrd k) => (v -> v -> v) -> k -> v -> MonoMap k v -> MonoMap k v+ insertWith = POMap.insertWith+ insertLookupWithKey :: (k -> v -> v -> v) -> k -> v -> MonoMap k v -> (Maybe v, MonoMap k v)+ default insertLookupWithKey :: (MonoMap k v ~ POMap k v, PartialOrd k) => (k -> v -> v -> v) -> k -> v -> MonoMap k v -> (Maybe v, MonoMap k v)+ insertLookupWithKey = POMap.insertLookupWithKey+ updateLookupWithKey :: (k -> v -> Maybe v) -> k -> MonoMap k v -> (Maybe v, MonoMap k v)+ default updateLookupWithKey :: (MonoMap k v ~ POMap k v, PartialOrd k) => (k -> v -> Maybe v) -> k -> MonoMap k v -> (Maybe v, MonoMap k v)+ updateLookupWithKey = POMap.updateLookupWithKey+ alter :: (Maybe v -> Maybe v) -> k -> MonoMap k v -> MonoMap k v+ default alter :: (MonoMap k v ~ POMap k v, PartialOrd k) => (Maybe v -> Maybe v) -> k -> MonoMap k v -> MonoMap k v+ alter = POMap.alter+ adjust :: (v -> v) -> k -> MonoMap k v -> MonoMap k v+ default adjust :: (MonoMap k v ~ POMap k v, PartialOrd k) => (v -> v) -> k -> MonoMap k v -> MonoMap k v+ adjust = POMap.adjust++-- | Delegates to 'Maybe'.+instance MonoMapKey () where+ type MonoMap () = Maybe+ empty = Nothing+ singleton _ = Just+ insert _ v _ = Just v+ delete _ _ = Nothing+ lookup _ m = m+ lookupLT _ = fmap ((,) ()) . maybeToList+ lookupMin = lookupLT ()+ difference _ (Just _) = Nothing+ difference a _ = a+ keys _ = [()]+ insertWith _ _ v Nothing = Just v+ insertWith f _ v (Just old) = Just (f v old)+ insertLookupWithKey _ _ v Nothing = (Nothing, Just v)+ insertLookupWithKey f _ v (Just old) = (Just old, Just (f () v old))+ updateLookupWithKey _ _ Nothing = (Nothing, Nothing)+ updateLookupWithKey f _ (Just old) = (Just old, f () old)+ alter f _ = f+ adjust f _ = fmap f++-- | Delegates to 'IntMap'.+instance MonoMapKey Int where+ type MonoMap Int = IntMap+ empty = IntMap.empty+ singleton = IntMap.singleton+ insert = IntMap.insert+ delete = IntMap.delete+ lookup = IntMap.lookup+ lookupLT k = maybeToList . IntMap.lookupLT k+ lookupMin = maybeToList . fmap fst . IntMap.minViewWithKey+ difference = IntMap.difference+ keys = IntMap.keys+ insertWith = IntMap.insertWith+ insertLookupWithKey = IntMap.insertLookupWithKey+ updateLookupWithKey = IntMap.updateLookupWithKey+ alter = IntMap.alter+ adjust = IntMap.adjust
+ src/Datafix/NodeAllocator.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- |+-- Module : Datafix.NodeAllocator+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Helpers for allocating 'Node's in an ergonomic manner, e.g.+-- taking care to get 'mfix' right under the hood for allocation+-- in recursive bindings groups through the key primitive 'allocateNode'.++module Datafix.NodeAllocator+ ( NodeAllocator+ , allocateNode+ , runAllocator+ ) where++import Control.Monad.Fix (mfix)+import Control.Monad.Primitive+import Control.Monad.Trans.Class+import Control.Monad.Trans.State.Strict+import Data.Primitive.Array+import Datafix.Description+import Datafix.Utils.GrowableVector (GrowableVector)+import qualified Datafix.Utils.GrowableVector as GV+import System.IO.Unsafe (unsafePerformIO)++-- | A state monad wrapping a mapping from 'Node' to some 'v'+-- which we will instantiate to appropriate 'LiftedFunc's.+newtype NodeAllocator v a+ = NodeAllocator { unwrapNodeAllocator :: StateT (GrowableVector (PrimState IO) v) IO a }+ deriving (Functor, Applicative, Monad)++-- | Allocates the next 'Node', which is greater than any+-- nodes requested before.+--+-- The value stored at that node is the result of a 'NodeAllocator'+-- computation which may already access the 'Node' associated+-- with that value. This is important for the case of recursive+-- let, where the denotation of an expression depends on itself.+allocateNode :: (Node -> NodeAllocator v (a, v)) -> NodeAllocator v a+allocateNode f = NodeAllocator $ do+ node <- gets GV.length+ (result, _) <- mfix $ \ ~(_, entry) -> do+ vec <- get+ lift (GV.pushBack vec entry) >>= put+ unwrapNodeAllocator (f (Node node))+ return result+{-# INLINE allocateNode #-}++-- | Runs the allocator, beginning with an empty mapping.+runAllocator :: NodeAllocator v a -> (a, Array v)+runAllocator (NodeAllocator alloc) = unsafePerformIO $ do+ vec <- GV.new 8+ (a, vec') <- runStateT alloc vec+ vec'' <- GV.freeze vec'+ return (a, vec'')+{-# INLINE runAllocator #-}
+ src/Datafix/ProblemBuilder.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++-- |+-- Module : Datafix.ProblemBuilder+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Offers an instance for 'MonadDatafix' based on 'NodeAllocator'.++module Datafix.ProblemBuilder+ ( ProblemBuilder+ , buildProblem+ ) where++import Data.Primitive.Array+import Datafix.Description+import Datafix.NodeAllocator+import Datafix.Utils.TypeLevel++-- | Constructs a build plan for a 'DataFlowProblem' by tracking allocation of+-- 'Node's mapping to 'ChangeDetector's and transfer functions.+newtype ProblemBuilder m a+ = ProblemBuilder { unwrapProblemBuilder :: NodeAllocator (ChangeDetector (Domain m), LiftedFunc (Domain m) m) a }+ deriving (Functor, Applicative, Monad)++instance MonadDependency m => MonadDatafix m (ProblemBuilder m) where+ datafix cd func = ProblemBuilder $ allocateNode $ \node -> do+ let deref = dependOn @m node+ (ret, transfer) <- unwrapProblemBuilder (func deref)+ return (ret, (cd, transfer))++-- | @(root, max, dfp) = buildProblem builder@ executes the build plan specified+-- by @builder@ and returns the resulting 'DataFlowProblem' @dfp@, as well as+-- the @root@ 'Node' denoting the transfer function returned by the+-- 'ProblemBuilder' action and the @max@imum node of the problem as a proof for+-- its denseness.+buildProblem+ :: forall m+ . MonadDependency m+ => Currying (ParamTypes (Domain m)) (ReturnType (Domain m) -> ReturnType (Domain m) -> Bool)+ => ProblemBuilder m (LiftedFunc (Domain m) 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))
+ src/Datafix/Tutorial.hs view
@@ -0,0 +1,270 @@+{-# OPTIONS_GHC -fno-warn-unused-imports #-}++-- |+-- Module : Datafix.Tutorial+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- = What is This?+--+-- The purpose of @datafix@ is to separate declaring+-- [data-flow problems](https://en.wikipedia.org/wiki/Data-flow_analysis)+-- from computing their solutions by+-- [fixed-point iteration](https://en.wikipedia.org/wiki/Fixed-point_iteration).+--+-- The need for this library arose when I was combining two analyses+-- within GHC for my master's thesis. I recently+-- [held a talk](https://cdn.rawgit.com/sgraf812/hiw17/2645b206d3f2b5e6e7c95bc791dfa4bf9cbc8d12/slides.pdf)+-- on that topic, feel free to click through if you want to know the details.+--+-- You can think of data-flow problems as problems that are solvable by+-- [dynamic programming](https://en.wikipedia.org/wiki/Dynamic_programming)+-- or [memoization](https://en.wikipedia.org/wiki/Memoization),+-- except that the dependency graph of data-flow problems doesn't need to be+-- acyclic.+--+-- Data-flow problems are declared with the primitives in+-- @"Datafix.Description"@ and solved by @Datafix.Worklist.'solveProblem'@.+--+-- With that out of the way, let's set in place the GHCi environment of our+-- examples:+--+-- >>> :set -XScopedTypeVariables+-- >>> :set -XTypeApplications+-- >>> :set -XTypeFamilies+-- >>> import Datafix+-- >>> import Data.Proxy (Proxy (..))+-- >>> import Algebra.Lattice (JoinSemiLattice (..), BoundedJoinSemiLattice (..))+-- >>> import Numeric.Natural+--+-- = Use Case: Solving Recurrences+--+-- Let's start out by computing the fibonacci series:+--+-- >>> :{+-- fib :: Natural -> Natural+-- fib 0 = 0+-- fib 1 = 1+-- fib n = fib (n-1) + fib (n-2)+-- :}+--+-- >>> fib 3+-- 2+-- >>> fib 10+-- 55+--+-- Bring your rabbits to the vet while you can still count them...+--+-- Anyway, the fibonacci series is a typical problem exhibiting+-- /overlapping subproblems/. As a result, our @fib@ function from above scales badly in+-- the size of its input argument @n@. Because we repeatedly recompute+-- solutions, the time complexity of our above function is in \(\mathcal{O}(2^n)\)!+--+-- We can do better by using /dynamic programming/ or /memoization/ to keep a+-- cache of already computed sub-problems, which helps computing the \(n\)th+-- item in \(\mathcal{O}(n)\) time and space:+--+-- >>> :{+-- fib2 :: Natural -> Natural+-- fib2 n = fibs !! fromIntegral n+-- where+-- fibs = 0 : 1 : zipWith (+) fibs (tail fibs)+-- :}+--+-- >>> fib2 3+-- 2+-- >>> fib2 10+-- 55+--+-- That's one of Haskell's pet issues: Expressing dynamic programs as lists+-- through laziness.+--+-- As promised in the previous section, we can do the same using @datafix@.+-- First, we need to declare a /transfer function/ that makes the data+-- dependencies for the recursive case explicit, as if we were using+-- 'Data.Function.fix' to eliminate the recursion:+--+-- >>> :{+-- transferFib+-- :: forall m+-- . (MonadDependency m, Domain m ~ Natural)+-- => Node+-- -> LiftedFunc Natural m+-- transferFib (Node 0) = return 0+-- transferFib (Node 1) = return 1+-- transferFib (Node n) = do+-- a <- dependOn @m (Node (n-1))+-- b <- dependOn @m (Node (n-2))+-- return (a + b)+-- :}+--+-- 'MonadDependency' contains a single primitive 'dependOn' for that purpose.+--+-- Every point of the fibonacci series is modeled as a seperate 'Node' of the+-- data-flow graph.+-- By looking at the definition of 'LiftedFunc', we can see that+-- @LiftedFunc Natural m ~ m Natural@, so for our simple+-- 'Natural' 'Domain', the transfer function is specified directly in+-- 'MonadDependency'.+--+-- Note that indeed we eliminated explicit recursion in @transferFib@.+-- This allows the solution algorithm to track and discover dependencies+-- of the transfer function as it is executed!+--+-- With our transfer function (which denotes data-flow nodes in the semantics+-- of 'Natural's) in place, we can construct a 'DataFlowProblem':+--+-- >>> :{+-- fibDfp :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+-- fibDfp = DFP transferFib (const (eqChangeDetector @(Domain m)))+-- :}+--+-- The 'eqChangeDetector' is important for cyclic dependency graphs and makes+-- sure we detect when a fixed-point has been reached.+--+-- That's it for describing the data-flow problem of fibonacci numbers.+-- We can ask @Datafix.Worklist.'solveProblem'@ for a solution in a minute.+--+-- The 'solveProblem' solver demands an instance of 'BoundedJoinSemiLattice'+-- on the 'Domain' for when the data-flow graph is cyclic. We conveniently+-- delegate to the total @Ord@ instance for 'Numeric.Natural.Natural', knowing+-- that its semantic interpretation is irrelevant to us:+--+-- >>> instance JoinSemiLattice Natural where (\/) = max+-- >>> instance BoundedJoinSemiLattice Natural where bottom = 0+--+-- And now the final incantation of the solver:+--+-- >>> solveProblem fibDfp Sparse NeverAbort (Node 10)+-- 55+--+-- This will also execute in \(\mathcal{O}(n)\) space and time, all without+-- worrying about a smart solution strategy involving how to tie knots or+-- allocate vectors.+-- Granted, this doesn't really pay off for simple problems like computing+-- fibonacci numbers because of the boilerplate involved and the somewhat+-- devious type-level story, but the intended use case is that of static+-- analysis of programming languages.+--+-- Before I delegate you to a blog post about strictness analysis,+-- we will look at a more devious reccurence relation with actual+-- cycles in the resulting data-flow graph.+--+-- = Use Case: Solving Cyclic Recurrences+--+-- The recurrence relation describing fibonacci numbers admits a clear+-- plan of how to compute a solution, because the dependency graph is+-- obviously acyclic: To compute the next new value of the sequence,+-- only the prior two values are needed.+--+-- This is not true of the following reccurence relation:+--+-- \[+-- f(n) = \begin{cases}+-- 2 \cdot f(\frac{n}{2}), & n \text{ even}\\+-- f(n+1)-1, & n \text{ odd}+-- \end{cases}+-- \]+--+-- The identity function is the only solution to this, but it is unclear+-- how we could arrive at that conclusion just by translating that relation+-- into Haskell:+--+-- >>> :{+-- f n+-- | even n = 2 * f (n `div` 2)+-- | odd n = f (n + 1) - 1+-- :}+--+-- Imagine a call @f 1@: This will call @f 2@ recursively, which again+-- will call @f 1@. We hit a cyclic dependency!+--+-- Fortunately, we can use @datafix@ to compute the solution by fixed-point+-- iteration (which assumes monotonicity of the function to approximate):+--+-- >>> :{+-- transferF+-- :: forall m+-- . (MonadDependency m, Domain m ~ Int)+-- => Node+-- -> LiftedFunc Int m+-- transferF (Node n)+-- | even n = (* 2) <$> dependOn @m (Node (n `div` 2))+-- | odd n = (subtract 1) <$> dependOn @m (Node (n + 1))+-- :}+--+-- >>> :{+-- fDfp :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m+-- fDfp = DFP transferF (const (eqChangeDetector @(Domain m)))+-- :}+--+-- Specification of the data-flow problem works the same as for the 'fib'+-- function.+--+-- As for 'Natural', we need an instance of 'BoundedJoinSemiLattice'+-- for 'Int' to compute a solution:+--+-- >>> instance JoinSemiLattice Int where (\/) = max+-- >>> instance BoundedJoinSemiLattice Int where bottom = minBound+--+-- Now it's just a matter of calling 'solveProblem' with the right parameters:+--+-- >>> solveProblem fDfp Sparse NeverAbort (Node 0)+-- 0+-- >>> solveProblem fDfp Sparse NeverAbort (Node 5)+-- 5+-- >>> solveProblem fDfp Sparse NeverAbort (Node 42)+-- 42+-- >>> solveProblem fDfp Sparse NeverAbort (Node (-10))+-- -10+--+-- Note how the /specification/ of the data-flow problem was as unexciting as+-- it was for the fibonacci sequence (modulo boilerplate), yet the recurrence+-- we solved was pretty complicated already.+--+-- Of course, encoding the identity function this way is inefficient.+-- But keep in mind that in general, we don't know the solution to a particular+-- recurrence! It's always possible to solve the recurrence by hand upfront,+-- but that's trading precious developer time for what might be a throw-away+-- problem anyway.+--+-- Which brings us to the prime and final use case...+--+-- = Use Case: Static Analysis+--+-- Recurrence equations occur /all the time/ in denotational+-- semantics and static data-flow analysis.+--+-- For every invocation of the compiler, for every module, for every analysis+-- within the compiler, a recurrence relation representing program semantics+-- is to be solved. Naturally, we can't task a human with solving a bunch of+-- complicated recurrences everytime we hit compile.+--+-- In the imperative world, it's common-place to have some kind of fixed-point+-- iteration framework carry out the iteration of the data-flow graph, but+-- I could not find a similar abstraction for functional programming languages+-- yet. Analyses for functional languages are typically carried out as iterated+-- traversals of the syntax tree, but that is unsatisfying for a number of+-- reasons:+--+-- 1. Solution logic of the data-flow problem is intertwined with its+-- specification.+-- 2. Solution logic is duplicated among multiple analyses, violating DRY.+-- 3. A consequence of the last two points is that performance tweaks+-- have to be adapted for every analysis separately.+-- In the case of GHC's Demand Analyser, going from chaotic iteration+-- (which corresponds to naive iterated tree traversals) to an iteration+-- scheme that caches results of inner let-bindings, annotations to the+-- syntax tree are suddenly used like 'State' threads, which makes+-- the analysis logic even more complex than it already was.+--+-- So, I can only encourage any compiler dev who wants to integrate static+-- analyses into their compiler to properly specify the data-flow problems+-- in terms of @datafix@ and leave the intricacies of finding a good iteration+-- order to this library :)++module Datafix.Tutorial () where++import Datafix
+ src/Datafix/Utils/GrowableVector.hs view
@@ -0,0 +1,68 @@+-- |+-- Module : Datafix.GrowableVector+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Internal module, does not follow the PVP. Breaking changes may happen at+-- any minor version.++module Datafix.Utils.GrowableVector+ ( GrowableVector+ , new+ , length+ , pushBack+ , write+ , freeze+ ) where++import Control.Monad.Primitive+import Data.Primitive.Array+import Prelude hiding (length)++data GrowableVector s v+ = GrowableVector+ { buffer :: !(MutableArray s v)+ , len :: !Int+ }++notInitializedError :: a+notInitializedError = error "newGrowableVector: Accessed uninitialized value"++new :: PrimMonad m => Int -> m (GrowableVector (PrimState m) v)+new c =+ GrowableVector <$> newArray c notInitializedError <*> pure 0+{-# INLINE new #-}++capacity :: GrowableVector s v -> Int+capacity = sizeofMutableArray . buffer+{-# INLINE capacity #-}++length :: GrowableVector s v -> Int+length = len+{-# INLINE length #-}++grow :: PrimMonad m => GrowableVector (PrimState m) v -> Int -> m (GrowableVector (PrimState m) v)+grow vec n = do+ arr <- newArray (capacity vec + n) notInitializedError+ copyMutableArray arr 0 (buffer vec) 0 (len vec)+ return (GrowableVector arr (len vec))+{-# INLINE grow #-}++pushBack :: PrimMonad m => GrowableVector (PrimState m) v -> v -> m (GrowableVector (PrimState m) v)+pushBack vec v = do+ vec' <- if length vec == capacity vec+ then grow vec (max 1 (capacity vec))+ else return vec+ writeArray (buffer vec') (len vec') v+ return vec' { len = len vec' + 1 }+{-# INLINE pushBack #-}++write :: PrimMonad m => GrowableVector (PrimState m) v -> Int -> v -> m ()+write = writeArray . buffer+{-# INLINE write #-}++freeze :: PrimMonad m => GrowableVector (PrimState m) v -> m (Array v)+freeze vec = freezeArray (buffer vec) 0 (len vec)+{-# INLINE freeze #-}
+ src/Datafix/Utils/TypeLevel.hs view
@@ -0,0 +1,164 @@+-- This is literally+-- https://github.com/agda/agda/blob/0aff32aa29652db1a7026f81bc57dc15d5930124/src/full/Agda/Utils/TypeLevel.hs+-- with some default-extensions added.+-- Let's just hope that they don't sue ;)++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+-- We need undecidable instances for the definition of @Foldr@,+-- and @ParamTypes@ and @ReturnType@ using @If@ for instance.+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Datafix.Utils.TypeLevel+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Some type-level helpers for 'curry'/'uncurry'ing arbitrary function types.+module Datafix.Utils.TypeLevel where++import Data.Type.Equality+import GHC.Exts (Constraint)+import Unsafe.Coerce (unsafeCoerce)++------------------------------------------------------------------+-- CONSTRAINTS+------------------------------------------------------------------++-- | @All p as@ ensures that the constraint @p@ is satisfied by+-- all the 'types' in @as@.+-- (Types is between scare-quotes here because the code is+-- actually kind polymorphic)++type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where+ All p '[] = ()+ All p (a ': as) = (p a, All p as)++------------------------------------------------------------------+-- FUNCTIONS+-- Type-level and Kind polymorphic versions of usual value-level+-- functions.+------------------------------------------------------------------++-- | On Booleans+type family If (b :: Bool) (l :: k) (r :: k) :: k where+ If 'True l r = l+ If 'False l r = r++-- | On Lists+type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where+ Foldr c n '[] = n+ Foldr c n (a ': as) = c a (Foldr c n as)++-- | Version of @Foldr@ taking a defunctionalised argument so+-- that we can use partially applied functions.+type family Foldr' (c :: Function k (Function l l -> *) -> *)+ (n :: l) (as :: [k]) :: l where+ Foldr' c n '[] = n+ Foldr' c n (a ': as) = Apply (Apply c a) (Foldr' c n as)++type family Map (f :: Function k l -> *) (as :: [k]) :: [l] where+ Map f as = Foldr' (ConsMap0 f) '[] as++data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *+data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *+type instance Apply (ConsMap0 f) a = ConsMap1 f a+type instance Apply (ConsMap1 f a) tl = Apply f a ': tl++type family Constant (b :: l) (as :: [k]) :: [l] where+ Constant b as = Map (Constant1 b) as++------------------------------------------------------------------+-- TYPE FORMERS+------------------------------------------------------------------++-- | @Arrows [a1,..,an] r@ corresponds to @a1 -> .. -> an -> r@+type Arrows (as :: [*]) (r :: *) = Foldr (->) r as++arrowsAxiom :: Arrows (ParamTypes func) (ReturnType func) :~: func+arrowsAxiom = unsafeCoerce Refl++-- | @Products []@ corresponds to @()@,+-- @Products [a]@ corresponds to @a@,+-- @Products [a1,..,an]@ corresponds to @(a1, (..,( an)..))@.+--+-- So, not quite a right fold, because we want to optimize for the+-- empty, singleton and pair case.+type family Products (as :: [*]) where+ Products '[] = ()+ Products '[a] = a+ Products (a ': as) = (a, Products as)++-- | @IsBase t@ is @'True@ whenever @t@ is *not* a function space.++type family IsBase (t :: *) :: Bool where+ IsBase (a -> t) = 'False+ IsBase a = 'True++-- | Using @IsBase@ we can define notions of @ParamTypes@ and @ReturnTypes@+-- which *reduce* under positive information @IsBase t ~ 'True@ even+-- though the shape of @t@ is not formally exposed++type family ParamTypes (t :: *) :: [*] where+ ParamTypes t = If (IsBase t) '[] (ParamTypes' t)+type family ParamTypes' (t :: *) :: [*] where+ ParamTypes' (a -> t) = a ': ParamTypes t++type family ReturnType (t :: *) :: * where+ ReturnType t = If (IsBase t) t (ReturnType' t)+type family ReturnType' (t :: *) :: * where+ ReturnType' (a -> t) = ReturnType t++------------------------------------------------------------------+-- TYPECLASS MAGIC+------------------------------------------------------------------++-- | @Currying as b@ witnesses the isomorphism between @Arrows as b@+-- and @Products as -> b@. It is defined as a type class rather+-- than by recursion on a singleton for @as@ so all of that these+-- conversions are inlined at compile time for concrete arguments.++class Currying as b where+ uncurrys :: Arrows as b -> Products as -> b+ currys :: (Products as -> b) -> Arrows as b++instance Currying '[] b where+ uncurrys f () = f+ currys f = f ()++instance Currying (a ': '[]) b where+ uncurrys f = f+ currys f = f++instance Currying (a2 ': as) b => Currying (a1 ': a2 ': as) b where+ uncurrys f = uncurry $ uncurrys @(a2 ': as) . f+ currys f = currys @(a2 ': as) . curry f++------------------------------------------------------------------+-- DEFUNCTIONALISATION+-- Cf. Eisenberg and Stolarek's paper:+-- Promoting Functions to Type Families in Haskell+------------------------------------------------------------------++data Function :: * -> * -> *++data Constant0 :: Function a (Function b a -> *) -> *+data Constant1 :: * -> Function b a -> *++type family Apply (t :: Function k l -> *) (u :: k) :: l++type instance Apply Constant0 a = Constant1 a+type instance Apply (Constant1 a) b = a
+ src/Datafix/Worklist.hs view
@@ -0,0 +1,20 @@+-- |+-- Module : Datafix.Worklist+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- This module provides the 'Impl.solveProblem' function, which solves the description of a+-- 'Datafix.Description.DataFlowProblem' by employing a worklist algorithm.++module Datafix.Worklist+ ( Impl.DependencyM+ , Impl.Datafixable+ , Impl.Density (..)+ , Impl.IterationBound (..)+ , Impl.solveProblem+ , Impl.evalDenotation+ ) where++import qualified Datafix.Worklist.Internal as Impl
+ src/Datafix/Worklist/Graph.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Datafix.Worklist.Graph+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Abstracts over the representation of the data-flow graph.+--+-- The contents of this module are more or less internal to the+-- "Datafix.Worklist" implementation.++module Datafix.Worklist.Graph where++import Control.Monad.Trans.Reader+import Datafix.IntArgsMonoSet (IntArgsMonoSet)+import qualified Datafix.IntArgsMonoSet as IntArgsMonoSet+import Datafix.MonoMap (MonoMapKey)+import Datafix.Utils.TypeLevel++-- | The data associated with each point in the transfer function of a data-flow+-- 'Node'.+data PointInfo domain+ = PointInfo+ { value :: !(Maybe (ReturnType domain))+ -- ^ The value at this point. Can be 'Nothing' only when a loop was detected.+ , references :: !(IntArgsMonoSet (Products (ParamTypes domain)))+ -- ^ Points this point of the transfer function depends on.+ , referrers :: !(IntArgsMonoSet (Products (ParamTypes domain)))+ -- ^ Points depending on this point.+ , iterations :: !Int+ -- ^ The number of times this point has been updated through calls to+ -- 'updateNodeValue'.+ }++deriving instance (Eq (ReturnType domain), Eq (IntArgsMonoSet (Products (ParamTypes domain)))) => Eq (PointInfo domain)+deriving instance (Show (ReturnType domain), Show (IntArgsMonoSet (Products (ParamTypes domain)))) => Show (PointInfo domain)++-- | The default 'PointInfo'.+emptyPointInfo :: PointInfo domain+emptyPointInfo = PointInfo Nothing IntArgsMonoSet.empty IntArgsMonoSet.empty 0+{-# INLINE emptyPointInfo #-}++-- | Diff between two 'IntArgsMonoSet's.+data Diff a+ = Diff+ { added :: !(IntArgsMonoSet a)+ , removed :: !(IntArgsMonoSet a)+ }++-- | Computes the diff between two 'IntArgsMonoSet's.+computeDiff :: MonoMapKey k => IntArgsMonoSet k -> IntArgsMonoSet k -> Diff k+computeDiff a b =+ Diff (IntArgsMonoSet.difference b a) (IntArgsMonoSet.difference a b)++-- | Abstracts over the concrete representation of the data-flow graph.+--+-- There are two instances: The default 'Datafix.Graph.Sparse.Ref'+-- for sparse graphs based on an 'IntMap' and 'Datafix.Graph.Dense.Ref' for+-- the dense case, storing the 'Node' mapping in a 'Data.IOVector'.+class GraphRef (ref :: * -> *) where+ updatePoint :: MonoMapKey (Products (ParamTypes domain)) => Int -> Products (ParamTypes domain) -> ReturnType domain -> IntArgsMonoSet (Products (ParamTypes domain)) -> ReaderT (ref domain) IO (PointInfo domain)+ lookup :: MonoMapKey (Products (ParamTypes domain)) => Int -> Products (ParamTypes domain) -> ReaderT (ref domain) IO (Maybe (PointInfo domain))+ lookupLT :: MonoMapKey (Products (ParamTypes domain)) => Int -> Products (ParamTypes domain) -> ReaderT (ref domain) IO [(Products (ParamTypes domain), PointInfo domain)]
+ src/Datafix/Worklist/Graph/Dense.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-}++-- |+-- Module : Datafix.Worklist.Graph+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Dense data-flow graph representation based on 'Data.IOVector'.++module Datafix.Worklist.Graph.Dense+ ( Ref+ , newRef+ ) where++import Control.Monad (forM_)+import Control.Monad.Trans.Class+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State.Strict+import Data.Maybe (fromMaybe)+import Data.Vector.Mutable (IOVector)+import qualified Data.Vector.Mutable as V+import qualified Datafix.IntArgsMonoSet as IntArgsMonoSet+import Datafix.MonoMap (MonoMap, MonoMapKey)+import qualified Datafix.MonoMap as MonoMap+import Datafix.Utils.TypeLevel+import Datafix.Worklist.Graph++-- | Models the points of a transfer function of a single+-- data-flow 'Node'.+type PointMap domain+ = MonoMap (Products (ParamTypes domain)) (PointInfo domain)++-- | Reference to a dense data-flow graph representation.+newtype Ref domain+ = Ref (IOVector (PointMap domain))++-- | Allocates a new dense graph 'Ref'.+newRef :: MonoMapKey (Products (ParamTypes domain)) => Int -> IO (Ref domain)+newRef size = Ref <$> V.replicate size MonoMap.empty++zoomNode :: Int -> State (PointMap domain) a -> ReaderT (Ref domain) IO a+zoomNode node s = do+ Ref graph <- ask+ points <- lift (V.read graph node)+ let (ret, points') = runState s points+ points' `seq` lift (V.write graph node points')+ return ret+{-# INLINE zoomNode #-}++instance GraphRef Ref where+ updatePoint node args val refs = do+ -- if we are lucky (e.g. no refs changed), we get away with one map access+ -- first update `node`s PointInfo+ let freshInfo = emptyPointInfo+ { value = Just val+ , references = refs+ , iterations = 1+ }+ let merger _ new old = new+ { referrers = referrers old+ , iterations = iterations old + 1+ }++ oldInfo <- fmap (fromMaybe emptyPointInfo) $ zoomNode node $ state $+ MonoMap.insertLookupWithKey merger args freshInfo++ -- Now compute the diff of changed references+ let diff = computeDiff (references oldInfo) refs++ -- finally register/unregister at all references as referrer.+ let updater f (depNode, depArgs) = zoomNode depNode $ modify' $+ MonoMap.insertWith (const f) depArgs (f emptyPointInfo)+ let addReferrer ni = ni { referrers = IntArgsMonoSet.insert node args (referrers ni) }+ let removeReferrer ni = ni { referrers = IntArgsMonoSet.delete node args (referrers ni) }+ forM_ (IntArgsMonoSet.toList (added diff)) (updater addReferrer)+ forM_ (IntArgsMonoSet.toList (removed diff)) (updater removeReferrer)++ return oldInfo+ {-# INLINE updatePoint #-}++ lookup node args = ReaderT $ \(Ref graph) ->+ MonoMap.lookup args <$> V.read graph node+ {-# INLINE lookup #-}++ lookupLT node args = ReaderT $ \(Ref graph) ->+ MonoMap.lookupLT args <$> V.read graph node+ {-# INLINE lookupLT #-}
+ src/Datafix/Worklist/Graph/Sparse.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-}++-- |+-- Module : Datafix.Worklist.Graph+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Sparse data-flow graph representation based on 'Data.IntMap.Strict.IntMap'.++module Datafix.Worklist.Graph.Sparse+ ( Ref+ , newRef+ ) where++import Control.Monad (forM_)+import Control.Monad.Trans.Class+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State.Strict+import Data.IORef+import Data.Maybe (fromMaybe)+import Datafix.IntArgsMonoMap (IntArgsMonoMap)+import qualified Datafix.IntArgsMonoMap as IntArgsMonoMap+import qualified Datafix.IntArgsMonoSet as IntArgsMonoSet+import Datafix.Utils.TypeLevel+import Datafix.Worklist.Graph++-- | Models a data-flow graph as a map from 'Node's to+-- associated points of their transfer function.+type Graph domain+ = IntArgsMonoMap (Products (ParamTypes domain)) (PointInfo domain)++-- | Reference to a sparse data-flow graph representation.+newtype Ref domain =+ Ref (IORef (Graph domain))++-- | Allocates a new sparse graph 'Ref'.+newRef :: IO (Ref domain)+newRef = Ref <$> newIORef IntArgsMonoMap.empty++fromState :: State (Graph domain) a -> ReaderT (Ref domain) IO a+fromState st = do+ Ref ref <- ask+ g <- lift (readIORef ref)+ let (a, g') = runState st g+ g' `seq` lift (writeIORef ref g')+ pure a+{-# INLINE fromState #-}++instance GraphRef Ref where+ updatePoint node args val refs = fromState $ do+ -- if we are lucky (e.g. no refs changed), we get away with one map access+ -- first update 'node's PointInfo+ let freshInfo = emptyPointInfo+ { value = Just val+ , references = refs+ , iterations = 1+ }+ let merger _ _ new old = new+ { referrers = referrers old+ , iterations = iterations old + 1+ }+ oldInfo <- fromMaybe emptyPointInfo <$>+ state (IntArgsMonoMap.insertLookupWithKey merger node args freshInfo)++ -- Now compute the diff of changed references+ let diff = computeDiff (references oldInfo) refs++ -- finally register/unregister at all references as referrer.+ let updater f (depNode, depArgs) = modify' $+ IntArgsMonoMap.insertWith (const f) depNode depArgs (f emptyPointInfo)+ let addReferrer ni = ni { referrers = IntArgsMonoSet.insert node args (referrers ni) }+ let removeReferrer ni = ni { referrers = IntArgsMonoSet.delete node args (referrers ni) }+ forM_ (IntArgsMonoSet.toList (added diff)) (updater addReferrer)+ forM_ (IntArgsMonoSet.toList (removed diff)) (updater removeReferrer)++ return oldInfo+ {-# INLINE updatePoint #-}++ lookup node args = do+ Ref ref <- ask+ IntArgsMonoMap.lookup node args <$> lift (readIORef ref)+ {-# INLINE lookup #-}++ lookupLT node args = do+ Ref ref <- ask+ IntArgsMonoMap.lookupLT node args <$> lift (readIORef ref)+ {-# INLINE lookupLT #-}
+ src/Datafix/Worklist/Internal.hs view
@@ -0,0 +1,555 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Datafix.Worklist.Internal+-- Copyright : (c) Sebastian Graf 2018+-- License : ISC+-- Maintainer : sgraf1337@gmail.com+-- Portability : portable+--+-- Internal module, does not follow the PVP. Breaking changes may happen at+-- any minor version.++module Datafix.Worklist.Internal where++import Algebra.Lattice+import Control.Monad (forM_, guard, when)+import Control.Monad.Trans.Class+import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State.Strict+import Data.IORef+import Data.Maybe (fromMaybe, listToMaybe,+ mapMaybe)+import Data.Type.Equality+import Datafix.Description hiding (dependOn)+import qualified Datafix.Description+import Datafix.IntArgsMonoSet (IntArgsMonoSet)+import qualified Datafix.IntArgsMonoSet as IntArgsMonoSet+import Datafix.MonoMap (MonoMapKey)+import Datafix.ProblemBuilder+import Datafix.Utils.TypeLevel+import Datafix.Worklist.Graph (GraphRef, PointInfo (..))+import qualified Datafix.Worklist.Graph as Graph+import qualified Datafix.Worklist.Graph.Dense as DenseGraph+import qualified Datafix.Worklist.Graph.Sparse as SparseGraph+import System.IO.Unsafe (unsafePerformIO)++-- | The concrete 'MonadDependency' for this worklist-based solver.+--+-- This essentially tracks the current approximation of the solution to the+-- 'DataFlowProblem' as mutable state while 'solveProblem' makes sure we will eventually+-- halt with a conservative approximation.+newtype DependencyM graph domain a+ = DM (ReaderT (Env graph domain) IO a)+ -- ^ Why does this use 'IO'? Actually, we only need 'ST' here, but that+ -- means we have to carry around the state thread in type signatures.+ --+ -- 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)) -> ...@+ -- and have to instead have the isomorphic+ -- @(forall s r. (Datafixable (DependencyM s graph 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+ -- the type-checker that @s@ is universally quantified in everything that+ -- touches it, e.g. @Analyses.StrAnal.LetDn.buildProblem@ from the test suite.+ --+ -- So, bottom line: We resort to 'IO' and 'unsafePerformIO' and promise not to+ -- launch missiles. In particular, we don't export 'DM' and also there+ -- must never be an instance of 'MonadIO' for this.+ deriving (Functor, Applicative, Monad)++-- | The iteration state of 'DependencyM'/'solveProblem'.+data Env graph domain+ = Env+ { problem :: !(DataFlowProblem (DependencyM graph domain))+ -- ^ Constant.+ -- The specification of the data-flow problem we ought to solve.+ , iterationBound :: !(IterationBound domain)+ -- ^ Constant.+ -- Whether to abort after a number of iterations or not.+ , callStack :: !(IntArgsMonoSet (Products (ParamTypes domain)))+ -- ^ Contextual state.+ -- The set of points in the 'domain' of 'Node's currently in the call stack.+ , graph :: !(graph domain)+ -- ^ Constant ref to stateful graph.+ -- The data-flow graph, modeling dependencies between data-flow 'Node's,+ -- or rather specific points in the 'domain' of each 'Node'.+ , referencedPoints :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))+ -- ^ Constant (but the the wrapped set is stateful).+ -- The set of points the currently 'recompute'd node references so far.+ , unstable :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))+ -- ^ Constant (but the the wrapped queue is stateful).+ -- Unstable nodes that will be 'recompute'd by the 'work'list algorithm.+ }++initialEnv+ :: IntArgsMonoSet (Products (ParamTypes domain))+ -> DataFlowProblem (DependencyM graph domain)+ -> IterationBound domain+ -> IO (graph domain)+ -> IO (Env graph domain)+initialEnv unstable_ prob ib newGraphRef =+ Env prob ib IntArgsMonoSet.empty+ <$> newGraphRef+ <*> newIORef IntArgsMonoSet.empty+ <*> 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))+ )++-- | 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+ dependOn = dependOn @domain @graph+ {-# INLINE dependOn #-}++-- | Specifies the /density/ of the problem, e.g. whether the domain of+-- 'Node's can be confined to a finite range, in which case 'solveProblem'+-- tries to use a "Data.Vector" based graph representation rather than+-- one based on "Data.IntMap".+data Density graph where+ Sparse :: Density SparseGraph.Ref+ Dense :: Node -> Density DenseGraph.Ref++-- | A function that computes a sufficiently conservative approximation+-- of a point in the abstract domain for when the solution algorithm+-- decides to have iterated the node often enough.+--+-- When 'domain' is a 'BoundedMeetSemilattice'/'BoundedLattice', the+-- simplest abortion function would be to constantly return 'top'.+--+-- As is the case for 'LiftedFunc' and 'ChangeDetector', this+-- carries little semantic meaning if viewed in isolation, so here+-- are a few examples for how the synonym expands:+--+-- @+-- AbortionFunction Int ~ Int -> Int+-- AbortionFunction (String -> Int) ~ String -> Int -> Int+-- AbortionFunction (a -> b -> c -> PowerSet) ~ a -> b -> c -> PowerSet -> PowerSet+-- @+--+-- E.g., the current value of the point is passed in (the tuple @(a, b, c, PowerSet)@)+-- and the function returns an appropriate conservative approximation in that+-- point.+type AbortionFunction domain+ = Arrows (ParamTypes domain) (ReturnType domain -> ReturnType domain)++-- | Aborts iteration of a value by 'const'antly returning the 'top' element+-- of the assumed 'BoundedMeetSemiLattice' of the 'ReturnType'.+abortWithTop+ :: forall domain+ . Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain)+ => BoundedMeetSemiLattice (ReturnType domain)+ => AbortionFunction domain+abortWithTop =+ currys @(ParamTypes domain) @(ReturnType domain -> ReturnType domain) $+ const top+{-# INLINE abortWithTop #-}++-- | Expresses that iteration should or shouldn't stop after a point has+-- been iterated a finite number of times.+data IterationBound domain+ = NeverAbort+ -- ^ Will keep on iterating until a precise, yet conservative approximation+ -- has been reached. Make sure that your 'domain' satisfies the+ -- [ascending chain condition](https://en.wikipedia.org/wiki/Ascending_chain_condition),+ -- e.g. that fixed-point iteration always comes to a halt!+ | AbortAfter Int (AbortionFunction domain)+ -- ^ For when your 'domain' doesn't satisfy the ascending chain condition+ -- or when you are sensitive about solution performance.+ --+ -- The 'Int'eger determines the maximum number of iterations of a single point+ -- of a 'Node' (with which an entire function with many points may be associated)+ -- before iteration aborts in that point by calling the supplied 'AbortionFunction'.+ -- The responsibility of the 'AbortionFunction' is to find a sufficiently+ -- conservative approximation for the current value at that point.+ --+ -- When your 'ReturnType' is an instance of 'BoundedMeetSemiLattice',+ -- 'abortWithTop' might be a worthwhile option.+ -- A more sophisticated solution would trim the current value to a certain+ -- cut-off depth, depending on the first parameter, instead.++zoomIORef+ :: State s a+ -> ReaderT (IORef s) IO a+zoomIORef s = do+ ref <- ask+ uns <- lift $ readIORef ref+ let (res, uns') = runState s uns+ uns' `seq` lift $ writeIORef ref uns'+ return res+{-# INLINE zoomIORef #-}++zoomReferencedPoints+ :: State (IntArgsMonoSet (Products (ParamTypes domain))) a+ -> ReaderT (Env graph domain) IO a+zoomReferencedPoints = withReaderT referencedPoints . zoomIORef+{-# INLINE zoomReferencedPoints #-}++zoomUnstable+ :: State (IntArgsMonoSet (Products (ParamTypes domain))) a+ -> ReaderT (Env graph domain) IO a+zoomUnstable = withReaderT unstable . zoomIORef+{-# INLINE zoomUnstable #-}++enqueueUnstable+ :: k ~ Products (ParamTypes domain)+ => MonoMapKey k+ => Int -> k -> ReaderT (Env graph domain) IO ()+enqueueUnstable i k = zoomUnstable (modify' (IntArgsMonoSet.insert i k))+{-# INLINE enqueueUnstable #-}++deleteUnstable+ :: k ~ Products (ParamTypes domain)+ => MonoMapKey k+ => Int -> k -> ReaderT (Env graph domain) IO ()+deleteUnstable i k = zoomUnstable (modify' (IntArgsMonoSet.delete i k))+{-# INLINE deleteUnstable #-}++highestPriorityUnstableNode+ :: k ~ Products (ParamTypes domain)+ => MonoMapKey k+ => ReaderT (Env graph domain) IO (Maybe (Int, k))+highestPriorityUnstableNode = zoomUnstable $+ listToMaybe . IntArgsMonoSet.highestPriorityNodes <$> get+{-# INLINE highestPriorityUnstableNode #-}++withCall+ :: Datafixable (DependencyM graph domain)+ => Int+ -> Products (ParamTypes domain)+ -> ReaderT (Env graph domain) IO a+ -> ReaderT (Env graph domain) IO a+withCall node args r = ReaderT $ \env -> do+ refs <- readIORef (referencedPoints env)+ refs `seq` writeIORef (referencedPoints env) IntArgsMonoSet.empty+ ret <- runReaderT r env+ { callStack = IntArgsMonoSet.insert node args (callStack env)+ }+ writeIORef (referencedPoints env) refs+ return ret+{-# INLINE withCall #-}++-- | The first of the two major functions of this module.+--+-- @recompute node args@ iterates the value of the passed @node@+-- at the point @args@ by invoking its transfer function.+-- It does so in a way that respects the 'IterationBound'.+--+-- This function is not exported, and is only called by 'work'+-- and 'dependOn', for when the iteration strategy decides that+-- the @node@ needs to be (and can be) re-iterated.+-- It performs tracking of which 'Node's the transfer function+-- depended on, do that the worklist algorithm can do its magic.+recompute+ :: forall domain graph dom cod depm+ . dom ~ ParamTypes domain+ => cod ~ ReturnType domain+ => depm ~ DependencyM graph domain+ => GraphRef graph+ => Datafixable depm+ => 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+ let detectChange' = uncurrys @dom @(cod -> cod -> Bool) (dfpDetectChange prob node') args+ -- 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+ -- 2. directly after the call to 'iterate', to get the 'oldInfo'+ -- 3. And again to actually write the 'newInfo'+ --+ -- The last two can be merged, whereas it's crucial that 'oldInfo'+ -- is captured *after* the call to 'iterate', otherwise we might+ -- not pick up all 'referrers'.+ -- If abortion is required, 'maybeAbortedVal' will not be 'Nothing'.+ maybeAbortedVal <- runMaybeT $ do+ AbortAfter n abort <- lift (asks iterationBound)+ 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)+ -- 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+ -- 'refs' will be empty, thus the node will never be marked unstable again.+ refs <- asks referencedPoints >>= lift . readIORef+ oldInfo <- withReaderT graph (Graph.updatePoint node args newVal refs)+ deleteUnstable node args+ case value oldInfo of+ Just oldVal | not (detectChange' oldVal newVal) ->+ return ()+ _ -> do+ forM_ (IntArgsMonoSet.toList (referrers oldInfo)) $+ uncurry enqueueUnstable+ when (IntArgsMonoSet.member node args refs) $+ -- This is a little unfortunate: The 'oldInfo' will+ -- not have listed the current node itself as a refererrer+ -- in case of a loop, so we have to check for+ -- that case manually in the new 'references' set.+ -- The info stored in the graph has the right 'referrers'+ -- set, though.+ enqueueUnstable node args+ return newVal+{-# INLINE recompute #-}++dependOn+ :: forall domain graph+ . Datafixable (DependencyM graph 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+{-# INLINE dependOn #-}++-- | Compute an optimistic approximation for a point of a given node that is+-- as precise as possible, given the other points of that node we already+-- computed.+--+-- E.g., it is always valid to return 'bottom' from this, but in many cases+-- we can be more precise since we possibly have computed points for the node+-- that are lower bounds to the current point.+optimisticApproximation+ :: GraphRef graph+ => Datafixable (DependencyM graph domain)+ => Int -> Products (ParamTypes domain) -> ReaderT (Env graph domain) IO (ReturnType domain)+optimisticApproximation node args = do+ points <- withReaderT graph (Graph.lookupLT node args)+ -- Note that 'points' might contain 'PointInfo's that have no 'value'.+ -- It's OK to filter these out: At worst, the approximation will be+ -- more optimistic than necessary.+ return (joins (mapMaybe (value . snd) points))++scheme1, scheme2+ :: GraphRef graph+ => Datafixable (DependencyM graph domain)+ => Maybe (ReturnType domain)+ -> Int+ -> Products (ParamTypes domain)+ -> ReaderT (Env graph domain) IO (ReturnType domain)+{-# INLINE scheme1 #-}+{-# INLINE scheme2 #-}++-- | scheme 1 (see https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).+--+-- Let the worklist algorithm figure things out.+scheme1 maybeVal node args =+ case maybeVal of+ Nothing -> do+ enqueueUnstable node args+ optimisticApproximation node args+ Just val ->+ return val++-- | scheme 2 (see https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).+--+-- Descend into \(\bot\) nodes when there is no cycle to discover the set of+-- reachable nodes as quick as possible.+-- Do *not* descend into unstable, non-\(\bot\) nodes.+scheme2 maybeVal node args =+ case maybeVal of+ Nothing ->+ -- Depth-first discovery of reachable nodes+ recompute node args+ Just val ->+ -- It is unclear if this really is beneficial:+ -- We don't discover any new nodes and should rather+ -- rely on the ordering in the worklist.+ return val++-- There used to be a third scheme that is no longer possible with the current+-- mode of dependency tracking.+-- See https://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like++-- |As long as the supplied "Maybe" expression returns "Just _", the loop+-- body will be called and passed the value contained in the 'Just'. Results+-- are discarded.+--+-- Taken from 'Control.Monad.Loops.whileJust_'.+whileJust_ :: Monad m => m (Maybe a) -> (a -> m b) -> m ()+whileJust_ cond action = go+ where+ go = cond >>= \case+ Nothing -> return ()+ Just a -> action a >> go+{-# INLINE whileJust_ #-}++-- | Defined as 'work = whileJust_ highestPriorityUnstableNode (uncurry recompute)'.+--+-- Tries to dequeue the 'highestPriorityUnstableNode' and 'recompute's the value of+-- one of its 'unstable' points, until the worklist is empty, indicating that a+-- fixed-point has been reached.+work+ :: GraphRef graph+ => Datafixable (DependencyM graph domain)+ => ReaderT (Env graph domain) IO ()+work = whileJust_ highestPriorityUnstableNode (uncurry recompute)+{-# INLINE work #-}++-- | Computes a solution to the described 'DataFlowProblem' by iterating+-- transfer functions until a fixed-point is reached.+--+-- It does do by employing a worklist algorithm, iterating unstable 'Node's+-- only.+-- 'Node's become unstable when the point of another 'Node' their transfer function+-- 'dependOn'ed changed.+--+-- The sole initially unstable 'Node' is the last parameter, and if your+-- 'domain' is function-valued (so the returned 'Arrows' expands to a function),+-- then any further parameters specify the exact point in the 'Node's transfer+-- function you are interested in.+--+-- If your problem only has finitely many different 'Node's , consider using+-- the 'ProblemBuilder' API (e.g. 'datafix' + 'evalDenotation') for a higher-level API+-- that let's you forget about 'Node's and instead let's you focus on building+-- more complex data-flow frameworks.+solveProblem+ :: forall domain graph+ . GraphRef graph+ => Datafixable (DependencyM graph domain)+ => DataFlowProblem (DependencyM graph domain)+ -- ^ The description of the @DataFlowProblem@ to solve.+ -> Density graph+ -- ^ Describes if the algorithm is free to use a 'Dense', 'Vector'-based+ -- graph representation or has to go with a 'Sparse' one based on 'IntMap'.+ -> 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.+ -> Node+ -- ^ The @Node@ that is initially assumed to be unstable. This should be+ -- the @Node@ you are interested in, e.g. @Node 42@ if you are interested+ -- in the value of @fib 42@ for a hypothetical @fibProblem@, or the+ -- @Node@ denoting the root expression of your data-flow analysis+ -- you specified via the @DataFlowProblem@.+ -> domain+solveProblem prob density ib (Node node) =+ castWith arrowsAxiom (currys @(ParamTypes domain) @(ReturnType domain) impl)+ where+ impl+ = fromMaybe (error "Broken invariant: The root node has no value")+ . (>>= value)+ . runProblem+ runProblem args = unsafePerformIO $ do+ -- Trust me, I'm an engineer! See the docs of the 'DM' constructor+ -- of 'DependencyM' for why we 'unsafePerformIO'.+ let newGraphRef = case density of+ Sparse -> SparseGraph.newRef+ Dense (Node maxNode) -> DenseGraph.newRef (maxNode + 1)+ 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 #-}
+ stack.yaml view
@@ -0,0 +1,64 @@+# Resolver to choose a 'specific' stackage snapshot or a compiler version.+# A snapshot resolver dictates the compiler version and the set of packages+# to be used for project dependencies. For example:+#+# resolver: lts-3.5+# resolver: nightly-2015-09-21+# resolver: ghc-7.10.2+# resolver: ghcjs-0.1.0_ghc-7.10.2+# resolver:+# name: custom-snapshot+# location: "./custom-snapshot.yaml"+resolver: lts-10.2++# User packages to be built.+# Various formats can be used as shown in the example below.+#+# packages:+# - some-directory+# - https://example.com/foo/bar/baz-0.0.2.tar.gz+# - location:+# git: https://github.com/commercialhaskell/stack.git+# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a+# - location: https://github.com/commercialhaskell/stack/commit/e7b331f14bcffb8367cd58fbfc8b40ec7642100a+# extra-dep: true+# subdirs:+# - auto-update+# - wai+#+# A package marked 'extra-dep: true' will only be built if demanded by a+# non-dependency (i.e. a user package), and its test suites and benchmarks+# will not be run. This is useful for tweaking upstream packages.+packages:+- '.'++# Dependency packages to be pulled from upstream that are not in the resolver+# (e.g., acme-missiles-0.3)+extra-deps:+- pomaps-0.0.0.2++allow-newer: true++# Override default flag values for local packages and extra-deps+flags: {}++# Extra package databases containing global packages+extra-package-dbs: []++# Control whether we use the GHC we find on the path+# system-ghc: true+#+# Require a specific version of stack, using version ranges+# require-stack-version: -any # Default+# require-stack-version: ">=1.2"+#+# Override the architecture used by stack, especially useful on Windows+# arch: i386+# arch: x86_64+#+# Extra directories used by stack for building+# extra-include-dirs: [/path/to/dir]+# extra-lib-dirs: [/path/to/dir]+#+# Allow a newer minor version of GHC than the snapshot specifies+# compiler-check: newer-minor
+ tests/Critical.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Critical (tests) where++import Algebra.Lattice+import Datafix+import Datafix.Worklist (Density (..), IterationBound (..),+ solveProblem)+import Datafix.Worklist.Graph (GraphRef)+import Numeric.Natural+import Test.Tasty+import Test.Tasty.HUnit++instance JoinSemiLattice Natural where+ (\/) = max++instance BoundedJoinSemiLattice Natural where+ bottom = 0+++fixLoop, fixDoubleDependency+ :: GraphRef graph => (Node -> Density graph) -> Int -> Natural+fixLoop density n = solveProblem loopProblem (density (Node 0)) NeverAbort (Node n)+fixDoubleDependency density n = solveProblem doubleDependencyProblem (density (Node 1)) NeverAbort (Node n)++tests :: [TestTree]+tests =+ [ testGroup "One node with loop"+ [ testGroup "Sparse"+ [ testCase "stabilises at 10" (fixLoop (const Sparse) 0 @?= 10)+ ]+ , testGroup "Dense"+ [ testCase "stabilises at 10" (fixLoop Dense 0 @?= 10)+ ]+ ]+ , testGroup "One node with double dependency on node with loop"+ [ testGroup "Sparse"+ [ testCase "stabilizes at 4" (fixDoubleDependency (const Sparse) 0 @?= 4)+ ]+ , testGroup "Dense"+ [ testCase "stabilizes at 4" (fixDoubleDependency Dense 0 @?= 4)+ ]+ , testGroup "Abortion"+ [ testCase "stabilizes at or over 4" (assertBool ">= 4" $ solveProblem doubleDependencyProblem Sparse (AbortAfter 1 (+ 4)) (Node 0) >= 4)+ ]+ ]+ ]++mkDFP :: forall m . (Domain m ~ Natural) => (Node -> LiftedFunc Natural m) -> DataFlowProblem m+mkDFP transfer = DFP transfer (const (eqChangeDetector @(Domain m)))++-- | One node graph with loop that stabilizes after 10 iterations.+loopProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+loopProblem = mkDFP transfer+ where+ transfer (Node 0) = do -- stabilizes at 10+ n <- dependOn @m (Node 0)+ return (min (n + 1) 10)+ transfer (Node _) = error "Invalid node"++-- | Two node graph (nodes @A@, @B@), where @A@ `dependOn` @B@ twice and @B@+-- has a loop.+--+-- The idea here is that the second change of @B@ from 1 to 2 makes @A@+-- unstable, so that it gets iterated again, which results in a value of+-- 4 instead of e.g. 3 (= 1 + 2, the values of @B@ in the first iteration+-- of @A@).+doubleDependencyProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m+doubleDependencyProblem = mkDFP transfer+ where+ transfer (Node 0) = do -- stabilizes at 4+ n <- dependOn @m (Node 1)+ m <- dependOn @m (Node 1)+ return (n + m)+ transfer (Node 1) = do -- stabilizes at 2+ n <- dependOn @m (Node 1)+ return (min (n + 1) 2)+ transfer (Node _) = error "Invalid node"
+ tests/Main.hs view
@@ -0,0 +1,20 @@+import qualified Critical+import qualified StrAnal+import System.Environment+import Test.Tasty+import qualified Trivial++main :: IO ()+main = do+ -- Parallel tests get us in trouble because of+ -- locks on the package db in GHC 8.2.2+ setEnv "TASTY_NUM_THREADS" "1"+ defaultMain $ testGroup "All tests"+ [ testGroup "Unit test"+ [ testGroup "Trivial" Trivial.tests+ , testGroup "Critical cases" Critical.tests+ ]+ , testGroup "Analyses"+ [ testGroup "Strictness" StrAnal.tests+ ]+ ]
+ tests/StrAnal.hs view
@@ -0,0 +1,253 @@+module StrAnal where++import qualified Analyses.AdHocStrAnal as AdHocStrAnal+import qualified Analyses.StrAnal as StrAnal+import Analyses.StrAnal.Strictness+import Analyses.Syntax.MkCoreFromFile (compileCoreExpr)+import Analyses.Syntax.MkCoreHelpers++import Test.Tasty+import Test.Tasty.HUnit++import CoreSyn+import CoreTidy (tidyExpr)+import Id+import VarEnv (emptyTidyEnv)++x, x1, x2, y, z, b, b1, b2, f, g :: Id+[x, x1, x2, y, z, b, b1, b2, f, g] = mkTestIds+ [ ("x", int)+ , ("x1", int)+ , ("x2", int)+ , ("y", int)+ , ("z", int)+ , ("b", bool)+ , ("b1", bool)+ , ("b2", bool)+ , ("f", bool2int2int)+ , ("g", bool2int2int)+ ]+++-- | @+-- let f b =+-- if b+-- then \y -> y+-- else \z -> z+-- in f False 1+-- @+example1 :: CoreExpr+example1 =+ letrec+ f (lam b $+ ite (var b)+ (lam y (var y))+ (lam z (var z)))+ (var f $$ boolLit False $$ intLit 1)++anns1 :: Annotations+anns1 = annotations (StrAnal.analyse example1)++-- | @+-- let f b =+-- if b+-- then \x -> z+-- else \y -> z+-- in f False 1+-- @+example2 :: CoreExpr+example2 =+ letrec+ f (lam b $+ ite (var b)+ (lam x (var z))+ (lam y (var z)))+ (var f $$ boolLit False $$ intLit 1)++ty2 :: StrType+anns2 :: Annotations+StrLattice (ty2, anns2) = StrAnal.analyse example2++-- | @+-- let f b =+-- if b+-- then f b+-- else \y -> z+-- in f False 1+-- @+example3 :: CoreExpr+example3 =+ letrec+ f (lam b $+ ite (var b)+ (var f $$ var b)+ (lam y (var z)))+ (var f $$ boolLit False $$ intLit 1)++ty3 :: StrType+anns3 :: Annotations+StrLattice (ty3, anns3) = StrAnal.analyse example3++-- | @+-- let f b =+-- if b+-- then \x -> f b z+-- else \y -> z+-- in f False 1+-- @+example4 :: CoreExpr+example4 =+ letrec+ f (lam b $+ ite (var b)+ (lam x (var f $$ var b $$ var z))+ (lam y (var z)))+ (var f $$ boolLit False $$ intLit 1)++ty4 :: StrType+StrLattice (ty4, _) = StrAnal.analyse example4++-- | @+-- let f b =+-- if b+-- then \x -> f b z+-- else \y -> 0+-- in f False 1+-- @+example5 :: CoreExpr+example5 =+ letrec+ f (lam b $+ ite (var b)+ (lam x (var f $$ var b $$ var z))+ (lam y (intLit 0)))+ (var f $$ boolLit False $$ intLit 1)++ty5 :: StrType+StrLattice (ty5, _) = StrAnal.analyse example5+++-- | @+-- let f b =+-- if b+-- then f b+-- else \y -> y+-- in f False 1+-- @+example6 :: CoreExpr+example6 =+ letrec+ f (lam b $+ ite (var b)+ (var f $$ var b)+ (lam y (var y)))+ (var f $$ boolLit False $$ intLit 1)++anns6 :: Annotations+StrLattice (_, anns6) = StrAnal.analyse example6+++-- | @+-- let f b x =+-- if b+-- then f b z+-- else z+-- in f False 1+-- @+simpleRecursive1 :: CoreExpr+simpleRecursive1 = tidyExpr emptyTidyEnv $+ letrec+ f (lam b $ lam x $+ ite (var b)+ (var f $$ var b $$ var z)+ (var z))+ (var f $$ boolLit False $$ intLit 1)+++-- | @+-- let f b1 x1 =+-- let g b2 x2 =+-- if b2+-- then g b2 z+-- else f b2 x2+-- in if b1+-- then g b1 x1+-- else z+-- in f False 1+-- @+nestedRecursive1 :: CoreExpr+nestedRecursive1 = tidyExpr emptyTidyEnv $+ letrec+ f (lam b1 $ lam x1 $+ letrec+ g (lam b2 $ lam x2 $+ ite (var b2)+ (var g $$ var b2 $$ var z)+ (var f $$ var b2 $$ var x2))+ (ite (var b)+ (var g $$ var b1 $$ var x1)+ (var z)))+ (var f $$ boolLit False $$ intLit 1)+++tests :: [TestTree]+tests =+ [ testGroup "example1"+ [ testCase "f is called strictly with two args" $+ lookupAnnotation f anns1 @?= Just (Strict 2)+ , testCase "b is evaluated strictly" $+ lookupAnnotation b anns1 @?= Just (Strict 0)+ , testCase "y is evaluated strictly" $+ lookupAnnotation y anns1 @?= Just (Strict 0)+ , testCase "z is evaluated strictly" $+ lookupAnnotation z anns1 @?= Just (Strict 0)+ ]+ , testGroup "example2"+ [ testCase "f is called strictly with two args" $+ lookupAnnotation f anns2 @?= Just (Strict 2)+ , testCase "x is evaluated lazily" $+ lookupAnnotation x anns2 @?= Just Lazy+ , testCase "y is evaluated lazily" $+ lookupAnnotation y anns2 @?= Just Lazy+ , testCase "fv z is evaluated strictly" $+ fst (peelFV z ty2) @?= Strict 0+ ]+ , testGroup "example3"+ [ testCase "f is called strictly with two args" $+ lookupAnnotation f anns3 @?= Just (Strict 2)+ , testCase "b is evaluated strictly" $+ lookupAnnotation b anns3 @?= Just (Strict 0)+ , testCase "y is evaluated lazily" $+ lookupAnnotation y anns3 @?= Just Lazy+ , testCase "fv z is evaluated strictly" $+ fst (peelFV z ty3) @?= Strict 0+ ]+ , testGroup "example4"+ [ testCase "fv z is evaluated strictly" $+ fst (peelFV z ty4) @?= Strict 0+ ]+ , testGroup "example5"+ [ testCase "fv z is evaluated lazily" $+ fst (peelFV z ty5) @?= Lazy+ ]+ , testGroup "example6"+ [ testCase "y is evaluated strictly" $+ lookupAnnotation y anns6 @?= Just (Strict 0)+ ]+ , coincidesWithAdHoc "simpleRecursive1" simpleRecursive1+ , coincidesWithAdHoc "nestedRecursive1" nestedRecursive1+ , coincidesWithAdHocOnFile "exprs/const.hs"+ , coincidesWithAdHocOnFile "exprs/findLT.hs"+ ] where+ coincidesWithAdHoc desc e =+ testGroup desc+ [ testCase "coincides with AdHocStrAnal" $+ StrAnal.analyse e @?= AdHocStrAnal.analyse e+ ]+ coincidesWithAdHocOnFile file =+ testGroup file+ [ testCase "coincides with AdHocStrAnal" $ do+ e <- compileCoreExpr file+ StrAnal.analyse e @?= AdHocStrAnal.analyse e+ ]+
+ tests/Trivial.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Trivial (tests) where++import Algebra.Lattice+import Datafix+import Datafix.Worklist (Density (..), IterationBound (..),+ solveProblem)+import Datafix.Worklist.Graph (GraphRef)+import Numeric.Natural+import Test.Tasty+import Test.Tasty.HUnit++import Fac+import Fib+import Mutual++instance JoinSemiLattice Natural where+ (\/) = max++instance BoundedJoinSemiLattice Natural where+ bottom = 0++fixFib, fixFac, fixMutualRecursive+ :: GraphRef graph => (Node -> Density graph) -> Int -> Natural+fixFib density n = solveProblem fibProblem (density (Node n)) NeverAbort (Node n)+fixFac density n = solveProblem facProblem (density (Node n)) NeverAbort (Node n)+fixMutualRecursive density n = solveProblem mutualRecursiveProblem (density (Node 1)) NeverAbort (Node n)++tests :: [TestTree]+tests =+ [ testGroup "Memoization"+ [ testGroup "Sparse"+ [ testCase "fibonacci 10" (fixFib (const Sparse) 10 @?= fib 10)+ , testCase "factorial 100" (fixFac (const Sparse) 100 @?= fac 100)+ ]+ , testGroup "Dense"+ [ testCase "fibonacci 10" (fixFib Dense 10 @?= fib 10)+ , testCase "factorial 100" (fixFac Dense 100 @?= fac 100)+ ]+ ]+ , testGroup "mutual recursion"+ [ testGroup "Sparse"+ [ testCase "first node is stable" (fixMutualRecursive (const Sparse) 0 @?= 11)+ , testCase "second node is stable" (fixMutualRecursive (const Sparse) 1 @?= 10)+ ]+ , testGroup "Dense"+ [ testCase "first node is stable" (fixMutualRecursive Dense 0 @?= 11)+ , testCase "second node is stable" (fixMutualRecursive Dense 1 @?= 10)+ ]+ , testGroup "Abortion"+ [ testCase "aborts after 5 updates with value 42" (solveProblem mutualRecursiveProblem Sparse (AbortAfter 5 (const 42)) (Node 1) @?= 42)+ ]+ ]+ ]
+ tests/doctest.hs view
@@ -0,0 +1,5 @@+import System.FilePath.Glob+import Test.DocTest++main :: IO ()+main = glob "src/**/*.hs" >>= doctest