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

module Spartan6.Import.Yosys where

open import Spartan6.Prelude

import FF.Json as JSON
import FF.Json.Native as Native
import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Import.Json as Import
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic

open import Agda.Builtin.Char using (Char; primCharEquality)
open import Agda.Builtin.String
  using (primShowNat; primStringEquality; primStringToList)
open import Cubical.Data.Nat.Base using (_<ᵇ_; _≡ᵇ_)
open import Cubical.Data.Nat.Mod using (quotient_/_; remainder_/_)

parameterProblem : Diagnostic.DiagnosticCode
                 → Import.JsonPath → String → String → String
                 → Diagnostic.Diagnostics
parameterProblem code path expected observed detail =
  Diagnostic.diagnostic code Diagnostic.reject
    (Import.renderPath path) expected observed detail
  ∷ᴸ []ᴸ

directionProblem : Import.JsonPath → String → String
                 → Diagnostic.Diagnostics
directionProblem path expected observed =
  Diagnostic.diagnostic Diagnostic.directionMismatch Diagnostic.reject
    (Import.renderPath path)
    expected observed
    "Yosys port directions must agree exactly with the canonical architecture schema."
  ∷ᴸ []ᴸ

widthProblem : Import.JsonPath → ℕ → ℕ → Diagnostic.Diagnostics
widthProblem path expected observed =
  Diagnostic.diagnostic Diagnostic.widthMismatch Diagnostic.reject
    (Import.renderPath path)
    (primShowNat expected <> " connections")
    (primShowNat observed <> " connections")
    "The connection count must equal the width in Architecture.PortSpecification."
  ∷ᴸ []ᴸ
  where
  open Import using (_<>_)

unknownPortProblem : Import.JsonPath → String → Diagnostic.Diagnostics
unknownPortProblem path name =
  Diagnostic.diagnostic Diagnostic.unknownPort Diagnostic.reject
    (Import.renderPath (Import.fieldAt path name))
    "a port named by the canonical architecture schema"
    name
    "Known-cell schemas are taken only from Architecture input/output port specifications."
  ∷ᴸ []ᴸ

missingDirectionProblem : Import.JsonPath → String → Diagnostic.Diagnostics
missingDirectionProblem path name =
  Diagnostic.diagnostic Diagnostic.missingPort Diagnostic.reject
    (Import.renderPath (Import.fieldAt path name))
    "one direction for every connection"
    "no direction entry"
    "Unknown cells preserve directions exactly and do not invent an inout fallback."
  ∷ᴸ []ᴸ

extraDirectionProblem : Import.JsonPath → String → Diagnostic.Diagnostics
extraDirectionProblem path name =
  Diagnostic.diagnostic Diagnostic.unknownPort Diagnostic.reject
    (Import.renderPath (Import.fieldAt path name))
    "one connection for every direction"
    "a direction without a connection"
    "Unknown-cell port direction and connection key sets must be identical."
  ∷ᴸ []ᴸ

decodeDirection : Import.JsonPath → Import.JsonValue
                → Diagnostic.CheckResult Raw.PortDirection
decodeDirection path value with Import.expectString path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted text =
  if primStringEquality text "input"
  then Diagnostic.accepted Raw.inputPort
  else if primStringEquality text "output"
  then Diagnostic.accepted Raw.outputPort
  else if primStringEquality text "inout"
  then Diagnostic.accepted Raw.bidirectionalPort
  else Diagnostic.rejected
    (directionProblem path "input, output, or inout" text)

decodeKnownDirection : Raw.PortDirection → String
                     → Import.JsonPath → Import.JsonValue
                     → Diagnostic.CheckResult Raw.PortDirection
decodeKnownDirection direction expected path value with
  Import.expectString path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted observed =
  if primStringEquality observed expected
  then Diagnostic.accepted direction
  else Diagnostic.rejected (directionProblem path expected observed)

decodeConnection : Import.JsonPath → Import.JsonValue
                 → Diagnostic.CheckResult Raw.Connection
decodeConnection path (JSON.atom Native.number net-id) =
  Diagnostic.accepted (Raw.net net-id)
