datafix 0.0.0.2 → 0.0.1.0

raw patch · 40 files changed

+741/−915 lines, 40 filesdep −Globdep ~basedep ~cabal-toolkitdep ~containerssetup-changednew-component:exe:firstfollow-examplePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: Glob

Dependency ranges changed: base, cabal-toolkit, containers, pomaps, primitive

API changes (from Hackage documentation)

Files

• Setup.hs +9/−1
• bench/Main.hs +2/−4
• datafix.cabal +34/−34
• examples/Analyses/StrAnal/Analysis.hs +5/−4
• examples/Analyses/Templates/LetDn.hs +6/−6
• examples/Fac.hs +2/−2
• examples/Fib.hs +2/−2
• examples/Mutual.hs +3/−3
• examples/SetRecurrences/FirstFollow.hs +201/−0
• examples/SetRecurrences/FirstFollow/Main.hs +23/−0
• examples/Sum.hs +2/−2
• exprs/lambda.hs +164/−162
• lattices/Algebra/Lattice.hs +0/−477
• src/Datafix.hs +4/−4
• src/Datafix/Common.hs +28/−2
• src/Datafix/Denotational.hs +5/−5
• src/Datafix/Entailments.hs +1/−1
• src/Datafix/Explicit.hs +10/−10
• src/Datafix/FrameworkBuilder.hs +59/−0
• src/Datafix/IntArgsMonoMap.hs +1/−1
• src/Datafix/IntArgsMonoSet.hs +1/−1
• src/Datafix/MonoMap.hs +1/−2
• src/Datafix/NodeAllocator.hs +1/−1
• src/Datafix/ProblemBuilder.hs +0/−63
• src/Datafix/Tutorial.hs +24/−13
• src/Datafix/Utils/Constraints.hs +1/−1
• src/Datafix/Utils/GrowableVector.hs +1/−1
• src/Datafix/Utils/TypeLevel.hs +1/−2
• src/Datafix/Worklist.hs +2/−2
• src/Datafix/Worklist/Denotational.hs +23/−11
• src/Datafix/Worklist/Graph.hs +1/−1
• src/Datafix/Worklist/Graph/Dense.hs +1/−1
• src/Datafix/Worklist/Graph/Sparse.hs +1/−1
• src/Datafix/Worklist/Internal.hs +50/−52
• stack.yaml +4/−23
• tests/Critical.hs +9/−12
• tests/FirstFollow.hs +44/−0
• tests/Main.hs +4/−0
• tests/Trivial.hs +5/−6
• tests/doctest.hs +6/−2

@@ -1,2 +1,10 @@+import           Distribution.Extra.Doctest+import           Distribution.Simple import           Distribution.Simple.Toolkit-main = defaultMainWithBuildInfo++main :: IO ()+main = defaultMainWithHooks simpleUserHooksWithBuildInfo+  { buildHook = \pkg lbi hooks flags -> do+      generateBuildModule "doctests" flags pkg lbi+      buildHook simpleUserHooks pkg lbi hooks flags+  }

@@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -fno-warn-orphans #-}  import           Algebra.Lattice@@ -6,9 +7,6 @@ import           Criterion import           Criterion.Main import           Datafix-import           Datafix.Worklist               (Density (..),-                                                 IterationBound (..),-                                                 solveProblem) import           Datafix.Worklist.Graph         (GraphRef) import           Numeric.Natural @@ -36,7 +34,7 @@   rnf = seqExpr  fixSum :: GraphRef graph => (Node -> Density graph) -> Int -> Natural-fixSum density n = solveProblem sumProblem (density (Node n)) NeverAbort (Node n)+fixSum density n = solveProblem sumFramework (density (Node n)) NeverAbort (dependOn @(DependencyM _ Natural) (Node n))  main :: IO () main = defaultMain

@@ -1,5 +1,5 @@ name:                datafix-version:             0.0.0.2+version:             0.0.1.0 synopsis:            Fixing data-flow problems description:         Fixing data-flow problems in expression trees.                      This should be useful if you want to write optimizations@@ -13,14 +13,16 @@ license-file:        LICENSE author:              Sebastian Graf maintainer:          sgraf1337@gmail.com-copyright:           © 2018 Sebastian Graf+copyright:           © 2017-2020 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+-- We have autogen-modules, so we need Cabal 2.0+cabal-version:       2.0+tested-with:         GHC==8.8.1, GHC==8.6.5, GHC==8.4.4, GHC==8.2.2  extra-source-files:   CHANGELOG.md@@ -36,15 +38,11 @@   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-doctest >= 1 && < 1.1     , cabal-toolkit >= 0.0.4  library@@ -57,7 +55,7 @@                      Datafix.Explicit                      Datafix.MonoMap                      Datafix.NodeAllocator-                     Datafix.ProblemBuilder+                     Datafix.FrameworkBuilder                      Datafix.Tutorial                      Datafix.Utils.Constraints                      Datafix.Utils.TypeLevel@@ -73,19 +71,16 @@                      Datafix.IntArgsMonoMap                      Datafix.IntArgsMonoSet   build-depends:     base >= 4.8 && < 5-                   , containers >= 0.5 && < 0.6+                   , containers >= 0.5 && < 0.7                    , 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+                   , primitive >= 0.6.2.0 && < 0.8+                   -- Prior to 0.2, pomaps used to offer a flag to compile without+                   -- lattices that confuses CI+                   , pomaps >= 0.2 && < 0.3+                   , lattices  test-suite tests   type:              exitcode-stdio-1.0@@ -102,16 +97,17 @@                      Analyses.Syntax.MkCoreHelpers                      Analyses.Syntax.MkCoreFromFile                      Analyses.Templates.LetDn+                     SetRecurrences.FirstFollow                      Fib                      Fac                      Mutual                      Critical                      Trivial                      StrAnal+                     FirstFollow   build-depends:     base >= 4.8 && < 5-                   -- let cabal-toolkit choose the Cabal version                    , Cabal-                   , cabal-toolkit == 0.0.4+                   , cabal-toolkit >= 0.0.4                    , tasty >= 0.11                    , tasty-hunit >= 0.9                    , tasty-smallcheck >= 0.8@@ -125,10 +121,7 @@                    , 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+                   , lattices < 2  test-suite doctests   type:              exitcode-stdio-1.0@@ -138,9 +131,10 @@   main-is:           doctest.hs   build-depends:     base >= 4.8 && < 5                    , doctest >=0.10-                   , Glob >= 0.7                    , QuickCheck >= 2.5                    , datafix+  other-modules:     Build_doctests+  autogen-modules:   Build_doctests  benchmark benchmarks   type:              exitcode-stdio-1.0@@ -148,8 +142,7 @@   ghc-options:       -Wall -threaded -rtsopts -with-rtsopts=-N   hs-source-dirs:    bench examples   main-is:           Main.hs-  other-modules:     Sum-                     Analyses.AdHocStrAnal+  other-modules:     Analyses.AdHocStrAnal                      Analyses.StrAnal                      Analyses.StrAnal.Analysis                      Analyses.StrAnal.Arity@@ -158,23 +151,30 @@                      Analyses.Syntax.MkCoreHelpers                      Analyses.Syntax.MkCoreFromFile                      Analyses.Templates.LetDn+                     Sum   build-depends:     base >= 4.8 && < 5-                   -- let cabal-toolkit choose the Cabal version                    , Cabal-                   , cabal-toolkit == 0.0.4+                   , cabal-toolkit >= 0.0.4                    , criterion >= 1.1                    , deepseq                    , containers                    , primitive                    , transformers < 0.6-                   , datafix                   +                   , 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+                   , lattices < 2++executable firstfollow-example+  default-language:  Haskell2010+  hs-source-dirs:    examples+  main-is:           SetRecurrences/FirstFollow/Main.hs+  ghc-options:       -Wall -threaded -rtsopts -with-rtsopts=-N+  other-modules:     SetRecurrences.FirstFollow+  build-depends:     base+                   , containers+                   , datafix

