{-# OPTIONS --cubical #-}

module SemanticExplanation.Industry.Logic 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 Cubical.Foundations.Prelude using (Type ; ℓ-zero ; _,_)
open import Cubical.Data.Sigma.Base using (_×_)
open import SemanticExplanation

import SM.Basic.Base as Basic
import SM.Basic.Properties as Properties

-- A concrete deterministic controller for a jacketed batch reactor.  Product
-- discharge is permitted only after controlled cooling and an independent
-- ambient-pressure confirmation.  An emergency trip isolates the vessel from
-- every operating state.

data ReactorState : Type ℓ-zero where
  idleVented charging reactionHold controlledCooling
    releaseReady emergencyIsolated : ReactorState

data ReactorCommand : Type ℓ-zero where
  beginCharge sealAndStartReaction startControlledCooling
    confirmAmbientPressure confirmProductDischarged emergencyTrip
    : ReactorCommand

data ReactorSignal : Type ℓ-zero where
  commandAccepted commandRejected heatingSteamIsolated
    productDischargeEnabled emergencyIsolationActive : ReactorSignal

reactorStep : ReactorState → ReactorCommand → ReactorState × ReactorSignal
reactorStep idleVented beginCharge = charging , commandAccepted
reactorStep charging sealAndStartReaction = reactionHold , commandAccepted
reactorStep reactionHold startControlledCooling =
  controlledCooling , heatingSteamIsolated
reactorStep controlledCooling confirmAmbientPressure =
  releaseReady , productDischargeEnabled
reactorStep releaseReady confirmProductDischarged =
  idleVented , commandAccepted
reactorStep state emergencyTrip = emergencyIsolated , emergencyIsolationActive
reactorStep state command = state , commandRejected

batchReactor : Basic.Machine ReactorCommand ReactorSignal ℓ-zero
batchReactor .Basic.Machine.State = ReactorState
batchReactor .Basic.Machine.step = reactorStep

-- The envelope has a deliberately explicit witness for every PLC operating
-- state.  In releaseReady the safety case is the verified pressure release;
-- in every other state it is the closed discharge interlock.

data DischargeSafetyEnvelope : ReactorState → Type ℓ-zero where
  idleDischargeLocked : DischargeSafetyEnvelope idleVented
  chargingDischargeLocked : DischargeSafetyEnvelope charging
  reactionDischargeLocked : DischargeSafetyEnvelope reactionHold
  coolingDischargeLocked : DischargeSafetyEnvelope controlledCooling
  verifiedReleaseReady : DischargeSafetyEnvelope releaseReady
  emergencyDischargeLocked : DischargeSafetyEnvelope emergencyIsolated

dischargeSafetyAt : (state : ReactorState) → DischargeSafetyEnvelope state
dischargeSafetyAt idleVented = idleDischargeLocked
dischargeSafetyAt charging = chargingDischargeLocked
dischargeSafetyAt reactionHold = reactionDischargeLocked
dischargeSafetyAt controlledCooling = coolingDischargeLocked
dischargeSafetyAt releaseReady = verifiedReleaseReady
dischargeSafetyAt emergencyIsolated = emergencyDischargeLocked

dischargeSafetyStep : Basic.StepInvariant batchReactor DischargeSafetyEnvelope
dischargeSafetyStep state command previousSafety =
  dischargeSafetyAt (Basic.next batchReactor state command)

singleCommandPreservesDischargeSafety
  : (current : ReactorState)
  → (request : ReactorCommand)
  → DischargeSafetyEnvelope current
  → DischargeSafetyEnvelope (Basic.next batchReactor current request)
singleCommandPreservesDischargeSafety = dischargeSafetyStep

initialDischargeSafety : DischargeSafetyEnvelope idleVented
initialDischargeSafety = idleDischargeLocked

reachableStatesRespectDischargeInterlock
  : ∀ {current}
  → Basic.Reachable batchReactor idleVented current
  → DischargeSafetyEnvelope current
reachableStatesRespectDischargeInterlock =
  Properties.reachableInvariant dischargeSafetyStep initialDischargeSafety

reachableBatchStateIsSafe
  : (current : ReactorState)
  → Basic.Reachable batchReactor idleVented current
  → DischargeSafetyEnvelope current
reachableBatchStateIsSafe current = reachableStatesRespectDischargeInterlock

-- These indexed certificates expose the validated recipe stages in plant
-- language while remaining tied to the concrete transition table above.

data SealedChargeTransition : ReactorState → ReactorState → Type ℓ-zero where
  sealedChargeStartsReaction :
    SealedChargeTransition charging reactionHold

data ControlledCoolingTransition : ReactorState → ReactorState → Type ℓ-zero where
  reactionCompletesIntoCooling :
    ControlledCoolingTransition reactionHold controlledCooling

data PressureReleaseTransition : ReactorState → ReactorState → Type ℓ-zero where
  dualTransmitterRelease :
    PressureReleaseTransition controlledCooling releaseReady

data PressureBelowReleaseThreshold : ReactorState → Type ℓ-zero where
  ambientPressureVerified : PressureBelowReleaseThreshold releaseReady

data ProductDischargeAuthorized : ReactorState → Type ℓ-zero where
  dischargeAuthorized : ProductDischargeAuthorized releaseReady

sealedChargeIsMachineStep
  : Basic.next batchReactor charging sealAndStartReaction ≡ reactionHold
sealedChargeIsMachineStep = refl

coolingIsMachineStep
  : Basic.next batchReactor reactionHold startControlledCooling
  ≡ controlledCooling
coolingIsMachineStep = refl

pressureReleaseIsMachineStep
  : Basic.next batchReactor controlledCooling confirmAmbientPressure
  ≡ releaseReady
pressureReleaseIsMachineStep = refl

pressureVerificationAuthorizesDischarge
  : (releaseCandidate : ReactorState)
  → PressureBelowReleaseThreshold releaseCandidate
  → ProductDischargeAuthorized releaseCandidate
pressureVerificationAuthorizesDischarge .releaseReady ambientPressureVerified =
  dischargeAuthorized

validatedBatchReleaseSequence
  : (sealed hot cooled ready : ReactorState)
  → SealedChargeTransition sealed hot
  → ControlledCoolingTransition hot cooled
  → PressureReleaseTransition cooled ready
  → PressureBelowReleaseThreshold ready
  → ProductDischargeAuthorized ready
validatedBatchReleaseSequence
  .charging .reactionHold .controlledCooling .releaseReady
  sealedChargeStartsReaction reactionCompletesIntoCooling
  dualTransmitterRelease ambientPressureVerified = dischargeAuthorized

industryLogicFuel : Nat
industryLogicFuel = 

batchReactorDomain : DomainSpec
batchReactorDomain =
  domain-spec
    "batch-reactor-safety-plc-v1"
    ( entity-rule "reactor.entity.state" (quote ReactorState) []
        "batch-reactor control state"
    ∷ entity-rule "reactor.entity.command" (quote ReactorCommand) []
        "validated safety-PLC command"
    ∷ [] )
    ( predicate-rule "reactor.safety.discharge-envelope"
        (quote DischargeSafetyEnvelope) (semanticExpression ∷ [])
        (unarySuffix "satisfies the pressure-dependent product-discharge safety envelope")
    ∷ predicate-rule "reactor.execution.reachable"
        (quote Basic.Reachable)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ semanticExpression ∷ [] )
        (unarySuffix "is reachable from the idle, vented vessel under the modeled safety-PLC command set")
    ∷ predicate-rule "reactor.recipe.sealed-charge"
        (quote SealedChargeTransition)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "advances through sealed charging into")
    ∷ predicate-rule "reactor.recipe.controlled-cooling"
        (quote ControlledCoolingTransition)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "completes the controlled cooling phase into")
    ∷ predicate-rule "reactor.recipe.pressure-release"
        (quote PressureReleaseTransition)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "records dual-transmitter ambient-pressure release into")
    ∷ predicate-rule "reactor.instrument.pressure-below-release-threshold"
        (quote PressureBelowReleaseThreshold) (semanticExpression ∷ [])
        (unarySuffix "has a reviewed two-transmitter pressure certificate below the discharge-release threshold")
    ∷ predicate-rule "reactor.permission.product-discharge"
        (quote ProductDischargeAuthorized) (semanticExpression ∷ [])
        (unarySuffix "authorizes the product-discharge valve to open")
    ∷ [] )
    ( expression-rule "reactor.execution.next-state" (quote Basic.next)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ infrastructureArgument ∷ infrastructureArgument
        ∷ semanticExpression ∷ semanticExpression ∷ [] )
        (binaryForm "the control state reached when " " receives " "")
    ∷ [] )
    []
    (quote Basic.StepInvariant ∷ [])
    industryLogicFuel

