{-# 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.Maybe (fromMaybe)
import Data.Text qualified as Text
import Data.Text.IO qualified as T
import System.Directory (createDirectoryIfMissing)
import System.FilePath (takeBaseName, (</>))

import FFI.AgdaUnparse (AgdaUnparse (..), renderAgdaUnparse)
import FFI.CostInfo
import FFI.OptimizerTrace (Trace, mkFfiOptimizerTrace, toEvalResult)
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.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 -> [Char]
prettyCertifierError (InvalidCertificate [Char]
certDir [Char]
report) =
  [Char]
"\n\nInvalid certificate: "
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
certDir
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\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"
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
report
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
prettyCertifierError CertifierError
InvalidCompilerOutput =
  [Char]
"\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 [Char]
name) =
  [Char]
"\n\nInvalid certificate name: \
  \\nThe certificate name "
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
name
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" 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
-> [Char]
-> CertifierOutput
-> [(Maybe
       (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun),
     ExBudget)]
-> Certifier Bool
mkCertifier OptimizerTrace Name DefaultUni DefaultFun a
simplTrace [Char]
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 [Char]
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
$ [Char] -> T_String_6 -> IO ()
T.writeFile [Char]
file T_String_6
report
        ProjectOutput [Char]
certDir -> do
          let cert :: AgdaCertificateProject
cert = Certificate -> AgdaCertificateProject
mkAgdaCertificateProject (Certificate -> AgdaCertificateProject)
-> Certificate -> AgdaCertificateProject
forall a b. (a -> b) -> a -> b
$ [Char] -> Trace UTerm -> Certificate
mkCertificate [Char]
certName Trace UTerm
rawAgdaTrace
          [Char] -> AgdaCertificateProject -> ExceptT CertifierError IO ()
writeCertificateProject [Char]
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
$ [Char] -> [Char] -> CertifierError
InvalidCertificate [Char]
certDir (T_String_6 -> [Char]
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

type EquivClass = Int

data TermWithId = TermWithId
  { TermWithId -> EquivClass
termId :: Int
  , TermWithId -> UTerm
term :: UTerm
  }

data Ast = Ast
  { Ast -> EquivClass
equivClass :: EquivClass
  , Ast -> TermWithId
astTermWithId :: TermWithId
  }

getTermId :: Ast -> Int
getTermId :: Ast -> EquivClass
getTermId Ast {astTermWithId :: Ast -> TermWithId
astTermWithId = TermWithId {EquivClass
termId :: TermWithId -> EquivClass
termId :: EquivClass
termId}} = EquivClass
termId

data Certificate = Certificate
  { Certificate -> [Char]
certName :: String
  , Certificate -> Trace Ast
certTrace :: Trace Ast
  , Certificate -> [Ast]
certReprAsts :: [Ast]
  }

mkCertificate :: String -> Trace UTerm -> Certificate
mkCertificate :: [Char] -> Trace UTerm -> Certificate
mkCertificate [Char]
certName Trace UTerm
rawTrace =
  let traceWithIds :: Trace TermWithId
traceWithIds = Trace UTerm -> Trace TermWithId
addIds Trace UTerm
rawTrace
      allTermWithIds :: [TermWithId]
allTermWithIds = Trace TermWithId -> [TermWithId]
extractTermWithIds Trace TermWithId
traceWithIds
      groupedAsts :: [NonEmpty Ast]
groupedAsts = [TermWithId] -> [NonEmpty Ast]
findEquivClasses [TermWithId]
allTermWithIds
      allAsts :: [Ast]
allAsts = [NonEmpty Ast]
groupedAsts [NonEmpty Ast] -> (NonEmpty Ast -> [Ast]) -> [Ast]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= NonEmpty Ast -> [Ast]
forall a. NonEmpty a -> [a]
NE.toList
      certTrace :: Trace Ast
certTrace = [Ast] -> Trace TermWithId -> Trace Ast
mkAstTrace [Ast]
allAsts Trace TermWithId
traceWithIds
      certReprAsts :: [Ast]
certReprAsts = [NonEmpty Ast] -> [Ast]
getRepresentatives [NonEmpty Ast]
groupedAsts
   in Certificate
        { [Char]
certName :: [Char]
certName :: [Char]
certName
        , Trace Ast
certTrace :: Trace Ast
certTrace :: Trace Ast
certTrace
        , [Ast]
certReprAsts :: [Ast]
certReprAsts :: [Ast]
certReprAsts
        }
  where
    addIds
      :: Trace UTerm
      -> Trace TermWithId
    addIds :: Trace UTerm -> Trace TermWithId
addIds = EquivClass -> Trace UTerm -> Trace TermWithId
go EquivClass
0
      where
        go
          :: Int
          -> Trace UTerm
          -> Trace TermWithId
        go :: EquivClass -> Trace UTerm -> Trace TermWithId
go EquivClass
_ [] = []
        go EquivClass
id' ((OptStage
stage, (Hints
hints, (UTerm
before, UTerm
after))) : Trace UTerm
rest) =
          let beforeWithId :: TermWithId
