introduce local types in patterns

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@13007 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

1 files changed, 467 insertions, 0 deletions

diff --git a/experimental/garrigue/pattern-local-types.diffs b/experimental/garrigue/pattern-local-types.diffs
new file mode 100644
index 0000000000..0e6f00a2ee
--- /dev/null
+++ b/experimental/garrigue/pattern-local-types.diffs
@@ -0,0 +1,467 @@
+Index: typing/typecore.ml
+===================================================================
+--- typing/typecore.ml	(revision 13003)
++++ typing/typecore.ml	(working copy)
+@@ -61,6 +61,7 @@
+   | Not_a_packed_module of type_expr
+   | Recursive_local_constraint of (type_expr * type_expr) list
+   | Unexpected_existential
++  | Pattern_newtype_non_closed of string * type_expr
+ 
+ exception Error of Location.t * error
+ 
+@@ -121,7 +122,7 @@
+     | Pexp_function (_, eo, pel) ->
+         may expr eo; List.iter (fun (_, e) -> expr e) pel
+     | Pexp_apply (e, lel) -> expr e; List.iter (fun (_, e) -> expr e) lel
+-    | Pexp_let (_, pel, e)
++    | Pexp_let (_, pel, e) -> expr e; List.iter (fun (_, e) -> expr e) pel
+     | Pexp_match (e, pel)
+     | Pexp_try (e, pel) -> expr e; List.iter (fun (_, e) -> expr e) pel
+     | Pexp_array el
+@@ -1454,7 +1455,7 @@
+ 
+ let duplicate_ident_types loc caselist env =
+   let caselist =
+-    List.filter (fun (pat, _) -> contains_gadt env pat) caselist in
++    List.filter (fun ((_,pat), _) -> contains_gadt env pat) caselist in
+   let idents = all_idents (List.map snd caselist) in
+   List.fold_left
+     (fun env s ->
+@@ -1552,7 +1553,7 @@
+         exp_env = env }
+   | Pexp_let(Nonrecursive, [spat, sval], sbody) when contains_gadt env spat ->
+       type_expect ?in_function env
+-        {sexp with pexp_desc = Pexp_match (sval, [spat, sbody])}
++        {sexp with pexp_desc = Pexp_match (sval, [([],spat), sbody])}
+         ty_expected
+   | Pexp_let(rec_flag, spat_sexp_list, sbody) ->
+       let scp =
+@@ -1572,20 +1573,21 @@
+         exp_env = env }
+   | Pexp_function (l, Some default, [spat, sbody]) ->
+       let default_loc = default.pexp_loc in
+-      let scases = [
++      let scases = [([],
+          {ppat_loc = default_loc;
+           ppat_desc =
+             Ppat_construct
+               (mknoloc (Longident.(Ldot (Lident "*predef*", "Some"))),
+                Some {ppat_loc = default_loc;
+                      ppat_desc = Ppat_var (mknoloc "*sth*")},
+-               false)},
++               false)}),
+          {pexp_loc = default_loc;
+           pexp_desc = Pexp_ident(mknoloc (Longident.Lident "*sth*"))};
++	 ([],
+          {ppat_loc = default_loc;
+           ppat_desc = Ppat_construct
+              (mknoloc (Longident.(Ldot (Lident "*predef*", "None"))),
+-              None, false)},
++              None, false)}),
+          default;
+       ] in
+       let smatch = {
+@@ -1603,10 +1605,10 @@
+         pexp_desc =
+          Pexp_function (
+            l, None,
+-           [ {ppat_loc = loc;
+-              ppat_desc = Ppat_var (mknoloc "*opt*")},
++           [ ([], {ppat_loc = loc;
++		   ppat_desc = Ppat_var (mknoloc "*opt*")}),
+              {pexp_loc = loc;
+-              pexp_desc = Pexp_let(Default, [spat, smatch], sbody);
++              pexp_desc = Pexp_let(Default, [snd spat, smatch], sbody);
+              }
+            ]
+          )
+@@ -2733,10 +2735,10 @@
+ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
+   (* ty_arg is _fully_ generalized *)
+   let dont_propagate, has_gadts =
+-    let patterns = List.map fst caselist in
++    let patterns = List.map (fun ((_,p),_) -> p) caselist in
+     List.exists contains_polymorphic_variant patterns,
+-    List.exists (contains_gadt env) patterns in
+-(*  prerr_endline ( if has_gadts then "contains gadt" else "no gadt"); *)
++    List.exists (contains_gadt env) patterns ||
++    List.exists (fun ((l,_),_) -> l <> []) caselist in
+   let ty_arg, ty_res, env =
+     if has_gadts && not !Clflags.principal then
+       correct_levels ty_arg, correct_levels ty_res,
+@@ -2761,9 +2763,21 @@
+     Printtyp.raw_type_expr ty_arg; *)
+   let pat_env_list =
+     List.map
+-      (fun (spat, sexp) ->
++      (fun ((stypes,spat), sexp) ->
+         let loc = sexp.pexp_loc in
+         if !Clflags.principal then begin_def (); (* propagation of pattern *)
++        (* For local types *)
++        if stypes <> [] then begin_def ();
++        let lev' = get_current_level () in
++        let types = List.map (fun name -> name, newvar ~name ()) stypes in
++        let env =
++          List.fold_left (fun env (name, manifest) ->
++            (* "Vanishing" definition *)
++            let decl = new_declaration ~manifest (lev',lev') in
++            snd (Env.enter_type name decl env))
++            env types
++        in
++        (* Type the pattern itself *)
+         let scope = Some (Annot.Idef loc) in
+         let (pat, ext_env, force, unpacks) =
+           let partial =
+@@ -2773,14 +2787,42 @@
+           in type_pattern ~lev env spat scope ty_arg
+         in
+         pattern_force := force @ !pattern_force;
++        (* For local types *)
++        let ext_env =
++          List.fold_left (fun env (name, ty) ->
++            let ty = expand_head env ty in
++            match ty.desc with
++              Tconstr ((Path.Pident id as p), [], _) when
++                let decl = Env.find_type p env in
++                decl.type_newtype_level = Some (lev, lev) &&
++                decl.type_kind = Type_abstract ->
++                  let (id', env) =
++                    Env.enter_type name (new_declaration (lev, lev)) env in
++                  let manifest = newconstr (Path.Pident id') [] in
++                  (* Make previous existential "vanish" *)
++                  Env.add_type id (new_declaration ~manifest (lev',lev')) env
++            | _ ->
++                if free_variables ty <> [] then
++                  raise (Error (spat.ppat_loc,
++                                Pattern_newtype_non_closed (name,ty)));
++                let manifest = correct_levels ty in
++                let decl = new_declaration ~manifest (lev, lev) in
++                snd (Env.enter_type name decl env))
++            ext_env types
++        in
++        if stypes <> [] then begin
++          end_def ();
++          iter_pattern (fun p -> unify_pat ext_env p (newvar())) pat;
++        end;
++        (* Principality *)
+         let pat =
+           if !Clflags.principal then begin
+             end_def ();
+             iter_pattern (fun {pat_type=t} -> generalize_structure t) pat;
+-            { pat with pat_type = instance env pat.pat_type }
++            { pat with pat_type = instance ext_env pat.pat_type }
+           end else pat
+         in
+-        unify_pat env pat ty_arg';
++        unify_pat ext_env pat ty_arg';
+         (pat, (ext_env, unpacks)))
+       caselist in
+   (* Check for polymorphic variants to close *)
+@@ -2802,7 +2844,7 @@
+   let in_function = if List.length caselist = 1 then in_function else None in
+   let cases =
+     List.map2
+-      (fun (pat, (ext_env, unpacks)) (spat, sexp) ->
++      (fun (pat, (ext_env, unpacks)) ((stypes,spat), sexp) ->
+         let sexp = wrap_unpacks sexp unpacks in
+         let ty_res' =
+           if !Clflags.principal then begin
+@@ -2811,8 +2853,8 @@
+             end_def ();
+             generalize_structure ty; ty
+           end
+-          else if contains_gadt env spat then correct_levels ty_res
+-          else ty_res in
++          else if contains_gadt env spat || stypes <> []
++          then correct_levels ty_res else ty_res in
+ (*        Format.printf "@[%i %i, ty_res' =@ %a@]@." lev (get_current_level())
+           Printtyp.raw_type_expr ty_res'; *)
+         let exp = type_expect ?in_function ext_env sexp ty_res' in
+@@ -3218,6 +3260,11 @@
+   | Unexpected_existential ->
+       fprintf ppf
+         "Unexpected existential"
++  | Pattern_newtype_non_closed (name, ty) ->
++      reset_and_mark_loops ty;
++      fprintf ppf
++       "@[In this pattern, local type %s has been inferred as@ %a@ %s@]"
++        name type_expr ty "It should not contain variables."
+ 
+ let () =
+   Env.add_delayed_check_forward := add_delayed_check
+Index: typing/ctype.mli
+===================================================================
+--- typing/ctype.mli	(revision 13003)
++++ typing/ctype.mli	(working copy)
+@@ -140,6 +140,9 @@
+         the parameters [pi] and returns the corresponding instance of
+         [t]. Exception [Cannot_apply] is raised in case of failure. *)
+ 
++val new_declaration:
++    ?manifest:type_expr -> ?loc:Location.t  -> (int * int) -> type_declaration
++
+ val expand_head_once: Env.t -> type_expr -> type_expr
+ val expand_head: Env.t -> type_expr -> type_expr
+ val try_expand_once_opt: Env.t -> type_expr -> type_expr
+Index: typing/typeclass.ml
+===================================================================
+--- typing/typeclass.ml	(revision 13003)
++++ typing/typeclass.ml	(working copy)
+@@ -347,8 +347,8 @@
+   let mkid s = mkloc s self_loc in
+   { pexp_desc =
+       Pexp_function ("", None,
+-                     [mkpat (Ppat_alias (mkpat (Ppat_var (mkid "self-*")),
+-                                         mkid ("self-" ^ cl_num))),
++                     [([],mkpat (Ppat_alias (mkpat (Ppat_var (mkid "self-*")),
++                                         mkid ("self-" ^ cl_num)))),
+                       expr]);
+     pexp_loc = expr.pexp_loc }
+ 
+@@ -836,15 +836,15 @@
+   | Pcl_fun (l, Some default, spat, sbody) ->
+       let loc = default.pexp_loc in
+       let scases =
+-        [{ppat_loc = loc; ppat_desc = Ppat_construct (
++        [([], {ppat_loc = loc; ppat_desc = Ppat_construct (
+           mknoloc (Longident.(Ldot (Lident"*predef*", "Some"))),
+           Some{ppat_loc = loc; ppat_desc = Ppat_var (mknoloc "*sth*")},
+-          false)},
++          false)}),
+          {pexp_loc = loc; pexp_desc =
+           Pexp_ident(mknoloc (Longident.Lident"*sth*"))};
+-         {ppat_loc = loc; ppat_desc =
++         ([], {ppat_loc = loc; ppat_desc =
+           Ppat_construct(mknoloc (Longident.(Ldot (Lident"*predef*", "None"))),
+-                         None, false)},
++                         None, false)}),
+          default] in
+       let smatch =
+         {pexp_loc = loc; pexp_desc =
+Index: typing/ctype.ml
+===================================================================
+--- typing/ctype.ml	(revision 13003)
++++ typing/ctype.ml	(working copy)
+@@ -696,6 +696,7 @@
+       Path.binding_time p
+ 
+ let rec update_level env level ty =
++  (* Format.eprintf "update_level %d %a@." level !Btype.print_raw ty; *)
+   let ty = repr ty in
+   if ty.level > level then begin
+     if Env.has_local_constraints env then begin
+@@ -1043,7 +1044,7 @@
+   reified_var_counter := Vars.add s index !reified_var_counter;
+   Printf.sprintf "%s#%d" s index
+ 
+-let new_declaration newtype manifest =
++let new_declaration ?manifest ?(loc=Location.none) newtype =
+   {
+     type_params = [];
+     type_arity = 0;
+@@ -1051,7 +1052,7 @@
+     type_private = Public;
+     type_manifest = manifest;
+     type_variance = [];
+-    type_newtype_level = newtype;
++    type_newtype_level = Some newtype;
+     type_loc = Location.none;
+   }
+ 
+@@ -1060,7 +1061,7 @@
+   | None -> ()
+   | Some (env, newtype_lev) ->
+       let process existential =
+-        let decl = new_declaration (Some (newtype_lev, newtype_lev)) None in
++        let decl = new_declaration (newtype_lev, newtype_lev) in
+         let name =
+           match repr existential with
+             {desc = Tvar (Some name)} -> name
+@@ -1808,7 +1809,7 @@
+ let reify env t =
+   let newtype_level = get_newtype_level () in
+   let create_fresh_constr lev name =
+-    let decl = new_declaration (Some (newtype_level, newtype_level)) None in
++    let decl = new_declaration (newtype_level, newtype_level) in
+     let name = get_new_abstract_name name in
+     let (id, new_env) = Env.enter_type name decl !env in
+     let t = newty2 lev (Tconstr (Path.Pident id,[],ref Mnil))  in
+@@ -2039,7 +2040,7 @@
+ let add_gadt_equation env source destination =
+   let destination = duplicate_type destination in
+   let source_lev = find_newtype_level !env (Path.Pident source) in
+-  let decl = new_declaration (Some source_lev) (Some destination) in
++  let decl = new_declaration ~manifest:destination source_lev in
+   let newtype_level = get_newtype_level () in
+   env := Env.add_local_constraint source decl newtype_level !env;
+   cleanup_abbrev ()
+Index: typing/typecore.mli
+===================================================================
+--- typing/typecore.mli	(revision 13003)
++++ typing/typecore.mli	(working copy)
+@@ -103,6 +103,7 @@
+   | Not_a_packed_module of type_expr
+   | Recursive_local_constraint of (type_expr * type_expr) list
+   | Unexpected_existential
++  | Pattern_newtype_non_closed of string * type_expr
+ 
+ exception Error of Location.t * error
+ 
+Index: testsuite/tests/typing-gadts/test.ml.reference
+===================================================================
+--- testsuite/tests/typing-gadts/test.ml.reference	(revision 13003)
++++ testsuite/tests/typing-gadts/test.ml.reference	(working copy)
+@@ -293,4 +293,18 @@
+ #       type 'a ty = Int : int -> int ty
+ #     val f : 'a ty -> 'a = <fun>
+ #       val g : 'a ty -> 'a = <fun>
++#         - : unit -> unit list = <fun>
++# - : unit list = []
++# Characters 17-19:
++  function type a. () -> ();; (* fail *)
++                   ^^
++Error: In this pattern, local type a has been inferred as 'a
++       It should not contain variables.
++#     type t = D : 'a * ('a -> int) -> t
++# val f : t -> int = <fun>
++# Characters 42-43:
++  let f = function type b. D ((x:b), f) -> (f:t->int) x;; (* fail *)
++                                            ^
++Error: This expression has type b -> int
++       but an expression was expected of type t -> int
+ # 
+Index: testsuite/tests/typing-gadts/test.ml
+===================================================================
+--- testsuite/tests/typing-gadts/test.ml	(revision 13003)
++++ testsuite/tests/typing-gadts/test.ml	(working copy)
+@@ -512,3 +512,15 @@
+ let g : type a. a ty -> a =
+   let () = () in
+   fun x -> match x with Int y -> y;;
++
++(* Implicit type declarations in patterns *)
++
++(* alias *)
++function type a. (() : a) -> ([] : a list);;
++(function type a. (() : a) -> ([] : a list)) ();;
++function type a. () -> ();; (* fail *)
++
++(* existential *)
++type t = D : 'a * ('a -> int) -> t;;
++let f = function type b. D ((x:b), f) -> (f:b->int) x;;
++let f = function type b. D ((x:b), f) -> (f:t->int) x;; (* fail *)
+Index: testsuite/tests/typing-gadts/test.ml.principal.reference
+===================================================================
+--- testsuite/tests/typing-gadts/test.ml.principal.reference	(revision 13003)
++++ testsuite/tests/typing-gadts/test.ml.principal.reference	(working copy)
+@@ -306,4 +306,18 @@
+ #       type 'a ty = Int : int -> int ty
+ #     val f : 'a ty -> 'a = <fun>
+ #       val g : 'a ty -> 'a = <fun>
++#         - : unit -> unit list = <fun>
++# - : unit list = []
++# Characters 17-19:
++  function type a. () -> ();; (* fail *)
++                   ^^
++Error: In this pattern, local type a has been inferred as 'a
++       It should not contain variables.
++#     type t = D : 'a * ('a -> int) -> t
++# val f : t -> int = <fun>
++# Characters 42-43:
++  let f = function type b. D ((x:b), f) -> (f:t->int) x;; (* fail *)
++                                            ^
++Error: This expression has type b -> int
++       but an expression was expected of type t -> int
+ # 
+Index: parsing/parser.mly
+===================================================================
+--- parsing/parser.mly	(revision 13003)
++++ parsing/parser.mly	(working copy)
+@@ -967,7 +967,7 @@
+   | FUNCTION opt_bar match_cases
+       { mkexp(Pexp_function("", None, List.rev $3)) }
+   | FUN labeled_simple_pattern fun_def
+-      { let (l,o,p) = $2 in mkexp(Pexp_function(l, o, [p, $3])) }
++      { let (l,o,p) = $2 in mkexp(Pexp_function(l, o, [([],p), $3])) }
+   | FUN LPAREN TYPE LIDENT RPAREN fun_def
+       { mkexp(Pexp_newtype($4, $6)) }
+   | MATCH seq_expr WITH opt_bar match_cases
+@@ -1187,18 +1187,18 @@
+     EQUAL seq_expr
+       { $2 }
+   | labeled_simple_pattern fun_binding
+-      { let (l, o, p) = $1 in ghexp(Pexp_function(l, o, [p, $2])) }
++      { let (l, o, p) = $1 in ghexp(Pexp_function(l, o, [([],p), $2])) }
+   | LPAREN TYPE LIDENT RPAREN fun_binding
+       { mkexp(Pexp_newtype($3, $5)) }
+ ;
+ match_cases:
+-    pattern match_action                        { [$1, $2] }
+-  | match_cases BAR pattern match_action        { ($3, $4) :: $1 }
++    match_pattern match_action                  { [$1, $2] }
++  | match_cases BAR match_pattern match_action  { ($3, $4) :: $1 }
+ ;
+ fun_def:
+     match_action                                { $1 }
+   | labeled_simple_pattern fun_def
+-      { let (l,o,p) = $1 in ghexp(Pexp_function(l, o, [p, $2])) }
++      { let (l,o,p) = $1 in ghexp(Pexp_function(l, o, [([],p), $2])) }
+   | LPAREN TYPE LIDENT RPAREN fun_def
+       { mkexp(Pexp_newtype($3, $5)) }
+ ;
+@@ -1245,6 +1245,10 @@
+ 
+ /* Patterns */
+ 
++match_pattern:
++    pattern                                     { [], $1 }
++  | TYPE lident_list DOT pattern                { $2, $4 }
++;
+ pattern:
+     simple_pattern
+       { $1 }
+Index: parsing/parsetree.mli
+===================================================================
+--- parsing/parsetree.mli	(revision 13003)
++++ parsing/parsetree.mli	(working copy)
+@@ -90,10 +90,11 @@
+     Pexp_ident of Longident.t loc
+   | Pexp_constant of constant
+   | Pexp_let of rec_flag * (pattern * expression) list * expression
+-  | Pexp_function of label * expression option * (pattern * expression) list
++  | Pexp_function of
++      label * expression option * ((string list * pattern) * expression) list
+   | Pexp_apply of expression * (label * expression) list
+-  | Pexp_match of expression * (pattern * expression) list
+-  | Pexp_try of expression * (pattern * expression) list
++  | Pexp_match of expression * ((string list * pattern) * expression) list
++  | Pexp_try of expression * ((string list * pattern) * expression) list
+   | Pexp_tuple of expression list
+   | Pexp_construct of Longident.t loc * expression option * bool
+   | Pexp_variant of label * expression option
+@@ -104,7 +105,8 @@
+   | Pexp_ifthenelse of expression * expression * expression option
+   | Pexp_sequence of expression * expression
+   | Pexp_while of expression * expression
+-  | Pexp_for of string loc *  expression * expression * direction_flag * expression
++  | Pexp_for of
++      string loc *  expression * expression * direction_flag * expression
+   | Pexp_constraint of expression * core_type option * core_type option
+   | Pexp_when of expression * expression
+   | Pexp_send of expression * string
+Index: parsing/printast.ml
+===================================================================
+--- parsing/printast.ml	(revision 13003)
++++ parsing/printast.ml	(working copy)
+@@ -686,8 +686,9 @@
+   line i ppf "%a\n" fmt_longident li;
+   pattern (i+1) ppf p;
+ 
+-and pattern_x_expression_case i ppf (p, e) =
++and pattern_x_expression_case i ppf ((l,p), e) =
+   line i ppf "<case>\n";
++  list (i+1) string ppf l;
+   pattern (i+1) ppf  p;
+   expression (i+1) ppf e;
+