-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Agda backend to generate training data for machine learning purposes.
--   
--   Compiles Agda modules to JSON files, containing information about the
--   imported scope of each module, its definitions and information about
--   each sub-term appearing in the code (i.e. context, goal type, term).
@package agda2train
@version 0.0.3.0


-- | Missing instances for WriterT in Agda's internals.
--   
--   NB: we are not exporting any definitions, just typeclass instances.
module AgdaInternals
instance (GHC.Base.Monoid r, GHC.Base.Monad m, GHC.Base.Semigroup (m Agda.TypeChecking.Pretty.Doc)) => GHC.Base.Semigroup (Control.Monad.Trans.Writer.Lazy.WriterT r m Agda.TypeChecking.Pretty.Doc)
instance (GHC.Base.Monoid r, GHC.Base.Monad m, Data.String.IsString (m a)) => Data.String.IsString (Control.Monad.Trans.Writer.Lazy.WriterT r m a)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Monad.Base.MonadStConcreteNames m) => Agda.TypeChecking.Monad.Base.MonadStConcreteNames (Control.Monad.Trans.Writer.Lazy.WriterT r m)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Monad.MetaVars.MonadInteractionPoints m) => Agda.TypeChecking.Monad.MetaVars.MonadInteractionPoints (Control.Monad.Trans.Writer.Lazy.WriterT r m)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Monad.Base.MonadFresh i m) => Agda.TypeChecking.Monad.Base.MonadFresh i (Control.Monad.Trans.Writer.Lazy.WriterT r m)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Warnings.MonadWarning m) => Agda.TypeChecking.Warnings.MonadWarning (Control.Monad.Trans.Writer.Lazy.WriterT r m)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Monad.Base.MonadBlock m) => Agda.TypeChecking.Monad.Base.MonadBlock (Control.Monad.Trans.Writer.Lazy.WriterT r m)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Monad.Base.MonadTCM m, Agda.TypeChecking.Monad.Constraints.MonadConstraint m) => Agda.TypeChecking.Monad.Constraints.MonadConstraint (Control.Monad.Trans.Writer.Lazy.WriterT r m)
instance (GHC.Base.Monoid r, Agda.TypeChecking.Monad.Base.MonadTCM m, Agda.TypeChecking.Monad.MetaVars.MonadMetaSolver m) => Agda.TypeChecking.Monad.MetaVars.MonadMetaSolver (Control.Monad.Trans.Writer.Lazy.WriterT r m)


-- | Defines the structure of the training data, as well as how to
--   translate internal Agda definition to this format.
module Output

-- | Name identifiers.
type Name = String

-- | DeBruijn indices.
type DB = Int

-- | A head of a λ-application can either be a defined name in the global
--   scope, or a DeBruijn index into the local context.
type Head = Either Name DB
pattern (:>) :: String -> a -> Pretty a
infixr 4 :>

-- | Bundle a thing with its "pretty" version.
--   
--   NB: In JSON format, we follow a <i>shallow</i> encoding with "pretty"
--   being an additional field and "thing" just inlined in the top-level
--   record.
data Pretty a
Pretty :: String -> a -> Pretty a
[pretty] :: Pretty a -> String
[thing] :: Pretty a -> a

-- | Bundle a term with (several of) its normalised forms.
--   
--   We do not repeat identical elements in subsequent evaluations (in the
--   order simp<i>red</i>norm) and some fields may not be populated due to
--   the evaluation taking to long and leading to a timeout (currently 2
--   seconds).
--   
--   NB: Like <a>Named</a>, encoded in a <i>shallow</i> JSON.
data Reduced a
Reduced :: a -> Maybe a -> Maybe a -> Maybe a -> Reduced a
[original] :: Reduced a -> a
[simplified] :: Reduced a -> Maybe a
[reduced] :: Reduced a -> Maybe a
[normalised] :: Reduced a -> Maybe a
pattern (:~) :: Name -> a -> Named a
infixr 4 :~

-- | Bundle a thing with its name.
--   
--   NB: Like <a>Named</a> and <a>Reduced</a>, encoded in a <i>shallow</i>
--   JSON.
data Named a
Named :: Name -> a -> Named a
[name] :: Named a -> Name
[item] :: Named a -> a

-- | Data for a file include the filename and its training data.
type FileData = Named TrainData

-- | The training data for a module, divided into three parts.
data TrainData
TrainData :: [ScopeEntry] -> [ScopeEntry] -> Maybe [ScopeEntry] -> TrainData

-- | The <i>global</i> scope, giving the types and definitions of all
--   <tt>import</tt> statements.
--   
--   NB: does not contain any <i>holes</i> for subterms.
[scopeGlobal] :: TrainData -> [ScopeEntry]

-- | The <i>local</i> scope, containing the types, definitions, and
--   training data for each of this module's definitions.
[scopeLocal] :: TrainData -> [ScopeEntry]

-- | The <i>private</i> scope, containing private definitions not exported
--   to the public, as well as system-generated definitions stemming from
--   <tt>where</tt> or <tt>with</tt>.
[scopePrivate] :: TrainData -> Maybe [ScopeEntry]

