erased.tt

-- vim: ft=ttstar

  let
    constructor Z : Nat
    constructor S : (x) -> Nat
    constructor True : Bool
    constructor False : Bool
    constructor Nil : List
    constructor Cons : (_x0) -> (_x1) -> List
    repl 
      repl Z x xs = xs
      repl (S n) x xs = Cons x (repl n x xs)
    constructor RNil : RLE
    constructor RCons : (n) -> (x) -> (_x4) -> RLE
    compress 
      compress Nil = RNil
      compress (Cons x xs) = 
        let aux 
          aux y RNil = RCons 1 y RNil
          aux True (RCons n True rzs) = RCons (S n) True rzs
          aux False (RCons n False rzs) = RCons (S n) False rzs
          aux True (RCons n False rzs) = RCons 1 True (RCons n False rzs)
          aux False (RCons n True rzs) = RCons 1 False (RCons n True rzs)
        in aux x (compress xs)
    decompress 
      decompress RNil = Nil
      decompress (RCons n x rxs) = repl n x (decompress rxs)
    foldl 
      foldl f z Nil = z
      foldl f z (Cons x xs) = foldl f (f z x) xs
    xor 
      xor False b = b
      xor True False = True
      xor True True = False
    xors = foldl xor False
    genInputList = (\n. repl n True Nil)
    main = 
      let
        foreign inputSize
        inputList = genInputList inputSize
      in xors (decompress (compress inputList))
  in main