GADT example in ATS2

gadt.dats

(*
  $ patscc -o gadt gadt.dats
  $ ./gadt
  res1=true and res2=8
*)
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

datatype Expr (t@ype) =
  | I(int) of int
  | B(bool) of bool
  | Add(int) of (Expr(int), Expr(int))
  | Mul(int) of (Expr(int), Expr(int))
  | Eq(bool) of (Expr(int), Expr(int))

fun{a:t@ype} eval (x:Expr(a)): a =
  case+ x of
  | I i => i
  | B b => b
  | Add (t1, t2) => eval(t1) + eval(t2)
  | Mul (t1, t2) => eval(t1) * eval(t2)
  | Eq (t1, t2) => eval(t1) = eval(t2)


implement main0() = let
  val term1 = Eq(I(5), Add(I(1), I(4)))
  val term2 = Mul(I(2), I(4))
  val res1 = eval(term1)
  val res2 = eval(term2)
in
  println!("res1=", res1, " and res2=", res2)
end