decodeConnection path (JSON.atom Native.string text) =
  if primStringEquality text "0"
  then Diagnostic.accepted (Raw.constant low)
  else if primStringEquality text "1"
  then Diagnostic.accepted (Raw.constant high)
  else Diagnostic.rejected
    (parameterProblem Diagnostic.malformedImport path
      "a natural net id or defined constant string 0/1"
      text
      "Constants x and z, uppercase variants, and other strings have no two-valued Raw.Connection representation.")
decodeConnection path value =
  Diagnostic.rejected
    (Import.malformedAt path
      "a natural net id or defined constant string 0/1"
      (Import.jsonShape value)
      "Yosys signal bits must be nets or two-valued constants.")

decodeConnections : Import.JsonPath → Import.JsonValue
                  → Diagnostic.CheckResult (List Raw.Connection)
decodeConnections path value with Import.expectArray path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted values =
  Import.decodeArray decodeConnection path values

decodeFixedConnections : ℕ → Import.JsonPath → Import.JsonValue
                       → Diagnostic.CheckResult (List Raw.Connection)
decodeFixedConnections expected path value with Import.expectArray path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted values with lengthList values ≡ᵇ expected
...   | false = Diagnostic.rejected
        (widthProblem path expected (lengthList values))
...   | true = Import.decodeArray decodeConnection path values

hexDigit : ℕ → String
hexDigit zero = "0"
hexDigit (suc zero) = "1"
hexDigit (suc (suc zero)) = "2"
hexDigit (suc (suc (suc zero))) = "3"
hexDigit (suc (suc (suc (suc zero)))) = "4"
hexDigit (suc (suc (suc (suc (suc zero))))) = "5"
hexDigit (suc (suc (suc (suc (suc (suc zero)))))) = "6"
hexDigit (suc (suc (suc (suc (suc (suc (suc zero))))))) = "7"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = "8"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = "9"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))) = "A"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))) = "B"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))) = "C"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))))) = "D"
hexDigit (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))) = "E"
hexDigit number = "F"

fixedHexAcc : ℕ → ℕ → String → String
fixedHexAcc zero number accumulator = accumulator
fixedHexAcc (suc digits) number accumulator =
  fixedHexAcc digits (quotient number / )
    (hexDigit (remainder number / ) <> accumulator)
  where
  open Import using (_<>_)

fixedHex : ℕ → ℕ → String
fixedHex digits number = fixedHexAcc digits number ""

binaryValueFrom : ℕ → List Char → Maybe ℕ
binaryValueFrom accumulator []ᴸ = just accumulator
binaryValueFrom accumulator (digit ∷ᴸ digits) =
  if primCharEquality digit '0'
  then binaryValueFrom (accumulator · ) digits
  else if primCharEquality digit '1'
  then binaryValueFrom (suc (accumulator · )) digits
  else nothing

binaryValue : String → Maybe ℕ
binaryValue text = binaryValueFrom zero (primStringToList text)

decodeLUTInit : ℕ → ℕ → Import.JsonPath → Import.JsonValue
              → Diagnostic.CheckResult String
decodeLUTInit bit-count digit-count path (JSON.atom Native.string text) =
  if lengthList (primStringToList text) ≡ᵇ bit-count
  then decode-binary (binaryValue text)
  else malformed "The binary text has the wrong width."
  where
  malformed : String → Diagnostic.CheckResult String
  malformed detail =
    Diagnostic.rejected
      (parameterProblem Diagnostic.malformedInitialisation path
        (primShowNat bit-count <> " defined binary digits")
        text
        detail)
    where open Import using (_<>_)

  decode-binary : Maybe ℕ → Diagnostic.CheckResult String
  decode-binary nothing =
    malformed "The LUT INIT string contains a non-binary digit; only 0 and 1 are accepted."
  decode-binary (just number) = Diagnostic.accepted (fixedHex digit-count number)
decodeLUTInit bit-count digit-count path (JSON.atom Native.number number) =
  if number <ᵇ ( ^ bit-count)
  then Diagnostic.accepted (fixedHex digit-count number)
  else Diagnostic.rejected
    (parameterProblem Diagnostic.malformedInitialisation path
      ("a natural number smaller than 2^" <> primShowNat bit-count)
      (primShowNat number)
      "Numeric LUT INIT is interpreted numerically and must fit the complete truth-table width.")
  where open Import using (_<>_)
decodeLUTInit bit-count digit-count path value =
  Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter path
      "a fixed-width binary string or natural number"
      (Import.jsonShape value)
      "Other JSON forms cannot encode a LUT truth table.")

