{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# 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 (intercalate)
import Data.List.Extra (replace)
import Data.List.NonEmpty (NonEmpty (..), cons)
import Data.List.NonEmpty qualified as NE
import Data.List.NonEmptySep as NES
import Data.Text qualified as Text
import Data.Text.IO qualified as T
import System.Directory (createDirectoryIfMissing)
import System.FilePath (takeBaseName, (</>))
import Text.Printf (printf)

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

type CertName = String
type CertDir = FilePath

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

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

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

type Certifier = ExceptT CertifierError IO

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

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

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

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

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

-- | Convert module name to an Agda identifier
toIdent :: ModuleName -> String
toIdent :: ModuleName -> String
toIdent = ModuleName -> String
forall m. Monoid m => NonEmpty m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (ModuleName -> String)
-> (ModuleName -> ModuleName) -> ModuleName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ModuleName -> ModuleName
forall a. a -> NonEmpty a -> NonEmpty a
NE.intersperse String
"."

-- | Convert module name to .agda filepath relative to the source directory
toFilePath :: ModuleName -> FilePath
toFilePath :: ModuleName -> String
toFilePath ModuleName
m = (String -> String -> String) -> String -> ModuleName -> String
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> String -> String
(</>) String
"" ModuleName
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".agda"

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

enclose :: String -> String -> String -> String
enclose :: String -> String -> String -> String
enclose String
l String
r String
x = String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r

data ImportHow = Open | Closed

type Import = (ImportHow, ModuleName, [String])

renderImport :: Import -> String
renderImport :: Import -> String
renderImport (ImportHow
how, ModuleName
name, [String]
idents) =
  String
renderHow String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"import " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
toIdent ModuleName
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
renderUsing
  where
    renderHow :: String
renderHow = case ImportHow
how of
      ImportHow
Open -> String
"open "
      ImportHow
Closed -> String
""
    renderUsing :: String
renderUsing
      | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
idents = String
""
      | Bool
otherwise = String
" using (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
idents String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

astModName :: Int -> ModuleName
astModName :: Int -> ModuleName
astModName Int
n = String -> Int -> ModuleName
passModName String
"AST" Int
n

proofModName :: Int -> ModuleName
proofModName :: Int -> ModuleName
proofModName Int
n = String -> Int -> ModuleName
passModName String
"Proof" Int
n

proofFile :: Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
proofFile :: Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
proofFile Int
n UTerm
_ Maybe (OptStage, Hints)
Nothing = (Int -> ModuleName
proofModName Int
n, [])
proofFile Int
n UTerm
_ (Just (OptStage
pass, Hints
_)) =
  ( ModuleName
modName
  , [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
      [ String
"module " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ModuleName -> String
toIdent ModuleName
modName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" where"
      , String
""
      ]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Import -> String) -> [Import] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Import -> String
renderImport [Import]
imports
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
           , String
"related : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proofSig
           , String
"related = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proofExpr
           ]
  )
  where
    modName :: ModuleName
modName = Int -> ModuleName
proofModName Int
n

    preMod :: ModuleName
preMod = Int -> ModuleName
astModName Int
n
    postMod :: ModuleName
