From 15a02c4762244c46538c5582a21eacacd94c8df8 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 2 Dec 2016 15:49:48 +0100 Subject: [PATCH] Uses the new NLambda features for an external teacher --- src/Main.hs | 30 +++++++++++++-------- src/Teacher.hs | 73 ++++++++++++++++++++------------------------------ 2 files changed, 48 insertions(+), 55 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index b923b0f..ae85e14 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -22,9 +22,8 @@ data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int -- existential wrapper data A = forall q i . (LearnableAlphabet i, NominalType q, Show q) => A (Automaton q i) -main :: IO () -main = do - [learnerName, teacherName, autName] <- getArgs +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 @@ -40,11 +39,20 @@ main = do NomNLStar -> learnBollig teacher putStrLn "Finished! Final hypothesis =" print h - --eqs <- readIORef eqCounter - --mqs <- readIORef mqCounter - --putStrLn "Number of equivalence queries:" - --print eqs - --putStrLn "Number of batched membership queries:" - --print (length mqs) - --putStrLn "Number of membership orbits:" - --mapM_ print $ reverse mqs + +mainWithIO :: String -> IO () +mainWithIO learnerName = do + let h = case read learnerName of + NomLStar -> learnAngluinRows teacherWithIO + NomLStarCol -> learnAngluin teacherWithIO + NomNLStar -> learnBollig teacherWithIO + putStrLn "Finished! Final hypothesis =" + print h + +main :: IO () +main = do + bla <- getArgs + case bla of + [learnerName, teacherName, autName] -> mainExample learnerName teacherName autName + [learnerName] -> mainWithIO learnerName + _ -> putStrLn "Give either 1 (for the IO teacher) or 3 (for automatic teacher) arguments" diff --git a/src/Teacher.hs b/src/Teacher.hs index d8f6311..b4e9096 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -13,10 +13,10 @@ import Data.List (zip, (!!), reverse) import Data.Maybe (Maybe (..)) import Prelude (Bool (..), Int, Read, Show, error, length, return, ($), (++), (-), (<), - (==), (.), (<=), (+), show, seq) + (==), (.), (<=), (+), show, seq, (<$>)) import qualified Prelude import Control.Monad.Identity (Identity(..)) -import Control.Monad (when) +import Control.Monad (when, forM) import Data.IORef (IORef, readIORef, newIORef, writeIORef) import System.IO.Unsafe (unsafePerformIO) @@ -81,7 +81,7 @@ teacherWithTargetNonDet n aut = Teacher -- consider the whole orbit generated by it. teacherWithIO :: Teacher Atom teacherWithIO = Teacher - { membership = foreachQuery ioMembership + { membership = ioMembership , equivalent = ioEquivalent , alphabet = atoms } @@ -227,31 +227,34 @@ bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates a sumMap f = sum . (map f) -- Posing a membership query to the terminal and waits for used to input a formula -ioMembership :: (Show i, NominalType i) => [i] -> Formula -ioMembership input = unsafePerformIO $ do - let supp = leastSupport input - Prelude.putStrLn "\n# Is the following word accepted?" - Prelude.putStr "# " - Prelude.print input - Prelude.putStrLn "# You can answer with a formula (EQ, NEQ, AND, OR, T, F)" - Prelude.putStrLn "# You may use the following atoms:" - Prelude.putStr "# " - Prelude.print $ zip supp [0..] - answer <- runInputT defaultSettings loop - return $ interpret supp answer - where - loop = do - x <- getInputLine "> " - case x of - Nothing -> error "Quit" - Just str -> do - case readMaybe str :: Maybe Form of - Nothing -> do - outputStrLn $ "Unable to parse " ++ str ++ " :: Form" - loop - Just f -> return f +ioMembership :: (Show i, NominalType i, Contextual i) => Set [i] -> Set ([i], Formula) +ioMembership inputs = unsafePerformIO $ do + let representedInputs = fromVariant . fromJust <$> (toList $ setOrbitsRepresentatives inputs) + Prelude.putStrLn "\n# Membership Queries:" + Prelude.putStrLn "# Please answer each query with either \"True\" or \"False\"" + answers <- forM representedInputs $ \input -> do + Prelude.putStr "Q: " + Prelude.print input + let loop = do + x <- getInputLine "A: " + case x of + Nothing -> error "Bye bye, have a good day!" + Just str -> do + case readMaybe str :: Maybe Bool of + Nothing -> do + outputStrLn $ "Unable to parse " ++ str ++ " :: Bool" + loop + Just f -> return f + answer <- runInputT defaultSettings loop + Prelude.print $ orbit [] (input, fromBool answer) + return $ orbit [] (input, fromBool answer) + let answersAsSet = sum . fromList $ answers + Prelude.putStrLn "\n# Thanks!" + Prelude.print answersAsSet + return answersAsSet -- 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 hypothesis = unsafePerformIO $ do Prelude.putStrLn "\n# Is the following automaton correct?" @@ -282,21 +285,3 @@ ioEquivalent hypothesis = unsafePerformIO $ do outputStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]" loop Just f -> return f - --- Data structure for reading formulas (with the derived Read instance) -data Form - = EQ Int Int - | NEQ Int Int - | AND Form Form - | OR Form Form - | T - | F - deriving (Read) - -interpret :: [Atom] -> Form -> Formula -interpret support (EQ i j) = eq (support !! i) (support !! j) -interpret support (NEQ i j) = neq (support !! i) (support !! j) -interpret support (AND f1 f2) = interpret support f1 /\ interpret support f2 -interpret support (OR f1 f2) = interpret support f1 \/ interpret support f2 -interpret _ T = true -interpret _ F = false