data-reify-gadt (empty) → 0.1.0.0

raw patch · 9 files changed

+429/−0 lines, 9 filesdep +basedep +containersdep +data-reify-gadtsetup-changed

Dependencies added: base, containers, data-reify-gadt, hashable, hspec, unordered-containers

Files

LICENSE +26/−0
README.md +9/−0
Setup.hs +3/−0
data-reify-gadt.cabal +96/−0
examples/ast.hs +54/−0
src/Data/Reify/GADT.hs +156/−0
src/Data/Reify/GADT/Graph.hs +22/−0
src/Lib.hs +6/−0
test/Spec.hs +57/−0

+ LICENSE view

@@ -0,0 +1,26 @@+Copyright 2025 Author name here++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1.  Redistributions of source code must retain the above copyright notice, this+    list of conditions and the following disclaimer.++2.  Redistributions in binary form must reproduce the above copyright notice,+    this list of conditions and the following disclaimer in the documentation+    and/or other materials provided with the distribution.++3.  Neither the name of the copyright holder nor the names of its contributors+    may be used to endorse or promote products derived from this software+    without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,9 @@+# `Data.Reify.GADT`++`data-reify-gadt` is a rewrite of [`data-reify`](https://hackage.haskell.org/package/data-reify) to make the library usable with GADTs.++With this implementation, it is possible to use `data-reify`'s technique to make a graph out of typed ASTs that uses GADTs.++The logic is the same, only the type definition changes slightly.++Take a look at the `examples/` directory.

+ Setup.hs view

@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain

+ data-reify-gadt.cabal view

@@ -0,0 +1,96 @@+cabal-version:      2.2+name:               data-reify-gadt+version:            0.1.0.0+license:            BSD-3-Clause+license-file:       LICENSE+copyright:          2025 Arthur Jamet+maintainer:         aj530@kent.ac.uk+author:             Arthur Jamet+tested-with:        ghc ==9.6.6 ghc ==9.8.4 ghc ==9.10.1 ghc ==9.12.1+homepage:           https://github.com/Arthi-chaud/data-reify-gadt#readme+bug-reports:        https://github.com/Arthi-chaud/data-reify-gadt/issues+synopsis:           Data.Reify for GADTs+description:+    Please see the README on GitHub at <https://github.com/Arthi-chaud/data-reify-gadt#readme>++category:           Data+build-type:         Simple+extra-source-files: README.md++source-repository head+    type:     git+    location: https://github.com/Arthi-chaud/data-reify-gadt++library+    exposed-modules:+        Data.Reify.GADT+        Data.Reify.GADT.Graph++    hs-source-dirs:     src+    other-modules:+        Lib+        Paths_data_reify_gadt++    autogen-modules:    Paths_data_reify_gadt+    default-language:   Haskell2010+    default-extensions:+        RankNTypes QuantifiedConstraints UndecidableInstances+        ExistentialQuantification TypeOperators++    ghc-options:+        -Wall -Wcompat -Widentities -Wincomplete-record-updates+        -Wincomplete-uni-patterns -Wmissing-export-lists+        -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints++    build-depends:+        base >=4.7 && <5,+        containers >=0.7 && <0.8,+        hashable >=1.5.0.0 && <1.6,+        unordered-containers >=0.2.20 && <0.3++executable example-ast+    main-is:            ast.hs+    hs-source-dirs:     examples+    other-modules:      Paths_data_reify_gadt+    autogen-modules:    Paths_data_reify_gadt+    default-language:   Haskell2010+    default-extensions:+        RankNTypes QuantifiedConstraints UndecidableInstances+        ExistentialQuantification TypeOperators++    ghc-options:+        -Wall -Wcompat -Widentities -Wincomplete-record-updates+        -Wincomplete-uni-patterns -Wmissing-export-lists+        -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints++    build-depends:+        base >=4.7 && <5,+        containers >=0.7 && <0.8,+        data-reify-gadt,+        hashable >=1.5.0.0 && <1.6,+        unordered-containers >=0.2.20 && <0.3++test-suite test+    type:               exitcode-stdio-1.0+    main-is:            Spec.hs+    hs-source-dirs:     test+    other-modules:      Paths_data_reify_gadt+    autogen-modules:    Paths_data_reify_gadt+    default-language:   Haskell2010+    default-extensions:+        RankNTypes QuantifiedConstraints UndecidableInstances+        ExistentialQuantification TypeOperators++    ghc-options:+        -Wall -Wcompat -Widentities -Wincomplete-record-updates+        -Wincomplete-uni-patterns -Wmissing-export-lists+        -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+        -threaded -rtsopts -with-rtsopts=-N++    build-depends:+        base >=4.7 && <5,+        containers >=0.7 && <0.8,+        data-reify-gadt,+        hashable >=1.5.0.0 && <1.6,+        hspec >=2.11.11 && <2.12,+        unordered-containers >=0.2.20 && <0.3

+ examples/ast.hs view

