Return Maybe from strengthen (#1540)

Co-authored-by: Fabián Heredia Montiel <303897+fabianhjr@users.noreply.github.com>

idris2api.ipkg

@@ -116,6 +116,7 @@ modules =
 
     Libraries.Data.ANameMap,
     Libraries.Data.DList,
+    Libraries.Data.Fin,
     Libraries.Data.IMaybe,
     Libraries.Data.IntMap,
     Libraries.Data.IOMatrix,

libs/base/Data/Fin.idr

@@ -100,14 +100,14 @@ weakenLTE  FZ    (LTESucc _) = FZ
 weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y
 
 ||| Attempt to tighten the bound on a Fin.
-||| Return `Left` if the bound could not be tightened, or `Right` if it could.
+||| Return the tightened bound if there is one, else nothing.
 export
-strengthen : {n : _} -> Fin (S n) -> Either (Fin (S n)) (Fin n)
-strengthen {n = S _} FZ = Right FZ
-strengthen {n = S _} (FS i) with (strengthen i)
-  strengthen (FS _) | Left x  = Left $ FS x
-  strengthen (FS _) | Right x = Right $ FS x
-strengthen f = Left f
+strengthen : {n : _} -> Fin (S n) -> Maybe (Fin n)
+strengthen {n = S _} FZ = Just FZ
+strengthen {n = S _} (FS p) with (strengthen p)
+  strengthen (FS _) | Nothing = Nothing
+  strengthen (FS _) | Just q  = Just $ FS q
+strengthen _ = Nothing
 
 ||| Add some natural number to a Fin, extending the bound accordingly
 ||| @ n the previous bound

libs/contrib/Data/Fin/Extra.idr

@@ -78,19 +78,19 @@ invFinInvolutive (FS k) = Calc $
 
 ||| It's possible to strengthen a weakened element of Fin **m**.
 export
-strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Right n
+strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n
 strengthenWeakenIsRight FZ = Refl
 strengthenWeakenIsRight (FS k) = rewrite strengthenWeakenIsRight k in Refl
 
 ||| It's not possible to strengthen the last element of Fin **n**.
 export
-strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Left (Fin.last {n})
+strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Nothing
 strengthenLastIsLeft {n=Z} = Refl
 strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
 
 ||| It's possible to strengthen the inverse of a succesor
 export
-strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (invFin (FS m)) = Right (invFin m)
+strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (invFin (FS m)) = Just (invFin m)
 strengthenNotLastIsRight m = strengthenWeakenIsRight (invFin m)
 
 ||| Either tightens the bound on a Fin or proves that it's the last.

src/Libraries/Data/Fin.idr

@@ -0,0 +1,16 @@
+module Libraries.Data.Fin
+
+import public Data.Fin
+
+%default total
+
+-- TODO: Remove this, once Data.Fin.strengthen from base is available
+--       to the compiler
+
+export
+strengthen : {n : _} -> Fin (S n) -> Maybe (Fin n)
+strengthen {n = S _} FZ = Just FZ
+strengthen {n = S _} (FS p) with (Libraries.Data.Fin.strengthen p)
+  strengthen (FS _) | Nothing = Nothing
+  strengthen (FS _) | Just q  = Just $ FS q
+strengthen _ = Nothing

src/TTImp/ProcessBuiltin.idr

@@ -2,9 +2,9 @@
 -- If we get more builtins it might be wise to move each builtin to it's own file.
 module TTImp.ProcessBuiltin
 
-import Data.Fin
 import Data.List
 
+import Libraries.Data.Fin as Libs
 import Libraries.Data.NameMap
 
 import Core.CaseTree
@@ -82,10 +82,7 @@ getNEIndex : (arity : Nat) -> Term vars -> Maybe (Fin arity)
 getNEIndex ar (Bind _ x b tm) = case b of
     Let _ _ val _ => getNEIndex ar $ subst {x} val tm
     Pi _ mul _ arg => if isErased mul
-        then getNEIndex ar tm >>=
-            \k => case strengthen (FS k) of
-                Left _ => Nothing
-                Right k' => Just k'
+        then getNEIndex ar tm >>= Libs.strengthen . FS
         else natToFin 0 ar
     _ => Nothing
 getNEIndex _ _ = Nothing