-- | Every <a>ScopeEntry'</a> is <i>named</i>.
type ScopeEntry = Named ScopeEntry'

-- | An entry in the scope: type, definitions, and holes.
data ScopeEntry'
ScopeEntry :: Pretty (Reduced Type) -> Maybe (Pretty Definition) -> Maybe [Sample] -> ScopeEntry'

-- | The entry's type.
[_type] :: ScopeEntry' -> Pretty (Reduced Type)

-- | The actual body of this entry's definition.
[definition] :: ScopeEntry' -> Maybe (Pretty Definition)

-- | Training data for each of the subterms in this entry's
--   <a>definition</a>.
[holes] :: ScopeEntry' -> Maybe [Sample]

-- | The training sample for each sub-hole.
data Sample
Sample :: Pretty Telescope -> Pretty (Reduced Type) -> Pretty (Reduced Term) -> [Name] -> Sample

-- | The current context, as a <i>binding telescope</i>.
[ctx] :: Sample -> Pretty Telescope

-- | The current goal, i.e. type of the sub-term.
--   
--   NB: DeBruijn indices here refer to the <a>ctx</a>.
[goal] :: Sample -> Pretty (Reduced Type)

-- | The term that successfully fills the current <a>goal</a>.
[term] :: Sample -> Pretty (Reduced Term)

-- | Definitions used in this "proof", intended to be used for <i>premise
--   selection</i>.
[premises] :: Sample -> [Name]

-- | Agda definitions: datatypes, records, functions, postulates and
--   primitives.
data Definition

-- | e.g. data ℕ : Set where zero : ℕ suc : ℕ → ℕ
ADT :: [Type] -> Definition
[variants] :: Definition -> [Type]

-- | e.g. `(ℕ, 0) ~ zero` or `(ℕ, 1) ~ suc`
Constructor :: Name -> Integer -> Definition
[reference] :: Definition -> Name
[variant] :: Definition -> Integer

-- | e.g. record X : Set where field x : ℕ y : ℕ
Record :: Telescope -> [Type] -> Definition
[telescope] :: Definition -> Telescope
[fields] :: Definition -> [Type]

-- | e.g. f [] = [] f (x ∷ xs) = x ∷ x ∷ xs
Function :: [Clause] -> Definition
[clauses] :: Definition -> [Clause]

-- | e.g. `postulate pred : ℕ → ℕ`
Postulate :: Definition

-- | e.g. `primitive primShowNat : ℕ → String`
Primitive :: Definition

-- | Function clauses.
data Clause
Clause :: Telescope -> [Pattern] -> Maybe Term -> Clause

-- | the telescope induced by the clause's context and patterns
[_telescope] :: Clause -> Telescope

-- | the actual patterns of this function clause
[patterns] :: Clause -> [Pattern]

-- | the right hand side of the clause (<tt>Nothing</tt> for absurd
--   clauses)
[body] :: Clause -> Maybe Term

-- | A telescope is a sequence of (named) types, a.k.a. bindings.
type Telescope = [Named (Pretty Type)]

-- | We under-approximate patterns as terms, e.g. losing information about
--   forced patterns.
type Pattern = Term

-- | Types are the same as terms.
type Type = Term

-- | The AST of Agda terms.
data Term

-- | e.g. <tt>∀ {A : Set}. A → A</tt>
Pi :: Bool -> Named Term -> Term -> Term

-- | e.g. <tt>λ x. x</tt>
Lam :: Named Term -> Term

-- | e.g. <tt>f x (x + x)</tt> or @<tt>0 (λ x. x)</tt>
App :: Head -> [Term] -> Term

-- | e.g. <tt>42</tt> or <tt>"something"</tt>
Lit :: String -> Term

-- | e.g. <tt>Set</tt>
Sort :: String -> Term

-- | e.g. <tt>0ℓ</tt>
Level :: String -> Term

-- | i.e. <tt>{!!}</tt>
UnsolvedMeta :: Term

-- | Converting between two types <tt>a</tt> and <tt>b</tt> under Agda's
--   typechecking monad.
--   
--   NB: <a>go</a> is only used internally to de-clutter the recursive
--   calls.
class (~>) a b | a -> b
convert :: (~>) a b => a -> TCM b
go :: (~>) a b => a -> TCM b
pp :: Pretty a => a -> String
ppm :: (MonadPretty m, PrettyTCM a) => a -> m Doc
prender :: Doc -> String
pinterleave :: (Applicative m, Semigroup (m Doc)) => m Doc -> [m Doc] -> m Doc
pbindings :: (MonadPretty m, PrettyTCM a) => [(String, a)] -> [m Doc]
report :: MonadTCM m => VerboseLevel -> TCM Doc -> m ()
panic :: (Pretty a, Show a) => String -> a -> b
ppName :: QName -> String
unqualify :: QName -> String
(\/) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
isNotCubical :: Clause -> Bool

