diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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 + } diff --git a/bench/Main.hs b/bench/Main.hs --- a/bench/Main.hs +++ b/bench/Main.hs @@ -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 diff --git a/datafix.cabal b/datafix.cabal --- a/datafix.cabal +++ b/datafix.cabal @@ -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 diff --git a/examples/Analyses/StrAnal/Analysis.hs b/examples/Analyses/StrAnal/Analysis.hs --- a/examples/Analyses/StrAnal/Analysis.hs +++ b/examples/Analyses/StrAnal/Analysis.hs @@ -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'. diff --git a/examples/Analyses/Templates/LetDn.hs b/examples/Analyses/Templates/LetDn.hs --- a/examples/Analyses/Templates/LetDn.hs +++ b/examples/Analyses/Templates/LetDn.hs @@ -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 diff --git a/examples/Fac.hs b/examples/Fac.hs --- a/examples/Fac.hs +++ b/examples/Fac.hs @@ -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 diff --git a/examples/Fib.hs b/examples/Fib.hs --- a/examples/Fib.hs +++ b/examples/Fib.hs @@ -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 diff --git a/examples/Mutual.hs b/examples/Mutual.hs --- a/examples/Mutual.hs +++ b/examples/Mutual.hs @@ -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 diff --git a/examples/SetRecurrences/FirstFollow.hs b/examples/SetRecurrences/FirstFollow.hs new file mode 100644 --- /dev/null +++ b/examples/SetRecurrences/FirstFollow.hs @@ -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' diff --git a/examples/SetRecurrences/FirstFollow/Main.hs b/examples/SetRecurrences/FirstFollow/Main.hs new file mode 100644 --- /dev/null +++ b/examples/SetRecurrences/FirstFollow/Main.hs @@ -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') + ] + diff --git a/examples/Sum.hs b/examples/Sum.hs --- a/examples/Sum.hs +++ b/examples/Sum.hs @@ -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 diff --git a/exprs/lambda.hs b/exprs/lambda.hs --- a/exprs/lambda.hs +++ b/exprs/lambda.hs @@ -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 = "" 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 = "" +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)) diff --git a/lattices/Algebra/Lattice.hs b/lattices/Algebra/Lattice.hs deleted file mode 100644 --- a/lattices/Algebra/Lattice.hs +++ /dev/null @@ -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 --- --- 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 --- a/src/Datafix.hs +++ b/src/Datafix.hs @@ -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 diff --git a/src/Datafix/Common.hs b/src/Datafix/Common.hs --- a/src/Datafix/Common.hs +++ b/src/Datafix/Common.hs @@ -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 + , (>> :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 + +( Functor f + => f arr + -> Products (ParamTypes arr) + -> f (ReturnType arr) +mfunc mfunc + where + app func = uncurrys @(ParamTypes arr) (castWith (sym arrowsAxiom) func) args diff --git a/src/Datafix/Denotational.hs b/src/Datafix/Denotational.hs --- a/src/Datafix/Denotational.hs +++ b/src/Datafix/Denotational.hs @@ -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)) diff --git a/src/Datafix/Entailments.hs b/src/Datafix/Entailments.hs --- a/src/Datafix/Entailments.hs +++ b/src/Datafix/Entailments.hs @@ -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 diff --git a/src/Datafix/Explicit.hs b/src/Datafix/Explicit.hs --- a/src/Datafix/Explicit.hs +++ b/src/Datafix/Explicit.hs @@ -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@: diff --git a/src/Datafix/FrameworkBuilder.hs b/src/Datafix/FrameworkBuilder.hs new file mode 100644 --- /dev/null +++ b/src/Datafix/FrameworkBuilder.hs @@ -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) diff --git a/src/Datafix/IntArgsMonoMap.hs b/src/Datafix/IntArgsMonoMap.hs --- a/src/Datafix/IntArgsMonoMap.hs +++ b/src/Datafix/IntArgsMonoMap.hs @@ -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 diff --git a/src/Datafix/IntArgsMonoSet.hs b/src/Datafix/IntArgsMonoSet.hs --- a/src/Datafix/IntArgsMonoSet.hs +++ b/src/Datafix/IntArgsMonoSet.hs @@ -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 diff --git a/src/Datafix/MonoMap.hs b/src/Datafix/MonoMap.hs --- a/src/Datafix/MonoMap.hs +++ b/src/Datafix/MonoMap.hs @@ -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 diff --git a/src/Datafix/NodeAllocator.hs b/src/Datafix/NodeAllocator.hs --- a/src/Datafix/NodeAllocator.hs +++ b/src/Datafix/NodeAllocator.hs @@ -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 diff --git a/src/Datafix/ProblemBuilder.hs b/src/Datafix/ProblemBuilder.hs deleted file mode 100644 --- a/src/Datafix/ProblemBuilder.hs +++ /dev/null @@ -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)) diff --git a/src/Datafix/Tutorial.hs b/src/Datafix/Tutorial.hs --- a/src/Datafix/Tutorial.hs +++ b/src/Datafix/Tutorial.hs @@ -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 diff --git a/src/Datafix/Utils/Constraints.hs b/src/Datafix/Utils/Constraints.hs --- a/src/Datafix/Utils/Constraints.hs +++ b/src/Datafix/Utils/Constraints.hs @@ -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 diff --git a/src/Datafix/Utils/GrowableVector.hs b/src/Datafix/Utils/GrowableVector.hs --- a/src/Datafix/Utils/GrowableVector.hs +++ b/src/Datafix/Utils/GrowableVector.hs @@ -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 diff --git a/src/Datafix/Utils/TypeLevel.hs b/src/Datafix/Utils/TypeLevel.hs --- a/src/Datafix/Utils/TypeLevel.hs +++ b/src/Datafix/Utils/TypeLevel.hs @@ -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 diff --git a/src/Datafix/Worklist.hs b/src/Datafix/Worklist.hs --- a/src/Datafix/Worklist.hs +++ b/src/Datafix/Worklist.hs @@ -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'. diff --git a/src/Datafix/Worklist/Denotational.hs b/src/Datafix/Worklist/Denotational.hs --- a/src/Datafix/Worklist/Denotational.hs +++ b/src/Datafix/Worklist/Denotational.hs @@ -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 #-} diff --git a/src/Datafix/Worklist/Graph.hs b/src/Datafix/Worklist/Graph.hs --- a/src/Datafix/Worklist/Graph.hs +++ b/src/Datafix/Worklist/Graph.hs @@ -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 diff --git a/src/Datafix/Worklist/Graph/Dense.hs b/src/Datafix/Worklist/Graph/Dense.hs --- a/src/Datafix/Worklist/Graph/Dense.hs +++ b/src/Datafix/Worklist/Graph/Dense.hs @@ -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 diff --git a/src/Datafix/Worklist/Graph/Sparse.hs b/src/Datafix/Worklist/Graph/Sparse.hs --- a/src/Datafix/Worklist/Graph/Sparse.hs +++ b/src/Datafix/Worklist/Graph/Sparse.hs @@ -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 diff --git a/src/Datafix/Worklist/Internal.hs b/src/Datafix/Worklist/Internal.hs --- a/src/Datafix/Worklist/Internal.hs +++ b/src/Datafix/Worklist/Internal.hs @@ -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 #-} diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -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 diff --git a/tests/Critical.hs b/tests/Critical.hs --- a/tests/Critical.hs +++ b/tests/Critical.hs @@ -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) diff --git a/tests/FirstFollow.hs b/tests/FirstFollow.hs new file mode 100644 --- /dev/null +++ b/tests/FirstFollow.hs @@ -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 diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -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 ] ] diff --git a/tests/Trivial.hs b/tests/Trivial.hs --- a/tests/Trivial.hs +++ b/tests/Trivial.hs @@ -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) ] ] ] diff --git a/tests/doctest.hs b/tests/doctest.hs --- a/tests/doctest.hs +++ b/tests/doctest.hs @@ -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