From a5b07672ae9fad959693be87d07b664d20a2ee92 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Sep 2021 20:14:13 +0200
Subject: [PATCH] renaming etc in closure stuff

---
 src/Quox/Syntax/Term.idr | 67 +++++++++++++++++++++++++---------------
 1 file changed, 42 insertions(+), 25 deletions(-)

diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 00a5836..d10d41d 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -259,29 +259,46 @@ comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
 comp' th ps ph = map (/// th) ps . ph
 
 
-||| true if an elimination has a closure or dimension closure at the top level
-public export %inline
-topCloE : Elim d n -> Bool
-topCloE (CloE  _ _) = True
-topCloE (DCloE _ _) = True
-topCloE _           = False
+mutual
+  ||| true if a term has a closure or dimension closure at the top level,
+  ||| or is `E` applied to such an elimination
+  public export %inline
+  topCloT : Term d n -> Bool
+  topCloT (CloT  _ _) = True
+  topCloT (DCloT _ _) = True
+  topCloT (E e)       = topCloE e
+  topCloT _           = False
 
-||| true if a term has a closure or dimension closure at the top level,
-||| or is `E` applied to such an elimination
-public export %inline
-topCloT : Term d n -> Bool
-topCloT (CloT  _ _) = True
-topCloT (DCloT _ _) = True
-topCloT (E e)       = topCloE e
-topCloT _           = False
+  ||| true if an elimination has a closure or dimension closure at the top level
+  public export %inline
+  topCloE : Elim d n -> Bool
+  topCloE (CloE  _ _) = True
+  topCloE (DCloE _ _) = True
+  topCloE _           = False
 
-||| an elimination which is not a top level closure
-public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) $ So . not . topCloE
+
+public export IsNotCloT : Term d n -> Type
+IsNotCloT = So . not . topCloT
 
 ||| a term which is not a top level closure
 public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) $ So . not . topCloT
+NotCloTerm d n = Subset (Term d n) IsNotCloT
+
+public export IsNotCloE : Elim d n -> Type
+IsNotCloE = So . not . topCloE
+
+||| an elimination which is not a top level closure
+public export NotCloElim : Nat -> Nat -> Type
+NotCloElim d n = Subset (Elim d n) IsNotCloE
+
+public export %inline
+ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
+ncloT t = Element t %search
+
+public export %inline
+ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
+ncloE e = Element e %search
+
 
 
 mutual
@@ -301,13 +318,13 @@ mutual
   pushSubstsT' : DSubst dfrom dto -> TSubst dto from to ->
                  Term dfrom from -> NotCloTerm dto to
   pushSubstsT' th ph (TYPE l) =
-    Element (TYPE l) Oh
+    ncloT $ TYPE l
   pushSubstsT' th ph (Pi qty qtm x a b) =
-    Element (Pi qty qtm x (subs a th ph) (subs b th (push ph))) Oh
+    ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph))
   pushSubstsT' th ph (Lam x t) =
-    Element (Lam x $ subs t th $ push ph) Oh
+    ncloT $ Lam x $ subs t th $ push ph
   pushSubstsT' th ph (E e) =
-    let Element e prf = pushSubstsE' th ph e in Element (E e) prf
+    let Element e _ = pushSubstsE' th ph e in ncloT $ E e
   pushSubstsT' th ph (CloT  s ps) =
     pushSubstsT' th (comp' th ps ph) s
   pushSubstsT' th ph (DCloT s ps) =
@@ -317,13 +334,13 @@ mutual
   pushSubstsE' : DSubst dfrom dto -> TSubst dto from to ->
                  Elim dfrom from -> NotCloElim dto to
   pushSubstsE' th ph (F x) =
-    Element (F x) Oh
+    ncloE $ F x
   pushSubstsE' th ph (B i) =
     assert_total pushSubstsE $ ph !! i
   pushSubstsE' th ph (f :@ s) =
-    Element (subs f th ph :@ subs s th ph) Oh
+    ncloE $ subs f th ph :@ subs s th ph
   pushSubstsE' th ph (s :# a) =
-    Element (subs s th ph :# subs a th ph) Oh
+    ncloE $ subs s th ph :# subs a th ph
   pushSubstsE' th ph (CloE  e ps) =
     pushSubstsE' th (comp' th ps ph) e
   pushSubstsE' th ph (DCloE e ps) =