0 | module Idrall.Derive.ToDhall

  2 | import Idrall.Expr

  3 | import Idrall.Pretty

  4 | import Idrall.Derive.Common

  6 | import public Data.SortedMap

  8 | import Language.Reflection

 10 | %language ElabReflection

 12 | %hide Idrall.Expr.Name

 14 | public export

 15 | interface ToDhall ty where

 16 |   constructor MkToDhall

 17 |   toDhallType : Expr Void

 18 |   toDhall : ty -> Expr Void

 21 | ToDhall Nat where

 22 |   toDhallType = ENatural EmptyFC

 23 |   toDhall x = ENaturalLit EmptyFC x

 26 | ToDhall Bool where

 27 |   toDhallType = EBool EmptyFC

 28 |   toDhall x = EBoolLit EmptyFC x

 31 | ToDhall Integer where

 32 |   toDhallType = EInteger EmptyFC

 33 |   toDhall x = EIntegerLit EmptyFC x

 36 | ToDhall Double where

 37 |   toDhallType = EDouble EmptyFC

 38 |   toDhall x = EDoubleLit EmptyFC x

 41 | ToDhall String where

 42 |   toDhallType = EText EmptyFC

 43 |   toDhall x = ETextLit EmptyFC (MkChunks [] x)

 46 | ToDhall ty => ToDhall (List ty) where

 47 |   toDhallType = EApp EmptyFC (EList EmptyFC) (toDhallType {ty=ty})

 48 |   toDhall xs = EListLit EmptyFC (Just (toDhallType {ty=ty})) (map toDhall xs)

 51 | ToDhall ty => ToDhall (Maybe ty) where

 52 |   toDhallType = EApp EmptyFC (EOptional EmptyFC) (toDhallType {ty=ty})

 53 |   toDhall Nothing = EApp EmptyFC (ENone EmptyFC) (toDhallType {ty=ty})

 54 |   toDhall (Just x) = ESome EmptyFC (toDhall x)

 57 | Pretty Void where

 58 |   pretty x = pretty ""

 60 | parameters (options : Options)

 61 |   -- Record Type functions

 62 |   -- given a idris Record constructor arg in the form (Name, type),

 63 |   -- return a dhall record field for use in the ERecord constructor.

 64 |   argToFieldType : List (Name, TTImp) -> TTImp

 65 |   argToFieldType [] = `([])

 66 |   argToFieldType ((n, t) :: xs) =

 67 |     let name = primStr $ options.fieldNameModifier (show n)

 68 |     in `(MkPair (MkFieldName ~name) (toDhallType {ty = ~t}) :: ~(argToFieldType xs))

 70 |   dhallRecTypeFromRecArg : List (Name, TTImp) -> TTImp

 71 |   dhallRecTypeFromRecArg xs =

 72 |     `(ERecord EmptyFC $ fromList $ ~(argToFieldType xs))

 74 |   genRecordTypeClauses : -- IdrisType ->

 75 |                Name -> Name -> Cons -> List Clause

 76 |   genRecordTypeClauses funName arg [] = do

 77 |     pure $ patClause `(~(var funName)) (dhallRecTypeFromRecArg [])

 78 |   genRecordTypeClauses funName arg ((n, ls) :: xs) = do

 79 |     pure $ patClause `(~(var funName)) (dhallRecTypeFromRecArg ls)

 81 |   -- Record Lit functions

 82 |   argToField : Name -> List (Name, TTImp) -> TTImp

 83 |   argToField arg [] = `([])

 84 |   argToField arg ((n, _) :: xs) =

 85 |     let name = primStr $ options.fieldNameModifier (show n)

 86 |     in `(MkPair (MkFieldName ~name) (toDhall (~(var n) ~(var arg))) :: ~(argToField arg xs))

 88 |   dhallRecLitFromRecArg : Name -> List (Name, TTImp) -> TTImp

 89 |   dhallRecLitFromRecArg arg xs =

 90 |     `(ERecordLit EmptyFC $ fromList $ ~(argToField arg xs))

 92 |   genRecordLitClauses : Name -> Name -> Cons -> List Clause

 93 |   genRecordLitClauses funName arg [] = do

 94 |     pure $ patClause `(~(var funName) ~(bindvar arg)) (dhallRecLitFromRecArg arg [])

 95 |   genRecordLitClauses funName arg ((n, ls) :: xs) = do

 96 |     pure $ patClause `(~(var funName) ~(bindvar arg)) (dhallRecLitFromRecArg arg ls)

 98 |   deriveToDhallRecord :  Name

 99 |                       -> Name

