Define shape views.

3 files changed, 101 insertions, 0 deletions

diff --git a/src/Core/LogRel/View.idr b/src/Core/LogRel/View.idr
new file mode 100644
index 0000000..ecb6cc2
--- /dev/null
+++ b/src/Core/LogRel/View.idr
@@ -0,0 +1,85 @@
+module Core.LogRel.View
+
+import Core.Environment
+import Core.Generic
+import Core.LogRel
+import Core.Reduction
+import Core.Term
+import Core.Term.NormalForm
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data ShapeView : (LogRel eq l1).TypeRed env a -> (LogRel eq l2).TypeRed env b -> Type where
+  Ntrl :
+    (red1 : NeutralTyRed eq l1 (LogRelRec eq l1) env a) ->
+    (red2 : NeutralTyRed eq l2 (LogRelRec eq l2) env b) ->
+    ShapeView (RedNtrlTy red1) (RedNtrlTy red2)
+  Set :
+    (red1 : SetTyRed eq l1 (LogRelRec eq l1) env a) ->
+    (red2 : SetTyRed eq l2 (LogRelRec eq l2) env b) ->
+    ShapeView (RedSetTy red1) (RedSetTy red2)
+  Pi :
+    (red1 : PiTyRed eq l1 (LogRelRec eq l1) env a) ->
+    (red2 : PiTyRed eq l2 (LogRelRec eq l2) env b) ->
+    ShapeView (RedPiTy red1) (RedPiTy red2)
+
+-- Construction ----------------------------------------------------------------
+
+export
+view :
+  (red1 : (LogRel eq l1).TypeRed {n} env a) ->
+  (red2 : (LogRel eq l2).TypeRed env b) ->
+  (LogRel eq l1).TypeEq env a b red1 ->
+  ShapeView red1 red2
+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)
+
+    ntrl : Neutral (Set {n})
+    ntrl = rewrite det in tyEq.ntrl
+  in
+  absurd ntrl
+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)
+
+    ntrl : Neutral (Pi red2.f red2.g)
+    ntrl = rewrite det in tyEq.ntrl
+  in
+  absurd ntrl
+view (RedSetTy red1) (RedNtrlTy red2) (EqSetTy tyEq) =
+  let
+    det : (red2.a' = Set)
+    det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Set
+
+    ntrl : Neutral (Set {n})
+    ntrl = rewrite sym det in red2.ntrl
+  in
+  absurd ntrl
+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
+  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
+
+    ntrl : Neutral (Pi tyEq.f tyEq.g)
+    ntrl = rewrite sym det in red2.ntrl
+  in
+  absurd ntrl
+view (RedPiTy red1) (RedSetTy red2) (EqPiTy tyEq) =
+  let
+    det : (Set = Pi tyEq.f tyEq.g)
+    det = typeRedDeterministic red2.steps tyEq.steps Set Pi
+  in
+  absurd det
+view (RedPiTy red1) (RedPiTy red2) (EqPiTy tyEq) = Pi red1 red2
diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index a3ddac5..8c05e03 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -20,6 +20,14 @@ data Term : Nat -> Type where
 
 %name Term t, u, v
 
+-- Impossibilities -------------------------------------------------------------
+
+export
+Uninhabited (Set = Pi f g) where uninhabited prf impossible
+
+export
+Uninhabited (Pi f g = Set) where uninhabited prf impossible
+
 -- Weakening -------------------------------------------------------------------
 
 public export
diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr
index 2cd16a1..fc7ed6e 100644
--- a/src/Core/Term/NormalForm.idr
+++ b/src/Core/Term/NormalForm.idr
@@ -28,6 +28,14 @@ public export
 NeutralTerm : Nat -> Type
 NeutralTerm n = Subset (Term n) Neutral
 
+-- Impossibilities -------------------------------------------------------------
+
+export
+Uninhabited (Neutral Set) where uninhabited n impossible
+
+export
+Uninhabited (Neutral $ Pi f g) where uninhabited n impossible
+
 -- Inversion -------------------------------------------------------------------
 
 invertNtrlApp : Neutral (App t u) -> Neutral t