open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Vec.Base

open import Realisability.PCA

import Realisability.Data.Pair
import Realisability.PCA.Sugar
import Realisability.Data.Sum
module Realisability.Base {β„“A} (pca@(𝔸 , _) : PCA β„“A) where
open Realisability.PCA.Sugar pca
open Realisability.Data.Pair pca
open Realisability.Data.Sum pca

private variable
  β„“ β„“' β„“'' : Level
  X Y Z : Type β„“'
  n : Nat

Realisability logicπŸ”—

record [_]_⊒_ (f : X β†’ Y) (P : X β†’ ℙ⁺ 𝔸) (Q : Y β†’ ℙ⁺ 𝔸) : Type (level-of X βŠ” level-of Y βŠ” β„“A) where
  field
    realiser : ↯⁺ 𝔸
    tracks   : βˆ€ x (a : β†― ⌞ 𝔸 ⌟) (ah : a ∈ P x) β†’ realiser ⋆ a ∈ Q (f x)

  realiser↓ : βˆ€ {x} (a : β†― ⌞ 𝔸 ⌟) (ah : a ∈ P x) β†’ ⌞ realiser ⋆ a ⌟
  realiser↓ a ah = Q _ .defined (tracks _ a ah)
private unquoteDecl eqv' = declare-record-iso eqv' (quote [_]_⊒_)

open [_]_⊒_ hiding (tracks) public

-- Evil hack to change the visibility of the arguments to tracks in
-- RHSes: instead of using the projection from that record we define a
-- new record with the first two arguments made implicit (with the same
-- name), convert the actual record to this new one, and export a copy
-- of the new projection; since this is all done in a module
-- parametrised by a [ f ] P ⊒ Q, the new definition is basically a
-- projection.
--
-- Since copies of postfix identifiers can be used postfix this works.

module _ {f : X β†’ Y} {P : X β†’ ℙ⁺ 𝔸} {Q : Y β†’ ℙ⁺ 𝔸} (i : [ f ] P ⊒ Q) where
  private
    module i = [_]_⊒_ i
    record hack : Type (level-of X βŠ” level-of Y βŠ” β„“A) where
      field
        tracks   : βˆ€ {x} {a : β†― ⌞ 𝔸 ⌟} (ah : a ∈ P x) β†’ i.realiser ⋆ a ∈ Q (f x)

    from : hack
    from = record { tracks = i.tracks _ _ }

  open hack from public

instance
  tracks-to-term : βˆ€ {V : Type} {P : X β†’ ℙ⁺ 𝔸} {Q : Y β†’ ℙ⁺ 𝔸} {f : X β†’ Y} β†’ To-term V ([ f ] P ⊒ Q)
  tracks-to-term = record { to = Ξ» x β†’ const (x .realiser) }

  tracks-to-part : βˆ€ {P : X β†’ ℙ⁺ 𝔸} {Q : Y β†’ ℙ⁺ 𝔸} {f : X β†’ Y} β†’ To-part ([ f ] P ⊒ Q) ⌞ 𝔸 ⌟
  tracks-to-part = record { to-part = Ξ» x β†’ x .realiser .fst }

private
  variable P Q R : X β†’ ℙ⁺ 𝔸

  subst-∈ : (P : ℙ⁺ 𝔸) {x y : β†― ⌞ 𝔸 ⌟} β†’ x ∈ P β†’ y ≑ x β†’ y ∈ P
  subst-∈ P hx p = subst (_∈ P) (sym p) hx

Basic structural rulesπŸ”—

id⊒ : [ id ] P ⊒ P
id⊒ {P = P} = record where
  realiser = val ⟨ x ⟩ x

  tracks x a ha = subst-∈ (P x) ha (abs-β _ [] (a , P x .defined ha))

_∘⊒_ : βˆ€ {f g} β†’ [ g ] Q ⊒ R β†’ [ f ] P ⊒ Q β†’ [ g ∘ f ] P ⊒ R
_∘⊒_ {R = R} {P = P} α β = record where
  realiser = val ⟨ x ⟩ α `· (β `· x)

  tracks x a ha = subst-∈ (R _) (α .tracks (β .tracks ha)) $
    (val ⟨ x ⟩ Ξ± `Β· (Ξ² `Β· x)) ⋆ a β‰‘βŸ¨ abs-Ξ² _ [] (a , P _ .defined ha) ⟩
    Ξ± ⋆ (Ξ² ⋆ a)                   ∎

ConjunctionπŸ”—

_∧T_ : (P Q : X β†’ ℙ⁺ 𝔸) β†’ X β†’ ℙ⁺ 𝔸
(P ∧T Q) x .mem a = elΩ do
  Ξ£[ u ∈ β†― ⌞ 𝔸 ⌟ ] Ξ£[ v ∈ β†― ⌞ 𝔸 ⌟ ]
    a ≑ `pair ⋆ u ⋆ v Γ— u ∈ P x Γ— v ∈ Q x
(P ∧T Q) x .defined = rec! Ξ» u v Ξ± rx ry β†’
  subst ⌞_⌟ (sym Ξ±) (`pair↓₂ (P _ .defined rx) (Q _ .defined ry))

Ο€β‚βŠ’ : [ id ] (P ∧T Q) ⊒ P
Ο€β‚βŠ’ {P = P} {Q = Q} = record where
  realiser = `fst

  tracks x = elim! Ξ» a p q Ξ± pp qq β†’ subst-∈ (P _) pp $
    `fst ⋆ a               β‰‘βŸ¨ ap (`fst ⋆_) Ξ± ⟩
    `fst ⋆ (`pair ⋆ p ⋆ q) β‰‘βŸ¨ `fst-Ξ² (P _ .defined pp) (Q _ .defined qq) ⟩
    p                      ∎

Ο€β‚‚βŠ’ : [ id ] (P ∧T Q) ⊒ Q
Ο€β‚‚βŠ’ {P = P} {Q = Q} = record where
  realiser = `snd

  tracks x = elim! Ξ» a p q Ξ± pp qq β†’ subst-∈ (Q _) qq $
    `snd ⋆ a               β‰‘βŸ¨ ap (`snd ⋆_) Ξ± ⟩
    `snd ⋆ (`pair ⋆ p ⋆ q) β‰‘βŸ¨ `snd-Ξ² (P _ .defined pp) (Q _ .defined qq) ⟩
    q                      ∎