@@ -1,12 +1,13 @@ {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-} -- 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'@.+-- that is passed on to @Analyses.Templates.LetDn.'buildFramework'@,+-- yielding a 'DataFlowFramework' to be solved by @Datafix.'solveProblem'@. module Analyses.StrAnal.Analysis (analyse) where  import           Algebra.Lattice@@ -24,7 +25,7 @@ import           VarEnv  analyse :: CoreExpr -> StrLattice-analyse expr = evalDenotation (buildDenotation transferFunctionAlg expr) NeverAbort (0 :: Arity)+analyse expr = evalDenotation @(Arity -> StrLattice) (buildDenotation transferFunctionAlg expr) NeverAbort (0 :: Arity)  applyWhen :: Bool -> (a -> a) -> a -> a applyWhen True f  = f@@ -32,7 +33,7 @@  -- | 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+-- @Analyses.Tempaltes.LetDn.'buildFramework'@, 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'.

@@ -12,8 +12,8 @@ -- 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+-- 'TransferAlgebra' for 'buildFramework' to get a specification for the desired+-- data-flow problem. Remarkably, 'buildFramework' 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@@@ -58,7 +58,7 @@ type TF m = LiftedFunc (Domain m) m  -- | Given a 'TransferAlgebra', this function takes care of building a--- 'DataFlowProblem' for 'CoreExpr's.+-- 'DataFlowFramework' 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@@ -66,12 +66,12 @@ -- -- 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+-- 'GraphRef'. The final return value is the 'DataFlowFramework' 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'+-- 'buildFramework' 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.@@ -81,7 +81,7 @@   => Currying (ParamTypes domain) (ReturnType domain -> ReturnType domain -> Bool)   => TransferAlgebra domain   -> CoreExpr-  -> Denotation domain+  -> Denotation domain domain buildDenotation = buildDenotation'  -- This brings in the scope the existentially quantified 'MonadDatafix'. Too

@@ -7,8 +7,8 @@ import           Datafix import           Numeric.Natural -facProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m-facProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+facFramework :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+facFramework = DFF transfer (const (eqChangeDetector @(Domain m)))   where     transfer :: Node -> LiftedFunc Natural m     transfer (Node 0) = return 1

@@ -7,8 +7,8 @@ import           Datafix import           Numeric.Natural -fibProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m-fibProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+fibFramework :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+fibFramework = DFF transfer (const (eqChangeDetector @(Domain m)))   where     transfer :: Node -> LiftedFunc Natural m     transfer (Node 0) = return 0

@@ -7,7 +7,7 @@ import           Datafix import           Numeric.Natural --- | A 'DataFlowProblem' with two nodes, mutually depending on another, like+-- | A 'DataFlowFramework' with two nodes, mutually depending on another, like -- -- @ --    a = b + 1@@ -16,8 +16,8 @@ -- -- 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)))+mutualRecursiveFramework :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+mutualRecursiveFramework = DFF transfer (const (eqChangeDetector @(Domain m)))   where     transfer :: Node -> LiftedFunc Natural m     transfer (Node 0) = do

