module Compiler.LanguageEdition

family LanguageEdition : Type 0
constructor Alpha2026
constructor Alpha2027

end-family

family LanguageEditionDecodeResult : Type 0
constructor LanguageEditionDecoded
field unrestricted decodedLanguageEdition : (family LanguageEdition)
constructor LanguageEditionRejected

end-family

def languageEditionFailureCode =
  (byte-to-nat (byte 88))

-- The driver protocol requires the exact edition name, without a newline.
def languageEditionName =
  (lambda unrestricted edition : (family LanguageEdition) .
    (eliminate
      LanguageEdition
      (lambda unrestricted current : (family LanguageEdition) . Bytes)
      edition
      (branch Alpha2026 . b"alpha-2026")
      (branch Alpha2027 . b"alpha-2027")))

def decodeLanguageEdition =
  (lambda unrestricted name : Bytes .
    (nat-eliminate
      (lambda unrestricted matched : Nat . (family LanguageEditionDecodeResult))
      (nat-eliminate
        (lambda unrestricted matched : Nat . (family LanguageEditionDecodeResult))
        (constructor LanguageEditionDecodeResult LanguageEditionRejected)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family LanguageEditionDecodeResult) .
            (constructor
              LanguageEditionDecodeResult
              LanguageEditionDecoded
              (constructor LanguageEdition Alpha2027))))
        (bytes-equal name (languageEditionName (constructor LanguageEdition Alpha2027))))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family LanguageEditionDecodeResult) .
          (constructor
            LanguageEditionDecodeResult
            LanguageEditionDecoded
            (constructor LanguageEdition Alpha2026))))
      (bytes-equal name (languageEditionName (constructor LanguageEdition Alpha2026)))))

-- Existing checkpoint envelopes already validate source identity. Bind the
-- selected edition into that identity before either save or restore. The fixed
-- domain and fixed-width edition name distinguish this from legacy source-only
-- hashes without introducing a second checkpoint representation.
def editionSourceIdentity =
  (lambda unrestricted edition : (family LanguageEdition) .
    (lambda unrestricted source : Bytes .
      (bytes-checksum
        (bytes-append
          b"ALPHA-EDITION-SOURCE-v1"
          (bytes-append (languageEditionName edition) source)))))

def editionAllowsNaturalArithmetic =
  (lambda unrestricted edition : (family LanguageEdition) .
    (eliminate
      LanguageEdition
      (lambda unrestricted current : (family LanguageEdition) . Nat)
      edition
      (branch Alpha2026 . zero)
      (branch Alpha2027 . (succ zero))))

-- Quoted Text/Bytes syntax is introduced by the alpha-2027 authoring edition.
def editionAllowsQuotedLiterals =
  (lambda unrestricted edition : (family LanguageEdition) .
    (eliminate
      LanguageEdition
      (lambda unrestricted current : (family LanguageEdition) . Nat)
      edition
      (branch Alpha2026 . zero)
      (branch Alpha2027 . (succ zero))))

-- Named record construction, projection and update are alpha-2027 surface
-- forms. Their lowering uses the existing constructor/eliminator core.
def editionAllowsNamedRecords =
  (lambda unrestricted edition : (family LanguageEdition) .
    (eliminate
      LanguageEdition
      (lambda unrestricted current : (family LanguageEdition) . Nat)
      edition
      (branch Alpha2026 . zero)
      (branch Alpha2027 . (succ zero))))

-- Readable match/match-with syntax is introduced by alpha-2027 and lowers to
-- the existing exhaustive eliminator core.
def editionAllowsReadableMatching =
  (lambda unrestricted edition : (family LanguageEdition) .
    (eliminate
      LanguageEdition
      (lambda unrestricted current : (family LanguageEdition) . Nat)
      edition
      (branch Alpha2026 . zero)
      (branch Alpha2027 . (succ zero))))

-- Local sequencing forms are introduced by the alpha-2027 authoring edition.
def editionAllowsSequencing =
  (lambda unrestricted edition : (family LanguageEdition) .
    (eliminate
      LanguageEdition
      (lambda unrestricted current : (family LanguageEdition) . Nat)
      edition
      (branch Alpha2026 . zero)
      (branch Alpha2027 . (succ zero))))