SemanticExplanation.Industry.OWL

{-# OPTIONS --cubical #-}

module SemanticExplanation.Industry.OWL where

open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Agda.Builtin.List using ([] ; _∷_)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Reflection using (Name)
open import Agda.Primitive using (Set)
open import SemanticExplanation

import OWL2.DirectSemantics.Lemmas as OWLLemmas

-- A concrete aircraft-engine maintenance, repair, and overhaul (MRO) case.
-- The declarations below are a deliberately small semantic adapter.  Their
-- Pi/premise shapes correspond to ff-owl's property-chain, existential
-- restriction, and HasKey rules; the live lemma Names are retained below.

data LicensedAircraftEngineer : Set where
  exampleCertifyingEngineer : LicensedAircraftEngineer

data InspectionWorkOrder : Set where
  exampleBorescopeWorkOrder : InspectionWorkOrder

data TurbofanEngineModule : Set where
  exampleHighPressureCompressor : TurbofanEngineModule

data SerializedLifeLimitedPart : Set where
  exampleCompressorDisk : SerializedLifeLimitedPart

data SignedOff
  : LicensedAircraftEngineer → InspectionWorkOrder → Set where
  signedOffEvidence : ∀ {certifyingEngineer workOrder} →
    SignedOff certifyingEngineer workOrder

data CoversEngineModule
  : InspectionWorkOrder → TurbofanEngineModule → Set where
  coverageEvidence : ∀ {workOrder engineModule} →
    CoversEngineModule workOrder engineModule

data HasTraceableInspection
  : LicensedAircraftEngineer → TurbofanEngineModule → Set where
  tracedThroughWorkOrder : ∀ {certifyingEngineer workOrder engineModule} →
    SignedOff certifyingEngineer workOrder →
    CoversEngineModule workOrder engineModule →
    HasTraceableInspection certifyingEngineer engineModule

data EngineModuleLinkedToOrder
  : TurbofanEngineModule → InspectionWorkOrder → Set where
  orderLinkEvidence : ∀ {engineModule workOrder} →
    EngineModuleLinkedToOrder engineModule workOrder

data IsConformingBorescopeInspection : InspectionWorkOrder → Set where
  conformingInspectionEvidence : ∀ {workOrder} →
    IsConformingBorescopeInspection workOrder

data HasRequiredBorescopeInspection : TurbofanEngineModule → Set where
  qualifyingInspectionWitness : ∀ {engineModule workOrder} →
    EngineModuleLinkedToOrder engineModule workOrder →
    IsConformingBorescopeInspection workOrder →
    HasRequiredBorescopeInspection engineModule

data HoldsModuleReleaseAuthorization
  : LicensedAircraftEngineer → TurbofanEngineModule → Set where
  releaseAuthorizationEvidence : ∀ {certifyingEngineer engineModule} →
    HoldsModuleReleaseAuthorization certifyingEngineer engineModule

data EligibleToIssueReturnToServiceRelease
  : LicensedAircraftEngineer → TurbofanEngineModule → Set where
  releaseEligibilityEvidence : ∀ {certifyingEngineer engineModule} →
    HasTraceableInspection certifyingEngineer engineModule →
    HasRequiredBorescopeInspection engineModule →
    HoldsModuleReleaseAuthorization certifyingEngineer engineModule →
    EligibleToIssueReturnToServiceRelease certifyingEngineer engineModule

data IsRegisteredLifeLimitedPart : SerializedLifeLimitedPart → Set where
  registeredPartEvidence : ∀ {part} → IsRegisteredLifeLimitedPart part

data SharesPartNumberAndSerial
  : SerializedLifeLimitedPart → SerializedLifeLimitedPart → Set where
  sharedAssetKeyEvidence : ∀ {left right} → SharesPartNumberAndSerial left right

data DenotesSameRegisteredAsset
  : SerializedLifeLimitedPart → SerializedLifeLimitedPart → Set where
  registeredAssetIdentity : ∀ {left right} →
    IsRegisteredLifeLimitedPart left →
    IsRegisteredLifeLimitedPart right →
    SharesPartNumberAndSerial left right →
    DenotesSameRegisteredAsset left right

-- Property-chain shape: signed-off-by ∘ covers-module entails a traceable
-- engineer-to-module inspection relation.
maintenanceTraceFromSignedWorkOrder :
  (certifyingEngineer : LicensedAircraftEngineer) →
  (workOrder : InspectionWorkOrder) →
  (engineModule : TurbofanEngineModule) →
  SignedOff certifyingEngineer workOrder →
  CoversEngineModule workOrder engineModule →
  HasTraceableInspection certifyingEngineer engineModule
maintenanceTraceFromSignedWorkOrder certifyingEngineer workOrder engineModule signed coverage =
  tracedThroughWorkOrder signed coverage

-- Existential-restriction introduction shape: an explicit related filler that
-- belongs to the qualifying class establishes some-values-from membership.
requiredInspectionFromConformingOrder :
  (engineModule : TurbofanEngineModule) →
  (workOrder : InspectionWorkOrder) →
  EngineModuleLinkedToOrder engineModule workOrder →
  IsConformingBorescopeInspection workOrder →
  HasRequiredBorescopeInspection engineModule
requiredInspectionFromConformingOrder engineModule workOrder linked conforming =
  qualifyingInspectionWitness linked conforming

moduleOrderLinkFromCoverage :
  (workOrder : InspectionWorkOrder) →
  (engineModule : TurbofanEngineModule) →
  CoversEngineModule workOrder engineModule →
  EngineModuleLinkedToOrder engineModule workOrder
moduleOrderLinkFromCoverage workOrder engineModule coverage = orderLinkEvidence

-- The operational compliance decision combines traceability, the required
-- inspection restriction, and role authorization.
returnToServiceEligibility :
  (certifyingEngineer : LicensedAircraftEngineer) →
  (engineModule : TurbofanEngineModule) →
  HasTraceableInspection certifyingEngineer engineModule →
  HasRequiredBorescopeInspection engineModule →
  HoldsModuleReleaseAuthorization certifyingEngineer engineModule →
  EligibleToIssueReturnToServiceRelease certifyingEngineer engineModule
returnToServiceEligibility certifyingEngineer engineModule trace inspection authorization =
  releaseEligibilityEvidence trace inspection authorization

-- A complete application of the three rules above.  Its type contains only
-- the evidence a release reviewer starts with; the proof constructs the
-- property-chain result and existential-restriction witness internally.
returnToServiceFromMaintenanceRecord :
  (certifyingEngineer : LicensedAircraftEngineer) →
  (workOrder : InspectionWorkOrder) →
  (engineModule : TurbofanEngineModule) →
  SignedOff certifyingEngineer workOrder →
  CoversEngineModule workOrder engineModule →
  IsConformingBorescopeInspection workOrder →
  HoldsModuleReleaseAuthorization certifyingEngineer engineModule →
  EligibleToIssueReturnToServiceRelease certifyingEngineer engineModule
returnToServiceFromMaintenanceRecord certifyingEngineer workOrder engineModule
  signed coverage conforming authorization =
  returnToServiceEligibility certifyingEngineer engineModule
    (maintenanceTraceFromSignedWorkOrder certifyingEngineer workOrder engineModule signed coverage)
    (requiredInspectionFromConformingOrder engineModule workOrder
      (moduleOrderLinkFromCoverage workOrder engineModule coverage) conforming)
    authorization

-- HasKey shape: key agreement identifies two names in the interpretation; it
-- does not assert that similarly described parts have distinct identities.
lifeLimitedPartIdentityFromAssetKey :
  (installedPart inventoryAlias : SerializedLifeLimitedPart) →
  IsRegisteredLifeLimitedPart installedPart →
  IsRegisteredLifeLimitedPart inventoryAlias →
  SharesPartNumberAndSerial installedPart inventoryAlias →
  DenotesSameRegisteredAsset installedPart inventoryAlias
lifeLimitedPartIdentityFromAssetKey installedPart inventoryAlias
  installedRegistered aliasRegistered sharedKey =
  registeredAssetIdentity installedRegistered aliasRegistered sharedKey

-- Compile-checked links to the live ff-owl semantic rules represented by the
-- local adapter.  These are evidence anchors, not printed QName dispatch.
liveObjectPropertyChainRule : Name
liveObjectPropertyChainRule = quote OWLLemmas.objectPropertyChain₂Intro

liveExistentialRestrictionRule : Name
liveExistentialRestrictionRule = quote OWLLemmas.objectSomeIntro

liveHasKeyRule : Name
liveHasKeyRule = quote OWLLemmas.hasKeyApply

maintenanceTraceSource : Name
maintenanceTraceSource = quote maintenanceTraceFromSignedWorkOrder

requiredInspectionSource : Name
requiredInspectionSource = quote requiredInspectionFromConformingOrder

returnToServiceSource : Name
returnToServiceSource = quote returnToServiceEligibility

maintenanceReleaseCaseSource : Name
maintenanceReleaseCaseSource = quote returnToServiceFromMaintenanceRecord

lifeLimitedPartIdentitySource : Name
lifeLimitedPartIdentitySource = quote lifeLimitedPartIdentityFromAssetKey

aircraftMaintenanceFuel : Nat
aircraftMaintenanceFuel = 768

aircraftMaintenanceDomain : DomainSpec
aircraftMaintenanceDomain =
  domain-spec
    "ff-owl-aircraft-engine-mro-v1"
    ( entity-rule "mro.entity.engineer" (quote LicensedAircraftEngineer) []
        "licensed aircraft engineer"
    ∷ entity-rule "mro.entity.work-order" (quote InspectionWorkOrder) []
        "inspection work order"
    ∷ entity-rule "mro.entity.engine-module" (quote TurbofanEngineModule) []
        "turbofan engine module"
    ∷ entity-rule "mro.entity.life-limited-part" (quote SerializedLifeLimitedPart) []
        "serialized life-limited part"
    ∷ [] )
    ( predicate-rule "mro.property.signed-off" (quote SignedOff)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "signed off")
    ∷ predicate-rule "mro.property.covers-module" (quote CoversEngineModule)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "covers")
    ∷ predicate-rule "mro.property.traceable-inspection" (quote HasTraceableInspection)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "has a traceable inspection for")
    ∷ predicate-rule "mro.property.module-order-link" (quote EngineModuleLinkedToOrder)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "is linked in the maintenance system to")
    ∷ predicate-rule "mro.class.conforming-borescope" (quote IsConformingBorescopeInspection)
        (semanticExpression ∷ [])
        (unarySuffix "is a conforming borescope inspection")
    ∷ predicate-rule "mro.restriction.required-borescope" (quote HasRequiredBorescopeInspection)
        (semanticExpression ∷ [])
        (unarySuffix "has at least one conforming borescope inspection on record")
    ∷ predicate-rule "mro.property.release-authorization" (quote HoldsModuleReleaseAuthorization)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "holds release authorization for")
    ∷ predicate-rule "mro.decision.return-to-service" (quote EligibleToIssueReturnToServiceRelease)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "is eligible to issue a return-to-service release for")
    ∷ predicate-rule "mro.class.registered-life-limited-part" (quote IsRegisteredLifeLimitedPart)
        (semanticExpression ∷ [])
        (unarySuffix "is registered as a life-limited part")
    ∷ predicate-rule "mro.key.part-number-and-serial" (quote SharesPartNumberAndSerial)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "has the same part-number-and-serial key as")
    ∷ predicate-rule "mro.identity.registered-asset" (quote DenotesSameRegisteredAsset)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "denotes the same registered maintenance asset as")
    ∷ [] )
    []
    []
    []
    aircraftMaintenanceFuel