@@ -0,0 +1,201 @@+{-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeApplications      #-}+{-# OPTIONS_GHC -fexpose-all-unfoldings #-}++module SetRecurrences.FirstFollow+  ( V (..)+  , WithEOF (..)+  , Grammar (..)+  , mkGrammar+  , augmentGrammar+  , first+  , follow+  , dyck+  , llsll+  , emptyL+  , leftrec+  ) where++import           Prelude hiding (words)++import           Datafix++import           Control.Applicative+import           Control.Monad+import           Data.Bifunctor (second)+import           Data.Functor.Identity+import           Data.List (unfoldr)+import           Data.Map (Map)+import qualified Data.Map as Map+import           Data.Maybe (fromMaybe)+import           Data.Set (Set)+import qualified Data.Set as Set++data V t nt+  = T t+  | NT nt+  deriving (Eq, Ord, Show)++eitherV :: (t -> r) -> (nt -> r) -> V t nt -> r+eitherV l _ (T t)   = l t+eitherV _ r (NT nt) = r nt++data WithEOF a+  = EOF+  | NoEOF a+  deriving (Eq, Ord, Show)++instance {-# OVERLAPPING #-} Show [WithEOF Char] where+  show = show . map f+    where+      f EOF       = '#'+      f (NoEOF c) = c++data Grammar t nt+  = G+  { terminals :: Set t+  , nonterminals :: Set nt+  , productions :: Map nt (Set [V t nt])+  , start :: nt+  }++mkGrammar :: (Ord v) => [v] -> [v] -> [(v, [v])] -> v -> Grammar v v+mkGrammar ts nts ps s+  = G+  { terminals    = Set.fromList ts+  , nonterminals = Set.fromList nts+  , productions  = Map.fromListWith Set.union (map (second (Set.singleton . map mkV)) ps)+  , start        = s+  }+  where+    mkV v+      | v `elem` ts  = T v+      | v `elem` nts = NT v+      | otherwise  = error "not part of vocabulary"++augmentGrammar :: (Ord t, Ord nt) => nt -> Grammar t nt -> Grammar t nt+augmentGrammar s' gr+  = G+  { terminals    = terminals gr+  , nonterminals = Set.insert s' (nonterminals gr)+  , productions  = Map.insert s' (Set.singleton [NT (start gr)]) $ productions gr+  , start        = s'+  }++epsilon :: [t]+epsilon = []++kconcat :: Int -> [a] -> [a] -> [a]+kconcat k pref suf = take k (pref ++ suf)++pointwise2 :: Ord c => (a -> b -> c) -> Set a -> Set b -> Set c+pointwise2 f as bs = Set.fromList (liftA2 f (Set.toList as) (Set.toList bs))++-- |+-- NB: A Monad here is strictly more performant than Applicative here, because+-- we can exit early. On the other this means we have this really adhoc fold over+subst :: (Monad m, Ord t) => Int -> (nt -> m (Set [t])) -> [V t nt] -> m (Set [t])+subst k lkup = go (Set.singleton epsilon)+  where+    go prefs [] = pure prefs+    go prefs (v:vs) = do+      suffs <- eitherV (pure . Set.singleton . (:[])) lkup v+      let words = pointwise2 (kconcat k) prefs suffs+      if any ((< k) . length) words+        then go words vs+        else pure words++first :: forall t nt . (Ord t, Ord nt, Datafixable (Set [t])) => Int -> Grammar t nt -> [V t nt] -> Set [t]+first k gr = runIdentity . subst k (Identity . (firstSolutions k gr Map.!))++firstSolutions :: forall t nt . (Ord t, Ord nt, Datafixable (Set [t])) => Int -> Grammar t nt -> Map nt (Set [t])+firstSolutions k gr = evalDenotation @(Set [t]) @(Map nt (Set [t])) plan NeverAbort+  where+    plan :: forall m . (MonadDatafix m, Domain (DepM m) ~ Set [t]) => m (DepM m (Map nt (Set [t])))+    plan = sequence <$> build Map.empty (Set.toList (nonterminals gr))+    build :: forall m . (MonadDatafix m, Domain (DepM m) ~ Set [t]) => Map nt (DepM m (Set [t])) -> [nt] -> m (Map nt (DepM m (Set [t])))+    build env []       = pure env+    build env (nt:nts) = datafixEq $ \self -> do+      env' <- build (Map.insert nt self env) nts+      let rhss = Set.toList (fromMaybe Set.empty (Map.lookup nt (productions gr)))+      let iter = Set.unions <$> mapM (subst k (env' Map.!)) rhss+      pure (env', iter)++-- | Assumes the given grammar is augmented+follow :: forall t nt . (Ord t, Ord nt, Datafixable (Set [WithEOF t])) => Int -> Grammar t nt -> nt -> Set [WithEOF t]+follow k gr = (evalDenotation @(Set [WithEOF t]) plan NeverAbort Map.!)+  where+    prods :: [(nt, [V t nt])]+    prods =+      [ (nt, rhs)+      | (nt, rhss) <- Map.toList (productions gr)+      , rhs <- Set.toList rhss+      ]+    firsts = firstSolutions k gr+    initialEnv :: forall m . Monad m => Map nt (m (Set [WithEOF t]))+    initialEnv = Map.singleton (start gr) (pure (Set.singleton (replicate k EOF)))+    plan :: forall m . (MonadDatafix m, Domain (DepM m) ~ Set [WithEOF t]) => m (DepM m (Map nt (Set [WithEOF t])))+    plan = sequence <$> build initialEnv (Set.toList (Set.delete (start gr) (nonterminals gr)))+    build :: forall m . (MonadDatafix m, Domain (DepM m) ~ Set [WithEOF t]) => Map nt (DepM m (Set [WithEOF t])) -> [nt] -> m (Map nt (DepM m (Set [WithEOF t])))+    build env []       = pure env+    build env (nt:nts) = datafixEq $ \self -> do+      env' <- build (Map.insert nt self env) nts+      let occs = flip concatMap prods $ \(parent, rhs) -> flip unfoldr rhs $ \rest ->+            case dropWhile (/= NT nt) rest of+              [] -> Nothing+              (_:follows) -> Just ((parent, follows), follows)++      let iter = fmap Set.unions $ forM occs $ \(parent, follows) -> do+            let prefs = Set.map (map NoEOF) $ runIdentity $ subst k (Identity . (firsts Map.!)) follows+            let (short, long) = Set.partition ((< k) . length) prefs+            if null short+              then pure prefs+              else Set.union long . pointwise2 (kconcat k) prefs <$> (env' Map.! parent)++      pure (env', iter)++dyck :: Grammar Char Char+dyck = augmentGrammar 'O' $ mkGrammar+  "()"+  "S"+  [ ('S', "")+  , ('S', "(S)S")+  ]+  'S'++llsll :: Grammar Char Char+llsll = augmentGrammar 'O' $ mkGrammar+  "ab"+  "ZA"+  [ ('Z', "aAab")+  , ('Z', "bAb")+  , ('A', "a")+  , ('A', "")+  ]+  'Z'++emptyL :: Grammar Char Char+emptyL = augmentGrammar 'O' $ mkGrammar+  ""+  "ABC"+  [ ('A', "BC")+  , ('B', "CA")+  , ('C', "A")+  ]+  'A'++leftrec :: Grammar Char Char+leftrec = augmentGrammar 'O' $ mkGrammar+  "abc"+  "SA"+  [ ('S', "Aa")+  , ('A', "Sb")+  , ('A', "c")+  ]+  'S'

@@ -0,0 +1,23 @@+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE FlexibleContexts      #-}++import           System.Environment+import           Text.Printf+import           SetRecurrences.FirstFollow++main :: IO ()+main = do+  (k:_) <- map read <$> getArgs+  let uncurry3 f (x,y,z) = f x y z+  let analyse name gr (s :: Char) = do+        printf "%s:\n" name+        printf "  first_%d(%s): %s\n" k (show s) (show $ first k gr [NT s])+        printf "  follow_%d(%s): %s\n" k (show s) (show $ follow k gr s)+        putStrLn ""+  mapM_ (uncurry3 analyse)+    [ ("Dyck", dyck, 'S')+    , ("LL(1), not SLL(k)", llsll, 'A')+    , ("empty", emptyL, 'A')+    , ("left recursive", leftrec, 'S')+    ]+

@@ -7,8 +7,8 @@ import           Datafix import           Numeric.Natural -sumProblem :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m-sumProblem = DFP transfer (const (eqChangeDetector @(Domain m)))+sumFramework :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+sumFramework = DFF transfer (const (eqChangeDetector @(Domain m)))   where     transfer :: Node -> LiftedFunc Natural m     transfer (Node 0) = return 0

@@ -1,6 +1,6 @@-{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-module Expr where+module Lambda ( expr ) where  -- From Mark: marku@cs.waikato.ac.nz [Nov 2001] -- This program contrasts the cost of direct and@@ -38,20 +38,20 @@ --              and about 7 times more memory. -- -import           System.Environment+import System.Environment -import           Control.Monad.Trans.State.Strict-import           Data.Functor.Identity+import Control.Monad.Trans.State.Strict+import Data.Functor.Identity+import Control.Monad (replicateM_) -------------------------------------------------------------------------- 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)+expr :: Id Term+expr = simpleEval [] (App sum0 (Con 1)) -instance Show a => Show (Id a) where-    show (Id i) = show (runIdentity i)+------------------------------------------------------------+-- Data structures+------------------------------------------------------------+--instance Show (a -> b) where+--    show f = "<function>"   data Term@@ -67,6 +67,18 @@     deriving (Eq,Read,Show)  type Env = [(String,Term)]+++----------------------------------------------------------------------+-- 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)++ ----------------------------------------------------------------- -- This class extends Monad to have the standard features -- we expect while evaluating/manipulating expressions.@@ -84,178 +96,168 @@  instance EvalEnvMonad (State Env) where     incr = return ()-    traverseTerm = undefined -- eval+    traverseTerm = eval     lookupVar v = do-        env <- get-        return $ lookup2 env+          env <- get+          return $ lookup2 env         where-        lookup2 env = maybe (error ("undefined var: " ++ v)) id (lookup v env)+          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 ()-+traverseCon :: (EvalEnvMonad m) => Term -> m Int+traverseCon t =+    do t' <- traverseTerm t+       case t' of+           Con c -> return c+           _ -> error ("Not a Con: " ++ show t') -    -------------------------------------------------------------    -- Data structures-    -------------------------------------------------------------    --instance Show (a -> b) where-    --    show f = "<function>"+eval :: (EvalEnvMonad m) => Term -> m Term+eval (Var x)   =+    do e <- currEnv+       t <- lookupVar x+       traverseTerm t+eval (Add u v) =+    do {u' <- traverseCon u;+        v' <- traverseCon 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) -    -----------------------------------------------------------------------    -- 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)+--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         = error ("bad application: " ++ pp a +++                              "  [ " ++ pp b ++ " ].")    -    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 ++ " ].")-+----------------------------------------------------------------------+-- 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) +simpleEvalCon :: Env -> Term -> Id Int+simpleEvalCon env e =+    do e' <- simpleEval env e+       case e' of+           Con c -> return c+           _ -> error ("Not a Con: " ++ show e') -    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+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 {u' <- simpleEvalCon env u;+        v' <- simpleEvalCon env v;+        return (Con (u' + v'))}+    where+    addCons (Con a) (Con b) = return (Con (a+b))+    addCons (Con _) b = error ("type error in second arg of Add: " ++ pp b)+    addCons a (Con _) = error ("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 ++ " ].")+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         = error ("bad application: " ++ pp a +++                              "  [ " ++ pp b ++ " ].") -    -------------------------------------------------------------    -- Utility functions for printing terms and envs.-    -------------------------------------------------------------    ppenv env = "[" ++ concatMap (\(v,t) -> v ++ "=" ++ pp t ++ ", ") env ++ "]"+------------------------------------------------------------+-- Utility functions for printing terms and envs.+------------------------------------------------------------+ppenv env = "[" ++ concatMap (\(v,t) -> v ++ "=" ++ pp t ++ ", ") env ++ "]"  -    pp :: Term -> String-    pp = ppn 0+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)+-- 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+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")))+------------------------------------------------------------+-- 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))+-- 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)))+-- 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"))))+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))+-- This is the fix point combinator:  Y+fix :: Term+fix = (Lam "F" (App lfxx lfxx))

