Ekdohibs
/
ocaml
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Ajout de btype.ml{,i} (operations de bases sur les types) 

Modification de correct_levels, moregeneral et subst
Changement de la valeur de generic_level
Correction d'un bug de correct_abbrev


git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@1452 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Jérôme Vouillon 1997-03-24 20:12:00 +00:00
parent 151e685171
commit 87e358d2eb
1 changed files with 75 additions and 138 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

213
typing/ctype.ml
View File

@ -16,6 +16,7 @@
open Misc
open Asttypes
open Types
open Btype
(*
Type manipulation after type inference
@ -24,7 +25,7 @@ open Types
instance, during code generation or in the debugger), one must
first make sure that the type levels are correct, using the
function [correct_levels]. Then, this type can be correctely
manipulated by [substitute], [expand_abbrev] and [moregeneral].
manipulated by [apply], [expand_abbrev] and [moregeneral].
*)
(*
@ -52,12 +53,9 @@ open Types
(*
A faire
=======
- Renommer [substitute] en [apply]
- Revoir affichage des types.
- Types recursifs sans limitation.
- Etendre la portee d'un alias [... as 'a] a tout le type englobant.
- #-type implementes comme de vraies abreviations.
- Deplacer Ctype.repr dans Types ?
- Niveaux plus fins pour les identificateurs :
Champ [global] renomme en [level];
Niveau -1 : global
@ -96,7 +94,6 @@ exception Recursive_abbrev
(**** Type level management ****)
let generic_level = (-1)
let current_level = ref 0
let global_level = ref 1
@ -107,21 +104,19 @@ let end_def () = decr current_level
let reset_global_level () =
global_level := !current_level + 1
(* Used to mark a type during a traversal. *)
let lowest_level = generic_level
let pivot_level = 2 * lowest_level - 1
(* pivot_level - lowest_level < lowest_level *)
(**** Some type creators ****)
(* Re-export generic type creators *)
let newty desc = { desc = desc; level = !current_level }
let newgenty desc = { desc = desc; level = generic_level }
let newgenty = newgenty
let new_global_ty desc = { desc = desc; level = !global_level }
let newvar () = { desc = Tvar; level = !current_level }
let newgenvar () = newgenty Tvar
let newmarkedvar () = { desc = Tvar; level = pivot_level - !current_level }
let newgenvar = newgenvar
let new_global_var () = new_global_ty Tvar
let newmarkedvar () = { desc = Tvar; level = pivot_level - generic_level }
let newmarkedgenvar = newmarkedgenvar
let newobj fields = newty (Tobject (fields, ref None))
@ -129,40 +124,8 @@ let none = newty (Ttuple []) (* Clearly ill-formed type *)
(**** Representative of a type ****)
let rec repr =
function
{desc = Tlink t'} ->
(*
We do no path compression. Path compression does not seem to
improve notably efficiency, and it prevents from changing a
[Tlink] into another type (for instance, for undoing a
unification).
*)
repr t'
| t -> t
(**********************************)
(* Utilities for type traversal *)
(**********************************)
let saved_desc = ref []
(* Saved association of generic nodes with their description. *)
(* Restored type descriptions *)
let cleanup_types () =
List.iter (fun (ty, desc) -> ty.desc <- desc) !saved_desc;
saved_desc := []
(* Remove marks from a type. *)
let rec unmark_type ty =
let ty = repr ty in
if ty.level < lowest_level then begin
ty.level <- pivot_level - ty.level;
iter_type_expr unmark_type ty
end
(* Re-export repr *)
let repr = repr
(**********************************************)
(* Miscellaneous operations on object types *)
@ -273,7 +236,7 @@ let remove_object_name ty =
*)
let rec generalize ty =
let ty = repr ty in
if ty.level > !current_level then begin
if (ty.level > !current_level) && (ty.level <> generic_level) then begin
ty.level <- generic_level;
begin match ty.desc with
Tconstr (_, _, abbrev) ->
@ -289,28 +252,6 @@ and generalize_expans =
| Mcons(_, ty, rem) -> generalize ty; generalize_expans rem
| Mlink rem -> generalize_expans !rem
(*
Lower in-place the level of a generic type. That way, [subst] can
do "unification" on generic types.
*)
let rec ungeneralize ty =
let ty = repr ty in
if ty.level = generic_level then begin
ty.level <- !current_level;
begin match ty.desc with
Tconstr (_, _, abbrev) ->
ungeneralize_expans !abbrev
| _ -> ()
end;
iter_type_expr ungeneralize ty
end
and ungeneralize_expans =
function
Mnil -> ()
| Mcons(_, ty, rem) -> ungeneralize ty; ungeneralize_expans rem
| Mlink rem -> ungeneralize_expans !rem
let expand_abbrev' = (* Forward declaration *)
ref (fun env path args abbrev level -> raise Cannot_expand)
@ -355,8 +296,8 @@ let rec update_level env level ty =
let make_nongen ty = update_level Env.empty !current_level ty
(* Correct the levels of type [ty]. *)
let correct_levels env ty =
Subst.type_expr (Subst.limit_level (Env.level env) Subst.identity) ty
let correct_levels ty =
Subst.type_expr Subst.identity ty
(*******************)
@ -366,12 +307,13 @@ let correct_levels env ty =
(*
Generic nodes are duplicated, while non-generic nodes are left
as-is. The instance cannot be generic.
as-is.
During instantiation, the description of a generic node is first
replaced by a link to a stub ([Tlink (newvar ())]). Once the copy
is made, it replaces the stub.
replaced by a link to a stub ([Tlink (newmarkedvar ())]). Once the
copy is made, it replaces the stub.
After instantiation, the description of generic node, which was
stored in [saved_desc], must be put back, using [cleanup_types].
stored by [save_desc], must be put back, using [cleanup_types].
Marked on the copy are removed by [unmark].
*)
let abbreviations = ref (ref Mnil)
@ -383,8 +325,8 @@ let rec copy ty =
ty
else begin
let desc = ty.desc in
saved_desc := (ty, desc)::!saved_desc;
let t = newvar () in (* Stub *)
save_desc ty desc;
let t = newmarkedvar () in (* Stub *)
ty.desc <- Tlink t;
t.desc <-
begin match desc with
@ -432,29 +374,34 @@ let rec copy ty =
let instance sch =
let ty = copy sch in
cleanup_types ();
unmark_type ty;
ty
let instance_list schl =
let tyl = List.map copy schl in
cleanup_types ();
List.iter unmark_type tyl;
tyl
let instance_constructor cstr =
let ty_res = copy cstr.cstr_res in
let ty_args = List.map copy cstr.cstr_args in
cleanup_types ();
List.iter unmark_type ty_args; unmark_type ty_res;
(ty_args, ty_res)
let instance_label lbl =
let ty_res = copy lbl.lbl_res in
let ty_arg = copy lbl.lbl_arg in
cleanup_types ();
unmark_type ty_arg; unmark_type ty_res;
(ty_arg, ty_res)
let instance_parameterized_type sch_args sch =
let ty_args = List.map copy sch_args in
let ty = copy sch in
cleanup_types ();
List.iter unmark_type ty_args; unmark_type ty;
(ty_args, ty)
let instance_parameterized_type_2 sch_args sch_lst sch =
@ -462,6 +409,8 @@ let instance_parameterized_type_2 sch_args sch_lst sch =
let ty_lst = List.map copy sch_lst in
let ty = copy sch in
cleanup_types ();
List.iter unmark_type ty_args; List.iter unmark_type ty_lst;
unmark_type ty;
(ty_args, ty_lst, ty)
let instance_class cl =
@ -475,6 +424,9 @@ let instance_class cl =
Vars.empty in
let self = copy cl.cty_self in
cleanup_types ();
List.iter unmark_type params; List.iter unmark_type args;
Vars.iter (fun l (m, t) -> unmark_type t) vars;
unmark_type self;
(params, args, vars, self)
(**** Instantiation with parameter substitution ****)
@ -483,9 +435,9 @@ let unify' = (* Forward declaration *)
ref (fun env ty1 ty2 -> raise (Unify []))
let rec subst env level abbrev path params args body =
if level <> generic_level then begin
let old_level = !current_level in
current_level := level;
let old_level = !current_level in
current_level := level;
try
let body0 = newvar () in (* Stub *)
begin match path with
None -> ()
@ -498,22 +450,9 @@ let rec subst env level abbrev path params args body =
List.iter2 (!unify' env) params' args;
current_level := old_level;
body'
end else begin
(* One cannot expand directly to a generic type. *)
begin_def ();
(* Make sure [!current_level] is high enough. *)
current_level := max !current_level (Env.level env);
(*
Arguments cannot be generic either, as they are unified to the
parameters.
*)
List.iter ungeneralize args;
let ty = subst env !current_level abbrev path params args body in
end_def ();
generalize ty;
List.iter generalize args;
ty
end
with Unify _ as exn ->
current_level := old_level;
raise exn
(*
Only the shape of the type matters, not whether is is generic or
@ -641,35 +580,33 @@ let generic_abbrev env path =
exception Occur
let marked_types = ref []
(* The marks are already used by [expand_abbrev]... *)
let visited = ref []
let rec non_recursive_abbrev env path ty =
let rec non_recursive_abbrev env ty =
let ty = repr ty in
if ty.level >= lowest_level then begin
if ty == none then raise Recursive_abbrev;
if not (List.memq ty !visited) then begin
let level = ty.level in
ty.level <- pivot_level - level;
visited := ty :: !visited;
match ty.desc with
Tconstr(p, _, _) when Path.same path p ->
raise Recursive_abbrev
| Tconstr(p, args, abbrev) ->
Tconstr(p, args, abbrev) ->
begin try
let ty' = repr (expand_abbrev env p args abbrev level) in
if ty'.level >= lowest_level then begin
marked_types := ty' :: !marked_types;
non_recursive_abbrev env path ty'
end
non_recursive_abbrev env ty'
with Cannot_expand -> () end
| Tobject (_, _) ->
()
| _ ->
iter_type_expr (non_recursive_abbrev env path) ty
iter_type_expr (non_recursive_abbrev env) ty
end
let correct_abbrev env ident params ty =
marked_types := [ty];
non_recursive_abbrev env (Path.Pident ident) ty;
List.iter unmark_type !marked_types;
marked_types := []
visited := [];
non_recursive_abbrev env
(subst env generic_level (ref (Mcons (Path.Pident ident, none, Mnil))) None
[] [] ty);
visited := []
let occur env ty0 ty =
let visited = ref ([] : type_expr list) in
@ -795,8 +732,11 @@ and unify2 env t1 t2 =
(* Second step: expansion of abbreviations *)
let t1' = expand_head env t1 in
let t2' = expand_head env t2 in
(* Expansion may have changed the representative of the types... *)
let t1' = repr t1' and t2' = repr t2' in
if t1' == t2' then () else
let t1 = repr t1 and t2 = repr t2 in
if (t1 == t1') || (t2 != t2') then
unify3 env t1 t1' t2 t2'
else
@ -864,13 +804,13 @@ and unify3 env t1 t1' t2 t2' =
if t1 != t1' (* && t2 != t2' *) then begin
match (t1.desc, t2.desc) with
(Tconstr (p, ty::_, _), _)
when ((repr ty).desc != Tvar)
when ((repr ty).desc <> Tvar)
&& weak_abbrev p
&& not (deep_occur t1 t2) ->
update_level env t1.level t2;
t1.desc <- Tlink t2
| (_, Tconstr (p, ty::_, _))
when ((repr ty).desc != Tvar)
when ((repr ty).desc <> Tvar)
&& weak_abbrev p
&& not (deep_occur t2 t1) ->
update_level env t2.level t1;
@ -980,8 +920,8 @@ let rec filter_method env name ty =
(*
Levels:
!current_level : generic variables from the pattern
!current_level - 1 : generic variables from the subject
generic_level : generic variables from the pattern
generic_level - 1 : generic variables from the subject
A generic variable from the subject cannot be instantiated, and its
level must remain unchanged. A generic variable from the pattern
@ -999,14 +939,14 @@ let rec filter_method env name ty =
let moregen_occur env level ty =
let rec occur_rec ty =
let ty = repr ty in
if ty.level >= !current_level - 1 then begin
if (ty.desc = Tvar) && (ty.level = !current_level - 1) then
if ty.level >= generic_level - 1 then begin
if (ty.desc = Tvar) && (ty.level = generic_level - 1) then
raise Occur;
ty.level <- pivot_level - ty.level;
iter_type_expr occur_rec ty
end
in
if level < !current_level - 1 then begin
if level < generic_level - 1 then begin
begin try
occur_rec ty; unmark_type ty
with Occur ->
@ -1026,14 +966,14 @@ let rec moregen env t1 t2 =
t2.desc <- Tlink t1;
try
begin match (t1.desc, !d2) with
(Tvar, _) when t1.level <> !current_level - 1 ->
(Tvar, _) when t1.level <> generic_level - 1 ->
t2.desc <- !d2;
begin try occur env t1 t2 with Occur ->
raise (Unify [])
end;
moregen_occur env t1.level t2;
t1.desc <- Tlink t2
| (_, Tvar) when t2.level <> !current_level - 1 ->
| (_, Tvar) when t2.level <> generic_level - 1 ->
begin try occur env t2 t1 with Occur ->
raise (Unify [])
end;
@ -1110,20 +1050,17 @@ and moregen_fields env ty1 ty2 =
List.iter (fun (t1, t2) -> moregen env t1 t2) pairs
let moregeneral env sch1 sch2 =
(* Make sure [!current_level] is high enough. *)
current_level := max !current_level (Env.level env);
begin_def ();
let old_level = !current_level in
current_level := generic_level - 1;
let ty2 = instance sch2 in
begin_def ();
current_level := generic_level;
let ty1 = instance sch1 in
try
moregen env ty1 ty2;
end_def ();
end_def ();
current_level := old_level;
true
with Unify _ ->
end_def ();
end_def ();
current_level := old_level;
false
@ -1414,11 +1351,11 @@ let rec arity ty =
Variables are left unchanged. Other type nodes are duplicated, with
levels set to generic level.
During copying, the description of a (non-variable) node is first
replaced by a link to a marked stub ([Tlink (newmarkedvar
())]). The mark allows to differentiate the original type from the
copy. Once the copy is made, it replaces the stub.
After copying, the description of node, which was stored in
[saved_desc], must be put back, using [cleanup_types], and the
replaced by a link to a marked stub ([Tlink (newmarkedgenvar ())]).
The mark allows to differentiate the original type from the copy.
Once the copy is made, it replaces the stub.
After copying, the description of node, which was stored by
[save_desc], must be put back, using [cleanup_types], and the
marks on the copy must be removed.
*)
@ -1428,8 +1365,8 @@ let rec nondep_type_rec env id ty =
ty
else begin
let desc = ty.desc in
saved_desc := (ty, desc)::!saved_desc;
let ty' = newmarkedvar () in (* Stub *)
save_desc ty desc;
let ty' = newmarkedgenvar () in (* Stub *)
ty.desc <- Tlink ty';
ty'.desc <-
begin match desc with
@ -1579,7 +1516,7 @@ let rec closed_schema_rec row ty =
let level = ty.level in
ty.level <- pivot_level - level;
match ty.desc with
Tvar when level != generic_level ->
Tvar when level <> generic_level ->
raise (Failed (if row then Row_var ty else Var ty))
| Tobject(f, {contents = Some (_, p)}) ->
closed_schema_rec true f;