{-# OPTIONS --safe --cubical-compatible --no-sized-types --no-guardedness #-}

module SemanticExplanation.Tutorial.IntegerArithmetic where

open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Agda.Builtin.List using (List ; [] ; _∷_)
open import Agda.Builtin.Nat using (Nat)
open import Data.Integer.Base using (ℤ ; _+_ ; _*_ ; _≤_ ; _<_)
open import Data.Integer.Properties using
  (≤-refl ; ≤-trans ; ≤-antisym ; <-≤-trans ; +-monoˡ-≤)
open import SemanticExplanation

------------------------------------------------------------------------
-- The domain declarations are ordinary standard-library integer facts.

integerOrderTransitive
  : (lower middle upper : ℤ)
  → lower ≤ middle
  → middle ≤ upper
  → lower ≤ upper
integerOrderTransitive lower middle upper = ≤-trans

addingSameOffsetPreservesOrder
  : (offset lower upper : ℤ)
  → lower ≤ upper
  → lower + offset ≤ upper + offset
addingSameOffsetPreservesOrder offset lower upper = +-monoˡ-≤ offset

strictThenNonStrictRemainsStrict
  : (lower middle upper : ℤ)
  → lower < middle
  → middle ≤ upper
  → lower < upper
strictThenNonStrictRemainsStrict lower middle upper = <-≤-trans

oppositeBoundsDetermineTheInteger
  : (lower upper : ℤ)
  → lower ≤ upper
  → upper ≤ lower
  → lower ≡ upper
oppositeBoundsDetermineTheInteger lower upper = ≤-antisym

WithinLimit : ℤ → ℤ → Set
WithinLimit value limit = value ≤ limit

boundFlowsThroughReviewedLimit
  : (value reviewedLimit finalLimit : ℤ)
  → value ≤ reviewedLimit
  → WithinLimit reviewedLimit finalLimit
  → WithinLimit value finalLimit
boundFlowsThroughReviewedLimit value reviewedLimit finalLimit = ≤-trans

-- Multiplication is intentionally absent from the first expression-rule set.
multiplicationIsReflexivelyBounded
  : (left right : ℤ) → left * right ≤ left * right
multiplicationIsReflexivelyBounded left right = ≤-refl

------------------------------------------------------------------------
-- The adapter classifies source heads by quoted Name and supplies surfaces.

integerFuel : Nat
integerFuel = 

integerDomain : DomainSpec
integerDomain =
  domain-spec
    "integer-arithmetic-tutorial-v1"
    (entity-rule "integer.entity.value" (quote ℤ) [] "integer" ∷ [])
    ( predicate-rule "integer.order.less-or-equal" (quote _≤_)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "is at most")
    ∷ predicate-rule "integer.order.strict" (quote _<_)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryVerb "is strictly less than")
    ∷ predicate-rule "integer.equality" (quote _≡_)
        ( infrastructureArgument ∷ infrastructureArgument
        ∷ semanticExpression ∷ semanticExpression ∷ [] )
        (equalityPhrase "is equal to")
    ∷ [] )
    ( expression-rule "integer.expression.addition" (quote _+_)
        (semanticExpression ∷ semanticExpression ∷ [])
        (binaryForm "" " plus " "")
    ∷ [] )
    []
    (quote WithinLimit ∷ [])
    integerFuel

integerDiscourse : DiscourseProfile
integerDiscourse =
  discourse-profile
    "integer-order-audit"
    "integer-order proof basis"
    "Order premise"
    "Order conclusion"
    ( statement-label "integer.order.less-or-equal" "Non-strict order evidence"
    ∷ statement-label "integer.order.strict" "Strict order evidence"
    ∷ statement-label "integer.equality" "Integer identity conclusion"
    ∷ [] )
    []

------------------------------------------------------------------------
-- Compile-time runs and literal goldens used by the HTML tutorial.

transitiveExplanation : Explanation
transitiveExplanation =
  explainNameCompact integerDomain integerOrderTransitive

transitiveText
  : Explanation.text transitiveExplanation
  ≡ "For every integer lower, every integer middle, and every integer upper, if lower is at most middle and middle is at most upper, then lower is at most upper."
transitiveText = refl

additionExplanation : Explanation
additionExplanation =
  explainNameCompact integerDomain addingSameOffsetPreservesOrder

additionText
  : Explanation.text additionExplanation
  ≡ "For every integer offset, every integer lower, and every integer upper, if lower is at most upper, then lower plus offset is at most upper plus offset."
additionText = refl

strictExplanation : Explanation
strictExplanation =
  explainNameCompact integerDomain strictThenNonStrictRemainsStrict

strictText
  : Explanation.text strictExplanation
  ≡ "For every integer lower, every integer middle, and every integer upper, if lower is strictly less than middle and middle is at most upper, then lower is strictly less than upper."
strictText = refl

identityExplanation : Explanation
identityExplanation =
  explainNameCompact integerDomain oppositeBoundsDetermineTheInteger

identityText
  : Explanation.text identityExplanation
  ≡ "For every integer lower and every integer upper, if lower is at most upper and upper is at most lower, then lower is equal to upper."
identityText = refl

aliasExplanation : Explanation
aliasExplanation =
  explainNameCompact integerDomain boundFlowsThroughReviewedLimit

aliasText
  : Explanation.text aliasExplanation
  ≡ "For every integer value, every integer reviewedLimit, and every integer finalLimit, if value is at most reviewedLimit and reviewedLimit is at most finalLimit, then value is at most finalLimit."
aliasText = refl

aliasUnfoldingIsAuditable
  : Explanation.provenance aliasExplanation
  ≡ ( ruleUsed "integer.entity.value"
    ∷ ruleUsed "integer.entity.value"
    ∷ ruleUsed "integer.entity.value"
    ∷ ruleUsed "integer.order.less-or-equal"
    ∷ aliasUnfolded (quote WithinLimit)
    ∷ ruleUsed "integer.order.less-or-equal"
    ∷ aliasUnfolded (quote WithinLimit)
    ∷ ruleUsed "integer.order.less-or-equal"
    ∷ [] )
aliasUnfoldingIsAuditable = refl

additionDomainExplanation : Explanation
additionDomainExplanation =
  explainNameDomainEvidence integerDiscourse integerDomain
    addingSameOffsetPreservesOrder

additionDomainText
  : Explanation.text additionDomainExplanation
  ≡ "For every integer offset, every integer lower, and every integer upper, the integer-order proof basis in declaration order is: Non-strict order evidence — lower is at most upper. Non-strict order evidence — lower plus offset is at most upper plus offset."
additionDomainText = refl

additionCandidates : List Explanation
additionCandidates =
  explainNameDomainFamily integerDiscourse integerDomain
    addingSameOffsetPreservesOrder

additionCandidateIds
  : candidateIds additionCandidates
  ≡ ( "canonical/v1" ∷ "compact/v1" ∷ "evidence/v1"
    ∷ "structured/v1" ∷ "domain-evidence/v1" ∷ [] )
additionCandidateIds = refl

multiplicationFailure : FailureTag
multiplicationFailure =
  failureTagForName integerDomain multiplicationIsReflexivelyBounded

multiplicationFailsAtTheUnregisteredExpression
  : multiplicationFailure ≡ unsupportedExpression
multiplicationFailsAtTheUnregisteredExpression = refl