-- | Configure JSON to omit empty (optional) fields and switch from
--   camelCase to kebab-case.
jsonOpts :: Options
instance GHC.Generics.Generic (Output.Pretty a)
instance Data.Traversable.Traversable Output.Reduced
instance Data.Foldable.Foldable Output.Reduced
instance GHC.Base.Functor Output.Reduced
instance GHC.Generics.Generic (Output.Reduced a)
instance GHC.Show.Show a => GHC.Show.Show (Output.Named a)
instance GHC.Generics.Generic (Output.Named a)
instance Data.Aeson.Types.FromJSON.FromJSON Output.Term
instance GHC.Show.Show Output.Term
instance GHC.Generics.Generic Output.Term
instance GHC.Show.Show Output.Clause
instance GHC.Generics.Generic Output.Clause
instance Data.Aeson.Types.FromJSON.FromJSON Output.Definition
instance Data.Aeson.Types.ToJSON.ToJSON Output.Definition
instance GHC.Show.Show Output.Definition
instance GHC.Generics.Generic Output.Definition
instance Data.Aeson.Types.FromJSON.FromJSON Output.Sample
instance Data.Aeson.Types.ToJSON.ToJSON Output.Sample
instance GHC.Show.Show Output.Sample
instance GHC.Generics.Generic Output.Sample
instance GHC.Show.Show Output.ScopeEntry'
instance GHC.Generics.Generic Output.ScopeEntry'
instance GHC.Generics.Generic Output.TrainData
instance GHC.Show.Show a => GHC.Show.Show (Output.Pretty a)
instance GHC.Show.Show a => GHC.Show.Show (Output.Reduced a)
instance Agda.TypeChecking.Monad.Base.Definition Output.~> Output.Definition
instance Agda.TypeChecking.Monad.Base.Defn Output.~> Output.Definition
instance Agda.Syntax.Internal.Clause Output.~> Output.Clause
instance Agda.Syntax.Internal.DeBruijnPattern Output.~> Output.Pattern
instance Agda.Syntax.Internal.Telescope Output.~> Output.Telescope
instance Agda.Syntax.Internal.Type Output.~> Output.Type
instance Agda.Syntax.Internal.Term Output.~> Output.Term
instance Agda.Syntax.Internal.Elim Output.~> Output.Term
instance Data.Aeson.Types.ToJSON.ToJSON Output.TrainData
instance Data.Aeson.Types.FromJSON.FromJSON Output.TrainData
instance Data.Aeson.Types.ToJSON.ToJSON Output.ScopeEntry'
instance Data.Aeson.Types.FromJSON.FromJSON Output.ScopeEntry'
instance Data.Aeson.Types.ToJSON.ToJSON Output.Clause
instance Data.Aeson.Types.FromJSON.FromJSON Output.Clause
instance Data.Aeson.Types.ToJSON.ToJSON Output.Term
instance Data.Aeson.Types.ToJSON.ToJSON a => Data.Aeson.Types.ToJSON.ToJSON (Output.Named a)
instance Data.Aeson.Types.FromJSON.FromJSON a => Data.Aeson.Types.FromJSON.FromJSON (Output.Named a)
instance Data.Aeson.Types.ToJSON.ToJSON a => Data.Aeson.Types.ToJSON.ToJSON (Output.Reduced a)
instance Data.Aeson.Types.FromJSON.FromJSON a => Data.Aeson.Types.FromJSON.FromJSON (Output.Reduced a)
instance Data.Aeson.Types.ToJSON.ToJSON a => Data.Aeson.Types.ToJSON.ToJSON (Output.Pretty a)
instance Data.Aeson.Types.FromJSON.FromJSON a => Data.Aeson.Types.FromJSON.FromJSON (Output.Pretty a)
instance Agda.TypeChecking.Pretty.PrettyTCM Agda.TypeChecking.Monad.Base.Definition


-- | This module contains everything related to the generation of the
--   training data.
module ToTrain

-- | Additionally records/outputs training samples.
type C = WriterT [Sample] TCM
runC :: C () -> TCM [Sample]
noop :: C ()
silently :: C a -> C ()

-- | A training function generates training data for each typed sub-term,
--   with access to the local context via the typechecking monad.
type TrainF = Type -> Term -> C ()

-- | An example training function that records a <a>Sample</a> (i.e.
--   context, type, and term) for a given subterm.
train :: TrainF

-- | Run the training function on each subterm of a definition.
forEachHole :: TrainF -> Definition -> C ()

-- | Read a list of definitions to skip from <tt>data/defsToSkip.txt</tt>.
defsToSkip :: [String]

-- | Gathering names from terms.
names :: Term -> [QName]

-- | The hard limit on how much time can be spent on normalising a single
--   term.
maxDuration :: Int
withTimeout :: TCM a -> TCM (Maybe a)
mkReduced :: (MonadFail m, MonadTCM m, PrettyTCM a, Simplify a, Reduce a, Normalise a, Eq a) => a -> m (Reduced a)
reportReduced :: (MonadTCM m, PrettyTCM a) => Reduced a -> m ()