From 0c1b3a78c3203d32030af16d80c7cee773f18037 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 8 Jan 2023 15:43:54 +0100
Subject: [PATCH] remove ope stuff too

---
 lib/Quox/Syntax/Term/Base.idr   |  2 +-
 lib/Quox/Syntax/Term/Reduce.idr | 74 ++++++++++++++++-----------------
 lib/Quox/Syntax/Var.idr         | 16 +++----
 lib/{ => on-hold}/Quox/OPE.idr  |  0
 lib/quox-lib.ipkg               |  2 +-
 5 files changed, 47 insertions(+), 47 deletions(-)
 rename lib/{ => on-hold}/Quox/OPE.idr (100%)

diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index a707495..f891a30 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -7,7 +7,7 @@ import public Quox.Syntax.Universe
 import public Quox.Syntax.Qty
 import public Quox.Syntax.Dim
 import public Quox.Name
-import public Quox.OPE
+-- import public Quox.OPE
 
 import Quox.Pretty
 
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index e1fac68..9ee5ab1 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -116,46 +116,46 @@ pushSubstsE' : Elim d n -> Elim d n
 pushSubstsE' e = (pushSubstsE e).fst
 
 
-mutual
-  -- tightening a term/elim also causes substitutions to be pushed through.
-  -- this is because otherwise a variable in an unused part of the subst
-  -- would cause it to incorrectly fail
+-- mutual
+--   -- tightening a term/elim also causes substitutions to be pushed through.
+--   -- this is because otherwise a variable in an unused part of the subst
+--   -- would cause it to incorrectly fail
 
-  export covering
-  Tighten (Term d) where
-    tighten p (TYPE l) =
-      pure $ TYPE l
-    tighten p (Pi qty x arg res) =
-      Pi qty x <$> tighten p arg
-               <*> tighten p res
-    tighten p (Lam x body) =
-      Lam x <$> tighten p body
-    tighten p (E e) =
-      E <$> tighten p e
-    tighten p (CloT tm th) =
-      tighten p $ pushSubstsTWith' id th tm
-    tighten p (DCloT tm th) =
-      tighten p $ pushSubstsTWith' th id tm
+--   export covering
+--   Tighten (Term d) where
+--     tighten p (TYPE l) =
+--       pure $ TYPE l
+--     tighten p (Pi qty x arg res) =
+--       Pi qty x <$> tighten p arg
+--                <*> tighten p res
+--     tighten p (Lam x body) =
+--       Lam x <$> tighten p body
+--     tighten p (E e) =
+--       E <$> tighten p e
+--     tighten p (CloT tm th) =
+--       tighten p $ pushSubstsTWith' id th tm
+--     tighten p (DCloT tm th) =
+--       tighten p $ pushSubstsTWith' th id tm
 
-  export covering
-  Tighten (Elim d) where
-    tighten p (F x) =
-      pure $ F x
-    tighten p (B i) =
-      B <$> tighten p i
-    tighten p (fun :@ arg) =
-      [|tighten p fun :@ tighten p arg|]
-    tighten p (tm :# ty) =
-      [|tighten p tm :# tighten p ty|]
-    tighten p (CloE el th) =
-      tighten p $ pushSubstsEWith' id th el
-    tighten p (DCloE el th) =
-      tighten p $ pushSubstsEWith' th id el
+--   export covering
+--   Tighten (Elim d) where
+--     tighten p (F x) =
+--       pure $ F x
+--     tighten p (B i) =
+--       B <$> tighten p i
+--     tighten p (fun :@ arg) =
+--       [|tighten p fun :@ tighten p arg|]
+--     tighten p (tm :# ty) =
+--       [|tighten p tm :# tighten p ty|]
+--     tighten p (CloE el th) =
+--       tighten p $ pushSubstsEWith' id th el
+--     tighten p (DCloE el th) =
+--       tighten p $ pushSubstsEWith' th id el
 
-  export covering
-  Tighten (ScopeTerm d) where
-    tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
-    tighten p (TUnused body) = TUnused <$> tighten p body
+--   export covering
+--   Tighten (ScopeTerm d) where
+--     tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
+--     tighten p (TUnused body) = TUnused <$> tighten p body
 
 
 public export %inline
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index a937fec..833f42f 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -2,7 +2,7 @@ module Quox.Syntax.Var
 
 import Quox.Name
 import Quox.Pretty
-import Quox.OPE
+-- import Quox.OPE
 
 import Data.Nat
 import Data.List
@@ -264,10 +264,10 @@ decEqFromBool i j =
 
 public export %inline DecEq (Var n) where decEq = varDecEq
 
-export
-Tighten Var where
-  tighten Id       i      = pure i
-  tighten (Drop q) VZ     = empty
-  tighten (Drop q) (VS i) = tighten q i
-  tighten (Keep q) VZ     = pure VZ
-  tighten (Keep q) (VS i) = VS <$> tighten q i
+-- export
+-- Tighten Var where
+--   tighten Id       i      = pure i
+--   tighten (Drop q) VZ     = empty
+--   tighten (Drop q) (VS i) = tighten q i
+--   tighten (Keep q) VZ     = pure VZ
+--   tighten (Keep q) (VS i) = VS <$> tighten q i
diff --git a/lib/Quox/OPE.idr b/lib/on-hold/Quox/OPE.idr
similarity index 100%
rename from lib/Quox/OPE.idr
rename to lib/on-hold/Quox/OPE.idr
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index d686162..eda73bb 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -10,7 +10,7 @@ depends = base, contrib, elab-util, sop, snocvect
 modules =
   Quox.NatExtra,
   -- Quox.Unicode,
-  Quox.OPE,
+  -- Quox.OPE,
   Quox.Pretty,
   Quox.Syntax,
   Quox.Syntax.Dim,