Prove escape theorems.

1 files changed, 60 insertions, 14 deletions

diff --git a/src/Core/LogRel.idr b/src/Core/LogRel.idr
index 9c18f02..19a7071 100644
--- a/src/Core/LogRel.idr
+++ b/src/Core/LogRel.idr
@@ -86,7 +86,7 @@ record NeutralTyRed
   tyWf : TypeWf env a
   steps : TypeReduce env a a'
   tyWf' : TypeWf env a'
-  0 ntrl : Neutral a'
+  ntrl : Neutral a'
   prf : eq.NtrlEq env (Element a' ntrl) (Element a' ntrl) Set
 
 public export
@@ -103,7 +103,7 @@ record NeutralTyEq
   tyWf : TypeWf env b
   steps : TypeReduce env b b'
   tyWf' : TypeWf env b'
-  0 ntrl : Neutral b'
+  ntrl : Neutral b'
   prf : eq.NtrlEq env (Element red.a' red.ntrl) (Element b' ntrl) Set
 
 public export
@@ -120,7 +120,7 @@ record NeutralTmRed
   tmWf : TermWf env t a
   steps : TermReduce env t t' a
   tmWf' : TermWf env t' a
-  0 ntrl : Neutral t'
+  ntrl : Neutral t'
   prf : eq.NtrlEq env (Element t' ntrl) (Element t' ntrl) a
 
 public export
@@ -140,8 +140,8 @@ record NeutralTmEq
   steps2 : TermReduce env u u' a
   tmWf1' : TermWf env t' a
   tmWf2' : TermWf env u' a
-  0 ntrl1 : Neutral t'
-  0 ntrl2 : Neutral u'
+  ntrl1 : Neutral t'
+  ntrl2 : Neutral u'
   prf : eq.NtrlEq env (Element t' ntrl1) (Element u' ntrl2) a
 
 -- Set
@@ -186,9 +186,9 @@ record SetTmRed
   constructor MkSetTmRed
   {0 t' : Term n}
   tmWf : TermWf env t a
-  steps : TypeReduce env t t'
+  steps : TermReduce env t t' a
   tmWf' : TermWf env t' a
-  0 whnf : Whnf t'
+  whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   tyRed : (rec Small red.prf).TypeRed env t
 
@@ -205,12 +205,12 @@ record SetTmEq
   {0 t', u' : Term n}
   tmWf1 : TermWf env t a
   tmWf2 : TermWf env u a
-  steps1 : TypeReduce env t t'
-  steps2 : TypeReduce env u u'
+  steps1 : TermReduce env t t' a
+  steps2 : TermReduce env u u' a
   tmWf1' : TermWf env t' a
   tmWf2' : TermWf env u' a
-  0 whnf1 : Whnf t'
-  0 whnf2 : Whnf u'
+  whnf1 : Whnf t'
+  whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
   tyRed1 : (rec Small red.prf).TypeRed env t
   tyRed2 : (rec Small red.prf).TypeRed env u
@@ -309,7 +309,7 @@ record PiTmRed
   tmWf : TermWf env t a
   steps : TermReduce env t t' a
   tmWf' : TermWf env t' a
-  0 whnf : Whnf t'
+  whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   codRed :
     forall m.
@@ -354,8 +354,8 @@ record PiTmEq
   steps2 : TermReduce env u u' a
   tmWf1' : TermWf env t' a
   tmWf2' : TermWf env u' a
-  0 whnf1 : Whnf t'
-  0 whnf2 : Whnf u'
+  whnf1 : Whnf t'
+  whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
   red1 : PiTmRed eq l rec env t a red
   red2 : PiTmRed eq l rec env u a red
@@ -498,3 +498,49 @@ termEqRefl l (RedPiTy red@(MkPiTyRed _ _ _ _ domRed _ _)) (RedPiTm redTm) =
     , red2 = redTm
     , codEq = \thinWf, red' => redTm.codEq thinWf red' red' (termEqRefl l (domRed thinWf) red')
     }
+
+-- Escape ----------------------------------------------------------------------
+
+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
+
+export
+escapeTypeEq :
+  IsEq eq =>
+  (l : Level) ->
+  (red : (LogRel eq l).TypeRed env a) ->
+  (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)
+escapeTypeEq l (RedSetTy red) (EqSetTy tyEq) =
+  expandType red.steps tyEq.steps Set Set (typeSet $ typeWfImpliesEnvWf red.tyWf')
+escapeTypeEq l (RedPiTy red) (EqPiTy tyEq) =
+  expandType red.steps tyEq.steps Pi Pi tyEq.prf
+
+export
+escapeTermRed :
+  (l : Level) ->
+  (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
+
+export
+escapeTermEq :
+  IsEq eq =>
+  (l : Level) ->
+  (red : (LogRel eq l).TypeRed env a) ->
+  (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)
+escapeTermEq l (RedSetTy red) (EqSetTm tmEq) =
+  expandTerm tmEq.steps1 tmEq.steps2 tmEq.whnf1 tmEq.whnf2 tmEq.prf
+escapeTermEq l (RedPiTy red) (EqPiTm tmEq) =
+  expandTerm tmEq.steps1 tmEq.steps2 tmEq.whnf1 tmEq.whnf2 tmEq.prf