From 650442cf9ea0ef8bfe8d49fc613d19461261714c Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 13:49:07 +0000
Subject: [PATCH 01/12] Initial plan
From c876ce923ec30d4dd84f2b949535af788bd2390e Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 14:19:08 +0000
Subject: [PATCH 02/12] Convert test infrastructure to tasty-golden based
testsuite
- Create test/Succeed/ and test/Fail/ directory structure
- Move .agda test files to appropriate directories
- Move golden .hs files next to their .agda files in test/Succeed/
- Move golden .err files next to their .agda files in test/Fail/
- Create test/Main.hs test runner using tasty-golden
- Add test-suite section to agda2hs.cabal
- Add test data files to cabal file
- Remove old AllTests.agda, AllFailTests.agda, AllCubicalTests.agda
- Remove old golden/ directory
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
agda2hs.cabal | 24 ++
test/AllCubicalTests.agda | 7 -
test/AllFailTests.agda | 47 ----
test/AllTests.agda | 212 ------------------
test/{golden => Fail}/ClashingImport.err | 0
test/{golden => Fail}/Copatterns.err | 0
.../{golden => Fail}/DerivingParseFailure.err | 0
.../ErasedRecordParameter.err | 0
test/{golden => Fail}/ExplicitInstance.err | 0
test/{golden => Fail}/ExplicitInstance2.err | 0
test/{golden => Fail}/Fixities.err | 0
test/{golden => Fail}/Inline.err | 0
test/{golden => Fail}/Inline2.err | 0
test/{golden => Fail}/InvalidName.err | 0
test/{golden => Fail}/Issue113a.err | 0
test/{golden => Fail}/Issue113b.err | 0
test/{golden => Fail}/Issue119.err | 0
test/{golden => Fail}/Issue125.err | 0
test/{golden => Fail}/Issue142.err | 0
test/{golden => Fail}/Issue146.err | 0
test/{golden => Fail}/Issue150.err | 0
test/{golden => Fail}/Issue154.err | 0
test/{golden => Fail}/Issue169-record.err | 0
test/{golden => Fail}/Issue185.err | 0
test/{golden => Fail}/Issue223.err | 0
test/{golden => Fail}/Issue306a.err | 0
test/{golden => Fail}/Issue306b.err | 0
test/{golden => Fail}/Issue306c.err | 0
test/{golden => Fail}/Issue320.err | 0
test/{golden => Fail}/Issue357a.err | 0
test/{golden => Fail}/Issue357b.err | 0
test/{golden => Fail}/Issue437.err | 0
test/{golden => Fail}/Issue71.err | 0
test/{golden => Fail}/MatchOnDelay.err | 0
.../MultiArgumentPatternLambda.err | 0
.../NewTypeRecordTwoFields.err | 0
.../NewTypeTwoConstructors.err | 0
test/{golden => Fail}/NewTypeTwoFields.err | 0
.../NonCanonicalSpecialFunction.err | 0
.../NonCanonicalSuperclass.err | 0
.../{golden => Fail}/NonCopatternInstance.err | 0
.../{golden => Fail}/NonStarDatatypeIndex.err | 0
test/{golden => Fail}/NonStarRecordIndex.err | 0
test/{golden => Fail}/PartialCase.err | 0
test/{golden => Fail}/PartialCaseNoLambda.err | 0
test/{golden => Fail}/PartialIf.err | 0
.../QualifiedRecordProjections.err | 0
test/{golden => Fail}/TypeLambda.err | 0
test/Main.hs | 180 +++++++++++++++
test/{ => Succeed}/Assert.agda | 0
test/{golden => Succeed}/Assert.hs | 0
test/{ => Succeed}/AutoLambdaCaseInBind.agda | 0
.../AutoLambdaCaseInBind.hs | 0
test/{ => Succeed}/AutoLambdaCaseInCase.agda | 0
.../AutoLambdaCaseInCase.hs | 0
test/{ => Succeed}/BangPatterns.agda | 0
test/{golden => Succeed}/BangPatterns.hs | 0
test/{ => Succeed}/CanonicalInstance.agda | 0
test/{golden => Succeed}/CanonicalInstance.hs | 0
test/{ => Succeed}/Coerce.agda | 0
test/{golden => Succeed}/Coerce.hs | 0
test/{ => Succeed}/Coinduction.agda | 0
test/{golden => Succeed}/Coinduction.hs | 0
.../{ => Succeed}/CommonQualifiedImports.agda | 0
.../CommonQualifiedImports.hs | 0
test/{ => Succeed}/CompileTo.agda | 0
test/{golden => Succeed}/CompileTo.hs | 0
test/{ => Succeed}/ConstrainedInstance.agda | 0
.../ConstrainedInstance.hs | 0
.../Cubical}/Cubical/StreamFusion.hs | 0
test/{ => Succeed}/Cubical/StreamFusion.agda | 0
test/Succeed/Cubical/StreamFusion.hs | 7 +
test/{ => Succeed}/CustomTuples.agda | 0
test/{golden => Succeed}/CustomTuples.hs | 0
test/{ => Succeed}/Datatypes.agda | 0
test/{golden => Succeed}/Datatypes.hs | 0
test/{ => Succeed}/Default.agda | 0
test/{golden => Succeed}/Default.hs | 0
test/{ => Succeed}/DefaultMethods.agda | 0
test/{golden => Succeed}/DefaultMethods.hs | 0
test/{ => Succeed}/Delay.agda | 0
test/{golden => Succeed}/Delay.hs | 0
test/{ => Succeed}/Deriving.agda | 0
test/{golden => Succeed}/Deriving.hs | 0
test/{ => Succeed}/DoNotation.agda | 0
test/{golden => Succeed}/DoNotation.hs | 0
test/{ => Succeed}/EraseType.agda | 0
test/{golden => Succeed}/EraseType.hs | 0
.../{ => Succeed}/ErasedLocalDefinitions.agda | 0
.../ErasedLocalDefinitions.hs | 0
test/{ => Succeed}/ErasedPatternLambda.agda | 0
.../ErasedPatternLambda.hs | 0
test/{ => Succeed}/ErasedTypeArguments.agda | 0
.../ErasedTypeArguments.hs | 0
test/{ => Succeed}/Fixities.agda | 0
test/{golden => Succeed}/Fixities.hs | 0
test/{ => Succeed}/FunCon.agda | 0
test/{golden => Succeed}/FunCon.hs | 0
test/{ => Succeed}/HeightMirror.agda | 0
test/{golden => Succeed}/HeightMirror.hs | 0
test/{ => Succeed}/IOFile.agda | 0
test/{golden => Succeed}/IOFile.hs | 0
test/{ => Succeed}/IOInput.agda | 0
test/{golden => Succeed}/IOInput.hs | 0
test/{ => Succeed}/Importee.agda | 0
test/{golden => Succeed}/Importee.hs | 0
test/{ => Succeed}/Importer.agda | 0
test/{golden => Succeed}/Importer.hs | 0
test/{ => Succeed}/Inlining.agda | 0
test/{golden => Succeed}/Inlining.hs | 0
test/{ => Succeed}/Issue107.agda | 0
test/{ => Succeed}/Issue115.agda | 0
test/{golden => Succeed}/Issue115.hs | 0
test/{ => Succeed}/Issue14.agda | 0
test/{golden => Succeed}/Issue14.hs | 0
test/{ => Succeed}/Issue145.agda | 0
test/{golden => Succeed}/Issue145.hs | 0
test/{ => Succeed}/Issue169.agda | 0
test/{golden => Succeed}/Issue169.hs | 0
test/{ => Succeed}/Issue200.agda | 0
test/{golden => Succeed}/Issue200.hs | 0
test/{ => Succeed}/Issue210.agda | 0
test/{golden => Succeed}/Issue210.hs | 0
test/{ => Succeed}/Issue218.agda | 0
test/{golden => Succeed}/Issue218.hs | 0
test/{ => Succeed}/Issue251.agda | 0
test/{golden => Succeed}/Issue251.hs | 0
test/{ => Succeed}/Issue257.agda | 0
test/{ => Succeed}/Issue264.agda | 0
test/{golden => Succeed}/Issue264.hs | 0
test/{ => Succeed}/Issue273.agda | 0
test/{golden => Succeed}/Issue273.hs | 0
test/{ => Succeed}/Issue286.agda | 0
test/{golden => Succeed}/Issue286.hs | 0
test/{ => Succeed}/Issue301.agda | 0
test/{golden => Succeed}/Issue301.hs | 0
test/{ => Succeed}/Issue302.agda | 0
test/{golden => Succeed}/Issue302.hs | 0
test/{ => Succeed}/Issue305.agda | 0
test/{golden => Succeed}/Issue305.hs | 0
test/{ => Succeed}/Issue306.agda | 0
test/{golden => Succeed}/Issue306.hs | 0
test/{ => Succeed}/Issue308.agda | 0
test/{golden => Succeed}/Issue308.hs | 0
test/{ => Succeed}/Issue309.agda | 0
test/{golden => Succeed}/Issue309.hs | 0
test/{ => Succeed}/Issue317.agda | 0
test/{golden => Succeed}/Issue317.hs | 0
test/{ => Succeed}/Issue324.agda | 0
test/{golden => Succeed}/Issue324.hs | 0
test/{ => Succeed}/Issue324instance.agda | 0
test/{golden => Succeed}/Issue324instance.hs | 0
test/{ => Succeed}/Issue346.agda | 0
test/{golden => Succeed}/Issue346.hs | 0
test/{ => Succeed}/Issue353.agda | 0
test/{golden => Succeed}/Issue353.hs | 0
test/{ => Succeed}/Issue377.agda | 0
test/{golden => Succeed}/Issue377.hs | 0
test/{ => Succeed}/Issue394.agda | 0
test/{golden => Succeed}/Issue394.hs | 0
test/{ => Succeed}/Issue408.agda | 0
test/{golden => Succeed}/Issue408.hs | 0
test/{ => Succeed}/Issue409.agda | 0
test/{golden => Succeed}/Issue409.hs | 0
test/{ => Succeed}/Issue421.agda | 0
test/{golden => Succeed}/Issue421.hs | 0
test/{ => Succeed}/Issue65.agda | 0
test/{golden => Succeed}/Issue65.hs | 0
test/{ => Succeed}/Issue69.agda | 0
test/{golden => Succeed}/Issue69.hs | 0
test/{ => Succeed}/Issue73.agda | 0
test/{golden => Succeed}/Issue73.hs | 0
test/{ => Succeed}/Issue90.agda | 0
test/{golden => Succeed}/Issue90.hs | 0
test/{ => Succeed}/Issue92.agda | 0
test/{golden => Succeed}/Issue92.hs | 0
test/{ => Succeed}/Issue93.agda | 0
test/{golden => Succeed}/Issue93.hs | 0
test/{ => Succeed}/Issue94.agda | 0
test/{golden => Succeed}/Issue94.hs | 0
test/{ => Succeed}/Kinds.agda | 0
test/{golden => Succeed}/Kinds.hs | 0
test/{ => Succeed}/LanguageConstructs.agda | 0
.../{golden => Succeed}/LanguageConstructs.hs | 0
test/{ => Succeed}/LawfulOrd.agda | 0
test/{golden => Succeed}/LawfulOrd.hs | 0
test/{ => Succeed}/LiteralPatterns.agda | 0
test/{golden => Succeed}/LiteralPatterns.hs | 0
test/{ => Succeed}/ModuleParameters.agda | 0
test/{golden => Succeed}/ModuleParameters.hs | 0
.../ModuleParametersImports.agda | 0
.../ModuleParametersImports.hs | 0
test/{ => Succeed}/NewTypePragma.agda | 0
test/{golden => Succeed}/NewTypePragma.hs | 0
test/{ => Succeed}/NonClassInstance.agda | 0
test/{golden => Succeed}/NonClassInstance.hs | 0
test/{ => Succeed}/Numbers.agda | 0
test/{golden => Succeed}/Numbers.hs | 0
test/{ => Succeed}/OtherImportee.agda | 0
test/{golden => Succeed}/OtherImportee.hs | 0
test/{ => Succeed}/Pragmas.agda | 0
test/{golden => Succeed}/Pragmas.hs | 0
test/{ => Succeed}/ProjLike.agda | 0
test/{golden => Succeed}/ProjLike.hs | 0
test/{ => Succeed}/ProjectionLike.agda | 0
test/{golden => Succeed}/ProjectionLike.hs | 0
test/{ => Succeed}/QualifiedImportee.agda | 0
test/{golden => Succeed}/QualifiedImportee.hs | 0
test/{ => Succeed}/QualifiedImports.agda | 0
test/{golden => Succeed}/QualifiedImports.hs | 0
test/{ => Succeed}/QualifiedModule.agda | 0
test/{golden => Succeed}/QualifiedModule.hs | 0
test/{ => Succeed}/QualifiedPrelude.agda | 0
test/{golden => Succeed}/QualifiedPrelude.hs | 0
test/{ => Succeed}/RankNTypes.agda | 0
test/{golden => Succeed}/RankNTypes.hs | 0
test/{ => Succeed}/Records.agda | 0
test/{golden => Succeed}/Records.hs | 0
test/{ => Succeed}/RelevantDotPattern1.agda | 0
.../RelevantDotPattern1.hs | 0
test/{ => Succeed}/RelevantDotPattern2.agda | 0
.../RelevantDotPattern2.hs | 0
test/{ => Succeed}/RelevantDotPattern3.agda | 0
.../RelevantDotPattern3.hs | 0
test/{ => Succeed}/RequalifiedImports.agda | 0
.../{golden => Succeed}/RequalifiedImports.hs | 0
test/{ => Succeed}/RuntimeCast.agda | 0
test/{golden => Succeed}/RuntimeCast.hs | 0
test/{ => Succeed}/ScopedTypeVariables.agda | 0
.../ScopedTypeVariables.hs | 0
test/{ => Succeed}/SecondImportee.agda | 0
test/{golden => Succeed}/SecondImportee.hs | 0
test/{ => Succeed}/Sections.agda | 0
test/{golden => Succeed}/Sections.hs | 0
test/{ => Succeed}/Superclass.agda | 0
test/{golden => Succeed}/Superclass.hs | 0
test/{ => Succeed}/Test.agda | 0
test/{golden => Succeed}/Test.hs | 0
test/{ => Succeed}/TransparentFun.agda | 0
test/{golden => Succeed}/TransparentFun.hs | 0
test/{ => Succeed}/Tree.agda | 0
test/{golden => Succeed}/Tree.hs | 0
test/{ => Succeed}/Tuples.agda | 0
test/{golden => Succeed}/Tuples.hs | 0
test/{ => Succeed}/TypeBasedUnboxing.agda | 0
test/{golden => Succeed}/TypeBasedUnboxing.hs | 0
test/{ => Succeed}/TypeDirected.agda | 0
test/{golden => Succeed}/TypeDirected.hs | 0
test/{ => Succeed}/TypeOperatorExport.agda | 0
.../{golden => Succeed}/TypeOperatorExport.hs | 0
test/{ => Succeed}/TypeOperatorImport.agda | 0
.../{golden => Succeed}/TypeOperatorImport.hs | 0
test/{ => Succeed}/TypeOperators.agda | 0
test/{golden => Succeed}/TypeOperators.hs | 0
test/{ => Succeed}/TypeSignature.agda | 0
test/{golden => Succeed}/TypeSignature.hs | 0
test/{ => Succeed}/TypeSynonyms.agda | 0
test/{golden => Succeed}/TypeSynonyms.hs | 0
test/{ => Succeed}/UnboxPragma.agda | 0
test/{golden => Succeed}/UnboxPragma.hs | 0
test/{ => Succeed}/Vector.agda | 0
test/{golden => Succeed}/Vector.hs | 0
test/{ => Succeed}/Where.agda | 0
test/{golden => Succeed}/Where.hs | 0
test/{ => Succeed}/WitnessedFlows.agda | 0
test/{golden => Succeed}/WitnessedFlows.hs | 0
test/agda2hs-test.agda-lib | 2 +-
test/golden/AllCubicalTests.hs | 4 -
test/golden/AllTests.hs | 104 ---------
269 files changed, 212 insertions(+), 375 deletions(-)
delete mode 100644 test/AllCubicalTests.agda
delete mode 100644 test/AllFailTests.agda
delete mode 100644 test/AllTests.agda
rename test/{golden => Fail}/ClashingImport.err (100%)
rename test/{golden => Fail}/Copatterns.err (100%)
rename test/{golden => Fail}/DerivingParseFailure.err (100%)
rename test/{golden => Fail}/ErasedRecordParameter.err (100%)
rename test/{golden => Fail}/ExplicitInstance.err (100%)
rename test/{golden => Fail}/ExplicitInstance2.err (100%)
rename test/{golden => Fail}/Fixities.err (100%)
rename test/{golden => Fail}/Inline.err (100%)
rename test/{golden => Fail}/Inline2.err (100%)
rename test/{golden => Fail}/InvalidName.err (100%)
rename test/{golden => Fail}/Issue113a.err (100%)
rename test/{golden => Fail}/Issue113b.err (100%)
rename test/{golden => Fail}/Issue119.err (100%)
rename test/{golden => Fail}/Issue125.err (100%)
rename test/{golden => Fail}/Issue142.err (100%)
rename test/{golden => Fail}/Issue146.err (100%)
rename test/{golden => Fail}/Issue150.err (100%)
rename test/{golden => Fail}/Issue154.err (100%)
rename test/{golden => Fail}/Issue169-record.err (100%)
rename test/{golden => Fail}/Issue185.err (100%)
rename test/{golden => Fail}/Issue223.err (100%)
rename test/{golden => Fail}/Issue306a.err (100%)
rename test/{golden => Fail}/Issue306b.err (100%)
rename test/{golden => Fail}/Issue306c.err (100%)
rename test/{golden => Fail}/Issue320.err (100%)
rename test/{golden => Fail}/Issue357a.err (100%)
rename test/{golden => Fail}/Issue357b.err (100%)
rename test/{golden => Fail}/Issue437.err (100%)
rename test/{golden => Fail}/Issue71.err (100%)
rename test/{golden => Fail}/MatchOnDelay.err (100%)
rename test/{golden => Fail}/MultiArgumentPatternLambda.err (100%)
rename test/{golden => Fail}/NewTypeRecordTwoFields.err (100%)
rename test/{golden => Fail}/NewTypeTwoConstructors.err (100%)
rename test/{golden => Fail}/NewTypeTwoFields.err (100%)
rename test/{golden => Fail}/NonCanonicalSpecialFunction.err (100%)
rename test/{golden => Fail}/NonCanonicalSuperclass.err (100%)
rename test/{golden => Fail}/NonCopatternInstance.err (100%)
rename test/{golden => Fail}/NonStarDatatypeIndex.err (100%)
rename test/{golden => Fail}/NonStarRecordIndex.err (100%)
rename test/{golden => Fail}/PartialCase.err (100%)
rename test/{golden => Fail}/PartialCaseNoLambda.err (100%)
rename test/{golden => Fail}/PartialIf.err (100%)
rename test/{golden => Fail}/QualifiedRecordProjections.err (100%)
rename test/{golden => Fail}/TypeLambda.err (100%)
create mode 100644 test/Main.hs
rename test/{ => Succeed}/Assert.agda (100%)
rename test/{golden => Succeed}/Assert.hs (100%)
rename test/{ => Succeed}/AutoLambdaCaseInBind.agda (100%)
rename test/{golden => Succeed}/AutoLambdaCaseInBind.hs (100%)
rename test/{ => Succeed}/AutoLambdaCaseInCase.agda (100%)
rename test/{golden => Succeed}/AutoLambdaCaseInCase.hs (100%)
rename test/{ => Succeed}/BangPatterns.agda (100%)
rename test/{golden => Succeed}/BangPatterns.hs (100%)
rename test/{ => Succeed}/CanonicalInstance.agda (100%)
rename test/{golden => Succeed}/CanonicalInstance.hs (100%)
rename test/{ => Succeed}/Coerce.agda (100%)
rename test/{golden => Succeed}/Coerce.hs (100%)
rename test/{ => Succeed}/Coinduction.agda (100%)
rename test/{golden => Succeed}/Coinduction.hs (100%)
rename test/{ => Succeed}/CommonQualifiedImports.agda (100%)
rename test/{golden => Succeed}/CommonQualifiedImports.hs (100%)
rename test/{ => Succeed}/CompileTo.agda (100%)
rename test/{golden => Succeed}/CompileTo.hs (100%)
rename test/{ => Succeed}/ConstrainedInstance.agda (100%)
rename test/{golden => Succeed}/ConstrainedInstance.hs (100%)
rename test/{golden => Succeed/Cubical}/Cubical/StreamFusion.hs (100%)
rename test/{ => Succeed}/Cubical/StreamFusion.agda (100%)
create mode 100644 test/Succeed/Cubical/StreamFusion.hs
rename test/{ => Succeed}/CustomTuples.agda (100%)
rename test/{golden => Succeed}/CustomTuples.hs (100%)
rename test/{ => Succeed}/Datatypes.agda (100%)
rename test/{golden => Succeed}/Datatypes.hs (100%)
rename test/{ => Succeed}/Default.agda (100%)
rename test/{golden => Succeed}/Default.hs (100%)
rename test/{ => Succeed}/DefaultMethods.agda (100%)
rename test/{golden => Succeed}/DefaultMethods.hs (100%)
rename test/{ => Succeed}/Delay.agda (100%)
rename test/{golden => Succeed}/Delay.hs (100%)
rename test/{ => Succeed}/Deriving.agda (100%)
rename test/{golden => Succeed}/Deriving.hs (100%)
rename test/{ => Succeed}/DoNotation.agda (100%)
rename test/{golden => Succeed}/DoNotation.hs (100%)
rename test/{ => Succeed}/EraseType.agda (100%)
rename test/{golden => Succeed}/EraseType.hs (100%)
rename test/{ => Succeed}/ErasedLocalDefinitions.agda (100%)
rename test/{golden => Succeed}/ErasedLocalDefinitions.hs (100%)
rename test/{ => Succeed}/ErasedPatternLambda.agda (100%)
rename test/{golden => Succeed}/ErasedPatternLambda.hs (100%)
rename test/{ => Succeed}/ErasedTypeArguments.agda (100%)
rename test/{golden => Succeed}/ErasedTypeArguments.hs (100%)
rename test/{ => Succeed}/Fixities.agda (100%)
rename test/{golden => Succeed}/Fixities.hs (100%)
rename test/{ => Succeed}/FunCon.agda (100%)
rename test/{golden => Succeed}/FunCon.hs (100%)
rename test/{ => Succeed}/HeightMirror.agda (100%)
rename test/{golden => Succeed}/HeightMirror.hs (100%)
rename test/{ => Succeed}/IOFile.agda (100%)
rename test/{golden => Succeed}/IOFile.hs (100%)
rename test/{ => Succeed}/IOInput.agda (100%)
rename test/{golden => Succeed}/IOInput.hs (100%)
rename test/{ => Succeed}/Importee.agda (100%)
rename test/{golden => Succeed}/Importee.hs (100%)
rename test/{ => Succeed}/Importer.agda (100%)
rename test/{golden => Succeed}/Importer.hs (100%)
rename test/{ => Succeed}/Inlining.agda (100%)
rename test/{golden => Succeed}/Inlining.hs (100%)
rename test/{ => Succeed}/Issue107.agda (100%)
rename test/{ => Succeed}/Issue115.agda (100%)
rename test/{golden => Succeed}/Issue115.hs (100%)
rename test/{ => Succeed}/Issue14.agda (100%)
rename test/{golden => Succeed}/Issue14.hs (100%)
rename test/{ => Succeed}/Issue145.agda (100%)
rename test/{golden => Succeed}/Issue145.hs (100%)
rename test/{ => Succeed}/Issue169.agda (100%)
rename test/{golden => Succeed}/Issue169.hs (100%)
rename test/{ => Succeed}/Issue200.agda (100%)
rename test/{golden => Succeed}/Issue200.hs (100%)
rename test/{ => Succeed}/Issue210.agda (100%)
rename test/{golden => Succeed}/Issue210.hs (100%)
rename test/{ => Succeed}/Issue218.agda (100%)
rename test/{golden => Succeed}/Issue218.hs (100%)
rename test/{ => Succeed}/Issue251.agda (100%)
rename test/{golden => Succeed}/Issue251.hs (100%)
rename test/{ => Succeed}/Issue257.agda (100%)
rename test/{ => Succeed}/Issue264.agda (100%)
rename test/{golden => Succeed}/Issue264.hs (100%)
rename test/{ => Succeed}/Issue273.agda (100%)
rename test/{golden => Succeed}/Issue273.hs (100%)
rename test/{ => Succeed}/Issue286.agda (100%)
rename test/{golden => Succeed}/Issue286.hs (100%)
rename test/{ => Succeed}/Issue301.agda (100%)
rename test/{golden => Succeed}/Issue301.hs (100%)
rename test/{ => Succeed}/Issue302.agda (100%)
rename test/{golden => Succeed}/Issue302.hs (100%)
rename test/{ => Succeed}/Issue305.agda (100%)
rename test/{golden => Succeed}/Issue305.hs (100%)
rename test/{ => Succeed}/Issue306.agda (100%)
rename test/{golden => Succeed}/Issue306.hs (100%)
rename test/{ => Succeed}/Issue308.agda (100%)
rename test/{golden => Succeed}/Issue308.hs (100%)
rename test/{ => Succeed}/Issue309.agda (100%)
rename test/{golden => Succeed}/Issue309.hs (100%)
rename test/{ => Succeed}/Issue317.agda (100%)
rename test/{golden => Succeed}/Issue317.hs (100%)
rename test/{ => Succeed}/Issue324.agda (100%)
rename test/{golden => Succeed}/Issue324.hs (100%)
rename test/{ => Succeed}/Issue324instance.agda (100%)
rename test/{golden => Succeed}/Issue324instance.hs (100%)
rename test/{ => Succeed}/Issue346.agda (100%)
rename test/{golden => Succeed}/Issue346.hs (100%)
rename test/{ => Succeed}/Issue353.agda (100%)
rename test/{golden => Succeed}/Issue353.hs (100%)
rename test/{ => Succeed}/Issue377.agda (100%)
rename test/{golden => Succeed}/Issue377.hs (100%)
rename test/{ => Succeed}/Issue394.agda (100%)
rename test/{golden => Succeed}/Issue394.hs (100%)
rename test/{ => Succeed}/Issue408.agda (100%)
rename test/{golden => Succeed}/Issue408.hs (100%)
rename test/{ => Succeed}/Issue409.agda (100%)
rename test/{golden => Succeed}/Issue409.hs (100%)
rename test/{ => Succeed}/Issue421.agda (100%)
rename test/{golden => Succeed}/Issue421.hs (100%)
rename test/{ => Succeed}/Issue65.agda (100%)
rename test/{golden => Succeed}/Issue65.hs (100%)
rename test/{ => Succeed}/Issue69.agda (100%)
rename test/{golden => Succeed}/Issue69.hs (100%)
rename test/{ => Succeed}/Issue73.agda (100%)
rename test/{golden => Succeed}/Issue73.hs (100%)
rename test/{ => Succeed}/Issue90.agda (100%)
rename test/{golden => Succeed}/Issue90.hs (100%)
rename test/{ => Succeed}/Issue92.agda (100%)
rename test/{golden => Succeed}/Issue92.hs (100%)
rename test/{ => Succeed}/Issue93.agda (100%)
rename test/{golden => Succeed}/Issue93.hs (100%)
rename test/{ => Succeed}/Issue94.agda (100%)
rename test/{golden => Succeed}/Issue94.hs (100%)
rename test/{ => Succeed}/Kinds.agda (100%)
rename test/{golden => Succeed}/Kinds.hs (100%)
rename test/{ => Succeed}/LanguageConstructs.agda (100%)
rename test/{golden => Succeed}/LanguageConstructs.hs (100%)
rename test/{ => Succeed}/LawfulOrd.agda (100%)
rename test/{golden => Succeed}/LawfulOrd.hs (100%)
rename test/{ => Succeed}/LiteralPatterns.agda (100%)
rename test/{golden => Succeed}/LiteralPatterns.hs (100%)
rename test/{ => Succeed}/ModuleParameters.agda (100%)
rename test/{golden => Succeed}/ModuleParameters.hs (100%)
rename test/{ => Succeed}/ModuleParametersImports.agda (100%)
rename test/{golden => Succeed}/ModuleParametersImports.hs (100%)
rename test/{ => Succeed}/NewTypePragma.agda (100%)
rename test/{golden => Succeed}/NewTypePragma.hs (100%)
rename test/{ => Succeed}/NonClassInstance.agda (100%)
rename test/{golden => Succeed}/NonClassInstance.hs (100%)
rename test/{ => Succeed}/Numbers.agda (100%)
rename test/{golden => Succeed}/Numbers.hs (100%)
rename test/{ => Succeed}/OtherImportee.agda (100%)
rename test/{golden => Succeed}/OtherImportee.hs (100%)
rename test/{ => Succeed}/Pragmas.agda (100%)
rename test/{golden => Succeed}/Pragmas.hs (100%)
rename test/{ => Succeed}/ProjLike.agda (100%)
rename test/{golden => Succeed}/ProjLike.hs (100%)
rename test/{ => Succeed}/ProjectionLike.agda (100%)
rename test/{golden => Succeed}/ProjectionLike.hs (100%)
rename test/{ => Succeed}/QualifiedImportee.agda (100%)
rename test/{golden => Succeed}/QualifiedImportee.hs (100%)
rename test/{ => Succeed}/QualifiedImports.agda (100%)
rename test/{golden => Succeed}/QualifiedImports.hs (100%)
rename test/{ => Succeed}/QualifiedModule.agda (100%)
rename test/{golden => Succeed}/QualifiedModule.hs (100%)
rename test/{ => Succeed}/QualifiedPrelude.agda (100%)
rename test/{golden => Succeed}/QualifiedPrelude.hs (100%)
rename test/{ => Succeed}/RankNTypes.agda (100%)
rename test/{golden => Succeed}/RankNTypes.hs (100%)
rename test/{ => Succeed}/Records.agda (100%)
rename test/{golden => Succeed}/Records.hs (100%)
rename test/{ => Succeed}/RelevantDotPattern1.agda (100%)
rename test/{golden => Succeed}/RelevantDotPattern1.hs (100%)
rename test/{ => Succeed}/RelevantDotPattern2.agda (100%)
rename test/{golden => Succeed}/RelevantDotPattern2.hs (100%)
rename test/{ => Succeed}/RelevantDotPattern3.agda (100%)
rename test/{golden => Succeed}/RelevantDotPattern3.hs (100%)
rename test/{ => Succeed}/RequalifiedImports.agda (100%)
rename test/{golden => Succeed}/RequalifiedImports.hs (100%)
rename test/{ => Succeed}/RuntimeCast.agda (100%)
rename test/{golden => Succeed}/RuntimeCast.hs (100%)
rename test/{ => Succeed}/ScopedTypeVariables.agda (100%)
rename test/{golden => Succeed}/ScopedTypeVariables.hs (100%)
rename test/{ => Succeed}/SecondImportee.agda (100%)
rename test/{golden => Succeed}/SecondImportee.hs (100%)
rename test/{ => Succeed}/Sections.agda (100%)
rename test/{golden => Succeed}/Sections.hs (100%)
rename test/{ => Succeed}/Superclass.agda (100%)
rename test/{golden => Succeed}/Superclass.hs (100%)
rename test/{ => Succeed}/Test.agda (100%)
rename test/{golden => Succeed}/Test.hs (100%)
rename test/{ => Succeed}/TransparentFun.agda (100%)
rename test/{golden => Succeed}/TransparentFun.hs (100%)
rename test/{ => Succeed}/Tree.agda (100%)
rename test/{golden => Succeed}/Tree.hs (100%)
rename test/{ => Succeed}/Tuples.agda (100%)
rename test/{golden => Succeed}/Tuples.hs (100%)
rename test/{ => Succeed}/TypeBasedUnboxing.agda (100%)
rename test/{golden => Succeed}/TypeBasedUnboxing.hs (100%)
rename test/{ => Succeed}/TypeDirected.agda (100%)
rename test/{golden => Succeed}/TypeDirected.hs (100%)
rename test/{ => Succeed}/TypeOperatorExport.agda (100%)
rename test/{golden => Succeed}/TypeOperatorExport.hs (100%)
rename test/{ => Succeed}/TypeOperatorImport.agda (100%)
rename test/{golden => Succeed}/TypeOperatorImport.hs (100%)
rename test/{ => Succeed}/TypeOperators.agda (100%)
rename test/{golden => Succeed}/TypeOperators.hs (100%)
rename test/{ => Succeed}/TypeSignature.agda (100%)
rename test/{golden => Succeed}/TypeSignature.hs (100%)
rename test/{ => Succeed}/TypeSynonyms.agda (100%)
rename test/{golden => Succeed}/TypeSynonyms.hs (100%)
rename test/{ => Succeed}/UnboxPragma.agda (100%)
rename test/{golden => Succeed}/UnboxPragma.hs (100%)
rename test/{ => Succeed}/Vector.agda (100%)
rename test/{golden => Succeed}/Vector.hs (100%)
rename test/{ => Succeed}/Where.agda (100%)
rename test/{golden => Succeed}/Where.hs (100%)
rename test/{ => Succeed}/WitnessedFlows.agda (100%)
rename test/{golden => Succeed}/WitnessedFlows.hs (100%)
delete mode 100644 test/golden/AllCubicalTests.hs
delete mode 100644 test/golden/AllTests.hs
diff --git a/agda2hs.cabal b/agda2hs.cabal
index d16228a5..7f057ed5 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -21,6 +21,14 @@ extra-doc-files: CHANGELOG.md
data-files:
lib/base/base.agda-lib
lib/base/**/*.agda
+ test/agda2hs-test.agda-lib
+ test/Haskell/**/*.agda
+ test/Succeed/*.agda
+ test/Succeed/*.hs
+ test/Succeed/**/*.agda
+ test/Succeed/**/*.hs
+ test/Fail/*.agda
+ test/Fail/*.err
source-repository head
type: git
@@ -83,3 +91,19 @@ executable agda2hs
NondecreasingIndentation
OverloadedStrings
ghc-options: -Werror -rtsopts
+
+test-suite agda2hs-test
+ type: exitcode-stdio-1.0
+ hs-source-dirs: test
+ main-is: Main.hs
+ build-depends: base >= 4.13 && < 4.22,
+ bytestring >= 0.11.5 && < 0.13,
+ directory >= 1.2.6.2 && < 1.4,
+ filepath >= 1.4.1.0 && < 1.6,
+ process >= 1.6 && < 1.7,
+ tasty >= 1.4 && < 1.6,
+ tasty-golden >= 2.3 && < 2.4,
+ default-language: Haskell2010
+ default-extensions: OverloadedStrings
+ build-tool-depends: agda2hs:agda2hs
+ ghc-options: -threaded
diff --git a/test/AllCubicalTests.agda b/test/AllCubicalTests.agda
deleted file mode 100644
index e0fdf48b..00000000
--- a/test/AllCubicalTests.agda
+++ /dev/null
@@ -1,7 +0,0 @@
-module AllCubicalTests where
-
-import Cubical.StreamFusion
-
-{-# FOREIGN AGDA2HS
-import Cubical.StreamFusion
-#-}
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
deleted file mode 100644
index 638b1706..00000000
--- a/test/AllFailTests.agda
+++ /dev/null
@@ -1,47 +0,0 @@
-{-# OPTIONS --guardedness #-}
-module AllFailTests where
-
-import Fail.ClashingImport
-import Fail.Issue142
-import Fail.MatchOnDelay
-import Fail.NewTypeRecordTwoFields
-import Fail.Issue150
-import Fail.NonCopatternInstance
-import Fail.Issue113a
-import Fail.Issue119
-import Fail.NonStarRecordIndex
-import Fail.ErasedRecordParameter
-import Fail.Issue146
-import Fail.PartialCase
-import Fail.Issue169-record
-import Fail.Issue113b
-import Fail.Fixities
-import Fail.PartialIf
-import Fail.Inline2
-import Fail.Issue71
-import Fail.Issue223
-import Fail.NewTypeTwoConstructors
-import Fail.MultiArgumentPatternLambda
-import Fail.Inline
-import Fail.ExplicitInstance2
-import Fail.QualifiedRecordProjections
-import Fail.NewTypeTwoFields
-import Fail.InvalidName
-import Fail.Issue185
-import Fail.ExplicitInstance
-import Fail.ClashingImport
-import Fail.Copatterns
-import Fail.Issue154
-import Fail.PartialCaseNoLambda
-import Fail.NonStarDatatypeIndex
-import Fail.NonCanonicalSpecialFunction
-import Fail.TypeLambda
-import Fail.NonCanonicalSuperclass
-import Fail.Issue125
-import Fail.Issue357a
-import Fail.Issue357b
-import Fail.Issue437
-import Fail.DerivingParseFailure
-import Fail.Issue306a
-import Fail.Issue306b
-import Fail.Issue306c
diff --git a/test/AllTests.agda b/test/AllTests.agda
deleted file mode 100644
index bc786d2b..00000000
--- a/test/AllTests.agda
+++ /dev/null
@@ -1,212 +0,0 @@
-{-# OPTIONS --prop #-}
-module AllTests where
-
-import AllCubicalTests
-
-import Issue14
-import Issue65
-import Issue69
-import Issue73
-import Fixities
-import LanguageConstructs
-import Numbers
-import Pragmas
-import Sections
-import Test
-import Tree
-import Tuples
-import Where
-import TypeSynonyms
-import CanonicalInstance
-import Coinduction
-import ConstrainedInstance
-import Datatypes
-import Records
-import Default
-import DefaultMethods
-import Vector
-import Issue90
-import Issue93
-import QualifiedModule
-import Superclass
-import UnboxPragma
-import ScopedTypeVariables
-import LiteralPatterns
-import Issue92
-import HeightMirror
-import TransparentFun
-import Issue115
-import BangPatterns
-import Issue94
-import Issue107
-import DoNotation
-import NewTypePragma
-import Importer
-import QualifiedImports
-import CommonQualifiedImports
-import RequalifiedImports
-import QualifiedPrelude
-import AutoLambdaCaseInCase
-import AutoLambdaCaseInBind
-import WitnessedFlows
-import Kinds
-import LawfulOrd
-import Deriving
-import ErasedLocalDefinitions
-import TypeOperators
-import ErasedTypeArguments
-import TypeOperatorExport
-import TypeOperatorImport
-import IOFile
-import IOInput
-import Issue200
-import Issue169
-import Issue210
-import TypeSignature
-import ModuleParameters
-import ModuleParametersImports
-import Coerce
-import Inlining
-import EraseType
-import Issue257
-import Delay
-import Issue273
-import TypeDirected
-import ProjLike
-import Issue286
-import NonClassInstance
-import Issue218
-import Issue251
-import TypeBasedUnboxing
-import Issue145
-import Issue264
-import Issue301
-import Issue305
-import Issue302
-import Issue309
-import Issue317
-import Issue353
-import RankNTypes
-import ErasedPatternLambda
-import CustomTuples
-import ProjectionLike
-import FunCon
-import Issue308
-import Issue324
-import Assert
-import Issue377
-import Issue394
-import Issue421
-import Issue409
-import Issue346
-import Issue408
-import CompileTo
-import RuntimeCast
-import Issue306
-import RelevantDotPattern1
-import RelevantDotPattern2
-import RelevantDotPattern3
-
-{-# FOREIGN AGDA2HS
-import Issue14
-import Issue65
-import Issue69
-import Issue73
-import Fixities
-import LanguageConstructs
-import Numbers
-import Pragmas
-import Sections
-import Test
-import Tree
-import Tuples
-import Where
-import TypeSynonyms
-import CanonicalInstance
-import Coinduction
-import ConstrainedInstance
-import Datatypes
-import Records
-import Default
-import DefaultMethods
-import Vector
-import Issue90
-import Issue93
-import QualifiedModule
-import Superclass
-import UnboxPragma
-import ScopedTypeVariables
-import LiteralPatterns
-import Issue92
-import HeightMirror
-import TransparentFun
-import Issue115
-import BangPatterns
-import Issue94
-import DoNotation
-import NewTypePragma
-import Importer
-import QualifiedImports
-import CommonQualifiedImports
-import RequalifiedImports
-import QualifiedPrelude
-import AutoLambdaCaseInCase
-import AutoLambdaCaseInBind
-import WitnessedFlows
-import Kinds
-import LawfulOrd
-import Deriving
-import ErasedLocalDefinitions
-import TypeOperators
-import ErasedTypeArguments
-import TypeOperatorExport
-import TypeOperatorImport
-import IOFile
-import IOInput
-import Issue200
-import Issue169
-import Issue210
-import TypeSignature
-import ModuleParameters
-import ModuleParametersImports
-import Coerce
-import Inlining
-import EraseType
-import Delay
-import Issue273
-import TypeDirected
-import ProjLike
-import Issue286
-import NonClassInstance
-import Issue218
-import Issue251
-import TypeBasedUnboxing
-import Issue145
-import Issue264
-import Issue301
-import Issue305
-import Issue302
-import Issue309
-import Issue317
-import Issue353
-import RankNTypes
-import ErasedPatternLambda
-import CustomTuples
-import ProjectionLike
-import FunCon
-import Issue308
-import Issue324
-import Assert
-import Issue377
-import Issue394
-import Issue421
-import Issue409
-import Issue346
-import Issue408
-import CompileTo
-import RuntimeCast
-import Issue306
-import RelevantDotPattern1
-import RelevantDotPattern2
-import RelevantDotPattern3
-#-}
diff --git a/test/golden/ClashingImport.err b/test/Fail/ClashingImport.err
similarity index 100%
rename from test/golden/ClashingImport.err
rename to test/Fail/ClashingImport.err
diff --git a/test/golden/Copatterns.err b/test/Fail/Copatterns.err
similarity index 100%
rename from test/golden/Copatterns.err
rename to test/Fail/Copatterns.err
diff --git a/test/golden/DerivingParseFailure.err b/test/Fail/DerivingParseFailure.err
similarity index 100%
rename from test/golden/DerivingParseFailure.err
rename to test/Fail/DerivingParseFailure.err
diff --git a/test/golden/ErasedRecordParameter.err b/test/Fail/ErasedRecordParameter.err
similarity index 100%
rename from test/golden/ErasedRecordParameter.err
rename to test/Fail/ErasedRecordParameter.err
diff --git a/test/golden/ExplicitInstance.err b/test/Fail/ExplicitInstance.err
similarity index 100%
rename from test/golden/ExplicitInstance.err
rename to test/Fail/ExplicitInstance.err
diff --git a/test/golden/ExplicitInstance2.err b/test/Fail/ExplicitInstance2.err
similarity index 100%
rename from test/golden/ExplicitInstance2.err
rename to test/Fail/ExplicitInstance2.err
diff --git a/test/golden/Fixities.err b/test/Fail/Fixities.err
similarity index 100%
rename from test/golden/Fixities.err
rename to test/Fail/Fixities.err
diff --git a/test/golden/Inline.err b/test/Fail/Inline.err
similarity index 100%
rename from test/golden/Inline.err
rename to test/Fail/Inline.err
diff --git a/test/golden/Inline2.err b/test/Fail/Inline2.err
similarity index 100%
rename from test/golden/Inline2.err
rename to test/Fail/Inline2.err
diff --git a/test/golden/InvalidName.err b/test/Fail/InvalidName.err
similarity index 100%
rename from test/golden/InvalidName.err
rename to test/Fail/InvalidName.err
diff --git a/test/golden/Issue113a.err b/test/Fail/Issue113a.err
similarity index 100%
rename from test/golden/Issue113a.err
rename to test/Fail/Issue113a.err
diff --git a/test/golden/Issue113b.err b/test/Fail/Issue113b.err
similarity index 100%
rename from test/golden/Issue113b.err
rename to test/Fail/Issue113b.err
diff --git a/test/golden/Issue119.err b/test/Fail/Issue119.err
similarity index 100%
rename from test/golden/Issue119.err
rename to test/Fail/Issue119.err
diff --git a/test/golden/Issue125.err b/test/Fail/Issue125.err
similarity index 100%
rename from test/golden/Issue125.err
rename to test/Fail/Issue125.err
diff --git a/test/golden/Issue142.err b/test/Fail/Issue142.err
similarity index 100%
rename from test/golden/Issue142.err
rename to test/Fail/Issue142.err
diff --git a/test/golden/Issue146.err b/test/Fail/Issue146.err
similarity index 100%
rename from test/golden/Issue146.err
rename to test/Fail/Issue146.err
diff --git a/test/golden/Issue150.err b/test/Fail/Issue150.err
similarity index 100%
rename from test/golden/Issue150.err
rename to test/Fail/Issue150.err
diff --git a/test/golden/Issue154.err b/test/Fail/Issue154.err
similarity index 100%
rename from test/golden/Issue154.err
rename to test/Fail/Issue154.err
diff --git a/test/golden/Issue169-record.err b/test/Fail/Issue169-record.err
similarity index 100%
rename from test/golden/Issue169-record.err
rename to test/Fail/Issue169-record.err
diff --git a/test/golden/Issue185.err b/test/Fail/Issue185.err
similarity index 100%
rename from test/golden/Issue185.err
rename to test/Fail/Issue185.err
diff --git a/test/golden/Issue223.err b/test/Fail/Issue223.err
similarity index 100%
rename from test/golden/Issue223.err
rename to test/Fail/Issue223.err
diff --git a/test/golden/Issue306a.err b/test/Fail/Issue306a.err
similarity index 100%
rename from test/golden/Issue306a.err
rename to test/Fail/Issue306a.err
diff --git a/test/golden/Issue306b.err b/test/Fail/Issue306b.err
similarity index 100%
rename from test/golden/Issue306b.err
rename to test/Fail/Issue306b.err
diff --git a/test/golden/Issue306c.err b/test/Fail/Issue306c.err
similarity index 100%
rename from test/golden/Issue306c.err
rename to test/Fail/Issue306c.err
diff --git a/test/golden/Issue320.err b/test/Fail/Issue320.err
similarity index 100%
rename from test/golden/Issue320.err
rename to test/Fail/Issue320.err
diff --git a/test/golden/Issue357a.err b/test/Fail/Issue357a.err
similarity index 100%
rename from test/golden/Issue357a.err
rename to test/Fail/Issue357a.err
diff --git a/test/golden/Issue357b.err b/test/Fail/Issue357b.err
similarity index 100%
rename from test/golden/Issue357b.err
rename to test/Fail/Issue357b.err
diff --git a/test/golden/Issue437.err b/test/Fail/Issue437.err
similarity index 100%
rename from test/golden/Issue437.err
rename to test/Fail/Issue437.err
diff --git a/test/golden/Issue71.err b/test/Fail/Issue71.err
similarity index 100%
rename from test/golden/Issue71.err
rename to test/Fail/Issue71.err
diff --git a/test/golden/MatchOnDelay.err b/test/Fail/MatchOnDelay.err
similarity index 100%
rename from test/golden/MatchOnDelay.err
rename to test/Fail/MatchOnDelay.err
diff --git a/test/golden/MultiArgumentPatternLambda.err b/test/Fail/MultiArgumentPatternLambda.err
similarity index 100%
rename from test/golden/MultiArgumentPatternLambda.err
rename to test/Fail/MultiArgumentPatternLambda.err
diff --git a/test/golden/NewTypeRecordTwoFields.err b/test/Fail/NewTypeRecordTwoFields.err
similarity index 100%
rename from test/golden/NewTypeRecordTwoFields.err
rename to test/Fail/NewTypeRecordTwoFields.err
diff --git a/test/golden/NewTypeTwoConstructors.err b/test/Fail/NewTypeTwoConstructors.err
similarity index 100%
rename from test/golden/NewTypeTwoConstructors.err
rename to test/Fail/NewTypeTwoConstructors.err
diff --git a/test/golden/NewTypeTwoFields.err b/test/Fail/NewTypeTwoFields.err
similarity index 100%
rename from test/golden/NewTypeTwoFields.err
rename to test/Fail/NewTypeTwoFields.err
diff --git a/test/golden/NonCanonicalSpecialFunction.err b/test/Fail/NonCanonicalSpecialFunction.err
similarity index 100%
rename from test/golden/NonCanonicalSpecialFunction.err
rename to test/Fail/NonCanonicalSpecialFunction.err
diff --git a/test/golden/NonCanonicalSuperclass.err b/test/Fail/NonCanonicalSuperclass.err
similarity index 100%
rename from test/golden/NonCanonicalSuperclass.err
rename to test/Fail/NonCanonicalSuperclass.err
diff --git a/test/golden/NonCopatternInstance.err b/test/Fail/NonCopatternInstance.err
similarity index 100%
rename from test/golden/NonCopatternInstance.err
rename to test/Fail/NonCopatternInstance.err
diff --git a/test/golden/NonStarDatatypeIndex.err b/test/Fail/NonStarDatatypeIndex.err
similarity index 100%
rename from test/golden/NonStarDatatypeIndex.err
rename to test/Fail/NonStarDatatypeIndex.err
diff --git a/test/golden/NonStarRecordIndex.err b/test/Fail/NonStarRecordIndex.err
similarity index 100%
rename from test/golden/NonStarRecordIndex.err
rename to test/Fail/NonStarRecordIndex.err
diff --git a/test/golden/PartialCase.err b/test/Fail/PartialCase.err
similarity index 100%
rename from test/golden/PartialCase.err
rename to test/Fail/PartialCase.err
diff --git a/test/golden/PartialCaseNoLambda.err b/test/Fail/PartialCaseNoLambda.err
similarity index 100%
rename from test/golden/PartialCaseNoLambda.err
rename to test/Fail/PartialCaseNoLambda.err
diff --git a/test/golden/PartialIf.err b/test/Fail/PartialIf.err
similarity index 100%
rename from test/golden/PartialIf.err
rename to test/Fail/PartialIf.err
diff --git a/test/golden/QualifiedRecordProjections.err b/test/Fail/QualifiedRecordProjections.err
similarity index 100%
rename from test/golden/QualifiedRecordProjections.err
rename to test/Fail/QualifiedRecordProjections.err
diff --git a/test/golden/TypeLambda.err b/test/Fail/TypeLambda.err
similarity index 100%
rename from test/golden/TypeLambda.err
rename to test/Fail/TypeLambda.err
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
index 00000000..f270d114
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+import Control.Exception (catch, SomeException)
+import Control.Monad (forM, unless)
+import qualified Data.ByteString.Lazy as LBS
+import qualified Data.ByteString.Lazy.Char8 as LBS8
+import Data.List (intercalate, isPrefixOf, isSuffixOf, sort)
+import System.Directory
+ ( doesFileExist
+ , getCurrentDirectory
+ , listDirectory
+ , removeFile
+ , setCurrentDirectory
+ )
+import System.Exit (ExitCode(..))
+import System.FilePath ((), dropExtension, makeRelative, takeDirectory, takeFileName)
+import System.Process (readProcessWithExitCode)
+import Test.Tasty (TestTree, defaultMain, testGroup)
+import Test.Tasty.Golden (goldenVsStringDiff)
+
+main :: IO ()
+main = do
+ -- Discover the test directory path (relative to the current working directory)
+ cwd <- getCurrentDirectory
+ let testDir = cwd "test"
+
+ -- Change to the test directory so that agda2hs can find the agda-lib
+ setCurrentDirectory testDir
+
+ -- Discover test cases
+ succeedTests <- discoverSucceedTests testDir
+ failTests <- discoverFailTests testDir
+
+ -- Run tests
+ defaultMain $ testGroup "agda2hs"
+ [ testGroup "Succeed" succeedTests
+ , testGroup "Fail" failTests
+ ]
+
+-- | Discover all .agda files under the Succeed directory recursively.
+discoverSucceedTests :: FilePath -> IO [TestTree]
+discoverSucceedTests testDir = do
+ agdaFiles <- findAgdaFilesRecursive (testDir "Succeed")
+ forM (sort agdaFiles) $ \agdaFile -> do
+ let relPath = makeRelative testDir agdaFile
+ testName = dropExtension (makeRelative (testDir "Succeed") agdaFile)
+ goldenFile = dropExtension agdaFile ++ ".hs"
+ return $ succeedTest testName relPath goldenFile
+
+-- | Discover all .agda files under the Fail directory.
+discoverFailTests :: FilePath -> IO [TestTree]
+discoverFailTests testDir = do
+ agdaFiles <- findAgdaFilesRecursive (testDir "Fail")
+ forM (sort agdaFiles) $ \agdaFile -> do
+ let relPath = makeRelative testDir agdaFile
+ testName = dropExtension (makeRelative (testDir "Fail") agdaFile)
+ goldenFile = dropExtension agdaFile ++ ".err"
+ return $ failTest testName relPath goldenFile
+
+-- | Find all .agda files recursively in a directory.
+findAgdaFilesRecursive :: FilePath -> IO [FilePath]
+findAgdaFilesRecursive dir = do
+ contents <- listDirectory dir
+ paths <- forM contents $ \name -> do
+ let path = dir name
+ isDir <- doesDirectoryExist path
+ if isDir
+ then findAgdaFilesRecursive path
+ else return [path | ".agda" `isSuffixOf` name]
+ return (concat paths)
+
+-- | Check if path is a directory.
+doesDirectoryExist :: FilePath -> IO Bool
+doesDirectoryExist path = do
+ exists <- doesFileExist path
+ if exists
+ then return False
+ else do
+ -- If it's not a file, check if it's a directory
+ contents <- listDirectory path `catch` \(_ :: SomeException) -> return []
+ return (not (null contents) || path `elem` ["Succeed", "Fail", "Cubical"])
+
+-- | Create a test for a succeed case.
+-- Runs agda2hs on the .agda file, compares the output .hs to the golden file,
+-- then compiles the .hs file with ghc.
+succeedTest :: String -> FilePath -> FilePath -> TestTree
+succeedTest testName agdaFile goldenFile =
+ goldenVsStringDiff testName diffCmd goldenFile $ do
+ -- Get the output directory (same as the agda file directory)
+ let outDir = takeDirectory agdaFile
+
+ -- Run agda2hs
+ (exitCode, stdout, stderr) <- readProcessWithExitCode
+ "agda2hs"
+ [agdaFile, "-o", outDir, "-v0"]
+ ""
+
+ case exitCode of
+ ExitSuccess -> do
+ -- Read the generated .hs file
+ let generatedFile = dropExtension agdaFile ++ ".hs"
+ content <- LBS.readFile generatedFile
+
+ -- Also run ghc to check the generated code compiles
+ (ghcExit, ghcOut, ghcErr) <- readProcessWithExitCode
+ "ghc"
+ ["-fno-code", generatedFile]
+ ""
+
+ case ghcExit of
+ ExitSuccess -> return content
+ ExitFailure _ -> return $ LBS8.pack $
+ "GHC compilation failed:\n" ++ ghcOut ++ ghcErr
+
+ ExitFailure _ -> return $ LBS8.pack $
+ "agda2hs failed:\n" ++ stdout ++ stderr
+
+-- | Create a test for a fail case.
+-- Runs agda2hs on the .agda file, expects it to fail, and compares the error
+-- message to the golden file.
+failTest :: String -> FilePath -> FilePath -> TestTree
+failTest testName agdaFile goldenFile =
+ goldenVsStringDiff testName diffCmd goldenFile $ do
+ -- Run agda2hs (expecting failure)
+ (exitCode, stdout, stderr) <- readProcessWithExitCode
+ "agda2hs"
+ [agdaFile, "-o", takeDirectory agdaFile, "-v0"]
+ ""
+
+ let output = stdout ++ stderr
+ -- Relativize paths in the output
+ relativizedOutput = relativizePaths output
+
+ case exitCode of
+ ExitSuccess ->
+ return $ LBS8.pack "UNEXPECTED SUCCESS"
+ ExitFailure _ ->
+ return $ LBS8.pack relativizedOutput
+
+-- | Relativize absolute paths in error messages.
+-- This replaces absolute paths with relative paths to make tests portable.
+relativizePaths :: String -> String
+relativizePaths = unlines . map relativizeLine . lines
+ where
+ relativizeLine line =
+ -- Look for patterns like /path/to/test/Foo.agda:line:col
+ -- and replace with test/Foo.agda:line:col or just Foo.agda:line:col
+ case break (== '/') line of
+ (prefix, '/':rest) ->
+ if "test/" `isInfixOf` rest || "Fail/" `isInfixOf` rest || "Succeed/" `isInfixOf` rest
+ then prefix ++ extractRelativePath rest
+ else line
+ _ -> line
+
+ extractRelativePath :: String -> String
+ extractRelativePath path =
+ -- Find "test/" in the path and take from there
+ case findTestPrefix path of
+ Just relPath -> relPath
+ Nothing -> path
+
+ findTestPrefix :: String -> Maybe String
+ findTestPrefix s
+ | "test/" `isPrefixOf` s = Just s
+ | null s = Nothing
+ | otherwise = findTestPrefix (drop 1 s)
+
+ isInfixOf :: String -> String -> Bool
+ isInfixOf needle haystack = any (isPrefixOf needle) (tails haystack)
+
+ tails :: String -> [String]
+ tails [] = [[]]
+ tails s@(_:xs) = s : tails xs
+
+-- | Diff command for golden tests.
+diffCmd :: FilePath -> FilePath -> [String]
+diffCmd ref new = ["diff", "-u", ref, new]
diff --git a/test/Assert.agda b/test/Succeed/Assert.agda
similarity index 100%
rename from test/Assert.agda
rename to test/Succeed/Assert.agda
diff --git a/test/golden/Assert.hs b/test/Succeed/Assert.hs
similarity index 100%
rename from test/golden/Assert.hs
rename to test/Succeed/Assert.hs
diff --git a/test/AutoLambdaCaseInBind.agda b/test/Succeed/AutoLambdaCaseInBind.agda
similarity index 100%
rename from test/AutoLambdaCaseInBind.agda
rename to test/Succeed/AutoLambdaCaseInBind.agda
diff --git a/test/golden/AutoLambdaCaseInBind.hs b/test/Succeed/AutoLambdaCaseInBind.hs
similarity index 100%
rename from test/golden/AutoLambdaCaseInBind.hs
rename to test/Succeed/AutoLambdaCaseInBind.hs
diff --git a/test/AutoLambdaCaseInCase.agda b/test/Succeed/AutoLambdaCaseInCase.agda
similarity index 100%
rename from test/AutoLambdaCaseInCase.agda
rename to test/Succeed/AutoLambdaCaseInCase.agda
diff --git a/test/golden/AutoLambdaCaseInCase.hs b/test/Succeed/AutoLambdaCaseInCase.hs
similarity index 100%
rename from test/golden/AutoLambdaCaseInCase.hs
rename to test/Succeed/AutoLambdaCaseInCase.hs
diff --git a/test/BangPatterns.agda b/test/Succeed/BangPatterns.agda
similarity index 100%
rename from test/BangPatterns.agda
rename to test/Succeed/BangPatterns.agda
diff --git a/test/golden/BangPatterns.hs b/test/Succeed/BangPatterns.hs
similarity index 100%
rename from test/golden/BangPatterns.hs
rename to test/Succeed/BangPatterns.hs
diff --git a/test/CanonicalInstance.agda b/test/Succeed/CanonicalInstance.agda
similarity index 100%
rename from test/CanonicalInstance.agda
rename to test/Succeed/CanonicalInstance.agda
diff --git a/test/golden/CanonicalInstance.hs b/test/Succeed/CanonicalInstance.hs
similarity index 100%
rename from test/golden/CanonicalInstance.hs
rename to test/Succeed/CanonicalInstance.hs
diff --git a/test/Coerce.agda b/test/Succeed/Coerce.agda
similarity index 100%
rename from test/Coerce.agda
rename to test/Succeed/Coerce.agda
diff --git a/test/golden/Coerce.hs b/test/Succeed/Coerce.hs
similarity index 100%
rename from test/golden/Coerce.hs
rename to test/Succeed/Coerce.hs
diff --git a/test/Coinduction.agda b/test/Succeed/Coinduction.agda
similarity index 100%
rename from test/Coinduction.agda
rename to test/Succeed/Coinduction.agda
diff --git a/test/golden/Coinduction.hs b/test/Succeed/Coinduction.hs
similarity index 100%
rename from test/golden/Coinduction.hs
rename to test/Succeed/Coinduction.hs
diff --git a/test/CommonQualifiedImports.agda b/test/Succeed/CommonQualifiedImports.agda
similarity index 100%
rename from test/CommonQualifiedImports.agda
rename to test/Succeed/CommonQualifiedImports.agda
diff --git a/test/golden/CommonQualifiedImports.hs b/test/Succeed/CommonQualifiedImports.hs
similarity index 100%
rename from test/golden/CommonQualifiedImports.hs
rename to test/Succeed/CommonQualifiedImports.hs
diff --git a/test/CompileTo.agda b/test/Succeed/CompileTo.agda
similarity index 100%
rename from test/CompileTo.agda
rename to test/Succeed/CompileTo.agda
diff --git a/test/golden/CompileTo.hs b/test/Succeed/CompileTo.hs
similarity index 100%
rename from test/golden/CompileTo.hs
rename to test/Succeed/CompileTo.hs
diff --git a/test/ConstrainedInstance.agda b/test/Succeed/ConstrainedInstance.agda
similarity index 100%
rename from test/ConstrainedInstance.agda
rename to test/Succeed/ConstrainedInstance.agda
diff --git a/test/golden/ConstrainedInstance.hs b/test/Succeed/ConstrainedInstance.hs
similarity index 100%
rename from test/golden/ConstrainedInstance.hs
rename to test/Succeed/ConstrainedInstance.hs
diff --git a/test/golden/Cubical/StreamFusion.hs b/test/Succeed/Cubical/Cubical/StreamFusion.hs
similarity index 100%
rename from test/golden/Cubical/StreamFusion.hs
rename to test/Succeed/Cubical/Cubical/StreamFusion.hs
diff --git a/test/Cubical/StreamFusion.agda b/test/Succeed/Cubical/StreamFusion.agda
similarity index 100%
rename from test/Cubical/StreamFusion.agda
rename to test/Succeed/Cubical/StreamFusion.agda
diff --git a/test/Succeed/Cubical/StreamFusion.hs b/test/Succeed/Cubical/StreamFusion.hs
new file mode 100644
index 00000000..20b64030
--- /dev/null
+++ b/test/Succeed/Cubical/StreamFusion.hs
@@ -0,0 +1,7 @@
+module Cubical.StreamFusion where
+
+data Stream a = (:>){shead :: a, stail :: Stream a}
+
+smap :: (a -> b) -> Stream a -> Stream b
+smap f (x :> xs) = f x :> smap f xs
+
diff --git a/test/CustomTuples.agda b/test/Succeed/CustomTuples.agda
similarity index 100%
rename from test/CustomTuples.agda
rename to test/Succeed/CustomTuples.agda
diff --git a/test/golden/CustomTuples.hs b/test/Succeed/CustomTuples.hs
similarity index 100%
rename from test/golden/CustomTuples.hs
rename to test/Succeed/CustomTuples.hs
diff --git a/test/Datatypes.agda b/test/Succeed/Datatypes.agda
similarity index 100%
rename from test/Datatypes.agda
rename to test/Succeed/Datatypes.agda
diff --git a/test/golden/Datatypes.hs b/test/Succeed/Datatypes.hs
similarity index 100%
rename from test/golden/Datatypes.hs
rename to test/Succeed/Datatypes.hs
diff --git a/test/Default.agda b/test/Succeed/Default.agda
similarity index 100%
rename from test/Default.agda
rename to test/Succeed/Default.agda
diff --git a/test/golden/Default.hs b/test/Succeed/Default.hs
similarity index 100%
rename from test/golden/Default.hs
rename to test/Succeed/Default.hs
diff --git a/test/DefaultMethods.agda b/test/Succeed/DefaultMethods.agda
similarity index 100%
rename from test/DefaultMethods.agda
rename to test/Succeed/DefaultMethods.agda
diff --git a/test/golden/DefaultMethods.hs b/test/Succeed/DefaultMethods.hs
similarity index 100%
rename from test/golden/DefaultMethods.hs
rename to test/Succeed/DefaultMethods.hs
diff --git a/test/Delay.agda b/test/Succeed/Delay.agda
similarity index 100%
rename from test/Delay.agda
rename to test/Succeed/Delay.agda
diff --git a/test/golden/Delay.hs b/test/Succeed/Delay.hs
similarity index 100%
rename from test/golden/Delay.hs
rename to test/Succeed/Delay.hs
diff --git a/test/Deriving.agda b/test/Succeed/Deriving.agda
similarity index 100%
rename from test/Deriving.agda
rename to test/Succeed/Deriving.agda
diff --git a/test/golden/Deriving.hs b/test/Succeed/Deriving.hs
similarity index 100%
rename from test/golden/Deriving.hs
rename to test/Succeed/Deriving.hs
diff --git a/test/DoNotation.agda b/test/Succeed/DoNotation.agda
similarity index 100%
rename from test/DoNotation.agda
rename to test/Succeed/DoNotation.agda
diff --git a/test/golden/DoNotation.hs b/test/Succeed/DoNotation.hs
similarity index 100%
rename from test/golden/DoNotation.hs
rename to test/Succeed/DoNotation.hs
diff --git a/test/EraseType.agda b/test/Succeed/EraseType.agda
similarity index 100%
rename from test/EraseType.agda
rename to test/Succeed/EraseType.agda
diff --git a/test/golden/EraseType.hs b/test/Succeed/EraseType.hs
similarity index 100%
rename from test/golden/EraseType.hs
rename to test/Succeed/EraseType.hs
diff --git a/test/ErasedLocalDefinitions.agda b/test/Succeed/ErasedLocalDefinitions.agda
similarity index 100%
rename from test/ErasedLocalDefinitions.agda
rename to test/Succeed/ErasedLocalDefinitions.agda
diff --git a/test/golden/ErasedLocalDefinitions.hs b/test/Succeed/ErasedLocalDefinitions.hs
similarity index 100%
rename from test/golden/ErasedLocalDefinitions.hs
rename to test/Succeed/ErasedLocalDefinitions.hs
diff --git a/test/ErasedPatternLambda.agda b/test/Succeed/ErasedPatternLambda.agda
similarity index 100%
rename from test/ErasedPatternLambda.agda
rename to test/Succeed/ErasedPatternLambda.agda
diff --git a/test/golden/ErasedPatternLambda.hs b/test/Succeed/ErasedPatternLambda.hs
similarity index 100%
rename from test/golden/ErasedPatternLambda.hs
rename to test/Succeed/ErasedPatternLambda.hs
diff --git a/test/ErasedTypeArguments.agda b/test/Succeed/ErasedTypeArguments.agda
similarity index 100%
rename from test/ErasedTypeArguments.agda
rename to test/Succeed/ErasedTypeArguments.agda
diff --git a/test/golden/ErasedTypeArguments.hs b/test/Succeed/ErasedTypeArguments.hs
similarity index 100%
rename from test/golden/ErasedTypeArguments.hs
rename to test/Succeed/ErasedTypeArguments.hs
diff --git a/test/Fixities.agda b/test/Succeed/Fixities.agda
similarity index 100%
rename from test/Fixities.agda
rename to test/Succeed/Fixities.agda
diff --git a/test/golden/Fixities.hs b/test/Succeed/Fixities.hs
similarity index 100%
rename from test/golden/Fixities.hs
rename to test/Succeed/Fixities.hs
diff --git a/test/FunCon.agda b/test/Succeed/FunCon.agda
similarity index 100%
rename from test/FunCon.agda
rename to test/Succeed/FunCon.agda
diff --git a/test/golden/FunCon.hs b/test/Succeed/FunCon.hs
similarity index 100%
rename from test/golden/FunCon.hs
rename to test/Succeed/FunCon.hs
diff --git a/test/HeightMirror.agda b/test/Succeed/HeightMirror.agda
similarity index 100%
rename from test/HeightMirror.agda
rename to test/Succeed/HeightMirror.agda
diff --git a/test/golden/HeightMirror.hs b/test/Succeed/HeightMirror.hs
similarity index 100%
rename from test/golden/HeightMirror.hs
rename to test/Succeed/HeightMirror.hs
diff --git a/test/IOFile.agda b/test/Succeed/IOFile.agda
similarity index 100%
rename from test/IOFile.agda
rename to test/Succeed/IOFile.agda
diff --git a/test/golden/IOFile.hs b/test/Succeed/IOFile.hs
similarity index 100%
rename from test/golden/IOFile.hs
rename to test/Succeed/IOFile.hs
diff --git a/test/IOInput.agda b/test/Succeed/IOInput.agda
similarity index 100%
rename from test/IOInput.agda
rename to test/Succeed/IOInput.agda
diff --git a/test/golden/IOInput.hs b/test/Succeed/IOInput.hs
similarity index 100%
rename from test/golden/IOInput.hs
rename to test/Succeed/IOInput.hs
diff --git a/test/Importee.agda b/test/Succeed/Importee.agda
similarity index 100%
rename from test/Importee.agda
rename to test/Succeed/Importee.agda
diff --git a/test/golden/Importee.hs b/test/Succeed/Importee.hs
similarity index 100%
rename from test/golden/Importee.hs
rename to test/Succeed/Importee.hs
diff --git a/test/Importer.agda b/test/Succeed/Importer.agda
similarity index 100%
rename from test/Importer.agda
rename to test/Succeed/Importer.agda
diff --git a/test/golden/Importer.hs b/test/Succeed/Importer.hs
similarity index 100%
rename from test/golden/Importer.hs
rename to test/Succeed/Importer.hs
diff --git a/test/Inlining.agda b/test/Succeed/Inlining.agda
similarity index 100%
rename from test/Inlining.agda
rename to test/Succeed/Inlining.agda
diff --git a/test/golden/Inlining.hs b/test/Succeed/Inlining.hs
similarity index 100%
rename from test/golden/Inlining.hs
rename to test/Succeed/Inlining.hs
diff --git a/test/Issue107.agda b/test/Succeed/Issue107.agda
similarity index 100%
rename from test/Issue107.agda
rename to test/Succeed/Issue107.agda
diff --git a/test/Issue115.agda b/test/Succeed/Issue115.agda
similarity index 100%
rename from test/Issue115.agda
rename to test/Succeed/Issue115.agda
diff --git a/test/golden/Issue115.hs b/test/Succeed/Issue115.hs
similarity index 100%
rename from test/golden/Issue115.hs
rename to test/Succeed/Issue115.hs
diff --git a/test/Issue14.agda b/test/Succeed/Issue14.agda
similarity index 100%
rename from test/Issue14.agda
rename to test/Succeed/Issue14.agda
diff --git a/test/golden/Issue14.hs b/test/Succeed/Issue14.hs
similarity index 100%
rename from test/golden/Issue14.hs
rename to test/Succeed/Issue14.hs
diff --git a/test/Issue145.agda b/test/Succeed/Issue145.agda
similarity index 100%
rename from test/Issue145.agda
rename to test/Succeed/Issue145.agda
diff --git a/test/golden/Issue145.hs b/test/Succeed/Issue145.hs
similarity index 100%
rename from test/golden/Issue145.hs
rename to test/Succeed/Issue145.hs
diff --git a/test/Issue169.agda b/test/Succeed/Issue169.agda
similarity index 100%
rename from test/Issue169.agda
rename to test/Succeed/Issue169.agda
diff --git a/test/golden/Issue169.hs b/test/Succeed/Issue169.hs
similarity index 100%
rename from test/golden/Issue169.hs
rename to test/Succeed/Issue169.hs
diff --git a/test/Issue200.agda b/test/Succeed/Issue200.agda
similarity index 100%
rename from test/Issue200.agda
rename to test/Succeed/Issue200.agda
diff --git a/test/golden/Issue200.hs b/test/Succeed/Issue200.hs
similarity index 100%
rename from test/golden/Issue200.hs
rename to test/Succeed/Issue200.hs
diff --git a/test/Issue210.agda b/test/Succeed/Issue210.agda
similarity index 100%
rename from test/Issue210.agda
rename to test/Succeed/Issue210.agda
diff --git a/test/golden/Issue210.hs b/test/Succeed/Issue210.hs
similarity index 100%
rename from test/golden/Issue210.hs
rename to test/Succeed/Issue210.hs
diff --git a/test/Issue218.agda b/test/Succeed/Issue218.agda
similarity index 100%
rename from test/Issue218.agda
rename to test/Succeed/Issue218.agda
diff --git a/test/golden/Issue218.hs b/test/Succeed/Issue218.hs
similarity index 100%
rename from test/golden/Issue218.hs
rename to test/Succeed/Issue218.hs
diff --git a/test/Issue251.agda b/test/Succeed/Issue251.agda
similarity index 100%
rename from test/Issue251.agda
rename to test/Succeed/Issue251.agda
diff --git a/test/golden/Issue251.hs b/test/Succeed/Issue251.hs
similarity index 100%
rename from test/golden/Issue251.hs
rename to test/Succeed/Issue251.hs
diff --git a/test/Issue257.agda b/test/Succeed/Issue257.agda
similarity index 100%
rename from test/Issue257.agda
rename to test/Succeed/Issue257.agda
diff --git a/test/Issue264.agda b/test/Succeed/Issue264.agda
similarity index 100%
rename from test/Issue264.agda
rename to test/Succeed/Issue264.agda
diff --git a/test/golden/Issue264.hs b/test/Succeed/Issue264.hs
similarity index 100%
rename from test/golden/Issue264.hs
rename to test/Succeed/Issue264.hs
diff --git a/test/Issue273.agda b/test/Succeed/Issue273.agda
similarity index 100%
rename from test/Issue273.agda
rename to test/Succeed/Issue273.agda
diff --git a/test/golden/Issue273.hs b/test/Succeed/Issue273.hs
similarity index 100%
rename from test/golden/Issue273.hs
rename to test/Succeed/Issue273.hs
diff --git a/test/Issue286.agda b/test/Succeed/Issue286.agda
similarity index 100%
rename from test/Issue286.agda
rename to test/Succeed/Issue286.agda
diff --git a/test/golden/Issue286.hs b/test/Succeed/Issue286.hs
similarity index 100%
rename from test/golden/Issue286.hs
rename to test/Succeed/Issue286.hs
diff --git a/test/Issue301.agda b/test/Succeed/Issue301.agda
similarity index 100%
rename from test/Issue301.agda
rename to test/Succeed/Issue301.agda
diff --git a/test/golden/Issue301.hs b/test/Succeed/Issue301.hs
similarity index 100%
rename from test/golden/Issue301.hs
rename to test/Succeed/Issue301.hs
diff --git a/test/Issue302.agda b/test/Succeed/Issue302.agda
similarity index 100%
rename from test/Issue302.agda
rename to test/Succeed/Issue302.agda
diff --git a/test/golden/Issue302.hs b/test/Succeed/Issue302.hs
similarity index 100%
rename from test/golden/Issue302.hs
rename to test/Succeed/Issue302.hs
diff --git a/test/Issue305.agda b/test/Succeed/Issue305.agda
similarity index 100%
rename from test/Issue305.agda
rename to test/Succeed/Issue305.agda
diff --git a/test/golden/Issue305.hs b/test/Succeed/Issue305.hs
similarity index 100%
rename from test/golden/Issue305.hs
rename to test/Succeed/Issue305.hs
diff --git a/test/Issue306.agda b/test/Succeed/Issue306.agda
similarity index 100%
rename from test/Issue306.agda
rename to test/Succeed/Issue306.agda
diff --git a/test/golden/Issue306.hs b/test/Succeed/Issue306.hs
similarity index 100%
rename from test/golden/Issue306.hs
rename to test/Succeed/Issue306.hs
diff --git a/test/Issue308.agda b/test/Succeed/Issue308.agda
similarity index 100%
rename from test/Issue308.agda
rename to test/Succeed/Issue308.agda
diff --git a/test/golden/Issue308.hs b/test/Succeed/Issue308.hs
similarity index 100%
rename from test/golden/Issue308.hs
rename to test/Succeed/Issue308.hs
diff --git a/test/Issue309.agda b/test/Succeed/Issue309.agda
similarity index 100%
rename from test/Issue309.agda
rename to test/Succeed/Issue309.agda
diff --git a/test/golden/Issue309.hs b/test/Succeed/Issue309.hs
similarity index 100%
rename from test/golden/Issue309.hs
rename to test/Succeed/Issue309.hs
diff --git a/test/Issue317.agda b/test/Succeed/Issue317.agda
similarity index 100%
rename from test/Issue317.agda
rename to test/Succeed/Issue317.agda
diff --git a/test/golden/Issue317.hs b/test/Succeed/Issue317.hs
similarity index 100%
rename from test/golden/Issue317.hs
rename to test/Succeed/Issue317.hs
diff --git a/test/Issue324.agda b/test/Succeed/Issue324.agda
similarity index 100%
rename from test/Issue324.agda
rename to test/Succeed/Issue324.agda
diff --git a/test/golden/Issue324.hs b/test/Succeed/Issue324.hs
similarity index 100%
rename from test/golden/Issue324.hs
rename to test/Succeed/Issue324.hs
diff --git a/test/Issue324instance.agda b/test/Succeed/Issue324instance.agda
similarity index 100%
rename from test/Issue324instance.agda
rename to test/Succeed/Issue324instance.agda
diff --git a/test/golden/Issue324instance.hs b/test/Succeed/Issue324instance.hs
similarity index 100%
rename from test/golden/Issue324instance.hs
rename to test/Succeed/Issue324instance.hs
diff --git a/test/Issue346.agda b/test/Succeed/Issue346.agda
similarity index 100%
rename from test/Issue346.agda
rename to test/Succeed/Issue346.agda
diff --git a/test/golden/Issue346.hs b/test/Succeed/Issue346.hs
similarity index 100%
rename from test/golden/Issue346.hs
rename to test/Succeed/Issue346.hs
diff --git a/test/Issue353.agda b/test/Succeed/Issue353.agda
similarity index 100%
rename from test/Issue353.agda
rename to test/Succeed/Issue353.agda
diff --git a/test/golden/Issue353.hs b/test/Succeed/Issue353.hs
similarity index 100%
rename from test/golden/Issue353.hs
rename to test/Succeed/Issue353.hs
diff --git a/test/Issue377.agda b/test/Succeed/Issue377.agda
similarity index 100%
rename from test/Issue377.agda
rename to test/Succeed/Issue377.agda
diff --git a/test/golden/Issue377.hs b/test/Succeed/Issue377.hs
similarity index 100%
rename from test/golden/Issue377.hs
rename to test/Succeed/Issue377.hs
diff --git a/test/Issue394.agda b/test/Succeed/Issue394.agda
similarity index 100%
rename from test/Issue394.agda
rename to test/Succeed/Issue394.agda
diff --git a/test/golden/Issue394.hs b/test/Succeed/Issue394.hs
similarity index 100%
rename from test/golden/Issue394.hs
rename to test/Succeed/Issue394.hs
diff --git a/test/Issue408.agda b/test/Succeed/Issue408.agda
similarity index 100%
rename from test/Issue408.agda
rename to test/Succeed/Issue408.agda
diff --git a/test/golden/Issue408.hs b/test/Succeed/Issue408.hs
similarity index 100%
rename from test/golden/Issue408.hs
rename to test/Succeed/Issue408.hs
diff --git a/test/Issue409.agda b/test/Succeed/Issue409.agda
similarity index 100%
rename from test/Issue409.agda
rename to test/Succeed/Issue409.agda
diff --git a/test/golden/Issue409.hs b/test/Succeed/Issue409.hs
similarity index 100%
rename from test/golden/Issue409.hs
rename to test/Succeed/Issue409.hs
diff --git a/test/Issue421.agda b/test/Succeed/Issue421.agda
similarity index 100%
rename from test/Issue421.agda
rename to test/Succeed/Issue421.agda
diff --git a/test/golden/Issue421.hs b/test/Succeed/Issue421.hs
similarity index 100%
rename from test/golden/Issue421.hs
rename to test/Succeed/Issue421.hs
diff --git a/test/Issue65.agda b/test/Succeed/Issue65.agda
similarity index 100%
rename from test/Issue65.agda
rename to test/Succeed/Issue65.agda
diff --git a/test/golden/Issue65.hs b/test/Succeed/Issue65.hs
similarity index 100%
rename from test/golden/Issue65.hs
rename to test/Succeed/Issue65.hs
diff --git a/test/Issue69.agda b/test/Succeed/Issue69.agda
similarity index 100%
rename from test/Issue69.agda
rename to test/Succeed/Issue69.agda
diff --git a/test/golden/Issue69.hs b/test/Succeed/Issue69.hs
similarity index 100%
rename from test/golden/Issue69.hs
rename to test/Succeed/Issue69.hs
diff --git a/test/Issue73.agda b/test/Succeed/Issue73.agda
similarity index 100%
rename from test/Issue73.agda
rename to test/Succeed/Issue73.agda
diff --git a/test/golden/Issue73.hs b/test/Succeed/Issue73.hs
similarity index 100%
rename from test/golden/Issue73.hs
rename to test/Succeed/Issue73.hs
diff --git a/test/Issue90.agda b/test/Succeed/Issue90.agda
similarity index 100%
rename from test/Issue90.agda
rename to test/Succeed/Issue90.agda
diff --git a/test/golden/Issue90.hs b/test/Succeed/Issue90.hs
similarity index 100%
rename from test/golden/Issue90.hs
rename to test/Succeed/Issue90.hs
diff --git a/test/Issue92.agda b/test/Succeed/Issue92.agda
similarity index 100%
rename from test/Issue92.agda
rename to test/Succeed/Issue92.agda
diff --git a/test/golden/Issue92.hs b/test/Succeed/Issue92.hs
similarity index 100%
rename from test/golden/Issue92.hs
rename to test/Succeed/Issue92.hs
diff --git a/test/Issue93.agda b/test/Succeed/Issue93.agda
similarity index 100%
rename from test/Issue93.agda
rename to test/Succeed/Issue93.agda
diff --git a/test/golden/Issue93.hs b/test/Succeed/Issue93.hs
similarity index 100%
rename from test/golden/Issue93.hs
rename to test/Succeed/Issue93.hs
diff --git a/test/Issue94.agda b/test/Succeed/Issue94.agda
similarity index 100%
rename from test/Issue94.agda
rename to test/Succeed/Issue94.agda
diff --git a/test/golden/Issue94.hs b/test/Succeed/Issue94.hs
similarity index 100%
rename from test/golden/Issue94.hs
rename to test/Succeed/Issue94.hs
diff --git a/test/Kinds.agda b/test/Succeed/Kinds.agda
similarity index 100%
rename from test/Kinds.agda
rename to test/Succeed/Kinds.agda
diff --git a/test/golden/Kinds.hs b/test/Succeed/Kinds.hs
similarity index 100%
rename from test/golden/Kinds.hs
rename to test/Succeed/Kinds.hs
diff --git a/test/LanguageConstructs.agda b/test/Succeed/LanguageConstructs.agda
similarity index 100%
rename from test/LanguageConstructs.agda
rename to test/Succeed/LanguageConstructs.agda
diff --git a/test/golden/LanguageConstructs.hs b/test/Succeed/LanguageConstructs.hs
similarity index 100%
rename from test/golden/LanguageConstructs.hs
rename to test/Succeed/LanguageConstructs.hs
diff --git a/test/LawfulOrd.agda b/test/Succeed/LawfulOrd.agda
similarity index 100%
rename from test/LawfulOrd.agda
rename to test/Succeed/LawfulOrd.agda
diff --git a/test/golden/LawfulOrd.hs b/test/Succeed/LawfulOrd.hs
similarity index 100%
rename from test/golden/LawfulOrd.hs
rename to test/Succeed/LawfulOrd.hs
diff --git a/test/LiteralPatterns.agda b/test/Succeed/LiteralPatterns.agda
similarity index 100%
rename from test/LiteralPatterns.agda
rename to test/Succeed/LiteralPatterns.agda
diff --git a/test/golden/LiteralPatterns.hs b/test/Succeed/LiteralPatterns.hs
similarity index 100%
rename from test/golden/LiteralPatterns.hs
rename to test/Succeed/LiteralPatterns.hs
diff --git a/test/ModuleParameters.agda b/test/Succeed/ModuleParameters.agda
similarity index 100%
rename from test/ModuleParameters.agda
rename to test/Succeed/ModuleParameters.agda
diff --git a/test/golden/ModuleParameters.hs b/test/Succeed/ModuleParameters.hs
similarity index 100%
rename from test/golden/ModuleParameters.hs
rename to test/Succeed/ModuleParameters.hs
diff --git a/test/ModuleParametersImports.agda b/test/Succeed/ModuleParametersImports.agda
similarity index 100%
rename from test/ModuleParametersImports.agda
rename to test/Succeed/ModuleParametersImports.agda
diff --git a/test/golden/ModuleParametersImports.hs b/test/Succeed/ModuleParametersImports.hs
similarity index 100%
rename from test/golden/ModuleParametersImports.hs
rename to test/Succeed/ModuleParametersImports.hs
diff --git a/test/NewTypePragma.agda b/test/Succeed/NewTypePragma.agda
similarity index 100%
rename from test/NewTypePragma.agda
rename to test/Succeed/NewTypePragma.agda
diff --git a/test/golden/NewTypePragma.hs b/test/Succeed/NewTypePragma.hs
similarity index 100%
rename from test/golden/NewTypePragma.hs
rename to test/Succeed/NewTypePragma.hs
diff --git a/test/NonClassInstance.agda b/test/Succeed/NonClassInstance.agda
similarity index 100%
rename from test/NonClassInstance.agda
rename to test/Succeed/NonClassInstance.agda
diff --git a/test/golden/NonClassInstance.hs b/test/Succeed/NonClassInstance.hs
similarity index 100%
rename from test/golden/NonClassInstance.hs
rename to test/Succeed/NonClassInstance.hs
diff --git a/test/Numbers.agda b/test/Succeed/Numbers.agda
similarity index 100%
rename from test/Numbers.agda
rename to test/Succeed/Numbers.agda
diff --git a/test/golden/Numbers.hs b/test/Succeed/Numbers.hs
similarity index 100%
rename from test/golden/Numbers.hs
rename to test/Succeed/Numbers.hs
diff --git a/test/OtherImportee.agda b/test/Succeed/OtherImportee.agda
similarity index 100%
rename from test/OtherImportee.agda
rename to test/Succeed/OtherImportee.agda
diff --git a/test/golden/OtherImportee.hs b/test/Succeed/OtherImportee.hs
similarity index 100%
rename from test/golden/OtherImportee.hs
rename to test/Succeed/OtherImportee.hs
diff --git a/test/Pragmas.agda b/test/Succeed/Pragmas.agda
similarity index 100%
rename from test/Pragmas.agda
rename to test/Succeed/Pragmas.agda
diff --git a/test/golden/Pragmas.hs b/test/Succeed/Pragmas.hs
similarity index 100%
rename from test/golden/Pragmas.hs
rename to test/Succeed/Pragmas.hs
diff --git a/test/ProjLike.agda b/test/Succeed/ProjLike.agda
similarity index 100%
rename from test/ProjLike.agda
rename to test/Succeed/ProjLike.agda
diff --git a/test/golden/ProjLike.hs b/test/Succeed/ProjLike.hs
similarity index 100%
rename from test/golden/ProjLike.hs
rename to test/Succeed/ProjLike.hs
diff --git a/test/ProjectionLike.agda b/test/Succeed/ProjectionLike.agda
similarity index 100%
rename from test/ProjectionLike.agda
rename to test/Succeed/ProjectionLike.agda
diff --git a/test/golden/ProjectionLike.hs b/test/Succeed/ProjectionLike.hs
similarity index 100%
rename from test/golden/ProjectionLike.hs
rename to test/Succeed/ProjectionLike.hs
diff --git a/test/QualifiedImportee.agda b/test/Succeed/QualifiedImportee.agda
similarity index 100%
rename from test/QualifiedImportee.agda
rename to test/Succeed/QualifiedImportee.agda
diff --git a/test/golden/QualifiedImportee.hs b/test/Succeed/QualifiedImportee.hs
similarity index 100%
rename from test/golden/QualifiedImportee.hs
rename to test/Succeed/QualifiedImportee.hs
diff --git a/test/QualifiedImports.agda b/test/Succeed/QualifiedImports.agda
similarity index 100%
rename from test/QualifiedImports.agda
rename to test/Succeed/QualifiedImports.agda
diff --git a/test/golden/QualifiedImports.hs b/test/Succeed/QualifiedImports.hs
similarity index 100%
rename from test/golden/QualifiedImports.hs
rename to test/Succeed/QualifiedImports.hs
diff --git a/test/QualifiedModule.agda b/test/Succeed/QualifiedModule.agda
similarity index 100%
rename from test/QualifiedModule.agda
rename to test/Succeed/QualifiedModule.agda
diff --git a/test/golden/QualifiedModule.hs b/test/Succeed/QualifiedModule.hs
similarity index 100%
rename from test/golden/QualifiedModule.hs
rename to test/Succeed/QualifiedModule.hs
diff --git a/test/QualifiedPrelude.agda b/test/Succeed/QualifiedPrelude.agda
similarity index 100%
rename from test/QualifiedPrelude.agda
rename to test/Succeed/QualifiedPrelude.agda
diff --git a/test/golden/QualifiedPrelude.hs b/test/Succeed/QualifiedPrelude.hs
similarity index 100%
rename from test/golden/QualifiedPrelude.hs
rename to test/Succeed/QualifiedPrelude.hs
diff --git a/test/RankNTypes.agda b/test/Succeed/RankNTypes.agda
similarity index 100%
rename from test/RankNTypes.agda
rename to test/Succeed/RankNTypes.agda
diff --git a/test/golden/RankNTypes.hs b/test/Succeed/RankNTypes.hs
similarity index 100%
rename from test/golden/RankNTypes.hs
rename to test/Succeed/RankNTypes.hs
diff --git a/test/Records.agda b/test/Succeed/Records.agda
similarity index 100%
rename from test/Records.agda
rename to test/Succeed/Records.agda
diff --git a/test/golden/Records.hs b/test/Succeed/Records.hs
similarity index 100%
rename from test/golden/Records.hs
rename to test/Succeed/Records.hs
diff --git a/test/RelevantDotPattern1.agda b/test/Succeed/RelevantDotPattern1.agda
similarity index 100%
rename from test/RelevantDotPattern1.agda
rename to test/Succeed/RelevantDotPattern1.agda
diff --git a/test/golden/RelevantDotPattern1.hs b/test/Succeed/RelevantDotPattern1.hs
similarity index 100%
rename from test/golden/RelevantDotPattern1.hs
rename to test/Succeed/RelevantDotPattern1.hs
diff --git a/test/RelevantDotPattern2.agda b/test/Succeed/RelevantDotPattern2.agda
similarity index 100%
rename from test/RelevantDotPattern2.agda
rename to test/Succeed/RelevantDotPattern2.agda
diff --git a/test/golden/RelevantDotPattern2.hs b/test/Succeed/RelevantDotPattern2.hs
similarity index 100%
rename from test/golden/RelevantDotPattern2.hs
rename to test/Succeed/RelevantDotPattern2.hs
diff --git a/test/RelevantDotPattern3.agda b/test/Succeed/RelevantDotPattern3.agda
similarity index 100%
rename from test/RelevantDotPattern3.agda
rename to test/Succeed/RelevantDotPattern3.agda
diff --git a/test/golden/RelevantDotPattern3.hs b/test/Succeed/RelevantDotPattern3.hs
similarity index 100%
rename from test/golden/RelevantDotPattern3.hs
rename to test/Succeed/RelevantDotPattern3.hs
diff --git a/test/RequalifiedImports.agda b/test/Succeed/RequalifiedImports.agda
similarity index 100%
rename from test/RequalifiedImports.agda
rename to test/Succeed/RequalifiedImports.agda
diff --git a/test/golden/RequalifiedImports.hs b/test/Succeed/RequalifiedImports.hs
similarity index 100%
rename from test/golden/RequalifiedImports.hs
rename to test/Succeed/RequalifiedImports.hs
diff --git a/test/RuntimeCast.agda b/test/Succeed/RuntimeCast.agda
similarity index 100%
rename from test/RuntimeCast.agda
rename to test/Succeed/RuntimeCast.agda
diff --git a/test/golden/RuntimeCast.hs b/test/Succeed/RuntimeCast.hs
similarity index 100%
rename from test/golden/RuntimeCast.hs
rename to test/Succeed/RuntimeCast.hs
diff --git a/test/ScopedTypeVariables.agda b/test/Succeed/ScopedTypeVariables.agda
similarity index 100%
rename from test/ScopedTypeVariables.agda
rename to test/Succeed/ScopedTypeVariables.agda
diff --git a/test/golden/ScopedTypeVariables.hs b/test/Succeed/ScopedTypeVariables.hs
similarity index 100%
rename from test/golden/ScopedTypeVariables.hs
rename to test/Succeed/ScopedTypeVariables.hs
diff --git a/test/SecondImportee.agda b/test/Succeed/SecondImportee.agda
similarity index 100%
rename from test/SecondImportee.agda
rename to test/Succeed/SecondImportee.agda
diff --git a/test/golden/SecondImportee.hs b/test/Succeed/SecondImportee.hs
similarity index 100%
rename from test/golden/SecondImportee.hs
rename to test/Succeed/SecondImportee.hs
diff --git a/test/Sections.agda b/test/Succeed/Sections.agda
similarity index 100%
rename from test/Sections.agda
rename to test/Succeed/Sections.agda
diff --git a/test/golden/Sections.hs b/test/Succeed/Sections.hs
similarity index 100%
rename from test/golden/Sections.hs
rename to test/Succeed/Sections.hs
diff --git a/test/Superclass.agda b/test/Succeed/Superclass.agda
similarity index 100%
rename from test/Superclass.agda
rename to test/Succeed/Superclass.agda
diff --git a/test/golden/Superclass.hs b/test/Succeed/Superclass.hs
similarity index 100%
rename from test/golden/Superclass.hs
rename to test/Succeed/Superclass.hs
diff --git a/test/Test.agda b/test/Succeed/Test.agda
similarity index 100%
rename from test/Test.agda
rename to test/Succeed/Test.agda
diff --git a/test/golden/Test.hs b/test/Succeed/Test.hs
similarity index 100%
rename from test/golden/Test.hs
rename to test/Succeed/Test.hs
diff --git a/test/TransparentFun.agda b/test/Succeed/TransparentFun.agda
similarity index 100%
rename from test/TransparentFun.agda
rename to test/Succeed/TransparentFun.agda
diff --git a/test/golden/TransparentFun.hs b/test/Succeed/TransparentFun.hs
similarity index 100%
rename from test/golden/TransparentFun.hs
rename to test/Succeed/TransparentFun.hs
diff --git a/test/Tree.agda b/test/Succeed/Tree.agda
similarity index 100%
rename from test/Tree.agda
rename to test/Succeed/Tree.agda
diff --git a/test/golden/Tree.hs b/test/Succeed/Tree.hs
similarity index 100%
rename from test/golden/Tree.hs
rename to test/Succeed/Tree.hs
diff --git a/test/Tuples.agda b/test/Succeed/Tuples.agda
similarity index 100%
rename from test/Tuples.agda
rename to test/Succeed/Tuples.agda
diff --git a/test/golden/Tuples.hs b/test/Succeed/Tuples.hs
similarity index 100%
rename from test/golden/Tuples.hs
rename to test/Succeed/Tuples.hs
diff --git a/test/TypeBasedUnboxing.agda b/test/Succeed/TypeBasedUnboxing.agda
similarity index 100%
rename from test/TypeBasedUnboxing.agda
rename to test/Succeed/TypeBasedUnboxing.agda
diff --git a/test/golden/TypeBasedUnboxing.hs b/test/Succeed/TypeBasedUnboxing.hs
similarity index 100%
rename from test/golden/TypeBasedUnboxing.hs
rename to test/Succeed/TypeBasedUnboxing.hs
diff --git a/test/TypeDirected.agda b/test/Succeed/TypeDirected.agda
similarity index 100%
rename from test/TypeDirected.agda
rename to test/Succeed/TypeDirected.agda
diff --git a/test/golden/TypeDirected.hs b/test/Succeed/TypeDirected.hs
similarity index 100%
rename from test/golden/TypeDirected.hs
rename to test/Succeed/TypeDirected.hs
diff --git a/test/TypeOperatorExport.agda b/test/Succeed/TypeOperatorExport.agda
similarity index 100%
rename from test/TypeOperatorExport.agda
rename to test/Succeed/TypeOperatorExport.agda
diff --git a/test/golden/TypeOperatorExport.hs b/test/Succeed/TypeOperatorExport.hs
similarity index 100%
rename from test/golden/TypeOperatorExport.hs
rename to test/Succeed/TypeOperatorExport.hs
diff --git a/test/TypeOperatorImport.agda b/test/Succeed/TypeOperatorImport.agda
similarity index 100%
rename from test/TypeOperatorImport.agda
rename to test/Succeed/TypeOperatorImport.agda
diff --git a/test/golden/TypeOperatorImport.hs b/test/Succeed/TypeOperatorImport.hs
similarity index 100%
rename from test/golden/TypeOperatorImport.hs
rename to test/Succeed/TypeOperatorImport.hs
diff --git a/test/TypeOperators.agda b/test/Succeed/TypeOperators.agda
similarity index 100%
rename from test/TypeOperators.agda
rename to test/Succeed/TypeOperators.agda
diff --git a/test/golden/TypeOperators.hs b/test/Succeed/TypeOperators.hs
similarity index 100%
rename from test/golden/TypeOperators.hs
rename to test/Succeed/TypeOperators.hs
diff --git a/test/TypeSignature.agda b/test/Succeed/TypeSignature.agda
similarity index 100%
rename from test/TypeSignature.agda
rename to test/Succeed/TypeSignature.agda
diff --git a/test/golden/TypeSignature.hs b/test/Succeed/TypeSignature.hs
similarity index 100%
rename from test/golden/TypeSignature.hs
rename to test/Succeed/TypeSignature.hs
diff --git a/test/TypeSynonyms.agda b/test/Succeed/TypeSynonyms.agda
similarity index 100%
rename from test/TypeSynonyms.agda
rename to test/Succeed/TypeSynonyms.agda
diff --git a/test/golden/TypeSynonyms.hs b/test/Succeed/TypeSynonyms.hs
similarity index 100%
rename from test/golden/TypeSynonyms.hs
rename to test/Succeed/TypeSynonyms.hs
diff --git a/test/UnboxPragma.agda b/test/Succeed/UnboxPragma.agda
similarity index 100%
rename from test/UnboxPragma.agda
rename to test/Succeed/UnboxPragma.agda
diff --git a/test/golden/UnboxPragma.hs b/test/Succeed/UnboxPragma.hs
similarity index 100%
rename from test/golden/UnboxPragma.hs
rename to test/Succeed/UnboxPragma.hs
diff --git a/test/Vector.agda b/test/Succeed/Vector.agda
similarity index 100%
rename from test/Vector.agda
rename to test/Succeed/Vector.agda
diff --git a/test/golden/Vector.hs b/test/Succeed/Vector.hs
similarity index 100%
rename from test/golden/Vector.hs
rename to test/Succeed/Vector.hs
diff --git a/test/Where.agda b/test/Succeed/Where.agda
similarity index 100%
rename from test/Where.agda
rename to test/Succeed/Where.agda
diff --git a/test/golden/Where.hs b/test/Succeed/Where.hs
similarity index 100%
rename from test/golden/Where.hs
rename to test/Succeed/Where.hs
diff --git a/test/WitnessedFlows.agda b/test/Succeed/WitnessedFlows.agda
similarity index 100%
rename from test/WitnessedFlows.agda
rename to test/Succeed/WitnessedFlows.agda
diff --git a/test/golden/WitnessedFlows.hs b/test/Succeed/WitnessedFlows.hs
similarity index 100%
rename from test/golden/WitnessedFlows.hs
rename to test/Succeed/WitnessedFlows.hs
diff --git a/test/agda2hs-test.agda-lib b/test/agda2hs-test.agda-lib
index b700128b..c82e9d29 100644
--- a/test/agda2hs-test.agda-lib
+++ b/test/agda2hs-test.agda-lib
@@ -1,4 +1,4 @@
name: agda2hs-test
depend:
-include: . ../lib/base/
+include: . Succeed Fail ../lib/base/
flags: --sized-types --erasure --no-projection-like
diff --git a/test/golden/AllCubicalTests.hs b/test/golden/AllCubicalTests.hs
deleted file mode 100644
index d1e2f81e..00000000
--- a/test/golden/AllCubicalTests.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module AllCubicalTests where
-
-import Cubical.StreamFusion
-
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
deleted file mode 100644
index 8c90d4aa..00000000
--- a/test/golden/AllTests.hs
+++ /dev/null
@@ -1,104 +0,0 @@
-module AllTests where
-
-import Issue14
-import Issue65
-import Issue69
-import Issue73
-import Fixities
-import LanguageConstructs
-import Numbers
-import Pragmas
-import Sections
-import Test
-import Tree
-import Tuples
-import Where
-import TypeSynonyms
-import CanonicalInstance
-import Coinduction
-import ConstrainedInstance
-import Datatypes
-import Records
-import Default
-import DefaultMethods
-import Vector
-import Issue90
-import Issue93
-import QualifiedModule
-import Superclass
-import UnboxPragma
-import ScopedTypeVariables
-import LiteralPatterns
-import Issue92
-import HeightMirror
-import TransparentFun
-import Issue115
-import BangPatterns
-import Issue94
-import DoNotation
-import NewTypePragma
-import Importer
-import QualifiedImports
-import CommonQualifiedImports
-import RequalifiedImports
-import QualifiedPrelude
-import AutoLambdaCaseInCase
-import AutoLambdaCaseInBind
-import WitnessedFlows
-import Kinds
-import LawfulOrd
-import Deriving
-import ErasedLocalDefinitions
-import TypeOperators
-import ErasedTypeArguments
-import TypeOperatorExport
-import TypeOperatorImport
-import IOFile
-import IOInput
-import Issue200
-import Issue169
-import Issue210
-import TypeSignature
-import ModuleParameters
-import ModuleParametersImports
-import Coerce
-import Inlining
-import EraseType
-import Delay
-import Issue273
-import TypeDirected
-import ProjLike
-import Issue286
-import NonClassInstance
-import Issue218
-import Issue251
-import TypeBasedUnboxing
-import Issue145
-import Issue264
-import Issue301
-import Issue305
-import Issue302
-import Issue309
-import Issue317
-import Issue353
-import RankNTypes
-import ErasedPatternLambda
-import CustomTuples
-import ProjectionLike
-import FunCon
-import Issue308
-import Issue324
-import Assert
-import Issue377
-import Issue394
-import Issue421
-import Issue409
-import Issue346
-import Issue408
-import CompileTo
-import RuntimeCast
-import Issue306
-import RelevantDotPattern1
-import RelevantDotPattern2
-import RelevantDotPattern3
-
From 34e225189730cf9c0e3be01efe838b1ad466b87f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 14:30:38 +0000
Subject: [PATCH 03/12] Fix test runner for module discovery and UTF-8 encoding
- Add include paths for agda2hs to find modules in Succeed directory
- Add include paths for GHC to find imported Haskell modules
- Fix UTF-8 encoding issue in error message comparison using Data.Text
- Add text dependency to test-suite
- Revert agda-lib changes (no longer needed with include path approach)
- Remove duplicate Cubical subdirectory
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
agda2hs.cabal | 1 +
test/Fail/Importee.hs | 19 ++++++++++++++++
test/Fail/OtherImportee.hs | 4 ++++
test/Fail/SecondImportee.hs | 5 +++++
test/Main.hs | 43 +++++++++++++++++++++++--------------
test/Succeed/Issue107.hs | 2 ++
test/Succeed/Issue257.hs | 2 ++
test/agda2hs-test.agda-lib | 2 +-
8 files changed, 61 insertions(+), 17 deletions(-)
create mode 100644 test/Fail/Importee.hs
create mode 100644 test/Fail/OtherImportee.hs
create mode 100644 test/Fail/SecondImportee.hs
create mode 100644 test/Succeed/Issue107.hs
create mode 100644 test/Succeed/Issue257.hs
diff --git a/agda2hs.cabal b/agda2hs.cabal
index 7f057ed5..4504e846 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -103,6 +103,7 @@ test-suite agda2hs-test
process >= 1.6 && < 1.7,
tasty >= 1.4 && < 1.6,
tasty-golden >= 2.3 && < 2.4,
+ text >= 2.0.2 && < 2.2,
default-language: Haskell2010
default-extensions: OverloadedStrings
build-tool-depends: agda2hs:agda2hs
diff --git a/test/Fail/Importee.hs b/test/Fail/Importee.hs
new file mode 100644
index 00000000..c8fd9109
--- /dev/null
+++ b/test/Fail/Importee.hs
@@ -0,0 +1,19 @@
+module Importee where
+
+foo :: Int
+foo = 42
+
+(!#) :: Int -> Int -> Int
+x !# y = x + y
+
+data Foo = MkFoo
+
+class Fooable a where
+ doTheFoo :: a
+ defaultFoo :: a
+ {-# MINIMAL doTheFoo #-}
+ defaultFoo = doTheFoo
+
+instance Fooable Foo where
+ doTheFoo = MkFoo
+
diff --git a/test/Fail/OtherImportee.hs b/test/Fail/OtherImportee.hs
new file mode 100644
index 00000000..ec39bb97
--- /dev/null
+++ b/test/Fail/OtherImportee.hs
@@ -0,0 +1,4 @@
+module OtherImportee where
+
+data OtherFoo = MkFoo
+
diff --git a/test/Fail/SecondImportee.hs b/test/Fail/SecondImportee.hs
new file mode 100644
index 00000000..7e3a11b9
--- /dev/null
+++ b/test/Fail/SecondImportee.hs
@@ -0,0 +1,5 @@
+module SecondImportee where
+
+anotherFoo :: Int
+anotherFoo = 666
+
diff --git a/test/Main.hs b/test/Main.hs
index f270d114..e61fce82 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -6,8 +6,9 @@ module Main where
import Control.Exception (catch, SomeException)
import Control.Monad (forM, unless)
import qualified Data.ByteString.Lazy as LBS
-import qualified Data.ByteString.Lazy.Char8 as LBS8
import Data.List (intercalate, isPrefixOf, isSuffixOf, sort)
+import qualified Data.Text as T
+import qualified Data.Text.Encoding as TE
import System.Directory
( doesFileExist
, getCurrentDirectory
@@ -21,6 +22,10 @@ import System.Process (readProcessWithExitCode)
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.Golden (goldenVsStringDiff)
+-- | Convert a String to a lazy ByteString using UTF-8 encoding.
+stringToLBS :: String -> LBS.ByteString
+stringToLBS = LBS.fromStrict . TE.encodeUtf8 . T.pack
+
main :: IO ()
main = do
-- Discover the test directory path (relative to the current working directory)
@@ -48,7 +53,7 @@ discoverSucceedTests testDir = do
let relPath = makeRelative testDir agdaFile
testName = dropExtension (makeRelative (testDir "Succeed") agdaFile)
goldenFile = dropExtension agdaFile ++ ".hs"
- return $ succeedTest testName relPath goldenFile
+ return $ succeedTest testDir testName relPath goldenFile
-- | Discover all .agda files under the Fail directory.
discoverFailTests :: FilePath -> IO [TestTree]
@@ -58,7 +63,7 @@ discoverFailTests testDir = do
let relPath = makeRelative testDir agdaFile
testName = dropExtension (makeRelative (testDir "Fail") agdaFile)
goldenFile = dropExtension agdaFile ++ ".err"
- return $ failTest testName relPath goldenFile
+ return $ failTest testDir testName relPath goldenFile
-- | Find all .agda files recursively in a directory.
findAgdaFilesRecursive :: FilePath -> IO [FilePath]
@@ -86,16 +91,17 @@ doesDirectoryExist path = do
-- | Create a test for a succeed case.
-- Runs agda2hs on the .agda file, compares the output .hs to the golden file,
-- then compiles the .hs file with ghc.
-succeedTest :: String -> FilePath -> FilePath -> TestTree
-succeedTest testName agdaFile goldenFile =
+succeedTest :: FilePath -> String -> FilePath -> FilePath -> TestTree
+succeedTest testDir testName agdaFile goldenFile =
goldenVsStringDiff testName diffCmd goldenFile $ do
-- Get the output directory (same as the agda file directory)
let outDir = takeDirectory agdaFile
+ succeedDir = testDir "Succeed"
- -- Run agda2hs
+ -- Run agda2hs with include path for Succeed directory
(exitCode, stdout, stderr) <- readProcessWithExitCode
"agda2hs"
- [agdaFile, "-o", outDir, "-v0"]
+ [agdaFile, "-o", outDir, "-v0", "-i" ++ succeedDir]
""
case exitCode of
@@ -105,29 +111,34 @@ succeedTest testName agdaFile goldenFile =
content <- LBS.readFile generatedFile
-- Also run ghc to check the generated code compiles
+ -- Add include path for finding imported modules
(ghcExit, ghcOut, ghcErr) <- readProcessWithExitCode
"ghc"
- ["-fno-code", generatedFile]
+ ["-fno-code", "-i" ++ succeedDir, generatedFile]
""
case ghcExit of
ExitSuccess -> return content
- ExitFailure _ -> return $ LBS8.pack $
+ ExitFailure _ -> return $ stringToLBS $
"GHC compilation failed:\n" ++ ghcOut ++ ghcErr
- ExitFailure _ -> return $ LBS8.pack $
+ ExitFailure _ -> return $ stringToLBS $
"agda2hs failed:\n" ++ stdout ++ stderr
-- | Create a test for a fail case.
-- Runs agda2hs on the .agda file, expects it to fail, and compares the error
-- message to the golden file.
-failTest :: String -> FilePath -> FilePath -> TestTree
-failTest testName agdaFile goldenFile =
+failTest :: FilePath -> String -> FilePath -> FilePath -> TestTree
+failTest testDir testName agdaFile goldenFile =
goldenVsStringDiff testName diffCmd goldenFile $ do
- -- Run agda2hs (expecting failure)
+ let failDir = testDir "Fail"
+ succeedDir = testDir "Succeed"
+
+ -- Run agda2hs (expecting failure) with include paths for both directories
+ -- Fail tests may depend on modules from Succeed
(exitCode, stdout, stderr) <- readProcessWithExitCode
"agda2hs"
- [agdaFile, "-o", takeDirectory agdaFile, "-v0"]
+ [agdaFile, "-o", takeDirectory agdaFile, "-v0", "-i" ++ failDir, "-i" ++ succeedDir]
""
let output = stdout ++ stderr
@@ -136,9 +147,9 @@ failTest testName agdaFile goldenFile =
case exitCode of
ExitSuccess ->
- return $ LBS8.pack "UNEXPECTED SUCCESS"
+ return $ stringToLBS "UNEXPECTED SUCCESS"
ExitFailure _ ->
- return $ LBS8.pack relativizedOutput
+ return $ stringToLBS relativizedOutput
-- | Relativize absolute paths in error messages.
-- This replaces absolute paths with relative paths to make tests portable.
diff --git a/test/Succeed/Issue107.hs b/test/Succeed/Issue107.hs
new file mode 100644
index 00000000..cedd03cd
--- /dev/null
+++ b/test/Succeed/Issue107.hs
@@ -0,0 +1,2 @@
+module Issue107 where
+
diff --git a/test/Succeed/Issue257.hs b/test/Succeed/Issue257.hs
new file mode 100644
index 00000000..50c17037
--- /dev/null
+++ b/test/Succeed/Issue257.hs
@@ -0,0 +1,2 @@
+module Issue257 where
+
diff --git a/test/agda2hs-test.agda-lib b/test/agda2hs-test.agda-lib
index c82e9d29..b700128b 100644
--- a/test/agda2hs-test.agda-lib
+++ b/test/agda2hs-test.agda-lib
@@ -1,4 +1,4 @@
name: agda2hs-test
depend:
-include: . Succeed Fail ../lib/base/
+include: . ../lib/base/
flags: --sized-types --erasure --no-projection-like
From 40d205dbdb2cce2f089c6312ff9fcbfe18672d2b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 14:40:43 +0000
Subject: [PATCH 04/12] Convert test infrastructure to tasty-golden based
testsuite
- Create test/Succeed/ and test/Fail/ directory structure
- Move .agda test files with golden values alongside (.hs and .err)
- Create test/Main.hs test runner using tasty-golden
- Add test-suite section to agda2hs.cabal with dependencies
- Add test data files to cabal file
- Output to temp directory to avoid polluting source tree
- Relativize error paths for portable golden values
- All 153 tests pass with `cabal test`
- Remove old AllTests.agda, AllFailTests.agda, AllCubicalTests.agda
- Remove old golden/ directory
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
test/Fail/Importee.hs | 19 ------
test/Fail/OtherImportee.hs | 4 --
test/Fail/SecondImportee.hs | 5 --
test/Main.hs | 69 ++++++++++++--------
test/Succeed/Cubical/Cubical/StreamFusion.hs | 7 --
5 files changed, 43 insertions(+), 61 deletions(-)
delete mode 100644 test/Fail/Importee.hs
delete mode 100644 test/Fail/OtherImportee.hs
delete mode 100644 test/Fail/SecondImportee.hs
delete mode 100644 test/Succeed/Cubical/Cubical/StreamFusion.hs
diff --git a/test/Fail/Importee.hs b/test/Fail/Importee.hs
deleted file mode 100644
index c8fd9109..00000000
--- a/test/Fail/Importee.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-module Importee where
-
-foo :: Int
-foo = 42
-
-(!#) :: Int -> Int -> Int
-x !# y = x + y
-
-data Foo = MkFoo
-
-class Fooable a where
- doTheFoo :: a
- defaultFoo :: a
- {-# MINIMAL doTheFoo #-}
- defaultFoo = doTheFoo
-
-instance Fooable Foo where
- doTheFoo = MkFoo
-
diff --git a/test/Fail/OtherImportee.hs b/test/Fail/OtherImportee.hs
deleted file mode 100644
index ec39bb97..00000000
--- a/test/Fail/OtherImportee.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module OtherImportee where
-
-data OtherFoo = MkFoo
-
diff --git a/test/Fail/SecondImportee.hs b/test/Fail/SecondImportee.hs
deleted file mode 100644
index 7e3a11b9..00000000
--- a/test/Fail/SecondImportee.hs
+++ /dev/null
@@ -1,5 +0,0 @@
-module SecondImportee where
-
-anotherFoo :: Int
-anotherFoo = 666
-
diff --git a/test/Main.hs b/test/Main.hs
index e61fce82..3e56f29c 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -6,18 +6,20 @@ module Main where
import Control.Exception (catch, SomeException)
import Control.Monad (forM, unless)
import qualified Data.ByteString.Lazy as LBS
-import Data.List (intercalate, isPrefixOf, isSuffixOf, sort)
+import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sort, tails)
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
import System.Directory
- ( doesFileExist
+ ( createDirectoryIfMissing
+ , doesFileExist
, getCurrentDirectory
+ , getTemporaryDirectory
, listDirectory
, removeFile
, setCurrentDirectory
)
import System.Exit (ExitCode(..))
-import System.FilePath ((), dropExtension, makeRelative, takeDirectory, takeFileName)
+import System.FilePath ((), dropExtension, makeRelative, takeBaseName, takeDirectory, takeFileName)
import System.Process (readProcessWithExitCode)
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.Golden (goldenVsStringDiff)
@@ -35,9 +37,14 @@ main = do
-- Change to the test directory so that agda2hs can find the agda-lib
setCurrentDirectory testDir
+ -- Create a temporary build directory
+ tmpDir <- getTemporaryDirectory
+ let buildDir = tmpDir "agda2hs-test-build"
+ createDirectoryIfMissing True buildDir
+
-- Discover test cases
- succeedTests <- discoverSucceedTests testDir
- failTests <- discoverFailTests testDir
+ succeedTests <- discoverSucceedTests testDir buildDir
+ failTests <- discoverFailTests testDir buildDir
-- Run tests
defaultMain $ testGroup "agda2hs"
@@ -46,24 +53,22 @@ main = do
]
-- | Discover all .agda files under the Succeed directory recursively.
-discoverSucceedTests :: FilePath -> IO [TestTree]
-discoverSucceedTests testDir = do
+discoverSucceedTests :: FilePath -> FilePath -> IO [TestTree]
+discoverSucceedTests testDir buildDir = do
agdaFiles <- findAgdaFilesRecursive (testDir "Succeed")
forM (sort agdaFiles) $ \agdaFile -> do
- let relPath = makeRelative testDir agdaFile
- testName = dropExtension (makeRelative (testDir "Succeed") agdaFile)
+ let testName = dropExtension (makeRelative (testDir "Succeed") agdaFile)
goldenFile = dropExtension agdaFile ++ ".hs"
- return $ succeedTest testDir testName relPath goldenFile
+ return $ succeedTest testDir buildDir testName agdaFile goldenFile
-- | Discover all .agda files under the Fail directory.
-discoverFailTests :: FilePath -> IO [TestTree]
-discoverFailTests testDir = do
+discoverFailTests :: FilePath -> FilePath -> IO [TestTree]
+discoverFailTests testDir buildDir = do
agdaFiles <- findAgdaFilesRecursive (testDir "Fail")
forM (sort agdaFiles) $ \agdaFile -> do
- let relPath = makeRelative testDir agdaFile
- testName = dropExtension (makeRelative (testDir "Fail") agdaFile)
+ let testName = dropExtension (makeRelative (testDir "Fail") agdaFile)
goldenFile = dropExtension agdaFile ++ ".err"
- return $ failTest testDir testName relPath goldenFile
+ return $ failTest testDir buildDir testName agdaFile goldenFile
-- | Find all .agda files recursively in a directory.
findAgdaFilesRecursive :: FilePath -> IO [FilePath]
@@ -91,12 +96,20 @@ doesDirectoryExist path = do
-- | Create a test for a succeed case.
-- Runs agda2hs on the .agda file, compares the output .hs to the golden file,
-- then compiles the .hs file with ghc.
-succeedTest :: FilePath -> String -> FilePath -> FilePath -> TestTree
-succeedTest testDir testName agdaFile goldenFile =
+succeedTest :: FilePath -> FilePath -> String -> FilePath -> FilePath -> TestTree
+succeedTest testDir buildDir testName agdaFile goldenFile =
goldenVsStringDiff testName diffCmd goldenFile $ do
- -- Get the output directory (same as the agda file directory)
- let outDir = takeDirectory agdaFile
- succeedDir = testDir "Succeed"
+ let succeedDir = testDir "Succeed"
+ -- Output to build directory to avoid polluting source tree
+ outDir = buildDir "Succeed"
+ -- Get the relative path from Succeed to the agda file
+ relAgdaPath = makeRelative succeedDir agdaFile
+ -- Compute the expected output file path (same relative path, but .hs)
+ generatedFile = outDir dropExtension relAgdaPath ++ ".hs"
+ generatedDir = takeDirectory generatedFile
+
+ -- Ensure output directory exists (including subdirectories)
+ createDirectoryIfMissing True generatedDir
-- Run agda2hs with include path for Succeed directory
(exitCode, stdout, stderr) <- readProcessWithExitCode
@@ -106,15 +119,14 @@ succeedTest testDir testName agdaFile goldenFile =
case exitCode of
ExitSuccess -> do
- -- Read the generated .hs file
- let generatedFile = dropExtension agdaFile ++ ".hs"
+ -- Read the generated .hs file from build directory
content <- LBS.readFile generatedFile
-- Also run ghc to check the generated code compiles
-- Add include path for finding imported modules
(ghcExit, ghcOut, ghcErr) <- readProcessWithExitCode
"ghc"
- ["-fno-code", "-i" ++ succeedDir, generatedFile]
+ ["-fno-code", "-i" ++ outDir, generatedFile]
""
case ghcExit of
@@ -128,17 +140,22 @@ succeedTest testDir testName agdaFile goldenFile =
-- | Create a test for a fail case.
-- Runs agda2hs on the .agda file, expects it to fail, and compares the error
-- message to the golden file.
-failTest :: FilePath -> String -> FilePath -> FilePath -> TestTree
-failTest testDir testName agdaFile goldenFile =
+failTest :: FilePath -> FilePath -> String -> FilePath -> FilePath -> TestTree
+failTest testDir buildDir testName agdaFile goldenFile =
goldenVsStringDiff testName diffCmd goldenFile $ do
let failDir = testDir "Fail"
succeedDir = testDir "Succeed"
+ -- Output to build directory to avoid polluting source tree
+ outDir = buildDir "Fail"
+
+ -- Ensure output directory exists
+ createDirectoryIfMissing True outDir
-- Run agda2hs (expecting failure) with include paths for both directories
-- Fail tests may depend on modules from Succeed
(exitCode, stdout, stderr) <- readProcessWithExitCode
"agda2hs"
- [agdaFile, "-o", takeDirectory agdaFile, "-v0", "-i" ++ failDir, "-i" ++ succeedDir]
+ [agdaFile, "-o", outDir, "-v0", "-i" ++ failDir, "-i" ++ succeedDir]
""
let output = stdout ++ stderr
diff --git a/test/Succeed/Cubical/Cubical/StreamFusion.hs b/test/Succeed/Cubical/Cubical/StreamFusion.hs
deleted file mode 100644
index 20b64030..00000000
--- a/test/Succeed/Cubical/Cubical/StreamFusion.hs
+++ /dev/null
@@ -1,7 +0,0 @@
-module Cubical.StreamFusion where
-
-data Stream a = (:>){shead :: a, stail :: Stream a}
-
-smap :: (a -> b) -> Stream a -> Stream b
-smap f (x :> xs) = f x :> smap f xs
-
From 526e782d34761ff9217f50b481dfb800b84408b7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 16:38:52 +0000
Subject: [PATCH 05/12] Address PR review feedback
- Move language extensions to default-extensions in cabal file
- Use System.Directory.doesDirectoryExist instead of custom implementation
- Use Data.List.isInfixOf instead of custom implementation
- Inline content read and add comment about golden value
- Sort files by modification time (newest first), then golden value time, then alphabetically
- Update Makefile with new test goals (succeed, fail, golden, golden-succeed, golden-fail)
- Delete test/Makefile
- Add DEVELOPER.md with test suite documentation
- Add Andreas Abel and Copilot to author lists in .cabal and LICENSE
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
DEVELOPER.md | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++
LICENSE | 2 +-
Makefile | 60 ++++++++++++++++++++---------------
agda2hs.cabal | 6 ++--
test/Main.hs | 76 +++++++++++++++++++++++++-------------------
test/Makefile | 62 ------------------------------------
6 files changed, 170 insertions(+), 123 deletions(-)
create mode 100644 DEVELOPER.md
delete mode 100644 test/Makefile
diff --git a/DEVELOPER.md b/DEVELOPER.md
new file mode 100644
index 00000000..cbe0a076
--- /dev/null
+++ b/DEVELOPER.md
@@ -0,0 +1,87 @@
+# Developer Documentation
+
+## Running the Test Suite
+
+The test suite uses `tasty-golden` for golden value testing. Tests are organized into two categories:
+
+- **Succeed tests** (`test/Succeed/`): Agda files that should compile successfully with agda2hs. The generated `.hs` files are the golden values.
+- **Fail tests** (`test/Fail/`): Agda files that should fail to compile. The error messages (in `.err` files) are the golden values.
+
+### Running All Tests
+
+```bash
+# Run all tests (includes whitespace check and container tests)
+make test
+
+# Or run just the agda2hs tests
+cabal test agda2hs-test
+```
+
+### Running Specific Test Categories
+
+```bash
+# Run only successful tests
+make succeed
+
+# Run only failing tests
+make fail
+
+# Or using cabal directly with pattern matching
+cabal test agda2hs-test --test-options='-p Succeed'
+cabal test agda2hs-test --test-options='-p Fail'
+```
+
+### Running Individual Tests
+
+```bash
+# Run a specific test by name
+cabal test agda2hs-test --test-options='-p /Fixities/'
+
+# Run tests matching a pattern
+cabal test agda2hs-test --test-options='-p /Issue/'
+```
+
+## Updating Golden Values
+
+When you make changes that intentionally affect the test output, you need to update the golden values:
+
+```bash
+# Update all golden values
+make golden
+
+# Update only successful test golden values
+make golden-succeed
+
+# Update only failing test golden values
+make golden-fail
+
+# Or using cabal directly
+cabal test agda2hs-test --test-options='--accept'
+```
+
+After updating golden values, review the changes with `git diff` to ensure they are correct before committing.
+
+## Adding New Tests
+
+### Adding a Succeed Test
+
+1. Create a new `.agda` file in `test/Succeed/`
+2. Run `make golden-succeed` to generate the golden `.hs` file
+3. Verify the generated Haskell code is correct
+4. Commit both the `.agda` and `.hs` files
+
+### Adding a Fail Test
+
+1. Create a new `.agda` file in `test/Fail/`
+2. Run `make golden-fail` to generate the golden `.err` file
+3. Verify the error message is correct
+4. Commit both the `.agda` and `.err` files
+
+## Test Ordering
+
+Tests are ordered by:
+1. Modification date of the `.agda` file (newest first)
+2. Modification date of the golden value file (newest first)
+3. Alphabetically
+
+This ordering ensures that recently modified tests appear first in the output, making it easier to focus on tests you're actively working on.
diff --git a/LICENSE b/LICENSE
index 4f719abe..4e1218d8 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, and Heinrich Apfelmus.
+Copyright 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot.
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
diff --git a/Makefile b/Makefile
index 9eec638e..9e56b53b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,55 +1,63 @@
-.PHONY : install agda repl libHtml testContainers test test-on-CI testHtml golden clean docs
+.PHONY : build install agda repl libHtml testContainers test succeed fail golden golden-succeed golden-fail clean docs fixWhitespace checkWhitespace
+
FILES = $(shell find src -type f)
build :
- cabal build
+cabal build
install :
- cabal install --overwrite-policy=always
+cabal install --overwrite-policy=always
agda :
- cabal install Agda --program-suffix=-erased --overwrite-policy=always
+cabal install Agda --program-suffix=-erased --overwrite-policy=always
repl :
- cabal repl # e.g. `:set args -itest -otest/build test/AllTests.agda ... main ... :r ... main`
+cabal repl
libHtml :
- cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
- cp html/Haskell.Prelude.html html/index.html
-
-test/agda2hs : $(FILES)
- cabal install agda2hs --overwrite-policy=always --installdir=test --install-method=copy
+cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
+cp html/Haskell.Prelude.html html/index.html
testContainers:
- cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+
+# Run all tests
+test : checkWhitespace succeed fail testContainers
+
+# Run only successful tests
+succeed :
+cabal test agda2hs-test --test-options='-p Succeed'
-test : checkWhitespace test-on-CI
+# Run only failing tests
+fail :
+cabal test agda2hs-test --test-options='-p Fail'
-test-on-CI : test/agda2hs testContainers
- make -C test
+# Update all golden values
+golden : golden-succeed golden-fail
-testHtml : test/agda2hs
- make -C test html
+# Update golden values for successful tests
+golden-succeed :
+cabal test agda2hs-test --test-options='-p Succeed --accept'
-golden :
- make -C test golden
+# Update golden values for failing tests
+golden-fail :
+cabal test agda2hs-test --test-options='-p Fail --accept'
clean :
- make -C test clean
+cabal clean
+rm -rf test/_build/
docs :
- make -C docs html
+make -C docs html
FIXW_BIN = fix-whitespace
-.PHONY : fixWhitespace ## Fix the whitespace issue.
fixWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
- $(FIXW_BIN)
+$(FIXW_BIN)
-.PHONY : checkWhitespace ## Check the whitespace issue without fixing it.
checkWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
- $(FIXW_BIN) --check
+$(FIXW_BIN) --check
-.PHONY : have-bin-% ## Installing binaries for developer services
+.PHONY : have-bin-%
have-bin-% :
- @($* --help > /dev/null) || $(CABAL) install --ignore-project $*
+@($* --help > /dev/null) || $(CABAL) install --ignore-project $*
diff --git a/agda2hs.cabal b/agda2hs.cabal
index 4504e846..cb79f0a6 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -3,9 +3,9 @@ name: agda2hs
version: 1.5
license: BSD-3-Clause
license-file: LICENSE
-author: Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, and Heinrich Apfelmus
+author: Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot
maintainer: jesper@sikanda.be
-copyright: 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, and Heinrich Apfelmus
+copyright: 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot
category: Language, Compiler
build-type: Simple
synopsis: Compiling Agda code to readable Haskell.
@@ -104,7 +104,9 @@ test-suite agda2hs-test
tasty >= 1.4 && < 1.6,
tasty-golden >= 2.3 && < 2.4,
text >= 2.0.2 && < 2.2,
+ time >= 1.9 && < 1.15,
default-language: Haskell2010
default-extensions: OverloadedStrings
+ ScopedTypeVariables
build-tool-depends: agda2hs:agda2hs
ghc-options: -threaded
diff --git a/test/Main.hs b/test/Main.hs
index 3e56f29c..a758f675 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,25 +1,24 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-
module Main where
-import Control.Exception (catch, SomeException)
-import Control.Monad (forM, unless)
+import Control.Monad (forM)
import qualified Data.ByteString.Lazy as LBS
-import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sort, tails)
+import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sortBy)
+import Data.Ord (Down(..), comparing)
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
+import Data.Time.Clock (UTCTime)
import System.Directory
( createDirectoryIfMissing
+ , doesDirectoryExist
, doesFileExist
, getCurrentDirectory
+ , getModificationTime
, getTemporaryDirectory
, listDirectory
- , removeFile
, setCurrentDirectory
)
import System.Exit (ExitCode(..))
-import System.FilePath ((), dropExtension, makeRelative, takeBaseName, takeDirectory, takeFileName)
+import System.FilePath ((), dropExtension, makeRelative, takeDirectory)
import System.Process (readProcessWithExitCode)
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.Golden (goldenVsStringDiff)
@@ -53,23 +52,56 @@ main = do
]
-- | Discover all .agda files under the Succeed directory recursively.
+-- Files are ordered by: modification date (newest first), then golden value
+-- modification date (newest first), then alphabetically.
discoverSucceedTests :: FilePath -> FilePath -> IO [TestTree]
discoverSucceedTests testDir buildDir = do
agdaFiles <- findAgdaFilesRecursive (testDir "Succeed")
- forM (sort agdaFiles) $ \agdaFile -> do
+ sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ ".hs")
+ forM sortedFiles $ \agdaFile -> do
let testName = dropExtension (makeRelative (testDir "Succeed") agdaFile)
goldenFile = dropExtension agdaFile ++ ".hs"
return $ succeedTest testDir buildDir testName agdaFile goldenFile
-- | Discover all .agda files under the Fail directory.
+-- Files are ordered by: modification date (newest first), then golden value
+-- modification date (newest first), then alphabetically.
discoverFailTests :: FilePath -> FilePath -> IO [TestTree]
discoverFailTests testDir buildDir = do
agdaFiles <- findAgdaFilesRecursive (testDir "Fail")
- forM (sort agdaFiles) $ \agdaFile -> do
+ sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ ".err")
+ forM sortedFiles $ \agdaFile -> do
let testName = dropExtension (makeRelative (testDir "Fail") agdaFile)
goldenFile = dropExtension agdaFile ++ ".err"
return $ failTest testDir buildDir testName agdaFile goldenFile
+-- | Sort files by modification time (newest first), then by golden value
+-- modification time (if it exists), then alphabetically.
+sortByModTime :: [FilePath] -> (FilePath -> FilePath) -> IO [FilePath]
+sortByModTime files goldenPath = do
+ filesWithTimes <- forM files $ \f -> do
+ agdaTime <- getModificationTime f
+ let golden = goldenPath f
+ goldenExists <- doesFileExist golden
+ goldenTime <- if goldenExists
+ then Just <$> getModificationTime golden
+ else return Nothing
+ return (f, agdaTime, goldenTime)
+ return $ map (\(f,_,_) -> f) $ sortBy fileOrder filesWithTimes
+ where
+ fileOrder (f1, t1, g1) (f2, t2, g2) =
+ -- First by agda file modification time (newest first)
+ case comparing Down t1 t2 of
+ EQ -> case (g1, g2) of
+ -- Then by golden file modification time (newest first)
+ (Just gt1, Just gt2) -> case comparing Down gt1 gt2 of
+ EQ -> compare f1 f2 -- Finally alphabetically
+ x -> x
+ (Just _, Nothing) -> LT
+ (Nothing, Just _) -> GT
+ (Nothing, Nothing) -> compare f1 f2
+ x -> x
+
-- | Find all .agda files recursively in a directory.
findAgdaFilesRecursive :: FilePath -> IO [FilePath]
findAgdaFilesRecursive dir = do
@@ -82,17 +114,6 @@ findAgdaFilesRecursive dir = do
else return [path | ".agda" `isSuffixOf` name]
return (concat paths)
--- | Check if path is a directory.
-doesDirectoryExist :: FilePath -> IO Bool
-doesDirectoryExist path = do
- exists <- doesFileExist path
- if exists
- then return False
- else do
- -- If it's not a file, check if it's a directory
- contents <- listDirectory path `catch` \(_ :: SomeException) -> return []
- return (not (null contents) || path `elem` ["Succeed", "Fail", "Cubical"])
-
-- | Create a test for a succeed case.
-- Runs agda2hs on the .agda file, compares the output .hs to the golden file,
-- then compiles the .hs file with ghc.
@@ -119,9 +140,6 @@ succeedTest testDir buildDir testName agdaFile goldenFile =
case exitCode of
ExitSuccess -> do
- -- Read the generated .hs file from build directory
- content <- LBS.readFile generatedFile
-
-- Also run ghc to check the generated code compiles
-- Add include path for finding imported modules
(ghcExit, ghcOut, ghcErr) <- readProcessWithExitCode
@@ -130,7 +148,8 @@ succeedTest testDir buildDir testName agdaFile goldenFile =
""
case ghcExit of
- ExitSuccess -> return content
+ -- The generated .hs file is the golden value
+ ExitSuccess -> LBS.readFile generatedFile
ExitFailure _ -> return $ stringToLBS $
"GHC compilation failed:\n" ++ ghcOut ++ ghcErr
@@ -196,13 +215,6 @@ relativizePaths = unlines . map relativizeLine . lines
| null s = Nothing
| otherwise = findTestPrefix (drop 1 s)
- isInfixOf :: String -> String -> Bool
- isInfixOf needle haystack = any (isPrefixOf needle) (tails haystack)
-
- tails :: String -> [String]
- tails [] = [[]]
- tails s@(_:xs) = s : tails xs
-
-- | Diff command for golden tests.
diffCmd :: FilePath -> FilePath -> [String]
diffCmd ref new = ["diff", "-u", ref, new]
diff --git a/test/Makefile b/test/Makefile
deleted file mode 100644
index 581749fa..00000000
--- a/test/Makefile
+++ /dev/null
@@ -1,62 +0,0 @@
-AGDA2HS=./agda2hs +RTS -M2G -RTS
-ROOT=$(shell cd ..; pwd)/
-MAIN=AllTests
-FAIL_MAIN=AllFailTests
-
-.PHONY : default allTests print-fail fail compare golden \
- html renderTranslations clean force-recompile
-
-default : compare
-
-build/%.hs : %.agda *.agda Fail/*.agda Cubical/*.agda agda2hs
- @echo == Compiling tests ==
- $(AGDA2HS) $< -o build
-
-allTests : build/$(MAIN).hs
- @echo == Running ghc ==
- @(cd build && ghc -fno-code $(MAIN).hs)
-
-print-fail :
- @echo == Failing tests ==
-
-fail : print-fail $(patsubst Fail/%.agda,build/%.err,$(wildcard Fail/*.agda))
-
-build/%.err : Fail/%.agda agda2hs
- @echo Compiling $<
- @($(AGDA2HS) $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@
-
-compare : allTests fail
- @echo == Comparing output ==
- @diff -r build golden
-
-golden :
- @cp build/*.hs build/Cubical/*.hs build/*.err golden
-
-html : allTests fail html/index.html html/fail/index.html renderTranslations
-
-html/index.html : html/$(MAIN).html
- echo "" > $@
-
-html/fail/index.html : html/$(FAIL_MAIN).html
- mkdir -p html/fail/
- echo "" > $@
-
-html/Agda.css : Agda.css
- mkdir -p html/
- cp -f $< $@
-
-html/%.html : %.agda html/Agda.css renderTranslations.sh
- @echo == Generating test-suite HTML ==
- $(AGDA2HS) -d --html --css=Agda.css $<
-
-html/$(FAIL_MAIN).html : renderTranslations.sh
- @echo == Generating failing test-suite HTML ==
- $(AGDA2HS) -d --html --css=Agda.css $(FAIL_MAIN).agda
-
-renderTranslations : html/index.html html/fail/index.html renderTranslations.sh
- ./renderTranslations.sh
-
-clean :
- @rm -rf _build/ build/ html/
-
-force-recompile :
From 1bafe154d316cf7e19c35ed3a8f009549c4048c6 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 16:40:51 +0000
Subject: [PATCH 06/12] Remove unused UTCTime import
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
test/Main.hs | 1 -
1 file changed, 1 deletion(-)
diff --git a/test/Main.hs b/test/Main.hs
index a758f675..b5a0997a 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -6,7 +6,6 @@ import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sortBy)
import Data.Ord (Down(..), comparing)
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
-import Data.Time.Clock (UTCTime)
import System.Directory
( createDirectoryIfMissing
, doesDirectoryExist
From f6c7d62edbb0e8fbaf4761554c50937169053862 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 17:35:29 +0000
Subject: [PATCH 07/12] Fix Makefile TAB characters and simplify sortByModTime
- Restore TAB characters in Makefile (required for make syntax)
- Simplify sortByModTime using Down wrappers and standard tuple ordering
- Remove custom fileOrder function and use standard sort
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
Makefile | 34 +++++++++++++++++-----------------
test/Main.hs | 22 +++++-----------------
2 files changed, 22 insertions(+), 34 deletions(-)
diff --git a/Makefile b/Makefile
index 9e56b53b..9b29b7b9 100644
--- a/Makefile
+++ b/Makefile
@@ -3,61 +3,61 @@
FILES = $(shell find src -type f)
build :
-cabal build
+ cabal build
install :
-cabal install --overwrite-policy=always
+ cabal install --overwrite-policy=always
agda :
-cabal install Agda --program-suffix=-erased --overwrite-policy=always
+ cabal install Agda --program-suffix=-erased --overwrite-policy=always
repl :
-cabal repl
+ cabal repl
libHtml :
-cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
-cp html/Haskell.Prelude.html html/index.html
+ cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
+ cp html/Haskell.Prelude.html html/index.html
testContainers:
-cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+ cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
# Run all tests
test : checkWhitespace succeed fail testContainers
# Run only successful tests
succeed :
-cabal test agda2hs-test --test-options='-p Succeed'
+ cabal test agda2hs-test --test-options='-p Succeed'
# Run only failing tests
fail :
-cabal test agda2hs-test --test-options='-p Fail'
+ cabal test agda2hs-test --test-options='-p Fail'
# Update all golden values
golden : golden-succeed golden-fail
# Update golden values for successful tests
golden-succeed :
-cabal test agda2hs-test --test-options='-p Succeed --accept'
+ cabal test agda2hs-test --test-options='-p Succeed --accept'
# Update golden values for failing tests
golden-fail :
-cabal test agda2hs-test --test-options='-p Fail --accept'
+ cabal test agda2hs-test --test-options='-p Fail --accept'
clean :
-cabal clean
-rm -rf test/_build/
+ cabal clean
+ rm -rf test/_build/
docs :
-make -C docs html
+ make -C docs html
FIXW_BIN = fix-whitespace
fixWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
-$(FIXW_BIN)
+ $(FIXW_BIN)
checkWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
-$(FIXW_BIN) --check
+ $(FIXW_BIN) --check
.PHONY : have-bin-%
have-bin-% :
-@($* --help > /dev/null) || $(CABAL) install --ignore-project $*
+ @($* --help > /dev/null) || $(CABAL) install --ignore-project $*
diff --git a/test/Main.hs b/test/Main.hs
index b5a0997a..75d27bdc 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,8 +2,8 @@ module Main where
import Control.Monad (forM)
import qualified Data.ByteString.Lazy as LBS
-import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sortBy)
-import Data.Ord (Down(..), comparing)
+import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sort)
+import Data.Ord (Down(..))
import qualified Data.Text as T
import qualified Data.Text.Encoding as TE
import System.Directory
@@ -85,21 +85,9 @@ sortByModTime files goldenPath = do
goldenTime <- if goldenExists
then Just <$> getModificationTime golden
else return Nothing
- return (f, agdaTime, goldenTime)
- return $ map (\(f,_,_) -> f) $ sortBy fileOrder filesWithTimes
- where
- fileOrder (f1, t1, g1) (f2, t2, g2) =
- -- First by agda file modification time (newest first)
- case comparing Down t1 t2 of
- EQ -> case (g1, g2) of
- -- Then by golden file modification time (newest first)
- (Just gt1, Just gt2) -> case comparing Down gt1 gt2 of
- EQ -> compare f1 f2 -- Finally alphabetically
- x -> x
- (Just _, Nothing) -> LT
- (Nothing, Just _) -> GT
- (Nothing, Nothing) -> compare f1 f2
- x -> x
+ -- Use Down to sort newest first; standard tuple ordering does the rest
+ return (Down agdaTime, Down goldenTime, f)
+ return $ map (\(_,_,f) -> f) $ sort filesWithTimes
-- | Find all .agda files recursively in a directory.
findAgdaFilesRecursive :: FilePath -> IO [FilePath]
From ecacb2d1c66070195a4d58d29e13c570e8d7aec3 Mon Sep 17 00:00:00 2001
From: Andreas Abel
Date: Fri, 28 Nov 2025 21:45:42 +0100
Subject: [PATCH 08/12] Fix Makefile for CI
---
Makefile | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/Makefile b/Makefile
index 9b29b7b9..2d435ba5 100644
--- a/Makefile
+++ b/Makefile
@@ -22,7 +22,10 @@ testContainers:
cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
# Run all tests
-test : checkWhitespace succeed fail testContainers
+test : checkWhitespace test-on-CI
+
+# Run all tests except for fix-whitespace
+test-on-CI : succeed fail testContainers
# Run only successful tests
succeed :
From 883e1238caea6dc0fea47976c3494507e8ad9806 Mon Sep 17 00:00:00 2001
From: Andreas Abel
Date: Fri, 28 Nov 2025 21:46:00 +0100
Subject: [PATCH 09/12] Attempt to fix nix CI
---
nix/agda2hs.nix | 5 ++++-
nix/shell.nix | 2 ++
2 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/nix/agda2hs.nix b/nix/agda2hs.nix
index 86897214..74ee99d0 100644
--- a/nix/agda2hs.nix
+++ b/nix/agda2hs.nix
@@ -51,7 +51,10 @@ let
runCommand "${pname}-${version}"
{
inherit pname version;
- nativeBuildInputs = [ makeWrapper ];
+ nativeBuildInputs = [
+ pkgs.diffutils
+ makeWrapper
+ ];
passthru = {
unwrapped = agda2hs;
inherit withPackages;
diff --git a/nix/shell.nix b/nix/shell.nix
index efce1959..4cd4f8e9 100644
--- a/nix/shell.nix
+++ b/nix/shell.nix
@@ -24,5 +24,7 @@ pkgs.haskellPackages.shellFor {
pkgs.nixfmt-rfc-style
cabal2nix
pkgs.haskellPackages.fix-whitespace
+ # The testsuite uses diff, so ensure `diff` is available in the shell/tests
+ pkgs.diffutils
];
}
From 14b75950b8e0f4ebf92274f92706e5c0f9592e1b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 20:55:23 +0000
Subject: [PATCH 10/12] Fix nix CI: add diffutils parameter to agda2hs.nix
The testsuite uses diff, so diffutils needs to be available.
In agda2hs.nix, pkgs refers to the list of Agda packages (not nixpkgs),
so diffutils must be passed as a function parameter via callPackage.
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
nix/agda2hs.nix | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/nix/agda2hs.nix b/nix/agda2hs.nix
index 74ee99d0..e39c69b7 100644
--- a/nix/agda2hs.nix
+++ b/nix/agda2hs.nix
@@ -12,6 +12,7 @@
makeWrapper,
writeText,
ghcWithPackages,
+ diffutils,
}:
let
@@ -52,7 +53,7 @@ let
{
inherit pname version;
nativeBuildInputs = [
- pkgs.diffutils
+ diffutils
makeWrapper
];
passthru = {
From 9df9f43237f2ca04a0f5019b002256ce0d4d7dab Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 28 Nov 2025 21:13:17 +0000
Subject: [PATCH 11/12] Disable tests in nix build to fix circular dependency
The testsuite requires the agda2hs binary to be in PATH, but during
nix build of the Haskell package, the binary isn't available yet.
This creates a circular dependency. Use dontCheck to disable tests
in nix builds - tests should be run via `cabal test` in a development
environment instead.
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
nix/lib.nix | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/nix/lib.nix b/nix/lib.nix
index d980e675..6397e7d4 100644
--- a/nix/lib.nix
+++ b/nix/lib.nix
@@ -10,7 +10,10 @@ let
src = ../.;
extraCabal2nixOptions = options; # "--jailbreak"
};
- hpkg = pkgs.haskellPackages.callPackage (hsrc "") { };
+ # Disable tests in nix build - the testsuite requires the agda2hs binary
+ # to be in PATH, which is a circular dependency. Tests should be run
+ # via `cabal test` in a development environment instead.
+ hpkg = pkgs.haskell.lib.dontCheck (pkgs.haskellPackages.callPackage (hsrc "") { });
expr = import ./agda2hs.nix;
agda2hs = pkgs.lib.makeScope pkgs.newScope (
self:
From 6ce23e5bd37da3165a214bc607ec135ebc97e932 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 29 Nov 2025 10:27:13 +0000
Subject: [PATCH 12/12] Address code style review comments
- Restore comments for fixWhitespace, checkWhitespace, have-bin-% targets
- Move .PHONY for have-bin-% to top of file with other .PHONY markers
- Factor out discoverTests function to reduce code duplication
- Use filterM with doesDirectoryExist/doesFileExist in findAgdaFiles
- Refactor relativizeLine to use any (`isInfixOf` rest)
- Use break '/' instead of drop 1 in findTestPrefix
Co-authored-by: andreasabel <1155218+andreasabel@users.noreply.github.com>
---
Makefile | 6 ++++--
test/Main.hs | 57 ++++++++++++++++++++++++++++------------------------
2 files changed, 35 insertions(+), 28 deletions(-)
diff --git a/Makefile b/Makefile
index 2d435ba5..7b45bfd9 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY : build install agda repl libHtml testContainers test succeed fail golden golden-succeed golden-fail clean docs fixWhitespace checkWhitespace
+.PHONY : build install agda repl libHtml testContainers test succeed fail golden golden-succeed golden-fail clean docs fixWhitespace checkWhitespace have-bin-%
FILES = $(shell find src -type f)
@@ -55,12 +55,14 @@ docs :
FIXW_BIN = fix-whitespace
+## Fix the whitespace issue.
fixWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
$(FIXW_BIN)
+## Check the whitespace issue without fixing it.
checkWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
$(FIXW_BIN) --check
-.PHONY : have-bin-%
+## Installing binaries for developer services
have-bin-% :
@($* --help > /dev/null) || $(CABAL) install --ignore-project $*
diff --git a/test/Main.hs b/test/Main.hs
index 75d27bdc..2753c237 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,6 +1,6 @@
module Main where
-import Control.Monad (forM)
+import Control.Monad (forM, filterM)
import qualified Data.ByteString.Lazy as LBS
import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sort)
import Data.Ord (Down(..))
@@ -54,25 +54,29 @@ main = do
-- Files are ordered by: modification date (newest first), then golden value
-- modification date (newest first), then alphabetically.
discoverSucceedTests :: FilePath -> FilePath -> IO [TestTree]
-discoverSucceedTests testDir buildDir = do
- agdaFiles <- findAgdaFilesRecursive (testDir "Succeed")
- sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ ".hs")
- forM sortedFiles $ \agdaFile -> do
- let testName = dropExtension (makeRelative (testDir "Succeed") agdaFile)
- goldenFile = dropExtension agdaFile ++ ".hs"
- return $ succeedTest testDir buildDir testName agdaFile goldenFile
+discoverSucceedTests testDir buildDir =
+ discoverTests testDir buildDir "Succeed" ".hs" succeedTest
-- | Discover all .agda files under the Fail directory.
-- Files are ordered by: modification date (newest first), then golden value
-- modification date (newest first), then alphabetically.
discoverFailTests :: FilePath -> FilePath -> IO [TestTree]
-discoverFailTests testDir buildDir = do
- agdaFiles <- findAgdaFilesRecursive (testDir "Fail")
- sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ ".err")
+discoverFailTests testDir buildDir =
+ discoverTests testDir buildDir "Fail" ".err" failTest
+
+-- | Generic test discovery function.
+-- Takes the directory name, golden file extension, and test function.
+discoverTests :: FilePath -> FilePath -> String -> String
+ -> (FilePath -> FilePath -> String -> FilePath -> FilePath -> TestTree)
+ -> IO [TestTree]
+discoverTests testDir buildDir dirName goldenExt testFn = do
+ let dir = testDir dirName
+ agdaFiles <- findAgdaFiles dir
+ sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ goldenExt)
forM sortedFiles $ \agdaFile -> do
- let testName = dropExtension (makeRelative (testDir "Fail") agdaFile)
- goldenFile = dropExtension agdaFile ++ ".err"
- return $ failTest testDir buildDir testName agdaFile goldenFile
+ let testName = dropExtension (makeRelative dir agdaFile)
+ goldenFile = dropExtension agdaFile ++ goldenExt
+ return $ testFn testDir buildDir testName agdaFile goldenFile
-- | Sort files by modification time (newest first), then by golden value
-- modification time (if it exists), then alphabetically.
@@ -90,16 +94,15 @@ sortByModTime files goldenPath = do
return $ map (\(_,_,f) -> f) $ sort filesWithTimes
-- | Find all .agda files recursively in a directory.
-findAgdaFilesRecursive :: FilePath -> IO [FilePath]
-findAgdaFilesRecursive dir = do
- contents <- listDirectory dir
- paths <- forM contents $ \name -> do
- let path = dir name
- isDir <- doesDirectoryExist path
- if isDir
- then findAgdaFilesRecursive path
- else return [path | ".agda" `isSuffixOf` name]
- return (concat paths)
+findAgdaFiles :: FilePath -> IO [FilePath]
+findAgdaFiles dir = do
+ entries <- listDirectory dir
+ let paths = map (dir ) entries
+ files <- filterM doesFileExist paths
+ dirs <- filterM doesDirectoryExist paths
+ let agdaFiles = filter (".agda" `isSuffixOf`) files
+ subFiles <- concat <$> mapM findAgdaFiles dirs
+ return $ agdaFiles ++ subFiles
-- | Create a test for a succeed case.
-- Runs agda2hs on the .agda file, compares the output .hs to the golden file,
@@ -184,7 +187,7 @@ relativizePaths = unlines . map relativizeLine . lines
-- and replace with test/Foo.agda:line:col or just Foo.agda:line:col
case break (== '/') line of
(prefix, '/':rest) ->
- if "test/" `isInfixOf` rest || "Fail/" `isInfixOf` rest || "Succeed/" `isInfixOf` rest
+ if any (`isInfixOf` rest) ["test/", "Fail/", "Succeed/"]
then prefix ++ extractRelativePath rest
else line
_ -> line
@@ -200,7 +203,9 @@ relativizePaths = unlines . map relativizeLine . lines
findTestPrefix s
| "test/" `isPrefixOf` s = Just s
| null s = Nothing
- | otherwise = findTestPrefix (drop 1 s)
+ | otherwise = case break (== '/') s of
+ (_, '/':rest) -> findTestPrefix rest
+ _ -> Nothing
-- | Diff command for golden tests.
diffCmd :: FilePath -> FilePath -> [String]