From 8d5f72c76289e4410ed9474551f42a5851b14230 Mon Sep 17 00:00:00 2001
From: LuoChen <luochen1990@gmail.com>
Date: Fri, 20 Sep 2019 12:43:25 +0800
Subject: [PATCH] reimpl: rigPlus & rigMult in Core/TT

---
 src/Core/TT.idr | 30 ++++++++++++------------------
 1 file changed, 12 insertions(+), 18 deletions(-)

diff --git a/src/Core/TT.idr b/src/Core/TT.idr
index 7cc4209..a3de943 100644
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@@ -231,29 +231,23 @@ Show RigCount where
   show Rig1 = "Rig1"
   show RigW = "RigW"
 
+fromInt : Int -> RigCount
+fromInt 0 = Rig0
+fromInt 1 = Rig1
+fromInt _ = RigW
+
+toInt : RigCount -> Int
+toInt Rig0 = 0
+toInt Rig1 = 1
+toInt RigW = 2
+
 export
 rigPlus : RigCount -> RigCount -> RigCount
-rigPlus Rig0 Rig0 = Rig0
-rigPlus Rig0 Rig1 = Rig1
-rigPlus Rig0 RigW = RigW
-rigPlus Rig1 Rig0 = Rig1
-rigPlus Rig1 Rig1 = RigW
-rigPlus Rig1 RigW = RigW
-rigPlus RigW Rig0 = RigW
-rigPlus RigW Rig1 = RigW
-rigPlus RigW RigW = RigW
+rigPlus a b = fromInt (toInt a + toInt b)
 
 export
 rigMult : RigCount -> RigCount -> RigCount
-rigMult Rig0 Rig0 = Rig0
-rigMult Rig0 Rig1 = Rig0
-rigMult Rig0 RigW = Rig0
-rigMult Rig1 Rig0 = Rig0
-rigMult Rig1 Rig1 = Rig1
-rigMult Rig1 RigW = RigW
-rigMult RigW Rig0 = Rig0
-rigMult RigW Rig1 = RigW
-rigMult RigW RigW = RigW
+rigMult a b = fromInt (toInt a * toInt b)
 
 public export
 data Binder : Type -> Type where