firstDisallowed : List String → Import.ObjectFields → Maybe String
firstDisallowed allowed []ᴸ = nothing
firstDisallowed allowed ((name , value) ∷ᴸ fields) =
  if member name allowed
  then firstDisallowed allowed fields
  else just name
  where
  member : String → List String → Bool
  member candidate []ᴸ = false
  member candidate (name ∷ᴸ names) =
    primStringEquality candidate name or member candidate names

requireOnly : Import.JsonPath → List String → Import.ObjectFields
            → Diagnostic.CheckResult Unit
requireOnly path allowed fields with firstDisallowed allowed fields
... | nothing = Diagnostic.accepted tt
... | just name =
  Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter
      (Import.fieldAt path name)
      "only parameters supported by this selected primitive mode"
      name
      "Unknown parameter names are rejected rather than ignored.")

decodeLUTParameters : ℕ → ℕ → Import.JsonPath → Import.JsonValue
                    → Diagnostic.CheckResult
                        (List Raw.RawParameter × Maybe Bit)
decodeLUTParameters bit-count digit-count path value with
  Import.expectUniqueObject path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted fields with requireOnly path ("INIT" ∷ᴸ []ᴸ) fields
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted unit with
        Import.requiredField path "INIT" fields
...     | Diagnostic.rejected problems = Diagnostic.rejected problems
...     | Diagnostic.accepted init-value with
          decodeLUTInit bit-count digit-count
            (Import.fieldAt path "INIT") init-value
...       | Diagnostic.rejected problems = Diagnostic.rejected problems
...       | Diagnostic.accepted canonical =
          Diagnostic.accepted
            (Raw.rawParameter "INIT" canonical ∷ᴸ []ᴸ , nothing)

decodeRegisterInit : Import.JsonPath → Import.JsonValue
                   → Diagnostic.CheckResult Bit
decodeRegisterInit path (JSON.atom Native.string text) =
  if primStringEquality text "0"
  then Diagnostic.accepted low
  else if primStringEquality text "1"
  then Diagnostic.accepted high
  else Diagnostic.rejected
    (parameterProblem Diagnostic.malformedInitialisation path
      "defined scalar bit 0 or 1" text
      "Register INIT does not admit x, z, wider strings, or alternate spellings.")
decodeRegisterInit path (JSON.atom Native.number zero) =
  Diagnostic.accepted low
decodeRegisterInit path (JSON.atom Native.number (suc zero)) =
  Diagnostic.accepted high
decodeRegisterInit path (JSON.atom Native.number number) =
  Diagnostic.rejected
    (parameterProblem Diagnostic.malformedInitialisation path
      "natural number 0 or 1" (primShowNat number)
      "Register INIT is exactly one defined bit.")
decodeRegisterInit path value =
  Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter path
      "string or natural scalar bit" (Import.jsonShape value)
      "Other JSON forms cannot encode register initial state.")

decodeRegisterParameters : Import.JsonPath → Import.JsonValue
                         → Diagnostic.CheckResult
                             (List Raw.RawParameter × Maybe Bit)
decodeRegisterParameters path value with Import.expectUniqueObject path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted []ᴸ = Diagnostic.accepted ([]ᴸ , nothing)
... | Diagnostic.accepted ((name , init-value) ∷ᴸ []ᴸ) =
  if primStringEquality name "INIT"
  then decode-init (decodeRegisterInit (Import.fieldAt path name) init-value)
  else Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter
      (Import.fieldAt path name) "INIT or no parameters" name
      "FDRE/FDSE expose only scalar INIT in the selected mode.")
  where
  decode-init : Diagnostic.CheckResult Bit
              → Diagnostic.CheckResult (List Raw.RawParameter × Maybe Bit)
  decode-init (Diagnostic.accepted bit) =
    Diagnostic.accepted ([]ᴸ , just bit)
  decode-init (Diagnostic.rejected problems) = Diagnostic.rejected problems
decodeRegisterParameters path value
  | Diagnostic.accepted (first ∷ᴸ second ∷ᴸ rest) =
  Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter path
      "zero parameters or exactly one INIT"
      "multiple parameter fields"
      "Register parameters are not assigned precedence by object order.")

decodeParameterless : Import.JsonPath → Import.JsonValue
                    → Diagnostic.CheckResult
                        (List Raw.RawParameter × Maybe Bit)
decodeParameterless path value with Import.expectUniqueObject path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted []ᴸ = Diagnostic.accepted ([]ᴸ , nothing)
... | Diagnostic.accepted fields =
  Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter path
      "an empty parameter object"
      "one or more parameter fields"
      "The selected digital primitive mode is parameterless.")

unsupportedKnownParameters : Import.JsonPath → Import.JsonValue
                           → Diagnostic.CheckResult
                               (List Raw.RawParameter × Maybe Bit)
unsupportedKnownParameters path value =
  Diagnostic.rejected
    (parameterProblem Diagnostic.unsupportedMode path
      "a parameter mode supported by the Yosys import slice"
      "an unsupported architecture mode"
      "Unsupported architecture kinds are normally retained as unknown primitives.")

decodeKnownParameters : Architecture.PrimitiveKind
                      → Import.JsonPath → Import.JsonValue
                      → Diagnostic.CheckResult
                          (List Raw.RawParameter × Maybe Bit)
decodeKnownParameters Architecture.LUT1 = decodeLUTParameters  
decodeKnownParameters Architecture.LUT2 = decodeLUTParameters  
decodeKnownParameters Architecture.LUT3 = decodeLUTParameters  
decodeKnownParameters Architecture.LUT4 = decodeLUTParameters  
decodeKnownParameters Architecture.LUT5 = decodeLUTParameters  
decodeKnownParameters Architecture.LUT6 = decodeLUTParameters  
decodeKnownParameters Architecture.MUXF7 = decodeParameterless
decodeKnownParameters Architecture.MUXF8 = decodeParameterless
decodeKnownParameters Architecture.CARRY4 = decodeParameterless
decodeKnownParameters Architecture.FDRE = decodeRegisterParameters
decodeKnownParameters Architecture.FDSE = decodeRegisterParameters
decodeKnownParameters Architecture.SRL16E = unsupportedKnownParameters
decodeKnownParameters Architecture.RAM64X1S = unsupportedKnownParameters
decodeKnownParameters Architecture.IBUF = decodeParameterless
decodeKnownParameters Architecture.OBUF = decodeParameterless
decodeKnownParameters Architecture.OBUFDS = decodeParameterless
decodeKnownParameters Architecture.OBUFT = unsupportedKnownParameters
decodeKnownParameters Architecture.BUFG = decodeParameterless
decodeKnownParameters Architecture.BUFGCE = decodeParameterless

supportedKind : String → Maybe Architecture.PrimitiveKind
supportedKind text =
  if primStringEquality text "LUT1" then just Architecture.LUT1 else
  if primStringEquality text "LUT2" then just Architecture.LUT2 else
  if primStringEquality text "LUT3" then just Architecture.LUT3 else
  if primStringEquality text "LUT4" then just Architecture.LUT4 else
  if primStringEquality text "LUT5" then just Architecture.LUT5 else
  if primStringEquality text "LUT6" then just Architecture.LUT6 else
  if primStringEquality text "MUXF7" then just Architecture.MUXF7 else
  if primStringEquality text "MUXF8" then just Architecture.MUXF8 else
  if primStringEquality text "CARRY4" then just Architecture.CARRY4 else
  if primStringEquality text "FDRE" then just Architecture.FDRE else
  if primStringEquality text "FDSE" then just Architecture.FDSE else
  if primStringEquality text "IBUF" then just Architecture.IBUF else
  if primStringEquality text "OBUF" then just Architecture.OBUF else
  if primStringEquality text "OBUFDS" then just Architecture.OBUFDS else
  if primStringEquality text "BUFG" then just Architecture.BUFG else
  if primStringEquality text "BUFGCE" then just Architecture.BUFGCE else
  nothing

specificationNames : List Architecture.PortSpecification → List String
specificationNames = mapList Architecture.canonicalPortName

knownPortNames : Architecture.PrimitiveKind → List String
knownPortNames kind =
  specificationNames (Architecture.inputPortSpecifications kind)
  ++ᴸ specificationNames (Architecture.outputPortSpecifications kind)

schemaKeyCheck : Architecture.PrimitiveKind → Import.JsonPath
               → Import.ObjectFields → Diagnostic.CheckResult Unit
schemaKeyCheck kind path fields with
  firstDisallowed (knownPortNames kind) fields
... | nothing = Diagnostic.accepted tt
... | just name = Diagnostic.rejected (unknownPortProblem path name)

decodeSpecificationPorts : Raw.PortDirection → String
                         → Import.ObjectFields → Import.ObjectFields
                         → Import.JsonPath → Import.JsonPath
                         → List Architecture.PortSpecification
                         → Diagnostic.CheckResult (List Raw.RawPort)
decodeSpecificationPorts direction expected connections directions
  connection-path direction-path []ᴸ = Diagnostic.accepted []ᴸ
decodeSpecificationPorts direction expected connections directions
  connection-path direction-path (specification ∷ᴸ specifications) =
  Import.prependResult decode-port
    (decodeSpecificationPorts direction expected connections directions
      connection-path direction-path specifications)
  where
  name : String
  name = Architecture.canonicalPortName specification

  decode-port : Diagnostic.CheckResult Raw.RawPort
  decode-port with Import.requiredField connection-path name connections
  ... | Diagnostic.rejected problems = Diagnostic.rejected problems
  ... | Diagnostic.accepted connection-value with
        Import.requiredField direction-path name directions
  ...   | Diagnostic.rejected problems = Diagnostic.rejected problems
  ...   | Diagnostic.accepted direction-value with
          Diagnostic.appendResult
            (decodeKnownDirection direction expected
              (Import.fieldAt direction-path name) direction-value)
            (decodeFixedConnections
              (Architecture.canonicalPortWidth specification)
              (Import.fieldAt connection-path name) connection-value)
  ...     | Diagnostic.rejected problems = Diagnostic.rejected problems
  ...     | Diagnostic.accepted (decoded-direction , decoded-connections) =
          Diagnostic.accepted
            (Raw.rawPort name decoded-direction
              (Architecture.canonicalPortWidth specification)
              decoded-connections)

assembleKnownPorts : Diagnostic.CheckResult Unit
                   → Diagnostic.CheckResult Unit
                   → Diagnostic.CheckResult (List Raw.RawPort)
                   → Diagnostic.CheckResult (List Raw.RawPort)
                   → Diagnostic.CheckResult (List Raw.RawPort)
assembleKnownPorts connection-keys direction-keys inputs outputs =
  Diagnostic.mapResult
    (λ combined → fst (snd combined) ++ᴸ snd (snd combined))
    (Diagnostic.appendResult
      (Diagnostic.appendResult connection-keys direction-keys)
      (Diagnostic.appendResult inputs outputs))

decodeKnownPorts : Architecture.PrimitiveKind
                 → Import.JsonPath → Import.JsonValue
                 → Import.JsonPath → Import.JsonValue
                 → Diagnostic.CheckResult (List Raw.RawPort)
decodeKnownPorts kind connection-path connection-value
  direction-path direction-value with
  Import.expectUniqueObject connection-path connection-value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted connections with
      Import.expectUniqueObject direction-path direction-value
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted directions =
      assembleKnownPorts
        (schemaKeyCheck kind connection-path connections)
        (schemaKeyCheck kind direction-path directions)
        (decodeSpecificationPorts Raw.inputPort "input"
          connections directions connection-path direction-path
          (Architecture.inputPortSpecifications kind))
        (decodeSpecificationPorts Raw.outputPort "output"
          connections directions connection-path direction-path
          (Architecture.outputPortSpecifications kind))

coverageCheck : Import.JsonPath → Import.JsonPath
              → Import.ObjectFields → Import.ObjectFields
              → Diagnostic.CheckResult Unit
coverageCheck connection-path direction-path connections directions =
  combine missing extra
  where
  missingProblems : Import.ObjectFields → Diagnostic.Diagnostics
  missingProblems []ᴸ = []ᴸ
  missingProblems ((name , value) ∷ᴸ fields) =
    (if Import.containsField name directions
     then []ᴸ else missingDirectionProblem direction-path name)
    ++ᴸ missingProblems fields

  extraProblems : Import.ObjectFields → Diagnostic.Diagnostics
  extraProblems []ᴸ = []ᴸ
  extraProblems ((name , value) ∷ᴸ fields) =
    (if Import.containsField name connections
     then []ᴸ else extraDirectionProblem direction-path name)
    ++ᴸ extraProblems fields

  missing : Diagnostic.Diagnostics
  missing = missingProblems connections

  extra : Diagnostic.Diagnostics
  extra = extraProblems directions

  combine : Diagnostic.Diagnostics → Diagnostic.Diagnostics
          → Diagnostic.CheckResult Unit
  combine []ᴸ []ᴸ = Diagnostic.accepted tt
  combine first second = Diagnostic.rejected (first ++ᴸ second)

