fix function return types (broke during rebase)

lemastero · Dec 18, 2023 · aa6d090 · aa6d090
1 parent e4de243
commit aa6d090
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 25 deletions.
diff --git a/src/Agda/Compiler/Rust/PrettyPrintingUtils.hs b/src/Agda/Compiler/Rust/PrettyPrintingUtils.hs
@@ -1,9 +1,10 @@
 module Agda.Compiler.Rust.PrettyPrintingUtils (
   argList,
   bracket,
-  indent,
-  exprSeparator,
   defsSeparator,
+  exprSeparator,
+  funReturnTypeSeparator,
+  indent,
   typeSeparator
 ) where
 
@@ -24,3 +25,6 @@ defsSeparator = "\n"
 
 typeSeparator :: String
 typeSeparator = ":"
+
+funReturnTypeSeparator :: String
+funReturnTypeSeparator = "->"
diff --git a/src/Agda/Compiler/Rust/ToRustCompiler.hs b/src/Agda/Compiler/Rust/ToRustCompiler.hs
@@ -9,7 +9,7 @@ import qualified Data.List.NonEmpty as Nel
 import Agda.Compiler.Backend ( IsMain )
 import Agda.Syntax.Abstract.Name ( QName )
 import Agda.Syntax.Common.Pretty ( prettyShow )
-import Agda.Syntax.Common ( Arg(..), Named(..), ArgName )
+import Agda.Syntax.Common ( Arg(..), ArgName, Named(..), moduleNameParts )
 import Agda.Syntax.Internal (
   Clause(..), DeBruijnPattern, DBPatVar(..), Dom(..), unDom, PatternInfo(..), Pattern'(..),
   qnameName, qnameModule, Telescope, Tele(..), Term(..), Type, Type''(..) )
@@ -22,9 +22,10 @@ import Agda.Compiler.Rust.CommonTypes ( Options, CompiledDef, ModuleEnv )
 import Agda.Compiler.Rust.PrettyPrintingUtils (
   argList,
   bracket,
-  indent,
-  exprSeparator,
   defsSeparator,
+  exprSeparator,
+  funReturnTypeSeparator,
+  indent,
   typeSeparator )
 
 compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
@@ -64,10 +65,10 @@ compileFunction defName funDef fc =
     <> showName defName
     <> argList (
       -- TODO handle multiple function clauses and arguments
-      compileFunctionArgument (head fc)
+      compileFunctionArgument fc
       <> typeSeparator <> exprSeparator
-      <> compileFunctionArgType (head fc) )
-    <> typeSeparator <> exprSeparator <> compileFunctionResultType (head fc)
+      <> compileFunctionArgType fc )
+    <> exprSeparator <> funReturnTypeSeparator <> exprSeparator <> compileFunctionResultType fc
     <> exprSeparator <> bracket (
     -- TODO proper indentation for every line of function body
     -- including nested expressions
@@ -86,8 +87,9 @@ compileFunctionArgument [] = ""
 compileFunctionArgument [fc] = fromDeBruijnPattern (namedThing (unArg (head (namedClausePats fc))))
 compileFunctionArgument xs = error "unsupported compileFunctionArgument" ++ (show xs)
 
-compileFunctionArgType :: Clause -> CompiledDef
-compileFunctionArgType Clause{clauseTel = ct} = fromTelescope ct
+compileFunctionArgType :: [Clause] -> CompiledDef
+compileFunctionArgType [ Clause{clauseTel = ct} ] = fromTelescope ct
+compileFunctionArgType xs = error "unsupported compileFunctionArgType" ++ (show xs)
 
 fromTelescope :: Telescope -> CompiledDef
 fromTelescope = \case
@@ -97,8 +99,9 @@ fromTelescope = \case
 fromDom :: Dom Type -> CompiledDef
 fromDom x = fromType (unDom x)
 
-compileFunctionResultType :: Clause -> CompiledDef
-compileFunctionResultType Clause{clauseType = ct} = fromMaybeType ct
+compileFunctionResultType :: [Clause] -> CompiledDef
+compileFunctionResultType [Clause{clauseType = ct}] = fromMaybeType ct
+compileFunctionResultType other = error ("unhandled compileFunctionResultType" ++ show other)
 
 fromMaybeType :: Maybe (Arg Type) -> CompiledDef
 fromMaybeType (Just argType) = fromArgType argType

diff --git a/test/Hello.rs b/test/Hello.rs
@@ -1,13 +1,12 @@
-mod hello {
-
-pub enum TheRgb {
+mod test {
+enum TheRgb {
   Red, Green, Blue
 }
 
 
 
-pub fn id_rgb(rgb_arg: TheRgb) -> TheRgb {
-  return rgb_arg
+pub fn idRgb(rgbArg: TheRgb) -> TheRgb {
+  return rgbArg
 }
 
 enum TheWeekDay {
@@ -20,9 +19,5 @@ enum TheWeekDay {
 
 
 
-pub fn asFriday(rgbArg: TheRgb) -> TheWeekDay {
-  return rgbArg
-}
-
 
 }
diff --git a/test/Hello.agda → test/hello.agda b/test/Hello.agda → test/hello.agda
@@ -1,4 +1,4 @@
-module Hello where
+module test.hello where
 
 -- simple record type
 data TheRgb : Set where
@@ -14,9 +14,9 @@ data TheWeekDay : Set where
   Monday Tuesday Wednesday Thursday Friday Saturday Sunday : TheWeekDay
 {-# COMPILE AGDA2RUST TheWeekDay #-}
 
-asFriday : TheRgb → TheWeekDay
-asFriday rgbArg = Friday -- TODO compile body
-{-# COMPILE AGDA2RUST asFriday #-}
+-- asFriday : TheRgb → TheWeekDay
+-- asFriday rgbArg = Friday -- TODO compile body
+-- {-# COMPILE AGDA2RUST asFriday #-}
 
 -- TODO multiple clauses
 -- day-color : TheWeekDay → TheRgb