\   Based on "Breadth-First Numbering: Lessons from a Small Exercise in
\   Algorithm Design" by Chris Okasaki.

Begin
    (STDIO.print_line "bfnum0")
    (show (bfnum0 test) "")
    (STDIO.print_line "")
    (STDIO.print_line "bfnum1")
    (show (bfnum1 test) "")
End

Where

\   Copy the structure of t but insert breadth-first sequence numbers into the
\   internal nodes.

Define (bfnum0 t)
    Let in
        Unfold {i in} From {1 (new [t & 'nil])}
            Match (pop in)
            | 'just.{t in}
                Match t
                | 'e (push (Fold i in) 'e)
                | 't.{a _ b}
                    Let out (Fold [i + 1] (push (push in a) b))
                    In
                    Match (pop out)
                    | 'just.{b out}
                        Match (pop out)
                        | 'just.{a out}
                            (push out 't.{a i b})
                        ;
                    ;
                ;
            | 'nothing empty
            ;
    In
    Match (pop in)
    | 'just.{t _} t
    ;

\   Same as bfnum0 but using an explicit stack and separate analysis and
\   synthesis loops.

Define (bfnum1 t)
    Define (analyze t)
        Iterate {i q stack} From {1 (new [t & 'nil]) 'nil}
            Match (pop q)
            | 'nothing stack
            | 'just.{t q}
                Match t
                | 'e (Continue i q [0 & stack])
                | 't.{a _ b}
                    (Continue [i + 1] (push (push q a) b) [i & stack])
                ;
            ;
    Define (synthesize stack)
        Iterate {q stack} From {empty stack}
            Match stack
            | 'nil Match (pop q) | 'just.{t _} t ;
            | 'cons.{i stack}
                If [i = 0]
                    (Continue (push q 'e) stack)
                    Match (pop q)
                    | 'just.{b q}
                        Match (pop q)
                        | 'just.{a q}
                            (Continue (push q 't.{a i b}) stack)
                        ;
                    ;
            ;
    In
    (synthesize (analyze t))

Define (show t indent)
    Unfold {t indent}
        Match t
        | 't.{a n b}
            Let more_indent (STRING.append "  " indent)
            In
            Begin
                (Fold a more_indent)
                (STDIO.print_line (STRING.append indent (Z.show n)))
                (Fold b more_indent)
            End
        | 'e
            (STDIO.print_line (STRING.append indent "$"))
        ;

Let test
    't.{
        't.{
            'e
            "2"
            't.{
                'e
                "4"
                'e
            }
        }
        "1"
        't.{
            'e
            "3"
            'e
        }
    }

Where

Let empty QUEUE.empty
Let new QUEUE.new
Let push QUEUE.push
Let pop QUEUE.pop

Where

Let LIST Package "list"
Let QUEUE Package "queue"
Let STDIO Package "stdio"
Let STRING Package "string"
Let Z Package "z"