From 348a57e18df85c74dee37a4013a1878716b91aac Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 23 Apr 2023 14:03:09 +0100
Subject: Use custom relation for even more control.

---
 src/Core/Reducible.idr | 105 ++++++++++++++++++++++---------------------------
 1 file changed, 47 insertions(+), 58 deletions(-)

(limited to 'src')

diff --git a/src/Core/Reducible.idr b/src/Core/Reducible.idr
index ea37093..0bb4027 100644
--- a/src/Core/Reducible.idr
+++ b/src/Core/Reducible.idr
@@ -1,7 +1,5 @@
 module Core.Reducible
 
-import Control.WellFounded
-
 import Core.Declarative
 import Core.Environment
 import Core.Generic
@@ -14,14 +12,20 @@ import Core.Thinning
 
 %prefix_record_projections off
 
+-- Levels ----------------------------------------------------------------------
+
 data Level = Small | Large
 
 %name Level l
 
-export
-Sized Level where
-  size Small = 0
-  size Large = 1
+public export
+data LT : Level -> Level -> Type where
+  LTSmall : Small `LT` Large
+
+Uninhabited (l `LT` Small) where uninhabited prf impossible
+Uninhabited (Large `LT` l) where uninhabited prf impossible
+
+-- Logical Relation ------------------------------------------------------------
 
 public export
 record LogicalRelation (eq : Equality) where
@@ -35,7 +39,7 @@ public export
 data TypeRed :
   (eq : Equality) ->
   (l : Level) ->
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq) ->
   (env : Env n) ->
   (a : Term n) ->
   Type
@@ -43,7 +47,7 @@ public export
 data TypeEq :
   (eq : Equality) ->
   (l : Level) ->
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq) ->
   (env : Env n) ->
   (a, b : Term n) ->
   TypeRed eq l rec {n} env a ->
@@ -52,7 +56,7 @@ public export
 data TermRed :
   (eq : Equality) ->
   (l : Level) ->
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq) ->
   (env : Env n) ->
   (t, a : Term n) ->
   TypeRed eq l rec {n} env a ->
@@ -61,7 +65,7 @@ public export
 data TermEq :
   (eq : Equality) ->
   (l : Level) ->
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq) ->
   (env : Env n) ->
   (t, u, a : Term n) ->
   TypeRed eq l rec {n} env a ->
@@ -73,7 +77,7 @@ public export
 record NeutralTyRed
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (a : Term n)
   where
@@ -89,7 +93,7 @@ public export
 record NeutralTyEq
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (a, b : Term n)
   (red : NeutralTyRed eq l rec {n} env a)
@@ -106,7 +110,7 @@ public export
 record NeutralTmRed
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (t, a : Term n)
   (red : NeutralTyRed eq l rec {n} env a)
@@ -123,7 +127,7 @@ public export
 record NeutralTmEq
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (t, u, a : Term n)
   (red : NeutralTyRed eq l rec {n} env a)
@@ -146,7 +150,7 @@ public export
 record SetTyRed
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (a : Term n)
   where
@@ -154,13 +158,13 @@ record SetTyRed
   tyWf : TypeWf env a
   steps : TypeReduce env a Set
   tyWf' : TypeWf env Set
-  prf : Smaller Small l
+  prf : Small `LT` l
 
 public export
 record SetTyEq
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (a, b : Term n)
   (red : SetTyRed eq l rec {n} env a)
@@ -174,7 +178,7 @@ public export
 record SetTmRed
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (t, a : Term n)
   (red : SetTyRed eq l rec {n} env a)
