formatting etc

src/Quox/Context.idr

@@ -106,8 +106,8 @@ telescopeLTE [<]        = reflexive {rel=Nat.LTE}
 telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
 
 export
-(from `GT` to) => Uninhabited (Telescope _ from to) where
+(gt : from `GT` to) => Uninhabited (Telescope _ from to) where
-  uninhabited tel = void $ LTEImpliesNotGT (telescopeLTE tel) %search
+  uninhabited tel = void $ LTEImpliesNotGT (telescopeLTE tel) gt
 
 export %hint
 0 succGT : S n `GT` n
@@ -135,18 +135,16 @@ parameters {auto _ : Applicative f}
   sequence : Telescope (f . tm) from to -> f (Telescope tm from to)
   sequence = traverse id
 
-export %inline
+parameters {0 tm1, tm2 : Nat -> Type}
-map : (forall n. tm1 n -> tm2 n) ->
+           (f : forall n. tm1 n -> tm2 n)
-      Telescope tm1 from to -> Telescope tm2 from to
+  export %inline
-map f = runIdentity . traverse (pure . f)
+  map : Telescope tm1 from to -> Telescope tm2 from to
+  map = runIdentity . traverse (pure . f)
 
-infixr 4 <$>
+  export %inline
-export %inline
+  (<$>) : Telescope tm1 from to -> Telescope tm2 from to
-(<$>) : (forall n. tm1 n -> tm2 n) ->
+  (<$>) = map
-        Telescope tm1 from to -> Telescope tm2 from to
-(<$>) = map
 
-infixl 3 <*>
 export %inline
 (<*>) : Telescope (\n => tm1 n -> tm2 n) from to ->
         Telescope tm1 from to -> Telescope tm2 from to

src/Quox/Syntax/DimEq.idr

@@ -52,37 +52,42 @@ export
 ZeroIsOne :<? d = ZeroIsOne
 C eqs     :<? d = C $ eqs :< d
 
-private
+
+private %inline
+ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
+ifVar i p = map $ \q => if isYes $ q `decEq` B i then p else q
+
+private %inline
 checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
 checkConst Zero Zero eqs = C eqs
 checkConst One  One  eqs = C eqs
 checkConst _    _    _   = ZeroIsOne
 
-
 export
 setConst : Var d -> DimConst -> DimEq' d -> DimEq d
 setConst VZ e (eqs :< Nothing)    = C $ eqs :< Just (K e)
 setConst VZ e (eqs :< Just (K f)) = checkConst e f $ eqs :< Just (K f)
 setConst VZ e (eqs :< Just (B i)) = setConst i e eqs :<? Just (K e)
-setConst (VS i) e (eqs :< x) =
+setConst (VS i) e (eqs :< p)      = setConst i e eqs :<? ifVar i (K e) p
-  setConst i e eqs :<? (if x == Just (B i) then Just (K e) else x)
 
 mutual
   private
   setVar' : (i, j : Var d) -> i `LT` j -> DimEq' d -> DimEq d
-  setVar' VZ (VS i) LTZ (eqs :< Nothing)    = C $ eqs :< Just (B i)
+  setVar' VZ (VS i) LTZ (eqs :< Nothing) =
-  setVar' VZ (VS i) LTZ (eqs :< Just (K e)) = setConst i e eqs :<? Just (K e)
+    C $ eqs :< Just (B i)
-  setVar' VZ (VS i) LTZ (eqs :< Just (B j)) = setVar i j eqs :<? Just (B (max i j))
+  setVar' VZ (VS i) LTZ (eqs :< Just (K e)) =
+    setConst i e eqs :<? Just (K e)
+  setVar' VZ (VS i) LTZ (eqs :< Just (B j)) =
+    setVar i j eqs :<? Just (B (max i j))
   setVar' (VS i) (VS j) (LTS lt) (eqs :< p) =
-    setVar' i j lt eqs :<? map (\k => if k == B i then B j else k) p
+    setVar' i j lt eqs :<? ifVar i (B j) p
 
   export
   setVar : (i, j : Var d) -> DimEq' d -> DimEq d
