{-# 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.Foldable
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 ((</>))

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 -> 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

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 -> String
certName :: String
  , Certificate -> Trace Ast
certTrace :: Trace Ast
  , Certificate -> [Ast]
certReprAsts :: [Ast]
  }

mkCertificate :: String -> Trace UTerm -> Certificate
mkCertificate :: String -> Trace UTerm -> Certificate
mkCertificate String
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
        { String
certName :: String
certName :: String
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 :: String
errorMessage =
      String
"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 (String -> Ast
forall a. HasCallStack => String -> a
error String
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 (String -> Ast
forall a. HasCallStack => String -> a
error String
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 -> String
mkAstModuleName Ast {EquivClass
equivClass :: Ast -> EquivClass
equivClass :: EquivClass
equivClass} =
  String
"Ast" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> EquivClass -> String
forall a. Show a => a -> String
show EquivClass
equivClass

mkAgdaAstFile :: Ast -> (FilePath, String)
mkAgdaAstFile :: Ast -> (String, String)
mkAgdaAstFile Ast
ast =
  let agdaAst :: String
agdaAst = UTerm -> String
forall a. AgdaUnparse a => a -> String
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 :: String
agdaModuleName = Ast -> String
mkAstModuleName Ast
ast
      agdaIdStr :: String
agdaIdStr = String
"ast" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> EquivClass -> String
forall a. Show a => a -> String
show EquivClass
agdaId
      agdaAstTy :: String
agdaAstTy = String
agdaIdStr String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" : Untyped"
      agdaAstDef :: String
agdaAstDef = String
agdaIdStr String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
agdaAst
      agdaAstFile :: String
agdaAstFile = String
agdaModuleName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".agda"
   in (String
agdaAstFile, String -> String -> String -> String
mkAstModule String
agdaModuleName String
agdaAstTy String
agdaAstDef)

mkAstModule :: String -> String -> String -> String
mkAstModule :: String -> String -> String -> String
mkAstModule String
agdaIdStr String
agdaAstTy String
agdaAstDef =
  String
"module "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
agdaIdStr
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" 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"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
agdaAstTy
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n\
       \\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
agdaAstDef
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"

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

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

mkCertificateModule :: String -> String -> [String] -> String
mkCertificateModule :: String -> String -> [String] -> String
mkCertificateModule String
certModule String
agdaTrace [String]
imports =
  String
"module "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
certModule
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" 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"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unlines [String]
imports
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n\
       \\nasts : List (OptTag × Hints × Untyped × Untyped)\
       \\nasts = "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
agdaTrace
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\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 -> (String, String)
mainModule :: (FilePath, String)
  , AgdaCertificateProject -> [(String, String)]
astModules :: [(FilePath, 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, String)
mainModule = Certificate -> (String, String)
mkCertificateFile Certificate
cert
      astModules :: [(String, String)]
astModules = (Ast -> (String, String)) -> [Ast] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ast -> (String, String)
mkAgdaAstFile (Certificate -> [Ast]
certReprAsts Certificate
cert)
      agdalib :: (String, String)
agdalib = String -> (String, String)
mkAgdaLib String
name
   in AgdaCertificateProject {(String, String)
mainModule :: (String, String)
mainModule :: (String, String)
mainModule, [(String, String)]
astModules :: [(String, String)]
astModules :: [(String, String)]
astModules, (String, String)
agdalib :: (String, String)
agdalib :: (String, String)
agdalib}

writeCertificateProject
  :: CertDir
  -> AgdaCertificateProject
  -> Certifier ()
writeCertificateProject :: String -> AgdaCertificateProject -> ExceptT CertifierError IO ()
writeCertificateProject
  String
certDir
  AgdaCertificateProject
    { (String, String)
mainModule :: AgdaCertificateProject -> (String, String)
mainModule :: (String, String)
mainModule
    , [(String, String)]
astModules :: AgdaCertificateProject -> [(String, String)]
astModules :: [(String, 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
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
certDir
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
certDir String -> String -> String
</> String
"src")
      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
      ((String, String) -> IO ()) -> [(String, String)] -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
        ( \(String
path, String
contents) ->
            String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> String
path) String
contents
        )
        [(String, String)]
astModules