{-# OPTIONS --cubical #-}

module SemanticExplanation.OWLDirect where

open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Agda.Builtin.List using ([] ; _∷_)
open import Agda.Primitive using (Level)
open import SemanticExplanation

import OWL2.Syntax as Syntax
import OWL2.DirectSemantics as Direct
import OWL2.DirectSemantics.Lemmas as Lemmas

owlDirectDomain : DomainSpec
owlDirectDomain =
  domain-spec
    "ff-owl-direct-v1"
    ( entity-rule "owl.entity.class-expression" (quote Syntax.ClassExpression)
        (infrastructureArgument ∷ infrastructureArgument ∷ []) "class"
    ∷ entity-rule "owl.entity.object" (quote Direct.ObjectDomain)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument ∷ [] ) "object"
    ∷ [] )
    ( predicate-rule "owl.axiom.satisfied" (quote Direct.SatisfiesAxiom)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ semanticExpression ∷ [] )
        (unarySuffix "is satisfied")
    ∷ predicate-rule "owl.class.membership" (quote Direct.evalClass)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ semanticExpression ∷ semanticExpression ∷ [] )
        (binaryVerb "contains")
    ∷ [] )
    ( expression-rule "owl.axiom.subclass" (quote Syntax.Axiom.subClassOf)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ semanticExpression ∷ semanticExpression ∷ [] )
        (binaryForm "the axiom that class " " is a subclass of class " "")
    ∷ [] )
    ( infrastructure-rule "agda.level" (quote Level)
    ∷ infrastructure-rule "owl.signature" (quote Syntax.Signature)
    ∷ infrastructure-rule "owl.interpretation" (quote Direct.Interpretation)
    ∷ [] )
    []
    

classSubsumptionDirect : Explanation
classSubsumptionDirect = explainName owlDirectDomain Lemmas.classSubsumption

classSubsumptionDirectText
  : Explanation.text classSubsumptionDirect
  ≡ "For every class c, for every class d, for every object x, if the axiom that class c is a subclass of class d is satisfied, then if c contains x, then d contains x."
classSubsumptionDirectText = refl

classSubsumptionCompact : Explanation
classSubsumptionCompact =
  explainNameCompact owlDirectDomain Lemmas.classSubsumption

classSubsumptionCompactText
  : Explanation.text classSubsumptionCompact
  ≡ "For every class c, every class d, and every object x, if the axiom that class c is a subclass of class d is satisfied and c contains x, then d contains x."
classSubsumptionCompactText = refl

subClassReflDirect : Explanation
subClassReflDirect = explainName owlDirectDomain Lemmas.subClassRefl

subClassReflDirectText
  : Explanation.text subClassReflDirect
  ≡ "For every class c, the axiom that class c is a subclass of class c is satisfied."
subClassReflDirectText = refl

subClassTransDirect : Explanation
subClassTransDirect = explainName owlDirectDomain Lemmas.subClassTrans

subClassTransDirectText
  : Explanation.text subClassTransDirect
  ≡ "For every class c, for every class d, for every class e, if the axiom that class c is a subclass of class d is satisfied, then if the axiom that class d is a subclass of class e is satisfied, then the axiom that class c is a subclass of class e is satisfied."
subClassTransDirectText = refl

subClassTransCompact : Explanation
subClassTransCompact = explainNameCompact owlDirectDomain Lemmas.subClassTrans

subClassTransCompactText
  : Explanation.text subClassTransCompact
  ≡ "For every class c, every class d, and every class e, if the axiom that class c is a subclass of class d is satisfied and the axiom that class d is a subclass of class e is satisfied, then the axiom that class c is a subclass of class e is satisfied."
subClassTransCompactText = refl