diff --git a/src/Deriving/DepTyCheck/Util/Collections.idr b/src/Deriving/DepTyCheck/Util/Collections.idr index 2124e06e0..86338e66a 100644 --- a/src/Deriving/DepTyCheck/Util/Collections.idr +++ b/src/Deriving/DepTyCheck/Util/Collections.idr @@ -11,6 +11,7 @@ import public Data.SortedSet import public Data.Vect import public Data.Vect.Dependent +import public Deriving.DepTyCheck.Util.Alternative import public Deriving.DepTyCheck.Util.Fin import public Deriving.DepTyCheck.Util.Syntax @@ -72,6 +73,11 @@ inits' : (xs : List a) -> DVect xs.length $ \idx => Vect (S $ finToNat idx) a inits' [] = [] inits' (x::xs) = [x] :: ((x ::) <$> inits' xs) +export +findLastIndex : (a -> Bool) -> (xs : List a) -> Maybe $ Fin xs.length +findLastIndex f [] = Nothing +findLastIndex f (x::xs) = FS <$> findLastIndex f xs <|> whenT (f x) FZ + --- Transitive clojure stuff --- export covering diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr index f3c17519b..1d53af2ed 100644 --- a/src/Deriving/DepTyCheck/Util/Reflection.idr +++ b/src/Deriving/DepTyCheck/Util/Reflection.idr @@ -35,7 +35,10 @@ Interpolation TTImp where export SingleLogPosition Con where - logPosition con = "\{show con.name}" + logPosition con = do + let fullName = show con.name + let fullName' = unpack fullName + maybe fullName (pack . flip drop fullName' . finToNat) $ findLastIndex (== '.') fullName' ---------------------------------------------- --- Compiler-based `TTImp` transformations ---