-  setVar i j eqs =
+  setVar i j eqs with (compareP i j)
-    case compareP i j of
+    _              | IsLT lt = setVar' i j lt eqs
-      IsLT lt => setVar' i j lt eqs
+    setVar i i eqs | IsEQ    = C eqs
-      IsEQ    => C eqs
+    _              | IsGT gt = setVar' j i gt eqs
-      IsGT gt => setVar' j i gt eqs
 
 
 export
@@ -123,13 +128,10 @@ split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs)
 
 export
 splits' : DimEq' d -> List (DSubst d 0)
-splits' [<] = [id]
+splits' [<]          = [id]
-splits' eqs@(_ :< _) = do
+splits' eqs@(_ :< _) = [th . ph | (eqs', th) <- split eqs, ph <- splits' eqs']
-  (eqs, th) <- split eqs
-  ph <- splits' eqs
-  pure $ th . ph
 
 export
 splits : DimEq d -> List (DSubst d 0)
 splits ZeroIsOne = []
-splits (C eqs) = splits' eqs
+splits (C eqs)   = splits' eqs

src/Quox/Syntax/Term.idr

@@ -51,7 +51,7 @@ mutual
   public export
   data Elim : (d, n : Nat) -> Type where
     ||| free variable
-    F  : (x : Name) -> Elim d n
+    F : (x : Name) -> Elim d n
     ||| bound variable
     B : (i : Var n) -> Elim d n
 
@@ -78,12 +78,12 @@ FT = E . F
 ||| abbreviation for a bound variable like `BV 4` instead of
 ||| `B (VS (VS (VS (VS VZ))))`
 public export %inline
-BV : (i : Nat) -> {auto 0 p : LT i n} -> Elim d n
+BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
 BV i = B $ V i
 
 ||| same as `BV` but as a term
 public export %inline
-BVT : (i : Nat) -> {auto 0 p : LT i n} -> Term d n
+BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
 BVT i = E $ BV i
 
 
@@ -213,8 +213,8 @@ CanSubst (Elim d) (Term d) where
 export CanSubst Var (Term d) where s // th = s // map (B {d}) th
 export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
 
-export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)}
+export CanShift (Term d) where i // by = i // Shift by {env = Elim d}
-export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}
+export CanShift (Elim d) where i // by = i // Shift by {env = Elim d}
 
 
 infixl 8 ///
@@ -294,11 +294,11 @@ 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
+ncloT t @{p} = Element t p
 
 public export %inline
 ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
-ncloE e = Element e %search
+ncloE e @{p} = Element e p
 
 
 
@@ -393,13 +393,16 @@ parameters {0 t : ty1 -> ty2 -> Type}
   some2 t = some $ some t
 
 ||| A term of some unknown scope sizes.
-public export SomeTerm : Type
+public export
+SomeTerm : Type
 SomeTerm = Exists2 Term
 
 ||| An elimination of some unknown scope sizes.
-public export SomeElim : Type
+public export
+SomeElim : Type
 SomeElim = Exists2 Elim
 
 ||| A dimension of some unknown scope size.
-public export SomeDim : Type
+public export
+SomeDim : Type
 SomeDim = Exists Dim

src/Quox/Syntax/Var.idr

@@ -120,7 +120,7 @@ weakSpecCorrect (LTESucc x) (VS i) = cong S $ weakSpecCorrect x i
 
 export
 0 weakCorrect : (p : m `LTE` n) -> (i : Var m) -> (weak p i).nat = i.nat
-weakCorrect LTEZero     _ impossible
+weakCorrect LTEZero     _      impossible
 weakCorrect (LTESucc p) VZ     = Refl
 weakCorrect (LTESucc p) (VS i) = cong S $ weakCorrect p i
 
@@ -149,7 +149,7 @@ i `GT` j = j `LT` i
 export
 Transitive (Var n) LT where
   transitive LTZ     (LTS _) = LTZ
-  transitive (LTS p) (LTS q) = LTS $ transitive p q {rel=Var.LT}
+  transitive (LTS p) (LTS q) = LTS $ transitive p q {rel = Var.LT}
 
 export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
 export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible

src/Quox/Typing.idr

@@ -8,9 +8,9 @@ import Data.SortedMap
 import Control.Monad.Reader
 import Control.Monad.State
 
-
 %default total
 
+
 public export
 data DContext : Nat -> Type where
   DNil  : DContext 0