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

do not fail when injectivity not proved in Pattern mode, use mcomp 

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11286 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Jacques Garrigue 2011-11-25 02:37:57 +00:00
parent 6c78f42d36
commit a3aad303be
8 changed files with 66 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -148,7 +148,7 @@ val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>)
^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type a * a vlist
but a pattern was expected which matches values of type
ex#42 = ex#43 * ex#44
ex#46 = ex#47 * ex#48
# type ('a, 'b) ty =
Int : (int, 'd) ty
| String : (string, 'f) ty

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

@ -148,7 +148,7 @@ val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>)
^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type a * a vlist
but a pattern was expected which matches values of type
ex#42 = ex#43 * ex#44
ex#46 = ex#47 * ex#48
# type ('a, 'b) ty =
Int : (int, 'd) ty
| String : (string, 'f) ty

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

@ -436,3 +436,21 @@ let f : type a. a ty -> a t -> int = fun x y ->
| {left=TA; right=D 0} -> -1
| {left=TA; right=D z} -> z
;; (* ok *)
(* Injectivity *)
module M : sig type 'a t val eq : ('a t, 'b t) eq end =
struct type 'a t = int let eq = Eq end
;;
let f : type a b. (a M.t, b M.t) eq -> (a, b) eq =
function Eq -> Eq (* fail *)
;;
let f : type a b. (a M.t * a, b M.t * b) eq -> (a, b) eq =
function Eq -> Eq (* ok *)
;;
let f : type a b. (a * a M.t, b * b M.t) eq -> (a, b) eq =
function Eq -> Eq (* ok *)
;;

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

@ -50,9 +50,9 @@ module Nonexhaustive :
# Characters 119-120:
let eval (D x) = x
^
Error: This expression has type ex#12 t
but an expression was expected of type ex#12 t
The type constructor ex#12 would escape its scope
Error: This expression has type ex#16 t
but an expression was expected of type ex#16 t
The type constructor ex#16 would escape its scope
# Characters 157-158:
C ->
^
@ -268,4 +268,12 @@ Here is an example of a value that is not matched:
{left=TE TC; right=D [| |]}
type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty -> 'a t -> int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end
# Characters 69-71:
function Eq -> Eq (* fail *)
^^
Error: This expression has type (a, a) eq
but an expression was expected of type (a, b) eq
# val f : ('a M.t * 'a, 'b M.t * 'b) eq -> ('a, 'b) eq = <fun>
# val f : ('a * 'a M.t, 'b * 'b M.t) eq -> ('a, 'b) eq = <fun>
#

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

@ -50,9 +50,9 @@ module Nonexhaustive :
# Characters 119-120:
let eval (D x) = x
^
Error: This expression has type ex#12 t
but an expression was expected of type ex#12 t
The type constructor ex#12 would escape its scope
Error: This expression has type ex#16 t
but an expression was expected of type ex#16 t
The type constructor ex#16 would escape its scope
# Characters 157-158:
C ->
^
@ -255,4 +255,12 @@ Here is an example of a value that is not matched:
{left=TE TC; right=D [| |]}
type ('a, 'b) pair = { left : 'a; right : 'b; }
val f : 'a ty -> 'a t -> int = <fun>
# module M : sig type 'a t val eq : ('a t, 'b t) eq end
# Characters 69-71:
function Eq -> Eq (* fail *)
^^
Error: This expression has type (a, a) eq
but an expression was expected of type (a, b) eq
# val f : ('a M.t * 'a, 'b M.t * 'b) eq -> ('a, 'b) eq = <fun>
# val f : ('a * 'a M.t, 'b * 'b M.t) eq -> ('a, 'b) eq = <fun>
#

8
testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference
View File

@ -1,10 +1,8 @@
# Characters 212-216:
# Characters 240-248:
let f (Refl : (a T.t, b T.t) eq) = (x :> b)
^^^^
Error: This pattern matches values of type (a T.t, a T.t) eq
but a pattern was expected which matches values of type
(a T.t, b T.t) eq
^^^^^^^^
Error: Type a is not a subtype of b
# Characters 36-67:
type (_, +_) eq = Refl : ('a, 'a) eq
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

8
testsuite/tests/typing-gadts/yallop_bugs.ml.reference
View File

@ -1,10 +1,8 @@
# Characters 212-216:
# Characters 240-248:
let f (Refl : (a T.t, b T.t) eq) = (x :> b)
^^^^
Error: This pattern matches values of type (a T.t, a T.t) eq
but a pattern was expected which matches values of type
(a T.t, b T.t) eq
^^^^^^^^
Error: Type a is not a subtype of b
# Characters 36-67:
type (_, +_) eq = Refl : ('a, 'a) eq
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

29
typing/ctype.ml
View File

@ -193,16 +193,21 @@ type unification_mode =
| Pattern (* unification in pattern which may add local constraints *)
let umode = ref Expression
let generate_equations = ref false
let set_mode mode f =
let old_unification_mode = !umode in
let set_mode mode ?(generate = (mode = Pattern)) f =
let old_unification_mode = !umode
and old_gen = !generate_equations in
try
umode := mode;
generate_equations := generate;
let ret = f () in
umode := old_unification_mode;
generate_equations := old_gen;
ret
with e ->
umode := old_unification_mode;
generate_equations := old_gen;
raise e
(**********************************************)
@ -2120,8 +2125,7 @@ and unify3 env t1 t1' t2 t2' =
occur_univar !env t1;
link_type t2' t1;
| _ ->
let umode = !umode in
begin match umode with
begin match !umode with
| Expression ->
occur !env t1' t2';
link_type t1' t2
@ -2140,30 +2144,33 @@ and unify3 env t1 t1' t2 t2' =
| (Ttuple tl1, Ttuple tl2) ->
unify_list env tl1 tl2
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
if umode = Expression || in_current_module p1 || in_pervasives p1
if !umode = Expression || not !generate_equations
|| in_current_module p1 || in_pervasives p1
|| is_datatype (Env.find_type p1 !env)
then unify_list env tl1 tl2
else set_mode Expression (fun () -> unify_list env tl1 tl2)
then
unify_list env tl1 tl2
else
set_mode Pattern ~generate:false (fun () -> unify_list env tl1 tl2)
| (Tconstr ((Path.Pident p) as path,[],_),
Tconstr ((Path.Pident p') as path',[],_))
when is_abstract_newtype !env path && is_abstract_newtype !env path'
&& umode = Pattern ->
&& !generate_equations ->
let source,destination =
if find_newtype_level !env path > find_newtype_level !env path'
then p,t2'
else p',t1'
in add_gadt_equation env source destination
| (Tconstr ((Path.Pident p) as path,[],_), _)
when is_abstract_newtype !env path && umode = Pattern ->
when is_abstract_newtype !env path && !generate_equations ->
reify env t2';
local_non_recursive_abbrev !env (Path.Pident p) t2';
add_gadt_equation env p t2'
| (_, Tconstr ((Path.Pident p) as path,[],_))
when is_abstract_newtype !env path && umode = Pattern ->
when is_abstract_newtype !env path && !generate_equations ->
reify env t1' ;
local_non_recursive_abbrev !env (Path.Pident p) t1';
add_gadt_equation env p t1'
| (Tconstr (p1,_,_), Tconstr (p2,_,_)) when umode = Pattern ->
| (Tconstr (_,[],_), _) | (_, Tconstr (_,[],_)) when !umode = Pattern ->
reify env t1';
reify env t2';
mcomp !env t1' t2'