beforeWithId = EquivClass -> UTerm -> TermWithId
TermWithId EquivClass
id' UTerm
before
              afterWithId :: TermWithId
afterWithId = EquivClass -> UTerm -> TermWithId
TermWithId (EquivClass
id' EquivClass -> EquivClass -> EquivClass
forall a. Num a => a -> a -> a
+ EquivClass
1) UTerm
after
           in (OptStage
stage, (Hints
hints, (TermWithId
beforeWithId, TermWithId
afterWithId))) TraceElem TermWithId -> Trace TermWithId -> Trace TermWithId
forall a. a -> [a] -> [a]
: EquivClass -> Trace UTerm -> Trace TermWithId
go (EquivClass
id' EquivClass -> EquivClass -> EquivClass
forall a. Num a => a -> a -> a
+ EquivClass
2) Trace UTerm
rest

    extractTermWithIds
      :: Trace TermWithId
      -> [TermWithId]
    extractTermWithIds :: Trace TermWithId -> [TermWithId]
extractTermWithIds = (TraceElem TermWithId -> [TermWithId])
-> Trace TermWithId -> [TermWithId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(OptStage
_, (Hints
_, (TermWithId
before, TermWithId
after))) -> [TermWithId
before, TermWithId
after])

    findEquivClasses :: [TermWithId] -> [NonEmpty Ast]
    findEquivClasses :: [TermWithId] -> [NonEmpty Ast]
findEquivClasses =
      EquivClass -> [NonEmpty TermWithId] -> [NonEmpty Ast]
go EquivClass
0 ([NonEmpty TermWithId] -> [NonEmpty Ast])
-> ([TermWithId] -> [NonEmpty TermWithId])
-> [TermWithId]
-> [NonEmpty Ast]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermWithId -> TermWithId -> Bool)
-> [TermWithId] -> [NonEmpty TermWithId]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
NE.groupBy (\TermWithId
x TermWithId
y -> TermWithId -> UTerm
term TermWithId
x UTerm -> UTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TermWithId -> UTerm
term TermWithId
y)
      where
        go :: EquivClass -> [NonEmpty TermWithId] -> [NonEmpty Ast]
        go :: EquivClass -> [NonEmpty TermWithId] -> [NonEmpty Ast]
go EquivClass
_ [] = []
        go EquivClass
cl (NonEmpty TermWithId
ts : [NonEmpty TermWithId]
rest) =
          let asts :: NonEmpty Ast
asts = (TermWithId -> Ast) -> NonEmpty TermWithId -> NonEmpty Ast
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\TermWithId
t -> Ast {astTermWithId :: TermWithId
astTermWithId = TermWithId
t, equivClass :: EquivClass
equivClass = EquivClass
cl}) NonEmpty TermWithId
ts
           in NonEmpty Ast
asts NonEmpty Ast -> [NonEmpty Ast] -> [NonEmpty Ast]
forall a. a -> [a] -> [a]
: EquivClass -> [NonEmpty TermWithId] -> [NonEmpty Ast]
go (EquivClass
cl EquivClass -> EquivClass -> EquivClass
forall a. Num a => a -> a -> a
+ EquivClass
1) [NonEmpty TermWithId]
rest

    getRepresentatives :: [NonEmpty Ast] -> [Ast]
    getRepresentatives :: [NonEmpty Ast] -> [Ast]
getRepresentatives = (NonEmpty Ast -> Ast) -> [NonEmpty Ast] -> [Ast]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty Ast -> Ast
forall a. NonEmpty a -> a
NE.head

    errorMessage :: String
    errorMessage :: [Char]
errorMessage =
      [Char]
"Internal error: could not find AST.\
      \ This is an issue in the certifier, please open a bug report at\
      \ https://github.com/IntersectMBO/plutus/issues"

    mkAstTrace
      :: [Ast]
      -> Trace TermWithId
      -> Trace Ast
    mkAstTrace :: [Ast] -> Trace TermWithId -> Trace Ast
