{-# OPTIONS_GHC -Wall #-}

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

import Control.Monad
import Control.Monad.Except (ExceptT (..), runExceptT, throwError)
import Control.Monad.IO.Class (liftIO)
import Data.Char (toUpper)
import Data.Foldable
import Data.List.NonEmpty (NonEmpty (..))
import Data.List.NonEmpty qualified as NE
import Data.Maybe (fromMaybe)
import Data.Text.IO qualified as T
import System.Directory (createDirectory)
import System.FilePath ((</>))

import FFI.AgdaUnparse (AgdaUnparse (..))
import FFI.SimplifierTrace (Trace, mkFfiSimplifierTrace)
import FFI.Untyped (UTerm)

import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Transform.Simplifier

import MAlonzo.Code.Certifier (runCertifierMain)

type CertName = String
type CertDir = FilePath

data CertifierError
  = InvalidCertificate CertDir
  | 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
"\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"
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
  :: SimplifierTrace UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a
  -- ^ The trace produced by the simplification process
  -> CertName
  -- ^ The name of the certificate to be produced
  -> CertifierOutput
  -> Certifier ()
mkCertifier :: forall a.
SimplifierTrace Name DefaultUni DefaultFun a
-> String -> CertifierOutput -> Certifier ()
mkCertifier SimplifierTrace Name DefaultUni DefaultFun a
simplTrace String
certName CertifierOutput
certOutput = do
  String
certName' <- String -> Certifier String
validCertName String
certName
  let rawAgdaTrace :: Trace UTerm
rawAgdaTrace = SimplifierTrace Name DefaultUni DefaultFun a -> Trace UTerm
forall a.
SimplifierTrace Name DefaultUni DefaultFun a -> Trace UTerm
mkFfiSimplifierTrace SimplifierTrace Name DefaultUni DefaultFun a
simplTrace
  case Trace UTerm -> T_Maybe_10 () (T__'215'__396 Bool T_String_6)
runCertifierMain Trace UTerm
rawAgdaTrace of
    Just (Bool
passed, T_String_6
report) -> do
      IO () -> Certifier ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Certifier ())
-> (String -> IO ()) -> String -> Certifier ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Certifier ()) -> String -> Certifier ()
forall a b. (a -> b) -> a -> b
$
        String
"Certifier result: "
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> if Bool
passed then String
"PASS" else String
"FAIL"
      case CertifierOutput
certOutput of
        CertifierOutput
BasicOutput -> () -> Certifier ()
forall a. a -> ExceptT CertifierError IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        ReportOutput String
file -> IO () -> Certifier ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Certifier ()) -> IO () -> Certifier ()
forall a b. (a -> b) -> a -> b
$ do
          String -> T_String_6 -> IO ()
T.writeFile String
file T_String_6
report
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Report written to " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
file
        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 -> Certifier ()
writeCertificateProject String
certDir AgdaCertificateProject
cert
          IO () -> Certifier ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Certifier ())
-> (String -> IO ()) -> String -> Certifier ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Certifier ()) -> String -> Certifier ()
forall a b. (a -> b) -> a -> b
$ String
"Certificate produced in " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
certDir
          Bool -> Certifier () -> Certifier ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
passed (Certifier () -> Certifier ())
-> (CertifierError -> Certifier ())
-> CertifierError
-> Certifier ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CertifierError -> Certifier ()
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CertifierError -> Certifier ()) -> CertifierError -> Certifier ()
forall a b. (a -> b) -> a -> b
$ String -> CertifierError
InvalidCertificate String
certDir
    T_Maybe_10 () (T__'215'__396 Bool T_String_6)
Nothing -> CertifierError -> Certifier ()
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError CertifierError
InvalidCompilerOutput

-- FIXME: ?????
validCertName :: String -> Certifier String
validCertName :: String -> Certifier String
validCertName [] = CertifierError -> Certifier String
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CertifierError -> Certifier String)
-> CertifierError -> Certifier String
forall a b. (a -> b) -> a -> b
$ String -> CertifierError
ValidationError []
validCertName name :: String
name@(Char
fstC : String
rest) =
  if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isValidChar String
name
    then String -> Certifier String
forall a. a -> ExceptT CertifierError IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Char -> Char
toUpper Char
fstC Char -> String -> String
forall a. a -> [a] -> [a]
: String
rest)
    else CertifierError -> Certifier String
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CertifierError -> Certifier String)
-> CertifierError -> Certifier String
forall a b. (a -> b) -> a -> b
$ String -> CertifierError
ValidationError String
name
  where
    isValidChar :: Char -> Bool
isValidChar Char
c = Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'a' .. Char
'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'A' .. Char
'Z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'0' .. Char
'9'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_-"

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' ((SimplifierStage
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 (SimplifierStage
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 (\(SimplifierStage
_, (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 ((SimplifierStage
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 (SimplifierStage
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
agdaUnparse (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 Untyped\
       \\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 :: AgdaVar -> String
agdaUnparse (AgdaVar String
var) = 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 =
        [(SimplifierStage, (Hints, (AgdaVar, AgdaVar)))] -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse ([(SimplifierStage, (Hints, (AgdaVar, AgdaVar)))] -> String)
-> [(SimplifierStage, (Hints, (AgdaVar, AgdaVar)))] -> String
forall a b. (a -> b) -> a -> b
$
          ( \(SimplifierStage
st, (Hints
hints, (Ast
ast1, Ast
ast2))) ->
              ( SimplifierStage
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 -> (SimplifierStage, (Hints, (AgdaVar, AgdaVar))))
-> Trace Ast -> [(SimplifierStage, (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\
       \\nopen import Untyped\
       \\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.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 (SimplifierTag × 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\
       \\ncertificate : passed? (runCertifier asts) ≡ true\
       \\ncertificate = refl\
       \\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.1.1\
             \\n  plutus-metatheory\
             \\ninclude: src"
   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 -> Certifier ()
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 () -> Certifier ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Certifier ()) -> IO () -> Certifier ()
forall a b. (a -> b) -> a -> b
$ do
      let (String
mainModulePath, String
mainModuleContents) = (String, String)
mainModule
          (String
agdalibPath, String
agdalibContents) = (String, String)
agdalib
      String -> IO ()
createDirectory String
certDir
      String -> IO ()
createDirectory (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