@@ -1,477 +0,0 @@-{-# LANGUAGE CPP                #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE FlexibleInstances  #-}-{-# LANGUAGE Safe               #-}-#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709-{-# OPTIONS_GHC -fno-warn-amp #-}-#endif-------------------------------------------------------------------------------- |--- Module      :  Algebra.Lattice--- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke--- License     :  BSD-3-Clause (see the file LICENSE)------ Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>------ In mathematics, a lattice is a partially ordered set in which every--- two elements have a unique supremum (also called a least upper bound--- or @join@) and a unique infimum (also called a greatest lower bound or--- @meet@).------ In this module lattices are defined using 'meet' and 'join' operators,--- as it's constructive one.---------------------------------------------------------------------------------module Algebra.Lattice (-    -- * Unbounded lattices-    JoinSemiLattice(..), MeetSemiLattice(..), Lattice,-    joinLeq, meetLeq,--    -- * Bounded lattices-    BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice,-    joins, meets,-    fromBool,--    -- * Monoid wrappers-    Meet(..), Join(..),--    -- * Fixed points of chains in lattices-    lfp, lfpFrom, unsafeLfp,-    gfp, gfpFrom, unsafeGfp,-  ) where--import qualified Algebra.PartialOrd    as PO--import           Control.Monad.Zip     (MonadZip (..))-import           Data.Data             (Data, Typeable)-import           Data.Proxy            (Proxy (..))-import           Data.Semigroup        (All (..), Any (..), Endo (..),-                                        Semigroup (..))-import           Data.Void             (Void)-import           GHC.Generics          (Generic)--import qualified Data.IntMap           as IM-import qualified Data.IntSet           as IS-import qualified Data.Map              as M-import qualified Data.Set              as S--import           Control.Applicative   (Const (..))-import           Data.Functor.Identity (Identity (..))--infixr 6 /\ -- This comment needed because of CPP-infixr 5 \/---- | A algebraic structure with element joins: <http://en.wikipedia.org/wiki/Semilattice>------ > Associativity: x \/ (y \/ z) == (x \/ y) \/ z--- > Commutativity: x \/ y == y \/ x--- > Idempotency:   x \/ x == x-class JoinSemiLattice a where-    (\/) :: a -> a -> a-    (\/) = join--    join :: a -> a -> a-    join = (\/)--#if __GLASGOW_HASKELL__ >= 707-    {-# MINIMAL (\/) | join #-}-#endif-{-# DEPRECATED join "Use '\\/' infix operator" #-}---- | The partial ordering induced by the join-semilattice structure-joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool-joinLeq x y = (x \/ y) == y---- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice>------ > Associativity: x /\ (y /\ z) == (x /\ y) /\ z--- > Commutativity: x /\ y == y /\ x--- > Idempotency:   x /\ x == x-class MeetSemiLattice a where-    (/\) :: a -> a -> a-    (/\) = meet--    meet :: a -> a -> a-    meet = (/\)--#if __GLASGOW_HASKELL__ >= 707-    {-# MINIMAL (/\) | meet #-}-#endif-{-# DEPRECATED meet "Use '/\\' infix operator" #-}---- | The partial ordering induced by the meet-semilattice structure-meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool-meetLeq x y = (x /\ y) == x------ | The combination of two semi lattices makes a lattice if the absorption law holds:--- see <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)>------ > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a-class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where---- | A join-semilattice with some element |bottom| that \/ approaches.------ > Identity: x \/ bottom == x-class JoinSemiLattice a => BoundedJoinSemiLattice a where-    bottom :: a---- | The join of a list of join-semilattice elements-joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a-joins = getJoin . foldMap Join---- | A meet-semilattice with some element |top| that /\ approaches.------ > Identity: x /\ top == x-class MeetSemiLattice a => BoundedMeetSemiLattice a where-    top :: a---- | The meet of a list of meet-semilattice elements-meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a-meets = getMeet . foldMap Meet---- | Lattices with both bounds-class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where---- | 'True' to 'top' and 'False' to 'bottom'-fromBool :: BoundedLattice a => Bool -> a-fromBool True  = top-fromBool False = bottom------- Sets-----instance Ord a => JoinSemiLattice (S.Set a) where-    (\/) = S.union--instance Ord a => MeetSemiLattice (S.Set a) where-    (/\) = S.intersection--instance Ord a => Lattice (S.Set a) where--instance Ord a => BoundedJoinSemiLattice (S.Set a) where-    bottom = S.empty------- IntSets-----instance JoinSemiLattice IS.IntSet where-    (\/) = IS.union--instance MeetSemiLattice IS.IntSet where-    (/\) = IS.intersection--instance Lattice IS.IntSet--instance BoundedJoinSemiLattice IS.IntSet where-    bottom = IS.empty------- Maps-----instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where-    (\/) = M.unionWith (\/)--instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where-    (/\) = M.intersectionWith (/\)--instance (Ord k, Lattice v) => Lattice (M.Map k v) where--instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where-    bottom = M.empty------- IntMaps-----instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where-    (\/) = IM.unionWith (\/)--instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where-    bottom = IM.empty--instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where-    (/\) = IM.intersectionWith (/\)--instance Lattice v => Lattice (IM.IntMap v)------- Functions-----instance JoinSemiLattice v => JoinSemiLattice (k -> v) where-    f \/ g = \x -> f x \/ g x--instance MeetSemiLattice v => MeetSemiLattice (k -> v) where-    f /\ g = \x -> f x /\ g x--instance Lattice v => Lattice (k -> v) where--instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where-    bottom = const bottom--instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where-    top = const top--instance BoundedLattice v => BoundedLattice (k -> v) where---- Unit-instance JoinSemiLattice () where-  _ \/ _ = ()--instance BoundedJoinSemiLattice () where-  bottom = ()--instance MeetSemiLattice () where-  _ /\ _ = ()--instance BoundedMeetSemiLattice () where-  top = ()--instance Lattice () where-instance BoundedLattice () where------- Tuples-----instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where-    (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2)--instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where-    (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2)--instance (Lattice a, Lattice b) => Lattice (a, b) where--instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where-    bottom = (bottom, bottom)--instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where-    top = (top, top)--instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where------- Bools-----instance JoinSemiLattice Bool where-    (\/) = (||)--instance MeetSemiLattice Bool where-    (/\) = (&&)--instance Lattice Bool where--instance BoundedJoinSemiLattice Bool where-    bottom = False--instance BoundedMeetSemiLattice Bool where-    top = True--instance BoundedLattice Bool where----- Monoids---- | Monoid wrapper for JoinSemiLattice-newtype Join a = Join { getJoin :: a }-  deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic)--instance JoinSemiLattice a => Semigroup (Join a) where-  Join a <> Join b = Join (a \/ b)--instance BoundedJoinSemiLattice a => Monoid (Join a) where-  mempty = Join bottom-  Join a `mappend` Join b = Join (a \/ b)--instance Functor Join where-  fmap f (Join x) = Join (f x)--instance Applicative Join where-  pure = Join-  Join f <*> Join x = Join (f x)-  _ *> x = x--instance Monad Join where-  return = pure-  Join m >>= f = f m-  (>>) = (*>)--instance MonadZip Join where-  mzip (Join x) (Join y) = Join (x, y)---- | Monoid wrapper for MeetSemiLattice-newtype Meet a = Meet { getMeet :: a }-  deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic)--instance MeetSemiLattice a => Semigroup (Meet a) where-  Meet a <> Meet b = Meet (a /\ b)--instance BoundedMeetSemiLattice a => Monoid (Meet a) where-  mempty = Meet top-  Meet a `mappend` Meet b = Meet (a /\ b)--instance Functor Meet where-  fmap f (Meet x) = Meet (f x)--instance Applicative Meet where-  pure = Meet-  Meet f <*> Meet x = Meet (f x)-  _ *> x = x--instance Monad Meet where-  return = pure-  Meet m >>= f = f m-  (>>) = (*>)--instance MonadZip Meet where-  mzip (Meet x) (Meet y) = Meet (x, y)---- All-instance JoinSemiLattice All where-  All a \/ All b = All $ a \/ b--instance BoundedJoinSemiLattice All where-  bottom = All False--instance MeetSemiLattice All where-  All a /\ All b = All $ a /\ b--instance BoundedMeetSemiLattice All where-  top = All True--instance Lattice All where-instance BoundedLattice All where---- Any-instance JoinSemiLattice Any where-  Any a \/ Any b = Any $ a \/ b--instance BoundedJoinSemiLattice Any where-  bottom = Any False--instance MeetSemiLattice Any where-  Any a /\ Any b = Any $ a /\ b--instance BoundedMeetSemiLattice Any where-  top = Any True--instance Lattice Any where-instance BoundedLattice Any where---- Endo-instance JoinSemiLattice a => JoinSemiLattice (Endo a) where-  Endo a \/ Endo b = Endo $ a \/ b--instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where-  bottom = Endo bottom--instance MeetSemiLattice a => MeetSemiLattice (Endo a) where-  Endo a /\ Endo b = Endo $ a /\ b--instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where-  top = Endo top--instance Lattice a => Lattice (Endo a) where-instance BoundedLattice a => BoundedLattice (Endo a) where---- Proxy-instance JoinSemiLattice (Proxy a) where-  _ \/ _ = Proxy--instance BoundedJoinSemiLattice (Proxy a) where-  bottom = Proxy--instance MeetSemiLattice (Proxy a) where-  _ /\ _ = Proxy--instance BoundedMeetSemiLattice (Proxy a) where-  top = Proxy--instance Lattice (Proxy a) where-instance BoundedLattice (Proxy a) where--#if MIN_VERSION_base(4,8,0)--- Identity-instance JoinSemiLattice a => JoinSemiLattice (Identity a) where-  Identity a \/ Identity b = Identity (a \/ b)--instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where-  bottom = Identity bottom--instance MeetSemiLattice a => MeetSemiLattice (Identity a) where-  Identity a /\ Identity b = Identity (a /\ b)--instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where-  top = Identity top--instance Lattice a => Lattice (Identity a) where-instance BoundedLattice a => BoundedLattice (Identity a) where-#endif---- Const-instance JoinSemiLattice a => JoinSemiLattice (Const a b) where-  Const a \/ Const b = Const (a \/ b)--instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where-  bottom = Const bottom--instance MeetSemiLattice a => MeetSemiLattice (Const a b) where-  Const a /\ Const b = Const (a /\ b)--instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where-  top = Const top--instance Lattice a => Lattice (Const a b) where-instance BoundedLattice a => BoundedLattice (Const a b) where---- Void-instance JoinSemiLattice Void where-  a \/ _ = a--instance MeetSemiLattice Void where-  a /\ _ = a--instance Lattice Void where---- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.--- Assumes that the function is monotone and does not check if that is correct.-{-# INLINE unsafeLfp #-}-unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a-unsafeLfp = PO.unsafeLfpFrom bottom---- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.--- Forces the function to be monotone.-{-# INLINE lfp #-}-lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a-lfp = lfpFrom bottom---- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.--- Forces the function to be monotone.-{-# INLINE lfpFrom #-}-lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a-lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x \/ x)----- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.--- Assumes that the function is antinone and does not check if that is correct.-{-# INLINE unsafeGfp #-}-unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a-unsafeGfp = PO.unsafeGfpFrom top---- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.--- Forces the function to be antinone.-{-# INLINE gfp #-}-gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a-gfp = gfpFrom top---- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.--- Forces the function to be antinone.-{-# INLINE gfpFrom #-}-gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a-gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x /\ x)

@@ -5,7 +5,7 @@  -- | -- Module      :  Datafix--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable@@ -19,7 +19,7 @@   , module Datafix.Denotational   , module Datafix.Explicit   , module Datafix.NodeAllocator-  , module Datafix.ProblemBuilder+  , module Datafix.FrameworkBuilder   , Datafix.MonoMap.MonoMap   , module Datafix.Utils.TypeLevel   , module Datafix.Worklist@@ -30,6 +30,6 @@ import           Datafix.Explicit import           Datafix.MonoMap import           Datafix.NodeAllocator-import           Datafix.ProblemBuilder-import           Datafix.Utils.TypeLevel+import           Datafix.FrameworkBuilder+import           Datafix.Utils.TypeLevel hiding (Map) import           Datafix.Worklist

@@ -11,7 +11,7 @@  -- | -- Module      :  Datafix.Common--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable@@ -26,12 +26,15 @@   , alwaysChangeDetector   , MonadDomain (..)   , Datafixable+  , evalAt+  , (<!)   ) where  import           Algebra.Lattice import           Datafix.MonoMap import           Datafix.Utils.Constraints import           Datafix.Utils.TypeLevel+import           Data.Type.Equality  -- $setup -- >>> :set -XTypeFamilies@@ -169,7 +172,7 @@ --      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'.+--      arguments in @Domain m@ into the 'Node' portion of the 'DataFlowFramework'. -- --  3.  For fixed-point iteration to work at all, the values which we iterate --      naturally have to be instances of 'BoundedJoinSemiLattice'.@@ -181,3 +184,26 @@   , MonoMapKey (Products (ParamTypes domain))   , BoundedJoinSemiLattice (ReturnType domain)   )+++evalAt+  :: forall f arr+   . Currying (ParamTypes arr) (ReturnType arr)+  => Functor f+  => f arr+  -> Products (ParamTypes arr)+  -> f (ReturnType arr)+evalAt mfunc args = app <$> mfunc+  where+    app func = uncurrys @(ParamTypes arr) (castWith (sym arrowsAxiom) func) args++(<!)+  :: forall f arr+   . Currying (ParamTypes arr) (ReturnType arr)+  => Functor f+  => f arr+  -> Products (ParamTypes arr)+  -> f (ReturnType arr)+mfunc <! args = app <$> mfunc+  where+    app func = uncurrys @(ParamTypes arr) (castWith (sym arrowsAxiom) func) args

