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

Improved exhaustiveness warnings for GADTs, with non-deterministic in type_pat 

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadt-warnings@16133 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Jacques Garrigue 2015-05-19 22:52:21 +00:00
parent 82c9bc58a0
commit c88f3d0634
13 changed files with 397 additions and 294 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
testsuite/tests/typing-gadts/omega07.ml.principal.reference
View File

@ -63,15 +63,7 @@ val plus_assoc :
# val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun> # val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff # type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun> # * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# Characters 87-243: # val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
..match a, b,le with (* warning *)
| NZ, m, LeZ _ -> Diff (m, PlusZ m)
| NS x, NS y, LeS q ->
match diff q x y with Diff (m, p) -> Diff (m, PlusS p)
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun> # val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter # type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun> val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun>

10
testsuite/tests/typing-gadts/omega07.ml.reference
View File

@ -63,15 +63,7 @@ val plus_assoc :
# val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun> # val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff # type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun> # * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# Characters 87-243: # val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
..match a, b,le with (* warning *)
| NZ, m, LeZ _ -> Diff (m, PlusZ m)
| NS x, NS y, LeS q ->
match diff q x y with Diff (m, p) -> Diff (m, PlusS p)
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun> # val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
# type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter # type (_, _) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun> val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun>

2
testsuite/tests/typing-gadts/pr5332.ml.reference
View File

@ -13,7 +13,7 @@
| Tvar var, tb -> 2 | Tvar var, tb -> 2
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
(Tbool, Tvar _) (Tbool, Tvar Zero)
val f : ('env, 'a) typ -> ('env, 'a) typ -> int = <fun> val f : ('env, 'a) typ -> ('env, 'a) typ -> int = <fun>
# Exception: Match_failure ("//toplevel//", 9, 1). # Exception: Match_failure ("//toplevel//", 9, 1).
# #

2
testsuite/tests/typing-gadts/pr6163.ml.principal.reference
View File

@ -13,6 +13,6 @@
| Succ (Succ (Succ (Succ Zero))) -> "4" | Succ (Succ (Succ (Succ Zero))) -> "4"
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _)))) Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux -> string = <fun> val f : aux -> string = <fun>
# #

2
testsuite/tests/typing-gadts/pr6163.ml.reference
View File

@ -13,6 +13,6 @@
| Succ (Succ (Succ (Succ Zero))) -> "4" | Succ (Succ (Succ (Succ Zero))) -> "4"
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
Succ (Succ (Succ (Succ (Succ _)))) Succ (Succ (Succ (Succ (Succ Zero))))
val f : aux -> string = <fun> val f : aux -> string = <fun>
# #

48
testsuite/tests/typing-gadts/test.ml
View File

@ -97,6 +97,52 @@ module PR6862 = struct
class d (Just x) = object method x : int = x end class d (Just x) = object method x : int = x end
end;; end;;
module Exhaustive2 = struct
type _ t = Int : int t
let f (x : bool t option) = match x with None -> ()
end;;
module PR6220 = struct
type 'a t = I : int t | F : float t
let f : int t -> int = function I -> 1
let g : int t -> int = function I -> 1 | _ -> 2 (* no warning *)
end;;
module PR6403 = struct
type (_, _) eq = Refl : ('a, 'a) eq
type empty = { bottom : 'a . 'a }
type ('a, 'b) sum = Left of 'a | Right of 'b
let notequal : ((int, bool) eq, empty) sum -> empty = function
| Right empty -> empty
end;;
module PR6437 = struct
type ('a, 'b) ctx =
| Nil : (unit, unit) ctx
| Cons : ('a, 'b) ctx -> ('a * unit, 'b * unit) ctx
type 'a var =
| O : ('a * unit) var
| S : 'a var -> ('a * unit) var
let rec f : type g1 g2. (g1, g2) ctx * g1 var -> g2 var = function
| Cons g, O -> O
| Cons g, S n -> S (f (g, n))
(*| Nil, _ -> (assert false) *) (* warns, but shouldn't *)
end;;
module PR6801 = struct
type _ value =
| String : string -> string value
| Float : float -> float value
| Any
let print_string_value (x : string value) =
match x with
| String s -> print_endline s (* warn : Any *)
end;;
module Existential_escape = module Existential_escape =
struct struct
type _ t = C : int -> int t type _ t = C : int -> int t
@ -114,7 +160,7 @@ module Rectype =
;; ;;
module Or_patterns = module Or_patterns =
struct struct
type _ t = type _ t =
| IntLit : int -> int t | IntLit : int -> int t
| BoolLit : bool -> bool t | BoolLit : bool -> bool t

49
testsuite/tests/typing-gadts/test.ml.principal.reference
View File

@ -65,6 +65,43 @@ module PR6862 :
type _ opt = Just : 'a -> 'a opt | Nothing : 'a opt type _ opt = Just : 'a -> 'a opt | Nothing : 'a opt
class d : int opt -> object method x : int end class d : int opt -> object method x : int end
end end
# module Exhaustive2 :
sig type _ t = Int : int t val f : bool t option -> unit end
# module PR6220 :
sig
type 'a t = I : int t | F : float t
val f : int t -> int
val g : int t -> int
end
# module PR6403 :
sig
type (_, _) eq = Refl : ('a, 'a) eq
type empty = { bottom : 'a. 'a; }
type ('a, 'b) sum = Left of 'a | Right of 'b
val notequal : ((int, bool) eq, empty) sum -> empty
end
# module PR6437 :
sig
type ('a, 'b) ctx =
Nil : (unit, unit) ctx
| Cons : ('a, 'b) ctx -> ('a * unit, 'b * unit) ctx
type 'a var = O : ('a * unit) var | S : 'a var -> ('a * unit) var
val f : ('g1, 'g2) ctx * 'g1 var -> 'g2 var
end
# Characters 175-221:
....match x with
| String s -> print_endline s.................
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Any
module PR6801 :
sig
type _ value =
String : string -> string value
| Float : float -> float value
| Any
val print_string_value : string value -> unit
end
# Characters 118-119: # Characters 118-119:
let eval (D x) = x let eval (D x) = x
^ ^
@ -73,7 +110,7 @@ Error: This expression has type a#2 t but an expression was expected of type
The type constructor a#2 would escape its scope The type constructor a#2 would escape its scope
# module Rectype : # module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end
# Characters 178-186: # Characters 180-188:
| (IntLit _ | BoolLit _) -> () | (IntLit _ | BoolLit _) -> ()
^^^^^^^^ ^^^^^^^^
Error: This pattern matches values of type int t Error: This pattern matches values of type int t
@ -265,7 +302,7 @@ val f : 'a ty -> 'a t -> int = <fun>
| TA, D z -> z | TA, D z -> z
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
(TE TC, D [| |]) (TE TC, D [| 0. |])
val f : 'a ty -> 'a t -> int = <fun> val f : 'a ty -> 'a t -> int = <fun>
# Characters 147-154: # Characters 147-154:
| D [|1.0|], TE TC -> 14 | D [|1.0|], TE TC -> 14
@ -287,7 +324,7 @@ Error: This pattern matches values of type 'a array
| {left=TA; right=D z} -> z | {left=TA; right=D z} -> z
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
{left=TE TC; right=D [| |]} {left=TE TC; right=D [| 0. |]}
type ('a, 'b) pair = { left : 'a; right : 'b; } type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty -> 'a t -> int = <fun> val f : 'a ty -> 'a t -> int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end # module M : sig type 'a t val eq : ('a t, 'b t) eq end
@ -309,14 +346,14 @@ type _ int_bar = IB_constr : < bar : int; .. > int_bar
^ ^
Error: This expression has type t = < foo : int; .. > Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int > but an expression was expected of type < foo : int >
Type ex#17 = < bar : int; .. > is not compatible with type < > Type ex#25 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar The second object type has no method bar
# Characters 98-99: # Characters 98-99:
(x:<foo:int;bar:int>) (x:<foo:int;bar:int>)
^ ^
Error: This expression has type t = < foo : int; .. > Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int > but an expression was expected of type < bar : int; foo : int >
Type ex#19 = < bar : int; .. > is not compatible with type Type ex#27 = < bar : int; .. > is not compatible with type
< bar : int > < bar : int >
The first object type has an abstract row, it cannot be closed The first object type has an abstract row, it cannot be closed
# Characters 98-99: # Characters 98-99:
@ -324,7 +361,7 @@ Error: This expression has type t = < foo : int; .. >
^ ^
Error: This expression has type < bar : int; foo : int; .. > Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a but an expression was expected of type 'a
The type constructor ex#22 would escape its scope The type constructor ex#30 would escape its scope
# val g : 'a -> 'a int_foo -> 'a int_bar -> 'a = <fun> # val g : 'a -> 'a int_foo -> 'a int_bar -> 'a = <fun>
# val g : 'a -> 'a int_foo -> 'a int_bar -> 'a * int * int = <fun> # val g : 'a -> 'a int_foo -> 'a int_bar -> 'a * int * int = <fun>
# type 'a ty = Int : int -> int ty # type 'a ty = Int : int -> int ty

