Same here, partial code from stackcodegen.ml in the said archive :<p>open Op;;
open Var;;
open Ctx;;
open Ltal;;
open Util;;<p>let debug msg = ();;<p>let rs = mkvar "rs";;
let ra = mkvar "ra";;
let rf = mkvar "rf";;
let rt = mkvar "rt";;
let rr = mkvar "rr";;
let ru = mkvar "ru";;<p>let retty stackty aty = (Code(Ctx.from_list[(rs,stackty);
(ra,aty);
(rt,toptp);
(rf,listtp);
(rr,toptp)]))<p>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 <i>)
| 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)<p>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'))]))<p><pre><code> | _ -> tcfail "expected a function type in forall"
</code></pre>
let typetrans tctx tp = tt tctx Ctx.emp tp
let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))<p>(</i> Need to specify the type ty of "the rest of the stack", in most cases
alpha <i>)<p>type code_env = {cctx : cctx;
cs : code_section;
fctx : Il.ctx;
lctx : var Ctx.ctx;
fp : int}<p>let get_fctx cenv = cenv.fctx
let get_lctx cenv = cenv.lctx<p>type block_env = {cenv : code_env;
ilist : instruction list;
lab : clab;
tctx : Ltal.tctx;
rctx : Ltal.rctx}<p>let get_from_cenv f benv = f benv.cenv<p>exception CodeFail of string </i> code_env
exception BlockFail of string * block_env<p>(*
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
<i>)<p>let do_print y x = (debug y; x)<p>let (>>) f g x = g(f(x))
let (>>=) f h x = let y = f x in h y x<p>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))<p>let current_ltp benv =
debug ("Generalizing "^(Ctx.pp_ctx (fun _ -> "") benv.tctx)^"\n");
(</i> rt is caller-save *)
let rctx = update benv.rctx rt toptp in
(mkltp benv.tctx rctx)