@@ -0,0 +1,54 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}++module Main (main) where++import Control.Monad+import Data.Reify.GADT+import Text.Printf++newtype Fix f a = Fx (f (Fix f) a)++-- Inspired by https://github.com/ku-fpg/data-reify/blob/master/examples/simplify.hs++data TreeF e a where+    Leaf :: (Show a) => a -> TreeF e a+    Node :: e a -> e a -> TreeF e a++type Tree = Fix TreeF++instance MuRef (Fix TreeF) where+    type DeRef (Fix TreeF) = TreeF+    type E (Fix TreeF) = Fix TreeF+    mapDeRef f (Fx e) = case e of+        Leaf a -> pure $ Leaf a+        Node l r -> Node <$> f l <*> f r++instance Show (TreeF Terminal f) where+    show e = case e of+        Leaf a -> "Leaf " ++ show a+        Node l r -> printf "Node (%s) (%s)" (show l) (show r)++-- Smart constructors++node :: Tree a -> Tree a -> Tree a+node l r = Fx $ Node l r++leaf :: (Show a) => a -> Tree a+leaf = Fx . Leaf++------++tree1 :: Tree Int+tree1 = node (node (leaf 1) tree1) tree2++tree2 :: Tree Int+tree2 = node tree1 (leaf 2)++main :: IO ()+main = do+    (Graph nodes root) <- reifyGraph tree1+    printf "Root: %d\n" root+    forM_ nodes $ \(u, MkNode n) -> do+        printf "%d: %s\n" u (show n)

+ src/Data/Reify/GADT.hs view

@@ -0,0 +1,156 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Data.Reify.GADT (+    MuRef (..),+    reifyGraph,+    reifyGraphs,+    module Data.Reify.GADT.Graph,+) where++import Control.Concurrent+import Data.HashMap.Lazy+import qualified Data.HashMap.Lazy as HM+import Data.Hashable+import Data.IntSet+import qualified Data.IntSet as IS+import Data.Kind+import Data.Reify.GADT.Graph+import System.Mem.StableName++-- | 'MuRef' is a class that provided a way to reference into a specific type,+-- and a way to map over the deferenced internals.+class MuRef (a :: Type -> Type) where+    type DeRef a :: (Type -> Type) -> (Type -> Type)+    type E a :: Type -> Type+    mapDeRef ::+        (Applicative f, e ~ E a) =>+        (forall t'. (MuRef e) => e t' -> f (u t')) ->+        a t ->+        f ((DeRef a) u t)++-- | 'reifyGraph' takes a data structure that admits 'MuRef', and returns a 'Graph' that contains+-- the dereferenced nodes, with their children as 'Unique's rather than recursive values.+reifyGraph ::+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s) =>+    s a ->+    IO (Graph (DeRef s) a)+reifyGraph m = do+    rt1 <- newMVar HM.empty+    uVar <- newMVar 0+    reifyWithContext rt1 uVar m++-- | 'reifyGraphs' takes a 'Traversable' container 't s' of a data structure 's'+-- admitting 'MuRef', and returns a 't (Graph (DeRef s))' with the graph nodes+-- resolved within the same context.+--+-- This allows for, e.g., a list of mutually recursive structures.+reifyGraphs ::+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s, Traversable t) =>+    t (s e) ->+    IO (t (Graph (DeRef s) e))+reifyGraphs coll = do+    rt1 <- newMVar HM.empty+    uVar <- newMVar 0+    traverse (reifyWithContext rt1 uVar) coll++-- NB: We deliberately reuse the same map of stable+-- names and unique supply across all iterations of the+-- traversal to ensure that the same context is used+-- when reifying all elements of the container.++-- Reify a data structure's 'Graph' using the supplied map of stable names and+-- unique supply.+reifyWithContext ::+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s) =>+    MVar (HashMap DynStableName Unique) ->+    MVar Unique ->+    s a ->+    IO (Graph (DeRef s) a)+reifyWithContext rt1 uVar j = do+    rt2 <- newMVar []+    nodeSetVar <- newMVar IS.empty+    Terminal root <- findNodes rt1 rt2 uVar nodeSetVar j+    pairs <- readMVar rt2+    return (Graph pairs root)++-- The workhorse for 'reifyGraph' and 'reifyGraphs'.+findNodes ::+    -- ‘DeRef (E (e t) t') ~ DeRef (e t')’+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s) =>+    -- | A map of stable names to unique numbers.+    --   Invariant: all 'Uniques' that appear in the range are less+    --   than the current value in the unique name supply.+    MVar (HashMap DynStableName Unique) ->+    -- | The key-value pairs in the 'Graph' that is being built.+    --   Invariant 1: the domain of this association list is a subset+    --   of the range of the map of stable names.+    --   Invariant 2: the domain of this association list will never+    --   contain duplicate keys.+    -- MVar [(Unique,DeRef s Unique)]+    MVar [(Unique, Node (DeRef s))] ->+    -- | A supply of unique names.+    MVar Unique ->+    -- | The unique numbers that we have encountered so far.+    --   Invariant: this set is a subset of the range of the map of+    --   stable names.+    MVar IntSet ->+    -- | The value for which we will reify a 'Graph'.+    s t ->+    -- | The unique number for the value above.+    IO (Terminal t)+findNodes rt1 rt2 uVar nodeSetVar !j = do+    st <- makeDynStableName j+    tab <- takeMVar rt1+    nodeSet <- takeMVar nodeSetVar+    case HM.lookup st tab of+        Just var -> do+            putMVar rt1 tab+            if var `IS.member` nodeSet+                then do+                    putMVar nodeSetVar nodeSet+                    return $ Terminal var+                else recurse var nodeSet+        Nothing -> do+            var <- newUnique uVar+            putMVar rt1 $ HM.insert st var tab+            recurse var nodeSet+  where+    recurse :: Unique -> IntSet -> IO (Terminal a)+    recurse var nodeSet = do+        putMVar nodeSetVar $ IS.insert var nodeSet+        res <- mapDeRef (findNodes rt1 rt2 uVar nodeSetVar) j+        tab' <- takeMVar rt2+        putMVar rt2 $ (var, MkNode res) : tab'+        return $ Terminal var++newUnique :: MVar Unique -> IO Unique+newUnique var = do+    v <- takeMVar var+    let v' = succ v+    putMVar var v'+    return v'++-- Stable names that do not use phantom types.+-- As suggested by Ganesh Sittampalam.+-- Note: GHC can't unpack these because of the existential+-- quantification, but there doesn't seem to be much+-- potential to unpack them anyway.+data DynStableName = forall a. DynStableName !(StableName a)++instance Hashable DynStableName where+    hashWithSalt s (DynStableName n) = hashWithSalt s n++instance Eq DynStableName where+    DynStableName m == DynStableName n =+        eqStableName m n++makeDynStableName :: a -> IO DynStableName+makeDynStableName a = do+    st <- makeStableName a+    return $ DynStableName st

