ersatz-viz (empty) → 0

raw patch · 4 files changed

+161/−0 lines, 4 filesdep +basedep +ersatzdep +ersatz-viz

Dependencies added: base, ersatz, ersatz-viz, lens, mtl, process-extras, text, unordered-containers

Files

• ersatz-viz.cabal +27/−0
• src/Ersatz/Bit/Display.hs +89/−0
• src/Ersatz/Internal/StableName.hs +23/−0
• test/Works.hs +22/−0

@@ -0,0 +1,27 @@+cabal-version: 3.8++name: ersatz-viz+version: 0+synopsis: draw circuit (DAG) for Ersatz.Bit+description:+  draw circuit (DAG) for Ersatz.Bit+  .+  example usage: see test/Works.hs+license: GPL-3.0-only+author: Johannes Waldmann+homepage: https://git.imn.htwk-leipzig.de/waldmann/ersatz-viz+  +library+  hs-source-dirs: src+  exposed-modules: Ersatz.Bit.Display+  other-modules: Ersatz.Internal.StableName+  build-depends: base < 4.24 , text, process-extras, unordered-containers,+    mtl, lens, ersatz+  default-language: GHC2021+  +test-suite works+  hs-source-dirs: test+  main-is: Works.hs+  type: exitcode-stdio-1.0+  build-depends: base, text, ersatz, ersatz-viz+  default-language: GHC2021

@@ -0,0 +1,89 @@+{-# language OverloadedStrings #-}+{-# language LambdaCase #-}++module Ersatz.Bit.Display where++import Ersatz.Bit (Bit(..))+import Ersatz.Internal.StableName+import Ersatz.Problem (runSAT')+import Control.Monad (void, forM, forM_)+import Control.Monad.RWS+import Data.HashMap.Lazy (HashMap)+import qualified Data.HashMap.Lazy as HashMap+import System.IO.Unsafe+import Control.Lens+import Data.Foldable (toList)+import Data.Text (Text)+import qualified Data.Text as T+import System.Process.Text+import System.Mem.StableName (StableName, makeStableName)+import Unsafe.Coerce (unsafeCoerce)+++display m = dot $ fst $ runSAT' m++dot b = void $ readProcessWithExitCode "dot" [ "-Tx11" ] $ toDot b++toDot :: Bit -> Text+toDot b = snd+  $ ( \ m -> evalRWS (do+       tell "digraph Bit {"+       tell "graph [ordering=\"out\"]"+       tell "node [style=\"plane\"]"+       m+       tell "}"+    ) () s0 )+  $ walk b++subs :: Bit -> [Bit]+subs b = case b of+  Not (And xs) -> toList xs+  And xs -> toList xs+  Xor a b -> [a,b]+  Mux a b c -> [a,b,c]+  Not a -> [a]+  Var {} -> []+  Run {} -> []++name :: Bit -> Text+name b = case b of+  Not (And {}) -> "nand"+  And {} -> "and"+  Xor {} -> "xor"+  Mux {} -> "mux"+  Not {} -> "not"+  Var l -> T.pack $ show l+  Run {} -> "run"++data State = State+  { _stableMap :: !(HashMap (StableName ()) Int)+  , _next :: !Int+  }++s0 :: State+s0 = State { _stableMap = HashMap.empty , _next = 0 }++stableMap :: Lens' State (HashMap (StableName ()) Int)+stableMap f (s@State {_stableMap = sm})+  = fmap (\ sm' -> s { _stableMap = sm'} ) (f sm)++next :: Lens' State Int+next f (s@State { _next = n })+  = fmap (\ n' -> s { _next = n' } ) (f n)+  +fresh :: RWST () Text State Identity Int+fresh = do this <- use next ; next += 1 ; return this++walk :: Bit -> RWST () Text State Identity Int+walk b = do+  let sn = unsafePerformIO (makeStableName' b)+  use (stableMap.at sn) >>= \ case+    Just n -> return n+    Nothing -> do+      this <- fresh+      stableMap.at sn ?= this+      cs <- forM (subs b) walk+      tell $ T.pack (show this) <> "[label=\"" <> name b <> "\"];"+      forM_ cs $ \ c -> do+        tell $ T.pack (show this) <> "->" <> T.pack (show c) <> ";"+      return this

@@ -0,0 +1,23 @@+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Internal.StableName+  ( StableName+  , makeStableName'+  ) where++import System.Mem.StableName (StableName, makeStableName)+import Unsafe.Coerce (unsafeCoerce)++makeStableName' :: a -> IO (StableName ())+makeStableName' a = a `seq` fmap coerceStableName (makeStableName a)+  where+    coerceStableName :: StableName a -> StableName ()+    coerceStableName = unsafeCoerce

@@ -0,0 +1,22 @@+import Prelude hiding (and,or,all,any,not,(&&),(||))+import Ersatz+import qualified Ersatz.Counting as C++import qualified Ersatz.Bit.Display as D+import Control.Monad (replicateM)+import qualified Data.Text.IO as T++-- | print dot expression to stdout+main :: IO ()+main = T.putStrLn $ D.toDot $ fst $ runSAT' mkBit++-- | render and display.+-- will open a window and block ghci,+-- hit 'q' in window to close window and unblock ghci.+run :: IO ()+run = D.display mkBit++mkBit :: MonadSAT s m => m Bit+mkBit = do+  xs <- replicateM 4 (exists @Bit)+  return $ C.exactly 1 xs