100 |                       -> Name

101 |                       -> Cons

102 |                       -> Elab ()

103 |   deriveToDhallRecord name funNameType funNameLit cons =

104 |     let argName = genReadableSym "arg"

105 |         funDeclType = IDef EmptyFC funNameType $ (genRecordTypeClauses funNameType !argName cons)

106 |         funDeclLit = IDef EmptyFC funNameLit $ (genRecordLitClauses funNameLit !argName cons)

107 |     in do

108 |       -- declare the fuction in the env

109 |       declare [funDeclType, funDeclLit]

112 | mkUnion : Name -> Cons -> Elab (TTImp)

113 | mkUnion n cons = pure `(EUnion EmptyFC $ fromList $ ~(!(go n cons)))

114 |   where

115 |   getTypeTTImp : Name -> List (Name, TTImp) -> Elab (TTImp)

116 |   getTypeTTImp consName [] =

117 |     let cn = primStr $ show $ stripNs consName in

118 |     do

119 |       pure `(MkPair (MkFieldName ~cn) Nothing)

120 |   getTypeTTImp consName ((n, t) :: []) =

121 |     let cn = primStr $ show $ stripNs consName in

122 |     do

123 |       pure $ `(MkPair (MkFieldName ~cn) $ Just (toDhallType {ty = ~t}))

124 |   getTypeTTImp consName (_ :: xs) = do

125 |      fail $ "too many args for constructor: " ++ show consName

126 |   go : Name -> Cons -> Elab (TTImp)

127 |   go name [] = pure `([])

128 |   go name ((n, t) :: xs) = do

129 |     pair <- getTypeTTImp n t