postMod = Int -> ModuleName
astModName (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

    preTerm :: String
preTerm = ModuleName -> String
toIdent ModuleName
preMod String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".ast"
    postTerm :: String
postTerm = ModuleName -> String
toIdent ModuleName
postMod String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".ast"
    hints :: String
hints = ModuleName -> String
toIdent ModuleName
preMod String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".hints"

    proofSig :: String
    proofSig :: String
proofSig =
      [String] -> String
unwords
        [String
"RelationOf", OptStage -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse OptStage
pass, String
preTerm, String
postTerm]

    proofExpr :: String
    proofExpr :: String
proofExpr =
      [String] -> String
unwords
        [ String
"to-witness-T"
        , String -> String -> String -> String
enclose String
"(" String
")" (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
            [ String
"certifyPass"
            , OptStage -> String
forall a. AgdaUnparse a => a -> String
renderAgdaUnparse OptStage
pass
            , String
hints
            , String
preTerm
            , String
postTerm
            ]
        , String
"tt"
        ]

    imports :: [(ImportHow, ModuleName, [String])]
    imports :: [Import]
imports =
      [ (ImportHow
Closed, ModuleName
preMod, [])
      , (ImportHow
Closed, ModuleName
postMod, [])
      , (ImportHow
Open, String
"Data" String -> [String] -> ModuleName
forall a. a -> [a] -> NonEmpty a
:| [String
"Unit"], [String
"tt"])
      , (ImportHow
Open, String
"VerifiedCompilation" String -> [String] -> ModuleName
forall a. a -> [a] -> NonEmpty a
:| [], [])
      , (ImportHow
Open, String
"VerifiedCompilation" String -> [String] -> ModuleName
forall a. a -> [a] -> NonEmpty a
:| String
"Trace" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [], [])
      , (ImportHow
Open, String
"VerifiedCompilation" String -> [String] -> ModuleName
forall a. a -> [a] -> NonEmpty a
:| String
"Certificate" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [], [])
      , (ImportHow
Open, String
"Utils" String -> [String] -> ModuleName
forall a. a -> [a] -> NonEmpty a
:| [], [])
      ]

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

newtype AgdaVar = AgdaVar String

qualify :: ModuleName -> AgdaVar -> AgdaVar
qualify :: ModuleName -> AgdaVar -> AgdaVar
qualify ModuleName
modName (AgdaVar String
x) = String -> AgdaVar
AgdaVar (ModuleName -> String
toIdent ModuleName
modName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x)

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

mkCertificateFile :: Certificate -> String
mkCertificateFile :: Certificate -> String
mkCertificateFile Certificate {String
certName :: Certificate -> String
certName :: String
certName, Trace UTerm
certTrace :: Certificate -> Trace UTerm
certTrace :: Trace UTerm
certTrace} =
  [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [ String
"module " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
certName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" where"
    , String
""
    , String
"open import VerifiedCompilation.Trace"
    , String
"open import Untyped using (_⊢)"
    , String
"open import Utils hiding (List; _>>=_)"
    , String
"open import VerifiedCompilation"
    , String
"open import Data.Unit"
    , String
""
    ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Import -> String) -> [Import] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Import -> String
renderImport ([Import]
astImports [Import] -> [Import] -> [Import]
forall a. [a] -> [a] -> [a]
++ [Import]
proofImports)
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
         , String
"trace : Trace (0 ⊢)"
         , String
"trace ="
         ]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (NonEmptySep (OptStage, AgdaVar) AgdaVar -> [String]
printTrace NonEmptySep (OptStage, AgdaVar) AgdaVar
traceExpr)
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
         , String
"certificate : Certificate trace"
         , String
"certificate = "
         , NonEmpty AgdaVar -> String
renderProof NonEmpty AgdaVar
proofExpr
         ]
  where
    astImports :: [Import]
    astImports :: [Import]
astImports = (Int -> Import) -> [Int] -> [Import]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
n -> (ImportHow
Closed, Int -> ModuleName
astModName Int
n, [])) [Int
0 .. Trace UTerm -> Int
forall a. NonEmptySep (OptStage, Hints) a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Trace UTerm
certTrace Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

    proofImports :: [Import]
    proofImports :: [Import]
proofImports = (Int -> Import) -> [Int] -> [Import]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
n -> (ImportHow
Closed, Int -> ModuleName
proofModName Int
n, [])) [Int
0 .. Trace UTerm -> Int
forall a. NonEmptySep (OptStage, Hints) a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Trace UTerm
certTrace Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2]

    -- Replace hints and ASTs in the trace by agda variables that point to the right definition
    traceExpr :: NonEmptySep (OptStage, AgdaVar) AgdaVar
    traceExpr :: NonEmptySep (OptStage, AgdaVar) AgdaVar
