5 | module Language.Reflection.Derive

  7 | import Data.DPair

  8 | import Data.List1

  9 | import Data.Vect

 10 | import Decidable.Equality

 11 | import Language.Reflection

 12 | import Language.Reflection.Syntax

 13 | import Language.Reflection.Types

 15 | %language ElabReflection

 17 | %default total

 25 | public export

 26 | interface Named a => Elaborateable a where

 27 |   find_ : Elaboration m => Name -> m a

 30 | public export %inline

 31 | find : (0 a : Type) -> Elaborateable a => Elaboration m => Name -> m a

 32 | find _ = find_

 34 | export %inline

 35 | Elaborateable TypeInfo where

 36 |   find_ = getInfo'

 38 | public export %inline

 39 | Named a => Named (Subset a p) where

 40 |   (.getName) (Element v _) = v.getName

 49 | funName : Named a => a -> String -> Name

 50 | funName n fun = UN $ Basic $ fun ++ n.nameStr

 54 | implName : Named a => a -> String -> Name

 55 | implName n iface = UN $ Basic $ "impl" ++ iface ++ n.nameStr

 64 | public export

 65 | record BoundArg (n : Nat) (p : Arg -> Type) where

 66 |   constructor BA

 67 |   arg  : Arg

 68 |   vars : Vect n Name

 69 |   prf  : p arg

 71 | public export

 72 | split : Vect k (Vect (S n) a) -> (Vect k a, Vect k (Vect n a))

 73 | split []                 = ([],[])

 74 | split ((x :: xs) :: yss) =

 75 |   let (zs,zss) := split yss

 76 |    in (x :: zs, xs :: zss)

 81 | boundArgs :

 82 |      {0 p : Arg -> Type}

 83 |   -> (f : (a : Arg) -> Maybe (p a))

 84 |   -> Vect n Arg

 85 |   -> Vect k (Vect n Name)

 86 |   -> SnocList (BoundArg k p)

 87 | boundArgs f = go Lin

 88 |   where

 89 |     go :  SnocList (BoundArg k p)

 90 |        -> Vect m Arg

 91 |        -> Vect k (Vect m Name)

 92 |        -> SnocList (BoundArg k p)

 93 |     go sx (x :: xs) ns =

 94 |       let (y, ys) := split ns

 95 |        in case f x of

 96 |             Just prf => go (sx :< BA x y prf) xs ys

 97 |             Nothing  => go sx xs ys

 98 |     go sx []        _  = sx

100 | public export

101 | data Explicit : Arg -> Type where

102 |   IsExplicit : Explicit (MkArg c ExplicitArg n t)

104 | public export

105 | explicit : (a : Arg) -> Maybe (Explicit a)

106 | explicit (MkArg _ ExplicitArg _ _) = Just IsExplicit

107 | explicit _                         = Nothing

109 | public export

110 | data NamedArg : Arg -> Type where

111 |   IsNamed : NamedArg (MkArg c p (Just (UN $ Basic n)) t)

113 | public export

114 | named : (a : Arg) -> Maybe (NamedArg a)

115 | named (MkArg _ _ (Just $ UN $ Basic n) _) = Just IsNamed

116 | named _                                   = Nothing

118 | public export

119 | argName : (a : Arg) -> {auto 0 prf : NamedArg a} -> Name

120 | argName (MkArg _ _ (Just $ UN $ Basic n) _) {prf = IsNamed} = UN $ Basic n

122 | public export

123 | data Unerased : Arg -> Type where

124 |   U1 : Unerased (MkArg M1 p n t)

125 |   UW : Unerased (MkArg MW p n t)

127 | public export

128 | unerased : (a : Arg) -> Maybe (Unerased a)

129 | unerased (MkArg M0 _ _ _) = Nothing

130 | unerased (MkArg M1 _ _ _) = Just U1

131 | unerased (MkArg MW _ _ _) = Just UW

133 | public export

134 | data Erased : Arg -> Type where

135 |   IsErased : Erased (MkArg M0 p n t)

137 | public export

138 | erased : (a : Arg) -> Maybe (Erased a)

139 | erased (MkArg M0 _ _ _) = Just IsErased

140 | erased _                = Nothing

142 | public export

143 | 0 Regular : Arg -> Type

144 | Regular a = (Unerased a, Explicit a)

146 | public export

147 | regular : (a : Arg) -> Maybe (Regular a)

148 | regular a = [| MkPair (unerased a) (explicit a) |]

150 | public export

151 | 0 RegularNamed : Arg -> Type

152 | RegularNamed a = (NamedArg a, Regular a)

154 | public export

155 | regularNamed : (a : Arg) -> Maybe (RegularNamed a)

156 | regularNamed a = [| MkPair (named a) (regular a) |]

