{-# OPTIONS --safe --cubical #-}

module OWL2.Examples.Family.Portable where

open import OWL2.Prelude using (String; []; _∷_)

import OWL2.Portable.Syntax as P

name : String → P.Name
name text =
  P.named (P.iri text)

className : String → P.ClassName
className =
  name

objectPropertyName : String → P.ObjectPropertyName
objectPropertyName =
  name

dataPropertyName : String → P.DataPropertyName
dataPropertyName =
  name

datatypeName : String → P.DatatypeName
datatypeName =
  name

individualName : String → P.NamedIndividualName
individualName =
  P.iri

Person Woman Man : P.ClassName
Person =
  className "https://example.org/family#Person"
Woman =
  className "https://example.org/family#Woman"
Man =
  className "https://example.org/family#Man"

hasWife hasSpouse hasParent : P.ObjectPropertyName
hasWife =
  objectPropertyName "https://example.org/family#hasWife"
hasSpouse =
  objectPropertyName "https://example.org/family#hasSpouse"
hasParent =
  objectPropertyName "https://example.org/family#hasParent"

age : P.DataPropertyName
age =
  dataPropertyName "https://example.org/family#age"

integer : P.DatatypeName
integer =
  datatypeName "http://www.w3.org/2001/XMLSchema#integer"

John Mary Bill : P.Individual
John =
  P.namedIndividual (individualName "https://example.org/family#John")
Mary =
  P.namedIndividual (individualName "https://example.org/family#Mary")
Bill =
  P.namedIndividual (individualName "https://example.org/family#Bill")

fortyTwo : P.Literal
fortyTwo =
  P.typedLiteral "42" integer

PersonC WomanC ManC : P.ClassExpression
PersonC =
  P.namedClass Person
WomanC =
  P.namedClass Woman
ManC =
  P.namedClass Man

HasWife HasSpouse HasParent : P.ObjectPropertyExpression
HasWife =
  P.objectProperty hasWife
HasSpouse =
  P.objectProperty hasSpouse
HasParent =
  P.objectProperty hasParent

Age : P.DataPropertyExpression
Age =
  P.dataProperty age

IntegerRange : P.DataRange
IntegerRange =
  P.datatype integer

axiom : P.Axiom → P.Annotated P.Axiom
axiom a =
  P.annotated [] a

portableFamilyOntology : P.Ontology
portableFamilyOntology =
  P.ontology
    (P.ontologyIRI (P.iri "https://example.org/family") P.absent)
    []
    []
    ( axiom (P.declaration (P.classEntity Person))
    ∷ axiom (P.declaration (P.classEntity Woman))
    ∷ axiom (P.declaration (P.objectPropertyEntity hasWife))
    ∷ axiom (P.subClassOf WomanC PersonC)
    ∷ axiom (P.subClassOf ManC PersonC)
    ∷ axiom (P.objectPropertyDomain HasWife ManC)
    ∷ axiom (P.objectPropertyRange HasWife WomanC)
    ∷ axiom
        (P.subObjectPropertyOf
          (P.subObjectProperty HasWife)
          HasSpouse)
    ∷ axiom (P.classAssertion ManC John)
    ∷ axiom (P.classAssertion WomanC Mary)
    ∷ axiom (P.objectPropertyAssertion HasWife John Mary)
    ∷ axiom (P.negativeObjectPropertyAssertion HasWife Bill Mary)
    ∷ axiom (P.dataPropertyRange Age IntegerRange)
    ∷ axiom (P.dataPropertyAssertion Age John fortyTwo)
    ∷ [] )

portableFamilyDocument : P.OntologyDocument
portableFamilyDocument =
  P.ontologyDocument [] portableFamilyOntology