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

module Spartan6.Validation.PortSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

open import Agda.Builtin.String using (primStringEquality)
open import Cubical.Data.Nat using (_≡ᵇ_)
open import Cubical.Data.Bool.Properties using (false≢true)
open import Cubical.Foundations.Path using (inspect; [_]ᵢ)
import Cubical.Data.Empty as Empty

private
  variable
    ℓ : Level

-- Agda's builtin String equality is executable, but this library exposes no
-- safe reflection principle turning a successful comparison into a String
-- path.  CanonicalPortShape therefore records precisely that Boolean witness,
-- while reflecting both natural-number comparisons to propositional paths.

record CanonicalPortShape
  (specification : Architecture.PortSpecification)
  (port : Raw.RawPort)
  : Type₀ where
  constructor canonicalPortShape
  field
    canonicalNameTest :
      primStringEquality
        (Raw.rawPortName port)
        (Architecture.canonicalPortName specification)
      ≡ true

    declaredWidthCanonical :
      Raw.rawPortWidth port
      ≡ Architecture.canonicalPortWidth specification

    connectionCountCanonical :
      lengthList (Raw.rawPortConnections port)
      ≡ Architecture.canonicalPortWidth specification

open CanonicalPortShape public

emptyList? : ∀ {A : Type ℓ} → List A → Bool
emptyList? []ᴸ = true
emptyList? (item ∷ᴸ items) = false

nonempty≢empty : ∀ {A : Type ℓ} {item : A} {items}
  → item ∷ᴸ items ≡ []ᴸ
  → Empty.⊥
nonempty≢empty path = false≢true (cong emptyList? path)

nat-equality-reflexive : ∀ number → (number ≡ᵇ number) ≡ true
nat-equality-reflexive zero = refl
nat-equality-reflexive (suc number) = nat-equality-reflexive number

nat-equality-sound : ∀ {left right}
  → (left ≡ᵇ right) ≡ true
  → left ≡ right
nat-equality-sound {zero} {zero} result = refl
nat-equality-sound {zero} {suc right} result =
  Empty.rec (false≢true result)
nat-equality-sound {suc left} {zero} result =
  Empty.rec (false≢true result)
nat-equality-sound {suc left} {suc right} result =
  cong suc (nat-equality-sound result)

nat-equality-complete : ∀ {left right}
  → left ≡ right
  → (left ≡ᵇ right) ≡ true
nat-equality-complete {left} equality =
  subst
    (λ right → (left ≡ᵇ right) ≡ true)
    equality
    (nat-equality-reflexive left)

-- Empty shape diagnostics imply all three canonical shape obligations.

portShapeDiagnostics-sound : ∀ specification port
  → Validation.portShapeDiagnostics specification port ≡ []ᴸ
  → CanonicalPortShape specification port
portShapeDiagnostics-sound
  (Architecture.portSpecification expected-name expected-width)
  (Raw.rawPort name direction declared-width connections)
  result
  with primStringEquality name expected-name
     | inspect (λ candidate → primStringEquality candidate expected-name) name
... | false | [ name-test ]ᵢ =
  Empty.rec (nonempty≢empty result)
... | true | [ name-test ]ᵢ
  with declared-width ≡ᵇ expected-width
     | inspect (λ width → width ≡ᵇ expected-width) declared-width
...   | false | [ width-test ]ᵢ =
  Empty.rec (nonempty≢empty result)
...   | true | [ width-test ]ᵢ
  with lengthList connections ≡ᵇ expected-width
     | inspect
         (λ count → count ≡ᵇ expected-width)
         (lengthList connections)
...     | false | [ count-test ]ᵢ =
  Empty.rec (nonempty≢empty result)
...     | true | [ count-test ]ᵢ =
  canonicalPortShape
    name-test
    (nat-equality-sound width-test)
    (nat-equality-sound count-test)

-- Conversely, a canonical shape makes each executable diagnostic branch
-- empty.  Together with soundness, this exactly characterizes successful
-- portShapeDiagnostics.

portShapeDiagnostics-complete : ∀ {specification port}
  → CanonicalPortShape specification port
  → Validation.portShapeDiagnostics specification port ≡ []ᴸ
portShapeDiagnostics-complete
  {specification =
    Architecture.portSpecification expected-name expected-width}
  {port = Raw.rawPort name direction declared-width connections}
  shape
  with primStringEquality name expected-name
     | inspect (λ candidate → primStringEquality candidate expected-name) name
... | false | [ name-test ]ᵢ =
  Empty.rec
    (false≢true (sym name-test ∙ canonicalNameTest shape))
... | true | [ name-test ]ᵢ
  with declared-width ≡ᵇ expected-width
     | inspect (λ width → width ≡ᵇ expected-width) declared-width
...   | false | [ width-test ]ᵢ =
  Empty.rec
    (false≢true
      (sym width-test
       ∙ nat-equality-complete (declaredWidthCanonical shape)))
...   | true | [ width-test ]ᵢ
  with lengthList connections ≡ᵇ expected-width
     | inspect
         (λ count → count ≡ᵇ expected-width)
         (lengthList connections)
...     | false | [ count-test ]ᵢ =
  Empty.rec
    (false≢true
      (sym count-test
       ∙ nat-equality-complete (connectionCountCanonical shape)))
...     | true | [ count-test ]ᵢ = refl

-- Named projections avoid requiring clients to unpack the characterization
-- merely to use one successful validation fact.

portShapeDiagnostics-name : ∀ {specification port}
  → Validation.portShapeDiagnostics specification port ≡ []ᴸ
  → primStringEquality
      (Raw.rawPortName port)
      (Architecture.canonicalPortName specification)
    ≡ true
portShapeDiagnostics-name {specification} {port} result =
  canonicalNameTest
    (portShapeDiagnostics-sound specification port result)

portShapeDiagnostics-declared-width : ∀ {specification port}
  → Validation.portShapeDiagnostics specification port ≡ []ᴸ
  → Raw.rawPortWidth port
    ≡ Architecture.canonicalPortWidth specification
portShapeDiagnostics-declared-width {specification} {port} result =
  declaredWidthCanonical
    (portShapeDiagnostics-sound specification port result)

portShapeDiagnostics-connection-count : ∀ {specification port}
  → Validation.portShapeDiagnostics specification port ≡ []ᴸ
  → lengthList (Raw.rawPortConnections port)
    ≡ Architecture.canonicalPortWidth specification
portShapeDiagnostics-connection-count {specification} {port} result =
  connectionCountCanonical
    (portShapeDiagnostics-sound specification port result)

portShapeDiagnostics-width-coherent : ∀ {specification port}
  → Validation.portShapeDiagnostics specification port ≡ []ᴸ
  → Raw.rawPortWidth port
    ≡ lengthList (Raw.rawPortConnections port)
portShapeDiagnostics-width-coherent {specification} {port} result =
  portShapeDiagnostics-declared-width
    {specification = specification} {port = port} result
  ∙ sym
      (portShapeDiagnostics-connection-count
        {specification = specification} {port = port} result)