Skip to content
Snippets Groups Projects
Commit 4dab88ec authored by chrg's avatar chrg
Browse files

Loads of work

parent b2c30d92
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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
......
......@@ -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"
......@@ -43,11 +43,6 @@ tests:
main: Main.hs
dependencies:
- rtree
- diagrams
- diagrams-lib
- diagrams-core
- diagrams-contrib
- diagrams-svg
# - template
# - hedgehog
# - hspec
......
......@@ -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
......
......@@ -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
......
......@@ -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)
......
{-# 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 ()
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment