assignment5.dats

//
// Title:
// Concepts of Programming Languages
// Number: CAS CS 320
// Semester: Spring 2014
// Class Time: TR 12:30-2:00
// Instructor: Hongwei Xi (hwxiATbuDOTedu)
// Teaching Fellow: Hanwen Wu (hwwuATbuDOTedu)
//
(*
//
// Assignment #5
// Due Thursday, February 27, 2014 at 11:59pm
//
*)
(* ****** ****** *)

#define
ATS_PACKNAME "CS320_HW5"

(* ****** ****** *)

#include
"./CS320-2014-Spring.hats"

(* ****** ****** *)

staload "./assignment5.sats"

(* ****** ****** *)

implement
{a}{b}(*tmp*)
list0_foldright
  (xs, f, res) =
(
  case+ xs of
  | nil0 () => res
  | cons0 (x, xs) => f (x, list0_foldright<a><b> (xs, f, res))
)
(* ****** ****** *)

fun{a:t@ype}
list0_length (xs: list0 (a)): int =
  list0_foldright<a><int> (xs, lam (_, res) => res + 1, 0)

(* ****** ****** *)
//
fun
list0_max (xs: list0 (int)): int =
  list0_foldright<int><int> (xs, lam (x, res) => max (x, res), 0)
//
(* ****** ****** *)
// my work


implement
{a}{b} (*tmp*)
tree0_fold
  (xs, f, res) =
(
  case+ xs of
  | tree0_nil () => res
  | tree0_cons (tl, x, tr) => f (tree0_fold<a><b> (tl, f, res), x, tree0_fold<a><b> (tr, f, res))
)

implement
{a}(*tmp*)
tree0_size (t0) = tree0_fold<a><int> (t0, lam (tl, _, tr) => tl + 1 + tr, 0)


implement
{a}
tree0_height (t0) = tree0_fold<a><int> (t0, lam (lh, _, rh) => 1 + max (lh, rh), 0)
(*(tree0_size<a>(tr) <= tree0_size<a> (tl) && tree0_size<a> (tl) <= tree0_size<a> (tr)+1)*)


implement
{a}
brauntree_test (t0) =
 case+ t0 of
  | tree0_nil () => true
  | tree0_cons (tL, x, tR) => (tree0_size(tR) <= tree0_size(tL)) && ( tree0_size(tL) <= (tree0_size(tR) + 1)) 

(* ****** ****** *)

fun {a: t@ype}
list0_getel (xs: list0(a), i: int, c: int): a =
 case+ xs of
  | list0_nil() => ~1
  | list0_cons (x, xs) =>
      if (c = i)
       then x
       else list0_getel<a> (xs, i, c+1)

fun {a: t@ype}
getfront_helper (xs: list0(a), ys: list0(a), i: int, c: int): list0(a) =
 case+ xs of
  | list0_nil() => list0_nil()
  | list0_cons (x, xs) =>
      if (c < i)
       then getfront_helper (xs, list0_cons(x, ys), i, c+1)
       else ys

fun {a: t@ype}
list0_getfront (xs: list0(a)): list0(a) = getfront_helper<a> (xs, list0_nil(), list0_length<a>(xs) / 2, 0)

fun {a:t@ype}
getback_helper (xs: list0(a), i: int, c: int): list0(a) =
 case+ xs of
  | list0_nil() => xs
  | list0_cons(x, xs) when c < i - 1 => getback_helper<a> (xs, i, c+1)
  | list0_cons(x, xs) when c = i - 1 => xs
  | list0_cons(x, xs) => xs


fun {a: t@ype}
list0_getback (xs: list0(a)): list0(a) = getback_helper<a> (xs, list0_length<a> (xs) / 2 + 2, 0)

(* ****** ****** *)

implement {a}
list2brauntree (xs) = let
 val length = list0_length (xs)
 val left = list0_getfront (xs)
 val right = list0_getback (xs)
 val root = if (length mod 2) = 0 then list0_getel (xs, (length/2)+1, 0) else list0_getel (xs, length/2, 0)
in
 case+ xs of
 | list0_nil () => tree0_nil ()
 | list0_cons (x, xs) => tree0_cons (list2brauntree(left), root, list2brauntree(right))
end // end of [list2brauntree]

(* ****** ****** *)

implement
main0 () = () where
{
//
val digits =
  list0_make_intrange (0, 10)
//
val length = list0_length<int> (digits)
val ((*void*)) = assertloc (length = 10)
val ((*void*)) = assertloc (list0_max (digits) = 9)
//
} (* end of [main0] *)

(* ****** ****** *)

(* end of [assignment5.dats] *)