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

import Control.Monad ((>=>))
import Control.Monad.Except (ExceptT (..), runExceptT, throwError)
import Control.Monad.IO.Class (liftIO)
import Data.Char (toUpper)
import Data.List (find)
import Data.List.NonEmpty (NonEmpty (..))
import Data.List.NonEmpty qualified as NE
import Data.Maybe (fromJust)
import Data.Time.Clock.System (getSystemTime, systemNanoseconds)
import System.Directory (createDirectory)
import System.FilePath ((</>))

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

import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Transform.Simplifier

import MAlonzo.Code.VerifiedCompilation (runCertifierMain)

type CertName = String
type CertDir = String

data CertifierError
  = InvalidCertificate CertDir
  | InvalidCompilerOutput
  | ValidationError CertName

newtype CertifierSuccess = CertifierSuccess
  { CertifierSuccess -> FilePath
certDir :: CertDir
  }

prettyCertifierError :: CertifierError -> String
prettyCertifierError :: CertifierError -> FilePath
prettyCertifierError (InvalidCertificate FilePath
certDir) =
  FilePath
"\n\nInvalid certificate: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
certDir FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>
  FilePath
"\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 =
  FilePath
"\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 FilePath
name) =
  FilePath
"\n\nInvalid certificate name: \
  \\nThe certificate name " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
name FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" is invalid. \
  \Please use only alphanumeric characters, underscores and dashes. \
  \The first character must be a letter.\n"

prettyCertifierSuccess :: CertifierSuccess -> String
prettyCertifierSuccess :: CertifierSuccess -> FilePath
prettyCertifierSuccess (CertifierSuccess FilePath
certDir) =
  FilePath
"\n\nCertificate successfully created: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
certDir FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>
  FilePath
"\nThe compilation was successfully certified.\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
  -> Certifier CertifierSuccess
mkCertifier :: forall a.
SimplifierTrace Name DefaultUni DefaultFun a
-> FilePath -> Certifier CertifierSuccess
mkCertifier SimplifierTrace Name DefaultUni DefaultFun a
simplTrace FilePath
certName = do
  FilePath
certName' <- FilePath -> Certifier FilePath
validCertName FilePath
certName
  let rawAgdaTrace :: [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace = SimplifierTrace Name DefaultUni DefaultFun a
-> [(SimplifierStage, (UTerm, UTerm))]
forall a.
SimplifierTrace Name DefaultUni DefaultFun a
-> [(SimplifierStage, (UTerm, UTerm))]
mkFfiSimplifierTrace SimplifierTrace Name DefaultUni DefaultFun a
simplTrace
  case [(SimplifierStage, (UTerm, UTerm))] -> T_Maybe_10 () Bool
runCertifierMain [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace of
    Just Bool
True -> do
      let cert :: AgdaCertificateProject
cert = Certificate -> AgdaCertificateProject
mkAgdaCertificateProject (Certificate -> AgdaCertificateProject)
-> Certificate -> AgdaCertificateProject
forall a b. (a -> b) -> a -> b
$ FilePath -> [(SimplifierStage, (UTerm, UTerm))] -> Certificate
mkCertificate FilePath
certName' [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace
      FilePath -> CertifierSuccess
CertifierSuccess (FilePath -> CertifierSuccess)
-> Certifier FilePath -> Certifier CertifierSuccess
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AgdaCertificateProject -> Certifier FilePath
writeCertificateProject AgdaCertificateProject
cert
    Just Bool
False -> do
      let cert :: AgdaCertificateProject
cert = Certificate -> AgdaCertificateProject
mkAgdaCertificateProject (Certificate -> AgdaCertificateProject)
-> Certificate -> AgdaCertificateProject
forall a b. (a -> b) -> a -> b
$ FilePath -> [(SimplifierStage, (UTerm, UTerm))] -> Certificate
mkCertificate FilePath
certName' [(SimplifierStage, (UTerm, UTerm))]
rawAgdaTrace
      FilePath
certDir <- AgdaCertificateProject -> Certifier FilePath
writeCertificateProject AgdaCertificateProject
cert
      CertifierError -> Certifier CertifierSuccess
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CertifierError -> Certifier CertifierSuccess)
-> CertifierError -> Certifier CertifierSuccess
forall a b. (a -> b) -> a -> b
$ FilePath -> CertifierError
InvalidCertificate FilePath
certDir
    T_Maybe_10 () Bool
Nothing -> CertifierError -> Certifier CertifierSuccess
forall a. CertifierError -> ExceptT CertifierError IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError CertifierError
InvalidCompilerOutput

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

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 -> FilePath
certName     :: String
  , Certificate -> [(SimplifierStage, (Ast, Ast))]
certTrace    :: [(SimplifierStage, (Ast, Ast))]
  , Certificate -> [Ast]
certReprAsts :: [Ast]
  }

