From 426c138c2b72d6b037d4d2c15c2d5462ddde6f23 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 8 Mar 2023 22:33:52 +0100
Subject: [PATCH] clean up some old unused stuff

---
 lib/Quox/Context.idr                | 97 ++---------------------------
 lib/{ => on-hold}/Quox/NatExtra.idr |  0
 lib/quox-lib.ipkg                   |  1 -
 3 files changed, 5 insertions(+), 93 deletions(-)
 rename lib/{ => on-hold}/Quox/NatExtra.idr (100%)

diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index a1183f8..d481a1d 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -2,7 +2,6 @@ module Quox.Context
 
 import Quox.Syntax.Shift
 import Quox.Pretty
-import public Quox.NatExtra
 
 import Data.DPair
 import Data.Nat
@@ -44,14 +43,12 @@ toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
 toSnocList [<]        = [<]
 toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
 
-private
-toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
-toListAcc [<]        acc = acc
-toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
-
 export %inline
 toList : Telescope tm _ _ -> List (Exists tm)
-toList tel = toListAcc tel []
+toList tel = toListAcc tel [] where
+  toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
+  toListAcc [<]        acc = acc
+  toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
 
 export %inline
 toSnocList' : Telescope' a _ _ -> SnocList a
@@ -100,16 +97,6 @@ find p [<]        = empty
 find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx)
 
 
-||| a triangle of bindings. each type binding in a context counts the ues of
-||| others in its type, and all of these together form a triangle.
-public export
-Triangle : (tm : Nat -> Type) -> (len : Nat) -> Type
-Triangle = Context . Context
-
-public export
-Triangle' : Type -> (len : Nat) -> Type
-Triangle' a = Context $ Context (\_ => a)
-
 export
 0 telescopeLTE : Telescope _ from to -> from `LTE` to
 telescopeLTE [<]        = reflexive
@@ -165,28 +152,6 @@ export %inline
 (<$) : (forall n. tm1 n) -> Telescope tm2 from to -> Telescope tm1 from to
 x <$ tel = const x <$> tel
 
-export
-teleLte' : Telescope tm from to -> from `LTE'` to
-teleLte' [<]        = LTERefl
-teleLte' (tel :< _) = LTESuccR (teleLte' tel)
-
-
-export
-tabulate : ((n : Nat) -> tm n) ->
-           (from, to : Nat) -> from `LTE'` to => Telescope tm from to
-tabulate f from from   @{LTERefl}    = [<]
-tabulate f from (S to) @{LTESuccR _} = tabulate f from to :< f to
-
-export
-tabulate0 : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
-tabulate0 f n = tabulate f 0 n
-
-
-export
-pure : from `LTE'` to => a -> Telescope' a from to
-pure @{LTERefl}    x = [<]
-pure @{LTESuccR _} x = pure x :< x
-
 
 export %inline
 zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
@@ -194,14 +159,6 @@ zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
           Telescope tm3 from to
 zipWith f tel1 tel2 = f <$> tel1 <*> tel2
 
-export %inline
-zipWith3 : (forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
-           Telescope tm1 from to ->
-           Telescope tm2 from to ->
-           Telescope tm3 from to ->
-           Telescope tm4 from to
-zipWith3 f tel1 tel2 tel3 = f <$> tel1 <*> tel2 <*> tel3
-
 export %inline
 zipWithLazy : forall tm1, tm2, tm3.
               (forall n. tm1 n -> tm2 n -> tm3 n) ->
@@ -209,22 +166,6 @@ zipWithLazy : forall tm1, tm2, tm3.
               Telescope (\n => Lazy (tm3 n)) from to
 zipWithLazy f = zipWith $ delay .: f
 
-export %inline
-zipWith3Lazy : forall tm1, tm2, tm3, tm4.
-               (forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
-               Telescope tm1 from to ->
-               Telescope tm2 from to ->
-               Telescope tm3 from to ->
-               Telescope (\n => Lazy (tm4 n)) from to
-zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
-
-
-export
-unzip : Telescope (\i => (tm1 i, tm2 i)) from to ->
-        (Telescope tm1 from to, Telescope tm2 from to)
-unzip [<]             = ([<], [<])
-unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y)
-
 
 export
 lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
@@ -264,37 +205,9 @@ foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
 foldLazy = foldMap force
 
 
-export %inline
-and : Telescope' (Lazy Bool) _ _ -> Bool
-and = force . fold @{All}
-
-export %inline
-all : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
-all p = and . map (delay . p)
-
-export %inline
-all2 : (forall n. tm n -> tm2 n -> Bool) ->
-       Telescope tm from to -> Telescope tm2 from to -> Bool
-all2 p = and .: zipWithLazy p
-
-
-export %inline
-or : Telescope' (Lazy Bool) _ _ -> Bool
-or = force . fold @{Any}
-
-export %inline
-any : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
-any p = or . map (delay . p)
-
-export %inline
-any2 : (forall n. tm1 n -> tm2 n -> Bool) ->
-       Telescope tm1 from to -> Telescope tm2 from to -> Bool
-any2 p = or .: zipWithLazy p
-
-
 export %inline
 (forall n. Eq (tm n)) => Eq (Telescope tm from to) where
-  (==) = all2 (==)
+  (==) = foldLazy @{All} .: zipWithLazy (==)
 
 export %inline
 (forall n. Ord (tm n)) => Ord (Telescope tm from to) where
diff --git a/lib/Quox/NatExtra.idr b/lib/on-hold/Quox/NatExtra.idr
similarity index 100%
rename from lib/Quox/NatExtra.idr
rename to lib/on-hold/Quox/NatExtra.idr
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index de96f7c..2134fa4 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -8,7 +8,6 @@ license   = "acsl"
 depends = base, contrib, elab-util, snocvect
 
 modules =
-  Quox.NatExtra,
   Quox.BoolExtra,
   Quox.CharExtra,
   Quox.Decidable,