Determine polymoprhic variables in compile

compile/compile.ml

@@ -5,7 +5,7 @@ type env = {
   cu: Compunit.t option;  (* None: toplevel *)
   vars: var_loc Env.t;
   sigma : sigma; (* symbolic substitutions (Lambda.sigma) *)
-  gamma : var_loc Env.t; (* map of type variables to types *)
+  gamma : Types.t Env.t; (* map of type variables to types *)
   stack_size: int;
   max_stack: int ref;
   global_size: int
@@ -58,6 +58,11 @@ let enter_global_cu cu env x =
       vars = Env.add x (Ext (cu,env.global_size)) env.vars;
       global_size = env.global_size + 1 }
 
+let rec domain = function 
+  |`List l -> Types.Tallying.domain l
+  |`Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
+  |`Sel(x,t,s) -> (domain s)
+
 (* from intermediate explicitely typed language to Evaluation language (lambda) *)
 let rec compile env e = compile_aux env e.Typed.exp_descr
 and compile_aux env = function
@@ -68,7 +73,8 @@ and compile_aux env = function
   | Typed.Var x -> Var (find x env)
   | Typed.TVar x ->
       let v = find x env in
-      if env.sigma = (`List []) (* && not (find v dom(env.sigma)) *) then Var (v)
+      let polyvars = Var.Set.inter (domain(env.sigma)) (Types.all_vars(Env.find x env.gamma)) in
+      if Var.Set.is_empty polyvars 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)
@@ -138,11 +144,19 @@ and compile_abstr env a =
   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(a.Typed.fun_fv,a.Typed.fun_iface,env.sigma) in
-  (*
-  if equal (inter (Types.all_vars(Env.find x env.gamma)) dom(env.sigma)) empty then
+  let polyvars =
+    let vs =
+      List.fold_left (fun acc (t1,t2) ->
+        let ts1 = Types.all_vars t1 in
+        let ts2 = Types.all_vars t2 in
+        (Var.Set.union acc (Var.Set.union ts1 ts2))
+      ) Var.Set.empty a.Typed.fun_iface
+    in
+    Var.Set.inter (domain(env.sigma)) vs 
+  in
+  if Var.Set.is_empty polyvars then
     Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma)
   else 
-    *)
     Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma)
 
 and compile_branches env (brs : Typed.branches) =

types/types.ml

@@ -2993,6 +2993,13 @@ module Tallying = struct
     Format.printf "Unify : %a\n" CS.ES.print el;
     List.map (CS.E.bindings) (CS.ES.elements el)
 
+  let domain ll = 
+    List.fold_left (fun acc l ->
+      List.fold_left (fun acc (v,_) ->
+        Var.Set.add v acc
+      ) acc l
+    ) Var.Set.empty ll
+
 end
 
 exception KeepGoing

types/types.mli

@@ -138,6 +138,7 @@ val abstract : Abstract.t -> t
 
 (** Helpers *)
 
+val all_vars : t -> Var.Set.t
 val tuple : Node.t list -> t
 
 val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
@@ -145,10 +146,6 @@ val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
 val empty_closed_record: t
 val empty_open_record: t
 
-(*
-val subst : t -> Var.var * t -> t
-*)
-
 (** Positive systems and least solutions **)
 
 module Positive :
@@ -406,6 +403,7 @@ module Tallying : sig
   val solve : CS.s -> CS.es
   val unify : CS.e -> CS.e
   val tallying : (t * t) list -> CS.sl
+  val domain : CS.sl -> Var.Set.t
 
 end
 

types/var.ml

@@ -54,6 +54,8 @@ module Set = struct
 
   let dump ppf s = aux_print ";" dump ppf s
   let print ppf s = aux_print ";" print ppf 
+  let is_empty s = equal s empty
+  let from_list l = List.fold_left (fun acc x -> add x acc) empty l
 end
 
 module Make (X : Custom.T) = struct