
  0 | module Derive.Iso
  1 | 
  2 | import public Derive.Lens.Options
  3 | import public Language.Reflection.Util
  4 | 
  5 | %default total
  6 | 
  7 | isoErr : Either String a
  8 | isoErr = Left "Isomorphisms can only be derived for newtypes"
  9 | 
 10 | parameters (o : LensOptions)
 11 |   iname : ParamTypeInfo -> Name
 12 |   iname p = UN $ Basic (o.dataTypeName $ nameStr p.info.name)
 13 | 
 14 |   iclaim : Visibility -> ParamTypeInfo -> Name -> TTImp -> Decl
 15 |   iclaim vis p con rtpe =
 16 |     let arg := p.applied
 17 |         tpe := piAll `(Iso' ~(arg) ~(rtpe)) p.implicits
 18 |     in simpleClaim vis (iname p) tpe
 19 | 
 20 |   idef : ParamTypeInfo -> Name -> Decl
 21 |   idef p con =
 22 |     let nme := iname p
 23 |         get := `(\case ~(var con) x => x)
 24 |      in def nme [patClause (var nme) `(I ~(get) ~(var con))]
 25 | 
 26 |   itl : Visibility -> ParamTypeInfo -> Con n vs -> Res (List TopLevel)
 27 |   itl vis p (MkCon con _ args _) = case boundArgs regular args [] of
 28 |     [<arg] => Right [TL (iclaim vis p con arg.arg.type) (idef p con)]
 29 |     _      => isoErr
 30 | 
 31 |   ||| Generate an isomorphism for a newtype
 32 |   export
 33 |   IsoVisO : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 34 |   IsoVisO vis nms p = case p.info.cons of
 35 |     [c] => itl vis p c
 36 |     _   => isoErr
 37 | 
 38 |   ||| Alias for `IsoVisO Public`
 39 |   export %inline
 40 |   IsoO : List Name -> ParamTypeInfo -> Res (List TopLevel)
 41 |   IsoO = IsoVisO Public
 42 | 
 43 | ||| Alias for `IsoVisO defaultOptions`
 44 | export %inline
 45 | IsoVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 46 | IsoVis = IsoVisO defaultOptions
 47 | 
 48 | ||| Alias for `IsoVis Public`
 49 | export %inline
 50 | Iso : List Name -> ParamTypeInfo -> Res (List TopLevel)
 51 | Iso = IsoVis Public
 52 |