-- Algorithmic equality.

{-# OPTIONS --without-K --safe #-}

module Definition.Conversion where

open import Definition.Untyped
open import Definition.Typed

open import Tools.Nat
import Tools.PropositionalEquality as PE


infix 10 _⊢_~_↑_
infix 10 _⊢_~_↓_
infix 10 _⊢_[conv↑]_
infix 10 _⊢_[conv↓]_
infix 10 _⊢_[conv↑]_∷_
infix 10 _⊢_[conv↓]_∷_

mutual
  -- Neutral equality.
  data _⊢_~_↑_ (Γ : Con Term) : (k l A : Term)  Set where
    var       :  {x y A}
               Γ  var x  A
               x PE.≡ y
               Γ  var x ~ var y  A
    app       :  {k l t v F G}
               Γ  k ~ l  Π F  G
               Γ  t [conv↑] v  F
               Γ  k  t ~ l  v  G [ t ]
    natrec    :  {k l h g a₀ b₀ F G}
               Γ    F [conv↑] G
               Γ  a₀ [conv↑] b₀  F [ zero ]
               Γ  h [conv↑] g  Π   (F ▹▹ F [ suc (var zero) ]↑)
               Γ  k ~ l  
               Γ  natrec F a₀ h k ~ natrec G b₀ g l  F [ k ]

  -- Neutral equality with types in WHNF.
  record _⊢_~_↓_ (Γ : Con Term) (k l B : Term) : Set where
    inductive
    constructor [~]
    field
      A     : Term
      D     : Γ  A ⇒* B
      whnfB : Whnf B
      k~l   : Γ  k ~ l  A

  -- Type equality.
  record _⊢_[conv↑]_ (Γ : Con Term) (A B : Term) : Set where
    inductive
    constructor [↑]
    field
      A′ B′  : Term
      D      : Γ  A ⇒* A′
      D′     : Γ  B ⇒* B′
      whnfA′ : Whnf A′
      whnfB′ : Whnf B′
      A′<>B′ : Γ  A′ [conv↓] B′

  -- Type equality with types in WHNF.
  data _⊢_[conv↓]_ (Γ : Con Term) : (A B : Term)  Set where
    U-refl    :  Γ  Γ  U [conv↓] U
    ℕ-refl    :  Γ  Γ   [conv↓] 
    ne        :  {K L}
               Γ  K ~ L  U
               Γ  K [conv↓] L
    Π-cong    :  {F G H E}
               Γ  F
               Γ  F [conv↑] H
               Γ  F  G [conv↑] E
               Γ  Π F  G [conv↓] Π H  E

  -- Term equality.
  record _⊢_[conv↑]_∷_ (Γ : Con Term) (t u A : Term) : Set where
    inductive
    constructor [↑]ₜ
    field
      B t′ u′ : Term
      D       : Γ  A ⇒* B
      d       : Γ  t ⇒* t′  B
      d′      : Γ  u ⇒* u′  B
      whnfB   : Whnf B
      whnft′  : Whnf t′
      whnfu′  : Whnf u′
      t<>u    : Γ  t′ [conv↓] u′  B

  -- Term equality with types and terms in WHNF.
  data _⊢_[conv↓]_∷_ (Γ : Con Term) : (t u A : Term)  Set where
    ℕ-ins     :  {k l}
               Γ  k ~ l  
               Γ  k [conv↓] l  
    ne-ins    :  {k l M N}
               Γ  k  N
               Γ  l  N
               Neutral N
               Γ  k ~ l  M
               Γ  k [conv↓] l  N
    univ      :  {A B}
               Γ  A  U
               Γ  B  U
               Γ  A [conv↓] B
               Γ  A [conv↓] B  U
    zero-refl :  Γ  Γ  zero [conv↓] zero  
    suc-cong  :  {m n}
               Γ  m [conv↑] n  
               Γ  suc m [conv↓] suc n  
    η-eq      :  {f g F G}
               Γ  F
               Γ  f  Π F  G
               Γ  g  Π F  G
               Whnf f
               Whnf g
               Γ  F  wk1 f  var zero [conv↑] wk1 g  var zero  G
               Γ  f [conv↓] g  Π F  G