Same here, partial code from stackcodegen.ml in the said archive :
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"
let typetrans tctx tp = tt tctx Ctx.emp tp
let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))
( 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
I think a challenge to me for typing assembly, unless you’re doing old-school C style minimally-useful types, is that assembly types tend to be both more ad hoc and more transient than types in higher level languages, because these types come from the intersection of the problem domain and the way of expressing the solution, instead of just from the problem domain. In C++ I might have a type for “aircraft velocity in mm/s”, but in assembly I might have that type on one line, and then go to velocity in 2x mm/s the next line to save a renormalization; or have types for various state flags, but have them pack differently into a word in different places in the code. This is all expressible, but I think it would make me favor a more implicit typing with a heavier emphasis on deduction, just to minimize the description of types that exist but are not in themselves interesting.
If you're gonna make a website for your programming language, you NEED to put an example of the language front and center on the landing page.
Three links deep and I finally found some code... packaged in a gz archive. I still have not seen a line of TAL
Same here, partial code from stackcodegen.ml in the said archive :
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'))]))
let typetrans tctx tp = tt tctx Ctx.emp tp let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))( 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)
I think a challenge to me for typing assembly, unless you’re doing old-school C style minimally-useful types, is that assembly types tend to be both more ad hoc and more transient than types in higher level languages, because these types come from the intersection of the problem domain and the way of expressing the solution, instead of just from the problem domain. In C++ I might have a type for “aircraft velocity in mm/s”, but in assembly I might have that type on one line, and then go to velocity in 2x mm/s the next line to save a renormalization; or have types for various state flags, but have them pack differently into a word in different places in the code. This is all expressible, but I think it would make me favor a more implicit typing with a heavier emphasis on deduction, just to minimize the description of types that exist but are not in themselves interesting.