Kwxm/metatheory/fix test2 (IntersectMBO#6414)

* WIP * Fix broken metatheory tests using textual comparison * Refactor detailed tests * Refactor detailed tests * Re-enable plutus-metatheory:test2 in CI * Fixes in project.nix * Remove unused files * Remove the preCheck hack from plutus-metatheory.components.tests.test-simple * Extra comments * WIP * Fix broken metatheory tests using textual comparison * Refactor detailed tests * Refactor detailed tests * Re-enable plutus-metatheory:test2 in CI * Fixes in project.nix * Remove unused files * Extra comments * Remove the preCheck hack from plutus-metatheory.components.tests.test-simple * Rebase and remove dead code * Remove newline in error message * Address some PR comments * WIP * WIP * Add Output option to plc to make it consistent with uplc * Tidy up output of evaluation/typecheching results * Tidy up output of evaluation/typecheching results * Name change --------- Co-authored-by: zeme <lorenzo.calegari@iohk.io>
v0d1ch · Dec 6, 2024 · 14bc29c · 14bc29c
1 parent 83e0db2
commit 14bc29c
Show file tree

Hide file tree

Showing 24 changed files with 381 additions and 539 deletions.
diff --git a/nix/project.nix b/nix/project.nix
@@ -44,28 +44,14 @@ let
         # Common 
         {
           packages = {
-            # In this case we can just propagate the native dependencies for the build of
-            # the test executable, which are actually set up right (we have a
-            # build-tool-depends on the executable we need)
-            # I'm slightly surprised this works, hooray for laziness!
-            plutus-metatheory.components.tests.test1.preCheck =
-              let
-                cmp = config.hsPkgs.plutus-metatheory.components.tests.test1;
-                deps = cmp.executableToolDepends;
-              in
-              ''PATH=${lib.makeBinPath deps}:$PATH'';
-
-            # FIXME: Somehow this is broken even with setting the path up as above
-            plutus-metatheory.components.tests.test2.doCheck = false;
-
             # plutus-metatheory needs agda with the stdlib around for the custom setup
             # I can't figure out a way to apply this as a blanket change for all the
             # components in the package, oh well
             plutus-metatheory.components.library.build-tools = [ repoRoot.nix.agda-with-stdlib ];
             plutus-metatheory.components.exes.plc-agda.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-metatheory.components.tests.test1.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-metatheory.components.tests.test2.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-metatheory.components.tests.test3.build-tools = [ repoRoot.nix.agda-with-stdlib ];
+            plutus-metatheory.components.tests.test-simple.build-tools = [ repoRoot.nix.agda-with-stdlib ];
+            plutus-metatheory.components.tests.test-detailed.build-tools = [ repoRoot.nix.agda-with-stdlib ];
+            plutus-metatheory.components.tests.test-NEAT.build-tools = [ repoRoot.nix.agda-with-stdlib ];
 
             plutus-core.components.benchmarks.update-cost-model = {
               build-tools = [ repoRoot.nix.r-with-packages ];

diff --git a/plutus-core/executables/pir/Main.hs b/plutus-core/executables/pir/Main.hs
@@ -275,7 +275,7 @@ runPrint (PrintOptions inp outp mode) = do
       Right (p::PirProg PLC.SrcSpan) -> do
         let
             printed :: String
-            printed = show $ getPrintMethod mode p
+            printed = show $ prettyPrintByMode mode p
         case outp of
             FileOutput path -> writeFile path printed
             StdOutput       -> putStrLn printed

diff --git a/plutus-core/executables/plc/Main.hs b/plutus-core/executables/plc/Main.hs
@@ -10,32 +10,37 @@ import PlutusCore.Data
 import PlutusCore.Default (BuiltinSemanticsVariant (..))
 import PlutusCore.Evaluation.Machine.Ck qualified as Ck
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC
+import PlutusCore.Executable.AstIO (toDeBruijnTermPLC, toDeBruijnTypePLC)
 import PlutusCore.Executable.Common
 import PlutusCore.Executable.Parsers
 import PlutusCore.MkPlc (mkConstant)
 import PlutusCore.Pretty qualified as PP
 import PlutusPrelude
 
 import Data.ByteString.Lazy qualified as BSL (readFile)
-import Data.Text.IO qualified as T
 import Flat (unflat)
 import Options.Applicative
-import System.Exit (exitFailure, exitSuccess)
+import System.Exit (exitFailure)
+import System.IO (hPrint, stderr)
 
 plcHelpText :: String
 plcHelpText = helpText "Typed Plutus Core"
 
 plcInfoCommand :: ParserInfo Command
 plcInfoCommand = plutus plcHelpText
 
-data TypecheckOptions = TypecheckOptions Input Format
+data TypecheckOptions = TypecheckOptions Input Format Output PrintMode NameFormat
+
 data EvalOptions =
     EvalOptions
       Input
       Format
+      Output
       PrintMode
+      NameFormat
       (BuiltinSemanticsVariant PLC.DefaultFun)
-data EraseOptions     = EraseOptions Input Format Output Format PrintMode
+
+data EraseOptions = EraseOptions Input Format Output Format PrintMode
 
 
 -- Main commands
@@ -54,14 +59,20 @@ data Command = Apply       ApplyOptions
 ---------------- Option parsers ----------------
 
 typecheckOpts :: Parser TypecheckOptions
-typecheckOpts = TypecheckOptions <$> input <*> inputformat
+typecheckOpts = TypecheckOptions <$> input <*> inputformat <*> output <*> printmode <*> nameformat
 
 eraseOpts :: Parser EraseOptions
 eraseOpts = EraseOptions <$> input <*> inputformat <*> output <*> outputformat <*> printmode
 
 evalOpts :: Parser EvalOptions
 evalOpts =
-  EvalOptions <$> input <*> inputformat <*> printmode <*> builtinSemanticsVariant
+  EvalOptions
+  <$> input
+  <*> inputformat
+  <*> output
+  <*> printmode
+  <*> nameformat
+  <*> builtinSemanticsVariant
 
 plutus ::
   -- | The @helpText@
@@ -161,16 +172,19 @@ runApplyToData (ApplyOptions inputfiles ifmt outp ofmt mode) = do
 ---------------- Typechecking ----------------
 
 runTypecheck :: TypecheckOptions -> IO ()
-runTypecheck (TypecheckOptions inp fmt) = do
+runTypecheck (TypecheckOptions inp fmt outp printMode nameFormat) = do
   prog <- readProgram fmt inp
   case PLC.runQuoteT $ do
     tcConfig <- PLC.getDefTypeCheckConfig ()
     PLC.inferTypeOfProgram tcConfig (void prog)
     of
       Left (e :: PLC.Error PLC.DefaultUni PLC.DefaultFun ()) ->
         errorWithoutStackTrace $ PP.displayPlc e
-      Right ty                                               ->
-        T.putStrLn (PP.displayPlc ty) >> exitSuccess
+      Right (PLC.Normalized ty) ->
+        case nameFormat of
+          IdNames -> writeToOutput outp $ prettyPrintByMode printMode ty
+          DeBruijnNames ->
+            writeToOutput outp $ prettyPrintByMode printMode $ toDeBruijnTypePLC ty
 
 ---------------- Optimisation ----------------
 
@@ -184,13 +198,17 @@ runOptimisations (OptimiseOptions inp ifmt outp ofmt mode) = do
 ---------------- Evaluation ----------------
 
 runEval :: EvalOptions -> IO ()
-runEval (EvalOptions inp ifmt printMode semvar) = do
+runEval (EvalOptions inp ifmt outp printMode nameFormat semvar) = do
   prog <- readProgram ifmt inp
   let evaluate = Ck.evaluateCkNoEmit (PLC.defaultBuiltinsRuntimeForSemanticsVariant semvar)
       term = void $ prog ^. PLC.progTerm
   case evaluate term of
-    Right v  -> print (getPrintMethod printMode v) >> exitSuccess
-    Left err -> print err *> exitFailure
+    Right v  ->
+      case nameFormat of
+        IdNames -> writeToOutput outp (prettyPrintByMode printMode v)
+        DeBruijnNames ->
+          writeToOutput outp (prettyPrintByMode printMode $ toDeBruijnTermPLC v)
+    Left err -> hPrint stderr err *> exitFailure
 
 ----------------- Print examples -----------------------
 
@@ -205,7 +223,7 @@ runErase (EraseOptions inp ifmt outp ofmt mode) = do
   typedProg <- (readProgram ifmt inp :: IO (PlcProg PLC.SrcSpan))
   let untypedProg = () <$ PLC.eraseProgram typedProg
   case ofmt of
-    Textual       -> writePrettyToFileOrStd outp mode untypedProg
+    Textual       -> writePrettyToOutput outp mode untypedProg
     Flat flatMode -> writeFlat outp flatMode untypedProg
 
 ---------------- Driver ----------------

diff --git a/plutus-core/executables/src/PlutusCore/Executable/AstIO.hs b/plutus-core/executables/src/PlutusCore/Executable/AstIO.hs
@@ -12,14 +12,19 @@ module PlutusCore.Executable.AstIO
     , loadPlcASTfromFlat
     , loadUplcASTfromFlat
     , fromNamedDeBruijnUPLC
+    , toDeBruijnTermPLC
+    , toDeBruijnTermUPLC
+    , toDeBruijnTypePLC
+    , toNamedDeBruijnUPLC
     )
 where
 
 import PlutusCore.Executable.Types
 import PlutusPrelude
 
 import PlutusCore qualified as PLC
-import PlutusCore.DeBruijn (fakeNameDeBruijn, fakeTyNameDeBruijn, unNameDeBruijn, unNameTyDeBruijn)
+import PlutusCore.DeBruijn (deBruijnTy, fakeNameDeBruijn, fakeTyNameDeBruijn, unNameDeBruijn,
+                            unNameTyDeBruijn)
 
 import PlutusIR.Core.Instance.Pretty ()
 
@@ -35,6 +40,17 @@ type UplcProgNDB ann = UPLC.Program PLC.NamedDeBruijn PLC.DefaultUni PLC.Default
 type PlcProgDB ann = PLC.Program PLC.TyDeBruijn PLC.DeBruijn PLC.DefaultUni PLC.DefaultFun ann
 type PlcProgNDB ann = PLC.Program PLC.NamedTyDeBruijn PLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ann
 
+-- For the plutus-metatheory tests
+type UplcTermDB ann = UPLC.Term PLC.DeBruijn PLC.DefaultUni PLC.DefaultFun ann
+type UplcTermNDB ann = UPLC.Term PLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ann
+
+type PlcTermDB ann = PLC.Term PLC.TyDeBruijn PLC.DeBruijn PLC.DefaultUni PLC.DefaultFun ann
+type PlcTermNDB ann = PLC.Term PLC.NamedTyDeBruijn PLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun ann
+
+type PlcType ann = PLC.Type PLC.TyName PLC.DefaultUni ann
+type PlcTypeDB ann = PLC.Type PLC.TyDeBruijn PLC.DefaultUni ann
+type PlcTypeNDB ann = PLC.Type PLC.NamedTyDeBruijn PLC.DefaultUni ann
+
 -- | PIR does not support names involving de Bruijn indices. We do allow these
 -- formats here to facilitate code sharing, but issue the error below if they're
 -- encountered.  This should never happen in practice because the options
@@ -44,17 +60,26 @@ unsupportedNameTypeError nameType = error $ "ASTs with " ++ show nameType ++ " n
 
 ---------------- Name conversions ----------------
 
--- Untyped programs
+-- Untyped terms and programs
+-- | Convert an untyped term to one where the 'name' type is textual names
+-- with de Bruijn indices.
+toNamedDeBruijnTermUPLC :: UplcTerm ann -> UplcTermNDB ann
+toNamedDeBruijnTermUPLC = unsafeFromRight @PLC.FreeVariableError . UPLC.deBruijnTerm
+
+-- | Convert an untyped term to one where the 'name' type is de Bruijn indices.
+toDeBruijnTermUPLC :: UplcTerm ann -> UplcTermDB ann
+toDeBruijnTermUPLC = UPLC.termMapNames unNameDeBruijn . toNamedDeBruijnTermUPLC
 
 -- | Convert an untyped program to one where the 'name' type is textual names
 -- with de Bruijn indices.
 toNamedDeBruijnUPLC :: UplcProg ann -> UplcProgNDB ann
-toNamedDeBruijnUPLC = unsafeFromRight @PLC.FreeVariableError
-                    . traverseOf UPLC.progTerm UPLC.deBruijnTerm
+toNamedDeBruijnUPLC (UPLC.Program ann ver term) =
+  UPLC.Program ann ver (toNamedDeBruijnTermUPLC term)
 
 -- | Convert an untyped program to one where the 'name' type is de Bruijn indices.
 toDeBruijnUPLC :: UplcProg ann -> UplcProgDB ann
-toDeBruijnUPLC = UPLC.programMapNames unNameDeBruijn . toNamedDeBruijnUPLC
+toDeBruijnUPLC (UPLC.Program ann ver term) =
+  UPLC.Program ann ver (toDeBruijnTermUPLC term)
 
 -- | Convert an untyped program with named de Bruijn indices to one with textual names.
 fromNamedDeBruijnUPLC :: UplcProgNDB ann -> UplcProg ann
@@ -65,18 +90,35 @@ fromNamedDeBruijnUPLC = unsafeFromRight @PLC.FreeVariableError
 fromDeBruijnUPLC :: UplcProgDB ann -> UplcProg ann
 fromDeBruijnUPLC = fromNamedDeBruijnUPLC . UPLC.programMapNames fakeNameDeBruijn
 
--- Typed programs
+-- Typed terms and programs
+
+-- | Convert a typed term to one where the 'name' type is textual names
+-- with de Bruijn indices.
+toNamedDeBruijnTermPLC :: PlcTerm ann -> PlcTermNDB ann
+toNamedDeBruijnTermPLC = unsafeFromRight @PLC.FreeVariableError . PLC.deBruijnTerm
+
+-- | Convert a typed term to one where the 'name' type is de Bruijn indices.
+toDeBruijnTermPLC :: PlcTerm ann -> PlcTermDB ann
+toDeBruijnTermPLC = PLC.termMapNames unNameTyDeBruijn unNameDeBruijn . toNamedDeBruijnTermPLC
 
 -- | Convert a typed program to one where the 'name' type is textual names with
 -- de Bruijn indices.
 toNamedDeBruijnPLC :: PlcProg ann -> PlcProgNDB ann
-toNamedDeBruijnPLC = unsafeFromRight @PLC.FreeVariableError
-                   . traverseOf PLC.progTerm PLC.deBruijnTerm
+toNamedDeBruijnPLC (PLC.Program ann ver term) =
+  PLC.Program ann ver (toNamedDeBruijnTermPLC term)
 
 -- | Convert a typed program to one where the 'name' type is de Bruijn indices.
 toDeBruijnPLC :: PlcProg ann -> PlcProgDB ann
-toDeBruijnPLC = PLC.programMapNames unNameTyDeBruijn unNameDeBruijn . toNamedDeBruijnPLC
+toDeBruijnPLC (PLC.Program ann ver term) =
+  PLC.Program ann ver (toDeBruijnTermPLC term)
+
+-- | Convert a type to one where the 'tyname' type is named de Bruijn indices.
+toNamedDeBruijnTypePLC :: PlcType ann -> PlcTypeNDB ann
+toNamedDeBruijnTypePLC = unsafeFromRight @PLC.FreeVariableError . deBruijnTy
 
+-- | Convert a type to one where the 'tyname' type is de Bruijn indices.
+toDeBruijnTypePLC :: PlcType ann -> PlcTypeDB ann
+toDeBruijnTypePLC = PLC.typeMapNames unNameTyDeBruijn. toNamedDeBruijnTypePLC
 
 -- | Convert a typed program with named de Bruijn indices to one with textual names.
 fromNamedDeBruijnPLC :: PlcProgNDB ann -> PlcProg ann

diff --git a/plutus-core/executables/src/PlutusCore/Executable/Common.hs b/plutus-core/executables/src/PlutusCore/Executable/Common.hs
@@ -14,7 +14,7 @@ module PlutusCore.Executable.Common
     , getInput
     , getInteresting
     , getPlcExamples
-    , getPrintMethod
+    , prettyPrintByMode
     , getUplcExamples
     , helpText
     , loadASTfromFlat
@@ -29,9 +29,9 @@ module PlutusCore.Executable.Common
     , runPrintExample
     , topSrcSpan
     , writeFlat
-    , writePrettyToFileOrStd
+    , writePrettyToOutput
     , writeProgram
-    , writeToFileOrStd
+    , writeToOutput
     ) where
 
 import PlutusPrelude
@@ -324,13 +324,13 @@ writeFlat outp flatMode prog = do
 
 ---------------- Write an AST as PLC source ----------------
 
-getPrintMethod ::
-    PP.PrettyPlc a => PrintMode -> (a -> Doc ann)
-getPrintMethod = \case
-    Classic        -> PP.prettyPlcClassic
-    Simple         -> PP.prettyPlcClassicSimple
-    Readable       -> PP.prettyPlcReadable
-    ReadableSimple -> PP.prettyPlcReadableSimple
+prettyPrintByMode ::
+    PP.PrettyPlc a => PrintMode -> (a -> Doc a)
+prettyPrintByMode = \case
+  Classic        -> PP.prettyPlcClassic
+  Simple         -> PP.prettyPlcClassicSimple
+  Readable       -> PP.prettyPlcReadable
+  ReadableSimple -> PP.prettyPlcReadableSimple
 
 writeProgram ::
     ( ProgramLike p
@@ -342,24 +342,24 @@ writeProgram ::
     PrintMode ->
     p ann ->
     IO ()
-writeProgram outp Textual mode prog      = writePrettyToFileOrStd outp mode prog
+writeProgram outp Textual mode prog      = writePrettyToOutput outp mode prog
 writeProgram outp (Flat flatMode) _ prog = writeFlat outp flatMode prog
 
-writePrettyToFileOrStd ::
+writePrettyToOutput ::
     (PP.PrettyBy PP.PrettyConfigPlc (p ann)) => Output -> PrintMode -> p ann -> IO ()
-writePrettyToFileOrStd outp mode prog = do
-    let printMethod = getPrintMethod mode
+writePrettyToOutput outp mode prog = do
+    let printMethod = prettyPrintByMode mode
     case outp of
         FileOutput file -> writeFile file . Prelude.show . printMethod $ prog
         StdOutput       -> print . printMethod $ prog
         NoOutput        -> pure ()
 
-writeToFileOrStd ::
-    Output -> String -> IO ()
-writeToFileOrStd outp v = do
+writeToOutput ::
+    Show a => Output -> a -> IO ()
+writeToOutput outp v = do
     case outp of
-        FileOutput file -> writeFile file v
-        StdOutput       -> putStrLn v
+        FileOutput file -> writeFile file $ show v
+        StdOutput       -> putStrLn $ show v
         NoOutput        -> pure ()
 
 ---------------- Examples ----------------
@@ -559,7 +559,7 @@ runPrint
     -> IO ()
 runPrint (PrintOptions inp outp mode) = do
     parsed <- (snd <$> parseInput inp :: IO (p PLC.SrcSpan))
-    let printed = show $ getPrintMethod mode parsed
+    let printed = show $ prettyPrintByMode mode parsed
     case outp of
         FileOutput path -> writeFile path printed
         StdOutput       -> putStrLn printed

diff --git a/plutus-core/executables/src/PlutusCore/Executable/Parsers.hs b/plutus-core/executables/src/PlutusCore/Executable/Parsers.hs
@@ -103,10 +103,17 @@ printmode = option auto
   <> value Simple
   <> showDefault
   <> help
-    ("Print mode for textual output (ignored elsewhere): Classic -> plcPrettyClassicDef, "
-     <> "Debug -> plcPrettyClassicDebug, "
+    ("Print mode for textual output (ignored elsewhere): Classic -> plcPrettyClassic, "
+     <> "Simple -> plcPrettyClassicSimple, "
      <> "Readable -> prettyPlcReadable, ReadableSimple -> prettyPlcReadableSimple" ))
 
+nameformat :: Parser NameFormat
+nameformat =
+  flag IdNames DeBruijnNames
+  (long "debruijn"
+   <> short 'j'
+   <> help "Output evaluation result with de Bruijn indices (default: show textual names)")
+
 printOpts :: Parser PrintOptions
 printOpts = PrintOptions <$> input <*> output <*> printmode
 

diff --git a/plutus-core/executables/src/PlutusCore/Executable/Types.hs b/plutus-core/executables/src/PlutusCore/Executable/Types.hs
@@ -54,6 +54,7 @@ data Output = FileOutput FilePath | StdOutput | NoOutput
 data TimingMode = NoTiming | Timing Integer deriving stock (Eq) -- Report program execution time?
 data CekModel = Default | Unit -- Which cost model should we use for CEK machine steps?
 data PrintMode = Classic | Simple | Readable | ReadableSimple deriving stock (Show, Read)
+data NameFormat = IdNames | DeBruijnNames -- Format for textual output of names
 data TraceMode = None | Logs | LogsWithTimestamps | LogsWithBudgets deriving stock (Show, Read)
 type ExampleName = T.Text
 data ExampleMode = ExampleSingle ExampleName | ExampleAvailable