@@ -183,7 +187,7 @@ record SetTmRed
   {0 t' : Term n}
   tmWf : TermWf env t a
   steps : TypeReduce env t t'
-  tyWf' : TermWf env t' a
+  tmWf' : TermWf env t' a
   0 whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   tyRed : (rec Small red.prf).TypeRed env t
@@ -192,7 +196,7 @@ public export
 record SetTmEq
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (t, u, a : Term n)
   (red : SetTyRed eq l rec {n} env a)
@@ -203,8 +207,8 @@ record SetTmEq
   tmWf2 : TermWf env u a
   steps1 : TypeReduce env t t'
   steps2 : TypeReduce env u u'
-  tyWf1' : TermWf env t' Set
-  tyWf2' : TermWf env u' Set
+  tmWf1' : TermWf env t' a
+  tmWf2' : TermWf env u' a
   0 whnf1 : Whnf t'
   0 whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
@@ -218,7 +222,7 @@ public export
 record PiTyRed
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (a : Term n)
   where
@@ -228,8 +232,7 @@ record PiTyRed
   tyWf : TypeWf env a
   steps : TypeReduce env a (Pi f g)
   tyWf' : TypeWf env (Pi f g)
-  domWf : TypeWf env f
-  codWf : TypeWf (env :< pure f) g
+  prf : eq.TypeEq env (Pi f g) (Pi f g)
   domRed :
     forall m.
     {0 thin : n `Thins` m} ->
@@ -262,7 +265,7 @@ public export
 record PiTyEq
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (a, b : Term n)
   (red : PiTyRed eq l rec env a)
@@ -296,7 +299,7 @@ public export
 record PiTmRed
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (t, a : Term n)
   (red : PiTyRed eq l rec env a)
@@ -338,7 +341,7 @@ public export
 record PiTmEq
   (eq : Equality)
   (l : Level)
-  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq)
   (env : Env n)
   (t, u, a : Term n)
   (red : PiTyRed eq l rec env a)
@@ -391,40 +394,26 @@ data TermEq where
   EqSetTm : SetTmEq eq l rec env t u a red -> TermEq eq l rec env t u a (RedSetTy red)
   EqPiTm : PiTmEq eq l rec env t u a red -> TermEq eq l rec env t u a (RedPiTy red)
 
--- Induction -------------------------------------------------------------------
-
-public export
-levelAccRecurse : (sizeL : Nat) -> (l' : Level) -> (size l' `LT` sizeL) -> SizeAccessible l'
-levelAccRecurse (S l) l' (LTESucc prf) =
-  Access (\l'', prf' => levelAccRecurse l l'' $ transitive prf' prf)
-
-public export
-levelAccessible : (l : Level) -> SizeAccessible l
-levelAccessible l = Access (levelAccRecurse $ size l)
-
 public export
-levelIndHelper :
-  {0 p : Level -> Type} ->
-  (step : (l : Level) -> ((l' : Level) -> Smaller l' l -> p l') -> p l) ->
+LogRelKit :
+  (eq : Equality) ->
   (l : Level) ->
-  (0 acc : SizeAccessible l) ->
-  p l
-levelIndHelper step l (Access rec) = step l (\l', prf => levelIndHelper step l' $ rec l' prf)
+  (rec : (l' : Level) -> l' `LT` l -> LogicalRelation eq) ->
+  LogicalRelation eq
+LogRelKit eq l rec =
+  MkLogRel
+    (TypeRed eq l rec)
+    (TypeEq eq l rec)
+    (TermRed eq l rec)
+    (TermEq eq l rec)
+
+-- Induction -------------------------------------------------------------------
 
 public export
-levelInd :
-  {0 p : Level -> Type} ->
-  (step : (l : Level) -> ((l' : Level) -> Smaller l' l -> p l') -> p l) ->
-  (l : Level) ->
-  p l
-levelInd step l = levelIndHelper step l (levelAccessible l)
+LogRelRec : (eq : Equality) -> (l, l' : Level) -> l' `LT` l -> LogicalRelation eq
+LogRelRec eq Small _ prf = absurd prf
+LogRelRec eq Large Small LTSmall = LogRelKit eq Small (\_, prf => absurd prf)
 
 public export
 LogRel : (eq : Equality) -> Level -> LogicalRelation eq
-LogRel eq =
-  levelInd $ \l, rec =>
-    MkLogRel
-      (TypeRed eq l rec)
-      (TypeEq eq l rec)
-      (TermRed eq l rec)
-      (TermEq eq l rec)
+LogRel eq l = LogRelKit eq l (LogRelRec eq l)
-- 
cgit v1.2.3