{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall #-}

module Certifier
  ( runCertifier
  , mkCertifier
  , prettyCertifierError
  , CertName
  , CertifierError (..)
  , CertifierOutput (..)
  ) where

import Control.Monad
import Control.Monad.Except (ExceptT (..), runExceptT, throwError)
import Control.Monad.IO.Class (liftIO)
import Data.FileEmbed (embedStringFile)
import Data.Foldable
import Data.List.Extra (replace)
import Data.List.NonEmpty (NonEmpty (..))
import Data.List.NonEmpty qualified as NE
import Data.List.NonEmptySep as NES
import Data.Text qualified as Text
import Data.Text.IO qualified as T
import System.Directory (createDirectoryIfMissing)
import System.FilePath (takeBaseName, (</>))
import Text.Printf (printf)

import FFI.AgdaUnparse (AgdaUnparse (..), renderAgdaUnparse)
import FFI.CostInfo
import FFI.OptimizerTrace
import FFI.Untyped (UTerm)
import MAlonzo.Code.Certifier (runCertifierMain)
import PlutusLedgerApi.Common
import Prettyprinter (pretty)
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Transform.Certify.Hints (Hints)
import UntypedPlutusCore.Transform.Optimizer

type CertName = String
type CertDir = FilePath

data CertifierError
  = -- | Certificate dir + certifier report
    InvalidCertificate CertDir String
  | InvalidCompilerOutput
  | ValidationError CertName

data CertifierOutput
  = -- | Print minimal basic info, such as "passed" or "failed"
    BasicOutput
  | -- | Produce a detailed human readable report
    ReportOutput FilePath
  | -- | Produce an Agda project that can be type checked
    ProjectOutput CertDir

prettyCertifierError :: CertifierError -> String
prettyCertifierError :: CertifierError -> String
prettyCertifierError (InvalidCertificate String
certDir String
report) =
  String
"\n\nInvalid certificate: "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
certDir
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\nThe compilation was not successfully certified. \
       \Please open a bug report at https://www.github.com/IntersectMBO/plutus \
       \and attach the faulty certificate.\n\
       \Certifier report:\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
report
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"
prettyCertifierError CertifierError
InvalidCompilerOutput =
  String
"\n\nInvalid compiler output: \
  \\nThe certifier was not able to process the trace produced by the compiler. \
  \Please open a bug report at https://www.github.com/IntersectMBO/plutus \
  \containing a minimal program that when compiled reproduces the issue.\n"
prettyCertifierError (ValidationError String
name) =
  String
"\n\nInvalid certificate name: \
  \\nThe certificate name "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
name
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" is invalid. \
       \Please use only alphanumeric characters, underscores and dashes. \
       \The first character must be a letter.\n"

type Certifier = ExceptT CertifierError IO

runCertifier :: Certifier a -> IO (Either CertifierError a)
runCertifier :: forall a. Certifier a -> IO (Either CertifierError a)
runCertifier = ExceptT CertifierError IO a -> IO (Either CertifierError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT

-- | Run the Agda certifier on the simplification trace, if requested
mkCertifier
  :: OptimizerTrace UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a
  -- ^ The trace produced by the simplification process
  -> CertName
  -- ^ The name of the certificate to be produced
  -> CertifierOutput
  -> [ ( Maybe
           (CekEvaluationException UPLC.NamedDeBruijn UPLC.DefaultUni UPLC.DefaultFun)
       , ExBudget
       )
     ]
  -> Certifier Bool
mkCertifier :: forall a.
OptimizerTrace Name DefaultUni DefaultFun a
-> String
-> CertifierOutput
-> [(Maybe
       (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
     ExBudget)]
-> Certifier Bool
mkCertifier OptimizerTrace Name DefaultUni DefaultFun a
simplTrace String
certName CertifierOutput
certOutput [(Maybe
    (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
  ExBudget)]
costs = do
  let rawAgdaTrace :: Trace UTerm
rawAgdaTrace = OptimizerTrace Name DefaultUni DefaultFun a -> Trace UTerm
forall a.
OptimizerTrace Name DefaultUni DefaultFun a -> Trace UTerm
mkFfiOptimizerTrace OptimizerTrace Name DefaultUni DefaultFun a
simplTrace
      costs' :: [EvalResult]
      costs' :: [EvalResult]
costs' = (Maybe (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
 -> ExBudget -> EvalResult)
-> (Maybe
      (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
    ExBudget)
-> EvalResult
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
-> ExBudget -> EvalResult
toEvalResult ((Maybe
    (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
  ExBudget)
 -> EvalResult)
-> [(Maybe
       (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
     ExBudget)]
-> [EvalResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe
    (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
  ExBudget)]
-> [(Maybe
       (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
     ExBudget)]
forall a. [a] -> [a]
reverse [(Maybe
    (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
  ExBudget)]
costs
  case Trace UTerm
-> [EvalResult] -> T_Maybe_10 () (T__'215'__436 Bool T_String_6)
runCertifierMain Trace UTerm
rawAgdaTrace [EvalResult]
costs' of
    Just (Bool
passed, T_String_6
report) -> do
      case CertifierOutput
certOutput of
        CertifierOutput
BasicOutput -> () -> ExceptT CertifierError IO ()
forall a. a -> ExceptT CertifierError IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        ReportOutput String
file -> IO () -> ExceptT CertifierError IO ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ExceptT CertifierError IO ())
-> IO () -> ExceptT CertifierError IO ()
forall a b. (a -> b) -> a -> b
$ String -> T_String_6 -> IO ()
T.writeFile String
file T_String_6
report
        ProjectOutput String
certDir -> do
          let cert :: AgdaCertificateProject
cert = Certificate -> AgdaCertificateProject
mkAgdaCertificateProject (Certificate -> AgdaCertificateProject)
-> Certificate -> AgdaCertificateProject
forall a b. (a -> b) -> a -> b
$ String -> Trace UTerm -> Certificate
mkCertificate String
certName Trace UTerm
rawAgdaTrace
          String -> AgdaCertificateProject -> ExceptT CertifierError IO ()
writeCertificateProject String
certDir AgdaCertificateProject
cert
          Bool
-> ExceptT CertifierError IO () -> ExceptT CertifierError IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
passed (ExceptT CertifierError IO () -> ExceptT CertifierError IO ())
-> (CertifierError -> ExceptT CertifierError IO ())
-> CertifierError
-> ExceptT CertifierError IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertifierError -> ExceptT CertifierError IO ()
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CertifierError -> ExceptT CertifierError IO ())
-> CertifierError -> ExceptT CertifierError IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> CertifierError
InvalidCertificate String
certDir (T_String_6 -> String
Text.unpack T_String_6
report)
      Bool -> Certifier Bool
forall a. a -> ExceptT CertifierError IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
passed
    T_Maybe_10 () (T__'215'__436 Bool T_String_6)
Nothing -> CertifierError -> Certifier Bool
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError CertifierError
InvalidCompilerOutput

data Certificate = Certificate
  { Certificate -> String
certName :: String
  , Certificate -> Trace UTerm
certTrace :: Trace UTerm
  }

mkCertificate :: String -> Trace UTerm -> Certificate
mkCertificate :: String -> Trace UTerm -> Certificate
mkCertificate String
certName Trace UTerm
rawTrace =
  let trace' :: Trace UTerm
trace' = Trace UTerm -> Trace UTerm
dedup Trace UTerm
rawTrace
   in Certificate
        { String
certName :: String
certName :: String
certName
        , certTrace :: Trace UTerm
certTrace = Trace UTerm
trace'
        }
  where
    dedup :: Trace UTerm -> Trace UTerm
    dedup :: Trace UTerm -> Trace UTerm
dedup (Singleton UTerm
x) = UTerm -> Trace UTerm
forall sep a. a -> NonEmptySep sep a
Singleton UTerm
x
    dedup (Cons UTerm
x (OptStage, Hints)
sep Trace UTerm
xs)
      -- If subsequent ASTs are equal, drop the pass
      | UTerm
x UTerm -> UTerm -> Bool
forall a. Eq a => a -> a -> Bool
== Trace UTerm -> UTerm
forall sep a. NonEmptySep sep a -> a
NES.head Trace UTerm
xs = Trace UTerm -> Trace UTerm
dedup Trace UTerm
xs
      | Bool
otherwise = UTerm -> (OptStage, Hints) -> Trace UTerm -> Trace UTerm
forall sep a. a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
Cons UTerm
x (OptStage, Hints)
sep (Trace UTerm -> Trace UTerm
dedup Trace UTerm
xs)

{-| Module name with string components, e.g.
  "Data" :| ["List", "NonEmpty"] -}
type ModuleName = NonEmpty String

moduleIdent :: ModuleName -> String
moduleIdent :: ModuleName -> String
moduleIdent = ModuleName -> String
forall m. Monoid m => NonEmpty m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (ModuleName -> String)
-> (ModuleName -> ModuleName) -> ModuleName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ModuleName -> ModuleName
forall a. a -> NonEmpty a -> NonEmpty a
NE.intersperse String
"."

moduleFileName :: ModuleName -> FilePath
moduleFileName :: ModuleName -> String
moduleFileName ModuleName
m = (String -> String -> String) -> String -> ModuleName -> String
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> String -> String
(</>) String
"" ModuleName
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".agda"

-- | Drops the last component of the module to obtain its directory
moduleDir :: ModuleName -> String
moduleDir :: ModuleName -> String
moduleDir ModuleName
m = (String -> String -> String) -> String -> [String] -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> String -> String
(</>) String
"" (ModuleName -> [String]
forall a. NonEmpty a -> [a]
NE.init ModuleName
m)

{-| Module name in agda, for a given equivalence class. Each list element is a module segment that is to be
separated by "." (agda identifier) or by "/" (files) -}
mkAstModuleName :: Int -> ModuleName
mkAstModuleName :: Int -> ModuleName
mkAstModuleName Int
n =
  (String
"Pass" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%03d" Int
n) String -> [String] -> ModuleName
forall a. a -> [a] -> NonEmpty a
:| [String
"AST"]

mkAgdaAstFile :: Int -> UTerm -> Maybe Hints -> (ModuleName, String)
mkAgdaAstFile :: Int -> UTerm -> Maybe Hints -> (ModuleName, String)
mkAgdaAstFile Int
n UTerm
pre Maybe Hints
mHints =
  ( ModuleName
modName
  , [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
      [ String
"module " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ModuleName -> String
moduleIdent ModuleName
modName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" where"
      , String
""
      , String
"open import Data.Unit"
      , String
"open import Data.Nat"
      , String
"open import Data.Integer"
      , String
"open import Data.Maybe"
      , String
"open import Data.Bool.Base using (Bool; false; true)"
      , String
"open import Data.List using (List; _∷_; [])"
      , String
""
      , String
"open import RawU"
      , String
"open import Builtin"
      , String
"open import Utils"
      , String
""
      , String
"open import Untyped using (_⊢)"
      , String
"open import VerifiedCompilation using (checkScope)"
      , String
"open import VerifiedCompilation.Trace"
      , String
""
      , String
"raw : Untyped"
      , String
"raw = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> UTerm -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse UTerm
pre
      , String
""
      , String
"ast : 0 ⊢"
      , String
"ast = to-witness-T (checkScope raw) tt"
      ]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ case Maybe Hints
mHints of
          Just Hints
hints ->
            [ String
""
            , String
"hints : Hints"
            , String
"hints = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Hints -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse Hints
hints
            ]
          Maybe Hints
Nothing -> []
  )
  where
    modName :: ModuleName
modName = Int -> ModuleName
mkAstModuleName Int
n

mkAgdaImport :: Bool -> ModuleName -> String
mkAgdaImport :: Bool -> ModuleName -> String
mkAgdaImport Bool
open ModuleName
moduleName =
  Bool -> String -> String
forall {a}. (Semigroup a, IsString a) => Bool -> a -> a
openModifier Bool
open (String
"import " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ModuleName -> String
moduleIdent ModuleName
moduleName)
  where
    openModifier :: Bool -> a -> a
openModifier Bool
True a
str = a
"open " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
str
    openModifier Bool
False a
str = a
str

newtype AgdaVar = AgdaVar String

instance AgdaUnparse AgdaVar where
  agdaUnparse :: forall ann. AgdaVar -> Doc ann
agdaUnparse (AgdaVar String
var) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
var

mkCertificateFile :: Certificate -> String
mkCertificateFile :: Certificate -> String
mkCertificateFile Certificate {String
certName :: Certificate -> String
certName :: String
certName, Trace UTerm
certTrace :: Certificate -> Trace UTerm
certTrace :: Trace UTerm
certTrace} =
  [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [ String
"module " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
certName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" where"
    , String
""
    , String
"open import VerifiedCompilation.Trace"
    , String
"open import Untyped using (_⊢)"
    , String
"open import Utils hiding (List; _>>=_)"
    , String
"open import VerifiedCompilation"
    , String
"open import Data.Unit"
    , String
""
    ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (ModuleName -> String) -> [ModuleName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> ModuleName -> String
mkAgdaImport Bool
False) [ModuleName]
astImports
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
         , String
"trace : Trace (0 ⊢)"
         , String
"trace ="
         ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (NonEmptySep (OptStage, AgdaVar) AgdaVar -> [String]
printTrace NonEmptySep (OptStage, AgdaVar) AgdaVar
traceExpr)
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
         , String
"certificate : Certificate trace"
         , String
"certificate = cert trace (certify trace) tt"
         , String
""
         ]
  where
    astImports :: [ModuleName]
    astImports :: [ModuleName]
astImports = (Int -> ModuleName) -> [Int] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map Int -> ModuleName
mkAstModuleName [Int
0 .. Trace UTerm -> Int
forall a. NonEmptySep (OptStage, Hints) a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Trace UTerm
certTrace Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

    -- replace hints and asts by agda variables that point to the right module
    traceExpr :: NonEmptySep (OptStage, AgdaVar) AgdaVar
    traceExpr :: NonEmptySep (OptStage, AgdaVar) AgdaVar
traceExpr = Int -> Trace UTerm -> NonEmptySep (OptStage, AgdaVar) AgdaVar
forall {a} {b} {a}.
Int -> NonEmptySep (a, b) a -> NonEmptySep (a, AgdaVar) AgdaVar
go Int
0 Trace UTerm
certTrace
      where
        go :: Int -> NonEmptySep (a, b) a -> NonEmptySep (a, AgdaVar) AgdaVar
go Int
n (Singleton a
_) = AgdaVar -> NonEmptySep (a, AgdaVar) AgdaVar
forall sep a. a -> NonEmptySep sep a
Singleton (Int -> String -> AgdaVar
moduleVar Int
n String
"ast")
        go Int
n (Cons a
_ (a
stage, b
_) NonEmptySep (a, b) a
xs) =
          AgdaVar
-> (a, AgdaVar)
-> NonEmptySep (a, AgdaVar) AgdaVar
-> NonEmptySep (a, AgdaVar) AgdaVar
forall sep a. a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
Cons
            (Int -> String -> AgdaVar
moduleVar Int
n String
"ast")
            (a
stage, Int -> String -> AgdaVar
moduleVar Int
n String
"hints")
            (Int -> NonEmptySep (a, b) a -> NonEmptySep (a, AgdaVar) AgdaVar
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NonEmptySep (a, b) a
xs)

    moduleVar :: Int -> String -> AgdaVar
    moduleVar :: Int -> String -> AgdaVar
moduleVar Int
n String
x =
      String -> AgdaVar
AgdaVar (String -> AgdaVar) -> String -> AgdaVar
forall a b. (a -> b) -> a -> b
$
        ModuleName -> String
moduleIdent (Int -> ModuleName
mkAstModuleName Int
n)
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"."
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
x

-- Ad-hoc pretty printing so it can be printed over multiple lines
printTrace :: NonEmptySep (OptStage, AgdaVar) AgdaVar -> [String]
printTrace :: NonEmptySep (OptStage, AgdaVar) AgdaVar -> [String]
printTrace (Singleton AgdaVar
x) = [String
"singleton" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AgdaVar -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse AgdaVar
x]
printTrace (Cons AgdaVar
x (OptStage
stage, AgdaVar
y) NonEmptySep (OptStage, AgdaVar) AgdaVar
xs) =
  [ AgdaVar -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse AgdaVar
x
  , String
"  ∷[ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OptStage -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse OptStage
stage String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" , " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AgdaVar -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse AgdaVar
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"
  ]
    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NonEmptySep (OptStage, AgdaVar) AgdaVar -> [String]
printTrace NonEmptySep (OptStage, AgdaVar) AgdaVar
xs

data AgdaCertificateProject = AgdaCertificateProject
  { AgdaCertificateProject -> (String, String)
mainModule :: (FilePath, String)
  , AgdaCertificateProject -> [(ModuleName, String)]
astModules :: [(ModuleName, String)]
  , AgdaCertificateProject -> (String, String)
agdalib :: (FilePath, String)
  }

mkAgdaLib :: String -> (FilePath, String)
mkAgdaLib :: String -> (String, String)
mkAgdaLib String
name =
  let contents :: String
contents =
        String
"name: "
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
name
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\ndepend:\
             \\n  standard-library-2.3\
             \\n  plutus-metatheory\
             \\ninclude: src\
             \\nflags: --polarity"
   in (String
name String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".agda-lib", String
contents)

mkAgdaCertificateProject
  :: Certificate
  -> AgdaCertificateProject
mkAgdaCertificateProject :: Certificate -> AgdaCertificateProject
mkAgdaCertificateProject Certificate
cert =
  let name :: String
name = Certificate -> String
certName Certificate
cert
      mainModule :: String
mainModule = Certificate -> String
mkCertificateFile Certificate
cert
      astModules :: [(ModuleName, String)]
astModules = Int -> Trace UTerm -> [(ModuleName, String)]
astModuleFiles Int
0 (Certificate -> Trace UTerm
certTrace Certificate
cert)
      agdalib :: (String, String)
agdalib = String -> (String, String)
mkAgdaLib String
name
   in AgdaCertificateProject
        { mainModule :: (String, String)
mainModule = (Certificate -> String
certName Certificate
cert String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".agda", String
mainModule)
        , [(ModuleName, String)]
astModules :: [(ModuleName, String)]
astModules :: [(ModuleName, String)]
astModules
        , (String, String)
agdalib :: (String, String)
agdalib :: (String, String)
agdalib
        }
  where
    astModuleFiles :: Int -> Trace UTerm -> [(ModuleName, String)]
    astModuleFiles :: Int -> Trace UTerm -> [(ModuleName, String)]
astModuleFiles Int
n (Singleton UTerm
x) = [Int -> UTerm -> Maybe Hints -> (ModuleName, String)
mkAgdaAstFile Int
n UTerm
x Maybe Hints
forall a. Maybe a
Nothing]
    astModuleFiles Int
n (Cons UTerm
x (OptStage
_, Hints
h) Trace UTerm
xs) = Int -> UTerm -> Maybe Hints -> (ModuleName, String)
mkAgdaAstFile Int
n UTerm
x (Hints -> Maybe Hints
forall a. a -> Maybe a
Just Hints
h) (ModuleName, String)
-> [(ModuleName, String)] -> [(ModuleName, String)]
forall a. a -> [a] -> [a]
: Int -> Trace UTerm -> [(ModuleName, String)]
astModuleFiles (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Trace UTerm
xs

writeCertificateProject
  :: CertDir
  -> AgdaCertificateProject
  -> Certifier ()
writeCertificateProject :: String -> AgdaCertificateProject -> ExceptT CertifierError IO ()
writeCertificateProject
  String
certDir
  AgdaCertificateProject
    { (String, String)
mainModule :: AgdaCertificateProject -> (String, String)
mainModule :: (String, String)
mainModule
    , [(ModuleName, String)]
astModules :: AgdaCertificateProject -> [(ModuleName, String)]
astModules :: [(ModuleName, String)]
astModules
    , (String, String)
agdalib :: AgdaCertificateProject -> (String, String)
agdalib :: (String, String)
agdalib
    } =
    IO () -> ExceptT CertifierError IO ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ExceptT CertifierError IO ())
-> IO () -> ExceptT CertifierError IO ()
forall a b. (a -> b) -> a -> b
$ do
      let (String
mainModulePath, String
mainModuleContents) = (String, String)
mainModule
          (String
agdalibPath, String
agdalibContents) = (String, String)
agdalib
          certName :: String
certName = String -> String
takeBaseName String
mainModulePath
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
certDir
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
certDir String -> String -> String
</> String
"src")
      [(ModuleName, String)] -> ((ModuleName, String) -> IO ()) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(ModuleName, String)]
astModules (((ModuleName, String) -> IO ()) -> IO ())
-> ((ModuleName, String) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(ModuleName
modName, String
_) -> do
        Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> ModuleName -> String
moduleDir ModuleName
modName)
      String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> String
mainModulePath) String
mainModuleContents
      String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
agdalibPath) String
agdalibContents
      let readmeTemplate :: String
readmeTemplate = $(embedStringFile "file-embed/certificate-README.md")
      String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"README.md") (String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace String
"{{NAME}}" String
certName String
readmeTemplate)
      ((ModuleName, String) -> IO ()) -> [(ModuleName, String)] -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
        ( \(ModuleName
modName, String
contents) ->
            String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> ModuleName -> String
moduleFileName ModuleName
modName) String
contents
        )
        [(ModuleName, String)]
astModules