singleCommandSafetyExplanation : Explanation
singleCommandSafetyExplanation =
  explainNameCompact batchReactorDomain singleCommandPreservesDischargeSafety

reachableInterlockExplanation : Explanation
reachableInterlockExplanation =
  explainNameCompact batchReactorDomain reachableBatchStateIsSafe

pressureReleaseExplanation : Explanation
pressureReleaseExplanation =
  explainNameCompact batchReactorDomain pressureVerificationAuthorizesDischarge

validatedReleaseSequenceExplanation : Explanation
validatedReleaseSequenceExplanation =
  explainNameCompact batchReactorDomain validatedBatchReleaseSequence

-- This separate canonical value exercises the explicit-fuel macro entry point.
singleCommandSafetyWithExplicitFuel : Explanation
singleCommandSafetyWithExplicitFuel =
  explainNameWithFuel industryLogicFuel batchReactorDomain
    singleCommandPreservesDischargeSafety

singleCommandSource reachableInterlockSource pressureReleaseSource
  validatedReleaseSequenceSource : Name
singleCommandSource = quote singleCommandPreservesDischargeSafety
reachableInterlockSource = quote reachableBatchStateIsSafe
pressureReleaseSource = quote pressureVerificationAuthorizesDischarge
validatedReleaseSequenceSource = quote validatedBatchReleaseSequence