traceExpr = Int -> Trace UTerm -> NonEmptySep (OptStage, AgdaVar) AgdaVar
forall {a} {b} {a}.
Int -> NonEmptySep (a, b) a -> NonEmptySep (a, AgdaVar) AgdaVar
go Int
0 Trace UTerm
certTrace
      where
        go :: Int -> NonEmptySep (a, b) a -> NonEmptySep (a, AgdaVar) AgdaVar
go Int
n (Singleton a
_) = AgdaVar -> NonEmptySep (a, AgdaVar) AgdaVar
forall sep a. a -> NonEmptySep sep a
Singleton (ModuleName -> AgdaVar -> AgdaVar
qualify (Int -> ModuleName
astModName Int
n) (String -> AgdaVar
AgdaVar String
"ast"))
        go Int
n (Cons a
_ (a
stage, b
_) NonEmptySep (a, b) a
xs) =
          AgdaVar
-> (a, AgdaVar)
-> NonEmptySep (a, AgdaVar) AgdaVar
-> NonEmptySep (a, AgdaVar) AgdaVar
forall sep a. a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
Cons
            (ModuleName -> AgdaVar -> AgdaVar
qualify (Int -> ModuleName
astModName Int
n) (String -> AgdaVar
AgdaVar String
"ast"))
            (a
stage, ModuleName -> AgdaVar -> AgdaVar
qualify (Int -> ModuleName
astModName Int
n) (String -> AgdaVar
AgdaVar String
"hints"))
            (Int -> NonEmptySep (a, b) a -> NonEmptySep (a, AgdaVar) AgdaVar
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NonEmptySep (a, b) a
xs)

    -- Non-empty list of variables that point to the proofs per pass
    proofExpr :: NonEmpty AgdaVar
    proofExpr :: NonEmpty AgdaVar
proofExpr = Int -> Trace UTerm -> NonEmpty AgdaVar
forall {sep} {a}. Int -> NonEmptySep sep a -> NonEmpty AgdaVar
go Int
0 Trace UTerm
certTrace
      where
        go :: Int -> NonEmptySep sep a -> NonEmpty AgdaVar
go Int
_ (Singleton a
_) = String -> AgdaVar
AgdaVar String
"tt" AgdaVar -> [AgdaVar] -> NonEmpty AgdaVar
forall a. a -> [a] -> NonEmpty a
:| []
        go Int
n (Cons a
_ sep
_ NonEmptySep sep a
xs) = AgdaVar -> NonEmpty AgdaVar -> NonEmpty AgdaVar
forall a. a -> NonEmpty a -> NonEmpty a
cons (ModuleName -> AgdaVar -> AgdaVar
qualify (Int -> ModuleName
proofModName Int
n) (String -> AgdaVar
AgdaVar String
"related")) (Int -> NonEmptySep sep a -> NonEmpty AgdaVar
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NonEmptySep sep a
xs)

-- Print the imported proofs as a big product
renderProof :: NonEmpty AgdaVar -> String
renderProof :: NonEmpty AgdaVar -> String
renderProof (AgdaVar String
x :| [AgdaVar]
xs) =
  [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [(String
"  ( " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x)]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (AgdaVar -> String) -> [AgdaVar] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(AgdaVar String
p) -> String
"  , " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
p) [AgdaVar]
xs
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(String
"  )")]

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

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

{-| For each term in the trace, create module contents using the given
function, which is also passed the index in the trace. -}
traceToFiles
  :: (Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String))
  -> Trace UTerm
  -> [(ModuleName, String)]
traceToFiles :: (Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String))
-> Trace UTerm -> [(ModuleName, String)]
traceToFiles Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
f Trace UTerm
t = Int -> Trace UTerm -> [(ModuleName, String)]
go Int
0 Trace UTerm
t
  where
    go :: Int -> Trace UTerm -> [(ModuleName, String)]
go Int
n (Singleton UTerm
x) = [Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
f Int
n UTerm
x Maybe (OptStage, Hints)
forall a. Maybe a
Nothing]
    go Int