@@ -9,7 +9,7 @@  -- | -- Module      :  Datafix.Denotational--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable@@ -34,11 +34,11 @@ -- | Builds on an associated 'DepM' that is a 'MonadDomain' (like any -- 'MonadDependency') by providing a way to track dependencies without explicit -- 'Node' management. Essentially, this allows to specify a build plan for a--- 'DataFlowProblem' through calls to 'datafix' in analogy to 'fix' or 'mfix'.+-- 'DataFlowFramework' through calls to 'datafix' in analogy to 'fix' or 'mfix'. class (Monad m, MonadDomain (DepM m)) => MonadDatafix m where   -- | The monad in which data dependencies are expressed.   -- Can and will be instantiated to some 'MonadDependency', if you choose-  -- to go through 'ProblemBuilder'.+  -- to go through 'FrameworkBuilder'.   type DepM m :: * -> *   -- | This is the closest we can get to an actual fixed-point combinator.   --@@ -69,5 +69,5 @@  -- | A denotation of some syntactic entity in a semantic @domain@, built in a -- some 'MonadDatafix' context.-type Denotation dom-  =  forall m. (MonadDatafix m, dom ~ Domain (DepM m)) => m (LiftedFunc dom (DepM m))+type Denotation domain func+  =  forall m. (MonadDatafix m, domain ~ Domain (DepM m)) => m (LiftedFunc func (DepM m))

