diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +`datafix` [![Build Status](https://travis-ci.org/sgraf812/datafix.svg?branch=master)](https://travis-ci.org/sgraf812/datafix) [![Hackage](https://img.shields.io/hackage/v/datafix.svg)](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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple.Toolkit +main = defaultMainWithBuildInfo diff --git a/bench/Main.hs b/bench/Main.hs new file mode 100644 --- /dev/null +++ b/bench/Main.hs @@ -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) diff --git a/datafix.cabal b/datafix.cabal new file mode 100644 --- /dev/null +++ b/datafix.cabal @@ -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 diff --git a/examples/Analyses/AdHocStrAnal.hs b/examples/Analyses/AdHocStrAnal.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/AdHocStrAnal.hs @@ -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) diff --git a/examples/Analyses/StrAnal.hs b/examples/Analyses/StrAnal.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/StrAnal.hs @@ -0,0 +1,5 @@ +module Analyses.StrAnal + ( Impl.analyse + ) where + +import qualified Analyses.StrAnal.Analysis as Impl diff --git a/examples/Analyses/StrAnal/Analysis.hs b/examples/Analyses/StrAnal/Analysis.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/StrAnal/Analysis.hs @@ -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]) diff --git a/examples/Analyses/StrAnal/Arity.hs b/examples/Analyses/StrAnal/Arity.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/StrAnal/Arity.hs @@ -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) diff --git a/examples/Analyses/StrAnal/Strictness.hs b/examples/Analyses/StrAnal/Strictness.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/StrAnal/Strictness.hs @@ -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 diff --git a/examples/Analyses/Syntax/CoreSynF.hs b/examples/Analyses/Syntax/CoreSynF.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/Syntax/CoreSynF.hs @@ -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 diff --git a/examples/Analyses/Syntax/MkCoreFromFile.hs b/examples/Analyses/Syntax/MkCoreFromFile.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/Syntax/MkCoreFromFile.hs @@ -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 () diff --git a/examples/Analyses/Syntax/MkCoreHelpers.hs b/examples/Analyses/Syntax/MkCoreHelpers.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/Syntax/MkCoreHelpers.hs @@ -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 diff --git a/examples/Analyses/Templates/LetDn.hs b/examples/Analyses/Templates/LetDn.hs new file mode 100644 --- /dev/null +++ b/examples/Analyses/Templates/LetDn.hs @@ -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 , 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 #-} diff --git a/examples/Fac.hs b/examples/Fac.hs new file mode 100644 --- /dev/null +++ b/examples/Fac.hs @@ -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] diff --git a/examples/Fib.hs b/examples/Fib.hs new file mode 100644 --- /dev/null +++ b/examples/Fib.hs @@ -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) diff --git a/examples/Mutual.hs b/examples/Mutual.hs new file mode 100644 --- /dev/null +++ b/examples/Mutual.hs @@ -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" diff --git a/examples/Sum.hs b/examples/Sum.hs new file mode 100644 --- /dev/null +++ b/examples/Sum.hs @@ -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) diff --git a/exprs/const.hs b/exprs/const.hs new file mode 100644 --- /dev/null +++ b/exprs/const.hs @@ -0,0 +1,5 @@ +module Expr where + +expr a b = const a b + where + const a b = a diff --git a/exprs/findLT.hs b/exprs/findLT.hs new file mode 100644 --- /dev/null +++ b/exprs/findLT.hs @@ -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 diff --git a/exprs/kahan.hs b/exprs/kahan.hs new file mode 100644 --- /dev/null +++ b/exprs/kahan.hs @@ -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 diff --git a/exprs/lambda.hs b/exprs/lambda.hs new file mode 100644 --- /dev/null +++ b/exprs/lambda.hs @@ -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 = "" + + ---------------------------------------------------------------------- + -- 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)) diff --git a/exprs/sieve.hs b/exprs/sieve.hs new file mode 100644 --- /dev/null +++ b/exprs/sieve.hs @@ -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 n0 then n:rs else rs + turn o n rs = + let n' = o+n in + if n'`mod`p>0 then n':rs else rs diff --git a/lattices/Algebra/Lattice.hs b/lattices/Algebra/Lattice.hs new file mode 100644 --- /dev/null +++ b/lattices/Algebra/Lattice.hs @@ -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 +-- +-- 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: +-- +-- > 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: +-- +-- > 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 and +-- +-- > 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 . +-- 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 . +-- 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 . +-- 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 . +-- 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 . +-- 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 . +-- 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) diff --git a/src/Datafix.hs b/src/Datafix.hs new file mode 100644 --- /dev/null +++ b/src/Datafix.hs @@ -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 diff --git a/src/Datafix/Description.hs b/src/Datafix/Description.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Description.hs @@ -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 #-} diff --git a/src/Datafix/IntArgsMonoMap.hs b/src/Datafix/IntArgsMonoMap.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/IntArgsMonoMap.hs @@ -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) diff --git a/src/Datafix/IntArgsMonoSet.hs b/src/Datafix/IntArgsMonoSet.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/IntArgsMonoSet.hs @@ -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 diff --git a/src/Datafix/MonoMap.hs b/src/Datafix/MonoMap.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/MonoMap.hs @@ -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 diff --git a/src/Datafix/NodeAllocator.hs b/src/Datafix/NodeAllocator.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/NodeAllocator.hs @@ -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 #-} diff --git a/src/Datafix/ProblemBuilder.hs b/src/Datafix/ProblemBuilder.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/ProblemBuilder.hs @@ -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)) diff --git a/src/Datafix/Tutorial.hs b/src/Datafix/Tutorial.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Tutorial.hs @@ -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 diff --git a/src/Datafix/Utils/GrowableVector.hs b/src/Datafix/Utils/GrowableVector.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Utils/GrowableVector.hs @@ -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 #-} diff --git a/src/Datafix/Utils/TypeLevel.hs b/src/Datafix/Utils/TypeLevel.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Utils/TypeLevel.hs @@ -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 diff --git a/src/Datafix/Worklist.hs b/src/Datafix/Worklist.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Worklist.hs @@ -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 diff --git a/src/Datafix/Worklist/Graph.hs b/src/Datafix/Worklist/Graph.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Worklist/Graph.hs @@ -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)] diff --git a/src/Datafix/Worklist/Graph/Dense.hs b/src/Datafix/Worklist/Graph/Dense.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Worklist/Graph/Dense.hs @@ -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 #-} diff --git a/src/Datafix/Worklist/Graph/Sparse.hs b/src/Datafix/Worklist/Graph/Sparse.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Worklist/Graph/Sparse.hs @@ -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 #-} diff --git a/src/Datafix/Worklist/Internal.hs b/src/Datafix/Worklist/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/Worklist/Internal.hs @@ -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 #-} diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -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 diff --git a/tests/Critical.hs b/tests/Critical.hs new file mode 100644 --- /dev/null +++ b/tests/Critical.hs @@ -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" diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -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 + ] + ] diff --git a/tests/StrAnal.hs b/tests/StrAnal.hs new file mode 100644 --- /dev/null +++ b/tests/StrAnal.hs @@ -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 + ] + diff --git a/tests/Trivial.hs b/tests/Trivial.hs new file mode 100644 --- /dev/null +++ b/tests/Trivial.hs @@ -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) + ] + ] + ] diff --git a/tests/doctest.hs b/tests/doctest.hs new file mode 100644 --- /dev/null +++ b/tests/doctest.hs @@ -0,0 +1,5 @@ +import System.FilePath.Glob +import Test.DocTest + +main :: IO () +main = glob "src/**/*.hs" >>= doctest