add some comments

lib/Quox/Reduce.idr

@@ -37,6 +37,10 @@ where
   whnf : {d, n : Nat} -> (defs : Definitions) ->
          (ctx : WhnfContext d n) ->
          tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
+  -- having isRedex be part of the class header, and needing to be explicitly
+  -- quantified on every use since idris can't infer its type, is a little ugly.
+  -- but none of the alternatives i've thought of so far work. e.g. in some
+  -- cases idris can't tell that `isRedex` and `isRedexT` are the same thing
 
 public export %inline
 whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
@@ -60,30 +64,35 @@ nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
 nred t = Element t nr
 
 
+||| an expression like `(λ x ⇒ s) ∷ π.(x : A) → B`
 public export %inline
 isLamHead : Elim {} -> Bool
 isLamHead (Ann (Lam {}) (Pi {}) _) = True
 isLamHead (Coe {})                 = True
 isLamHead _                        = False
 
+||| an expression like `(δ 𝑖 ⇒ s) ∷ Eq (𝑖 ⇒ A) s t`
 public export %inline
 isDLamHead : Elim {} -> Bool
 isDLamHead (Ann (DLam {}) (Eq {}) _) = True
 isDLamHead (Coe {})                  = True
 isDLamHead _                         = False
 
+||| an expression like `(s, t) ∷ (x : A) × B`
 public export %inline
 isPairHead : Elim {} -> Bool
 isPairHead (Ann (Pair {}) (Sig {}) _) = True
 isPairHead (Coe {})                   = True
 isPairHead _                          = False
 
+||| an expression like `'a ∷ {a, b, c}`
 public export %inline
 isTagHead : Elim {} -> Bool
 isTagHead (Ann (Tag {}) (Enum {}) _) = True
 isTagHead (Coe {})                   = True
 isTagHead _                          = False
 
+||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ`
 public export %inline
 isNatHead : Elim {} -> Bool
 isNatHead (Ann (Zero {}) (Nat {}) _) = True
@@ -91,23 +100,26 @@ isNatHead (Ann (Succ {}) (Nat {}) _) = True
 isNatHead (Coe {})                   = True
 isNatHead _                          = False
 
+||| an expression like `[s] ∷ [π. A]`
 public export %inline
 isBoxHead : Elim {} -> Bool
 isBoxHead (Ann (Box {}) (BOX {}) _) = True
 isBoxHead (Coe {})                  = True
 isBoxHead _                         = False
 
+||| an elimination in a term context
 public export %inline
 isE : Term {} -> Bool
 isE (E {}) = True
 isE _      = False
 
+||| an expression like `s ∷ A`
 public export %inline
 isAnn : Elim {} -> Bool
 isAnn (Ann {}) = True
 isAnn _        = False
 
-||| true if a term is syntactically a type.
+||| a syntactic type
 public export %inline
 isTyCon : Term {} -> Bool
 isTyCon (TYPE  {}) = True
@@ -128,17 +140,18 @@ isTyCon (E     {}) = False
 isTyCon (CloT  {}) = False
 isTyCon (DCloT {}) = False
 
-||| true if a term is syntactically a type, or a neutral.
+||| a syntactic type, or a neutral
 public export %inline
 isTyConE : Term {} -> Bool
 isTyConE s = isTyCon s || isE s
 
-||| true if a term is syntactically a type.
+||| a syntactic type with an annotation `★ᵢ`
 public export %inline
 isAnnTyCon : Elim {} -> Bool
 isAnnTyCon (Ann ty (TYPE {}) _) = isTyCon ty
 isAnnTyCon _                    = False
 
+||| 0 or 1
 public export %inline
 isK : Dim d -> Bool
 isK (K {}) = True
@@ -146,6 +159,24 @@ isK _      = False
 
 
 mutual
+  ||| a reducible elimination
+  |||
+  ||| - a free variable, if its definition is known
+  ||| - an application whose head is an annotated lambda,
+  |||   a case expression whose head is an annotated constructor form, etc
+  ||| - a redundant annotation, or one whose term or type is reducible
+  ||| - coercions `coe (𝑖 ⇒ A) @p @q s` where:
+  |||     - `A` is in whnf, or
+  |||     - `𝑖` is not mentioned in `A`, or
+  |||     - `p = q`
+  |||     - [fixme] this is not true right now but that's because i wrote it
+  |||       wrong
+  ||| - compositions `comp A @p @q s @r {⋯}` where:
+  |||     - `A` is in whnf, or
+  |||     - `p = q`, or
+  |||     - `r = 0` or `r = 1`
+  |||     - [fixme] the p=q condition is also missing here
+  ||| - closures
   public export
   isRedexE : RedexTest Elim
   isRedexE defs (F {x, _}) {d, n} =
@@ -174,6 +205,12 @@ mutual
   isRedexE _ (CloE  {}) = True
   isRedexE _ (DCloE {}) = True
 
+  ||| a reducible term
+  |||
+  ||| - a reducible elimination, as `isRedexE`
+  ||| - an annotated elimination
+  |||   (the annotation is redundant in a checkable context)
+  ||| - a closure
   public export
   isRedexT : RedexTest Term
   isRedexT _    (CloT  {}) = True
@@ -328,7 +365,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
     pure (a0, a1, a, l, r)
   tycaseEq t = throw $ ExpectedEq t.loc ctx.names t
 
--- new block because the functions below might pass a different ctx
+
+-- new block because the functions below pass a different ctx
 -- into the ones above
 parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   ||| reduce a function application `App (Coe ty p q val) s loc`