<commit_before>(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(* <NAME> and <NAME>, projet Cristal, INRIA Rocquencourt*)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  Automatique.  Distributed only by permission.                      *)
(*                                                                     *)
(***********************************************************************)

(* $Id$ *)

(* Operations on core types *)

open Misc
open Asttypes
open Types

exception Unify of (type_expr * type_expr) list
exception Subtype of
        (type_expr * type_expr) list * (type_expr * type_expr) list

let current_level = ref 0
let global_level = ref 1
let generic_level = (-1)

let init_def level = current_level := level
let begin_def () = incr current_level
let end_def () = decr current_level

let reset_global_level () =
  global_level := !current_level + 1

let newty desc         = { desc = desc; level = !current_level }
let new_global_ty desc = { desc = desc; level = !global_level }
let newgenty desc      = { desc = desc; level = generic_level }
let newvar ()          = { desc = Tvar; level = !current_level }
let new_global_var ()  = new_global_ty Tvar
let new_gen_var ()     = newgenty Tvar
let newobj fields      = newty (Tobject (fields, ref None))

let rec repr = function
    {desc = Tlink t'} as t ->
      let r = repr t' in
      if r != t' then t.desc <- Tlink r;
      r
  | t -> t

let rec repr2 = function                (* No path compression *)
                                        (* during unification *)
    {desc = Tlink ty} ->
      repr2 ty
  | t -> t

let none = newty (Ttuple [])                (* Clearly ill-formed type *)

(* --- *)

let flatten_fields ty =
  let rec flatten l ty =
    let ty = repr ty in
    match ty.desc with
      Tfield(s, ty1, ty2) ->
        flatten ((s, ty1)::l) ty2
    | Tvar | Tnil ->
        (l, ty)
    | _ ->
      fatal_error "Ctype.flatten_fields"
  in
    let (l, r) = flatten [] ty in
      (List.rev l, r)

let build_fields =
  List.fold_right
    (fun (s, ty1) ty2 ->
       {desc = Tfield(s, ty1, ty2);
        level = ty2.level})

let associate_fields fields1 fields2 =
  let rec associate p s s' =
    function
      (l, []) ->
        (List.rev p, (List.rev s) @ l, List.rev s')
    | ([], l') ->
        (List.rev p, List.rev s, (List.rev s') @ l')
    | (((n, t)::r as l), ((n', t')::r' as l')) ->
        if n = n' then
          associate ((t, t')::p) s s' (r, r')
        else if n < n' then
          associate p ((n, t)::s) s' (r, l')
        else
          associate p s ((n', t')::s') (l, r')
  in let sort = Sort.list (fun (n, _) (n', _) -> n < n') in
  associate [] [] [] (sort fields1, sort fields2)

(* Check whether an object is open *)

let rec opened ty =
  match (repr ty).desc with
    Tfield(_, _, t) -> opened t
  | Tvar            -> true
  | Tnil            -> false
  | _               -> fatal_error "Ctype.opened"

let opened_object ty =
  match (repr ty).desc with
    Tobject (ty', _)  -> opened ty'
  | Tconstr (_, _, _) -> false
  | _                 -> fatal_error "Ctype.opened_object"

(* Type generalization *)

let rec generalize ty =
  let ty = repr ty in
  if ty.level > !current_level then begin
    ty.level <- generic_level;
    match ty.desc with
      Tvar               -> ()
    | Tarrow(t1, t2)     -> generalize t1; generalize t2
    | Ttuple tl          -> List.iter generalize tl
    | Tconstr(_, tl, ab) -> ab := []; List.iter generalize tl
    | Tobject(f, {contents = Some (_, p)})
                         -> generalize f; List.iter generalize p
    | Tobject(f, _)      -> generalize f
    | Tfield(_, t1, t2)  -> generalize t1; generalize t2
    | Tnil               -> ()
    | Tlink _            -> fatal_error "Ctype.generalize"
  end

let rec make_nongen ty =
  let ty = repr ty in
  if ty.level > !current_level then begin
    ty.level <- !current_level;
    match ty.desc with
      Tvar              -> ()
    | Tarrow(t1, t2)    ->  make_nongen t1; make_nongen t2
    | Ttuple tl         -> List.iter make_nongen tl
    | Tconstr(p, tl, _) -> List.iter make_nongen tl
    | Tobject(f, {contents = Some (_, p)})
                        -> make_nongen f; List.iter make_nongen p
    | Tobject(f, _)      -> make_nongen f
    | Tfield(_, t1, t2) -> make_nongen t1; make_nongen t2
    | Tnil              -> ()
    | Tlink _           -> fatal_error "Ctype.make_nongen"
  end

(* Remove abbreviations from generalized types *)

let visited = ref ([] : type_expr list)

let remove_abbrev ty =
  let rec remove ty =
    let ty = repr ty in
    if ty.level = generic_level & not (List.memq ty !visited) then begin
      visited := ty :: !visited;
      match ty.desc with
        Tvar               -> ()
      | Tarrow(t1, t2)     -> remove t1; remove t2
      | Ttuple tl          -> List.iter remove tl
      | Tconstr(_, tl, ab) -> ab := []; List.iter remove tl
      | Tobject(f, {contents = Some (_, p)})
                           -> remove f; List.iter remove p
      | Tobject(f, _)      -> remove f
      | Tfield(_, t1, t2)  -> remove t1; remove t2
      | Tnil               -> ()
      | Tlink _            -> fatal_error "Ctype.remove_abbrev"
      end
  in
    visited := []; remove ty; visited := []


(* Taking instances of type schemes *)

type 'a visited = Zero | One | Many of 'a

let inst_subst = ref ([] : (type_expr * type_expr) list)

let rec copy_rec abbrev visited ty =
  let ty = repr ty in
  if ty.level <> generic_level then ty else
  try
    match List.assq ty visited with
      {contents = Zero} as v ->
      	let t = newvar () in
	v := Many t;
	let ty' = copy_rec_2 abbrev visited ty v in
	t.desc <- ty'.desc;
	t
    | {contents = One} as v ->
        let t = newvar () in
        v := Many t;
        t
    | {contents = Many t} ->
        t
  with Not_found ->
    let v = ref One in
    let ty' = copy_rec_2 abbrev ((ty, v)::visited) ty v in
    match v with
      {contents = Many t} ->
      	t.desc <- ty'.desc;
	t
    | _ ->
      	ty'

and copy_rec_2 abbrev visited ty v =
  match ty.desc with
    Tvar ->
      begin try List.assq ty !inst_subst with Not_found ->
        let ty' = newvar () in
        inst_subst := (ty, ty') :: !inst_subst;
        ty'
      end
  | Tarrow (t1, t2) ->
      newty (Tarrow (copy_rec abbrev visited t1,
                     copy_rec abbrev visited t2))
  | Ttuple tl ->
      newty (Ttuple (List.map (copy_rec abbrev visited) tl))
  | Tconstr (p, [], _) ->
      newty (Tconstr (p, [], ref abbrev))
  | Tconstr (p, tl, _) ->
      newty (Tconstr (p, List.map (copy_rec abbrev visited) tl,
                      ref abbrev))
  | Tobject (t1, {contents = name}) ->
      let ty' () =
        let name' =
          match name with
            None ->
              None
          | Some (p, tl) ->
              Some (p, List.map (copy_rec abbrev visited) tl)
        in
          newty (Tobject (copy_rec abbrev visited t1, ref name'))
      in
      if opened_object ty then
        try
          List.assq ty !inst_subst
        with Not_found ->
          if v = ref One then begin
            let t = newvar () in
    	    v := Many t;
            inst_subst := (ty, t):: !inst_subst
          end;
          ty' ()
      else
        ty' ()
  | Tfield (label, t1, t2) ->
      newty (Tfield (label, copy_rec abbrev visited t1,
                            copy_rec abbrev visited t2))
  | Tnil ->
      newty Tnil
  | Tlink _ ->
      fatal_error "Ctype.copy_rec"

let copy ty = copy_rec [] [] ty
let subst abbrev ty = copy_rec abbrev [] ty
let copy_parameterized params ty = copy_rec [] params ty

let instance sch =
  inst_subst := [];
  let ty = copy sch in
  inst_subst := [];
  ty

let instance_constructor cstr =
  inst_subst := [];
  let ty_res = copy cstr.cstr_res in
  let ty_args = List.map copy cstr.cstr_args in
  inst_subst := [];
  (ty_args, ty_res)

let instance_label lbl =
  inst_subst := [];
  let ty_res = copy lbl.lbl_res in
  let ty_arg = copy lbl.lbl_arg in
  inst_subst := [];
  (ty_arg, ty_res)

let substitute abbrev params args body =
  inst_subst := List.combine params args;
  let ty = subst abbrev body in
  inst_subst := [];
  ty

let instance_parameterized_type sch_args sch =
  inst_subst := [];
  let params = List.map (function p -> (repr p, ref Zero)) sch_args in
  let ty_args = List.map (copy_parameterized params) sch_args in
  let ty = copy_parameterized params sch in
  inst_subst := [];
  (ty_args, ty)

let instance_parameterized_type_2 sch_args sch_lst sch =
  inst_subst := [];
  let params = List.map (function p -> (repr p, ref Zero)) sch_args in
  let ty_args = List.map (copy_parameterized params) sch_args in
  let ty_lst = List.map (copy_parameterized params) sch_lst in
  let ty = copy_parameterized params sch in
  inst_subst := [];
  (ty_args, ty_lst, ty)

let instance_class cl =
  inst_subst := [];
  let params0 = List.map (function p -> (repr p, ref Zero)) cl.cty_params in
  let params = List.map (copy_parameterized params0) cl.cty_params in
  let args = List.map (copy_parameterized params0) cl.cty_args in
  let vars =
    Vars.fold
      (fun lab (mut, ty) ->
         Vars.add lab (mut, copy_parameterized params0 ty))
      cl.cty_vars
      Vars.empty in
  let self = copy_parameterized params0 cl.cty_self in
  inst_subst := [];
  (params, args, vars, self)

(* Unification *)

let rec update_level level ty =
  let ty = repr2 ty in
  if ty.level > level then begin
    ty.level <- level;
    match ty.desc with
      Tvar               -> ()
    | Tarrow(t1,t2)      -> update_level level t1; update_level level t2
    | Ttuple(ty_list)    -> List.iter (update_level level) ty_list
    | Tconstr(_, tl, _)  -> List.iter (update_level level) tl
    | Tobject(f, {contents = Some (_, p)})
                         -> update_level level f;
                            List.iter (update_level level) p
    | Tobject (f, _)     -> update_level level f
    | Tfield(_, t1, t2)  -> update_level level t1; update_level level t2
    | Tnil               -> ()
    | Tlink _            -> fatal_error "Ctype.update_level"
  end

exception Cannot_expand

let rec find_expans p1 =
  function
    [] ->
      None
  | (p2, ty)::l ->
      if Path.same p1 p2 then
        Some ty
      else
        find_expans p1 l

let expand_abbrev env path args abbrev level =
  match find_expans path !abbrev with
    Some ty ->
      update_level level ty;
      ty
  | None ->
      let decl =
        try Env.find_type path env with Not_found -> raise Cannot_expand in
      match decl.type_manifest with
        Some body ->
          let v = newvar () in
          abbrev := (path, v)::!abbrev;
          let old_level = !current_level in
          current_level := level;
          let ty = substitute !abbrev decl.type_params args body in
          current_level := old_level;
          v.desc <- Tlink ty;
          ty
      | _ ->
          raise Cannot_expand

let rec expand_root env ty =
  let ty = repr ty in
  match ty.desc with
    Tconstr(p, tl, abbrev) ->
      begin try
        expand_root env (expand_abbrev env p tl (ref !abbrev) ty.level)
      with Cannot_expand ->
        ty
      end
  | _ ->
      ty

let rec full_expand env ty =
  let ty = repr (expand_root env ty) in
  match ty.desc with
    Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
      { desc = Tobject (fi, ref None); level = ty.level }
  | _ ->
      ty

let generic_abbrev env path =
  try
    let decl = Env.find_type path env in
    match decl.type_manifest with
      Some body ->
        body.level = generic_level
    | _ ->
        false
  with
    Not_found ->
      false

let occur env ty0 ty =
  let visited = ref ([] : type_expr list) in
  let rec occur_rec ty =
    let ty = repr ty in
    if ty == ty0 then raise (Unify []);
    match ty.desc with
      Tvar ->
        ()
    | Tarrow(t1, t2) ->
        occur_rec t1; occur_rec t2
    | Ttuple tl ->
        List.iter occur_rec tl
    | Tconstr(p, [], abbrev) ->
        if ty0.level < Path.binding_time p then begin
          let ty' =
            try expand_abbrev env p [] abbrev ty.level
            with Cannot_expand -> raise (Unify []) in
          occur_rec ty'
        end
    | Tconstr(p, tl, abbrev) ->
        if not (List.memq ty !visited) then begin
          visited := ty :: !visited;
          try
            if ty0.level < Path.binding_time p then raise(Unify []);
            List.iter occur_rec tl
          with Unify lst ->
            let ty' =
              try expand_abbrev env p tl abbrev ty.level
              with Cannot_expand -> raise (Unify lst) in
            occur_rec ty'
        end
    | Tobject (_, _) ->
        ()
    | _ (* Tfield (_, _, _) | Tnil | Tlink _ *) ->
        fatal_error "Ctype.occur"
  in
    occur_rec ty

let rec unify_rec env a1 a2 t1 t2 =     (* Variables and abbreviations *)
  if t1 == t2 then () else
  let t1 = repr2 t1 in
  let t2 = repr2 t2 in
  if t1 == t2 then () else
  try
    match (t1.desc, t2.desc) with
      (Tvar, _) ->
         update_level t1.level t2;
         begin match a2 with
           None    -> occur env t1 t2; t1.desc <- Tlink t2
         | Some l2 -> occur env t1 l2; t1.desc <- Tlink l2
         end
    | (_, Tvar) ->
         update_level t2.level t1;
         begin match a1 with
           None    -> occur env t2 t1; t2.desc <- Tlink t1
         | Some l1 -> occur env t2 l1; t2.desc <- Tlink l1
         end
    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
         unify_core env a1 a2 t1 t2
    | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) ->
        begin
          try
            let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
            update_level t2.level t1;
            unify_rec env (Some t1) a2 t3 t2
          with Cannot_expand ->
          try
            let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
            update_level t1.level t2;
            unify_rec env a1 (Some t2) t1 t3
          with Cannot_expand ->
            raise (Unify [])
        end
    | (Tconstr (p1, tl1, abbrev1), _) ->
        begin try
          let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
          update_level t2.level t1;
          unify_rec env (Some t1) a2 t3 t2
        with Cannot_expand ->
          unify_core env a1 a2 t1 t2
        end
    | (_, Tconstr (p2, tl2, abbrev2)) ->
        begin try
          let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
          update_level t1.level t2;
          unify_rec env a1 (Some t2) t1 t3
        with Cannot_expand ->
          unify_core env a1 a2 t1 t2
        end
    | (_, _) ->
        unify_core env a1 a2 t1 t2
  with
    Unify [] ->
      raise (Unify [(t1, t2)])
  | Unify (_::l) ->
      raise (Unify ((t1, t2)::l))

and unify_core env a1 a2 t1 t2 =        (* Other cases *)
  let d1 = t1.desc and d2 = t2.desc in
  begin match (a1, a2) with
    (None,    Some l2) ->
      update_level t1.level t2; t1.desc <- Tlink l2
  | (Some l1, None) ->
      update_level t2.level t1; t2.desc <- Tlink l1
  | (_, _) ->
      update_level t1.level t2; occur env t1 t2; t1.desc <- Tlink t2
  end;
  try
    match (d1, d2) with
      (Tarrow (t1, u1), Tarrow (t2, u2)) ->
        unify_rec env None None t1 t2; unify_rec env None None u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        unify_list env tl1 tl2
    | (Tconstr (p1, [], _), Tconstr (p2, [], _)) (*when Path.same p1 p2*) ->
        ()
    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) (*when Path.same p1 p2*) ->
        unify_list env tl1 tl2
    | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
        unify_fields env fi1 fi2;
        begin match !nm2 with
          Some (_, va::_) when (repr va).desc = Tvar -> ()
        | _                                          -> nm2 := !nm1
        end
    | (_, _) ->
        raise (Unify [])
  with
    Unify l ->
      t1.desc <- d1;
      t2.desc <- d2;
      raise (Unify ((t1, t2)::l))
  | exn ->
      t1.desc <- d1;
      t2.desc <- d2;
      raise exn

and unify_list env tl1 tl2 =
  if List.length tl1 <> List.length tl2 then
    raise (Unify []);
  List.iter2 (unify_rec env None None) tl1 tl2

and unify_fields env ty1 ty2 =
  let (fields1, rest1) = flatten_fields ty1
  and (fields2, rest2) = flatten_fields ty2 in
  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
  let va = newvar () in
    begin match rest1.desc with
      Tvar ->
        let nr = build_fields miss2 va in
        update_level rest1.level nr;
        rest1.desc <- Tlink nr
    | Tnil ->
        if miss2 <> [] then raise (Unify []);
        va.desc <- Tlink {desc = Tnil; level = va.level}
    | _ ->
        fatal_error "Ctype.unify_fields (1)"
    end;
    begin match rest2.desc with
      Tvar ->
        let nr = build_fields miss1 va in
        update_level rest2.level nr;
        rest2.desc <- Tlink nr
    | Tnil ->
        if miss1 <> [] then raise (Unify []);
        va.desc <- Tlink {desc = Tnil; level = va.level}
    | _ ->
        fatal_error "Ctype.unify_fields (2)"
    end;
    List.iter (fun (t1, t2) -> unify_rec env None None t1 t2) pairs

let expand_trace env trace =
  List.fold_right
    (fun (t1, t2) rem ->
       (t1, full_expand env t1)::(t2, full_expand env t2)::rem)
    trace []

let rec filter_trace =
  function
    (t1, t1')::(t2, t2')::rem ->
      let rem' = filter_trace rem in
      if (t1 == t1') & (t2 == t2') then
        rem'
      else
        (t1, t1')::(t2, t2')::rem
  | _ ->
      []

let unify env ty1 ty2 =
  try
    unify_rec env None None ty1 ty2
  with Unify trace ->
    let trace = expand_trace env trace in
    match trace with
      t1::t2::rem ->
        raise (Unify (t1::t2::filter_trace rem))
    | _ ->
        fatal_error "Ctype.unify"

let rec filter_arrow env t =
  let t = repr t in
  match t.desc with
    Tvar ->
      let t1 = newvar () and t2 = newvar () in
      let t' = newty (Tarrow (t1, t2)) in
      update_level t.level t';
      t.desc <- Tlink t';
      (t1, t2)
  | Tarrow(t1, t2) ->
      (t1, t2)
  | Tconstr(p, tl, abbrev) ->
      begin try
        filter_arrow env (expand_abbrev env p tl abbrev t.level)
      with Cannot_expand ->
        raise (Unify [])
      end
  | _ ->
      raise (Unify [])

let rec filter_method_field name ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      let ty1 = newvar () and ty2 = newvar () in
      let ty' = newty (Tfield (name, ty1, ty2)) in
      update_level ty.level ty';
      ty.desc <- Tlink ty';
      ty1
  | Tfield(n, ty1, ty2) ->
      if n = name then
        ty1
      else
        filter_method_field name ty2
  | _ ->
      raise (Unify [])

let rec filter_method env name ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      let ty1 = newvar ()in
      let ty' = newobj ty1 in
      update_level ty.level ty';
      ty.desc <- Tlink ty';
      filter_method_field name ty1
  | Tobject(f, _) ->
      filter_method_field name f
  | Tconstr(p, tl, abbrev) ->
      begin try
        filter_method env name (expand_abbrev env p tl abbrev ty.level)
      with Cannot_expand ->
        raise (Unify [])
      end
  | _ ->
      raise (Unify [])

(* Matching between type schemes *)

let moregen_occur env ty0 ty =
  let visited = ref [] in
  let rec occur_rec ty =
    let ty = repr ty in
    match ty.desc with
      Tvar ->
        (* ty0 has level = !current_level iff it is generic
           in the original type scheme. In this case, it can be freely
           instantiated. Otherwise, ty0 is not generic
           and cannot be instantiated by a type that contains
           generic variables. *)
        if ty.level = generic_level & ty0.level < !current_level
        then raise (Unify [])
    | Tarrow(t1, t2) ->
        occur_rec t1; occur_rec t2
    | Ttuple tl ->
        List.iter occur_rec tl
    | Tconstr(p, tl, abbrev) ->
        if not (List.memq ty !visited) then begin
          visited := ty::!visited;
          try
            List.iter occur_rec tl
          with Unify lst ->
            let ty' =
              try expand_abbrev env p tl abbrev ty.level
              with Cannot_expand -> raise (Unify lst) in
            occur_rec ty'
        end
    | Tobject(f, _) ->
        if not (List.memq ty !visited) then begin
          visited := ty::!visited;
          occur_rec f
        end
    | Tfield(_, t1, t2) ->
        occur_rec t1; occur_rec t2
    | Tnil ->
        ()
    | Tlink _ ->
        fatal_error "Ctype.moregen_occur"
  in
    occur_rec ty

let rec moregen env t1 t2 =
  if t1 == t2 then () else
  let t1 = repr t1 in
  let t2 = repr t2 in
  if t1 == t2 then () else
  let d1 = t1.desc in
  try
    begin match (t1.desc, t2.desc) with
      (Tvar, _) ->
        if t1.level = generic_level then raise (Unify []);
        moregen_occur env t1 t2;
        t1.desc <- Tlink t2
    | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
        moregen env t1 t2; moregen env u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        moregen_list env tl1 tl2
    | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) ->
        if Path.same p1 p2 then begin
          t1.desc <- Tlink t2;
          moregen_list env tl1 tl2;
          t1.desc <- d1
        end else begin
          try
            moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
          with Cannot_expand ->
          try
            moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
          with Cannot_expand -><commit_msg>Revision de la fonction `occur' : accepte de nouveau les recursions a travers des types construits qui ne sont pas des abreviations (e.g.: unification de 'a list avec 'a). Gestion correcte des abreviations du genre 'a t = int.<commit_after>(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(* <NAME> and <NAME>, projet Cristal, INRIA Rocquencourt*)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  Automatique.  Distributed only by permission.                      *)
(*                                                                     *)
(***********************************************************************)

(* $Id$ *)

(* Operations on core types *)

open Misc
open Asttypes
open Types

exception Unify of (type_expr * type_expr) list
exception Subtype of
        (type_expr * type_expr) list * (type_expr * type_expr) list

let current_level = ref 0
let global_level = ref 1
let generic_level = (-1)

let init_def level = current_level := level
let begin_def () = incr current_level
let end_def () = decr current_level

let reset_global_level () =
  global_level := !current_level + 1

let newty desc         = { desc = desc; level = !current_level }
let new_global_ty desc = { desc = desc; level = !global_level }
let newgenty desc      = { desc = desc; level = generic_level }
let newvar ()          = { desc = Tvar; level = !current_level }
let new_global_var ()  = new_global_ty Tvar
let new_gen_var ()     = newgenty Tvar
let newobj fields      = newty (Tobject (fields, ref None))

let rec repr = function
    {desc = Tlink t'} as t ->
      let r = repr t' in
      if r != t' then t.desc <- Tlink r;
      r
  | t -> t

let rec repr2 = function                (* No path compression *)
                                        (* during unification *)
    {desc = Tlink ty} ->
      repr2 ty
  | t -> t

let none = newty (Ttuple [])                (* Clearly ill-formed type *)

(* --- *)

let flatten_fields ty =
  let rec flatten l ty =
    let ty = repr ty in
    match ty.desc with
      Tfield(s, ty1, ty2) ->
        flatten ((s, ty1)::l) ty2
    | Tvar | Tnil ->
        (l, ty)
    | _ ->
      fatal_error "Ctype.flatten_fields"
  in
    let (l, r) = flatten [] ty in
      (List.rev l, r)

let build_fields =
  List.fold_right
    (fun (s, ty1) ty2 ->
       {desc = Tfield(s, ty1, ty2);
        level = ty2.level})

let associate_fields fields1 fields2 =
  let rec associate p s s' =
    function
      (l, []) ->
        (List.rev p, (List.rev s) @ l, List.rev s')
    | ([], l') ->
        (List.rev p, List.rev s, (List.rev s') @ l')
    | (((n, t)::r as l), ((n', t')::r' as l')) ->
        if n = n' then
          associate ((t, t')::p) s s' (r, r')
        else if n < n' then
          associate p ((n, t)::s) s' (r, l')
        else
          associate p s ((n', t')::s') (l, r')
  in let sort = Sort.list (fun (n, _) (n', _) -> n < n') in
  associate [] [] [] (sort fields1, sort fields2)

(* Check whether an object is open *)

let rec opened ty =
  match (repr ty).desc with
    Tfield(_, _, t) -> opened t
  | Tvar            -> true
  | Tnil            -> false
  | _               -> fatal_error "Ctype.opened"

let opened_object ty =
  match (repr ty).desc with
    Tobject (ty', _)  -> opened ty'
  | Tconstr (_, _, _) -> false
  | _                 -> fatal_error "Ctype.opened_object"

(* Type generalization *)

let rec generalize ty =
  let ty = repr ty in
  if ty.level > !current_level then begin
    ty.level <- generic_level;
    match ty.desc with
      Tvar               -> ()
    | Tarrow(t1, t2)     -> generalize t1; generalize t2
    | Ttuple tl          -> List.iter generalize tl
    | Tconstr(_, tl, ab) -> ab := []; List.iter generalize tl
    | Tobject(f, {contents = Some (_, p)})
                         -> generalize f; List.iter generalize p
    | Tobject(f, _)      -> generalize f
    | Tfield(_, t1, t2)  -> generalize t1; generalize t2
    | Tnil               -> ()
    | Tlink _            -> fatal_error "Ctype.generalize"
  end

let rec make_nongen ty =
  let ty = repr ty in
  if ty.level > !current_level then begin
    ty.level <- !current_level;
    match ty.desc with
      Tvar              -> ()
    | Tarrow(t1, t2)    ->  make_nongen t1; make_nongen t2
    | Ttuple tl         -> List.iter make_nongen tl
    | Tconstr(p, tl, _) -> List.iter make_nongen tl
    | Tobject(f, {contents = Some (_, p)})
                        -> make_nongen f; List.iter make_nongen p
    | Tobject(f, _)      -> make_nongen f
    | Tfield(_, t1, t2) -> make_nongen t1; make_nongen t2
    | Tnil              -> ()
    | Tlink _           -> fatal_error "Ctype.make_nongen"
  end

(* Remove abbreviations from generalized types *)

let visited = ref ([] : type_expr list)

let remove_abbrev ty =
  let rec remove ty =
    let ty = repr ty in
    if ty.level = generic_level & not (List.memq ty !visited) then begin
      visited := ty :: !visited;
      match ty.desc with
        Tvar               -> ()
      | Tarrow(t1, t2)     -> remove t1; remove t2
      | Ttuple tl          -> List.iter remove tl
      | Tconstr(_, tl, ab) -> ab := []; List.iter remove tl
      | Tobject(f, {contents = Some (_, p)})
                           -> remove f; List.iter remove p
      | Tobject(f, _)      -> remove f
      | Tfield(_, t1, t2)  -> remove t1; remove t2
      | Tnil               -> ()
      | Tlink _            -> fatal_error "Ctype.remove_abbrev"
      end
  in
    visited := []; remove ty; visited := []


(* Taking instances of type schemes *)

type 'a visited = Zero | One | Many of 'a

let inst_subst = ref ([] : (type_expr * type_expr) list)

let rec copy_rec abbrev visited ty =
  let ty = repr ty in
  if ty.level <> generic_level then ty else
  try
    match List.assq ty visited with
      {contents = Zero} as v ->
      	let t = newvar () in
	v := Many t;
	let ty' = copy_rec_2 abbrev visited ty v in
	t.desc <- ty'.desc;
	t
    | {contents = One} as v ->
        let t = newvar () in
        v := Many t;
        t
    | {contents = Many t} ->
        t
  with Not_found ->
    let v = ref One in
    let ty' = copy_rec_2 abbrev ((ty, v)::visited) ty v in
    match v with
      {contents = Many t} ->
      	t.desc <- ty'.desc;
	t
    | _ ->
      	ty'

and copy_rec_2 abbrev visited ty v =
  match ty.desc with
    Tvar ->
      begin try List.assq ty !inst_subst with Not_found ->
        let ty' = newvar () in
        inst_subst := (ty, ty') :: !inst_subst;
        ty'
      end
  | Tarrow (t1, t2) ->
      newty (Tarrow (copy_rec abbrev visited t1,
                     copy_rec abbrev visited t2))
  | Ttuple tl ->
      newty (Ttuple (List.map (copy_rec abbrev visited) tl))
  | Tconstr (p, [], _) ->
      newty (Tconstr (p, [], ref abbrev))
  | Tconstr (p, tl, _) ->
      newty (Tconstr (p, List.map (copy_rec abbrev visited) tl,
                      ref abbrev))
  | Tobject (t1, {contents = name}) ->
      let ty' () =
        let name' =
          match name with
            None ->
              None
          | Some (p, tl) ->
              Some (p, List.map (copy_rec abbrev visited) tl)
        in
          newty (Tobject (copy_rec abbrev visited t1, ref name'))
      in
      if opened_object ty then
        try
          List.assq ty !inst_subst
        with Not_found ->
          if v = ref One then begin
            let t = newvar () in
    	    v := Many t;
            inst_subst := (ty, t):: !inst_subst
          end;
          ty' ()
      else
        ty' ()
  | Tfield (label, t1, t2) ->
      newty (Tfield (label, copy_rec abbrev visited t1,
                            copy_rec abbrev visited t2))
  | Tnil ->
      newty Tnil
  | Tlink _ ->
      fatal_error "Ctype.copy_rec"

let copy ty = copy_rec [] [] ty
let subst abbrev ty = copy_rec abbrev [] ty
let copy_parameterized params ty = copy_rec [] params ty

let instance sch =
  inst_subst := [];
  let ty = copy sch in
  inst_subst := [];
  ty

let instance_constructor cstr =
  inst_subst := [];
  let ty_res = copy cstr.cstr_res in
  let ty_args = List.map copy cstr.cstr_args in
  inst_subst := [];
  (ty_args, ty_res)

let instance_label lbl =
  inst_subst := [];
  let ty_res = copy lbl.lbl_res in
  let ty_arg = copy lbl.lbl_arg in
  inst_subst := [];
  (ty_arg, ty_res)

let substitute abbrev params args body =
  inst_subst := List.combine params args;
  let ty = subst abbrev body in
  inst_subst := [];
  ty

let instance_parameterized_type sch_args sch =
  inst_subst := [];
  let params = List.map (function p -> (repr p, ref Zero)) sch_args in
  let ty_args = List.map (copy_parameterized params) sch_args in
  let ty = copy_parameterized params sch in
  inst_subst := [];
  (ty_args, ty)

let instance_parameterized_type_2 sch_args sch_lst sch =
  inst_subst := [];
  let params = List.map (function p -> (repr p, ref Zero)) sch_args in
  let ty_args = List.map (copy_parameterized params) sch_args in
  let ty_lst = List.map (copy_parameterized params) sch_lst in
  let ty = copy_parameterized params sch in
  inst_subst := [];
  (ty_args, ty_lst, ty)

let instance_class cl =
  inst_subst := [];
  let params0 = List.map (function p -> (repr p, ref Zero)) cl.cty_params in
  let params = List.map (copy_parameterized params0) cl.cty_params in
  let args = List.map (copy_parameterized params0) cl.cty_args in
  let vars =
    Vars.fold
      (fun lab (mut, ty) ->
         Vars.add lab (mut, copy_parameterized params0 ty))
      cl.cty_vars
      Vars.empty in
  let self = copy_parameterized params0 cl.cty_self in
  inst_subst := [];
  (params, args, vars, self)

(* Unification *)

let rec update_level level ty =
  let ty = repr2 ty in
  if ty.level > level then begin
    ty.level <- level;
    match ty.desc with
      Tvar               -> ()
    | Tarrow(t1,t2)      -> update_level level t1; update_level level t2
    | Ttuple(ty_list)    -> List.iter (update_level level) ty_list
    | Tconstr(_, tl, _)  -> List.iter (update_level level) tl
    | Tobject(f, {contents = Some (_, p)})
                         -> update_level level f;
                            List.iter (update_level level) p
    | Tobject (f, _)     -> update_level level f
    | Tfield(_, t1, t2)  -> update_level level t1; update_level level t2
    | Tnil               -> ()
    | Tlink _            -> fatal_error "Ctype.update_level"
  end

exception Cannot_expand

let rec find_expans p1 =
  function
    [] ->
      None
  | (p2, ty)::l ->
      if Path.same p1 p2 then
        Some ty
      else
        find_expans p1 l

let expand_abbrev env path args abbrev level =
  match find_expans path !abbrev with
    Some ty ->
      update_level level ty;
      ty
  | None ->
      let decl =
        try Env.find_type path env with Not_found -> raise Cannot_expand in
      match decl.type_manifest with
        Some body ->
          let v = newvar () in
          abbrev := (path, v)::!abbrev;
          let old_level = !current_level in
          current_level := level;
          let ty = substitute !abbrev decl.type_params args body in
          current_level := old_level;
          v.desc <- Tlink ty;
          ty
      | _ ->
          raise Cannot_expand

let rec expand_root env ty =
  let ty = repr ty in
  match ty.desc with
    Tconstr(p, tl, abbrev) ->
      begin try
        expand_root env (expand_abbrev env p tl (ref !abbrev) ty.level)
      with Cannot_expand ->
        ty
      end
  | _ ->
      ty

let rec full_expand env ty =
  let ty = repr (expand_root env ty) in
  match ty.desc with
    Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
      { desc = Tobject (fi, ref None); level = ty.level }
  | _ ->
      ty

let generic_abbrev env path =
  try
    let decl = Env.find_type path env in
    match decl.type_manifest with
      Some body ->
        body.level = generic_level
    | _ ->
        false
  with
    Not_found ->
      false

let occur env ty0 ty =
  let visited = ref ([] : type_expr list) in
  let rec occur_rec ty =
    let ty = repr ty in
    if ty == ty0 then raise (Unify []);
    match ty.desc with
      Tvar ->
        ()
    | Tarrow(t1, t2) ->
        occur_rec t1; occur_rec t2
    | Ttuple tl ->
        List.iter occur_rec tl
    | Tconstr(p, [], abbrev) ->
        if ty0.level < Path.binding_time p then begin
          if not (List.memq ty !visited) then begin
            visited := ty :: !visited;
            let ty' =
              try expand_abbrev env p [] abbrev ty.level
              with Cannot_expand -> raise (Unify []) in
            occur_rec ty'
          end
        end
    | Tconstr(p, tl, abbrev) ->
        if not (List.memq ty !visited) then begin
          visited := ty :: !visited;
          if ty0.level < Path.binding_time p then begin
            let ty' =
              try expand_abbrev env p [] abbrev ty.level
              with Cannot_expand -> raise (Unify []) in
            occur_rec ty'
          end else begin
            try
              List.iter occur_rec tl
            with Unify lst ->
            try
              let ty' = expand_abbrev env p tl abbrev ty.level in
              occur_rec ty'
            with Cannot_expand -> ()
          end
        end
    | Tobject (_, _) ->
        ()
    | _ (* Tfield (_, _, _) | Tnil | Tlink _ *) ->
        fatal_error "Ctype.occur"
  in
    occur_rec ty

let rec unify_rec env a1 a2 t1 t2 =     (* Variables and abbreviations *)
  if t1 == t2 then () else
  let t1 = repr2 t1 in
  let t2 = repr2 t2 in
  if t1 == t2 then () else
  try
    match (t1.desc, t2.desc) with
      (Tvar, _) ->
         update_level t1.level t2;
         begin match a2 with
           None    -> occur env t1 t2; t1.desc <- Tlink t2
         | Some l2 -> occur env t1 l2; t1.desc <- Tlink l2
         end
    | (_, Tvar) ->
         update_level t2.level t1;
         begin match a1 with
           None    -> occur env t2 t1; t2.desc <- Tlink t1
         | Some l1 -> occur env t2 l1; t2.desc <- Tlink l1
         end
    | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2))
            when Path.same p1 p2 ->
        begin
          try
            unify_core env a1 a2 t1 t2
          with Unify lst ->
          try
            let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
            update_level t2.level t1;
            unify_rec env (Some t1) a2 t3 t2
          with Cannot_expand ->
          try
            let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
            update_level t1.level t2;
            unify_rec env a1 (Some t2) t1 t3
          with Cannot_expand ->
            raise (Unify lst)
        end
    | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) ->
        begin
          try
            let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
            update_level t2.level t1;
            unify_rec env (Some t1) a2 t3 t2
          with Cannot_expand ->
          try
            let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
            update_level t1.level t2;
            unify_rec env a1 (Some t2) t1 t3
          with Cannot_expand ->
            raise (Unify [])
        end
    | (Tconstr (p1, tl1, abbrev1), _) ->
        begin try
          let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
          update_level t2.level t1;
          unify_rec env (Some t1) a2 t3 t2
        with Cannot_expand ->
          unify_core env a1 a2 t1 t2
        end
    | (_, Tconstr (p2, tl2, abbrev2)) ->
        begin try
          let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
          update_level t1.level t2;
          unify_rec env a1 (Some t2) t1 t3
        with Cannot_expand ->
          unify_core env a1 a2 t1 t2
        end
    | (_, _) ->
        unify_core env a1 a2 t1 t2
  with
    Unify [] ->
      raise (Unify [(t1, t2)])
  | Unify (_::l) ->
      raise (Unify ((t1, t2)::l))

and unify_core env a1 a2 t1 t2 =        (* Other cases *)
  let d1 = t1.desc and d2 = t2.desc in
  begin match (a1, a2) with
    (None,    Some l2) ->
      update_level t1.level t2; t1.desc <- Tlink l2
  | (Some l1, None) ->
      update_level t2.level t1; t2.desc <- Tlink l1
  | (_, _) ->
      update_level t1.level t2; occur env t1 t2; t1.desc <- Tlink t2
  end;
  try
    match (d1, d2) with
      (Tarrow (t1, u1), Tarrow (t2, u2)) ->
        unify_rec env None None t1 t2; unify_rec env None None u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        unify_list env tl1 tl2
    | (Tconstr (p1, [], _), Tconstr (p2, [], _)) (*when Path.same p1 p2*) ->
        ()
    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) (*when Path.same p1 p2*) ->
        unify_list env tl1 tl2
    | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
        unify_fields env fi1 fi2;
        begin match !nm2 with
          Some (_, va::_) when (repr va).desc = Tvar -> ()
        | _                                          -> nm2 := !nm1
        end
    | (_, _) ->
        raise (Unify [])
  with
    Unify l ->
      t1.desc <- d1;
      t2.desc <- d2;
      raise (Unify ((t1, t2)::l))
  | exn ->
      t1.desc <- d1;
      t2.desc <- d2;
      raise exn

and unify_list env tl1 tl2 =
  if List.length tl1 <> List.length tl2 then
    raise (Unify []);
  List.iter2 (unify_rec env None None) tl1 tl2

and unify_fields env ty1 ty2 =
  let (fields1, rest1) = flatten_fields ty1
  and (fields2, rest2) = flatten_fields ty2 in
  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
  let va = newvar () in
    begin match rest1.desc with
      Tvar ->
        let nr = build_fields miss2 va in
        update_level rest1.level nr;
        rest1.desc <- Tlink nr
    | Tnil ->
        if miss2 <> [] then raise (Unify []);
        va.desc <- Tlink {desc = Tnil; level = va.level}
    | _ ->
        fatal_error "Ctype.unify_fields (1)"
    end;
    begin match rest2.desc with
      Tvar ->
        let nr = build_fields miss1 va in
        update_level rest2.level nr;
        rest2.desc <- Tlink nr
    | Tnil ->
        if miss1 <> [] then raise (Unify []);
        va.desc <- Tlink {desc = Tnil; level = va.level}
    | _ ->
        fatal_error "Ctype.unify_fields (2)"
    end;
    List.iter (fun (t1, t2) -> unify_rec env None None t1 t2) pairs

let expand_trace env trace =
  List.fold_right
    (fun (t1, t2) rem ->
       (t1, full_expand env t1)::(t2, full_expand env t2)::rem)
    trace []

let rec filter_trace =
  function
    (t1, t1')::(t2, t2')::rem ->
      let rem' = filter_trace rem in
      if (t1 == t1') & (t2 == t2') then
        rem'
      else
        (t1, t1')::(t2, t2')::rem
  | _ ->
      []

let unify env ty1 ty2 =
  try
    unify_rec env None None ty1 ty2
  with Unify trace ->
    let trace = expand_trace env trace in
    match trace with
      t1::t2::rem ->
        raise (Unify (t1::t2::filter_trace rem))
    | _ ->
        fatal_error "Ctype.unify"

let rec filter_arrow env t =
  let t = repr t in
  match t.desc with
    Tvar ->
      let t1 = newvar () and t2 = newvar () in
      let t' = newty (Tarrow (t1, t2)) in
      update_level t.level t';
      t.desc <- Tlink t';
      (t1, t2)
  | Tarrow(t1, t2) ->
      (t1, t2)
  | Tconstr(p, tl, abbrev) ->
      begin try
        filter_arrow env (expand_abbrev env p tl abbrev t.level)
      with Cannot_expand ->
        raise (Unify [])
      end
  | _ ->
      raise (Unify [])

let rec filter_method_field name ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      let ty1 = newvar () and ty2 = newvar () in
      let ty' = newty (Tfield (name, ty1, ty2)) in
      update_level ty.level ty';
      ty.desc <- Tlink ty';
      ty1
  | Tfield(n, ty1, ty2) ->
      if n = name then
        ty1
      else
        filter_method_field name ty2
  | _ ->
      raise (Unify [])

let rec filter_method env name ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      let ty1 = newvar ()in
      let ty' = newobj ty1 in
      update_level ty.level ty';
      ty.desc <- Tlink ty';
      filter_method_field name ty1
  | Tobject(f, _) ->
      filter_method_field name f
  | Tconstr(p, tl, abbrev) ->
      begin try
        filter_method env name (expand_abbrev env p tl abbrev ty.level)
      with Cannot_expand ->
        raise (Unify [])
      end
  | _ ->
      raise (Unify [])

(* Matching between type schemes *)

let moregen_occur env ty0 ty =
  let visited = ref [] in
  let rec occur_rec ty =
    let ty = repr ty in
    match ty.desc with
      Tvar ->
        (* ty0 has level = !current_level iff it is generic
           in the original type scheme. In this case, it can be freely
           instantiated. Otherwise, ty0 is not generic
           and cannot be instantiated by a type that contains
           generic variables. *)
        if ty.level = generic_level & ty0.level < !current_level
        then raise (Unify [])
    | Tarrow(t1, t2) ->
        occur_rec t1; occur_rec t2
    | Ttuple tl ->
        List.iter occur_rec tl
    | Tconstr(p, tl, abbrev) ->
        if not (List.memq ty !visited) then begin
          visited := ty::!visited;
          try
            List.iter occur_rec tl
          with Unify lst ->
            let ty' =
              try expand_abbrev env p tl abbrev ty.level
              with Cannot_expand -> raise (Unify lst) in
            occur_rec ty'
        end
    | Tobject(f, _) ->
        if not (List.memq ty !visited) then begin
          visited := ty::!visited;
          occur_rec f
        end
    | Tfield(_, t1, t2) ->
        occur_rec t1; occur_rec t2
    | Tnil ->
        ()
    | Tlink _ ->
        fatal_error "Ctype.moregen_occur"
  in
    occur_rec ty

let rec moregen env t1 t2 =
  if t1 == t2 then () else
  let t1 = repr t1 in
  let t2 = repr t2 in
  if t1 == t2 then () else
  let d1 = t1.desc in
  try
    begin match (t1.desc, t2.desc) with
      (Tvar, _) ->
        if t1.level = generic_level then raise (Unify []);
        moregen_occur env t1 t2;
        t1.desc <- Tlink t2
    | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
        moregen env t1 t2; moregen env u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        moregen_list env tl1 tl2
    | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) ->
        if Path.same p1 p2 then begin
          try
            t1.desc <- Tlink t2;
            moregen_list env tl1 tl2;
            t1.desc <- d1
          with Unify lst ->
          t1.desc <- d1;
          try
            moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
          with Cannot_expand ->
          try
            moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
          with Cannot_expand ->
            raise (Unify lst)
        end else begin
          try
            moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
          with Cannot_expand ->
          try
            moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
          with Cannot_expand ->
{'fraction_non_alphanumeric': 0.11253111664295874, 'fraction_numerical': 0.01995910384068279, 'mean_word_length': 1.754055212095244, 'pattern_counts': {'":': 0, '<': 82, '<?xml version=': 0, '>': 378, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5063240', 'n_tokens_mistral': 15746, 'n_tokens_neox': 15292, 'n_words': 4955}