From 8d446a03052e89a8187f9792aee64c9d22973afd Mon Sep 17 00:00:00 2001
From: Christian Gram Kalhauge <chrg@dtu.dk>
Date: Tue, 20 Feb 2024 22:48:20 +0100
Subject: [PATCH] A step closer to a good solution
---
rtree-c/.hspec | 1 -
rtree-c/.hspec-failures | 1 +
rtree-c/develop.sh | 1 +
rtree-c/hie.yml | 6 +
rtree-c/package.yaml | 6 +-
rtree-c/rtree-c.cabal | 13 +-
rtree-c/src/ReduceC.hs | 510 +++++++++++-----------
rtree-c/test/cases/main/main.c | 3 +
rtree-c/test/cases/main/pp.c | 4 +
rtree-c/test/expected/main/pp.c | 4 +
rtree-c/test/expected/main/reduction/r0.c | 4 +
rtree-c/test/expected/main/reduction/r1.c | 1 +
rtree-c/test/src/ReduceCSpec.hs | 84 +++-
rtree/src/Data/RPath.hs | 6 +-
14 files changed, 391 insertions(+), 253 deletions(-)
create mode 100644 rtree-c/.hspec-failures
create mode 100755 rtree-c/develop.sh
create mode 100644 rtree-c/hie.yml
create mode 100644 rtree-c/test/cases/main/main.c
create mode 100644 rtree-c/test/cases/main/pp.c
create mode 100644 rtree-c/test/expected/main/pp.c
create mode 100644 rtree-c/test/expected/main/reduction/r0.c
create mode 100644 rtree-c/test/expected/main/reduction/r1.c
diff --git a/rtree-c/.hspec b/rtree-c/.hspec
index c2400d4..6e9b625 100644
--- a/rtree-c/.hspec
+++ b/rtree-c/.hspec
@@ -1,3 +1,2 @@
--failure-report .hspec-failures
---rerun
--rerun-all-on-success
diff --git a/rtree-c/.hspec-failures b/rtree-c/.hspec-failures
new file mode 100644
index 0000000..fc74144
--- /dev/null
+++ b/rtree-c/.hspec-failures
@@ -0,0 +1 @@
+FailureReport {failureReportSeed = 860042728, failureReportMaxSuccess = 100, failureReportMaxSize = 100, failureReportMaxDiscardRatio = 10, failureReportPaths = [(["ReduceC","test/expected/main/reduction"],"should validate all reductions"),(["ReduceC","test/expected/main/reduction"],"should not have changed")]}
\ No newline at end of file
diff --git a/rtree-c/develop.sh b/rtree-c/develop.sh
new file mode 100755
index 0000000..a661dcf
--- /dev/null
+++ b/rtree-c/develop.sh
@@ -0,0 +1 @@
+ghcid --command='cabal repl rtree-c-test' -r --reload=test/cases
diff --git a/rtree-c/hie.yml b/rtree-c/hie.yml
new file mode 100644
index 0000000..41aa90e
--- /dev/null
+++ b/rtree-c/hie.yml
@@ -0,0 +1,6 @@
+cradle:
+ cabal:
+ - path: "./src"
+ component: "lib:rtree-c"
+ - path: "./test/src"
+ component: "test:rtree-c-test"
diff --git a/rtree-c/package.yaml b/rtree-c/package.yaml
index 626ea07..9b4cfa2 100644
--- a/rtree-c/package.yaml
+++ b/rtree-c/package.yaml
@@ -16,6 +16,7 @@ dependencies:
- pretty-simple
- transformers
- language-c
+ - pretty
library:
source-dirs: src
@@ -36,7 +37,7 @@ executables:
- text
tests:
- rtree-test:
+ rtree-c-test:
source-dirs: test/src
main: Main.hs
dependencies:
@@ -46,3 +47,6 @@ tests:
- hspec-discover
- hspec-expectations-pretty-diff
- hspec-glitter
+ - directory
+ - filepath
+ - typed-process
diff --git a/rtree-c/rtree-c.cabal b/rtree-c/rtree-c.cabal
index 631e4ed..7253184 100644
--- a/rtree-c/rtree-c.cabal
+++ b/rtree-c/rtree-c.cabal
@@ -21,6 +21,7 @@ library
, containers
, language-c
, mtl
+ , pretty
, pretty-simple
, rtree
, transformers
@@ -54,10 +55,12 @@ executable rtree-c
, vector
default-language: Haskell2010
-test-suite rtree-test
+test-suite rtree-c-test
type: exitcode-stdio-1.0
main-is: Main.hs
other-modules:
+ ReduceCSpec
+ Spec
Paths_rtree_c
hs-source-dirs:
test/src
@@ -65,11 +68,19 @@ test-suite rtree-test
build-depends:
base >=4.9 && <5
, containers
+ , directory
+ , filepath
+ , hspec
+ , hspec-discover
+ , hspec-expectations-pretty-diff
+ , hspec-glitter
, language-c
, mtl
+ , pretty
, pretty-simple
, rtree
, rtree-c
, transformers
+ , typed-process
, vector
default-language: Haskell2010
diff --git a/rtree-c/src/ReduceC.hs b/rtree-c/src/ReduceC.hs
index 778e8c0..cfaebdf 100644
--- a/rtree-c/src/ReduceC.hs
+++ b/rtree-c/src/ReduceC.hs
@@ -6,265 +6,279 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
module ReduceC where
import Control.Monad.Reduce
-
-import qualified Data.Valuation as Val
-
-import Control.Applicative
-import Control.Monad.State
-import Control.Monad.Trans.Maybe
-import Data.Data
-import Data.Function
-import Data.Functor
-import qualified Data.Map.Strict as Map
-import Data.Maybe (catMaybes)
import qualified Language.C as C
-type Lab = C.Ident
-
-data LabInfo
- = Type [C.CDeclarationSpecifier C.NodeInfo]
-
-type CState = Map.Map Lab LabInfo
-
-reduceC :: (MonadReduce Lab m, MonadState CState m) => C.CTranslUnit -> m C.CTranslUnit
-reduceC (C.CTranslUnit es ni) = do
- es' <- collect reduceCExternalDeclaration es
- pure $ C.CTranslUnit es' ni
- where
- reduceCExternalDeclaration = \case
- C.CFDefExt fun -> do
- C.CFDefExt <$> reduce @C.CFunctionDef fun
- C.CDeclExt decl ->
- C.CDeclExt <$> reduce @C.CDeclaration decl
- a -> error (show a)
-
-identifiers :: forall a. (Data a) => a -> [Lab]
-identifiers d = case cast d of
- Just l -> [l]
- Nothing -> concat $ gmapQ identifiers d
-
-type Reducer m a = a -> m a
-
-class CReducible c where
- reduce :: (MonadReducePlus Lab m, MonadState CState m) => Reducer m (c C.NodeInfo)
-
-cDeclaratorIdentifiers :: C.CDeclarator C.NodeInfo -> (Maybe Lab, [Lab])
-cDeclaratorIdentifiers (C.CDeclr mi dd _ la _) =
- (mi, identifiers dd <> identifiers la)
-
-instance CReducible C.CFunctionDef where
- reduce (C.CFunDef spc dec cdecls smt ni) = do
- let (fn, ids) = cDeclaratorIdentifiers dec
- let requirements = identifiers spc <> identifiers cdecls <> ids
- case fn of
- Just fn' ->
- conditionalGivenThat requirements (Val.is fn')
- Nothing ->
- mapM_ (givenThat . Val.is) requirements
- smt' <- reduce @C.CStatement smt
- pure $ C.CFunDef spc dec cdecls smt' ni
-
-instance CReducible C.CDeclaration where
- reduce = \case
- C.CDecl spc@(C.CStorageSpec (C.CTypedef _) : rst) decl ni -> do
- decl' <-
- decl & collectNonEmpty' \case
- C.CDeclarationItem d Nothing Nothing -> do
- let (x, _) = cDeclaratorIdentifiers d
- case x of
- Just x' ->
- splitOn
- (Val.is x')
- ( do
- modify (Map.insert x' (Type rst))
- mzero
- )
- (pure $ C.CDeclarationItem d Nothing Nothing)
- Nothing ->
- pure $ C.CDeclarationItem d Nothing Nothing
- a -> error (show a)
- pure (C.CDecl spc decl' ni)
- C.CDecl spc@[C.CTypeSpec (C.CTypeDef i ni')] decl ni -> do
- x <- gets (Map.lookup i)
- case x of
- Just (Type rst) -> do
- decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers rst) decl
- pure $ C.CDecl rst decl' ni
- Nothing -> do
- decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers spc) decl
- pure $ C.CDecl spc decl' ni
- C.CDecl spc decl ni -> do
- decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers spc) decl
- pure $ C.CDecl spc decl' ni
- a -> error (show a)
- where
- reduceCDeclarationItem rq' = \case
- C.CDeclarationItem d i e -> do
- let (fn, reqs) = cDeclaratorIdentifiers d
- case fn of
- Just fn' ->
- conditionalGivenThat (rq' <> reqs) (Val.is fn')
- Nothing ->
- mapM_ (givenThat . Val.is) (rq' <> reqs)
-
- i' <- optional do
- liftMaybe i >>= reduce @C.CInitializer
- e' <- optional do
- liftMaybe e >>= reduce @C.CExpression
+data Context = Context
- pure (C.CDeclarationItem d i' e')
- a -> error (show a)
+class CReducible a where
+ reduceC :: (MonadReduce String m) => a -> m a
-instance CReducible C.CInitializer where
- reduce = \case
- C.CInitExpr e ni -> reduce @C.CExpression e <&> \e' -> C.CInitExpr e' ni
- C.CInitList (C.CInitializerList items) ni -> do
- collectNonEmpty' rmCInitializerListItem items <&> \items' ->
- C.CInitList (C.CInitializerList items') ni
+instance CReducible C.CTranslUnit where
+ reduceC (C.CTranslUnit es ni) = do
+ es' <- rList es
+ -- es' <- collect reduceCExternalDeclaration es
+ pure $ C.CTranslUnit es' ni
where
- rmCInitializerListItem (pds, is) = do
- pds' <- collect rmCPartDesignator pds
- is' <- reduce is
- pure (pds', is')
-
- rmCPartDesignator = \case
- a -> error (show a)
-
-instance CReducible C.CStatement where
- reduce = \case
- C.CCompound is cbi ni -> do
- cbi' <- collect (reduce @C.CCompoundBlockItem) cbi
- pure $ C.CCompound is cbi' ni
- C.CExpr e ni -> do
- e' <- optional do
- e' <- liftMaybe e
- reduce @C.CExpression e'
- pure $ C.CExpr e' ni
- C.CIf e s els ni -> do
- s' <- reduce s
- e' <- optional do
- reduce @C.CExpression e
- els' <- optional do
- els' <- liftMaybe els
- given >> reduce els'
- case (e', els') of
- (Nothing, Nothing) -> pure s'
- (Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
- (Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
- (Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
- C.CFor e1 e2 e3 s ni -> do
- reduce s <| do
- e1' <- reduce @C.CForInit e1
- e2' <- optional $ liftMaybe e2 >>= reduce @C.CExpression
- e3' <- optional $ liftMaybe e3 >>= reduce @C.CExpression
- s' <- reduce s
- pure $ C.CFor e1' e2' e3' s' ni
- C.CReturn e ni -> do
- e' <- traverse (fmap orZero reduce) e
- pure $ C.CReturn e' ni
- C.CBreak ni -> pure (C.CBreak ni)
- C.CCont ni -> pure (C.CCont ni)
- C.CLabel i s [] ni -> do
- -- todo fix attrs
- s' <- reduce s
- withFallback s' do
- givenThat (Val.is i)
- pure $ C.CLabel i s' [] ni
- C.CGoto i ni ->
- withFallback (C.CExpr Nothing ni) do
- givenThat (Val.is i)
- pure $ C.CGoto i ni
- C.CWhile e s dow ni -> do
- e' <- orZero (reduce @C.CExpression e)
- s' <- reduce s
- pure $ C.CWhile e' s' dow ni
- a -> error (show a)
-
-instance CReducible C.CForInit where
- reduce = \case
- C.CForDecl decl -> withFallback (C.CForInitializing Nothing) do
- C.CForDecl <$> reduce @C.CDeclaration decl
- C.CForInitializing n -> do
- C.CForInitializing <$> optional do
- n' <- liftMaybe n
- reduce @C.CExpression n'
-
-instance CReducible C.CExpression where
- reduce = \case
- C.CVar i ni -> do
- givenThat (Val.is i)
- pure $ C.CVar i ni
- C.CCall e es ni -> do
- e' <- reduce e
- es' <- traverse (fmap orZero reduce) es
- pure $ C.CCall e' es' ni
- C.CCond ec et ef ni -> do
- ec' <- reduce ec
- ef' <- reduce ef
- et' <- optional do
- et' <- liftMaybe et
- reduce et'
- pure $ C.CCond ec' et' ef' ni
- C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs ->
- pure $ C.CBinary o lhs rhs ni
- C.CUnary o elhs ni -> do
- lhs <- reduce elhs
- pure $ C.CUnary o lhs ni
- C.CConst c -> do
- -- TODO fix
- pure $ C.CConst c
- C.CCast cd e ni -> do
- -- TODO fix
- cd' <- reduce @C.CDeclaration cd
- e' <- reduce e
- pure $ C.CCast cd' e' ni
- C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
- pure $ C.CAssign op e1' e2' ni
- C.CIndex e1 e2 ni -> do
- e1' <- reduce e1
- e2' <- orZero (reduce e2)
- pure $ C.CIndex e1' e2' ni
- C.CMember e i b ni -> do
- givenThat (Val.is i)
- e' <- reduce e
- pure $ C.CMember e' i b ni
- C.CComma items ni -> do
- C.CComma <$> collectNonEmpty' reduce items <*> pure ni
- e -> error (show e)
- where
- onBothExpr elhs erhs = onBoth (reduce elhs) (reduce erhs)
-
-zeroExp :: C.CExpression C.NodeInfo
-zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
-
-withFallback :: (Alternative m) => a -> m a -> m a
-withFallback a ma = ma <|> pure a
-
-orZero :: (Alternative m) => m (C.CExpression C.NodeInfo) -> m (C.CExpression C.NodeInfo)
-orZero = withFallback zeroExp
-
-instance CReducible C.CCompoundBlockItem where
- reduce = \case
- C.CBlockStmt s ->
- C.CBlockStmt <$> do
- given >> reduce @C.CStatement s
- C.CBlockDecl d ->
- C.CBlockDecl <$> do
- reduce @C.CDeclaration d
- a -> error (show a)
+ rList (a : as) = rList as <| ((a :) <$> rList as)
+ rList [] = pure []
-mtry :: (Functor m) => MaybeT m a -> MaybeT m (Maybe a)
-mtry (MaybeT mt) = MaybeT (Just <$> mt)
+-- reduceCExternalDeclaration = \case
+-- C.CFDefExt fun -> do
+-- C.CFDefExt <$> reduce @C.CFunctionDef fun
+-- C.CDeclExt decl ->
+-- C.CDeclExt <$> reduce @C.CDeclaration decl
+-- [] -> error (show a)
-mlift :: (Applicative m) => Maybe a -> MaybeT m a
-mlift a = MaybeT (pure a)
+-- import Control.Monad.Reduce
+--
+-- import qualified Data.Valuation as Val
+--
+-- import Control.Applicative
+-- import Control.Monad.State
+-- import Control.Monad.Trans.Maybe
+-- import Data.Data
+-- import Data.Function
+-- import Data.Functor
+-- import qualified Data.Map.Strict as Map
+-- import Data.Maybe (catMaybes)
+-- import qualified Language.C as C
-munder :: (Monad m) => Maybe a -> (a -> MaybeT m b) -> MaybeT m b
-munder a mf = mlift a >>= mf
+-- type Lab = C.Ident
+--
+-- data LabInfo
+-- = Type [C.CDeclarationSpecifier C.NodeInfo]
+--
+-- type CState = Map.Map Lab LabInfo
+--
+-- reduceC :: (MonadReduce Lab m, MonadState CState m) => C.CTranslUnit -> m C.CTranslUnit
+-- reduceC (C.CTranslUnit es ni) = do
+-- es' <- collect reduceCExternalDeclaration es
+-- pure $ C.CTranslUnit es' ni
+-- where
+-- reduceCExternalDeclaration = \case
+-- C.CFDefExt fun -> do
+-- C.CFDefExt <$> reduce @C.CFunctionDef fun
+-- C.CDeclExt decl ->
+-- C.CDeclExt <$> reduce @C.CDeclaration decl
+-- a -> error (show a)
+--
+-- identifiers :: forall a. (Data a) => a -> [Lab]
+-- identifiers d = case cast d of
+-- Just l -> [l]
+-- Nothing -> concat $ gmapQ identifiers d
+--
+-- type Reducer m a = a -> m a
+--
+-- class CReducible c where
+-- reduce :: (MonadReducePlus Lab m, MonadState CState m) => Reducer m (c C.NodeInfo)
+--
+-- cDeclaratorIdentifiers :: C.CDeclarator C.NodeInfo -> (Maybe Lab, [Lab])
+-- cDeclaratorIdentifiers (C.CDeclr mi dd _ la _) =
+-- (mi, identifiers dd <> identifiers la)
+--
+-- instance CReducible C.CFunctionDef where
+-- reduce (C.CFunDef spc dec cdecls smt ni) = do
+-- let (fn, ids) = cDeclaratorIdentifiers dec
+-- let requirements = identifiers spc <> identifiers cdecls <> ids
+-- case fn of
+-- Just fn' ->
+-- conditionalGivenThat requirements (Val.is fn')
+-- Nothing ->
+-- mapM_ (givenThat . Val.is) requirements
+-- smt' <- reduce @C.CStatement smt
+-- pure $ C.CFunDef spc dec cdecls smt' ni
+--
+-- instance CReducible C.CDeclaration where
+-- reduce = \case
+-- C.CDecl spc@(C.CStorageSpec (C.CTypedef _) : rst) decl ni -> do
+-- decl' <-
+-- decl & collectNonEmpty' \case
+-- C.CDeclarationItem d Nothing Nothing -> do
+-- let (x, _) = cDeclaratorIdentifiers d
+-- case x of
+-- Just x' ->
+-- splitOn
+-- (Val.is x')
+-- ( do
+-- modify (Map.insert x' (Type rst))
+-- mzero
+-- )
+-- (pure $ C.CDeclarationItem d Nothing Nothing)
+-- Nothing ->
+-- pure $ C.CDeclarationItem d Nothing Nothing
+-- a -> error (show a)
+-- pure (C.CDecl spc decl' ni)
+-- C.CDecl spc@[C.CTypeSpec (C.CTypeDef i ni')] decl ni -> do
+-- x <- gets (Map.lookup i)
+-- case x of
+-- Just (Type rst) -> do
+-- decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers rst) decl
+-- pure $ C.CDecl rst decl' ni
+-- Nothing -> do
+-- decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers spc) decl
+-- pure $ C.CDecl spc decl' ni
+-- C.CDecl spc decl ni -> do
+-- decl' <- collectNonEmpty' (reduceCDeclarationItem $ identifiers spc) decl
+-- pure $ C.CDecl spc decl' ni
+-- a -> error (show a)
+-- where
+-- reduceCDeclarationItem rq' = \case
+-- C.CDeclarationItem d i e -> do
+-- let (fn, reqs) = cDeclaratorIdentifiers d
+-- case fn of
+-- Just fn' ->
+-- conditionalGivenThat (rq' <> reqs) (Val.is fn')
+-- Nothing ->
+-- mapM_ (givenThat . Val.is) (rq' <> reqs)
+--
+-- i' <- optional do
+-- liftMaybe i >>= reduce @C.CInitializer
+-- e' <- optional do
+-- liftMaybe e >>= reduce @C.CExpression
+--
+-- pure (C.CDeclarationItem d i' e')
+-- a -> error (show a)
+--
+-- instance CReducible C.CInitializer where
+-- reduce = \case
+-- C.CInitExpr e ni -> reduce @C.CExpression e <&> \e' -> C.CInitExpr e' ni
+-- C.CInitList (C.CInitializerList items) ni -> do
+-- collectNonEmpty' rmCInitializerListItem items <&> \items' ->
+-- C.CInitList (C.CInitializerList items') ni
+-- where
+-- rmCInitializerListItem (pds, is) = do
+-- pds' <- collect rmCPartDesignator pds
+-- is' <- reduce is
+-- pure (pds', is')
+--
+-- rmCPartDesignator = \case
+-- a -> error (show a)
+--
+-- instance CReducible C.CStatement where
+-- reduce = \case
+-- C.CCompound is cbi ni -> do
+-- cbi' <- collect (reduce @C.CCompoundBlockItem) cbi
+-- pure $ C.CCompound is cbi' ni
+-- C.CExpr e ni -> do
+-- e' <- optional do
+-- e' <- liftMaybe e
+-- reduce @C.CExpression e'
+-- pure $ C.CExpr e' ni
+-- C.CIf e s els ni -> do
+-- s' <- reduce s
+-- e' <- optional do
+-- reduce @C.CExpression e
+-- els' <- optional do
+-- els' <- liftMaybe els
+-- given >> reduce els'
+-- case (e', els') of
+-- (Nothing, Nothing) -> pure s'
+-- (Just e'', Nothing) -> pure $ C.CIf e'' s' Nothing ni
+-- (Nothing, Just x) -> pure $ C.CIf zeroExp s' (Just x) ni
+-- (Just e'', Just x) -> pure $ C.CIf e'' s' (Just x) ni
+-- C.CFor e1 e2 e3 s ni -> do
+-- reduce s <| do
+-- e1' <- reduce @C.CForInit e1
+-- e2' <- optional $ liftMaybe e2 >>= reduce @C.CExpression
+-- e3' <- optional $ liftMaybe e3 >>= reduce @C.CExpression
+-- s' <- reduce s
+-- pure $ C.CFor e1' e2' e3' s' ni
+-- C.CReturn e ni -> do
+-- e' <- traverse (fmap orZero reduce) e
+-- pure $ C.CReturn e' ni
+-- C.CBreak ni -> pure (C.CBreak ni)
+-- C.CCont ni -> pure (C.CCont ni)
+-- C.CLabel i s [] ni -> do
+-- -- todo fix attrs
+-- s' <- reduce s
+-- withFallback s' do
+-- givenThat (Val.is i)
+-- pure $ C.CLabel i s' [] ni
+-- C.CGoto i ni ->
+-- withFallback (C.CExpr Nothing ni) do
+-- givenThat (Val.is i)
+-- pure $ C.CGoto i ni
+-- C.CWhile e s dow ni -> do
+-- e' <- orZero (reduce @C.CExpression e)
+-- s' <- reduce s
+-- pure $ C.CWhile e' s' dow ni
+-- a -> error (show a)
+--
+-- instance CReducible C.CForInit where
+-- reduce = \case
+-- C.CForDecl decl -> withFallback (C.CForInitializing Nothing) do
+-- C.CForDecl <$> reduce @C.CDeclaration decl
+-- C.CForInitializing n -> do
+-- C.CForInitializing <$> optional do
+-- n' <- liftMaybe n
+-- reduce @C.CExpression n'
+--
+-- instance CReducible C.CExpression where
+-- reduce = \case
+-- C.CVar i ni -> do
+-- givenThat (Val.is i)
+-- pure $ C.CVar i ni
+-- C.CCall e es ni -> do
+-- e' <- reduce e
+-- es' <- traverse (fmap orZero reduce) es
+-- pure $ C.CCall e' es' ni
+-- C.CCond ec et ef ni -> do
+-- ec' <- reduce ec
+-- ef' <- reduce ef
+-- et' <- optional do
+-- et' <- liftMaybe et
+-- reduce et'
+-- pure $ C.CCond ec' et' ef' ni
+-- C.CBinary o elhs erhs ni -> onBothExpr elhs erhs \lhs rhs ->
+-- pure $ C.CBinary o lhs rhs ni
+-- C.CUnary o elhs ni -> do
+-- lhs <- reduce elhs
+-- pure $ C.CUnary o lhs ni
+-- C.CConst c -> do
+-- -- TODO fix
+-- pure $ C.CConst c
+-- C.CCast cd e ni -> do
+-- -- TODO fix
+-- cd' <- reduce @C.CDeclaration cd
+-- e' <- reduce e
+-- pure $ C.CCast cd' e' ni
+-- C.CAssign op e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
+-- pure $ C.CAssign op e1' e2' ni
+-- C.CIndex e1 e2 ni -> do
+-- e1' <- reduce e1
+-- e2' <- orZero (reduce e2)
+-- pure $ C.CIndex e1' e2' ni
+-- C.CMember e i b ni -> do
+-- givenThat (Val.is i)
+-- e' <- reduce e
+-- pure $ C.CMember e' i b ni
+-- C.CComma items ni -> do
+-- C.CComma <$> collectNonEmpty' reduce items <*> pure ni
+-- e -> error (show e)
+-- where
+-- onBothExpr elhs erhs = onBoth (reduce elhs) (reduce erhs)
+--
+-- zeroExp :: C.CExpression C.NodeInfo
+-- zeroExp = C.CConst (C.CIntConst (C.cInteger 0) C.undefNode)
+--
+-- withFallback :: (Alternative m) => a -> m a -> m a
+-- withFallback a ma = ma <|> pure a
+--
+-- orZero :: (Alternative m) => m (C.CExpression C.NodeInfo) -> m (C.CExpression C.NodeInfo)
+-- orZero = withFallback zeroExp
+--
+-- instance CReducible C.CCompoundBlockItem where
+-- reduce = \case
+-- C.CBlockStmt s ->
+-- C.CBlockStmt <$> do
+-- given >> reduce @C.CStatement s
+-- C.CBlockDecl d ->
+-- C.CBlockDecl <$> do
+-- reduce @C.CDeclaration d
+-- a -> error (show a)
diff --git a/rtree-c/test/cases/main/main.c b/rtree-c/test/cases/main/main.c
new file mode 100644
index 0000000..33c14ce
--- /dev/null
+++ b/rtree-c/test/cases/main/main.c
@@ -0,0 +1,3 @@
+int main() {
+ return 0;
+}
diff --git a/rtree-c/test/cases/main/pp.c b/rtree-c/test/cases/main/pp.c
new file mode 100644
index 0000000..905869d
--- /dev/null
+++ b/rtree-c/test/cases/main/pp.c
@@ -0,0 +1,4 @@
+int main()
+{
+ return 0;
+}
diff --git a/rtree-c/test/expected/main/pp.c b/rtree-c/test/expected/main/pp.c
new file mode 100644
index 0000000..905869d
--- /dev/null
+++ b/rtree-c/test/expected/main/pp.c
@@ -0,0 +1,4 @@
+int main()
+{
+ return 0;
+}
diff --git a/rtree-c/test/expected/main/reduction/r0.c b/rtree-c/test/expected/main/reduction/r0.c
new file mode 100644
index 0000000..905869d
--- /dev/null
+++ b/rtree-c/test/expected/main/reduction/r0.c
@@ -0,0 +1,4 @@
+int main()
+{
+ return 0;
+}
diff --git a/rtree-c/test/expected/main/reduction/r1.c b/rtree-c/test/expected/main/reduction/r1.c
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/rtree-c/test/expected/main/reduction/r1.c
@@ -0,0 +1 @@
+
diff --git a/rtree-c/test/src/ReduceCSpec.hs b/rtree-c/test/src/ReduceCSpec.hs
index 1fe5d64..31e87d2 100644
--- a/rtree-c/test/src/ReduceCSpec.hs
+++ b/rtree-c/test/src/ReduceCSpec.hs
@@ -1,3 +1,85 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE LambdaCase #-}
+
module ReduceCSpec where
-spec = pure ()
+import Control.Monad
+
+import System.Directory
+import System.FilePath
+import Test.Hspec
+
+import Test.Hspec.Glitter
+
+import qualified Language.C as C
+import qualified Text.PrettyPrint as P
+
+import Control.Monad.RTree (extract, iinputs)
+import Data.Functor
+import Data.RPath
+import qualified Language.C.System.GCC as C
+import ReduceC
+import System.Process.Typed
+
+spec :: Spec
+spec = do
+ cases <- runIO (listDirectory "test/cases")
+
+ forM_ cases \cname -> do
+ let cfrom = "test/cases" </> cname </> "main.c"
+ let expected = "test/expected" </> cname
+ onGlitterWith
+ (expected </> "pp.c")
+ (preproc cfrom)
+ do
+ it "should be valid" \(cf, _) ->
+ validate cf
+
+ it "should be parsed equally" \(cf, c) -> do
+ C.parseCFilePre cf >>= \case
+ Left err -> fail (show err)
+ Right c' -> c' $> () `shouldBe` c $> ()
+
+ describe "reduction" do
+ it "should extract itself" \(_, c) -> do
+ extract (reduceC c) `shouldBe` c
+
+ onGlitterWith
+ (expected </> "reduction")
+ ( \a () -> do
+ c <- parse cfrom
+ createDirectoryIfMissing True a
+ forM_ (take 20 $ iinputs (reduceC c)) \(i, c') -> do
+ let rfile = expected </> "reduction" </> "r" <> debugShow i <.> "c"
+ render rfile c'
+ pure a
+ )
+ do
+ it "should validate all reductions" \a -> do
+ listDirectory a >>= mapM_ \x ->
+ validate (a </> x)
+
+validate :: FilePath -> IO ()
+validate fp = do
+ ec <- runProcess (proc "clang" ["-o", "/dev/null", fp])
+ case ec of
+ ExitFailure _ -> fail ("could not validate " <> show fp)
+ ExitSuccess -> pure ()
+
+render :: FilePath -> C.CTranslUnit -> IO ()
+render cto c = do
+ createDirectoryIfMissing True (takeDirectory cto)
+ writeFile cto (P.render (C.pretty c) <> "\n")
+
+parse :: FilePath -> IO C.CTranslUnit
+parse cfrom = do
+ cf <- C.parseCFile (C.newGCC "clang") Nothing [] cfrom
+ case cf of
+ Left err -> fail (show err)
+ Right cf' -> pure cf'
+
+preproc :: FilePath -> FilePath -> () -> IO (FilePath, C.CTranslUnit)
+preproc cfrom cto _ = do
+ cf' <- parse cfrom
+ render cto cf'
+ pure (cfrom, cf')
diff --git a/rtree/src/Data/RPath.hs b/rtree/src/Data/RPath.hs
index 1018591..e3f2c46 100644
--- a/rtree/src/Data/RPath.hs
+++ b/rtree/src/Data/RPath.hs
@@ -11,6 +11,7 @@ module Data.RPath (
toPredicateDebug,
-- * Helpers
+ debugShow,
debugShowWithDepth,
) where
@@ -72,8 +73,11 @@ debugShowWithDepth rp i =
(map (bool '0' '1') . take (i + 1) . toChoiceList $ rp)
<> replicate (numberOfChoices rp - i - 1) '*'
+debugShow :: RPath -> String
+debugShow = map (bool '0' '1') . toChoiceList
+
instance Show RPath where
- show = show . map (bool '0' '1') . toChoiceList
+ show = show . debugShow
instance Read RPath where
readsPrec i s = [(fromString a, r) | (a, r) <- readsPrec i s]
--
GitLab