WIP agda tests.

plutus-conformance/README.md

@@ -15,15 +15,31 @@ The tests currently cover or will cover the Haskell and Agda implementation of:
 - Coverage test
 <!-- - Costing conformance? -->
 
-There are also executables for users to run:
+## Adding/updating test outputs
 
-1. `add-test-output` for easy addition/alteration of test cases. Run
+To update test outputs, use the accept test option of the tests. E.g., to have the test results overwriting the `.expected` files in the Haskell implementation test suite (`haskell-conformance`) , run:
+
+`cabal test haskell-conformance --test-options=--accept`
+
+There is also an executable (`add-test-output`) for adding test output with more refined options:
+
+E.g., run
+
+`cabal run add-test-output .uplc plutus-conformance/uplc/ eval -- --missing`
+
+to have the executable search for files with extension `.uplc` in the /uplc directory that are missing output files. It will evaluate and create output files for them.
+
+Or, to update and add outputs to all files in the /uplc directory, run
+
+cabal run add-test-output .uplc plutus-conformance/uplc/ eval -- --all
+
+For the manual, run:
 
 `cabal run add-test-output -- -h`
 
-for the manual.
+## Executable for Haskell implementation
 
-2. (WIP) `haskell-implementation` for Haskell implementation CLI testing/usage. 
+(WIP) `haskell-implementation` is an executable for Haskell implementation CLI testing/usage. 
 
 ## The Plutus Conformance Test Suite Library
 

plutus-conformance/agda/Spec.hs

@@ -3,7 +3,14 @@
 module Main (main) where
 
 import MAlonzo.Code.Main (runUAgda)
-import PlutusConformance.Common (agdaEvalUplcProg, runUplcEvalTests)
+import PlutusConformance.Common
+
+-- | Our `evaluator` for the Agda UPLC tests is the CEK machine.
+agdaEvalUplcProg :: UplcProg -> Maybe UplcProg
+agdaEvalUplcProg p =
+    case runUAgda (mkTerm p) of
+        Left _  -> Nothing
+        Right p -> Just p
 
 main :: IO ()
 main =

plutus-conformance/haskell/Spec.hs

@@ -2,7 +2,25 @@
 
 module Main (main) where
 
-import PlutusConformance.Common (evalUplcProg, runUplcEvalTests)
+import Control.Lens (traverseOf)
+import PlutusConformance.Common
+import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekParameters)
+import UntypedPlutusCore qualified as UPLC
+import UntypedPlutusCore.Evaluation.Machine.Cek (evaluateCekNoEmit)
+
+
+-- | Our `evaluator` for the Haskell UPLC tests is the CEK machine.
+evalUplcProg :: UplcEvaluator
+evalUplcProg = traverseOf UPLC.progTerm eval
+  where
+    eval t = do
+        -- The evaluator throws if the term has free variables
+        case UPLC.deBruijnTerm t of
+            Left (_ :: UPLC.FreeVariableError) -> Nothing
+            Right _                            -> Just ()
+        case evaluateCekNoEmit defaultCekParameters t of
+            Left _     -> Nothing
+            Right prog -> Just prog
 
 main :: IO ()
 main =

plutus-conformance/plutus-conformance.cabal

@@ -49,7 +49,6 @@ library
     , base
     , directory
     , filepath
-    , lens
     , megaparsec
     , plutus-core
     , tasty
@@ -86,18 +85,19 @@ executable haskell-implementation
     , tasty-golden
     , text
 
-test-suite haskell-implementation-conformance
+test-suite haskell-conformance
   import:         lang
   type:           exitcode-stdio-1.0
   main-is:        Spec.hs
   hs-source-dirs: haskell
   other-modules:
   build-depends:
     , base                >=4.9 && <5
+    , lens
     , plutus-conformance
     , plutus-core
 
-test-suite agda-implementation-conformance
+test-suite agda-conformance
   import:         lang
   type:           exitcode-stdio-1.0
   main-is:        Spec.hs

plutus-conformance/src/PlutusConformance/Common.hs

@@ -6,13 +6,12 @@
 {- | Plutus conformance test suite library. -}
 module PlutusConformance.Common where
 
-import Control.Lens (traverseOf)
 import Data.Proxy (Proxy (Proxy))
 import Data.Text qualified as T
 import Data.Text.IO qualified as T
+import PlutusCore.Core.Type qualified as PLC
 import PlutusCore.Default (DefaultFun, DefaultUni)
 import PlutusCore.Error (ParserErrorBundle)
-import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekParameters)
 import PlutusCore.Name (Name)
 import PlutusCore.Quote (runQuoteT)
 import PlutusPrelude
@@ -23,7 +22,6 @@ import Test.Tasty.Options
 import Test.Tasty.Providers
 import Text.Megaparsec (SourcePos)
 import UntypedPlutusCore qualified as UPLC
-import UntypedPlutusCore.Evaluation.Machine.Cek (evaluateCekNoEmit)
 import UntypedPlutusCore.Parser qualified as UPLC
 import Witherable
 
@@ -90,6 +88,10 @@ type UplcProg = UPLC.Program Name DefaultUni DefaultFun ()
 
 type UplcEvaluator = UplcProg -> Maybe UplcProg
 
+-- | Turn a UPLC program to a UPLC term.
+mkTerm :: UPLC.Program name uni fun () -> UPLC.Term name uni fun ()
+mkTerm (UPLC.Program _ _ t) = t
+
 -- | A UPLC evaluation test suite.
 data UplcEvaluationTest =
     MkUplcEvaluationTest {
@@ -119,30 +121,13 @@ instance IsTest UplcEvaluationTest where
 
     testOptions = pure [Option (Proxy :: Proxy AcceptTests)]
 
--- | The default parser to parse the inputs.
+-- | The default parser to parse the UPLC program inputs.
 parseTxt ::
     T.Text
     -> Either ParserErrorBundle (UPLC.Program Name DefaultUni DefaultFun SourcePos)
 parseTxt resTxt = runQuoteT $ UPLC.parseProgram resTxt
 
--- | Our `evaluator` for the Haskell UPLC tests is the CEK machine.
-evalUplcProg :: UplcEvaluator
-evalUplcProg = traverseOf UPLC.progTerm eval
-  where
-    eval t = do
-        -- The evaluator throws if the term has free variables
-        case UPLC.deBruijnTerm t of
-            Left (_ :: UPLC.FreeVariableError) -> Nothing
-            Right _                            -> Just ()
-        case evaluateCekNoEmit defaultCekParameters t of
-            Left _     -> Nothing
-            Right prog -> Just prog
-
--- | Our `evaluator` for the Agda UPLC tests is the CEK machine.
-agdaEvalUplcProg :: UplcProg -> Maybe UplcProg
-agdaEvalUplcProg _p = undefined
-
--- | Run the tests given a `evaluator` that evaluates UPLC programs.
+-- | Run the UPLC evaluation tests given an `evaluator` that evaluates UPLC programs.
 runUplcEvalTests ::
     UplcEvaluator -- ^ The action to run the input through for the tests.
     -> IO ()