Adds a class for tables

nominal-lstar.cabal

@@ -11,9 +11,7 @@ common stuff
   ghc-options:       -O2 -Wall
   build-depends:
     base >= 4.8 && < 5,
-    containers,
     haskeline,
-    mtl,
     NLambda >= 1.1
 
 library
@@ -32,6 +30,7 @@ library
     Examples.RunningExample,
     Examples.Stack,
     ObservationTable,
+    ObservationTableClass,
     SimpleObservationTable,
     Teacher,
     Teachers.Teacher,

src/Bollig.hs

@@ -1,9 +1,9 @@
 {-# language PartialTypeSignatures #-}
-{-# language RecordWildCards #-}
 {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 module Bollig where
 
 import AbstractLStar
+import ObservationTableClass
 import SimpleObservationTable
 import Teacher
 
@@ -31,55 +31,53 @@ mqToBool teacher words = answer
         answer = map (setB True) inw `union` map (setB False) outw
         setB b (w, _) = (w, b)
 
-tableAt :: NominalType i => BTable i -> [i] -> [i] -> Formula
-tableAt t s e = singleton True `eq` mapFilter (\(i, o) -> maybeIf ((s ++ e) `eq` i) o) (content t)
-
 rfsaClosednessTest :: NominalType i => Set (BRow i) -> BTable i -> TestResult i
-rfsaClosednessTest primesUpp t@Table{..} = case solve (isEmpty defect) of
+rfsaClosednessTest primesUpp t = case solve (isEmpty defect) of
     Just True  -> Succes
     Just False -> trace "Not closed" $ Failed defect empty
     Nothing    -> trace "@@@ Unsolved Formula (rfsaClosednessTest) @@@" $
                   Failed defect empty
     where
-        defect = filter (\ua -> brow t ua `neq` sum (filter (`isSubsetOf` brow t ua) primesUpp)) (rowsExt t)
+        defect = filter (\ua -> row t ua `neq` sum (filter (`isSubsetOf` row t ua) primesUpp)) (rowsExt t)
 
 rfsaConsistencyTest :: NominalType i => BTable i -> TestResult i
-rfsaConsistencyTest t@Table{..} = case solve (isEmpty defect) of
+rfsaConsistencyTest t = case solve (isEmpty defect) of
     Just True  -> Succes
     Just False -> trace "Not consistent" $ Failed empty defect
     Nothing    -> trace "@@@ Unsolved Formula (rfsaConsistencyTest) @@@" $
                   Failed empty defect
     where
-        candidates = pairsWithFilter (\u1 u2 -> maybeIf (brow t u2 `isSubsetOf` brow t u1) (u1, u2)) rows rows
-        defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt t (u1 ++ [a]) v) /\ tableAt t (u2 ++ [a]) v) (a:v)) candidates alph columns
+        candidates = pairsWithFilter (\u1 u2 -> maybeIf (row t u2 `isSubsetOf` row t u1) (u1, u2)) (rows t) (rows t)
+        defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt2 (u1 ++ [a]) v) /\ tableAt2 (u2 ++ [a]) v) (a:v)) candidates (alph t) (cols t)
+        tableAt2 s e = singleton True `eq` tableAt t s e
 
 constructHypothesisBollig :: NominalType i => Set (BRow i) -> BTable i -> Automaton (BRow i) i
-constructHypothesisBollig primesUpp t@Table{..} = automaton q alph d i f
+constructHypothesisBollig primesUpp t = automaton q (alph t) d i f
     where
         q = primesUpp
-        i = filter (`isSubsetOf` brow t []) q
+        i = filter (`isSubsetOf` rowEps t) q
         f = filter (`contains` []) q
         -- TODO: compute indices of primesUpp only once
