diff --git a/bin/rtree-c/Main.hs b/bin/rtree-c/Main.hs index 629be3f15d5d96d4454a5c3450d1f8aee2d496b5..727b715ab1eb6c1a63a6b6cbfe6da05dfffc7e86 100644 --- a/bin/rtree-c/Main.hs +++ b/bin/rtree-c/Main.hs @@ -3,7 +3,6 @@ {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} import Control.RTree @@ -50,44 +49,74 @@ process sev p ma = do run :: (HasCallStack) => Parser (IO ()) run = do - file <- strArgument $ fold [metavar "FILE"] + expmode <- + flag False True + $ fold + [ long "exp" + , help "run in exponential mode" + ] validity <- - flag False True + optional + $ strOption $ fold [ long "validity" - , help "check for validity, throw error if command fails" + , short 'v' + , help "check every output for validity" ] - expmode <- + pedandic <- flag False True $ fold - [ long "exp" - , help "run in exponential mode" + [ long "pedandic" + , short 'P' + , help "when checking for validity, throw error if command fails" ] + debug <- + flag False True + $ fold + [ long "debug" + , help "enable debugging" + ] + + cmd <- strArgument $ fold [metavar "COMMAND"] + + file <- strArgument $ fold [metavar "FILE"] pure $ usingLoggerT (cmap fmtMessage logTextStdout) $ do let test f = process D ("test " <> Text.pack f) do - err <- liftIO $ runProcess (proc "clang" ["-O0", file]) + err <- liftIO $ runProcess cmd log D (Text.pack $ show err) pure (err == ExitSuccess) + validiate f = case validity of + Just vcmd -> process D ("validiate " <> Text.pack f) do + err <- liftIO $ runProcess vcmd + log D (Text.pack $ show err) + pure (err == ExitSuccess) + Nothing -> pure True + output f c = process D ("writing " <> Text.pack f) do let x = P.render (C.pretty (c $> C.undefNode)) liftIO $ writeFile f x - check' f c = do - when validity do + check' f val c = do + logInfo "Checking predictate" + when debug do + pPrint [(void k, v) | (k, v) <- Map.toList val] + pPrint (void c) + when pedandic do liftIO $ copyFile file (file <.> "last") output f c - t <- test f - if t - then pure True + v <- validiate f + if v + then test f else do - liftIO $ when validity do + logWarning "Produced invalid code" + liftIO $ when pedandic do copyFile file (file <.> "fail") copyFile (file <.> "last") file exitFailure @@ -98,14 +127,24 @@ run = do process D "backing up file" do liftIO $ copyFile file bak + process I "validiating" do + v <- validiate file + unless v do + logError "did not validiate program" + liftIO exitFailure + process I "check predicate" do t <- test file unless t do + logError "did not satisify predicate" liftIO exitFailure c <- process D "parsing file" do parseCFile file + when debug do + pPrint (void c) + output file c process I "sanity checks" do diff --git a/bin/rtree-c/ReduceC.hs b/bin/rtree-c/ReduceC.hs index 0a4fea667561bb1165f6a3c19e764cfb27a8ea2c..90fde902bad3274ce917780859280d37ada1d643 100644 --- a/bin/rtree-c/ReduceC.hs +++ b/bin/rtree-c/ReduceC.hs @@ -12,6 +12,7 @@ import Control.Monad.Reduce import Control.Applicative import Control.Monad.Trans import Control.Monad.Trans.Maybe +import Data.Foldable import Data.Functor import Data.Maybe import qualified Language.C as C @@ -26,24 +27,92 @@ reduceC (C.CTranslUnit es ni) = do mrCExternalDeclaration :: (MonadReduce Lab m) => C.CExternalDeclaration C.NodeInfo -> MaybeT m (C.CExternalDeclaration C.NodeInfo) mrCExternalDeclaration = \case C.CFDefExt fun -> do - givenWith (funName fun) - C.CFDefExt <$> rCFunctionDef fun + C.CFDefExt <$> mrCFunctionDef fun C.CDeclExt decl -> C.CDeclExt <$> mrCDeclaration decl a -> error (show a) - where - funName (C.CFunDef _ (C.CDeclr x _ _ _ _) _ _ _) = - x + +mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo) +mrCDeclaration = \case + C.CDecl spc decl ni -> do + mapM_ cCDeclarationSpecifier spc + decl' <- lift $ collect mrCDeclarationItem decl + case decl' of + [] -> empty + decl'' -> pure $ C.CDecl spc decl'' ni + a -> error (show a) mrCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m (C.CDeclarationItem C.NodeInfo) mrCDeclarationItem = \case - C.CDeclarationItem d@(C.CDeclr x _ _ _ _) i e -> do - givenWith x + C.CDeclarationItem d i e -> do i' <- mtry $ munder i mrCInitializer e' <- mtry $ munder e mrCExpression + cCDeclr d pure (C.CDeclarationItem d i' e') a -> error (show a) +cCDeclarationItem :: (MonadReduce Lab m) => C.CDeclarationItem C.NodeInfo -> MaybeT m () +cCDeclarationItem = \case + C.CDeclarationItem d i e -> do + munder i cCInitializer + munder e cCExpression + cCDeclr d + a -> error (show a) + +cCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m () +cCDeclaration = \case + C.CDecl spc decl _ -> do + forM_ spc cCDeclarationSpecifier + mapM_ cCDeclarationItem decl + a -> error (show a) + +cCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m () +cCExpression e = + -- TODO not optimal, create version that only checks for identifiers . + void $ mrCExpression e + +cCDeclarationSpecifier :: (MonadReduce Lab m) => C.CDeclarationSpecifier C.NodeInfo -> MaybeT m () +cCDeclarationSpecifier = \case + C.CTypeSpec t -> cCTypeSpecifier t + C.CStorageSpec _ -> pure () + C.CTypeQual t -> cCTypeQualifier t + C.CFunSpec _ -> pure () + C.CAlignSpec (C.CAlignAsType t _) -> cCDeclaration t + C.CAlignSpec (C.CAlignAsExpr t _) -> cCExpression t + +cCTypeQualifier :: (MonadReduce Lab m) => C.CTypeQualifier C.NodeInfo -> MaybeT m () +cCTypeQualifier = \case + C.CAttrQual a -> cCAttr a + _ -> pure () + +cCTypeSpecifier :: (MonadReduce Lab m) => C.CTypeSpecifier C.NodeInfo -> MaybeT m () +cCTypeSpecifier = \case + C.CVoidType _ -> pure () + C.CCharType _ -> pure () + C.CShortType _ -> pure () + C.CIntType _ -> pure () + C.CLongType _ -> pure () + C.CFloatType _ -> pure () + C.CDoubleType _ -> pure () + C.CSignedType _ -> pure () + C.CUnsigType _ -> pure () + C.CBoolType _ -> pure () + C.CComplexType _ -> pure () + C.CInt128Type _ -> pure () + -- C.CUInt128Type a -> pure () + C.CFloatNType{} -> pure () + C.CTypeDef i _ -> do + givenThat i + pure () + (C.CTypeOfExpr e _) -> cCExpression e + (C.CTypeOfType t _) -> cCDeclaration t + (C.CAtomicType t _) -> cCDeclaration t + a@(C.CSUType _ _) -> error (show a) + a@(C.CEnumType _ _) -> error (show a) + +cCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m () +cCInitializer = void . mrCInitializer + mrCInitializer :: (MonadReduce Lab m) => C.CInitializer C.NodeInfo -> MaybeT m (C.CInitializer C.NodeInfo) mrCInitializer = \case C.CInitExpr e ni -> mrCExpression e <&> \e' -> C.CInitExpr e' ni @@ -60,20 +129,38 @@ mrCInitializer = \case rmCPartDesignator = \case a -> error (show a) -mrCDeclaration :: (MonadReduce Lab m) => C.CDeclaration C.NodeInfo -> MaybeT m (C.CDeclaration C.NodeInfo) -mrCDeclaration = \case - C.CDecl spc decl ni -> do - decl' <- lift $ collect mrCDeclarationItem decl - case decl' of - [] -> empty - decl'' -> pure $ C.CDecl spc decl'' ni - a -> error (show a) - -rCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> m (C.CFunctionDef C.NodeInfo) -rCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do - smt' <- rCStatement smt +mrCFunctionDef :: (MonadReduce Lab m) => C.CFunctionDef C.NodeInfo -> MaybeT m (C.CFunctionDef C.NodeInfo) +mrCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do + smt' <- lift $ rCStatement smt + mapM_ cCDeclaration cdecls + mapM_ cCDeclarationSpecifier spc + cCDeclr dec pure $ C.CFunDef spc dec cdecls smt' ni +cCDeclr :: (MonadReduce Lab m) => C.CDeclarator C.NodeInfo -> MaybeT m () +cCDeclr (C.CDeclr x dd _ _ _) = do + mapM_ cCDerivedDeclarator dd + givenWith x + where + cCDerivedDeclarator = \case + C.CPtrDeclr ts _ -> mapM_ cCTypeQualifier ts + C.CArrDeclr ts as _ -> do + mapM_ cCTypeQualifier ts + case as of + C.CNoArrSize _ -> pure () + C.CArrSize _ e -> cCExpression e + C.CFunDeclr f attr _ -> do + mapM_ cCAttr attr + cCFunParams f + cCFunParams = \case + C.CFunParamsOld o -> mapM_ givenThat o + C.CFunParamsNew o _ -> mapM_ cCDeclaration o + +cCAttr :: (MonadReduce Lab m) => C.CAttribute C.NodeInfo -> MaybeT m () +cCAttr (C.CAttr i e _) = do + mapM_ cCExpression e + givenThat i + rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo) rCStatement = \case C.CCompound is cbi ni -> do @@ -117,6 +204,10 @@ rCStatement = \case -- todo fix attrs splitOn i (pure $ C.CExpr Nothing ni) do pure $ C.CGoto i ni + C.CWhile e s dow ni -> do + e' <- zrCExpression e + s' <- rCStatement s + pure $ C.CWhile e' s' dow ni a -> error (show a) where rCForInit = \case diff --git a/hie.yaml b/hie.yaml index 78dbf933a015048dd47cd97d24703c6ca013962f..8764232366804781ea91e3786e62d0a3e2e19d3c 100644 --- a/hie.yaml +++ b/hie.yaml @@ -2,5 +2,7 @@ cradle: cabal: - path: "./src" component: "lib:rtree" - - path: "./bin" + - path: "./bin/rtree-c" component: "exe:rtree-c" + - path: "./test/src" + component: "test:rtree-test" diff --git a/package.yaml b/package.yaml index 3024540c1817491c119469e46575f592da11bda3..084d3cec27da819839cf1cf76a27bd18add0a72f 100644 --- a/package.yaml +++ b/package.yaml @@ -43,11 +43,6 @@ tests: main: Main.hs dependencies: - rtree - - diagrams - - diagrams-lib - - diagrams-core - - diagrams-contrib - - diagrams-svg # - template # - hedgehog # - hspec diff --git a/rtree.cabal b/rtree.cabal index 6c39356775e59a0a78b060263e6cf1c816f8f252..bfb31809c479de8992263636921707709a204a9c 100644 --- a/rtree.cabal +++ b/rtree.cabal @@ -69,11 +69,6 @@ test-suite rtree-test base >=4.9 && <5 , containers , data-fix - , diagrams - , diagrams-contrib - , diagrams-core - , diagrams-lib - , diagrams-svg , directory , free , mtl diff --git a/src/Control/Monad/Reduce.hs b/src/Control/Monad/Reduce.hs index 5627b5141f59ec682cc17a42693834452a2a36e3..4bdb12c3426f9b6d298cb5083e6acda1ec5c4c1c 100644 --- a/src/Control/Monad/Reduce.hs +++ b/src/Control/Monad/Reduce.hs @@ -42,6 +42,7 @@ module Control.Monad.Reduce ( onBoth, ) where +import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe import qualified Data.List.NonEmpty as NE @@ -114,12 +115,12 @@ given = givenWith Nothing {-# INLINE given #-} -- | Continues if the labeled fact is true. -givenWith :: (MonadReduce l m) => Maybe l -> MaybeT m () -givenWith l = MaybeT $ splitWith l (pure Nothing) (pure (Just ())) +givenWith :: (MonadReduce l m, MonadPlus m) => Maybe l -> m () +givenWith l = splitWith l mzero (pure ()) {-# INLINE givenWith #-} -- | Continues if the labeled fact is true. -givenThat :: (MonadReduce l m) => l -> MaybeT m () +givenThat :: (MonadReduce l m, MonadPlus m) => l -> m () givenThat l = givenWith (Just l) {-# INLINE givenThat #-} @@ -129,16 +130,16 @@ collect fn = fmap catMaybes . traverse (runMaybeT . fn) {-# INLINE collect #-} -- | Given a list of item try to remove each of them, but keep atleast one. -collectNonEmpty' :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> MaybeT m [b] +collectNonEmpty' :: (MonadReduce l m, MonadPlus m) => (a -> MaybeT m b) -> [a] -> m [b] collectNonEmpty' fn as = NE.toList <$> collectNonEmpty fn as {-# INLINE collectNonEmpty' #-} -- | Given a list of item try to remove each of them, but keep atleast one. -collectNonEmpty :: (MonadReduce l m) => (a -> MaybeT m b) -> [a] -> MaybeT m (NE.NonEmpty b) +collectNonEmpty :: (MonadReduce l m, MonadPlus m) => (a -> MaybeT m b) -> [a] -> m (NE.NonEmpty b) collectNonEmpty fn as = do - as' <- lift . fmap catMaybes . traverse (runMaybeT . fn) $ as - MaybeT . pure $ NE.nonEmpty as' + as' <- fmap catMaybes . traverse (runMaybeT . fn) $ as + maybe mzero pure $ NE.nonEmpty as' {-# INLINE collectNonEmpty #-} instance (MonadReduce l m) => MonadReduce l (MaybeT m) where diff --git a/src/Control/RTree.hs b/src/Control/RTree.hs index 5403a5cffb7d511826fd9686a963ac1fe2a1847d..82cb58a837293b731b3be4b18d0b25d26e06087c 100644 --- a/src/Control/RTree.hs +++ b/src/Control/RTree.hs @@ -124,7 +124,7 @@ iextractT v (IRTreeT m) = evalStateT m (ReState [] v) ireduce :: forall m l i . (Monad m, Ord l) - => (i -> m Bool) + => (Valuation l -> i -> m Bool) -> Valuation l -> IRTree l i -> m i @@ -137,7 +137,7 @@ ireduceT . (Monad m, Monad t, Ord l) => (forall a. m a -> t a) -- ^ a lift of monad m into t (normally @id@ or @lift@) - -> (i -> t Bool) + -> (Valuation l -> i -> t Bool) -> Valuation l -> IRTreeT l m i -> t i @@ -145,8 +145,8 @@ ireduceT lift_ p v (IRTreeT m) = go [] where go pth = lift_ (runStateT m (ReState pth v)) >>= \case - (i, ReState [] _) -> do - t <- p i + (i, ReState [] v') -> do + t <- p v' i -- if the predicate is true, we can reduce to the false branch. go (pth <> [not t]) (i, _) -> pure i @@ -155,7 +155,7 @@ ireduceT lift_ p v (IRTreeT m) = go [] ireduceExp :: forall m l i . (Monad m, Ord l) - => (i -> m Bool) + => (Valuation l -> i -> m Bool) -> Valuation l -> IRTree l i -> m i @@ -168,7 +168,7 @@ ireduceExpT . (Monad m, Monad t, Ord l) => (forall a. m a -> t a) -- ^ a lift of monad m into t (normally @id@ or @lift@) - -> (i -> t Bool) + -> (Valuation l -> i -> t Bool) -> Valuation l -> IRTreeT l m i -> t i @@ -177,8 +177,8 @@ ireduceExpT lift_ p v (IRTreeT (StateT m)) = go 0 [] -- here n is the number of explorative elements go n pth = lift_ (m $ ReState pth v) >>= \case - (i, ReState [] _) -> do - p i >>= \case + (i, ReState [] v') -> do + p v' i >>= \case True -> do let n' = next n go n' (pth <> replicate n' False) diff --git a/test/src/Main.hs b/test/src/Main.hs index 5be905a2dd31a3b13ab2c87066c4ec657e7a9035..d2a6c17d9e2e241440f4117b53cbc0198af82f0b 100644 --- a/test/src/Main.hs +++ b/test/src/Main.hs @@ -1,110 +1,3 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# HLINT ignore "Redundant bracket" #-} -{-# LANGUAGE PackageImports #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE NoMonomorphismRestriction #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -{-# OPTIONS_GHC -Wno-unused-top-binds #-} - -import Control.RTree - -import Control.RTree (exponentialSearch) -import qualified Data.List.NonEmpty as NE -import "diagrams-contrib" Diagrams.TwoD.Layout.Tree -import "diagrams-lib" Diagrams.Prelude hiding (Empty, (<|)) -import "diagrams-svg" Diagrams.Backend.SVG () -import "diagrams-svg" Diagrams.Backend.SVG.CmdLine - -type Var = String - -data Exp - = Num Int - | Add Exp Exp - | Let Var Exp Exp - | Var Var - -replace :: Var -> Exp -> Exp -> Exp -replace v e = \case - Num n -> Num n - Add e1 e2 -> Add (replace v e e1) (replace v e e2) - Let v1 e1 e2 - | v1 /= v -> Let v1 (replace v e e1) (replace v e e2) - | otherwise -> Let v1 e1 e2 - Var v' - | v == v' -> e - | otherwise -> Var v' - -instance Show Exp where - showsPrec n = \case - Num n' -> shows n' - Add e1 e2 -> - showParen (n > 2) (showsPrec 2 e1 . showString " + " . showsPrec 3 e2) - Let v e1 e2 -> - showParen (n > 0) - $ showString v - . showString ":=" - . showsPrec 1 e1 - . showString "; " - . shows e2 - Var v -> showString v - -expR :: Exp -> RTree Exp -expR = \case - Num n -> - pure (Num 0) <| pure (Num n) - Add e1 e2 -> - expR e1 <| expR e2 <| (Add <$> expR e1 <*> expR e2) - Let v e1 e2 -> - expR (replace v e1 e2) <| Let v <$> expR e1 <*> expR e2 - Var v -> pure (Var v) - -genD :: (Show e) => RTree e -> BTree (QDiagram SVG V2 Double Any) -genD = - foldR - ( \(lhs :<| rhs) -> - BNode - ( triangle 0.2 - # rotate (90 @@ deg) - <> circle 0.2 - # fc white - # lc white - ) - lhs - rhs - ) - . fmap - ( \i -> - BNode - ( text (show i) - # fontSizeL 0.3 - <> circle 0.3 - # fc white - # lc white - ) - Empty - Empty - ) - --- ( text n --- # fontSizeL (0.5 :: (Double)) --- <> circle 0.3 --- # fc white --- ) main :: IO () -main = do - let Just t' = - uniqueXLayout - 1 - 1.2 - -- (genD (binarySearch (1 NE.:| [2, 3, 4, 5, 7, 6, 8 :: Int]))) - -- (genD (binarySearch (1 NE.:| [2, 3, 4, 5, 7, 6, 8 :: Int]))) - (genD (rSuffixList [1, 2, 3, 4, 5 :: Int])) - -- (genD (expR (Let "x" (Num 10) (Add (Num 2) (Add (Var "x") (Num 3)))))) - defaultMain - $ renderTree id (~~) (forceLayoutTree t') - # centerXY - # pad 1.1 +main = pure ()