singleCommandSafetyText
  : Explanation.text singleCommandSafetyExplanation
  ≡ "For every batch-reactor control state current and every validated safety-PLC command request, if current satisfies the pressure-dependent product-discharge safety envelope, then the control state reached when current receives request satisfies the pressure-dependent product-discharge safety envelope."
singleCommandSafetyText = refl

reachableInterlockText
  : Explanation.text reachableInterlockExplanation
  ≡ "For every batch-reactor control state current, if current is reachable from the idle, vented vessel under the modeled safety-PLC command set, then current satisfies the pressure-dependent product-discharge safety envelope."
reachableInterlockText = refl

pressureReleaseText
  : Explanation.text pressureReleaseExplanation
  ≡ "For every batch-reactor control state releaseCandidate, if releaseCandidate has a reviewed two-transmitter pressure certificate below the discharge-release threshold, then releaseCandidate authorizes the product-discharge valve to open."
pressureReleaseText = refl

validatedReleaseSequenceText
  : Explanation.text validatedReleaseSequenceExplanation
  ≡ "For every batch-reactor control state sealed, every batch-reactor control state hot, every batch-reactor control state cooled, and every batch-reactor control state ready, if sealed advances through sealed charging into hot, hot completes the controlled cooling phase into cooled, cooled records dual-transmitter ambient-pressure release into ready, and ready has a reviewed two-transmitter pressure certificate below the discharge-release threshold, then ready authorizes the product-discharge valve to open."
validatedReleaseSequenceText = refl

singleCommandCandidate
  : Explanation.candidateId singleCommandSafetyExplanation ≡ "compact/v1"
singleCommandCandidate = refl

logicIndustryDomainId
  : Explanation.domainId validatedReleaseSequenceExplanation
  ≡ "batch-reactor-safety-plc-v1"
logicIndustryDomainId = refl

singleCommandProvenance
  : Explanation.provenance singleCommandSafetyExplanation
  ≡ ( ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.entity.command"
    ∷ ruleUsed "reactor.safety.discharge-envelope"
    ∷ ruleUsed "reactor.safety.discharge-envelope"
    ∷ ruleUsed "reactor.execution.next-state"
    ∷ argumentOmitted "reactor.execution.next-state" 
    ∷ argumentOmitted "reactor.execution.next-state" 
    ∷ argumentOmitted "reactor.execution.next-state" 
    ∷ argumentOmitted "reactor.execution.next-state" 
    ∷ argumentOmitted "reactor.execution.next-state" 
    ∷ argumentOmitted "reactor.execution.next-state" 
    ∷ [] )
singleCommandProvenance = refl

reachableInterlockProvenance
  : Explanation.provenance reachableInterlockExplanation
  ≡ ( ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.execution.reachable"
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ argumentOmitted "reactor.execution.reachable" 
    ∷ ruleUsed "reactor.safety.discharge-envelope"
    ∷ [] )
reachableInterlockProvenance = refl

pressureReleaseProvenance
  : Explanation.provenance pressureReleaseExplanation
  ≡ ( ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.instrument.pressure-below-release-threshold"
    ∷ ruleUsed "reactor.permission.product-discharge"
    ∷ [] )
pressureReleaseProvenance = refl

validatedReleaseSequenceProvenance
  : Explanation.provenance validatedReleaseSequenceExplanation
  ≡ ( ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.entity.state"
    ∷ ruleUsed "reactor.recipe.sealed-charge"
    ∷ ruleUsed "reactor.recipe.controlled-cooling"
    ∷ ruleUsed "reactor.recipe.pressure-release"
    ∷ ruleUsed "reactor.instrument.pressure-below-release-threshold"
    ∷ ruleUsed "reactor.permission.product-discharge"
    ∷ [] )
validatedReleaseSequenceProvenance = refl

explicitFuelCandidate
  : Explanation.candidateId singleCommandSafetyWithExplicitFuel
  ≡ "canonical/v1"
explicitFuelCandidate = refl