-        d0 = triplesWithFilter (\s a bs2 -> maybeIf (bs2 `isSubsetOf` brow t (s ++ [a])) (brow t s, a, bs2)) rows alph q
+        d0 = triplesWithFilter (\s a bs2 -> maybeIf (bs2 `isSubsetOf` row t (s ++ [a])) (row t s, a, bs2)) (rows t) (alph t) q
         d = filter (\(q1, _, _) -> q1 `member` q) d0
 
 -- Adds all suffixes as columns
 -- TODO: do actual Rivest and Schapire
 addCounterExample :: NominalType i => MQ i Bool -> Set [i] -> BTable i -> BTable i
-addCounterExample mq ces t@Table{..} =
+addCounterExample mq ces t =
     let newColumns = sum . map (fromList . tails) $ ces
-        newColumnsRed = newColumns \\ columns
+        newColumnsRed = newColumns \\ cols t
      in addColumns mq newColumnsRed t
 
 learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (BRow i) i
-learnBollig k n teacher = learnBolligLoop teacher (initialTableSize (mqToBool teacher) (alphabet teacher) k n)
+learnBollig k n teacher = learnBolligLoop teacher (initialBTableSize (mqToBool teacher) (alphabet teacher) k n)
 
 learnBolligLoop :: (NominalType i, _) => Teacher i -> BTable i -> Automaton (BRow i) i
-learnBolligLoop teacher t@Table{..} =
+learnBolligLoop teacher t =
     let
         -- These simplify's do speed up
-        allRowsUpp = simplify $ map (brow t) rows
-        allRows = simplify $ allRowsUpp `union` map (brow t) (rowsExt t)
+        allRowsUpp = simplify $ map (row t) (rows t)
+        allRows = simplify $ allRowsUpp `union` map (row t) (rowsExt t)
         primesUpp = simplify $ filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp
 
         -- No worry, these are computed lazily

src/ObservationTableClass.hs

