{-# OPTIONS --cubical #-}

module SemanticExplanation.TargetShowcase 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.Test.Core
open import SemanticExplanation.Test.ExpandedShowcase
open import SemanticExplanation.Test.Fixtures
open import SemanticExplanation.Test.ExpandedFixtures
open import SemanticExplanation.OWLDirect
open import SemanticExplanation.SpartanDirect

import SM.Basic.Properties as SM
import SMLogic.Examples.Parity as LogicParity
import SMLogic.Examples.Turnstile as Turnstile
import SMLogic.Examples.TrafficLight as TrafficLight
import SMLogic.Temporal.PredicateTransformers as PT
import SMLogic.Temporal.HProp as HProp
import OWL2.DirectSemantics.Lemmas as OWL
import OWL2.Examples.Family.Lemmas as Family
import OWL2.Examples.Countermodels as Countermodels
import Spartan6.Examples.StateDomains as SpartanDomains
import Spartan6.Examples.ToggleEquivalence as SpartanToggle
import Spartan6.Semantics.Invariant as SpartanInvariant
import Spartan6.Semantics.Refinement as SpartanRefinement
import Spartan6.Examples.DuplicatedToggle as DuplicatedToggle
import Spartan6.Examples.GenericSemantics as GenericSemantics

record ShowcaseExample : Set where
  constructor example
  field
    target : String
    sourceDeclaration : Name
    sourceType : String
    adapterFixture : Name
    generatedReading : String
    supportStatus : String

logicExamples : List ShowcaseExample
logicExamples =
  example "cubical-sm / logic" (quote SM.reachableAfter)
    "Reachable M s₀ s → (is : List In) → Reachable M s₀ (runState M s is)"
    (quote logicSlice) (Explanation.text logicExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "cubical-sm / logic" (quote LogicParity.consistentAfterMirrorStep)
    "(s t : Bool × Bool) → Step s t → ConsistentState t"
    (quote logicStepPreservesValidity) (Explanation.text logicValidityExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "cubical-sm / logic" (quote LogicParity.pathConsistent)
    "(π : TemporalPath) → ConsistentState (head π) → (n : ℕ) → ConsistentState (at π n)"
    (quote logicValidityPropagates) (Explanation.text logicPropagationExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "cubical-sm / logic" (quote SM.reachableInvariant)
    "StepInvariant M P → P s₀ → InvariantFrom M s₀ P"
    (quote logicReachabilityTransitive) (Explanation.text logicTransitivityExplanation)
    "checked representative Π/relation fixture"
  ∷ example "cubical-sm / logic" (quote SM.runState-++)
    "runState M s (xs ++ ys) ≡ runState M (runState M s xs) ys"
    (quote logicRunAppend) (Explanation.text logicRunAppendExplanation) "checked run-composition schema fixture"
  ∷ example "cubical-sm / logic" (quote SM.invariantRun)
    "StepInvariant M P → P s → (is : List In) → P (runState M s is)"
    (quote logicInvariantRun) (Explanation.text logicInvariantRunExplanation) "checked invariant schema fixture"
  ∷ example "cubical-sm / logic" (quote SM.reachableInputs)
    "Reachable M s₀ s → Σ[ is ∈ List In ] runState M s₀ is ≡ s"
    (quote logicReachableInputs) (Explanation.text logicReachableInputsExplanation) "checked reachability-witness schema fixture"
  ∷ example "cubical-sm / logic" (quote SM.homRunState)
    "mapState h (runState M s is) ≡ runState N (mapState h s) is"
    (quote logicHomRunState) (Explanation.text logicHomRunStateExplanation) "checked homomorphism schema fixture"
  ∷ example "cubical-sm / logic" (quote SM.homReachable)
    "Reachable M s₀ s → Reachable N (mapState h s₀) (mapState h s)"
    (quote logicHomReachable) (Explanation.text logicHomReachableExplanation) "checked mapped-reachability schema fixture"
  ∷ example "cubical-sm / logic" (quote SM.simulationRunOutputs)
    "s ~ t → (is : List In) → runOutputs M s is ≡ runOutputs N t is"
    (quote logicSimulationOutputs) (Explanation.text logicSimulationOutputsExplanation) "checked simulation-output schema fixture"
  ∷ example "cubical-sm / logic" (quote SM.simulationReachable)
    "s₀ ~ t₀ → Reachable M s₀ s → Σ[ t ] Reachable N t₀ t × s ~ t"
    (quote logicSimulationReachable) (Explanation.text logicSimulationReachableExplanation) "checked simulation-reachability schema fixture"
  ∷ example "cubical-sm / logic" (quote Turnstile.lockedPushLoopDropHead)
    "(n : ℕ) → Locked ≡ head (drop n lockedPushLoop)"
    (quote logicLockedLoop) (Explanation.text logicLockedLoopExplanation) "checked loop/equality schema fixture"
  ∷ example "cubical-sm / logic" (quote TrafficLight.cycleStep)
    "(n : ℕ) → ⟨ Step trafficTemporal (cycleAt n) (cycleAt (suc n)) ⟩"
    (quote logicCycleStep) (Explanation.text logicCycleStepExplanation) "checked temporal-step schema fixture"
  ∷ example "cubical-sm / logic" (quote PT.EXᵀ-monotone)
    "P ≤ Q → EXᵀ M P ≤ EXᵀ M Q"
    (quote logicEXMonotone) (Explanation.text logicEXMonotoneExplanation) "checked existential-next monotonicity fixture"
  ∷ example "cubical-sm / logic" (quote PT.AXᵀ-monotone)
    "P ≤ Q → AXᵀ M P ≤ AXᵀ M Q"
    (quote logicAXMonotone) (Explanation.text logicAXMonotoneExplanation) "checked universal-next monotonicity fixture"
  ∷ example "cubical-sm / logic" (quote HProp.mapᵖ)
    "(⟨ P ⟩ → ⟨ Q ⟩) → ⟨ P ⟩ → ⟨ Q ⟩"
    (quote logicHPropMap) (Explanation.text logicHPropMapExplanation) "checked hProp entailment fixture"
  ∷ []

owlExamples : List ShowcaseExample
owlExamples =
  example "ff-owl" (quote OWL.classSubsumption)
    "SatisfiesAxiom I (subClassOf c d) → evalClass I c x → evalClass I d x"
    (quote OWL.classSubsumption) (Explanation.text classSubsumptionCompact)
    "direct live-type translation · compact/v1"
  ∷ example "ff-owl" (quote OWL.objectSubProperty)
    "SatisfiesAxiom I (subObjectPropertyOf p q) → p x y → q x y"
    (quote owlSubpropertyPropagation) (Explanation.text owlSubpropertyExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "ff-owl" (quote OWL.objectPropertyChain₂Intro)
    "p x y → q y z → propertyChain p q x z"
    (quote owlPropertyChain) (Explanation.text owlChainExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "ff-owl" (quote OWL.subClassTrans)
    "SubClass c d → SubClass d e → SubClass c e"
    (quote OWL.subClassTrans) (Explanation.text subClassTransCompact)
    "direct live-type translation · compact/v1"
  ∷ example "ff-owl" (quote OWL.subsetTrans)
    "Subset p q → Subset q r → Subset p r"
    (quote owlSubsetTrans) (Explanation.text owlSubsetTransExplanation) "checked subset-transitivity fixture"
  ∷ example "ff-owl" (quote OWL.disjointSym)
    "Disjoint p q → Disjoint q p"
    (quote owlDisjointSym) (Explanation.text owlDisjointSymExplanation) "checked disjointness symmetry fixture"
  ∷ example "ff-owl" (quote OWL.equivalentClassForward)
    "SameExtension (evalClass I c) (evalClass I d) → evalClass I c x → evalClass I d x"
    (quote owlEquivalentForward) (Explanation.text owlEquivalentForwardExplanation) "checked equivalent-class fixture"
  ∷ example "ff-owl" (quote OWL.subObjectPropertyTrans)
    "SubObjectProperty p q → SubObjectProperty q r → SubObjectProperty p r"
    (quote owlSubpropertyTrans) (Explanation.text owlSubpropertyTransExplanation) "checked subproperty-transitivity fixture"
  ∷ example "ff-owl" (quote OWL.sharedObjectPropertyValueIntro)
    "p x z → p y z → SharedObjectPropertyValue I p x y"
    (quote owlSharedValue) (Explanation.text owlSharedValueExplanation) "checked shared-value fixture"
  ∷ example "ff-owl" (quote OWL.hasKeyApply)
    "HasKey c key → c a → c b → SharedKey key a b → ObjectEq a b"
    (quote owlHasKey) (Explanation.text owlHasKeyExplanation) "checked key-identity fixture"
  ∷ example "ff-owl" (quote OWL.objectCardinalityAtMostOneFromUnique)
    "((y z : Object) → Filler x y → Filler x z → ObjectEq y z) → CardinalityAtMost 1 x"
    (quote owlAtMostOne) (Explanation.text owlAtMostOneExplanation) "checked uniqueness/cardinality fixture"
  ∷ example "ff-owl" (quote Family.johnHasSpouseMary)
    "evalObjectProperty familyInterpretation HasSpouse johnObject maryObject"
    (quote owlJohnSpouseMary) (Explanation.text owlJohnSpouseMaryExplanation) "checked named-individual relation fixture"
  ∷ example "ff-owl" (quote Family.johnIsManFromHasWife)
    "evalClass familyInterpretation ManC johnObject"
    (quote owlJohnManFromWife) (Explanation.text owlJohnManFromWifeExplanation) "checked property-domain inference fixture"
  ∷ example "ff-owl" (quote Family.johnHasSomeWife)
    "evalClass familyInterpretation (objectSomeValuesFrom HasWife WomanC) johnObject"
    (quote owlJohnSomeWife) (Explanation.text owlJohnSomeWifeExplanation) "checked existential-restriction fixture"
  ∷ example "ff-owl" (quote Countermodels.openWorldDoesNotEntailAlicePerson)
    "¬ Entails openWorldOntology alicePersonOntology"
    (quote owlOpenWorld) (Explanation.text owlOpenWorldExplanation) "checked open-world non-entailment fixture"
  ∷ example "ff-owl" (quote Countermodels.complementContradictionNoModel)
    "(I : Interpretation CounterSignature ...) → ¬ Model I complementContradictionOntology"
    (quote owlComplementContradiction) (Explanation.text owlComplementExplanation) "checked inconsistency/no-model fixture"
  ∷ []

spartanExamples : List ShowcaseExample
spartanExamples =
  example "ff-spartan6" (quote SpartanDomains.sameClockDomain-sound)
    "(source target : ClockDomain) → sameClockDomain source target ≡ high → source ≡ target"
    (quote SpartanDomains.sameClockDomain-sound)
    (Explanation.text sameClockDomainSoundCompact)
    "direct live-type translation · compact/v1"
  ∷ example "ff-spartan6" (quote SpartanInvariant.run-preserves)
    "Invariant design Property → Property state → Property (run design state samples)"
    (quote spartanTransitionPreservesSafety) (Explanation.text spartanSafetyExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "ff-spartan6" (quote SpartanRefinement.transitionPreserved)
    "Related machineState systemState → Related (machineStep ...) (systemStep ...)"
    (quote spartanSimulationStep) (Explanation.text spartanSimulationExplanation)
    "checked shape-faithful adapter fixture"
  ∷ example "ff-spartan6" (quote SpartanToggle.all-finite-runs-agree)
    "(stimuli : List Stimulus) → run toggle stimuli ≡ run toggleSpecification stimuli"
    (quote spartanSlice) (Explanation.text spartanExplanation)
    "checked representative transition/relation fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.unsupported-cross-domain-is-rejected)
    "checkInteraction noCrossDomainPolicy domainA domainB ≡ nothing"
    (quote spartanRejected) (Explanation.text spartanRejectedExplanation) "checked rejection fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.unsupported-cross-domain-has-no-permission)
    "PermissionFor noCrossDomainPolicy domainA domainB → ⊥"
    (quote spartanNoPermission) (Explanation.text spartanNoPermissionExplanation) "checked permission-failure fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.two-domain-simultaneous-update)
    "stepPair swapPair bothDomains tt (low , high) ≡ (high , low)"
    (quote spartanSimultaneousUpdate) (Explanation.text spartanSimultaneousUpdateExplanation) "checked simultaneous-update fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.one-domain-edge-holds-the-other)
    "stepPair swapPair onlyDomainA tt (low , high) ≡ (high , high)"
    (quote spartanOneDomainHolds) (Explanation.text spartanOneDomainHoldsExplanation) "checked selective-clock fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.pair-default-initialization)
    "decodePairInitial swapPair (nothing , nothing) ≡ just (low , low)"
    (quote spartanDefaultInitialization) (Explanation.text spartanDefaultInitializationExplanation) "checked initialization fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.swap-flattening-preserves-the-two-domain-step)
    "StateRelation swapFlattening (stepPair ...) (flatStep ...)"
    (quote spartanFlattening) (Explanation.text spartanFlatteningExplanation) "checked flattening fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.srl16e-owned-edge-loads-first-stage)
    "readSRL16E (stepResource ... bothDomains ...) address0000 ≡ high"
    (quote spartanOwnedEdge) (Explanation.text spartanOwnedEdgeExplanation) "checked owned-edge fixture"
  ∷ example "ff-spartan6" (quote SpartanDomains.srl16e-foreign-edge-holds)
    "stepResource ... onlyDomainA ... defaultInitialState ≡ defaultInitialState"
    (quote spartanForeignEdge) (Explanation.text spartanForeignEdgeExplanation) "checked foreign-edge fixture"
  ∷ example "ff-spartan6" (quote SpartanToggle.toggle-refines-specification)
    "BehaviorallyEquivalent toggle toggleSpecification"
    (quote spartanBehavior) (Explanation.text spartanBehaviorExplanation) "checked behavioral-equivalence fixture"
  ∷ example "ff-spartan6" (quote SpartanInvariant.initial-run-preserves)
    "Invariant design Property → (samples : List Stimulus) → Property (run design initial samples)"
    (quote spartanInitialRun) (Explanation.text spartanInitialRunExplanation) "checked initial-invariant fixture"
  ∷ example "ff-spartan6" (quote DuplicatedToggle.all-finite-runs-keep-copies-equal)
    "∀ samples → EqualState (run duplicatedToggle initial samples)"
    (quote spartanCopiesEqual) (Explanation.text spartanCopiesEqualExplanation) "checked duplicated-register fixture"
  ∷ example "ff-spartan6" (quote GenericSemantics.singleImplementsDuplicated)
    "Refinement.Implements singleToggle duplicatedSystem"
    (quote spartanImplements) (Explanation.text spartanImplementsExplanation) "checked implementation/refinement fixture"
  ∷ []

allExamples : List ShowcaseExample
allExamples = logicExamples ++ (owlExamples ++ spartanExamples)
  where
  _++_ : List ShowcaseExample → List ShowcaseExample → List ShowcaseExample
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)