n (Cons UTerm
x (OptStage
o, Hints
h) Trace UTerm
xs) = Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
f Int
n UTerm
x ((OptStage, Hints) -> Maybe (OptStage, Hints)
forall a. a -> Maybe a
Just (OptStage
o, Hints
h)) (ModuleName, String)
-> [(ModuleName, String)] -> [(ModuleName, String)]
forall a. a -> [a] -> [a]
: Int -> Trace UTerm -> [(ModuleName, String)]
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Trace UTerm
xs

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

mkAgdaCertificateProject
  :: Certificate
  -> AgdaCertificateProject
mkAgdaCertificateProject :: Certificate -> AgdaCertificateProject
mkAgdaCertificateProject Certificate
cert =
  let name :: String
name = Certificate -> String
certName Certificate
cert
      mainModule :: String
mainModule = Certificate -> String
mkCertificateFile Certificate
cert
      astModules :: [(ModuleName, String)]
astModules = (Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String))
-> Trace UTerm -> [(ModuleName, String)]
traceToFiles Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
mkAgdaAstFile (Certificate -> Trace UTerm
certTrace Certificate
cert)
      proofModNames :: [(ModuleName, String)]
proofModNames = (Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String))
-> Trace UTerm -> [(ModuleName, String)]
traceToFiles Int -> UTerm -> Maybe (OptStage, Hints) -> (ModuleName, String)
proofFile (Certificate -> Trace UTerm
certTrace Certificate
cert)
      agdalib :: (String, String)
agdalib = String -> (String, String)
mkAgdaLib String
name
   in AgdaCertificateProject
        { mainModule :: (String, String)
mainModule = (Certificate -> String
certName Certificate
cert String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".agda", String
mainModule)
        , [(ModuleName, String)]
astModules :: [(ModuleName, String)]
astModules :: [(ModuleName, String)]
astModules
        , [(ModuleName, String)]
proofModNames :: [(ModuleName, String)]
proofModNames :: [(ModuleName, String)]
proofModNames
        , (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
    , [(ModuleName, String)]
astModules :: AgdaCertificateProject -> [(ModuleName, String)]
astModules :: [(ModuleName, String)]
astModules
    , [(ModuleName, String)]
proofModNames :: AgdaCertificateProject -> [(ModuleName, String)]
proofModNames :: [(ModuleName, String)]
proofModNames
    , (String, String)
agdalib :: AgdaCertificateProject -> (String, String)
agdalib :: (String, String)
agdalib
    } =
    IO () -> ExceptT CertifierError IO ()
forall a. IO a -> ExceptT CertifierError IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ExceptT CertifierError IO ())
-> IO () -> ExceptT CertifierError IO ()
forall a b. (a -> b) -> a -> b
$ do
      let (String
mainModulePath, String
mainModuleContents) = (String, String)
mainModule
          (String
agdalibPath, String
agdalibContents) = (String, String)
agdalib
          certName :: String
certName = String -> String
takeBaseName String
mainModulePath
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
certDir
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
certDir String -> String -> String
</> String
"src")

      -- directory per AST in trace
      [(ModuleName, String)] -> ((ModuleName, String) -> IO ()) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ ([(ModuleName, String)]
astModules [(ModuleName, String)]
-> [(ModuleName, String)] -> [(ModuleName, String)]
forall a. [a] -> [a] -> [a]
++ [(ModuleName, String)]
proofModNames) (((ModuleName, String) -> IO ()) -> IO ())
-> ((ModuleName, String) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(ModuleName
modName, String
contents) -> do
        Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> ModuleName -> String
moduleDir ModuleName
modName)
        String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> ModuleName -> String
toFilePath ModuleName
modName) String
contents

      String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"src" String -> String -> String
</> String
mainModulePath) String
mainModuleContents
      String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
agdalibPath) String
agdalibContents
      let readmeTemplate :: String
readmeTemplate = $(embedStringFile "file-embed/certificate-README.md")
      String -> String -> IO ()
writeFile (String
certDir String -> String -> String
</> String
"README.md") (String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace String
"{{NAME}}" String
certName String
readmeTemplate)