decodeUnknownPort : Import.ObjectFields → Import.JsonPath
                  → Import.JsonPath → Import.JsonPath
                  → String → Import.JsonValue
                  → Diagnostic.CheckResult Raw.RawPort
decodeUnknownPort directions connection-path direction-path entry-path name value with
  Import.requiredField direction-path name directions
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted direction-value with
      Diagnostic.appendResult
        (decodeDirection (Import.fieldAt direction-path name) direction-value)
        (decodeConnections entry-path value)
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted (direction , connections) =
      Diagnostic.accepted
        (Raw.rawPort name direction (lengthList connections) connections)

decodeUnknownPorts : Import.JsonPath → Import.JsonValue
                   → Import.JsonPath → Import.JsonValue
                   → Diagnostic.CheckResult (List Raw.RawPort)
decodeUnknownPorts connection-path connection-value
  direction-path direction-value with
  Import.expectUniqueObject connection-path connection-value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted connections with
      Import.expectUniqueObject direction-path direction-value
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted directions with
        coverageCheck connection-path direction-path connections directions
...     | Diagnostic.rejected problems = Diagnostic.rejected problems
...     | Diagnostic.accepted unit =
        Import.decodeObjectFields
          (decodeUnknownPort directions connection-path direction-path)
          connection-path connections

decodeUnknownParameter : Import.JsonPath → String → Import.JsonValue
                       → Diagnostic.CheckResult Raw.RawParameter
decodeUnknownParameter path name (JSON.atom Native.string value) =
  Diagnostic.accepted (Raw.rawParameter name value)
decodeUnknownParameter path name (JSON.atom Native.number value) =
  Diagnostic.accepted (Raw.rawParameter name (primShowNat value))
decodeUnknownParameter path name value =
  Diagnostic.rejected
    (parameterProblem Diagnostic.illegalParameter path
      "a string or natural parameter value"
      (Import.jsonShape value)
      "Raw.RawParameter preserves supported Yosys scalar parameter text only.")

decodeUnknownParameters : Import.JsonPath → Import.JsonValue
                        → Diagnostic.CheckResult (List Raw.RawParameter)
decodeUnknownParameters path value with Import.expectUniqueObject path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted fields =
  Import.decodeObjectFields decodeUnknownParameter path fields

decodeTopPort : Import.JsonPath → String → Import.JsonValue
              → Diagnostic.CheckResult Raw.RawTopPort
decodeTopPort path name value with Import.expectUniqueObject path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted fields with
      Import.requiredField path "direction" fields
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted direction-value with
        Import.requiredField path "bits" fields
...     | Diagnostic.rejected problems = Diagnostic.rejected problems
...     | Diagnostic.accepted bits-value with
          Diagnostic.appendResult
            (decodeDirection (Import.fieldAt path "direction") direction-value)
            (decodeConnections (Import.fieldAt path "bits") bits-value)
...       | Diagnostic.rejected problems = Diagnostic.rejected problems
...       | Diagnostic.accepted (direction , connections) =
          Diagnostic.accepted
            (Raw.rawTopPort name direction
              (lengthList connections) connections)

decodeCellFields : Import.JsonPath → String → Import.ObjectFields
                 → Diagnostic.CheckResult Raw.RawInstance
decodeCellFields path name fields with Import.requiredField path "type" fields
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted type-value with
      Import.expectString (Import.fieldAt path "type") type-value
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted type-name with
        Import.requiredField path "connections" fields
...     | Diagnostic.rejected problems = Diagnostic.rejected problems
...     | Diagnostic.accepted connection-value with
          Import.requiredField path "port_directions" fields
...       | Diagnostic.rejected problems = Diagnostic.rejected problems
...       | Diagnostic.accepted direction-value with
            Import.requiredField path "parameters" fields
