Use new notion of Fin to reduce casts.

1 files changed, 24 insertions, 24 deletions

diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 2435c98..d65d185 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -13,8 +13,8 @@ import Syntax.PreorderReasoning
 public export
 record Property (sig : Signature) (k : Nat) where
   constructor MkProp
-  0 Prop : forall n. (Fin k -> Term sig n) -> Type
-  cong : forall n. {f, g : Fin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
+  0 Prop : forall n. (SFin k -> Term sig n) -> Type
+  cong : forall n. {f, g : SFin k -> Term sig n} -> f .=. g -> Prop f -> Prop g
 
 %name Property p, q
 
@@ -39,7 +39,7 @@ All ps = MkProp (\f => All (\p => p.Prop f) ps) (\cong => mapRel (\p => p.cong c
 
 public export 0
 (<=>) : Property sig k -> Property sig k -> Type
-p <=> q = forall n. (f : Fin k -> Term sig n) -> p.Prop f <=> q.Prop f
+p <=> q = forall n. (f : SFin k -> Term sig n) -> p.Prop f <=> q.Prop f
 
 -- Properties
 
@@ -81,7 +81,7 @@ unifiesOp f = MkEquivalence
 
 public export 0
 Nothing : Property sig k -> Type
-Nothing p = forall n. (f : Fin k -> Term sig n) -> Not (p.Prop f)
+Nothing p = forall n. (f : SFin k -> Term sig n) -> Not (p.Prop f)
 
 -- Properties
 
@@ -92,7 +92,7 @@ nothingEquiv eq absurd f x = absurd f ((eq f).rightToLeft x)
 -- Extensions ------------------------------------------------------------------
 
 public export
-Extension : Property sig k -> (Fin k -> Term sig n) -> Property sig n
+Extension : Property sig k -> (SFin k -> Term sig n) -> Property sig n
 Extension p f = MkProp
   { Prop = \g => p.Prop (g . f)
   , cong = \prf => p.cong (\i => subCong prf (f i))
@@ -105,14 +105,14 @@ nothingExtends : Nothing p -> Nothing (Extension p f)
 nothingExtends absurd g x = void $ absurd (g . f) x
 
 export
-extendUnit : (p : Property sig k) -> p <=> Extension p Var
+extendUnit : (p : Property sig k) -> p <=> Extension p Var'
 extendUnit p f = MkEquivalence id id
 
 export
 extendAssoc :
   (p : Property sig j) ->
-  (f : Fin j -> Term sig k) ->
-  (g : Fin k -> Term sig m) ->
+  (f : SFin j -> Term sig k) ->
+  (g : SFin k -> Term sig m) ->
   Extension (Extension p f) g <=> Extension p (g . f)
 extendAssoc p f g h =
   MkEquivalence
@@ -122,8 +122,8 @@ extendAssoc p f g h =
 export
 extendUnify :
   (t, u : Term sig j) ->
-  (f : Fin j -> Term sig k) ->
-  (g : Fin k -> Term sig m) ->
+  (f : SFin j -> Term sig k) ->
+  (g : SFin k -> Term sig m) ->
   Extension (Unifies t u) (g . f) <=> Extension (Unifies (f <$> t) (f <$> u)) g
 extendUnify t u f g h =
   MkEquivalence
@@ -145,9 +145,9 @@ extendUnify t u f g h =
 -- Ordering --------------------------------------------------------------------
 
 public export
-record (<=) (f : Fin k -> Term sig m) (g : Fin k -> Term sig n) where
+record (<=) (f : SFin k -> Term sig m) (g : SFin k -> Term sig n) where
   constructor MkLte
-  sub : Fin n -> Term sig m
+  sub : SFin n -> Term sig m
   prf : f .=. sub . g
 
 %name Property.(<=) prf
@@ -166,8 +166,8 @@ lteCong prf1 prf2 prf3 = MkLte
   }
 
 export
-Reflexive (Fin k -> Term sig m) (<=) where
-  reflexive = MkLte Var (\i => sym $ subUnit _)
+Reflexive (SFin k -> Term sig m) (<=) where
+  reflexive = MkLte Var' (\i => sym $ subUnit _)
 
 export
 transitive : f <= g -> g <= h -> f <= h
@@ -181,11 +181,11 @@ transitive prf1 prf2 = MkLte
   }
 
 export
-varMax : (f : Fin k -> Term sig m) -> f <= Var
+varMax : (f : SFin k -> Term sig m) -> f <= Var'
 varMax f = MkLte f (\i => Refl)
 
 export
-compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
+compLte : f <= g -> (h : SFin k -> Term sig m) -> f . h <= g . h
 compLte prf h = MkLte
   { sub = prf.sub
   , prf = \i => Calc $
@@ -197,8 +197,8 @@ compLte prf h = MkLte
 export
 lteExtend : 
   {p : Property sig k} ->
-  {f : Fin k -> Term sig m} ->
-  {g : Fin k -> Term sig n} ->
+  {f : SFin k -> Term sig m} ->
+  {g : SFin k -> Term sig n} ->
   (prf : f <= g) -> 
   p.Prop f -> 
   (Extension p g).Prop prf.sub
@@ -209,7 +209,7 @@ lteExtend prf x = p.cong prf.prf x
 public export
 Max : Property sig k -> Property sig k
 Max p = MkProp
-  { Prop = \f => (p.Prop f, forall n. (g : Fin k -> Term sig n) -> p.Prop g -> g <= f)
+  { Prop = \f => (p.Prop f, forall n. (g : SFin k -> Term sig n) -> p.Prop g -> g <= f)
   , cong = \cong, (x, max) => (p.cong cong x, \g, y => lteCong (\_ => Refl) cong (max g y))
   }
 
@@ -226,8 +226,8 @@ public export 0
 DClosed : Property sig k -> Type
 DClosed p =
   forall m, n.
-  (f : Fin k -> Term sig m) ->
-  (g : Fin k -> Term sig n) ->
+  (f : SFin k -> Term sig m) ->
+  (g : SFin k -> Term sig n) ->
   f <= g ->
   p.Prop g ->
   p.Prop f
@@ -245,9 +245,9 @@ unifiesDClosed t u f g prf1 prf2 = Calc $
 
 optimistLemma :
   {q : Property sig j} ->
-  {a : Fin j -> Term sig k} ->
-  {f : Fin k -> Term sig m} ->
-  {g : Fin m -> Term sig n} ->
+  {a : SFin j -> Term sig k} ->
+  {f : SFin k -> Term sig m} ->
+  {g : SFin m -> Term sig n} ->
   DClosed p ->
   (Max (Extension p a)).Prop f ->
   (Max (Extension q (f . a))).Prop g ->