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

Fix problem with monomorphic variable detection

parent ec4c848f
...@@ -122,14 +122,14 @@ and compile_aux env = function ...@@ -122,14 +122,14 @@ and compile_aux env = function
| Typed.TVar x -> | Typed.TVar x ->
let v = find x env in let v = find x env in
let ts = Types.all_vars (Types.descr (IdMap.assoc x env.gamma)) in let ts = Types.all_vars (Types.descr (IdMap.assoc x env.gamma)) in
let is_mono () = let is_mono x =
let from_xi = try IdMap.assoc x env.xi with Not_found -> assert false in let from_xi = try IdMap.assoc x env.xi with Not_found -> Var.Set.empty in
let d = Var.Set.inter from_xi (domain(env.sigma)) in let d = Var.Set.inter from_xi (domain(env.sigma)) in
Var.Set.is_empty (Var.Set.inter ts d) Var.Set.is_empty (Var.Set.inter ts d)
in in
if Var.Set.is_empty ts then Var (v) else if Var.Set.is_empty ts then Var (v) else
if env.sigma = Identity then TVar(v,env.sigma) else if env.sigma = Identity then TVar(v,env.sigma) else
if is_mono () then Var (v) else TVar(v,env.sigma) if is_mono x then Var (v) else TVar(v,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = comp env.sigma (List sl) } e | Typed.Subst(e,sl) -> compile { env with sigma = comp env.sigma (List sl) } e
| Typed.ExtVar (cu,x,_) -> Var (find_ext cu x) | Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
| Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2) | Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
......
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