{-# LANGUAGE TypeApplications #-}
-- | Main driver for the @agda2train@ executable.
module Main where

import GHC.Generics

import System.Environment ( getArgs, withArgs )
import System.Directory ( createDirectoryIfMissing, doesFileExist )
import System.FilePath ( (</>) )
import System.Console.GetOpt ( OptDescr(..), ArgDescr(..) )

import qualified Data.List as L
import qualified Data.Set as S
import qualified Data.HashMap.Strict as HM
import qualified Data.ByteString.Lazy as BL
import Data.Aeson ( ToJSON )
import Data.Aeson.Encode.Pretty
  ( encodePretty', Config(..), defConfig, Indent(..), keyOrder )

import Control.Monad
import Control.Monad.IO.Class ( liftIO )
import Control.DeepSeq ( NFData )

import Agda.Main ( runAgda )
import Agda.Compiler.Backend hiding (Reduced)
import Agda.Compiler.Common ( curDefs )

import Agda.Utils.Pretty
import Agda.Utils.Maybe
import Agda.Utils.Monad

import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.TopLevelModuleName

import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Pretty as P

import Agda.Compiler.Common ( curIF )

import ToTrain
import Output

-- | The main entrypoint for the @agda2train@ executable.
main :: IO ()
IO ()
main = do
  [FilePath]
as <- IO [FilePath]
getArgs
  let extraFlags :: [a]
extraFlags = [] -- ["--no-projection-like"]
  [FilePath] -> IO () -> IO ()
forall a. [FilePath] -> IO a -> IO a
withArgs ([FilePath]
forall a. [a]
extraFlags [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
as) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    [Backend] -> IO ()
runAgda [Backend'
  Options
  Options
  ([ScopeEntry], [ScopeEntry])
  ()
  (FilePath, [Sample])
-> Backend
forall opts env menv mod def.
NFData opts =>
Backend' opts env menv mod def -> Backend
Backend (Backend'
   Options
   Options
   ([ScopeEntry], [ScopeEntry])
   ()
   (FilePath, [Sample])
 -> Backend)
-> Backend'
     Options
     Options
     ([ScopeEntry], [ScopeEntry])
     ()
     (FilePath, [Sample])
-> Backend
forall a b. (a -> b) -> a -> b
$ TrainF
-> Backend'
     Options
     Options
     ([ScopeEntry], [ScopeEntry])
     ()
     (FilePath, [Sample])
mkBackend TrainF
train]

-- | Make an Agda backend from a given training function (c.f. 'ToTrain.TrainF').
mkBackend :: TrainF ->
  Backend' Options Options ([ScopeEntry], [ScopeEntry]) () (String, [Sample])
mkBackend :: TrainF
-> Backend'
     Options
     Options
     ([ScopeEntry], [ScopeEntry])
     ()
     (FilePath, [Sample])
mkBackend TrainF
trainF = Backend'
  { backendName :: FilePath
backendName      = FilePath
"agda2train"
  , backendVersion :: Maybe FilePath
backendVersion   = Maybe FilePath
forall a. Maybe a
Nothing
  , options :: Options
options          = Options
defaultOptions
  , commandLineFlags :: [OptDescr (Flag Options)]
commandLineFlags =
      [ FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [Char
'r'] [FilePath
"recurse"] (Flag Options -> ArgDescr (Flag Options)
forall a. a -> ArgDescr a
NoArg Flag Options
forall (m :: * -> *). Monad m => Options -> m Options
recOpt)
        FilePath
"Recurse into imports/dependencies."
      , FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [Char
'x'] [FilePath
"no-json"] (Flag Options -> ArgDescr (Flag Options)
forall a. a -> ArgDescr a
NoArg Flag Options
forall (m :: * -> *). Monad m => Options -> m Options
noJsonOpt)
        FilePath
"Skip generation of JSON files. (just debug print)"
      , FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [] [FilePath
"ignore-existing-json"] (Flag Options -> ArgDescr (Flag Options)
forall a. a -> ArgDescr a
NoArg Flag Options
forall (m :: * -> *). Monad m => Options -> m Options
ignoreJsonOpt)
        FilePath
"Ignore existing JSON files. (i.e. always overwrite)"
      , FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [] [FilePath
"print-json"] (Flag Options -> ArgDescr (Flag Options)
forall a. a -> ArgDescr a
NoArg Flag Options
forall (m :: * -> *). Monad m => Options -> m Options
printJsonOpt)
        FilePath
"Print JSON output. (for debugging)"
      , FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [] [FilePath
"no-terms"] (Flag Options -> ArgDescr (Flag Options)
forall a. a -> ArgDescr a
NoArg Flag Options
forall (m :: * -> *). Monad m => Options -> m Options
includeDefsOpt)
        FilePath
"Do not include definitions of things in scope"
      , FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [] [FilePath
"no-privates"] (Flag Options -> ArgDescr (Flag Options)
forall a. a -> ArgDescr a
NoArg Flag Options
forall (m :: * -> *). Monad m => Options -> m Options
includePrivsOpt)
        FilePath
"Do not include private definitions"
      , FilePath
-> [FilePath]
-> ArgDescr (Flag Options)
-> FilePath
-> OptDescr (Flag Options)
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option [Char
'o'] [FilePath
"out-dir"] ((FilePath -> Flag Options) -> FilePath -> ArgDescr (Flag Options)
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag Options
forall (m :: * -> *). Monad m => FilePath -> Options -> m Options
outDirOpt FilePath
"DIR")
        FilePath
"Generate data at DIR. (default: project root)"
      ]
  , isEnabled :: Options -> Bool
isEnabled             = \ Options
_ -> Bool
True
  , scopeCheckingSuffices :: Bool
scopeCheckingSuffices = Bool
False
  , mayEraseType :: QName -> TCM Bool
mayEraseType          = \ QName
_ -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  , preCompile :: Options -> TCM Options
preCompile  = Options -> TCM Options
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  , postCompile :: Options -> IsMain -> Map TopLevelModuleName () -> TCM ()
postCompile = \ Options
_ IsMain
_ Map TopLevelModuleName ()
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , preModule :: Options
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
preModule   = \ Options
opts IsMain
isMain TopLevelModuleName
md Maybe FilePath
_ ->
      let
        processScopeEntry :: QName -> TCM (Maybe ScopeEntry)
        processScopeEntry :: QName -> TCM (Maybe ScopeEntry)
processScopeEntry QName
qn =
          TCMT IO (Maybe Type)
-> TCM (Maybe ScopeEntry)
-> (Type -> TCM (Maybe ScopeEntry))
-> TCM (Maybe ScopeEntry)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCMT IO Type -> TCMT IO (Maybe Type)
forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe (TCMT IO Type -> TCMT IO (Maybe Type))
-> TCMT IO Type -> TCMT IO (Maybe Type)
forall a b. (a -> b) -> a -> b
$ do
            Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
            case Definition -> Defn
theDef Definition
def of
              Defn
GeneralizableVar -> FilePath -> TCMT IO Type
forall a. FilePath -> TCMT IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
"not handling `variable` definitions"
              DataOrRecSig Int
_   -> FilePath -> TCMT IO Type
forall a. FilePath -> TCMT IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
"not handling `DataOrRecSig` definitions"
              Defn
_ -> QName -> TCMT IO Type
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
qn) (Maybe ScopeEntry -> TCM (Maybe ScopeEntry)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ScopeEntry
forall a. Maybe a
Nothing) ((Type -> TCM (Maybe ScopeEntry)) -> TCM (Maybe ScopeEntry))
-> (Type -> TCM (Maybe ScopeEntry)) -> TCM (Maybe ScopeEntry)
forall a b. (a -> b) -> a -> b
$ \Type
ty -> do
            Reduced Type
rty  <- Type -> TCMT IO (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
            Doc
pty  <- Type -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Type
ty
            Reduced Type
rty' <- (Type -> TCMT IO Type) -> Reduced Type -> TCMT IO (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

            Definition
def  <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
            Doc
pdef <- Definition -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Definition
def
            Definition
def' <- Definition -> TCM Definition
forall a b. (a ~> b) => a -> TCM b
convert Definition
def

            Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ FilePath -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (QName -> FilePath
forall a. Pretty a => a -> FilePath
pp QName
qn) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
" : " 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 Type
ty
            Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
<> FilePath -> TCMT IO Doc
forall (m :: * -> *). Applicative m => FilePath -> m Doc
P.text (Type -> FilePath
forall a. Pretty a => a -> FilePath
pp Type
ty)
            Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ FilePath -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (QName -> FilePath
forall a. Pretty a => a -> FilePath
pp QName
qn) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
" = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Definition -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Definition
def
            Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
<> FilePath -> TCMT IO Doc
forall (m :: * -> *). Applicative m => FilePath -> m Doc
P.text (Definition -> FilePath
forall a. Pretty a => a -> FilePath
pp Definition
def)
            Reduced Type -> TCM ()
forall (m :: * -> *) a.
(MonadTCM m, PrettyTCM a) =>
Reduced a -> m ()
reportReduced Reduced Type
rty
            Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
20 TCMT IO Doc
""

            Maybe ScopeEntry -> TCM (Maybe ScopeEntry)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ScopeEntry -> TCM (Maybe ScopeEntry))
-> Maybe ScopeEntry -> TCM (Maybe ScopeEntry)
forall a b. (a -> b) -> a -> b
$ ScopeEntry -> Maybe ScopeEntry
forall a. a -> Maybe a
Just (ScopeEntry -> Maybe ScopeEntry) -> ScopeEntry -> Maybe ScopeEntry
forall a b. (a -> b) -> a -> b
$ QName -> FilePath
ppName QName
qn FilePath -> ScopeEntry' -> ScopeEntry
forall {a}. FilePath -> a -> Named a
:~ ScopeEntry
              { _type :: Pretty (Reduced Type)
_type      = Doc -> FilePath
prender Doc
pty FilePath -> Reduced Type -> Pretty (Reduced Type)
forall {a}. FilePath -> a -> Pretty a
:> Reduced Type
rty'
              , definition :: Maybe (Pretty Definition)
definition = Bool -> Pretty Definition -> Maybe (Pretty Definition)
forall a. Bool -> a -> Maybe a
boolToMaybe (Options -> Bool
includeDefs Options
opts)
                           (Pretty Definition -> Maybe (Pretty Definition))
-> Pretty Definition -> Maybe (Pretty Definition)
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
prender Doc
pdef FilePath -> Definition -> Pretty Definition
forall {a}. FilePath -> a -> Pretty a
:> Definition
def'
              , holes :: Maybe [Sample]
holes = Maybe [Sample]
forall a. Maybe a
Nothing
              }
      in
        TCM Bool
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Options -> IsMain -> TopLevelModuleName -> TCM Bool
skip Options
opts IsMain
isMain TopLevelModuleName
md) (Recompile ([ScopeEntry], [ScopeEntry]) ()
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Recompile ([ScopeEntry], [ScopeEntry]) ()
 -> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ()))
-> Recompile ([ScopeEntry], [ScopeEntry]) ()
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
forall a b. (a -> b) -> a -> b
$ () -> Recompile ([ScopeEntry], [ScopeEntry]) ()
forall menv mod. mod -> Recompile menv mod
Skip ()) (TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
 -> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ()))
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
forall a b. (a -> b) -> a -> b
$ do
          Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"************************ "
                   TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TopLevelModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm TopLevelModuleName
md TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
" (" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> FilePath -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (IsMain -> FilePath
forall a. Show a => a -> FilePath
show IsMain
isMain)
                   TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
") ***********************************"
          -- printScope "" 1 ""
          ScopeInfo -> TCM ()
setScope (ScopeInfo -> TCM ())
-> (Interface -> ScopeInfo) -> Interface -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ScopeInfo
iInsideScope (Interface -> TCM ()) -> TCMT IO Interface -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF
          -- ** public
          NameSpace NamesInScope
_ ModulesInScope
_ InScopeSet
ns <- Scope -> NameSpace
allThingsInScope (Scope -> NameSpace) -> TCMT IO Scope -> TCMT IO NameSpace
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Scope
getCurrentScope
          [ScopeEntry]
scopeEntries <- (QName -> TCM (Maybe ScopeEntry))
-> [QName] -> TCMT IO [ScopeEntry]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM QName -> TCM (Maybe ScopeEntry)
processScopeEntry (InScopeSet -> [QName]
forall a. Set a -> [a]
S.toList InScopeSet
ns)
          -- ** private
          HashMap QName Definition
privs <- (QName -> Definition -> Bool)
-> HashMap QName Definition -> HashMap QName Definition
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HM.filterWithKey (\QName
k Definition
_ -> QName
k QName -> InScopeSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` InScopeSet
ns) (HashMap QName Definition -> HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCMT IO (HashMap QName Definition)
forall (m :: * -> *). ReadTCState m => m (HashMap QName Definition)
curDefs
          [ScopeEntry]
privScopeEntries <- (QName -> TCM (Maybe ScopeEntry))
-> [QName] -> TCMT IO [ScopeEntry]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM QName -> TCM (Maybe ScopeEntry)
processScopeEntry (HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HM.keys HashMap QName Definition
privs)
          Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
10 TCMT IO Doc
"******************************************************************"
          Recompile ([ScopeEntry], [ScopeEntry]) ()
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Recompile ([ScopeEntry], [ScopeEntry]) ()
 -> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ()))
-> Recompile ([ScopeEntry], [ScopeEntry]) ()
-> TCM (Recompile ([ScopeEntry], [ScopeEntry]) ())
forall a b. (a -> b) -> a -> b
$ ([ScopeEntry], [ScopeEntry])
-> Recompile ([ScopeEntry], [ScopeEntry]) ()
forall menv mod. menv -> Recompile menv mod
Recompile ([ScopeEntry]
scopeEntries, [ScopeEntry]
privScopeEntries)
  , compileDef :: Options
-> ([ScopeEntry], [ScopeEntry])
-> IsMain
-> Definition
-> TCM (FilePath, [Sample])
compileDef = \ Options
_ ([ScopeEntry], [ScopeEntry])
_ IsMain
_ Definition
def -> (QName -> FilePath
ppName (Definition -> QName
defName Definition
def) ,) ([Sample] -> (FilePath, [Sample]))
-> TCMT IO [Sample] -> TCM (FilePath, [Sample])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> C () -> TCMT IO [Sample]
runC (TrainF -> Definition -> C ()
forEachHole TrainF
trainF Definition
def)
  , postModule :: Options
-> ([ScopeEntry], [ScopeEntry])
-> IsMain
-> TopLevelModuleName
-> [(FilePath, [Sample])]
-> TCM ()
postModule = \ Options
opts ([ScopeEntry]
scopeEntries, [ScopeEntry]
privScopeEntries) IsMain
isMain TopLevelModuleName
md [(FilePath, [Sample])]
samples ->
    let mn :: FilePath
mn = TopLevelModuleName -> FilePath
forall a. Pretty a => a -> FilePath
pp TopLevelModuleName
md in
    TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Options -> IsMain -> TopLevelModuleName -> TCM Bool
skip Options
opts IsMain
isMain TopLevelModuleName
md) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Maybe FilePath -> (FilePath -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Options -> Maybe FilePath
outDir Options
opts) (IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> (FilePath -> IO ()) -> FilePath -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True)
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Options -> Bool
noJson Options
opts) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        let
          isGlobal :: ScopeEntry -> Bool
isGlobal = \(FilePath
n :~ ScopeEntry'
_) -> Maybe [Sample] -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe [Sample] -> Bool) -> Maybe [Sample] -> Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> [(FilePath, [Sample])] -> Maybe [Sample]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
n [(FilePath, [Sample])]
samples
          ([ScopeEntry]
globals, [ScopeEntry]
locals') = (ScopeEntry -> Bool)
-> [ScopeEntry] -> ([ScopeEntry], [ScopeEntry])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ScopeEntry -> Bool
isGlobal [ScopeEntry]
scopeEntries
          locals :: [ScopeEntry]
locals = ((ScopeEntry -> ScopeEntry) -> [ScopeEntry] -> [ScopeEntry])
-> [ScopeEntry] -> (ScopeEntry -> ScopeEntry) -> [ScopeEntry]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ScopeEntry -> ScopeEntry) -> [ScopeEntry] -> [ScopeEntry]
forall a b. (a -> b) -> [a] -> [b]
map [ScopeEntry]
locals' ((ScopeEntry -> ScopeEntry) -> [ScopeEntry])
-> (ScopeEntry -> ScopeEntry) -> [ScopeEntry]
forall a b. (a -> b) -> a -> b
$ \(FilePath
n :~ ScopeEntry'
l) ->
              FilePath
n FilePath -> ScopeEntry' -> ScopeEntry
forall {a}. FilePath -> a -> Named a
:~ ScopeEntry'
l { holes :: Maybe [Sample]
holes = [Sample] -> Maybe [Sample]
forall a. a -> Maybe a
Just ([Sample] -> Maybe [Sample]) -> [Sample] -> Maybe [Sample]
forall a b. (a -> b) -> a -> b
$ Maybe [Sample] -> [Sample]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Sample] -> [Sample]) -> Maybe [Sample] -> [Sample]
forall a b. (a -> b) -> a -> b
$ FilePath -> [(FilePath, [Sample])] -> Maybe [Sample]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
n [(FilePath, [Sample])]
samples }
          plocals :: [ScopeEntry]
plocals = ((ScopeEntry -> ScopeEntry) -> [ScopeEntry] -> [ScopeEntry])
-> [ScopeEntry] -> (ScopeEntry -> ScopeEntry) -> [ScopeEntry]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ScopeEntry -> ScopeEntry) -> [ScopeEntry] -> [ScopeEntry]
forall a b. (a -> b) -> [a] -> [b]
map [ScopeEntry]
privScopeEntries ((ScopeEntry -> ScopeEntry) -> [ScopeEntry])
-> (ScopeEntry -> ScopeEntry) -> [ScopeEntry]
forall a b. (a -> b) -> a -> b
$ \(FilePath
n :~ ScopeEntry'
l) ->
              FilePath
n FilePath -> ScopeEntry' -> ScopeEntry
forall {a}. FilePath -> a -> Named a
:~ ScopeEntry'
l { holes :: Maybe [Sample]
holes = [Sample] -> Maybe [Sample]
forall a. a -> Maybe a
Just ([Sample] -> Maybe [Sample]) -> [Sample] -> Maybe [Sample]
forall a b. (a -> b) -> a -> b
$ Maybe [Sample] -> [Sample]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Sample] -> [Sample]) -> Maybe [Sample] -> [Sample]
forall a b. (a -> b) -> a -> b
$ FilePath -> [(FilePath, [Sample])] -> Maybe [Sample]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
n [(FilePath, [Sample])]
samples }
          fileData :: Named TrainData
fileData = FilePath
mn FilePath -> TrainData -> Named TrainData
forall {a}. FilePath -> a -> Named a
:~ TrainData
            { scopeGlobal :: [ScopeEntry]
scopeGlobal  = [ScopeEntry]
globals
            , scopeLocal :: [ScopeEntry]
scopeLocal   = [ScopeEntry]
locals
            , scopePrivate :: Maybe [ScopeEntry]
scopePrivate = Bool -> [ScopeEntry] -> Maybe [ScopeEntry]
forall a. Bool -> a -> Maybe a
boolToMaybe (Options -> Bool
includePrivs Options
opts) [ScopeEntry]
plocals
            }

        FilePath -> Named TrainData -> IO ()
forall a. ToJSON a => FilePath -> a -> IO ()
encodeFile (Options -> FilePath -> FilePath
getOutFn Options
opts FilePath
mn) Named TrainData
fileData
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Options -> Bool
printJson Options
opts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          FilePath -> IO ()
putStrLn FilePath
"************************ JSON ************************"
          ByteString -> IO ()
BL.putStr (Named TrainData -> ByteString
forall a. ToJSON a => a -> ByteString
encode Named TrainData
fileData)
          FilePath -> IO ()
putStrLn FilePath
"******************************************************"
  }
  where
    skip :: Options -> IsMain -> TopLevelModuleName -> TCM Bool
    skip :: Options -> IsMain -> TopLevelModuleName -> TCM Bool
skip opts :: Options
opts@Options{Bool
Maybe FilePath
includeDefs :: Options -> Bool
outDir :: Options -> Maybe FilePath
noJson :: Options -> Bool
includePrivs :: Options -> Bool
printJson :: Options -> Bool
recurse :: Bool
noJson :: Bool
ignoreJson :: Bool
printJson :: Bool
includeDefs :: Bool
includePrivs :: Bool
outDir :: Maybe FilePath
recurse :: Options -> Bool
ignoreJson :: Options -> Bool
..} IsMain
isMain TopLevelModuleName
md = do
      Bool
jsonExists <- IO Bool -> TCM Bool
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> TCM Bool) -> IO Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist (Options -> FilePath -> FilePath
getOutFn Options
opts (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FilePath
forall a. Pretty a => a -> FilePath
pp TopLevelModuleName
md)
      Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool
not Bool
recurse Bool -> Bool -> Bool
&& (IsMain
isMain IsMain -> IsMain -> Bool
forall a. Eq a => a -> a -> Bool
== IsMain
NotMain))
            Bool -> Bool -> Bool
|| (Bool -> Bool
not Bool
noJson Bool -> Bool -> Bool
&& Bool
jsonExists Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
ignoreJson)

-- * Command-line flags

-- | Available options to configure how @agda2train@ generates training data:
--
-- ['recurse'] whether to recursively generate data from all transitive dependencies
--
-- ['noJson'] mock run without generating any actual JSON files
--
-- ['ignoreJson'] compile everything from scratch
--
-- ['includeDefs'] whether to include definitions in scope, or just their type
--
-- ['includePrivs'] whether to include private definitions as well
--
-- (run @agda2train -h/--help@ for a human-readable description of all options)
data Options = Options
  { Options -> Bool
recurse, Options -> Bool
noJson, Options -> Bool
ignoreJson, Options -> Bool
printJson, Options -> Bool
includeDefs, Options -> Bool
includePrivs :: Bool
  , Options -> Maybe FilePath
outDir  :: Maybe FilePath
  } deriving ((forall x. Options -> Rep Options x)
-> (forall x. Rep Options x -> Options) -> Generic Options
forall x. Rep Options x -> Options
forall x. Options -> Rep Options x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Options -> Rep Options x
from :: forall x. Options -> Rep Options x
$cto :: forall x. Rep Options x -> Options
to :: forall x. Rep Options x -> Options
Generic, Options -> ()
(Options -> ()) -> NFData Options
forall a. (a -> ()) -> NFData a
$crnf :: Options -> ()
rnf :: Options -> ()
NFData)

-- | The default options.
defaultOptions :: Options
defaultOptions = Options
  { recurse :: Bool
recurse      = Bool
False
  , noJson :: Bool
noJson       = Bool
False
  , ignoreJson :: Bool
ignoreJson   = Bool
False
  , printJson :: Bool
printJson    = Bool
False
  , includeDefs :: Bool
includeDefs  = Bool
True
  , includePrivs :: Bool
includePrivs = Bool
True
  , outDir :: Maybe FilePath
outDir       = Maybe FilePath
forall a. Maybe a
Nothing
  }

recOpt, noJsonOpt, ignoreJsonOpt, printJsonOpt, includeDefsOpt, includePrivsOpt
  :: Monad m => Options -> m Options
recOpt :: forall (m :: * -> *). Monad m => Options -> m Options
recOpt          Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { recurse :: Bool
recurse      = Bool
True }
noJsonOpt :: forall (m :: * -> *). Monad m => Options -> m Options
noJsonOpt       Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { noJson :: Bool
noJson       = Bool
True }
printJsonOpt :: forall (m :: * -> *). Monad m => Options -> m Options
printJsonOpt    Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { printJson :: Bool
printJson    = Bool
True }
ignoreJsonOpt :: forall (m :: * -> *). Monad m => Options -> m Options
ignoreJsonOpt   Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { ignoreJson :: Bool
ignoreJson   = Bool
True }
includeDefsOpt :: forall (m :: * -> *). Monad m => Options -> m Options
includeDefsOpt  Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { includeDefs :: Bool
includeDefs  = Bool
False }
includePrivsOpt :: forall (m :: * -> *). Monad m => Options -> m Options
includePrivsOpt Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { includePrivs :: Bool
includePrivs = Bool
False }

outDirOpt :: Monad m => FilePath -> Options -> m Options
outDirOpt :: forall (m :: * -> *). Monad m => FilePath -> Options -> m Options
outDirOpt FilePath
fp Options
opts = Options -> m Options
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> m Options) -> Options -> m Options
forall a b. (a -> b) -> a -> b
$ Options
opts { outDir :: Maybe FilePath
outDir = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
fp }

getOutDir :: Options -> FilePath
getOutDir :: Options -> FilePath
getOutDir Options
opts = case Options -> Maybe FilePath
outDir Options
opts of
  Just FilePath
fp -> FilePath
fp
  Maybe FilePath
Nothing -> FilePath
"."

getOutFn :: Options -> String -> FilePath
getOutFn :: Options -> FilePath -> FilePath
getOutFn Options
opts FilePath
mn = Options -> FilePath
getOutDir Options
opts FilePath -> FilePath -> FilePath
</> FilePath
mn FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
".json"

-- * JSON encoding

-- | Uses "Aeson.Pretty" to order the JSON fields.
encode :: ToJSON a => a -> BL.ByteString
encode :: forall a. ToJSON a => a -> ByteString
encode = Config -> a -> ByteString
forall a. ToJSON a => Config -> a -> ByteString
encodePretty' (Config -> a -> ByteString) -> Config -> a -> ByteString
forall a b. (a -> b) -> a -> b
$ Config
defConfig
  { confIndent :: Indent
confIndent = Int -> Indent
Spaces Int
2
  , confCompare :: Text -> Text -> Ordering
confCompare = [Text] -> Text -> Text -> Ordering
keyOrder
      [ Text
"pretty"
      , Text
"tag"
      , Text
"name"
      , Text
"original", Text
"simplified", Text
"reduced", Text
"normalised"
      , Text
"telescope", Text
"patterns", Text
"fields"
      , Text
"domain", Text
"codomain"
      , Text
"abstraction", Text
"body"
      , Text
"sort", Text
"level", Text
"literal"
      , Text
"head", Text
"arguments"
      , Text
"variants", Text
"reference", Text
"variant"
      , Text
"index"
      , Text
"scopeGlobal", Text
"scopeLocal"
      , Text
"type", Text
"definition", Text
"holes"
      , Text
"ctx", Text
"goal", Text
"term", Text
"premises"
      ]
  }

encodeFile :: ToJSON a => FilePath -> a -> IO ()
encodeFile :: forall a. ToJSON a => FilePath -> a -> IO ()
encodeFile = \FilePath
fn -> FilePath -> ByteString -> IO ()
BL.writeFile FilePath
fn (ByteString -> IO ()) -> (a -> ByteString) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ByteString
forall a. ToJSON a => a -> ByteString
encode