Commit 80ad7fed authored by Bastian Kauschke's avatar Bastian Kauschke

add minimize command

parent 47afebfd
......@@ -64,6 +64,7 @@ library
, Copar.Coalgebra.Parser
, Copar.Coalgebra.Parser.Class
, Copar.Coalgebra.Parser.Internal
, Copar.Coalgebra.Printer
, Copar.PartitionPrinter
, Copar.Dot
, Copar.PrettyShow
......
{-# LANGUAGE AllowAmbiguousTypes #-}
module Copar.CoalgebraPrinter (printEncoding) where
import Control.Monad.ST
import qualified Data.HashMap.Strict as HM
import Data.MorphismEncoding
import qualified Data.Text.Lazy.Builder as Build
import qualified Data.Text as T
import Data.Foldable.Utils
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import qualified Data.Vector.Utils as V
import qualified Data.List as List
import Copar.FunctorExpression.Desorting
import Copar.Coalgebra.Parser
import Copar.Coalgebra.Printer
import Copar.RefinementInterface
printEncoding :: forall f. (ParseMorphism f, PrintMorphism f)
=> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> SymbolTable
-> V.Vector (f ())
-> Build.Builder
printEncoding encoding symbols sorts =
sepFold "\n" printEncodingState (List.sortOn snd (HM.toList (fromSymbolTable symbols)))
where
adjacencyList = buildAdjacencyList $ edges encoding
printEncodingState :: (State, T.Text) -> Build.Builder
printEncodingState (state, s) = Build.fromText s <> ": " <> morphismPoint state
morphismPoint :: State -> Build.Builder
morphismPoint state =
let ty = typeOf encoding state
in printMorphismPoint
(sorts V.! (fromEnum (sortedSort ty) - 1))
(sortedElem ty)
(adjacencyList V.! state)
buildAdjacencyList :: V.Vector (Edge (Label (Desorted f))) -> V.Vector [(Label f, Build.Builder)]
buildAdjacencyList edges =
runST $ do
list <- MV.replicate (size encoding) []
V.rforM_ edges $
\edge -> MV.modify list ((desortedLabel @f (label edge), printState (to edge)):) (from edge)
V.freeze list
printState :: State -> Build.Builder
printState state = maybe (morphismPoint state) Build.fromText (HM.lookup state (fromSymbolTable symbols))
......@@ -5,6 +5,7 @@ module Copar.FunctorExpression.Desorting
( Desorted
, Sorted(..)
, desort
, desortedLabel
, mkDesortedLabel
) where
......@@ -39,11 +40,18 @@ mkDesortedLabel (Sorted _ x) = x
mkDesortedLabel = id
#endif
desortedLabel :: Label (Desorted f) -> (Label f)
#ifdef RELEASE
desortedLabel = id
#else
desortedLabel (Sorted _ x) = x
#endif
instance RefinementInterface f => RefinementInterface (Desorted f) where
{-# SPECIALIZE instance RefinementInterface (Desorted SomeFunctor) #-}
#ifdef RELEASE
init (Sorted sort f1) labels = init @f f1 labels
init (Sorted _sort f1) labels = init @f f1 labels
#else
init (Sorted sort f1) labels = Sorted sort (init @f f1 (filterBySort sort labels))
#endif
......
......@@ -23,7 +23,6 @@ module Copar.Parser
import Prelude hiding ( readFile )
import Data.Bifunctor
import Data.Function ( on )
import Data.Proxy
import qualified Data.List.NonEmpty as E
import qualified Data.List as L
......@@ -66,27 +65,28 @@ functorExpressionParser varReplacement functors = do
-- optimize the expression in other ways.
data ApplyFunctorTransformations = ApplyTransformations | DontApplyTransformations
coalgebraParser
:: Either
(FunctorExpression SomeFunctor Precedence, [FunctorParser SomeFunctor])
(FunctorExpression SomeFunctor Sort)
(FunctorExpression SomeFunctor Precedence, [FunctorParser SomeFunctor])
(FunctorExpression SomeFunctor Sort)
-> ApplyFunctorTransformations
-> SanityChecks
-> Parser
( SymbolTable
, Encoding
(Label (Desorted SomeFunctor))
(F1 (Desorted SomeFunctor))
)
( FunctorExpression SomeFunctor Sort
, ( SymbolTable
, Encoding
(Label (Desorted SomeFunctor))
(F1 (Desorted SomeFunctor))
)
)
coalgebraParser functor transPolicy sanity = do
L.space *> L.newlines
f <- case functor of
Left (varReplacement, functors) ->
functorExpressionParser varReplacement functors <* L.newlines1
Right f' -> return f'
morphismsParser (transformFunctor f) sanity
<?> "morphism definition"
let f' = transformFunctor f
(f',) <$> morphismsParser f' sanity <?> "morphism definition"
where
transformFunctor = case transPolicy of
ApplyTransformations -> applyFunctorRewrites
......@@ -167,7 +167,7 @@ parseCoalgebra
-> Text -- ^ Input text
-> Either
String
( Proxy TheFunctor
( FunctorExpression SomeFunctor Sort
, (SymbolTable, Encoding (Label TheFunctor) (F1 TheFunctor))
)
parseCoalgebra config name input =
......@@ -182,7 +182,7 @@ parseCoalgebra config name input =
maybe (Left (identity, functorParsers)) Right (functor config)
in bimap
errorBundlePretty
(Proxy, )
id
(parse
(coalgebraParser eitherFunctor
(functorTransforms config)
......@@ -201,7 +201,7 @@ readFile
-> IO
( Either
String
( Proxy TheFunctor
( FunctorExpression SomeFunctor Sort
, (SymbolTable, Encoding (Label TheFunctor) (F1 TheFunctor))
)
)
......@@ -216,7 +216,7 @@ readStdin
-> IO
( Either
String
( Proxy TheFunctor
( FunctorExpression SomeFunctor Sort
, (SymbolTable, Encoding (Label TheFunctor) (F1 TheFunctor))
)
)
......
module Data.Vector.Utils
( iforM_
, rforM_
, sort
, sortBy
, sortOn
......@@ -8,6 +9,7 @@ module Data.Vector.Utils
import Data.Ord (comparing)
import Control.Monad (forM_)
import Data.Vector (Vector)
import qualified Data.Vector as V
import qualified Data.Vector.Algorithms.Intro as V
......@@ -33,3 +35,9 @@ sortOn f = V.modify (V.sortBy (comparing f))
hasDuplicates :: Eq a => Vector a -> Bool
hasDuplicates v = V.length (V.uniq v) /= V.length v
{-# INLINE hasDuplicates #-}
rforM_ :: (Monad m) => Vector a -> (a -> m b) -> m ()
rforM_ v f = do
forM_ (map (V.length v-) [1..V.length v]) $ \i -> do
f (v V.! i)
......@@ -21,8 +21,11 @@ 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
import qualified Data.Text.Lazy.Builder as Build
import Data.Proxy
import qualified Data.Vector as V
import Options.Applicative
......@@ -36,14 +39,16 @@ import Copar.FunctorPrinter
import Copar.Functors
import Copar.FunctorDescription
import qualified Data.MorphismEncoding as Encoding
import Copar.FunctorExpression.Sorts (Sort, sortedSort)
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.Desorting (Desorted)
import Copar.Dot
import Copar.RewriteFunctors
import Copar.Timing
import Copar.Functors
import Copar.CoalgebraPrinter
import qualified Hardwired as Hardwired
import Stats
......@@ -59,6 +64,7 @@ data SubCommand
= HelpCommand (Maybe HelpCommand)
| RefineCommand RefineOptions
| RefineHardwiredCommand RefineOptions
| MinimizeCommand MinimizeOptions
| PrettyPrintCommand PrettyPrintOptions
| GraphCommand GraphOptions
| DebugCommand DebugCommand
......@@ -90,6 +96,15 @@ subcommand =
)
)
)
<> (command
"minimize"
(info
(MinimizeCommand <$> minimizeOptions)
( progDesc "(WORK IN PROGRESS) Minimize the given coalgebra."
<> footer "Refines the given coalgebra and returns a minimal behaviorally equivalent"
)
)
)
-- <> (command
-- "pretty-print"
-- (info
......@@ -215,6 +230,52 @@ refineOptions = do
)
pure RefineOptions { .. }
data MinimizeOptions = MinimizeOptions
{ minimizeApplyTransformations :: Bool
, minimizeEnableSanity :: Bool
, minimizeFunctor :: Maybe (FunctorExpression SomeFunctor Sort)
, minimizeInputFile :: Maybe FilePath
}
minimizeOptions :: Parser MinimizeOptions
minimizeOptions = do
minimizeInputFile <- optional
(argument
str
( metavar "INPUT_FILE"
<> help
"Name of file to read the input coalgebra from or \"-\" for standard input. \
\See the \"help\" command for a description of available syntax."
<> value "-"
<> showDefault
)
)
minimizeFunctor <- optional
(option
functorReader
( long "functor"
<> short 'f'
<> metavar "FUNCTOR_EXPR"
<> help
"Functor for the input coalgebra. This is normally the first line of \
\the input, but can also alternatively be given here."
)
)
minimizeApplyTransformations <- not <$> switch
( long "no-functor-transforms"
<> help
"Don't try to optimize functor expression. \
\This flag can drastically *reduce* performace."
)
minimizeEnableSanity <- not <$> switch
( long "no-sanity-checks"
<> help
"Disable sanity checks in the parser. Do not use this lightly. It \
\might speed up the parser but require the input to be absolutely \
\correct. Otherwise, nasal demons might be created."
)
pure MinimizeOptions { .. }
data PrettyPrintOptions = PrettyPrintOptions
{ prettyPrintInputFile :: Maybe FilePath
}
......@@ -426,11 +487,13 @@ main = do
partition <- case statsType stats of
NoStats ->
withTimeStat stats "algorithm-duration" (stToIO (refine f encoding (refineEnableOpt r)))
withTimeStat stats "algorithm-duration" (
stToIO (refine (Proxy :: Proxy (Desorted SomeFunctor)) encoding (refineEnableOpt r))
)
_ -> do
(part, algoStats) <-
withTimeStat stats "algorithm-duration"
$ refineWithStats f encoding (refineEnableOpt r)
$ refineWithStats (Proxy :: Proxy (Desorted SomeFunctor)) encoding (refineEnableOpt r)
logStat stats
"initial-partition-size"
(tshow (initialBlocks algoStats))
......@@ -460,7 +523,6 @@ main = do
(outputPartition (refineOutputFile r) encoding symbolTable partition)
finalizeStats stats
(RefineHardwiredCommand r) -> do
stats <- initStats (refineStats r) (refineStatsJson r)
Hardwired.main
......@@ -469,6 +531,30 @@ main = do
(outputPartition (refineOutputFile r))
(refineEnableOpt r)
(MinimizeCommand r) -> do
(f, (symbolTable, encoding)) <- do
let transPolicy = if minimizeApplyTransformations r
then P.ApplyTransformations
else P.DontApplyTransformations
let sanity = if minimizeEnableSanity r
then P.EnableSanityChecks
else P.DisableSanityChecks
let parserConfig = P.Config
{ functorTransforms = transPolicy
, sanityChecks = sanity
, functor = minimizeFunctor r
}
readCoalgebra parserConfig (minimizeInputFile r)
>>= \case
Left err -> hPutStrLn stderr err >> exitFailure
Right res -> evaluate res
T.putStrLn $ printParseableFunctor f
T.putStrLn ""
LT.putStrLn $ Build.toLazyText $ printEncoding encoding symbolTable (sortTable f)
(PrettyPrintCommand r) -> do
(f, (symbolTable, encoding)) <- do
......@@ -484,7 +570,7 @@ main = do
hPutStrLn stderr "tesetste"
(GraphCommand r) -> do
(f, (symbolTable, encoding)) <- do
(_, (symbolTable, encoding)) <- do
let transPolicy = if graphApplyTransformations r
then P.ApplyTransformations
else P.DontApplyTransformations
......@@ -499,7 +585,7 @@ main = do
Right res -> evaluate res
part <- if graphDrawPartition r
then Just <$> stToIO (refine f encoding True)
then Just <$> stToIO (refine (Proxy :: Proxy (Desorted SomeFunctor)) encoding True)
else return Nothing
let config = DotConfig { nodeLabels = graphDrawNodeLabels r
......
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