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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.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.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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.steps Set Pi
  in
  absurd det
view (RedPiTy red1) (RedPiTy red2) (EqPiTy tyEq) = Pi red1 red2

public export
viewRefl :
  (red1 : (LogRel eq l1).TypeRed env a) ->
  (red2 : (LogRel eq l2).TypeRed env a) ->
  ShapeView red1 red2
viewRefl red1 red2 = view red1 red2 (typeEqRefl _ red1)