+ src/Data/Reify/GADT/Graph.hs view

@@ -0,0 +1,22 @@+module Data.Reify.GADT.Graph (+    Unique,+    Node (..),+    Graph (..),+    Terminal (..),+) where++-- 'Label' for a node in the graph+type Unique = Int++data Node e = forall t. MkNode (e Terminal t)++instance (forall t. Show (e Terminal t)) => Show (Node e) where+    show (MkNode e) = show e++data Graph e a = Graph [(Unique, Node e)] Unique++-- An AST node that refers to a Graph Node+newtype Terminal a = Terminal {unTerminal :: Unique}++instance Show (Terminal a) where+    show (Terminal a) = "Terminal " ++ show a

+ src/Lib.hs view

@@ -0,0 +1,6 @@+module Lib (+    someFunc,+) where++someFunc :: IO ()+someFunc = putStrLn "someFunc"

+ test/Spec.hs view

@@ -0,0 +1,57 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}++import Data.Reify.GADT+import Test.Hspec+import Unsafe.Coerce++data ExprF e a where+    Val :: a -> ExprF e a+    Dup :: e a -> ExprF e (a, a)+    Pair :: e a -> e b -> ExprF e (a, b)+    Fst :: e (a, b) -> ExprF e a+    Snd :: e (a, b) -> ExprF e b+    Max :: (Ord a) => e a -> e a -> ExprF e a++newtype Fix f a = Fx (f (Fix f) a)++instance MuRef (Fix ExprF) where+    type DeRef (Fix ExprF) = ExprF+    type E (Fix ExprF) = Fix ExprF+    mapDeRef f (Fx e) = case e of+        Val a -> pure $ Val a+        Dup a -> Dup <$> f a+        Pair a b -> Pair <$> f a <*> f b+        Fst a -> Fst <$> f a+        Snd a -> Snd <$> f a+        Max a b -> Max <$> f a <*> f b++ast :: Fix ExprF Int+ast = Fx $ Max (Fx (Val (2 :: Int))) (Fx $ Snd $ Fx $ Pair ast (Fx $ Val 1))++evalGraph :: Graph (DeRef (Fix ExprF)) a -> a+evalGraph g@(Graph _ root) = evalNode g $ Terminal root++evalNode :: Graph (DeRef (Fix ExprF)) b -> Terminal a -> a+evalNode g@(Graph nodes _) (Terminal u) = case lookup u nodes of+    Nothing -> error "Node not found"+    Just (MkNode e) -> case unsafeCoerce e :: ExprF Terminal a of+        Val a -> a+        Dup a -> let res = evalNode g a in (res, res)+        Pair a b -> (evalNode g a, evalNode g b)+        Fst a -> fst $ evalNode g a+        Snd a -> snd $ evalNode g a+        Max a b -> max (evalNode g a) (evalNode g b)++specs :: Spec+specs = describe "Data.Reify.GADT" $ do+    describe "reifyGraph" $ do+        it "Compute and eval graph" $ do+            g@(Graph nodes root) <- reifyGraph ast+            root `shouldBe` 1+            length nodes `shouldBe` 5+            evalGraph g `shouldBe` 2++main :: IO ()+main = hspec specs