Experiment: branch for running decision procedures without TransMatch

plutus-benchmark/plutus-benchmark.cabal

@@ -571,7 +571,7 @@ test-suite plutus-benchmark-marlowe-tests
 -- TODO: Add benchmarks for the executable semantics when we have a UPLC version
 
 library agda-internal
-  import:          lang, ghc-version-support, os-support
+  import:          lang, os-support
   hs-source-dirs:  agda-common
   exposed-modules: PlutusBenchmark.Agda.Common
   build-depends:
@@ -581,7 +581,7 @@ library agda-internal
     , plutus-metatheory
 
 benchmark validation-agda-cek
-  import:         lang, ghc-version-support, os-support, 
+  import:         lang, os-support
   type:           exitcode-stdio-1.0
   main-is:        BenchAgdaCek.hs
   hs-source-dirs: validation/bench

plutus-conformance/plutus-conformance.cabal

@@ -44,10 +44,6 @@ common os-support
   if (impl(ghcjs) || os(windows))
     buildable: False
 
-common ghc-version-support
-  if (impl(ghc <9.6) || impl(ghc >=9.7))
-    buildable: False
-
 library
   import:          lang, os-support
   hs-source-dirs:  src
@@ -95,7 +91,7 @@ test-suite haskell-steppable-conformance
     , plutus-core         ^>=1.42
 
 test-suite agda-conformance
-  import:         lang, os-support, ghc-version-support
+  import:         lang, os-support
   type:           exitcode-stdio-1.0
   main-is:        Spec.hs
   ghc-options:    -threaded -rtsopts -with-rtsopts=-N

plutus-executables/plutus-executables.cabal

@@ -52,18 +52,13 @@ common lang
   if impl(ghc >=9.8)
     ghc-options: -Wno-x-partial
 
-common ghc-version-support
-  -- See the section on GHC versions in CONTRIBUTING
-  if (impl(ghc <9.6) || impl(ghc >=9.7))
-    buildable: False
-
 -- This means that we no longer support uplc/plc/pir on Windows
 common os-support
   if (impl(ghcjs) || os(windows))
     buildable: False
 
 library lib
-  import:          lang, os-support, ghc-version-support
+  import:          lang, os-support
   hs-source-dirs:  src
   exposed-modules: AgdaUnparse
   build-depends:
@@ -104,7 +99,7 @@ executable plc
     , plutus-core:plutus-core-execlib
 
 executable uplc
-  import:         lang, os-support, ghc-version-support
+  import:         lang, os-support
   main-is:        uplc/Main.hs
   hs-source-dirs: executables
   build-depends:
@@ -128,7 +123,7 @@ executable uplc
 -- build-tool-depends: Agda:agda
 
 test-suite test-simple
-  import:             lang, os-support, ghc-version-support
+  import:             lang, os-support
   type:               exitcode-stdio-1.0
   main-is:            Spec.hs
   hs-source-dirs:     test/simple
@@ -143,7 +138,7 @@ test-suite test-simple
     , plutus-executables:uplc
 
 test-suite test-detailed
-  import:             lang, os-support, ghc-version-support
+  import:             lang, os-support
   type:               exitcode-stdio-1.0
   main-is:            Spec.hs
   hs-source-dirs:     test/detailed
@@ -161,21 +156,3 @@ test-suite test-detailed
   build-tool-depends:
     , plutus-executables:plc
     , plutus-executables:uplc
-
-test-suite test-certifier
-  import:             lang, os-support, ghc-version-support
-  type:               exitcode-stdio-1.0
-  main-is:            Spec.hs
-  hs-source-dirs:     test/certifier
-  build-depends:
-    , base
-    , filepath
-    , plutus-core:plutus-core-testlib
-    , process
-    , tasty
-    , tasty-hunit
-    , text
-
-  build-tool-depends:
-    , plutus-executables:plc
-    , plutus-executables:uplc

plutus-executables/src/AgdaUnparse.hs

@@ -31,8 +31,7 @@ instance AgdaUnparse AgdaFFI.UTerm where
       AgdaFFI.UBuiltin fun -> "(UBuiltin " ++ agdaUnparse fun ++ ")"
       AgdaFFI.UDelay term -> "(UDelay " ++ agdaUnparse term ++ ")"
       AgdaFFI.UForce term -> "(UForce " ++ agdaUnparse term ++ ")"
-      AgdaFFI.UConstr i terms -> "(UConstr " ++ agdaUnparse (fromInteger i :: Natural)
-                                      ++ " " ++ agdaUnparse terms ++ ")"
+      AgdaFFI.UConstr i terms -> "(UConstr " ++ agdaUnparse i ++ " " ++ agdaUnparse terms ++ ")"
       AgdaFFI.UCase term cases -> "(UCase " ++ agdaUnparse term ++ " " ++ agdaUnparse cases ++ ")"
 
 instance AgdaUnparse UPLC.DefaultFun where
@@ -50,10 +49,7 @@ instance AgdaUnparse Natural where
   agdaUnparse = show
 
 instance AgdaUnparse Integer where
-  agdaUnparse x =
-    case (x < 0) of
-      True  -> "(ℤ.negsuc " ++ show (x - 1) ++ ")"
-      False ->  "(ℤ.pos " ++ show x ++ ")"
+  agdaUnparse x = "(ℤ.pos " ++ show x ++ ")"
 
 instance AgdaUnparse Bool where
   agdaUnparse True  = "true"