Bundle well-formed reductions.nameless

2 files changed, 78 insertions, 94 deletions

diff --git a/src/Core/LogRel.idr b/src/Core/LogRel.idr
index f7e2e06..b4fe23f 100644
--- a/src/Core/LogRel.idr
+++ b/src/Core/LogRel.idr
@@ -28,6 +28,20 @@ Uninhabited (Large `LT` l) where uninhabited prf impossible
 -- Logical Relation ------------------------------------------------------------
 
 public export
+record TypeReduceWf (env : Env n) (a, b : Term n) where
+  constructor MkTyReduceWf
+  tyWf : TypeWf env a
+  steps : TypeReduce env a b
+  tyWf' : TypeWf env b
+
+public export
+record TermReduceWf (env : Env n) (t, u, a : Term n) where
+  constructor MkTmReduceWf
+  tmWf : TermWf env t a
+  steps : TermReduce env t u a
+  tmWf' : TermWf env u a
+
+public export
 record LogicalRelation (eq : Equality) where
   constructor MkLogRel
   0 TypeRed : forall n. Env n -> Term n -> Type
@@ -83,9 +97,7 @@ record NeutralTyRed
   where
   constructor MkNtrlTyRed
   {0 a' : Term n}
-  tyWf : TypeWf env a
-  steps : TypeReduce env a a'
-  tyWf' : TypeWf env a'
+  stepsWf : TypeReduceWf env a a'
   ntrl : Neutral a'
   prf : eq.NtrlEq env (Element a' ntrl) (Element a' ntrl) Set
 
@@ -100,9 +112,7 @@ record NeutralTyEq
   where
   constructor MkNtrlTyEq
   {0 b' : Term n}
-  tyWf : TypeWf env b
-  steps : TypeReduce env b b'
-  tyWf' : TypeWf env b'
+  stepsWf : TypeReduceWf env b b'
   ntrl : Neutral b'
   prf : eq.NtrlEq env (Element red.a' red.ntrl) (Element b' ntrl) Set
 
@@ -117,9 +127,7 @@ record NeutralTmRed
   where
   constructor MkNtrlTmRed
   {0 t' : Term n}
-  tmWf : TermWf env t a
-  steps : TermReduce env t t' a
-  tmWf' : TermWf env t' a
+  stepsWf : TermReduceWf env t t' a
   ntrl : Neutral t'
   prf : eq.NtrlEq env (Element t' ntrl) (Element t' ntrl) a
 
@@ -134,12 +142,8 @@ record NeutralTmEq
   where
   constructor MkNtrlTmEq
   {0 t', u' : Term n}
-  tmWf1 : TermWf env t a
-  tmWf2 : TermWf env u a
-  steps1 : TermReduce env t t' a
-  steps2 : TermReduce env u u' a
-  tmWf1' : TermWf env t' a
-  tmWf2' : TermWf env u' a
+  stepsWf1 : TermReduceWf env t t' a
+  stepsWf2 : TermReduceWf env u u' a
   ntrl1 : Neutral t'
   ntrl2 : Neutral u'
   prf : eq.NtrlEq env (Element t' ntrl1) (Element u' ntrl2) a
@@ -155,9 +159,7 @@ record SetTyRed
   (a : Term n)
   where
   constructor MkSetTyRed
-  tyWf : TypeWf env a
-  steps : TypeReduce env a Set
-  tyWf' : TypeWf env Set
+  stepsWf : TypeReduceWf env a Set
   prf : Small `LT` l
 
 public export
@@ -170,9 +172,7 @@ record SetTyEq
   (red : SetTyRed eq l rec {n} env a)
   where
   constructor MkSetTyEq
-  tyWf : TypeWf env b
-  steps : TypeReduce env b Set
-  tyWf' : TypeWf env Set
+  stepsWf : TypeReduceWf env b Set
 
 public export
 record SetTmRed
@@ -185,9 +185,7 @@ record SetTmRed
   where
   constructor MkSetTmRed
   {0 t' : Term n}
-  tmWf : TermWf env t a
-  steps : TermReduce env t t' a
-  tmWf' : TermWf env t' a
+  stepsWf : TermReduceWf env t t' a
   whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   tyRed : (rec Small red.prf).TypeRed env t
@@ -203,12 +201,8 @@ record SetTmEq
   where
   constructor MkSetTmEq
   {0 t', u' : Term n}
-  tmWf1 : TermWf env t a
-  tmWf2 : TermWf env u a
-  steps1 : TermReduce env t t' a
-  steps2 : TermReduce env u u' a
-  tmWf1' : TermWf env t' a
-  tmWf2' : TermWf env u' a
+  stepsWf1 : TermReduceWf env t t' a
+  stepsWf2 : TermReduceWf env u u' a
   whnf1 : Whnf t'
   whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
@@ -229,9 +223,7 @@ record PiTyRed
   constructor MkPiTyRed
   {0 f : Term n}
   {0 g : Term (S n)}
-  tyWf : TypeWf env a
-  steps : TypeReduce env a (Pi f g)
-  tyWf' : TypeWf env (Pi f g)
+  stepsWf : TypeReduceWf env a (Pi f g)
   prf : eq.TypeEq env (Pi f g) (Pi f g)
   domRed :
     forall m.
@@ -273,9 +265,7 @@ record PiTyEq
   constructor MkPiTyEq
   {0 f : Term n}
   {0 g : Term (S n)}
-  tyWf : TypeWf env b
-  steps : TypeReduce env b (Pi f g)
-  tyWf' : TypeWf env (Pi f g)
+  stepsWf : TypeReduceWf env b (Pi f g)
   prf : eq.TypeEq env (Pi red.f red.g) (Pi f g)
   domEq :
     forall m.
@@ -306,9 +296,7 @@ record PiTmRed
   where
   constructor MkPiTmRed
   {0 t' : Term n}
-  tmWf : TermWf env t a
-  steps : TermReduce env t t' a
-  tmWf' : TermWf env t' a
+  stepsWf : TermReduceWf env t t' a
   whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   codRed :
@@ -348,12 +336,8 @@ record PiTmEq
   where
   constructor MkPiTmEq
   {0 t', u' : Term n}
-  tmWf1 : TermWf env t a
-  tmWf2 : TermWf env u a
-  steps1 : TermReduce env t t' a
-  steps2 : TermReduce env u u' a
-  tmWf1' : TermWf env t' a
-  tmWf2' : TermWf env u' a
+  stepsWf1 : TermReduceWf env t t' a
+  stepsWf2 : TermReduceWf env u u' a
   whnf1 : Whnf t'
   whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
@@ -427,24 +411,18 @@ typeEqRefl :
   (LogRel eq l).TypeEq env a a red
 typeEqRefl l (RedNtrlTy red) =
   EqNtrlTy $ MkNtrlTyEq
-    { tyWf = red.tyWf
-    , steps = red.steps
-    , tyWf' = red.tyWf'
+    { stepsWf = red.stepsWf
     , ntrl = red.ntrl
     , prf = red.prf
     }
 typeEqRefl l (RedSetTy red) =
   EqSetTy $ MkSetTyEq
-    { tyWf = red.tyWf
-    , steps = red.steps
-    , tyWf' = red.tyWf'
+    { stepsWf = red.stepsWf
     }
-typeEqRefl l (RedPiTy (MkPiTyRed tyWf steps tyWf' prf domRed codRed codEq)) =
+typeEqRefl l (RedPiTy red@(MkPiTyRed _ _ domRed codRed _)) =
   EqPiTy $ MkPiTyEq
-    { tyWf = tyWf
-    , steps = steps
-    , tyWf' = tyWf'
-    , prf = prf
+    { stepsWf = red.stepsWf
+    , prf = red.prf
     , domEq = \thinWf => typeEqRefl l (domRed thinWf)
     , codEq = \thinWf, red' => typeEqRefl l (codRed thinWf red')
     }
@@ -457,24 +435,16 @@ termEqRefl :
   (LogRel eq l).TermEq env t t a red
 termEqRefl l (RedNtrlTy red) (RedNtrlTm redTm) =
   EqNtrlTm $ MkNtrlTmEq
-    { tmWf1 = redTm.tmWf
-    , tmWf2 = redTm.tmWf
-    , steps1 = redTm.steps
-    , steps2 = redTm.steps
-    , tmWf1' = redTm.tmWf'
-    , tmWf2' = redTm.tmWf'
+    { stepsWf1 = redTm.stepsWf
+    , stepsWf2 = redTm.stepsWf
     , ntrl1 = redTm.ntrl
     , ntrl2 = redTm.ntrl
     , prf = redTm.prf
     }
-termEqRefl Large (RedSetTy (MkSetTyRed tyWf steps tyWf' LTSmall)) (RedSetTm redTm) =
+termEqRefl Large (RedSetTy (MkSetTyRed stepsWf LTSmall)) (RedSetTm redTm) =
   EqSetTm $ MkSetTmEq
-    { tmWf1 = redTm.tmWf
-    , tmWf2 = redTm.tmWf
-    , steps1 = redTm.steps
-    , steps2 = redTm.steps
-    , tmWf1' = redTm.tmWf'
-    , tmWf2' = redTm.tmWf'
+    { stepsWf1 = redTm.stepsWf
+    , stepsWf2 = redTm.stepsWf
     , whnf1 = redTm.whnf
     , whnf2 = redTm.whnf
     , prf = redTm.prf
@@ -482,14 +452,10 @@ termEqRefl Large (RedSetTy (MkSetTyRed tyWf steps tyWf' LTSmall)) (RedSetTm redT
     , tyRed2 = redTm.tyRed
     , tyEq = typeEqRefl {eq} Small redTm.tyRed
     }
-termEqRefl l (RedPiTy red@(MkPiTyRed _ _ _ _ domRed _ _)) (RedPiTm redTm) =
+termEqRefl l (RedPiTy red@(MkPiTyRed _ _ domRed _ _)) (RedPiTm redTm) =
   EqPiTm $ MkPiTmEq
-    { tmWf1 = redTm.tmWf
-    , tmWf2 = redTm.tmWf
-    , steps1 = redTm.steps
-    , steps2 = redTm.steps
-    , tmWf1' = redTm.tmWf'
-    , tmWf2' = redTm.tmWf'
+    { stepsWf1 = redTm.stepsWf
+    , stepsWf2 = redTm.stepsWf
     , whnf1 = redTm.whnf
     , whnf2 = redTm.whnf
     , prf = redTm.prf
@@ -502,9 +468,9 @@ termEqRefl l (RedPiTy red@(MkPiTyRed _ _ _ _ domRed _ _)) (RedPiTm redTm) =
 
 export
 escapeTypeRed : (l : Level) -> (red : (LogRel eq l).TypeRed env a) -> TypeWf env a
-escapeTypeRed l (RedNtrlTy red) = red.tyWf
-escapeTypeRed l (RedSetTy red) = red.tyWf
-escapeTypeRed l (RedPiTy red) = red.tyWf
+escapeTypeRed l (RedNtrlTy red) = red.stepsWf.tyWf
+escapeTypeRed l (RedSetTy red) = red.stepsWf.tyWf
+escapeTypeRed l (RedPiTy red) = red.stepsWf.tyWf
 
 export
 escapeTypeEq :
@@ -514,11 +480,20 @@ escapeTypeEq :
   (LogRel eq l).TypeEq env a b red ->
   eq.TypeEq env a b
 escapeTypeEq l (RedNtrlTy red) (EqNtrlTy tyEq) =
-  expandType red.steps tyEq.steps (Ntrl red.ntrl) (Ntrl tyEq.ntrl) (ntrlEqImpliesTypeEq tyEq.prf)
+  expandType
+    red.stepsWf.steps tyEq.stepsWf.steps
+    (Ntrl red.ntrl) (Ntrl tyEq.ntrl)
+    (ntrlEqImpliesTypeEq tyEq.prf)
 escapeTypeEq l (RedSetTy red) (EqSetTy tyEq) =
-  expandType red.steps tyEq.steps Set Set (typeSet $ typeWfImpliesEnvWf red.tyWf')
+  expandType
+    red.stepsWf.steps tyEq.stepsWf.steps
+    Set Set
+    (typeSet $ typeWfImpliesEnvWf red.stepsWf.tyWf')
 escapeTypeEq l (RedPiTy red) (EqPiTy tyEq) =
-  expandType red.steps tyEq.steps Pi Pi tyEq.prf
+  expandType
+    red.stepsWf.steps tyEq.stepsWf.steps
+    Pi Pi
+    tyEq.prf
 
 export
 escapeTermRed :
@@ -526,9 +501,9 @@ escapeTermRed :
   (red : (LogRel eq l).TypeRed env a) ->
   (LogRel eq l).TermRed env t a red ->
   TermWf env t a
-escapeTermRed l (RedNtrlTy red) (RedNtrlTm tmRed) = tmRed.tmWf
-escapeTermRed l (RedSetTy red) (RedSetTm tmRed) = tmRed.tmWf
-escapeTermRed l (RedPiTy red) (RedPiTm tmRed) = tmRed.tmWf
+escapeTermRed l (RedNtrlTy red) (RedNtrlTm tmRed) = tmRed.stepsWf.tmWf
+escapeTermRed l (RedSetTy red) (RedSetTm tmRed) = tmRed.stepsWf.tmWf
+escapeTermRed l (RedPiTy red) (RedPiTm tmRed) = tmRed.stepsWf.tmWf
 
 export
 escapeTermEq :
@@ -538,8 +513,17 @@ escapeTermEq :
   (LogRel eq l).TermEq env t u a red ->
   eq.TermEq env t u a
 escapeTermEq l (RedNtrlTy red) (EqNtrlTm tmEq) =
-  expandTerm tmEq.steps1 tmEq.steps2 (Ntrl tmEq.ntrl1) (Ntrl tmEq.ntrl2) (ntrlEqImpliesTermEq tmEq.prf)
+  expandTerm
+    tmEq.stepsWf1.steps tmEq.stepsWf2.steps
+    (Ntrl tmEq.ntrl1) (Ntrl tmEq.ntrl2)
+    (ntrlEqImpliesTermEq tmEq.prf)
 escapeTermEq l (RedSetTy red) (EqSetTm tmEq) =
-  expandTerm tmEq.steps1 tmEq.steps2 tmEq.whnf1 tmEq.whnf2 tmEq.prf
+  expandTerm
+    tmEq.stepsWf1.steps tmEq.stepsWf2.steps
+    tmEq.whnf1 tmEq.whnf2
+    tmEq.prf
 escapeTermEq l (RedPiTy red) (EqPiTm tmEq) =
-  expandTerm tmEq.steps1 tmEq.steps2 tmEq.whnf1 tmEq.whnf2 tmEq.prf
+  expandTerm
+    tmEq.stepsWf1.steps tmEq.stepsWf2.steps
+    tmEq.whnf1 tmEq.whnf2
+    tmEq.prf
diff --git a/src/Core/LogRel/View.idr b/src/Core/LogRel/View.idr
index 1790c9f..64e6c97 100644
--- a/src/Core/LogRel/View.idr
+++ b/src/Core/LogRel/View.idr
@@ -36,7 +36,7 @@ view (RedNtrlTy red1) (RedNtrlTy red2) (EqNtrlTy tyEq) = Ntrl red1 red2
 view (RedNtrlTy red1) (RedSetTy red2) (EqNtrlTy tyEq) =
   let
     det : (Set = tyEq.b')
-    det = typeRedDeterministic red2.steps tyEq.steps Set (Ntrl tyEq.ntrl)
+    det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Set (Ntrl tyEq.ntrl)
 
     ntrl : Neutral (Set {n})
     ntrl = rewrite det in tyEq.ntrl
@@ -45,7 +45,7 @@ view (RedNtrlTy red1) (RedSetTy red2) (EqNtrlTy tyEq) =
 view (RedNtrlTy red1) (RedPiTy red2) (EqNtrlTy tyEq) =
   let
     det : (Pi red2.f red2.g = tyEq.b')
-    det = typeRedDeterministic red2.steps tyEq.steps Pi (Ntrl tyEq.ntrl)
+    det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Pi (Ntrl tyEq.ntrl)
 
     ntrl : Neutral (Pi red2.f red2.g)
     ntrl = rewrite det in tyEq.ntrl
@@ -54,7 +54,7 @@ view (RedNtrlTy red1) (RedPiTy red2) (EqNtrlTy tyEq) =
 view (RedSetTy red1) (RedNtrlTy red2) (EqSetTy tyEq) =
   let
     det : (red2.a' = Set)
-    det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Set
+    det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps (Ntrl red2.ntrl) Set
 
     ntrl : Neutral (Set {n})
     ntrl = rewrite sym det in red2.ntrl
@@ -64,13 +64,13 @@ view (RedSetTy red1) (RedSetTy red2) (EqSetTy tyEq) = Set red1 red2
 view (RedSetTy red1) (RedPiTy red2) (EqSetTy tyEq) =
   let
     det : (Pi red2.f red2.g = Set)
-    det = typeRedDeterministic red2.steps tyEq.steps Pi Set
+    det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Pi Set
   in
   absurd det
 view (RedPiTy red1) (RedNtrlTy red2) (EqPiTy tyEq) =
   let
     det : (red2.a' = Pi tyEq.f tyEq.g)
-    det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Pi
+    det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps (Ntrl red2.ntrl) Pi
 
     ntrl : Neutral (Pi tyEq.f tyEq.g)
     ntrl = rewrite sym det in red2.ntrl
@@ -79,7 +79,7 @@ view (RedPiTy red1) (RedNtrlTy red2) (EqPiTy tyEq) =
 view (RedPiTy red1) (RedSetTy red2) (EqPiTy tyEq) =
   let
     det : (Set = Pi tyEq.f tyEq.g)
-    det = typeRedDeterministic red2.steps tyEq.steps Set Pi
+    det = typeRedDeterministic red2.stepsWf.steps tyEq.stepsWf.steps Set Pi
   in
   absurd det
 view (RedPiTy red1) (RedPiTy red2) (EqPiTy tyEq) = Pi red1 red2