99 lines
2.7 KiB
Agda
99 lines
2.7 KiB
Agda
{-# 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))
|