@@ -0,0 +1,43 @@
+{-# language TypeFamilies #-}
+{-# language FunctionalDependencies #-}
+
+module ObservationTableClass where
+
+import NLambda
+import Prelude ((++))
+
+-- Words are indices to our table
+type RowIndex i = [i]
+type ColumnIndex i = [i]
+
+-- Membership queries (TODO: move to Teacher)
+type MQ i o = Set [i] -> Set ([i], o)
+
+-- This is a fat class, so that instances could give more efficient implementations
+class (NominalType table, NominalType i, NominalType o) => ObservationTable table i o | table -> i o where
+  -- The type of data in a row is determined by the table
+  type Row table :: *
+
+  -- getters
+  rows :: table -> Set (RowIndex i)
+  cols :: table -> Set (ColumnIndex i)
+  alph :: table -> Set i
+  row :: table -> RowIndex i -> Row table
+  
+  -- perhaps not needed
+  tableAt :: table -> RowIndex i -> ColumnIndex i -> Set o
+
+  -- compound getters
+  rowsExt :: table -> Set (RowIndex i)
+  colsExt :: table -> Set (ColumnIndex i)
+
+  rowEps :: table -> Row table
+
+  -- updaters
+  addRows :: MQ i o -> Set (RowIndex i) -> table -> table
+  addColumns :: MQ i o -> Set (ColumnIndex i) -> table -> table
+
+  -- default implementations
+  rowsExt t = pairsWith (\r a -> r ++ [a]) (rows t) (alph t)
+  colsExt t = pairsWith (:) (alph t) (cols t)
+  rowEps t = row t []

src/SimpleObservationTable.hs

@@ -1,14 +1,22 @@
 {-# language DeriveAnyClass #-}
 {-# language DeriveGeneric #-}
 {-# language RecordWildCards #-}
+{-# language FlexibleInstances #-}
+{-# language MultiParamTypeClasses #-}
+{-# language TypeFamilies #-}
+{-# language PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 
 module SimpleObservationTable where
 
+import ObservationTableClass
+
 import NLambda hiding (fromJust)
 
 import GHC.Generics (Generic)
-import Prelude (Bool (..), Eq, Int, Ord, Show (..), fst, (++))
+import Prelude (Bool (..), Eq, Int, Ord, Show (..), fst, (++), (.))
 import qualified Prelude ()
+import Data.Coerce (coerce)
 
 
 -- We represent functions as their graphs
@@ -18,55 +26,88 @@ type Fun i o = Set (i, o)
 dom :: (NominalType i, NominalType o) => Fun i o -> Set i
 dom = map fst
 
--- Words are indices to our table
-type RowIndex i = [i]
-type ColumnIndex i = [i]
-
 -- A table is nothing more than a part of the language.
 -- Invariant: content is always defined for elements in
 -- `rows * columns` and `rows * alph * columns`.
 data Table i o = Table
     { content :: Fun [i] o
-    , rows    :: Set (RowIndex i)
-    , columns :: Set (ColumnIndex i)
-    , alph    :: Set i
+    , rowIndices :: Set (RowIndex i)
+    , colIndices :: Set (ColumnIndex i)
+    , aa    :: Set i
     }
     deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual)
 
-rowsExt :: (NominalType i, NominalType o) => Table i o -> Set (RowIndex i)
-rowsExt Table{..} = pairsWith (\r a -> r ++ [a]) rows alph
+instance (NominalType i, NominalType o) => ObservationTable (Table i o) i o where
+    type Row (Table i o) = Fun [i] o
+    rows = rowIndices
+    cols = colIndices
+    alph = aa
+    row Table{..} r = pairsWithFilter (\e (a, b) -> maybeIf (a `eq` (r ++ e)) (e, b)) colIndices content
+    tableAt Table{..} r c = mapFilter (\(i, o) -> maybeIf ((r ++ c) `eq` i) o) content
 
-columnsExt :: (NominalType i, NominalType o) => Table i o -> Set (RowIndex i)
-columnsExt Table{..} = pairsWith (:) alph columns
+    -- Assumption: newRows is disjoint from rows (for efficiency)
+    addRows mq newRows t@Table{..} =
+        t { content = content `union` newContent
+          , rowIndices = rowIndices `union` newRows
+          }
+        where
+            newRowsExt = pairsWith (\r a -> r ++ [a]) newRows aa
+            newPart = pairsWith (++) (newRows `union` newRowsExt) colIndices
+            newPartRed = newPart \\ dom content
+            newContent = mq newPartRed
 
--- I could make a more specific implementation for booleans
--- But for now we reuse the above.
-type BTable i = Table i Bool
-
--- A row is the data in a table, i.e. a function from columns to the output
-type Row i o = Fun [i] o
-
-row :: (NominalType i, NominalType o) => Table i o -> RowIndex i -> Row i o
-row Table{..} r = pairsWithFilter (\e (a, b) -> maybeIf (a `eq` (r ++ e)) (e, b)) columns content
-
--- Special case of a boolean: functions to Booleans are subsets
-type BRow i = Set [i]
-
--- TODO: slightly inefficient
-brow :: NominalType i => BTable i -> RowIndex i -> BRow i
-brow Table{..} r = let lang = mapFilter (\(i, o) -> maybeIf (fromBool o) i) content
-                   in filter (\a -> lang `contains` (r ++ a)) columns
+    -- Assumption: newColumns is disjoint from columns (for efficiency)
+    addColumns mq newColumns t@Table{..} =
+        t { content = content `union` newContent
+          , colIndices = colIndices `union` newColumns
+          }
+        where
+            newColumnsExt = pairsWith (:) aa newColumns
+            newPart = pairsWith (++) rowIndices (newColumns `union` newColumnsExt)
+            newPartRed = newPart \\ dom content
+            newContent = mq newPartRed
 
 
--- Membership queries (TODO: move to Teacher)
-type MQ i o = Set [i] -> Set ([i], o)
+-- I could make a more specific implementation for booleans.
+-- But for now we reuse the above, and do minor optimisations
+
+newtype Boolean table = B { unB :: table }
+    deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual)
+
+type BTable i = Boolean (Table i Bool)
+
+instance (NominalType i) => ObservationTable (BTable i) i Bool where
+    -- Special case of a boolean: functions to Booleans are subsets
+    type Row (BTable i) = Set [i]
+    rows = coerce (rows :: _ => Table i Bool -> _)
+    cols = coerce (cols :: _ => Table i Bool -> _)
+    rowsExt = coerce (rowsExt :: _ => Table i Bool -> _)
+    colsExt = coerce (colsExt :: _ => Table i Bool -> _)
+    alph = coerce (alph :: _ => Table i Bool -> _)
+    tableAt = coerce (tableAt :: _ => Table i Bool -> _)
+    --rows = rowIndices . unB
+    --cols = colIndices . unB
+    --alph = aa . unB
+    --tableAt = tableAt . unB
+
+    -- TODO: slightly inefficient
+    row (B Table{..}) r = let lang = mapFilter (\(i, o) -> maybeIf (fromBool o) i) content
+                          in filter (\a -> lang `contains` (r ++ a)) colIndices
+    rowEps (B Table{..}) = mapFilter (\(i, o) -> maybeIf (fromBool o /\ i `member` colIndices) i) content
+    
+    --addRows mq newRows = B . addRows mq newRows . unB
+    addRows = coerce (addRows :: _ => _ -> _ -> Table i Bool -> Table i Bool)
+    --addColumns mq newColumns = B . addColumns mq newColumns . unB
+    addColumns = coerce (addColumns :: _ => _ -> _ -> Table i Bool -> Table i Bool)
+
+type BRow i = Row (BTable i)
 
 initialTableWith :: (NominalType i, NominalType o) => MQ i o -> Set i -> Set (RowIndex i) -> Set (ColumnIndex i) -> Table i o
 initialTableWith mq alphabet newRows newColumns = Table
     { content = content
-    , rows = newRows
-    , columns = newColumns
-    , alph = alphabet
+    , rowIndices = newRows
+    , colIndices = newColumns
+    , aa = alphabet
     }
     where
         newColumnsExt = pairsWith (:) alphabet newColumns
@@ -79,26 +120,11 @@ initialTable mq alphabet = initialTableWith mq alphabet (singleton []) (singleto
 initialTableSize :: (NominalType i, NominalType o) => MQ i o -> Set i -> Int -> Int -> Table i o
 initialTableSize mq alphabet rs cs = initialTableWith mq alphabet (replicateSetUntil rs alphabet) (replicateSetUntil cs alphabet)
 
--- Assumption: newRows is disjoint from rows (for efficiency)
-addRows :: (NominalType i, NominalType o) => MQ i o -> Set (RowIndex i) -> Table i o -> Table i o
-addRows mq newRows t@Table{..} =
-    t { content = content `union` newContent
-      , rows = rows `union` newRows
-      }
-    where
-        newRowsExt = pairsWith (\r a -> r ++ [a]) newRows alph
-        newPart = pairsWith (++) (newRows `union` newRowsExt) columns
-        newPartRed = newPart \\ dom content
-        newContent = mq newPartRed
+initialBTableWith :: NominalType i => MQ i Bool -> Set i -> Set (RowIndex i) -> Set (ColumnIndex i) -> BTable i
+initialBTableWith = coerce initialTableWith
 
--- Assumption: newColumns is disjoint from columns (for efficiency)
-addColumns :: (NominalType i, NominalType o) => MQ i o -> Set (ColumnIndex i) -> Table i o -> Table i o
-addColumns mq newColumns t@Table{..} =
-    t { content = content `union` newContent
-      , columns = columns `union` newColumns
-      }
-    where
-        newColumnsExt = pairsWith (:) alph newColumns
-        newPart = pairsWith (++) rows (newColumns `union` newColumnsExt)
-        newPartRed = newPart \\ dom content
-        newContent = mq newPartRed
+initialBTable :: NominalType i => MQ i Bool -> Set i -> BTable i
+initialBTable = coerce initialTable
+
+initialBTableSize :: NominalType i => MQ i Bool -> Set i -> Int -> Int -> BTable i
+initialBTableSize = coerce initialTableSize