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

(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)))

(def .public (monad monad)
  (All (_ !) (-> (Monad !) (IxMonad (Procedure !))))
  (implementation
   (def (in value)
     (function (_ keys)
       (at 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

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

    [ordered_key     Ordered]
    [commutative_key Commutative]
    ))

(primitive .public (Res key value)
  value

  (with_template [<name> <mode> <key>]
    [(def .public (<name> monad value)
       (All (_ ! v) (Ex (_ k) (-> (Monad !) v (Affine ! (Key <mode> k) (Res k v)))))
       (function (_ keys)
         (at 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])
      (at  monad in [keys (representation resource)])))
  )

(exception.def .public (index_cannot_be_repeated index)
  (Exception Nat)
  (exception.report
   (list ["Index" (%.nat index)])))

(exception.def .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 (list.partial head tail))))))))

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

(def .public exchange
  (syntax (_ [swaps ..indices])
    (macro.with_symbols [g!_ g!context g!!]
      (when 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)])
                             (at (, 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)))

(with_template [<name> <from> <to>]
  [(def .public <name>
     (syntax (_ [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)])
                              (at (, g!!) (,' in) [[<to> (, g!context)] []]))))))))))]

  [group    (,* g!keys)   [(,* g!keys)]]
  [un_group [(,* g!keys)] (,* g!keys)]
  )