Use new notion of Fin to reduce casts.

1 files changed, 25 insertions, 16 deletions

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 3b16f38..4b0ac3e 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -1,6 +1,7 @@
 module Data.Term
 
 import public Data.Vect
+import public Data.Fin.Strong
 import Data.Vect.Properties.Map
 import Syntax.PreorderReasoning
 
@@ -16,30 +17,38 @@ record Signature where
 
 public export
 data Term : Signature -> Nat -> Type where
-  Var : Fin n -> Term sig n
+  Var : SFin (S n) -> Term sig (S n)
   Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
 
 %name Term t, u, v
 
+export
+Var' : SFin n -> Term sig n
+Var' x = rewrite indexPred'Prf x in Var (replace {p = SFin} (indexPred'Prf x) x)
+
+export
+varIsVar : (x : SFin (S n)) -> Var' x = Var x
+varIsVar x = Refl
+
 -- Substitution ----------------------------------------------------------------
 
 export
-pure : (Fin k -> Fin n) -> Fin k -> Term sig n
-pure r = Var . r
+pure : (SFin k -> SFin n) -> SFin k -> Term sig n
+pure r = Var' . r
 
 export
-(<$>) : (Fin k -> Term sig n) -> Term sig k -> Term sig n
+(<$>) : (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)
 
 -- Extensional Equality --------------------------------------------------------
 
 public export
-0 (.=.) : Rel (Fin k -> Term sig n)
-f .=. g = (i : Fin k) -> f i = g i
+0 (.=.) : Rel (SFin k -> Term sig n)
+f .=. g = (i : SFin k) -> f i = g i
 
 export
-subCong : {f, g : Fin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
+subCong : {f, g : SFin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
 subCong prf (Var i) = prf i
 subCong prf (Op op ts) =
   cong (Op op) $
@@ -48,23 +57,23 @@ subCong prf (Op op ts) =
 -- Substitution is Monadic -----------------------------------------------------
 
 export
-(.) : (Fin k -> Term sig n) -> (Fin j -> Term sig k) -> Fin j -> Term sig n
+(.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin j -> Term sig n
 f . g = (f <$>) . g
 
 -- Properties
 
 export
-subUnit : (t : Term sig n) -> Var <$> t = t
+subUnit : (t : Term sig n) -> Var' <$> t = t
 subUnit (Var i) = Refl
 subUnit (Op op ts) = cong (Op op) $ Calc $
-  |~ map (Var <$>) ts
-  ~~ map id ts        ...(mapExtensional (Var <$>) id (\t => subUnit (assert_smaller ts t)) ts)
-  ~~ ts               ...(mapId ts)
+  |~ map (Var' <$>) ts
+  ~~ map id ts         ...(mapExtensional (Var' <$>) id (\t => subUnit (assert_smaller ts t)) ts)
+  ~~ ts                ...(mapId ts)
 
 export
 subAssoc :
-  (f : Fin k -> Term sig n) ->
-  (g : Fin j -> Term sig k) ->
+  (f : SFin k -> Term sig n) ->
+  (g : SFin j -> Term sig k) ->
   (t : Term sig j) ->
   (f . g) <$> t = f <$> g <$> t
 subAssoc f g (Var i) = Refl
@@ -75,8 +84,8 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : Fin k -> Term sig n) ->
-  (r : Fin j -> Fin k) ->
+  (f : SFin (S k) -> Term sig n) ->
+  (r : SFin j -> SFin (S k)) ->
   f . pure r .=. f . r
 subComp f r i = Refl