49
testsuite/tests/typing-gadts/test.ml.reference
View File

@ -65,6 +65,43 @@ module PR6862 :
type _ opt = Just : 'a -> 'a opt | Nothing : 'a opt type _ opt = Just : 'a -> 'a opt | Nothing : 'a opt
class d : int opt -> object method x : int end class d : int opt -> object method x : int end
end end
# module Exhaustive2 :
sig type _ t = Int : int t val f : bool t option -> unit end
# module PR6220 :
sig
type 'a t = I : int t | F : float t
val f : int t -> int
val g : int t -> int
end
# module PR6403 :
sig
type (_, _) eq = Refl : ('a, 'a) eq
type empty = { bottom : 'a. 'a; }
type ('a, 'b) sum = Left of 'a | Right of 'b
val notequal : ((int, bool) eq, empty) sum -> empty
end
# module PR6437 :
sig
type ('a, 'b) ctx =
Nil : (unit, unit) ctx
| Cons : ('a, 'b) ctx -> ('a * unit, 'b * unit) ctx
type 'a var = O : ('a * unit) var | S : 'a var -> ('a * unit) var
val f : ('g1, 'g2) ctx * 'g1 var -> 'g2 var
end
# Characters 175-221:
....match x with
| String s -> print_endline s.................
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Any
module PR6801 :
sig
type _ value =
String : string -> string value
| Float : float -> float value
| Any
val print_string_value : string value -> unit
end
# Characters 118-119: # Characters 118-119:
let eval (D x) = x let eval (D x) = x
^ ^
@ -73,7 +110,7 @@ Error: This expression has type a#2 t but an expression was expected of type
The type constructor a#2 would escape its scope The type constructor a#2 would escape its scope
# module Rectype : # module Rectype :
sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end sig type (_, _) t = C : ('a, 'a) t val f : ('s, 's * 's) t -> unit end
# Characters 178-186: # Characters 180-188:
| (IntLit _ | BoolLit _) -> () | (IntLit _ | BoolLit _) -> ()
^^^^^^^^ ^^^^^^^^
Error: This pattern matches values of type int t Error: This pattern matches values of type int t
@ -252,7 +289,7 @@ val f : 'a ty -> 'a t -> int = <fun>
| TA, D z -> z | TA, D z -> z
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
(TE TC, D [| |]) (TE TC, D [| 0. |])
val f : 'a ty -> 'a t -> int = <fun> val f : 'a ty -> 'a t -> int = <fun>
# Characters 147-154: # Characters 147-154:
| D [|1.0|], TE TC -> 14 | D [|1.0|], TE TC -> 14
@ -274,7 +311,7 @@ Error: This pattern matches values of type 'a array
| {left=TA; right=D z} -> z | {left=TA; right=D z} -> z
Warning 8: this pattern-matching is not exhaustive. Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: Here is an example of a value that is not matched:
{left=TE TC; right=D [| |]} {left=TE TC; right=D [| 0. |]}
type ('a, 'b) pair = { left : 'a; right : 'b; } type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty -> 'a t -> int = <fun> val f : 'a ty -> 'a t -> int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end # module M : sig type 'a t val eq : ('a t, 'b t) eq end
@ -296,14 +333,14 @@ type _ int_bar = IB_constr : < bar : int; .. > int_bar
^ ^
Error: This expression has type t = < foo : int; .. > Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < foo : int > but an expression was expected of type < foo : int >
Type ex#17 = < bar : int; .. > is not compatible with type < > Type ex#25 = < bar : int; .. > is not compatible with type < >
The second object type has no method bar The second object type has no method bar
# Characters 98-99: # Characters 98-99:
(x:<foo:int;bar:int>) (x:<foo:int;bar:int>)
^ ^
Error: This expression has type t = < foo : int; .. > Error: This expression has type t = < foo : int; .. >
but an expression was expected of type < bar : int; foo : int > but an expression was expected of type < bar : int; foo : int >
Type ex#19 = < bar : int; .. > is not compatible with type Type ex#27 = < bar : int; .. > is not compatible with type
< bar : int > < bar : int >
The first object type has an abstract row, it cannot be closed The first object type has an abstract row, it cannot be closed
# Characters 98-99: # Characters 98-99:
@ -311,7 +348,7 @@ Error: This expression has type t = < foo : int; .. >
^ ^
Error: This expression has type < bar : int; foo : int; .. > Error: This expression has type < bar : int; foo : int; .. >
but an expression was expected of type 'a but an expression was expected of type 'a
The type constructor ex#22 would escape its scope The type constructor ex#30 would escape its scope
# val g : 'a -> 'a int_foo -> 'a int_bar -> 'a = <fun> # val g : 'a -> 'a int_foo -> 'a int_bar -> 'a = <fun>
# val g : 'a -> 'a int_foo -> 'a int_bar -> 'a * int * int = <fun> # val g : 'a -> 'a int_foo -> 'a int_bar -> 'a * int * int = <fun>
# type 'a ty = Int : int -> int ty # type 'a ty = Int : int -> int ty

14
typing/ctype.ml
View File

@ -116,6 +116,20 @@ let nongen_level = ref 0
let global_level = ref 1 let global_level = ref 1
let saved_level = ref [] let saved_level = ref []
type levels =
{ current_level: int; nongen_level: int; global_level: int;
saved_level: (int * int) list; }
let save_levels () =
{ current_level = !current_level;
nongen_level = !nongen_level;
global_level = !global_level;
saved_level = !saved_level }
let set_levels l =
current_level := l.current_level;
nongen_level := l.nongen_level;
global_level := l.global_level;
saved_level := l.saved_level
let get_current_level () = !current_level let get_current_level () = !current_level
let init_def level = current_level := level; nongen_level := level let init_def level = current_level := level; nongen_level := level
let begin_def () = let begin_def () =

5
typing/ctype.mli
View File

@ -37,6 +37,11 @@ val reset_global_level: unit -> unit
val increase_global_level: unit -> int val increase_global_level: unit -> int
val restore_global_level: int -> unit val restore_global_level: int -> unit
(* This pair of functions is only used in Typetexp *) (* This pair of functions is only used in Typetexp *)
type levels =
{ current_level: int; nongen_level: int; global_level: int;
saved_level: (int * int) list; }
val save_levels: unit -> levels
val set_levels: levels -> unit
val newty: type_desc -> type_expr val newty: type_desc -> type_expr
val newvar: ?name:string -> unit -> type_expr val newvar: ?name:string -> unit -> type_expr

258
typing/parmatch.ml
View File

@ -621,18 +621,10 @@ let clean_env env =
in in
loop env loop env
let full_match ignore_generalized closing env = match env with let full_match closing env = match env with
| ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ -> | ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ ->
if c.cstr_consts < 0 then false (* extensions *) if c.cstr_consts < 0 then false (* extensions *)
else else List.length env = c.cstr_consts + c.cstr_nonconsts
if ignore_generalized then
(* remove generalized constructors;
those cases will be handled separately *)
let env = clean_env env in
List.length env = c.cstr_normal
else
List.length env = c.cstr_consts + c.cstr_nonconsts
| ({pat_desc = Tpat_variant _} as p,_) :: _ -> | ({pat_desc = Tpat_variant _} as p,_) :: _ ->
let fields = let fields =
List.map List.map
@ -666,11 +658,6 @@ let full_match ignore_generalized closing env = match env with
| ({pat_desc = Tpat_lazy(_)},_) :: _ -> true | ({pat_desc = Tpat_lazy(_)},_) :: _ -> true
| _ -> fatal_error "Parmatch.full_match" | _ -> fatal_error "Parmatch.full_match"
let full_match_gadt env = match env with
| ({pat_desc = Tpat_construct(_,c,_);pat_type=typ},_) :: _ ->
List.length env = c.cstr_consts + c.cstr_nonconsts
| _ -> true
let extendable_match env = match env with let extendable_match env = match env with
| ({pat_desc=Tpat_construct(_,{cstr_tag=(Cstr_constant _|Cstr_block _)},_)} | ({pat_desc=Tpat_construct(_,{cstr_tag=(Cstr_constant _|Cstr_block _)},_)}
as p,_) :: _ -> as p,_) :: _ ->
@ -715,19 +702,34 @@ let complete_tags nconsts nconstrs tags =
(* build a pattern from a constructor list *) (* build a pattern from a constructor list *)
let pat_of_constr ex_pat cstr = let pat_of_constr ex_pat cstr =
{ex_pat with pat_desc = {ex_pat with pat_desc =
Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"), Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
cstr,omegas cstr.cstr_arity)} cstr, omegas cstr.cstr_arity)}
let rec pat_of_constrs ex_pat = function let rec orify_many = function
| [] -> raise Empty | [] -> assert false
| [cstr] -> pat_of_constr ex_pat cstr | [x] -> x
| cstr::rem -> | x :: xs ->
{ex_pat with make_pat (Tpat_or (x, orify_many xs, None)) x.pat_type x.pat_env
pat_desc=
Tpat_or let pat_of_constrs ex_pat cstrs =
(pat_of_constr ex_pat cstr, if cstrs = [] then raise Empty else
pat_of_constrs ex_pat rem, None)} orify_many (List.map (pat_of_constr ex_pat) cstrs)
let pats_of_type env ty =
let ty' = Ctype.expand_head env ty in
match ty'.desc with
| Tconstr (path, _, _) ->
begin match Env.find_type path env with
| {type_kind = Type_variant cl}
when List.for_all (fun cd -> cd.Types.cd_res <> None) cl ->
let cstrs = fst (Env.find_type_descrs path env) in
List.map
(pat_of_constr {omega with pat_type=ty; pat_env=env})
cstrs
| _ -> [omega]
end
| _ -> [omega]
let rec get_variant_constructors env ty = let rec get_variant_constructors env ty =
match (Ctype.repr ty).desc with match (Ctype.repr ty).desc with
@ -756,11 +758,12 @@ let complete_constrs p all_tags =
| Tpat_construct (_,c,_) -> | Tpat_construct (_,c,_) ->
let not_tags = complete_tags c.cstr_consts c.cstr_nonconsts all_tags in let not_tags = complete_tags c.cstr_consts c.cstr_nonconsts all_tags in
let constrs = get_variant_constructors p.pat_env c.cstr_res in let constrs = get_variant_constructors p.pat_env c.cstr_res in
map_filter let others =
(fun cnstr -> List.filter (fun cnstr -> List.mem cnstr.cstr_tag not_tags) constrs in
if List.mem cnstr.cstr_tag not_tags then Some cnstr else None) let const, nonconst =
constrs List.partition (fun cnstr -> cnstr.cstr_arity = 0) others in
| _ -> fatal_error "Parmatch.complete_constr" const @ nonconst
| _ -> fatal_error "Parmatch.complete_constrs"
(* Auxiliary for build_other *) (* Auxiliary for build_other *)
@ -778,7 +781,7 @@ let build_other_constant proj make first next p env =
in the first column of env in the first column of env
*) *)
let build_other ext env = match env with let build_other ext env = match env with
| ({pat_desc = Tpat_construct (lid, | ({pat_desc = Tpat_construct (lid,
({cstr_tag=Cstr_extension _} as c),_)},_) :: _ -> ({cstr_tag=Cstr_extension _} as c),_)},_) :: _ ->
let c = {c with cstr_name = "*extension*"} in let c = {c with cstr_name = "*extension*"} in
@ -902,20 +905,6 @@ let build_other ext env = match env with
| [] -> omega | [] -> omega
| _ -> omega | _ -> omega
let build_other_gadt ext env =
match env with
| ({pat_desc = Tpat_construct _} as p,_) :: _ ->
let get_tag = function
| {pat_desc = Tpat_construct (_,c,_)} -> c.cstr_tag
| _ -> fatal_error "Parmatch.get_tag" in
let all_tags = List.map (fun (p,_) -> get_tag p) env in
let cnstrs = complete_constrs p all_tags in
let pats = List.map (pat_of_constr p) cnstrs in
(* List.iter (Format.eprintf "%a@." top_pretty) pats;
Format.eprintf "@.@."; *)
pats
| _ -> assert false
(* (*
Core function : Core function :
Is the last row of pattern matrix pss + qs satisfiable ? Is the last row of pattern matrix pss + qs satisfiable ?
@ -956,7 +945,7 @@ let rec satisfiable pss qs = match pss with
(* first column of pss is made of variables only *) (* first column of pss is made of variables only *)
| [] -> satisfiable (filter_extra pss) qs | [] -> satisfiable (filter_extra pss) qs
| constrs -> | constrs ->
if full_match false false constrs then if full_match false constrs then
List.exists List.exists
(fun (p,pss) -> (fun (p,pss) ->
not (is_absent_pat p) && not (is_absent_pat p) &&
@ -981,15 +970,6 @@ type 'a result =
| Rnone (* No matching value *) | Rnone (* No matching value *)
| Rsome of 'a (* This matching value *) | Rsome of 'a (* This matching value *)
let rec orify_many =
let orify x y =
make_pat (Tpat_or (x, y, None)) x.pat_type x.pat_env
in
function
| [] -> assert false
| [x] -> x
| x :: xs -> orify x (orify_many xs)
let rec try_many f = function let rec try_many f = function
| [] -> Rnone | [] -> Rnone
| (p,pss)::rest -> | (p,pss)::rest ->
@ -1008,6 +988,7 @@ let rec try_many_gadt f = function
| (p,pss)::rest -> | (p,pss)::rest ->
rappend (f (p, pss)) (try_many_gadt f rest) rappend (f (p, pss)) (try_many_gadt f rest)
(*
let rec exhaust ext pss n = match pss with let rec exhaust ext pss n = match pss with
| [] -> Rsome (omegas n) | [] -> Rsome (omegas n)
| []::_ -> Rnone | []::_ -> Rnone
@ -1068,7 +1049,7 @@ let combinations f lst lst' =
| x :: xs -> iter2 x lst' @ iter xs | x :: xs -> iter2 x lst' @ iter xs
in in
iter lst iter lst
*)
(* (*
let print_pat pat = let print_pat pat =
let rec string_of_pat pat = let rec string_of_pat pat =
@ -1119,7 +1100,7 @@ let rec exhaust_gadt (ext:Path.t option) pss n = match pss with
| r -> r in | r -> r in
let before = try_many_gadt try_non_omega constrs in let before = try_many_gadt try_non_omega constrs in
if if
full_match_gadt constrs && not (should_extend ext constrs) full_match false constrs && not (should_extend ext constrs)
then then
before before
else else
@ -1136,13 +1117,8 @@ let rec exhaust_gadt (ext:Path.t option) pss n = match pss with
| Rnone -> before | Rnone -> before
| Rsome r -> | Rsome r ->
try try
let missing_trailing = build_other_gadt ext constrs in let p = build_other ext constrs in
let dug = let dug = List.map (fun tail -> p :: tail) r in
combinations
(fun head tail -> head :: tail)
missing_trailing
r
in
match before with match before with
| Rnone -> Rsome dug | Rnone -> Rsome dug
| Rsome x -> Rsome (x @ dug) | Rsome x -> Rsome (x @ dug)
@ -1193,12 +1169,12 @@ let rec pressure_variants tdefs = function
try_non_omega rem && ok try_non_omega rem && ok
| [] -> true | [] -> true
in in
if full_match true (tdefs=None) constrs then if full_match (tdefs=None) constrs then
try_non_omega constrs try_non_omega constrs
else if tdefs = None then else if tdefs = None then
pressure_variants None (filter_extra pss) pressure_variants None (filter_extra pss)
else else
let full = full_match true true constrs in let full = full_match true constrs in
let ok = let ok =
if full then try_non_omega constrs if full then try_non_omega constrs
else try_non_omega (filter_all q0 (mark_partial pss)) else try_non_omega (filter_all q0 (mark_partial pss))
@ -1662,119 +1638,71 @@ let check_partial_all v casel =
(* Exhaustiveness check *) (* Exhaustiveness check *)
(************************) (************************)
let rec get_first f =
function
| [] -> None
| x :: xs ->
match f x with
| None -> get_first f xs
| x -> x
(* conversion from Typedtree.pattern to Parsetree.pattern list *) (* conversion from Typedtree.pattern to Parsetree.pattern list *)
module Conv = struct module Conv = struct
open Parsetree open Parsetree
let mkpat desc = Ast_helper.Pat.mk desc let mkpat desc = Ast_helper.Pat.mk desc
let rec select : 'a list list -> 'a list list =
function
| xs :: [] -> List.map (fun y -> [y]) xs
| (x::xs)::ys ->
List.map
(fun lst -> x :: lst)
(select ys)
@
select (xs::ys)
| _ -> []
let name_counter = ref 0 let name_counter = ref 0
let fresh name = let fresh name =
let current = !name_counter in let current = !name_counter in
name_counter := !name_counter + 1; name_counter := !name_counter + 1;
"#$" ^ name ^ string_of_int current "#$" ^ name ^ string_of_int current
let conv (typed: Typedtree.pattern) : let conv typed =
Parsetree.pattern list * let constrs = Hashtbl.create 7 in
(string, Types.constructor_description) Hashtbl.t * let labels = Hashtbl.create 7 in
(string, Types.label_description) Hashtbl.t
=
let constrs = Hashtbl.create 0 in
let labels = Hashtbl.create 0 in
let rec loop pat = let rec loop pat =
match pat.pat_desc with match pat.pat_desc with
Tpat_or (a,b,_) -> Tpat_or (pa,pb,_) ->
loop a @ loop b mkpat (Ppat_or (loop pa, loop pb))
| Tpat_any | Tpat_constant _ | Tpat_var _ -> | Tpat_any
[mkpat Ppat_any] | Tpat_var _ ->
mkpat Ppat_any
| Tpat_constant c ->
mkpat (Ppat_constant c)
| Tpat_alias (p,_,_) -> loop p | Tpat_alias (p,_,_) -> loop p
| Tpat_tuple lst -> | Tpat_tuple lst ->
let results = select (List.map loop lst) in mkpat (Ppat_tuple (List.map loop lst))
List.map | Tpat_construct (cstr_lid, cstr, lst) ->
(fun lst -> mkpat (Ppat_tuple lst))
results
| Tpat_construct (cstr_lid, cstr,lst) ->
let id = fresh cstr.cstr_name in let id = fresh cstr.cstr_name in
let lid = { cstr_lid with txt = Longident.Lident id } in let lid = { cstr_lid with txt = Longident.Lident id } in
Hashtbl.add constrs id cstr; Hashtbl.add constrs id cstr;
let results = select (List.map loop lst) in let arg =
begin match lst with match List.map loop lst with
[] -> | [] -> None
[mkpat (Ppat_construct(lid, None))] | [p] -> Some p
| _ -> | lst -> Some (mkpat (Ppat_tuple lst))
List.map
(fun lst ->
let arg =
match lst with
[] -> assert false
| [x] -> Some x
| _ -> Some (mkpat (Ppat_tuple lst))
in
mkpat (Ppat_construct(lid, arg)))
results
end
| Tpat_variant(label,p_opt,row_desc) ->
begin match p_opt with
| None ->
[mkpat (Ppat_variant(label, None))]
| Some p ->
let results = loop p in
List.map
(fun p ->
mkpat (Ppat_variant(label, Some p)))
results
end
| Tpat_record (subpatterns, _closed_flag) ->
let pats =
select
(List.map (fun (_,_,x) -> loop x) subpatterns)
in in
let label_idents = mkpat (Ppat_construct(lid, arg))
List.map | Tpat_variant(label,p_opt,row_desc) ->
(fun (_,lbl,_) -> let arg = Misc.may_map loop p_opt in
mkpat (Ppat_variant(label, arg))
| Tpat_record (subpatterns, _closed_flag) ->
let fields =
List.map
(fun (_, lbl, p) ->
let id = fresh lbl.lbl_name in let id = fresh lbl.lbl_name in
Hashtbl.add labels id lbl; Hashtbl.add labels id lbl;
Longident.Lident id) (mknoloc (Longident.Lident id), loop p))
subpatterns subpatterns
in in
List.map mkpat (Ppat_record (fields, Open))
(fun lst ->
let lst = List.map2 (fun lid pat ->
(mknoloc lid, pat)
) label_idents lst in
mkpat (Ppat_record (lst, Open)))
pats
| Tpat_array lst -> | Tpat_array lst ->
let results = select (List.map loop lst) in mkpat (Ppat_array (List.map loop lst))
List.map (fun lst -> mkpat (Ppat_array lst)) results
| Tpat_lazy p -> | Tpat_lazy p ->
let results = loop p in mkpat (Ppat_lazy (loop p))
List.map (fun p -> mkpat (Ppat_lazy p)) results
in in
let ps = loop typed in let ps = loop typed in
(ps, constrs, labels) (ps, constrs, labels)
end end
let ppat_of_type env ty =
match pats_of_type env ty with
[{pat_desc = Tpat_any}] ->
(Conv.mkpat Parsetree.Ppat_any, Hashtbl.create 0, Hashtbl.create 0)
| pats ->
Conv.conv (orify_many pats)
let do_check_partial ?pred exhaust loc casel pss = match pss with let do_check_partial ?pred exhaust loc casel pss = match pss with
| [] -> | [] ->
@ -1798,12 +1726,12 @@ let do_check_partial ?pred exhaust loc casel pss = match pss with
let v = let v =
match pred with match pred with
| Some pred -> | Some pred ->
let (patterns,constrs,labels) = Conv.conv u in let (pattern,constrs,labels) = Conv.conv u in
(* Hashtbl.iter (fun s (path, _) -> (* Hashtbl.iter (fun s (path, _) ->
Printf.fprintf stderr "CONV: %s -> %s \n%!" s (Path.name path)) Printf.fprintf stderr "CONV: %s -> %s \n%!" s (Path.name path))
constrs constrs
; *) ; *)
get_first (pred constrs labels) patterns pred constrs labels pattern
| None -> Some u | None -> Some u
in in
begin match v with begin match v with
@ -1839,8 +1767,10 @@ let do_check_partial ?pred exhaust loc casel pss = match pss with
fatal_error "Parmatch.check_partial" fatal_error "Parmatch.check_partial"
end end
(*
let do_check_partial_normal loc casel pss = let do_check_partial_normal loc casel pss =
do_check_partial exhaust loc casel pss do_check_partial exhaust loc casel pss
*)
let do_check_partial_gadt pred loc casel pss = let do_check_partial_gadt pred loc casel pss =
do_check_partial ~pred exhaust_gadt loc casel pss do_check_partial ~pred exhaust_gadt loc casel pss
@ -1916,7 +1846,7 @@ let do_check_fragile_param exhaust loc casel pss =
| Rsome _ -> ()) | Rsome _ -> ())
exts exts
let do_check_fragile_normal = do_check_fragile_param exhaust (*let do_check_fragile_normal = do_check_fragile_param exhaust*)
let do_check_fragile_gadt = do_check_fragile_param exhaust_gadt let do_check_fragile_gadt = do_check_fragile_param exhaust_gadt
(********************************) (********************************)
@ -2012,19 +1942,11 @@ let check_partial_param do_check_partial do_check_fragile loc casel =
end else end else
Partial Partial
let check_partial = (*let check_partial =
check_partial_param check_partial_param
do_check_partial_normal do_check_partial_normal
do_check_fragile_normal do_check_fragile_normal*)
let check_partial_gadt pred loc casel = let check_partial_gadt pred loc casel =
(*ignores GADT constructors *) check_partial_param (do_check_partial_gadt pred)
let first_check = check_partial loc casel in do_check_fragile_gadt loc casel
match first_check with
| Partial -> Partial
| Total ->
(* checks for missing GADT constructors *)
(* let casel =
match casel with [] -> [] | a :: l -> a :: l @ [a] in *)
check_partial_param (do_check_partial_gadt pred)
do_check_fragile_gadt loc casel

5
typing/parmatch.mli
View File

@ -51,6 +51,11 @@ val set_args_erase_mutable : pattern -> pattern list -> pattern list
val pat_of_constr : pattern -> constructor_description -> pattern val pat_of_constr : pattern -> constructor_description -> pattern
val complete_constrs : val complete_constrs :
pattern -> constructor_tag list -> constructor_description list pattern -> constructor_tag list -> constructor_description list
val ppat_of_type :
Env.t -> type_expr ->
Parsetree.pattern *
(string, constructor_description) Hashtbl.t *
(string, label_description) Hashtbl.t
val pressure_variants: Env.t -> pattern list -> unit val pressure_variants: Env.t -> pattern list -> unit
val check_partial_gadt: val check_partial_gadt:

237
typing/typecore.ml
View File

@ -827,7 +827,11 @@ let rec find_record_qual = function
| ({ txt = Longident.Ldot (modname, _) }, _) :: _ -> Some modname | ({ txt = Longident.Ldot (modname, _) }, _) :: _ -> Some modname
| _ :: rest -> find_record_qual rest | _ :: rest -> find_record_qual rest
let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list = let map_fold_cont f xs k =
List.fold_right (fun x k ys -> f x (fun y -> k (y :: ys)))
xs (fun ys -> k (List.rev ys)) []
let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list k =
let lbl_a_list = let lbl_a_list =
match lid_a_list, labels with match lid_a_list, labels with
({txt=Longident.Lident s}, _)::_, Some labels when Hashtbl.mem labels s -> ({txt=Longident.Lident s}, _)::_, Some labels when Hashtbl.mem labels s ->
@ -857,7 +861,7 @@ let type_label_a_list ?labels loc closed env type_lbl_a opath lid_a_list =
(fun (_,lbl1,_) (_,lbl2,_) -> compare lbl1.lbl_pos lbl2.lbl_pos) (fun (_,lbl1,_) (_,lbl2,_) -> compare lbl1.lbl_pos lbl2.lbl_pos)
lbl_a_list lbl_a_list
in in
List.map type_lbl_a lbl_a_list map_fold_cont type_lbl_a lbl_a_list k
;; ;;
(* Checks over the labels mentioned in a record pattern: (* Checks over the labels mentioned in a record pattern:
@ -917,32 +921,59 @@ type type_pat_mode =
| Normal | Normal
| Inside_or | Inside_or
(* Remember current state for backtracking.
No variable information, as we only backtrack on
patterns without variables (cf. assert statements). *)
type state =
{ snapshot: Btype.snapshot;
levels: Ctype.levels;
env: Env.t; }
let save_state env =
{ snapshot = Btype.snapshot ();
levels = Ctype.save_levels ();
env = !env; }
let set_state s env =
Btype.backtrack s.snapshot;
Ctype.set_levels s.levels;
env := s.env
(* type_pat propagates the expected type as well as maps for (* type_pat propagates the expected type as well as maps for
constructors and labels. constructors and labels.
Unification may update the typing environment. *) Unification may update the typing environment. *)
let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty = (* constrs <> None => called from parmatch: backtrack on or-patterns
let type_pat ?(mode=mode) ?(env=env) = labels <> None => explode Ppat_any for gadts *)
let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty k =
let type_pat ?(constrs=constrs) ?(labels=labels) ?(mode=mode) ?(env=env) =
type_pat ~constrs ~labels ~no_existentials ~mode ~env in type_pat ~constrs ~labels ~no_existentials ~mode ~env in
let loc = sp.ppat_loc in let loc = sp.ppat_loc in
let rp k x : pattern = if constrs = None then k (rp x) else k x in
match sp.ppat_desc with match sp.ppat_desc with
Ppat_any -> Ppat_any ->
rp { let k' d = rp k {
pat_desc = Tpat_any; pat_desc = d;
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env }
in
if labels <> None then
let (sp, constrs, labels) = Parmatch.ppat_of_type !env expected_ty in
if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any
else type_pat ~constrs:(Some constrs) ~labels:None sp expected_ty k
else k' Tpat_any
| Ppat_var name -> | Ppat_var name ->
assert (constrs = None);
let id = enter_variable loc name expected_ty in let id = enter_variable loc name expected_ty in
rp { rp k {
pat_desc = Tpat_var (id, name); pat_desc = Tpat_var (id, name);
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env }
| Ppat_unpack name -> | Ppat_unpack name ->
assert (constrs = None);
let id = enter_variable loc name expected_ty ~is_module:true in let id = enter_variable loc name expected_ty ~is_module:true in
rp { rp k {
pat_desc = Tpat_var (id, name); pat_desc = Tpat_var (id, name);
pat_loc = sp.ppat_loc; pat_loc = sp.ppat_loc;
pat_extra=[Tpat_unpack, loc, sp.ppat_attributes]; pat_extra=[Tpat_unpack, loc, sp.ppat_attributes];
@ -952,6 +983,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
| Ppat_constraint({ppat_desc=Ppat_var name; ppat_loc=lloc}, | Ppat_constraint({ppat_desc=Ppat_var name; ppat_loc=lloc},
({ptyp_desc=Ptyp_poly _} as sty)) -> ({ptyp_desc=Ptyp_poly _} as sty)) ->
(* explicitly polymorphic type *) (* explicitly polymorphic type *)
assert (constrs = None);
let cty, force = Typetexp.transl_simple_type_delayed !env sty in let cty, force = Typetexp.transl_simple_type_delayed !env sty in
let ty = cty.ctyp_type in let ty = cty.ctyp_type in
unify_pat_types lloc !env ty expected_ty; unify_pat_types lloc !env ty expected_ty;
@ -963,7 +995,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
end_def (); end_def ();
generalize ty'; generalize ty';
let id = enter_variable lloc name ty' in let id = enter_variable lloc name ty' in
rp { rp k {
pat_desc = Tpat_var (id, name); pat_desc = Tpat_var (id, name);
pat_loc = lloc; pat_loc = lloc;
pat_extra = [Tpat_constraint cty, loc, sp.ppat_attributes]; pat_extra = [Tpat_constraint cty, loc, sp.ppat_attributes];
@ -974,21 +1006,22 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
| _ -> assert false | _ -> assert false
end end
| Ppat_alias(sq, name) -> | Ppat_alias(sq, name) ->
let q = type_pat sq expected_ty in assert (constrs = None);
begin_def (); type_pat sq expected_ty (fun q ->
let ty_var = build_as_type !env q in begin_def ();
end_def (); let ty_var = build_as_type !env q in
generalize ty_var; end_def ();
let id = enter_variable ~is_as_variable:true loc name ty_var in generalize ty_var;
rp { let id = enter_variable ~is_as_variable:true loc name ty_var in
pat_desc = Tpat_alias(q, id, name); rp k {
pat_loc = loc; pat_extra=[]; pat_desc = Tpat_alias(q, id, name);
pat_type = q.pat_type; pat_loc = loc; pat_extra=[];
pat_attributes = sp.ppat_attributes; pat_type = q.pat_type;
pat_env = !env } pat_attributes = sp.ppat_attributes;
pat_env = !env })
| Ppat_constant cst -> | Ppat_constant cst ->
unify_pat_types loc !env (type_constant cst) expected_ty; unify_pat_types loc !env (type_constant cst) expected_ty;
rp { rp k {
pat_desc = Tpat_constant cst; pat_desc = Tpat_constant cst;
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
@ -1006,7 +1039,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
in in
let p = if c1 <= c2 then loop c1 c2 else loop c2 c1 in let p = if c1 <= c2 then loop c1 c2 else loop c2 c1 in
let p = {p with ppat_loc=loc} in let p = {p with ppat_loc=loc} in
type_pat p expected_ty type_pat ~labels:None p expected_ty k
(* TODO: record 'extra' to remember about interval *) (* TODO: record 'extra' to remember about interval *)
| Ppat_interval _ -> | Ppat_interval _ ->
raise (Error (loc, !env, Invalid_interval)) raise (Error (loc, !env, Invalid_interval))
@ -1016,13 +1049,13 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
let spl_ann = List.map (fun p -> (p,newvar ())) spl in let spl_ann = List.map (fun p -> (p,newvar ())) spl in
let ty = newty (Ttuple(List.map snd spl_ann)) in let ty = newty (Ttuple(List.map snd spl_ann)) in
unify_pat_types loc !env ty expected_ty; unify_pat_types loc !env ty expected_ty;
let pl = List.map (fun (p,t) -> type_pat p t) spl_ann in map_fold_cont (fun (p,t) -> type_pat p t) spl_ann (fun pl ->
rp { rp k {
pat_desc = Tpat_tuple pl; pat_desc = Tpat_tuple pl;
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env })
| Ppat_construct(lid, sarg) -> | Ppat_construct(lid, sarg) ->
let opath = let opath =
try try
@ -1090,13 +1123,14 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
in in
if constr.cstr_inlined <> None then List.iter check_non_escaping sargs; if constr.cstr_inlined <> None then List.iter check_non_escaping sargs;
let args = List.map2 (fun p t -> type_pat p t) sargs ty_args in map_fold_cont (fun (p,t) -> type_pat p t) (List.combine sargs ty_args)
rp { (fun args ->
pat_desc=Tpat_construct(lid, constr, args); rp k {
pat_loc = loc; pat_extra=[]; pat_desc=Tpat_construct(lid, constr, args);
pat_type = expected_ty; pat_loc = loc; pat_extra=[];
pat_attributes = sp.ppat_attributes; pat_type = expected_ty;
pat_env = !env } pat_attributes = sp.ppat_attributes;
pat_env = !env })
| Ppat_variant(l, sarg) -> | Ppat_variant(l, sarg) ->
let arg_type = match sarg with None -> [] | Some _ -> [newvar()] in let arg_type = match sarg with None -> [] | Some _ -> [newvar()] in
let row = { row_fields = let row = { row_fields =
@ -1107,18 +1141,19 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
row_fixed = false; row_fixed = false;
row_name = None } in row_name = None } in
unify_pat_types loc !env (newty (Tvariant row)) expected_ty; unify_pat_types loc !env (newty (Tvariant row)) expected_ty;
let arg = let k arg =
(* PR#6235: propagate type information *) rp k {
match sarg, arg_type with
Some p, [ty] -> Some (type_pat p ty)
| _ -> None
in
rp {
pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()}); pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()});
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env }
in begin
(* PR#6235: propagate type information *)
match sarg, arg_type with
Some p, [ty] -> type_pat p ty (fun p -> k (Some p))
| _ -> k None
end
| Ppat_record(lid_sp_list, closed) -> | Ppat_record(lid_sp_list, closed) ->
if lid_sp_list = [] then if lid_sp_list = [] then
Syntaxerr.ill_formed_ast loc "Records cannot be empty."; Syntaxerr.ill_formed_ast loc "Records cannot be empty.";
@ -1128,7 +1163,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
Some (p0, p, true), expected_ty Some (p0, p, true), expected_ty
with Not_found -> None, newvar () with Not_found -> None, newvar ()
in in
let type_label_pat (label_lid, label, sarg) = let type_label_pat (label_lid, label, sarg) k =
begin_def (); begin_def ();
let (vars, ty_arg, ty_res) = instance_label false label in let (vars, ty_arg, ty_res) = instance_label false label in
if vars = [] then end_def (); if vars = [] then end_def ();
@ -1138,55 +1173,72 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
raise(Error(label_lid.loc, !env, raise(Error(label_lid.loc, !env,
Label_mismatch(label_lid.txt, trace))) Label_mismatch(label_lid.txt, trace)))
end; end;
let arg = type_pat sarg ty_arg in type_pat sarg ty_arg (fun arg ->
if vars <> [] then begin if vars <> [] then begin
end_def (); end_def ();
generalize ty_arg; generalize ty_arg;
List.iter generalize vars; List.iter generalize vars;
let instantiated tv = let instantiated tv =
let tv = expand_head !env tv in let tv = expand_head !env tv in
not (is_Tvar tv) || tv.level <> generic_level in not (is_Tvar tv) || tv.level <> generic_level in
if List.exists instantiated vars then if List.exists instantiated vars then
raise (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt)) raise
end; (Error(label_lid.loc, !env, Polymorphic_label label_lid.txt))
(label_lid, label, arg) end;
k (label_lid, label, arg))
in in
let lbl_pat_list = let k' k lbl_pat_list =
wrap_disambiguate "This record pattern is expected to have" expected_ty check_recordpat_labels loc lbl_pat_list closed;
(type_label_a_list ?labels loc false !env type_label_pat opath) unify_pat_types loc !env record_ty expected_ty;
lid_sp_list rp k {
in
check_recordpat_labels loc lbl_pat_list closed;
unify_pat_types loc !env record_ty expected_ty;
rp {
pat_desc = Tpat_record (lbl_pat_list, closed); pat_desc = Tpat_record (lbl_pat_list, closed);
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env }
in
if constrs = None then
k (wrap_disambiguate "This record pattern is expected to have"
expected_ty
(type_label_a_list ?labels loc false !env type_label_pat opath
lid_sp_list)
(k' (fun x -> x)))
else
type_label_a_list ?labels loc false !env type_label_pat opath
lid_sp_list (k' k)
| Ppat_array spl -> | Ppat_array spl ->
let ty_elt = newvar() in let ty_elt = newvar() in
unify_pat_types unify_pat_types
loc !env (instance_def (Predef.type_array ty_elt)) expected_ty; loc !env (instance_def (Predef.type_array ty_elt)) expected_ty;
let spl_ann = List.map (fun p -> (p,newvar())) spl in let spl_ann = List.map (fun p -> (p,newvar())) spl in
let pl = List.map (fun (p,t) -> type_pat p ty_elt) spl_ann in map_fold_cont (fun (p,t) -> type_pat p ty_elt) spl_ann (fun pl ->
rp { rp k {
pat_desc = Tpat_array pl; pat_desc = Tpat_array pl;
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env })
| Ppat_or(sp1, sp2) -> | Ppat_or(sp1, sp2) ->
if constrs <> None &&
match sp1.ppat_desc, sp2.ppat_desc with
Ppat_constant _, _ | _, Ppat_constant _ -> false
| _ -> true
then
let state = save_state env in
try type_pat sp1 expected_ty k with exn when exn <> Exit ->
set_state state env;
type_pat sp2 expected_ty k
else
let initial_pattern_variables = !pattern_variables in let initial_pattern_variables = !pattern_variables in
let p1 = type_pat ~mode:Inside_or sp1 expected_ty in let p1 = type_pat ~mode:Inside_or sp1 expected_ty (fun x -> x) in
let p1_variables = !pattern_variables in let p1_variables = !pattern_variables in
pattern_variables := initial_pattern_variables; pattern_variables := initial_pattern_variables;
let p2 = type_pat ~mode:Inside_or sp2 expected_ty in let p2 = type_pat ~mode:Inside_or sp2 expected_ty (fun x -> x) in
let p2_variables = !pattern_variables in let p2_variables = !pattern_variables in
let alpha_env = let alpha_env =
enter_orpat_variables loc !env p1_variables p2_variables in enter_orpat_variables loc !env p1_variables p2_variables in
pattern_variables := p1_variables; pattern_variables := p1_variables;
rp { rp k {
pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None); pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None);
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
@ -1196,13 +1248,13 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
let nv = newvar () in let nv = newvar () in
unify_pat_types loc !env (instance_def (Predef.type_lazy_t nv)) unify_pat_types loc !env (instance_def (Predef.type_lazy_t nv))
expected_ty; expected_ty;
let p1 = type_pat sp1 nv in type_pat sp1 nv (fun p1 ->
rp { rp k {
pat_desc = Tpat_lazy p1; pat_desc = Tpat_lazy p1;
pat_loc = loc; pat_extra=[]; pat_loc = loc; pat_extra=[];
pat_type = expected_ty; pat_type = expected_ty;
pat_attributes = sp.ppat_attributes; pat_attributes = sp.ppat_attributes;
pat_env = !env } pat_env = !env })
| Ppat_constraint(sp, sty) -> | Ppat_constraint(sp, sty) ->
(* Separate when not already separated by !principal *) (* Separate when not already separated by !principal *)
let separate = true in let separate = true in
@ -1217,27 +1269,28 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
end else ty, ty end else ty, ty
in in
unify_pat_types loc !env ty expected_ty; unify_pat_types loc !env ty expected_ty;
let p = type_pat sp expected_ty' in type_pat sp expected_ty' (fun p ->
(*Format.printf "%a@.%a@." (*Format.printf "%a@.%a@."
Printtyp.raw_type_expr ty Printtyp.raw_type_expr ty
Printtyp.raw_type_expr p.pat_type;*) Printtyp.raw_type_expr p.pat_type;*)
pattern_force := force :: !pattern_force; pattern_force := force :: !pattern_force;
let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in let extra = (Tpat_constraint cty, loc, sp.ppat_attributes) in
if separate then let p =
match p.pat_desc with if not separate then p else
Tpat_var (id,s) -> match p.pat_desc with
{p with pat_type = ty; Tpat_var (id,s) ->
pat_desc = Tpat_alias {p with pat_type = ty;
({p with pat_desc = Tpat_any; pat_attributes = []}, id,s); pat_desc = Tpat_alias
pat_extra = [extra]; ({p with pat_desc = Tpat_any; pat_attributes = []}, id,s);
} pat_extra = [extra];
| _ -> {p with pat_type = ty; }
pat_extra = extra :: p.pat_extra} | _ -> {p with pat_type = ty;
else p pat_extra = extra :: p.pat_extra}
in k p)
| Ppat_type lid -> | Ppat_type lid ->
let (path, p,ty) = build_or_pat !env loc lid.txt in let (path, p,ty) = build_or_pat !env loc lid.txt in
unify_pat_types loc !env ty expected_ty; unify_pat_types loc !env ty expected_ty;
{ p with pat_extra = k { p with pat_extra =
(Tpat_type (path, lid), loc, sp.ppat_attributes) :: p.pat_extra } (Tpat_type (path, lid), loc, sp.ppat_attributes) :: p.pat_extra }
| Ppat_exception _ -> | Ppat_exception _ ->
raise (Error (loc, !env, Exception_pattern_below_toplevel)) raise (Error (loc, !env, Exception_pattern_below_toplevel))
@ -1250,7 +1303,7 @@ let type_pat ?(allow_existentials=false) ?constrs ?labels
try try
let r = let r =
type_pat ~no_existentials:(not allow_existentials) ~constrs ~labels type_pat ~no_existentials:(not allow_existentials) ~constrs ~labels
~mode:Normal ~env sp expected_ty in ~mode:Normal ~env sp expected_ty (fun x -> x) in
iter_pattern (fun p -> p.pat_env <- !env) r; iter_pattern (fun p -> p.pat_env <- !env) r;
newtype_level := None; newtype_level := None;
r r
@ -2089,9 +2142,9 @@ and type_expect_ ?in_function ?(recarg=Rejected) env sexp ty_expected =
let lbl_exp_list = let lbl_exp_list =
wrap_disambiguate "This record expression is expected to have" ty_record wrap_disambiguate "This record expression is expected to have" ty_record
(type_label_a_list loc closed env (type_label_a_list loc closed env
(type_label_exp true env loc ty_record) (fun e k -> k (type_label_exp true env loc ty_record e))
opath) opath lid_sexp_list)
lid_sexp_list (fun x -> x)
in in
unify_exp_types loc env ty_record (instance env ty_expected); unify_exp_types loc env ty_record (instance env ty_expected);