From 5dc3eeba713d32bbc8a9c5b590c202540c8af41c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 17 Dec 2024 22:15:41 +0000 Subject: [PATCH] Add support for code auto-generation of records with non-dependent function fields --- docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda index 2911f971db..98149a3766 100644 --- a/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda +++ b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda @@ -241,6 +241,7 @@ private renderHsType (def (quote Pair) (_ ∷ _ ∷ vArg a ∷ vArg b ∷ [])) = printf "(%s, %s)" (renderHsType a) (renderHsType b) renderHsType (def d []) = renderHsTypeName d renderHsType (def d vs) = printf "(%s %s)" (renderHsTypeName d) (joinStrings " " (renderHsArgs vs)) + renderHsType (Π[ s ∶ arg _ a ] b) = printf "%s -> %s" (renderHsType a) (renderHsType b) renderHsType t = printf "(TODO: renderHsType %s)" (show t) renderHsArgs [] = [] @@ -269,14 +270,17 @@ private (showName d) con hsImports : String - hsImports = "import GHC.Generics (Generic)" + hsImports = "import GHC.Generics (Generic)\nimport Text.Show.Functions\n" + + hsInstances : String + hsInstances = "instance Eq (a -> b) where _ == _ = False\n" -- functions are never equal -- Take the name of a simple data type and generate the COMPILE and -- FOREIGN pragmas to bind to Haskell. bindHsType : NameEnv → Name → Name → TC ⊤ bindHsType env agdaName hsName = getDefinition hsName >>= λ where (data-type pars cs) → do - pragmaForeign "GHC" hsImports + pragmaForeign "GHC" (hsImports & "\n" & hsInstances) pragmaCompile "GHC" hsName $ compilePragma hsName cs getDefinition agdaName >>= λ where (data-type _ _) → pragmaForeign "GHC" =<< foreignPragma hsName cs