{-# LANGUAGE TemplateHaskell #-}
-- | This module contains everything related to the generation of the training data.
module ToTrain where

import Data.Maybe ( isJust )
import Data.List ( isPrefixOf, isInfixOf, find, nub )
import qualified Data.Set as S
import Data.FileEmbed ( embedStringFile )

import Control.Monad ( forM_, void, when, unless )
import Control.Monad.Writer ( WriterT(runWriterT) )
import Control.Monad.Error.Class ( catchError )
import Control.Monad.IO.Class ( liftIO )
import Control.Concurrent ( threadDelay )
import Control.Concurrent.Async ( race )

import Agda.Syntax.Common
  ( unArg, defaultArg, defaultArgInfo, namedArg )
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names ( namesIn )
import Agda.Syntax.Literal ( Literal(..) )
import Agda.Syntax.Internal.Generic ( TermLike, foldTerm )
import Agda.Syntax.Scope.Base ( nsInScope, allThingsInScope )
import Agda.Syntax.Scope.Monad ( getCurrentScope )

import Agda.Utils.Monad ( whenM, tell1 )
import Agda.Utils.Either ( caseEitherM )

import Agda.TypeChecking.Monad hiding (Reduced)
import Agda.TypeChecking.Reduce
  ( Simplify, simplify, Normalise, normalise, Reduce, reduce )
import Agda.TypeChecking.CheckInternal ( Action(..), defaultAction, checkInternal' )
import Agda.TypeChecking.Pretty ( PrettyTCM )


import AgdaInternals ()
import Output hiding ( Definition(..), Clause(..), Term(..), Type(..) )

-- * Wrapper around Agda's typechecking monad 'TCM'

-- | Additionally records/outputs training samples.
type C = WriterT [Sample] TCM

runC :: C () -> TCM [Sample]
runC :: C () -> TCM [Sample]
runC = (((), [Sample]) -> [Sample]
forall a b. (a, b) -> b
snd (((), [Sample]) -> [Sample])
-> TCMT IO ((), [Sample]) -> TCM [Sample]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (TCMT IO ((), [Sample]) -> TCM [Sample])
-> (C () -> TCMT IO ((), [Sample])) -> C () -> TCM [Sample]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C () -> TCMT IO ((), [Sample])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT

noop :: C ()
noop :: C ()
noop = () -> C ()
forall a. a -> WriterT [Sample] TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

silently :: C a -> C ()
silently :: forall a. C a -> C ()
silently C a
k = C a -> C ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void C a
k C () -> (TCErr -> C ()) -> C ()
forall a.
WriterT [Sample] TCM a
-> (TCErr -> WriterT [Sample] TCM a) -> WriterT [Sample] TCM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> C ()
noop

-- * Training data generation

-- | 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 'Output.Sample'
-- (i.e. context, type, and term) for a given subterm.
train :: TrainF
train :: TrainF
train Type
ty Term
t = do
  let ns :: [QName]
ns = Term -> [QName]
names Term
t
  InScopeSet
allNs <- NameSpace -> InScopeSet
nsInScope (NameSpace -> InScopeSet)
-> (Scope -> NameSpace) -> Scope -> InScopeSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope -> NameSpace
allThingsInScope (Scope -> InScopeSet)
-> WriterT [Sample] TCM Scope -> WriterT [Sample] TCM InScopeSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Scope -> WriterT [Sample] TCM Scope
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Scope
getCurrentScope
  Bool -> C () -> C ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([QName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QName]
ns) (C () -> C ()) -> C () -> C ()
forall a b. (a -> b) -> a -> b
$
    Bool -> C () -> C ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([QName] -> InScopeSet
forall a. Ord a => [a] -> Set a
S.fromList [QName]
ns InScopeSet -> InScopeSet -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` InScopeSet
allNs) (C () -> C ()) -> C () -> C ()
forall a b. (a -> b) -> a -> b
$ do
      Telescope
ctx <- WriterT [Sample] TCM Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      Doc
pctx <- TCMT IO Doc -> WriterT [Sample] TCM Doc
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Doc -> WriterT [Sample] TCM Doc)
-> TCMT IO Doc -> WriterT [Sample] TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Telescope
ctx; Doc
pty <- TCMT IO Doc -> WriterT [Sample] TCM Doc
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Doc -> WriterT [Sample] TCM Doc)
-> TCMT IO Doc -> WriterT [Sample] TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Type
ty; Doc
pt <- TCMT IO Doc -> WriterT [Sample] TCM Doc
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Doc -> WriterT [Sample] TCM Doc)
-> TCMT IO Doc -> WriterT [Sample] TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Term
t
      Reduced Type
rty <- Type -> WriterT [Sample] TCM (Reduced Type)
forall (m :: * -> *) a.
(MonadFail m, MonadTCM m, PrettyTCM a, Simplify a, Reduce a,
 Normalise a, Eq a) =>
a -> m (Reduced a)
mkReduced Type
ty
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"rty: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Type -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (Reduced Type -> Type
forall a. Reduced a -> a
original Reduced Type
rty)

      Reduced Term
rt <- Term -> WriterT [Sample] TCM (Reduced Term)
forall (m :: * -> *) a.
(MonadFail m, MonadTCM m, PrettyTCM a, Simplify a, Reduce a,
 Normalise a, Eq a) =>
a -> m (Reduced a)
mkReduced Term
t

      Telescope
ctx' <- TCM Telescope -> WriterT [Sample] TCM Telescope
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Telescope -> WriterT [Sample] TCM Telescope)
-> TCM Telescope -> WriterT [Sample] TCM Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Telescope
forall a b. (a ~> b) => a -> TCM b
convert Telescope
ctx
      Reduced Type
rty' <- TCM (Reduced Type) -> WriterT [Sample] TCM (Reduced Type)
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Reduced Type) -> WriterT [Sample] TCM (Reduced Type))
-> TCM (Reduced Type) -> WriterT [Sample] TCM (Reduced Type)
forall a b. (a -> b) -> a -> b
$ (Type -> TCMT IO Type) -> Reduced Type -> TCM (Reduced Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Reduced a -> f (Reduced b)
traverse Type -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
convert Reduced Type
rty
      Reduced Type
rt'  <- TCM (Reduced Type) -> WriterT [Sample] TCM (Reduced Type)
forall a. TCM a -> WriterT [Sample] TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Reduced Type) -> WriterT [Sample] TCM (Reduced Type))
-> TCM (Reduced Type) -> WriterT [Sample] TCM (Reduced Type)
forall a b. (a -> b) -> a -> b
$ (Term -> TCMT IO Type) -> Reduced Term -> TCM (Reduced Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Reduced a -> f (Reduced b)
traverse Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
convert Reduced Term
rt
      Sample -> C ()
forall ws w (m :: * -> *).
(Monoid ws, Singleton w ws, MonadWriter ws m) =>
w -> m ()
tell1 (Sample -> C ()) -> Sample -> C ()
forall a b. (a -> b) -> a -> b
$ Sample
        { ctx :: Pretty Telescope
ctx      = Doc -> String
prender Doc
pctx String -> Telescope -> Pretty Telescope
forall {a}. String -> a -> Pretty a
:> Telescope
ctx'
        , goal :: Pretty (Reduced Type)
goal     = Doc -> String
prender Doc
pty  String -> Reduced Type -> Pretty (Reduced Type)
forall {a}. String -> a -> Pretty a
:> Reduced Type
rty'
        , term :: Pretty (Reduced Type)
term     = Doc -> String
prender Doc
pt   String -> Reduced Type -> Pretty (Reduced Type)
forall {a}. String -> a -> Pretty a
:> Reduced Type
rt'
        , premises :: [String]
premises = (QName -> String) -> [QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QName -> String
ppName [QName]
ns
        }
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 TCMT IO Doc
"{"
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" ctx: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> String -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (Telescope -> String
forall a. Pretty a => a -> String
pp Telescope
ctx)
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"      *pretty: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
pctx
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" goal: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> String -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (Type -> String
forall a. Pretty a => a -> String
pp Type
ty)
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"      *pretty: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
pty
      Reduced Type -> C ()
forall (m :: * -> *) a.
(MonadTCM m, PrettyTCM a) =>
Reduced a -> m ()
reportReduced Reduced Type
rty
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" term: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> String -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (Term -> String
forall a. Pretty a => a -> String
pp Term
t)
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"      *pretty: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
pt
      Reduced Term -> C ()
forall (m :: * -> *) a.
(MonadTCM m, PrettyTCM a) =>
Reduced a -> m ()
reportReduced Reduced Term
rt
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" premises: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> [QName] -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm [QName]
ns
      Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 TCMT IO Doc
"}"

-- | Run the training function on each subterm of a definition.
forEachHole :: TrainF -> Definition -> C ()
forEachHole :: TrainF -> Definition -> C ()
forEachHole TrainF
trainF def :: Definition
def@Defn{Bool
[Maybe Name]
[Occurrence]
[Polarity]
[LocalDisplayForm]
Maybe QName
ArgInfo
Language
QName
Blocked_
Type
MutualId
Defn
NumGeneralizableArgs
CompiledRepresentation
InScopeSet
defArgInfo :: ArgInfo
defName :: QName
defType :: Type
defPolarity :: [Polarity]
defArgOccurrences :: [Occurrence]
defArgGeneralizable :: NumGeneralizableArgs
defGeneralizedParams :: [Maybe Name]
defDisplay :: [LocalDisplayForm]
defMutual :: MutualId
defCompiledRep :: CompiledRepresentation
defInstance :: Maybe QName
defCopy :: Bool
defMatchable :: InScopeSet
defNoCompilation :: Bool
defInjective :: Bool
defCopatternLHS :: Bool
defBlocked :: Blocked_
defLanguage :: Language
theDef :: Defn
defArgInfo :: Definition -> ArgInfo
defName :: Definition -> QName
defType :: Definition -> Type
defPolarity :: Definition -> [Polarity]
defArgOccurrences :: Definition -> [Occurrence]
defArgGeneralizable :: Definition -> NumGeneralizableArgs
defGeneralizedParams :: Definition -> [Maybe Name]
defDisplay :: Definition -> [LocalDisplayForm]
defMutual :: Definition -> MutualId
defCompiledRep :: Definition -> CompiledRepresentation
defInstance :: Definition -> Maybe QName
defCopy :: Definition -> Bool
defMatchable :: Definition -> InScopeSet
defNoCompilation :: Definition -> Bool
defInjective :: Definition -> Bool
defCopatternLHS :: Definition -> Bool
defBlocked :: Definition -> Blocked_
defLanguage :: Definition -> Language
theDef :: Definition -> Defn
..} = Bool -> C () -> C ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Definition -> Bool
ignoreDef Definition
def) (C () -> C ()) -> C () -> C ()
forall a b. (a -> b) -> a -> b
$ do
  Int -> TCMT IO Doc -> C ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
10 (TCMT IO Doc -> C ()) -> TCMT IO Doc -> C ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"------ definition: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> String -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (QName -> String
forall a. Pretty a => a -> String
pp QName
defName) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
" -------"
  ScopeInfo
sc <- WriterT [Sample] TCM ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  case Defn
theDef of
    (Function{[Clause]
Maybe Bool
Maybe [QName]
Maybe QName
Maybe Compiled
Maybe SplitTree
Maybe CompiledClauses
Maybe ExtLamInfo
Either ProjectionLikenessMissing Projection
IsAbstract
Delayed
FunctionInverse
Set FunctionFlag
funClauses :: [Clause]
funCompiled :: Maybe CompiledClauses
funSplitTree :: Maybe SplitTree
funTreeless :: Maybe Compiled
funCovering :: [Clause]
funInv :: FunctionInverse
funMutual :: Maybe [QName]
funAbstr :: IsAbstract
funDelayed :: Delayed
funProjection :: Either ProjectionLikenessMissing Projection
funFlags :: Set FunctionFlag
funTerminates :: Maybe Bool
funExtLam :: Maybe ExtLamInfo
funWith :: Maybe QName
funIsKanOp :: Maybe QName
funClauses :: Defn -> [Clause]
funCompiled :: Defn -> Maybe CompiledClauses
funSplitTree :: Defn -> Maybe SplitTree
funTreeless :: Defn -> Maybe Compiled
funCovering :: Defn -> [Clause]
funInv :: Defn -> FunctionInverse
funMutual :: Defn -> Maybe [QName]
funAbstr :: Defn -> IsAbstract
funDelayed :: Defn -> Delayed
funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funFlags :: Defn -> Set FunctionFlag
funTerminates :: Defn -> Maybe Bool
funExtLam :: Defn -> Maybe ExtLamInfo
funWith :: Defn -> Maybe QName
funIsKanOp :: Defn -> Maybe QName
..}) ->
      [Clause] -> (Clause -> C ()) -> C ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Clause]
funClauses ((Clause -> C ()) -> C ()) -> (Clause -> C ()) -> C ()
forall a b. (a -> b) -> a -> b
$ \c :: Clause
c@(Clause{Bool
NAPs
Maybe Bool
Maybe (Arg Type)
Maybe ModuleName
Maybe Term
Range
ExpandedEllipsis
Telescope
clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
namedClausePats :: NAPs
clauseBody :: Maybe Term
clauseType :: Maybe (Arg Type)
clauseCatchall :: Bool
clauseExact :: Maybe Bool
clauseRecursive :: Maybe Bool
clauseUnreachable :: Maybe Bool
clauseEllipsis :: ExpandedEllipsis
clauseWhereModule :: Maybe ModuleName
clauseLHSRange :: Clause -> Range
clauseFullRange :: Clause -> Range
clauseTel :: Clause -> Telescope
namedClausePats :: Clause -> NAPs
clauseBody :: Clause -> Maybe Term
clauseType :: Clause -> Maybe (Arg Type)
clauseCatchall :: Clause -> Bool
clauseExact :: Clause -> Maybe Bool
clauseRecursive :: Clause -> Maybe Bool
clauseUnreachable :: Clause -> Maybe Bool
clauseEllipsis :: Clause -> ExpandedEllipsis
clauseWhereModule :: Clause -> Maybe ModuleName
..}) -> Telescope -> C () -> C ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
clauseTel (C () -> C ()) -> C () -> C ()
forall a b. (a -> b) -> a -> b
$
        case (Maybe Term
clauseBody, Arg Type -> Type
forall e. Arg e -> e
unArg (Arg Type -> Type) -> Maybe (Arg Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Arg Type)
clauseType) of
          (Just Term
t, Just Type
ty) -> TrainF
go Type
ty Term
t
          (Maybe Term, Maybe Type)
_ -> C ()
noop
    Defn
_ -> C ()
noop
    -- TODO: get data from other places other than clause bodies
  where
    ignoreDef :: Definition -> Bool
    ignoreDef :: Definition -> Bool
ignoreDef Defn{Bool
[Maybe Name]
[Occurrence]
[Polarity]
[LocalDisplayForm]
Maybe QName
ArgInfo
Language
QName
Blocked_
Type
MutualId
Defn
NumGeneralizableArgs
CompiledRepresentation
InScopeSet
defArgInfo :: Definition -> ArgInfo
defName :: Definition -> QName
defType :: Definition -> Type
defPolarity :: Definition -> [Polarity]
defArgOccurrences :: Definition -> [Occurrence]
defArgGeneralizable :: Definition -> NumGeneralizableArgs
defGeneralizedParams :: Definition -> [Maybe Name]
defDisplay :: Definition -> [LocalDisplayForm]
defMutual :: Definition -> MutualId
defCompiledRep :: Definition -> CompiledRepresentation
defInstance :: Definition -> Maybe QName
defCopy :: Definition -> Bool
defMatchable :: Definition -> InScopeSet
defNoCompilation :: Definition -> Bool
defInjective :: Definition -> Bool
defCopatternLHS :: Definition -> Bool
defBlocked :: Definition -> Blocked_
defLanguage :: Definition -> Language
theDef :: Definition -> Defn
defArgInfo :: ArgInfo
defName :: QName
defType :: Type
defPolarity :: [Polarity]
defArgOccurrences :: [Occurrence]
defArgGeneralizable :: NumGeneralizableArgs
defGeneralizedParams :: [Maybe Name]
defDisplay :: [LocalDisplayForm]
defMutual :: MutualId
defCompiledRep :: CompiledRepresentation
defInstance :: Maybe QName
defCopy :: Bool
defMatchable :: InScopeSet
defNoCompilation :: Bool
defInjective :: Bool
defCopatternLHS :: Bool
defBlocked :: Blocked_
defLanguage :: Language
theDef :: Defn
..}
        = Bool
False
       Bool -> Bool -> Bool
|| String -> Bool
tooSlow (QName -> String
forall a. Pretty a => a -> String
pp QName
defName)
      -- || defCopy
      -- || defNoCompilation
      -- || null (inverseScopeLookupName defName sc)
      -- || isAnonymousModuleName (qnameModule defName)
      -- || ("._." `isInfixOf` pp defName)
      -- || (getOrigin defName /= UserWritten)
      -- || ( ("with-" `isPrefixOf` pp (qnameName defName))

    ignore :: Type -> C Bool
    ignore :: Type -> C Bool
ignore Type
ty = do
      [Type]
ctx <- (Dom' Term (Name, Type) -> Type)
-> [Dom' Term (Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (Name, Type)] -> [Type])
-> WriterT [Sample] TCM [Dom' Term (Name, Type)]
-> WriterT [Sample] TCM [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT [Sample] TCM [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
      Bool -> C Bool
forall a. a -> WriterT [Sample] TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Bool
ignoreType Type
ty Bool -> Bool -> Bool
|| (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
ignoreCtxType [Type]
ctx)

    ignoreType, ignoreCtxType :: Type -> Bool
    ignoreType :: Type -> Bool
ignoreType    = (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any String -> Bool
cubicalRelated ([String] -> Bool) -> (Type -> [String]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> String) -> [QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QName -> String
forall a. Pretty a => a -> String
pp ([QName] -> [String]) -> (Type -> [QName]) -> Type -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [QName]
names (Term -> [QName]) -> (Type -> Term) -> Type -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl
    ignoreCtxType :: Type -> Bool
ignoreCtxType = (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any String -> Bool
cubicalRelated ([String] -> Bool) -> (Type -> [String]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> String) -> [QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QName -> String
forall a. Pretty a => a -> String
pp ([QName] -> [String]) -> (Type -> [QName]) -> Type -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [QName]
names (Term -> [QName]) -> (Type -> Term) -> Type -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl

    cubicalRelated, tooSlow :: String -> Bool
    cubicalRelated :: String -> Bool
cubicalRelated = (String
"Agda.Primitive.Cubical.I" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf`)
    tooSlow :: String -> Bool
tooSlow
       = (String
"Data.Rational.Properties" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`)
      (String -> Bool) -> (String -> Bool) -> String -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
\/ (String
"Prelude.Solvers" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`)
      (String -> Bool) -> (String -> Bool) -> String -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
\/ (String
"foundation.partitions" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`)
      (String -> Bool) -> (String -> Bool) -> String -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
\/ (String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
defsToSkip)

    go :: Type -> Term -> C ()
    go :: TrainF
go Type
ty Term
t = C Bool -> C () -> C ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Bool -> Bool
not (Bool -> Bool) -> C Bool -> C Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> C Bool
ignore Type
ty)
            (C () -> C ()) -> C () -> C ()
forall a b. (a -> b) -> a -> b
$ C Term -> C ()
forall a. C a -> C ()
silently (Action (WriterT [Sample] TCM)
-> Term -> Comparison -> Type -> C Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action (WriterT [Sample] TCM)
act Term
t Comparison
CmpLeq Type
ty)

    act :: Action C
    act :: Action (WriterT [Sample] TCM)
act = Action (WriterT [Sample] TCM)
forall (m :: * -> *). PureTCM m => Action m
defaultAction {preAction :: Type -> Term -> C Term
preAction = Type -> Term -> C Term
pre}

    pre :: Type -> Term -> C Term
    pre :: Type -> Term -> C Term
pre Type
ty Term
t = TrainF
trainF Type
ty Term
t C () -> C Term -> C Term
forall a b.
WriterT [Sample] TCM a
-> WriterT [Sample] TCM b -> WriterT [Sample] TCM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> C Term
forall a. a -> WriterT [Sample] TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

-- | Read a list of definitions to skip from @data/defsToSkip.txt@.
defsToSkip :: [String]
defsToSkip :: [String]
defsToSkip = String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ $(embedStringFile "data/defsToSkip.txt")

-- | Gathering names from terms.
names :: Term -> [QName]
names :: Term -> [QName]
names = [QName] -> [QName]
forall a. Eq a => [a] -> [a]
nub ([QName] -> [QName]) -> (Term -> [QName]) -> Term -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [QName]
forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn

-- * Reduction

-- | The hard limit on how much time can be spent on normalising a single term.
maxDuration :: Int
maxDuration = Int
2 -- seconds

withTimeout :: TCM a -> TCM (Maybe a)
withTimeout :: forall a. TCM a -> TCM (Maybe a)
withTimeout TCM a
k = TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC TCMT IO TCState
-> (TCState -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ TCState
s -> IO (Maybe a) -> TCMT IO (Maybe a)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe a) -> TCMT IO (Maybe a))
-> IO (Maybe a) -> TCMT IO (Maybe a)
forall a b. (a -> b) -> a -> b
$
  IO (Either () a)
-> (() -> IO (Maybe a)) -> (a -> IO (Maybe a)) -> IO (Maybe a)
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM
    (IO () -> IO a -> IO (Either () a)
forall a b. IO a -> IO b -> IO (Either a b)
race (Int -> IO ()
threadDelay (Int
maxDuration Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000000))
          ((a, TCState) -> a
forall a b. (a, b) -> a
fst ((a, TCState) -> a) -> IO (a, TCState) -> IO a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a -> TCState -> IO (a, TCState)
forall a. TCM a -> TCState -> IO (a, TCState)
runSafeTCM TCM a
k TCState
s))
    (\() -> Maybe a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing)
    (Maybe a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> (a -> Maybe a) -> a -> IO (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just)

mkReduced ::
  ( MonadFail m, MonadTCM m, PrettyTCM a
  , Simplify a, Reduce a, Normalise a, Eq a
  ) => a -> m (Reduced a)
mkReduced :: forall (m :: * -> *) a.
(MonadFail m, MonadTCM m, PrettyTCM a, Simplify a, Reduce a,
 Normalise a, Eq a) =>
a -> m (Reduced a)
mkReduced a
t = do
  -- try different reductions (with timeout)
  [Maybe a
_, Maybe a
simplified, Maybe a
reduced, Maybe a
normalised] <- [Maybe a] -> [Maybe a]
forall a. Eq a => [Maybe a] -> [Maybe a]
compressList ([Maybe a] -> [Maybe a])
-> ([Maybe a] -> [Maybe a]) -> [Maybe a] -> [Maybe a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe a
forall a. a -> Maybe a
Just a
t Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
:)
    ([Maybe a] -> [Maybe a]) -> m [Maybe a] -> m [Maybe a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCM a -> m (Maybe a)) -> [TCM a] -> m [Maybe a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TCM (Maybe a) -> m (Maybe a)
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe a) -> m (Maybe a))
-> (TCM a -> TCM (Maybe a)) -> TCM a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM a -> TCM (Maybe a)
forall a. TCM a -> TCM (Maybe a)
withTimeout) [a -> TCM a
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify a
t, a -> TCM a
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce a
t, a -> TCM a
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise a
t]
  Reduced a -> m (Reduced a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced a -> m (Reduced a)) -> Reduced a -> m (Reduced a)
forall a b. (a -> b) -> a -> b
$ Reduced {original :: a
original = a
t, Maybe a
simplified :: Maybe a
reduced :: Maybe a
normalised :: Maybe a
simplified :: Maybe a
reduced :: Maybe a
normalised :: Maybe a
..}
  where
    compressList :: Eq a => [Maybe a] -> [Maybe a]
    compressList :: forall a. Eq a => [Maybe a] -> [Maybe a]
compressList [Maybe a]
xs = (a -> Bool) -> Maybe a -> Maybe a
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Maybe a -> [Maybe a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Maybe a]
xs) (Maybe a -> Bool) -> (a -> Maybe a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just) (Maybe a -> Maybe a) -> [Maybe a] -> [Maybe a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe a]
xs

reportReduced :: (MonadTCM m, PrettyTCM a) => Reduced a -> m ()
reportReduced :: forall (m :: * -> *) a.
(MonadTCM m, PrettyTCM a) =>
Reduced a -> m ()
reportReduced Reduced{a
Maybe a
original :: forall a. Reduced a -> a
simplified :: forall a. Reduced a -> Maybe a
reduced :: forall a. Reduced a -> Maybe a
normalised :: forall a. Reduced a -> Maybe a
original :: a
simplified :: Maybe a
reduced :: Maybe a
normalised :: Maybe a
..} = do
  Int -> TCMT IO Doc -> m ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  *simplified: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Maybe a -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Maybe a
simplified
  Int -> TCMT IO Doc -> m ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"     *reduced: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Maybe a -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Maybe a
reduced
  Int -> TCMT IO Doc -> m ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  *normalised: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Maybe a -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Maybe a
normalised