From d6173c4381068a9bdf14f8bca8e5666f68cecb93 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 25 May 2020 17:21:01 +0200 Subject: [PATCH] some cleanup --- .stylish-haskell.yaml | 141 +++++++++++++++++++++++++++++++++ NominalAngluin.cabal | 6 +- src/Bollig.hs | 5 +- src/Examples.hs | 18 ++--- src/Examples/Contrived.hs | 12 +-- src/Examples/ContrivedNFAs.hs | 15 ++-- src/Examples/Fifo.hs | 13 +-- src/Examples/RunningExample.hs | 16 ++-- src/Examples/Stack.hs | 16 ++-- src/Main.hs | 55 ++++++------- src/Main2.hs | 18 ++--- src/NLStar.hs | 21 +++-- src/ObservationTable.hs | 28 +++---- src/Teacher.hs | 15 ++-- src/Teachers/Teacher.hs | 4 +- src/Teachers/Terminal.hs | 50 +++++++----- src/Teachers/Whitebox.hs | 13 ++- 17 files changed, 298 insertions(+), 148 deletions(-) create mode 100644 .stylish-haskell.yaml diff --git a/.stylish-haskell.yaml b/.stylish-haskell.yaml new file mode 100644 index 0000000..73243a4 --- /dev/null +++ b/.stylish-haskell.yaml @@ -0,0 +1,141 @@ +# stylish-haskell configuration file +# ================================== + +# The stylish-haskell tool is mainly configured by specifying steps. These steps +# are a list, so they have an order, and one specific step may appear more than +# once (if needed). Each file is processed by these steps in the given order. +steps: + # Convert some ASCII sequences to their Unicode equivalents. This is disabled + # by default. + # - unicode_syntax: + # # In order to make this work, we also need to insert the UnicodeSyntax + # # language pragma. If this flag is set to true, we insert it when it's + # # not already present. You may want to disable it if you configure + # # language extensions using some other method than pragmas. Default: + # # true. + # add_language_pragma: true + + # Format record definitions + # Disabled: don't like it for simple sum types + # - records: {} + + # Align the right hand side of some elements. This is quite conservative + # and only applies to statements where each element occupies a single + # line. All default to true. + - simple_align: + cases: true + top_level_patterns: true + records: true + + # Import cleanup + - imports: + # There are different ways we can align names and lists. + # + # - global: Align the import names and import list throughout the entire + # file. + # + # - file: Like global, but don't add padding when there are no qualified + # imports in the file. + # + # - group: Only align the imports per group (a group is formed by adjacent + # import lines). + # + # - none: Do not perform any alignment. + # + # Default: global. + align: none + + # The following options affect only import list alignment. + # + # List align has following options: + # + # - after_alias: Import list is aligned with end of import including + # 'as' and 'hiding' keywords. + # + # > import qualified Data.List as List (concat, foldl, foldr, head, + # > init, last, length) + # + # - with_alias: Import list is aligned with start of alias or hiding. + # + # > import qualified Data.List as List (concat, foldl, foldr, head, + # > init, last, length) + # + # - with_module_name: Import list is aligned `list_padding` spaces after + # the module name. + # + # > import qualified Data.List as List (concat, foldl, foldr, head, + # init, last, length) + # + # This is mainly intended for use with `pad_module_names: false`. + # + # > import qualified Data.List as List (concat, foldl, foldr, head, + # init, last, length, scanl, scanr, take, drop, + # sort, nub) + # + # - new_line: Import list starts always on new line. + # + # > import qualified Data.List as List + # > (concat, foldl, foldr, head, init, last, length) + # + # Default: after_alias + list_align: after_alias + + # Right-pad the module names to align imports in a group: + # + # - true: a little more readable + # + # > import qualified Data.List as List (concat, foldl, foldr, + # > init, last, length) + # > import qualified Data.List.Extra as List (concat, foldl, foldr, + # > init, last, length) + # + # - false: diff-safe + # + # > import qualified Data.List as List (concat, foldl, foldr, init, + # > last, length) + # > import qualified Data.List.Extra as List (concat, foldl, foldr, + # > init, last, length) + # + # Default: true + pad_module_names: false + + + # Language pragmas + - language_pragmas: + # We can generate different styles of language pragma lists. + # + # - vertical: Vertical-spaced language pragmas, one per line. + # + # - compact: A more compact style. + # + # - compact_line: Similar to compact, but wrap each line with + # `{-#LANGUAGE #-}'. + # + # Default: vertical. + style: vertical + + # Align affects alignment of closing pragma brackets. + # + # - true: Brackets are aligned in same column. + # + # - false: Brackets are not aligned together. There is only one space + # between actual import and closing bracket. + # + # Default: true + align: false + + # Language prefix to be used for pragma declaration, this allows you to + # use other options non case-sensitive like "language" or "Language". + # If a non correct String is provided, it will default to: LANGUAGE. + language_prefix: language + + # Remove trailing whitespace + - trailing_whitespace: {} + + # Squash multiple spaces between the left and right hand sides of some + # elements into single spaces. Basically, this undoes the effect of + # simple_align but is a bit less conservative. + # - squash: {} + +# A common indentation setting. Different steps take this into account. +indent: 4 diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal index 5174044..37bc1ca 100644 --- a/NominalAngluin.cabal +++ b/NominalAngluin.cabal @@ -2,7 +2,7 @@ name: NominalAngluin version: 0.1.0.0 license: UnspecifiedLicense author: Joshua Moerman -copyright: (c) 2016, Joshua Moerman +copyright: (c) 2016 - 2020, Joshua Moerman build-type: Simple cabal-version: >=1.10 @@ -34,7 +34,7 @@ executable NominalAngluin NLambda >= 1.1 hs-source-dirs: src default-language: Haskell2010 - ghc-options: -O2 + ghc-options: -O2 -Wall executable NominalAngluin2 ghc-options: @@ -66,4 +66,4 @@ executable NominalAngluin2 NLambda >= 1.1 hs-source-dirs: src default-language: Haskell2010 - ghc-options: -O2 + ghc-options: -O2 -Wall diff --git a/src/Bollig.hs b/src/Bollig.hs index c2b1fe7..c956b82 100644 --- a/src/Bollig.hs +++ b/src/Bollig.hs @@ -6,10 +6,9 @@ import Angluin import ObservationTable import Teacher -import Data.List (tails) import Debug.Trace import NLambda -import Prelude (Bool (..), Int, Maybe (..), fst, show, ($), (++), (.)) +import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.)) import qualified Prelude hiding () rowUnion :: NominalType i => Set (BRow i) -> BRow i @@ -60,7 +59,7 @@ constructHypothesisBollig State{..} = automaton q a d i f i = filter (\r -> r `sublang` row t []) q f = filter (\r -> singleton True `eq` mapFilter (\(i,b) -> maybeIf (i `eq` []) b) r) q d0 = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss - d = filter (\(q1,a,q2) -> q1 `member` q /\ q2 `member` q) d0 + d = filter (\(q1, _, q2) -> q1 `member` q /\ q2 `member` q) d0 primesUpp = filter (\r -> nonEmpty r /\ r `neq` rowUnion (sublangs r (allRows \\ orbit [] r))) allRowsUpp nonEmpty = isNotEmpty . filter (fromBool . Prelude.snd) allRowsUpp = map (row t) ss diff --git a/src/Examples.hs b/src/Examples.hs index 2dc87e7..0237191 100644 --- a/src/Examples.hs +++ b/src/Examples.hs @@ -9,15 +9,15 @@ module Examples , module Examples.Stack ) where -import Examples.Contrived -import Examples.ContrivedNFAs -import Examples.Fifo -import Examples.NonResidual -import Examples.Residual -import Examples.RunningExample -import Examples.Stack -import NLambda (Atom) -import Teacher (teacherWithTarget, Teacher) +import Examples.Contrived +import Examples.ContrivedNFAs +import Examples.Fifo +import Examples.NonResidual +import Examples.Residual +import Examples.RunningExample +import Examples.Stack +import NLambda (Atom) +import Teacher (Teacher, teacherWithTarget) -- Wrapping it in a teacher exampleTeacher :: Teacher Atom diff --git a/src/Examples/Contrived.hs b/src/Examples/Contrived.hs index 9f117d4..4d9c9bf 100644 --- a/src/Examples/Contrived.hs +++ b/src/Examples/Contrived.hs @@ -1,13 +1,13 @@ -{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-} +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} module Examples.Contrived where -import NLambda +import NLambda -- Explicit Prelude, as NLambda has quite some clashes -import Prelude (Eq, Ord, Show, ($)) -import qualified Prelude () - -import GHC.Generics (Generic) +import GHC.Generics (Generic) +import Prelude (Eq, Ord, Show, ($)) +import qualified Prelude () -- Example automaton from the whiteboard. Three orbits with 0, 1 and 2 -- registers. The third orbit has a local symmetry (S2). diff --git a/src/Examples/ContrivedNFAs.hs b/src/Examples/ContrivedNFAs.hs index ff3b0f8..c5518b4 100644 --- a/src/Examples/ContrivedNFAs.hs +++ b/src/Examples/ContrivedNFAs.hs @@ -1,14 +1,14 @@ -{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-} -{-# LANGUAGE TupleSections #-} +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} +{-# language TupleSections #-} module Examples.ContrivedNFAs where -import NLambda +import NLambda -- Explicit Prelude, as NLambda has quite some clashes -import Prelude (Eq, Ord, Show, ($), Int, (+), (-)) -import qualified Prelude () - -import GHC.Generics (Generic) +import GHC.Generics (Generic) +import Prelude (Eq, Int, Ord, Show, (+), (-)) +import qualified Prelude () -- Language = u a v a w for any words u,v,w and atom a -- The complement of 'all distinct atoms' @@ -45,6 +45,7 @@ exampleNFA1 = automaton data NFA2 = Initial2 | Distinguished Atom | Count Int deriving (Show, Eq, Ord, Generic, NominalType, Contextual) +exampleNFA2 :: Int -> Automaton NFA2 Atom exampleNFA2 n = automaton (singleton Initial2 `union` map Distinguished atoms diff --git a/src/Examples/Fifo.hs b/src/Examples/Fifo.hs index bc00ff0..c815b33 100644 --- a/src/Examples/Fifo.hs +++ b/src/Examples/Fifo.hs @@ -1,11 +1,12 @@ -{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-} +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} module Examples.Fifo (DataInput(..), fifoExample) where -import GHC.Generics (Generic) -import NLambda -import Prelude (Eq, Int, Maybe (..), Ord, Show, Read, length, reverse, - ($), (+), (-), (.), (>=)) -import qualified Prelude () +import GHC.Generics (Generic) +import NLambda +import Prelude (Eq, Int, Maybe (..), Ord, Read, Show, length, reverse, ($), (+), + (-), (.), (>=)) +import qualified Prelude () -- Functional queue data type. First list is for push stuff onto, the diff --git a/src/Examples/RunningExample.hs b/src/Examples/RunningExample.hs index 3dd8f4d..b05393b 100644 --- a/src/Examples/RunningExample.hs +++ b/src/Examples/RunningExample.hs @@ -1,5 +1,6 @@ -{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-} -{-# LANGUAGE TupleSections #-} +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} +{-# language TupleSections #-} module Examples.RunningExample where {- In this file we define the running example of the paper @@ -8,19 +9,20 @@ module Examples.RunningExample where but in terms of FO definable sets it is quite small. -} -import NLambda +import NLambda -- Explicit Prelude, as NLambda has quite some clashes -import Data.List (reverse) -import Prelude (Eq, Ord, Show, ($), (.), (-)) -import qualified Prelude () +import Data.List (reverse) +import Prelude (Eq, Int, Ord, Show, ($), (-), (.)) +import qualified Prelude () -import GHC.Generics (Generic) +import GHC.Generics (Generic) -- Parametric in the alphabet, because why not? data RunningExample a = Store [a] | Check [a] | Accept | Reject deriving (Eq, Ord, Show, Generic, NominalType, Contextual) +runningExample :: NominalType a => Set a -> Int -> Automaton (RunningExample a) a runningExample alphabet 0 = automaton (fromList [Accept, Reject]) alphabet diff --git a/src/Examples/Stack.hs b/src/Examples/Stack.hs index 185ef15..4a5418b 100644 --- a/src/Examples/Stack.hs +++ b/src/Examples/Stack.hs @@ -1,16 +1,16 @@ -{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-} +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} module Examples.Stack (DataInput(..), stackExample) where -import Examples.Fifo (DataInput (..)) -import GHC.Generics (Generic) -import NLambda -import Prelude (Eq, Int, Maybe (..), Ord, Show, length, ($), - (.), (>=)) -import qualified Prelude () +import Examples.Fifo (DataInput (..)) +import GHC.Generics (Generic) +import NLambda +import Prelude (Eq, Int, Maybe (..), Ord, Show, length, ($), (.), (>=)) +import qualified Prelude () -- Functional stack data type is simply a list. -data Stack a = Stack [a] +newtype Stack a = Stack [a] deriving (Eq, Ord, Show, Generic, NominalType, Contextual) push :: a -> Stack a -> Stack a diff --git a/src/Main.hs b/src/Main.hs index a214080..dc3b632 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,46 +1,47 @@ -{-# LANGUAGE ExistentialQuantification #-} -import Angluin -import Bollig -import Examples -import Teacher -import ObservationTable -import NLStar +{-# language ExistentialQuantification #-} +import Angluin +import Bollig +import Examples +import ObservationTable +import Teacher -import Data.IORef (readIORef) -import System.Environment -import NLambda - -import Prelude hiding (map) +import NLambda +import Prelude hiding (map) +import System.Environment data Learner - = NomLStar -- nominal L* for nominal automata - | NomLStarCol -- nominal L* with counterexamples as columns (suffix closed) - | NomNLStar -- NL* for nominal automata, counterexamples as columns (suffix closed) + = NomLStar -- nominal L* for nominal automata + | NomLStarCol -- nominal L* with counterexamples as columns (suffix closed) + | NomNLStar -- NL* for nominal automata, counterexamples as columns (suffix closed) deriving (Show, Read) -data Teacher = EqDFA | EqNFA Int +data Teacher + = EqDFA -- Automatic teacher with membership and equivalence (only for DFAs) + | EqNFA Int -- Automatic teacher with membership and bounded equivalence + | EquivalenceIO -- Teacher with automatic membership but manual equivalence deriving (Show, Read) data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int | NonResidual | Residual1 | Residual2 deriving (Show, Read) -- existential wrapper -data A = forall q i . (LearnableAlphabet i, NominalType q, Show q) => A (Automaton q i) +data A = forall q i . (LearnableAlphabet i, Read i, NominalType q, Show q) => A (Automaton q i) mainExample :: String -> String -> String -> IO () mainExample learnerName teacherName autName = do A automaton <- return $ case read autName of - Fifo n -> A $ Examples.fifoExample n - Stack n -> A $ Examples.stackExample n - Running n -> A $ Examples.runningExample atoms n - NFA1 -> A $ Examples.exampleNFA1 - Bollig n -> A $ Examples.exampleNFA2 n + Fifo n -> A $ Examples.fifoExample n + Stack n -> A $ Examples.stackExample n + Running n -> A $ Examples.runningExample atoms n + NFA1 -> A $ Examples.exampleNFA1 + Bollig n -> A $ Examples.exampleNFA2 n NonResidual -> A $ Examples.exampleNonResidual - Residual1 -> A $ Examples.exampleResidual1 - Residual2 -> A $ Examples.exampleResidual2 + Residual1 -> A $ Examples.exampleResidual1 + Residual2 -> A $ Examples.exampleResidual2 let teacher = case read teacherName of - EqDFA -> teacherWithTarget automaton - EqNFA k -> teacherWithTargetNonDet k automaton + EqDFA -> teacherWithTarget automaton + EqNFA k -> teacherWithTargetNonDet k automaton + EquivalenceIO -> teacherWithTargetAndIO automaton let h = case read learnerName of NomLStar -> learnAngluinRows teacher NomLStarCol -> learnAngluin teacher @@ -49,7 +50,7 @@ mainExample learnerName teacherName autName = do mainWithIO :: String -> IO () mainWithIO learnerName = do - let t = teacherWithIO (atoms) + let t = teacherWithIO atoms let h = case read learnerName of NomLStar -> learnAngluinRows t NomLStarCol -> learnAngluin t diff --git a/src/Main2.hs b/src/Main2.hs index 2896c3b..a20bd08 100644 --- a/src/Main2.hs +++ b/src/Main2.hs @@ -1,17 +1,16 @@ -import Angluin -import Bollig -import Examples -import Teacher -import ObservationTable -import NLStar +import Angluin +import Bollig +import Examples +import Teacher -import System.Environment -import System.IO -import NLambda +import NLambda +import System.Environment +import System.IO data Learner = NomLStar | NomLStarCol | NomNLStar deriving (Show, Read) +learn :: (Read i, Contextual i, NominalType i, Show i) => Set i -> IO () learn alphSet = do [learnerName] <- getArgs let t = teacherWithIO2 alphSet @@ -23,7 +22,6 @@ learn alphSet = do main :: IO () main = do - [learnerName] <- getArgs putStrLn "ALPHABET" -- ask for the alphabet from the teacher hFlush stdout alph <- getLine diff --git a/src/NLStar.hs b/src/NLStar.hs index 08f7ba2..11d5e71 100644 --- a/src/NLStar.hs +++ b/src/NLStar.hs @@ -1,18 +1,15 @@ -{-# LANGUAGE RecordWildCards #-} +{-# language RecordWildCards #-} module NLStar where -import AbstractLStar -import Angluin -import Bollig -import ObservationTable -import Teacher +import AbstractLStar +import Angluin +import Bollig +import ObservationTable +import Teacher -import NLambda - -import Debug.Trace -import Data.List (inits, tails) -import Prelude hiding (and, curry, filter, lookup, map, not, - sum) +import Debug.Trace +import NLambda +import Prelude hiding (and, curry, filter, lookup, map, not, sum) {- This is not NL* from the Bollig et al paper. This is a very naive approximation. You see, the consistency in their paper is quite weak, diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs index 0e6512b..00eaba2 100644 --- a/src/ObservationTable.hs +++ b/src/ObservationTable.hs @@ -1,20 +1,20 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE RecordWildCards #-} +{-# language ConstraintKinds #-} +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} +{-# language FlexibleContexts #-} +{-# language FlexibleInstances #-} +{-# language RecordWildCards #-} module ObservationTable where -import NLambda hiding (fromJust) -import Teacher +import NLambda hiding (fromJust) +import Teacher -import Data.Maybe (fromJust) -import Debug.Trace (trace) -import GHC.Generics (Generic) -import Prelude (Bool (..), Eq, Ord, Show (..), ($), (++), (.), uncurry, id) -import qualified Prelude () +import Data.Maybe (fromJust) +import Debug.Trace (trace) +import GHC.Generics (Generic) +import Prelude (Bool (..), Eq, Ord, Show (..), id, uncurry, ($), (++), (.)) +import qualified Prelude () -- We represent functions as their graphs @@ -66,7 +66,7 @@ type BRow i = Row i Bool fillTable :: LearnableAlphabet i => Teacher i -> Set [i] -> Set [i] -> BTable i fillTable teacher sssa ee = Prelude.uncurry union . map2 (map slv) . map2 simplify . partition (\(_, _, f) -> f) $ base where - base0 = pairsWith (\s e -> (s++e)) sssa ee + base0 = pairsWith (++) sssa ee base1 = membership teacher base0 base1b s e = forAll id $ mapFilter (\(i,f) -> maybeIf (i `eq` (s++e)) f) base1 base = pairsWith (\s e -> (s, e, base1b s e)) sssa ee diff --git a/src/Teacher.hs b/src/Teacher.hs index a932d78..41c5adb 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -1,5 +1,5 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE FlexibleInstances #-} +{-# language FlexibleInstances #-} +{-# language RankNTypes #-} module Teacher ( module Teachers.Teacher @@ -11,8 +11,8 @@ module Teacher ) where import Teachers.Teacher -import Teachers.Whitebox import Teachers.Terminal +import Teachers.Whitebox import NLambda hiding (alphabet) import qualified NLambda (alphabet) @@ -65,16 +65,17 @@ teacherWithIO2 alph = Teacher -- 3. A teacher uses a target for the mebership queries, but you for equivalence -- Useful as long as you don't have an equivalence check -- used for NFAs when there was no bounded bisimulation yet -teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom +teacherWithTargetAndIO :: (Show i, Read i, NominalType i, Contextual i, NominalType q) => Automaton q i -> Teacher i teacherWithTargetAndIO aut = Teacher { membership = foreachQuery $ accepts aut , equivalent = ioEquivalent - , alphabet = atoms + , alphabet = NLambda.alphabet aut } +automaticEquivalent :: (p1 -> p2 -> Set a) -> p1 -> p2 -> Maybe (Set a) automaticEquivalent bisimlator aut hypo = case solve isEq of - Nothing -> error "should be solved" - Just True -> Nothing + Nothing -> error "should be solved" + Just True -> Nothing Just False -> Just bisimRes where bisimRes = bisimlator aut hypo diff --git a/src/Teachers/Teacher.hs b/src/Teachers/Teacher.hs index 66e7991..ff7174a 100644 --- a/src/Teachers/Teacher.hs +++ b/src/Teachers/Teacher.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes #-} +{-# language RankNTypes #-} module Teachers.Teacher where import NLambda @@ -25,4 +25,4 @@ data Teacher i = Teacher -- Often a membership query is defined by a function [i] -> Formula. This wraps -- such a function to the required type for a membership query (see above). foreachQuery :: NominalType i => ([i] -> Formula) -> Set[i] -> Set ([i], Formula) -foreachQuery f qs = map (\q -> (q, f q)) qs +foreachQuery f = map (\q -> (q, f q)) diff --git a/src/Teachers/Terminal.hs b/src/Teachers/Terminal.hs index 57b92ac..788af05 100644 --- a/src/Teachers/Terminal.hs +++ b/src/Teachers/Terminal.hs @@ -1,11 +1,9 @@ module Teachers.Terminal where -import NLambda - import Control.Monad import Data.IORef -import Data.List (intersperse, concat) -import Prelude hiding (filter, map, and, sum) +import NLambda +import Prelude hiding (and, filter, map, sum) import System.Console.Haskeline import System.IO.Unsafe (unsafePerformIO) import Text.Read (readMaybe) @@ -14,7 +12,7 @@ import Text.Read (readMaybe) ioMembership :: (Show i, NominalType i, Contextual i) => Set [i] -> Set ([i], Formula) ioMembership queries = unsafePerformIO $ do cache <- readIORef mqCache - let cachedAnswers = filter (\(a, f) -> a `member` queries) cache + let cachedAnswers = filter (\(a, _) -> a `member` queries) cache let newQueries = simplify $ queries \\ map fst cache let representedInputs = toList . mapFilter id . setOrbitsRepresentatives $ newQueries putStrLn "\n# Membership Queries:" @@ -27,7 +25,7 @@ ioMembership queries = unsafePerformIO $ do case x of Nothing -> error "Bye bye, have a good day!" Just Nothing -> do - outputStrLn $ "Unable to parse, try again" + outputStrLn "Unable to parse, try again" loop Just (Just f) -> return f answer <- runInputT defaultSettings loop @@ -46,18 +44,18 @@ ioMembership queries = unsafePerformIO $ do ioMembership2 :: (Show i, NominalType i, Contextual i) => Set [i] -> Set ([i], Formula) ioMembership2 queries = unsafePerformIO $ do cache <- readIORef mqCache - let cachedAnswers = filter (\(a, f) -> a `member` queries) cache + let cachedAnswers = filter (\(a, _) -> a `member` queries) cache let newQueries = simplify $ queries \\ map fst cache let representedInputs = toList . mapFilter id . setOrbitsRepresentatives $ newQueries answers <- forM representedInputs $ \input -> do - let str = Data.List.concat . intersperse " " . fmap show $ input + let str = unwords . fmap show $ input putStrLn $ "MQ \"" ++ str ++ "\"" let askit = do x <- getInputLine "" case x of Just "Y" -> return True Just "N" -> return False - _ -> error "Unable to parse, or quit. Bye!" + _ -> error "Unable to parse, or quit. Bye!" answer <- runInputT defaultSettings askit return $ orbit [] (input, fromBool answer) let answersAsSet = simplify . sum . fromList $ answers @@ -70,28 +68,40 @@ ioMembership2 queries = unsafePerformIO $ do mqCache = unsafePerformIO $ newIORef empty +newtype TestIO i = T [i] + deriving (Show, Read, Eq, Ord) + -- Poses a query to the terminal, waiting for the user to provide a counter example --- TODO: extend to any alphabet type (hard because of parsing) +-- User can pose a "test query" which is evaluated on the hypothesis ioEquivalent :: (Show q, NominalType q, Show i, Read i, NominalType i) => Automaton q i -> Maybe (Set [i]) ioEquivalent hypothesis = unsafePerformIO $ do putStrLn "\n# Is the following automaton correct?" putStr "# " print hypothesis - putStrLn "# \"^D\" for equivalent, \"[...]\" for a counter example (eg \"[0,1,0]\")" + putStrLn "# \"^D\" for equivalent; \"[...]\" for a counter example (eg \"[0,1,0]\"); \"T [...]\" for a test query." let loop = do - x <- fmap readMaybe <$> getInputLine "> " - case x of - Nothing -> do - outputStrLn $ "Ok, we're done" + resp <- getInputLine "> " + case resp of + Nothing -> do + outputStrLn "Ok, we're done" return Nothing - Just Nothing -> do - outputStrLn $ "Unable to parse (88), try again" - loop - Just (Just f) -> return (Just f) + Just inp -> + case readMaybe inp of + Just (T w) -> do + let a = accepts hypothesis w + outputStrLn $ show a + loop + Nothing -> + case readMaybe inp of + Just f -> return (Just f) + Nothing -> do + outputStrLn "Unable to parse (88), try again" + loop answer <- runInputT defaultSettings loop return (orbit [] <$> answer) -- Same as above but in different format. +-- This is used for automation and benchmarking different nominal tools ioEquivalent2 :: (Show q, NominalType q, Show i, Read i, NominalType i) => Automaton q i -> Maybe (Set [i]) ioEquivalent2 hypothesis = unsafePerformIO $ do putStrLn "EQ\n\"Is the following automaton correct?" @@ -110,4 +120,4 @@ ioEquivalent2 hypothesis = unsafePerformIO $ do readCE (' ' : xs) = readCE xs readCE xs = case reads xs of [(a, str)] -> a : readCE str - _ -> error "Unable to parse (113)" + _ -> error "Unable to parse (113)" diff --git a/src/Teachers/Whitebox.hs b/src/Teachers/Whitebox.hs index 3bdf6a9..27ab232 100644 --- a/src/Teachers/Whitebox.hs +++ b/src/Teachers/Whitebox.hs @@ -3,7 +3,7 @@ module Teachers.Whitebox where import NLambda import Control.Monad.Identity -import Prelude hiding (map, sum, filter, not) +import Prelude hiding (filter, map, not, sum) -- I found it a bit easier to write a do-block below. So I needed this -- Conditional instance. @@ -21,7 +21,7 @@ bisim aut1 aut2 = runIdentity $ go empty (pairsWith addEmptyWord (initialStates -- if elements are already in R, we can skip them let todo2 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo -- split into correct pairs and wrong pairs - let (cont, ces) = partition (\(_, x, y) -> (x `member` (finalStates aut1)) <==> (y `member` (finalStates aut2))) todo2 + let (cont, ces) = partition (\(_, x, y) -> (x `member` finalStates aut1) <==> (y `member` finalStates aut2)) todo2 let aa = NLambda.alphabet aut1 -- the good pairs should make one step let dtodo = sum (pairsWith (\(w, x, y) a -> pairsWith (\x2 y2 -> (a:w, x2, y2)) (d aut1 a x) (d aut2 a y)) cont aa) @@ -32,7 +32,7 @@ bisim aut1 aut2 = runIdentity $ go empty (pairsWith addEmptyWord (initialStates -- else continue with good pairs (ite (isEmpty dtodo) (return empty) - (go (rel `union` map stripWord cont) (dtodo)) + (go (rel `union` map stripWord cont) dtodo) ) d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut) stripWord (_, x, y) = (x, y) @@ -63,7 +63,7 @@ bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates a -- filter out things expressed as sums let todo2 = filter (\(_, x, y) -> notSums x y) todo1 -- split into correct pairs and wrong pairs - let (cont, ces) = partition (\(_, x, y) -> (x `intersect` (finalStates aut1)) <==> (y `intersect` (finalStates aut2))) todo2 + let (cont, ces) = partition (\(_, x, y) -> (x `intersect` finalStates aut1) <==> (y `intersect` finalStates aut2)) todo2 let aa = NLambda.alphabet aut1 -- the good pairs should make one step let dtodo = pairsWith (\(w, x, y) a -> (a:w, sumMap (d aut1 a) x, sumMap (d aut2 a) y)) cont aa @@ -75,10 +75,9 @@ bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates a -- else continue with good pairs (ite (isEmpty dtodo) (return empty) - (go (rel `union` map stripWord cont) (dtodo)) + (go (rel `union` map stripWord cont) dtodo) ) d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut) stripWord (_, x, y) = (x, y) getRevWord (w, _, _) = reverse w - addEmptyWord x y = ([], x, y) - sumMap f = sum . (map f) + sumMap f = sum . map f