... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/.

(.def# dummy_location
       ["" 0 0]
       #0)

(.def# prelude
       "library/lux"
       #1)

... (type .public Any
...   (Ex (_ a) a))
(.def# Any
       (.is_type#
        {9 #1
           [..prelude "Any"]
           {8 #0
              {0 #0}
              {4 #0 1}}})
       #1)

... (type .public Nothing
...   (All (_ a) a))
(.def# Nothing
       (.is_type#
        {9 #1
           [..prelude "Nothing"]
           {7 #0
              {0 #0}
              {4 #0 1}}})
       #1)

(.def# Bit
       (.is_type#
        {9 #1
           [..prelude "Bit"]
           {0 #0 "#Bit" {0 #0}}})
       #1)

(.def# I64
       (.is_type#
        {9 #1
           [..prelude "I64"]
           {7 #0
              {0 #0}
              {0 #0 "#I64" {0 #1 {4 #0 1} {0 #0}}}}})
       #1)

(.def# Nat
       (.is_type#
        {9 #1
           [..prelude "Nat"]
           {0 #0 "#I64" {0 #1 {0 #0 "#Nat" {0 #0}} {0 #0}}}})
       #1)

(.def# Int
       (.is_type#
        {9 #1
           [..prelude "Int"]
           {0 #0 "#I64" {0 #1 {0 #0 "#Int" {0 #0}} {0 #0}}}})
       #1)

(.def# Rev
       (.is_type#
        {9 #1
           [..prelude "Rev"]
           {0 #0 "#I64" {0 #1 {0 #0 "#Rev" {0 #0}} {0 #0}}}})
       #1)

(.def# Frac
       (.is_type#
        {9 #1
           [..prelude "Frac"]
           {0 #0 "#Frac" {0 #0}}})
       #1)

(.def# Text
       (.is_type#
        {9 #1
           [..prelude "Text"]
           {0 #0 "#Text" {0 #0}}})
       #1)

(.def# Symbol
       (.is_type#
        {9 #1
           [..prelude "Symbol"]
           {2 #0 Text Text}})
       #1)

... (type .public (List a)
...   (Variant
...    {#End}
...    {#Item a (List a)}))
(.def# List
       (.is_type#
        {9 #1
           [..prelude "List"]
           {7 #0
              {0 #0}
              {1 #0
                 ... End
                 Any
                 ... Item
                 {2 #0
                    {4 #0 1}
                    {9 #0
                       {4 #0 1}
                       {4 #0 0}}}}}})
       #1)

... (type .public Tag
...   (Nominal "#Tag"))
(.def# Tag
       (.is_type#
        {9 #1 [..prelude "Tag"]
           {0 #0 "#Tag" {0 #0}}})
       #1)

... (type .public Slot
...   (Nominal "#Slot"))
(.def# Slot
       (.is_type#
        {9 #1 [..prelude "Slot"]
           {0 #0 "#Slot" {0 #0}}})
       #1)

(.def# Label'
       (.is_type#
        {1 #0 [Any {2 #0 [Nat {2 #0 [Bit {9 #0 Symbol List}]}]}]})
       #0)

(.def# list_tags
       (.is# {9 #0 Symbol List}
             {0 #1 [[..prelude "#End"]
                    {0 #1 [[..prelude "#Item"]
                           {0 #0}]}]})
       #0)
(.def# #End (.as# Tag [(.is# Label' {0 #1 [0 #0 ..list_tags]}) List]) #1)
(.def# #Item (.as# Tag [(.is# Label' {0 #1 [0 #1 ..list_tags]}) List]) #1)

... (type .public (Maybe a)
...   {#None}
...   {#Some a})
(.def# Maybe
       (.is_type#
        {9 #1
           [..prelude "Maybe"]
           {7 #0
              {#End}
              {1 #0
                 ... None
                 Any
                 ... Some
                 {4 #0 1}}}})
       #1)
(.def# maybe_tags
       (.is# {9 #0 Symbol List}
             {0 #1 [[..prelude "#None"]
                    {0 #1 [[..prelude "#Some"]
                           {0 #0}]}]})
       #0)
(.def# #None (.as# Tag [(.is# Label' {0 #1 [0 #0 ..maybe_tags]}) Maybe]) #1)
(.def# #Some (.as# Tag [(.is# Label' {0 #1 [0 #1 ..maybe_tags]}) Maybe]) #1)

... (type .public Type
...   (Rec Type
...     (Variant
...      {#Nominal Text (List Type)}
...      {#Sum Type Type}
...      {#Product Type Type}
...      {#Function Type Type}
...      {#Parameter Nat}
...      {#Var Nat}
...      {#Ex Nat}
...      {#UnivQ (List Type) Type}
...      {#ExQ (List Type) Type}
...      {#Apply Type Type}
...      {#Named Symbol Type})))
(.def# Type
       (.is_type#
        {9 #1 [..prelude "Type"]
           ({Type
             ({Type_List
               ({Type_Pair
                 {9 #0
                    {0 #0 ["" {#End}]}
                    {7 #0
                       {#End}
                       {1 #0
                          ... Nominal
                          {2 #0 Text Type_List}
                          {1 #0
                             ... Sum
                             Type_Pair
                             {1 #0
                                ... Product
                                Type_Pair
                                {1 #0
                                   ... Function
                                   Type_Pair
                                   {1 #0
                                      ... Parameter
                                      Nat
                                      {1 #0
                                         ... Var
                                         Nat
                                         {1 #0
                                            ... Ex
                                            Nat
                                            {1 #0
                                               ... UnivQ
                                               {2 #0 Type_List Type}
                                               {1 #0
                                                  ... ExQ
                                                  {2 #0 Type_List Type}
                                                  {1 #0
                                                     ... Apply
                                                     Type_Pair
                                                     ... Named
                                                     {2 #0 Symbol Type}}}}}}}}}}}}}}
                (.is_type# {2 #0 Type Type}))}
              (.is_type# {9 #0 Type List}))}
            (.is_type# {9 #0 {0 #0 ["" {#End}]} {4 #0 0}}))})
       #1)

(.def# type_tags
       (.is# {9 #0 Symbol List}
             {0 #1 [[..prelude "#Nominal"]
                    {0 #1 [[..prelude "#Sum"]
                           {0 #1 [[..prelude "#Product"]
                                  {0 #1 [[..prelude "#Function"]
                                         {0 #1 [[..prelude "#Parameter"]
                                                {0 #1 [[..prelude "#Var"]
                                                       {0 #1 [[..prelude "#Ex"]
                                                              {0 #1 [[..prelude "#UnivQ"]
                                                                     {0 #1 [[..prelude "#ExQ"]
                                                                            {0 #1 [[..prelude "#Apply"]
                                                                                   {0 #1 [[..prelude "#Named"]
                                                                                          {0 #0}]}]}]}]}]}]}]}]}]}]}]})
       #0)
(.def# #Nominal (.as# Tag [(.is# Label' {#Some [0 #0 ..type_tags]}) Type]) #1)
(.def# #Sum (.as# Tag [(.is# Label' {#Some [1 #0 ..type_tags]}) Type]) #1)
(.def# #Product (.as# Tag [(.is# Label' {#Some [2 #0 ..type_tags]}) Type]) #1)
(.def# #Function (.as# Tag [(.is# Label' {#Some [3 #0 ..type_tags]}) Type]) #1)
(.def# #Parameter (.as# Tag [(.is# Label' {#Some [4 #0 ..type_tags]}) Type]) #1)
(.def# #Var (.as# Tag [(.is# Label' {#Some [5 #0 ..type_tags]}) Type]) #1)
(.def# #Ex (.as# Tag [(.is# Label' {#Some [6 #0 ..type_tags]}) Type]) #1)
(.def# #UnivQ (.as# Tag [(.is# Label' {#Some [7 #0 ..type_tags]}) Type]) #1)
(.def# #ExQ (.as# Tag [(.is# Label' {#Some [8 #0 ..type_tags]}) Type]) #1)
(.def# #Apply (.as# Tag [(.is# Label' {#Some [9 #0 ..type_tags]}) Type]) #1)
(.def# #Named (.as# Tag [(.is# Label' {#Some [9 #1 ..type_tags]}) Type]) #1)

... (type .public Label
...   [(Maybe [Nat Bit (List Symbol)]) Type])
(.def# Label
       (.is# Type
             {#Named [..prelude "Label"]
                     {#Product {#Apply {#Product Nat {#Product Bit {#Apply Symbol List}}} Maybe}
                               Type}})
       #1)

(.def# tag
       (.is# {#Function Label Tag}
             ([_ it] (.as# Tag it)))
       #0)

(.def# slot
       (.is# {#Function Label Slot}
             ([_ it] (.as# Slot it)))
       #0)

... (type .public Location
...   (Record
...    [#module Text
...     #line   Nat
...     #column Nat]))
(.def# Location
       (.is# Type
             {#Named [..prelude "Location"]
                     {#Product Text {#Product Nat Nat}}})
       #1)
(.def# location_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#module"]
                    {#Item [..prelude "#line"]
                           {#Item [..prelude "#column"]
                                  {#End}}}})
       #0)
(.def# #module (slot [{#Some [0 #0 ..location_slots]} Location]) #1)
(.def# #line (slot [{#Some [1 #0 ..location_slots]} Location]) #1)
(.def# #column (slot [{#Some [1 #1 ..location_slots]} Location]) #1)

... (type .public (Ann m v)
...   (Record
...    [#meta  m
...     #datum v]))
(.def# Ann
       (.is# Type
             {#Named [..prelude "Ann"]
                     {#UnivQ {#End}
                             {#UnivQ {#End}
                                     {#Product
                                      {#Parameter 3}
                                      {#Parameter 1}}}}})
       #1)
(.def# ann_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#meta"]
                    {#Item [..prelude "#datum"]
                           {#End}}})
       #0)
(.def# #meta (slot [{#Some [0 #0 ..ann_slots]} Ann]) #1)
(.def# #datum (slot [{#Some [0 #1 ..ann_slots]} Ann]) #1)

... (type .public (Code' w)
...   (Variant
...    {#Bit Bit}
...    {#Nat Nat}
...    {#Int Int}
...    {#Rev Rev}
...    {#Frac Frac}
...    {#Text Text}
...    {#Symbol Symbol}
...    {#Form (List (w (Code' w)))}
...    {#Variant (List (w (Code' w)))}
...    {#Tuple (List (w (Code' w)))}))
(.def# Code'
       (.is# Type
             {#Named [..prelude "Code'"]
                     ({Code
                       ({Code_List
                         {#UnivQ {#End}
                                 {#Sum
                                  ... Bit
                                  Bit
                                  {#Sum
                                   ... Nat
                                   Nat
                                   {#Sum
                                    ... Int
                                    Int
                                    {#Sum
                                     ... Rev
                                     Rev
                                     {#Sum
                                      ... Frac
                                      Frac
                                      {#Sum
                                       ... Text
                                       Text
                                       {#Sum
                                        ... Symbol
                                        Symbol
                                        {#Sum
                                         ... Form
                                         Code_List
                                         {#Sum
                                          ... Variant
                                          Code_List
                                          ... Tuple
                                          Code_List
                                          }}}}}}}}}
                                 }}
                        (.is# Type
                              {#Apply Code List}))}
                      (.is# Type
                            {#Apply {#Apply {#Parameter 1}
                                            {#Parameter 0}}
                                    {#Parameter 1}}))})
       #1)
(.def# code'_tags
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#Bit"]
                    {#Item [..prelude "#Nat"]
                           {#Item [..prelude "#Int"]
                                  {#Item [..prelude "#Rev"]
                                         {#Item [..prelude "#Frac"]
                                                {#Item [..prelude "#Text"]
                                                       {#Item [..prelude "#Symbol"]
                                                              {#Item [..prelude "#Form"]
                                                                     {#Item [..prelude "#Variant"]
                                                                            {#Item [..prelude "#Tuple"]
                                                                                   {#End}}}}}}}}}}})
       #0)
(.def# #Bit (tag [{#Some [0 #0 ..code'_tags]} Code']) #1)
(.def# #Nat (tag [{#Some [1 #0 ..code'_tags]} Code']) #1)
(.def# #Int (tag [{#Some [2 #0 ..code'_tags]} Code']) #1)
(.def# #Rev (tag [{#Some [3 #0 ..code'_tags]} Code']) #1)
(.def# #Frac (tag [{#Some [4 #0 ..code'_tags]} Code']) #1)
(.def# #Text (tag [{#Some [5 #0 ..code'_tags]} Code']) #1)
(.def# #Symbol (tag [{#Some [6 #0 ..code'_tags]} Code']) #1)
(.def# #Form (tag [{#Some [7 #0 ..code'_tags]} Code']) #1)
(.def# #Variant (tag [{#Some [8 #0 ..code'_tags]} Code']) #1)
(.def# #Tuple (tag [{#Some [8 #1 ..code'_tags]} Code']) #1)

... (type .public Code
...   (Ann Location (Code' (Ann Location))))
(.def# Code
       (.is# Type
             {#Named [..prelude "Code"]
                     ({w
                       {#Apply {#Apply w Code'} w}}
                      (.is# Type {#Apply Location Ann}))})
       #1)

(.def# private
       #0
       #1)

(.def# public
       #1
       #1)

(.def# local
       #0
       #1)

(.def# global
       #1
       #1)

(.def# _ann
       (.is# {#Function {#Apply {#Apply Location Ann} Code'}
                        Code}
             ([_ data]
              [dummy_location data]))
       #0)

(.def# bit$
       (.is# {#Function Bit Code}
             ([_ value] (_ann {#Bit value})))
       #0)

(.def# nat$
       (.is# {#Function Nat Code}
             ([_ value] (_ann {#Nat value})))
       #0)

(.def# int$
       (.is# {#Function Int Code}
             ([_ value] (_ann {#Int value})))
       #0)

(.def# rev$
       (.is# {#Function Rev Code}
             ([_ value] (_ann {#Rev value})))
       #0)

(.def# frac$
       (.is# {#Function Frac Code}
             ([_ value] (_ann {#Frac value})))
       #0)

(.def# text$
       (.is# {#Function Text Code}
             ([_ text] (_ann {#Text text})))
       #0)

(.def# symbol$
       (.is# {#Function Symbol Code}
             ([_ name] (_ann {#Symbol name})))
       #0)

(.def# local$
       (.is# {#Function Text Code}
             ([_ name] (_ann {#Symbol ["" name]})))
       #0)

(.def# form$
       (.is# {#Function {#Apply Code List} Code}
             ([_ tokens] (_ann {#Form tokens})))
       #0)

(.def# variant$
       (.is# {#Function {#Apply Code List} Code}
             ([_ tokens] (_ann {#Variant tokens})))
       #0)

(.def# tuple$
       (.is# {#Function {#Apply Code List} Code}
             ([_ tokens] (_ann {#Tuple tokens})))
       #0)

... (type .public Definition
...   [Type Any])
(.def# Definition
       (.is# Type
             {#Named [..prelude "Definition"]
                     {#Product Type Any}})
       .public)

... (type .public Default
...   Definition)
(.def# Default
       (.is# Type
             {#Named [..prelude "Default"]
                     Definition})
       .public)

... (type .public Alias
...   Symbol)
(.def# Alias
       (.is# Type
             {#Named [..prelude "Alias"]
                     Symbol})
       .public)

... (type .public Global
...   (Variant
...    {#Definition Definition}
...    {#Alias Alias}
...    {#Default Default}))
(.def# Global
       (.is# Type
             {#Named [..prelude "Global"]
                     {#Sum Definition
                           {#Sum Alias
                                 Default}}})
       .public)

(.def# global_tags
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#Definition"]
                    {#Item [..prelude "#Alias"]
                           {#Item [..prelude "#Default"]
                                  {#End}}}})
       #0)
(.def# #Definition (tag [{#Some [0 #0 ..global_tags]} Global]) .public)
(.def# #Alias (tag [{#Some [1 #0 ..global_tags]} Global]) .public)
(.def# #Default (tag [{#Some [1 #1 ..global_tags]} Global]) .public)

... (type .public (Bindings k v)
...   (Record
...    [#counter Nat
...     #mappings (List [k v])]))
(.def# Bindings
       (.is# Type
             {#Named [..prelude "Bindings"]
                     {#UnivQ {#End}
                             {#UnivQ {#End}
                                     {#Product
                                      ... counter
                                      Nat
                                      ... mappings
                                      {#Apply {#Product {#Parameter 3}
                                                        {#Parameter 1}}
                                              List}}}}})
       .public)

(.def# bindings_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#counter"]
                    {#Item [..prelude "#mappings"]
                           {#End}}})
       #0)
(.def# #counter (slot [{#Some [0 #0 ..bindings_slots]} Bindings]) .public)
(.def# #mappings (slot [{#Some [0 #1 ..bindings_slots]} Bindings]) .public)

... (type .public Ref
...   {#Local Nat}
...   {#Captured Nat})
(.def# Ref
       (.is# Type
             {#Named [..prelude "Ref"]
                     {#Sum
                      ... Local
                      Nat
                      ... Captured
                      Nat}})
       .public)

(.def# ref_tags
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#Local"]
                    {#Item [..prelude "#Captured"]
                           {#End}}})
       #0)
(.def# #Local (tag [{#Some [0 #0 ..ref_tags]} Ref]) .public)
(.def# #Captured (tag [{#Some [0 #1 ..ref_tags]} Ref]) .public)

... TODO: Get rid of both #scope_name & #inner_scopes
... (type .public Scope
...   (Record
...    [#scope_name (List Text)
...     #inner_scopes Nat
...     #locals (Bindings Text [Type Nat])
...     #captured (Bindings Text [Type Ref])]))
(.def# Scope
       (.is# Type
             {#Named [..prelude "Scope"]
                     {#Product
                      ... name
                      {#Apply Text List}
                      {#Product
                       ... inner
                       Nat
                       {#Product
                        ... locals
                        {#Apply {#Product Type Nat} {#Apply Text Bindings}}
                        ... captured
                        {#Apply {#Product Type Ref} {#Apply Text Bindings}}}}}})
       .public)

(.def# scope_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#scope_name"]
                    {#Item [..prelude "#inner_scopes"]
                           {#Item [..prelude "#locals"]
                                  {#Item [..prelude "#captured"]
                                         {#End}}}}})
       #0)
(.def# #scope_name (slot [{#Some [0 #0 ..scope_slots]} Scope]) .public)
(.def# #inner_scopes (slot [{#Some [1 #0 ..scope_slots]} Scope]) .public)
(.def# #locals (slot [{#Some [2 #0 ..scope_slots]} Scope]) .public)
(.def# #captured (slot [{#Some [2 #1 ..scope_slots]} Scope]) .public)

(.def# Code_List
       (.is# Type
             {#Apply Code List})
       #0)

... (type .public (Either l r)
...   (Variant
...    {#Left l}
...    {#Right r}))
(.def# Either
       (.is# Type
             {#Named [..prelude "Either"]
                     {#UnivQ {#End}
                             {#UnivQ {#End}
                                     {#Sum
                                      ... Left
                                      {#Parameter 3}
                                      ... Right
                                      {#Parameter 1}}}}})
       .public)

(.def# either_tags
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#Left"]
                    {#Item [..prelude "#Right"]
                           {#End}}})
       #0)
(.def# #Left (tag [{#Some [0 #0 ..either_tags]} Either]) .public)
(.def# #Right (tag [{#Some [0 #1 ..either_tags]} Either]) .public)

... (type .public Source
...   [Location Nat Text])
(.def# Source
       (.is# Type
             {#Named [..prelude "Source"]
                     {#Product Location {#Product Nat Text}}})
       .public)

... (type .public Module_State
...   (Variant
...    #Active
...    #Compiled
...    #Cached))
(.def# Module_State
       (.is# Type
             {#Named [..prelude "Module_State"]
                     {#Sum
                      ... #Active
                      Any
                      {#Sum
                       ... #Compiled
                       Any
                       ... #Cached
                       Any}}})
       .public)

(.def# module_state_tags
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#Active"]
                    {#Item [..prelude "#Compiled"]
                           {#Item [..prelude "#Cached"]
                                  {#End}}}})
       #0)
(.def# #Active (tag [{#Some [0 #0 ..module_state_tags]} Module_State]) .public)
(.def# #Compiled (tag [{#Some [1 #0 ..module_state_tags]} Module_State]) .public)
(.def# #Cached (tag [{#Some [1 #1 ..module_state_tags]} Module_State]) .public)

... (type .public Module
...   (Record
...    [#module_hash        Nat
...     #module_aliases     (List [Text Text])
...     #definitions        (List [Text [Bit Global]])
...     #imports            (List Text)
...     #module_state       Module_State]))
(.def# Module
       (.is# Type
             {#Named [..prelude "Module"]
                     {#Product
                      ... module_hash
                      Nat
                      {#Product
                       ... module_aliases
                       {#Apply {#Product Text Text} List}
                       {#Product
                        ... definitions
                        {#Apply {#Product Text {#Product Bit Global}} List}
                        {#Product
                         ... imports
                         {#Apply Text List}
                         ... module_state
                         Module_State
                         }}}}})
       .public)

(.def# module_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#module_hash"]
                    {#Item [..prelude "#module_aliases"]
                           {#Item [..prelude "#definitions"]
                                  {#Item [..prelude "#imports"]
                                         {#Item [..prelude "#module_state"]
                                                {#End}}}}}})
       #0)
(.def# #module_hash (slot [{#Some [0 #0 ..module_slots]} Module]) .public)
(.def# #module_aliases (slot [{#Some [1 #0 ..module_slots]} Module]) .public)
(.def# #definitions (slot [{#Some [2 #0 ..module_slots]} Module]) .public)
(.def# #imports (slot [{#Some [3 #0 ..module_slots]} Module]) .public)
(.def# #module_state (slot [{#Some [3 #1 ..module_slots]} Module]) .public)

... (type .public Type_Context
...   (Record
...    [#ex_counter Nat
...     #var_counter Nat
...     #var_bindings (List [Nat (Maybe Type)])]))
(.def# Type_Context
       (.is# Type
             {#Named [..prelude "Type_Context"]
                     {#Product ... ex_counter
                      Nat
                      {#Product ... var_counter
                       Nat
                       ... var_bindings
                       {#Apply {#Product Nat {#Apply Type Maybe}}
                               List}}}})
       .public)

(.def# type_context_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#ex_counter"]
                    {#Item [..prelude "#var_counter"]
                           {#Item [..prelude "#var_bindings"]
                                  {#End}}}})
       #0)
(.def# #ex_counter (slot [{#Some [0 #0 ..type_context_slots]} Type_Context]) .public)
(.def# #var_counter (slot [{#Some [1 #0 ..type_context_slots]} Type_Context]) .public)
(.def# #var_bindings (slot [{#Some [1 #1 ..type_context_slots]} Type_Context]) .public)

... (type .public Mode
...   (Variant
...    {#Build}
...    {#Eval}
...    {#Interpreter}))
(.def# Mode
       (.is# Type
             {#Named [..prelude "Mode"]
                     {#Sum
                      ... Build
                      Any
                      {#Sum
                       ... Eval
                       Any
                       ... Interpreter
                       Any}}})
       .public)

(.def# mode_tags
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#Build"]
                    {#Item [..prelude "#Eval"]
                           {#Item [..prelude "#Interpreter"]
                                  {#End}}}})
       #0)
(.def# #Build (tag [{#Some [0 #0 ..mode_tags]} Mode]) .public)
(.def# #Eval (tag [{#Some [1 #0 ..mode_tags]} Mode]) .public)
(.def# #Interpreter (tag [{#Some [1 #1 ..mode_tags]} Mode]) .public)

... (type .public Info
...   (Record
...    [#target        Text
...     #version       Text
...     #mode          Mode
...     #configuration (List [Text Text])]))
(.def# Info
       (.is# Type
             {#Named [..prelude "Info"]
                     {#Product
                      ... target
                      Text
                      {#Product
                       ... version
                       Text
                       {#Product
                        ... mode
                        Mode
                        ... configuration
                        {#Apply {#Product Text Text} List}}}}})
       .public)

(.def# info_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#target"]
                    {#Item [..prelude "#version"]
                           {#Item [..prelude "#mode"]
                                  {#Item [..prelude "#configuration"]
                                         {#End}}}}})
       #0)
(.def# #target (slot [{#Some [0 #0 ..info_slots]} Info]) .public)
(.def# #version (slot [{#Some [1 #0 ..info_slots]} Info]) .public)
(.def# #mode (slot [{#Some [2 #0 ..info_slots]} Info]) .public)
(.def# #configuration (slot [{#Some [2 #1 ..info_slots]} Info]) .public)

... (type .public Lux
...   (Rec Lux
...     (Record
...      [#info            Info
...       #source          Source
...       #location        Location
...       #current_module  (Maybe Text)
...       #modules         (List [Text Module])
...       #scopes          (List Scope)
...       #type_context    Type_Context
...       #expected        (Maybe Type)
...       #seed            Nat
...       #scope_type_vars (List Nat)
...       #extensions      Any
...       #eval            (-> Type Code (-> Lux (Either Text [Lux Any])))
...       #host            Any])))
(.def# Lux
       (.is# Type
             {#Named [..prelude "Lux"]
                     ({Lux
                       {#Apply {0 #0 ["" {#End}]}
                               {#UnivQ {#End}
                                       {#Product
                                        ... info
                                        Info
                                        {#Product
                                         ... source
                                         Source
                                         {#Product
                                          ... location
                                          Location
                                          {#Product
                                           ... current_module
                                           {#Apply Text Maybe}
                                           {#Product
                                            ... modules
                                            {#Apply {#Product Text Module} List}
                                            {#Product
                                             ... scopes
                                             {#Apply Scope List}
                                             {#Product
                                              ... type_context
                                              Type_Context
                                              {#Product
                                               ... expected
                                               {#Apply Type Maybe}
                                               {#Product
                                                ... seed
                                                Nat
                                                {#Product
                                                 ... scope_type_vars
                                                 {#Apply Nat List}
                                                 {#Product
                                                  ... extensions
                                                  Any
                                                  {#Product
                                                   ... eval
                                                   {#Function Type
                                                              {#Function Code
                                                                         {#Function Lux
                                                                                    {#Sum Text {#Product Lux Any}}}}}
                                                   ... host
                                                   Any}}}}}}}}}}}}}}}
                      {#Apply {0 #0 ["" {#End}]} {#Parameter 0}})})
       .public)

(.def# lux_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#info"]
                    {#Item [..prelude "#source"]
                           {#Item [..prelude "#location"]
                                  {#Item [..prelude "#current_module"]
                                         {#Item [..prelude "#modules"]
                                                {#Item [..prelude "#scopes"]
                                                       {#Item [..prelude "#type_context"]
                                                              {#Item [..prelude "#expected"]
                                                                     {#Item [..prelude "#seed"]
                                                                            {#Item [..prelude "#scope_type_vars"]
                                                                                   {#Item [..prelude "#extensions"]
                                                                                          {#Item [..prelude "#eval"]
                                                                                                 {#Item [..prelude "#host"]
                                                                                                        {#End}}}}}}}}}}}}}})
       #0)
(.def# #info (slot [{#Some [0 #0 ..lux_slots]} Lux]) .public)
(.def# #source (slot [{#Some [1 #0 ..lux_slots]} Lux]) .public)
(.def# #location (slot [{#Some [2 #0 ..lux_slots]} Lux]) .public)
(.def# #current_module (slot [{#Some [3 #0 ..lux_slots]} Lux]) .public)
(.def# #modules (slot [{#Some [4 #0 ..lux_slots]} Lux]) .public)
(.def# #scopes (slot [{#Some [5 #0 ..lux_slots]} Lux]) .public)
(.def# #type_context (slot [{#Some [6 #0 ..lux_slots]} Lux]) .public)
(.def# #expected (slot [{#Some [7 #0 ..lux_slots]} Lux]) .public)
(.def# #seed (slot [{#Some [8 #0 ..lux_slots]} Lux]) .public)
(.def# #scope_type_vars (slot [{#Some [9 #0 ..lux_slots]} Lux]) .public)
(.def# #extensions (slot [{#Some [10 #0 ..lux_slots]} Lux]) .public)
(.def# #eval (slot [{#Some [11 #0 ..lux_slots]} Lux]) .public)
(.def# #host (slot [{#Some [11 #1 ..lux_slots]} Lux]) .public)

... (type .public (Meta a)
...   (-> Lux (Either Text [Lux a])))
(.def# Meta
       (.is# Type
             {#Named [..prelude "Meta"]
                     {#UnivQ {#End}
                             {#Function Lux
                                        {#Apply {#Product Lux {#Parameter 1}}
                                                {#Apply Text Either}}}}})
       .public)

... (type .public Macro'
...   (-> (List Code) (Meta (List Code))))
(.def# Macro'
       (.is# Type
             {#Named [..prelude "Macro'"]
                     {#Function Code_List {#Apply Code_List Meta}}})
       .public)

... (type .public Macro
...   (Nominal "#Macro"))
(.def# Macro
       (.is# Type
             {#Named [..prelude "Macro"]
                     {#Nominal "#Macro" {#End}}})
       .public)

... Base functions & macros
(.def# meta#in
       (.is# {#UnivQ {#End} {#Function {#Parameter 1} {#Apply {#Parameter 1} Meta}}}
             ([_ val]
              ([_ state]
               {#Right [state val]})))
       #0)

(.def# failure
       (.is# {#UnivQ {#End} {#Function Text {#Apply {#Parameter 1} Meta}}}
             ([_ msg]
              ([_ state]
               {#Left msg})))
       #0)

(.def# text#composite
       (.is# {#Function Text {#Function Text Text}}
             ([_ x]
              ([_ y]
               (.text_composite# x y))))
       #0)

(.def# symbol_separator
       (.is# Text
             ".")
       #0)

(.def# symbol#encoded
       (.is# {#Function Symbol Text}
             ([_ full_name]
              ({[module name]
                ({"" name
                  _  (.text_composite# module ..symbol_separator name)}
                 module)}
               full_name)))
       #0)

(.def# \''
       (.is# Text
             (.int_char# +34))
       #0)

... TODO: Allow asking the compiler for the name of the definition
... currently being defined. That name can then be fed into
... 'wrong_syntax_error' for easier maintenance of the error_messages.
(.def# wrong_syntax_error
       (.is# {#Function Symbol Text}
             ([_ it]
              (.text_composite# "Wrong syntax for " \'' (symbol#encoded it) \'' ".")))
       #0)

(.def# let''
       (.as# Macro
             (.is# Macro'
                   ([_ tokens]
                    ({{#Item lhs {#Item rhs {#Item body {#End}}}}
                      (meta#in {#Item (form$ {#Item (variant$ {#Item lhs {#Item body {#End}}})
                                                    {#Item rhs {#End}}})
                                      {#End}})

                      _
                      (failure "Wrong syntax for let''")}
                     tokens))))
       #0)

(.def# function''
       (.as# Macro
             (.is# Macro'
                   ([_ tokens]
                    ({{#Item [_ {#Tuple {#Item arg args'}}] {#Item body {#End}}}
                      (meta#in {#Item (_ann {#Form {#Item (_ann {#Tuple {#Item (_ann {#Symbol ["" ""]})
                                                                               {#Item arg {#End}}}})
                                                          {#Item ({{#End}
                                                                   body

                                                                   _
                                                                   (_ann {#Form {#Item (_ann {#Symbol [..prelude "function''"]})
                                                                                       {#Item (_ann {#Tuple args'})
                                                                                              {#Item body {#End}}}}})}
                                                                  args')
                                                                 {#End}}}})
                                      {#End}})

                      {#Item [_ {#Symbol ["" self]}] {#Item [_ {#Tuple {#Item arg args'}}] {#Item body {#End}}}}
                      (meta#in {#Item (_ann {#Form {#Item (_ann {#Tuple {#Item (_ann {#Symbol ["" self]})
                                                                               {#Item arg {#End}}}})
                                                          {#Item ({{#End}
                                                                   body

                                                                   _
                                                                   (_ann {#Form {#Item (_ann {#Symbol [..prelude "function''"]})
                                                                                       {#Item (_ann {#Tuple args'})
                                                                                              {#Item body {#End}}}}})}
                                                                  args')
                                                                 {#End}}}})
                                      {#End}})

                      _
                      (failure "Wrong syntax for function''")}
                     tokens))))
       #0)

(.def# as_def
       (.is# {#Function Code {#Function Code {#Function Code Code}}}
             (function'' [name value export_policy]
                         (form$ {#Item (symbol$ [..prelude "def#"]) {#Item name {#Item value {#Item export_policy {#End}}}}})))
       #0)

(.def# as_checked
       (.is# {#Function Code {#Function Code Code}}
             (function'' [type value]
                         (form$ {#Item (symbol$ [..prelude "is#"]) {#Item type {#Item value {#End}}}})))
       #0)

(.def# as_function
       (.is# {#Function Code {#Function {#Apply Code List} {#Function Code Code}}}
             (function'' as_function [self inputs output]
                         ({{#End}
                           output

                           {#Item head tail}
                           (_ann {#Form {#Item (_ann {#Tuple {#Item self {#Item head {#End}}}})
                                               {#Item (as_function (_ann {#Symbol ["" ""]}) tail output)
                                                      {#End}}}})}
                          inputs)))
       #0)

(.def# as_macro
       (.is# {#Function Code Code}
             (function'' [expression]
                         (form$ {#Item (symbol$ [..prelude "as#"])
                                       {#Item (symbol$ [..prelude "Macro"])
                                              {#Item (form$ {#Item (symbol$ [..prelude "is#"])
                                                                   {#Item (symbol$ [..prelude "Macro'"])
                                                                          {#Item expression
                                                                                 {#End}}}})
                                                     {#End}}}})))
       #0)

(.def# def'
       (.as# Macro
             (.is# Macro'
                   (function'' [tokens]
                               ({{#Item [export_policy
                                         {#Item [[_ {#Form {#Item [name args]}}]
                                                 {#Item [type {#Item [body {#End}]}]}]}]}
                                 (meta#in {#Item [(as_def name
                                                          (as_checked type (as_function name args body))
                                                          export_policy)
                                                  {#End}]})

                                 {#Item [export_policy {#Item [name {#Item [type {#Item [body {#End}]}]}]}]}
                                 (meta#in {#Item [(as_def name (as_checked type body)
                                                          export_policy)
                                                  {#End}]})

                                 _
                                 (failure "Wrong syntax for def'")}
                                tokens))))
       #0)

(.def# macro
       (.as# Macro
             (.is# Macro'
                   (function'' [tokens]
                               ({{#Item [_ {#Form {#Item name {#Item head tail}}}] {#Item body {#End}}}
                                 (meta#in {#Item (as_macro (as_function name {#Item head tail} body))
                                                 {#End}})

                                 _
                                 (failure (wrong_syntax_error [..prelude "macro"]))}
                                tokens))))
       #1)

(def' .public comment
      Macro
      (macro (_ tokens)
        (meta#in {#End})))

(def' .private $
      Macro
      (macro (_ tokens)
        ({{#Item x {#End}}
          (meta#in tokens)

          {#Item x {#Item y xs}}
          (meta#in {#Item (form$ {#Item (symbol$ [..prelude "$"])
                                        {#Item (variant$ {#Item (symbol$ [..prelude "#Apply"])
                                                                {#Item y {#Item x {#End}}}})
                                               xs}})
                          {#End}})

          _
          (failure "Wrong syntax for $")}
         tokens)))

(def' .private (list#mix f init xs)
      ... (All (_ a b) (-> (-> b a a) a (List b) a))
      {#UnivQ {#End} {#UnivQ {#End} {#Function {#Function {#Parameter 1}
                                                          {#Function {#Parameter 3}
                                                                     {#Parameter 3}}}
                                               {#Function {#Parameter 3}
                                                          {#Function ($ List {#Parameter 1})
                                                                     {#Parameter 3}}}}}}
      ({{#End}
        init

        {#Item x xs'}
        (list#mix f (f x init) xs')}
       xs))

(def' .private (list#reversed list)
      {#UnivQ {#End}
              {#Function ($ List {#Parameter 1}) ($ List {#Parameter 1})}}
      (list#mix (.is# {#UnivQ {#End}
                              {#Function {#Parameter 1} {#Function ($ List {#Parameter 1}) ($ List {#Parameter 1})}}}
                      (function'' [head tail] {#Item head tail}))
                {#End}
                list))

(def' .private (list#each f xs)
      {#UnivQ {#End}
              {#UnivQ {#End}
                      {#Function {#Function {#Parameter 3} {#Parameter 1}}
                                 {#Function ($ List {#Parameter 3})
                                            ($ List {#Parameter 1})}}}}
      (list#mix (function'' [head tail] {#Item (f head) tail})
                {#End}
                (list#reversed xs)))

(def' .private Replacement_Environment
      Type
      ($ List {#Product Text Code}))

(def' .private (replacement_environment xs ys)
      {#Function ($ List Text) {#Function ($ List Code) Replacement_Environment}}
      ({[{#Item x xs'} {#Item y ys'}]
        {#Item [x y] (replacement_environment xs' ys')}

        _
        {#End}}
       [xs ys]))

(def' .private (text#= reference sample)
      {#Function Text {#Function Text Bit}}
      (.text_=# reference sample))

(def' .private (replacement for environment)
      {#Function Text {#Function Replacement_Environment ($ Maybe Code)}}
      ({{#End}
        {#None}

        {#Item [k v] environment'}
        ({[#1] {#Some v}
          [#0] (replacement for environment')}
         (text#= k for))}
       environment))

(def' .private (with_replacements reps syntax)
      {#Function Replacement_Environment {#Function Code Code}}
      ({[_ {#Symbol "" name}]
        ({{#Some replacement}
          replacement

          {#None}
          syntax}
         (..replacement name reps))

        [meta {#Form parts}]
        [meta {#Form (list#each (with_replacements reps) parts)}]

        [meta {#Variant members}]
        [meta {#Variant (list#each (with_replacements reps) members)}]

        [meta {#Tuple members}]
        [meta {#Tuple (list#each (with_replacements reps) members)}]
        
        _
        syntax}
       syntax))

(def' .private (n#* param subject)
      {#Function Nat {#Function Nat Nat}}
      (.as# Nat
            (.int_*# (.as# Int param)
                     (.as# Int subject))))

(def' .private (list#size list)
      {#UnivQ {#End}
              {#Function ($ List {#Parameter 1}) Nat}}
      (list#mix (function'' [_ acc] (.i64_+# 1 acc)) 0 list))

(def' .private (let$ binding value body)
      {#Function Code {#Function Code {#Function Code Code}}}
      (form$ {#Item (variant$ {#Item binding {#Item body {#End}}})
                    {#Item value {#End}}}))

(def' .private |#End|
      Code
      (variant$ {#Item (symbol$ [..prelude "#End"]) {#End}}))

(def' .private (|#Item| head tail)
      {#Function Code {#Function Code Code}}
      (variant$ {#Item (symbol$ [..prelude "#Item"])
                       {#Item head
                              {#Item tail
                                     {#End}}}}))

(def' .private (UnivQ$ body)
      {#Function Code Code}
      (variant$ {#Item (symbol$ [..prelude "#UnivQ"]) {#Item ..|#End| {#Item body {#End}}}}))

(def' .private (ExQ$ body)
      {#Function Code Code}
      (variant$ {#Item (symbol$ [..prelude "#ExQ"]) {#Item ..|#End| {#Item body {#End}}}}))

(def' .private quantification_level
      Text
      (.text_composite# \'' "quantification_level" \''))

(def' .private quantified
      {#Function Code Code}
      (let$ (local$ ..quantification_level) (nat$ 0)))

(def' .private (quantified_type_parameter idx)
      {#Function Nat Code}
      (variant$ {#Item (symbol$ [..prelude "#Parameter"])
                       {#Item (form$ {#Item (symbol$ [..prelude "i64_+#"])
                                            {#Item (local$ ..quantification_level)
                                                   {#Item (nat$ idx)
                                                          {#End}}}})
                              {#End}}}))

(def' .private (next_level depth)
      {#Function Nat Nat}
      (.i64_+# 2 depth))

(def' .private (self_id? id)
      {#Function Nat Bit}
      (.i64_=# id (.as# Nat
                        (.int_*# +2
                                 (.int_/# +2
                                          (.as# Int
                                                id))))))

(def' .public (__adjusted_quantified_type__ permission depth type)
      {#Function Nat {#Function Nat {#Function Type Type}}}
      ({0
        ({... Jackpot!
          {#Parameter id}
          ({id'
            ({[#0] {#Parameter id'}
              [#1] {#Parameter (.i64_-# 2 id')}}
             (self_id? id))}
           (.i64_-# (.i64_-# depth id) 0))
          
          ... Recur
          {#Nominal name parameters}
          {#Nominal name (list#each (__adjusted_quantified_type__ permission depth)
                                    parameters)}

          {#Sum left right}
          {#Sum (__adjusted_quantified_type__ permission depth left)
                (__adjusted_quantified_type__ permission depth right)}
          
          {#Product left right}
          {#Product (__adjusted_quantified_type__ permission depth left)
                    (__adjusted_quantified_type__ permission depth right)}
          
          {#Function input output}
          {#Function (__adjusted_quantified_type__ permission depth input)
                     (__adjusted_quantified_type__ permission depth output)}
          
          {#UnivQ environment body}
          {#UnivQ environment
                  (__adjusted_quantified_type__ permission (next_level depth) body)}
          
          {#ExQ environment body}
          {#ExQ environment
                (__adjusted_quantified_type__ permission (next_level depth) body)}
          
          {#Apply parameter function}
          {#Apply (__adjusted_quantified_type__ permission depth parameter)
                  (__adjusted_quantified_type__ permission depth function)}

          ... Leave these alone.
          {#Named name anonymous} type
          {#Var id} type
          {#Ex id} type}
         type)

        _
        type}
       permission))

(def' .private (with_correct_quantification body)
      {#Function Code Code}
      (form$ {#Item (symbol$ [prelude "__adjusted_quantified_type__"])
                    {#Item (local$ ..quantification_level)
                           {#Item (nat$ 0)
                                  {#Item body
                                         {#End}}}}}))

(def' .private (with_quantification depth body)
      {#Function Nat {#Function Code Code}}
      ({g!level
        (let$ g!level
              (form$ {#Item (symbol$ [..prelude "i64_+#"])
                            {#Item g!level
                                   {#Item (nat$ (.as# Nat
                                                      (.int_*# +2
                                                               (.as# Int
                                                                     depth))))
                                          {#End}}}})
              body)}
       (local$ ..quantification_level)))

(def' .private (initialized_quantification? lux)
      {#Function Lux Bit}
      ({[..#info _ ..#source _ ..#current_module _ ..#modules _
         ..#scopes scopes ..#type_context _ ..#host _
         ..#seed _ ..#expected _ ..#location _ ..#extensions _
         ..#scope_type_vars _ ..#eval _]
        (list#mix (function'' [scope verdict]
                              ({[#1] #1
                                _ ({[..#scope_name _ ..#inner_scopes _ ..#captured _
                                     ..#locals [..#counter _
                                                ..#mappings locals]]
                                    (list#mix (function'' [local verdict]
                                                          ({[local _]
                                                            ({[#1] #1
                                                              _ (.text_=# ..quantification_level local)}
                                                             verdict)}
                                                           local))
                                              #0
                                              locals)}
                                   scope)}
                               verdict))
                  #0
                  scopes)}
       lux))

(def' .public All
      Macro
      (macro (_ tokens lux)
        ({{#Item [_ {#Form {#Item self_name args}}]
                 {#Item body {#End}}}
          {#Right [lux
                   {#Item ({raw
                            ({[#1] raw
                              [#0] (..quantified raw)}
                             (initialized_quantification? lux))}
                           ({{#End}
                             body

                             {#Item head tail}
                             (with_correct_quantification
                               (let$ self_name (quantified_type_parameter 0)
                                     ({[_ raw]
                                       raw}
                                      (list#mix (function'' [parameter offset,body']
                                                            ({[offset body']
                                                              [(.i64_+# 2 offset)
                                                               (let$ parameter (quantified_type_parameter (.i64_+# offset 1))
                                                                     (UnivQ$ body'))]}
                                                             offset,body'))
                                                [0 (with_quantification (list#size args)
                                                     body)]
                                                args))))}
                            args))
                          {#End}}]}
          
          _
          {#Left (wrong_syntax_error [..prelude "All"])}}
         tokens)))

(def' .public Ex
      Macro
      (macro (_ tokens lux)
        ({{#Item [_ {#Form {#Item self_name args}}]
                 {#Item body {#End}}}
          {#Right [lux
                   {#Item ({raw
                            ({[#1] raw
                              [#0] (..quantified raw)}
                             (initialized_quantification? lux))}
                           ({{#End}
                             body

                             {#Item head tail}
                             (with_correct_quantification
                               (let$ self_name (quantified_type_parameter 0)
                                     ({[_ raw]
                                       raw}
                                      (list#mix (function'' [parameter offset,body']
                                                            ({[offset body']
                                                              [(.i64_+# 2 offset)
                                                               (let$ parameter (quantified_type_parameter (.i64_+# offset 1))
                                                                     (ExQ$ body'))]}
                                                             offset,body'))
                                                [0 (with_quantification (list#size args)
                                                     body)]
                                                args))))}
                            args))
                          {#End}}]}
          
          _
          {#Left (wrong_syntax_error [..prelude "Ex"])}}
         tokens)))

(def' .public ->
      Macro
      (macro (_ tokens)
        ({{#Item output inputs}
          (meta#in {#Item (list#mix (.is# {#Function Code {#Function Code Code}}
                                          (function'' [i o] (variant$ {#Item (symbol$ [..prelude "#Function"]) {#Item i {#Item o {#End}}}})))
                                    output
                                    inputs)
                          {#End}})
          
          _
          (failure (wrong_syntax_error [..prelude "->"]))}
         (list#reversed tokens))))

(def' .public list
      Macro
      (macro (_ xs)
        (meta#in {#Item (list#mix |#Item| |#End| (list#reversed xs))
                        {#End}})))

(def' .private list#partial
      Macro
      (macro (_ xs)
        ({{#Item last init}
          (meta#in (list (list#mix |#Item| last init)))

          _
          (failure "Wrong syntax for list#partial")}
         (list#reversed xs))))

(def' .public Union
      Macro
      (macro (_ tokens)
        ({{#End}
          (meta#in (list (symbol$ [..prelude "Nothing"])))

          {#Item last prevs}
          (meta#in (list (list#mix (function'' [left right] (variant$ (list (symbol$ [..prelude "#Sum"]) left right)))
                                   last
                                   prevs)))}
         (list#reversed tokens))))

(def' .public Tuple
      Macro
      (macro (_ tokens)
        ({{#End}
          (meta#in (list (symbol$ [..prelude "Any"])))

          {#Item last prevs}
          (meta#in (list (list#mix (function'' [left right] (variant$ (list (symbol$ [..prelude "#Product"]) left right)))
                                   last
                                   prevs)))}
         (list#reversed tokens))))

(def' .private function'
      Macro
      (macro (_ tokens)
        (let'' [name tokens'] ({{#Item [[_ {#Symbol ["" name]}] tokens']}
                                [name tokens']

                                _
                                ["" tokens]}
                               tokens)
               ({{#Item [[_ {#Tuple args}] {#Item [body {#End}]}]}
                 ({{#End}
                   (failure "function' requires a non-empty arguments tuple.")
                   
                   {#Item [harg targs]}
                   (meta#in (list (form$ (list (tuple$ (list (local$ name)
                                                             harg))
                                               (list#mix (function'' [arg body']
                                                                     (form$ (list (tuple$ (list (local$ "")
                                                                                                arg))
                                                                                  body')))
                                                         body
                                                         (list#reversed targs))))))}
                  args)

                 _
                 (failure "Wrong syntax for function'")}
                tokens'))))

(def' .public Or
      Macro
      ..Union)

(def' .public And
      Macro
      ..Tuple)

(def' .private (pairs xs)
      (All (_ a) (-> ($ List a) ($ Maybe ($ List (Tuple a a)))))
      ({{#Item x {#Item y xs'}}
        ({{#Some tail}
          {#Some {#Item [x y] tail}}
          
          {#None}
          {#None}}
         (pairs xs'))

        {#End}
        {#Some {#End}}

        _
        {#None}}
       xs))

(def' .private let'
      Macro
      (macro (_ tokens)
        ({{#Item [_ {#Tuple bindings}] {#Item body {#End}}}
          ({{#Some bindings}
            (meta#in (list (list#mix (.is# (-> (Tuple Code Code) Code
                                               Code)
                                           (function' [binding body]
                                                      ({[label value]
                                                        (form$ (list (variant$ (list label body)) value))}
                                                       binding)))
                                     body
                                     (list#reversed bindings))))
            
            {#None}
            (failure "Wrong syntax for let'")}
           (pairs bindings))

          _
          (failure "Wrong syntax for let'")}
         tokens)))

(def' .private (any? p xs)
      (All (_ a)
        (-> (-> a Bit) ($ List a) Bit))
      ({{#End}
        #0

        {#Item x xs'}
        ({[#1] #1
          [#0] (any? p xs')}
         (p x))}
       xs))

(def' .private (with_location @ content)
      (-> Location Code Code)
      (let' [[module line column] @]
            (tuple$ (list (tuple$ (list (text$ module) (nat$ line) (nat$ column)))
                          content))))

(def' .private (untemplated_list tokens)
      (-> ($ List Code) Code)
      ({{#End}
        |#End|

        {#Item token tokens'}
        (|#Item| token (untemplated_list tokens'))}
       tokens))

(def' .private (list#composite xs ys)
      (All (_ a) (-> ($ List a) ($ List a) ($ List a)))
      (list#mix (function' [head tail] {#Item head tail})
                ys
                (list#reversed xs)))

(def' .private (right_associativity op a1 a2)
      (-> Code Code Code Code)
      ({[_ {#Form parts}]
        (form$ (list#composite parts (list a1 a2)))

        _
        (form$ (list op a1 a2))}
       op))

(def' .private (function#flipped func)
      (All (_ a b c)
        (-> (-> a b c) (-> b a c)))
      (function' [right left]
                 (func left right)))

(def' .public left
      Macro
      (macro (_ tokens)
        ({{#Item op tokens'}
          ({{#Item first nexts}
            (meta#in (list (list#mix (function#flipped (right_associativity op)) first nexts)))

            _
            (failure (wrong_syntax_error [..prelude "left"]))}
           tokens')
          
          _
          (failure (wrong_syntax_error [..prelude "left"]))}
         tokens)))

(def' .public right
      Macro
      (macro (_ tokens)
        ({{#Item op tokens'}
          ({{#Item last prevs}
            (meta#in (list (list#mix (right_associativity op) last prevs)))

            _
            (failure (wrong_syntax_error [..prelude "right"]))}
           (list#reversed tokens'))
          
          _
          (failure (wrong_syntax_error [..prelude "right"]))}
         tokens)))

(def' .public all Macro ..right)

... (type (Monad m)
...   (Interface
...    (is (All (_ a) (-> a (m a)))
...        #in)
...    (is (All (_ a b) (-> (-> a (m b)) (m a) (m b)))
...        #then)))
(.def# Monad
       (.is# Type
             {#Named [..prelude "Monad"]
                     (All (_ !)
                       (Tuple (All (_ a)
                                (-> a ($ ! a)))
                              (All (_ a b)
                                (-> (-> a ($ ! b))
                                    (-> ($ ! a) ($ ! b))))))})
       #0)

(.def# monad_slots
       (.is# {#Apply Symbol List}
             {#Item [..prelude "#in"]
                    {#Item [..prelude "#then"]
                           {#End}}})
       #0)
(.def# #in (slot [{#Some [0 #0 ..monad_slots]} Monad]) .private)
(.def# #then (slot [{#Some [0 #1 ..monad_slots]} Monad]) .private)

(def' .private maybe#monad
      ($ Monad Maybe)
      [#in
       (function' [x] {#Some x})
       
       #then
       (function' [f ma]
                  ({{#None}
                    {#None}
                    
                    {#Some a}
                    (f a)}
                   ma))])

(def' .private meta#monad
      ($ Monad Meta)
      [#in
       (function' [x]
                  (function' [state]
                             {#Right state x}))
       
       #then
       (function' [f ma]
                  (function' [state]
                             ({{#Left msg}
                               {#Left msg}

                               {#Right [state' a]}
                               (f a state')}
                              (ma state))))])

(def' .private do
      Macro
      (macro (_ tokens)
        ({{#Item monad {#Item [_ {#Tuple bindings}] {#Item body {#End}}}}
          ({{#Some bindings}
            (let' [g!in (local$ "in")
                   g!then (local$ " then ")
                   body' (list#mix (.is# (-> (Tuple Code Code) Code Code)
                                         (function' [binding body']
                                                    (let' [[var value] binding]
                                                          ({[_ {#Symbol [module short]}]
                                                            ({""
                                                              (form$ (list g!then
                                                                           (form$ (list (tuple$ (list (local$ "") var)) body'))
                                                                           value))

                                                              _
                                                              (form$ (list var value body'))}
                                                             module)
                                                            

                                                            _
                                                            (form$ (list g!then
                                                                         (form$ (list (tuple$ (list (local$ "") var)) body'))
                                                                         value))}
                                                           var))))
                                   body
                                   (list#reversed bindings))]
                  (meta#in (list (form$ (list (variant$ (list (tuple$ (list g!in g!then))
                                                              body'))
                                              monad)))))
            
            {#None}
            (failure "Wrong syntax for do")}
           (pairs bindings))

          _
          (failure "Wrong syntax for do")}
         tokens)))

(def' .private (monad#each m f xs)
      (All (_ m a b)
        (-> ($ Monad m)
            (-> a ($ m b))
            ($ List a)
            ($ m ($ List b))))
      (let' [[..#in in ..#then _] m]
            ({{#End}
              (in {#End})
              
              {#Item x xs'}
              (do m
                [y (f x)
                 ys (monad#each m f xs')]
                (in {#Item y ys}))}
             xs)))

(def' .private (monad#each#meta $ items)
      (All (_ input output)
        (-> (-> input
                ($ Meta output))
            (-> ($ List input)
                ($ Meta ($ List output)))))
      (function' [lux]
                 ((.is# (All (_ input output)
                          (-> Lux (-> input ($ Meta output)) ($ List input) ($ List output)
                              ($ Either Text (And Lux ($ List output)))))
                        (function' again [lux $ items output]
                                   ({{#End}
                                     {#Right [lux (list#reversed output)]}
                                     
                                     {#Item head tail}
                                     ({{#Right [lux head]}
                                       (again lux $ tail {#Item head output})

                                       {#Left failure}
                                       {#Left failure}}
                                      ($ head lux))}
                                    items)))
                  lux
                  $
                  items
                  {#End})))

(def' .private (monad#mix m f y xs)
      (All (_ m a b)
        (-> ($ Monad m)
            (-> a b ($ m b))
            b
            ($ List a)
            ($ m b)))
      (let' [[..#in in ..#then _] m]
            ({{#End}
              (in y)
              
              {#Item x xs'}
              (do m
                [y' (f x y)]
                (monad#mix m f y' xs'))}
             xs)))

(def' .public if
      Macro
      (macro (_ tokens)
        ({{#Item test {#Item then {#Item else {#End}}}}
          (meta#in (list (form$ (list (variant$ (list (bit$ #1)  then
                                                      (bit$ #0) else))
                                      test))))

          _
          (failure (wrong_syntax_error [..prelude "if"]))}
         tokens)))

(def' .private Property_List
      Type
      (All (_ a) ($ List (Tuple Text a))))

(def' .private (property#value k property_list)
      (All (_ a)
        (-> Text ($ Property_List a) ($ Maybe a)))
      ({{#Item [[k' v] property_list']}
        (if (text#= k k')
          {#Some v}
          (property#value k property_list'))

        {#End}
        {#None}}
       property_list))

(def' .private (property#with k v property_list)
      (All (_ a)
        (-> Text a ($ Property_List a) ($ Property_List a)))
      ({{#Item [k' v'] property_list'}
        (if (text#= k k')
          (list#partial [k v] property_list')
          (list#partial [k' v'] (property#with k v property_list')))

        {#End}
        (list [k v])}
       property_list))

(def' .private (global_symbol full_name state)
      (-> Symbol ($ Meta Symbol))
      (let' [[module name] full_name
             [..#info info ..#source    source  ..#current_module _ ..#modules modules
              ..#scopes scopes ..#type_context types    ..#host    host
              ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
              ..#scope_type_vars scope_type_vars ..#eval _eval] state]
            ({{#Some [..#module_hash _ ..#module_aliases _ ..#definitions definitions ..#imports _ ..#module_state _]}
              ({{#Some [_ constant]}
                ({{#Definition _}
                  {#Right [state full_name]}

                  {#Alias real_name}
                  {#Right [state real_name]}

                  {#Default _}
                  {#Left (.text_composite# "Unknown definition: " (symbol#encoded full_name))}}
                 constant)

                {#None}
                {#Left (.text_composite# "Unknown definition: " (symbol#encoded full_name))}}
               (property#value name definitions))
              
              {#None}
              {#Left (.text_composite# "Unknown module: " module " @ " (symbol#encoded full_name))}}
             (property#value module modules))))

(def' .private (|List<Code>| expression)
      (-> Code Code)
      (let' [type (variant$ (list (symbol$ [..prelude "#Apply"])
                                  (symbol$ [..prelude "Code"])
                                  (symbol$ [..prelude "List"])))]
            (form$ (list (symbol$ [..prelude "is#"]) type expression))))

(def' .private (untemplated_text value)
      (-> Text Code)
      (with_location ..dummy_location
        (variant$ (list (symbol$ [..prelude "#Text"]) (text$ value)))))

(def' .public UnQuote
      Type
      {#Named [..prelude "UnQuote"]
              {#Nominal "#Macro/UnQuote" {#End}}})

(def' .public (unquote it)
      (-> Macro UnQuote)
      (.as# UnQuote it))

(def' .public (unquote_macro it)
      (-> UnQuote Macro')
      (.as# Macro' it))

(def' .public Spliced_UnQuote
      Type
      {#Named [..prelude "Spliced_UnQuote"]
              {#Nominal "#Macro/Spliced_UnQuote" {#End}}})

(def' .public (spliced_unquote it)
      (-> Macro Spliced_UnQuote)
      (.as# Spliced_UnQuote it))

(def' .public (spliced_unquote_macro it)
      (-> Spliced_UnQuote Macro')
      (.as# Macro' it))

(def' .private (list#one f xs)
      (All (_ a b)
        (-> (-> a ($ Maybe b)) ($ List a) ($ Maybe b)))
      ({{#End}
        {#None}

        {#Item x xs'}
        ({{#None}
          (list#one f xs')

          {#Some y}
          {#Some y}}
         (f x))}
       xs))

(def' .private (in_env name state)
      (-> Text Lux ($ Maybe Type))
      (let' [[..#info info ..#source    source  ..#current_module _ ..#modules modules
              ..#scopes scopes ..#type_context types    ..#host    host
              ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
              ..#scope_type_vars scope_type_vars ..#eval _eval] state]
            (list#one (.is# (-> Scope ($ Maybe Type))
                            (function' [env]
                                       (let' [[..#scope_name _
                                               ..#inner_scopes _
                                               ..#locals [..#counter _ ..#mappings locals]
                                               ..#captured _] env]
                                             (list#one (.is# (-> (Tuple Text (Tuple Type Any)) ($ Maybe Type))
                                                             (function' [it]
                                                                        (let' [[bname [type _]] it]
                                                                              (if (text#= name bname)
                                                                                {#Some type}
                                                                                {#None}))))
                                                       locals))))
                      scopes)))

(def' .private (available? expected_module current_module exported?)
      (-> Text ($ Maybe Text) Bit Bit)
      (if exported?
        #1
        ({{.#None}
          #0
          
          {.#Some current_module}
          (text#= expected_module current_module)}
         current_module)))

(def' .private (definition_value name state)
      (-> Symbol ($ Meta (Tuple Type Any)))
      (let' [[expected_module expected_short] name
             [..#info info
              ..#source source
              ..#current_module current_module
              ..#modules modules
              ..#scopes scopes
              ..#type_context types
              ..#host host
              ..#seed seed
              ..#expected expected
              ..#location location
              ..#extensions extensions
              ..#scope_type_vars scope_type_vars
              ..#eval _eval] state]
            ({{#None}
              {#Left (.text_composite# "Unknown definition: " (symbol#encoded name))}

              {#Some [..#definitions definitions
                      ..#module_hash _
                      ..#module_aliases _
                      ..#imports _
                      ..#module_state _]}
              ({{#None}
                {#Left (.text_composite# "Unknown definition: " (symbol#encoded name))}

                {#Some [exported? definition]}
                ({{#Alias real_name}
                  (definition_value real_name state)
                  
                  {#Definition [def_type def_value]}
                  (if (available? expected_module current_module exported?)
                    {#Right [state [def_type def_value]]}
                    {#Left (.text_composite# "Unavailable definition: " (symbol#encoded name))})

                  {#Default _}
                  {#Left (.text_composite# "Unknown definition: " (symbol#encoded name))}}
                 definition)}
               (property#value expected_short definitions))}
             (property#value expected_module modules))))

(def' .private (global_value global lux)
      (-> Symbol ($ Meta ($ Maybe (Tuple Type Any))))
      (let' [[module short] global]
            ({{#Right [lux' type,value]}
              {#Right [lux' {#Some type,value}]}
              
              {#Left error}
              {#Right [lux {#None}]}}
             ({"" ({{#None}
                    (definition_value global lux)
                    
                    {#Some _}
                    {#Left (.text_composite# "Not a global value: " (symbol#encoded global))}}
                   (in_env short lux))

               _
               (definition_value global lux)}
              module))))

(def' .private (and' left right)
      (-> Bit Bit Bit)
      (if left
        right
        #0))

(def' .private (symbol#= left right)
      (-> Symbol Symbol Bit)
      (let' [[moduleL shortL] left
             [moduleR shortR] right]
            (all and'
                 (text#= moduleL moduleR)
                 (text#= shortL shortR))))

(def' .private (every? ?)
      (All (_ a)
        (-> (-> a Bit) ($ List a) Bit))
      (list#mix (function' [_2 _1] (if _1 (? _2) #0)) #1))

(def' .private (zipped_2 xs ys)
      (All (_ a b)
        (-> ($ List a) ($ List b) ($ List (Tuple a b))))
      ({{#Item x xs'}
        ({{#Item y ys'}
          (list#partial [x y] (zipped_2 xs' ys'))

          _
          (list)}
         ys)
        
        _
        (list)}
       xs))

(def' .private (type#= left right)
      (-> Type Type Bit)
      ({[{#Nominal nameL parametersL} {#Nominal nameR parametersR}]
        (all and'
             (text#= nameL nameR)
             (.i64_=# (list#size parametersL) (list#size parametersR))
             (every? (function' [l,r] (let' [[itL itR] l,r] (type#= itL itR)))
                     (zipped_2 parametersL parametersR)))

        [{#Sum leftL rightL} {#Sum leftR rightR}]
        (all and'
             (type#= leftL leftR)
             (type#= rightL rightR))

        [{#Product leftL rightL} {#Product leftR rightR}]
        (all and'
             (type#= leftL leftR)
             (type#= rightL rightR))

        [{#Function leftL rightL} {#Function leftR rightR}]
        (all and'
             (type#= leftL leftR)
             (type#= rightL rightR))

        [{#Apply leftL rightL} {#Apply leftR rightR}]
        (all and'
             (type#= leftL leftR)
             (type#= rightL rightR))

        [{#Parameter idL} {#Parameter idR}]
        (.i64_=# idL idR)

        [{#Var idL} {#Var idR}]
        (.i64_=# idL idR)

        [{#Ex idL} {#Ex idR}]
        (.i64_=# idL idR)

        [{#UnivQ envL bodyL} {#UnivQ envR bodyR}]
        (all and'
             (.i64_=# (list#size envL) (list#size envR))
             (every? (function' [l,r] (let' [[itL itR] l,r] (type#= itL itR)))
                     (zipped_2 envL envR))
             (type#= bodyL bodyR))

        [{#ExQ envL bodyL} {#ExQ envR bodyR}]
        (all and'
             (.i64_=# (list#size envL) (list#size envR))
             (every? (function' [l,r] (let' [[itL itR] l,r] (type#= itL itR)))
                     (zipped_2 envL envR))
             (type#= bodyL bodyR))

        [{#Named nameL anonL} {#Named nameR anonR}]
        (all and'
             (symbol#= nameL nameR)
             (type#= anonL anonR))

        _
        #0}
       [left right]))

(def' .private (one_expansion it)
      (-> ($ Meta ($ List Code)) ($ Meta Code))
      (do meta#monad
        [it it]
        ({{#Item it {#End}}
          (in it)

          _
          (failure "Must expand to 1 element.")}
         it)))

(def' .private (current_module_name state)
      ($ Meta Text)
      ({[..#info info ..#source    source  ..#current_module current_module ..#modules modules
         ..#scopes scopes ..#type_context types    ..#host    host
         ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
         ..#scope_type_vars scope_type_vars ..#eval _eval]
        ({{#Some module_name}
          {#Right [state module_name]}

          _
          {#Left "Cannot get the module name without a module!"}}
         current_module)}
       state))

(def' .private (normal name)
      (-> Symbol ($ Meta Symbol))
      ({["" name]
        (do meta#monad
          [module_name ..current_module_name]
          (in [module_name name]))

        _
        (meta#in name)}
       name))

(def' .private (untemplated_composite tag @composite untemplated replace? subst elements)
      (-> Text Location (-> Bit Text Code ($ Meta Code)) Bit Text ($ List Code)
          ($ Meta Code))
      (do meta#monad
        [.let' [cons (.is# (-> Code Code ($ Meta Code))
                           (function' [head tail]
                                      (do meta#monad
                                        [head (untemplated replace? subst head)]
                                        (in (|#Item| head tail)))))]
         output (if replace?
                  (monad#mix meta#monad
                             (function' [head tail]
                                        ({[@composite {#Form {#Item [@symbol {#Symbol global}] parameters}}]
                                          (do meta#monad
                                            [|global| (..normal global)
                                             ?type,value (global_value |global|)]
                                            ({{#Some [type value]}
                                              (if (type#= Spliced_UnQuote type)
                                                (do meta#monad
                                                  [.let' [it (spliced_unquote_macro (.as# Spliced_UnQuote value))]
                                                   output (one_expansion (it {#Item tail parameters}))
                                                   .let' [[_ output] output]]
                                                  (in [@composite output]))
                                                (cons head tail))
                                              
                                              {#None}
                                              (cons head tail)}
                                             ?type,value))

                                          _
                                          (cons head tail)}
                                         head))
                             |#End|
                             (list#reversed elements))
                  (do meta#monad
                    [=elements (monad#each#meta (untemplated replace? subst) elements)]
                    (in (untemplated_list =elements))))
         .let' [[_ output'] (with_location ..dummy_location
                              (variant$ (list (symbol$ [..prelude tag]) output)))]]
        (in [@composite output'])))

(def' .private untemplated_form
      (-> Location (-> Bit Text Code ($ Meta Code)) Bit Text ($ List Code)
          ($ Meta Code))
      (untemplated_composite "#Form"))

(def' .private untemplated_variant
      (-> Location (-> Bit Text Code ($ Meta Code)) Bit Text ($ List Code)
          ($ Meta Code))
      (untemplated_composite "#Variant"))

(def' .private untemplated_tuple
      (-> Location (-> Bit Text Code ($ Meta Code)) Bit Text ($ List Code)
          ($ Meta Code))
      (untemplated_composite "#Tuple"))

(def' .private (untemplated replace? subst token)
      (-> Bit Text Code ($ Meta Code))
      ({[_ [@token {#Bit value}]]
        (meta#in (with_location ..dummy_location
                   (variant$ (list (symbol$ [..prelude "#Bit"]) (bit$ value)))))

        [_ [@token {#Nat value}]]
        (meta#in (with_location ..dummy_location
                   (variant$ (list (symbol$ [..prelude "#Nat"]) (nat$ value)))))

        [_ [@token {#Int value}]]
        (meta#in (with_location ..dummy_location
                   (variant$ (list (symbol$ [..prelude "#Int"]) (int$ value)))))

        [_ [@token {#Rev value}]]
        (meta#in (with_location ..dummy_location
                   (variant$ (list (symbol$ [..prelude "#Rev"]) (rev$ value)))))
        
        [_ [@token {#Frac value}]]
        (meta#in (with_location ..dummy_location
                   (variant$ (list (symbol$ [..prelude "#Frac"]) (frac$ value)))))

        [_ [@token {#Text value}]]
        (meta#in (untemplated_text value))

        [#1 [@token {#Symbol [module name]}]]
        (do meta#monad
          [real_name ({""
                       (if (text#= "" subst)
                         (in [module name])
                         (global_symbol [subst name]))

                       _
                       (in [module name])}
                      module)
           .let' [[module name] real_name]]
          (meta#in (with_location [module 0 0]
                     (variant$ (list (symbol$ [..prelude "#Symbol"]) (tuple$ (list (text$ module) (text$ name))))))))

        [#0 [@token {#Symbol [module name]}]]
        (meta#in (with_location @token
                   (variant$ (list (symbol$ [..prelude "#Symbol"]) (tuple$ (list (text$ module) (text$ name)))))))

        [#1 [@composite {#Form {#Item [@symbol {#Symbol global}] parameters}}]]
        (do meta#monad
          [|global| (..normal global)
           ?type,value (global_value |global|)]
          ({{#Some [type value]}
            (if (type#= UnQuote type)
              (do meta#monad
                [.let' [it (unquote_macro (.as# UnQuote value))]
                 output (one_expansion (it parameters))
                 .let' [[_ output] output]]
                (in [@composite output]))
              (untemplated_form @composite untemplated replace? subst {#Item [@symbol {#Symbol global}] parameters}))
            
            {#None}
            (untemplated_form @composite untemplated replace? subst {#Item [@symbol {#Symbol global}] parameters})}
           ?type,value))

        [_ [@composite {#Form elements}]]
        (untemplated_form @composite untemplated replace? subst elements)

        [_ [@composite {#Variant elements}]]
        (untemplated_variant @composite untemplated replace? subst elements)

        [_ [@composite {#Tuple elements}]]
        (untemplated_tuple @composite untemplated replace? subst elements)}
       [replace? token]))

(def' .public Nominal
      Macro
      (macro (_ tokens)
        ({{#Item [_ {#Text class_name}] {#End}}
          (meta#in (list (variant$ (list (symbol$ [..prelude "#Nominal"]) (text$ class_name) |#End|))))

          {#Item [_ {#Text class_name}] {#Item [_ {#Tuple params}] {#End}}}
          (meta#in (list (variant$ (list (symbol$ [..prelude "#Nominal"]) (text$ class_name) (untemplated_list params)))))

          _
          (failure (wrong_syntax_error [..prelude "Nominal"]))}
         tokens)))

(def' .public `
      Macro
      (macro (_ tokens)
        ({{#Item template {#End}}
          (do meta#monad
            [current_module current_module_name
             =template (untemplated #1 current_module template)]
            (in (list (form$ (list (symbol$ [..prelude "is#"])
                                   (symbol$ [..prelude "Code"])
                                   =template)))))

          _
          (failure (wrong_syntax_error [..prelude "`"]))}
         tokens)))

(def' .public syntax_quote Macro `)

(def' .public `'
      Macro
      (macro (_ tokens)
        ({{#Item template {#End}}
          (do meta#monad
            [=template (untemplated #1 "" template)]
            (in (list (form$ (list (symbol$ [..prelude "is#"]) (symbol$ [..prelude "Code"]) =template)))))

          _
          (failure (wrong_syntax_error [..prelude "`'"]))}
         tokens)))

(def' .public partial_quote Macro `')

(def' .public '
      Macro
      (macro (_ tokens)
        ({{#Item template {#End}}
          (do meta#monad
            [=template (untemplated #0 "" template)]
            (in (list (form$ (list (symbol$ [..prelude "is#"]) (symbol$ [..prelude "Code"]) =template)))))

          _
          (failure (wrong_syntax_error [..prelude "'"]))}
         tokens)))

(def' .public literal_quote Macro ')

(def' .public ,
      UnQuote
      (..unquote
       (macro (_ tokens)
         ({{#Item it {#End}}
           (meta#in (list (form$ (list (symbol$ [..prelude "is#"])
                                       (symbol$ [..prelude "Code"])
                                       it))))

           _
           (failure (wrong_syntax_error [..prelude ","]))}
          tokens))))

(def' .public but UnQuote ,)

(def' .public ,'
      UnQuote
      (..unquote
       (macro (_ tokens)
         ({{#Item it {#End}}
           (do meta#monad
             [current_module ..current_module_name
              it (untemplated #0 current_module it)]
             (in (list it)))

           _
           (failure (wrong_syntax_error [..prelude ",'"]))}
          tokens))))

(def' .public literally UnQuote ,')

(def' .public ,*
      Spliced_UnQuote
      (let' [g!list#composite (form$ (list (symbol$ [..prelude "in_module#"])
                                           (text$ ..prelude)
                                           (symbol$ [..prelude "list#composite"])))]
            (..spliced_unquote
             (macro (_ tokens)
               ({{#Item tail {#Item it {#End}}}
                 (meta#in (list (form$ (list g!list#composite (|List<Code>| it) tail))))

                 _
                 (failure (wrong_syntax_error [..prelude ",*"]))}
                tokens)))))

(def' .public also Spliced_UnQuote ,*)

(def' .public |>
      Macro
      (macro (_ tokens)
        ({{#Item [init apps]}
          (meta#in (list (list#mix (.is# (-> Code Code Code)
                                         (function' [app acc]
                                                    ({[_ {#Variant parts}]
                                                      (variant$ (list#composite parts (list acc)))

                                                      [_ {#Tuple parts}]
                                                      (tuple$ (list#composite parts (list acc)))

                                                      [_ {#Form parts}]
                                                      (form$ (list#composite parts (list acc)))

                                                      _
                                                      (` ((, app) (, acc)))}
                                                     app)))
                                   init
                                   apps)))

          _
          (failure (wrong_syntax_error [..prelude "|>"]))}
         tokens)))

(def' .public <|
      Macro
      (macro (_ tokens)
        ({{#Item [init apps]}
          (meta#in (list (list#mix (.is# (-> Code Code Code)
                                         (function' [app acc]
                                                    ({[_ {#Variant parts}]
                                                      (variant$ (list#composite parts (list acc)))

                                                      [_ {#Tuple parts}]
                                                      (tuple$ (list#composite parts (list acc)))

                                                      [_ {#Form parts}]
                                                      (form$ (list#composite parts (list acc)))

                                                      _
                                                      (` ((, app) (, acc)))}
                                                     app)))
                                   init
                                   apps)))

          _
          (failure (wrong_syntax_error [..prelude "<|"]))}
         (list#reversed tokens))))

(def' .private meta#failure
      Macro
      (macro (_ tokens)
        ({{#Item 'error {#End}}
          (meta#in (list (` {.#Left (, 'error)})))

          _
          (failure (..wrong_syntax_error [..prelude "meta#failure"]))}
         tokens)))

(def' .private meta#return
      Macro
      (macro (_ tokens)
        ({{#Item 'lux {#Item 'term {#End}}}
          (meta#in (list (` {.#Right [(, 'lux) (, 'term)]})))

          _
          (failure (..wrong_syntax_error [..prelude "meta#return"]))}
         tokens)))

(def' .private meta#let
      Macro
      (macro (_ tokens)
        ({{#Item 'lux {#Item [_ {#Tuple {#Item 'binding {#Item 'term {#End}}}}]
                             {#Item 'body {#End}}}}
          (meta#in (list (` ({{.#Right [(, 'lux) (, 'binding)]}
                              (, 'body)

                              {.#Left (, 'lux)}
                              {.#Left (, 'lux)}}
                             ((, 'term) (, 'lux))))))

          _
          (failure (..wrong_syntax_error [..prelude "meta#let"]))}
         tokens)))

(def' .private (function#composite f g)
      (All (_ a b c)
        (-> (-> b c) (-> a b) (-> a c)))
      (function' [x] (f (g x))))

(def' .private (symbol_name x)
      (-> Code ($ Maybe Symbol))
      ({[_ {#Symbol sname}]
        {#Some sname}

        _
        {#None}}
       x))

(def' .private (symbol_short x)
      (-> Code ($ Maybe Text))
      ({[_ {#Symbol "" sname}]
        {#Some sname}

        _
        {#None}}
       x))

(def' .private (tuple_list tuple)
      (-> Code ($ Maybe ($ List Code)))
      ({[_ {#Tuple members}]
        {#Some members}

        _
        {#None}}
       tuple))

(def' .private (realized_template env template)
      (-> Replacement_Environment Code Code)
      ({[_ {#Symbol "" sname}]
        ({{#Some subst}
          subst

          _
          template}
         (..replacement sname env))

        [meta {#Form elems}]
        [meta {#Form (list#each (realized_template env) elems)}]

        [meta {#Tuple elems}]
        [meta {#Tuple (list#each (realized_template env) elems)}]

        [meta {#Variant elems}]
        [meta {#Variant (list#each (realized_template env) elems)}]

        _
        template}
       template))

(def' .private (high_bits value)
      (-> ($ I64 Any) I64)
      (.i64_right# 32 value))

(def' .private low_mask
      I64
      (|> 1 (.i64_left# 32) (.i64_-# 1)))

(def' .private (low_bits value)
      (-> ($ I64 Any) I64)
      (.i64_and# low_mask value))

(def' .private (n#< reference sample)
      (-> Nat Nat Bit)
      (let' [referenceH (high_bits reference)
             sampleH (high_bits sample)]
            (if (.int_<# referenceH sampleH)
              #1
              (if (.i64_=# referenceH sampleH)
                (.int_<# (low_bits reference)
                         (low_bits sample))
                #0))))

(def' .private (list#conjoint xs)
      (All (_ a)
        (-> ($ List ($ List a)) ($ List a)))
      (list#mix list#composite {#End} (list#reversed xs)))

(def' .public symbol
      Macro
      (macro (_ tokens)
        ({{#Item [_ {#Symbol [module name]}] {#End}}
          (meta#in (list (tuple$ (list (text$ module) (text$ name)))))

          _
          (failure (..wrong_syntax_error [..prelude "symbol"]))}
         tokens)))

(def' .public with_template
      Macro
      (macro (_ tokens)
        ({{#Item [[_ {#Tuple bindings}] {#Item [[_ {#Tuple templates}] data]}]}
          ({[{#Some bindings'} {#Some data'}]
            (let' [apply (.is# (-> Replacement_Environment ($ List Code))
                               (function' [env] (list#each (realized_template env) templates)))
                   num_bindings (list#size bindings')]
                  (if (every? (function' [size] (.i64_=# num_bindings size))
                              (list#each list#size data'))
                    (|> data'
                        (list#each (function#composite apply (replacement_environment bindings')))
                        list#conjoint
                        meta#in)
                    (failure (..wrong_syntax_error (symbol ..with_template)))))

            _
            (failure (..wrong_syntax_error (symbol ..with_template)))}
           [(monad#each maybe#monad symbol_short bindings)
            (monad#each maybe#monad tuple_list data)])

          _
          (failure (..wrong_syntax_error (symbol ..with_template)))}
         tokens)))

(def' .private (n#/ param subject)
      (-> Nat Nat Nat)
      (if (.int_<# +0 (.as# Int param))
        (if (n#< param subject)
          0
          1)
        (let' [quotient (|> subject
                            (.i64_right# 1)
                            (.int_/# (.as# Int param))
                            (.i64_left# 1))
               flat (.int_*# (.as# Int param)
                             (.as# Int quotient))
               remainder (.i64_-# flat subject)]
              (if (n#< param remainder)
                quotient
                (.i64_+# 1 quotient)))))

(def' .private (n#% param subject)
      (-> Nat Nat Nat)
      (let' [flat (.int_*# (.as# Int param)
                           (.as# Int (n#/ param subject)))]
            (.i64_-# flat subject)))

(def' .private (n#min left right)
      (-> Nat Nat Nat)
      (if (n#< right left)
        left
        right))

(def' .private (bit#encoded x)
      (-> Bit Text)
      (if x "#1" "#0"))

(def' .private (digit::format digit)
      (-> Nat Text)
      ({[0] "0"
        [1] "1" [2] "2" [3] "3"
        [4] "4" [5] "5" [6] "6"
        [7] "7" [8] "8" [9] "9"
        _ (.error# "@digit::format Undefined behavior.")}
       digit))

(def' .private (nat#encoded value)
      (-> Nat Text)
      ({[0] "0"
        _ (let' [loop (.is# (-> Nat Text Text)
                            (function' again [input output]
                                       (if (.i64_=# 0 input)
                                         output
                                         (again (n#/ 10 input)
                                                (.text_composite# (|> input (n#% 10) digit::format)
                                                                  output)))))]
                (loop value ""))}
       value))

(def' .private (int#abs value)
      (-> Int Int)
      (if (.int_<# +0 value)
        (.int_*# -1 value)
        value))

(def' .private (int#encoded value)
      (-> Int Text)
      (if (.i64_=# +0 value)
        "+0"
        (let' [sign (if (.int_<# value +0)
                      "+"
                      "-")]
              ((.is# (-> Int Text Text)
                     (function' again [input output]
                                (if (.i64_=# +0 input)
                                  (.text_composite# sign output)
                                  (again (.int_/# +10 input)
                                         (.text_composite# (|> input (.int_%# +10) (.as# Nat) digit::format)
                                                           output)))))
               (|> value (.int_/# +10) int#abs)
               (|> value (.int_%# +10) int#abs (.as# Nat) digit::format)))))

(def' .private (frac#encoded x)
      (-> Frac Text)
      (.f64_encoded# x))

(def' .public (not x)
      (-> Bit Bit)
      (if x #0 #1))

(def' .private (macro_type? type)
      (-> Type Bit)
      ({{#Named ["library/lux" "Macro"] {#Nominal "#Macro" {#End}}}
        #1

        _
        #0}
       type))

(def' .private (named_macro' modules current_module module name)
      (-> ($ List (Tuple Text Module))
          Text Text Text
          ($ Maybe Macro))
      (do maybe#monad
        [$module (property#value module modules)
         exported?,gdef (let' [[..#module_hash _ ..#module_aliases _ ..#definitions bindings ..#imports _ ..#module_state _] (.is# Module $module)]
                              (property#value name bindings))
         .let' [[exported? gdef] exported?,gdef]]
        ({{#Alias [r_module r_name]}
          (named_macro' modules current_module r_module r_name)

          {#Definition [def_type def_value]}
          (if (macro_type? def_type)
            (if exported?
              {#Some (.as# Macro def_value)}
              (if (text#= module current_module)
                {#Some (.as# Macro def_value)}
                {#None}))
            {#None})

          {#Default _}
          {#None}}
         (.is# Global gdef))))

(def' .private (named_macro full_name)
      (-> Symbol ($ Meta ($ Maybe Macro)))
      (<| (function' [lux])
          (meta#let lux [current_module current_module_name])
          (let' [[module name] full_name
                 [..#info info ..#source source ..#current_module _ ..#modules modules
                  ..#scopes   scopes   ..#type_context   types   ..#host host
                  ..#seed   seed ..#expected expected
                  ..#location location ..#extensions extensions
                  ..#scope_type_vars scope_type_vars ..#eval _eval] lux])
          (meta#return lux (named_macro' modules current_module module name))))

(def' .private (macro? name)
      (-> Symbol ($ Meta Bit))
      (<| (function' [lux])
          (meta#let lux [name (normal name)])
          (meta#let lux [output (named_macro name)])
          (meta#return lux ({{#Some _} #1
                             {#None}   #0}
                            output))))

(def' .private (list#interposed sep xs)
      (All (_ a)
        (-> a ($ List a) ($ List a)))
      ({{#End}
        xs

        {#Item [x {#End}]}
        xs

        {#Item [x xs']}
        (list#partial x sep (list#interposed sep xs'))}
       xs))

(def' .private (text#encoded original)
      (-> Text Text)
      (.text_composite# \'' original \''))

(def' .private (code#encoded code)
      (-> Code Text)
      ({[_ {#Bit value}]
        (bit#encoded value)

        [_ {#Nat value}]
        (nat#encoded value)

        [_ {#Int value}]
        (int#encoded value)

        [_ {#Rev value}]
        (.error# "@code#encoded Undefined behavior.")
        
        [_ {#Frac value}]
        (frac#encoded value)

        [_ {#Text value}]
        (text#encoded value)
        
        [_ {#Symbol [module name]}]
        (symbol#encoded [module name])
        
        [_ {#Form xs}]
        (.text_composite#
         "("
         (|> xs
             (list#each code#encoded)
             (list#interposed " ")
             list#reversed
             (list#mix text#composite ""))
         ")")
        
        [_ {#Tuple xs}]
        (.text_composite#
         "["
         (|> xs
             (list#each code#encoded)
             (list#interposed " ")
             list#reversed
             (list#mix text#composite ""))
         "]")
        
        [_ {#Variant xs}]
        (.text_composite#
         "{"
         (|> xs
             (list#each code#encoded)
             (list#interposed " ")
             list#reversed
             (list#mix text#composite ""))
         "}")}
       code))

(def' .private (single_expansion token)
      (-> Code ($ Meta ($ List Code)))
      ({[_ {#Form {#Item [_ {#Symbol name}] args}}]
        (<| (function' [lux])
            (meta#let lux [name' (normal name)])
            (meta#let lux [?macro (named_macro name')])
            ({{#Some macro}
              (((.as# Macro' macro) args) lux)
              
              {#None}
              (meta#return lux (list token))}
             ?macro))

        _
        (meta#in (list token))}
       token))

(def' .private (complete_expansion token)
      (-> Code ($ Meta ($ List Code)))
      ({[_ {#Form {#Item [_ {#Symbol name}] args}}]
        (<| (function' [lux])
            (meta#let lux [name' (normal name)])
            (meta#let lux [?macro (named_macro name')])
            ({{#Some macro}
              (<| (meta#let lux [top_level_expansion ((.as# Macro' macro) args)])
                  (meta#let lux [recursive_expansion (monad#each#meta complete_expansion top_level_expansion)])
                  (meta#return lux (list#conjoint recursive_expansion)))
              
              {#None}
              (meta#return lux (list token))}
             ?macro))

        _
        (meta#in (list token))}
       token))

(def' .public exec
      Macro
      (macro (_ tokens)
        ({{#Item value actions}
          (let' [dummy (local$ "")]
                (meta#in (list (list#mix (.is# (-> Code Code Code)
                                               (function' [pre post] (` ({(, dummy) (, post)} (, pre)))))
                                         value
                                         actions))))

          _
          (failure (..wrong_syntax_error (symbol ..exec)))}
         (list#reversed tokens))))

(def' .private (total_expansion' total_expansion @name name args)
      (-> (-> Code ($ Meta ($ List Code))) Location Symbol ($ List Code)
          ($ Meta ($ List Code)))
      (<| (function' [lux])
          (meta#let lux [name' (normal name)])
          (meta#let lux [?macro (named_macro name')])
          ({{#Some macro}
            (<| (meta#let lux [expansion ((.as# Macro' macro) args)])
                (meta#let lux [expansion' (monad#each#meta total_expansion expansion)])
                (meta#return lux (list#conjoint expansion')))
            
            {#None}
            (<| (meta#let lux [args' (monad#each#meta total_expansion args)])
                (meta#return lux (list (form$ {#Item [@name {#Symbol name}] (list#conjoint args')}))))}
           ?macro)))

(def' .private (in_module module meta)
      (All (_ a)
        (-> Text ($ Meta a) ($ Meta a)))
      (function' [lux]
                 ({[..#info info ..#source source
                    ..#current_module current_module ..#modules modules
                    ..#scopes scopes ..#type_context type_context
                    ..#host host ..#seed seed
                    ..#expected expected ..#location location
                    ..#extensions extensions ..#scope_type_vars scope_type_vars
                    ..#eval eval]
                   ({{#Left error}
                     {#Left error}
                     
                     {#Right [[..#info info' ..#source source'
                               ..#current_module _ ..#modules modules'
                               ..#scopes scopes' ..#type_context type_context'
                               ..#host host' ..#seed seed'
                               ..#expected expected' ..#location location'
                               ..#extensions extensions' ..#scope_type_vars scope_type_vars'
                               ..#eval eval']
                              output]}
                     {#Right [[..#info info' ..#source source'
                               ..#current_module current_module ..#modules modules'
                               ..#scopes scopes' ..#type_context type_context'
                               ..#host host' ..#seed seed'
                               ..#expected expected' ..#location location'
                               ..#extensions extensions' ..#scope_type_vars scope_type_vars'
                               ..#eval eval']
                              output]}}
                    (meta [..#info info ..#source source
                           ..#current_module {.#Some module} ..#modules modules
                           ..#scopes scopes ..#type_context type_context
                           ..#host host ..#seed seed
                           ..#expected expected ..#location location
                           ..#extensions extensions ..#scope_type_vars scope_type_vars
                           ..#eval eval]))}
                  lux)))

(def' .private (total_expansion syntax)
      (-> Code ($ Meta ($ List Code)))
      ({[_ {#Form {#Item head tail}}]
        ({[@name {#Symbol name}]
          (..total_expansion' total_expansion @name name tail)

          _
          (<| (function' [lux])
              (meta#let lux [members' (monad#each#meta total_expansion {#Item head tail})])
              (meta#return lux (list (form$ (list#conjoint members')))))}
         head)

        [_ {#Variant members}]
        (<| (function' [lux])
            (meta#let lux [members' (monad#each#meta total_expansion members)])
            (meta#return lux (list (variant$ (list#conjoint members')))))

        [_ {#Tuple members}]
        (<| (function' [lux])
            (meta#let lux [members' (monad#each#meta total_expansion members)])
            (meta#return lux (list (tuple$ (list#conjoint members')))))

        _
        (meta#in (list syntax))}
       syntax))

(def' .private (normal_type type)
      (-> Code ($ Meta Code))
      ({[_ {#Variant {#Item [_ {#Symbol symbol}] parts}}]
        (<| (function' [lux])
            (meta#let lux [parts (monad#each#meta normal_type parts)])
            (meta#return lux (` {(, (symbol$ symbol)) (,* parts)})))

        [_ {#Tuple members}]
        (<| (function' [lux])
            (meta#let lux [members (monad#each#meta normal_type members)])
            (meta#return lux (` (Tuple (,* members)))))

        [_ {#Form {#Item [_ {#Symbol ["library/lux" "in_module#"]}]
                         {#Item [_ {#Text module}]
                                {#Item type'
                                       {#End}}}}}]
        (<| (function' [lux])
            (meta#let lux [type' (normal_type type')])
            (meta#return lux (` (.in_module# (, (text$ module)) (, type')))))

        [_ {#Form {#Item [_ {#Symbol ["" ","]}] {#Item expression {#End}}}}]
        (meta#in expression)

        [_0 {#Form {#Item [_1 {#Variant {#Item binding {#Item body {#End}}}}]
                          {#Item value
                                 {#End}}}}]
        (<| (function' [lux])
            (meta#let lux [body (normal_type body)])
            (meta#return lux [_0 {#Form {#Item [_1 {#Variant {#Item binding {#Item body {#End}}}}]
                                               {#Item value
                                                      {#End}}}}]))

        [_0 {#Form {#Item [_1 {#Symbol ["library/lux" "__adjusted_quantified_type__"]}]
                          {#Item _permission
                                 {#Item _level
                                        {#Item body
                                               {#End}}}}}}]
        (<| (function' [lux])
            (meta#let lux [body (normal_type body)])
            (meta#return lux [_0 {#Form {#Item [_1 {#Symbol [..prelude "__adjusted_quantified_type__"]}]
                                               {#Item _permission
                                                      {#Item _level
                                                             {#Item body
                                                                    {#End}}}}}}]))

        [_ {#Form {#Item type_fn args}}]
        (<| (function' [lux])
            (meta#let lux [type_fn (normal_type type_fn)])
            (meta#let lux [args (monad#each#meta normal_type args)])
            (meta#return lux (list#mix (.is# (-> Code Code Code)
                                             (function' [arg type_fn] (` {.#Apply (, arg) (, type_fn)})))
                                       type_fn
                                       args)))

        _
        (meta#in type)}
       type))

(def' .private (with_quantification' body lux)
      (-> ($ Meta Code) ($ Meta Code))
      (let' [[..#info info/pre
              ..#source source/pre
              ..#current_module current_module/pre
              ..#modules modules/pre
              ..#scopes scopes/pre
              ..#type_context type_context/pre
              ..#host host/pre
              ..#seed seed/pre
              ..#expected expected/pre
              ..#location location/pre
              ..#extensions extensions/pre
              ..#scope_type_vars scope_type_vars/pre
              ..#eval eval/pre] lux]
            ({{..#Right [lux/post output]}
              (let' [[..#info info/post
                      ..#source source/post
                      ..#current_module current_module/post
                      ..#modules modules/post
                      ..#scopes scopes/post
                      ..#type_context type_context/post
                      ..#host host/post
                      ..#seed seed/post
                      ..#expected expected/post
                      ..#location location/post
                      ..#extensions extensions/post
                      ..#scope_type_vars scope_type_vars/post
                      ..#eval eval/post] lux/post]
                    {..#Right [[..#info info/post
                                ..#source source/post
                                ..#current_module current_module/post
                                ..#modules modules/post
                                ..#scopes scopes/pre
                                ..#type_context type_context/post
                                ..#host host/post
                                ..#seed seed/post
                                ..#expected expected/post
                                ..#location location/post
                                ..#extensions extensions/post
                                ..#scope_type_vars scope_type_vars/post
                                ..#eval eval/post]
                               output]})
              
              failure
              failure}
             (body [..#info info/pre
                    ..#source source/pre
                    ..#current_module current_module/pre
                    ..#modules modules/pre
                    ..#scopes (list#partial [#scope_name (list)
                                             #inner_scopes 0
                                             #locals [#counter 0
                                                      #mappings (list [..quantification_level [.Nat (.as# Nat -1)]])]
                                             #captured [#counter 0
                                                        #mappings (list)]]
                                            scopes/pre)
                    ..#type_context type_context/pre
                    ..#host host/pre
                    ..#seed seed/pre
                    ..#expected expected/pre
                    ..#location location/pre
                    ..#extensions extensions/pre
                    ..#scope_type_vars scope_type_vars/pre
                    ..#eval eval/pre]))))

(def' .public type_literal
      Macro
      (macro (type_literal tokens)
        ({{#Item type {#End}}
          (<| (function' [lux])
              (let' [initialized_quantification? (initialized_quantification? lux)])
              (if initialized_quantification?
                (<| (meta#let lux [type+ (total_expansion type)])
                    ({{#Item type' {#End}}
                      (<| (meta#let lux [type'' (normal_type type')])
                          (meta#return lux (list type'')))

                      _
                      (meta#failure "The expansion of the type-syntax had to yield a single element.")}
                     type+))
                (<| (meta#let lux [it (with_quantification'
                                        (one_expansion
                                         (type_literal tokens)))])
                    (meta#return lux (list (..quantified it))))))

          _
          (failure (..wrong_syntax_error (symbol ..type_literal)))}
         tokens)))

(def' .public is
      Macro
      (macro (_ tokens)
        ({{#Item type {#Item value {#End}}}
          (meta#in (list (` (.is# (..type_literal (, type))
                                  (, value)))))

          _
          (failure (..wrong_syntax_error (symbol ..is)))}
         tokens)))

(def' .public as
      Macro
      (macro (_ tokens)
        ({{#Item type {#Item value {#End}}}
          (meta#in (list (` (.as# (..type_literal (, type))
                                  (, value)))))

          _
          (failure (..wrong_syntax_error (symbol ..as)))}
         tokens)))

(def' .private (empty? xs)
      (All (_ a)
        (-> ($ List a) Bit))
      ({{#End} #1
        _      #0}
       xs))

(with_template [<name> <type> <value>]
  [(def' .private (<name> xy)
         (All (_ a b)
           (-> (Tuple a b) <type>))
         (let' [[x y] xy]
               <value>))]

  [product#left  a x]
  [product#right b y])

(def' .private (generated_symbol prefix state)
      (-> Text ($ Meta Code))
      ({[..#info info ..#source source ..#current_module _ ..#modules modules
         ..#scopes   scopes   ..#type_context   types   ..#host host
         ..#seed   seed ..#expected expected
         ..#location location ..#extensions extensions
         ..#scope_type_vars scope_type_vars ..#eval _eval]
        {#Right [..#info info ..#source source ..#current_module _ ..#modules modules
                 ..#scopes   scopes   ..#type_context   types   ..#host host
                 ..#seed   (.i64_+# 1 seed) ..#expected expected
                 ..#location location ..#extensions extensions
                 ..#scope_type_vars scope_type_vars ..#eval _eval]
                (local$ (.text_composite# "__gensym__" prefix (nat#encoded seed)))}}
       state))

(with_template [<name> <tag>]
  [(def' .private (<name> type)
         (type_literal (-> Type (List Type)))
         ({{<tag> left right}
           (list#partial left (<name> right))

           _
           (list type)}
          type))]

  [flat_variant #Sum]
  [flat_tuple   #Product]
  [flat_lambda  #Function]
  )

(def' .private (flat_application type)
      (type_literal (-> Type [Type (List Type)]))
      ({{#Apply head func'}
        (let' [[func tail] (flat_application func')]
              [func {#Item head tail}])

        _
        [type (list)]}
       type))

(def' .private (type#encoded type)
      (-> Type Text)
      ({{#Nominal name params}
        (.text_composite#
         "(Nominal " (text#encoded name)
         (|> params
             (list#each (function' [it] (|> it type#encoded (.text_composite# " "))))
             list#reversed
             (list#mix text#composite ""))
         ")")

        {#Sum _}
        (.text_composite# "{" (|> (flat_variant type) (list#each type#encoded) (list#interposed " ") list#reversed (list#mix text#composite "")) "}")
        
        {#Product _}
        (.text_composite# "[" (|> (flat_tuple type) (list#each type#encoded) (list#interposed " ") list#reversed (list#mix text#composite "")) "]")

        {#Function _}
        (.text_composite# "(-> " (|> (flat_lambda type) (list#each type#encoded) (list#interposed " ") list#reversed (list#mix text#composite "")) ")")

        {#Parameter id}
        (nat#encoded id)
        
        {#Var id}
        (.text_composite# "-" (nat#encoded id))
        
        {#Ex id}
        (.text_composite# "+" (nat#encoded id))
        
        {#UnivQ env body}
        (.text_composite# "(All " (type#encoded body) ")")

        {#ExQ env body}
        (.text_composite# "(Ex " (type#encoded body) ")")
        
        {#Apply _}
        (let' [[func args] (flat_application type)]
              (.text_composite#
               "(" (type#encoded func) " "
               (|> args (list#each type#encoded) (list#interposed " ") list#reversed (list#mix text#composite ""))
               ")"))
        
        {#Named name _}
        (symbol#encoded name)}
       type))

(def' .private (meta#try it)
      (type_literal (All (_ a) (-> (Meta a) (Meta (Either Text a)))))
      (function' [state]
                 ({{#Left error}
                   {#Right [state {#Left error}]}
                   
                   {#Right [state output]}
                   {#Right [state {#Right output}]}}
                  (it state))))

(def' .private (anonymous_type it)
      (-> Type Type)
      ({{#Named _ it}
        (anonymous_type it)
        
        _
        it}
       it))

(def' .private static'
      (type_literal (-> Bit Code (Meta Code)))
      (let' [simple_literal (is (-> Symbol (Meta Code))
                                (function' [name]
                                           (do meta#monad
                                             [type+value (meta#try (definition_value name))]
                                             ({{#Left error}
                                               (in (symbol$ name))
                                               
                                               {#Right [type value]}
                                               ({{#Nominal "#Bit" {#End}}
                                                 (in (bit$ (as Bit value)))

                                                 {#Nominal "#Frac" {#End}}
                                                 (in (frac$ (as Frac value)))

                                                 {#Nominal "#Text" {#End}}
                                                 (in (text$ (as Text value)))

                                                 {#Nominal "#I64" {#Item {#Nominal "#Nat" {#End}} {#End}}}
                                                 (in (nat$ (as Nat value)))

                                                 {#Nominal "#I64" {#Item {#Nominal "#Int" {#End}} {#End}}}
                                                 (in (int$ (as Int value)))

                                                 {#Nominal "#I64" {#Item {#Nominal "#Rev" {#End}} {#End}}}
                                                 (in (rev$ (as Rev value)))

                                                 {#Nominal "#Tag" {#End}}
                                                 (in (symbol$ name))
                                                 
                                                 {#Nominal "#Slot" {#End}}
                                                 (in (symbol$ name))
                                                 
                                                 _
                                                 (failure (.text_composite# "Invalid static value: " (symbol#encoded name)
                                                                            " : " (type#encoded type)))}
                                                (anonymous_type type))}
                                              type+value))))]
            (function' literal [only_global? token]
                       ({[_ {#Symbol [def_module def_name]}]
                         (if (text#= "" def_module)
                           (if only_global?
                             (meta#in (symbol$ [def_module def_name]))
                             (do meta#monad
                               [current_module current_module_name]
                               (simple_literal [current_module def_name])))
                           (simple_literal [def_module def_name]))

                         [meta {#Form parts}]
                         (do meta#monad
                           [=parts (monad#each#meta (literal only_global?) parts)]
                           (in [meta {#Form =parts}]))

                         [meta {#Variant parts}]
                         (do meta#monad
                           [=parts (monad#each#meta (literal only_global?) parts)]
                           (in [meta {#Variant =parts}]))

                         [meta {#Tuple parts}]
                         (do meta#monad
                           [=parts (monad#each#meta (literal only_global?) parts)]
                           (in [meta {#Tuple =parts}]))

                         _
                         ... TODO: Figure out why this doesn't work:
                         ... (meta#in token)
                         (meta#in token)}
                        token))))

(def' .public static
      Macro
      (macro (_ tokens)
        ({{#Item pattern {#End}}
          (do meta#monad
            [pattern' (static' #0 pattern)]
            (in (list pattern')))
          
          _
          (failure (..wrong_syntax_error (symbol ..static)))}
         tokens)))

(def' .public Pattern
      Type
      {#Named [..prelude "Pattern"]
              {#Nominal "#Macro/Pattern" {#End}}})

(def' .public (pattern it)
      (-> Macro Pattern)
      (.as# Pattern it))

(def' .public (pattern_macro it)
      (-> Pattern Macro')
      (.as# Macro' it))

(def' .private (when_expansion#macro when_expansion pattern body branches)
      (type_literal (-> (-> (List Code) (Meta (List Code)))
                        Code Code (List Code)
                        (Meta (List Code))))
      (do meta#monad
        [pattern (one_expansion (total_expansion pattern))
         pattern (static' #1 pattern)
         branches (when_expansion branches)]
        (in (list#partial pattern body branches))))

(def' .private (when_expansion branches)
      (type_literal (-> (List Code) (Meta (List Code))))
      ({{#Item [@composite {#Form {#Item [@symbol {#Symbol global}] parameters}}]
               {#Item body
                      branches'}}
        (do meta#monad
          [|global| (..normal global)
           ?type,value (global_value |global|)]
          ({{#Some [type value]}
            (if (type#= Pattern type)
              (do meta#monad
                [branches'' ((pattern_macro (.as# Pattern value))
                             (list#partial (form$ parameters) body branches'))]
                (when_expansion branches''))
              (when_expansion#macro when_expansion [@composite {#Form {#Item [@symbol {#Symbol global}] parameters}}] body branches'))
            
            {#None}
            (when_expansion#macro when_expansion [@composite {#Form {#Item [@symbol {#Symbol global}] parameters}}] body branches')}
           ?type,value))

        {#Item pattern {#Item body branches'}}
        (when_expansion#macro when_expansion pattern body branches')

        {#End}
        (meta#in (list))

        _
        (failure (.text_composite# "'when' expects an even number of tokens: "
                                   (|> branches
                                       (list#each code#encoded)
                                       (list#interposed " ")
                                       list#reversed
                                       (list#mix text#composite ""))))}
       branches))

(def' .public when
      Macro
      (macro (_ tokens)
        ({{#Item value branches}
          (do meta#monad
            [expansion (when_expansion branches)]
            (in (list (` ((, (variant$ expansion)) (, value))))))

          _
          (failure (..wrong_syntax_error (symbol ..when)))}
         tokens)))

(def' .private pattern#or
      Pattern
      (pattern
       (macro (_ tokens)
         (when tokens
           (list#partial [_ {#Form patterns}] body branches)
           (when patterns
             {#End}
             (failure "pattern#or cannot have 0 patterns")

             _
             (let' [pairs (|> patterns
                              (list#each (function' [pattern] (list pattern body)))
                              (list#conjoint))]
                   (meta#in (list#composite pairs branches))))
           _
           (failure "Wrong syntax for pattern#or")))))

(def' .private (symbol? code)
      (type_literal (-> Code Bit))
      (when code
        [_ {#Symbol _}]
        #1

        _
        #0))

(def' .public let
      Macro
      (macro (_ tokens)
        (when tokens
          (list [_ {#Tuple bindings}] body)
          (when (..pairs bindings)
            {#Some bindings}
            (|>  bindings
                 list#reversed
                 (list#mix (is (-> [Code Code] Code Code)
                               (function' [lr body']
                                          (let' [[l r] lr]
                                                (if (symbol? l)
                                                  (` ({(, l) (, body')} (, r)))
                                                  (` (when (, r) (, l) (, body')))))))
                           body)
                 list
                 meta#in)

            {#None}
            (failure "let requires an even number of parts"))

          _
          (failure (..wrong_syntax_error (symbol ..let))))))

(def' .public function
      Macro
      (macro (_ tokens)
        (when (is (Maybe [Text Code (List Code) Code])
                  (when tokens
                    (list [_ {#Form (list#partial [_ {#Symbol ["" name]}] head tail)}] body)
                    {#Some name head tail body}
                    
                    _
                    {#None}))
          {#Some g!name head tail body}
          (let [g!blank (local$ "")
                nest (is (-> Code (-> Code Code Code))
                         (function' [g!name]
                                    (function' [arg body']
                                               (if (symbol? arg)
                                                 (` ([(, g!name) (, arg)] (, body')))
                                                 (` ([(, g!name) (, g!blank)]
                                                     (.when (, g!blank) (, arg) (, body'))))))))]
            (meta#in (list (nest (..local$ g!name) head
                                 (list#mix (nest g!blank) body (list#reversed tail))))))

          {#None}
          (failure (..wrong_syntax_error (symbol ..function))))))

(def' .private Parser
      Type
      {#Named [..prelude "Parser"]
              (type_literal
               (All (_ a)
                 (-> (List Code)
                     (Maybe [(List Code) a]))))})

(def' .private (parsed parser tokens)
      (type_literal (All (_ a) (-> (Parser a) (List Code) (Maybe a))))
      (when (parser tokens)
        {#Some [(list) it]}
        {#Some it}

        _
        {#None}))

(def' .private (inP it tokens)
      (type_literal
       (All (_ a)
         (-> a (Parser a))))
      {#Some [tokens it]})

(def' .private (orP leftP rightP tokens)
      (type_literal
       (All (_ l r)
         (-> (Parser l)
             (Parser r)
             (Parser (Or l r)))))
      (when (leftP tokens)
        {#Some [tokens left]}
        {#Some [tokens {#Left left}]}

        _
        (when (rightP tokens)
          {#Some [tokens right]}
          {#Some [tokens {#Right right}]}

          _
          {#None})))

(def' .private (eitherP leftP rightP tokens)
      (type_literal
       (All (_ a)
         (-> (Parser a)
             (Parser a)
             (Parser a))))
      (when (leftP tokens)
        {#None}
        (rightP tokens)

        it
        it))

(def' .private (andP leftP rightP tokens)
      (type_literal
       (All (_ l r)
         (-> (Parser l)
             (Parser r)
             (Parser [l r]))))
      (do maybe#monad
        [left (leftP tokens)
         .let [[tokens left] left]
         right (rightP tokens)
         .let [[tokens right] right]]
        (in [tokens [left right]])))

(def' .private (afterP leftP rightP tokens)
      (type_literal
       (All (_ l r)
         (-> (Parser l)
             (Parser r)
             (Parser r))))
      (do maybe#monad
        [left (leftP tokens)
         .let [[tokens left] left]]
        (rightP tokens)))

(def' .private (someP itP tokens)
      (type_literal
       (All (_ a)
         (-> (Parser a)
             (Parser (List a)))))
      (when (itP tokens)
        {#Some [tokens head]}
        (do maybe#monad
          [it (someP itP tokens)
           .let [[tokens tail] it]]
          (in [tokens (list#partial head tail)]))

        {#None}
        {#Some [tokens (list)]}))

(def' .private (manyP itP tokens)
      (type_literal
       (All (_ a)
         (-> (Parser a)
             (Parser (List a)))))
      (do maybe#monad
        [it (itP tokens)
         .let [[tokens head] it]
         it (someP itP tokens)
         .let [[tokens tail] it]]
        (in [tokens (list#partial head tail)])))

(def' .private (maybeP itP tokens)
      (type_literal
       (All (_ a)
         (-> (Parser a)
             (Parser (Maybe a)))))
      (when (itP tokens)
        {#Some [tokens it]}
        {#Some [tokens {#Some it}]}

        {#None}
        {#Some [tokens {#None}]}))

(def' .private (tupleP itP tokens)
      (type_literal
       (All (_ a)
         (-> (Parser a) (Parser a))))
      (when tokens
        (list#partial [_ {#Tuple input}] tokens')
        (do maybe#monad
          [it (parsed itP input)]
          (in [tokens' it]))

        _
        {#None}))

(def' .private (formP itP tokens)
      (type_literal
       (All (_ a)
         (-> (Parser a) (Parser a))))
      (when tokens
        (list#partial [_ {#Form input}] tokens')
        (do maybe#monad
          [it (parsed itP input)]
          (in [tokens' it]))

        _
        {#None}))

(def' .private (bindingP tokens)
      (type_literal (Parser [Text Code]))
      (when tokens
        (list#partial [_ {#Symbol ["" name]}] value &rest)
        {#Some [&rest [name value]]}

        _
        {#None}))

(def' .private (endP tokens)
      (type_literal (Parser Any))
      (when tokens
        (list)
        {#Some [tokens []]}

        _
        {#None}))

(def' .private (anyP tokens)
      (type_literal (Parser Code))
      (when tokens
        (list#partial code tokens')
        {#Some [tokens' code]}

        _
        {#None}))

(def' .private (localP tokens)
      (type_literal (-> (List Code) (Maybe [(List Code) Text])))
      (when tokens
        (list#partial [_ {#Symbol ["" local]}] tokens')
        {#Some [tokens' local]}

        _
        {#None}))

(def' .private (symbolP tokens)
      (type_literal (-> (List Code) (Maybe [(List Code) Symbol])))
      (when tokens
        (list#partial [_ {#Symbol it}] tokens')
        {#Some [tokens' it]}

        _
        {#None}))

(with_template [<parser> <item_type> <item_parser>]
  [(def' .private (<parser> tokens)
         (type_literal (-> (List Code) (Maybe (List <item_type>))))
         (when tokens
           {#End}
           {#Some {#End}}

           _
           (do maybe#monad
             [% (<item_parser> tokens)
              .let' [[tokens head] %]
              tail (<parser> tokens)]
             (in {#Item head tail}))))]

  [parametersP Text localP]
  [enhanced_parametersP Code anyP]
  )

(with_template [<parser> <parameter_type> <parameters_parser>]
  [(def' .private (<parser> tokens)
         (type_literal (Parser [Text (List <parameter_type>)]))
         (when tokens
           (list#partial [_ {#Form local_declaration}] tokens')
           (do maybe#monad
             [% (localP local_declaration)
              .let' [[local_declaration name] %]
              parameters (<parameters_parser> local_declaration)]
             (in [tokens' [name parameters]]))
           
           _
           (do maybe#monad
             [% (localP tokens)
              .let' [[tokens' name] %]]
             (in [tokens' [name {#End}]]))))]

  [local_declarationP Text parametersP]
  [enhanced_local_declarationP Code enhanced_parametersP]
  )

(def' .private (export_policyP tokens)
      (type_literal (-> (List Code) [(List Code) Code]))
      (when tokens
        (list#partial candidate tokens')
        (when candidate
          [_ {#Bit it}]
          [tokens' candidate]
          
          [_ {#Symbol ["" _]}]
          [tokens (` .private)]
          
          [_ {#Symbol it}]
          [tokens' candidate]

          _
          [tokens (` .private)])

        _
        [tokens (` .private)]))

(with_template [<parser> <parameter_type> <local>]
  [(def' .private (<parser> tokens)
         (type_literal (-> (List Code) (Maybe [(List Code) [Code Text (List <parameter_type>)]])))
         (do maybe#monad
           [.let' [[tokens export_policy] (export_policyP tokens)]
            % (<local> tokens)
            .let' [[tokens [name parameters]] %]]
           (in [tokens [export_policy name parameters]])))]

  [declarationP Text local_declarationP]
  [enhanced_declarationP Code enhanced_local_declarationP]
  )

(def' .private (bodyP tokens)
      (type_literal (-> (List Code) (Maybe [(List Code) [(Maybe Code) Code]])))
      (when tokens
        ... TB
        (list#partial type body tokens')
        {#Some [tokens' [{#Some type} body]]}

        ... B
        (list#partial body tokens')
        {#Some [tokens' [{#None} body]]}

        _
        {#None}))

(def' .private (definitionP tokens)
      (type_literal (-> (List Code) (Maybe [Code Text (List Code) (Maybe Code) Code])))
      (do maybe#monad
        [% (enhanced_declarationP tokens)
         .let' [[tokens [export_policy name parameters]] %]
         % (bodyP tokens)
         .let' [[tokens [?type body]] %]
         _ (endP tokens)]
        (in [export_policy name parameters ?type body])))

(def' .public def
      Macro
      (macro (_ tokens)
        (when (definitionP tokens)
          {#Some [export_policy name parameters ?type body]}
          (let [body (when parameters
                       {#End}
                       body

                       _
                       (` (function ((, (..local$ name)) (,* parameters))
                            (, body))))
                body (when ?type
                       {#Some type}
                       (` (is (, type)
                              (, body)))
                       
                       {#None}
                       body)]
            (meta#in (list (` (.def# (, (..local$ name))
                                     (, body)
                                     (, export_policy))))))
          
          {#None}
          (failure (..wrong_syntax_error (symbol ..def))))))

(with_template [<name> <nullary> <form>]
  [(def .public <name>
     (macro (_ tokens)
       (when (list#reversed tokens)
         (list#partial last init)
         (meta#in (list (list#mix (is (-> Code Code Code)
                                      (function (_ pre post) (` <form>)))
                                  last
                                  init)))
         
         _
         (meta#in (list (` <nullary>))))))]

  [and #1 (if (, pre) (, post) #0)]
  [or  #0 (if (, pre) #1 (, post))]
  )

(def (index part text)
  (-> Text Text (Maybe Nat))
  (.text_index# 0 part text))

(def .public (panic! message)
  (-> Text Nothing)
  (.error# message))

(def maybe#else
  (macro (_ tokens state)
    (when tokens
      (list else maybe)
      (let [g!temp (is Code [dummy_location {#Symbol ["" ""]}])
            code (` (when (, maybe)
                      {.#Some (, g!temp)}
                      (, g!temp)

                      {.#None}
                      (, else)))]
        {#Right [state (list code)]})

      _
      {#Left (..wrong_syntax_error (symbol ..maybe#else))})))

(def (text#all_split_by splitter input)
  (-> Text Text (List Text))
  (when (..index splitter input)
    {#None}
    (list input)

    {#Some idx}
    (list#partial (.text_clip# 0 idx input)
                  (text#all_split_by splitter
                                     (let [after_offset (.i64_+# 1 idx)
                                           after_length (.i64_-# after_offset
                                                                 (.text_size# input))]
                                       (.text_clip# after_offset after_length input))))))

(def (item idx xs)
  (All (_ a)
    (-> Nat (List a) (Maybe a)))
  (when xs
    {#End}
    {#None}

    {#Item x xs'}
    (if (.i64_=# 0 idx)
      {#Some x}
      (item (.i64_-# 1 idx) xs'))))

... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
(def (reduced env type)
  (-> (List Type) Type Type)
  (when type
    {#Sum left right}
    {#Sum (reduced env left) (reduced env right)}

    {#Product left right}
    {#Product (reduced env left) (reduced env right)}
    
    {#Apply arg func}
    {#Apply (reduced env arg) (reduced env func)}

    {#UnivQ ?local_env ?local_def}
    (when ?local_env
      {#End}
      {#UnivQ env ?local_def}

      _
      type)

    {#ExQ ?local_env ?local_def}
    (when ?local_env
      {#End}
      {#ExQ env ?local_def}

      _
      type)

    {#Function ?input ?output}
    {#Function (reduced env ?input) (reduced env ?output)}

    {#Parameter idx}
    (when (item idx env)
      {#Some parameter}
      parameter

      _
      type)
    
    {#Named name type}
    (reduced env type)

    _
    type
    ))

(def (applied_type param type_fn)
  (-> Type Type (Maybe Type))
  (when type_fn
    {#UnivQ env body}
    {#Some (reduced (list#partial type_fn param env) body)}

    {#ExQ env body}
    {#Some (reduced (list#partial type_fn param env) body)}

    {#Apply A F}
    (do maybe#monad
      [type_fn* (applied_type A F)]
      (applied_type param type_fn*))

    {#Named name type}
    (applied_type param type)
    
    _
    {#None}))

(def (interface_methods type)
  (-> Type (Maybe (List Type)))
  (when type
    {#Product _}
    {#Some (flat_tuple type)}

    {#Apply arg func}
    (do maybe#monad
      [output (applied_type arg func)]
      (interface_methods output))

    {#UnivQ _ body}
    (interface_methods body)

    {#ExQ _ body}
    (interface_methods body)

    {#Named name type}
    (interface_methods type)

    {#Sum _}
    {#None}
    
    _
    {#Some (list type)}))

(def (module name)
  (-> Text (Meta Module))
  (function (_ state)
    (let [[..#info info ..#source    source  ..#current_module _ ..#modules modules
           ..#scopes scopes ..#type_context types    ..#host    host
           ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
           ..#scope_type_vars scope_type_vars ..#eval _eval] state]
      (when (property#value name modules)
        {#Some module}
        {#Right state module}

        _
        {#Left (.text_composite# "Unknown module: " name)}))))

(def (type_slot [module name])
  (-> Symbol (Meta [Bit Label]))
  (do meta#monad
    [=module (..module module)
     .let [[..#module_hash _
            ..#module_aliases _
            ..#definitions definitions
            ..#imports _
            ..#module_state _] =module]]
    (when (property#value name definitions)
      {#Some [exported {#Definition [type value]}]}
      (meta#in [exported (as Label value)])

      _
      (failure (.text_composite# "Unknown slot: " (symbol#encoded [module name]))))))

(def (slot_family expected_module expected_record)
  (-> Text Type (Meta (Maybe (List Symbol))))
  (do meta#monad
    [module (..module expected_module)
     actual_module ..current_module_name
     .let [[..#module_hash _
            ..#module_aliases _
            ..#definitions definitions
            ..#imports _
            ..#module_state _] module]]
    (in ((is (-> (List [Text [Bit Global]])
                 (Maybe (List Symbol)))
             (function (again remaining)
               (when remaining
                 {#Item [slot head] tail}
                 (when head
                   [exported? {#Definition [type value]}]
                   (if (and (type#= Slot type)
                            (or exported?
                                (text#= expected_module actual_module)))
                     (let [[label actual_record] (as Label value)]
                       (if (type#= expected_record actual_record)
                         (when label
                           {#Some [lefts right? family]}
                           {#Some family}
                           
                           {#None}
                           {#Some (list [expected_module slot])})
                         (again tail)))
                     (again tail))

                   _
                   (again tail))

                 {#End}
                 {#None})))
         definitions))))

(def (record_slots type)
  (-> Type (Meta (Maybe [(List Symbol) (List Type)])))
  (when type
    {#Apply arg func}
    (record_slots func)

    {#UnivQ env body}
    (record_slots body)

    {#ExQ env body}
    (record_slots body)

    {#Named [module name] unnamed}
    (do meta#monad
      [=module (..module module)
       .let [[..#module_hash _
              ..#module_aliases _
              ..#definitions definitions
              ..#imports _
              ..#module_state _] =module]]
      (when (property#value name definitions)
        {#Some [exported? {#Definition [type value]}]}
        (if (type#= Type type)
          (do meta#monad
            [slots (slot_family module (as Type value))]
            (when [slots (interface_methods (as Type value))]
              [{#Some slots} {#Some members}]
              (in {#Some [slots members]})

              _
              (record_slots unnamed)))
          (in {#None}))

        _
        (record_slots unnamed)))
    
    _
    (meta#in {#None})))

(def expected_type
  (Meta Type)
  (function (_ state)
    (let [[..#info info ..#source    source  ..#current_module _ ..#modules modules
           ..#scopes scopes ..#type_context types    ..#host    host
           ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
           ..#scope_type_vars scope_type_vars ..#eval _eval] state]
      (when expected
        {#Some type}
        {#Right state type}

        {#None}
        {#Left "Not expecting any type."}))))

(def .public implementation
  (macro (_ tokens)
    (do meta#monad
      [tokens' (monad#each#meta complete_expansion tokens)
       implementation_type ..expected_type
       tags+type (record_slots implementation_type)
       tags (is (Meta (List Symbol))
                (when tags+type
                  {#Some [tags _]}
                  (meta#in tags)

                  _
                  (failure (.text_composite# "No tags available for type: "
                                             (type#encoded implementation_type)))))
       .let [tag_mappings (is (List [Text Code])
                              (list#each (function (_ tag)
                                           [(product#right tag)
                                            (symbol$ tag)])
                                         tags))]
       members (monad#each#meta (is (-> Code (Meta (List Code)))
                                    (function (_ token)
                                      (when token
                                        [_ {#Form (list [_ {#Symbol [..prelude "def#"]}] [_ {#Symbol ["" slot_name]}] value export_policy)}]
                                        (when (property#value slot_name tag_mappings)
                                          {#Some tag}
                                          (in (list tag value))

                                          _
                                          (failure (.text_composite# "Unknown implementation member: " slot_name)))

                                        _
                                        (failure "Invalid implementation member."))))
                                (list#conjoint tokens'))]
      (in (list (tuple$ (list#conjoint members)))))))

(def (text#interposed separator parts)
  (-> Text (List Text) Text)
  (when parts
    {#End}
    ""
    
    {#Item head tail}
    (list#mix (function (_ right left)
                (.text_composite# left separator right))
              head
              tail)))

(def (function#identity value)
  (All (_ a)
    (-> a a))
  value)

(def (everyP itP tokens)
  (All (_ a)
    (-> (-> (List Code) (Maybe [(List Code) a]))
        (-> (List Code) (Maybe (List a)))))
  (when tokens
    {#Item _}
    (do maybe#monad
      [% (itP tokens)
       .let [[tokens' head] %]
       tail (when tokens'
              {#Item _}
              (everyP itP tokens')

              {#End}
              (in (list)))]
      (in (list#partial head tail)))

    {#End}
    {#Some (list)}))

(def (whenP tokens)
  (-> (List Code) (Maybe [(List Code) [Text Code]]))
  (when tokens
    (list#partial [_ {#Variant (list [_ {#Symbol ["" niladic]}])}] tokens')
    {#Some [tokens' [niladic (` .Any)]]}

    (list#partial [_ {#Variant (list#partial [_ {#Symbol ["" polyadic]}] whenT)}] tokens')
    {#Some [tokens' [polyadic (` (..Tuple (,* whenT)))]]}

    _
    {#None}))

(def .public Variant
  (macro (_ tokens)
    (when (everyP whenP tokens)
      {#Some whens}
      (meta#in (list (` (..Union (,* (list#each product#right whens))))
                     (variant$ (list#each (function (_ when)
                                            (text$ (product#left when)))
                                          whens))))
      
      {#None}
      (failure (..wrong_syntax_error (symbol ..Variant))))))

(def (slotP tokens)
  (-> (List Code) (Maybe [(List Code) [Text Code]]))
  (when tokens
    (list#partial [_ {#Symbol ["" slot]}] type tokens')
    {#Some [tokens' [slot type]]}

    _
    {#None}))

(def .public Record
  (macro (_ tokens)
    (when tokens
      (list [_ {#Tuple record}])
      (when (everyP slotP record)
        {#Some slots}
        (meta#in (list (` (..Tuple (,* (list#each product#right slots))))
                       (tuple$ (list#each (function (_ slot)
                                            (text$ (product#left slot)))
                                          slots))))
        
        {#None}
        (failure (..wrong_syntax_error (symbol ..Record))))

      _
      (failure (..wrong_syntax_error (symbol ..Record))))))

(def (typeP tokens)
  (-> (List Code) (Maybe [Code Text (List Text) Code]))
  (do maybe#monad
    [% (declarationP tokens)
     .let' [[tokens [export_policy name parameters]] %]
     % (anyP tokens)
     .let' [[tokens definition] %]
     _ (endP tokens)]
    (in [export_policy name parameters definition])))

(def (textP tokens)
  (-> (List Code) (Maybe [(List Code) Text]))
  (when tokens
    (list#partial [_ {#Text it}] tokens')
    {#Some [tokens' it]}

    _
    {#None}))

(def (type_declaration it)
  (-> Code (Meta (Tuple Code (Maybe (Either (List Text) (List Text))))))
  ({[_ {#Form {#Item [_ {#Symbol declarer}] parameters}}]
    (do meta#monad
      [declaration (single_expansion (form$ (list#partial (symbol$ declarer) parameters)))]
      (when declaration
        (list type [_ {#Variant tags}])
        (when (everyP textP tags)
          {#Some tags}
          (meta#in [type {#Some {#Left tags}}])
          
          {#None}
          (failure "Improper type-definition syntax"))

        (list type [_ {#Tuple slots}])
        (when (everyP textP slots)
          {#Some slots}
          (meta#in [type {#Some {#Right slots}}])
          
          {#None}
          (failure "Improper type-definition syntax"))

        (list type)
        (meta#in [it {#None}])

        _
        (failure "Improper type-definition syntax")))

    type
    (meta#in [type {#None}])}
   it))

(def (enumeration' idx xs)
  (All (_ a)
    (-> Nat (List a) (List [Nat a])))
  (when xs
    {#Item x xs'}
    {#Item [idx x] (enumeration' (.i64_+# 1 idx) xs')}

    {#End}
    {#End}))

(def (enumeration xs)
  (All (_ a)
    (-> (List a) (List [Nat a])))
  (enumeration' 0 xs))

(def (label_definitions module export_policy associated_type label_type family labels)
  (-> Text Code Code Code Code (List Text) (List Code))
  (when (list#reversed labels)
    (list single)
    (list (` (def (, export_policy) (, (local$ single))
               (<| (as (, label_type))
                   (is Label)
                   [{#None} (, associated_type)]))))

    (list#partial right lefts)
    (list#partial
     (` (def (, family)
          (List Symbol)
          (list (,* (list#each (function (_ it)
                                 (` [(, (text$ module)) (, (text$ it))]))
                               labels)))))
     (` (def (, export_policy) (, (local$ right))
          (<| (as (, label_type))
              (is Label)
              [{#Some [(, (nat$ (.i64_-# 1 (list#size lefts)))) #1 (, family)]} (, associated_type)])))
     (list#each (function (_ [lefts it])
                  (` (def (, export_policy) (, (local$ it))
                       (<| (as (, label_type))
                           (is Label)
                           [{#Some [(, (nat$ lefts)) #0 (, family)]} (, associated_type)]))))
                (enumeration (list#reversed lefts))))

    _
    (list)))

(def .public type
  (macro (_ tokens)
    (when (typeP tokens)
      {#Some [export_policy name args type_codes]}
      (do meta#monad
        [type+labels?? (..type_declaration type_codes)
         module_name current_module_name
         g!family (..generated_symbol "g!family")
         .let' [type_name (local$ name)
                [type labels??] type+labels??
                type' (is (Maybe Code)
                          (when args
                            {#End}
                            {#Some type}

                            _
                            {#Some (` (.All ((, type_name) (,* (list#each local$ args)))
                                        (, type)))}))]]
        (when type'
          {#Some type''}
          (let [typeC (` {.#Named [(, (text$ module_name))
                                   (, (text$ name))]
                                  (..type_literal (, type''))})]
            (in (when labels??
                  {#Some labels}
                  (list#partial (` (def (, export_policy) (, type_name)
                                     Type
                                     (, typeC)))
                                (when labels
                                  {#Left tags}
                                  (label_definitions module_name export_policy type_name (` Tag) g!family tags)
                                  
                                  {#Right slots}
                                  (label_definitions module_name export_policy type_name (` Slot) g!family slots)))
                  
                  _
                  (list (` (def (, export_policy) (, type_name)
                             Type
                             (, typeC)))))))

          {#None}
          (failure (..wrong_syntax_error (symbol ..type)))))

      {#None}
      (failure (..wrong_syntax_error (symbol ..type))))))

(type Referral
  [Symbol (List Code)])

(type Importation
  (Record
   [#import_name Text
    #import_alias (Maybe Text)
    #import_referrals (List Referral)]))

(def referral_parser
  (Parser Referral)
  (formP (andP symbolP (someP anyP))))

(def (referrals_parser aliased?)
  (-> Bit (Parser (List Referral)))
  (all eitherP
       (manyP referral_parser)
       (afterP endP
               (inP (if aliased?
                      (list [(symbol ..only) (list)])
                      (list))))
       (inP (list))))

(def (text#split_at' at x)
  (-> Nat Text [Text Text])
  [(.text_clip# 0 at x)
   (.text_clip# at (|> x .text_size# (.i64_-# at)) x)])

(def (text#split_by token sample)
  (-> Text Text (Maybe [Text Text]))
  (do ..maybe#monad
    [index (..index token sample)
     .let [[pre post'] (text#split_at' index sample)
           [_ post] (text#split_at' (.text_size# token) post')]]
    (in [pre post])))

(def (replaced pattern replacement template)
  (-> Text Text Text Text)
  ((is (-> Text Text Text)
       (function (again left right)
         (when (..text#split_by pattern right)
           {#Some [pre post]}
           (again (.text_composite# left pre replacement) post)

           {#None}
           (.text_composite# left right))))
   "" template))

(def (alias_stand_in index)
  (-> Nat Text)
  (.text_composite# "[" (nat#encoded index) "]"))

(def (module_alias context aliased)
  (-> (List Text) Text Text)
  (product#right
   (list#mix (function (_ replacement [index aliased])
               [(.i64_+# 1 index)
                (replaced (alias_stand_in index) replacement aliased)])
             [0 aliased]
             context)))

(def .public module_separator
  "/")

(def parallel_hierarchy_sigil
  "\")

(def (normal_parallel_path' hierarchy root)
  (-> Text Text Text)
  (when [(text#split_by ..module_separator hierarchy)
         (text#split_by ..parallel_hierarchy_sigil root)]
    [{#Some [_ hierarchy']}
     {#Some ["" root']}]
    (normal_parallel_path' hierarchy' root')

    _
    (when root
      "" hierarchy
      _ (.text_composite# root ..module_separator hierarchy))))

(def (normal_parallel_path hierarchy root)
  (-> Text Text (Maybe Text))
  (when (text#split_by ..parallel_hierarchy_sigil root)
    {#Some ["" root']}
    {#Some (normal_parallel_path' hierarchy root')}

    _
    {#None}))

(def (relative_ups relatives input)
  (-> Nat Text Nat)
  (when (.text_index# relatives ..module_separator input)
    {#None}
    relatives

    {#Some found}
    (if (.i64_=# relatives found)
      (relative_ups (.i64_+# 1 relatives) input)
      relatives)))

(def (list#after amount list)
  (All (_ a) (-> Nat (List a) (List a)))
  (when [amount list]
    (pattern#or [0 _]
                [_ {#End}])
    list

    [_ {#Item _ tail}]
    (list#after (.i64_-# 1 amount) tail)))

(def \n
  Text
  (.int_char# +10))

(def (absolute_module_name nested? relative_root module)
  (-> Bit Text Text (Meta Text))
  (when (relative_ups 0 module)
    0
    (meta#in (if nested?
               (.text_composite# relative_root ..module_separator module)
               module))
    
    relatives
    (let [parts (text#all_split_by ..module_separator relative_root)
          jumps (.i64_-# 1 relatives)]
      (if (n#< (list#size parts) jumps)
        (let [prefix (|> parts
                         list#reversed
                         (list#after jumps)
                         list#reversed
                         (text#interposed ..module_separator))
              clean (.text_clip# relatives (|> module .text_size# (.i64_-# relatives)) module)
              output (when (.text_size# clean)
                       0 prefix
                       _ (.text_composite# prefix ..module_separator clean))]
          (meta#in output))
        (failure (.text_composite# "Cannot climb the module hierarchy..." \n
                                   "Importing module: " module \n
                                   "   Relative Root: " relative_root \n))))))

(def (imports_parser nested? relative_root context imports)
  (-> Bit Text (List Text) (List Code) (Meta (List Importation)))
  (do meta#monad
    [imports' (monad#each#meta (is (-> Code (Meta (List Importation)))
                                   (function (_ token)
                                     (when token
                                       ... Nested
                                       [_ {#Tuple (list#partial [_ {#Symbol ["" module_name]}] extra)}]
                                       (do meta#monad
                                         [absolute_module_name (when (normal_parallel_path relative_root module_name)
                                                                 {#Some parallel_path}
                                                                 (in parallel_path)

                                                                 {#None}
                                                                 (..absolute_module_name nested? relative_root module_name))
                                          extra,referral (when (referrals_parser #0 extra)
                                                           {#Some extra,referral}
                                                           (in extra,referral)

                                                           {#None}
                                                           (failure ""))
                                          .let [[extra referral] extra,referral]
                                          sub_imports (imports_parser #1 absolute_module_name context extra)]
                                         (in (when referral
                                               {#End}
                                               sub_imports
                                               
                                               _
                                               (list#partial [#import_name absolute_module_name
                                                              #import_alias {#None}
                                                              #import_referrals referral]
                                                             sub_imports))))

                                       [_ {#Tuple (list#partial [_ {#Text alias}] [_ {#Symbol ["" module_name]}] extra)}]
                                       (do meta#monad
                                         [absolute_module_name (when (normal_parallel_path relative_root module_name)
                                                                 {#Some parallel_path}
                                                                 (in parallel_path)

                                                                 {#None}
                                                                 (..absolute_module_name nested? relative_root module_name))
                                          extra,referral (when (referrals_parser #1 extra)
                                                           {#Some extra,referral}
                                                           (in extra,referral)

                                                           {#None}
                                                           (failure ""))
                                          .let [[extra referral] extra,referral]
                                          .let [module_alias (..module_alias {#Item module_name context} alias)]
                                          sub_imports (imports_parser #1 absolute_module_name {#Item module_alias context} extra)]
                                         (in (when referral
                                               {#End}
                                               sub_imports
                                               
                                               _
                                               (list#partial [#import_name absolute_module_name
                                                              #import_alias {#Some module_alias}
                                                              #import_referrals referral]
                                                             sub_imports))))

                                       ... Unrecognized syntax.
                                       _
                                       (do meta#monad
                                         [current_module current_module_name]
                                         (failure (.text_composite# "Wrong syntax for import @ " current_module
                                                                    \n (code#encoded token)))))))
                               imports)]
    (in (list#conjoint imports'))))

(def (exported_definitions module state)
  (-> Text (Meta (List Text)))
  (let [[current_module modules] (when state
                                   [..#info info ..#source    source  ..#current_module current_module ..#modules modules
                                    ..#scopes scopes ..#type_context types    ..#host    host
                                    ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
                                    ..#scope_type_vars scope_type_vars ..#eval _eval]
                                   [current_module modules])]
    (when (property#value module modules)
      {#Some =module}
      (let [to_alias (list#each (is (-> [Text [Bit Global]]
                                        (List Text))
                                    (function (_ [name [exported? definition]])
                                      (when definition
                                        {#Alias _}
                                        (if exported?
                                          (list name)
                                          (list))

                                        {#Definition [def_type def_value]}
                                        (if exported?
                                          (list name)
                                          (list))

                                        {#Default _}
                                        (list))))
                                (let [[..#module_hash _ ..#module_aliases _ ..#definitions definitions ..#imports _ ..#module_state _] =module]
                                  definitions))]
        {#Right state (list#conjoint to_alias)})
      
      {#None}
      {#Left (.text_composite# "Unknown module: " (text#encoded module) \n
                               "Current module: " (when current_module
                                                    {#Some current_module}
                                                    (text#encoded current_module)

                                                    {#None}
                                                    "???") \n
                                                    "Known modules: " (|> modules
                                                                          (list#each (function (_ [name module])
                                                                                       (text$ name)))
                                                                          tuple$
                                                                          code#encoded))})
    ))

(def (list#only p xs)
  (All (_ a)
    (-> (-> a Bit) (List a) (List a)))
  (when xs
    {#End}
    (list)

    {#Item x xs'}
    (if (p x)
      {#Item x (list#only p xs')}
      (list#only p xs'))))

(def (is_member? whens name)
  (-> (List Text) Text Bit)
  (let [output (list#mix (function (_ when prev)
                           (or prev
                               (text#= when name)))
                         #0
                         whens)]
    output))

(def (test_referrals current_module imported_module all_defs referred_defs)
  (-> Text Text (List Text) (List Text) (Meta (List Any)))
  (monad#each#meta (is (-> Text (Meta Any))
                       (function (_ _def)
                         (if (is_member? all_defs _def)
                           (meta#in [])
                           (failure (.text_composite# _def " is not defined in module " imported_module " @ " current_module)))))
                   referred_defs))

(def (alias_definition imported_module def)
  (-> Text Text Code)
  (` (.def# (, (local$ def))
            (, (symbol$ [imported_module def]))
            .private)))

(def .public only
  (macro (_ tokens)
    (when (..parsed (all ..andP
                         ..textP
                         ..textP
                         ..textP
                         (..someP ..localP))
                    tokens)
      {.#Some [current_module imported_module import_alias actual]}
      (do meta#monad
        [expected (exported_definitions imported_module)
         _ (test_referrals current_module imported_module expected actual)]
        (in (list#each (..alias_definition imported_module) actual)))

      {.#None}
      (failure (..wrong_syntax_error (symbol ..only))))))

(def .public |>>
  (macro (_ tokens)
    (do meta#monad
      [g!_ (..generated_symbol "_")
       g!arg (..generated_symbol "arg")]
      (meta#in (list (` (function ((, g!_) (, g!arg)) (|> (, g!arg) (,* tokens)))))))))

(def .public <<|
  (macro (_ tokens)
    (do meta#monad
      [g!_ (..generated_symbol "_")
       g!arg (..generated_symbol "arg")]
      (meta#in (list (` (function ((, g!_) (, g!arg)) (<| (,* tokens) (, g!arg)))))))))

(def .public except
  (macro (_ tokens)
    (when (..parsed (all ..andP
                         ..textP
                         ..textP
                         ..textP
                         (..someP ..localP))
                    tokens)
      {.#Some [current_module imported_module import_alias actual]}
      (do meta#monad
        [expected (exported_definitions imported_module)
         _ (test_referrals current_module imported_module expected actual)]
        (in (|> expected
                (..list#only (|>> (is_member? actual) not))
                (list#each (..alias_definition imported_module)))))

      {.#None}
      (failure (..wrong_syntax_error (symbol ..except))))))

(def (definition_type name state)
  (-> Symbol Lux (Maybe Type))
  (let [[expected_module expected_short] name
        [..#info info ..#source    source  ..#current_module _ ..#modules modules
         ..#scopes scopes ..#type_context types    ..#host    host
         ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
         ..#scope_type_vars scope_type_vars ..#eval _eval] state]
    (when (property#value expected_module modules)
      {#None}
      {#None}

      {#Some [..#definitions definitions
              ..#module_hash _
              ..#module_aliases _
              ..#imports _
              ..#module_state _]}
      (when (property#value expected_short definitions)
        {#None}
        {#None}

        {#Some [exported? definition]}
        (when definition
          {#Alias real_name}
          (definition_type real_name state)
          
          {#Definition [def_type def_value]}
          {#Some def_type}

          {#Default _}
          {#None})))))

(def (type_variable idx bindings)
  (-> Nat (List [Nat (Maybe Type)]) (Maybe Type))
  (when bindings
    {#End}
    {#End}
    
    {#Item [var bound] bindings'}
    (if (.i64_=# idx var)
      bound
      (type_variable idx bindings'))))

(def (clean_type variables it)
  (-> (List [Nat (Maybe Type)]) Type Type)
  (when it
    {#Nominal name parameters}
    {#Nominal name (list#each (clean_type variables) parameters)}
    
    {#Sum left right}
    {#Sum (clean_type variables left)
          (clean_type variables right)}

    {#Product left right}
    {#Product (clean_type variables left)
              (clean_type variables right)}

    {#Function left right}
    {#Function (clean_type variables left)
               (clean_type variables right)}

    {#Apply left right}
    {#Apply (clean_type variables left)
            (clean_type variables right)}

    {#UnivQ environment unquantified}
    {#UnivQ (list#each (clean_type variables) environment)
            (clean_type variables unquantified)}
    
    {#ExQ environment unquantified}
    {#ExQ (list#each (clean_type variables) environment)
          (clean_type variables unquantified)}
    
    {#Named name anonymous}
    it

    {#Parameter _}
    it
    
    {#Ex _}
    it
    
    {#Var id}
    (when (type_variable id variables)
      {#None}
      it

      {#Some {#Var _}}
      it

      {#Some it}
      (clean_type variables it))))

(def (type_definition full_name)
  (-> Symbol (Meta Type))
  (do meta#monad
    [.let [[module name] full_name]
     current_module current_module_name]
    (function (_ compiler)
      (let [temp (is (Either Text [Lux Type])
                     (if (text#= "" module)
                       (when (in_env name compiler)
                         {#Some implementation_type}
                         {#Right [compiler implementation_type]}

                         _
                         (when (definition_type [current_module name] compiler)
                           {#Some implementation_type}
                           {#Right [compiler implementation_type]}

                           _
                           {#Left (.text_composite# "Unknown var: " (symbol#encoded full_name))}))
                       (when (definition_type full_name compiler)
                         {#Some implementation_type}
                         {#Right [compiler implementation_type]}

                         _
                         {#Left (.text_composite# "Unknown var: " (symbol#encoded full_name))})))]
        (when temp
          {#Right [compiler temp]}
          (let [[..#info _ ..#source _ ..#current_module _ ..#modules _
                 ..#scopes _ ..#type_context type_context ..#host _
                 ..#seed _ ..#expected _ ..#location _ ..#extensions extensions
                 ..#scope_type_vars _ ..#eval _eval] compiler
                 [..#ex_counter _ ..#var_counter _ ..#var_bindings var_bindings] type_context]
            {#Right [compiler (clean_type var_bindings temp)]})

          _
          temp)))))

(def (list#all choice items)
  (All (_ a b) (-> (-> a (Maybe b)) (List a) (List b)))
  (when items
    {#Item head tail}
    (when (choice head)
      {#Some head}
      {#Item head (list#all choice tail)}
      
      {#None}
      (list#all choice tail))
    
    {#End}
    {#End}))

(type Implementation_Interface
  [(List Symbol) (List Type)])

(def (open_layer alias [tags members])
  (-> Text Implementation_Interface (Meta [Code (List [Symbol Implementation_Interface])]))
  (do meta#monad
    [pattern (monad#each#meta (function (_ [slot slot_type])
                                (do meta#monad
                                  [.let [[_ slot_name] slot
                                         local ["" (..module_alias (list slot_name) alias)]]
                                   implementation (record_slots slot_type)]
                                  (in [(list (symbol$ slot)
                                             (symbol$ local))
                                       [local implementation]])))
                              (zipped_2 tags members))]
    (in [(|> pattern
             (list#each product#left)
             list#conjoint
             tuple$)
         (list#all (function (_ [_ [sub_binding sub_implementation]])
                     (do maybe#monad
                       [sub_implementation sub_implementation]
                       (in [sub_binding sub_implementation])))
                   pattern)])))

(def (open_layers alias interfaces body)
  (-> Text (List Implementation_Interface) Code (Meta [Code Code]))
  (do meta#monad
    [layer (monad#each#meta (open_layer alias) interfaces)
     .let [pattern (tuple$ (list#each product#left layer))
           next (|> layer
                    (list#each product#right)
                    list#conjoint)]]
    (when next
      {#End}
      (in [pattern body])

      _
      (do meta#monad
        [.let [sub_value (tuple$ (list#each (|>> product#left symbol$) next))]
         sub_pattern,sub_body (open_layers alias (list#each product#right next) body)
         .let [[sub_pattern sub_body] sub_pattern,sub_body]]
        (in [pattern (` (when (, sub_value)
                          (, sub_pattern)
                          (, sub_body)))])))))

(def .public open
  (pattern
   (macro (_ tokens)
     (when tokens
       (list#partial [_ {#Form (list [_ {#Text alias}])}] body branches)
       (do meta#monad
         [g!temp (..generated_symbol "temp")]
         (in (list#partial g!temp
                           (` (..when (, g!temp)
                                (..open (, g!temp) (, (text$ alias)))
                                (, body)))
                           branches)))

       (list#partial [_ {#Form (list [@temp_var {#Symbol name}] [_ {#Text alias}])}]
                     body
                     branches)
       (do meta#monad
         [init_type (type_definition name)
          implementation_evidence (record_slots init_type)]
         (when implementation_evidence
           {#None}
           (failure (.text_composite# "Can only 'open' implementations: " (type#encoded init_type)))

           {#Some tags,members}
           (do meta#monad
             [pattern,body (open_layers alias (list tags,members) body)
              .let [[pattern body] pattern,body]]
             (in (list#partial pattern body branches)))))

       _
       (failure (..wrong_syntax_error (symbol ..open)))))))

(def .public cond
  (macro (_ tokens)
    (when (list#reversed tokens)
      (list#partial else branches')
      (when (pairs branches')
        {#Some branches'}
        (meta#in (list (list#mix (is (-> [Code Code] Code Code)
                                     (function (_ branch else)
                                       (let [[then ?] branch]
                                         (` (if (, ?) (, then) (, else))))))
                                 else
                                 branches')))

        {#None}
        (failure "cond requires an uneven number of arguments."))
      
      _
      (failure (..wrong_syntax_error (symbol ..cond))))))

(type (Try value)
  (Variant
   {#Failure Text}
   {#Success value}))

(def (access_pattern g!_ g!output lefts right? members)
  (-> Code Code Nat Bit (List Type) (Try (List Code)))
  (when ((is (-> Nat (List Type) (List Code)
                 (List Code))
             (function (again index input output)
               (when input
                 (list#partial head tail)
                 (if (.i64_=# index (if right?
                                      (.i64_+# 1 lefts)
                                      lefts))
                   (list#reversed (list#partial g!output output))
                   (again (.i64_+# 1 index) tail (list#partial g!_ output)))

                 (list)
                 (list))))
         0 members (list))
    (list)
    {#Failure "Cannot synthesize access pattern."}

    pattern
    {#Success pattern}))

(def .public the
  (macro (_ tokens)
    (when tokens
      (list [_ {#Symbol slot'}] record)
      (do meta#monad
        [slot (normal slot')
         output (..type_slot slot)
         .let [[exported? [label' type]] output]]
        (when label'
          {.#None}
          (in (list record))
          
          {.#Some [lefts right? family]}
          (do meta#monad
            [g!_ (..generated_symbol "_")
             g!output (..generated_symbol "")
             .let [idx (if right?
                         (is Nat (.i64_+# 1 lefts))
                         lefts)
                   pattern (|> (enumeration family)
                               (list#each (is (-> [Nat Symbol] (List Code))
                                              (function (_ [r_idx slot])
                                                (list (symbol$ slot)
                                                      (if (.i64_=# idx r_idx)
                                                        g!output
                                                        g!_)))))
                               list#conjoint)]]
            (in (list (` ({[(,* pattern)] (, g!output)} (, record))))))))

      (list [_ {#Tuple slots}] record)
      (meta#in (list (list#mix (is (-> Code Code Code)
                                   (function (_ slot inner)
                                     (` (..the (, slot) (, inner)))))
                               record
                               slots)))

      (list selector)
      (do meta#monad
        [g!_ (..generated_symbol "_")
         g!record (..generated_symbol "record")]
        (in (list (` (function ((, g!_) (, g!record)) (..the (, selector) (, g!record)))))))
      
      _
      (failure (..wrong_syntax_error (symbol ..the))))))

(def (open_declaration imported_module alias tags my_tag_index [module short] source type)
  (-> Text Text (List Symbol) Nat Symbol Code Type (Meta (List Code)))
  (do meta#monad
    [output (record_slots type)
     g!_ (..generated_symbol "g!_")
     .let [g!output (local$ short)
           pattern (|> tags
                       enumeration
                       (list#each (function (_ [tag_idx tag])
                                    (if (.i64_=# my_tag_index tag_idx)
                                      g!output
                                      g!_)))
                       tuple$)
           source+ (` ({(, pattern) (, g!output)} (, source)))]]
    (when output
      {#Some [tags' members']}
      (do meta#monad
        [decls' (monad#each#meta (is (-> [Nat Symbol Type] (Meta (List Code)))
                                     (function (_ [sub_tag_index sname stype])
                                       (open_declaration imported_module alias tags' sub_tag_index sname source+ stype)))
                                 (enumeration (zipped_2 tags' members')))]
        (in (list#conjoint decls')))

      _
      (in (list (` (.def# (, (local$ (..module_alias (list short imported_module) alias)))
                          (, source+)
                          #0)))))))

(def (implementation_declarations imported_module alias implementation)
  (-> Text Text Symbol (Meta (List Code)))
  (do meta#monad
    [interface (type_definition implementation)
     output (record_slots interface)]
    (when output
      {#Some [slots terms]}
      (do meta#monad
        [.let [g!implementation (symbol$ implementation)]
         declarations (monad#each#meta (is (-> [Nat Symbol Type] (Meta (List Code)))
                                           (function (_ [index slot_label slot_type])
                                             (open_declaration imported_module alias slots index slot_label g!implementation slot_type)))
                                       (enumeration (zipped_2 slots terms)))]
        (in (list#conjoint declarations)))

      _
      (failure (.text_composite# "Can only 'use' implementations: " (symbol#encoded implementation)
                                 " : " (type#encoded interface))))))

(def (localized module global)
  (-> Text Symbol Symbol)
  (when global
    ["" local]
    [module local]

    _
    global))

(def .public use
  (macro (_ tokens)
    (when (..parsed (all ..andP
                         (..maybeP (all ..andP
                                        ..textP
                                        ..textP
                                        ..textP))
                         ..textP
                         (..orP (..manyP ..symbolP)
                                (..manyP ..anyP)))
                    tokens)
      {.#Some [current_module,imported_module,import_alias alias implementations]}
      (let [[current_module imported_module import_alias]
            (when current_module,imported_module,import_alias
              {#Some [current_module imported_module import_alias]}
              [current_module imported_module import_alias]
              
              {#None}
              ["" "" ""])]
        (when implementations
          {#Left implementations}
          (do meta#monad
            [declarations (|> implementations
                              (list#each (localized imported_module))
                              (monad#each#meta (implementation_declarations import_alias alias)))]
            (in (list#conjoint declarations)))
          
          {#Right implementations}
          (do meta#monad
            [pre_defs,implementations (is (Meta [(List Code) (List Code)])
                                          (monad#mix meta#monad
                                                     (function (_ it [pre_defs implementations])
                                                       (when it
                                                         [_ {#Symbol _}]
                                                         (in [pre_defs
                                                              {#Item it implementations}])
                                                         
                                                         _
                                                         (do meta#monad
                                                           [g!implementation (..generated_symbol "implementation")]
                                                           (in [{#Item (` (.def# (, g!implementation) (, it) #0)) pre_defs}
                                                                {#Item g!implementation implementations}]))))
                                                     [(list) (list)]
                                                     implementations))
             .let [[pre_defs implementations] pre_defs,implementations]]
            (in (|> pre_defs
                    {#Item (` (..use
                               (, (text$ current_module))
                               (, (text$ imported_module))
                               (, (text$ import_alias))
                               (, (text$ alias))
                               (,* implementations)))}
                    list#reversed)))))
      

      {.#None}
      (failure (..wrong_syntax_error (symbol ..use))))))

(def (imported_by? import_name module_name)
  (-> Text Text (Meta Bit))
  (do meta#monad
    [module (module module_name)
     .let [[..#module_hash _ ..#module_aliases _ ..#definitions _ ..#imports imports ..#module_state _] module]]
    (in (is_member? imports import_name))))

(def (referrals module_name extra)
  (-> Text (List Code) (Meta (List Referral)))
  (do meta#monad
    [extra,referral (when (referrals_parser #0 extra)
                      {#Some extra,referral}
                      (in extra,referral)

                      {#None}
                      (failure ""))
     .let [[extra referral] extra,referral]
     current_module current_module_name]
    (when extra
      {#End}
      (in referral)

      _
      (failure (.text_composite# (..wrong_syntax_error (symbol ..refer))
                                 \n "@ " current_module
                                 \n (|> extra
                                        (list#each code#encoded)
                                        (list#interposed " ")
                                        (list#mix text#composite "")))))))

(def .public refer
  (macro (_ tokens)
    (when tokens
      (list#partial [_ {#Text imported_module}] [_ {#Text alias}] options)
      (do meta#monad
        [referrals (..referrals imported_module options)
         current_module ..current_module_name]
        (in (list#each (function (_ [macro parameters])
                         (` ((, (symbol$ macro))
                             (, (text$ current_module))
                             (, (text$ imported_module))
                             (, (text$ alias))
                             (,* parameters))))
                       referrals)))

      _
      (failure (..wrong_syntax_error (symbol ..refer))))))

(def .public with
  (macro (_ tokens)
    (when (..parsed (..andP ..anyP ..anyP)
                    tokens)
      {.#Some [implementation expression]}
      (meta#in (list (` (..let [(..open (, (text$ (alias_stand_in 0)))) (, implementation)]
                          (, expression)))))

      {.#None}
      (failure (..wrong_syntax_error (symbol ..with))))))

(def .public of
  (macro (_ tokens)
    (when tokens
      (list implementation [_ {#Symbol member}])
      (meta#in (list (` (..with (, implementation) (, (symbol$ member))))))

      (list#partial implementation member args)
      (meta#in (list (` ((..of (, implementation) (, member)) (,* args)))))
      
      _
      (failure (..wrong_syntax_error (symbol ..of))))))

(def .public has
  (macro (_ tokens)
    (when tokens
      (list [_ {#Symbol slot'}] value record)
      (do meta#monad
        [slot (normal slot')
         output (..type_slot slot)
         .let [[exported? [label' type]] output]]
        (when label'
          {.#None}
          (in (list value))

          {.#Some [lefts right? family]}
          (do meta#monad
            [pattern' (monad#each#meta (is (-> [Nat Symbol] (Meta [Symbol Nat Code]))
                                           (function (_ [r_idx r_slot_name])
                                             (do meta#monad
                                               [g!slot (..generated_symbol "")]
                                               (in [r_slot_name r_idx g!slot]))))
                                       (enumeration family))
             .let [pattern (|> pattern'
                               (list#each (is (-> [Symbol Nat Code] (List Code))
                                              (function (_ [r_slot_name r_idx r_var])
                                                (list (symbol$ r_slot_name)
                                                      r_var))))
                               list#conjoint)
                   idx (if right?
                         (is Nat (.i64_+# 1 lefts))
                         lefts)
                   output (|> pattern'
                              (list#each (is (-> [Symbol Nat Code] (List Code))
                                             (function (_ [r_slot_name r_idx r_var])
                                               (list (symbol$ r_slot_name)
                                                     (if (.i64_=# idx r_idx)
                                                       value
                                                       r_var)))))
                              list#conjoint)]]
            (in (list (` ({[(,* pattern)] [(,* output)]} (, record))))))))

      (list [_ {#Tuple slots}] value record)
      (when slots
        {#End}
        (failure (..wrong_syntax_error (symbol ..has)))

        _
        (do meta#monad
          [bindings (monad#each#meta (is (-> Code (Meta Code))
                                         (function (_ _) (..generated_symbol "temp")))
                                     slots)
           .let [pairs (zipped_2 slots bindings)
                 update_expr (list#mix (is (-> [Code Code] Code Code)
                                           (function (_ [s b] v)
                                             (` (..has (, s) (, v) (, b)))))
                                       value
                                       (list#reversed pairs))
                 [_ accesses'] (list#mix (is (-> [Code Code] [Code (List (List Code))] [Code (List (List Code))])
                                             (function (_ [new_slot new_binding] [old_record accesses'])
                                               [(` (the (, new_slot) (, new_binding)))
                                                {#Item (list new_binding old_record) accesses'}]))
                                         [record (is (List (List Code)) {#End})]
                                         pairs)
                 accesses (list#conjoint (list#reversed accesses'))]]
          (in (list (` (let [(,* accesses)]
                         (, update_expr)))))))
      
      (list selector value)
      (do meta#monad
        [g!_ (..generated_symbol "_")
         g!record (..generated_symbol "record")]
        (in (list (` (function ((, g!_) (, g!record))
                       (..has (, selector) (, value) (, g!record)))))))

      (list selector)
      (do meta#monad
        [g!_ (..generated_symbol "_")
         g!value (..generated_symbol "value")
         g!record (..generated_symbol "record")]
        (in (list (` (function ((, g!_) (, g!value) (, g!record))
                       (..has (, selector) (, g!value) (, g!record)))))))

      _
      (failure (..wrong_syntax_error (symbol ..has))))))

(def .public revised
  (macro (_ tokens)
    (when tokens
      (list [_ {#Symbol slot'}] fun record)
      (do meta#monad
        [slot (normal slot')
         output (..type_slot slot)
         .let [[exported? [label' type]] output]]
        (when label'
          {.#None}
          (in (list (` ((, fun) (, record)))))

          {.#Some [lefts right? family]}
          (do meta#monad
            [pattern' (monad#each#meta (is (-> [Nat Symbol] (Meta [Symbol Nat Code]))
                                           (function (_ [r_idx r_slot_name])
                                             (do meta#monad
                                               [g!slot (..generated_symbol "")]
                                               (in [r_slot_name r_idx g!slot]))))
                                       (enumeration family))
             .let [pattern (|> pattern'
                               (list#each (is (-> [Symbol Nat Code] (List Code))
                                              (function (_ [r_slot_name r_idx r_var])
                                                (list (symbol$ r_slot_name)
                                                      r_var))))
                               list#conjoint)
                   idx (if right?
                         (is Nat (.i64_+# 1 lefts))
                         lefts)
                   output (|> pattern'
                              (list#each (is (-> [Symbol Nat Code] (List Code))
                                             (function (_ [r_slot_name r_idx r_var])
                                               (list (symbol$ r_slot_name)
                                                     (if (.i64_=# idx r_idx)
                                                       (` ((, fun) (, r_var)))
                                                       r_var)))))
                              list#conjoint)]]
            (in (list (` ({[(,* pattern)] [(,* output)]} (, record))))))))

      (list [_ {#Tuple slots}] fun record)
      (when slots
        {#End}
        (failure (..wrong_syntax_error (symbol ..revised)))

        _
        (do meta#monad
          [g!record (..generated_symbol "record")
           g!temp (..generated_symbol "temp")]
          (in (list (` (let [(, g!record) (, record)
                             (, g!temp) (the [(,* slots)] (, g!record))]
                         (has [(,* slots)] ((, fun) (, g!temp)) (, g!record))))))))

      (list selector fun)
      (do meta#monad
        [g!_ (..generated_symbol "_")
         g!record (..generated_symbol "record")]
        (in (list (` (function ((, g!_) (, g!record))
                       (..revised (, selector) (, fun) (, g!record)))))))

      (list selector)
      (do meta#monad
        [g!_ (..generated_symbol "_")
         g!fun (..generated_symbol "fun")
         g!record (..generated_symbol "record")]
        (in (list (` (function ((, g!_) (, g!fun) (, g!record))
                       (..revised (, selector) (, g!fun) (, g!record)))))))
      
      _
      (failure (..wrong_syntax_error (symbol ..revised))))))

(def .private with_template#pattern
  (pattern
   (macro (_ tokens)
     (when tokens
       (list#partial [_ {#Form (list [_ {#Tuple bindings}]
                                     [_ {#Tuple templates}])}]
                     [_ {#Form data}]
                     branches)
       (when (is (Maybe (List Code))
                 (do maybe#monad
                   [bindings' (monad#each maybe#monad symbol_short bindings)
                    data' (monad#each maybe#monad tuple_list data)]
                   (let [num_bindings (list#size bindings')]
                     (if (every? (|>> (.i64_=# num_bindings))
                                 (list#each list#size data'))
                       (let [apply (is (-> Replacement_Environment (List Code))
                                       (function (_ env) (list#each (realized_template env) templates)))]
                         (|> data'
                             (list#each (function#composite apply (replacement_environment bindings')))
                             list#conjoint
                             in))
                       {#None}))))
         {#Some output}
         (meta#in (list#composite output branches))
         
         {#None}
         (failure (..wrong_syntax_error (symbol ..with_template#pattern))))
       
       _
       (failure (..wrong_syntax_error (symbol ..with_template#pattern)))))))

(with_template [<name> <extension>]
  [(def .public <name>
     (All (_ s)
       (-> (I64 s) (I64 s)))
     (|>> (<extension> 1)))]

  [++ .i64_+#]
  [-- .i64_-#]
  )

(def (interleaved xs ys)
  (All (_ a)
    (-> (List a) (List a) (List a)))
  (when xs
    {#End}
    {#End}
    
    {#Item x xs'}
    (when ys
      {#End}
      {#End}
      
      {#Item y ys'}
      (list#partial x y (interleaved xs' ys')))))

(def (type_code type)
  (-> Type Code)
  (when type
    {#Nominal name params}
    (` {.#Nominal (, (text$ name)) (, (untemplated_list (list#each type_code params)))})

    (with_template#pattern [<tag>]
      [{<tag> left right}
       (` {<tag> (, (type_code left)) (, (type_code right))})])
    ([.#Sum] [.#Product]
     [.#Function]
     [.#Apply])

    (with_template#pattern [<tag>]
      [{<tag> id}
       (` {<tag> (, (nat$ id))})])
    ([.#Parameter] [.#Var] [.#Ex])

    (with_template#pattern [<tag>]
      [{<tag> env type}
       (let [env' (untemplated_list (list#each type_code env))]
         (` {<tag> (, env') (, (type_code type))}))])
    ([.#UnivQ] [.#ExQ])
    
    {#Named [module name] anonymous}
    ... TODO: Generate the explicit type definition instead of using
    ... the "symbol$" shortcut below.
    ... (` {.#Named [(, (text$ module)) (, (text$ name))]
    ...     (, (type_code anonymous))})
    (symbol$ [module name])))

(def .public loop
  (macro (_ tokens)
    (let [?params (when tokens
                    (list [_ {#Form (list name [_ {#Tuple bindings}])}] body)
                    {#Some [name bindings body]}

                    _
                    {#None})]
      (when ?params
        {#Some [name bindings body]}
        (when (pairs bindings)
          {#Some pairs}
          (let [vars (list#each product#left pairs)
                inits (list#each product#right pairs)]
            (if (every? symbol? inits)
              (do meta#monad
                [inits' (is (Meta (List Symbol))
                            (when (monad#each maybe#monad symbol_name inits)
                              {#Some inits'} (meta#in inits')
                              {#None}        (failure (..wrong_syntax_error (symbol ..loop)))))
                 init_types (monad#each#meta type_definition inits')
                 expected ..expected_type]
                (meta#in (list (` ((.is# (-> (,* (list#each type_code init_types))
                                             (, (type_code expected)))
                                         (function ((, name) (,* vars))
                                           (, body)))
                                   (,* inits))))))
              (do meta#monad
                [aliases (monad#each#meta (is (-> Code (Meta Code))
                                              (function (_ _) (..generated_symbol "")))
                                          inits)]
                (meta#in (list (` (..let [(,* (..interleaved aliases inits))]
                                    (..loop ((, name) [(,* (..interleaved vars aliases))])
                                      (, body)))))))))

          {#None}
          (failure (..wrong_syntax_error (symbol ..loop))))

        {#None}
        (failure (..wrong_syntax_error (symbol ..loop)))))))

(def .public with_expansions
  (let [with_expansions' (is (-> Text (List Code) Code (List Code))
                             (function (with_expansions' label tokens target)
                               (when target
                                 (pattern#or [_ {#Bit _}]
                                             [_ {#Nat _}]
                                             [_ {#Int _}]
                                             [_ {#Rev _}]
                                             [_ {#Frac _}]
                                             [_ {#Text _}])
                                 (list target)

                                 [_ {#Symbol [module name]}]
                                 (if (and (text#= "" module)
                                          (text#= label name))
                                   tokens
                                   (list target))

                                 (with_template#pattern [<tag>]
                                   [[location {<tag> elems}]
                                    (list [location {<tag> (list#conjoint (list#each (with_expansions' label tokens) elems))}])])
                                 ([#Form]
                                  [#Variant]
                                  [#Tuple]))))]
    (macro (_ tokens)
      (when (parsed (andP (tupleP (someP bindingP)) (someP anyP)) tokens)
        {#Some [bindings bodies]}
        (loop (again [bindings bindings
                      map (is (Property_List (List Code))
                              (list))])
          (let [normal (is (-> Code (List Code))
                           (function (_ it)
                             (list#mix (function (_ [binding expansion] it)
                                         (list#conjoint (list#each (with_expansions' binding expansion) it)))
                                       (list it)
                                       map)))]
            (when bindings
              {#Item [var_name expr] &rest}
              (do meta#monad
                [expansion (when (normal expr)
                             (list expr)
                             (single_expansion expr)

                             _
                             (failure (.text_composite# "Incorrect expansion in with_expansions"
                                                        " | Binding: " (text#encoded var_name)
                                                        " | Expression: " (code#encoded expr))))]
                (again &rest (property#with var_name expansion map)))
              
              {#End}
              (meta#in (list#conjoint (list#each normal bodies))))))
        
        {#None}
        (failure (..wrong_syntax_error (symbol ..with_expansions)))))))

(def .public (same? reference sample)
  (All (_ of)
    (-> of of
        Bit))
  (.is?# reference sample))

(def .public as_expected
  (macro (_ tokens)
    (when tokens
      (list expr)
      (do meta#monad
        [type ..expected_type]
        (in (list (` (.as# (, (type_code type))
                           (, expr))))))
      
      _
      (failure (..wrong_syntax_error (symbol ..as_expected))))))

(def .public undefined
  (let [location (is (Meta Location)
                     (function (_ compiler)
                       {#Right [compiler (the #location compiler)]}))]
    (macro (_ tokens)
      (when tokens
        {#End}
        (do meta#monad
          [location location
           .let [[module line column] location
                 location (.text_composite# (text#encoded module) "," (nat#encoded line) "," (nat#encoded column))
                 message (.text_composite# "Undefined behavior at " location)]]
          (exec
            (.log!# (.text_composite# "WARNING: " message))
            (in (list (` (..panic! (, (text$ message))))))))
        
        _
        (failure (..wrong_syntax_error (symbol ..undefined)))))))

(def .public type_of
  (macro (_ tokens)
    (when tokens
      (list [_ {#Symbol var_name}])
      (do meta#monad
        [var_type (type_definition var_name)]
        (in (list (type_code var_type))))

      (list expression)
      (do meta#monad
        [g!temp (..generated_symbol "g!temp")]
        (in (list (` (let [(, g!temp) (, expression)]
                       (..type_of (, g!temp)))))))

      _
      (failure (..wrong_syntax_error (symbol ..type_of))))))

(def .public template
  (let [templateP (is (-> (List Code) (Maybe [Text (List Text) (List Code)]))
                      (function (_ tokens)
                        (do maybe#monad
                          [% (local_declarationP tokens)
                           .let' [[tokens [name parameters]] %]
                           % (tupleP (someP anyP) tokens)
                           .let' [[tokens templates] %]
                           _ (endP tokens)]
                          (in [name parameters templates]))))
        simple_replacement_environment (is (-> (List Text) Replacement_Environment)
                                           (list#each (function (_ arg)
                                                        [arg (` ((,' ,) (, (local$ arg))))])))
        instantiated_template (is (-> Replacement_Environment Code Code)
                                  (function (_ replacement_environment template)
                                    (` (`' (, (with_replacements replacement_environment
                                                template))))))]
    (macro (_ tokens)
      (when (templateP tokens)
        {#Some [name args input_templates]}
        (do meta#monad
          [g!tokens (..generated_symbol "tokens")
           g!compiler (..generated_symbol "compiler")
           g!_ (..generated_symbol "_")
           this_module ..current_module_name]
          (in (list (` (..macro ((, (local$ name)) (, g!tokens) (, g!compiler))
                         (when (, g!tokens)
                           (list (,* (list#each local$ args)))
                           {.#Right [(, g!compiler)
                                     (list (,* (list#each (instantiated_template (simple_replacement_environment args))
                                                          input_templates)))]}
                           
                           (, g!_)
                           {.#Left "Invalid syntax."}))))))

        {#None}
        (failure (..wrong_syntax_error (symbol ..template)))))))

(with_template [<name> <to>]
  [(def .public <name>
     (template (<name> it)
       [(..|> it (..is (..I64 ..Any)) (..as <to>))]))]

  [i64 ..I64]
  [nat ..Nat]
  [int ..Int]
  [rev ..Rev]
  )

(def .public these
  (macro (_ tokens compiler)
    {#Right [compiler tokens]}))

(def .public char
  (macro (_ tokens compiler)
    (when tokens
      (list [_ {#Text input}])
      (if (|> input .text_size# (.i64_=# 1))
        (|> input (.text_char# 0)
            nat$ list
            [compiler] {#Right})
        {#Left (..wrong_syntax_error (symbol ..char))})

      _
      {#Left (..wrong_syntax_error (symbol ..char))})))

(def .public for
  (let [target (is (Meta Text)
                   (function (_ compiler)
                     {#Right [compiler (the [#info #target] compiler)]}))
        platform_name (is (-> Code (Meta Text))
                          (function (_ choice)
                            (when choice
                              [_ {#Text platform}]
                              (..meta#in platform)

                              [_ {#Symbol symbol}]
                              (do meta#monad
                                [symbol (..global_symbol symbol)
                                 type+value (..definition_value symbol)
                                 .let [[type value] type+value]]
                                (when (anonymous_type type)
                                  {#Nominal "#Text" {#End}}
                                  (in (as ..Text value))

                                  _
                                  (failure (.text_composite# "Invalid target platform (must be a value of type Text): " (symbol#encoded symbol)
                                                             " : " (..code#encoded (..type_code type))))))

                              _
                              (failure (.text_composite# "Invalid target platform syntax: " (..code#encoded choice)
                                                         \n "Must be either a text literal or a symbol.")))))
        target_pick (is (-> Text (List [Code Code]) (Maybe Code) (Meta (List Code)))
                        (function (target_pick target options default)
                          (when options
                            {#End}
                            (when default
                              {#None}
                              (failure (.text_composite# "No code for target platform: " target))

                              {#Some default}
                              (meta#in (list default)))

                            {#Item [key pick] options'}
                            (do meta#monad
                              [platform (platform_name key)]
                              (if (text#= target platform)
                                (meta#in (list pick))
                                (target_pick target options' default))))))]
    (macro (_ tokens)
      (when (..parsed (..andP (..someP (..andP ..anyP ..anyP))
                              (..maybeP ..anyP))
                      tokens)
        {.#Some [options default]}
        (do meta#monad
          [target target]
          (target_pick target options default))

        {.#None}
        (failure (..wrong_syntax_error (symbol ..for)))))))

... TODO: Delete "scope_type_vars" (including the #scope_type_vars Lux state) and "parameter" ASAP.
(for "{old}" (these (def (scope_type_vars state)
                      (Meta (List Nat))
                      (when state
                        [..#info info ..#source    source ..#current_module _   ..#modules modules
                         ..#scopes scopes ..#type_context types    ..#host    host
                         ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
                         ..#scope_type_vars scope_type_vars ..#eval _eval]
                        {#Right [state scope_type_vars]}))

                    (def .public parameter
                      (macro (_ tokens)
                        (when tokens
                          (list [_ {#Nat idx}])
                          (do meta#monad
                            [stvs ..scope_type_vars]
                            (when (..item idx (list#reversed stvs))
                              {#Some var_id}
                              (in (list (` {.#Ex (, (nat$ var_id))})))

                              {#None}
                              (failure (.text_composite# "Indexed-type does not exist: " (nat#encoded idx)))))

                          _
                          (failure (..wrong_syntax_error (symbol ..$)))))))
     (these (def .public parameter "")))

(def .public require
  (let [refer_code (is (-> Text Text (List Referral) Code)
                       (function (_ imported_module alias referrals)
                         (` (..refer (, (text$ imported_module))
                                     (, (text$ alias))
                                     (,* (list#each (function (_ [macro parameters])
                                                      (` ((, (symbol$ macro)) (,* parameters))))
                                                    referrals))))))]
    (macro (_ _imports)
      (do meta#monad
        [current_module ..current_module_name
         imports (imports_parser #0 current_module {#End} _imports)
         .let [=imports (|> imports
                            (list#each (is (-> Importation Code)
                                           (function (_ [module_name m_alias =refer])
                                             (` [(, (text$ module_name)) (, (text$ (..maybe#else "" m_alias)))]))))
                            tuple$)
               =refers (list#each (is (-> Importation Code)
                                      (function (_ [module_name m_alias =refer])
                                        (refer_code module_name (..maybe#else "" m_alias) =refer)))
                                  imports)
               =module (` (.module# (, =imports)))]
         g!_ (..generated_symbol "")]
        (in {#Item =module =refers})))))

(type .public Immediate_UnQuote
  (Nominal "#Macro/Immediate_UnQuote"))

(def .public immediate_unquote
  (-> Macro Immediate_UnQuote)
  (|>> (as Immediate_UnQuote)))

(def immediate_unquote_macro
  (-> Immediate_UnQuote Macro')
  (|>> (as Macro')))

(def .public ,,
  (..immediate_unquote
   (macro (_ it)
     (when it
       (list it)
       (meta#in (list it))

       _
       (failure (wrong_syntax_error (symbol ..,,)))))))

(def aggregate_embedded_expansions
  (template (_ embedded_expansions <@> <tag> <*>)
    [(do meta#monad
       [<*>' (monad#each#meta embedded_expansions <*>)]
       (in [(|> <*>'
                list#reversed
                (list#each product#left)
                (list#mix list#composite (list)))
            [<@> {<tag> (list#each product#right <*>')}]]))]))

(def (embedded_expansions code)
  (-> Code (Meta [(List Code) Code]))
  (when code
    [@ {#Form (list#partial [@symbol {#Symbol original_symbol}] parameters)}]
    (with_expansions [<failure> (aggregate_embedded_expansions embedded_expansions @ #Form (list#partial [@symbol {#Symbol original_symbol}] parameters))]
      (do meta#monad
        [resolved_symbol (..normal original_symbol)
         ?resolved_symbol (meta#try (..global_symbol resolved_symbol))]
        (when ?resolved_symbol
          {#Left _}
          <failure>

          {#Right resolved_symbol}
          (do meta#monad
            [?type,value (meta#try (..definition_value resolved_symbol))]
            (when ?type,value
              {#Left _}
              <failure>

              {#Right [type value]}
              (if (type#= ..Immediate_UnQuote type)
                (do meta#monad
                  [bound ((immediate_unquote_macro (as Immediate_UnQuote value)) parameters)
                   g!expansion (..generated_symbol "g!expansion")]
                  (in [{#Item g!expansion bound}
                       g!expansion]))
                <failure>))))))

    (with_template#pattern [<tag>]
      [[@ {<tag> parts}]
       (aggregate_embedded_expansions embedded_expansions @ <tag> parts)])
    ([#Form]
     [#Variant]
     [#Tuple])
    
    _
    (meta#in [(list) code])))

(def .public ``
  (macro (_ tokens)
    (when tokens
      (list raw)
      (do meta#monad
        [=raw (..embedded_expansions raw)
         .let [[labels labelled] =raw]]
        (in (list (` (with_expansions [(,* labels)]
                       (, labelled))))))

      _
      (failure (..wrong_syntax_error (symbol ..``))))))

(with_template [<bit> <name>]
  [(def .public <name> Bit <bit>)]

  [#0 false]
  [#1 true]
  )

(def .public try
  (macro (_ tokens)
    (when tokens
      (list expression)
      (do meta#monad
        [g!_ (..generated_symbol "g!_")]
        (in (list (` (.try# (.function ((, g!_) (, g!_))
                              (, expression)))))))

      _
      (..failure (..wrong_syntax_error (symbol ..try))))))

(def (methodP tokens)
  (-> (List Code) (Maybe [(List Code) [Text Code]]))
  (when tokens
    (list#partial [_ {#Form (list [_ {#Symbol [..prelude "is#"]}]
                                  type
                                  [_ {#Symbol ["" name]}])}]
                  tokens')
    {#Some [tokens' [name type]]}

    _
    {#None}))

(def .public Interface
  (macro (_ tokens)
    (do meta#monad
      [methods' (monad#each#meta complete_expansion tokens)]
      (when (everyP methodP (list#conjoint methods'))
        {#Some methods}
        (in (list (` (..Tuple (,* (list#each product#right methods))))
                  (tuple$ (list#each (|>> product#left text$) methods))))

        {#None}
        (failure (..wrong_syntax_error (symbol ..Interface)))))))

(def .public Rec
  (let [recursive_type (is (-> Code Code Text Code Code)
                           (function (recursive_type g!self g!dummy name body)
                             (` {.#Apply (..Nominal "")
                                         (.All ((, g!self) (, g!dummy))
                                           (, (let$ (local$ name) (` {.#Apply (..Nominal "") (, g!self)})
                                                    body)))})))]
    (macro (_ tokens)
      (when tokens
        (list [_ {#Symbol "" name}] body)
        (do meta#monad
          [body' (complete_expansion body)
           g!self (generated_symbol "g!self")
           g!dummy (generated_symbol "g!dummy")]
          (when body'
            (list body' labels)
            (in (list (recursive_type g!self g!dummy name body')
                      labels))

            (list body')
            (in (list (recursive_type g!self g!dummy name body')))

            _
            (failure (..wrong_syntax_error (symbol ..Rec)))))

        _
        (failure (..wrong_syntax_error (symbol ..Rec)))))))

(with_template [<type>]
  [(def .public <type>
     Type
     (let [[_ short] (symbol <type>)]
       {#Named [..prelude short]
               {.#Nominal (.text_composite# "#Extension/" short) (list)}}))]

  [Analysis]
  [Synthesis]
  [Translation]
  [Declaration]
  )

(def .public alias
  (macro (_ tokens)
    (when (parsed (andP (tupleP (manyP localP))
                        symbolP)
                  tokens)
      {#Some [alias/+ original]}
      (meta#in (list#each (function (_ it)
                            (` (def .public (, (local$ it))
                                 (, (symbol$ original)))))
                          alias/+))
      
      {#None}
      (failure (..wrong_syntax_error (symbol ..alias))))))

(alias [F64 Double]
       ..Frac)

(alias [alias?]
       ..same?)