mkAstTrace [Ast]
_ [] = []
    mkAstTrace [Ast]
allAsts ((OptStage
stage, (Hints
hints, (TermWithId
rawBefore, TermWithId
rawAfter))) : Trace TermWithId
rest) =
      let processedBefore :: Ast
processedBefore =
            Ast -> Maybe Ast -> Ast
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Ast
forall a. HasCallStack => [Char] -> a
error [Char]
errorMessage) (Maybe Ast -> Ast) -> Maybe Ast -> Ast
forall a b. (a -> b) -> a -> b
$
              (Ast -> Bool) -> [Ast] -> Maybe Ast
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Ast
ast -> Ast -> EquivClass
getTermId Ast
ast EquivClass -> EquivClass -> Bool
forall a. Eq a => a -> a -> Bool
== TermWithId -> EquivClass
termId TermWithId
rawBefore) [Ast]
allAsts
          processedAfter :: Ast
processedAfter =
            Ast -> Maybe Ast -> Ast
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Ast
forall a. HasCallStack => [Char] -> a
error [Char]
errorMessage) (Maybe Ast -> Ast) -> Maybe Ast -> Ast
forall a b. (a -> b) -> a -> b
$
              (Ast -> Bool) -> [Ast] -> Maybe Ast
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Ast
ast -> Ast -> EquivClass
getTermId Ast
ast EquivClass -> EquivClass -> Bool
forall a. Eq a => a -> a -> Bool
== TermWithId -> EquivClass
termId TermWithId
rawAfter) [Ast]
allAsts
       in (OptStage
stage, (Hints
hints, (Ast
processedBefore, Ast
processedAfter))) TraceElem Ast -> Trace Ast -> Trace Ast
forall a. a -> [a] -> [a]
: [Ast] -> Trace TermWithId -> Trace Ast
mkAstTrace [Ast]
allAsts Trace TermWithId
rest

mkAstModuleName :: Ast -> String
mkAstModuleName :: Ast -> [Char]
mkAstModuleName Ast {EquivClass
equivClass :: Ast -> EquivClass
equivClass :: EquivClass
equivClass} =
  [Char]
"Ast" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> EquivClass -> [Char]
forall a. Show a => a -> [Char]
show EquivClass
equivClass

mkAgdaAstFile :: Ast -> (FilePath, String)
mkAgdaAstFile :: Ast -> ([Char], [Char])
mkAgdaAstFile Ast
ast =
  let agdaAst :: [Char]
agdaAst = UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
renderAgdaUnparse (TermWithId -> UTerm
term (TermWithId -> UTerm) -> (Ast -> TermWithId) -> Ast -> UTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ast -> TermWithId
astTermWithId (Ast -> UTerm) -> Ast -> UTerm
forall a b. (a -> b) -> a -> b
$ Ast
ast)
      agdaId :: EquivClass
agdaId = Ast -> EquivClass
equivClass Ast
ast
      agdaModuleName :: [Char]
agdaModuleName = Ast -> [Char]
mkAstModuleName Ast
ast
      agdaIdStr :: [Char]
agdaIdStr = [Char]
"ast" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> EquivClass -> [Char]
forall a. Show a => a -> [Char]
show EquivClass
agdaId
      agdaAstTy :: [Char]