158 | public export

159 | 0 NamedExplicit : Arg -> Type

160 | NamedExplicit a = (NamedArg a, Explicit a)

162 | public export

163 | namedExplicit : (a : Arg) -> Maybe (NamedExplicit a)

164 | namedExplicit a = [| MkPair (named a) (explicit a) |]

166 | public export

167 | toNamed : BoundArg n p -> Maybe (BoundArg n (\a => (NamedArg a, p a)))

168 | toNamed (BA arg vars prf) = case named arg of

169 |   Just v  => Just (BA arg vars (v, prf))

170 |   Nothing => Nothing

177 | failRecord : String -> Res a

178 | failRecord s =

179 |   Left "Interface \{s} can only be derived for single-constructor data types"

204 | accumArgs :

205 |      {0 p : Arg -> Type}

206 |   -> (f : (a : Arg) -> Maybe (p a))

207 |   -> (lhs : TTImp -> TTImp)

208 |   -> (rhs : SnocList TTImp -> TTImp)

209 |   -> (arg : BoundArg 1 p -> TTImp)

210 |   -> (con : Con n vs)

211 |   -> Clause

212 | accumArgs f lhs rhs arg c =

213 |   let xs := freshNames "x" c.arty

214 |       cx := bindCon c xs

215 |       sx := map arg (boundArgs f c.args [xs])

216 |    in patClause (lhs cx) (rhs sx)

242 | accumArgs2 :

243 |      {0 p : Arg -> Type}

244 |   -> (f : (a : Arg) -> Maybe (p a))

245 |   -> (lhs : TTImp -> TTImp -> TTImp)

246 |   -> (rhs : SnocList TTImp -> TTImp)

247 |   -> (arg : BoundArg 2 p -> TTImp)

248 |   -> (con : Con n vs)

249 |   -> Clause

250 | accumArgs2 f lhs rhs arg c =

251 |   let xs := freshNames "x" c.arty

252 |       ys := freshNames "y" c.arty

253 |       cx := bindCon c xs

254 |       cy := bindCon c ys

255 |       sx := map arg (boundArgs f c.args [xs,ys])

256 |    in patClause (lhs cx cy) (rhs sx)

277 | mapArgs :

278 |      {0 p : Arg -> Type}

279 |   -> (f : (a : Arg) -> Maybe (p a))

280 |   -> (lhs : TTImp -> TTImp)

281 |   -> (arg : BoundArg 1 p -> TTImp)

282 |   -> (con : Con n vs)

283 |   -> Clause

284 | mapArgs f lhs arg c =

285 |   let xs := freshNames "x" c.arty

286 |       cx := bindCon c xs

287 |       sx := map arg (boundArgs f c.args [xs])

288 |    in patClause (lhs cx) (appAll c.name $ sx <>> [])

310 | mapArgs2 :

311 |      {0 p : Arg -> Type}

312 |   -> (f : (a : Arg) -> Maybe (p a))

313 |   -> (lhs : TTImp -> TTImp -> TTImp)

314 |   -> (arg : BoundArg 2 p -> TTImp)

315 |   -> (con : Con n vs)

316 |   -> Clause

317 | mapArgs2 f lhs arg c =

318 |   let xs := freshNames "x" c.arty

319 |       ys := freshNames "y" c.arty

320 |       cx := bindCon c xs

321 |       cy := bindCon c ys

322 |       sx := map arg (boundArgs f c.args [xs,ys])

323 |    in patClause (lhs cx cy) (appAll c.name $ sx <>> [])

339 | injArgs :

340 |      {0 p : Arg -> Type}

341 |   -> (f : (a : Arg) -> Maybe (p a))

342 |   -> (arg : BoundArg 0 p -> TTImp)

343 |   -> (con : Con n vs)

344 |   -> TTImp

345 | injArgs f arg c =

346 |   let sx := map arg (boundArgs f c.args [])

347 |    in appAll c.name (sx <>> [])

354 | public export

355 | record TopLevel where

356 |   constructor TL

357 |   claim : Decl

358 |   defn  : Decl

366 | public export %inline

367 | implClaimVis : Visibility -> Name -> TTImp -> Decl

368 | implClaimVis vis = interfaceHintOpts vis [Inline]

376 | public export %inline

377 | implClaim : Name -> TTImp -> Decl

378 | implClaim = implClaimVis Public

391 | implType : Name -> ParamTypeInfo -> TTImp

392 | implType n p = piAll (var n `app` p.applied) (allImplicits p n)

397 | unAppAny : TTImp -> TTImp

398 | unAppAny (IApp fc s t)         = unAppAny s

399 | unAppAny (INamedApp fc s nm t) = unAppAny s

400 | unAppAny (IAutoApp fc s t)     = unAppAny s

