This was obviously someone's research project, and some of the papers have example code in them, e.g. see https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf.

open Op;; open Var;; open Ctx;; open Ltal;; open Util;;

let debug msg = ();;

let rs = mkvar "rs";; let ra = mkvar "ra";; let rf = mkvar "rf";; let rt = mkvar "rt";; let rr = mkvar "rr";; let ru = mkvar "ru";;

let retty stackty aty = (Code(Ctx.from_list[(rs,stackty); (ra,aty); (rt,toptp); (rf,listtp); (rr,toptp)]))

let rec tt tctx ctx tp = match tp with Il.TVar a -> if bound tctx a then TVar a else lookup ctx a | Il.Int -> DTp Word | Il.Top -> DTp Top (* for now ) | Il.Tensor(t1,t2) -> Ref(Tcltal.mkpair (tt tctx ctx t1, tt tctx ctx t2)) | Il.Exists (alpha, tp) -> let beta = rename alpha in Exists (beta, W, tt tctx (extend ctx alpha (TVar beta)) tp) | Il.List t -> let tv = mkvar "list" in Mu(tv,NRef(Tcltal.mkpair(tt tctx ctx t, TVar tv))) | _ -> DTp(arrowtt tctx ctx tp)

and arrowtt tctx ctx t = match t with Il.Forall(alpha,t) -> let beta = Var.rename alpha in Forall(beta, W, arrowtt tctx (extend ctx alpha (TVar beta)) t) | Il.Arrow(t1,t2) -> let t1' = tt tctx ctx t1 in let t2' = tt tctx ctx t2 in let stk = mkvar "s" in Forall (stk,M, Code(Ctx.from_list[(rs,Stack(Tensor(t1',MTVar stk))); (ra,toptp); (rt,toptp); (rf,listtp); (rr,DTp(retty (Stack(MTVar stk)) t2'))]))

  | _ -> tcfail "expected a function type in forall"

( Need to specify the type ty of "the rest of the stack", in most cases alpha )

type code_env = {cctx : cctx; cs : code_section; fctx : Il.ctx; lctx : var Ctx.ctx; fp : int}

let get_fctx cenv = cenv.fctx let get_lctx cenv = cenv.lctx

type block_env = {cenv : code_env; ilist : instruction list; lab : clab; tctx : Ltal.tctx; rctx : Ltal.rctx}

let get_from_cenv f benv = f benv.cenv

exception CodeFail of string code_env exception BlockFail of string * block_env

(* val begin_fn : code_env -> clab -> register_file -> block_env val end_fn : block_env -> code_env val emit_label : fn_env -> clab -> dtp -> block_env val emit : block_env -> instruction -> block_env -> block_env val emit_end : end_instruction -> block_env -> fn_env val drop : reg -> block_env -> block_env val free : reg -> block_env -> block_env val push : reg -> reg -> block_env -> block_env val pop : reg -> reg -> block_env -> block_env val malloc : reg -> block_env -> block_env )

let do_print y x = (debug y; x)

let (>>) f g x = g(f(x)) let (>>=) f h x = let y = f x in h y x

let rec mkltp tctx rctx = Ctx.fold (fun t sk dtp -> let k = match sk with _,W -> W | _,M -> M in Forall(t,k,dtp)) tctx (Code (rctx))

let current_ltp benv = debug ("Generalizing "^(Ctx.pp_ctx (fun _ -> "") benv.tctx)^"\n"); ( rt is caller-save *) let rctx = update benv.rctx rt toptp in (mkltp benv.tctx rctx)

Did you consider the possibility that this sort of thing was done to avoid wasting time with non-experts who think an "example" of a language they don't know is enough to make comments about?

> I still have not seen a line of TAL

My suggestion: Start with the "Papers" and then look at the paper that introduces TAL. It has an example program with analysis

Your "feelings" may help you make snap judgements that can keep you alive, but they cannot help you code and they will conspire against you when you effort to learn new things. Nobody wants to feel wrong, and you will feel wrong many times when you learn something new, but it is the only way to actually learn the thing. Remember this the next time you have "feelings" about knowledge