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

module SemanticExplanation.Industry.DiscourseProfiles where

open import Agda.Builtin.List using ([] ; _∷_)
open import SemanticExplanation

-- These profiles are deliberately small and auditable.  Their keys are the
-- stable semantic-rule IDs emitted into PropIR, never printed Agda names.

batchReactorProfile : DiscourseProfile
batchReactorProfile =
  discourse-profile
    "batch-reactor-release"
    "batch-release authorization basis"
    "Supporting process evidence"
    "Batch-release decision"
    ( statement-label
        "reactor.instrument.pressure-below-release-threshold"
        "Dual-transmitter release-threshold evidence"
    ∷ statement-label
        "reactor.permission.product-discharge"
        "Product-discharge authorization"
    ∷ [] )
    (entity-referent "reactor.entity.state" "the release candidate" ∷ [])

railMovementProfile : DiscourseProfile
railMovementProfile =
  discourse-profile
    "rail-protected-movement"
    "protected-movement authority basis"
    "Supporting route evidence"
    "Movement-authority decision"
    ( statement-label "rail.barriers.down" "Physical barrier proof"
    ∷ statement-label "rail.road.clear" "Conflict-zone clearance"
    ∷ statement-label "rail.movement.authorized" "Protected-movement authority"
    ∷ [] )
    (entity-referent "rail.entity.movement" "the movement" ∷ [])

coldChainProfile : DiscourseProfile
coldChainProfile =
  discourse-profile
    "cold-chain-disposition"
    "distribution-release disposition basis"
    "Supporting quality evidence"
    "Distribution disposition"
    ( statement-label "cold.quarantine" "Controlled-hold status"
    ∷ statement-label "cold.stability.acceptable" "Stability-impact assessment"
    ∷ statement-label "cold.quality.review" "Quality-unit approval"
    ∷ statement-label "cold.release.eligible" "Distribution-release disposition"
    ∷ [] )
    (entity-referent "cold.entity.shipment" "the consignment" ∷ [])

aircraftMroProfile : DiscourseProfile
aircraftMroProfile =
  discourse-profile
    "aircraft-mro-release"
    "return-to-service release basis"
    "Supporting maintenance evidence"
    "Return-to-service disposition"
    ( statement-label
        "mro.property.traceable-inspection" "Traceable maintenance record"
    ∷ statement-label
        "mro.restriction.required-borescope" "Mandatory borescope evidence"
    ∷ statement-label
        "mro.property.release-authorization" "Engineer release authorization"
    ∷ statement-label
        "mro.decision.return-to-service" "Return-to-service disposition"
    ∷ [] )
    ( entity-referent "mro.entity.engineer" "the certifying engineer"
    ∷ entity-referent "mro.entity.engine-module" "the engine module"
    ∷ [] )

medicineRecallProfile : DiscourseProfile
medicineRecallProfile =
  discourse-profile
    "serialized-medicine-recall"
    "serialized-pack recall entailment basis"
    "Supporting recall assertion"
    "Recall consequence"
    ( statement-label "pharma.pack.batch" "Pack-to-batch traceability"
    ∷ statement-label "pharma.batch.recall" "Recall-scope assertion"
    ∷ statement-label "pharma.pack.recall" "Serialized-pack recall consequence"
    ∷ [] )
    ( entity-referent "pharma.entity.pack" "the pack"
    ∷ entity-referent "pharma.entity.batch" "the batch"
    ∷ entity-referent "pharma.entity.recall" "the recall"
    ∷ [] )

windEnergizationProfile : DiscourseProfile
windEnergizationProfile =
  discourse-profile
    "offshore-wind-energization"
    "grid-energization release basis"
    "Supporting asset evidence"
    "Grid-energization disposition"
    ( statement-label "wind.inspection.current" "Current inspection evidence"
    ∷ statement-label "wind.protection.reviewed" "Grid-protection review"
    ∷ statement-label "wind.engineer.authorized" "Engineer release authority"
    ∷ statement-label
        "wind.energization.eligible" "Grid-energization disposition"
    ∷ [] )
    ( entity-referent "wind.entity.engineer" "the engineer"
    ∷ entity-referent "wind.entity.turbine" "the turbine"
    ∷ [] )

motorPermitProfile : DiscourseProfile
motorPermitProfile =
  discourse-profile
    "redundant-motor-permit"
    "motor-permit interlock proof basis"
    "Supporting sampled condition"
    "Motor-permit output"
    ( statement-label
        "spartan.industry.predicate.guard-closed" "Guard interlock input"
    ∷ statement-label
        "spartan.industry.predicate.estop-healthy" "E-stop safety-loop input"
    ∷ statement-label
        "spartan.industry.predicate.restart-present" "Operator restart demand"
    ∷ statement-label
        "spartan.industry.predicate.valid-rising-update"
        "Checked rising-edge transition"
    ∷ statement-label
        "spartan.industry.predicate.both-permits-high" "Motor-permit output"
    ∷ [] )
    ( entity-referent
        "spartan.industry.entity.motor-cycle" "the recorded cycle"
    ∷ [] )

burnerIgnitionProfile : DiscourseProfile
burnerIgnitionProfile =
  discourse-profile
    "burner-ignition-permissive"
    "burner ignition-permissive proof basis"
    "Supporting burner interlock"
    "Ignition-sequence output"
    ( statement-label "burner.purge.complete" "Purge completion permissive"
    ∷ statement-label "burner.furnace.clear" "Furnace-clear permissive"
    ∷ statement-label "burner.valves.closed" "Fuel-valve closure proof"
    ∷ statement-label "burner.ignition.enabled" "Ignition-sequence output"
    ∷ [] )
    (entity-referent "burner.entity.sample" "the burner sample" ∷ [])

pumpStartProfile : DiscourseProfile
pumpStartProfile =
  discourse-profile
    "three-channel-pump-start"
    "drainage-pump start-permit proof basis"
    "Supporting voter condition"
    "Pump-start output"
    ( statement-label "pump.vote.confirmed" "Two-out-of-three demand vote"
    ∷ statement-label "pump.drive.available" "Pump-drive availability"
    ∷ statement-label "pump.start.permitted" "Pump-start output"
    ∷ [] )
    (entity-referent "pump.entity.sample" "the pump-demand sample" ∷ [])