(* Below is an implementation in Polite of the algorithm from Song's
   Linear Time Addition of Fibonacci Encodings for normalizing Fibonacci sums:
   http://reports-archive.adm.cs.cmu.edu/anon/2020/CMU-CS-20-118.pdf *)

type fib        = +{'0 : fib,      '1 : fib,        'e : 1}
type normal     = +{'0 : normal,   '1 : normal1,    'e : 1}
type normal1    = +{'0 : normal,                    'e : 1}
type buffered   = +{'0 : buffered, '1 : buffered1,  'e : 1}
type buffered1  = +{'0 : buffered, '1 : buffered11, 'e : 1}
type buffered11 = +{'0 : buffered1,                 'e : 1}

comp pass1 : fib -> <buffered>
   = fun x0 => pass1_0 x0

comp pass1_0 : fib -> <buffered1>
   = fun x0 => match x0 { '0 x1 => let <x2> = pass1_0 x1 in
                                   <'0 x2>
                        | '1 x3 => let <x4> = pass1_01 x3 in
                                   <x4>
                        | 'e x5 => <'0 'e ()> }

comp pass1_01 : fib -> <buffered1>
   = fun x0 => match x0 { '0 x1 => let <x2> = pass1_0 x1 in
                                   <'0 '1 x2>
                        | '1 x3 => let <x4> = pass1_0 x3 in
                                   <'1 '0 x4>
                        | 'e x5 => <'0 '1 'e ()> }

comp pass2 : buffered -> <normal>
   = fun x0 => match x0 { '0 x1 => let <x2> = pass2 x1 in
                                   <'0 x2>
                        | '1 x3 => let <x4> = pass2_1 x3 in
                                   <x4>
                        | 'e x5 => <'e ()> }

comp pass2_1 : buffered1 -> <normal>
   = fun x0 => match x0 { '0 x1 => let <x2> = pass2 x1 in
                                   <'1 '0 x2>
                        | '1 x3 => let <x4> = pass2_11 x3 in
                                   <x4>
                        | 'e x5 => <'1 'e ()> }

comp pass2_11 : buffered11 -> <normal>
   = fun x0 => match x0 { '0 x1 => let <x2> = pass2_1 x1 in
                                   <'0 '0 x2>
                                   | 'e x3 => <'0 '0 '1 'e ()> }

comp rev : fib -> fib -> <fib> /\ buffered -> buffered11 ->
           <buffered> /\ buffered1 -> buffered1 ->
           <buffered> /\ buffered11 -> buffered -> <buffered>
   = fun x0 => fun x1 => match x0 { '0 x2 => rev x2 ('0 x1)
                                  | '1 x3 => rev x3 ('1 x1)
                                  | 'e x4 => <x1> }

comp reverse : fib -> <fib> /\ buffered -> <buffered>
   = fun x0 => rev x0 ('e ())
comp normalize : fib -> <normal>
   = fun x0 => let <x1> = reverse x0 in
               let <x2> = pass1 x1 in
               let <x3> = reverse x2 in
               let <x4> = pass2 x3 in
               <x4>

(* 63 = 11011101 = 1+2+5+8+13+34 (non-canonical) *)
comp fib63 : <fib>
   = <'1 '1 '0 '1 '1 '1 '0 '1 'e ()>

(* fib63normal = 000010001 = 8 + 55 (canonical) *)
eval fib63normal : <normal>
   = let <f63> = fib63 in normalize f63

Generated by Zeeshan Lakhani using scpaste at Sat Aug 10 01:39:25 2024. EDT. (original)