401 | unAppAny (IWithApp fc s t)     = unAppAny s

402 | unAppAny t                     = t

411 | extractResult : TTImp -> Maybe (TTImp, Name)

412 | extractResult (IApp _ _ tpe) = case unAppAny tpe of

413 |   IVar _ nm => Just (tpe, nm)

414 |   _         => Nothing

415 | extractResult _              = Nothing

417 | export %inline

418 | sequenceJoin : Applicative f => List (f $ List a) -> f (List a)

419 | sequenceJoin = map join . sequence

421 | public export

422 | record ParamInfo where

423 |   constructor PI

424 |   name     : Name

425 |   strategy : (n : Nat) -> Maybe (Exists $ ParamPattern n)

426 |   goals    : List (List Name -> ParamTypeInfo -> Res (List TopLevel))

428 | fromParamInfo : List Name -> TypeInfo -> ParamInfo -> Res (List TopLevel)

429 | fromParamInfo nms ti (PI n f gs) = case f ti.arty of

430 |   Just (Evidence _ pat) => do

431 |     pti <- paramType ti pat

432 |     map join $ traverse (\g => g nms pti) gs

434 |   Nothing               => Left """

441 | deriveParam : Elaboration m => List ParamInfo -> m ()

442 | deriveParam is = do

443 |   ts <- traverse (find TypeInfo . name) is

444 |   let ns := map (.getName) ts

446 |   Right tls <- pure . map join . sequence $ zipWith (fromParamInfo ns) ts is

447 |     | Left err => fail err

449 |   let claims := map claim tls

450 |       defns  := map defn tls

452 |   logMsg "derive.claims" 1 $ unlines (map show claims)

453 |   logMsg "derive.definitions" 1 $ unlines (map show defns)

454 |   declare $ claims ++ defns

457 | allParams : (n : Nat) -> Maybe (Exists $ ParamPattern n)

458 | allParams n = Just $ Evidence _ $ paramsOnly n

461 | allIndices : (n : Nat) -> Maybe (Exists $ ParamPattern n)

462 | allIndices n = Just $ Evidence _ $ indicesOnly n

465 | match : ParamPattern m k -> (n : Nat) -> Maybe (Exists $ ParamPattern n)

466 | match p n = map (\v => Evidence _ v) $ go n p

468 |   where

469 |     go : (z : Nat) -> ParamPattern x y -> Maybe (ParamPattern z y)

470 |     go 0 []           = Just []

471 |     go (S j) (a :: b) = (a ::) <$> go j b

472 |     go 0 (_ :: _)     = Nothing

473 |     go (S j) []       = Nothing

476 | deriveMutual :

477 |      Elaboration m

478 |   => List Name

479 |   -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

480 |   -> m ()

481 | deriveMutual ns fs = deriveParam $ map (\n => PI n allParams fs) ns

490 | export %inline

491 | derive :

492 |      Elaboration m

493 |   => Name

494 |   -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

495 |   -> m ()

496 | derive n = deriveMutual [n]

498 | export %inline

499 | deriveIndexed :

500 |      Elaboration m

501 |   => Name

502 |   -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

503 |   -> m ()

504 | deriveIndexed n fs = deriveParam [PI n allIndices fs]

506 | export %inline

507 | derivePattern :

508 |      Elaboration m

509 |   => Name

510 |   -> ParamPattern n k

511 |   -> List (List Name -> ParamTypeInfo -> Res (List TopLevel))

512 |   -> m ()

513 | derivePattern n pat fs = deriveParam [PI n (match pat) fs]

520 | public export %inline

521 | mkEq : (eq : a -> a -> Bool) -> Eq a

522 | mkEq eq = MkEq eq (\a,b => not $ eq a b)

527 | public export

528 | mkOrd : Eq a => (comp : a -> a -> Ordering) -> Ord a

529 | mkOrd comp =

530 |   MkOrd comp

531 |     (\a,b => comp a b == LT)

532 |     (\a,b => comp a b == GT)

533 |     (\a,b => comp a b /= GT)

534 |     (\a,b => comp a b /= LT)

535 |     (\a,b => if comp a b == GT then a else b)

536 |     (\a,b => if comp a b == LT then a else b)

539 | public export

540 | mkShow : (show : a -> String) -> Show a

541 | mkShow show = MkShow show (\_ => show)

544 | public export

545 | mkShowPrec : (showPrec : Prec -> a -> String) -> Show a

546 | mkShowPrec showPrec = MkShow (showPrec Open) showPrec

550 | public export

551 | mkDecEq : (decEq : (x1 : a) -> (x2 : a) -> Dec (x1 = x2)) -> DecEq a

552 | mkDecEq = %runElab check (var $ singleCon "DecEq")