module Total.Encoded.Test

import Total.NormalForm
import Total.Pretty
import Total.Encoded.Util

namespace List
  ListC : Container
  ListC = (Unit, 0) ::: [(N, 1)]

  export
  List : Ty
  List = fix ListC

  export
  nil : FullTerm List [<]
  nil = app (intro {c = ListC} Here) (app' pair [<arb, Pair.nil])

  export
  cons : FullTerm (N ~> List ~> List) [<]
  cons = abs' (S $ S Z)
    (\t, ts =>
      app (lift $ intro {c = ListC} $ There Here)
        (app' (lift pair)
          [<t
          , app' (lift Pair.cons) [<ts, lift Pair.nil]
          ]))

  export
  fold : {ty : Ty} -> FullTerm ((N ~> ty ~> ty) ~> ty ~> List ~> ty) [<]
  fold = abs' (S $ S Z)
    (\f, z => elim
      [ abs (drop z)
      , abs' (S Z) (\p =>
        app' (drop f)
          [<app (lift $ fst {u = Vect 1 ty}) p
          , app (lift (index {n = 1} FZ . snd {t = N})) p
          ])
      ])

MkList : List Nat -> FullTerm List [<]
MkList = foldr (\n, ts => app' cons [<lit n, ts]) nil

sum : FullTerm (List ~> N) [<]
sum = app' fold [<add, zero]

ten : FullTerm N [<]
ten = (app sum (MkList [1,2,3,4]))

tenNf : Term [<] N
tenNf = toTerm (normalize ten).term

main : IO Builtin.Unit
main = do
  let
    cases =
      [(lit 1, id)
      ,(lit 3, abs' (S Z) (\n => app' (lift add) [<n, n]))
      ,(lit 2, abs' (S Z) (\n => app (lift pred) n))]
  let t : FullTerm (N ~> N) [<] = cond cases
  -- let t : FullTerm N [<] = app sum (MkList [1,2,3,4])
  putDoc (group $ Doc.pretty "Input:" <+> line <+> pretty (toTerm t))
  putDoc (group $ Doc.pretty "Normal Form:" <+> line <+> pretty (toTerm (normalize t).term))