import Level

record Signature {ℓ} : Set (Level.suc ℓ) where
  field
    C O R : Set ℓ

module Syntax {ℓ} (Σ : Signature {ℓ}) where
  open Signature Σ

  infixr 80 _⊓_
  infixr 85 _⊔_
  infix 90 all[_]_
  infix 90 ex[_]_
  data Concept : Set ℓ where
    `_ : C → Concept
    ⊤ ⊥ : Concept
    comp : Concept → Concept
    _⊔_ _⊓_ : Concept → Concept → Concept
    all[_]_ ex[_]_ : R → Concept → Concept

  data Formula : Set ℓ where
    _∶_ : O → Concept → Formula
    _⊑_ : Concept → Concept → Formula
    [_,_]∶_ : O → O → R → Formula

open import Relation.Unary
open import Relation.Binary
open import Relation.Nullary using (¬_)
open import Data.Empty renaming (⊥ to false)
open import Data.Unit renaming (⊤ to true)
open import Data.Product renaming (_×_ to _∧_)
open import Data.Sum renaming (_⊎_ to _∨_)
record Semantics {ℓ} (Σ : Signature {ℓ}) : Set (Level.suc ℓ) where
  open Signature Σ
  field
    𝓓 : Set ℓ
    ⟦_⟧C : C → Pred 𝓓 ℓ
    ⟦_⟧O : O → 𝓓
    ⟦_⟧R : R → Rel 𝓓 ℓ

  open Syntax Σ
  ⟦_⟧ : Concept → Pred 𝓓 ℓ
  ⟦ ` c ⟧ x = ⟦ c ⟧C x
  ⟦ ⊤ ⟧ x = Level.Lift ℓ true
  ⟦ ⊥ ⟧ x = Level.Lift ℓ false
  ⟦ comp A ⟧ x = ¬ (⟦ A ⟧ x)
  ⟦ A ⊔ B ⟧ x = (⟦ A ⟧ x) ∨ (⟦ B ⟧ x)
  ⟦ A ⊓ B ⟧ x = (⟦ A ⟧ x) ∧ (⟦ B ⟧ x)
  ⟦ all[ S ] A ⟧ x = ∀ {y} → ⟦ S ⟧R x y → ⟦ A ⟧ y
  ⟦ ex[ S ] A ⟧ x = ∃ λ y → ⟦ S ⟧R x y ∧ ⟦ A ⟧ y

  ⊨⟦_⟧ : Formula → Set ℓ
  ⊨⟦ a ∶ A ⟧ = ⟦ A ⟧ (⟦ a ⟧O)
  ⊨⟦ A ⊑ B ⟧ = ∀ x → ⟦ A ⟧ x → ⟦ B ⟧ x
  ⊨⟦ [ a , b ]∶ S ⟧ = ⟦ S ⟧R (⟦ a ⟧O) (⟦ b ⟧O)

module Example where
  data O : Set where
    Alice Bob Eve : O

  data C : Set where
    LetterWriter : C

  data R : Set where
    Likes : R

  D : Set
  D = O

  data _writesLetters : D → Set where
    shedoes : Alice writesLetters
    hedoes : Bob writesLetters

  data _likes_ : D → D → Set where
    indeed : Alice likes Bob

  Sig : Signature {Level.zero}
  Sig .Signature.C = C
  Sig .Signature.O = O
  Sig .Signature.R = R

  Sem : Semantics Sig
  Sem .Semantics.𝓓 = D
  Semantics.⟦ Sem ⟧C LetterWriter = _writesLetters
  Semantics.⟦ Sem ⟧O = λ x → x
  Semantics.⟦ Sem ⟧R Likes = _likes_

  open Syntax Sig
  open Semantics Sem

  example : ⊨⟦ Alice ∶ (all[ Likes ] (` LetterWriter)) ⟧
  example indeed = hedoes

  example' : ⊨⟦ (ex[ Likes ] (` LetterWriter)) ⊑ (` LetterWriter) ⟧
  example' Alice _ = shedoes
  example' Bob _ = hedoes
  example' Eve ()