{-# OPTIONS --cubical #-}

module SemanticExplanation.IndustryShowcase where

open import Agda.Builtin.List using (List ; [] ; _∷_)
open import Agda.Builtin.Reflection using (Name)
open import Agda.Builtin.String using (String)
open import Agda.Primitive using (Set)
open import SemanticExplanation
open import SemanticExplanation.Industry.Logic
open import SemanticExplanation.Industry.LogicMore
open import SemanticExplanation.Industry.OWL
open import SemanticExplanation.Industry.OWLMore
open import SemanticExplanation.Industry.Spartan
open import SemanticExplanation.Industry.SpartanMore

record IndustryExample : Set where
  constructor industry-example
  field
    formalisation : String
    caseStudy : String
    sourceDeclaration : Name
    sourceType : String
    generatedReading : String
    evidenceBoundary : String
    operationalValue : String

logicIndustryExamples : List IndustryExample
logicIndustryExamples =
  industry-example "logic" "Batch-reactor discharge interlock"
    (quote singleCommandPreservesDischargeSafety)
    "(current : ReactorState) → (request : ReactorCommand) → DischargeSafetyEnvelope current → DischargeSafetyEnvelope (next batchReactor current request)"
    (Explanation.text singleCommandSafetyExplanation)
    "direct local application type · live Machine.next"
    "Checks that every modeled PLC command preserves the reviewed discharge envelope."
  ∷ industry-example "logic" "Batch-reactor discharge interlock"
    (quote reachableBatchStateIsSafe)
    "(current : ReactorState) → Reachable batchReactor idleVented current → DischargeSafetyEnvelope current"
    (Explanation.text reachableInterlockExplanation)
    "direct local application type · live reachableInvariant proof"
    "Connects one-step review evidence to every state reachable by the modeled command set."
  ∷ industry-example "logic" "Batch-reactor discharge interlock"
    (quote pressureVerificationAuthorizesDischarge)
    "(current : ReactorState) → PressureBelowReleaseThreshold current → ProductDischargeAuthorized current"
    (Explanation.text pressureReleaseExplanation)
    "direct local certificate rule"
    "Makes the reviewed pressure certificate an explicit premise of valve authorization."
  ∷ industry-example "logic" "Batch-reactor discharge interlock"
    (quote validatedBatchReleaseSequence)
    "(sealed hot cooled ready : ReactorState) → SealedChargeTransition sealed hot → ControlledCoolingTransition hot cooled → PressureReleaseTransition cooled ready → PressureBelowReleaseThreshold ready → ProductDischargeAuthorized ready"
    (Explanation.text validatedReleaseSequenceExplanation)
    "direct indexed application type · live steps linked by refl"
    "Shows the complete reviewed release chain without hiding any stage premise."
  ∷ []

logicMoreIndustryExamples : List IndustryExample
logicMoreIndustryExamples =
  industry-example "logic" "Railway level-crossing movement authority"
    (quote approachDetectionCommandsBarrierClosure)
    "(movement : CrossingMovement) → TrainApproachDetected movement → BarrierClosureCommanded movement"
    (Explanation.text railApproachExplanation)
    "direct local policy type · state-machine command schema"
    "Connects a proved approach detection to the barrier-closing command obligation."
  ∷ industry-example "logic" "Railway level-crossing movement authority"
    (quote provedBarriersProtectRailMovement)
    "(movement : CrossingMovement) → BothBarriersProvedDown movement → RoadConflictZoneClear movement → ProtectedRailMovementAuthorized movement"
    (Explanation.text railProtectionExplanation)
    "direct local policy type · conjunctive movement authority"
    "Makes both barrier and road-zone evidence visible before rail movement authority."
  ∷ industry-example "logic" "Railway level-crossing movement authority"
    (quote occupiedCrossingInhibitsBarrierRelease)
    "(movement : CrossingMovement) → TrainOccupiesCrossing movement → BothBarriersProvedDown movement → BarrierReleaseInhibited movement"
    (Explanation.text railOccupancyExplanation)
    "direct local policy type · interlock invariant schema"
    "States why barrier release remains inhibited while a train occupies the crossing."
  ∷ industry-example "logic" "Railway level-crossing movement authority"
    (quote clearTrainAuthorizesRoadReopening)
    "(movement : CrossingMovement) → RearOfTrainClear movement → RoadConflictZoneClear movement → RoadReopeningAuthorized movement"
    (Explanation.text railReopeningExplanation)
    "direct local policy type · release transition schema"
    "Requires both rear-of-train and road-zone clearance before reopening."
  ∷ industry-example "logic" "Pharmaceutical cold-chain disposition"
    (quote confirmedExcursionRequiresQuarantine)
    "(consignment : ColdChainShipment) → CalibratedLoggerSampleAvailable consignment → TemperatureOutsideQualifiedRange consignment → ShipmentQuarantineRequired consignment"
    (Explanation.text coldQuarantineExplanation)
    "direct local policy type · observation-to-hold rule"
    "Makes calibrated out-of-range evidence the trigger for quality quarantine."
  ∷ industry-example "logic" "Pharmaceutical cold-chain disposition"
    (quote pendingAssessmentBlocksDistribution)
    "(consignment : ColdChainShipment) → ShipmentQuarantineRequired consignment → ExcursionAssessmentPending consignment → DistributionReleaseBlocked consignment"
    (Explanation.text coldHoldExplanation)
    "direct local policy type · hold-preservation rule"
    "Explains why distribution remains blocked while excursion assessment is pending."
  ∷ industry-example "logic" "Pharmaceutical cold-chain disposition"
    (quote reviewedStabilityEvidenceAllowsRelease)
    "(consignment : ColdChainShipment) → ShipmentQuarantineRequired consignment → StabilityImpactAcceptable consignment → QualityUnitReviewComplete consignment → EligibleForDistributionRelease consignment"
    (Explanation.text coldReleaseExplanation)
    "direct local policy type · reviewed release decision"
    "Lists stability and quality-review evidence needed to release a quarantined shipment."
  ∷ industry-example "logic" "Pharmaceutical cold-chain disposition"
    (quote pairedLoggerRecordsEstablishTemperatureTrace)
    "(consignment : ColdChainShipment) → OriginLoggerTracePresent consignment → DestinationLoggerTracePresent consignment → EndToEndTemperatureTraceAvailable consignment"
    (Explanation.text coldTraceExplanation)
    "direct local policy type · traceability join"
    "Combines origin and destination logger records into reviewable end-to-end traceability."
  ∷ []

owlIndustryExamples : List IndustryExample
owlIndustryExamples =
  industry-example "owl" "Turbofan-engine maintenance release"
    (quote maintenanceTraceFromSignedWorkOrder)
    "(certifyingEngineer : LicensedAircraftEngineer) → (workOrder : InspectionWorkOrder) → (engineModule : TurbofanEngineModule) → SignedOff certifyingEngineer workOrder → CoversEngineModule workOrder engineModule → HasTraceableInspection certifyingEngineer engineModule"
    (Explanation.text maintenanceTraceExplanation)
    "direct local application type · OWL property-chain schema"
    "Joins sign-off and work-scope records into traceable engineer-to-module evidence."
  ∷ industry-example "owl" "Turbofan-engine maintenance release"
    (quote requiredInspectionFromConformingOrder)
    "(engineModule : TurbofanEngineModule) → (workOrder : InspectionWorkOrder) → EngineModuleLinkedToOrder engineModule workOrder → IsConformingBorescopeInspection workOrder → HasRequiredBorescopeInspection engineModule"
    (Explanation.text requiredInspectionExplanation)
    "direct local application type · OWL someValuesFrom schema"
    "Exposes the concrete inspection record that witnesses an existential requirement."
  ∷ industry-example "owl" "Turbofan-engine maintenance release"
    (quote returnToServiceEligibility)
    "(certifyingEngineer : LicensedAircraftEngineer) → (engineModule : TurbofanEngineModule) → HasTraceableInspection certifyingEngineer engineModule → HasRequiredBorescopeInspection engineModule → HoldsModuleReleaseAuthorization certifyingEngineer engineModule → EligibleToIssueReturnToServiceRelease certifyingEngineer engineModule"
    (Explanation.text returnToServiceExplanation)
    "direct local application type · audited decision rule"
    "Lists all knowledge and authorization premises behind release eligibility."
  ∷ industry-example "owl" "Turbofan-engine maintenance release"
    (quote returnToServiceFromMaintenanceRecord)
    "(certifyingEngineer : LicensedAircraftEngineer) → (workOrder : InspectionWorkOrder) → (engineModule : TurbofanEngineModule) → SignedOff certifyingEngineer workOrder → CoversEngineModule workOrder engineModule → IsConformingBorescopeInspection workOrder → HoldsModuleReleaseAuthorization certifyingEngineer engineModule → EligibleToIssueReturnToServiceRelease certifyingEngineer engineModule"
    (Explanation.text maintenanceReleaseCaseExplanation)
    "direct composed local type · three OWL-shaped rules"
    "Carries raw maintenance-record evidence through to the operational release judgment."
  ∷ industry-example "owl" "Turbofan-engine maintenance release"
    (quote lifeLimitedPartIdentityFromAssetKey)
    "(installedPart inventoryAlias : SerializedLifeLimitedPart) → IsRegisteredLifeLimitedPart installedPart → IsRegisteredLifeLimitedPart inventoryAlias → SharesPartNumberAndSerial installedPart inventoryAlias → DenotesSameRegisteredAsset installedPart inventoryAlias"
    (Explanation.text lifeLimitedPartIdentityExplanation)
    "direct local application type · OWL HasKey schema"
    "Explains when duplicate inventory names denote one registered life-limited asset."
  ∷ []

owlMoreIndustryExamples : List IndustryExample
owlMoreIndustryExamples =
  industry-example "owl" "Medicine-pack serialization and recall"
    (quote serializedPackIdentityFromKey)
    "(installed inventoryRecord : SerializedMedicinePack) → RegisteredSaleablePack installed → RegisteredSaleablePack inventoryRecord → SharesProductCodeAndSerial installed inventoryRecord → DenotesSameSaleablePack installed inventoryRecord"
    (Explanation.text pharmaIdentityExplanation)
    "direct local application type · OWL HasKey schema"
    "Explains when installed and inventory records denote one serialized saleable pack."
  ∷ industry-example "owl" "Medicine-pack serialization and recall"
    (quote batchRecallPropagatesToPack)
    "(pack : SerializedMedicinePack) → (lot : ProductionBatch) → (recall : MarketRecall) → PackBelongsToBatch pack lot → BatchIncludedInRecall lot recall → PackAffectedByRecall pack recall"
    (Explanation.text pharmaRecallChainExplanation)
    "direct local application type · OWL property-chain schema"
    "Propagates batch-level recall scope to each serialized pack in that batch."
  ∷ industry-example "owl" "Medicine-pack serialization and recall"
    (quote distributedRecalledPackRequiresQuarantineDispatch)
    "(pack : SerializedMedicinePack) → (recall : MarketRecall) → PackAffectedByRecall pack recall → PackDistributedToMarket pack → QuarantineDispatchRequired pack"
    (Explanation.text pharmaQuarantineExplanation)
    "direct local application type · operational recall rule"
    "Separates recall membership from the extra distributed-state evidence requiring dispatch."
  ∷ industry-example "owl" "Medicine-pack serialization and recall"
    (quote recalledPackRequiresWholesaleRemoval)
    "(pack : SerializedMedicinePack) → (recall : MarketRecall) → PackAffectedByRecall pack recall → QuarantineDispatchRequired pack → WholesaleRemovalRequired pack"
    (Explanation.text pharmaRemovalExplanation)
    "direct local application type · composed recall action"
    "Carries recalled-pack and quarantine evidence into wholesale removal."
  ∷ industry-example "owl" "Offshore wind-turbine energization knowledge"
    (quote currentCertificateEstablishesInspection)
    "(certificate : InspectionCertificate) → (turbine : OffshoreWindTurbine) → CertificateCoversTurbine certificate turbine → InspectionCertificateCurrent certificate → TurbineHasCurrentInspection turbine"
    (Explanation.text windInspectionExplanation)
    "direct local application type · OWL someValuesFrom schema"
    "Exposes the current certificate that witnesses inspection status."
  ∷ industry-example "owl" "Offshore wind-turbine energization knowledge"
    (quote reviewedTurbineEligibleForEnergization)
    "(engineer : AuthorizedGridEngineer) → (turbine : OffshoreWindTurbine) → TurbineHasCurrentInspection turbine → ProtectionSettingsReviewed turbine → EngineerAuthorizedForTurbine engineer turbine → EligibleForGridEnergization turbine"
    (Explanation.text windEnergizationExplanation)
    "direct local application type · audited eligibility rule"
    "Lists inspection, protection, and authorization knowledge behind energization eligibility."
  ∷ industry-example "owl" "Offshore wind-turbine energization knowledge"
    (quote openDefectBlocksEnergization)
    "(turbine : OffshoreWindTurbine) → OpenBladeDefect turbine → RepairEvidencePending turbine → GridEnergizationBlocked turbine"
    (Explanation.text windDefectHoldExplanation)
    "direct local application type · positive blocking evidence"
    "Uses explicit defect and pending-repair facts instead of treating missing approval as negation."
  ∷ []

spartanIndustryExamples : List IndustryExample
spartanIndustryExamples =
  industry-example "spartan" "Redundant motor-permit interlock"
    (quote allAuditedControlSequencesPreserveRedundancy)
    "(trace : AuditedControlSequence) → RedundantChannelsRemainSynchronized trace"
    (Explanation.text finiteRunExplanation)
    "direct local application type · live Design run/invariant proof"
    "Checks redundant permit-bit agreement in the final state of every sampled sequence."
  ∷ industry-example "spartan" "Redundant motor-permit interlock"
    (quote healthyRestartEnergizesBothMotorPermitChannels)
    "(event : RecordedMotorControlCycle) → PerimeterGuardDoorIsClosed event → EmergencyStopSafetyLoopIsHealthy event → RestartCommandIsPresent event → RecordedRisingEdgeUpdateIsValid event → BothMotorPermitChannelsAreEnergized event"
    (Explanation.text healthyRestartExplanation)
    "direct local application type · live Transition computation"
    "Makes all four sampled permissive conditions visible before both permit bits go high."
  ∷ industry-example "spartan" "Redundant motor-permit interlock"
    (quote emergencyStopTripDropsBothMotorPermitChannels)
    "(event : RecordedMotorControlCycle) → EmergencyStopSafetyLoopIsTripped event → RecordedRisingEdgeUpdateIsValid event → BothMotorPermitChannelsAreDeEnergized event"
    (Explanation.text emergencyStopTripExplanation)
    "direct local application type · live Transition computation"
    "Shows the modeled rising-edge result of a sampled emergency-stop trip."
  ∷ []

spartanMoreIndustryExamples : List IndustryExample
spartanMoreIndustryExamples =
  industry-example "spartan" "Industrial burner-management permissives"
    (quote verifiedPurgeAllowsIgnition)
    "(cycle : BurnerManagementSample) → PurgeCycleComplete cycle → FurnaceProvedClear cycle → FuelValvesProvedClosed cycle → IgnitionSequenceEnabled cycle"
    (Explanation.text burnerIgnitionExplanation)
    "direct local application type · proved Boolean permissive"
    "Requires all three sampled purge permissives before the ignition bit may go high."
  ∷ industry-example "spartan" "Industrial burner-management permissives"
    (quote incompletePurgeBlocksIgnition)
    "(cycle : BurnerManagementSample) → PurgeCycleIncomplete cycle → IgnitionSequenceBlocked cycle"
    (Explanation.text burnerPurgeBlockExplanation)
    "direct local application type · proved Boolean blocking path"
    "Shows that an incomplete purge alone forces the modeled ignition permit low."
  ∷ industry-example "spartan" "Industrial burner-management permissives"
    (quote establishedFlameEnablesFuelTrain)
    "(cycle : BurnerManagementSample) → MainFlameEstablished cycle → BurnerSafetyLoopHealthy cycle → FuelTrainEnabled cycle"
    (Explanation.text burnerFlamePermitExplanation)
    "direct local application type · proved Boolean fuel permit"
    "Makes flame and safety-loop evidence jointly necessary for the modeled fuel permit."
  ∷ industry-example "spartan" "Industrial burner-management permissives"
    (quote flameLossDropsFuelTrain)
    "(cycle : BurnerManagementSample) → MainFlameLost cycle → FuelTrainDisabled cycle"
    (Explanation.text burnerFlameTripExplanation)
    "direct local application type · proved Boolean trip path"
    "Checks the digital fuel-permit result of a sampled lost-flame input."
  ∷ industry-example "spartan" "Three-channel high-water pump voter"
    (quote channelsABConfirmHighWater)
    "(sample : PumpDemandSample) → ChannelAReportsHighWater sample → ChannelBReportsHighWater sample → TwoOfThreeHighWaterDemand sample"
    (Explanation.text pumpABVoteExplanation)
    "direct local application type · proved two-out-of-three Boolean vote"
    "Checks the A+B majority path independently of channel C."
  ∷ industry-example "spartan" "Three-channel high-water pump voter"
    (quote channelsACConfirmHighWater)
    "(sample : PumpDemandSample) → ChannelAReportsHighWater sample → ChannelCReportsHighWater sample → TwoOfThreeHighWaterDemand sample"
    (Explanation.text pumpACVoteExplanation)
    "direct local application type · proved two-out-of-three Boolean vote"
    "Checks the A+C majority path for both possible channel-B values."
  ∷ industry-example "spartan" "Three-channel high-water pump voter"
    (quote channelsBCConfirmHighWater)
    "(sample : PumpDemandSample) → ChannelBReportsHighWater sample → ChannelCReportsHighWater sample → TwoOfThreeHighWaterDemand sample"
    (Explanation.text pumpBCVoteExplanation)
    "direct local application type · proved two-out-of-three Boolean vote"
    "Checks the B+C majority path for both possible channel-A values."
  ∷ industry-example "spartan" "Three-channel high-water pump voter"
    (quote confirmedDemandPermitsPumpStart)
    "(sample : PumpDemandSample) → TwoOfThreeHighWaterDemand sample → PumpDriveAvailable sample → DrainagePumpStartPermitted sample"
    (Explanation.text pumpStartExplanation)
    "direct local application type · proved Boolean output gate"
    "Requires both voted demand and drive availability before asserting pump start."
  ∷ industry-example "spartan" "Three-channel high-water pump voter"
    (quote channelDisagreementRequiresDiagnostic)
    "(sample : PumpDemandSample) → ChannelDisagreementRecorded sample → InstrumentDiagnosticRequired sample"
    (Explanation.text pumpDiagnosticExplanation)
    "direct local application type · diagnostic policy schema"
    "Turns explicit channel-disagreement evidence into a maintenance review obligation."
  ∷ []

allIndustryExamples : List IndustryExample
allIndustryExamples =
  logicIndustryExamples ++I
    (logicMoreIndustryExamples ++I
    (owlIndustryExamples ++I
    (owlMoreIndustryExamples ++I
    (spartanIndustryExamples ++I spartanMoreIndustryExamples))))
  where
  _++I_ : ∀ {a} {A : Set a} → List A → List A → List A
  [] ++I ys = ys
  (x ∷ xs) ++I ys = x ∷ (xs ++I ys)