{-# OPTIONS --guardedness #-}
{-# OPTIONS --allow-unsolved-metas #-}

open import Data.Unit
open import Data.Bool using (Bool)
import Data.Bool as Bool
open import Data.Fin using (Fin)
import Data.Fin as Fin
open import Data.Nat
open import Relation.Nullary.Decidable using (Dec)

module Owen where

data Con (S : Set) : Set where
  • : Con S
  _▷_ : Con S -> S -> Con S

data Var {S : Set} : Con S -> S -> Set where
  q : {A : S} -> {Γ : Con S} -> Var (Γ ▷ A) A
  p_ : {A B : S} -> {Γ : Con S} -> Var Γ A -> Var (Γ ▷ B) A

module RegularLogic (Sort : Set) (Rel : Con Sort -> Set) where
  variable Γ Δ : Con Sort
  variable A B : Sort
  Tm = Var
  Sub : Con Sort -> Con Sort -> Set
  Sub Γ Δ = (A : Sort) -> Tm Δ A -> Tm Γ A

  data Prop : Con Sort -> Set where
    true : Prop Γ
    _$_ : Rel Δ -> Sub Γ Δ -> Prop Γ
    _∧_ : Prop Γ -> Prop Γ -> Prop Γ
    _===_ : Tm Γ A -> Tm Γ A -> Prop Γ
    ∃ : Prop (Γ ▷ A) -> Prop Γ

  record Axiom : Set where
    field
      con : Con Sort
      ante : Prop con
      cons : Prop con

record Sig : Set where
  field
    sorts : Con ⊤
    rels : Con (Con (Var sorts tt))

Sort : (S : Sig) -> Set
Sort S = Var (Sig.sorts S) tt

Rel : (S : Sig) -> Con (Sort S) -> Set
Rel S = Var (Sig.rels S)

record Theory : Set where
  field
    sig : Sig
    axioms : Con (RegularLogic.Axiom (Sort sig) (Rel sig))

Tuple : (S : Sig) -> (Sort S -> ℕ) -> Con (Sort S) -> Set
Tuple S elts Γ = (A : Sort S) -> Var Γ A -> Fin (elts A)

record ModelData (S : Sig) : Set where
  field
    elts : Sort S -> ℕ
    sat : {Γ : Con (Sort S)} -> Rel S Γ -> Tuple S elts Γ -> Bool

module Interp (S : Sig) (M : ModelData S) where
  open RegularLogic (Sort S) (Rel S)
  t = Tuple S (ModelData.elts M)

  Elt : Sort S -> Set
  Elt A = Fin (ModelData.elts M A)

  extend : (Γ : Con (Sort S)) -> t Γ -> (A : Sort S) -> Elt A -> t (Γ ▷ A)
  extend = {!!}

  any : {n : ℕ} -> (Fin n -> Bool) -> Bool
  any = {!!}

  allTuples : (Γ : Con (Sort S)) -> (t Γ -> Bool) -> Bool
  allTuples = {!!}

  eval : {Γ : Con (Sort S)} -> {A : Sort S} -> Tm Γ A -> t Γ -> Elt A
  eval {Γ} {A} v f = f A v

  evalSub : {Γ Δ : Con (Sort S)} -> Sub Γ Δ -> t Γ -> t Δ
  evalSub s f A v = f A (s A v)

  interp : {Γ : Con (Sort S)} -> Prop Γ -> t Γ -> Bool
  interp true _ = Bool.true
  interp (r $ xs) f = ModelData.sat M r (evalSub xs f)
  interp (ϕ ∧ ψ) f = interp ϕ f Bool.∧ interp ψ f
  interp (x₁ === x₂) f = Dec.does (eval x₁ f Fin.≟ eval x₂ f)
  interp (∃ {Γ} {A} ϕ) f = any (λ i -> interp ϕ (extend Γ f A i))

  satisfies : Axiom -> Bool
  satisfies a = allTuples
    (Axiom.con a)
    (λ f -> Dec.does (interp (Axiom.ante a) f Bool.≤? interp (Axiom.cons a) f))