(define $Something
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     }))

(define $Suit
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (deconstructor
        {[spade []
          {[<spade> {[]}]
           [_ {}]}]
         [heart []
          {[<heart> {[]}]
           [_ {}]}]
         [club []
          {[<club> {[]}]
           [_ {}]}]
         [diamond []
          {[<diamond> {[]}]
           [_ {}]}]
         })]
     [$=
      (lambda [$val $tgt]
        (match [val tgt] [Card Card]
          {[[<spade> <spade>] <true>]
           [[<heart> <heart>] <true>]
           [[<club> <club>] <true>]
           [[<diamond> <diamond>] <true>]
           [[_ _] <false>]}))]
     }))

(test (match-map <club> Suit [<club> <ok>]))

(define $Nat
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (deconstructor
        {[o []
          {[<o> {[]}]
           [_ {}]
           }]
         [s [Nat]
          {[<s $x> {x}]
           [_ {}]
           }]
         })]
     [$=
      (lambda [$val $tgt]
        (match [val tgt] [Nat Nat]
          {[[<o> <o>] <true>]
           [[<s $n1> <s $n2>] (= n1 n2)]
           [[_ _] <false>]}))]
     }))

(define $monus
  (lambda [$m $n]
    (match [m n] [Nat Nat]
      {[[_ <o>] m]
       [[<o> _] <o>]
       [[<s $m1> <s $n1>] (monus m1 n1)]})))

(test (monus <s <s <o>>> <s <o>>))

(define $mod
  (lambda [$m $n]
    (match (monus m n) Nat
      {[<o> m]
       [$m1 (mod m1 n)]})))

(test (mod <s <s <s <s <o>>>>> <s <s <s <o>>>>))

(define $Mod
  (lambda [$m]
    (let {[$Loop
           (type {[$var-match (lambda [$tgt] {tgt})]
                  [$inductive-match
                   (deconstructor
                     {[o []
                       {[<o> {[]}]
                        [_ {}]
                        }]
                      [s [Loop]
                       {[<s $x> {x}]
                        [<o> {m}]
                        }]})]
                  [$= (lambda [$val $tgt]
                        ((type-ref Nat =) (mod val m) tgt))]})]}
      (type
        {[$var-match (lambda [$tgt] {(mod tgt m)})]
         [$inductive-match
          (lambda [$tgt]
            ((type-ref Loop inductive-match) (mod tgt m)))]
         [$= (lambda [$val $tgt]
               ((type-ref Nat =) (mod val m) (mod tgt m)))]}))))

(test (match <s <s <s <s <o>>>>> (Mod <s <s <s <o>>>>)
        {[<o> <not-ok>]
         [<s <o>> <ok>]
         [<s <s <o>>> <not-ok>]}))

(define $List
  (lambda [$a]
    (type
      {[$var-match (lambda [$tgt] {tgt})]
       [$inductive-match
        (deconstructor
          {[nil []
            {[{} {[]}]
             [_ {}]
             }]
           [cons [a (List a)]
            {[{$x .$xs} {[x xs]}]
             [_ {}]
             }]
           [snoc [a (List a)]
            {[{.$xs $x} {[x xs]}]
             [_ {}]
             }]
           [join [(List a) (List a)]
            {[$tgt (let {[$loop
                       (lambda [$ts]
                         (match ts (List a)
                           {[<nil> {[{} {}]}]
                            [<cons $x $xs>
                             {[{} ts]
                              @(map (lambda [$as $bs]
                                      [{x @as} bs])
                                    (loop xs))}]}))]}
                   (loop tgt))]
             }]
           [nioj [(List a) (List a)]
            {[$tgt (let {[$loop
                       (lambda [$ts]
                         (match ts (List a)
                           {[<nil> {[{} {}]}]
                            [<snoc $x $xs>
                             {[{} ts]
                              @(map (lambda [$as $bs]
                                      [{@as x} bs])
                                    (loop xs))}]}))]}
                   (loop tgt))]
             }]
           })]
       [$= (lambda [$val $tgt]
             (match [val tgt] [(List a) (List a)]
               {[[<nil> <nil>] <true>]
                [[<cons $x $xs>
                  <cons (on [$x] ,x) (on [$xs] ,xs)>]
                 <true>]
                [[_ _] <false>]}))]
       })))