130 |     pure $ `(~(pair) :: ~(!(go name xs)))

132 | genClauseADT : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp, TTImp)

133 | genClauseADT name funName constructor' xs =

134 |   let cnShort = show $ stripNs $ constructor'

135 |       cn = primStr cnShort

136 |       nameShort = show $ stripNs $ name

137 |       lhs0 = `(~(var funName) ~(var constructor'))

138 |       toDhallTypeFunName = "toDhallType" ++ nameShort

139 |       fieldName = IPrimVal EmptyFC $ Str cnShort

140 |   in do

141 |     case xs of

142 |          [] => pure $ MkPair lhs0

143 |             `(EField EmptyFC (~(varStr toDhallTypeFunName)) (MkFieldName ~cn))

144 |          ((n, t) :: []) => do

145 |             argName <- genReadableSym "arg"

146 |             pure $ MkPair

147 |               `(~(var funName) (~(varStr cnShort) ~(bindvar argName)))

148 |               `(EApp EmptyFC (EField EmptyFC (~(varStr toDhallTypeFunName)) (MkFieldName ~fieldName)) (toDhall ~(var argName)))

149 |          (x :: _) => fail $ "too many args for constructor: " ++ show constructor'

151 | deriveToDhallADT : Name

152 |                  -> Name

153 |                  -> Name

154 |                  -> Cons

155 |                  -> Elab ()

156 | deriveToDhallADT name funNameType funNameLit cons = do

157 |   -- given constructors, lookup names in dhall records for those constructors

158 |   rhs <- mkUnion name cons

159 |   clausesType <- pure $ patClause

160 |      `(~(var funNameType)) rhs

161 |   let funDeclType = IDef EmptyFC funNameType [clausesType]

162 |   declare [funDeclType]

164 |   clausesADTLit <- traverse (\(cn, as) => genClauseADT name funNameLit cn (reverse as)) cons

165 |   clausesLit <- pure $ map (\x => patClause (fst x) (snd x)) clausesADTLit

166 |   let funDeclLit = IDef EmptyFC funNameLit clausesLit

167 |    -- declare []

168 |   declare [funDeclLit]

170 | toDhallImpl : String -> List Decl

171 | toDhallImpl typeName =

172 |   let -- names

173 |       mkToDhall = UN $ Basic "MkToDhall"

174 |       toDhallType = UN $ Basic "toDhallType"

175 |       toDhallName = UN $ Basic "toDhall"

176 |       rhsToDhallType = UN $ Basic $ "toDhallType" ++ typeName

177 |       rhsToDhallLit = UN $ Basic $ "toDhallLit" ++ typeName

178 |       functionName = UN . Basic $ "implToDhall" ++ typeName

180 |       typeNameImp = var $ UN $ Basic typeName

181 |       toDhallType = var toDhallType

182 |       toDhall = var toDhallName

183 |       function = var functionName

185 |       toDhallLitClause = patClause toDhall $ var rhsToDhallLit

187 |       impl = ILocal EmptyFC

188 |           [ IClaim $ NoFC $ MkIClaimData MW Private [] (MkTy EmptyFC (NoFC toDhallName) `(~(typeNameImp) -> Expr Void))

189 |           , IDef EmptyFC toDhallName [toDhallLitClause]

190 |           ]

191 |           `(~(var mkToDhall) ~(var rhsToDhallType) ~(var rhsToDhallLit))

193 |   in [ IClaim $ NoFC $ MkIClaimData MW Public [Hint True] $ MkTy EmptyFC (NoFC functionName) `(ToDhall ~(typeNameImp))

194 |      , IDef EmptyFC functionName [patClause function impl]

195 |      ]

198 | deriveToDhall : IdrisType

199 |               -> {default Common.defaultOptions options : Options}

200 |               -> (name : Name)

201 |               -> Elab ()

202 | deriveToDhall it {options} n = do

203 |   [(name, _)] <- getType n

204 |           | _ => fail "Ambiguous name"

205 |   let nameShortStr = show (stripNs name)

206 |   let funNameType = UN $ Basic ("toDhallType" ++ nameShortStr)

207 |   let funNameLit = UN $ Basic ("toDhallLit" ++ nameShortStr)

208 |   let objNameType = UN $ Basic ("__impl_toDhallType" ++ nameShortStr)

209 |   let objNameLit = UN $ Basic ("__impl_toDhallLit" ++ nameShortStr)

211 |   conNames <- getCons name

213 |   -- get the constructors of the record

214 |   -- cons : (List (Name, List (Name, TTImp)))

215 |   cons <- for conNames $ \n => do

216 |     [(conName, conImpl)] <- getType n

217 |       | _ => fail $ show n ++ "constructor must be in scope and unique"

218 |     args <- getArgs conImpl

219 |     pure (conName, args)

221 |   -- logCons cons

223 |   -- create the function type signatures

224 |   let funClaimType = IClaim $ NoFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funNameType) `(Expr Void))

225 |   let funClaimLit = IClaim $ NoFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funNameLit) `(~(var name) -> Expr Void))

227 |   -- declare the function type signatures in the env

228 |   declare [funClaimType, funClaimLit]

229 |   case it of

230 |        Record => do

231 |          deriveToDhallRecord options name funNameType funNameLit cons

232 |          declare $ toDhallImpl $ nameShortStr

233 |        ADT => do

234 |          deriveToDhallADT name funNameType funNameLit cons

235 |          declare $ toDhallImpl $ nameShortStr

238 | record ExRec1 where

239 |   constructor MkExRec1

240 |   mn : Maybe Nat

241 |   st : String

243 | %runElab (deriveToDhall Record `{ ExRec1 })

245 | data ExADTTest

246 |   = Bar

247 |   | ADouble Double

248 | %runElab (deriveToDhall ADT `{ ExADTTest })

250 | data Ex1

251 |   = ANat Nat

252 |   | ADoub Double

253 |   | ANone