WIP

compile/compile.ml

@@ -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