metafib.mela

let and = fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then b2 else false in
let or =  fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then true else b2 in
let map = fn (f : int * int * int -> int * int * int) ->
          fix (mapf : list (int * int * int) -> list (int * int * int)) xs ->
            case xs of
              { [] -> [] of (int * int * int)
              ; x :: xs -> f x :: mapf xs
              } in
let append = fix (append : list (int * int * int) -> list (int * int * int) -> list (int * int * int)) xs ->
             fn (ys : list (int * int * int)) ->
               case xs of
                 { [] -> ys
                 ; x :: xs -> x :: append xs ys
                 } in
let lexLt = fn (x1 : int * int) -> fn (x2 : int * int) ->
              case x1 of
                (m1, n1) ->
                  case x2 of
                    (m2, n2) -> or (m1 < m2) (and (m1 == m2) (n1 < n2)) in
let lexEq = fn (x1 : int * int) -> fn (x2 : int * int) ->
              case x1 of
                (m1, n1) ->
                  case x2 of
                    (m2, n2) -> and (m1 == m2) (n1 == n2) in
let insert = fn (x : int * int * int) ->
               case x of
                 (i, c1) -> fix (insert : list (int * int * int) -> list (int * int * int)) xs ->
                              case xs of
                                { [] -> (i, c1) :: [] of (int * int * int)
                                ; x :: xs ->
                                  case x of
                                    (j, c2) ->
                                      if lexLt i j then
                                        (i,c1) :: (i,c2) :: xs
                                      else if lexEq i j then
                                        (i,c1+c2) :: xs
                                      else
                                        (j, c2) :: insert xs
                                } in
let minimize = fix (mini : list (int * int * int) -> list (int * int * int)) xs ->
                 case xs of
                   { []      -> [] of (int * int * int)
                   ; x :: xs -> insert x (mini xs)
                   } in
let filterZero = fix (filter : list (int * int * int) -> list (int * int * int)) xs ->
                   case xs of
                     { []      -> [] of (int * int * int)
                     ; x :: xs ->
                       case x of
                         (mn, c) ->
                           case c == 0 of
                             { true -> filter xs
                             ; false -> x :: filter xs
                             }
                     } in
let mulAlpha = fn (x : int * int * int) ->
                 case x of
                   (mn, c) ->
                   case mn of
                     (m, n) -> ((m+1,n),c) in
let mulBeta  = fn (x : int * int * int) ->
                 case x of
                   (mn, c) ->
                   case mn of
                     (m, n) -> ((m,n+1),c) in
let fibPoly =
      let f = fix (fib : int -> list (int * int * int)) n ->
                case n <= 1 of
                { true -> ((0,0), n) :: [] of (int * int * int)
                ; false -> append (map mulAlpha (fib (n-1))) (map mulBeta (fib (n-2)))
                } in
      fn (n : int) -> filterZero (minimize (f n)) in
let genTerm = fn (x : int * int * int) ->
                case x of
                  (mn, c) ->
                  case mn of
                    (m, n) ->
                    if and (c == 1) (m == 0) then
                        if n == 0 then
                          box[a:int,b:int. 1 ]
                        else if n == 1 then
                          box[a:int,b:int. b ]
                        else
                          let box[N] = inject n in
                          box[a:int,b:int. b ^ N with [] ]
                    else
                      let box[CA] =
                        if c == 1 then
                          if m == 1 then
                            box[a:int. a ]
                          else
                            let box[M] = inject m in
                            box[a:int. a ^ M with [] ]
                        else
                          let box[C] = inject c in
                          if m == 0 then
                            box[a:int. C with [] ]
                          else if m == 1 then
                            box[a:int. C with [] * a ]
                          else
                            let box[M] = inject m in
                            box[a:int. C with [] * a ^ M with [] ]
                      in
                      if n == 0 then
                        box[a:int,b:int. CA with [a/a] ]
                      else if n == 1 then
                        box[a:int,b:int. CA with [a/a] * b ]
                      else
                        let box[N] = inject n in
                        box[a:int,b:int. CA with [a/a] * b ^ N with [] ] in
let codegen = fix (poly : list (int * int * int) -> [a : int, b : int |- int]) xs ->
                case xs of
                { [] -> box[a:int,b:int. 0]
                ; x :: xs ->
                  let box[T] = genTerm x in
                  case xs of
                  { [] -> box[a:int,b:int. T with [a/a,b/b] ]
                  ; y :: ys -> let box[U] = poly xs in
                               box[a:int,b:int. U with [a/a,b/b] + T with [a/a,b/b] ]
                  }
                } in
let fibcode = fn (n : int) -> codegen (fibPoly n) in
let fib = fn (n : int) ->
            let box[U] = fibcode n in
            U with [1/a,1/b] in
( fibcode 0 :: fibcode 1 :: fibcode 2 :: fibcode 3 :: fibcode 4 :: fibcode 5 ::
  fibcode 6 :: fibcode 7 :: fibcode 8 :: fibcode 9 :: fibcode 10 :: [] of [a:int,b:int |- int]
, fib 0 :: fib 1 :: fib 2 :: fib 3 :: fib 4 :: fib 5 ::
  fib 6 :: fib 7 :: fib 8 :: fib 9 :: fib 10 :: [] of int
)

result

( box[a : int, b : int . 0] ::
  box[a : int, b : int . 1] ::
  box[a : int, b : int . a] ::
  box[a : int, b : int . a ^ 2 + b] ::
  box[a : int, b : int . a ^ 3 + 2 * a * b] ::
  box[a : int, b : int . a ^ 4 + 3 * a ^ 2 * b + b ^ 2] ::
  box[a : int, b : int . a ^ 5 + 4 * a ^ 3 * b + 3 * a * b ^ 2] ::
  box[a : int, b : int . a ^ 6 + 5 * a ^ 4 * b + 6 * a ^ 2 * b ^ 2 + b ^ 3] ::
  box[a : int, b : int . a ^ 7 + 6 * a ^ 5 * b + 10 * a ^ 3 * b ^ 2 + 4 * a * b ^ 3] ::
  box[a : int, b : int . a ^ 8 + 7 * a ^ 6 * b + 15 * a ^ 4 * b ^ 2 + 10 * a ^ 2 * b ^ 3 + b ^ 4] ::
  box[a : int, b : int . a ^ 9 + 8 * a ^ 7 * b + 21 * a ^ 5 * b ^ 2 + 20 * a ^ 3 * b ^ 3 + 5 * a * b ^ 4] ::
  [] of [a : int, b : int |- int]
, 0 :: 1 :: 1 :: 2 :: 3 :: 5 :: 8 :: 13 :: 21 :: 34 :: 55 :: [] of int
)