Idris2 elaboration for injectivity

ElabInj.idr

-- From ShinKage on FP Slack
mapName : (String -> String) -> Name -> Name
mapName f (UN n) = UN (f n)
mapName f (MN n i) = (MN (f n) i)
mapName f (NS ns n) = (NS ns (mapName f n))
mapName f (DN n realn) = (DN (f n) realn)
mapName f (RF n) = RF (f n)

appTyCon : List String -> Name -> TTImp
appTyCon ns n = foldl (\tt, v => `(~(tt) ~(IBindVar EmptyFC v))) (IVar EmptyFC n) ns

deriveInjectivity : Name -> Elab ()
deriveInjectivity name = do
    [(name, imp)] <- getType name
      | xs => fail "not unique"
    let args = getArgs 0 imp
    let from = `(~(appTyCon (fst . snd <$> args) name) === ~(appTyCon (snd . snd <$> args) name))
    let claims = getDecls args from
    declare claims
    let decls = getImpls args
    declare decls
    logTerm "debug" 10 "claims" $ ILocal EmptyFC claims `(())
    logTerm "debug" 10 "decls" $ ILocal EmptyFC decls `(())
  where
    getArgs : Int -> TTImp -> (List (Name, String, String))
    getArgs idx (IPi _ c ExplicitArg n argTy retTy) = (mapName (\x => x ++ "Injective" ++ show idx) name, "left" ++ show idx, "right" ++ show idx) :: (getArgs (idx + 1) retTy)
    getArgs idx (IPi _ _ _ _ _ retTy) = getArgs idx retTy
    getArgs _ _ = []
    getDecls : List (Name, String, String) -> TTImp -> List Decl
    getDecls [] _ = []
    getDecls ((n, l, r) :: args) prf = (IClaim EmptyFC MW Public [Inline] (MkTy EmptyFC EmptyFC n `(~prf -> ~(IBindVar EmptyFC l) === ~(IBindVar EmptyFC r)))) :: getDecls args prf
    getImpls : List (Name, String, String) -> List Decl
    getImpls [] = []
    getImpls ((n, l, r) :: args) = (IDef EmptyFC n [PatClause EmptyFC `(~(IVar EmptyFC n) Refl) `(Refl)]) :: getImpls args

%runElab deriveInjectivity `{{Elem}}