Uses the new NLambda features for an external teacher

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"

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