{-# OPTIONS --safe #-}

-- ----------------------------------------
-- Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda
-- ----------------------------------------
-- The source tarball with all source and html files can be downloaded via:
-- 
-- https://arxiv.org/src/⟨ARXIVID⟩v1
-- 
-- where ⟨ARXIVID⟩ is the identifier of this arxiv article (is not known
-- to the uploader prior to uploading version 1)

import Apartness
import Auxiliary-Definitions
import Finite
import Partial-Map
import ListBisect
import Utils
import Polynomial-vs-Exponential-Growth

-- Automata models:
import Mealy
import Moore
import DFA

import DFA-Examples.Password-DFA -- example of DFAs with singleton languages

-- General definitions of a learning game, learners, and teachers:
import Game-Basics
import Game-Definitions

-- The main theorem for verifying the run-time bound and thus also
-- the correctness of a learning algorithm:
import Learner-Correctness

-- ------------------------------------
-- Instances of the natural number ℕ guessing game:
-- ------------------------------------
import NatLearning
import NatExamples.SimpleLogLearner
import NatExamples.HonestTeacher
-- A learner that learns any number n within n guesses:
import NatExamples.LinearLearner
-- A learner that learns any number n within log(n) guesses:
import NatExamples.LogLearner
-- Even for a fixed interval of size k, there is a teacher
-- that keeps the learning game runing for at least log(k)
-- guesses:
import NatExamples.AdversarialTeacher
-- If the teacher does not have internal state, then there
-- is some learner that guesses the secret right away within
-- at most 2 guesses:
import NatExamples.GuessingLearner

-- ------------------------------------
-- Game definitions for other types of automata:
-- ------------------------------------
-- Deterministic Finite Automata:
import DFALearning
import DFA-Examples.Enumerator
import DFA-CE-Size-Learning
import DFA-Restricted-Learning
-- A teacher that proves that in the restricted setting
-- (without counterexamples but only a yes/no), learning with
-- a polynomial bound on queries is not possible:
import DFA-Examples.DFA-Restricted-Bound

-- Mealy machines:
import MealyLearning