test.timl

datatype 'a list =
         nil
         | cons of 'a * 'a list

datatype {Nat} 'a ilist =
         NilI of unit -> {0} 'a ilist
         | ConsI of {n' : Nat} 'a * {n'} 'a ilist -> {n' + 1} 'a ilist

datatype {Nat} {Bool} 'a rbt =
         Leaf of unit -> {0} {true} 'a rbt
         | Black of {lc : Bool} {rc : Bool} {bh : Nat}
                                'a * {bh} {lc} 'a rbt * {bh} {rc} 'a rbt -> {bh + 1} {true} 'a rbt
         | Red of {bh : Nat}
                      'a * {bh} {true} 'a rbt * {bh} {true} 'a rbt -> {bh} {false} 'a rbt

val n = 77

val _ =
    let                                                              
        val n = 77
    in
        n
    end

val (a, (b, (c, ()))) = (1, (2, (3, ())))

val _ = fn ['a] ['b] ((x, y) : 'a * 'b) => (y, x)

(*(* not exhaustive *)*)
(* val _ = fn ['a] (nil : 'a list) => nil ['a] *)

val _ = 
 fn ['a] (ls : 'a list) =>
    case ls of
        nil => nil ['a]
      | cons _ => nil ['a]

val _ = 
 fn ['a] {n : Nat} (ls : {n} 'a ilist) =>
    case ls of
        NilI => 0
      | ConsI {_} _ => 0

(* redundant *)

(* val _ = *)
(*  fn ['a] {n : Nat} (ls : {n} 'a ilist) => *)
(*     case ls of *)
(*         NilI => 0 *)
(*       | ConsI {_} _ => 0 *)
(*       | ConsI {_} (_, NilI) => 0 *)

(* not exhaustive *)

(* val _ = *)
(*  fn ['a] {n : Nat} (ls : {n} 'a ilist) => *)
(*     case ls of *)
(*         NilI => 0 *)
(*       | ConsI {_} (_, NilI) => 0 *)
(*       | ConsI {_} (_, (ConsI {_} (_, NilI))) => 0 *)

val map = 
 fn ['a] ['b] {m : Time} (f : 'a -- m --> 'b) =>
    fix map {n : Nat} (ls : {n} 'a ilist) : {n} 'b ilist |> (m + 2.0) * $n =>
    case ls return {n} 'b ilist |> (m + 2.0) * $n of
        NilI => NilI ['b]
      | ConsI {n'} (x, xs) => ConsI ['b] {n'} (f x, map {n'} xs)

(* omit time in return clause *)
val map2 = 
 fn ['a] ['b] {m : Time} (f : 'a -- m --> 'b) =>
    rec (map : forall {n : Nat}, {n} 'a ilist -- (m + 2.0) * $n --> {n} 'b ilist) {n : Nat} (ls : {n} 'a ilist) =>
    case ls return {n} 'b ilist of
        NilI => NilI ['b]
      | ConsI {n'} (x, xs) => ConsI ['b] {n'} (f x, map {n'} xs) |> (m + 2.0) * $n

(* omit return clause *)
val map3 = 
 fn ['a] ['b] {m : Time} (f : 'a -- m --> 'b) =>
    rec (map : forall {n : Nat}, {n} 'a ilist -- (m + 2.0) * $n --> {n} 'b ilist) {n : Nat} (ls : {n} 'a ilist) =>
    case ls of
        NilI => NilI ['b] : {n} 'b ilist
      | ConsI {n'} (x, xs) => ConsI ['b] {n'} (f x, map {n'} xs) : {n} 'b ilist |> (m + 2.0) * $n

val map4 = 
 fn ['a] ['b] {m : Time} (f : 'a -- m --> 'b) =>
    rec (map : forall {n : Nat}, {n} 'a ilist -- (m + 2.0) * $n --> {n} 'b ilist) {n : Nat} (ls : {n} 'a ilist) =>
    case ls return {n} 'b ilist |> (m + 2.0) * $n of
        NilI => NilI ['b]
      | ConsI {n'} (pair as (x, xs as NilI)) => ConsI ['b] {n'} (f x, map {n'} xs)
      | ConsI {n'} (x, xs) => ConsI ['b] {n'} (f x, map {n'} xs)