From b273931b9caa5f8f7c85b4bc8194e739b0bd91a1 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <joshua.moerman@ou.nl>
Date: Wed, 6 Nov 2024 12:48:23 +0100
Subject: [PATCH] Made the teacher actually do something nontrivial

---
 app/IO.hs      |  15 ++++++
 app/LStar.hs   |   4 +-
 app/Teacher.hs | 135 ++++++++++++++++++++++++++++++++++++++++---------
 3 files changed, 127 insertions(+), 27 deletions(-)

diff --git a/app/IO.hs b/app/IO.hs
index c244241..dbe0ccd 100644
--- a/app/IO.hs
+++ b/app/IO.hs
@@ -56,3 +56,18 @@ instance FromStr a => FromStr [a] where
     where
       (a, str2) = fromStr str
       (l, emptyStr)    = fromStr (dropWhile isSpace str2)
+
+newtype MQ a = MQ a
+  deriving (Eq, Ord, Show)
+
+instance ToStr a => ToStr (MQ a) where
+  toStr (MQ a) = "MQ \"" <> toStr a <> "\""
+
+-- totally a hack, should do proper parsing at some point
+instance FromStr a => FromStr (MQ a) where
+  fromStr ('M':'Q':str) = let (a, rem) = fromStr (clean str) in (MQ a, rem)
+    where
+      trim str = dropWhile isSpace str
+      takeQ ('\"':rem) = rem
+      takeQ rem = error $ "parse error for MQ: " <> rem
+      clean = reverse . takeQ . trim . reverse . takeQ . trim
diff --git a/app/LStar.hs b/app/LStar.hs
index c769b1d..ca5bf05 100644
--- a/app/LStar.hs
+++ b/app/LStar.hs
@@ -153,9 +153,7 @@ learn mq eq = do
 -- Here is the teacher: just pose the queries in the terminal
 askMember :: _ => Word a -> IO Bool
 askMember w = do
-  putStr "MQ \""
-  putStr (toStr w)
-  putStrLn "\""
+  putStrLn (toStr (MQ w))
   hFlush stdout
   a <- getLine
   case a of
diff --git a/app/Teacher.hs b/app/Teacher.hs
index 9a9f62e..c0d360a 100644
--- a/app/Teacher.hs
+++ b/app/Teacher.hs
@@ -1,29 +1,116 @@
-import System.IO (hFlush, stderr, stdout, hPutStrLn)
+{-# LANGUAGE ImportQualifiedPost #-}
+
+import System.IO (hFlush, hPutStrLn, stderr, stdout)
+
+import Data.IORef
+import Data.Maybe (isJust)
+import System.Exit (exitFailure)
+import System.IO
+
+import ExampleAutomata
+import IO
+import Nominal (Atom)
+import OrbitList qualified
+import Support (Rat (..))
+
+data Example
+  = Fifo Int
+  | DoubleWord Int
 
--- TODO: Actually implement interesting languages... Not sure yet how I want
--- to do equivalence queries. Maybe let the teacher respond with a test
--- query to the learner?
 main :: IO ()
-main = do
+main =
+  let ex = Fifo 2
+   in case ex of
+        Fifo n -> teach "FIFO" (fifoFun n) (fifoCex n)
+        DoubleWord n -> teach "ATOMS" (doubleFun n) (doubleCex n)
+
+teach :: (ToStr a, FromStr a, Show a) => String -> ([a] -> Bool) -> [[a]] -> IO ()
+teach alphStr fun cexes = do
+  -- Set up some counters
+  countMQ <- newIORef (0 :: Int)
+  countEQ <- newIORef (0 :: Int)
+  cexChecks <- newIORef cexes
+
+  let
+    -- Helper functions for answering/logging
+    log str = hPutStrLn stderr str
+    answer str = hPutStrLn stdout str >> hFlush stdout
+
+    -- Parsing the commands from the learner
+    act message =
+      case message of
+        "ALPHABET" -> handleAlphabet
+        ('M' : 'Q' : _) -> handleMQ message
+        ('E' : 'Q' : _) -> handleEQ message
+        _ -> do
+          hPutStrLn stderr "Invalid command"
+          exitFailure
+
+    handleAlphabet = answer alphStr
+
+    handleMQ str = do
+      let (MQ word, _) = fromStr str
+          acc = fun word
+      answer $ if acc then "Y" else "N"
+
+      modifyIORef countMQ succ
+      n <- readIORef countMQ
+      log $ "MQ " <> show n <> ": " <> str <> " -> " <> show acc -- <> " (parsed as " <> show word <> ")"
+
+    handleEQ str = do
+      modifyIORef countEQ succ
+      n <- readIORef countEQ
+      log $ "EQ " <> show n <> ": " <> str
+
+      -- Currently, we handle equivalence queries very lazily: we simply pose
+      -- a possible counterexample to the learner (which it might actually do
+      -- correctly). There is no guarantee is will work.
+      possibleCexes <- readIORef cexChecks
+      case possibleCexes of
+        [] -> do
+          log " -> Y"
+          answer "Y"
+        (c : cs) -> do
+          log $ " -> N " <> toStr c
+          -- TODO: make this syntax the same as for MQs
+          answer $ "N " <> toStr c
+          writeIORef cexChecks cs
+
+  -- Lazily answer all queries, until the stream is closed
   messages <- lines <$> getContents
   mapM_ act messages
+
+  -- Then output some statistics
+  m <- readIORef countMQ
+  e <- readIORef countEQ
+  hPutStrLn stderr $ "Total number of MQ: " <> show m
+  hPutStrLn stderr $ "Total number of EQ: " <> show e
+
+-- examples from https://gitlab.science.ru.nl/moerman/nominal-learning-ons/-/blob/master/examples.hpp
+-- Note: we do not implement them as state machines. Instead we implement them
+-- as functions, to really make the point that this is "black box learning".
+
+fifoFun :: Int -> [FifoA] -> Bool
+fifoFun n = acc . foldl' step (Just [])
  where
-  act message =
-    case message of
-      "ALPHABET" -> handleAlphabet
-      str -> case take 2 message of
-        "MQ" -> handleMQ (drop 3 message)
-        "EQ" -> handleEQ (drop 3 message)
-  handleAlphabet = do
-    putStrLn "ATOMS"
-    hFlush stdout
-  handleMQ str = do
-    -- accepts any string
-    putStrLn "Y"
-    hPutStrLn stderr $ "MQ received: " <> str
-    hFlush stdout
-  handleEQ str = do
-    -- immediately accepts the hypothesis
-    putStrLn "Y"
-    hPutStrLn stderr $ "EQ received: " <> str
-    hFlush stdout
+  step Nothing _ = Nothing
+  step (Just ls) (Put a)
+    | length ls >= n = Nothing
+    | otherwise = Just (ls <> [a])
+  step (Just []) (Get a) = Nothing
+  step (Just (x : xs)) (Get a)
+    | a == x = Just xs
+    | otherwise = Nothing
+  acc = isJust
+
+fifoCex :: Int -> [[FifoA]]
+fifoCex n = concatMap dw [1 .. n]
+ where
+  dw k = [fmap Put w <> fmap Get w | w <- OrbitList.toList (OrbitList.repeatRationals k)]
+
+doubleFun :: Int -> [Atom] -> Bool
+doubleFun 0 w = w == []
+doubleFun n w = let (l, r) = splitAt n w in w /= [] && l == r
+
+doubleCex :: Int -> [[Atom]]
+doubleCex n = [w <> w | w <- OrbitList.toList (OrbitList.repeatRationals n)]