From 04968cc2e6bd6f97beda87440ba1569f2ffb4815 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 10 Mar 2011 06:27:24 +0000 Subject: [PATCH] fix principality by expanding local definitions when exporting a value git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10979 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02 --- testsuite/tests/typing-gadts/test.ml | 55 ++++++++++++++----- .../typing-gadts/test.ml.principal.reference | 20 ++++++- .../tests/typing-gadts/test.ml.reference | 30 ++++++++-- typing/ctype.ml | 40 ++++++++------ typing/env.ml | 41 ++++++++++++-- typing/env.mli | 3 +- 6 files changed, 144 insertions(+), 45 deletions(-) diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml index fbc96761c..26962402f 100644 --- a/testsuite/tests/typing-gadts/test.ml +++ b/testsuite/tests/typing-gadts/test.ml @@ -131,21 +131,46 @@ module Polymorphic_variants = end ;; -module Propagation = - struct - type _ t = - IntLit : int -> int t - | BoolLit : bool -> bool t +module Propagation = struct + type _ t = + IntLit : int -> int t + | BoolLit : bool -> bool t -let check : type s. s t -> s = function - | IntLit n -> n - | BoolLit b -> b -;; -let check : type s. s t -> s = fun x -> - let r = match x with - | IntLit n -> (n : s ) - | BoolLit b -> b - in r -;; + let check : type s. s t -> s = function + | IntLit n -> n + | BoolLit b -> b + + let check : type s. s t -> s = fun x -> + let r = match x with + | IntLit n -> (n : s ) + | BoolLit b -> b + in r end ;; + +type _ t = Int : int t ;; + +let ky x y = ignore (x = y); x ;; + +let test : type a. a t -> a = fun x -> + let r = match x with Int -> ky (1 : a) 1 + in r +;; +let test : type a. a t -> a = fun x -> + let r = match x with Int -> ky 1 (1 : a) + in r +;; +let test : type a. a t -> a = fun x -> + let r = match x with Int -> (1 : a) + in r (* fails too *) +;; +let test2 : type a. a t -> a option = fun x -> + let r = ref None in + begin match x with Int -> r := Some (1 : a) end; + !r (* normalized to int option *) +;; +let test2 : type a. a t -> a option = fun x -> + let r = ref (None : a option) in + begin match x with Int -> r := Some 1 end; + !r (* ok *) +;; diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference index 0b70c140a..b08b90662 100644 --- a/testsuite/tests/typing-gadts/test.ml.principal.reference +++ b/testsuite/tests/typing-gadts/test.ml.principal.reference @@ -67,8 +67,22 @@ Error: This pattern matches values of type int t ^^^^^^^^^^^^^ Error: This pattern matches values of type ([? `A ] as 'a) * bool t but a pattern was expected which matches values of type 'a * int t -# Characters 288-289: - | BoolLit b -> b - ^ +# Characters 300-301: + | BoolLit b -> b + ^ Error: This expression has type bool but an expression was expected of type s +# type 'a t = Int : int t +# val ky : 'a -> 'a -> 'a = +# val test : 'a t -> 'a = +# Characters 87-88: + in r + ^ +Error: This expression has type int but an expression was expected of type a +# val test : 'a t -> 'a = +# Characters 122-124: + !r (* normalized to int option *) + ^^ +Error: This expression has type int option + but an expression was expected of type a option +# val test2 : 'a t -> 'a option = # diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference index 177ff66b6..6fbe77e66 100644 --- a/testsuite/tests/typing-gadts/test.ml.reference +++ b/testsuite/tests/typing-gadts/test.ml.reference @@ -66,9 +66,29 @@ Error: This pattern matches values of type int t ^^^^^^^^^^^^^ Error: This pattern matches values of type ([? `A ] as 'a) * bool t but a pattern was expected which matches values of type 'a * int t -# module Propagation : - sig - type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t - val check : 'a t -> 'a - end +# Characters 300-301: + | BoolLit b -> b + ^ +Error: This expression has type bool but an expression was expected of type + int +# type 'a t = Int : int t +# val ky : 'a -> 'a -> 'a = +# Characters 88-89: + in r + ^ +Error: This expression has type int but an expression was expected of type a +# Characters 87-88: + in r + ^ +Error: This expression has type int but an expression was expected of type a +# Characters 82-83: + in r (* fails too *) + ^ +Error: This expression has type int but an expression was expected of type a +# Characters 122-124: + !r (* normalized to int option *) + ^^ +Error: This expression has type int option + but an expression was expected of type a option +# val test2 : 'a t -> 'a option = # diff --git a/typing/ctype.ml b/typing/ctype.ml index 4d1023149..6708a0a74 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -698,16 +698,18 @@ let rec update_level env level ty = let ty = repr ty in if ty.level > level then begin begin match ty.desc with - Tconstr(p, tl, abbrev) when level < get_level env p -> + Tconstr(p, tl, abbrev) + when level < Env.map_newtype_level env (get_level env p) -> (* Try first to replace an abbreviation by its expansion. *) begin try - if is_newtype env p then raise Cannot_expand; + (* if is_newtype env p then raise Cannot_expand; *) link_type ty (!forward_try_expand_once env ty); update_level env level ty with Cannot_expand -> (* +++ Levels should be restored... *) (* Format.printf "update_level: %i < %i@." level (get_level env p); *) - raise (Unify [(ty, newvar2 level)]) + if level < get_level env p then raise (Unify [(ty, newvar2 level)]); + iter_type_expr (update_level env level) ty end | Tpackage (p, _, _) when level < get_level env p -> raise (Unify [(ty, newvar2 level)]) @@ -1699,15 +1701,16 @@ let deep_occur t0 ty = let newtype_level = ref None +let get_newtype_level () = + match !newtype_level with + | None -> assert false + | Some x -> x + (* a local constraint can be added only if the rhs of the constraint does not contain any Tvars. They need to be removed using this function *) let reify env t = - let newtype_level = - match !newtype_level with - | None -> assert false - | Some x -> x - in + let newtype_level = get_newtype_level () in let create_fresh_constr lev row = let decl = new_declaration (Some (newtype_level)) None in let name = @@ -1997,7 +2000,7 @@ and mcomp_record_description type_pairs subst env = let mcomp env t1 t2 = mcomp (TypePairs.create 4) () env t1 t2 -let get_newtype_level env path = +let find_newtype_level env path = match (Env.find_type path env).type_newtype_level with | None -> assert false | Some x -> x @@ -2128,32 +2131,35 @@ and unify3 env t1 t1' t2 t2' = when is_abstract_newtype !env path && is_abstract_newtype !env path' && umode = Pattern -> let source,destination = - if get_newtype_level !env path > get_newtype_level !env path' + if find_newtype_level !env path > find_newtype_level !env path' then p,t2' else p',t1' in let destination = duplicate_type destination in - let source_lev = get_newtype_level !env (Path.Pident source) in - let decl = new_declaration (Some source_lev) (Some destination) in - env := Env.add_local_constraint source decl !env; + let source_lev = find_newtype_level !env (Path.Pident source) in + let decl = new_declaration (Some source_lev) (Some destination) in + let newtype_level = get_newtype_level () in + env := Env.add_local_constraint source decl newtype_level !env; cleanup_abbrev () | (Tconstr ((Path.Pident p) as path,[],_), _) when is_abstract_newtype !env path && umode = Pattern -> reify env t2'; local_non_recursive_abbrev !env (Path.Pident p) t2'; let t2' = duplicate_type t2' in - let source_level = get_newtype_level !env path in + let source_level = find_newtype_level !env path in let decl = new_declaration (Some source_level) (Some t2') in - env := Env.add_local_constraint p decl !env; + let newtype_level = get_newtype_level () in + env := Env.add_local_constraint p decl newtype_level !env; cleanup_abbrev () | (_, Tconstr ((Path.Pident p) as path,[],_)) when is_abstract_newtype !env path && umode = Pattern -> reify env t1' ; local_non_recursive_abbrev !env (Path.Pident p) t1'; let t1' = duplicate_type t1' in - let source_level = get_newtype_level !env path in + let source_level = find_newtype_level !env path in let decl = new_declaration (Some source_level) (Some t1') in - env := Env.add_local_constraint p decl !env; + let newtype_level = get_newtype_level () in + env := Env.add_local_constraint p decl newtype_level !env; cleanup_abbrev () | (Tconstr (p1,_,_), Tconstr (p2,_,_)) when umode = Pattern -> reify env t1'; diff --git a/typing/env.ml b/typing/env.ml index 8ba5a7376..9812f4992 100644 --- a/typing/env.ml +++ b/typing/env.ml @@ -56,6 +56,7 @@ type t = { cltypes: (Path.t * cltype_declaration) Ident.tbl; summary: summary; local_constraints: bool; + level_map: (int * int) list; } and module_components = module_components_repr Lazy.t @@ -95,7 +96,7 @@ let empty = { modules = Ident.empty; modtypes = Ident.empty; components = Ident.empty; classes = Ident.empty; cltypes = Ident.empty; - summary = Env_empty; local_constraints = false; } + summary = Env_empty; local_constraints = false; level_map = [] } let diff_keys is_local tbl1 tbl2 = let keys2 = Ident.keys tbl2 in @@ -446,6 +447,33 @@ and lookup_class = and lookup_cltype = lookup (fun env -> env.cltypes) (fun sc -> sc.comp_cltypes) +(* Level handling *) + +(* The level map is a list of pairs describing separate segments (lv,lv'), + lv < lv', organized in decreasing order. + The definition level is obtained by mapping a level in a segment to the + high limit of this segment. + The definition level of a newtype should be greater or equal to + the highest level of the newtypes in its manifest type. + *) + +let rec map_level lv = function + | [] -> lv + | (lv1, lv2) :: rem -> + if lv > lv2 then lv else + if lv >= lv1 then lv2 else map_level lv rem + +let map_newtype_level env lv = map_level lv env.level_map + +(* precondition: lv < lv' *) +let rec add_level lv lv' = function + | [] -> [lv, lv'] + | (lv1, lv2) :: rem as l -> + if lv2 < lv then (lv, lv') :: l else + if lv' < lv1 then (lv1, lv2) :: add_level lv lv' rem + else add_level (max lv lv1) (min lv' lv2) rem + + (* Expand manifest module type names at the top of the given module type *) let rec scrape_modtype mty env = @@ -739,9 +767,14 @@ and add_class id ty env = and add_cltype id ty env = store_cltype id (Pident id) ty env -let add_local_constraint id info env = - let env = add_type id info env in - { env with local_constraints = true } +let add_local_constraint id info mlv env = + match info with + {type_manifest = Some ty; type_newtype_level = Some lv} -> + let env = add_type id info env in + let level_map = + if lv < mlv then add_level lv mlv env.level_map else env.level_map in + { env with local_constraints = true; level_map = level_map } + | _ -> assert false (* Insertion of bindings by name *) diff --git a/typing/env.mli b/typing/env.mli index 62cedb0e8..b401892cb 100644 --- a/typing/env.mli +++ b/typing/env.mli @@ -21,6 +21,7 @@ type t val empty: t val initial: t val diff: t -> t -> Ident.t list +val map_newtype_level: t -> int -> int (* Lookup by paths *) @@ -64,7 +65,7 @@ val add_module: Ident.t -> module_type -> t -> t val add_modtype: Ident.t -> modtype_declaration -> t -> t val add_class: Ident.t -> class_declaration -> t -> t val add_cltype: Ident.t -> cltype_declaration -> t -> t -val add_local_constraint: Ident.t -> type_declaration -> t -> t +val add_local_constraint: Ident.t -> type_declaration -> int -> t -> t (* Insertion of all fields of a signature. *)