("lux def" dummy_location
 ["" 0 0]
 [["" 0 0] (9 #1 (0 #0))]
 #0)

("lux def" double_quote
 ("lux i64 char" +34)
 [dummy_location (9 #1 (0 #0))]
 #0)

("lux def" \n
 ("lux i64 char" +10)
 [dummy_location (9 #1 (0 #0))]
 #0)

("lux def" prelude_module
 "library/lux"
 [dummy_location (9 #1 (0 #0))]
 #1)

... (type: .public Any
...   (Ex (_ a) a))
("lux def" Any
 ("lux type check type"
  (9 #1 ["library/lux" "Any"]
     (8 #0 (0 #0) (4 #0 1))))
 [dummy_location
  (9 #1 (0 #0))]
 #1)

... (type: .public Nothing
...   (All (_ a) a))
("lux def" Nothing
 ("lux type check type"
  (9 #1 ["library/lux" "Nothing"]
     (7 #0 (0 #0) (4 #0 1))))
 [dummy_location
  (9 #1 (0 #0))]
 #1)

... (type: .public (List a)
...   #End
...   (#Item a (List a)))
("lux def type tagged" List
 (9 #1 ["library/lux" "List"]
    (7 #0 (0 #0)
       (1 #0 ... "lux.End"
          Any
          ... "lux.Item"
          (2 #0 (4 #0 1)
             (9 #0 (4 #0 1) (4 #0 0))))))
 [dummy_location
  (9 #1 (0 #0))]
 ("End" "Item")
 #1)

("lux def" Bit
 ("lux type check type"
  (9 #1 ["library/lux" "Bit"]
     (0 #0 "#Bit" #End)))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" I64
 ("lux type check type"
  (9 #1 ["library/lux" "I64"]
     (7 #0 (0 #0)
        (0 #0 "#I64" (#Item (4 #0 1) #End)))))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" Nat
 ("lux type check type"
  (9 #1 ["library/lux" "Nat"]
     (0 #0 "#I64" (#Item (0 #0 "#Nat" #End) #End))))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" Int
 ("lux type check type"
  (9 #1 ["library/lux" "Int"]
     (0 #0 "#I64" (#Item (0 #0 "#Int" #End) #End))))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" Rev
 ("lux type check type"
  (9 #1 ["library/lux" "Rev"]
     (0 #0 "#I64" (#Item (0 #0 "#Rev" #End) #End))))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" Frac
 ("lux type check type"
  (9 #1 ["library/lux" "Frac"]
     (0 #0 "#Frac" #End)))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" Text
 ("lux type check type"
  (9 #1 ["library/lux" "Text"]
     (0 #0 "#Text" #End)))
 [dummy_location
  (9 #1 #End)]
 #1)

("lux def" Name
 ("lux type check type"
  (9 #1 ["library/lux" "Name"]
     (2 #0 Text Text)))
 [dummy_location
  (9 #1 #End)]
 #1)

... (type: .public (Maybe a)
...   #None
...   (#Some a))
("lux def type tagged" Maybe
 (9 #1 ["library/lux" "Maybe"]
    (7 #0 #End
       (1 #0 ... "lux.None"
          Any
          ... "lux.Some"
          (4 #0 1))))
 [dummy_location
  (9 #1 #End)]
 ("None" "Some")
 #1)

... (type: .public Type
...   (Rec Type
...     (Variant
...      (#Primitive 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 Name Type))))
("lux def type tagged" Type
 (9 #1 ["library/lux" "Type"]
    ({Type
      ({Type_List
        ({Type_Pair
          (9 #0 Nothing
             (7 #0 #End
                (1 #0
                   ... "lux.Primitive"
                   (2 #0 Text Type_List)
                   (1 #0
                      ... "lux.Sum"
                      Type_Pair
                      (1 #0
                         ... "lux.Product"
                         Type_Pair
                         (1 #0
                            ... "lux.Function"
                            Type_Pair
                            (1 #0
                               ... "lux.Parameter"
                               Nat
                               (1 #0
                                  ... "lux.Var"
                                  Nat
                                  (1 #0
                                     ... "lux.Ex"
                                     Nat
                                     (1 #0
                                        ... "lux.UnivQ"
                                        (2 #0 Type_List Type)
                                        (1 #0
                                           ... "lux.ExQ"
                                           (2 #0 Type_List Type)
                                           (1 #0
                                              ... "lux.Apply"
                                              Type_Pair
                                              ... "lux.Named"
                                              (2 #0 Name Type)))))))))))))}
         ("lux type check type" (2 #0 Type Type)))}
       ("lux type check type" (9 #0 Type List)))}
     ("lux type check type" (9 #0 (4 #0 1) (4 #0 0)))))
 [dummy_location
  (9 #1 #End)]
 ("Primitive" "Sum" "Product" "Function" "Parameter" "Var" "Ex" "UnivQ" "ExQ" "Apply" "Named")
 #1)

... (type: .public Location
...   {#module Text
...    #line   Nat
...    #column Nat})
("lux def type tagged" Location
 (#Named ["library/lux" "Location"]
         (#Product Text (#Product Nat Nat)))
 [dummy_location
  (9 #1 #End)]
 ["module" "line" "column"]
 #1)

... (type: .public (Ann m v)
...   {#meta  m
...    #datum v})
("lux def type tagged" Ann
 (#Named ["library/lux" "Ann"]
         (#UnivQ #End
                 (#UnivQ #End
                         (#Product (#Parameter 3)
                                   (#Parameter 1)))))
 [dummy_location
  (9 #1 #End)]
 ["meta" "datum"]
 #1)

... (type: .public (Code' w)
...   (#Bit Bit)
...   (#Nat Nat)
...   (#Int Int)
...   (#Rev Rev)
...   (#Frac Frac)
...   (#Text Text)
...   (#Identifier Name)
...   (#Tag Name)
...   (#Form (List (w (Code' w))))
...   (#Tuple (List (w (Code' w))))
...   (#Record (List [(w (Code' w)) (w (Code' w))])))
("lux def type tagged" Code'
 (#Named ["library/lux" "Code'"]
         ({Code
           ({Code_List
             (#UnivQ #End
                     (#Sum ... "lux.Bit"
                      Bit
                      (#Sum ... "lux.Nat"
                       Nat
                       (#Sum ... "lux.Int"
                        Int
                        (#Sum ... "lux.Rev"
                         Rev
                         (#Sum ... "lux.Frac"
                          Frac
                          (#Sum ... "lux.Text"
                           Text
                           (#Sum ... "lux.Identifier"
                            Name
                            (#Sum ... "lux.Tag"
                             Name
                             (#Sum ... "lux.Form"
                              Code_List
                              (#Sum ... "lux.Tuple"
                               Code_List
                               ... "lux.Record"
                               (#Apply (#Product Code Code) List)
                               ))))))))))
                     )}
            ("lux type check type" (#Apply Code List)))}
          ("lux type check type" (#Apply (#Apply (#Parameter 1)
                                                 (#Parameter 0))
                                         (#Parameter 1)))))
 [dummy_location
  (9 #1 #End)]
 ("Bit" "Nat" "Int" "Rev" "Frac" "Text" "Identifier" "Tag" "Form" "Tuple" "Record")
 #1)

... (type: .public Code
...   (Ann Location (Code' (Ann Location))))
("lux def" Code
 (#Named ["library/lux" "Code"]
         ({w
           (#Apply (#Apply w Code') w)}
          ("lux type check type" (#Apply Location Ann))))
 [dummy_location
  (#Record #End)]
 #1)

("lux def" private
 #0
 [dummy_location
  (#Record #End)]
 #1)

("lux def" public
 #1
 [dummy_location
  (#Record #End)]
 #1)

("lux def" local
 #0
 [dummy_location
  (#Record #End)]
 #1)

("lux def" global
 #1
 [dummy_location
  (#Record #End)]
 #1)

("lux def" _ann
 ("lux type check"
  (#Function (#Apply (#Apply Location Ann)
                     Code')
             Code)
  ([_ data]
   [dummy_location data]))
 [dummy_location (#Record #End)]
 #0)

("lux def" bit$
 ("lux type check" (#Function Bit Code)
  ([_ value] (_ann (#Bit value))))
 [dummy_location (#Record #End)]
 #0)

("lux def" nat$
 ("lux type check" (#Function Nat Code)
  ([_ value] (_ann (#Nat value))))
 [dummy_location (#Record #End)]
 #0)

("lux def" int$
 ("lux type check" (#Function Int Code)
  ([_ value] (_ann (#Int value))))
 [dummy_location (#Record #End)]
 #0)

("lux def" rev$
 ("lux type check" (#Function Rev Code)
  ([_ value] (_ann (#Rev value))))
 [dummy_location (#Record #End)]
 #0)

("lux def" frac$
 ("lux type check" (#Function Frac Code)
  ([_ value] (_ann (#Frac value))))
 [dummy_location (#Record #End)]
 #0)

("lux def" text$
 ("lux type check" (#Function Text Code)
  ([_ text] (_ann (#Text text))))
 [dummy_location (#Record #End)]
 #0)

("lux def" identifier$
 ("lux type check" (#Function Name Code)
  ([_ name] (_ann (#Identifier name))))
 [dummy_location (#Record #End)]
 #0)

("lux def" local_identifier$
 ("lux type check" (#Function Text Code)
  ([_ name] (_ann (#Identifier ["" name]))))
 [dummy_location (#Record #End)]
 #0)

("lux def" tag$
 ("lux type check" (#Function Name Code)
  ([_ name] (_ann (#Tag name))))
 [dummy_location (#Record #End)]
 #0)

("lux def" local_tag$
 ("lux type check" (#Function Text Code)
  ([_ name] (_ann (#Tag ["" name]))))
 [dummy_location (#Record #End)]
 #0)

("lux def" form$
 ("lux type check" (#Function (#Apply Code List) Code)
  ([_ tokens] (_ann (#Form tokens))))
 [dummy_location (#Record #End)]
 #0)

("lux def" tuple$
 ("lux type check" (#Function (#Apply Code List) Code)
  ([_ tokens] (_ann (#Tuple tokens))))
 [dummy_location (#Record #End)]
 #0)

("lux def" record$
 ("lux type check" (#Function (#Apply (#Product Code Code) List) Code)
  ([_ tokens] (_ann (#Record tokens))))
 [dummy_location (#Record #End)]
 #0)

... (type: .public Definition
...   [Bit Type Code Any])
("lux def" Definition
 ("lux type check type"
  (#Named ["library/lux" "Definition"]
          (#Product Bit (#Product Type (#Product Code Any)))))
 (record$ #End)
 .public)

... (type: .public Alias
...   Name)
("lux def" Alias
 ("lux type check type"
  (#Named ["library/lux" "Alias"]
          Name))
 (record$ #End)
 .public)

... (type: .public Label
...   [Bit Type (List Text) Nat])
("lux def" Label
 ("lux type check type"
  (#Named ["library/lux" "Label"]
          (#Product Bit (#Product Type (#Product (#Apply Text List) Nat)))))
 (record$ #End)
 .public)

... (type: .public Global
...   (Variant
...    (#Definition Definition)
...    (#Type [Bit Type (Either [Text (List Text)] [Text (List Text)])])
...    (#Tag Label)
...    (#Slot Label)
...    (#Alias Alias)))
("lux def type tagged" Global
 (#Named ["library/lux" "Global"]
         (#Sum Definition
               (#Sum ({labels
                       (#Product Bit (#Product Type (#Sum labels labels)))}
                      (#Product Text (#Apply Text List)))
                     (#Sum Label
                           (#Sum Label
                                 Alias)))))
 (record$ #End)
 ("Definition" "Type" "Label" "Slot" "Alias")
 .public)

... (type: .public (Bindings k v)
...   {#counter Nat
...    #mappings (List [k v])})
("lux def type tagged" Bindings
 (#Named ["library/lux" "Bindings"]
         (#UnivQ #End
                 (#UnivQ #End
                         (#Product ... "lux.counter"
                          Nat
                          ... "lux.mappings"
                          (#Apply (#Product (#Parameter 3)
                                            (#Parameter 1))
                                  List)))))
 (record$ #End)
 ["counter" "mappings"]
 .public)

... (type: .public Ref
...   (#Local Nat)
...   (#Captured Nat))
("lux def type tagged" Ref
 (#Named ["library/lux" "Ref"]
         (#Sum ... Local
          Nat
          ... Captured
          Nat))
 (record$ #End)
 ("Local" "Captured")
 .public)

... (type: .public Scope
...   {#name     (List Text)
...    #inner    Nat
...    #locals   (Bindings Text [Type Nat])
...    #captured (Bindings Text [Type Ref])})
("lux def type tagged" Scope
 (#Named ["library/lux" "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))))))
 (record$ #End)
 ["name" "inner" "locals" "captured"]
 .public)

("lux def" Code_List
 ("lux type check type"
  (#Apply Code List))
 (record$ #End)
 #0)

... (type: .public (Either l r)
...   (#Left l)
...   (#Right r))
("lux def type tagged" Either
 (#Named ["library/lux" "Either"]
         (#UnivQ #End
                 (#UnivQ #End
                         (#Sum ... "lux.Left"
                          (#Parameter 3)
                          ... "lux.Right"
                          (#Parameter 1)))))
 (record$ #End)
 ("Left" "Right")
 .public)

... (type: .public Source
...   [Location Nat Text])
("lux def" Source
 ("lux type check type"
  (#Named ["library/lux" "Source"]
          (#Product Location (#Product Nat Text))))
 (record$ #End)
 .public)

... (type: .public Module_State
...   #Active
...   #Compiled
...   #Cached)
("lux def type tagged" Module_State
 (#Named ["library/lux" "Module_State"]
         (#Sum
          ... #Active
          Any
          (#Sum
           ... #Compiled
           Any
           ... #Cached
           Any)))
 (record$ #End)
 ("Active" "Compiled" "Cached")
 .public)

... (type: .public Module
...   (Record
...    {#module_hash        Nat
...     #module_aliases     (List [Text Text])
...     #definitions        (List [Text Global])
...     #imports            (List Text)
...     #module_annotations (Maybe Code)
...     #module_state       Module_State}))
("lux def type tagged" Module
 (#Named ["library/lux" "Module"]
         (#Product
          ... "lux.module_hash"
          Nat
          (#Product
           ... "lux.module_aliases"
           (#Apply (#Product Text Text) List)
           (#Product
            ... "lux.definitions"
            (#Apply (#Product Text Global) List)
            (#Product
             ... "lux.imports"
             (#Apply Text List)
             (#Product
              ... "lux.module_annotations"
              (#Apply Code Maybe)
              ... module_state
              Module_State)
             )))))
 (record$ #End)
 ["module_hash" "module_aliases" "definitions" "imports" "module_annotations" "module_state"]
 .public)

... (type: .public Type_Context
...   {#ex_counter Nat
...    #var_counter Nat
...    #var_bindings (List [Nat (Maybe Type)])})
("lux def type tagged" Type_Context
 (#Named ["library/lux" "Type_Context"]
         (#Product ... ex_counter
          Nat
          (#Product ... var_counter
           Nat
           ... var_bindings
           (#Apply (#Product Nat (#Apply Type Maybe))
                   List))))
 (record$ #End)
 ["ex_counter" "var_counter" "var_bindings"]
 .public)

... (type: .public Mode
...   #Build
...   #Eval
...   #Interpreter)
("lux def type tagged" Mode
 (#Named ["library/lux" "Mode"]
         (#Sum ... Build
          Any
          (#Sum ... Eval
           Any
           ... Interpreter
           Any)))
 (record$ #End)
 ("Build" "Eval" "Interpreter")
 .public)

... (type: .public Info
...   {#target  Text
...    #version Text
...    #mode    Mode})
("lux def type tagged" Info
 (#Named ["library/lux" "Info"]
         (#Product
          ... target
          Text
          (#Product
           ... version
           Text
           ... mode
           Mode)))
 (record$ #End)
 ["target" "version" "mode"]
 .public)

... (type: .public Lux
...   {#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})
("lux def type tagged" Lux
 (#Named ["library/lux" "Lux"]
         ({Lux
           (#Apply Nothing
                   (#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 (#Parameter 1) (#Parameter 0))))
 (record$ #End)
 ["info" "source" "location" "current_module" "modules" "scopes" "type_context" "expected" "seed" "scope_type_vars" "extensions" "eval" "host"]
 .public)

... (type: .public (Meta a)
...   (-> Lux (Either Text [Lux a])))
("lux def" Meta
 ("lux type check type"
  (#Named ["library/lux" "Meta"]
          (#UnivQ #End
                  (#Function Lux
                             (#Apply (#Product Lux (#Parameter 1))
                                     (#Apply Text Either))))))
 (record$ #End)
 .public)

... (type: .public Macro'
...   (-> (List Code) (Meta (List Code))))
("lux def" Macro'
 ("lux type check type"
  (#Named ["library/lux" "Macro'"]
          (#Function Code_List (#Apply Code_List Meta))))
 (record$ #End)
 .public)

... (type: .public Macro
...   (primitive "#Macro"))
("lux def" Macro
 ("lux type check type"
  (#Named ["library/lux" "Macro"]
          (#Primitive "#Macro" #End)))
 (record$ #End)
 .public)

... Base functions & macros
("lux def" in_meta
 ("lux type check"
  (#UnivQ #End
          (#Function (#Parameter 1)
                     (#Function Lux
                                (#Apply (#Product Lux
                                                  (#Parameter 1))
                                        (#Apply Text Either)))))
  ([_ val]
   ([_ state]
    (#Right state val))))
 (record$ #End)
 #0)

("lux def" failure
 ("lux type check"
  (#UnivQ #End
          (#Function Text
                     (#Function Lux
                                (#Apply (#Product Lux
                                                  (#Parameter 1))
                                        (#Apply Text Either)))))
  ([_ msg]
   ([_ state]
    (#Left msg))))
 (record$ #End)
 #0)

("lux def" let''
 ("lux macro"
  ([_ tokens]
   ({(#Item lhs (#Item rhs (#Item body #End)))
     (in_meta (#Item (form$ (#Item (record$ (#Item [lhs body] #End)) (#Item rhs #End)))
                     #End))

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

("lux def" function''
 ("lux macro"
  ([_ tokens]
   ({(#Item [_ (#Tuple (#Item arg args'))] (#Item body #End))
     (in_meta (#Item (_ann (#Form (#Item (_ann (#Tuple (#Item (_ann (#Identifier ["" ""]))
                                                              (#Item arg #End))))
                                         (#Item ({#End
                                                  body

                                                  _
                                                  (_ann (#Form (#Item (_ann (#Identifier ["library/lux" "function''"]))
                                                                      (#Item (_ann (#Tuple args'))
                                                                             (#Item body #End)))))}
                                                 args')
                                                #End))))
                     #End))

     (#Item [_ (#Identifier ["" self])] (#Item [_ (#Tuple (#Item arg args'))] (#Item body #End)))
     (in_meta (#Item (_ann (#Form (#Item (_ann (#Tuple (#Item (_ann (#Identifier ["" self]))
                                                              (#Item arg #End))))
                                         (#Item ({#End
                                                  body

                                                  _
                                                  (_ann (#Form (#Item (_ann (#Identifier ["library/lux" "function''"]))
                                                                      (#Item (_ann (#Tuple args'))
                                                                             (#Item body #End)))))}
                                                 args')
                                                #End))))
                     #End))

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

("lux def" location_code
 ("lux type check" Code
  (tuple$ (#Item (text$ "") (#Item (nat$ 0) (#Item (nat$ 0) #End)))))
 (record$ #End)
 #0)

("lux def" meta_code
 ("lux type check" (#Function Name (#Function Code Code))
  ([_ tag]
   ([_ value]
    (tuple$ (#Item location_code
                   (#Item (form$ (#Item (tag$ tag) (#Item value #End)))
                          #End))))))
 (record$ #End)
 #0)

("lux def" flag_meta
 ("lux type check" (#Function Text Code)
  ([_ tag]
   (tuple$ (#Item [(meta_code ["library/lux" "Tag"] (tuple$ (#Item (text$ "library/lux") (#Item (text$ tag) #End))))
                   (#Item [(meta_code ["library/lux" "Bit"] (bit$ #1))
                           #End])]))))
 (record$ #End)
 #0)

("lux def" as_def
 ("lux type check" (#Function Code (#Function Code (#Function Code (#Function Code Code))))
  (function'' [name value annotations export_policy]
              (form$ (#Item (text$ "lux def") (#Item name (#Item value (#Item annotations (#Item export_policy #End))))))))
 (record$ #End)
 #0)

("lux def" as_checked
 ("lux type check" (#Function Code (#Function Code Code))
  (function'' [type value]
              (form$ (#Item (text$ "lux type check") (#Item type (#Item value #End))))))
 (record$ #End)
 #0)

("lux def" as_function
 ("lux type check" (#Function Code (#Function (#Apply Code List) (#Function Code Code)))
  (function'' [self inputs output]
              (form$ (#Item (identifier$ ["library/lux" "function''"])
                            (#Item self
                                   (#Item (tuple$ inputs)
                                          (#Item output #End)))))))
 (record$ #End)
 #0)

("lux def" as_macro
 ("lux type check" (#Function Code Code)
  (function'' [expression]
              (form$ (#Item (text$ "lux macro")
                            (#Item expression
                                   #End)))))
 (record$ #End)
 #0)

("lux def" def:''
 ("lux macro"
  (function'' [tokens]
              ({(#Item [export_policy
                        (#Item [[_ (#Form (#Item [name args]))]
                                (#Item [meta (#Item [type (#Item [body #End])])])])])
                (in_meta (#Item [(as_def name (as_checked type (as_function name args body))
                                         (form$ (#Item (identifier$ ["library/lux" "record$"])
                                                       (#Item meta
                                                              #End)))
                                         export_policy)
                                 #End]))

                (#Item [export_policy (#Item [name (#Item [meta (#Item [type (#Item [body #End])])])])])
                (in_meta (#Item [(as_def name (as_checked type body)
                                         (form$ (#Item (identifier$ ["library/lux" "record$"])
                                                       (#Item meta
                                                              #End)))
                                         export_policy)
                                 #End]))

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

("lux def" macro:'
 ("lux macro"
  (function'' [tokens]
              ({(#Item export_policy (#Item [_ (#Form (#Item name args))] (#Item body #End)))
                (in_meta (#Item (as_def name (as_macro (as_function name args body))
                                        (form$ (#Item (identifier$ ["library/lux" "record$"])
                                                      (#Item (tag$ ["library/lux" "End"])
                                                             #End)))
                                        export_policy)
                                #End))

                (#Item export_policy (#Item [_ (#Form (#Item name args))] (#Item meta_data (#Item body #End))))
                (in_meta (#Item (as_def name (as_macro (as_function name args body))
                                        (form$ (#Item (identifier$ ["library/lux" "record$"])
                                                      (#Item meta_data
                                                             #End)))
                                        export_policy)
                                #End))

                _
                (failure "Wrong syntax for macro:'")}
               tokens)))
 (record$ #End)
 #0)

(macro:' .public (comment tokens)
         #End
         (in_meta #End))

(macro:' .private ($' tokens)
         ({(#Item x #End)
           (in_meta tokens)

           (#Item x (#Item y xs))
           (in_meta (#Item (form$ (#Item (identifier$ ["library/lux" "$'"])
                                         (#Item (form$ (#Item (tag$ ["library/lux" "Apply"])
                                                              (#Item y (#Item x #End))))
                                                xs)))
                           #End))

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

(def:'' .private (list\each f xs)
        #End
        (#UnivQ #End
                (#UnivQ #End
                        (#Function (#Function (#Parameter 3) (#Parameter 1))
                                   (#Function ($' List (#Parameter 3))
                                              ($' List (#Parameter 1))))))
        ({#End
          #End

          (#Item x xs')
          (#Item (f x) (list\each f xs'))}
         xs))

(def:'' .private Replacement_Environment
        #End
        Type
        ($' List (#Product Text Code)))

(def:'' .private (replacement_environment xs ys)
        #End
        (#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)
        #End
        (#Function Text (#Function Text Bit))
        ("lux text =" reference sample))

(def:'' .private (replacement for environment)
        #End
        (#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)
        #End
        (#Function Replacement_Environment (#Function Code Code))
        ({[_ (#Identifier "" name)]
          ({(#Some replacement)
            replacement

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

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

          [meta (#Tuple members)]
          [meta (#Tuple (list\each (with_replacements reps) members))]

          [meta (#Record slots)]
          [meta (#Record (list\each ("lux type check" (#Function (#Product Code Code) (#Product Code Code))
                                     (function'' [slot]
                                                 ({[k v]
                                                   [(with_replacements reps k) (with_replacements reps v)]}
                                                  slot)))
                                    slots))]
          
          _
          syntax}
         syntax))

(def:'' .private (n/* param subject)
        #End
        (#Function Nat (#Function Nat Nat))
        ("lux type as" Nat
         ("lux i64 *"
          ("lux type as" Int param)
          ("lux type as" Int subject))))

(def:'' .private (list\mix f init xs)
        #End
        ... (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\size list)
        #End
        (#UnivQ #End
                (#Function ($' List (#Parameter 1)) Nat))
        (list\mix (function'' [_ acc] ("lux i64 +" 1 acc)) 0 list))

(def:'' .private (let$ binding value body)
        #End
        (#Function Code (#Function Code (#Function Code Code)))
        (form$ (#Item (record$ (#Item [binding body] #End))
                      (#Item value #End))))

(def:'' .private (UnivQ$ body)
        #End
        (#Function Code Code)
        (form$ (#Item (tag$ ["library/lux" "UnivQ"]) (#Item (tag$ ["library/lux" "End"]) (#Item body #End)))))

(def:'' .private (ExQ$ body)
        #End
        (#Function Code Code)
        (form$ (#Item (tag$ ["library/lux" "ExQ"]) (#Item (tag$ ["library/lux" "End"]) (#Item body #End)))))

(def:'' .private quantification_level
        #End
        Text
        ("lux text concat" double_quote
         ("lux text concat" "quantification_level"
          double_quote)))

(def:'' .private quantified
        #End
        (#Function Code Code)
        (let$ (local_identifier$ ..quantification_level) (nat$ 0)))

(def:'' .private (quantified_type_parameter idx)
        #End
        (#Function Nat Code)
        (form$ (#Item (tag$ ["library/lux" "Parameter"])
                      (#Item (form$ (#Item (text$ "lux i64 +")
                                           (#Item (local_identifier$ ..quantification_level)
                                                  (#Item (nat$ idx)
                                                         #End))))
                             #End))))

(def:'' .private (next_level depth)
        #End
        (#Function Nat Nat)
        ("lux i64 +" 2 depth))

(def:'' .private (self_id? id)
        #End
        (#Function Nat Bit)
        ("lux i64 =" id ("lux type as" Nat
                         ("lux i64 *" +2
                          ("lux i64 /" +2
                           ("lux type as" Int
                            id))))))

(def:'' .public (__adjusted_quantified_type__ permission depth type)
        #End
        (#Function Nat (#Function Nat (#Function Type Type)))
        ({0
          ({... Jackpot!
            (#Parameter id)
            ({id'
              ({#0 (#Parameter id')
                #1 (#Parameter ("lux i64 -" 2 id'))}
               (self_id? id))}
             ("lux i64 -" ("lux i64 -" depth id) 0))
            
            ... Recur
            (#Primitive name parameters)
            (#Primitive 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)
        #End
        (#Function Code Code)
        (form$ (#Item (identifier$ [prelude_module "__adjusted_quantified_type__"])
                      (#Item (local_identifier$ ..quantification_level)
                             (#Item (nat$ 0)
                                    (#Item body
                                           #End))))))

(def:'' .private (with_quantification depth body)
        #End
        (#Function Nat (#Function Code Code))
        ({g!level
          (let$ g!level
                (form$ (#Item (text$ "lux i64 +")
                              (#Item g!level
                                     (#Item (nat$ ("lux type as" Nat
                                                   ("lux i64 *" +2
                                                    ("lux type as" Int
                                                     depth))))
                                            #End))))
                body)}
         (local_identifier$ ..quantification_level)))

(def:'' .private (initialized_quantification? lux)
        #End
        (#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
                                  _ ({{#name _ #inner _ #captured _
                                       #locals {#counter _
                                                #mappings locals}}
                                      (list\mix (function'' [local verdict]
                                                            ({[local _]
                                                              ({#1 #1
                                                                _ ("lux text =" ..quantification_level local)}
                                                               verdict)}
                                                             local))
                                                #0
                                                locals)}
                                     scope)}
                                 verdict))
                    #0
                    scopes)}
         lux))

(macro:' .public (All tokens lux)
         #End
         ({(#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']
                                                               [("lux i64 +" 2 offset)
                                                                (let$ parameter (quantified_type_parameter ("lux i64 +" offset 1))
                                                                      (UnivQ$ body'))]}
                                                              offset,body'))
                                                 [0 (with_quantification (list\size args)
                                                      body)]
                                                 args))))}
                             args))
                           #End)])
           
           _
           (#Left "Wrong syntax for All")}
          tokens))

(macro:' .public (Ex tokens lux)
         #End
         ({(#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']
                                                               [("lux i64 +" 2 offset)
                                                                (let$ parameter (quantified_type_parameter ("lux i64 +" offset 1))
                                                                      (ExQ$ body'))]}
                                                              offset,body'))
                                                 [0 (with_quantification (list\size args)
                                                      body)]
                                                 args))))}
                             args))
                           #End)])
           
           _
           (#Left "Wrong syntax for Ex")}
          tokens))

(def:'' .private (list\reversed list)
        #End
        (All (_ a)
          (#Function ($' List a) ($' List a)))
        (list\mix ("lux type check" (All (_ a)
                                      (#Function a (#Function ($' List a) ($' List a))))
                   (function'' [head tail] (#Item head tail)))
                  #End
                  list))

(macro:' .public (-> tokens)
         #End
         ({(#Item output inputs)
           (in_meta (#Item (list\mix ("lux type check" (#Function Code (#Function Code Code))
                                      (function'' [i o] (form$ (#Item (tag$ ["library/lux" "Function"]) (#Item i (#Item o #End))))))
                                     output
                                     inputs)
                           #End))
           
           _
           (failure "Wrong syntax for ->")}
          (list\reversed tokens)))

(macro:' .public (list xs)
         #End
         (in_meta (#Item (list\mix (function'' [head tail]
                                               (form$ (#Item (tag$ ["library/lux" "Item"])
                                                             (#Item (tuple$ (#Item [head (#Item [tail #End])]))
                                                                    #End))))
                                   (tag$ ["library/lux" "End"])
                                   (list\reversed xs))
                         #End)))

(macro:' .public (list& xs)
         #End
         ({(#Item last init)
           (in_meta (list (list\mix (function'' [head tail]
                                                (form$ (list (tag$ ["library/lux" "Item"])
                                                             (tuple$ (list head tail)))))
                                    last
                                    init)))

           _
           (failure "Wrong syntax for list&")}
          (list\reversed xs)))

(macro:' .public (Union tokens)
         #End
         ({#End
           (in_meta (list (identifier$ ["library/lux" "Nothing"])))

           (#Item last prevs)
           (in_meta (list (list\mix (function'' [left right] (form$ (list (tag$ ["library/lux" "Sum"]) left right)))
                                    last
                                    prevs)))}
          (list\reversed tokens)))

(macro:' .public (Tuple tokens)
         #End
         ({#End
           (in_meta (list (identifier$ ["library/lux" "Any"])))

           (#Item last prevs)
           (in_meta (list (list\mix (function'' [left right] (form$ (list (tag$ ["library/lux" "Product"]) left right)))
                                    last
                                    prevs)))}
          (list\reversed tokens)))

(macro:' .private (function' tokens)
         (let'' [name tokens'] ({(#Item [[_ (#Identifier ["" name])] tokens'])
                                 [name tokens']

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

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

(macro:' .private (def:''' tokens)
         ({(#Item [export_policy
                   (#Item [[_ (#Form (#Item [name args]))]
                           (#Item [meta (#Item [type (#Item [body #End])])])])])
           (in_meta (list (form$ (list (text$ "lux def")
                                       name
                                       (form$ (list (text$ "lux type check")
                                                    type
                                                    (form$ (list (identifier$ ["library/lux" "function'"])
                                                                 name
                                                                 (tuple$ args)
                                                                 body))))
                                       (form$ (#Item (identifier$ ["library/lux" "record$"])
                                                     (#Item meta
                                                            #End)))
                                       export_policy))))

           (#Item [export_policy (#Item [name (#Item [meta (#Item [type (#Item [body #End])])])])])
           (in_meta (list (form$ (list (text$ "lux def")
                                       name
                                       (form$ (list (text$ "lux type check")
                                                    type
                                                    body))
                                       (form$ (#Item (identifier$ ["library/lux" "record$"])
                                                     (#Item meta
                                                            #End)))
                                       export_policy))))

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

(def:''' .public Or
         #End
         Macro
         ..Union)

(def:''' .public And
         #End
         Macro
         ..Tuple)

(def:''' .private (pairs xs)
         #End
         (All (_ a) (-> ($' List a) ($' List (Tuple a a))))
         ({(#Item x (#Item y xs'))
           (#Item [x y] (pairs xs'))

           _
           #End}
          xs))

(macro:' .private (let' tokens)
         ({(#Item [[_ (#Tuple bindings)] (#Item [body #End])])
           (in_meta (list (list\mix ("lux type check" (-> (Tuple Code Code) Code
                                                          Code)
                                     (function' [binding body]
                                                ({[label value]
                                                  (form$ (list (record$ (list [label body])) value))}
                                                 binding)))
                                    body
                                    (list\reversed (pairs bindings)))))

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

(def:''' .private (any? p xs)
         #End
         (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)
         #End
         (-> Code Code)
         (tuple$ (list (tuple$ (list (text$ "") (nat$ 0) (nat$ 0)))
                       content)))

(def:''' .private (untemplated_list tokens)
         #End
         (-> ($' List Code) Code)
         ({#End
           (_ann (#Tag ["library/lux" "End"]))

           (#Item [token tokens'])
           (_ann (#Form (list (_ann (#Tag ["library/lux" "Item"])) token (untemplated_list tokens'))))}
          tokens))

(def:''' .private (list\composite xs ys)
         #End
         (All (_ a) (-> ($' List a) ($' List a) ($' List a)))
         ({(#Item x xs')
           (#Item x (list\composite xs' ys))

           #End
           ys}
          xs))

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

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

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

(macro:' .public (_$ tokens)
         #End
         ({(#Item op tokens')
           ({(#Item first nexts)
             (in_meta (list (list\mix (function\flipped (right_associativity op)) first nexts)))

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

(macro:' .public ($_ tokens)
         #End
         ({(#Item op tokens')
           ({(#Item last prevs)
             (in_meta (list (list\mix (right_associativity op) last prevs)))

             _
             (failure "Wrong syntax for $_")}
            (list\reversed tokens'))
           
           _
           (failure "Wrong syntax for $_")}
          tokens))

... (type: (Monad m)
...   (Interface
...    (: (All (_ a) (-> a (m a)))
...       in)
...    (: (All (_ a b) (-> (-> a (m b)) (m a) (m b)))
...       then)))
("lux def type tagged" Monad
 (#Named ["library/lux" "Monad"]
         (All (_ !)
           (Tuple (All (_ a)
                    (-> a ($' ! a)))
                  (All (_ a b)
                    (-> (-> a ($' ! b))
                        ($' ! a)
                        ($' ! b))))))
 (record$ (list))
 ["in" "then"]
 #0)

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

(def:''' .private meta_monad
         #End
         ($' 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))))})

(macro:' .private (do tokens)
         ({(#Item monad (#Item [_ (#Tuple bindings)] (#Item body #End)))
           (let' [g!in (local_identifier$ "in")
                  g!then (local_identifier$ " then ")
                  body' (list\mix ("lux type check" (-> (Tuple Code Code) Code Code)
                                   (function' [binding body']
                                              (let' [[var value] binding]
                                                    ({[_ (#Identifier [module short])]
                                                      ({""
                                                        (form$ (list g!then
                                                                     (form$ (list (tuple$ (list (local_identifier$ "") var)) body'))
                                                                     value))

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

                                                      _
                                                      (form$ (list g!then
                                                                   (form$ (list (tuple$ (list (local_identifier$ "") var)) body'))
                                                                   value))}
                                                     var))))
                                  body
                                  (list\reversed (pairs bindings)))]
                 (in_meta (list (form$ (list (record$ (list [(record$ (list [(tag$ ["library/lux" "in"]) g!in] [(tag$ ["library/lux" "then"]) g!then]))
                                                             body']))
                                             monad)))))

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

(def:''' .private (monad\each m f xs)
         #End
         (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\mix m f y xs)
         #End
         (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)))

(macro:' .public (if tokens)
         (list)
         ({(#Item test (#Item then (#Item else #End)))
           (in_meta (list (form$ (list (record$ (list [(bit$ #1)  then]
                                                      [(bit$ #0) else]))
                                       test))))

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

(def:''' .private PList
         #End
         Type
         (All (_ a) ($' List (Tuple Text a))))

(def:''' .private (plist\value k plist)
         #End
         (All (_ a)
           (-> Text ($' PList a) ($' Maybe a)))
         ({(#Item [[k' v] plist'])
           (if (text\= k k')
             (#Some v)
             (plist\value k plist'))

           #End
           #None}
          plist))

(def:''' .private (text\composite x y)
         #End
         (-> Text Text Text)
         ("lux text concat" x y))

(def:''' .private (name\encoded full_name)
         #End
         (-> Name Text)
         (let' [[module name] full_name]
               ({"" name
                 _  ($_ text\composite module "." name)}
                module)))

(def:''' .private (global_identifier full_name state)
         #End
         (-> Name ($' Meta 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} state]
               ({(#Some {#module_hash _ #module_aliases _ #definitions definitions #imports _ #module_annotations _ #module_state _})
                 ({(#Some constant)
                   ({(#Alias real_name)
                     (#Right [state real_name])
                     
                     (#Definition [exported? def_type def_meta def_value])
                     (#Right [state full_name])

                     (#Type [exported? type labels])
                     (#Right [state full_name])

                     (#Label _)
                     (#Left ($_ text\composite "Unknown definition: " (name\encoded full_name)))

                     (#Slot _)
                     (#Left ($_ text\composite "Unknown definition: " (name\encoded full_name)))}
                    constant)

                   #None
                   (#Left ($_ text\composite "Unknown definition: " (name\encoded full_name)))}
                  (plist\value name definitions))
                 
                 #None
                 (#Left ($_ text\composite "Unknown module: " module " @ " (name\encoded full_name)))}
                (plist\value module modules))))

(def:''' .private (code_list expression)
         #End
         (-> Code Code)
         (let' [type (form$ (list (tag$ ["library/lux" "Apply"])
                                  (identifier$ ["library/lux" "Code"])
                                  (identifier$ ["library/lux" "List"])))]
               (form$ (list (text$ "lux type check") type expression))))

(def:''' .private (spliced replace? untemplated elems)
         #End
         (-> Bit (-> Code ($' Meta Code)) ($' List Code) ($' Meta Code))
         ({#1
           ({#End
             (in_meta (tag$ ["library/lux" "End"]))
             
             (#Item lastI inits)
             (do meta_monad
               [lastO ({[_ (#Form (#Item [[_ (#Identifier ["" "~+"])] (#Item [spliced #End])]))]
                        (in (code_list spliced))

                        _
                        (do meta_monad
                          [lastO (untemplated lastI)]
                          (in (code_list (form$ (list (tag$ ["library/lux" "Item"])
                                                      (tuple$ (list lastO (tag$ ["library/lux" "End"]))))))))}
                       lastI)]
               (monad\mix meta_monad
                          (function' [leftI rightO]
                                     ({[_ (#Form (#Item [[_ (#Identifier ["" "~+"])] (#Item [spliced #End])]))]
                                       (let' [g!in-module (form$ (list (text$ "lux in-module")
                                                                       (text$ "library/lux")
                                                                       (identifier$ ["library/lux" "list\composite"])))]
                                             (in (form$ (list g!in-module (code_list spliced) rightO))))

                                       _
                                       (do meta_monad
                                         [leftO (untemplated leftI)]
                                         (in (form$ (list (tag$ ["library/lux" "Item"]) (tuple$ (list leftO rightO))))))}
                                      leftI))
                          lastO
                          inits))}
            (list\reversed elems))
           #0
           (do meta_monad
             [=elems (monad\each meta_monad untemplated elems)]
             (in (untemplated_list =elems)))}
          replace?))

(def:''' .private (untemplated_text value)
         #End
         (-> Text Code)
         (with_location (form$ (list (tag$ ["library/lux" "Text"]) (text$ value)))))

(def:''' .private (untemplated replace? subst token)
         #End
         (-> Bit Text Code ($' Meta Code))
         ({[_ [_ (#Bit value)]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Bit"]) (bit$ value)))))

           [_ [_ (#Nat value)]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Nat"]) (nat$ value)))))

           [_ [_ (#Int value)]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Int"]) (int$ value)))))

           [_ [_ (#Rev value)]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Rev"]) (rev$ value)))))
           
           [_ [_ (#Frac value)]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Frac"]) (frac$ value)))))

           [_ [_ (#Text value)]]
           (in_meta (untemplated_text value))

           [#0 [_ (#Tag [module name])]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Tag"]) (tuple$ (list (text$ module) (text$ name)))))))

           [#1 [_ (#Tag [module name])]]
           (let' [module' ({""
                            subst

                            _
                            module}
                           module)]
                 (in_meta (with_location (form$ (list (tag$ ["library/lux" "Tag"]) (tuple$ (list (text$ module') (text$ name))))))))

           [#1 [_ (#Identifier [module name])]]
           (do meta_monad
             [real_name ({""
                          (if (text\= "" subst)
                            (in [module name])
                            (global_identifier [subst name]))

                          _
                          (in [module name])}
                         module)
              .let' [[module name] real_name]]
             (in_meta (with_location (form$ (list (tag$ ["library/lux" "Identifier"]) (tuple$ (list (text$ module) (text$ name))))))))

           [#0 [_ (#Identifier [module name])]]
           (in_meta (with_location (form$ (list (tag$ ["library/lux" "Identifier"]) (tuple$ (list (text$ module) (text$ name)))))))

           [#1 [_ (#Form (#Item [[_ (#Identifier ["" "~"])] (#Item [unquoted #End])]))]]
           (in_meta (form$ (list (text$ "lux type check")
                                 (identifier$ ["library/lux" "Code"])
                                 unquoted)))

           [#1 [_ (#Form (#Item [[_ (#Identifier ["" "~!"])] (#Item [dependent #End])]))]]
           (do meta_monad
             [independent (untemplated replace? subst dependent)]
             (in (with_location (form$ (list (tag$ ["library/lux" "Form"])
                                             (untemplated_list (list (untemplated_text "lux in-module")
                                                                     (untemplated_text subst)
                                                                     independent)))))))

           [#1 [_ (#Form (#Item [[_ (#Identifier ["" "~'"])] (#Item [keep_quoted #End])]))]]
           (untemplated #0 subst keep_quoted)

           [_ [meta (#Form elems)]]
           (do meta_monad
             [output (spliced replace? (untemplated replace? subst) elems)
              .let' [[_ output'] (with_location (form$ (list (tag$ ["library/lux" "Form"]) output)))]]
             (in [meta output']))

           [_ [meta (#Tuple elems)]]
           (do meta_monad
             [output (spliced replace? (untemplated replace? subst) elems)
              .let' [[_ output'] (with_location (form$ (list (tag$ ["library/lux" "Tuple"]) output)))]]
             (in [meta output']))

           [_ [_ (#Record fields)]]
           (do meta_monad
             [=fields (monad\each meta_monad
                                  ("lux type check" (-> (Tuple Code Code) ($' Meta Code))
                                   (function' [kv]
                                              (let' [[k v] kv]
                                                    (do meta_monad
                                                      [=k (untemplated replace? subst k)
                                                       =v (untemplated replace? subst v)]
                                                      (in (tuple$ (list =k =v)))))))
                                  fields)]
             (in (with_location (form$ (list (tag$ ["library/lux" "Record"]) (untemplated_list =fields))))))}
          [replace? token]))

(macro:' .public (primitive tokens)
         (list)
         ({(#Item [_ (#Text class_name)] #End)
           (in_meta (list (form$ (list (tag$ ["library/lux" "Primitive"]) (text$ class_name) (tag$ ["library/lux" "End"])))))

           (#Item [_ (#Text class_name)] (#Item [_ (#Tuple params)] #End))
           (in_meta (list (form$ (list (tag$ ["library/lux" "Primitive"]) (text$ class_name) (untemplated_list params)))))

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

(def:'' .private (current_module_name state)
        #End
        ($' 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))

(macro:' .public (` tokens)
         (list)
         ({(#Item template #End)
           (do meta_monad
             [current_module current_module_name
              =template (untemplated #1 current_module template)]
             (in (list (form$ (list (text$ "lux type check")
                                    (identifier$ ["library/lux" "Code"])
                                    =template)))))

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

(macro:' .public (`' tokens)
         (list)
         ({(#Item template #End)
           (do meta_monad
             [=template (untemplated #1 "" template)]
             (in (list (form$ (list (text$ "lux type check") (identifier$ ["library/lux" "Code"]) =template)))))

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

(macro:' .public (' tokens)
         (list)
         ({(#Item template #End)
           (do meta_monad
             [=template (untemplated #0 "" template)]
             (in (list (form$ (list (text$ "lux type check") (identifier$ ["library/lux" "Code"]) =template)))))

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

(macro:' .public (|> tokens)
         (list)
         ({(#Item [init apps])
           (in_meta (list (list\mix ("lux type check" (-> Code Code Code)
                                     (function' [app 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 for |>")}
          tokens))

(macro:' .public (<| tokens)
         (list)
         ({(#Item [init apps])
           (in_meta (list (list\mix ("lux type check" (-> Code Code Code)
                                     (function' [app 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 for <|")}
          (list\reversed tokens)))

(def:''' .private (function\composite f g)
         (list [(tag$ ["library/lux" "doc"])
                (text$ "Function composition.")])
         (All (_ a b c)
           (-> (-> b c) (-> a b) (-> a c)))
         (function' [x] (f (g x))))

(def:''' .private (identifier_name x)
         #End
         (-> Code ($' Maybe Name))
         ({[_ (#Identifier sname)]
           (#Some sname)

           _
           #None}
          x))

(def:''' .private (tag_name x)
         #End
         (-> Code ($' Maybe Name))
         ({[_ (#Tag sname)]
           (#Some sname)

           _
           #None}
          x))

(def:''' .private (identifier_short x)
         #End
         (-> Code ($' Maybe Text))
         ({[_ (#Identifier "" sname)]
           (#Some sname)

           _
           #None}
          x))

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

           _
           #None}
          tuple))

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

             _
             template}
            (..replacement sname env))

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

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

           [meta (#Record members)]
           [meta (#Record (list\each ("lux type check" (-> (Tuple Code Code) (Tuple Code Code))
                                      (function' [kv]
                                                 (let' [[slot value] kv]
                                                       [(realized_template env slot) (realized_template env value)])))
                                     members))]

           _
           template}
          template))

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

(def:''' .private (high_bits value)
         (list)
         (-> ($' I64 Any) I64)
         ("lux i64 right-shift" 32 value))

(def:''' .private low_mask
         (list)
         I64
         (|> 1 ("lux i64 left-shift" 32) ("lux i64 -" 1)))

(def:''' .private (low_bits value)
         (list)
         (-> ($' I64 Any) I64)
         ("lux i64 and" low_mask value))

(def:''' .private (n/< reference sample)
         (list)
         (-> Nat Nat Bit)
         (let' [referenceH (high_bits reference)
                sampleH (high_bits sample)]
               (if ("lux i64 <" referenceH sampleH)
                 #1
                 (if ("lux i64 =" referenceH sampleH)
                   ("lux i64 <"
                    (low_bits reference)
                    (low_bits sample))
                   #0))))

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

(macro:' .public (template tokens)
         (list)
         ({(#Item [[_ (#Tuple bindings)] (#Item [[_ (#Tuple templates)] data])])
           ({[(#Some bindings') (#Some data')]
             (let' [apply ("lux type check" (-> Replacement_Environment ($' List Code))
                           (function' [env] (list\each (realized_template env) templates)))
                    num_bindings (list\size bindings')]
                   (if (every? (function' [size] ("lux i64 =" num_bindings size))
                               (list\each list\size data'))
                     (|> data'
                         (list\each (function\composite apply (replacement_environment bindings')))
                         list\conjoint
                         in_meta)
                     (failure "Irregular arguments tuples for template.")))

             _
             (failure "Wrong syntax for template")}
            [(monad\each maybe_monad identifier_short bindings)
             (monad\each maybe_monad tuple_list data)])

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

(def:''' .private (n// param subject)
         (list)
         (-> Nat Nat Nat)
         (if ("lux i64 <" +0 ("lux type as" Int param))
           (if (n/< param subject)
             0
             1)
           (let' [quotient (|> subject
                               ("lux i64 right-shift" 1)
                               ("lux i64 /" ("lux type as" Int param))
                               ("lux i64 left-shift" 1))
                  flat ("lux i64 *"
                        ("lux type as" Int param)
                        ("lux type as" Int quotient))
                  remainder ("lux i64 -" flat subject)]
                 (if (n/< param remainder)
                   quotient
                   ("lux i64 +" 1 quotient)))))

(def:''' .private (n/% param subject)
         (list)
         (-> Nat Nat Nat)
         (let' [flat ("lux i64 *"
                      ("lux type as" Int param)
                      ("lux type as" Int (n// param subject)))]
               ("lux i64 -" flat subject)))

(def:''' .private (n/min left right)
         (list)
         (-> Nat Nat Nat)
         (if (n/< right left)
           left
           right))

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

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

(def:''' .private (nat\encoded value)
         #End
         (-> Nat Text)
         ({0
           "0"

           _
           (let' [loop ("lux type check" (-> Nat Text Text)
                        (function' recur [input output]
                                   (if ("lux i64 =" 0 input)
                                     output
                                     (recur (n// 10 input)
                                            (text\composite (|> input (n/% 10) digit::format)
                                                            output)))))]
                 (loop value ""))}
          value))

(def:''' .private (int\abs value)
         #End
         (-> Int Int)
         (if ("lux i64 <" +0 value)
           ("lux i64 *" -1 value)
           value))

(def:''' .private (int\encoded value)
         #End
         (-> Int Text)
         (if ("lux i64 =" +0 value)
           "+0"
           (let' [sign (if ("lux i64 <" value +0)
                         "+"
                         "-")]
                 (("lux type check" (-> Int Text Text)
                   (function' recur [input output]
                              (if ("lux i64 =" +0 input)
                                (text\composite sign output)
                                (recur ("lux i64 /" +10 input)
                                       (text\composite (|> input ("lux i64 %" +10) ("lux type as" Nat) digit::format)
                                                       output)))))
                  (|> value ("lux i64 /" +10) int\abs)
                  (|> value ("lux i64 %" +10) int\abs ("lux type as" Nat) digit::format)))))

(def:''' .private (frac\encoded x)
         #End
         (-> Frac Text)
         ("lux f64 encode" x))

(def:''' .private (multiple? div n)
         #End
         (-> Nat Nat Bit)
         (|> n (n/% div) ("lux i64 =" 0)))

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

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

           _
           #0}
          type))

(def:''' .private (macro'' modules current_module module name)
         #End
         (-> ($' List (Tuple Text Module))
             Text Text Text
             ($' Maybe Macro))
         (do maybe_monad
           [$module (plist\value module modules)
            gdef (let' [{#module_hash _ #module_aliases _ #definitions bindings #imports _ #module_annotations _ #module_state _} ("lux type check" Module $module)]
                       (plist\value name bindings))]
           ({(#Alias [r_module r_name])
             (macro'' modules current_module r_module r_name)

             (#Definition [exported? def_type def_meta def_value])
             (if (macro_type? def_type)
               (if exported?
                 (#Some ("lux type as" Macro def_value))
                 (if (text\= module current_module)
                   (#Some ("lux type as" Macro def_value))
                   #None))
               #None)

             (#Type [exported? type labels])
             #None

             (#Label _)
             #None

             (#Slot _)
             #None}
            ("lux type check" Global gdef))))

(def:''' .private (normal name)
         #End
         (-> Name ($' Meta Name))
         ({["" name]
           (do meta_monad
             [module_name current_module_name]
             (in [module_name name]))

           _
           (in_meta name)}
          name))

(def:''' .private (macro' full_name)
         #End
         (-> Name ($' Meta ($' Maybe Macro)))
         (do meta_monad
           [current_module current_module_name]
           (let' [[module name] full_name]
                 (function' [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 (macro'' modules current_module module name))}
                             state)))))

(def:''' .private (macro? name)
         #End
         (-> Name ($' Meta Bit))
         (do meta_monad
           [name (normal name)
            output (macro' name)]
           (in ({(#Some _) #1
                 #None     #0}
                output))))

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

           (#Item [x #End])
           xs

           (#Item [x xs'])
           (list& x sep (list\interposed sep xs'))}
          xs))

(def:''' .private (single_expansion token)
         #End
         (-> Code ($' Meta ($' List Code)))
         ({[_ (#Form (#Item [_ (#Identifier name)] args))]
           (do meta_monad
             [name' (normal name)
              ?macro (macro' name')]
             ({(#Some macro)
               (("lux type as" Macro' macro) args)
               
               #None
               (in_meta (list token))}
              ?macro))

           _
           (in_meta (list token))}
          token))

(def:''' .private (expansion token)
         #End
         (-> Code ($' Meta ($' List Code)))
         ({[_ (#Form (#Item [_ (#Identifier name)] args))]
           (do meta_monad
             [name' (normal name)
              ?macro (macro' name')]
             ({(#Some macro)
               (do meta_monad
                 [top_level_expansion (("lux type as" Macro' macro) args)
                  recursive_expansion (monad\each meta_monad expansion top_level_expansion)]
                 (in (list\conjoint recursive_expansion)))
               
               #None
               (in_meta (list token))}
              ?macro))

           _
           (in_meta (list token))}
          token))

(def:''' .private (full_expansion syntax)
         #End
         (-> Code ($' Meta ($' List Code)))
         ({[_ (#Form (#Item [_ (#Identifier name)] args))]
           (do meta_monad
             [name' (normal name)
              ?macro (macro' name')]
             ({(#Some macro)
               (do meta_monad
                 [expansion (("lux type as" Macro' macro) args)
                  expansion' (monad\each meta_monad full_expansion expansion)]
                 (in (list\conjoint expansion')))
               
               #None
               (do meta_monad
                 [args' (monad\each meta_monad full_expansion args)]
                 (in (list (form$ (#Item (identifier$ name) (list\conjoint args'))))))}
              ?macro))

           [_ (#Form members)]
           (do meta_monad
             [members' (monad\each meta_monad full_expansion members)]
             (in (list (form$ (list\conjoint members')))))

           [_ (#Tuple members)]
           (do meta_monad
             [members' (monad\each meta_monad full_expansion members)]
             (in (list (tuple$ (list\conjoint members')))))

           [_ (#Record pairs)]
           (do meta_monad
             [pairs' (monad\each meta_monad
                                 (function' [kv]
                                            (let' [[key val] kv]
                                                  (do meta_monad
                                                    [val' (full_expansion val)]
                                                    ({(#Item val'' #End)
                                                      (in_meta [key val''])

                                                      _
                                                      (failure "The value-part of a KV-pair in a record must macro-expand to a single Code.")}
                                                     val'))))
                                 pairs)]
             (in (list (record$ pairs'))))

           _
           (in_meta (list syntax))}
          syntax))

(def:''' .private (text\encoded original)
         #End
         (-> Text Text)
         ($_ text\composite ..double_quote original ..double_quote))

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

           [_ (#Nat value)]
           (nat\encoded value)

           [_ (#Int value)]
           (int\encoded value)

           [_ (#Rev value)]
           ("lux io error" "@code\encoded Undefined behavior.")
           
           [_ (#Frac value)]
           (frac\encoded value)

           [_ (#Text value)]
           (text\encoded value)
           
           [_ (#Identifier [module name])]
           (if (text\= "" module)
             name
             ($_ text\composite module "." name))
           
           [_ (#Tag [module name])]
           (if (text\= "" module)
             ($_ text\composite "#" name)
             ($_ text\composite "#" 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 "")) "]")
           
           [_ (#Record kvs)]
           ($_ text\composite "{" (|> kvs
                                      (list\each (function' [kv] ({[k v] ($_ text\composite (code\encoded k) " " (code\encoded v))}
                                                                  kv)))
                                      (list\interposed " ")
                                      list\reversed
                                      (list\mix text\composite "")) "}")}
          code))

(def:''' .private (normal_type type)
         #End
         (-> Code Code)
         ({[_ (#Form (#Item [_ (#Tag tag)] parts))]
           (form$ (#Item (tag$ tag) (list\each normal_type parts)))

           [_ (#Tuple members)]
           (` (Tuple (~+ (list\each normal_type members))))

           [_ (#Form (#Item [_ (#Text "lux in-module")]
                            (#Item [_ (#Text module)]
                                   (#Item type'
                                          #End))))]
           (` ("lux in-module" (~ (text$ module)) (~ (normal_type type'))))

           [_ (#Form (#Item [_ (#Identifier ["" ":~"])] (#Item expression #End)))]
           expression

           [_0 (#Form (#Item [_1 (#Record (#Item [binding body] #End))]
                             (#Item value
                                    #End)))]
           [_0 (#Form (#Item [_1 (#Record (#Item [binding (normal_type body)] #End))]
                             (#Item value
                                    #End)))]

           [_0 (#Form (#Item [_1 (#Identifier ["library/lux" "__adjusted_quantified_type__"])]
                             (#Item _permission
                                    (#Item _level
                                           (#Item body
                                                  #End)))))]
           [_0 (#Form (#Item [_1 (#Identifier ["library/lux" "__adjusted_quantified_type__"])]
                             (#Item _permission
                                    (#Item _level
                                           (#Item (normal_type body)
                                                  #End)))))]

           [_ (#Form (#Item type_fn args))]
           (list\mix ("lux type check" (-> Code Code Code)
                      (function' [arg type_fn] (` (#.Apply (~ arg) (~ type_fn)))))
                     (normal_type type_fn)
                     (list\each normal_type args))

           _
           type}
          type))

(macro:' .public (type tokens)
         (list)
         ({(#Item type #End)
           (do meta_monad
             [initialized_quantification? (function' [lux] (#Right [lux (initialized_quantification? lux)]))]
             (if initialized_quantification?
               (do meta_monad
                 [type+ (full_expansion type)]
                 ({(#Item type' #End)
                   (in (list (normal_type type')))

                   _
                   (failure "The expansion of the type-syntax had to yield a single element.")}
                  type+))
               (in (list (..quantified (` (..type (~ type))))))))

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

(macro:' .public (: tokens)
         (list)
         ({(#Item type (#Item value #End))
           (in_meta (list (` ("lux type check"
                              (..type (~ type))
                              (~ value)))))

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

(macro:' .public (:as tokens)
         (list)
         ({(#Item type (#Item value #End))
           (in_meta (list (` ("lux type as"
                              (..type (~ type))
                              (~ value)))))

           _
           (failure "Wrong syntax for :as")}
          tokens))

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

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

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

(def:''' .private (identifier prefix state)
         #End
         (-> 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   ("lux i64 +" 1 seed) #expected expected
                    #location location #extensions extensions
                    #scope_type_vars scope_type_vars #eval _eval}
                   (local_identifier$ ($_ text\composite "__gensym__" prefix (nat\encoded seed))))}
          state))

(macro:' .public (exec tokens)
         (list)
         ({(#Item value actions)
           (let' [dummy (local_identifier$ "")]
                 (in_meta (list (list\mix ("lux type check" (-> Code Code Code)
                                           (function' [pre post] (` ({(~ dummy) (~ post)}
                                                                     (~ pre)))))
                                          value
                                          actions))))

           _
           (failure "Wrong syntax for exec")}
          (list\reversed tokens)))

(macro:' .private (def:' tokens)
         (let' [parts (: (Maybe [Code Code (List Code) (Maybe Code) Code])
                         ({(#Item export_policy (#Item [_ (#Form (#Item name args))] (#Item type (#Item body #End))))
                           (#Some [export_policy name args (#Some type) body])
                           
                           (#Item export_policy (#Item name (#Item type (#Item body #End))))
                           (#Some [export_policy name #End (#Some type) body])
                           
                           (#Item export_policy (#Item [_ (#Form (#Item name args))] (#Item body #End)))
                           (#Some [export_policy name args #None body])
                           
                           (#Item export_policy (#Item name (#Item body #End)))
                           (#Some [export_policy name #End #None body])

                           _
                           #None}
                          tokens))]
               ({(#Some [export_policy name args ?type body])
                 (let' [body' ({#End
                                body

                                _
                                (` (function' (~ name) [(~+ args)] (~ body)))}
                               args)
                        body'' ({(#Some type)
                                 (` (: (~ type) (~ body')))
                                 
                                 #None
                                 body'}
                                ?type)]
                       (in_meta (list (` ("lux def" (~ name)
                                          (~ body'')
                                          [(~ location_code)
                                           (#.Record #.End)]
                                          (~ export_policy))))))
                 
                 #None
                 (failure "Wrong syntax for def'")}
                parts)))

(def:' .private (expander branches)
       (-> (List Code) (Meta (List Code)))
       ({(#Item [_ (#Form (#Item [_ (#Identifier name)] args))]
                (#Item body
                       branches'))
         (do meta_monad
           [??? (macro? name)]
           (if ???
             (do meta_monad
               [init_expansion (single_expansion (form$ (list& (identifier$ name) (form$ args) body branches')))]
               (expander init_expansion))
             (do meta_monad
               [sub_expansion (expander branches')]
               (in (list& (form$ (list& (identifier$ name) args))
                          body
                          sub_expansion)))))

         (#Item pattern (#Item body branches'))
         (do meta_monad
           [sub_expansion (expander branches')]
           (in (list& pattern body sub_expansion)))

         #End
         (do meta_monad [] (in (list)))

         _
         (failure ($_ text\composite "'lux.case' expects an even number of tokens: " (|> branches
                                                                                         (list\each code\encoded)
                                                                                         (list\interposed " ")
                                                                                         list\reversed
                                                                                         (list\mix text\composite ""))))}
        branches))

(macro:' .public (case tokens)
         (list)
         ({(#Item value branches)
           (do meta_monad
             [expansion (expander branches)]
             (in (list (` ((~ (record$ (pairs expansion))) (~ value))))))

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

(macro:' .public (^ tokens)
         (list)
         (case tokens
           (#Item [_ (#Form (#Item pattern #End))] (#Item body branches))
           (do meta_monad
             [pattern+ (full_expansion pattern)]
             (case pattern+
               (#Item pattern' #End)
               (in (list& pattern' body branches))
               
               _
               (failure "^ can only expand to 1 pattern.")))
           
           _
           (failure "Wrong syntax for ^ macro")))

(macro:' .public (^or tokens)
         (list)
         (case tokens
           (^ (list& [_ (#Form patterns)] body branches))
           (case patterns
             #End
             (failure "^or cannot have 0 patterns")

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

(def:' .private (identifier? code)
       (-> Code Bit)
       (case code
         [_ (#Identifier _)]
         #1

         _
         #0))

(macro:' .public (let tokens)
         (list)
         (case tokens
           (^ (list [_ (#Tuple bindings)] body))
           (if (multiple? 2 (list\size bindings))
             (|> bindings pairs list\reversed
                 (list\mix (: (-> [Code Code] Code Code)
                              (function' [lr body']
                                         (let' [[l r] lr]
                                               (if (identifier? l)
                                                 (` ({(~ l) (~ body')} (~ r)))
                                                 (` (case (~ r) (~ l) (~ body')))))))
                           body)
                 list
                 in_meta)
             (failure "let requires an even number of parts"))

           _
           (failure "Wrong syntax for let")))

(macro:' .public (function tokens)
         (list)
         (case (: (Maybe [Text Code (List Code) Code])
                  (case tokens
                    (^ (list [_ (#Form (list& [_ (#Identifier ["" name])] head tail))] body))
                    (#Some name head tail body)
                    
                    _
                    #None))
           (#Some g!name head tail body)
           (let [g!blank (local_identifier$ "")
                 nest (: (-> Code (-> Code Code Code))
                         (function' [g!name]
                                    (function' [arg body']
                                               (if (identifier? arg)
                                                 (` ([(~ g!name) (~ arg)] (~ body')))
                                                 (` ([(~ g!name) (~ g!blank)]
                                                     (.case (~ g!blank) (~ arg) (~ body'))))))))]
             (in_meta (list (nest (..local_identifier$ g!name) head
                                  (list\mix (nest g!blank) body (list\reversed tail))))))

           #None
           (failure "Wrong syntax for function")))

(def:' .private (definition_annotation_value code)
       (-> Code Code)
       (case code
         [_ (#Bit value)]
         (meta_code ["library/lux" "Bit"] (bit$ value))
         
         [_ (#Nat value)]
         (meta_code ["library/lux" "Nat"] (nat$ value))

         [_ (#Int value)]
         (meta_code ["library/lux" "Int"] (int$ value))

         [_ (#Rev value)]
         (meta_code ["library/lux" "Rev"] (rev$ value))

         [_ (#Frac value)]
         (meta_code ["library/lux" "Frac"] (frac$ value))

         [_ (#Text value)]
         (meta_code ["library/lux" "Text"] (text$ value))

         [_ (#Tag [module name])]
         (meta_code ["library/lux" "Tag"] (` [(~ (text$ module)) (~ (text$ name))]))

         (^or [_ (#Form _)] [_ (#Identifier _)])
         code

         [_ (#Tuple xs)]
         (|> xs
             (list\each definition_annotation_value)
             untemplated_list
             (meta_code ["library/lux" "Tuple"]))

         [_ (#Record kvs)]
         (|> kvs
             (list\each (: (-> [Code Code] Code)
                           (function (_ [k v])
                             (` [(~ (definition_annotation_value k))
                                 (~ (definition_annotation_value v))]))))
             untemplated_list
             (meta_code ["library/lux" "Record"]))
         ))

(def:' .private (definition_annotations kvs)
       (-> (List [Code Code]) Code)
       (untemplated_list (list\each (: (-> [Code Code] Code)
                                       (function (_ [k v])
                                         (` [(~ (definition_annotation_value k))
                                             (~ (definition_annotation_value v))])))
                                    kvs)))

(def:' .private (endP tokens)
       (-> (List Code) (Maybe Any))
       (case tokens
         (^ (list))
         (#Some [])

         _
         #None))

(def:' .private (anyP tokens)
       (-> (List Code) (Maybe [(List Code) Code]))
       (case tokens
         (^ (list& code tokens'))
         (#Some [tokens' code])

         _
         #None))

(def:' .private (local_identifierP tokens)
       (-> (List Code) (Maybe [(List Code) Text]))
       (case tokens
         (^ (list& [_ (#Identifier ["" local_identifier])] tokens'))
         (#Some [tokens' local_identifier])

         _
         #None))

(template [<parser> <item_type> <item_parser>]
  [(def:' .private (<parser> tokens)
          (-> (List Code) (Maybe (List <item_type>)))
          (case tokens
            #End
            (#Some #End)

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

  [parametersP Text local_identifierP]
  [enhanced_parametersP Code anyP]
  )

(template [<parser> <parameter_type> <parameters_parser>]
  [(def:' .private (<parser> tokens)
          (-> (List Code) (Maybe [(List Code) [Text (List <parameter_type>)]]))
          (case tokens
            (^ (list& [_ (#Form local_declaration)] tokens'))
            (do maybe_monad
              [% (local_identifierP local_declaration)
               .let' [[local_declaration name] %]
               parameters (<parameters_parser> local_declaration)]
              (in [tokens' [name parameters]]))
            
            _
            (do maybe_monad
              [% (local_identifierP tokens)
               .let' [[tokens' name] %]]
              (in [tokens' [name #End]]))))]

  [local_declarationP Text parametersP]
  [enhanced_local_declarationP Code enhanced_parametersP]
  )

(template [<parser> <parameter_type> <local>]
  [(def:' .private (<parser> tokens)
          (-> (List Code) (Maybe [(List Code) [Code Text (List <parameter_type>)]]))
          (do maybe_monad
            [% (anyP tokens)
             .let' [[tokens export_policy] %]
             % (<local> tokens)
             .let' [[tokens [name parameters]] %]]
            (in [tokens [export_policy name parameters]])))]

  [declarationP Text local_declarationP]
  [enhanced_declarationP Code enhanced_local_declarationP]
  )

(def:' .private (annotationsP tokens)
       (-> (List Code) (Maybe [(List Code) (List [Code Code])]))
       (case tokens
         (^ (list& [_ (#Record annotations)] tokens'))
         (#Some [tokens' annotations])

         tokens'
         #None))

(def:' .private (bodyP tokens)
       (-> (List Code) (Maybe [(List Code) [(Maybe Code) Code]]))
       (case tokens
         ... TB
         (^ (list& type body tokens'))
         (#Some [tokens' [(#Some type) body]])

         ... B
         (^ (list& body tokens'))
         (#Some [tokens' [#None body]])

         _
         #None))

(macro:' .private (maybe\else' tokens)
         (case tokens
           (^ (list else then))
           (do meta_monad
             [g!_ (..identifier "g!_")]
             (in (list (` (..case (~ then)
                            (#..Some (~ g!_))
                            (#..Some (~ g!_))

                            #..None
                            (~ else))))))

           _
           (failure "Wrong syntax for maybe\else'")))

(def:' .private (definitionP tokens)
       (-> (List Code) (Maybe [Code Text (List Code) (List [Code Code]) (Maybe Code) Code]))
       (|> (do maybe_monad
             [% (anyP tokens)
              .let' [[tokens export_policy] %]
              % (enhanced_local_declarationP tokens)
              .let' [[tokens [name parameters]] %]
              % (annotationsP tokens)
              .let' [[tokens annotations] %]
              % (bodyP tokens)
              .let' [[tokens [?type body]] %]
              _ (endP tokens)]
             (in [export_policy name parameters annotations ?type body]))
           ... (^ (list _export_policy _declaration _annotations _type _body))
           ... (^ (list _export_policy _declaration _annotations _body))
           (maybe\else' (do maybe_monad
                          [% (enhanced_local_declarationP tokens)
                           .let' [[tokens [name parameters]] %]
                           % (bodyP tokens)
                           .let' [[tokens [?type body]] %]
                           _ (endP tokens)]
                          (in [(` ..private) name parameters #End ?type body])))
           ... (^ (list _declaration _type _body))
           ... (^ (list _declaration _body))
           (maybe\else' (do maybe_monad
                          [% (enhanced_local_declarationP tokens)
                           .let' [[tokens [name parameters]] %]
                           % (annotationsP tokens)
                           .let' [[tokens annotations] %]
                           % (bodyP tokens)
                           .let' [[tokens [?type body]] %]
                           _ (endP tokens)]
                          (in [(` ..private) name parameters annotations ?type body])))
           ... (^ (list _declaration _annotations _type _body))
           ... (^ (list _declaration _annotations _body))
           (maybe\else' (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 #End ?type body])))
           ... (^ (list _export_policy _declaration _type _body))
           ... (^ (list _export_policy _declaration _body))
           ))

(macro:' .public (def: tokens)
         (list)
         (case (definitionP tokens)
           (#Some [export_policy name parameters annotations ?type body])
           (let [body (case parameters
                        #End
                        body

                        _
                        (` (function ((~ (..local_identifier$ name)) (~+ parameters))
                             (~ body))))
                 body (case ?type
                        (#Some type)
                        (` (: (~ type)
                              (~ body)))
                        
                        #None
                        body)
                 =annotations (definition_annotations annotations)]
             (in_meta (list (` ("lux def" (~ (..local_identifier$ name))
                                (~ body)
                                [(~ location_code)
                                 (#.Record (~ =annotations))]
                                (~ export_policy))))))
           
           #None
           (failure "Wrong syntax for def:")))

(def: (with_definition_annotation addition annotations)
  (-> [Code Code] Code Code)
  (case [addition annotations]
    [[name value] [location (#Record pairs)]]
    [location (#Record (#Item [name value] pairs))]

    _
    annotations))

(def: (merged_definition_annotations addition base)
  (-> Code Code Code)
  (case addition
    [location (#Record pairs)]
    (list\mix with_definition_annotation base pairs)
    
    _
    base))

(def:' .private (macroP tokens)
       (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) Code]))
       (|> (do maybe_monad
             [% (anyP tokens)
              .let' [[tokens export_policy] %]
              % (local_declarationP tokens)
              .let' [[tokens [name parameters]] %]
              % (annotationsP tokens)
              .let' [[tokens annotations] %]
              % (anyP tokens)
              .let' [[tokens body] %]
              _ (endP tokens)]
             (in [export_policy name parameters annotations body]))
           ... (^ (list _export_policy _declaration _annotations _body))
           (maybe\else' (do maybe_monad
                          [% (local_declarationP tokens)
                           .let' [[tokens [name parameters]] %]
                           % (anyP tokens)
                           .let' [[tokens body] %]
                           _ (endP tokens)]
                          (in [(` ..private) name parameters #End body])))
           ... (^ (list _declaration _body))
           (maybe\else' (do maybe_monad
                          [% (local_declarationP tokens)
                           .let' [[tokens [name parameters]] %]
                           % (annotationsP tokens)
                           .let' [[tokens annotations] %]
                           % (anyP tokens)
                           .let' [[tokens body] %]
                           _ (endP tokens)]
                          (in [(` ..private) name parameters annotations body])))
           ... (^ (list _declaration _annotations _body))
           (maybe\else' (do maybe_monad
                          [% (declarationP tokens)
                           .let' [[tokens [export_policy name parameters]] %]
                           % (anyP tokens)
                           .let' [[tokens body] %]
                           _ (endP tokens)]
                          (in [export_policy name parameters #End body])))
           ... (^ (list _export_policy _declaration _body))
           ))

(macro:' .public (macro: tokens)
         (list)
         (case (macroP tokens)
           (#Some [export_policy name args annotations body])
           (let [name (local_identifier$ name)
                 body (case args
                        #End
                        body

                        _
                        (` ("lux macro"
                            (function ((~ name) (~+ (list\each local_identifier$ args))) (~ body)))))
                 =annotations (definition_annotations annotations)]
             (in_meta (list (` ("lux def" (~ name)
                                (~ body)
                                [(~ location_code)
                                 (#Record (~ =annotations))]
                                (~ export_policy))))))

           #None
           (failure "Wrong syntax for macro:")))

(def: (list\one f xs)
  (All (_ a b)
    (-> (-> a (Maybe b)) (List a) (Maybe b)))
  (case xs
    #End
    #None

    (#Item x xs')
    (case (f x)
      #None
      (list\one f xs')

      (#Some y)
      (#Some y))))

(template [<name> <form> <message>]
  [(macro: .public (<name> tokens)
     (case (list\reversed tokens)
       (^ (list& last init))
       (in_meta (list (list\mix (: (-> Code Code Code)
                                   (function (_ pre post) (` <form>)))
                                last
                                init)))
       
       _
       (failure <message>)))]

  [and (if (~ pre) (~ post) #0) "'and' requires >=1 clauses."]
  [or  (if (~ pre) #1 (~ post)) "'or' requires >=1 clauses."])

(def: (index part text)
  (-> Text Text (Maybe Nat))
  ("lux text index" 0 part text))

(def: .public (panic! message)
  (-> Text Nothing)
  ("lux io error" message))

(macro: (maybe\else tokens state)
  (case tokens
    (^ (list else maybe))
    (let [g!temp (: Code [dummy_location (#Identifier ["" ""])])
          code (` (case (~ maybe)
                    (#.Some (~ g!temp))
                    (~ g!temp)

                    #.None
                    (~ else)))]
      (#Right [state (list code)]))

    _
    (#Left "Wrong syntax for maybe\else")))

(def: (text\all_split_by splitter input)
  (-> Text Text (List Text))
  (case (..index splitter input)
    #None
    (list input)

    (#Some idx)
    (list& ("lux text clip" 0 idx input)
           (text\all_split_by splitter
                              (let [after_offset ("lux i64 +" 1 idx)
                                    after_length ("lux i64 -"
                                                  after_offset
                                                  ("lux text size" input))]
                                ("lux text clip" after_offset after_length input))))))

(def: (item idx xs)
  (All (_ a)
    (-> Nat (List a) (Maybe a)))
  (case xs
    #End
    #None

    (#Item x xs')
    (if ("lux i64 =" 0 idx)
      (#Some x)
      (item ("lux i64 -" 1 idx) xs'))))

... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
(def: (reduced env type)
  (-> (List Type) Type Type)
  (case 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)
    (case ?local_env
      #End
      (#UnivQ env ?local_def)

      _
      type)

    (#ExQ ?local_env ?local_def)
    (case ?local_env
      #End
      (#ExQ env ?local_def)

      _
      type)

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

    (#Parameter idx)
    (case (item idx env)
      (#Some parameter)
      parameter

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

    _
    type
    ))

(def: (applied_type param type_fn)
  (-> Type Type (Maybe Type))
  (case type_fn
    (#UnivQ env body)
    (#Some (reduced (list& type_fn param env) body))

    (#ExQ env body)
    (#Some (reduced (list& 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))

(template [<name> <tag>]
  [(def: (<name> type)
     (-> Type (List Type))
     (case type
       (<tag> left right)
       (list& left (<name> right))

       _
       (list type)))]

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

(def: (flat_application type)
  (-> Type [Type (List Type)])
  (case type
    (#Apply head func')
    (let [[func tail] (flat_application func')]
      [func (#Item head tail)])

    _
    [type (list)]))

(def: (interface_methods type)
  (-> Type (Maybe (List Type)))
  (case 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]
      (case (plist\value name modules)
        (#Some module)
        (#Right state module)

        _
        (#Left ($_ text\composite "Unknown module: " name))))))

(def: (type_slot [module name])
  (-> Name (Meta [Nat (List Name) Bit Type]))
  (do meta_monad
    [=module (..module module)
     .let [{#module_hash _ #module_aliases _ #definitions definitions #imports _ #module_annotations _ #module_state _} =module]]
    (case (plist\value (text\composite "#" name) definitions)
      (#Some (#Slot [exported type group index]))
      (in_meta [index
                (list\each (function (_ slot)
                             [module slot])
                           group)
                exported
                type])

      _
      (failure (text\composite "Unknown slot: " (name\encoded [module name]))))))

(def: (record_slots type)
  (-> Type (Meta (Maybe [(List Name) (List Type)])))
  (case 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_annotations _ #module_state _} =module]]
      (case (plist\value name definitions)
        (#Some (#Type [exported? (#Named _ _type) (#Right slots)]))
        (case (interface_methods _type)
          (#Some members)
          (in_meta (#Some [(list\each (function (_ slot) [module slot])
                                      (#Item slots))
                           members]))

          _
          (in_meta #None))

        _
        (record_slots unnamed)))
    
    _
    (in_meta #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]
      (case expected
        (#Some type)
        (#Right state type)

        #None
        (#Left "Not expecting any type.")))))

(def: (type\encoded type)
  (-> Type Text)
  (case type
    (#Primitive name params)
    (case params
      #End
      name

      _
      ($_ text\composite "(" name " " (|> params (list\each type\encoded) (list\interposed " ") list\reversed (list\mix text\composite "")) ")"))

    (#Sum _)
    ($_ text\composite "(Or " (|> (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 "⌈v:" (nat\encoded id) "⌋")
    
    (#Ex id)
    ($_ text\composite "⟨e:" (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 _)
    (name\encoded name)
    ))

(macro: .public (implementation tokens)
  (do meta_monad
    [tokens' (monad\each meta_monad expansion tokens)
     struct_type ..expected_type
     tags+type (record_slots struct_type)
     tags (: (Meta (List Name))
             (case tags+type
               (#Some [tags _])
               (in_meta tags)

               _
               (failure ($_ text\composite
                            "No tags available for type: "
                            (type\encoded struct_type)))))
     .let [tag_mappings (: (List [Text Code])
                           (list\each (function (_ tag) [(product\right tag) (tag$ tag)])
                                      tags))]
     members (monad\each meta_monad
                         (: (-> Code (Meta [Code Code]))
                            (function (_ token)
                              (case token
                                (^ [_ (#Form (list [_ (#Text "lux def")] [_ (#Identifier "" tag_name)] value meta export_policy))])
                                (case (plist\value tag_name tag_mappings)
                                  (#Some tag)
                                  (in [tag value])

                                  _
                                  (failure (text\composite "Unknown implementation member: " tag_name)))

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

(def: (text\interposed separator parts)
  (-> Text (List Text) Text)
  (case parts
    #End
    ""
    
    (#Item head tail)
    (list\mix (function (_ right left)
                ($_ text\composite left separator right))
              head
              tail)))

(def: (remainderP tokens)
  (-> (List Code) (Maybe (List Code)))
  (case tokens
    #End
    #None

    _
    (#Item tokens)))

(def: (implementationP tokens)
  (-> (List Code) (Maybe [Code Text (List Code) (List [Code Code]) Code (List Code)]))
  (|> (do maybe_monad
        [% (enhanced_declarationP tokens)
         .let' [[tokens [export_policy name parameters]] %]
         % (annotationsP tokens)
         .let' [[tokens annotations] %]
         % (anyP tokens)
         .let' [[tokens type] %]
         tokens (remainderP tokens)]
        (in [export_policy name parameters annotations type tokens]))
      ... (^ (list _export_policy _declaration _annotations _type _body))
      ... (^ (list _declaration _annotations _type _body))
      (maybe\else' (do maybe_monad
                     [% (enhanced_local_declarationP tokens)
                      .let' [[tokens [name parameters]] %]
                      % (anyP tokens)
                      .let' [[tokens type] %]
                      tokens (remainderP tokens)]
                     (in [(` ..private) name parameters #End type tokens])))
      ... (^ (list _declaration _type _body))
      (maybe\else' (do maybe_monad
                     [% (anyP tokens)
                      .let' [[tokens export_policy] %]
                      % (enhanced_local_declarationP tokens)
                      .let' [[tokens [name parameters]] %]
                      % (anyP tokens)
                      .let' [[tokens type] %]
                      tokens (remainderP tokens)]
                     (in [export_policy name parameters #End type tokens])))
      ... (^ (list _export_policy _declaration _type _body))
      ))

(macro: .public (implementation: tokens)
  (case (implementationP tokens)
    (#Some [export_policy name args annotations type definitions])
    (let [usage (case args
                  #End
                  (local_identifier$ name)

                  _
                  (` ((~ (local_identifier$ name)) (~+ args))))]
      (in_meta (list (` (..def: (~ export_policy) (~ usage)
                          (~ (merged_definition_annotations (` {#.implementation? #1})
                                                            (record$ annotations)))
                          (~ type)
                          (implementation (~+ definitions)))))))

    #None
    (failure "Wrong syntax for implementation:")))

(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)))))
  (case tokens
    (#Item _)
    (do maybe_monad
      [% (itP tokens)
       .let [[tokens' head] %]
       tail (case tokens'
              (#Item _)
              (everyP itP tokens')

              #End
              (in (list)))]
      (in (list& head tail)))

    #End
    (#Some (list))))

(def: (caseP tokens)
  (-> (List Code) (Maybe [(List Code) [Text Code]]))
  (case tokens
    (^ (list& [_ (#Tag ["" niladic])] tokens'))
    (#Some [tokens' [niladic (` .Any)]])

    (^ (list& [_ (#Form (list& [_ (#Tag ["" polyadic])] caseT))] tokens'))
    (#Some [tokens' [polyadic (` (..Tuple (~+ caseT)))]])

    _
    #None))

(macro: .public (Variant tokens)
  (case (everyP caseP tokens)
    (#Some cases)
    (in_meta (list (` (..Union (~+ (list\each product\right cases))))
                   (form$ (list\each (function (_ case)
                                       (text$ (product\left case)))
                                     cases))))
    
    #None
    (failure "Wrong syntax for Variant")))

(def: (slotP tokens)
  (-> (List Code) (Maybe [(List Code) [Text Code]]))
  (case tokens
    (^ (list& [_ (#Tag ["" slot])] type tokens'))
    (#Some [tokens' [slot type]])

    _
    #None))

(def: un_paired
  (-> (List [Code Code]) (List Code))
  (let [pair_list (: (-> [Code Code] (List Code))
                     (function (_ [left right])
                       (list left right)))]
    (function (_ it)
      (|> it
          (list\each pair_list)
          list\conjoint))))

(macro: .public (Record tokens)
  (case tokens
    (^ (list [_ (#Record record)]))
    (case (everyP slotP (un_paired record))
      (#Some slots)
      (in_meta (list (` (..Tuple (~+ (list\each product\right slots))))
                     (tuple$ (list\each (function (_ slot)
                                          (text$ (product\left slot)))
                                        slots))))
      
      #None
      (failure "Wrong syntax for Record"))

    _
    (failure "Wrong syntax for Record")))

(def: (typeP tokens)
  (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) Code]))
  (|> (do maybe_monad
        [% (anyP tokens)
         .let' [[tokens export_policy] %]
         % (local_declarationP tokens)
         .let' [[tokens [name parameters]] %]
         % (annotationsP tokens)
         .let' [[tokens annotations] %]
         % (anyP tokens)
         .let' [[tokens definition] %]
         _ (endP tokens)]
        (in [export_policy name parameters annotations definition]))
      ... (^ (list _export_policy _declaration _annotations _body))
      (maybe\else' (do maybe_monad
                     [% (local_declarationP tokens)
                      .let' [[tokens [name parameters]] %]
                      % (annotationsP tokens)
                      .let' [[tokens annotations] %]
                      % (anyP tokens)
                      .let' [[tokens definition] %]
                      _ (endP tokens)]
                     (in [(` ..private) name parameters annotations definition])))
      ... (^ (list _declaration _annotations _body))
      (maybe\else' (do maybe_monad
                     [% (local_declarationP tokens)
                      .let' [[tokens [name parameters]] %]
                      % (anyP tokens)
                      .let' [[tokens definition] %]
                      _ (endP tokens)]
                     (in [(` ..private) name parameters #End definition])))
      ... (^ (list _declaration _body))
      (maybe\else' (do maybe_monad
                     [% (anyP tokens)
                      .let' [[tokens export_policy] %]
                      % (local_declarationP tokens)
                      .let' [[tokens [name parameters]] %]
                      % (anyP tokens)
                      .let' [[tokens definition] %]
                      _ (endP tokens)]
                     (in [export_policy name parameters #End definition])))
      ... (^ (list _export_policy _declaration _body))
      ))

(def: (textP tokens)
  (-> (List Code) (Maybe [(List Code) Text]))
  (case tokens
    (^ (list& [_ (#Text it)] tokens'))
    (#Some [tokens' it])

    _
    #None))

(def: (type_declaration it)
  (-> Code (Meta (Tuple Code (Maybe (Either (List Text) (List Text))))))
  ({[_ (#Form (#Item [_ (#Identifier declarer)] parameters))]
    (do meta_monad
      [declaration (single_expansion (form$ (list& (identifier$ declarer) parameters)))]
      (case declaration
        (^ (list type [_ (#Form tags)]))
        (case (everyP textP tags)
          (#Some tags)
          (in_meta [type (#Some (#Left tags))])
          
          #None
          (failure "Improper type-definition syntax"))

        (^ (list type [_ (#Tuple slots)]))
        (case (everyP textP slots)
          (#Some slots)
          (in_meta [type (#Some (#Right slots))])
          
          #None
          (failure "Improper type-definition syntax"))

        (^ (list type))
        (in_meta [it #None])

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

    type
    (in_meta [type #None])}
   it))

(macro: .public (type: tokens)
  (case (typeP tokens)
    (#Some [export_policy name args meta type_codes])
    (do meta_monad
      [type+labels?? (..type_declaration type_codes)
       module_name current_module_name
       .let' [type_name (local_identifier$ name)
              [type labels??] type+labels??
              type' (: (Maybe Code)
                       (case args
                         #End
                         (#Some type)

                         _
                         (#Some (` (.All ((~ type_name) (~+ (list\each local_identifier$ args)))
                                     (~ type))))))
              total_meta (let [meta (definition_annotations meta)]
                           (` [(~ location_code)
                               (#.Record (~ meta))]))]]
      (case type'
        (#Some type'')
        (let [typeC (` (#.Named [(~ (text$ module_name))
                                 (~ (text$ name))]
                                (.type (~ type''))))]
          (in_meta (list (case labels??
                           (#Some labels)
                           (case labels
                             (#Left tags)
                             (` ("lux def type tagged" (~ type_name)
                                 (~ typeC)
                                 (~ total_meta)
                                 ((~+ (list\each text$ tags)))
                                 (~ export_policy)))
                             
                             (#Right slots)
                             (` ("lux def type tagged" (~ type_name)
                                 (~ typeC)
                                 (~ total_meta)
                                 [(~+ (list\each text$ slots))]
                                 (~ export_policy))))
                           
                           _
                           (` ("lux def" (~ type_name)
                               ("lux type check type"
                                (~ typeC))
                               (~ total_meta)
                               (~ export_policy)))))))

        #None
        (failure "Wrong syntax for type:")))

    #None
    (failure "Wrong syntax for type:")))

(template [<name> <to>]
  [(def: .public (<name> value)
     (-> (I64 Any) <to>)
     (:as <to> value))]

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

(type: Referrals
  (Variant
   #All
   (#Only (List Text))
   (#Exclude (List Text))
   #Ignore
   #Nothing))

(type: Openings
  [Text (List Text)])

(type: Refer
  (Record
   {#refer_defs Referrals
    #refer_open (List Openings)}))

(type: Importation
  (Record
   {#import_name Text
    #import_alias (Maybe Text)
    #import_refer Refer}))

(def: (referral_references defs)
  (-> (List Code) (Meta (List Text)))
  (monad\each meta_monad
              (: (-> Code (Meta Text))
                 (function (_ def)
                   (case def
                     [_ (#Identifier ["" name])]
                     (in_meta name)

                     _
                     (failure "#only/#+ and #exclude/#- require identifiers."))))
              defs))

(def: (referrals_parser tokens)
  (-> (List Code) (Meta [Referrals (List Code)]))
  (case tokens
    (^or (^ (list& [_ (#Form (list& [_ (#Tag ["" "+"])] defs))] tokens'))
         (^ (list& [_ (#Form (list& [_ (#Tag ["" "only"])] defs))] tokens')))
    (do meta_monad
      [defs' (..referral_references defs)]
      (in [(#Only defs') tokens']))

    (^or (^ (list& [_ (#Form (list& [_ (#Tag ["" "-"])] defs))] tokens'))
         (^ (list& [_ (#Form (list& [_ (#Tag ["" "exclude"])] defs))] tokens')))
    (do meta_monad
      [defs' (..referral_references defs)]
      (in [(#Exclude defs') tokens']))

    (^or (^ (list& [_ (#Tag ["" "*"])] tokens'))
         (^ (list& [_ (#Tag ["" "all"])] tokens')))
    (in_meta [#All tokens'])

    (^or (^ (list& [_ (#Tag ["" "_"])] tokens'))
         (^ (list& [_ (#Tag ["" "ignore"])] tokens')))
    (in_meta [#Ignore tokens'])
    
    _
    (in_meta [#Nothing tokens])))

(def: (openings_parser parts)
  (-> (List Code) (Meta [(List Openings) (List Code)]))
  (case parts
    #End
    (in_meta [#End #End])

    (^ (list& [_ (#Form (list& [_ (#Text prefix)] structs))] parts'))
    (do meta_monad
      [structs' (monad\each meta_monad
                            (function (_ struct)
                              (case struct
                                [_ (#Identifier ["" struct_name])]
                                (in_meta struct_name)

                                _
                                (failure "Expected all implementations of opening form to be identifiers.")))
                            structs)
       next+remainder (openings_parser parts')]
      (let [[next remainder] next+remainder]
        (in_meta [(#Item [prefix structs'] next)
                  remainder])))

    _
    (in_meta [#End parts])))

(def: (text\split_at' at x)
  (-> Nat Text [Text Text])
  [("lux text clip" 0 at x)
   ("lux text clip" at (|> x "lux text size" ("lux 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' ("lux text size" token) post')]]
    (in [pre post])))

(def: (replaced pattern replacement template)
  (-> Text Text Text Text)
  ((: (-> Text Text Text)
      (function (recur left right)
        (case (..text\split_by pattern right)
          (#Some [pre post])
          (recur ($_ "lux text concat" left pre replacement) post)

          #None
          ("lux text concat" left right))))
   "" template))

(def: contextual_reference "#")
(def: self_reference ".")

(def: (module_alias context self aliased)
  (-> Text Text Text Text)
  (|> aliased
      (replaced ..self_reference self)
      (replaced ..contextual_reference context)))

(def: .public module_separator
  "/")

(def: parallel_hierarchy_sigil
  "\")

(def: (normal_parallel_path' hierarchy root)
  (-> Text Text Text)
  (case [(text\split_by ..module_separator hierarchy)
         (text\split_by ..parallel_hierarchy_sigil root)]
    [(#Some [_ hierarchy'])
     (#Some ["" root'])]
    (normal_parallel_path' hierarchy' root')

    _
    (case root
      "" hierarchy
      _ ($_ text\composite root ..module_separator hierarchy))))

(def: (normal_parallel_path hierarchy root)
  (-> Text Text (Maybe Text))
  (case (text\split_by ..parallel_hierarchy_sigil root)
    (#Some ["" root'])
    (#Some (normal_parallel_path' hierarchy root'))

    _
    #None))

(def: (relative_ups relatives input)
  (-> Nat Text Nat)
  (case ("lux text index" relatives ..module_separator input)
    #None
    relatives

    (#Some found)
    (if ("lux i64 =" relatives found)
      (relative_ups ("lux i64 +" 1 relatives) input)
      relatives)))

(def: (list\after amount list)
  (All (_ a) (-> Nat (List a) (List a)))
  (case [amount list]
    (^or [0 _] [_ #End])
    list

    [_ (#Item _ tail)]
    (list\after ("lux i64 -" 1 amount) tail)))

(def: (absolute_module_name nested? relative_root module)
  (-> Bit Text Text (Meta Text))
  (case (relative_ups 0 module)
    0
    (in_meta (if nested?
               ($_ "lux text concat" relative_root ..module_separator module)
               module))
    
    relatives
    (let [parts (text\all_split_by ..module_separator relative_root)
          jumps ("lux i64 -" 1 relatives)]
      (if (n/< (list\size parts) jumps)
        (let [prefix (|> parts
                         list\reversed
                         (list\after jumps)
                         list\reversed
                         (text\interposed ..module_separator))
              clean ("lux text clip" relatives (|> module "lux text size" ("lux i64 -" relatives)) module)
              output (case ("lux text size" clean)
                       0 prefix
                       _ ($_ text\composite prefix ..module_separator clean))]
          (in_meta output))
        (failure ($_ "lux text concat"
                     "Cannot climb the module hierarchy..." ..\n
                     "Importing module: " module ..\n
                     "   Relative Root: " relative_root ..\n))))))

(def: (imports_parser nested? relative_root context_alias imports)
  (-> Bit Text Text (List Code) (Meta (List Importation)))
  (do meta_monad
    [imports' (monad\each meta_monad
                          (: (-> Code (Meta (List Importation)))
                             (function (_ token)
                               (case token
                                 ... Simple
                                 [_ (#Identifier ["" module_name])]
                                 (do meta_monad
                                   [absolute_module_name (..absolute_module_name nested? relative_root module_name)]
                                   (in (list {#import_name absolute_module_name
                                              #import_alias #None
                                              #import_refer {#refer_defs #All
                                                             #refer_open (list)}})))

                                 ... Nested
                                 (^ [_ (#Tuple (list& [_ (#Identifier ["" module_name])] extra))])
                                 (do meta_monad
                                   [absolute_module_name (case (normal_parallel_path relative_root module_name)
                                                           (#Some parallel_path)
                                                           (in parallel_path)

                                                           #None
                                                           (..absolute_module_name nested? relative_root module_name))
                                    referral+extra (referrals_parser extra)
                                    .let [[referral extra] referral+extra]
                                    openings+extra (openings_parser extra)
                                    .let [[openings extra] openings+extra]
                                    sub_imports (imports_parser #1 absolute_module_name context_alias extra)]
                                   (in (case [referral openings]
                                         [#Nothing #End]
                                         sub_imports
                                         
                                         _
                                         (list& {#import_name absolute_module_name
                                                 #import_alias #None
                                                 #import_refer {#refer_defs referral
                                                                #refer_open openings}}
                                                sub_imports))))

                                 (^ [_ (#Tuple (list& [_ (#Text alias)] [_ (#Identifier ["" module_name])] extra))])
                                 (do meta_monad
                                   [absolute_module_name (case (normal_parallel_path relative_root module_name)
                                                           (#Some parallel_path)
                                                           (in parallel_path)

                                                           #None
                                                           (..absolute_module_name nested? relative_root module_name))
                                    referral+extra (referrals_parser extra)
                                    .let [[referral extra] referral+extra]
                                    openings+extra (openings_parser extra)
                                    .let [[openings extra] openings+extra
                                          module_alias (..module_alias context_alias module_name alias)]
                                    sub_imports (imports_parser #1 absolute_module_name module_alias extra)]
                                   (in (case [referral openings]
                                         [#Ignore #End]
                                         sub_imports
                                         
                                         _
                                         (list& {#import_name absolute_module_name
                                                 #import_alias (#Some module_alias)
                                                 #import_refer {#refer_defs referral
                                                                #refer_open openings}}
                                                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] (case 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])]
    (case (plist\value module modules)
      (#Some =module)
      (let [to_alias (list\each (: (-> [Text Global]
                                       (List Text))
                                   (function (_ [name definition])
                                     (case definition
                                       (#Alias _)
                                       (list)

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

                                       (#Type [exported? type labels])
                                       (if exported?
                                         (list name)
                                         (list))

                                       (#Label _)
                                       (list)

                                       (#Slot _)
                                       (list))))
                                (let [{#module_hash _ #module_aliases _ #definitions definitions #imports _ #module_annotations _ #module_state _} =module]
                                  definitions))]
        (#Right state (list\conjoint to_alias)))
      
      #None
      (#Left ($_ text\composite
                 "Unknown module: " (text\encoded module) ..\n
                 "Current module: " (case 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)))
  (case xs
    #End
    (list)

    (#Item x xs')
    (if (p x)
      (#Item x (list\only p xs'))
      (list\only p xs'))))

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

(def: (on_either f x1 x2)
  (All (_ a b)
    (-> (-> a (Maybe b)) a a (Maybe b)))
  (case (f x1)
    #None     (f x2)
    (#Some y) (#Some y)))

(def: (in_env name state)
  (-> Text Lux (Maybe Type))
  (case 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}
    (list\one (: (-> Scope (Maybe Type))
                 (function (_ env)
                   (case env
                     {#name _
                      #inner _
                      #locals {#counter _ #mappings locals}
                      #captured {#counter _ #mappings closure}}
                     (on_either (list\one (: (-> [Text [Type Any]] (Maybe Type))
                                             (function (_ [bname [type _]])
                                               (if (text\= name bname)
                                                 (#Some type)
                                                 #None))))
                                (: (List [Text [Type Any]]) locals)
                                (: (List [Text [Type Any]]) closure)))))
              scopes)))

(def: (definition_type name state)
  (-> Name Lux (Maybe Type))
  (let [[v_module v_name] 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]
    (case (plist\value v_module modules)
      #None
      #None

      (#Some {#definitions definitions #module_hash _ #module_aliases _ #imports _ #module_annotations _ #module_state _})
      (case (plist\value v_name definitions)
        #None
        #None

        (#Some definition)
        (case definition
          (#Alias real_name)
          (definition_type real_name state)
          
          (#Definition [exported? def_type def_meta def_value])
          (#Some def_type)

          (#Type [exported? type labels])
          (#Some ..Type)

          (#Label _)
          #None

          (#Slot _)
          #None)))))

(def: (definition_value name state)
  (-> Name (Meta [Type Any]))
  (let [[v_module v_name] 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]
    (case (plist\value v_module modules)
      #None
      (#Left (text\composite "Unknown definition: " (name\encoded name)))

      (#Some {#definitions definitions #module_hash _ #module_aliases _ #imports _ #module_annotations _ #module_state _})
      (case (plist\value v_name definitions)
        #None
        (#Left (text\composite "Unknown definition: " (name\encoded name)))

        (#Some definition)
        (case definition
          (#Alias real_name)
          (definition_value real_name state)
          
          (#Definition [exported? def_type def_meta def_value])
          (#Right [state [def_type def_value]])

          (#Type [exported? type labels])
          (#Right [state [..Type type]])

          (#Label _)
          (#Left (text\composite "Unknown definition: " (name\encoded name)))

          (#Slot _)
          (#Left (text\composite "Unknown definition: " (name\encoded name))))))))

(def: (type_variable idx bindings)
  (-> Nat (List [Nat (Maybe Type)]) (Maybe Type))
  (case bindings
    #End
    #End
    
    (#Item [var bound] bindings')
    (if ("lux i64 =" idx var)
      bound
      (type_variable idx bindings'))))

(def: (type_definition full_name)
  (-> Name (Meta Type))
  (do meta_monad
    [.let [[module name] full_name]
     current_module current_module_name]
    (function (_ compiler)
      (let [temp (if (text\= "" module)
                   (case (in_env name compiler)
                     (#Some struct_type)
                     (#Right [compiler struct_type])

                     _
                     (case (definition_type [current_module name] compiler)
                       (#Some struct_type)
                       (#Right [compiler struct_type])

                       _
                       (#Left ($_ text\composite "Unknown var: " (name\encoded full_name)))))
                   (case (definition_type full_name compiler)
                     (#Some struct_type)
                     (#Right [compiler struct_type])

                     _
                     (#Left ($_ text\composite "Unknown var: " (name\encoded full_name)))))]
        (case temp
          (#Right [compiler (#Var type_id)])
          (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]
            (case (type_variable type_id var_bindings)
              #None
              temp

              (#Some actualT)
              (#Right [compiler actualT])))

          _
          temp))
      )))

(def: (zipped/2 xs ys)
  (All (_ a b)
    (-> (List a) (List b) (List [a b])))
  (case xs
    (#Item x xs')
    (case ys
      (#Item y ys')
      (list& [x y] (zipped/2 xs' ys'))

      _
      (list))
    
    _
    (list)))

(macro: .public (^open tokens)
  (case tokens
    (^ (list& [_ (#Form (list [_ (#Text alias)]))] body branches))
    (do meta_monad
      [g!temp (..identifier "temp")]
      (in (list& g!temp (` (..^open (~ g!temp) (~ (text$ alias)) (~ body))) branches)))

    (^ (list [_ (#Identifier name)] [_ (#Text alias)] body))
    (do meta_monad
      [init_type (type_definition name)
       struct_evidence (record_slots init_type)]
      (case struct_evidence
        #None
        (failure (text\composite "Can only 'open' structs: " (type\encoded init_type)))

        (#Some tags&members)
        (do meta_monad
          [full_body ((: (-> Name [(List Name) (List Type)] Code (Meta Code))
                         (function (recur source [tags members] target)
                           (let [locals (list\each (function (_ [t_module t_name])
                                                     ["" (..module_alias "" t_name alias)])
                                                   tags)
                                 pattern (tuple$ (list\each identifier$ locals))]
                             (do meta_monad
                               [enhanced_target (monad\mix meta_monad
                                                           (function (_ [m_local m_type] enhanced_target)
                                                             (do meta_monad
                                                               [m_implementation (record_slots m_type)]
                                                               (case m_implementation
                                                                 (#Some m_tags&members)
                                                                 (recur m_local
                                                                        m_tags&members
                                                                        enhanced_target)

                                                                 #None
                                                                 (in enhanced_target))))
                                                           target
                                                           (zipped/2 locals members))]
                               (in (` ({(~ pattern) (~ enhanced_target)} (~ (identifier$ source)))))))))
                      name tags&members body)]
          (in (list full_body)))))

    _
    (failure "Wrong syntax for ^open")))

(macro: .public (cond tokens)
  (if ("lux i64 =" 0 (n/% 2 (list\size tokens)))
    (failure "cond requires an uneven number of arguments.")
    (case (list\reversed tokens)
      (^ (list& else branches'))
      (in_meta (list (list\mix (: (-> [Code Code] Code Code)
                                  (function (_ branch else)
                                    (let [[right left] branch]
                                      (` (if (~ left) (~ right) (~ else))))))
                               else
                               (pairs branches'))))
      
      _
      (failure "Wrong syntax for cond"))))

(def: (enumeration' idx xs)
  (All (_ a)
    (-> Nat (List a) (List [Nat a])))
  (case xs
    (#Item x xs')
    (#Item [idx x] (enumeration' ("lux i64 +" 1 idx) xs'))

    #End
    #End))

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

(macro: .public (value@ tokens)
  (case tokens
    (^ (list [_ (#Tag slot')] record))
    (do meta_monad
      [slot (normal slot')
       output (..type_slot slot)
       .let [[idx tags exported? type] output]
       g!_ (..identifier "_")
       g!output (..identifier "")]
      (case (interface_methods type)
        (#Some members)
        (let [pattern (record$ (list\each (: (-> [Name [Nat Type]] [Code Code])
                                             (function (_ [[r_module r_name] [r_idx r_type]])
                                               [(tag$ [r_module r_name])
                                                (if ("lux i64 =" idx r_idx)
                                                  g!output
                                                  g!_)]))
                                          (zipped/2 tags (enumeration members))))]
          (in_meta (list (` ({(~ pattern) (~ g!output)} (~ record))))))

        _
        (failure "value@ can only use records.")))

    (^ (list [_ (#Tuple slots)] record))
    (in_meta (list (list\mix (: (-> Code Code Code)
                                (function (_ slot inner)
                                  (` (..value@ (~ slot) (~ inner)))))
                             record
                             slots)))

    (^ (list selector))
    (do meta_monad
      [g!_ (..identifier "_")
       g!record (..identifier "record")]
      (in (list (` (function ((~ g!_) (~ g!record)) (..value@ (~ selector) (~ g!record)))))))
    
    _
    (failure "Wrong syntax for value@")))

(def: (open_declaration alias tags my_tag_index [module short] source type)
  (-> Text (List Name) Nat Name Code Type (Meta (List Code)))
  (do meta_monad
    [output (record_slots type)
     g!_ (..identifier "g!_")
     .let [g!output (local_identifier$ short)
           pattern (|> tags
                       enumeration
                       (list\each (function (_ [tag_idx tag])
                                    (if ("lux i64 =" my_tag_index tag_idx)
                                      g!output
                                      g!_)))
                       tuple$)
           source+ (` ({(~ pattern) (~ g!output)} (~ source)))]]
    (case output
      (#Some [tags' members'])
      (do meta_monad
        [decls' (monad\each meta_monad
                            (: (-> [Nat Name Type] (Meta (List Code)))
                               (function (_ [sub_tag_index sname stype])
                                 (open_declaration alias tags' sub_tag_index sname source+ stype)))
                            (enumeration (zipped/2 tags' members')))]
        (in_meta (list\conjoint decls')))

      _
      (in_meta (list (` ("lux def" (~ (local_identifier$ (..module_alias "" short alias)))
                         (~ source+)
                         [(~ location_code) (#.Record #.End)]
                         #0)))))))

(macro: .public (open: tokens)
  (case tokens
    (^ (list [_ (#Text alias)] struct))
    (case struct
      [_ (#Identifier struct_name)]
      (do meta_monad
        [struct_type (type_definition struct_name)
         output (record_slots struct_type)
         .let [source (identifier$ struct_name)]]
        (case output
          (#Some [tags members])
          (do meta_monad
            [decls' (monad\each meta_monad (: (-> [Nat Name Type] (Meta (List Code)))
                                              (function (_ [tag_index sname stype])
                                                (open_declaration alias tags tag_index sname source stype)))
                                (enumeration (zipped/2 tags members)))]
            (in_meta (list\conjoint decls')))

          _
          (failure (text\composite "Can only 'open:' structs: " (type\encoded struct_type)))))

      _
      (do meta_monad
        [g!struct (..identifier "struct")]
        (in_meta (list (` ("lux def" (~ g!struct) (~ struct)
                           [(~ location_code) (#.Record #.End)]
                           #0))
                       (` (..open: (~ (text$ alias)) (~ g!struct)))))))

    _
    (failure "Wrong syntax for open:")))

(macro: .public (|>> tokens)
  (do meta_monad
    [g!_ (..identifier "_")
     g!arg (..identifier "arg")]
    (in_meta (list (` (function ((~ g!_) (~ g!arg)) (|> (~ g!arg) (~+ tokens))))))))

(macro: .public (<<| tokens)
  (do meta_monad
    [g!_ (..identifier "_")
     g!arg (..identifier "arg")]
    (in_meta (list (` (function ((~ g!_) (~ g!arg)) (<| (~+ tokens) (~ g!arg))))))))

(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_annotations _ #module_state _} module]]
    (in (is_member? imports import_name))))

(def: (referrals module_name options)
  (-> Text (List Code) (Meta Refer))
  (do meta_monad
    [referral+options (referrals_parser options)
     .let [[referral options] referral+options]
     openings+options (openings_parser options)
     .let [[openings options] openings+options]
     current_module current_module_name]
    (case options
      #End
      (in {#refer_defs referral
           #refer_open openings})

      _
      (failure ($_ text\composite "Wrong syntax for refer @ " current_module
                   ..\n (|> options
                            (list\each code\encoded)
                            (list\interposed " ")
                            (list\mix text\composite "")))))))

(def: (referral_definitions module_name [r_defs r_opens])
  (-> Text Refer (Meta (List Code)))
  (do meta_monad
    [current_module current_module_name
     .let [test_referrals (: (-> Text (List Text) (List Text) (Meta (List Any)))
                             (function (_ module_name all_defs referred_defs)
                               (monad\each meta_monad
                                           (: (-> Text (Meta Any))
                                              (function (_ _def)
                                                (if (is_member? all_defs _def)
                                                  (in_meta [])
                                                  (failure ($_ text\composite _def " is not defined in module " module_name " @ " current_module)))))
                                           referred_defs)))]
     defs' (case r_defs
             #All
             (exported_definitions module_name)

             (#Only +defs)
             (do meta_monad
               [*defs (exported_definitions module_name)
                _ (test_referrals module_name *defs +defs)]
               (in +defs))
             
             (#Exclude _defs)
             (do meta_monad
               [*defs (exported_definitions module_name)
                _ (test_referrals module_name *defs _defs)]
               (in (..list\only (|>> (is_member? _defs) not) *defs)))

             #Ignore
             (in (list))

             #Nothing
             (in (list)))
     .let [defs (list\each (: (-> Text Code)
                              (function (_ def)
                                (` ("lux def alias" (~ (local_identifier$ def)) (~ (identifier$ [module_name def]))))))
                           defs')
           openings (|> r_opens
                        (list\each (: (-> Openings (List Code))
                                      (function (_ [alias structs])
                                        (list\each (function (_ name)
                                                     (` (open: (~ (text$ alias)) (~ (identifier$ [module_name name])))))
                                                   structs))))
                        list\conjoint)]]
    (in (list\composite defs openings))))

(macro: (refer tokens)
  (case tokens
    (^ (list& [_ (#Text module_name)] options))
    (do meta_monad
      [=refer (referrals module_name options)]
      (referral_definitions module_name =refer))

    _
    (failure "Wrong syntax for refer")))

(def: (refer_code module_name module_alias' [r_defs r_opens])
  (-> Text (Maybe Text) Refer Code)
  (let [module_alias (..maybe\else module_name module_alias')
        localizations (: (List Code)
                         (case r_defs
                           #All
                           (list (' #*))
                           
                           (#Only defs)
                           (list (form$ (list& (' #+) (list\each local_identifier$ defs))))
                           
                           (#Exclude defs)
                           (list (form$ (list& (' #-) (list\each local_identifier$ defs))))
                           
                           #Ignore
                           (list)

                           #Nothing
                           (list)))
        openings (list\each (function (_ [alias structs])
                              (form$ (list& (text$ (..replaced ..contextual_reference module_alias alias))
                                            (list\each local_identifier$ structs))))
                            r_opens)]
    (` ((~! ..refer) (~ (text$ module_name))
        (~+ localizations)
        (~+ openings)))))

(macro: .public (module: tokens)
  (do meta_monad
    [.let [[_meta _imports] (: [(List [Code Code]) (List Code)]
                               (case tokens
                                 (^ (list& [_ (#Record _meta)] _imports))
                                 [_meta _imports]

                                 _
                                 [(list) tokens]))]
     current_module current_module_name
     imports (imports_parser #0 current_module "" _imports)
     .let [=imports (|> imports
                        (list\each (: (-> Importation Code)
                                      (function (_ [module_name m_alias =refer])
                                        (` [(~ (text$ module_name)) (~ (text$ (..maybe\else "" m_alias)))]))))
                        tuple$)
           =refers (list\each (: (-> Importation Code)
                                 (function (_ [module_name m_alias =refer])
                                   (refer_code module_name m_alias =refer)))
                              imports)
           =module (` ("lux def module" [(~ location_code)
                                         (#.Record (~ (definition_annotations _meta)))]
                       (~ =imports)))]]
    (in (#Item =module =refers))))

(macro: .public (\ tokens)
  (case tokens
    (^ (list struct [_ (#Identifier member)]))
    (in_meta (list (` (let [(^open (~ (text$ ..self_reference))) (~ struct)] (~ (identifier$ member))))))

    (^ (list& struct member args))
    (in_meta (list (` ((..\ (~ struct) (~ member)) (~+ args)))))
    
    _
    (failure "Wrong syntax for \")))

(macro: .public (with@ tokens)
  (case tokens
    (^ (list [_ (#Tag slot')] value record))
    (do meta_monad
      [slot (normal slot')
       output (..type_slot slot)
       .let [[idx tags exported? type] output]]
      (case (interface_methods type)
        (#Some members)
        (do meta_monad
          [pattern' (monad\each meta_monad
                                (: (-> [Name [Nat Type]] (Meta [Name Nat Code]))
                                   (function (_ [r_slot_name [r_idx r_type]])
                                     (do meta_monad
                                       [g!slot (..identifier "")]
                                       (in_meta [r_slot_name r_idx g!slot]))))
                                (zipped/2 tags (enumeration members)))]
          (let [pattern (record$ (list\each (: (-> [Name Nat Code] [Code Code])
                                               (function (_ [r_slot_name r_idx r_var])
                                                 [(tag$ r_slot_name)
                                                  r_var]))
                                            pattern'))
                output (record$ (list\each (: (-> [Name Nat Code] [Code Code])
                                              (function (_ [r_slot_name r_idx r_var])
                                                [(tag$ r_slot_name)
                                                 (if ("lux i64 =" idx r_idx)
                                                   value
                                                   r_var)]))
                                           pattern'))]
            (in_meta (list (` ({(~ pattern) (~ output)} (~ record)))))))

        _
        (failure "with@ can only use records.")))

    (^ (list [_ (#Tuple slots)] value record))
    (case slots
      #End
      (failure "Wrong syntax for with@")

      _
      (do meta_monad
        [bindings (monad\each meta_monad
                              (: (-> Code (Meta Code))
                                 (function (_ _) (..identifier "temp")))
                              slots)
         .let [pairs (zipped/2 slots bindings)
               update_expr (list\mix (: (-> [Code Code] Code Code)
                                        (function (_ [s b] v)
                                          (` (..with@ (~ s) (~ v) (~ b)))))
                                     value
                                     (list\reversed pairs))
               [_ accesses'] (list\mix (: (-> [Code Code] [Code (List (List Code))] [Code (List (List Code))])
                                          (function (_ [new_slot new_binding] [old_record accesses'])
                                            [(` (value@ (~ new_slot) (~ new_binding)))
                                             (#Item (list new_binding old_record) accesses')]))
                                       [record (: (List (List Code)) #End)]
                                       pairs)
               accesses (list\conjoint (list\reversed accesses'))]]
        (in (list (` (let [(~+ accesses)]
                       (~ update_expr)))))))
    
    (^ (list selector value))
    (do meta_monad
      [g!_ (..identifier "_")
       g!record (..identifier "record")]
      (in (list (` (function ((~ g!_) (~ g!record))
                     (..with@ (~ selector) (~ value) (~ g!record)))))))

    (^ (list selector))
    (do meta_monad
      [g!_ (..identifier "_")
       g!value (..identifier "value")
       g!record (..identifier "record")]
      (in (list (` (function ((~ g!_) (~ g!value) (~ g!record))
                     (..with@ (~ selector) (~ g!value) (~ g!record)))))))

    _
    (failure "Wrong syntax for with@")))

(macro: .public (revised@ tokens)
  (case tokens
    (^ (list [_ (#Tag slot')] fun record))
    (do meta_monad
      [slot (normal slot')
       output (..type_slot slot)
       .let [[idx tags exported? type] output]]
      (case (interface_methods type)
        (#Some members)
        (do meta_monad
          [pattern' (monad\each meta_monad
                                (: (-> [Name [Nat Type]] (Meta [Name Nat Code]))
                                   (function (_ [r_slot_name [r_idx r_type]])
                                     (do meta_monad
                                       [g!slot (..identifier "")]
                                       (in_meta [r_slot_name r_idx g!slot]))))
                                (zipped/2 tags (enumeration members)))]
          (let [pattern (record$ (list\each (: (-> [Name Nat Code] [Code Code])
                                               (function (_ [r_slot_name r_idx r_var])
                                                 [(tag$ r_slot_name)
                                                  r_var]))
                                            pattern'))
                output (record$ (list\each (: (-> [Name Nat Code] [Code Code])
                                              (function (_ [r_slot_name r_idx r_var])
                                                [(tag$ r_slot_name)
                                                 (if ("lux i64 =" idx r_idx)
                                                   (` ((~ fun) (~ r_var)))
                                                   r_var)]))
                                           pattern'))]
            (in_meta (list (` ({(~ pattern) (~ output)} (~ record)))))))

        _
        (failure "revised@ can only use records.")))

    (^ (list [_ (#Tuple slots)] fun record))
    (case slots
      #End
      (failure "Wrong syntax for revised@")

      _
      (do meta_monad
        [g!record (..identifier "record")
         g!temp (..identifier "temp")]
        (in (list (` (let [(~ g!record) (~ record)
                           (~ g!temp) (value@ [(~+ slots)] (~ g!record))]
                       (with@ [(~+ slots)] ((~ fun) (~ g!temp)) (~ g!record))))))))

    (^ (list selector fun))
    (do meta_monad
      [g!_ (..identifier "_")
       g!record (..identifier "record")]
      (in (list (` (function ((~ g!_) (~ g!record))
                     (..revised@ (~ selector) (~ fun) (~ g!record)))))))

    (^ (list selector))
    (do meta_monad
      [g!_ (..identifier "_")
       g!fun (..identifier "fun")
       g!record (..identifier "record")]
      (in (list (` (function ((~ g!_) (~ g!fun) (~ g!record))
                     (..revised@ (~ selector) (~ g!fun) (~ g!record)))))))
    
    _
    (failure "Wrong syntax for revised@")))

(macro: .public (^template tokens)
  (case tokens
    (^ (list& [_ (#Form (list [_ (#Tuple bindings)]
                              [_ (#Tuple templates)]))]
              [_ (#Form data)]
              branches))
    (case (: (Maybe (List Code))
             (do maybe_monad
               [bindings' (monad\each maybe_monad identifier_short bindings)
                data' (monad\each maybe_monad tuple_list data)]
               (let [num_bindings (list\size bindings')]
                 (if (every? (|>> ("lux i64 =" num_bindings))
                             (list\each list\size data'))
                   (let [apply (: (-> 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)
      (in_meta (list\composite output branches))
      
      #None
      (failure "Wrong syntax for ^template"))
    
    _
    (failure "Wrong syntax for ^template")))

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

  [++ "lux i64 +"]
  [-- "lux i64 -"]
  )

(def: (interleaved xs ys)
  (All (_ a)
    (-> (List a) (List a) (List a)))
  (case xs
    #End
    #End
    
    (#Item x xs')
    (case ys
      #End
      #End
      
      (#Item y ys')
      (list& x y (interleaved xs' ys')))))

(def: (type_code type)
  (-> Type Code)
  (case type
    (#Primitive name params)
    (` (#.Primitive (~ (text$ name)) (~ (untemplated_list (list\each type_code params)))))

    (^template [<tag>]
      [(<tag> left right)
       (` (<tag> (~ (type_code left)) (~ (type_code right))))])
    ([#.Sum] [#.Product]
     [#.Function]
     [#.Apply])

    (^template [<tag>]
      [(<tag> id)
       (` (<tag> (~ (nat$ id))))])
    ([#.Parameter] [#.Var] [#.Ex])

    (^template [<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 "identifier$" shortcut below.
    ... (` (#.Named [(~ (text$ module)) (~ (text$ name))]
    ...             (~ (type_code anonymous))))
    (identifier$ [module name])))

(macro: .public (loop tokens)
  (let [?params (case tokens
                  (^ (list name [_ (#Tuple bindings)] body))
                  (#Some [name bindings body])
                  
                  (^ (list [_ (#Tuple bindings)] body))
                  (#Some [(local_identifier$ "recur") bindings body])

                  _
                  #None)]
    (case ?params
      (#Some [name bindings body])
      (let [pairs (pairs bindings)
            vars (list\each product\left pairs)
            inits (list\each product\right pairs)]
        (if (every? identifier? inits)
          (do meta_monad
            [inits' (: (Meta (List Name))
                       (case (monad\each maybe_monad identifier_name inits)
                         (#Some inits') (in_meta inits')
                         #None          (failure "Wrong syntax for loop")))
             init_types (monad\each meta_monad type_definition inits')
             expected ..expected_type]
            (in_meta (list (` (("lux type check"
                                (-> (~+ (list\each type_code init_types))
                                    (~ (type_code expected)))
                                (function ((~ name) (~+ vars))
                                  (~ body)))
                               (~+ inits))))))
          (do meta_monad
            [aliases (monad\each meta_monad
                                 (: (-> Code (Meta Code))
                                    (function (_ _) (..identifier "")))
                                 inits)]
            (in_meta (list (` (let [(~+ (..interleaved aliases inits))]
                                (.loop (~ name)
                                  [(~+ (..interleaved vars aliases))]
                                  (~ body)))))))))

      #None
      (failure "Wrong syntax for loop"))))

(macro: .public (^slots tokens)
  (case tokens
    (^ (list& [_ (#Form (list [_ (#Tuple (list& hslot' tslots'))]))] body branches))
    (do meta_monad
      [slots (: (Meta [Name (List Name)])
                (case (: (Maybe [Name (List Name)])
                         (do maybe_monad
                           [hslot (..tag_name hslot')
                            tslots (monad\each maybe_monad ..tag_name tslots')]
                           (in [hslot tslots])))
                  (#Some slots)
                  (in_meta slots)
                  
                  #None
                  (failure "Wrong syntax for ^slots")))
       .let [[hslot tslots] slots]
       hslot (..normal hslot)
       tslots (monad\each meta_monad ..normal tslots)
       output (..type_slot hslot)
       g!_ (..identifier "_")
       .let [[idx tags exported? type] output
             slot_pairings (list\each (: (-> Name [Text Code])
                                         (function (_ [module name])
                                           [name (local_identifier$ name)]))
                                      (list& hslot tslots))
             pattern (record$ (list\each (: (-> Name [Code Code])
                                            (function (_ [module name])
                                              (let [tag (tag$ [module name])]
                                                (case (plist\value name slot_pairings)
                                                  (#Some binding) [tag binding]
                                                  #None           [tag g!_]))))
                                         tags))]]
      (in_meta (list& pattern body branches)))
    
    _
    (failure "Wrong syntax for ^slots")))

(def: (with_expansions' label tokens target)
  (-> Text (List Code) Code (Maybe (List Code)))
  (case target
    (^or [_ (#Bit _)] [_ (#Nat _)] [_ (#Int _)] [_ (#Rev _)] [_ (#Frac _)] [_ (#Text _)] [_ (#Tag _)])
    (#Some (list target))

    [_ (#Identifier [module name])]
    (if (and (text\= "" module)
             (text\= label name))
      (#Some tokens)
      (#Some (list target)))

    (^template [<tag>]
      [[location (<tag> elems)]
       (do maybe_monad
         [placements (monad\each maybe_monad (with_expansions' label tokens) elems)]
         (in (list [location (<tag> (list\conjoint placements))])))])
    ([#Tuple]
     [#Form])

    [location (#Record pairs)]
    (do maybe_monad
      [=pairs (monad\each maybe_monad
                          (: (-> [Code Code] (Maybe [Code Code]))
                             (function (_ [slot value])
                               (do maybe_monad
                                 [slot' (with_expansions' label tokens slot)
                                  value' (with_expansions' label tokens value)]
                                 (case [slot' value']
                                   (^ [(list =slot) (list =value)])
                                   (in [=slot =value])

                                   _
                                   #None))))
                          pairs)]
      (in (list [location (#Record =pairs)])))))

(macro: .public (with_expansions tokens)
  (case tokens
    (^ (list& [_ (#Tuple bindings)] bodies))
    (case bindings
      (^ (list& [_ (#Identifier ["" var_name])] expr bindings'))
      (do meta_monad
        [expansion (single_expansion expr)]
        (case (with_expansions' var_name expansion
                (` (.with_expansions
                     [(~+ bindings')]
                     (~+ bodies))))
          (#Some output)
          (in output)

          _
          (failure "[with_expansions] Improper macro expansion.")))

      #End
      (in_meta bodies)

      _
      (failure "Wrong syntax for with_expansions"))

    _
    (failure "Wrong syntax for with_expansions")))

(def: (flat_alias type)
  (-> Type Type)
  (case type
    (^template [<name>]
      [(#Named ["library/lux" <name>] _)
       type])
    (["Bit"]
     ["Nat"]
     ["Int"]
     ["Rev"]
     ["Frac"]
     ["Text"])
    
    (#Named _ type')
    (flat_alias type')
    
    _
    type))

(def: (static_simple_literal name)
  (-> Name (Meta Code))
  (do meta_monad
    [type+value (definition_value name)
     .let [[type value] type+value]]
    (case (flat_alias type)
      (^template [<name> <type> <wrapper>]
        [(#Named ["library/lux" <name>] _)
         (in (<wrapper> (:as <type> value)))])
      (["Bit"  Bit  bit$]
       ["Nat"  Nat  nat$]
       ["Int"  Int  int$]
       ["Rev"  Rev  rev$]
       ["Frac" Frac frac$]
       ["Text" Text text$])
      
      _
      (failure (text\composite "Cannot anti-quote type: " (name\encoded name))))))

(def: (static_literal token)
  (-> Code (Meta Code))
  (case token
    [_ (#Identifier [def_module def_name])]
    (if (text\= "" def_module)
      (do meta_monad
        [current_module current_module_name]
        (static_simple_literal [current_module def_name]))
      (static_simple_literal [def_module def_name]))

    (^template [<tag>]
      [[meta (<tag> parts)]
       (do meta_monad
         [=parts (monad\each meta_monad static_literal parts)]
         (in [meta (<tag> =parts)]))])
    ([#Form]
     [#Tuple])
    
    [meta (#Record pairs)]
    (do meta_monad
      [=pairs (monad\each meta_monad
                          (: (-> [Code Code] (Meta [Code Code]))
                             (function (_ [slot value])
                               (do meta_monad
                                 [=value (static_literal value)]
                                 (in [slot =value]))))
                          pairs)]
      (in [meta (#Record =pairs)]))

    _
    (\ meta_monad in_meta token)
    ... TODO: Figure out why this doesn't work:
    ... (\ meta_monad in token)
    ))

(macro: .public (static tokens)
  (case tokens
    (^ (list pattern))
    (do meta_monad
      [pattern' (static_literal pattern)]
      (in (list pattern')))
    
    _
    (failure "Wrong syntax for 'static'.")))

(type: Multi_Level_Case
  [Code (List [Code Code])])

(def: (case_level^ level)
  (-> Code (Meta [Code Code]))
  (case level
    (^ [_ (#Record (list [expr binding]))])
    (in_meta [expr binding])

    _
    (in_meta [level (` #1)])
    ))

(def: (multi_level_case^ levels)
  (-> (List Code) (Meta Multi_Level_Case))
  (case levels
    #End
    (failure "Multi-level patterns cannot be empty.")

    (#Item init extras)
    (do meta_monad
      [extras' (monad\each meta_monad case_level^ extras)]
      (in [init extras']))))

(def: (multi_level_case$ g!_ [[init_pattern levels] body])
  (-> Code [Multi_Level_Case Code] (List Code))
  (let [inner_pattern_body (list\mix (function (_ [calculation pattern] success)
                                       (let [bind? (case pattern
                                                     [_ (#Identifier _)]
                                                     #1

                                                     _
                                                     #0)]
                                         (` (case (~ calculation)
                                              (~ pattern)
                                              (~ success)

                                              (~+ (if bind?
                                                    (list)
                                                    (list g!_ (` #.None))))))))
                                     (` (#.Some (~ body)))
                                     (: (List [Code Code]) (list\reversed levels)))]
    (list init_pattern inner_pattern_body)))

(macro: .public (^multi tokens)
  (case tokens
    (^ (list& [_meta (#Form levels)] body next_branches))
    (do meta_monad
      [mlc (multi_level_case^ levels)
       .let [initial_bind? (case mlc
                             [[_ (#Identifier _)] _]
                             #1

                             _
                             #0)]
       expected ..expected_type
       g!temp (..identifier "temp")]
      (let [output (list g!temp
                         (` ({(#Some (~ g!temp))
                              (~ g!temp)

                              #None
                              (case (~ g!temp)
                                (~+ next_branches))}
                             ("lux type check" (#.Apply (~ (type_code expected)) Maybe)
                              (case (~ g!temp)
                                (~+ (multi_level_case$ g!temp [mlc body]))

                                (~+ (if initial_bind?
                                      (list)
                                      (list g!temp (` #.None)))))))))]
        (in output)))
    
    _
    (failure "Wrong syntax for ^multi")))

... 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
  (-> Name Text)
  (|>> name\encoded
       (text\composite "Wrong syntax for ")))

(macro: .public (name_of tokens)
  (case tokens
    (^template [<tag>]
      [(^ (list [_ (<tag> [module name])]))
       (in_meta (list (` [(~ (text$ module)) (~ (text$ name))])))])
    ([#Identifier] [#Tag])
    
    _
    (failure (..wrong_syntax_error ["library/lux" "name_of"]))))

(def: (scope_type_vars state)
  (Meta (List Nat))
  (case 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])))

(macro: .public (:parameter tokens)
  (case tokens
    (^ (list [_ (#Nat idx)]))
    (do meta_monad
      [stvs ..scope_type_vars]
      (case (..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 (name_of ..$)))))

(def: .public (same? reference sample)
  (All (_ a)
    (-> a a Bit))
  ("lux is" reference sample))

(macro: .public (^@ tokens)
  (case tokens
    (^ (list& [_meta (#Form (list [_ (#Identifier ["" name])] pattern))] body branches))
    (let [g!whole (local_identifier$ name)]
      (in_meta (list& g!whole
                      (` (case (~ g!whole) (~ pattern) (~ body)))
                      branches)))
    
    _
    (failure (..wrong_syntax_error (name_of ..^@)))))

(macro: .public (^|> tokens)
  (case tokens
    (^ (list& [_meta (#Form (list [_ (#Identifier ["" name])] [_ (#Tuple steps)]))] body branches))
    (let [g!name (local_identifier$ name)]
      (in_meta (list& g!name
                      (` (let [(~ g!name) (|> (~ g!name) (~+ steps))]
                           (~ body)))
                      branches)))
    
    _
    (failure (..wrong_syntax_error (name_of ..^|>)))))

(macro: .public (:expected tokens)
  (case tokens
    (^ (list expr))
    (do meta_monad
      [type ..expected_type]
      (in (list (` ("lux type as" (~ (type_code type)) (~ expr))))))
    
    _
    (failure (..wrong_syntax_error (name_of ..:expected)))))

(def: location
  (Meta Location)
  (function (_ compiler)
    (#Right [compiler (value@ #location compiler)])))

(macro: .public (undefined tokens)
  (case tokens
    #End
    (do meta_monad
      [location ..location
       .let [[module line column] location
             location ($_ "lux text concat" (text\encoded module) "," (nat\encoded line) "," (nat\encoded column))
             message ($_ "lux text concat" "Undefined behavior @ " location)]]
      (in (list (` (..panic! (~ (text$ message)))))))
    
    _
    (failure (..wrong_syntax_error (name_of ..undefined)))))

(macro: .public (:of tokens)
  (case tokens
    (^ (list [_ (#Identifier var_name)]))
    (do meta_monad
      [var_type (type_definition var_name)]
      (in (list (type_code var_type))))

    (^ (list expression))
    (do meta_monad
      [g!temp (..identifier "g!temp")]
      (in (list (` (let [(~ g!temp) (~ expression)]
                     (..:of (~ g!temp)))))))

    _
    (failure (..wrong_syntax_error (name_of ..:of)))))

(def: (tupleP tokens)
  (-> (List Code) (Maybe [(List Code) (List Code)]))
  (case tokens
    (^ (list& [_ (#Tuple tuple)] tokens'))
    (#Some [tokens' tuple])

    _
    #None))

(def: (templateP tokens)
  (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) (List Code)]))
  (|> (do maybe_monad
        [% (declarationP tokens)
         .let' [[tokens [export_policy name parameters]] %]
         % (annotationsP tokens)
         .let' [[tokens annotations] %]
         % (tupleP tokens)
         .let' [[tokens templates] %]
         _ (endP tokens)]
        (in [export_policy name parameters annotations templates]))
      ... (^ (list _export_policy _declaration _annotations _body))
      ... (^ (list _declaration _annotations _body))
      (maybe\else' (do maybe_monad
                     [% (declarationP tokens)
                      .let' [[tokens [export_policy name parameters]] %]
                      % (tupleP tokens)
                      .let' [[tokens templates] %]
                      _ (endP tokens)]
                     (in [export_policy name parameters #End templates])))
      ... (^ (list _export_policy _declaration _body))
      (maybe\else' (do maybe_monad
                     [% (local_declarationP tokens)
                      .let' [[tokens [name parameters]] %]
                      % (tupleP tokens)
                      .let' [[tokens templates] %]
                      _ (endP tokens)]
                     (in [(` ..private) name parameters #End templates])))
      ... (^ (list _declaration _body))
      ))

(macro: .public (template: tokens)
  (case (templateP tokens)
    (#Some [export_policy name args anns input_templates])
    (do meta_monad
      [g!tokens (..identifier "tokens")
       g!compiler (..identifier "compiler")
       g!_ (..identifier "_")
       .let [rep_env (list\each (function (_ arg)
                                  [arg (` ((~' ~) (~ (local_identifier$ arg))))])
                                args)]
       this_module current_module_name]
      (in (list (` (macro: (~ export_policy)
                     ((~ (local_identifier$ name)) (~ g!tokens) (~ g!compiler))
                     (~ (record$ anns))
                     (case (~ g!tokens)
                       (^ (list (~+ (list\each local_identifier$ args))))
                       (#.Right [(~ g!compiler)
                                 (list (~+ (list\each (function (_ template)
                                                        (` (`' (~ (with_replacements rep_env
                                                                    template)))))
                                                      input_templates)))])
                       
                       (~ g!_)
                       (#.Left (~ (text$ (..wrong_syntax_error [this_module name]))))))))))

    #None
    (failure (..wrong_syntax_error (name_of ..template:)))))

(macro: .public (as_is tokens compiler)
  (#Right [compiler tokens]))

(macro: .public (char tokens compiler)
  (case tokens
    (^multi (^ (list [_ (#Text input)]))
            (|> input "lux text size" ("lux i64 =" 1)))
    (|> input ("lux text char" 0)
        nat$ list
        [compiler] #Right)

    _
    (#Left (..wrong_syntax_error (name_of ..char)))))

(def: target
  (Meta Text)
  (function (_ compiler)
    (#Right [compiler (value@ [#info #target] compiler)])))

(def: (platform_name choice)
  (-> Code (Meta Text))
  (case choice
    [_ (#Text platform)]
    (..in_meta platform)

    [_ (#Identifier identifier)]
    (do meta_monad
      [identifier (..global_identifier identifier)
       type+value (..definition_value identifier)
       .let [[type value] type+value]]
      (case (..flat_alias type)
        (^or (#Primitive "#Text" #End)
             (#Named ["library/lux" "Text"] (#Primitive "#Text" #End)))
        (in (:as ..Text value))

        _
        (failure ($_ text\composite
                     "Invalid target platform (must be a value of type Text): " (name\encoded identifier)
                     " : " (..code\encoded (..type_code type))))))

    _
    (failure ($_ text\composite
                 "Invalid target platform syntax: " (..code\encoded choice)
                 ..\n "Must be either a text literal or an identifier."))))

(def: (target_pick target options default)
  (-> Text (List [Code Code]) (Maybe Code) (Meta (List Code)))
  (case options
    #End
    (case default
      #None
      (failure ($_ text\composite "No code for target platform: " target))

      (#Some default)
      (in_meta (list default)))

    (#Item [key pick] options')
    (do meta_monad
      [platform (..platform_name key)]
      (if (text\= target platform)
        (in_meta (list pick))
        (target_pick target options' default)))))

(macro: .public (for tokens)
  (do meta_monad
    [target ..target]
    (case tokens
      (^ (list [_ (#Record options)]))
      (target_pick target options #None)
      
      (^ (list [_ (#Record options)] default))
      (target_pick target options (#Some default))

      _
      (failure (..wrong_syntax_error (name_of ..for))))))

(def: (embedded_expansions code)
  (-> Code (Meta [(List [Code Code]) Code]))
  (case code
    (^ [ann (#Form (list [_ (#Identifier ["" "~~"])] expansion))])
    (do meta_monad
      [g!expansion (..identifier "g!expansion")]
      (in [(list [g!expansion expansion]) g!expansion]))

    (^template [<tag>]
      [[ann (<tag> parts)]
       (do meta_monad
         [=parts (monad\each meta_monad embedded_expansions parts)]
         (in [(list\mix list\composite (list) (list\each product\left =parts))
              [ann (<tag> (list\each product\right =parts))]]))])
    ([#Form] [#Tuple])

    [ann (#Record kvs)]
    (do meta_monad
      [=kvs (monad\each meta_monad
                        (function (_ [key val])
                          (do meta_monad
                            [=key (embedded_expansions key)
                             =val (embedded_expansions val)
                             .let [[key_labels key_labelled] =key
                                   [val_labels val_labelled] =val]]
                            (in [(list\composite key_labels val_labels) [key_labelled val_labelled]])))
                        kvs)]
      (in [(list\mix list\composite (list) (list\each product\left =kvs))
           [ann (#Record (list\each product\right =kvs))]]))
    
    _
    (in_meta [(list) code])))

(macro: .public (`` tokens)
  (case tokens
    (^ (list raw))
    (do meta_monad
      [=raw (..embedded_expansions raw)
       .let [[labels labelled] =raw]]
      (in (list (` (with_expansions [(~+ (|> labels
                                             (list\each (function (_ [label expansion]) (list label expansion)))
                                             list\conjoint))]
                     (~ labelled))))))

    _
    (failure (..wrong_syntax_error (name_of ..``)))))

(def: (name$ [module name])
  (-> Name Code)
  (` [(~ (text$ module)) (~ (text$ name))]))

(def: (untemplated_list& last inits)
  (-> Code (List Code) Code)
  (case inits
    #End
    last

    (#Item [init inits'])
    (` (#.Item (~ init) (~ (untemplated_list& last inits'))))))

(def: (untemplated_record g!meta untemplated_pattern fields)
  (-> Code (-> Code (Meta Code))
      (-> (List [Code Code]) (Meta Code)))
  (do meta_monad
    [=fields (monad\each meta_monad
                         (function (_ [key value])
                           (do meta_monad
                             [=key (untemplated_pattern key)
                              =value (untemplated_pattern value)]
                             (in (` [(~ =key) (~ =value)]))))
                         fields)]
    (in (` [(~ g!meta) (#.Record (~ (untemplated_list =fields)))]))))

(template [<tag> <name>]
  [(def: (<name> g!meta untemplated_pattern elems)
     (-> Code (-> Code (Meta Code))
         (-> (List Code) (Meta Code)))
     (case (list\reversed elems)
       (#Item [_ (#Form (#Item [[_ (#Identifier ["" "~+"])] (#Item [spliced #End])]))]
              inits)
       (do meta_monad
         [=inits (monad\each meta_monad untemplated_pattern (list\reversed inits))]
         (in (` [(~ g!meta) (<tag> (~ (untemplated_list& spliced =inits)))])))

       _
       (do meta_monad
         [=elems (monad\each meta_monad untemplated_pattern elems)]
         (in (` [(~ g!meta) (<tag> (~ (untemplated_list =elems)))])))))]

  [#.Tuple untemplated_tuple]
  [#.Form untemplated_form]
  )

(def: (untemplated_pattern pattern)
  (-> Code (Meta Code))
  (do meta_monad
    [g!meta (..identifier "g!meta")]
    (case pattern
      (^template [<tag> <gen>]
        [[_ (<tag> value)]
         (in (` [(~ g!meta) (<tag> (~ (<gen> value)))]))])
      ([#.Bit        bit$]
       [#.Nat        nat$]
       [#.Int        int$]
       [#.Rev        rev$]
       [#.Frac       frac$]
       [#.Text       text$]
       [#.Tag        name$]
       [#.Identifier name$])

      [_ (#Form (#Item [[_ (#Identifier ["" "~"])] (#Item [unquoted #End])]))]
      (in_meta unquoted)

      [_ (#Form (#Item [[_ (#Identifier ["" "~+"])] (#Item [spliced #End])]))]
      (failure "Cannot use (~+) inside of ^code unless it is the last element in a form or a tuple.")

      (^template [<tag> <untemplated>]
        [[_ (<tag> elems)]
         (<untemplated> g!meta untemplated_pattern elems)])
      ([#Tuple ..untemplated_tuple]
       [#Form ..untemplated_form])

      [_ (#Record fields)]
      (..untemplated_record g!meta untemplated_pattern fields)
      )))

(macro: .public (^code tokens)
  (case tokens
    (^ (list& [_meta (#Form (list template))] body branches))
    (do meta_monad
      [pattern (untemplated_pattern template)]
      (in (list& pattern body branches)))

    (^ (list template))
    (do meta_monad
      [pattern (untemplated_pattern template)]
      (in (list pattern)))

    _
    (failure (..wrong_syntax_error (name_of ..^code)))))

(def: .public false
  Bit
  #0)

(def: .public true
  Bit
  #1)

(macro: .public (:let tokens)
  (case tokens
    (^ (list [_ (#Tuple bindings)] bodyT))
    (if (multiple? 2 (list\size bindings))
      (in_meta (list (` (..with_expansions [(~+ (|> bindings
                                                    ..pairs
                                                    (list\each (function (_ [localT valueT])
                                                                 (list localT (` (..as_is (~ valueT))))))
                                                    (list\mix list\composite (list))))]
                          (~ bodyT)))))
      (..failure ":let requires an even number of parts"))

    _
    (..failure (..wrong_syntax_error (name_of ..:let)))))

(macro: .public (try tokens)
  (case tokens
    (^ (list expression))
    (do meta_monad
      [g!_ (..identifier "g!_")]
      (in (list (` ("lux try"
                    (.function ((~ g!_) (~ g!_))
                      (~ expression)))))))

    _
    (..failure (..wrong_syntax_error (name_of ..try)))))

(def: (methodP tokens)
  (-> (List Code) (Maybe [(List Code) [Text Code]]))
  (case tokens
    (^ (list& [_ (#Form (list [_ (#Text "lux type check")] type [_ (#Identifier ["" name])]))]
              tokens'))
    (#Some [tokens' [name type]])

    _
    #None))

(macro: .public (Interface tokens)
  (do meta_monad
    [methods' (monad\each meta_monad expansion tokens)]
    (case (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 for Interface"))))

(def: (recursive_type g!self g!dummy name body)
  (-> Code Code Text Code Code)
  (` ((.All ((~ g!self) (~ g!dummy))
        (~ (let$ (local_identifier$ name) (` (#.Apply .Nothing (~ g!self)))
                 body)))
      .Nothing)))

(macro: .public (Rec tokens)
  (case tokens
    (^ (list [_ (#Identifier "" name)] body))
    (do meta_monad
      [body' (expansion body)
       g!self (identifier "g!self")
       g!dummy (identifier "g!dummy")]
      (case 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 for Rec")))

    _
    (failure "Wrong syntax for Rec")))

(def: .public macro
  (-> Macro Macro')
  (|>> (:as Macro')))