@@ -3,7 +3,7 @@  -- | -- Module      :  Datafix.Entailments--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -9,7 +9,7 @@  -- | -- Module      :  Datafix.Explicit--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable@@ -21,11 +21,11 @@ -- -- Import this module transitively through "Datafix" and get access to -- "Datafix.Worklist" for functions that compute solutions to your--- 'DataFlowProblem's.+-- 'DataFlowFramework's.  module Datafix.Explicit   ( Node (..)-  , DataFlowProblem (..)+  , DataFlowFramework (..)   , MonadDependency (..)   ) where @@ -50,11 +50,11 @@ -- 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)+data DataFlowFramework m+  = DFF+  { dffTransfer     :: !(Node -> LiftedFunc (Domain m) m)   -- ^ A transfer function per each 'Node' of the modeled data-flow problem.-  , dfpDetectChange :: !(Node -> ChangeDetector (Domain m))+  , dffDetectChange :: !(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.   }@@ -76,11 +76,11 @@ --   -- sparing the negative n error case -- :} ----- We can construct a description of a 'DataFlowProblem' with this @transferFib@ function:+-- We can construct a description of a 'DataFlowFramework' with this @transferFib@ function: -- -- >>> :{---   dataFlowProblem :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m---   dataFlowProblem = DFP transferFib (const (eqChangeDetector @(Domain m)))+--   dataFlowFramework :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowFramework m+--   dataFlowFramework = DFF transferFib (const (eqChangeDetector @(Domain m))) -- :} -- -- We regard the ordinary @fib@ function a solution to the recurrence modeled by @transferFib@:

@@ -0,0 +1,59 @@+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE TypeFamilies               #-}++-- |+-- Module      :  Datafix.FrameworkBuilder+-- Copyright   :  (c) Sebastian Graf 2017-2020+-- License     :  ISC+-- Maintainer  :  sgraf1337@gmail.com+-- Portability :  portable+--+-- Builds a 'DataFlowFramework' for a 'Denotation'al formulation in terms of+-- 'MonadDatafix'. Effectively reduces descriptions from "Datafix.Denotational"+-- to ones from "Datafix.Explicit", so that solvers such as "Datafix.Worklist"+-- only have to provide an interpreter for 'MonadDependency'.++module Datafix.FrameworkBuilder+  ( FrameworkBuilder+  , buildFramework+  ) where++import           Data.Primitive.Array+import           Datafix.Common+import           Datafix.Denotational+import           Datafix.Explicit+import           Datafix.NodeAllocator++-- | Constructs a build plan for a 'DataFlowFramework' by tracking allocation of+-- 'Node's mapping to 'ChangeDetector's and transfer functions.+newtype FrameworkBuilder m a+  = FrameworkBuilder { unwrapFB :: NodeAllocator (ChangeDetector (Domain m), LiftedFunc (Domain m) m) a }+  deriving (Functor, Applicative, Monad)++instance MonadDependency m => MonadDatafix (FrameworkBuilder m) where+  type DepM (FrameworkBuilder m) = m+  datafix cd func = FrameworkBuilder $ allocateNode $ \node -> do+    let deref = dependOn @m node+    (ret, transfer) <- unwrapFB (func deref)+    return (ret, (cd, transfer))++-- | @(root, max, dff) = buildFramework builder@ executes the build plan specified+-- by @builder@ and returns the resulting 'DataFlowFramework' @dff@, as well as+-- the @root@ 'Node' denoting the transfer function returned by the+-- 'FrameworkBuilder' action and the @max@imum node of the problem as a proof for+-- its denseness.+buildFramework+  :: forall m a+   . MonadDependency m+  => (forall md . (MonadDatafix md, DepM md ~ m) => md a)+  -> (a, Node, DataFlowFramework m)+buildFramework plan = (a, Node (sizeofArray arr - 1), prob)+  where+    prob = DFF (snd . indexArray arr . unwrapNode) (fst . indexArray arr . unwrapNode)+    (a, arr) = runAllocator $ unwrapFB $ plan @(FrameworkBuilder m)

@@ -4,7 +4,7 @@  -- | -- Module      :  Datafix.IntArgsMonoMap--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -4,7 +4,7 @@  -- | -- Module      :  Datafix.IntArgsMonoSet--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -1,11 +1,10 @@ {-# LANGUAGE DefaultSignatures      #-} {-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE TypeFamilyDependencies #-}  -- | -- Module      :  Datafix.MonoMap--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -2,7 +2,7 @@  -- | -- Module      :  Datafix.NodeAllocator--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -1,63 +0,0 @@-{-# LANGUAGE FlexibleContexts           #-}-{-# LANGUAGE FlexibleInstances          #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE MultiParamTypeClasses      #-}-{-# LANGUAGE RankNTypes                 #-}-{-# LANGUAGE ScopedTypeVariables        #-}-{-# LANGUAGE TypeApplications           #-}-{-# LANGUAGE TypeFamilies               #-}---- |--- Module      :  Datafix.ProblemBuilder--- Copyright   :  (c) Sebastian Graf 2018--- License     :  ISC--- Maintainer  :  sgraf1337@gmail.com--- Portability :  portable------ Builds a 'DataFlowProblem' for a 'Denotation'al formulation in terms of--- 'MonadDatafix'. Effectively reduces descriptions from "Datafix.Denotational"--- to ones from "Datafix.Explicit", so that solvers such as "Datafix.Worklist"--- only have to provide an interpreter for 'MonadDependency'.--module Datafix.ProblemBuilder-  ( ProblemBuilder-  , buildProblem-  ) where--import           Data.Primitive.Array-import           Datafix.Common-import           Datafix.Denotational-import           Datafix.Entailments-import           Datafix.Explicit-import           Datafix.NodeAllocator-import           Datafix.Utils.Constraints---- | 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 (ProblemBuilder m) where-  type DepM (ProblemBuilder m) = m-  datafix cd func = ProblemBuilder $ allocateNode $ \node -> do-    let deref = dependOn @m node-    (ret, transfer) <- unwrapProblemBuilder (func deref)-    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-  => Denotation (Domain m)-  -> (Node, Node, DataFlowProblem m)-buildProblem buildDenotation = (root, Node (sizeofArray arr - 1), prob)-  where-    prob = DFP (snd . indexArray arr . unwrapNode) (fst . indexArray arr . unwrapNode)-    (root, arr) = runAllocator $ allocateNode $ \root_ -> do-      denotation <- unwrapProblemBuilder (buildDenotation @(ProblemBuilder m))-      return (root_, (alwaysChangeDetector @(Domain m) \\ cdInst @(Domain m), denotation))

@@ -2,7 +2,7 @@  -- | -- Module      :  Datafix.Tutorial--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable@@ -15,8 +15,8 @@ -- [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)+-- within GHC for my master's thesis. I+-- [held a talk](https://cdn.jsdelivr.net/gh/sgraf812/hiw17@master/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@@ -114,11 +114,11 @@ -- 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':+-- of 'Natural's) in place, we can construct a 'DataFlowFramework': -- -- >>> :{---   fibDfp :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowProblem m---   fibDfp = DFP transferFib (const (eqChangeDetector @(Domain m)))+--   fibDff :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+--   fibDff = DFF transferFib (const (eqChangeDetector @(Domain m))) -- :} -- -- The 'eqChangeDetector' is important for cyclic dependency graphs and makes@@ -137,7 +137,7 @@ -- -- And now the final incantation of the solver: ----- >>> solveProblem fibDfp Sparse NeverAbort (Node 10)+-- >>> solveProblem fibDff Sparse NeverAbort (dependOn @(DependencyM _ Natural) (Node 10)) -- 55 -- -- This will also execute in \(\mathcal{O}(n)\) space and time, all without@@ -196,8 +196,8 @@ -- :} -- -- >>> :{---   fDfp :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowProblem m---   fDfp = DFP transferF (const (eqChangeDetector @(Domain m)))+--   fDff :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowFramework m+--   fDff = DFF transferF (const (eqChangeDetector @(Domain m))) -- :} -- -- Specification of the data-flow problem works the same as for the 'fib'@@ -211,13 +211,13 @@ -- -- Now it's just a matter of calling 'solveProblem' with the right parameters: ----- >>> solveProblem fDfp Sparse NeverAbort (Node 0)+-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node 0)) -- 0--- >>> solveProblem fDfp Sparse NeverAbort (Node 5)+-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node 5)) -- 5--- >>> solveProblem fDfp Sparse NeverAbort (Node 42)+-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node 42)) -- 42--- >>> solveProblem fDfp Sparse NeverAbort (Node (-10))+-- >>> solveProblem fDff Sparse NeverAbort (dependOn @(DependencyM _ Int) (Node (-10))) -- -10 -- -- Note how the /specification/ of the data-flow problem was as unexciting as@@ -264,6 +264,17 @@ -- 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 :)+--+-- = Comparison to Datalog/Soufflé+--+-- In its most declarative form, @datafix@ is an embedded DSL for specifying+-- static analyses. In that regard, it is really similar to+-- [Soufflé](https://souffle-lang.github.io/index.html), only that Soufflé uses+-- an external DSL (a Datalog dialect) to specify the analysis. The resulting+-- compiled executable needs to run in a separate process and gets the facts of+-- the input program encoded in datalog facts. @datafix@ analyses, on the other+-- hand, will be compiled into the host program and don't need an additional+-- communication layer.  module Datafix.Tutorial () where 