maintenanceTraceExplanation : Explanation
maintenanceTraceExplanation =
  explainNameCompact aircraftMaintenanceDomain maintenanceTraceFromSignedWorkOrder

maintenanceTraceText :
  Explanation.text maintenanceTraceExplanation ≡
  "For every licensed aircraft engineer certifyingEngineer, every inspection work order workOrder, and every turbofan engine module engineModule, if certifyingEngineer signed off workOrder and workOrder covers engineModule, then certifyingEngineer has a traceable inspection for engineModule."
maintenanceTraceText = refl

requiredInspectionExplanation : Explanation
requiredInspectionExplanation =
  explainNameCompact aircraftMaintenanceDomain requiredInspectionFromConformingOrder

requiredInspectionText :
  Explanation.text requiredInspectionExplanation ≡
  "For every turbofan engine module engineModule and every inspection work order workOrder, if engineModule is linked in the maintenance system to workOrder and workOrder is a conforming borescope inspection, then engineModule has at least one conforming borescope inspection on record."
requiredInspectionText = refl

returnToServiceExplanation : Explanation
returnToServiceExplanation =
  explainNameCompact aircraftMaintenanceDomain returnToServiceEligibility

returnToServiceText :
  Explanation.text returnToServiceExplanation ≡
  "For every licensed aircraft engineer certifyingEngineer and every turbofan engine module engineModule, if certifyingEngineer has a traceable inspection for engineModule, engineModule has at least one conforming borescope inspection on record, and certifyingEngineer holds release authorization for engineModule, then certifyingEngineer is eligible to issue a return-to-service release for engineModule."
