Minor changes for use by other projects.

3 files changed, 76 insertions, 39 deletions

diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
index a0ed5df..1fcd667 100644
--- a/src/Data/Fin/Strong.idr
+++ b/src/Data/Fin/Strong.idr
@@ -4,11 +4,29 @@ import Data.Fin
 import Decidable.Equality.Core
 import Syntax.PreorderReasoning
 
+-- Definition ------------------------------------------------------------------
+
 public export
 data SFin : Nat -> Type where
   FZ : SFin (S n)
   FS : SFin (S n) -> SFin (S (S n))
 
+-- Properties
+
+export
+Injective (FS {n}) where
+  injective Refl = Refl
+
+export
+Uninhabited (SFin 0) where uninhabited x impossible
+
+export
+Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
+
+-- Conversion ------------------------------------------------------------------
+
+-- Utlities
+
 public export
 0 indexPred : (0 x : Fin n) -> Nat
 indexPred {n = S n} x = n
@@ -37,6 +55,8 @@ strongToFin : SFin n -> Fin n
 strongToFin FZ = FZ
 strongToFin (FS x) = FS (strongToFin x)
 
+-- Properties
+
 export
 finToStrongToFin : (x : Fin n) -> strongToFin (finToStrong x) = x
 finToStrongToFin FZ = Refl
@@ -48,20 +68,6 @@ strongToFinToStrong : (x : SFin n) -> finToStrong (strongToFin x) = x
 strongToFinToStrong FZ = Refl
 strongToFinToStrong (FS x) = cong FS (strongToFinToStrong x)
 
