Merge pull request #103 from mattpolzin/override-record-field-names

Allow transforming Idris record names for to/from Dhall

Idrall/Derive.idr

@@ -74,8 +74,8 @@ Alternative (Either Error) where
   (Right x) <|> _ = (Right x)
 
 export
-deriveFromDhall : IdrisType -> (name : Name) -> Elab ()
-deriveFromDhall it n =
+deriveFromDhall : IdrisType -> {default Common.defaultOptions options : Options} -> (name : Name) -> Elab ()
+deriveFromDhall it {options} n =
   do [(name, _)] <- getType n
              | _ => fail "Ambiguous name"
      let funName = UN $ Basic ("fromDhall" ++ show (stripNs name))
@@ -119,7 +119,7 @@ deriveFromDhall it n =
     genClauseRecord : Name -> Name -> List (Name, TTImp) -> Elab (TTImp)
     genClauseRecord constructor' arg xs = do
           let rhs = foldr (\(n, type), acc =>
-                            let name = primStr $ (show n) in
+                            let name = primStr $ options.fieldNameModifier (show n) in
                                 case type of
                                      _ => `(~acc <*> (lookupEither ~(varStr "fc") (MkFieldName ~name) ~(var arg) >>= fromDhall)))
                           `(pure ~(var constructor')) xs

Idrall/Derive/Common.idr

@@ -118,3 +118,15 @@ public export
 data IdrisType
   = ADT
   | Record
+
+public export
+record Options where
+  constructor MkOptions
+  ||| This function is used to adjust constructor argument names
+  ||| during encoding and decoding
+  fieldNameModifier          : String -> String
+
+export
+defaultOptions : Options
+defaultOptions = MkOptions id
+

Idrall/Derive/ToDhall.idr

@@ -58,55 +58,56 @@ export
 Pretty Void where
   pretty x = pretty ""
 
--- Record Type functions
--- given a idris Record constructor arg in the form (Name, type),
--- return a dhall record field for use in the ERecord constructor.
-argToFieldType : List (Name, TTImp) -> TTImp
-argToFieldType [] = `([])
-argToFieldType ((n, t) :: xs) =
-  let name = primStr $ (show n)
-  in `(MkPair (MkFieldName ~name) (toDhallType {ty = ~t}) :: ~(argToFieldType xs))
-
-dhallRecTypeFromRecArg : List (Name, TTImp) -> TTImp
-dhallRecTypeFromRecArg xs =
-  `(ERecord EmptyFC $ fromList $ ~(argToFieldType xs))
-
-genRecordTypeClauses : -- IdrisType ->
-             Name -> Name -> Cons -> List Clause
-genRecordTypeClauses funName arg [] = do
-  pure $ patClause `(~(var funName)) (dhallRecTypeFromRecArg [])
-genRecordTypeClauses funName arg ((n, ls) :: xs) = do
-  pure $ patClause `(~(var funName)) (dhallRecTypeFromRecArg ls)
-
--- Record Lit functions
-argToField : Name -> List (Name, TTImp) -> TTImp
-argToField arg [] = `([])
-argToField arg ((n, _) :: xs) =
-  let name = primStr $ (show n)
-  in `(MkPair (MkFieldName ~name) (toDhall (~(var n) ~(var arg))) :: ~(argToField arg xs))
-
-dhallRecLitFromRecArg : Name -> List (Name, TTImp) -> TTImp
-dhallRecLitFromRecArg arg xs =
-  `(ERecordLit EmptyFC $ fromList $ ~(argToField arg xs))
-
-genRecordLitClauses : Name -> Name -> Cons -> List Clause
-genRecordLitClauses funName arg [] = do
-  pure $ patClause `(~(var funName) ~(bindvar $ show arg)) (dhallRecLitFromRecArg arg [])
-genRecordLitClauses funName arg ((n, ls) :: xs) = do
-  pure $ patClause `(~(var funName) ~(bindvar $ show arg)) (dhallRecLitFromRecArg arg ls)
-
-deriveToDhallRecord : Name
-                    -> Name
-                    -> Name
-                    -> Cons
-                    -> Elab ()
-deriveToDhallRecord name funNameType funNameLit cons =
-  let argName = genReadableSym "arg"
-      funDeclType = IDef EmptyFC funNameType $ (genRecordTypeClauses funNameType !argName cons)
-      funDeclLit = IDef EmptyFC funNameLit $ (genRecordLitClauses funNameLit !argName cons)
-  in do
-    -- declare the fuction in the env
-    declare [funDeclType, funDeclLit]
+parameters (options : Options)
+  -- Record Type functions
+  -- given a idris Record constructor arg in the form (Name, type),
+  -- return a dhall record field for use in the ERecord constructor.
+  argToFieldType : List (Name, TTImp) -> TTImp
+  argToFieldType [] = `([])
+  argToFieldType ((n, t) :: xs) =
+    let name = primStr $ options.fieldNameModifier (show n)
+    in `(MkPair (MkFieldName ~name) (toDhallType {ty = ~t}) :: ~(argToFieldType xs))
+
+  dhallRecTypeFromRecArg : List (Name, TTImp) -> TTImp
+  dhallRecTypeFromRecArg xs =
+    `(ERecord EmptyFC $ fromList $ ~(argToFieldType xs))
+
+  genRecordTypeClauses : -- IdrisType ->
+               Name -> Name -> Cons -> List Clause
+  genRecordTypeClauses funName arg [] = do
+    pure $ patClause `(~(var funName)) (dhallRecTypeFromRecArg [])
+  genRecordTypeClauses funName arg ((n, ls) :: xs) = do
+    pure $ patClause `(~(var funName)) (dhallRecTypeFromRecArg ls)
+
+  -- Record Lit functions
+  argToField : Name -> List (Name, TTImp) -> TTImp
+  argToField arg [] = `([])
+  argToField arg ((n, _) :: xs) =
+    let name = primStr $ options.fieldNameModifier (show n)
+    in `(MkPair (MkFieldName ~name) (toDhall (~(var n) ~(var arg))) :: ~(argToField arg xs))
+
+  dhallRecLitFromRecArg : Name -> List (Name, TTImp) -> TTImp
+  dhallRecLitFromRecArg arg xs =
+    `(ERecordLit EmptyFC $ fromList $ ~(argToField arg xs))
+
+  genRecordLitClauses : Name -> Name -> Cons -> List Clause
+  genRecordLitClauses funName arg [] = do
+    pure $ patClause `(~(var funName) ~(bindvar $ show arg)) (dhallRecLitFromRecArg arg [])
+  genRecordLitClauses funName arg ((n, ls) :: xs) = do
+    pure $ patClause `(~(var funName) ~(bindvar $ show arg)) (dhallRecLitFromRecArg arg ls)
+
+  deriveToDhallRecord :  Name
+                      -> Name
+                      -> Name
+                      -> Cons
+                      -> Elab ()
+  deriveToDhallRecord name funNameType funNameLit cons =
+    let argName = genReadableSym "arg"
+        funDeclType = IDef EmptyFC funNameType $ (genRecordTypeClauses funNameType !argName cons)
+        funDeclLit = IDef EmptyFC funNameLit $ (genRecordLitClauses funNameLit !argName cons)
+    in do
+      -- declare the fuction in the env
+      declare [funDeclType, funDeclLit]
 
 -- ADT Type functions
 mkUnion : Name -> Cons -> Elab (TTImp)
@@ -196,9 +197,10 @@ toDhallImpl typeName =
 
 export
 deriveToDhall : IdrisType
+              -> {default Common.defaultOptions options : Options}
               -> (name : Name)
               -> Elab ()
-deriveToDhall it n = do
+deriveToDhall it {options} n = do
   [(name, _)] <- getType n
           | _ => fail "Ambiguous name"
   let nameShortStr = show (stripNs name)
@@ -227,7 +229,7 @@ deriveToDhall it n = do
   declare [funClaimType, funClaimLit]
   case it of
        Record => do
-         deriveToDhallRecord name funNameType funNameLit cons
+         deriveToDhallRecord options name funNameType funNameLit cons
          declare $ toDhallImpl $ nameShortStr
        ADT => do
          deriveToDhallADT name funNameType funNameLit cons

examples/ForbiddenNames.idr

@@ -0,0 +1,26 @@
+module ForbiddenNames
+
+import Idrall.API.V2
+
+import Language.Reflection
+%language ElabReflection
+
+record ForbiddenNames where
+  constructor MkForbiddenNames
+  ns : String
+  rc : String
+
+dhallOptions : Options
+dhallOptions =
+  { fieldNameModifier :=
+    \case "ns" => "namespace"; "rc" => "record"; fieldName => fieldName } defaultOptions
+
+%runElab deriveFromDhall Record {options=dhallOptions} `{ ForbiddenNames }
+%runElab deriveToDhall Record {options=dhallOptions} `{ ForbiddenNames }
+
+main : IO ()
+main = do
+  Right names <- liftIOEither $ deriveFromDhallString {ty=ForbiddenNames} "./forbidden-names.dhall"
+    | Left e => putStrLn $ !(fancyError e)
+  putStrLn $ "namespace: " ++ names.ns
+  putStrLn $ "record: " ++ names.rc

examples/forbidden-names.dhall

@@ -0,0 +1,3 @@
+{ namespace = "myNamespace"
+, record = "myRecord"
+}

tests/Main.idr

@@ -33,12 +33,14 @@ deriveTests : TestPool
 deriveTests = MkTestPool "derive tests" [] Default
   [ "derive001"
   , "derive002"
+  , "derive003"
   ]
 
 examplesTests : TestPool
 examplesTests = MkTestPool "examples tests" [] Default
   [ "example001"
   , "example002"
+  , "example003"
   , "inigo001"
   ]
 

tests/derive/derive003/.gitignore

@@ -0,0 +1,2 @@
+Package.idr
+package.dhall

tests/derive/derive003/Main.idr

@@ -0,0 +1,38 @@
+module Main
+
+import Idrall.API.V2
+import Idrall.Pretty
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
+
+import System
+
+import Language.Reflection
+
+%language ElabReflection
+
+testPretty : ToDhall ty => ty -> IO ()
+testPretty x = do
+  putDoc $ pretty $ toDhall x
+
+record NeedsTranslation where
+  constructor MkNeedsTranslation
+  ns : String
+  name : String
+
+dhallOptions : Options
+dhallOptions = { fieldNameModifier := \case "ns" => "namespace"; fieldName => fieldName } defaultOptions
+
+%runElab deriveFromDhall Record {options=dhallOptions} `{ NeedsTranslation }
+%runElab deriveToDhall Record {options=dhallOptions} `{ NeedsTranslation }
+
+main : IO ()
+main = do
+  testPretty $ MkNeedsTranslation "myNamespace" "myName"
+  Right fromD <- liftIOEither $ 
+    deriveFromDhallString {ty=NeedsTranslation} 
+                          #" { namespace = "hi", name = "there" } "#
+    | Left e => putStrLn (show e)
+  if (fromD.ns /= "hi" || fromD.name /= "there")
+     then putStrLn "from dhall failed"
+     else pure ()
+

tests/derive/derive003/expected

@@ -0,0 +1 @@
+{ name = "myName", namespace = "myNamespace" }

tests/derive/derive003/run

@@ -0,0 +1,3 @@
+idris2 -q --no-banner --no-color --console-width 0 -p contrib -p idrall Main.idr --exec main
+
+rm -rf build

tests/examples/example003/.gitignore

@@ -0,0 +1,2 @@
+ForbiddenNames.idr
+forbidden-names.dhall

tests/examples/example003/expected

@@ -0,0 +1,2 @@
+namespace: myNamespace
+record: myRecord

tests/examples/example003/run

@@ -0,0 +1,5 @@
+cp ../../../examples/ForbiddenNames.idr .
+cp ../../../examples/forbidden-names.dhall .
+idris2 -q --no-banner --no-color --console-width 0 -p contrib -p idrall ForbiddenNames.idr --exec main
+
+rm -rf build