Compiler.LanguageEdition

1module Compiler.LanguageEdition
2
3family LanguageEdition : Type 0
4constructor Alpha2026
5constructor Alpha2027
6
7end-family
8
9family LanguageEditionDecodeResult : Type 0
10constructor LanguageEditionDecoded
11field unrestricted decodedLanguageEdition : (family LanguageEdition)
12constructor LanguageEditionRejected
13
14end-family
15
16def languageEditionFailureCode =
17  (byte-to-nat (byte 88))
18
19-- The driver protocol requires the exact edition name, without a newline.
20def languageEditionName =
21  (lambda unrestricted edition : (family LanguageEdition) .
22    (eliminate
23      LanguageEdition
24      (lambda unrestricted current : (family LanguageEdition) . Bytes)
25      edition
26      (branch Alpha2026 . b"alpha-2026")
27      (branch Alpha2027 . b"alpha-2027")))
28
29def decodeLanguageEdition =
30  (lambda unrestricted name : Bytes .
31    (nat-eliminate
32      (lambda unrestricted matched : Nat . (family LanguageEditionDecodeResult))
33      (nat-eliminate
34        (lambda unrestricted matched : Nat . (family LanguageEditionDecodeResult))
35        (constructor LanguageEditionDecodeResult LanguageEditionRejected)
36        (lambda unrestricted predecessor : Nat .
37          (lambda unrestricted induction : (family LanguageEditionDecodeResult) .
38            (constructor
39              LanguageEditionDecodeResult
40              LanguageEditionDecoded
41              (constructor LanguageEdition Alpha2027))))
42        (bytes-equal name (languageEditionName (constructor LanguageEdition Alpha2027))))
43      (lambda unrestricted predecessor : Nat .
44        (lambda unrestricted induction : (family LanguageEditionDecodeResult) .
45          (constructor
46            LanguageEditionDecodeResult
47            LanguageEditionDecoded
48            (constructor LanguageEdition Alpha2026))))
49      (bytes-equal name (languageEditionName (constructor LanguageEdition Alpha2026)))))
50
51-- Existing checkpoint envelopes already validate source identity. Bind the
52-- selected edition into that identity before either save or restore. The fixed
53-- domain and fixed-width edition name distinguish this from legacy source-only
54-- hashes without introducing a second checkpoint representation.
55def editionSourceIdentity =
56  (lambda unrestricted edition : (family LanguageEdition) .
57    (lambda unrestricted source : Bytes .
58      (bytes-checksum
59        (bytes-append
60          b"ALPHA-EDITION-SOURCE-v1"
61          (bytes-append (languageEditionName edition) source)))))
62
63def editionAllowsNaturalArithmetic =
64  (lambda unrestricted edition : (family LanguageEdition) .
65    (eliminate
66      LanguageEdition
67      (lambda unrestricted current : (family LanguageEdition) . Nat)
68      edition
69      (branch Alpha2026 . zero)
70      (branch Alpha2027 . (succ zero))))
71
72-- Quoted Text/Bytes syntax is introduced by the alpha-2027 authoring edition.
73def editionAllowsQuotedLiterals =
74  (lambda unrestricted edition : (family LanguageEdition) .
75    (eliminate
76      LanguageEdition
77      (lambda unrestricted current : (family LanguageEdition) . Nat)
78      edition
79      (branch Alpha2026 . zero)
80      (branch Alpha2027 . (succ zero))))
81
82-- Named record construction, projection and update are alpha-2027 surface
83-- forms. Their lowering uses the existing constructor/eliminator core.
84def editionAllowsNamedRecords =
85  (lambda unrestricted edition : (family LanguageEdition) .
86    (eliminate
87      LanguageEdition
88      (lambda unrestricted current : (family LanguageEdition) . Nat)
89      edition
90      (branch Alpha2026 . zero)
91      (branch Alpha2027 . (succ zero))))
92
93-- Readable match/match-with syntax is introduced by alpha-2027 and lowers to
94-- the existing exhaustive eliminator core.
95def editionAllowsReadableMatching =
96  (lambda unrestricted edition : (family LanguageEdition) .
97    (eliminate
98      LanguageEdition
99      (lambda unrestricted current : (family LanguageEdition) . Nat)
100      edition
101      (branch Alpha2026 . zero)
102      (branch Alpha2027 . (succ zero))))
103
104-- Local sequencing forms are introduced by the alpha-2027 authoring edition.
105def editionAllowsSequencing =
106  (lambda unrestricted edition : (family LanguageEdition) .
107    (eliminate
108      LanguageEdition
109      (lambda unrestricted current : (family LanguageEdition) . Nat)
110      edition
111      (branch Alpha2026 . zero)
112      (branch Alpha2027 . (succ zero))))