From f42ebab77aa49477de97d84213137b4b4cb9ab91 Mon Sep 17 00:00:00 2001
From: lemastero <piotr.paradzinski@iohk.io>
Date: Tue, 19 Dec 2023 02:23:58 +0100
Subject: [PATCH] compile record name

---
 src/Agda/Compiler/Rust/AgdaToRustExpr.hs      | 16 +++++++++++-----
 src/Agda/Compiler/Rust/PrettyPrintingUtils.hs |  9 ++++++---
 src/Agda/Compiler/Rust/RustExpr.hs            |  9 +++++----
 test/hello.agda                               | 10 +++++-----
 test/hello.rs                                 |  4 ++++
 5 files changed, 31 insertions(+), 17 deletions(-)

diff --git a/src/Agda/Compiler/Rust/AgdaToRustExpr.hs b/src/Agda/Compiler/Rust/AgdaToRustExpr.hs
index 3e63c95..45920c4 100644
--- a/src/Agda/Compiler/Rust/AgdaToRustExpr.hs
+++ b/src/Agda/Compiler/Rust/AgdaToRustExpr.hs
@@ -30,22 +30,28 @@ compile _ _ _ Defn{..}
 
 compileDefn :: QName -> Defn -> CompiledDef
 compileDefn defName theDef =
+  -- https://hackage.haskell.org/package/Agda/docs/Agda-Compiler-Backend.html#t:Defn
   case theDef of 
     Datatype{dataCons = fields} ->
       compileDataType defName fields
     Function{funCompiled = funDef, funClauses = fc} ->
       compileFunction defName funDef fc
-    _ ->
-      Unhandled "compileDefn" (show defName ++ " = " ++ show theDef)
+    RecordDefn(RecordData{_recFields = recFields, _recTel = recTel}) ->
+      compileRecord defName recFields recTel
+    other ->
+      Unhandled "compileDefn" (show defName ++ "\n = \n" ++ show theDef)
 
 compileDataType :: QName -> [QName] -> CompiledDef
-compileDataType defName fields = TeEnum (showName defName) (map showName fields)
+compileDataType defName fields = ReEnum (showName defName) (map showName fields)
+
+compileRecord :: QName -> [Dom QName] -> Telescope -> CompiledDef
+compileRecord defName recFields recTel = ReRec (showName defName) (prettyShow recTel)
 
 compileFunction :: QName
   -> Maybe CompiledClauses
   -> [Clause]
   -> CompiledDef
-compileFunction defName funDef fc = TeFun
+compileFunction defName funDef fc = ReFun
   (showName defName)
   (RustElem (compileFunctionArgument fc) (compileFunctionArgType fc))
   (compileFunctionResultType fc)
@@ -120,7 +126,7 @@ showName = prettyShow . qnameName
 
 compileModule :: TopLevelModuleName -> [CompiledDef] -> CompiledDef
 compileModule mName cdefs =
-  TeMod (moduleName mName) cdefs
+  ReMod (moduleName mName) cdefs
 
 moduleName :: TopLevelModuleName -> String
 moduleName n = prettyShow (Nel.last (moduleNameParts n))
diff --git a/src/Agda/Compiler/Rust/PrettyPrintingUtils.hs b/src/Agda/Compiler/Rust/PrettyPrintingUtils.hs
index f14e4d3..9501a80 100644
--- a/src/Agda/Compiler/Rust/PrettyPrintingUtils.hs
+++ b/src/Agda/Compiler/Rust/PrettyPrintingUtils.hs
@@ -6,7 +6,7 @@ import Agda.Compiler.Rust.RustExpr ( RustExpr(..), RustElem(..), FunBody )
 
 prettyPrintRustExpr :: CompiledDef -> String
 prettyPrintRustExpr def = case def of
-  (TeEnum name fields) ->
+  (ReEnum name fields) ->
     "enum" <> exprSeparator
       <> name
       <> exprSeparator
@@ -14,7 +14,7 @@ prettyPrintRustExpr def = case def of
         indent -- TODO this is too simplistic indentation
         <> concat (intersperse ", " fields))
       <> defsSeparator
-  (TeFun fName (RustElem aName aType) resType fBody) ->
+  (ReFun fName (RustElem aName aType) resType fBody) ->
       "pub fn" <> exprSeparator
         <> fName
         <> argList (
@@ -25,12 +25,15 @@ prettyPrintRustExpr def = case def of
         <> exprSeparator <> bracket (
         indent <> (prettyPrintFunctionBody fBody))
         <> defsSeparator
-  (TeMod mName defs) ->
+  (ReMod mName defs) ->
     moduleHeader mName
     <> bracket (
       defsSeparator -- empty line before first definition in module
       <> combineLines (map prettyPrintRustExpr defs))
     <> defsSeparator 
+  (ReRec name payload) -> "pub struct" <> exprSeparator <> name
+    <> exprSeparator <> (bracket payload)
+    <> defsSeparator
   (Unhandled name payload) -> ""
   -- XXX at the end there should be no Unhandled expression
   -- other -> "unsupported prettyPrintRustExpr " ++ (show other)
diff --git a/src/Agda/Compiler/Rust/RustExpr.hs b/src/Agda/Compiler/Rust/RustExpr.hs
index 3bdae4d..2f327ba 100644
--- a/src/Agda/Compiler/Rust/RustExpr.hs
+++ b/src/Agda/Compiler/Rust/RustExpr.hs
@@ -15,12 +15,13 @@ data RustElem = RustElem RustName RustType
   deriving ( Show )
 
 data RustExpr
-  = TeMod RustName [RustExpr]
-  | TeEnum RustName [RustName]
-  | TeFun RustName RustElem RustType FunBody
+  = ReMod RustName [RustExpr]
+  | ReEnum RustName [RustName]
+  | ReFun RustName RustElem RustType FunBody -- TODO [RustElem]
+  | ReRec RustName RustName -- TODO [RustElem]
   | Unhandled RustName String
   deriving ( Show )
 
 unHandled :: RustExpr -> Bool
-unHandled (Unhandled _ _) = True
+unHandled (Unhandled "" "") = True
 unHandled _               = False
diff --git a/test/hello.agda b/test/hello.agda
index c904561..be2aa2c 100644
--- a/test/hello.agda
+++ b/test/hello.agda
@@ -18,11 +18,11 @@ id_rgb x = x
 
 -- product types
 
--- record ThePair : Set where
---   field
---     pairFst : Rgb
---     pairSnd : WeekDay
--- {-# COMPILE AGDA2RUST ThePair #-}
+record ThePair : Set where
+  field
+    pairFst : Rgb
+    pairSnd : WeekDay
+{-# COMPILE AGDA2RUST ThePair #-}
 
 -- record Foo (A : Set) : Set where
 --   field
diff --git a/test/hello.rs b/test/hello.rs
index 6f5a207..5f9c865 100644
--- a/test/hello.rs
+++ b/test/hello.rs
@@ -12,5 +12,9 @@ pub fn id_rgb(x: Rgb) -> Rgb {
   return x;
 }
 
+pub struct ThePair {
+(pairFst : test.hello.Rgb) (pairSnd : test.hello.WeekDay)
+}
+
 
 }