{-# OPTIONS -vtc.display:60 #-}
open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Fin.Base hiding (_<_ ; _≀_)
open import Data.Vec.Base
module Realisability.PCA where

Partial combinatory algebrasπŸ”—

private variable
  β„“ : Level
  A : Type β„“
  n : Nat
data Term (A : Type β„“) (n : Nat) : Type (level-of A) where
  var   : Fin n β†’ Term A n
  const : ↯⁺ A β†’ Term A n
  app   : Term A n β†’ Term A n β†’ Term A n

module eval (_%_ : β†― A β†’ β†― A β†’ β†― A) where
  eval : Term A n β†’ Vec (↯⁺ A) n β†’ β†― A
  eval (var x)   ρ = lookup ρ x .fst
  eval (const x) ρ = x .fst
  eval (app f x) ρ = eval f ρ % eval x ρ

  inst : Term A (suc n) β†’ Term A n β†’ Term A n
  inst (var x) a with fin-view x
  ... | zero = a
  ... | suc i = var i
  inst (const a) _ = const a
  inst (app f x) a = app (inst f a) (inst x a)

  abstract
    eval-inst
      : (t : Term A (suc n)) (x : ↯⁺ A) (ρ : Vec (↯⁺ A) n)
      β†’ eval (inst t (const x)) ρ ≑ eval t (x ∷ ρ)
    eval-inst (var i) y ρ with fin-view i
    ... | zero  = refl
    ... | suc j = refl
    eval-inst (const a) y ρ = refl
    eval-inst (app f x) y ρ = apβ‚‚ _%_ (eval-inst f y ρ) (eval-inst x y ρ)
record is-pca (_%_ : β†― A β†’ β†― A β†’ β†― A) : Type (level-of A) where
  open eval _%_ public
  field
    abs   : Term A (suc n) β†’ Term A n
    abs↓  : (t : Term A (suc n)) (ρ : Vec (↯⁺ A) n) β†’ ⌞ eval (abs t) ρ ⌟
    abs-Ξ² : (t : Term A (suc n)) (ρ : Vec (↯⁺ A) n) (a : ↯⁺ A)
          β†’ eval (abs t) ρ % a .fst ≑ eval (inst t (const a)) ρ

  absβ‚™ : (k : Nat) β†’ Term A (k + n) β†’ Term A n
  absβ‚™ zero    e = e
  absβ‚™ (suc k) e = absβ‚™ k (abs e)

  _%β‚™_ : βˆ€ {n} β†’ β†― A β†’ Vec (↯⁺ A) n β†’ β†― A
  a %β‚™ []       = a
  a %β‚™ (b ∷ bs) = (a %β‚™ bs) % b .fst

  abstract
    abs-Ξ²β‚™
      : {k n : Nat} {e : Term A (k + n)}
      β†’ (ρ : Vec (↯⁺ A) n) (as : Vec (↯⁺ A) k)
      β†’ (eval (absβ‚™ k e) ρ %β‚™ as) ≑ eval e (as ++ ρ)
    abs-Ξ²β‚™ ρ [] = refl
    abs-Ξ²β‚™ {e = e} ρ (x ∷ as) = ap (_% x .fst) (abs-Ξ²β‚™ ρ as) βˆ™ abs-Ξ² _ (as ++ ρ) x βˆ™ eval-inst e x (as ++ ρ)

record PCA-on (A : Type β„“) : Type β„“ where
  infixl 25 _%_

  field
    has-is-set : is-set A
    _%_        : β†― A β†’ β†― A β†’ β†― A
    has-is-pca : is-pca _%_

  open is-pca has-is-pca public

PCA : (β„“ : Level) β†’ Type (lsuc β„“)
PCA β„“ = Ξ£[ X ∈ Set β„“ ] PCA-on ∣ X ∣

module PCA {β„“} (A : PCA β„“) where
  open PCA-on (A .snd) public