agdaAstTy = [Char]
agdaIdStr [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" : Untyped"
      agdaAstDef :: [Char]
agdaAstDef = [Char]
agdaIdStr [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" = " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
agdaAst
      agdaAstFile :: [Char]
agdaAstFile = [Char]
agdaModuleName [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
".agda"
   in ([Char]
agdaAstFile, [Char] -> [Char] -> [Char] -> [Char]
mkAstModule [Char]
agdaModuleName [Char]
agdaAstTy [Char]
agdaAstDef)

mkAstModule :: String -> String -> String -> String
mkAstModule :: [Char] -> [Char] -> [Char] -> [Char]
mkAstModule [Char]
agdaIdStr [Char]
agdaAstTy [Char]
agdaAstDef =
  [Char]
"module "
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
agdaIdStr
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" where\
       \\n\
       \\nopen import VerifiedCompilation\
       \\nopen import VerifiedCompilation.Certificate\
       \\nopen import VerifiedCompilation.Trace\
       \\nopen import RawU\
       \\nopen import Builtin\
       \\nopen import Data.Unit\
       \\nopen import Data.Nat\
       \\nopen import Data.Integer\
       \\nopen import Utils\
       \\nimport Agda.Builtin.Bool\
       \\nimport Relation.Nullary\
       \\nimport VerifiedCompilation.UntypedTranslation\
       \\nopen import Agda.Builtin.Maybe\
       \\nopen import Data.Empty using (⊥)\
       \\nopen import Data.Bool.Base using (Bool; false; true)\
       \\nopen import Agda.Builtin.Equality using (_≡_; refl)\
       \\n\
       \\n"
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
agdaAstTy
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n\
       \\n"
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
agdaAstDef
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"

mkAgdaOpenImport :: String -> String
mkAgdaOpenImport :: [Char] -> [Char]
mkAgdaOpenImport [Char]
agdaModuleName =
  [Char]
"open import " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
agdaModuleName

newtype AgdaVar = AgdaVar String

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

mkCertificateFile :: Certificate -> (FilePath, String)
mkCertificateFile :: Certificate -> ([Char], [Char])
mkCertificateFile Certificate {[Char]
certName :: Certificate -> [Char]
certName :: [Char]
certName, Trace Ast
certTrace :: Certificate -> Trace Ast
certTrace :: Trace Ast
certTrace, [Ast]
certReprAsts :: Certificate -> [Ast]
certReprAsts :: [Ast]
certReprAsts} =
  let imports :: [[Char]]
imports = (Ast -> [Char]) -> [Ast] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> [Char]
mkAgdaOpenImport ([Char] -> [Char]) -> (Ast -> [Char]) -> Ast -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ast -> [Char]
mkAstModuleName) [Ast]
certReprAsts
      agdaTrace :: [Char]
agdaTrace =
        [(OptStage, (Hints, (AgdaVar, AgdaVar)))] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
renderAgdaUnparse ([(OptStage, (Hints, (AgdaVar, AgdaVar)))] -> [Char])
-> [(OptStage, (Hints, (AgdaVar, AgdaVar)))] -> [Char]
forall a b. (a -> b) -> a -> b
$
          ( \(OptStage
st, (Hints
hints, (Ast
ast1, Ast
ast2))) ->
              ( OptStage
st
              ,
                ( Hints
hints
                ,
                  ( [Char] -> AgdaVar
AgdaVar ([Char] -> AgdaVar) -> [Char] -> AgdaVar
forall a b. (a -> b) -> a -> b
$ [Char]
"ast" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> (EquivClass -> [Char]
forall a. Show a => a -> [Char]
show (EquivClass -> [Char]) -> (Ast -> EquivClass) -> Ast -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ast -> EquivClass
equivClass) Ast
ast1
                  , [Char] -> AgdaVar
AgdaVar ([Char] -> AgdaVar) -> [Char] -> AgdaVar
forall a b. (a -> b) -> a -> b
$ [Char]
"ast" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> (EquivClass -> [Char]
forall a. Show a => a -> [Char]
show (EquivClass -> [Char]) -> (Ast -> EquivClass) -> Ast -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ast -> EquivClass
equivClass) Ast
ast2
                  )
                )
              )
          )
            (TraceElem Ast -> (OptStage, (Hints, (AgdaVar, AgdaVar))))
-> Trace Ast -> [(OptStage, (Hints, (AgdaVar, AgdaVar)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Trace Ast
certTrace
      certFile :: [Char]
certFile = [Char]
certName [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
".agda"
   in ([Char]
certFile, [Char] -> [Char] -> [[Char]] -> [Char]
mkCertificateModule [Char]
certName [Char]
agdaTrace [[Char]]
imports)

mkCertificateModule :: String -> String -> [String] -> String
mkCertificateModule :: [Char] -> [Char] -> [[Char]] -> [Char]
mkCertificateModule [Char]
certModule [Char]
agdaTrace [[Char]]
imports =
  [Char]
"module "
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
certModule
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" where\
       \\n\
       \\nopen import Certifier\
       \\nopen import VerifiedCompilation\
       \\nopen import VerifiedCompilation.Certificate hiding (_>>=_)\
       \\nopen import VerifiedCompilation.Trace\
       \\nopen import Untyped\
       \\nopen import RawU\
       \\nopen import Builtin\
       \\nopen import Data.Unit\
       \\nopen import Data.Nat\
       \\nopen import Data.Integer\
       \\nopen import Data.Maybe\
       \\nopen import Data.List\
       \\nopen import Utils hiding (List; _>>=_)\
       \\nimport Agda.Builtin.Bool\
       \\nimport Relation.Nullary\
       \\nimport VerifiedCompilation.UntypedTranslation\
       \\nopen import Agda.Builtin.List using (_∷_; [])\
       \\nopen import Agda.Builtin.Maybe\
       \\nopen import Data.Empty using (⊥)\
       \\nopen import Data.Bool.Base using (Bool; false; true)\
       \\nopen import Agda.Builtin.Equality using (_≡_; refl)\
       \\n"
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [[Char]] -> [Char]
unlines [[Char]]
imports
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n\
       \\nasts : List (OptTag × Hints × Untyped × Untyped)\
       \\nasts = "
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
agdaTrace
    [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n\
       \\nasts_trace : Trace (0 ⊢)\
       \\nasts_trace = to-witness-T (toTrace asts >>= checkScopeᵗ) tt\
       \\n\
       \\ncertificate : Certificate asts_trace\
       \\ncertificate = cert asts_trace (certify asts_trace) tt\
       \\n"

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

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

mkAgdaCertificateProject
  :: Certificate
  -> AgdaCertificateProject
mkAgdaCertificateProject :: Certificate -> AgdaCertificateProject
mkAgdaCertificateProject Certificate
cert =
  let name :: [Char]
name = Certificate -> [Char]
certName Certificate
cert
      mainModule :: ([Char], [Char])
mainModule = Certificate -> ([Char], [Char])
mkCertificateFile Certificate
cert
      astModules :: [([Char], [Char])]
astModules = (Ast -> ([Char], [Char])) -> [Ast] -> [([Char], [Char])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ast -> ([Char], [Char])
mkAgdaAstFile (Certificate -> [Ast]
certReprAsts Certificate
cert)
      agdalib :: ([Char], [Char])
agdalib = [Char] -> ([Char], [Char])
mkAgdaLib [Char]
name
   in AgdaCertificateProject {([Char], [Char])
mainModule :: ([Char], [Char])
mainModule :: ([Char], [Char])
mainModule, [([Char], [Char])]
astModules :: [([Char], [Char])]
astModules :: [([Char], [Char])]
astModules, ([Char], [Char])
agdalib :: ([Char], [Char])
agdalib :: ([Char], [Char])
agdalib}

writeCertificateProject
  :: CertDir
  -> AgdaCertificateProject
  -> Certifier ()
writeCertificateProject :: [Char] -> AgdaCertificateProject -> ExceptT CertifierError IO ()
writeCertificateProject
  [Char]
certDir
  AgdaCertificateProject
    { ([Char], [Char])
mainModule :: AgdaCertificateProject -> ([Char], [Char])
mainModule :: ([Char], [Char])
mainModule
    , [([Char], [Char])]
astModules :: AgdaCertificateProject -> [([Char], [Char])]
astModules :: [([Char], [Char])]
astModules
    , ([Char], [Char])
agdalib :: AgdaCertificateProject -> ([Char], [Char])
agdalib :: ([Char], [Char])
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 ([Char]
mainModulePath, [Char]
mainModuleContents) = ([Char], [Char])
mainModule
          ([Char]
agdalibPath, [Char]
agdalibContents) = ([Char], [Char])
agdalib
          certName :: [Char]
certName = [Char] -> [Char]
takeBaseName [Char]
mainModulePath
      Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True [Char]
certDir
      Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True ([Char]
certDir [Char] -> [Char] -> [Char]
</> [Char]
"src")
      [Char] -> [Char] -> IO ()
writeFile ([Char]
certDir [Char] -> [Char] -> [Char]
</> [Char]
"src" [Char] -> [Char] -> [Char]
</> [Char]
mainModulePath) [Char]
mainModuleContents
      [Char] -> [Char] -> IO ()
writeFile ([Char]
certDir [Char] -> [Char] -> [Char]
</> [Char]
agdalibPath) [Char]
agdalibContents
      let readmeTemplate :: [Char]
readmeTemplate = $(embedStringFile "file-embed/certificate-README.md")
      [Char] -> [Char] -> IO ()
writeFile ([Char]
certDir [Char] -> [Char] -> [Char]
</> [Char]
"README.md") ([Char] -> [Char] -> [Char] -> [Char]
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace [Char]
"{{NAME}}" [Char]
certName [Char]
readmeTemplate)
      (([Char], [Char]) -> IO ()) -> [([Char], [Char])] -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
        ( \([Char]
path, [Char]
contents) ->
            [Char] -> [Char] -> IO ()
writeFile ([Char]
certDir [Char] -> [Char] -> [Char]
</> [Char]
"src" [Char] -> [Char] -> [Char]
</> [Char]
path) [Char]
contents
        )
        [([Char], [Char])]
astModules