Commit b213aa49 authored by Bastian Kauschke's avatar Bastian Kauschke

test minimization

parent 16f165a7
......@@ -9,3 +9,11 @@ For example, a file called `foo` containing a coalgebra should have a `.out`
file with the output of:
stack exec copar refine < foo
Similarly, `.mini` files contain the output of CoPaR's `minimize` command, when
applied to the original file. This is also checked as part of the test suite.
## ui-tests
In this subdirectory there are further example snippets which might not be
necessarily useful as examples, as they are mostly used for testing.
{f, n}xX^{a, b}
s0_q1_q2: (n, {a: s0_q1_q2, b: s1_q3})
s1_q3: (f, {a: s0_q1_q2, b: s0_q1_q2})
\ No newline at end of file
P(XxX)
s00_a1_a2_a3: {(s00_a1_a2_a3, s00_a1_a2_a3)}
s01_b1_b4: {(s02_b2_b3_bot, s02_b2_b3_bot)}
s02_b2_b3_bot: {}
s03_c1_c10_c2_c3_c4_c5_c6_c7_c8_c9: {(s03_c1_c10_c2_c3_c4_c5_c6_c7_c8_c9, s02_b2_b3_bot)}
s04_d1: {(s06_d2, s02_b2_b3_bot)}
s05_d10: {(s04_d1, s04_d1)}
s06_d2: {(s07_d3, s02_b2_b3_bot)}
s07_d3: {(s08_d4, s02_b2_b3_bot)}
s08_d4: {(s09_d5, s02_b2_b3_bot)}
s09_d5: {(s10_d6, s02_b2_b3_bot)}
s10_d6: {(s11_d7, s02_b2_b3_bot)}
s11_d7: {(s12_d8, s02_b2_b3_bot)}
s12_d8: {(s13_d9, s02_b2_b3_bot)}
s13_d9: {(s05_d10, s02_b2_b3_bot)}
\ No newline at end of file
P(X)
x: { x, y }
y: { x }
z: { x, y }
\ No newline at end of file
C^X
s0: {s0: 1.0 + 1.0i, s1: 1.0 + 1.0i}
s1: {}
\ No newline at end of file
{square, circle, triangle}xP(X)
s0: (triangle, {s2, s3})
s1: (square, {})
s2: (circle, {})
s3: (circle, {s1})
s4: (circle, {s2})
s5: (triangle, {s2, s3, s4})
# a non-determ. automaton parsing binary trees
Ƥ(X×X)
bot: {}
d1: { (d2,bot) }
d2: { (d3,bot) }
d3: { (d4,bot) }
d4: { (d5,bot) }
d5: { (d6,bot) }
d6: { (d7,bot) }
d7: { (d8,bot) }
d8: { (d9,bot) }
d9: { (d10,bot) }
d10: { (d3,d3) }
{circled, normal} x Ƥ(ƤX)
a1: (normal, {{a1}})
\ No newline at end of file
{init, non_init} x Ƥ({a,b} + {f}×X×X)
q_i: (init, { inj1 (f, q_a, q_b), inj1 (f, q_b, q_a) })
q_a: (non_init, { inj0 a })
q_b: (non_init, { inj0 b })
......@@ -9,7 +9,8 @@
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Copar.Coalgebra.Parser
( parseMorphisms
( anonymizeSymbols
, parseMorphisms
, morphismsParser
, SymbolTable(..)
, module Copar.Coalgebra.Parser.Class
......@@ -26,6 +27,7 @@ import Control.Monad.State.Strict (execStateT, MonadState)
import qualified Data.HashMap.Strict as M
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.List as List
import Lens.Micro.Platform
import Text.Megaparsec hiding (State)
import qualified Data.Vector as V
......@@ -43,6 +45,8 @@ import qualified Copar.Parser.Lexer as L
import Copar.Parser.Types
import Copar.Coalgebra.Parser.Class
import GHC.Float (integerLogBase)
import Text.Printf
class HasSanityChecks m where
-- | When this returns 'True', morphism parsers are allowed (encouraged) to skip
......@@ -93,6 +97,16 @@ checkUndefinedRefs = use (symbolTable . to M.toList . to (filter isUndefined)) >
newtype SymbolTable = SymbolTable { fromSymbolTable :: M.HashMap State Text }
deriving (Show,Eq,Ord,NFData)
anonymizeSymbols :: SymbolTable -> SymbolTable
anonymizeSymbols symTbl = SymbolTable $ M.fromList (map anonymize
(zip [(0 :: Int)..] (List.sortOn snd $ M.toList table)))
where
anonymize (idx, (k, _)) =
( k
, T.pack (printf "s%0*d" ((+1) . (integerLogBase 10) . toInteger $ M.size table) idx)
)
table = fromSymbolTable symTbl
finalizeState :: forall f.
ParserState (Label f) (F1 f) -> (SymbolTable, Encoding (Label (Desorted f)) (F1 (Desorted f)))
finalizeState state =
......
......@@ -7,21 +7,16 @@
module Main (main) where
import Control.Arrow ((***))
import Control.Exception (evaluate)
import Control.Monad.ST
import Data.IORef
import Data.List (sortOn)
import System.Exit
import System.IO
import System.Environment
import Data.Map (Map)
import qualified Data.Map as M
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.IO as LT
import Data.Text.Prettyprint.Convert.AnsiWlPprint
import Data.Text.Prettyprint
......@@ -29,8 +24,6 @@ import qualified Data.Text.Lazy.Builder as Build
import Data.Proxy
import qualified Data.Vector as V
import Options.Applicative
import Text.JSON
import Text.Show.Pretty (pPrint)
import Copar.Algorithm
import qualified Copar.Parser as P
......@@ -42,13 +35,13 @@ import qualified Data.MorphismEncoding as Encoding
import Copar.FunctorExpression.Sorts (Sort, sortedSort, sortTable)
import qualified Data.Partition as Partition
import Copar.Functors.SomeFunctor (SomeFunctor)
import Copar.FunctorExpression.Type (FunctorExpression)
import Copar.FunctorExpression.Type (FunctorExpression (..))
import Copar.FunctorExpression.Desorting (Desorted)
import Copar.Dot
import Copar.RewriteFunctors
import Copar.Timing
import Copar.Functors
import Copar.CoalgebraPrinter
import Copar.Minimize
import qualified Hardwired as Hardwired
import Stats
......@@ -234,6 +227,7 @@ data MinimizeOptions = MinimizeOptions
{ minimizeApplyTransformations :: Bool
, minimizeEnableSanity :: Bool
, minimizeFunctor :: Maybe (FunctorExpression SomeFunctor Sort)
, minimizeEnableOpt :: Bool
, minimizeInputFile :: Maybe FilePath
}
......@@ -274,6 +268,12 @@ minimizeOptions = do
\might speed up the parser but require the input to be absolutely \
\correct. Otherwise, nasal demons might be created."
)
minimizeEnableOpt <- not <$> switch
( long "disable-optimizations"
<> help "Disable some optimizations. Currently, this is just the \
\one-element optimization. Obviously, this will reduce \
\performance."
)
pure MinimizeOptions { .. }
data PrettyPrintOptions = PrettyPrintOptions
......@@ -532,7 +532,7 @@ main = do
(refineEnableOpt r)
(MinimizeCommand r) -> do
(f, (symbolTable, encoding)) <- do
(f :: FunctorExpression SomeFunctor Sort, (symbolTable, encoding)) <- do
let transPolicy = if minimizeApplyTransformations r
then P.ApplyTransformations
else P.DontApplyTransformations
......@@ -552,9 +552,12 @@ main = do
Left err -> hPutStrLn stderr err >> exitFailure
Right res -> evaluate res
part <- stToIO $ refine (Proxy :: Proxy (Desorted SomeFunctor)) encoding (minimizeEnableOpt r)
let (encoding', symbolTable') = minimize f encoding symbolTable part
T.putStrLn $ printParseableFunctor f
T.putStrLn ""
LT.putStrLn $ Build.toLazyText $ printEncoding encoding symbolTable (sortTable f)
LT.putStrLn $ Build.toLazyText $ printEncoding encoding' symbolTable' (sortTable f)
(PrettyPrintCommand r) -> do
(f, (symbolTable, encoding)) <- do
......
......@@ -4,7 +4,6 @@
module Main (main) where
import Control.Monad.ST
import Control.Exception (evaluate)
import Data.List
import Data.Proxy
......@@ -18,25 +17,44 @@ import Test.Hspec
import Copar.Algorithm
import qualified Copar.Parser as P
import Copar.PartitionPrinter
import Copar.Coalgebra.Parser
import Copar.CoalgebraPrinter
import Copar.FunctorPrinter
import Copar.Minimize
import Copar.Functors.SomeFunctor
import Copar.FunctorExpression.Desorting (Desorted)
import Copar.FunctorExpression.Sorts (sortTable)
main :: IO ()
main = do
let exampleDir = "examples/"
files <- listDirectory exampleDir
hspec $ testFiles testFileRefine (map (exampleDir ++) (filter isOutput files))
hspec $ testFiles testFileMinimize (map (exampleDir ++) (filter isTestFile files))
let exampleDir = "examples"
exampleFiles <- directoryFiles exampleDir
hspec $ testFiles testFileRefine (filter isOutput exampleFiles)
hspec $ testFiles testFileMinimize (filter isMinimized exampleFiles)
hspec $ testFiles testFileMinimizeIdentity (filter isTestFile exampleFiles)
directoryFiles :: String -> IO [String]
directoryFiles dir = do
items <- (listDirectory dir)
subdirs <- sequence $ map expandDir (map ((dir <> "/")++) (items))
return (concat subdirs)
where
expandDir :: String -> IO [String]
expandDir dir = doesDirectoryExist dir >>= \is_dir -> if is_dir then directoryFiles dir else return [dir]
outSuffix :: String
outSuffix = ".out"
minimizeSuffix :: String
minimizeSuffix = ".mini"
isOutput :: FilePath -> Bool
isOutput = (outSuffix `isSuffixOf`)
isMinimized :: FilePath -> Bool
isMinimized = (minimizeSuffix `isSuffixOf`)
isTestFile :: FilePath -> Bool
isTestFile path = (not $ isOutput path) && (not $ ".md" `isSuffixOf` path)
......@@ -56,27 +74,55 @@ testFileRefine outfile =
P.readFile P.defaultConfig file
>>= \case
Left err -> return err
Right (f, (symTab, enc)) -> do
Right (_, (symTab, enc)) -> do
partition <- stToIO (refine (Proxy :: Proxy (Desorted SomeFunctor)) enc True)
return $ T.unpack (showPartition enc symTab partition)
testFileMinimize :: FilePath -> Spec
testFileMinimize file =
specify ("minimize " <> file) $ do
testFileMinimize mini =
let file = dropSuffix minimizeSuffix mini
in specify ("minimize " <> file) $ do
minimized <- readFile (file ++ minimizeSuffix)
process file `shouldReturn` minimized
where
process :: FilePath -> IO String
process file =
P.readFile P.defaultConfig file >>=
\case
Left err -> return err
Right (f, (symTab, enc)) -> do
part <- stToIO (refine (Proxy :: Proxy (Desorted SomeFunctor)) enc True)
let
(enc', symTab') = minimize f enc symTab part
return (LT.unpack . Build.toLazyText $ Build.fromText (printParseableFunctor f)
<> "\n\n"
<> printEncoding enc' symTab' (sortTable f))
testFileMinimizeIdentity :: FilePath -> Spec
testFileMinimizeIdentity file =
specify ("minimizeIdentity " <> file) $ do
P.readFile P.defaultConfig file >>=
\case
Left err -> expectationFailure $ "initialParse: " <> err
Right (f, (symTab, enc)) ->
Right (f, (symTab, enc)) -> do
part <- stToIO (refine (Proxy :: Proxy (Desorted SomeFunctor)) enc True)
let
(enc', symTab') = minimize f enc symTab part
coalgebra = Build.fromText (printParseableFunctor f)
<> "\n"
<> printEncoding enc symTab (sortTable f)
<> "\n\n"
<> printEncoding enc' (anonymizeSymbols symTab') (sortTable f)
reparsed = P.parseCoalgebra P.defaultConfig "(minized)" $ LT.toStrict (Build.toLazyText coalgebra)
in case reparsed of
Left err -> expectationFailure $ "parseMinimized: " <> err
Right (f', (symTab', enc')) -> (
Build.fromText (printParseableFunctor f')
<> "\n"
<> printEncoding enc' symTab' (sortTable f')
) `shouldBe` coalgebra
reparsed = P.parseCoalgebra P.defaultConfig "(minimized)" $ LT.toStrict (Build.toLazyText coalgebra)
case reparsed of
Left err -> expectationFailure $ "parseMinimized: " <> err
Right (f', (symTab'', enc'')) -> do
part' <- stToIO (refine (Proxy :: Proxy (Desorted SomeFunctor)) enc'' True)
let
(enc''', symTab''') = minimize f' enc'' symTab'' part'
Build.fromText (printParseableFunctor f)
<> "\n\n"
<> (printEncoding enc''' (anonymizeSymbols symTab''') (sortTable f')) `shouldBe`
coalgebra
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment