F tuple

datatype opr = Sub | Add | Mul | Leq
     and ty = Arrow of ty * ty | Bool | Int | Star of ty list
     and con = IC of int | False | True
     and exp = Abs of string * ty * exp | If of exp * exp * exp | Opr of opr * exp * exp | App of exp * exp | Var of string | Con of con | Tuple of exp list | Proj of int * exp;
exception Error of string;
val nth = List.nth;
fun update env k v l = if k=l then v else env l;
fun map f nil = nil
  | map f (x::xr) = f x::map f xr;
fun elabCon (IC x) = Int
  | elabCon True = Bool
  | elabCon False = Bool;
fun elabOpr Add Int Int = Int
  | elabOpr Sub Int Int = Int
  | elabOpr Mul Int Int = Int
  | elabOpr Leq Int Int = Bool
  | elabOpr _ _ _ = raise Error "T Opr";
fun elab env (Con c) = elabCon c
  | elab env (Var v) = env v
  | elab env (Opr (pr,e1,e2)) = elabOpr pr (elab env e1) (elab env e2)
  | elab env (If (i,t,e)) = (case (elab env i, elab env t, elab env e) of
                               (Bool, t, t') => if t=t' then t else raise Error "T If1"
                             | _ => raise Error "T If2")
  | elab env (Abs (x,t,e)) = Arrow(t,elab (update env x t) e)
  | elab env (App (f,v)) = (case (elab env f, elab env v) of
                              (Arrow(ta,ts), ta') => if ta=ta' then ts else raise Error "T App1"
                            | _ => raise Error "T App2")
  | elab env (Tuple el) = Star (foldr (fn (x,a)=>elab env x :: a) nil el)
  | elab env (Tuple el) = Star (map (elab env) el)
  | elab env (Proj (i,e)) = (case elab env e of
                               Star tl => (nth (tl,i-1) handle Subscript => raise Error "T Proj1")
                             | _ => raise Error "T Proj2");

datatype value = IV of int | ProcV of string*(string->value)*exp | TupleV of value list;
fun evalCon (IC x) = IV x
  | evalCon True = IV 1
  | evalCon False = IV 0
fun evalOpr Add (IV x) (IV y) = IV (x+y)
  | evalOpr Sub (IV x) (IV y) = IV (x-y)
  | evalOpr Mul (IV x) (IV y) = IV (x*y)
  | evalOpr Leq (IV x) (IV y) = IV (if x<=y then 1 else 0)
  | evalOpr _ _ _ = raise Error "R Opr"
fun eval env (Con c) = evalCon c
  | eval env (Var v) = env v
  | eval env (Opr(pr,e1,e2)) = evalOpr pr (eval env e1) (eval env e2)
  | eval env (If(i,t,e)) = (case eval env i of
                              IV 0 => eval env e
                            | IV 1 => eval env t
                            | _ => raise Error "R If")
  | eval env (Abs(x,_,e)) = ProcV(x,env,e)
  | eval env (App(f,v)) = (case eval env f of
                             ProcV(x,env',e) => eval (update env' x (eval env v)) e
                           | _ => raise Error "R App")
  | eval env (Tuple es) = TupleV (foldl (fn (x,a) => a@[eval env x]) nil es)
  | eval env (Tuple es) = TupleV (map (eval env) es)
  | eval env (Proj (i,e)) = (case eval env e of
                               TupleV tv => (nth (tv,i-1) handle Subscript => raise Error "R Proj1")
                             |  _ => raise Error "R Proj2");
exception Unbound of string;
fun empty k = raise Unbound k;
fun elabeval k = let
                   val ty = elab empty k
                   val res = eval empty k
                 in print(ty,res) end;
val max_cart = Abs("p",Star[Int,Int],If(Opr(Leq,Proj(1,Var "p"),Proj(2,Var "p")),Proj(2,Var "p"),Proj(1,Var "p")));
elabeval max_cart;
elabeval (App(max_cart,Tuple[Con(IC 3), Con(IC 1)]));
elabeval (Tuple[Con True, Con (IC 5), Abs("x", Int, Opr(Leq,Var "x", Con (IC 5)))]);