{-# OPTIONS --cubical #-}

module SemanticExplanation.SpartanDirect where

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

import Spartan6.Prelude as Spartan
import Spartan6.Examples.StateDomains as Domains
import Cubical.Foundations.Prelude as Cubical

spartanDirectDomain : DomainSpec
spartanDirectDomain =
  domain-spec
    "ff-spartan6-direct-v1"
    (entity-rule "spartan.entity.clock-domain" (quote Domains.ClockDomain) []
      "clock domain" ∷ [])
    ( predicate-rule "core.path-equality" (quote Cubical._≡_)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ semanticExpression ∷ semanticExpression ∷ [] )
        (equalityPhrase "is equal to")
    ∷ [] )
    ( expression-rule "spartan.expression.same-clock-domain"
        (quote Domains.sameClockDomain)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryForm "the clock-domain comparison of " " and " "")
    ∷ expression-rule "spartan.constant.high" (quote Spartan.high) []
        (constantWord "high")
    ∷ [] )
    [] [] 

sameClockDomainSoundDirect : Explanation
sameClockDomainSoundDirect =
  explainName spartanDirectDomain Domains.sameClockDomain-sound

sameClockDomainSoundDirectText
  : Explanation.text sameClockDomainSoundDirect
  ≡ "For every clock domain source, for every clock domain target, if the clock-domain comparison of source and target is equal to high, then source is equal to target."
sameClockDomainSoundDirectText = refl

sameClockDomainSoundCompact : Explanation
sameClockDomainSoundCompact =
  explainNameCompact spartanDirectDomain Domains.sameClockDomain-sound

sameClockDomainSoundCompactText
  : Explanation.text sameClockDomainSoundCompact
  ≡ "For every clock domain source and every clock domain target, if the clock-domain comparison of source and target is equal to high, then source is equal to target."
sameClockDomainSoundCompactText = refl