mkCertificate :: String -> [(SimplifierStage, (UTerm, UTerm))] -> Certificate
mkCertificate :: FilePath -> [(SimplifierStage, (UTerm, UTerm))] -> Certificate
mkCertificate FilePath
certName [(SimplifierStage, (UTerm, UTerm))]
rawTrace =
  let traceWithIds :: [(SimplifierStage, (TermWithId, TermWithId))]
traceWithIds = [(SimplifierStage, (UTerm, UTerm))]
-> [(SimplifierStage, (TermWithId, TermWithId))]
addIds [(SimplifierStage, (UTerm, UTerm))]
rawTrace
      allTermWithIds :: [TermWithId]
allTermWithIds = [(SimplifierStage, (TermWithId, TermWithId))] -> [TermWithId]
extractTermWithIds [(SimplifierStage, (TermWithId, 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 :: [(SimplifierStage, (Ast, Ast))]
certTrace = [Ast]
-> [(SimplifierStage, (TermWithId, TermWithId))]
-> [(SimplifierStage, (Ast, Ast))]
mkAstTrace [Ast]
allAsts [(SimplifierStage, (TermWithId, TermWithId))]
traceWithIds
      certReprAsts :: [Ast]
certReprAsts = [NonEmpty Ast] -> [Ast]
getRepresentatives [NonEmpty Ast]
groupedAsts
   in Certificate
        { FilePath
certName :: FilePath
certName :: FilePath
certName
        , [(SimplifierStage, (Ast, Ast))]
certTrace :: [(SimplifierStage, (Ast, Ast))]
certTrace :: [(SimplifierStage, (Ast, Ast))]
certTrace
        , [Ast]
certReprAsts :: [Ast]
certReprAsts :: [Ast]
certReprAsts
        }
  where
    addIds
      :: [(SimplifierStage, (UTerm, UTerm))]
      -> [(SimplifierStage, (TermWithId, TermWithId))]
    addIds :: [(SimplifierStage, (UTerm, UTerm))]
-> [(SimplifierStage, (TermWithId, TermWithId))]
addIds = EquivClass
-> [(SimplifierStage, (UTerm, UTerm))]
-> [(SimplifierStage, (TermWithId, TermWithId))]
go EquivClass
0
      where
        go
          :: Int
          -> [(SimplifierStage, (UTerm, UTerm))]
          -> [(SimplifierStage, (TermWithId, TermWithId))]
        go :: EquivClass
-> [(SimplifierStage, (UTerm, UTerm))]
-> [(SimplifierStage, (TermWithId, TermWithId))]
go EquivClass
_ [] = []
        go EquivClass
id ((SimplifierStage
stage, (UTerm
before, UTerm
after)) : [(SimplifierStage, (UTerm, 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, (TermWithId
beforeWithId, TermWithId
afterWithId)) (SimplifierStage, (TermWithId, TermWithId))
-> [(SimplifierStage, (TermWithId, TermWithId))]
-> [(SimplifierStage, (TermWithId, TermWithId))]
forall a. a -> [a] -> [a]
: EquivClass
-> [(SimplifierStage, (UTerm, UTerm))]
-> [(SimplifierStage, (TermWithId, TermWithId))]
go (EquivClass
id EquivClass -> EquivClass -> EquivClass
forall a. Num a => a -> a -> a
+ EquivClass
2) [(SimplifierStage, (UTerm, UTerm))]
rest

    extractTermWithIds
      :: [(SimplifierStage, (TermWithId, TermWithId))]
      -> [TermWithId]
    extractTermWithIds :: [(SimplifierStage, (TermWithId, TermWithId))] -> [TermWithId]
extractTermWithIds = ((SimplifierStage, (TermWithId, TermWithId)) -> [TermWithId])
-> [(SimplifierStage, (TermWithId, TermWithId))] -> [TermWithId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(SimplifierStage
_, (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

    mkAsts :: [TermWithId] -> [Ast]
    mkAsts :: [TermWithId] -> [Ast]
mkAsts = [TermWithId] -> [NonEmpty Ast]
findEquivClasses ([TermWithId] -> [NonEmpty Ast])
-> (NonEmpty Ast -> [Ast]) -> [TermWithId] -> [Ast]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> NonEmpty Ast -> [Ast]
forall a. NonEmpty a -> [a]
NE.toList

    mkAstTrace
      :: [Ast]
      -> [(SimplifierStage, (TermWithId, TermWithId))]
      -> [(SimplifierStage, (Ast, Ast))]
    mkAstTrace :: [Ast]
-> [(SimplifierStage, (TermWithId, TermWithId))]
-> [(SimplifierStage, (Ast, Ast))]
mkAstTrace [Ast]
_ [] = []
    mkAstTrace [Ast]
allAsts ((SimplifierStage
stage, (TermWithId
rawBefore, TermWithId
rawAfter)) : [(SimplifierStage, (TermWithId, TermWithId))]
rest) =
      let Just Ast
processedBefore = (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
          Just Ast
processedAfter = (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, (Ast
processedBefore, Ast
processedAfter)) (SimplifierStage, (Ast, Ast))
-> [(SimplifierStage, (Ast, Ast))]
-> [(SimplifierStage, (Ast, Ast))]
forall a. a -> [a] -> [a]
: [Ast]
-> [(SimplifierStage, (TermWithId, TermWithId))]
-> [(SimplifierStage, (Ast, Ast))]
mkAstTrace [Ast]
allAsts [(SimplifierStage, (TermWithId, TermWithId))]
rest

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

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

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

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

newtype AgdaVar = AgdaVar String

instance AgdaUnparse AgdaVar where
  agdaUnparse :: AgdaVar -> FilePath
agdaUnparse (AgdaVar FilePath
var) = FilePath
var

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

mkCertificateModule :: String -> String -> [String] -> String
mkCertificateModule :: FilePath -> FilePath -> [FilePath] -> FilePath
mkCertificateModule FilePath
certModule FilePath
agdaTrace [FilePath]
imports =
  FilePath
"module " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
certModule FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" 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" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> [FilePath] -> FilePath
unlines [FilePath]
imports FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>
  FilePath
"\n\
  \\nasts : List (SimplifierTag × Untyped × Untyped)\
  \\nasts = " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
agdaTrace FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>
  FilePath
"\n\
  \\ncertificate : passed? (runCertifier asts) ≡ true\
  \\ncertificate = refl\
  \\n"

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

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

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

writeCertificateProject
  :: AgdaCertificateProject
  -> Certifier CertDir
writeCertificateProject :: AgdaCertificateProject -> Certifier FilePath
writeCertificateProject
  AgdaCertificateProject
    { (FilePath, FilePath)
mainModule :: AgdaCertificateProject -> (FilePath, FilePath)
mainModule :: (FilePath, FilePath)
mainModule, [(FilePath, FilePath)]
astModules :: AgdaCertificateProject -> [(FilePath, FilePath)]
astModules :: [(FilePath, FilePath)]
astModules, FilePath
projectDir :: AgdaCertificateProject -> FilePath
projectDir :: FilePath
projectDir, (FilePath, FilePath)
agdalib :: AgdaCertificateProject -> (FilePath, FilePath)
agdalib :: (FilePath, FilePath)
agdalib }
  = IO FilePath -> Certifier FilePath
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FilePath -> Certifier FilePath)
-> IO FilePath -> Certifier FilePath
forall a b. (a -> b) -> a -> b
$ do
      let (FilePath
mainModulePath, FilePath
mainModuleContents) = (FilePath, FilePath)
mainModule
          (FilePath
agdalibPath, FilePath
agdalibContents) = (FilePath, FilePath)
agdalib
          astModulePaths :: [FilePath]
astModulePaths = ((FilePath, FilePath) -> FilePath)
-> [(FilePath, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> a
fst [(FilePath, FilePath)]
astModules
          astModuleContents :: [FilePath]
astModuleContents = ((FilePath, FilePath) -> FilePath)
-> [(FilePath, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd [(FilePath, FilePath)]
astModules
      Word32
time <- SystemTime -> Word32
systemNanoseconds (SystemTime -> Word32) -> IO SystemTime -> IO Word32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO SystemTime
getSystemTime
      let actualProjectDir :: FilePath
actualProjectDir = FilePath
projectDir FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
"-" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Word32 -> FilePath
forall a. Show a => a -> FilePath
show Word32
time
      FilePath -> IO ()
createDirectory FilePath
actualProjectDir
      FilePath -> IO ()
createDirectory (FilePath
actualProjectDir FilePath -> FilePath -> FilePath
</> FilePath
"src")
      FilePath -> FilePath -> IO ()
writeFile (FilePath
actualProjectDir FilePath -> FilePath -> FilePath
</> FilePath
"src" FilePath -> FilePath -> FilePath
</> FilePath
mainModulePath) FilePath
mainModuleContents
      FilePath -> FilePath -> IO ()
writeFile (FilePath
actualProjectDir FilePath -> FilePath -> FilePath
</> FilePath
agdalibPath) FilePath
agdalibContents
      ((FilePath, FilePath) -> IO ()) -> [(FilePath, FilePath)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(FilePath
path, FilePath
contents) ->
        FilePath -> FilePath -> IO ()
writeFile (FilePath
actualProjectDir FilePath -> FilePath -> FilePath
</> FilePath
"src" FilePath -> FilePath -> FilePath
</> FilePath
path) FilePath
contents) [(FilePath, FilePath)]
astModules
      FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
actualProjectDir