Commit 0f0b52ec authored by Pietro Abate's avatar Pietro Abate
Browse files

WIP

parent 83714ed6
......@@ -4,7 +4,7 @@ open Lambda
type env = {
cu: Compunit.t option; (* None: toplevel *)
vars: var_loc Env.t;
sigma : sigma; (* symbolic substitutions sets Lambda.sigma *)
sigma : sigma; (* symbolic substitutions (Lambda.sigma) *)
gamma : var_loc Env.t; (* map of type variables to types *)
stack_size: int;
max_stack: int ref;
......@@ -13,7 +13,15 @@ type env = {
let global_size env = env.global_size
let mk cu = { cu = cu; vars = Env.empty; stack_size = 0; max_stack = ref 0; global_size = 0 }
let mk cu = {
cu = cu;
vars = Env.empty;
sigma = `List [];
gamma = Env.empty;
stack_size = 0;
max_stack = ref 0;
global_size = 0
}
let empty_toplevel = mk None
let empty x = mk (Some x)
......@@ -60,9 +68,9 @@ and compile_aux env = function
| Typed.Var x -> Var (find x env)
| Typed.TVar x ->
let v = find x env in
if env.sigma = [[]] && not (find v dom(env.sigma)) then Var (v)
else TVar(x,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = Comp(env.sigma,List sl) } e
if env.sigma = (`List []) (* && not (find v dom(env.sigma)) *) then Var (v)
else TVar(v,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = `Comp(env.sigma,`List sl) } e
| Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
| Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
| Typed.Abstraction a -> compile_abstr env a
......@@ -129,7 +137,7 @@ and compile_abstr env a =
let slots = Array.of_list (List.rev slots) in
let env = { env with vars = fun_env; stack_size = 0; max_stack = ref 0 } in
let body = compile_branches env a.Typed.fun_body in
let sigma = Sel (x,t,env.sigma) in
let sigma = (* `Sel (x,t,env.sigma) *) `List [] in
if equal (inter vars(t) dom(env.sigma)) empty then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma)
else
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment