Skip to content

Commit

Permalink
[ new ] derive FromCell and ToCell for newtypes
Browse files Browse the repository at this point in the history
  • Loading branch information
stefan-hoeck committed Nov 10, 2023
1 parent 731ae0f commit 8c98cbd
Show file tree
Hide file tree
Showing 3 changed files with 71 additions and 19 deletions.
38 changes: 30 additions & 8 deletions src/Derive/Sqlite3/FromCell.idr
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,21 @@ import Language.Reflection.Util
-- Claims
--------------------------------------------------------------------------------

cellType : Vect n Name -> ParamCon n -> Maybe TTImp
cellType vs (MkParamCon _ _ args) =
case mapMaybe convert $ toList args of
[t] => Just `(FromCellType ~(t))
_ => Nothing
where
convert : ConArg n -> Maybe TTImp
convert (CArg _ MW _ t) = Just $ ttimp vs t
convert _ = Nothing

||| Top-level declaration of the `FromCell` implementation
||| for the given data type.
export
fromCellEnumImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
fromCellEnumImplClaim impl p = implClaim impl (implType "FromCell" p)
fromCellImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
fromCellImplClaim impl p = implClaim impl (implType "FromCell" p)

--------------------------------------------------------------------------------
-- Definitions
Expand Down Expand Up @@ -43,6 +53,13 @@ parameters (nms : List Name)
fromCellEnumDef f ti =
def f [patClause (var f) `(MkFromCell TEXT ~(decEnum ti))]

decNewtype : ParamCon n -> TTImp
decNewtype c = `(map ~(var c.name) . fromCell)

fromCellNewtypeDef : Name -> TTImp -> ParamCon n -> Decl
fromCellNewtypeDef f ct c =
def f [patClause (var f) `(MkFromCell ~(ct) ~(decNewtype c))]

--------------------------------------------------------------------------------
-- Deriving
--------------------------------------------------------------------------------
Expand All @@ -52,9 +69,14 @@ parameters (nms : List Name)
export %inline
FromCell : List Name -> ParamTypeInfo -> Res (List TopLevel)
FromCell nms p =
case isEnum p.info of
True =>
let impl := implName p "FromCell"
in Right [ TL (fromCellEnumImplClaim impl p) (fromCellEnumDef nms impl p.info) ]
False =>
Left "Interface FromCell can only be derived for enumerations and newtypes."
let impl := implName p "FromCell"
in if isEnum p.info
then
Right [ TL (fromCellImplClaim impl p) (fromCellEnumDef nms impl p.info) ]
else
case p.cons of
[c] =>
case cellType p.paramNames c of
Just ct => Right [ TL (fromCellImplClaim impl p) (fromCellNewtypeDef nms impl ct c) ]
Nothing => Left "Interface FromCell can only be derived for enumerations and newtypes."
_ => Left "Interface FromCell can only be derived for enumerations and newtypes."
41 changes: 32 additions & 9 deletions src/Derive/Sqlite3/ToCell.idr
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,21 @@ import Language.Reflection.Util
-- Claims
--------------------------------------------------------------------------------

cellType : Vect n Name -> ParamCon n -> Maybe TTImp
cellType vs (MkParamCon _ _ args) =
case mapMaybe convert $ toList args of
[t] => Just `(ToCellType ~(t))
_ => Nothing
where
convert : ConArg n -> Maybe TTImp
convert (CArg _ MW _ t) = Just $ ttimp vs t
convert _ = Nothing

||| Top-level declaration of the `ToCell` implementation for the given
||| data type.
export
toCellEnumImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
toCellEnumImplClaim impl p = implClaim impl (implType "ToCell" p)
toCellImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
toCellImplClaim impl p = implClaim impl (implType "ToCell" p)

--------------------------------------------------------------------------------
-- Definitions
Expand All @@ -35,6 +45,15 @@ parameters (nms : List Name)
toCellEnumDef f ti =
def f [patClause (var f) `(MkToCell TEXT ~(encEnum ti))]

encNT : ParamCon n -> TTImp
encNT c =
lam (lambdaArg x) $ iCase (var x) implicitFalse
[patClause `(~(var c.name) y) `(toCell y)]

toCellNewtypeDef : Name -> TTImp -> ParamCon n -> Decl
toCellNewtypeDef f ct c =
def f [patClause (var f) `(MkToCell ~(ct) ~(encNT c))]

--------------------------------------------------------------------------------
-- Deriving
--------------------------------------------------------------------------------
Expand All @@ -44,10 +63,14 @@ parameters (nms : List Name)
export %inline
ToCell : List Name -> ParamTypeInfo -> Res (List TopLevel)
ToCell nms p =
case isEnum p.info of
True =>
let impl := implName p "ToCell"
in Right [ TL (toCellEnumImplClaim impl p) (toCellEnumDef nms impl p.info) ]
False =>
Left "Interface ToCell can only be derived for enumerations and newtypes."

let impl := implName p "ToCell"
in if isEnum p.info
then
Right [ TL (toCellImplClaim impl p) (toCellEnumDef nms impl p.info) ]
else
case p.cons of
[c] =>
case cellType p.paramNames c of
Just ct => Right [ TL (toCellImplClaim impl p) (toCellNewtypeDef nms impl ct c) ]
Nothing => Left "Interface ToCell can only be derived for enumerations and newtypes."
_ => Left "Interface ToCell can only be derived for enumerations and newtypes."
11 changes: 9 additions & 2 deletions test/src/Schema.idr
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,13 @@ createEmployees =
-- Idris Types
--------------------------------------------------------------------------------

public export
record Salary where
constructor S
value : Double

%runElab derive "Schema.Salary" [Show, Eq, Ord, FromDouble, ToCell, FromCell]

public export
record OrgUnit (h : Type) where
constructor U
Expand All @@ -108,7 +115,7 @@ public export
record Employee (u : Type) where
constructor E
name : String
salary : Double
salary : Salary
unit : u

%runElab derive "Schema.Employee" [Show, Eq, ToRow, FromRow]
Expand Down Expand Up @@ -178,7 +185,7 @@ employee =
`ORDER_BY` [ASC "e.salary", ASC "e.name"]

export
unitStats : LQuery [String,Bits32,Double,Double,Double]
unitStats : LQuery [String,Bits32,Salary,Salary,Salary]
unitStats =
SELECT
[ "u.name"
Expand Down

0 comments on commit 8c98cbd

Please sign in to comment.