...         | Diagnostic.rejected problems = Diagnostic.rejected problems
...         | Diagnostic.accepted parameter-value with supportedKind type-name
...           | nothing with
              Diagnostic.appendResult
                (decodeUnknownPorts
                  (Import.fieldAt path "connections") connection-value
                  (Import.fieldAt path "port_directions") direction-value)
                (decodeUnknownParameters
                  (Import.fieldAt path "parameters") parameter-value)
...             | Diagnostic.rejected problems = Diagnostic.rejected problems
...             | Diagnostic.accepted (ports , parameters) =
                Diagnostic.accepted
                  (Raw.rawInstance name (Raw.unknownPrimitive type-name)
                    ports parameters nothing)
decodeCellFields path name fields
    | Diagnostic.accepted type-value
    | Diagnostic.accepted type-name
    | Diagnostic.accepted connection-value
    | Diagnostic.accepted direction-value
    | Diagnostic.accepted parameter-value
    | just kind with
      Diagnostic.appendResult
        (decodeKnownPorts kind
          (Import.fieldAt path "connections") connection-value
          (Import.fieldAt path "port_directions") direction-value)
        (decodeKnownParameters kind
          (Import.fieldAt path "parameters") parameter-value)
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted (ports , (parameters , initial-bit)) =
    Diagnostic.accepted
      (Raw.rawInstance name (Raw.knownPrimitive kind)
        ports parameters initial-bit)

decodeCell : Import.JsonPath → String → Import.JsonValue
           → Diagnostic.CheckResult Raw.RawInstance
decodeCell path name value with Import.expectUniqueObject path value
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted fields = decodeCellFields path name fields

decodeModuleFields : Import.JsonPath → Import.ObjectFields
                   → Diagnostic.CheckResult Raw.RawDesign
decodeModuleFields path fields with Import.requiredField path "ports" fields
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted ports-value with
      Import.expectUniqueObject (Import.fieldAt path "ports") ports-value
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted port-fields with
        Import.requiredField path "cells" fields
...     | Diagnostic.rejected problems = Diagnostic.rejected problems
...     | Diagnostic.accepted cells-value with
          Import.expectUniqueObject (Import.fieldAt path "cells") cells-value
...       | Diagnostic.rejected problems = Diagnostic.rejected problems
...       | Diagnostic.accepted cell-fields with
          Diagnostic.appendResult
            (Import.decodeObjectFields decodeTopPort
              (Import.fieldAt path "ports") port-fields)
            (Import.decodeObjectFields decodeCell
              (Import.fieldAt path "cells") cell-fields)
...         | Diagnostic.rejected problems = Diagnostic.rejected problems
...         | Diagnostic.accepted (ports , cells) =
            Diagnostic.accepted (Raw.rawDesign nothing ports cells)

decodeSelectedModule : String → Import.JsonValue
                     → Diagnostic.CheckResult Raw.RawDesign
decodeSelectedModule selected document with
  Import.expectUniqueObject Import.root document
... | Diagnostic.rejected problems = Diagnostic.rejected problems
... | Diagnostic.accepted root-fields with
      Import.requiredField Import.root "modules" root-fields
...   | Diagnostic.rejected problems = Diagnostic.rejected problems
...   | Diagnostic.accepted modules-value with
        Import.expectUniqueObject
          (Import.fieldAt Import.root "modules") modules-value
...     | Diagnostic.rejected problems = Diagnostic.rejected problems
...     | Diagnostic.accepted modules with
          Import.requiredField
            (Import.fieldAt Import.root "modules") selected modules
...       | Diagnostic.rejected problems = Diagnostic.rejected problems
...       | Diagnostic.accepted module-value with
            Import.expectUniqueObject
              (Import.fieldAt
                (Import.fieldAt Import.root "modules") selected)
              module-value
...         | Diagnostic.rejected problems = Diagnostic.rejected problems
...         | Diagnostic.accepted fields =
            decodeModuleFields
              (Import.fieldAt
                (Import.fieldAt Import.root "modules") selected)
              fields

SelectedModuleAccepted : String → Import.JsonValue → Type₀
SelectedModuleAccepted selected document =
  Import.AcceptedResult (decodeSelectedModule selected document)

extractSelectedModule : (selected : String) → (document : Import.JsonValue)
                      → SelectedModuleAccepted selected document
                      → Raw.RawDesign
extractSelectedModule selected document = Import.extractAccepted