From cd8ee29281cd35886d38f27dd08fe0361e6ed2a6 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Mon, 25 Jul 2022 00:35:20 +0200
Subject: [PATCH] changed some case orders to maybe optimize code a bit
 (maybe?)

---
 src/Core/Check.idr     | 30 +++++++++++++++---------------
 src/Core/Convert.idr   | 15 ++++++++-------
 src/Core/Normalize.idr | 12 ++++++------
 3 files changed, 29 insertions(+), 28 deletions(-)

diff --git a/src/Core/Check.idr b/src/Core/Check.idr
index 68954df..0683650 100644
--- a/src/Core/Check.idr
+++ b/src/Core/Check.idr
@@ -65,8 +65,13 @@ mutual
 
   -- terms types term
   infer : Ctx n -> Ctx n -> Term n -> PI Value
-  infer trs tys (TVar i)   = pure (index i tys)
   infer trs tys TType      = pure VType
+  infer trs tys TTop      = pure VType
+  infer trs tys TBot      = pure VType
+  infer trs tys TNat      = pure VType
+  infer trs tys TStar     = pure VTop
+  infer trs tys TZero     = pure VNat
+  infer trs tys (TVar i)   = pure (index i tys)
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
                               \case
                                  VClos env (TPi a b) => do
@@ -76,24 +81,10 @@ mutual
 
                                  _ => oops "expected infer pi"
 
-  infer trs tys TTop      = pure VType
-  infer trs tys TBot      = pure VType
-  infer trs tys TNat      = pure VType
-  infer trs tys TStar     = pure VTop
-  infer trs tys TZero     = pure VNat
   infer trs tys (TSuc n)  = do 
     guardS "suc n" =<< check trs tys VNat n
     pure VNat
 
-  infer trs tys (TTopInd c st) = do
-    guardS "⊤ C" =<< check trs tys (VClos trs (TPi TTop TType)) c
-    guardS "⊤ ★" =<< check trs tys (VApp (VClos trs c) VStar)   st
-    pure (VClos trs (TPi TTop (TApp (weakTr c) (TVar 0))))
-
-  infer trs tys (TBotInd c) = do
-    guardS "⊥ C" =<< check trs tys (VClos trs (TPi TBot TType)) c
-    pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
-
   infer trs tys (TNatInd c z s) = do
     guardS "ℕ C" =<< check trs tys (VClos trs (TPi TNat TType)) c
     guardS "ℕ z" =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
@@ -116,6 +107,15 @@ mutual
         guardS "let infer" =<< check trs tys (VClos trs ty) tr
         infer !(extT trs trs tr) !(extT tys trs ty) tri
 
+  infer trs tys (TTopInd c st) = do
+    guardS "⊤ C" =<< check trs tys (VClos trs (TPi TTop TType)) c
+    guardS "⊤ ★" =<< check trs tys (VApp (VClos trs c) VStar)   st
+    pure (VClos trs (TPi TTop (TApp (weakTr c) (TVar 0))))
+
+  infer trs tys (TBotInd c) = do
+    guardS "⊥ C" =<< check trs tys (VClos trs (TPi TBot TType)) c
+    pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
+
   infer trs tys x          = oops ("cannot infer type" ++ show x)
 
 public export
diff --git a/src/Core/Convert.idr b/src/Core/Convert.idr
index c293a95..8c1efd9 100644
--- a/src/Core/Convert.idr
+++ b/src/Core/Convert.idr
@@ -23,13 +23,15 @@ convert u1 u2 = do
   logS ("with value representations '" ++ show u1' ++ "' and '" ++ show u2' ++ "'.")
   assert_total $ -- :(
     case (u1', u2') of
-      (VGen k1, VGen k2) => pure (k1 == k2)
       (VType, VType) => pure True
       (VTop, VTop)   => pure True
       (VStar, VStar) => pure True
       (VBot, VBot)   => pure True
       (VNat, VNat)   => pure True
 
+      (VGen k1, VGen k2) => pure (k1 == k2)
+      (VNatTr n, VNatTr m) => pure (n == m)
+
       (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
 
       (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
@@ -41,14 +43,8 @@ convert u1 u2 = do
         guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2)
         convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
 
-      (VNatTr n, VNatTr m) => pure (n == m)
-
       (VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2
 
-      (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
-        termGuard env1 env2 c1 c2
-        termConv  env1 env2 st1 st2
-
       (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
 
       (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
@@ -75,6 +71,11 @@ convert u1 u2 = do
         v <- VGen <$> fresh
         convert vsc (VClos (v :: env) sc)
 
+      (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
+        termGuard env1 env2 c1 c2
+        termConv  env1 env2 st1 st2
+
+
       _ => pure False
   where
     termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool
diff --git a/src/Core/Normalize.idr b/src/Core/Normalize.idr
index de9d31a..aabc450 100644
--- a/src/Core/Normalize.idr
+++ b/src/Core/Normalize.idr
@@ -50,16 +50,16 @@ mutual
   public export
   eval : Ctx n -> Term n -> PI Value
   eval env (TVar i)   = pure (index i env)
-  eval env (TApp f x) = do
-    f' <- eval env f
-    x' <- eval env x
-    assert_total (app f' x') -- :(
   eval env TType       = pure VType
   eval env TTop        = pure VTop
   eval env TStar       = pure VStar
   eval env TBot        = pure VBot
   eval env TNat        = pure VNat
   eval env TZero       = pure (VNatTr 0)
+  eval env (TApp f x)  = do
+    f' <- eval env f
+    x' <- eval env x
+    assert_total (app f' x') -- :(
 
   eval env (TSuc n)    = do
     n' <- eval env n
@@ -77,10 +77,11 @@ mutual
     tr' <- eval env tr
     eval (tr' :: env) tri
 
-  eval env tr          = pure (VClos env tr)
+  eval env tr         = pure (VClos env tr)
 
 public export
 whnf : Value -> PI Value
+whnf (VClos env tr) = eval env tr
 whnf (VApp f x) = do
   f' <- whnf f
   x' <- whnf x
@@ -89,5 +90,4 @@ whnf (VPair a b) = do
   a' <- whnf a
   b' <- whnf b
   pure (VPair a' b')
-whnf (VClos env tr) = eval env tr
 whnf v              = pure v