(test ((type-ref (List Nat) =) {<o> <s <o>>} {<o> <s <o>>}))

(test (match-map {<o> <s <o>> <s <s <o>>>} (List Nat) [<snoc $x $xs> [x xs]]))

(test (match-map {<o> <s <o>> <s <s <o>>>} (List Nat) [<nioj $xs $ys> [xs ys]]))

(define $map
  (lambda [$fn $ls]
    (match ls (List Something)
      {[<nil> {}]
       [<cons $x $xs> {(fn x) @(map fn xs)}]})))

(test (map (lambda [$a] <s a>) {<o> <s <o>>}))

(test (match {} (List Something)
        {[<join $hs $ts> [hs ts]]}))

(test (match-map {<x> <y>} (List Something)
        [<join $hs $ts> [hs ts]]))

(test (match-map {<x> <y> <z> <w>} (List Something)
        [<join $hs <cons $x $ts>> [hs x ts]]))

(define $remove
  (lambda [$a]
    (lambda [$xs $x]
      (match xs (List a)
        {[<nil> {}]
         [<cons x $rs> rs]
         [<cons $y $rs> {y @((remove a) rs x)}]}))))

(test ((remove Nat) {<o> <s <o>>} <o>))

(define $remove-collection
  (lambda [$a]
    (lambda [$xs $ys]
      (match ys (List a)
        {[<nil> xs]
         [<cons $y $rs> ((remove-collection a) ((remove a) xs y) rs)]}))))

(test ((remove-collection Nat) {<o> <s <o>> <s <s <o>>>} {<o> <s <s <o>>>}))

(define $subcollection
  (lambda [$xs]
    (match xs (List Something)
      {[<nil> {{}}]
       [<cons $x $rs>
        (let {[$subs (subcollection rs)]}
          {@subs @(map (lambda [$sub] {x @sub})
                       subs)})]
       })))

(test (subcollection {<o> <s <o>> <s <s <o>>>}))

(define $Multiset
  (lambda [$a]
    (type
      {[$var-match (lambda [$tgt] {tgt})]
       [$inductive-match
        (deconstructor
         {[nil []
           {[{} {[]}]
            [_ {}]
            }]
          [cons [a (Multiset a)]
           {[$tgt (map (lambda [$t] [t ((remove a) tgt t)])
                    tgt)]
            }]
          [join [(Multiset a) (Multiset a)]
           {[$tgt (map (lambda [$ts] [ts ((remove-collection a) tgt ts)])
                    (subcollections tgt))]
            }]
          })]
       [$= (lambda [$val $tgt]
             (match [val tgt] [(Multiset a) (Multiset a)]
               {[[<nil> <nil>] <true>]
                [[<cons $x $xs>
                  <cons (on [$x] x) (on [$xs] xs)>]
                 <true>]
                [[_ _] <false>]}))]
       })))

(define $one-pair
  (lambda [$ns]
    (match ns (Multiset Nat)
      {[<cons $m
         <cons (on [$m] m)
          _>>
        <ok>]
       [_ <nothing>]
       })))

(test (one-pair {<o> <s <o>> <o>}))

(define $full-house
  (lambda [$ns]
    (match ns (Multiset Nat)
      {[<cons $m
         <cons (on [$m] m)
          <cons (on [$m] m)
           !<cons $n
             !<cons (on [$n] n)
               !<nil>
               >>>>>
        <full-house>]
       [_ <nothing>]
       })))

(test (full-house {<o> <o> <s <o>> <o> <s <o>>}))

(define $thirteen <s <s <s <s <s <s <s <s <s <s <s <s <s <o>>>>>>>>>>>>>>)

(define $Card
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (deconstructor
        {[card [Suit (Mod thirteen)]
          {[<card $s $n> {[s n]}]}]})]
     [$= <undefined>]}))

