{-# OPTIONS --safe  #-}

open import Level
open import Function.Base
open import Agda.Builtin.Equality

open import Data.Empty
open import Data.Product
open import Data.List
open import Data.Unit
import Data.Maybe.Relation.Unary.Any as Maybe-Any

import Data.List.Base as L
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All hiding (map)

open import Relation.Nullary
open import Relation.Unary using (Pred)
open import Relation.Binary
import Relation.Unary as Pred
open import Relation.Binary.PropositionalEquality

open import Auxiliary-Definitions

open import Data.Maybe using (Maybe; Is-just; Is-nothing; nothing)

module Partial-Map where

infix -5 _⇀_
-- Shorter notation for partial maps: X → Maybe Y
_⇀_ : {a b : Level} → Set a → Set b → Set (a ⊔ b)
_⇀_ X Y = X → Maybe Y


module _ {a b : Level} {A : Set a} {B : Set b} (f : A ⇀ B) where
  -- A function has a finite domain if it is only defined for A elements from the given list.
  -- We do not need the converse direction, because for every element in the list,
  -- one can simply check whether the partial function is defined.
  HasFiniteDomain : (dom : List A) → Set (a ⊔ b)
  HasFiniteDomain dom = ∀ x → Is-just (f x) → x ∈ dom

  finite-domain-∃-dec : ∀ {p} {P : A → Set p} {l}
                      → Pred.Decidable P
                      → HasFiniteDomain l
                      → Dec (∃[ x ] Is-just (f x) × P x)
  finite-domain-∃-dec {p} {P} {l} dec-P dom =
    case richer-dec of λ
    { (yes (x , x∈l , just-fx , px)) → yes (x , just-fx , px)
    ; (no contra) → no λ { (x , just-fx , px) → contra (x , dom x just-fx , just-fx , px) }
    }
    where
      just×P-dec : ∀ x → Dec (Is-just (f x) × P x)
      just×P-dec x with (f x) | dec-P x
      ... | nothing | _ = no λ { (() , _) }
      ... | _ | no bc = no λ { (_ , hyp) → bc hyp }
      ... | Maybe.just y | yes px = yes (Maybe-Any.just tt , px)
      richer-dec : Dec (∃[ x ] (x ∈ l) × Is-just (f x) × P x)
      richer-dec = map′ list-Any⇒∃ list-∃⇒Any (any? just×P-dec l)


  Domain : Pred A b
  Domain x = Is-just (f x)

  omit-nothing-from-domain : ∀ {u} {l} → HasFiniteDomain (u ∷ l) → f u ≡ nothing → HasFiniteDomain l
  omit-nothing-from-domain {u} has-dom eq x just-fx with (has-dom x just-fx)
  ... | there t = t
  ... | here x≡u rewrite x≡u rewrite eq with just-fx
  ...                                   | ()


module Order⇀ {a b : Level} {A : Set a} {B : Set b} where
  -- Partial order on partial maps:
  _⊑_ : (f f' : A ⇀ B) → Set (a ⊔ b)
  _⊑_ f f' = ∀ x → Is-just (f x) → f x ≡ f' x

  ⊑-elim : ∀ {x} {y} {f g : A ⇀ B} → (f ⊑ g) → (f x ≡ Maybe.just y) → (g x ≡ Maybe.just y)
  ⊑-elim {x = x} f⊑g x↦y rewrite (sym (f⊑g x (ret-just-⇒-is-just x↦y))) = x↦y


module _ {a b : Level} {A : Set a} {B : Set b} (_≟_ : DecidableEquality A) where
  List-to-⇀ : List (A × B) → A ⇀ B
  List-to-⇀ [] i = nothing
  List-to-⇀ ((j , o) ∷ xs) i with (j ≟ i)
  ... | yes _ = Maybe.just o
  ... | no _ = List-to-⇀ xs i

  List-to-finite-domain : ∀ l → HasFiniteDomain (List-to-⇀ l) (L.map proj₁ l)
  List-to-finite-domain ((i , o) ∷ l) j j-is-just with (i ≟ j)
  ... | yes refl = here refl
  List-to-finite-domain ((i , o) ∷ l) j zz | no neq = there (List-to-finite-domain l j zz)

  -- List-to-⇀-dom : ∀ l i → Is-just (List-to-⇀ l i) ↔ ∃[ o ] (i , o) ∈ l
  -- List-to-⇀-dom [] i = (λ ()) , λ ()
  -- List-to-⇀-dom ((j , o) ∷ l) i with (j ≟ i)
  -- ... | yes refl = (λ _ → o , here refl) , λ x → Maybe-Any.just tt
  -- ... | no neq = (λ z → {!!}) , {!!}

  open Order⇀
  ⇀-∷-⊑ : ∀ i o l → Is-nothing (List-to-⇀ l i) → List-to-⇀ l ⊑ List-to-⇀ ((i , o) ∷ l)
  ⇀-∷-⊑ i o l i∉dom j j∈dom with (i ≟ j)
  ... | no neq = refl
  ... | yes refl = ⊥-elim (Is-just¬nothing j∈dom i∉dom)