Merge pull request #327 from garrigue/repr_and_unused_performance
Solve new performance problems of PR#6542master
commit
7a2a87f27d
|
@ -9,7 +9,7 @@ Here is an example of a value that is not matched:
|
|||
0
|
||||
File "w01.ml", line 36, characters 0-1:
|
||||
Warning 10: this expression should have type unit.
|
||||
File "w01.ml", line 20, characters 8-9:
|
||||
Warning 27: unused variable y.
|
||||
File "w01.ml", line 43, characters 2-3:
|
||||
Warning 11: this match case is unused.
|
||||
File "w01.ml", line 20, characters 8-9:
|
||||
Warning 27: unused variable y.
|
||||
|
|
106
typing/btype.ml
106
typing/btype.ml
|
@ -62,6 +62,34 @@ let default_mty = function
|
|||
Some mty -> mty
|
||||
| None -> Mty_signature []
|
||||
|
||||
(**** Definitions for backtracking ****)
|
||||
|
||||
type change =
|
||||
Ctype of type_expr * type_desc
|
||||
| Ccompress of type_expr * type_desc * type_desc
|
||||
| Clevel of type_expr * int
|
||||
| Cname of
|
||||
(Path.t * type_expr list) option ref * (Path.t * type_expr list) option
|
||||
| Crow of row_field option ref * row_field option
|
||||
| Ckind of field_kind option ref * field_kind option
|
||||
| Ccommu of commutable ref * commutable
|
||||
| Cuniv of type_expr option ref * type_expr option
|
||||
| Ctypeset of TypeSet.t ref * TypeSet.t
|
||||
|
||||
type changes =
|
||||
Change of change * changes ref
|
||||
| Unchanged
|
||||
| Invalid
|
||||
|
||||
let trail = Weak.create 1
|
||||
|
||||
let log_change ch =
|
||||
match Weak.get trail 0 with None -> ()
|
||||
| Some r ->
|
||||
let r' = ref Unchanged in
|
||||
r := Change (ch, r');
|
||||
Weak.set trail 0 (Some r')
|
||||
|
||||
(**** Representative of a type ****)
|
||||
|
||||
let rec field_kind_repr =
|
||||
|
@ -69,25 +97,25 @@ let rec field_kind_repr =
|
|||
Fvar {contents = Some kind} -> field_kind_repr kind
|
||||
| kind -> kind
|
||||
|
||||
(*
|
||||
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'
|
||||
| {desc = Tfield (_, k, _, t')} when field_kind_repr k = Fabsent ->
|
||||
repr t'
|
||||
| t -> t
|
||||
*)
|
||||
let rec repr_link compress t d =
|
||||
function
|
||||
{desc = Tlink t' as d'} ->
|
||||
repr_link true t d' t'
|
||||
| {desc = Tfield (_, k, _, t') as d'} when field_kind_repr k = Fabsent ->
|
||||
repr_link true t d' t'
|
||||
| t' ->
|
||||
if compress then begin
|
||||
log_change (Ccompress (t, t.desc, d)); t.desc <- d
|
||||
end;
|
||||
t'
|
||||
|
||||
(* Path compression must be undone by backtracking *)
|
||||
let repr_link' = ref (fun _ -> assert false)
|
||||
let repr t = !repr_link' 0 t t.desc t
|
||||
let repr t =
|
||||
match t.desc with
|
||||
Tlink t' as d ->
|
||||
repr_link false t d t'
|
||||
| Tfield (_, k, _, t') as d when field_kind_repr k = Fabsent ->
|
||||
repr_link false t d t'
|
||||
| _ -> t
|
||||
|
||||
let rec commu_repr = function
|
||||
Clink r when !r <> Cunknown -> commu_repr !r
|
||||
|
@ -599,18 +627,6 @@ let extract_label l ls = extract_label_aux [] l ls
|
|||
(* Utilities for backtracking *)
|
||||
(**********************************)
|
||||
|
||||
type change =
|
||||
Ctype of type_expr * type_desc
|
||||
| Ccompress of type_expr * type_desc * type_desc
|
||||
| Clevel of type_expr * int
|
||||
| Cname of
|
||||
(Path.t * type_expr list) option ref * (Path.t * type_expr list) option
|
||||
| Crow of row_field option ref * row_field option
|
||||
| Ckind of field_kind option ref * field_kind option
|
||||
| Ccommu of commutable ref * commutable
|
||||
| Cuniv of type_expr option ref * type_expr option
|
||||
| Ctypeset of TypeSet.t ref * TypeSet.t
|
||||
|
||||
let undo_change = function
|
||||
Ctype (ty, desc) -> ty.desc <- desc
|
||||
| Ccompress (ty, desc, _) -> ty.desc <- desc
|
||||
|
@ -622,23 +638,9 @@ let undo_change = function
|
|||
| Cuniv (r, v) -> r := v
|
||||
| Ctypeset (r, v) -> r := v
|
||||
|
||||
type changes =
|
||||
Change of change * changes ref
|
||||
| Unchanged
|
||||
| Invalid
|
||||
|
||||
type snapshot = changes ref * int
|
||||
|
||||
let trail = Weak.create 1
|
||||
let last_snapshot = ref 0
|
||||
|
||||
let log_change ch =
|
||||
match Weak.get trail 0 with None -> ()
|
||||
| Some r ->
|
||||
let r' = ref Unchanged in
|
||||
r := Change (ch, r');
|
||||
Weak.set trail 0 (Some r')
|
||||
|
||||
let log_type ty =
|
||||
if ty.id <= !last_snapshot then log_change (Ctype (ty, ty.desc))
|
||||
let link_type ty ty' =
|
||||
|
@ -725,19 +727,3 @@ let undo_compress (changes, old) =
|
|||
ty.desc <- desc; r := !next
|
||||
| _ -> ())
|
||||
log
|
||||
|
||||
let rec repr_link n t d =
|
||||
function
|
||||
{desc = Tlink t' as d'} ->
|
||||
repr_link (succ n) t d' t'
|
||||
| {desc = Tfield (_, k, _, t') as d'} when field_kind_repr k = Fabsent ->
|
||||
repr_link (succ n) t d' t'
|
||||
| t' ->
|
||||
if n > 1 then begin
|
||||
log_change (Ccompress (t, t.desc, d)); t.desc <- d
|
||||
end;
|
||||
t'
|
||||
|
||||
let () = repr_link' := repr_link
|
||||
|
||||
let repr t = repr_link 0 t t.desc t
|
||||
|
|
|
@ -3670,9 +3670,8 @@ and type_statement env sexp =
|
|||
and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
|
||||
(* ty_arg is _fully_ generalized *)
|
||||
let patterns = List.map (fun {pc_lhs=p} -> p) caselist in
|
||||
let erase_either =
|
||||
List.exists contains_polymorphic_variant patterns
|
||||
&& contains_variant_either ty_arg
|
||||
let contains_polyvars = List.exists contains_polymorphic_variant patterns in
|
||||
let erase_either = contains_polyvars && contains_variant_either ty_arg
|
||||
and has_gadts = List.exists (contains_gadt env) patterns in
|
||||
(* prerr_endline ( if has_gadts then "contains gadt" else "no gadt"); *)
|
||||
let ty_arg =
|
||||
|
@ -3696,7 +3695,18 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
|
|||
in
|
||||
(* if has_gadts then
|
||||
Format.printf "lev = %d@.%a@." lev Printtyp.raw_type_expr ty_res; *)
|
||||
begin_def (); (* propagation of the argument *)
|
||||
(* Do we need to propagate polymorphism *)
|
||||
let propagate =
|
||||
!Clflags.principal || do_init || (repr ty_arg).level = generic_level ||
|
||||
let rec is_var spat =
|
||||
match spat.ppat_desc with
|
||||
Ppat_any | Ppat_var _ -> true
|
||||
| Ppat_alias (spat, _) -> is_var spat
|
||||
| _ -> false in
|
||||
match caselist with
|
||||
[{pc_lhs}] when is_var pc_lhs -> false
|
||||
| _ -> true in
|
||||
if propagate then begin_def (); (* propagation of the argument *)
|
||||
let ty_arg' = newvar () in
|
||||
let pattern_force = ref [] in
|
||||
(* Format.printf "@[%i %i@ %a@]@." lev (get_current_level())
|
||||
|
@ -3740,11 +3750,15 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
|
|||
(* `Contaminating' unifications start here *)
|
||||
List.iter (fun f -> f()) !pattern_force;
|
||||
(* Post-processing and generalization *)
|
||||
List.iter (iter_pattern (fun {pat_type=t} -> unify_var env t (newvar())))
|
||||
patl;
|
||||
List.iter (fun pat -> unify_pat env pat (instance env ty_arg)) patl;
|
||||
end_def ();
|
||||
List.iter (iter_pattern (fun {pat_type=t} -> generalize t)) patl;
|
||||
let unify_pats ty = List.iter (fun pat -> unify_pat env pat ty) patl in
|
||||
if propagate then begin
|
||||
List.iter
|
||||
(iter_pattern (fun {pat_type=t} -> unify_var env t (newvar()))) patl;
|
||||
unify_pats (instance env ty_arg);
|
||||
end_def ();
|
||||
List.iter (iter_pattern (fun {pat_type=t} -> generalize t)) patl;
|
||||
end
|
||||
else if erase_either then unify_pats (instance env ty_arg);
|
||||
(* type bodies *)
|
||||
let in_function = if List.length caselist = 1 then in_function else None in
|
||||
let cases =
|
||||
|
@ -3789,14 +3803,19 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
|
|||
else
|
||||
Partial
|
||||
in
|
||||
let ty_arg_check =
|
||||
(* Hack: use for_saving to copy variables too *)
|
||||
Subst.type_expr (Subst.for_saving Subst.identity) ty_arg in
|
||||
add_delayed_check
|
||||
(fun () ->
|
||||
List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
|
||||
pat_env_list;
|
||||
check_unused ~lev env (instance env ty_arg_check) cases);
|
||||
let unused_check ty_arg () =
|
||||
List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
|
||||
pat_env_list;
|
||||
check_unused ~lev env (instance env ty_arg) cases
|
||||
in
|
||||
if contains_polyvars then
|
||||
let ty_arg_check =
|
||||
(* Hack: use for_saving to copy variables too *)
|
||||
Subst.type_expr (Subst.for_saving Subst.identity) ty_arg in
|
||||
add_delayed_check (unused_check ty_arg_check)
|
||||
else
|
||||
unused_check ty_arg ();
|
||||
(* Check for unused cases, do not delay because of gadts *)
|
||||
if do_init then begin
|
||||
end_def ();
|
||||
(* Ensure that existential types do not escape *)
|
||||
|
|
Loading…
Reference in New Issue