module Cubical.Reflection.StrictEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv.Base
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.List.Base
open import Cubical.Data.Unit.Base

import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

strictEquivClauses : R.Term → R.Term → List R.Clause
strictEquivClauses f g =
  R.clause []
    (R.proj (quote fst) v∷ [])
    f
  ∷ R.clause []
    (R.proj (quote snd) v∷ R.proj (quote equiv-proof) v∷ [])
    (R.def (quote strictContrFibers) (g v∷ []))
  ∷ []

strictEquivTerm : R.Term → R.Term → R.Term
strictEquivTerm f g = R.pat-lam (strictEquivClauses f g) []

strictEquivMacro : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → (A → B) → (B → A) → R.Term → R.TC Unit
strictEquivMacro {A = A} {B} f g hole =
  R.quoteTC (A ≃ B) >>= λ equivTy →
  R.checkType hole equivTy >>
  R.quoteTC f >>= λ `f` →
  R.quoteTC g >>= λ `g` →
  R.unify (strictEquivTerm `f` `g`) hole

strictIsoToEquivMacro : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → Iso A B → R.Term → R.TC Unit
strictIsoToEquivMacro isom =
  strictEquivMacro (Iso.fun isom) (Iso.inv isom)

-- For use with unquoteDef

defStrictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → (A → B) → (B → A) → R.TC Unit
defStrictEquiv idName f g =
  R.quoteTC f >>= λ `f` →
  R.quoteTC g >>= λ `g` →
  R.defineFun idName (strictEquivClauses `f` `g`)

defStrictIsoToEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → Iso A B → R.TC Unit
defStrictIsoToEquiv idName isom =
  defStrictEquiv idName (Iso.fun isom) (Iso.inv isom)

-- For use with unquoteDef

declStrictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → (A → B) → (B → A) → R.TC Unit
declStrictEquiv {A = A} {B = B} idName f g =
  R.quoteTC (A ≃ B) >>= λ ty →
  R.declareDef (varg idName) ty >>
  defStrictEquiv idName f g

declStrictIsoToEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → Iso A B → R.TC Unit
declStrictIsoToEquiv idName isom =
  declStrictEquiv idName (Iso.fun isom) (Iso.inv isom)

macro
  -- (f : A → B) → (g : B → A) → (A ≃ B)
  -- Assumes that `f` and `g` are inverse up to definitional equality
  strictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
    → (A → B) → (B → A) → R.Term → R.TC Unit
  strictEquiv = strictEquivMacro

  -- (isom : Iso A B) → (A ≃ B)
  -- Assumes that the functions defining `isom` are inverse up to definitional equality
  strictIsoToEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
    → Iso A B → R.Term → R.TC Unit
  strictIsoToEquiv = strictIsoToEquivMacro