{-# OPTIONS --cubical #-}
module SemanticExplanation.Industry.OWLMore 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 OWL
data SerializedMedicinePack : Set where samplePack : SerializedMedicinePack
data ProductionBatch : Set where sampleLot : ProductionBatch
data MarketRecall : Set where sampleRecall : MarketRecall
data RegisteredSaleablePack : SerializedMedicinePack → Set where registeredPack : ∀ {x} → RegisteredSaleablePack x
data SharesProductCodeAndSerial : SerializedMedicinePack → SerializedMedicinePack → Set where sharedPackKey : ∀ {x y} → SharesProductCodeAndSerial x y
data DenotesSameSaleablePack : SerializedMedicinePack → SerializedMedicinePack → Set where samePack : ∀ {x y} → DenotesSameSaleablePack x y
data PackBelongsToBatch : SerializedMedicinePack → ProductionBatch → Set where packBatch : ∀ {x y} → PackBelongsToBatch x y
data BatchIncludedInRecall : ProductionBatch → MarketRecall → Set where batchRecall : ∀ {x y} → BatchIncludedInRecall x y
data PackAffectedByRecall : SerializedMedicinePack → MarketRecall → Set where affectedPack : ∀ {x y} → PackAffectedByRecall x y
data PackDistributedToMarket : SerializedMedicinePack → Set where distributedPack : ∀ {x} → PackDistributedToMarket x
data QuarantineDispatchRequired : SerializedMedicinePack → Set where quarantineDispatch : ∀ {x} → QuarantineDispatchRequired x
data WholesaleRemovalRequired : SerializedMedicinePack → Set where wholesaleRemoval : ∀ {x} → WholesaleRemovalRequired x
serializedPackIdentityFromKey
: (installed inventoryRecord : SerializedMedicinePack)
→ RegisteredSaleablePack installed
→ RegisteredSaleablePack inventoryRecord
→ SharesProductCodeAndSerial installed inventoryRecord
→ DenotesSameSaleablePack installed inventoryRecord
serializedPackIdentityFromKey installed inventoryRecord left right key = samePack
batchRecallPropagatesToPack
: (pack : SerializedMedicinePack) (lot : ProductionBatch) (recall : MarketRecall)
→ PackBelongsToBatch pack lot
→ BatchIncludedInRecall lot recall
→ PackAffectedByRecall pack recall
batchRecallPropagatesToPack pack lot recall membership recall-scope = affectedPack
distributedRecalledPackRequiresQuarantineDispatch
: (pack : SerializedMedicinePack) (recall : MarketRecall)
→ PackAffectedByRecall pack recall
→ PackDistributedToMarket pack
→ QuarantineDispatchRequired pack
distributedRecalledPackRequiresQuarantineDispatch pack recall affected distributed = quarantineDispatch
recalledPackRequiresWholesaleRemoval
: (pack : SerializedMedicinePack) (recall : MarketRecall)
→ PackAffectedByRecall pack recall
→ QuarantineDispatchRequired pack
→ WholesaleRemovalRequired pack
recalledPackRequiresWholesaleRemoval pack recall affected quarantine = wholesaleRemoval
data OffshoreWindTurbine : Set where sampleTurbine : OffshoreWindTurbine
data InspectionCertificate : Set where sampleInspectionCertificate : InspectionCertificate
data AuthorizedGridEngineer : Set where sampleGridEngineer : AuthorizedGridEngineer
data CertificateCoversTurbine : InspectionCertificate → OffshoreWindTurbine → Set where coversTurbine : ∀ {x y} → CertificateCoversTurbine x y
data InspectionCertificateCurrent : InspectionCertificate → Set where currentCertificate : ∀ {x} → InspectionCertificateCurrent x
data TurbineHasCurrentInspection : OffshoreWindTurbine → Set where currentInspection : ∀ {x} → TurbineHasCurrentInspection x
data ProtectionSettingsReviewed : OffshoreWindTurbine → Set where settingsReviewed : ∀ {x} → ProtectionSettingsReviewed x
data EngineerAuthorizedForTurbine : AuthorizedGridEngineer → OffshoreWindTurbine → Set where engineerAuthorized : ∀ {x y} → EngineerAuthorizedForTurbine x y
data EligibleForGridEnergization : OffshoreWindTurbine → Set where energizationEligible : ∀ {x} → EligibleForGridEnergization x
data OpenBladeDefect : OffshoreWindTurbine → Set where bladeDefect : ∀ {x} → OpenBladeDefect x
data RepairEvidencePending : OffshoreWindTurbine → Set where repairPending : ∀ {x} → RepairEvidencePending x
data GridEnergizationBlocked : OffshoreWindTurbine → Set where energizationBlocked : ∀ {x} → GridEnergizationBlocked x
currentCertificateEstablishesInspection
: (certificate : InspectionCertificate) (turbine : OffshoreWindTurbine)
→ CertificateCoversTurbine certificate turbine
→ InspectionCertificateCurrent certificate
→ TurbineHasCurrentInspection turbine
currentCertificateEstablishesInspection certificate turbine coverage current = currentInspection
reviewedTurbineEligibleForEnergization
: (engineer : AuthorizedGridEngineer) (turbine : OffshoreWindTurbine)
→ TurbineHasCurrentInspection turbine
→ ProtectionSettingsReviewed turbine
→ EngineerAuthorizedForTurbine engineer turbine
→ EligibleForGridEnergization turbine
reviewedTurbineEligibleForEnergization engineer turbine inspection settings authorization = energizationEligible
openDefectBlocksEnergization
: (turbine : OffshoreWindTurbine)
→ OpenBladeDefect turbine
→ RepairEvidencePending turbine
→ GridEnergizationBlocked turbine
openDefectBlocksEnergization turbine defect pending = energizationBlocked
owlMoreFuel : Nat
owlMoreFuel = 768
owlMoreDomain : DomainSpec
owlMoreDomain =
domain-spec "industry-owl-pharma-wind-v1"
( entity-rule "pharma.entity.pack" (quote SerializedMedicinePack) [] "serialized medicine pack"
∷ entity-rule "pharma.entity.batch" (quote ProductionBatch) [] "production batch"
∷ entity-rule "pharma.entity.recall" (quote MarketRecall) [] "market recall"
∷ entity-rule "wind.entity.turbine" (quote OffshoreWindTurbine) [] "offshore wind-turbine asset"
∷ entity-rule "wind.entity.certificate" (quote InspectionCertificate) [] "inspection certificate"
∷ entity-rule "wind.entity.engineer" (quote AuthorizedGridEngineer) [] "authorized grid engineer"
∷ [] )
( predicate-rule "pharma.pack.registered" (quote RegisteredSaleablePack) (semanticExpression ∷ []) (unarySuffix "is registered as a saleable medicine pack")
∷ predicate-rule "pharma.pack.key" (quote SharesProductCodeAndSerial) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "has the same product-code-and-serial key as")
∷ predicate-rule "pharma.pack.identity" (quote DenotesSameSaleablePack) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "denotes the same serialized saleable pack as")
∷ predicate-rule "pharma.pack.batch" (quote PackBelongsToBatch) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "belongs to")
∷ predicate-rule "pharma.batch.recall" (quote BatchIncludedInRecall) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "is included in")
∷ predicate-rule "pharma.pack.recall" (quote PackAffectedByRecall) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "is affected by")
∷ predicate-rule "pharma.pack.distributed" (quote PackDistributedToMarket) (semanticExpression ∷ []) (unarySuffix "has already been distributed to market")
∷ predicate-rule "pharma.pack.quarantine-dispatch" (quote QuarantineDispatchRequired) (semanticExpression ∷ []) (unarySuffix "requires a quarantine instruction to be dispatched")
∷ predicate-rule "pharma.pack.wholesale-removal" (quote WholesaleRemovalRequired) (semanticExpression ∷ []) (unarySuffix "requires removal from wholesale distribution")
∷ predicate-rule "wind.certificate.covers" (quote CertificateCoversTurbine) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "covers")
∷ predicate-rule "wind.certificate.current" (quote InspectionCertificateCurrent) (semanticExpression ∷ []) (unarySuffix "is within its reviewed validity period")
∷ predicate-rule "wind.inspection.current" (quote TurbineHasCurrentInspection) (semanticExpression ∷ []) (unarySuffix "has a current inspection on record")
∷ predicate-rule "wind.protection.reviewed" (quote ProtectionSettingsReviewed) (semanticExpression ∷ []) (unarySuffix "has reviewed grid-protection settings")
∷ predicate-rule "wind.engineer.authorized" (quote EngineerAuthorizedForTurbine) (semanticExpression ∷ semanticExpression ∷ []) (binaryVerb "is authorized to release")
∷ predicate-rule "wind.energization.eligible" (quote EligibleForGridEnergization) (semanticExpression ∷ []) (unarySuffix "is eligible for grid energization")
∷ predicate-rule "wind.blade.defect" (quote OpenBladeDefect) (semanticExpression ∷ []) (unarySuffix "has an open blade-defect record")
∷ predicate-rule "wind.repair.pending" (quote RepairEvidencePending) (semanticExpression ∷ []) (unarySuffix "still has repair evidence pending")
∷ predicate-rule "wind.energization.blocked" (quote GridEnergizationBlocked) (semanticExpression ∷ []) (unarySuffix "remains blocked from grid energization")
∷ [] ) [] [] [] owlMoreFuel
pharmaIdentityExplanation = explainNameCompact owlMoreDomain serializedPackIdentityFromKey
pharmaRecallChainExplanation = explainNameCompact owlMoreDomain batchRecallPropagatesToPack
pharmaQuarantineExplanation = explainNameCompact owlMoreDomain distributedRecalledPackRequiresQuarantineDispatch
pharmaRemovalExplanation = explainNameCompact owlMoreDomain recalledPackRequiresWholesaleRemoval
windInspectionExplanation = explainNameCompact owlMoreDomain currentCertificateEstablishesInspection
windEnergizationExplanation = explainNameCompact owlMoreDomain reviewedTurbineEligibleForEnergization
windDefectHoldExplanation = explainNameCompact owlMoreDomain openDefectBlocksEnergization
pharmaIdentityText : Explanation.text pharmaIdentityExplanation ≡ "For every serialized medicine pack installed and every serialized medicine pack inventoryRecord, if installed is registered as a saleable medicine pack, inventoryRecord is registered as a saleable medicine pack, and installed has the same product-code-and-serial key as inventoryRecord, then installed denotes the same serialized saleable pack as inventoryRecord."
pharmaIdentityText = refl
pharmaRecallChainText : Explanation.text pharmaRecallChainExplanation ≡ "For every serialized medicine pack pack, every production batch lot, and every market recall recall, if pack belongs to lot and lot is included in recall, then pack is affected by recall."
pharmaRecallChainText = refl
pharmaQuarantineText : Explanation.text pharmaQuarantineExplanation ≡ "For every serialized medicine pack pack and every market recall recall, if pack is affected by recall and pack has already been distributed to market, then pack requires a quarantine instruction to be dispatched."
pharmaQuarantineText = refl
pharmaRemovalText : Explanation.text pharmaRemovalExplanation ≡ "For every serialized medicine pack pack and every market recall recall, if pack is affected by recall and pack requires a quarantine instruction to be dispatched, then pack requires removal from wholesale distribution."
pharmaRemovalText = refl
windInspectionText : Explanation.text windInspectionExplanation ≡ "For every inspection certificate certificate and every offshore wind-turbine asset turbine, if certificate covers turbine and certificate is within its reviewed validity period, then turbine has a current inspection on record."
windInspectionText = refl
windEnergizationText : Explanation.text windEnergizationExplanation ≡ "For every authorized grid engineer engineer and every offshore wind-turbine asset turbine, if turbine has a current inspection on record, turbine has reviewed grid-protection settings, and engineer is authorized to release turbine, then turbine is eligible for grid energization."
windEnergizationText = refl
windDefectHoldText : Explanation.text windDefectHoldExplanation ≡ "For every offshore wind-turbine asset turbine, if turbine has an open blade-defect record and turbine still has repair evidence pending, then turbine remains blocked from grid energization."
windDefectHoldText = refl
liveOWLPropertyChain liveOWLSomeValues liveOWLHasKey : Name
liveOWLPropertyChain = quote OWL.objectPropertyChain₂Intro
liveOWLSomeValues = quote OWL.objectSomeIntro
liveOWLHasKey = quote OWL.hasKeyApply