Use new notion of Fin to reduce casts.

1 files changed, 56 insertions, 57 deletions

diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index 2955aa2..7cb01d6 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -2,6 +2,7 @@ module Data.Term.Unify
 
 import Data.DPair
 import Data.Fin.Occurs
+import Data.Fin.Strong
 import Data.Maybe.Properties
 import Data.Term
 import Data.Term.Zipper
@@ -13,10 +14,10 @@ import Syntax.PreorderReasoning
 -- Check -----------------------------------------------------------------------
 
 export
-check : Fin k -> Term sig k -> Maybe (Term sig (pred k))
-checkAll : Fin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))
+check : SFin k -> Term sig k -> Maybe (Term sig (pred k))
+checkAll : SFin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))
 
-check x (Var y) = Var <$> thick x y
+check x (Var y) = Var' <$> thick x y
 check x (Op op ts) = Op op <$> checkAll x ts
 
 checkAll x [] = Just []
@@ -25,15 +26,18 @@ checkAll x (t :: ts) = [| check x t :: checkAll x ts |]
 -- Properties
 
 export
-checkOccurs : (x : Fin k) -> (zip : Zipper sig k) -> IsNothing (check x (zip + Var x))
+checkOccurs :
+  (x : SFin k) ->
+  (zip : Zipper sig k) ->
+  IsNothing (check x (zip + Var' x))
 checkAllOccurs :
-  (x : Fin k) ->
-  (i : Fin (S n)) ->
-  (ts : Vect n (Term sig k)) ->
+  (x : SFin k) ->
+  (i : SFin n) ->
+  (ts : Vect (pred n) (Term sig k)) ->
   (zip : Zipper sig k) ->
-  IsNothing (checkAll x (insertAt i (zip + Var x) ts))
+  IsNothing (checkAll x (insertAt' i (zip + Var' x) ts))
 
-checkOccurs x Top = mapNothing Var (thickRefl x)
+checkOccurs x Top = mapNothing Var' (thickRefl x)
 checkOccurs x (Op op i ts zip) = mapNothing (Op op) (checkAllOccurs x i ts zip)
 
 checkAllOccurs x FZ ts zip =
@@ -47,19 +51,19 @@ checkAllOccurs x (FS i) (t :: ts) zip =
 
 export
 checkNothing :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (0 _ : IsNothing (check x t)) ->
-  (zip : Zipper sig k ** t = zip + Var x)
+  (zip : Zipper sig k ** t = zip + Var' x)
 checkAllNothing :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (ts : Vect n (Term sig k)) ->
   (0 _ : IsNothing (checkAll x (t :: ts))) ->
-  (i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt i (zip + Var x) ts')
+  (i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt' i (zip + Var' x) ts')
 
 checkNothing x (Var y) prf =
-  (Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var (thick x y) prf))))
+  (Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var' (thick x y) prf))))
 checkNothing x (Op op (t :: ts)) prf =
   let (i ** ts' ** zip ** prf) = checkAllNothing x t ts (mapNothingInverse (Op op) _ prf) in
   (Op op i ts' zip ** cong (Op op) prf)
@@ -74,13 +78,18 @@ checkAllNothing x t ts prf with (appNothingInverse (Just (::) <*> check x t) (ch
     (FS i ** t :: ts ** zip ** cong (t ::) prf)
 
 export
-checkThin : (x : Fin k) -> (t : Term sig (pred k)) -> IsJust (check x (pure (thin x) <$> t))
+checkThin :
+  (x : SFin (S k)) ->
+  (t : Term sig k) ->
+  IsJust (check x (pure (thin x) <$> t))
 checkAllThin :
-  (x : Fin k) ->
-  (ts : Vect n (Term sig (pred k))) ->
+  (x : SFin (S k)) ->
+  (ts : Vect n (Term sig k)) ->
   IsJust (checkAll x (map (pure (thin x) <$>) ts))
 
-checkThin x (Var y) = mapIsJust Var (thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf))
+checkThin x (Var y) =
+  mapIsJust Var' $
+  thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf)
 checkThin x (Op op ts) = mapIsJust (Op op) (checkAllThin x ts)
 
 checkAllThin x [] = ItIsJust
@@ -91,23 +100,23 @@ checkAllThin x (t :: ts) =
 
 export
 checkJust :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (0 _ : check x t = Just u) ->
   t = pure (thin x) <$> u
 checkAllJust :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (ts : Vect n (Term sig k)) ->
   (0 _ : checkAll x ts = Just us) ->
   ts = map (pure (thin x) <$>) us
 
 checkJust x (Var y) prf =
-  let 0 z = mapJustInverse Var (thick x y) prf in
+  let 0 z = mapJustInverse Var' (thick x y) prf in
   let 0 prf = thickJust x y (fst z.snd) in
   sym $ Calc $
     |~ pure (thin x) <$> u
-    ~~ pure (thin x) <$> Var z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
-    ~~ Var y                       ...(cong Var prf)
+    ~~ pure (thin x) <$> Var' z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
+    ~~ Var' y                       ...(cong Var' prf)
 checkJust x (Op op ts) prf =
   let 0 z = mapJustInverse (Op op) (checkAll x ts) prf in
   let 0 prf = checkAllJust x ts (fst z.snd) in
@@ -130,44 +139,47 @@ checkAllJust x (t :: ts) prf =
 -- Single Variable Substitution ------------------------------------------------
 
 export
-for : Term sig (pred k) -> Fin k -> Fin k -> Term sig (pred k)
-(t `for` x) y = maybe t Var (thick x y)
+for : Term sig (pred k) -> SFin k -> SFin k -> Term sig (pred k)
+(t `for` x) y = maybe t Var' (thick x y)
 
 export
-forThin : (0 t : Term sig (pred k)) -> (x : Fin k) -> (t `for` x) . thin x .=. Var
-forThin t x i = cong (maybe t Var) (thickThin x i)
+forThin :
+  (0 t : Term sig (pred k)) ->
+  (x : SFin k) ->
+  (t `for` x) . thin x .=. Var'
+forThin t x i = cong (maybe t Var') (thickThin x i)
 
 export
 forUnifies :
-  (x : Fin k) ->
+  (x : SFin k) ->
   (t : Term sig k) ->
   (0 _ : check x t = Just u) ->
-  (u `for` x) <$> t = (u `for` x) <$> Var x
+  (u `for` x) <$> t = (u `for` x) <$> Var' x
 forUnifies x t prf = Calc $
   |~ (u `for` x) <$> t
   ~~ (u `for` x) <$> pure (thin x) <$> u ...(cong ((u `for` x) <$>) $ checkJust x t prf)
   ~~ (u `for` x) . thin x <$> u          ...(sym $ subAssoc (u `for` x) (pure (thin x)) u)
-  ~~ Var <$> u                           ...(subCong (forThin u x) u)
+  ~~ Var' <$> u                          ...(subCong (forThin u x) u)
   ~~ u                                   ...(subUnit u)
-  ~~ (u `for` x) <$> Var x               ...(sym $ cong (maybe u Var) $ extractIsNothing $ thickRefl x)
+  ~~ (u `for` x) <$> Var' x              ...(sym $ cong (maybe u Var') $ extractIsNothing $ thickRefl x)
 
 -- Substitution List -----------------------------------------------------------
 
 public export
 data AList : Signature -> Nat -> Nat -> Type where
   Lin : AList sig n n
-  (:<) : AList sig k n -> (Term sig k, Fin (S k)) -> AList sig (S k) n
+  (:<) : AList sig k n -> (Term sig k, SFin (S k)) -> AList sig (S k) n
 
 %name AList sub
 
 namespace Exists
   public export
-  (:<) : Exists (AList sig n) -> (Term sig n, Fin (S n)) -> Exists (AList sig (S n))
+  (:<) : Exists (AList sig n) -> (Term sig n, SFin (S n)) -> Exists (AList sig (S n))
   Evidence _ sub :< tx = Evidence _ (sub :< tx)
 
 export
-eval : AList sig k n -> Fin k -> Term sig n
-eval [<] = Var
+eval : AList sig k n -> SFin k -> Term sig n
+eval [<] = Var'
 eval (sub :< (t, x)) = eval sub . (t `for` x)
 
 export
@@ -190,28 +202,15 @@ evalHomo sub2 (sub1 :< (t, x)) i = Calc $
 
 -- Unification -----------------------------------------------------------------
 
-flexFlex : (x, y : Fin n) -> Exists (AList sig n)
-flexFlex x y =
-  rewrite (snd $ indexIsSuc x) in
-  case thick x' y' of
-    Just z => Evidence _ [<(Var z, x')]
-    Nothing => Evidence _ [<]
-  where
-  x', y' : Fin (S $ fst $ indexIsSuc x)
-  x' = replace {p = Fin} (snd $ indexIsSuc x) x
-  y' = replace {p = Fin} (snd $ indexIsSuc x) y
-
-flexRigid : Fin n -> Term sig n -> Maybe (Exists (AList sig n))
-flexRigid x t =
-  rewrite (snd $ indexIsSuc x) in
-  case check x' t' of
-    Just u => Just (Evidence _ [<(u, x')])
-    Nothing => Nothing
-  where
-  x' : Fin (S $ fst $ indexIsSuc x)
-  x' = replace {p = Fin} (snd $ indexIsSuc x) x
-  t' : Term sig (S $ fst $ indexIsSuc x)
-  t' = replace {p = Term sig} (snd $ indexIsSuc x) t
+flexFlex : (x : SFin (S n)) -> (y : SFin (S n)) -> Exists (AList sig (S n))
+flexFlex x y = case thick x y of
+  Just z => Evidence _ [<(Var' z, x)]
+  Nothing => Evidence _ [<]
+
+flexRigid : SFin (S n) -> Term sig (S n) -> Maybe (Exists (AList sig (S n)))
+flexRigid x t = case check x t of
+  Just u => Just (Evidence _ [<(u, x)])
+  Nothing => Nothing
 
 export
 amgu :