-%inline
-export
-FS' : SFin n -> SFin (S n)
-FS' = finToStrong . FS . strongToFin
-
-export
-Injective (FS {n}) where
-  injective Refl = Refl
-
-export
-Injective (FS' {n}) where
-  injective {x = FZ, y = FZ} prf = Refl
-  injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
-
 export
 Injective (strongToFin {n}) where
   injective {x, y} prf = Calc $
@@ -70,11 +76,25 @@ Injective (strongToFin {n}) where
     ~~ finToStrong (strongToFin y) ...(cong finToStrong prf)
     ~~ y                           ...(strongToFinToStrong y)
 
+-- Decidable Equality ----------------------------------------------------------
+
 export
-Uninhabited (SFin 0) where uninhabited x impossible
+DecEq (SFin n) where
+  decEq x y = viaEquivalence
+    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
+    (decEq (strongToFin x) (strongToFin y))
 
+-- Useful Constructor ----------------------------------------------------------
+
+%inline
 export
-Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
+FS' : SFin n -> SFin (S n)
+FS' = finToStrong . FS . strongToFin
+
+export
+Injective (FS' {n}) where
+  injective {x = FZ, y = FZ} prf = Refl
+  injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
 
 export
 sucNonZero : (x : SFin n) -> Not (FS' x = FZ)
@@ -85,8 +105,20 @@ export
 sucIsFS : (x : SFin (S n)) -> FS' x = FS x
 sucIsFS x = rewrite strongToFinToStrong x in Refl
 
+-- Num Interface ---------------------------------------------------------------
+
+public export
+{n : Nat} -> Num (SFin (S n)) where
+  x + y = finToStrong (strongToFin x + strongToFin y)
+  x * y = finToStrong (strongToFin x * strongToFin y)
+  fromInteger = finToStrong . restrict n
+
+-- Weaken and Shift ------------------------------------------------------------
+
 export
-DecEq (SFin n) where
-  decEq x y = viaEquivalence
-    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
-    (decEq (strongToFin x) (strongToFin y))
+weakenN : (0 k : Nat) -> SFin n -> SFin (n + k)
+weakenN k = finToStrong . weakenN k . strongToFin
+
+export
+shift : (k : Nat) -> SFin n -> SFin (k + n)
+shift k = finToStrong . shift k . strongToFin
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 01de5d2..4bb787f 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -22,6 +22,10 @@ public export
 sig .Op = Exists sig.Operator
 
 public export
+interface DecOp (0 sig : Signature) where
+  decOp : (op, op' : sig.Op) -> Dec (op = op')
+
+public export
 data Term : Signature -> Nat -> Type where
   Var : SFin (S n) -> Term sig (S n)
   Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
@@ -45,7 +49,7 @@ export
 pure : (SFin k -> SFin n) -> SFin k -> Term sig n
 pure r = Var' . r
 
-export
+public export
 (<$>) : (SFin k -> Term sig n) -> Term sig k -> Term sig n
 f <$> Var i = f i
 f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts)
@@ -65,7 +69,7 @@ subCong prf (Op op ts) =
 
 -- Substitution is Monadic -----------------------------------------------------
 
-export
+public export
 (.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin j -> Term sig n
 f . g = (f <$>) . g
 
@@ -93,8 +97,8 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : SFin (S k) -> Term sig n) ->
-  (r : SFin j -> SFin (S k)) ->
+  (f : SFin k -> Term sig n) ->
+  (r : SFin j -> SFin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl
 
diff --git a/src/Data/Term/Unify.idr b/src/Data/Term/Unify.idr
index f75a61a..b87ab21 100644
--- a/src/Data/Term/Unify.idr
+++ b/src/Data/Term/Unify.idr
@@ -4,6 +4,7 @@ import Data.DPair
 import Data.Fin.Occurs
 import Data.Fin.Strong
 import Data.Maybe.Properties
+import Data.Singleton
 import Data.Term
 import Data.Term.Property
 import Data.Term.Zipper
@@ -198,6 +199,11 @@ sub ++ sub1 :< tx = (sub ++ sub1) :< tx
 -- Properties
 
 export
+recover : Singleton k -> AList sig k n -> Singleton n
+recover x [<] = x
+recover x (sub :< _) = recover (pure pred <*> x) sub
+
+export
 evalHomo :
   (0 sub2 : AList sig k n) ->
   (sub1 : AList sig j k) ->
@@ -239,17 +245,17 @@ flexRigid x t = case check x t of
 
 export
 amgu :
-  DecEq sig.Op =>
+  DecOp sig =>
   (t, u : Term sig n) ->
   Exists (AList sig n) ->
   Maybe (Exists (AList sig n))
 amguAll :
-  DecEq sig.Op =>
+  DecOp sig =>
   (ts, us : Vect k (Term sig n)) ->
   Exists (AList sig n) ->
   Maybe (Exists (AList sig n))
 
-amgu (Op op ts) (Op op' us) acc with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op'))
+amgu (Op op ts) (Op op' us) acc with (decOp (Evidence _ op) (Evidence _ op'))
   amgu (Op op ts) (Op op us) acc | Yes Refl = amguAll ts us acc
   _ | No neq = Nothing
 amgu (Var x) (Var y) (Evidence _ [<]) = Just (flexFlex x y)
@@ -268,7 +274,7 @@ amguAll (t :: ts) (u :: us) acc = do
   amguAll ts us acc
 
 export
-mgu : DecEq sig.Op => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
+mgu : DecOp sig => (t, u : Term sig n) -> Maybe (Exists (AList sig n))
 mgu t u = amgu t u (Evidence _ [<])
 
 -- Properties
@@ -364,7 +370,7 @@ stepEquiv :
   Extension (Unifies ((v `for` x) <$> t) ((v `for` x) <$> u)) (eval sub)
 stepEquiv t u sub v x = extendUnify t u (v `for` x) (eval sub)
 
-parameters {auto _ : DecEq sig.Op}
+parameters {auto _ : DecOp sig}
   public export
   data AmguProof : (t, u : Term sig k) -> Exists (AList sig k) -> Type where
     Success :
@@ -394,20 +400,15 @@ parameters {auto _ : DecEq sig.Op}
       AmguAllProof ts us sub
 
 export
-amguProof :
-  DecEq sig.Op =>
-  (t, u : Term sig n) ->
-  (sub : Exists (AList sig n)) ->
-  AmguProof t u sub
+amguProof : DecOp sig => (t, u : Term sig n) -> (sub : Exists (AList sig n)) -> AmguProof t u sub
 export
 amguAllProof :
-  DecEq sig.Op =>
+  DecOp sig =>
   (ts, us : Vect k (Term sig n)) ->
   (sub : Exists (AList sig n)) ->
   AmguAllProof ts us sub
 
-amguProof (Op op ts) (Op op' us) sub
-  with (decEq {t = sig.Op} (Evidence _ op) (Evidence _ op')) proof prf
+amguProof (Op op ts) (Op op' us) sub with (decOp (Evidence _ op) (Evidence _ op')) proof prf
   amguProof (Op op ts) (Op op us) sub | Yes Refl
     with (amguAllProof ts us sub)
     _ | SuccessAll sub' val prf' =
@@ -541,7 +542,7 @@ amguAllProof (t :: ts) (u :: us) sub with (amguProof t u sub)
       (failHead absurd)
       (bindNothing prf (amguAll ts us))
 
-parameters {auto _ : DecEq sig.Op}
+parameters {auto _ : DecOp sig}
   namespace MguProof
     public export
     data MguProof : (t, u : Term sig k) -> Type where
@@ -556,7 +557,7 @@ parameters {auto _ : DecEq sig.Op}
         MguProof t u
 
 export
-mguProof : DecEq sig.Op => (t, u : Term sig k) -> MguProof t u
+mguProof : DecOp sig => (t, u : Term sig k) -> MguProof t u
 mguProof t u with (amguProof t u (Evidence _ [<]))
   _ | Success (Evidence _ sub) val prf = Success (Evidence _ sub) val prf
   _ | Failure absurd prf = Failure absurd prf