(.using
 [library
  [lux (.full)
   ["[0]" meta]
   [abstract
    ["[0]" monad (.only Monad do)
     [indexed (.only IxMonad)]]]
   [control
    ["[0]" maybe]
    ["[0]" exception (.only exception:)]
    ["<>" parser
     ["<[0]>" code (.only Parser)]]]
   [data
    [text
     ["%" format (.only format)]]
    [collection
     ["[0]" set]
     ["[0]" sequence (.only Sequence)]
     ["[0]" list ("[1]#[0]" functor mix)]]]
   ["[0]" macro
    [syntax (.only syntax:)]]
   [math
    [number
     ["n" nat]]]
   [type
    [primitive (.full)]]]])

(type: .public (Procedure monad input output value)
  (-> input (monad [output value])))

(type: .public (Linear monad value)
  (All (_ keys)
    (Procedure monad keys keys value)))

(type: .public (Affine monad permissions value)
  (All (_ keys)
    (Procedure monad keys [permissions keys] value)))

(type: .public (Relevant monad permissions value)
  (All (_ keys)
    (Procedure monad [permissions keys] keys value)))

(implementation: .public (monad monad)
  (All (_ !) (-> (Monad !) (IxMonad (Procedure !))))
  
  (def: (in value)
    (function (_ keys)
      (# monad in [keys value])))

  (def: (then f input)
    (function (_ keysI)
      (do monad
        [[keysT value] (input keysI)]
        ((f value) keysT)))))

(def: .public (run! monad procedure)
  (All (_ ! v) (-> (Monad !) (Linear ! v) (! v)))
  (do monad
    [[_ output] (procedure [])]
    (in output)))

(def: .public (lifted monad procedure)
  (All (_ ! v) (-> (Monad !) (! v) (Linear ! v)))
  (function (_ keys)
    (do monad
      [output procedure]
      (in [keys output]))))

(primitive: .public Ordered Any)
(primitive: .public Commutative Any)

(primitive: .public (Key mode key)
  Any

  (template [<name> <mode>]
    [(def: <name>
       (Ex (_ k) (-> Any (Key <mode> k)))
       (|>> abstraction))]

    [ordered_key     Ordered]
    [commutative_key Commutative]
    ))

(primitive: .public (Res key value)
  value

  (template [<name> <mode> <key>]
    [(def: .public (<name> monad value)
       (All (_ ! v) (Ex (_ k) (-> (Monad !) v (Affine ! (Key <mode> k) (Res k v)))))
       (function (_ keys)
         (# monad in [[(<key> []) keys] (abstraction value)])))]

    [ordered     Ordered     ..ordered_key]
    [commutative Commutative ..commutative_key]
    )

  (def: .public (read monad resource)
    (All (_ ! v k m)
      (-> (Monad !) (Res k v) (Relevant ! (Key m k) v)))
    (function (_ [key keys])
      (#  monad in [keys (representation resource)])))
  )

(exception: .public (index_cannot_be_repeated [index Nat])
  (exception.report
   "Index" (%.nat index)))

(exception: .public amount_cannot_be_zero)

(def: indices
  (Parser (List Nat))
  (<code>.tuple (loop (again [seen (set.empty n.hash)])
                  (do [! <>.monad]
                    [done? <code>.end?]
                    (if done?
                      (in (list))
                      (do !
                        [head <code>.nat
                         _ (<>.assertion (exception.error ..index_cannot_be_repeated head)
                                         (not (set.member? seen head)))
                         tail (again (set.has head seen))]
                        (in (partial_list head tail))))))))

(def: (no_op monad)
  (All (_ m) (-> (Monad m) (Linear m Any)))
  (function (_ context)
    (# monad in [context []])))

(syntax: .public (exchange [swaps ..indices])
  (macro.with_symbols [g!_ g!context g!!]
    (case swaps
      {.#End}
      (in (list (` (~! no_op))))

      {.#Item head tail}
      (do [! meta.monad]
        [.let [max_idx (list#mix n.max head tail)]
         g!inputs (<| (monad.all !) (list.repeated (++ max_idx)) (macro.symbol "input"))
         .let [g!outputs (|> (monad.mix maybe.monad
                                        (function (_ from to)
                                          (do maybe.monad
                                            [input (list.item from g!inputs)]
                                            (in (sequence.suffix input to))))
                                        (is (Sequence Code) sequence.empty)
                                        swaps)
                             maybe.trusted
                             sequence.list)
               g!inputsT+ (list#each (|>> (~) (..Key ..Commutative) (`)) g!inputs)
               g!outputsT+ (list#each (|>> (~) (..Key ..Commutative) (`)) g!outputs)]]
        (in (list (` (is (All ((~ g!_) (~ g!!) (~+ g!inputs) (~ g!context))
                           (-> ((~! monad.Monad) (~ g!!))
                               (Procedure (~ g!!)
                                          [(~+ g!inputsT+) (~ g!context)]
                                          [(~+ g!outputsT+) (~ g!context)]
                                          .Any)))
                         (function ((~ g!_) (~ g!!) [(~+ g!inputs) (~ g!context)])
                           (# (~ g!!) (~' in) [[(~+ g!outputs) (~ g!context)] []]))))))))))

(def: amount
  (Parser Nat)
  (do <>.monad
    [raw <code>.nat
     _ (<>.assertion (exception.error ..amount_cannot_be_zero [])
                     (n.> 0 raw))]
    (in raw)))

(template [<name> <from> <to>]
  [(syntax: .public (<name> [amount ..amount])
     (macro.with_symbols [g!_ g!context g!!]
       (do [! meta.monad]
         [g!keys (|> (macro.symbol "keys")
                     (list.repeated amount)
                     (monad.all !))]
         (in (list (` (is (All ((~ g!_) (~ g!!) (~+ g!keys) (~ g!context))
                            (-> ((~! monad.Monad) (~ g!!))
                                (Procedure (~ g!!)
                                           [<from> (~ g!context)]
                                           [<to> (~ g!context)]
                                           .Any)))
                          (function ((~ g!_) (~ g!!) [<from> (~ g!context)])
                            (# (~ g!!) (~' in) [[<to> (~ g!context)] []])))))))))]

  [group    (~+ g!keys)   [(~+ g!keys)]]
  [un_group [(~+ g!keys)] (~+ g!keys)]
  )