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

module OWL2.Corpus.Accepted.SymbolTable where

open import OWL2.Prelude
open import OWL2.Elab.SymbolTable
open import OWL2.Foundation.Fin
open import OWL2.Raw
import OWL2.Kernel as K

leftClassIRI rightClassIRI : RawIRI
leftClassIRI =
  rawIRI "http://example.test/project/LeftClass"
rightClassIRI =
  rawIRI "http://example.test/project/RightClass"

leftObjectPropertyIRI rightObjectPropertyIRI : RawIRI
leftObjectPropertyIRI =
  rawIRI "http://example.test/project/leftObjectProperty"
rightObjectPropertyIRI =
  rawIRI "http://example.test/project/rightObjectProperty"

leftSymbolTable rightSymbolTable : SymbolTable
leftSymbolTable =
  symbolTable
    (leftClassIRI ∷ [])
    (leftObjectPropertyIRI ∷ [])
    []
    []
    []
    []
    []
    []
    []
    K.noPunning
rightSymbolTable =
  symbolTable
    (rightClassIRI ∷ [])
    (rightObjectPropertyIRI ∷ [])
    []
    []
    []
    []
    []
    []
    []
    K.noPunning

combinedSymbolTable : SymbolTable
combinedSymbolTable =
  appendSymbolTables K.noPunning leftSymbolTable rightSymbolTable

combinedClassCount :
  K.classCount (symbolTableSignature combinedSymbolTable) ≡ 2
combinedClassCount =
  refl

combinedObjectPropertyCount :
  K.objectPropertyCount (symbolTableSignature combinedSymbolTable) ≡ 2
combinedObjectPropertyCount =
  refl

leftTableMorphism :
  K.SignatureMorphism
    (symbolTableSignature leftSymbolTable)
    (symbolTableSignature combinedSymbolTable)
leftTableMorphism =
  leftSymbolTableMorphism
    K.noPunning
    leftSymbolTable
    rightSymbolTable

rightTableMorphism :
  K.SignatureMorphism
    (symbolTableSignature rightSymbolTable)
    (symbolTableSignature combinedSymbolTable)
rightTableMorphism =
  rightSymbolTableMorphism
    K.noPunning
    leftSymbolTable
    rightSymbolTable

leftClassMapsToLeftSlot :
  lookupByFin
    (classIRIs combinedSymbolTable)
    (K.symbol
      (K.mapClassName leftTableMorphism (K.className fzero))) ≡
  leftClassIRI
leftClassMapsToLeftSlot =
  refl

rightClassMapsToRightSlot :
  lookupByFin
    (classIRIs combinedSymbolTable)
    (K.symbol
      (K.mapClassName rightTableMorphism (K.className fzero))) ≡
  rightClassIRI
rightClassMapsToRightSlot =
  refl

leftObjectPropertyMapsToLeftSlot :
  lookupByFin
    (objectPropertyIRIs combinedSymbolTable)
    (K.symbol
      (K.mapObjectPropertyName
        leftTableMorphism
        (K.objectPropertyName fzero))) ≡
  leftObjectPropertyIRI
leftObjectPropertyMapsToLeftSlot =
  refl

rightObjectPropertyMapsToRightSlot :
  lookupByFin
    (objectPropertyIRIs combinedSymbolTable)
    (K.symbol
      (K.mapObjectPropertyName
        rightTableMorphism
        (K.objectPropertyName fzero))) ≡
  rightObjectPropertyIRI
rightObjectPropertyMapsToRightSlot =
  refl