{-# OPTIONS --type-in-type #-}

open import NeilPrelude hiding (result ; argument)
open import Extensionality
open import CPO
open import CPOFunctions
open import CPOLemmas

module ContinuityProps

  (_ : Extensionality)

  (fix : {τ : Type} → CPO (τ ⇒ τ) → CPO τ)

where

------------------------------------------------------------------------

app' : {σ τ : Type} → CPO ((σ ⇒ τ) ⊗ σ) → CPO τ
app' (f , x) = f $ x

------------------------------------------------------------------------

-- The continuity of application is well established.  See for example:
--   * H. P. Barendregt, H. P. "The Lambda Calculus: Its Syntax and Semantics", North Holland (1984).
--   * Glynn Winskel. "The Formal Semantics of Programming Languages: An Introduction", MIT (1993).
--
-- Their proof makes use of the property that a function on a product is continuous if it is continuous in each argument seperately.
--
-- postulate pointwise-continuity : {σ τ υ : Type} → (f : CPO (σ ⊗ τ) → CPO υ) → ((x : CPO σ) → Continuous (λ y → f (x , y)))
--                                                                             → ((y : CPO τ) → Continuous (λ x → f (x , y)))
--                                                                             → Continuous f
--
-- However, in this model I have been unable to prove either that implication or its antecedent.
-- Contributions welcome.

abstract

  postulate preservesLUB-app : {σ τ : Type} → PreservesLUB {(σ ⇒ τ) ⊗ σ} app'

  monotonic-app : {σ τ : Type} → Monotonic {(σ ⇒ τ) ⊗ σ} app'
  monotonic-app (⊑-prod p q) = ⊑-app p q

  continuous-app : {σ τ : Type} → Continuous {(σ ⇒ τ) ⊗ σ} app'
  continuous-app = monotonic-app , preservesLUB-app

-- app = λ (f , x) → f x
app : {σ τ : Type} → CPO (((σ ⇒ τ) ⊗ σ) ⇒ τ)
app = fun app' continuous-app

-- appTo x = λ h → h $ x
appTo : {σ τ : Type} → (x : CPO σ) → CPO ((σ ⇒ τ) ⇒ τ)
appTo x = app ∙ (identity :&: constant x)

------------------------------------------------------------------------

abstract

  monotonic-curry-underlying : {σ τ υ : Type} → (f : CPO ((σ ⊗ τ) ⇒ υ)) → (x : CPO σ) → Monotonic (λ y → f $ (x , y))
  monotonic-curry-underlying f x lt = monotonic f (⊑-prod ⊑-refl lt)

  preservesLUB-curry-underlying : {σ τ υ : Type} → (f : CPO ((σ ⊗ τ) ⇒ υ)) → (x : CPO σ) → PreservesLUB (λ y → f $ (x , y))
  preservesLUB-curry-underlying {σ} {τ} {υ} f x Y p z zUB = preservesLUB f (firstChain x Y) (firstIsNonEmptyChain x Y p) z preservesLUB-curry-aux
    where
      preservesLUB-curry-aux : (z' : CPO υ) → Σ (CPO (σ ⊗ τ)) (λ xy → (uncurry-prop (λ x' y → (x ≡ x') × y ∈ Y) xy) × f $ xy ≡ z') → z' ⊑ z
      preservesLUB-curry-aux ._ ((.x , y) , (refl , Py) , refl) = zUB (f $ (x , y)) (y , (Py , refl))

  continuous-curry-underlying : {σ τ υ : Type} → (f : CPO ((σ ⊗ τ) ⇒ υ)) → (x : CPO σ) → Continuous (λ y → f $ (x , y))
  continuous-curry-underlying f x = monotonic-curry-underlying f x , preservesLUB-curry-underlying f x

curry-⊗' : {σ τ υ : Type} → CPO ((σ ⊗ τ) ⇒ υ) → CPO σ → CPO (τ ⇒ υ)
curry-⊗' f x = fun (λ y → f $ (x , y)) (continuous-curry-underlying f x)

abstract

  monotonic-curry : {σ τ υ : Type} → (f : CPO ((σ ⊗ τ) ⇒ υ)) → Monotonic (curry-⊗' f)
  monotonic-curry f lt = ⊑-fun (monotonic f (⊑-prod lt ⊑-refl))

  preservesLUB-curry : {σ τ υ : Type} → (f : CPO ((σ ⊗ τ) ⇒ υ)) → PreservesLUB (curry-⊗' f)
  preservesLUB-curry {σ} {τ} {υ} f X p (fun g cg) gUB = ⊑-fun (λ {y} → preservesLUB f (secondChain y X) (secondIsNonEmptyChain y X p) (g y) (preservesLUB-curry-aux y))
    where
      preservesLUB-curry-aux : (y : CPO τ) → (z : CPO υ) → Σ (CPO (σ ⊗ τ)) (λ xy → uncurry-prop (λ x' y' → y ≡ y' × (x' ∈ X)) xy × (f $ xy ≡ z)) → z ⊑ g y
      preservesLUB-curry-aux y ._ ((x' , ._) , (refl , Px') , refl) with gUB (f ∙ (constant x' :&: identity)) (x' , (Px' , injective-$ refl))
      ... | ⊑-fun lt = lt

  continuous-curry : {σ τ υ : Type} → (f : CPO ((σ ⊗ τ) ⇒ υ)) → Continuous (curry-⊗' f)
  continuous-curry f = monotonic-curry f , preservesLUB-curry f

-- curry-⊗ f = λ x y → f (x , y)
curry-⊗ : {σ τ υ : Type} → CPO ((σ ⊗ τ) ⇒ υ) → CPO (σ ⇒ τ ⇒ υ)
curry-⊗ f = fun (curry-⊗' f) (continuous-curry f)

------------------------------------------------------------------------

subst-cont : {σ τ : Type} → {f g : CPO σ → CPO τ} → f ≡ g → Continuous f → Continuous g
subst-cont refl cf = cf

resultArg-def : {σ τ υ ν : Type} → (f : CPO (υ ⇒ ν)) → (g : CPO (σ ⇒ τ)) → CPO ((τ ⇒ υ) ⇒ (σ ⇒ ν))
resultArg-def f g = curry-⊗ (f ∙ app ∙ (identity :×: g))

abstract

  continuous-resultArg : {σ τ υ ν : Type} → (f : CPO (υ ⇒ ν)) → (g : CPO (σ ⇒ τ)) → Continuous (λ h → f ∙ h ∙ g)
  continuous-resultArg f g = subst-cont (ext' (injective-$ refl)) (continuous (resultArg-def f g))

  continuous-result : {σ τ υ : Type} → (f : CPO (τ ⇒ υ)) → Continuous {σ ⇒ τ} {σ ⇒ υ} (λ h → f ∙ h)
  continuous-result f = subst-cont (ext' (injective-$ refl)) (continuous-resultArg f identity)

  continuous-argument : {σ τ υ : Type} → (f : CPO (σ ⇒ τ)) → Continuous {τ ⇒ υ} (λ h → h ∙ f)
  continuous-argument f = subst-cont (ext' (injective-$ refl)) (continuous-resultArg identity f)

--------------------------------------------------------------------------------------------------------

-- resultArg f g = (λ h → f ∙ h ∙ g)
resultArg : {σ τ υ ν : Type} → (f : CPO (υ ⇒ ν)) → (g : CPO (σ ⇒ τ)) → CPO ((τ ⇒ υ) ⇒ (σ ⇒ ν))
resultArg f g = fun (λ h → f ∙ h ∙ g) (continuous-resultArg f g)

-- result f = λ h → f ∙ h
result : {σ τ υ : Type} → (f : CPO (τ ⇒ υ)) → CPO ((σ ⇒ τ) ⇒ (σ ⇒ υ))
result f = fun (λ h → f ∙ h) (continuous-result f)

-- argument f = λ h → h ∙ f
argument : {σ τ υ : Type} → (f : CPO (σ ⇒ τ)) → CPO ((τ ⇒ υ) ⇒ (σ ⇒ υ))
argument f = fun (λ h → h ∙ f) (continuous-argument f)

--------------------------------------------------------------------------------------------------------