(define $poker-hands
  (lambda [$Cs]
    (match Cs (Multiset Card)
      {[<cons <card $S $n>
         <cons <card (on [$S] ,S) (on [$n] ,(- n 1))>
          <cons <card (on [$S] ,S) (on [$n] ,(- n 2))>
           <cons <card (on [$S] ,S) (on [$n] ,(- n 3))>
            <cons <card (on [$S] ,S) (on [$n] ,(- n 4))>
             !<nil>
             >>>>>
        <straight-flush>]
       [<cons <card _ $n>
         <cons <card _ (on [$n] ,n)>
          !<cons <card _ (on [$n] ,n)>
            !<cons <card _ (on [$n] ,n)>
              !<cons _
                !<nil>
                >>>>>
        <four-of-kind>]
       [<cons <card _ $m>
         <cons <card _ (on [$m] ,m)>
          <cons <card _ (on [$m] ,m)>
           !<cons <card _ $n>
             !<cons <card _ (on [$n] ,n)>
               !<nil>
               >>>>>
        <full-house>]
       [<cons <card $S _>
         !<cons <card (on [$S] ,S) _>
           !<cons <card (on [$S] ,S) _>
             !<cons <card (on [$S] ,S) _>
               !<cons <card (on [$S] ,S) _>
                 !<nil>
                 >>>>>
        <flush>]
       [<cons <card _ $n>
         <cons <card _ (on [$n] ,(- n 1))>
          <cons <card _ (on [$n] ,(- n 2))>
           <cons <card _ (on [$n] ,(- n 3))>
            <cons <card _ (on [$n] ,(- n 4))>
             !<nil>
             >>>>>
        <straight>]
       [<cons <card _ $n>
         <cons <card _ (on [$n] ,n)>
          <cons <card _ (on [$n] ,n)>
           !<cons _
             !<cons _
               !<nil>
               >>>>>
        <three-of-kind>]
       [<cons <card _ $m>
         <cons <card _ (on [$m] ,m)>
          !<cons <card _ $n>
            <cons <card _ (on [$n] ,n)>
             !<cons _
               !<nil>
               >>>>>
        <two-pair>]
       [<cons <card _ $n>
         <cons <card _ (on [$n] ,n)>
          !<cons _
            !<cons _
              !<cons _
                !<nil>
                >>>>>
        <one-pair>]
       [<cons _
         !<cons _
           !<cons _
             !<cons _
               !<cons _
                 !<nil>
                 >>>>>
        <nothing>]})))

(define $poker-hands-without-strait
  (lambda [$Cs]
    (match Cs (Multiset Card)
      {[<cons <card _ $n>
         <cons <card _ (on [$n] ,n)>
          !<cons <card _ (on [$n] ,n)>
            !<cons <card _ (on [$n] ,n)>
              !<cons _
                !<nil>
                >>>>>
        <four-of-kind>]
       [<cons <card _ $m>
         <cons <card _ (on [$m] ,m)>
          <cons <card _ (on [$m] ,m)>
           !<cons <card _ $n>
             !<cons <card _ (on [$n] ,n)>
               !<nil>
               >>>>>
        <full-house>]
       [<cons <card $S _>
         !<cons <card (on [$S] ,S) _>
           !<cons <card (on [$S] ,S) _>
             !<cons <card (on [$S] ,S) _>
               !<cons <card (on [$S] ,S) _>
                 !<nil>
                 >>>>>
        <flush>]
       [<cons <card _ $n>
         <cons <card _ (on [$n] ,n)>
          <cons <card _ (on [$n] ,n)>
           !<cons _
             !<cons _
               !<nil>
               >>>>>
        <three-of-kind>]
       [<cons <card _ $m>
         <cons <card _ (on [$m] ,m)>
          !<cons <card _ $n>
            <cons <card _ (on [$n] ,n)>
             !<cons _
               !<nil>
               >>>>>
        <two-pair>]
       [<cons <card _ $n>
         <cons <card _ (on [$n] ,n)>
          !<cons _
            !<cons _
              !<cons _
                !<nil>
                >>>>>
        <one-pair>]
       [<cons _
         !<cons _
           !<cons _
             !<cons _
               !<cons _
                 !<nil>
                 >>>>>
        <nothing>]})))

(test (poker-hands-without-strait {<card <diamond> <o>>
                                   <card <club> <s <o>>>
                                   <card <club> <o>>
                                   <card <heart> <o>>
                                   <card <diamond> <s <o>>>}))

(define $car
  (lambda [$as]
    (match as (List Something)
      {[<cons $a _> a]})))

(define $reverse
  (lambda [$as]
    (match as (List Something)
      {[<nil> {}]
       [<cons $a $rs>
        {@(reverse rs) a}]})))