diff --git a/src/Examples/Fifo.hs b/src/Examples/Fifo.hs index d38d9db..0e308d0 100644 --- a/src/Examples/Fifo.hs +++ b/src/Examples/Fifo.hs @@ -4,7 +4,7 @@ module Examples.Fifo (DataInput(..), fifoExample) where import Control.DeepSeq (NFData) import GHC.Generics (Generic) import NLambda -import Prelude (Eq, Int, Maybe (..), Ord, Show, length, reverse, +import Prelude (Eq, Int, Maybe (..), Ord, Show, Read, length, reverse, ($), (+), (-), (.), (>=)) import qualified Prelude () @@ -35,7 +35,7 @@ sizeFifo (Fifo l1 l2) = length l1 + length l2 -- nominal automaton. -- The alphabet: -data DataInput = Put Atom | Get Atom deriving (Eq, Ord, Show, Generic, NFData) +data DataInput = Put Atom | Get Atom deriving (Eq, Ord, Show, Read, Generic, NFData) instance BareNominalType DataInput instance Contextual DataInput where when f (Put a) = Put (when f a) diff --git a/src/Main.hs b/src/Main.hs index 81fdfcf..6437b54 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -10,6 +10,8 @@ import Data.IORef (readIORef) import System.Environment import NLambda +import Prelude hiding (map) + data Learner = NomLStar | NomLStarCol | NomNLStar deriving (Show, Read) @@ -41,10 +43,11 @@ mainExample learnerName teacherName autName = do mainWithIO :: String -> IO () mainWithIO learnerName = do + let t = teacherWithIO (map Put atoms `union` map Get atoms) let h = case read learnerName of - NomLStar -> learnAngluinRows teacherWithIO - NomLStarCol -> learnAngluin teacherWithIO - NomNLStar -> learnBollig teacherWithIO + NomLStar -> learnAngluinRows t + NomLStarCol -> learnAngluin t + NomNLStar -> learnBollig t print h main :: IO () diff --git a/src/Teacher.hs b/src/Teacher.hs index 5757f2e..0c0c293 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -46,11 +46,11 @@ teacherWithTargetNonDet n aut = Teacher -- Note that parsing is very unforgiving, one mistake, and there is no way back -- Atoms are referenced by Ints. When the user provides a counter example, we -- consider the whole orbit generated by it. -teacherWithIO :: Teacher Atom -teacherWithIO = Teacher +teacherWithIO :: (Show i, Read i, NominalType i, Contextual i) => Set i -> Teacher i +teacherWithIO alph = Teacher { membership = ioMembership , equivalent = ioEquivalent - , alphabet = atoms + , alphabet = alph } -- 3. A teacher uses a target for the mebership queries, but you for equivalence diff --git a/src/Teachers/Terminal.hs b/src/Teachers/Terminal.hs index e5b4592..5b4f621 100644 --- a/src/Teachers/Terminal.hs +++ b/src/Teachers/Terminal.hs @@ -10,12 +10,12 @@ import System.IO.Unsafe (unsafePerformIO) import Text.Read (readMaybe) -- Posing a membership query to the terminal and waits for used to input a formula -ioMembership :: Set [Atom] -> Set ([Atom], Formula) +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 newQueries = simplify $ queries \\ map fst cache - let representedInputs = fromVariant . fromJust <$> (toList $ setOrbitsRepresentatives newQueries) + let representedInputs = toList . mapFilter id . setOrbitsRepresentatives $ newQueries putStrLn "\n# Membership Queries:" putStrLn "# Please answer each query with \"True\" or \"False\" (\"^D\" for quit)" answers <- forM representedInputs $ \input -> do @@ -28,22 +28,22 @@ ioMembership queries = unsafePerformIO $ do Just Nothing -> do outputStrLn $ "Unable to parse, try again" loop - Just (Just f) -> return (f :: Bool) + Just (Just f) -> return f answer <- runInputT defaultSettings loop return $ orbit [] (input, fromBool answer) let answersAsSet = simplify . sum . fromList $ answers writeIORef mqCache (simplify $ cache `union` answersAsSet) return (simplify $ cachedAnswers `union` answersAsSet) + where + -- We use a cache, so that questions will not be repeated. + -- It is a bit hacky, as the Teacher interface does not allow state... + {-# NOINLINE mqCache #-} + mqCache = unsafePerformIO $ newIORef empty --- We use a cache, so that questions will not be repeated. --- It is a bit hacky, as the Teacher interface does not allow state... -mqCache :: IORef (Set ([Atom], Formula)) -{-# NOINLINE mqCache #-} -mqCache = unsafePerformIO $ newIORef empty -- 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) -ioEquivalent :: (Show q, NominalType q) => Automaton q Atom -> Maybe (Set [Atom]) +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 "# " @@ -58,17 +58,6 @@ ioEquivalent hypothesis = unsafePerformIO $ do Just Nothing -> do outputStrLn $ "Unable to parse, try again" loop - Just (Just f) -> return (Just f :: Maybe [Int]) + Just (Just f) -> return (Just f) answer <- runInputT defaultSettings loop - case answer of - Nothing -> return Nothing - Just input -> do - -- create sequences of same length - let n = length input - let sequence = replicateAtoms n - -- whenever two are identiacl in input, we will use eq, if not neq - let op i j = if (input !! i) == (input !! j) then eq else neq - -- copy the relations from input to sequence - let rels s = and [op i j (s !! i) (s !! j) | i <- [0..n - 1], j <- [0..n - 1], i < j] - let fseq = filter rels sequence - return $ Just fseq + return (orbit [] <$> answer)