@@ -13,7 +13,7 @@  -- | -- Module      :  Datafix.Utils.Constraints--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -1,6 +1,6 @@ -- | -- Module      :  Datafix.GrowableVector--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -9,7 +9,6 @@ {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE GADTs                 #-}-{-# LANGUAGE KindSignatures        #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds             #-} {-# LANGUAGE ScopedTypeVariables   #-}@@ -22,7 +21,7 @@  -- | -- Module      :  Datafix.Utils.TypeLevel--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -1,12 +1,12 @@ -- | -- Module      :  Datafix.Worklist--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- 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.+-- 'Datafix.Description.DataFlowFramework' by employing a worklist algorithm. -- There's also an interpreter for 'Denotation'al problems in the form of -- 'Denotational.evalDenotation'. 

@@ -4,15 +4,16 @@ {-# LANGUAGE RankNTypes            #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeApplications      #-}  -- | -- Module      :  Datafix.Worklist.Denotational--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable ----- Bridges the "Datafix.Worklist" solver for 'DataFlowProblem's ('solveProblem')+-- Bridges the "Datafix.Worklist" solver for 'DataFlowFramework's ('solveProblem') -- with the "Datafix.Denotational" approach, using 'MonadDatafix' to describe -- a 'Denotation'. @@ -22,26 +23,37 @@  import           Datafix.Common import           Datafix.Denotational-import           Datafix.ProblemBuilder+import           Datafix.Entailments+import           Datafix.Utils.Constraints+import           Datafix.Utils.TypeLevel+import           Datafix.FrameworkBuilder+import qualified Datafix.Worklist.Graph.Dense     as DenseGraph import           Datafix.Worklist.Internal+import           Data.Type.Equality  -- | @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@+-- It does so by building up the 'DataFlowFramework' 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.+-- the 'IterationBound' @ib@, domain ~ Domain (DepM m) is for. evalDenotation-  :: Datafixable domain-  => Denotation domain+  :: forall domain func+   . Datafixable domain+  => Forall (Currying (ParamTypes func))+  => Denotation domain func   -- ^ 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+  -> func+evalDenotation plan ib =+  castWith arrowsAxiom (currys @(ParamTypes func) @(ReturnType func) impl \\ idInst @func)+    where+      impl :: Products (ParamTypes func) -> ReturnType func+      impl args = solveProblem prob (Dense max_) ib (uncurriedDenot args)+      uncurriedDenot = uncurrys @(ParamTypes func) denot \\ lfInst @func @(DependencyM DenseGraph.Ref domain)+      (denot, max_, prob) = buildFramework plan {-# INLINE evalDenotation #-}

@@ -5,7 +5,7 @@  -- | -- Module      :  Datafix.Worklist.Graph--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -3,7 +3,7 @@  -- | -- Module      :  Datafix.Worklist.Graph--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -3,7 +3,7 @@  -- | -- Module      :  Datafix.Worklist.Graph--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable

@@ -13,7 +13,7 @@  -- | -- Module      :  Datafix.Worklist.Internal--- Copyright   :  (c) Sebastian Graf 2018+-- Copyright   :  (c) Sebastian Graf 2017-2020 -- License     :  ISC -- Maintainer  :  sgraf1337@gmail.com -- Portability :  portable@@ -30,9 +30,7 @@ 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           Data.Maybe                       (listToMaybe, mapMaybe) import           Datafix.Common import           Datafix.Entailments import           Datafix.Explicit                 hiding (dependOn)@@ -51,7 +49,7 @@ -- | 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+-- 'DataFlowFramework' 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)@@ -60,14 +58,15 @@   --   -- 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 domain => (forall s. DataFlowProblem (DependencyM s graph domain)) -> ...@+  -- @(forall s. Datafixable domain => (forall s. DataFlowFramework (DependencyM s graph domain)) -> ...@   -- and have to instead have the isomorphic-  -- @(forall s r. (Datafixable domain => r) -> r) -> (forall s. DataFlowProblem (DependencyM s graph domain)) -> ...@+  -- @(forall s r. (Datafixable domain => r) -> r) -> (forall s. DataFlowFramework (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.+  -- touches it, e.g. @Analyses.StrAnal.LetDn.buildDenotation@ 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@@ -77,7 +76,7 @@ -- | The iteration state of 'DependencyM'/'solveProblem'. data Env graph domain   = Env-  { problem          :: !(DataFlowProblem (DependencyM graph domain))+  { problem          :: !(DataFlowFramework (DependencyM graph domain))   -- ^ Constant.   -- The specification of the data-flow problem we ought to solve.   , iterationBound   :: !(IterationBound domain)@@ -100,7 +99,7 @@  initialEnv   :: IntArgsMonoSet (Products (ParamTypes domain))-  -> DataFlowProblem (DependencyM graph domain)+  -> DataFlowFramework (DependencyM graph domain)   -> IterationBound domain   -> IO (graph domain)   -> IO (Env graph domain)@@ -115,7 +114,7 @@ instance Datafixable domain => MonadDomain (DependencyM graph domain) where   type Domain (DependencyM graph domain) = domain --- | This allows us to solve @MonadDependency m => DataFlowProblem m@ descriptions+-- | This allows us to solve @MonadDependency m => DataFlowFramework m@ descriptions -- with 'solveProblem'. instance (Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) where   dependOn = dependOn @domain @graph@@ -270,9 +269,9 @@ 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 DM iterate' = uncurrys @dom @(depm cod) (dffTransfer prob node') args                   \\ lfInst @domain @depm-  let detectChange' = uncurrys @dom @(cod -> cod -> Bool) (dfpDetectChange prob node') args+  let detectChange' = uncurrys @dom @(cod -> cod -> Bool) (dffDetectChange prob node') args                     \\ cdInst @domain   -- We need to access the graph at three different points in time:   --@@ -435,55 +434,54 @@ work = whileJust_ highestPriorityUnstableNode (uncurry recompute) {-# INLINE work #-} --- | Computes a solution to the described 'DataFlowProblem' by iterating--- transfer functions until a fixed-point is reached.+-- | Computes the (pure) solution of the 'DependencyM' action @act@ specified in+-- the last parameter. @act@ may reference (via 'dependOn') 'Node's of the+-- 'DataFlowFramework' @dff@'s fixed-point, specified as the first parameter. ----- 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.+-- @dff@'s fixed-point is determined by its transfer functions, and+-- @solveProblem@ will make sure that all (relevant) 'Node's will have reached+-- their fixed-point according to their transfer function before computing the+-- solution for @act@. ----- 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.+-- We try to be smart in saving unnecessary iterations of transfer functions by+-- employing a worklist algorithm. For function domains, where each Node denotes+-- a monotone function, each point's dependencies' will be tracked individually. ----- 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.+-- Apart from @dff@ and @act@, the 'Density' of the data-flow graph and the+-- 'IterationBound' can be specified. Pass 'Sparse' and 'NeverAbort' when in+-- doubt.+--+-- If your problem only has finitely many different 'Node's , consider using the+-- 'FrameworkBuilder' 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.+--+-- See "Datafix.Tutorial" and the @examples/@ subfolder for examples. solveProblem-  :: forall domain graph+  :: forall domain graph a    . GraphRef graph   => Datafixable domain-  => DataFlowProblem (DependencyM graph domain)-  -- ^ The description of the @DataFlowProblem@ to solve.+  => DataFlowFramework (DependencyM graph domain)+  -- ^ The description of the @DataFlowFramework@.   -> 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 \\ idInst @domain)-    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+  -> DependencyM graph domain a+  -- ^ The action for which we want to compute the solution. May reference+  -- 'Node's from the @DataFlowFramework@. If you just want to know the value of+  -- 'Node' 42, use `dependOn @(DependecyM _ domain) (Node 42)`.+  -> a+solveProblem prob density ib (DM act) = 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.empty prob ib newGraphRef+  -- Run act once to discover dependencies and an additional time when all+  -- values reached a fixed-point.+  runReaderT (act >> work >> act) env {-# INLINE solveProblem #-}

@@ -9,33 +9,14 @@ # 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:-- '.'+resolver: lts-13.30  # 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+- cabal-toolkit-0.0.7+- cabal-doctest-1.0.8+- pomaps-0.2.0.0  allow-newer: true 

@@ -7,8 +7,6 @@  import           Algebra.Lattice import           Datafix-import           Datafix.Worklist       (Density (..), IterationBound (..),-                                         solveProblem) import           Datafix.Worklist.Graph (GraphRef) import           Numeric.Natural import           Test.Tasty@@ -20,11 +18,10 @@ 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)+fixLoop density n = solveProblem loopFramework (density (Node 0)) NeverAbort (dependOn @(DependencyM _ Natural) (Node n))+fixDoubleDependency density n = solveProblem doubleDependencyFramework (density (Node 1)) NeverAbort (dependOn @(DependencyM _ Natural) (Node n))  tests :: [TestTree] tests =@@ -44,17 +41,17 @@           [ 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)+          [ testCase "stabilizes at or over 4" (assertBool ">= 4" $ solveProblem doubleDependencyFramework Sparse (AbortAfter 1 (+ 4)) (dependOn @(DependencyM _ Natural) (Node 0)) >= 4)           ]       ]   ] -mkDFP :: forall m . (Domain m ~ Natural) => (Node -> LiftedFunc Natural m) -> DataFlowProblem m-mkDFP transfer = DFP transfer (const (eqChangeDetector @(Domain m)))+mkDFF :: forall m . (Domain m ~ Natural) => (Node -> LiftedFunc Natural m) -> DataFlowFramework m+mkDFF transfer = DFF 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+loopFramework :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+loopFramework = mkDFF transfer   where     transfer (Node 0) = do -- stabilizes at 10       n <- dependOn @m (Node 0)@@ -68,8 +65,8 @@ -- 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+doubleDependencyFramework :: forall m . (MonadDependency m, Domain m ~ Natural) => DataFlowFramework m+doubleDependencyFramework = mkDFF transfer   where     transfer (Node 0) = do -- stabilizes at 4       n <- dependOn @m (Node 1)

@@ -0,0 +1,44 @@+{-# LANGUAGE FlexibleContexts #-}++module FirstFollow where++import           Prelude hiding (seq, exp)++import           SetRecurrences.FirstFollow+import qualified Data.Set as Set+import           Test.Tasty+import           Test.Tasty.HUnit++tests :: [TestTree]+tests =+  [ testGroup "Dyck"+      [ testFirst 3 dyck "S(S)" ["(((", "(()", "()", "()("]+      , testFollow 3 dyck 'S' ["###",")##",")((",")()","))#","))(",")))"]+      ]+  , testGroup "LL(1), not SLL(k)"+      [ testFirst 3 llsll "A" ["","a"]+      , testFollow 3 llsll 'A' ["ab#","b##"]+      ]+  , testGroup "empty"+      [ testFirst 3 emptyL "A" []+      , testFollow 3 emptyL 'A' ["###"]+      ]+  , testGroup "Left recursion"+      [ testFirst 3 leftrec "A" ["c","cab"]+      , testFollow 3 leftrec 'A' ["a##","aba"]+      ]+  ] where+      testFirst :: Int -> Grammar Char Char -> String -> [String] -> TestTree+      testFirst k gr seq exp =+        testCase ("First_" ++ show k ++ "('" ++ seq ++ "')") $+          first k gr (map (mkV gr) seq) @?= Set.fromList exp+      testFollow :: Int -> Grammar Char Char -> Char -> [String] -> TestTree+      testFollow k gr nt exp =+        testCase ("Follow_" ++ show k ++ "(" ++ show nt ++ ")") $+          follow k gr nt @?= Set.fromList (map (map mkWithEOF) exp)+      mkV gr v+        | elem v (terminals gr)    = T v+        | elem v (nonterminals gr) = NT v+        | otherwise                = error "not part of vocabulary"+      mkWithEOF '#' = EOF+      mkWithEOF c   = NoEOF c

@@ -1,5 +1,6 @@ import qualified Critical import qualified StrAnal+import qualified FirstFollow import           System.Environment import           Test.Tasty import qualified Trivial@@ -16,5 +17,8 @@         ]     , testGroup "Analyses"         [ testGroup "Strictness" StrAnal.tests+        ]+    , testGroup "Set recurrences"+        [ testGroup "First/Follow" FirstFollow.tests         ]     ]

@@ -1,13 +1,12 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeApplications    #-} {-# 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@@ -25,9 +24,9 @@  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)+fixFib density n = solveProblem fibFramework (density (Node n)) NeverAbort (dependOn @(DependencyM _ Natural) (Node n))+fixFac density n = solveProblem facFramework (density (Node n)) NeverAbort (dependOn @(DependencyM _ Natural) (Node n))+fixMutualRecursive density n = solveProblem mutualRecursiveFramework (density (Node 1)) NeverAbort (dependOn @(DependencyM _ Natural) (Node n))  tests :: [TestTree] tests =@@ -51,7 +50,7 @@           , 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)+          [ testCase "aborts after 5 updates with value 42" (solveProblem mutualRecursiveFramework Sparse (AbortAfter 5 (const 42)) (dependOn @(DependencyM _ Natural) (Node 1)) @?= 42)           ]       ]   ]

@@ -1,5 +1,9 @@-import System.FilePath.Glob+import Build_doctests import Test.DocTest+import System.Environment (unsetEnv)  main :: IO ()-main = glob "src/**/*.hs" >>= doctest+main = do+  unsetEnv "GHC_ENVIRONMENT"+  let args = flags ++ pkgs ++ module_sources+  doctest args