open import Data.Product
open import Relation.Binary
open import Data.Nat hiding (_^_)
open import Data.Nat.Properties
open import Level renaming (suc to lsuc) hiding (zero)
open import Data.List
open import Data.List.Membership.Propositional
open import Data.Empty renaming (⊥ to False)
open import Data.Unit renaming (⊤ to True)
open import Relation.Binary.PropositionalEquality
open import Data.List.Relation.Unary.Any

data Formula {ℓ} (A : Set ℓ) : Set ℓ where
  `_ : A → Formula A
  ⊥ : Formula A
  ⊤ : Formula A
  _∧_ : Formula A → Formula A → Formula A
  ¬_ : Formula A → Formula A
  X_ : Formula A → Formula A
  F_ : Formula A → Formula A
  G_ : Formula A → Formula A
  _U_ : Formula A → Formula A → Formula A

record TS {ℓ} : Set (lsuc ℓ) where
  field
    S : Set ℓ
    _⟶_ : Rel S ℓ

NT : ∀ {ℓ} (ts : TS {ℓ}) → Set ℓ
NT ts = ∀ (s : S) → Σ (S) λ s' → s ⟶ s'
  where open TS ts

module Path {ℓ} (ts : TS {ℓ}) where
  open TS ts

  record Path : Set ℓ where
    constructor ⟨_,_⟩
    field
      π : ℕ → S
      con : ∀ {n : ℕ} → (π n) ⟶ (π (suc n))

  _^_ : Path → ℕ → Path
  ⟨ π , con ⟩ ^ n = ⟨ (λ x → π (n + x)) , (λ {m} → subst (λ h → (π (n + m)) ⟶ π h) (sym (+-suc n m)) (con {n + m})) ⟩
    
module Model {ℓ} (ts : TS {ℓ}) {nt : NT ts} (A : Set ℓ) where
  open TS ts
  
  record Model : Set ℓ where
    field
      L : S → List A            -- poor man's powerset

module SAT {ℓ} (ts : TS {ℓ}) {nt : NT ts} (A : Set ℓ) where
  open TS ts
  open Path ts
  open Model ts {nt} A
  
  ⟨_,_⟩⊩_ : Model → Path → Formula A → Set ℓ
  ⟨ 𝓜 , ⟨ π , _ ⟩ ⟩⊩ (` x) = x ∈ (Model.L 𝓜 (π zero))
  ⟨ 𝓜 , _ ⟩⊩ ⊥ = Lift ℓ False
  ⟨ 𝓜 , _ ⟩⊩ ⊤ = Lift ℓ True
  ⟨ 𝓜 , p ⟩⊩ (φ ∧ ψ) = (⟨ 𝓜 , p ⟩⊩ φ) × (⟨ 𝓜 , p ⟩⊩ ψ)
  ⟨ 𝓜 , p ⟩⊩ (¬ φ) = ⟨ 𝓜 , p ⟩⊩ φ → False
  ⟨ 𝓜 , p ⟩⊩ (X φ) = ⟨ 𝓜 , p ^ 1 ⟩⊩ φ
  ⟨ 𝓜 , p ⟩⊩ (F φ) = Σ ℕ λ k → ⟨ 𝓜 , p ^ k ⟩⊩ φ
  ⟨ 𝓜 , p ⟩⊩ (G φ) = ∀ (k : ℕ) → ⟨ 𝓜 , p ^ k ⟩⊩ φ
  ⟨ 𝓜 , p ⟩⊩ (φ U ψ) = (Σ ℕ (λ k → (⟨ 𝓜 , p ^ k ⟩⊩ ψ)
                          × (∀ (l : ℕ) → {l < k} → ⟨ 𝓜 , p ^ l ⟩⊩ φ)))

module Example where

  data S : Set where
    a : S
    b : S
    c : S
    d : S

  data A : Set where
    p : A
    q : A
    r : A

  _⟶_ : S → S → Set
  a ⟶ b = True
  b ⟶ c = True
  c ⟶ a = True
  b ⟶ d = True
  d ⟶ d = True
  _ ⟶ _ = False
  
  ts : TS
  ts .TS.S = S
  ts .TS._⟶_ = _⟶_

  nt : NT ts
  nt a = b , tt
  nt b = c , tt
  nt c = a , tt
  nt d = d , tt

  open Model ts {nt} A

  M : Model
  M .Model.L a = p ∷ q ∷ []
  M .Model.L b = p ∷ r ∷ []
  M .Model.L c = p ∷ []
  M .Model.L d = r ∷ []
    
  open Path ts
  δ : Path
  δ .Path.π zero = a
  δ .Path.π (suc zero) = b
  δ .Path.π (2+ zero) = c
  δ .Path.π (2+ (suc x)) = δ .Path.Path.π x
  δ .Path.con {zero} = tt
  δ .Path.con {suc zero} = tt
  δ .Path.con {2+ zero} = tt
  δ .Path.con {2+ (suc n)} = δ .Path.Path.con {n}

  ρ : Path
  ρ .Path.π zero = a
  ρ .Path.π (suc zero) = b
  ρ .Path.π (2+ _) = d
  ρ .Path.con {zero} = tt
  ρ .Path.con {suc zero} = tt
  ρ .Path.con {2+ n} = tt
  
  open SAT ts {nt} A

  foo : ⟨ M , δ ⟩⊩ G (` p)
  foo zero = here refl
  foo (suc zero) = here refl
  foo (2+ zero) = here refl
  foo (2+ (suc k)) = foo k

  bar : ⟨ M , ρ ⟩⊩ F G (` r)
  bar = 2 , λ _ → here refl