returnToServiceText = refl

maintenanceReleaseCaseExplanation : Explanation
maintenanceReleaseCaseExplanation =
  explainNameCompact aircraftMaintenanceDomain returnToServiceFromMaintenanceRecord

maintenanceReleaseCaseText :
  Explanation.text maintenanceReleaseCaseExplanation ≡
  "For every licensed aircraft engineer certifyingEngineer, every inspection work order workOrder, and every turbofan engine module engineModule, if certifyingEngineer signed off workOrder, workOrder covers engineModule, workOrder is a conforming borescope inspection, and certifyingEngineer holds release authorization for engineModule, then certifyingEngineer is eligible to issue a return-to-service release for engineModule."
maintenanceReleaseCaseText = refl

lifeLimitedPartIdentityExplanation : Explanation
lifeLimitedPartIdentityExplanation =
  explainNameCompact aircraftMaintenanceDomain lifeLimitedPartIdentityFromAssetKey

lifeLimitedPartIdentityText :
  Explanation.text lifeLimitedPartIdentityExplanation ≡
  "For every serialized life-limited part installedPart and every serialized life-limited part inventoryAlias, if installedPart is registered as a life-limited part, inventoryAlias is registered as a life-limited part, and installedPart has the same part-number-and-serial key as inventoryAlias, then installedPart denotes the same registered maintenance asset as inventoryAlias."
lifeLimitedPartIdentityText = refl

maintenanceTraceProvenance :
  Explanation.provenance maintenanceTraceExplanation ≡
  ( ruleUsed "mro.entity.engineer"
  ∷ ruleUsed "mro.entity.work-order"
  ∷ ruleUsed "mro.entity.engine-module"
  ∷ ruleUsed "mro.property.signed-off"
  ∷ ruleUsed "mro.property.covers-module"
  ∷ ruleUsed "mro.property.traceable-inspection"
  ∷ [] )
maintenanceTraceProvenance = refl

maintenanceTraceCandidate :
  Explanation.candidateId maintenanceTraceExplanation ≡ "compact/v1"
maintenanceTraceCandidate = refl

maintenanceTraceDomain :
  Explanation.domainId maintenanceTraceExplanation ≡
  "ff-owl-aircraft-engine-mro-v1"
maintenanceTraceDomain = refl

-- The domain fuel is intentionally explicit and generous.  All five compact
-- macros consume aircraftMaintenanceDomain.reductionFuel (= 768).