0 | module Derive.Prism
 1 |
 2 | import public Derive.Lens.Options
 3 | import public Language.Reflection.Util
 4 |
 5 | %default total
 6 |
 7 | parameters (o : LensOptions)
 8 |   pname : Name -> Name
 9 |   pname n = UN $ Basic (o.constructorName $ nameStr n)
10 |
11 |   pclaim : Visibility -> ParamTypeInfo -> Name -> TTImp -> Decl
12 |   pclaim vis p con rtpe =
13 |     let arg := p.applied
14 |         tpe := piAll `(Prism' ~(arg) ~(rtpe)) p.implicits
15 |     in simpleClaim vis (pname con) tpe
16 |
17 |   pdef0 : Name -> Decl
18 |   pdef0 con =
19 |     let nme := pname con
20 |         get := `(\case ~(var con) => Just (); _ => Nothing)
21 |      in def nme [patClause (var nme) `(prism' (const ~(var con)) ~(get))]
22 |
23 |   pdef1 : Name -> Decl
24 |   pdef1 con =
25 |     let nme := pname con
26 |         get := `(\case ~(var con) x => Just x; _ => Nothing)
27 |      in def nme [patClause (var nme) `(prism' ~(var con) ~(get))]
28 |
29 |   ptl : Visibility -> ParamTypeInfo -> Con n vs -> Maybe TopLevel
30 |   ptl vis p (MkCon con _ args _) = case boundArgs regular args [] of
31 |     [<]    => Just (TL (pclaim vis p con `(Unit))  (pdef0 con))
32 |     [<arg] => Just (TL (pclaim vis p con arg.arg.type) (pdef1 con))
33 |     _      => Nothing
34 |
35 |   ||| Generate monomorphic prisms for a sum type.
36 |   export
37 |   PrismsVisO : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
38 |   PrismsVisO vis nms p = Right $ mapMaybe (ptl vis p) p.info.cons
39 |
40 |   ||| Alias for `PrismsVisO Public`
41 |   export %inline
42 |   PrismsO : List Name -> ParamTypeInfo -> Res (List TopLevel)
43 |   PrismsO = PrismsVisO Public
44 |
45 | ||| Alias for `PrismVisO defaultOptions`
46 | export %inline
47 | PrismsVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
48 | PrismsVis = PrismsVisO defaultOptions
49 |
50 | ||| Alias for `PrismsVis Public`
51 | export %inline
52 | Prisms : List Name -> ParamTypeInfo -> Res (List TopLevel)
53 | Prisms = PrismsVis Public
54 |