summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Core/Reducible.idr105
1 files changed, 47 insertions, 58 deletions
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)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 17:17:15 +0000