summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--parsing/parser.mly4
-rw-r--r--parsing/printast.ml2
-rw-r--r--parsing/printast.mli1
-rw-r--r--typing/btype.ml10
-rw-r--r--typing/btype.mli2
-rw-r--r--typing/ctype.ml296
-rw-r--r--typing/ctype.mli10
-rw-r--r--typing/datarepr.ml61
-rw-r--r--typing/env.ml6
-rw-r--r--typing/parmatch.ml122
-rw-r--r--typing/parmatch.mli2
-rw-r--r--typing/typeclass.ml6
-rw-r--r--typing/typecore.ml235
-rw-r--r--typing/typecore.mli2
-rw-r--r--typing/typedecl.ml61
-rw-r--r--typing/types.ml17
-rw-r--r--typing/types.mli17
-rw-r--r--typing/typetexp.ml81
-rw-r--r--typing/typetexp.mli2
-rw-r--r--utils/misc.ml12
-rw-r--r--utils/misc.mli2
21 files changed, 671 insertions, 280 deletions
diff --git a/parsing/parser.mly b/parsing/parser.mly
index 87cb9ddec..888938d40 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -1300,7 +1300,9 @@ constructor_arguments:
generalized_constructor_arguments:
| COLON core_type_list MINUSGREATER simple_core_type
- { (List.rev $2,$4) }
+ { (List.rev $2, $4) }
+ | COLON simple_core_type
+ { ([],$2) }
;
diff --git a/parsing/printast.ml b/parsing/printast.ml
index e173dcb50..ee52f7d9d 100644
--- a/parsing/printast.ml
+++ b/parsing/printast.ml
@@ -747,3 +747,5 @@ let print_expression = expression 0 ;;
let print_pattern = pattern 0 ;;
+let print_core_type = core_type 0 ;;
+
diff --git a/parsing/printast.mli b/parsing/printast.mli
index 4bf4635cc..307b5a208 100644
--- a/parsing/printast.mli
+++ b/parsing/printast.mli
@@ -20,3 +20,4 @@ val implementation : formatter -> structure_item list -> unit;;
val top_phrase : formatter -> toplevel_phrase -> unit;;
val print_expression : formatter -> expression -> unit;;
val print_pattern : formatter -> pattern -> unit;;
+val print_core_type : formatter -> core_type -> unit;;
diff --git a/typing/btype.ml b/typing/btype.ml
index 759ed50f5..edfc4bee4 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -23,7 +23,7 @@ let generic_level = 100000000
(* Used to mark a type during a traversal. *)
let lowest_level = 0
let pivot_level = 2 * lowest_level - 1
- (* pivot_level - lowest_level < lowest_level *)
+ (* pivot_level - lowest_level < lowest_level *)
(**** Some type creators ****)
@@ -197,6 +197,11 @@ let iter_type_expr f ty =
| Tpoly (ty, tyl) -> f ty; List.iter f tyl
| Tpackage (_, _, l) -> List.iter f l
+
+
+
+
+
let rec iter_abbrev f = function
Mnil -> ()
| Mcons(_, _, ty, ty', rem) -> f ty; f ty'; iter_abbrev f rem
@@ -286,7 +291,7 @@ let cleanup_types () =
(* Mark a type. *)
let rec mark_type ty =
- let ty = repr ty in
+ let ty = repr ty in (* GAH : why do we call repr? *)
if ty.level >= lowest_level then begin
ty.level <- pivot_level - ty.level;
iter_type_expr mark_type ty
@@ -520,6 +525,7 @@ let backtrack (changes, old) =
last_snapshot := old;
Weak.set trail 0 (Some changes)
+
(**** Sets, maps and hashtables of types ****)
module TypeSet = Set.Make(TypeOps)
diff --git a/typing/btype.mli b/typing/btype.mli
index f230b2f2d..bdf70a53a 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -154,6 +154,8 @@ val set_commu: commutable ref -> commutable -> unit
val log_type: type_expr -> unit
(* Log the old value of a type, before modifying it by hand *)
+
+
(**** Sets, maps and hashtables of types ****)
module TypeSet : Set.S with type elt = type_expr
diff --git a/typing/ctype.ml b/typing/ctype.ml
index bfc9b1243..84408fe8e 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -80,6 +80,11 @@ open Btype
[unify].
*)
+
+
+
+
+
(**** Errors ****)
exception Unify of (type_expr * type_expr) list
@@ -102,6 +107,8 @@ let nongen_level = ref 0
let global_level = ref 1
let saved_level = ref []
+let get_current_level = !current_level
+
let init_def level = current_level := level; nongen_level := level
let begin_def () =
saved_level := (!current_level, !nongen_level) :: !saved_level;
@@ -150,6 +157,7 @@ let newty desc = newty2 !current_level desc
let new_global_ty desc = newty2 !global_level desc
let newvar () = newty2 !current_level Tvar
+let newtunivar () = newty2 !current_level Tunivar
let newvar2 level = newty2 level Tvar
let new_global_var () = newty2 !global_level Tvar
@@ -435,7 +443,7 @@ let free_vars ?env ty =
let free_variables ?env ty =
let tl = List.map fst (free_vars ?env ty) in
- unmark_type ty;
+ unmark_type ty; (* GAH : ask garrigue, unmark_type ??? *)
tl
let rec closed_type ty =
@@ -1353,7 +1361,7 @@ let rec unify_univar t1 t2 = function
Some {contents=Some t'2}, Some _ when t2 == repr t'2 ->
()
| Some({contents=None} as r1), Some({contents=None} as r2) ->
- set_univar r1 t2; set_univar r2 t1
+ set_univar r1 t2; set_univar r2 t1 (* GAH : ask garrigue, setting univars?? *)
| None, None ->
unify_univar t1 t2 rem
| _ ->
@@ -1367,6 +1375,7 @@ let add_free_univars tl =
let old = !free_univars in
free_univars := List.fold_right TypeSet.add tl old;
old
+
let set_free_univars tl = free_univars := tl
(* Test the occurence of free univars in a type *)
@@ -1391,7 +1400,7 @@ let occur_univar env ty =
match ty.desc with
Tunivar ->
if not (TypeSet.mem ty bound) && not (TypeSet.mem ty !free_univars)
- then raise (Unify [ty, newgenvar()])
+ then (print_endline "raising occur_univar";raise (Unify [ty, newgenvar()]))
| Tpoly (ty, tyl) ->
let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
occur_rec bound ty
@@ -1552,8 +1561,10 @@ let deep_occur t0 ty =
*)
let pattern_unification = ref false
-let local_unifier = ref []
+let pattern_level = ref 0
+let set_gadt_pattern_level i = pattern_level := !current_level
+let get_gadt_pattern_level () = !pattern_level
let set_unification_type x =
match x with
@@ -1567,74 +1578,132 @@ let get_unification_type () =
| true -> `Pattern
| false -> `Expression
-let reset_local_unifier () =
- local_unifier := []
+let reified_var_counter = ref 0
+
+let get_new_abstract_name () =
+ let ret = Printf.sprintf "&x%d" !reified_var_counter in
+ incr reified_var_counter;
+ ret
+
+let reify env t = (* GAH: ask garrigue; is this right? *)
+ let rec iterator ty =
+
+ match (repr ty).desc with
+ | Tvar ->
+ let decl = {
+ type_params = [];
+ type_arity = 0;
+ type_kind = Type_abstract;
+ type_private = Public;
+ type_manifest = None;
+ type_variance = [];
+ }
+ in
+ if ty.level < get_gadt_pattern_level () then
+ raise (Unify [])
+ else
+ let ty = newvar () in
+ Ident.set_current_time ty.level;
+ let (id, new_env) = Env.enter_type (get_new_abstract_name ()) decl !env in
+ let to_unify = newty2 (get_gadt_pattern_level ()) (Tconstr (Path.Pident id,[],ref Mnil)) in (* GAH : ask garrigue, what in the world is an abbrev_memo ?? *)
+ env := new_env;
+ link_type ty to_unify
+ | _ ->
+ iter_type_expr iterator ty
+ in
+ iter_type_expr iterator (full_expand !env t)
+
+
+let print_path_names t1 t2 =
+ match t1.desc,t2.desc with
+ | Tconstr (p1,[],_),Tconstr (p2,[],_) ->
+ begin match p1,p2 with
+ | Path.Pident q1,Path.Pident q2 ->
+ Printf.printf "different paths but %s %s\n%!" (Ident.name q1) (Ident.name q2)
+ | _ -> print_endline "not idents"
+ end
+ | _ -> print_endline "not constructors"
+
+let unify_eq_set = Btype.TypeHash.create 10
+
+let add_type_equality t1 t2 =
+ try
+ let set = TypeHash.find unify_eq_set t1 in
+ set := Btype.TypeSet.add t2 !set
+ with
+ | Not_found ->
+ TypeHash.add unify_eq_set t1 (ref (TypeSet.add t2 TypeSet.empty))
+
+
-let get_local_unifier () = !local_unifier
-let uni_equalities = ref TypeSetPair.empty
-let uni_eq t1 t2 = t1 == t2 || TypeSetPair.mem (t1,t2) !uni_equalities || TypeSetPair.mem (t2,t1) !uni_equalities
-let add_equality t1 t2 =
- uni_equalities := TypeSetPair.add (t1, t2) !uni_equalities
+let unify_eq t1 t2 =
+ let test t1 t2 =
+ try
+ Btype.TypeSet.mem t2 !(TypeHash.find unify_eq_set t1) ;
+ with
+ | Not_found -> false
+ in
+ t1 == t2 || test t1 t2 || test t2 t1
-let rec unify env t1 t2 =
+
+let rec unify (env:Env.t ref) t1 t2 =
(* First step: special cases (optimizations) *)
- if uni_eq t1 t2 then () else
+
+
+
+ if unify_eq t1 t2 then () else
let t1 = repr t1 in
let t2 = repr t2 in
- if uni_eq t1 t2 then () else
+ if unify_eq t1 t2 then () else
+
try
type_changed := true;
match (t1.desc, t2.desc) with
- | (Tvar, Tconstr _) when deep_occur t1 t2 ->
+ (Tvar, Tconstr _) when deep_occur t1 t2 ->
unify2 env t1 t2
- | (Tconstr _, Tvar) when deep_occur t2 t1 ->
+ | (Tconstr _, Tvar) when deep_occur t2 t1 ->
unify2 env t1 t2
- | (Tvar, _) ->
- occur env t1 t2; occur_univar env t2;
- update_level env t1.level t2;
+ | (Tvar, _) ->
+ occur !env t1 t2; occur_univar !env t2;
+ update_level !env t1.level t2;
link_type t1 t2
- | (_, Tvar) ->
- occur env t2 t1; occur_univar env t1;
- update_level env t2.level t1;
+ | (_, Tvar) ->
+ occur !env t2 t1; occur_univar !env t1;
+ update_level !env t2.level t1;
link_type t2 t1
- | (Tunivar, Tunivar) -> (* GAH : ask garrigue: when do we unify univars? *)
+ | (Tunivar, Tunivar) ->
unify_univar t1 t2 !univar_pairs;
- update_level env t1.level t2;
+ update_level !env t1.level t2;
link_type t1 t2
-
| (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
when Path.same p1 p2
(* This optimization assumes that t1 does not expand to t2
(and conversely), so we fall back to the general case
when any of the types has a cached expansion. *)
&& not (has_cached_expansion p1 !a1
- || has_cached_expansion p2 !a2) ->
- update_level env t1.level t2;
+ || has_cached_expansion p2 !a2) ->
+ update_level !env t1.level t2;
link_type t1 t2
-
-
- | _ ->
+ | _ ->
unify2 env t1 t2
with Unify trace ->
raise (Unify ((t1, t2)::trace))
and unify2 env t1 t2 =
-
-
-
(* Second step: expansion of abbreviations *)
let rec expand_both t1'' t2'' =
- let t1' = expand_head_unif env t1 in
- let t2' = expand_head_unif env t2 in
+ let t1' = expand_head_unif !env t1 in
+ let t2' = expand_head_unif !env t2 in
(* Expansion may have changed the representative of the types... *)
- if uni_eq t1' t1'' && uni_eq t2' t2'' then (t1',t2') else
+ if unify_eq t1' t1'' && unify_eq t2' t2'' then (t1',t2') else
expand_both t1' t2'
in
let t1', t2' = expand_both t1 t2 in
- if uni_eq t1' t2' then () else
+ if unify_eq t1' t2' then () else
+
let t1 = repr t1 and t2 = repr t2 in
- if (uni_eq t1 t1') || (not (uni_eq t2 t2')) then (* GAH: ask garrigue why this code seems so strange *)
+ if unify_eq t1 t1' || not (unify_eq t2 t2') then
unify3 env t1 t1' t2 t2'
else
try unify3 env t2 t2' t1 t1' with Unify trace ->
@@ -1646,48 +1715,100 @@ and unify3 env t1 t1' t2 t2' =
let d1 = t1'.desc and d2 = t2'.desc in
let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
- occur env t1' t2;
- update_level env t1'.level t2;
-
- add_equality t1' t2;
-
-
-
+ occur !env t1' t2;
+ update_level !env t1'.level t2;
+ add_type_equality t1' t2;
try
begin match (d1, d2) with
(Tvar, _) ->
link_type t1' t2;
- occur_univar env t2
+ occur_univar !env t2
| (_, Tvar) ->
link_type t2' t1;
- occur_univar env t1;
-(* let td1 = newgenty d1 in
- occur env t2' td1;
-
+ let td1 = newgenty d1 in
+ occur !env t2' td1;
+ occur_univar !env td1;
if t1 == t1' then begin
(* The variable must be instantiated... *)
let ty = newty2 t1'.level d1 in
- update_level env t2'.level ty;
+ update_level !env t2'.level ty;
link_type t2' ty
end else begin
log_type t1';
t1'.desc <- d1;
- update_level env t2'.level t1;
+ update_level !env t2'.level t1;
link_type t2' t1
- end*)
+ end
| (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
- unify env t1 t2; unify env u1 u2;
+ unify env t1 t2; unify env u1 u2;
begin match commu_repr c1, commu_repr c2 with
Clink r, c2 -> set_commu r c2
| c1, Clink r -> set_commu r c1
| _ -> ()
end
| (Ttuple tl1, Ttuple tl2) ->
+
unify_list env tl1 tl2
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
+
unify_list env tl1 tl2
+
+ | _,(Tconstr (Path.Pident p,[],_)) when not !pattern_unification -> (* GAH : must be abstract or else it would have been expanded, ask garrigue *)
+ raise (Unify [])
+
+(* let _,td = Env.lookup_type (Longident.parse (Ident.name p)) !env in*)
+(* let td = Env.lookup_type (Ident.name "t") !env in
+ (match td.type_manifest with
+ | None ->
+ print_endline "no manifest 1"
+ | Some ty ->
+ print_endline (string_of_bool (ty == t1));
+ print_endline "have a manifest 1");
+*)
+
+(* ignore(Env.find_type_expansion (Path.Pident p) !env);*)
+
+
+
+ | Tconstr (p1,[],_),Tconstr (p2,[],_) when Path.same p1 p2 ->
+ print_endline "same path yo";
+
+
+(* GAH : must be abstract or else it would have been expanded, ask garrigue *)
+
+ | (Tconstr (Path.Pident p,[],_)),_ when !pattern_unification -> (* GAH : must be abstract or else it would have been expanded, ask garrigue *)
+ let t2 = copy t2 in
+
+ reify env t2 ;
+
+ let decl = {
+ type_params = [];
+ type_arity = 0;
+ type_kind = Type_abstract;
+ type_private = Public;
+ type_manifest = Some t2;
+ type_variance = [];
+ }
+ in
+ let new_env = Env.add_type p decl !env in
+ env := new_env
+ | _,(Tconstr (Path.Pident p,[],_)) when !pattern_unification ->
+ let t1 = copy t1 in
+ reify env t1 ;
+ let decl = {
+ type_params = [];
+ type_arity = 0;
+ type_kind = Type_abstract;
+ type_private = Public;
+ type_manifest = Some t1;
+ type_variance = [];
+ }
+ in
+ let new_env = Env.add_type p decl !env in
+ env := new_env
| (Tobject (fi1, nm1), Tobject (fi2, _)) ->
+ link_type t1' t2;
unify_fields env fi1 fi2;
(* Type [t2'] may have been instantiated by [unify_fields] *)
(* XXX One should do some kind of unification... *)
@@ -1701,10 +1822,13 @@ and unify3 env t1 t1' t2 t2' =
()
end
| (Tvariant row1, Tvariant row2) ->
+ link_type t1' t2;
unify_row env row1 row2
| (Tfield _, Tfield _) -> (* Actually unused *)
+ link_type t1' t2;
unify_fields env t1' t2'
| (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
+ link_type t1' t2;
begin match field_kind_repr kind with
Fvar r when f <> dummy_method -> set_kind r Fabsent
| _ -> raise (Unify [])
@@ -1712,23 +1836,14 @@ and unify3 env t1 t1' t2 t2' =
| (Tnil, Tnil) ->
()
| (Tpoly (t1, []), Tpoly (t2, [])) ->
- unify env t1 t2
+ link_type t1' t2;
+ unify env t1 t2
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
- enter_poly env univar_pairs t1 tl1 t2 tl2 (unify env)
+ link_type t1' t2;
+ enter_poly !env univar_pairs t1 tl1 t2 tl2 (unify env)
| (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)) when Path.same p1 p2 && n1 = n2 ->
+ link_type t1' t2;
unify_list env tl1 tl2
- | (Tunivar,_) ->
-
- if !pattern_unification then
- local_unifier:= (t1,t2) :: !local_unifier
- else
- raise (Unify [])
- | (_,Tunivar) ->
-
- if !pattern_unification then
- local_unifier:= (t2,t1) :: !local_unifier
- else
- ( raise (Unify []) )
| (_, _) ->
raise (Unify [])
end;
@@ -1738,7 +1853,7 @@ and unify3 env t1 t1' t2 t2' =
match t2.desc with
Tconstr (p, tl, abbrev) ->
forget_abbrev abbrev p;
- let t2'' = expand_head_unif env t2 in
+ let t2'' = expand_head_unif !env t2 in
if not (closed_parameterized_type tl t2'') then
link_type (repr t2) (repr t2')
| _ ->
@@ -1835,7 +1950,7 @@ and unify_row env row1 row2 =
if row1.row_fixed then rm1 else
if row2.row_fixed then rm2 else
newgenvar ()
- in update_level env (min rm1.level rm2.level) more;
+ in update_level !env (min rm1.level rm2.level) more;
let fixed = row1.row_fixed || row2.row_fixed
and closed = row1.row_closed || row2.row_closed in
let keep switch =
@@ -1882,7 +1997,7 @@ and unify_row env row1 row2 =
unify env rm row0.row_more
else
let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
- update_level env rm.level ty;
+ update_level !env rm.level ty;
link_type rm ty
in
let md1 = rm1.desc and md2 = rm2.desc in
@@ -1904,7 +2019,7 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
if f1 == f2 then () else
match f1, f2 with
- Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2
+ Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2
| Rpresent None, Rpresent None -> ()
| Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) ->
if e1 == e2 then () else
@@ -1925,7 +2040,7 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
in
let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in
(* Is this handling of levels really principal? *)
- List.iter (update_level env (repr more).level) (tl1' @ tl2');
+ List.iter (update_level !env (repr more).level) (tl1' @ tl2');
let e = ref None in
let f1' = Reither(c1 || c2, tl1', m1 || m2, e)
and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in
@@ -1950,14 +2065,31 @@ and unify_row_field env fixed1 fixed2 more l f1 f2 =
;;
+let bare_tunivar x = (* GAH: ask garrigue about this. is it correct *)
+ match (repr x).desc with
+ | Tunivar -> true
+ | _ -> false
+
+let bare_tvar x = (* GAH: ask garrigue about this. is it correct *)
+ match (repr x).desc with
+ | Tvar -> true
+ | _ -> false
+
+
+
let unify env ty1 ty2 =
try
- uni_equalities := TypeSetPair.empty;
+ unify env ty1 ty2
+ with Unify trace ->
+ raise (Unify (expand_trace !env trace))
+
+let unify_gadt (env:Env.t ref) ty1 ty2 =
+ try
+ pattern_unification:=true;
unify env ty1 ty2;
- uni_equalities := TypeSetPair.empty;
+ pattern_unification:=false;
with Unify trace ->
- uni_equalities := TypeSetPair.empty;
- raise (Unify (expand_trace env trace))
+ raise (Unify (expand_trace !env trace))
let unify_var env t1 t2 =
@@ -1973,7 +2105,7 @@ let unify_var env t1 t2 =
raise (Unify (expand_trace env ((t1,t2)::trace)))
end
| _ ->
- unify env t1 t2
+ unify (ref env) t1 t2
let _ = unify' := unify_var
@@ -1983,7 +2115,11 @@ let unify_pairs env ty1 ty2 pairs =
let unify env ty1 ty2 =
univar_pairs := [];
- unify env ty1 ty2
+ unify (ref env) ty1 ty2
+
+let unify_gadt env ty1 ty2 =
+ univar_pairs := [];
+ unify_gadt env ty1 ty2
(**** Special cases of unification ****)
@@ -3205,7 +3341,7 @@ let subtype env ty1 ty2 =
function () ->
List.iter
(function (trace0, t1, t2, pairs) ->
- try unify_pairs env t1 t2 pairs with Unify trace ->
+ try unify_pairs (ref env) t1 t2 pairs with Unify trace ->
raise (Subtype (expand_trace env (List.rev trace0),
List.tl (List.tl trace))))
(List.rev cstrs)
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 108b251a1..1213dc25f 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -148,6 +148,8 @@ val set_free_univars: Btype.TypeSet.t -> unit
val unify: Env.t -> type_expr -> type_expr -> unit
(* Unify the two types given. Raise [Unify] if not possible. *)
+val unify_gadt: Env.t ref -> type_expr -> type_expr -> unit
+ (* Unify the two types given and update the environment with the local constraints. Raise [Unify] if not possible. *)
val unify_var: Env.t -> type_expr -> type_expr -> unit
(* Same as [unify], but allow free univars when first type
is a variable. *)
@@ -250,7 +252,11 @@ val arity: type_expr -> int
val collapse_conj_params: Env.t -> type_expr list -> unit
(* Collapse conjunctive types in class parameters *)
-val reset_local_unifier: unit -> unit
-val get_local_unifier: unit -> (type_expr * type_expr) list
val set_unification_type : [`Pattern | `Expression] -> unit
val get_unification_type : unit -> [`Pattern | `Expression]
+val bare_tunivar : type_expr -> bool
+val bare_tvar : type_expr -> bool
+
+val set_gadt_pattern_level : unit -> unit
+val get_gadt_pattern_level : unit -> int
+
diff --git a/typing/datarepr.ml b/typing/datarepr.ml
index 2482059c5..1f4f05230 100644
--- a/typing/datarepr.ml
+++ b/typing/datarepr.ml
@@ -19,18 +19,53 @@ open Misc
open Asttypes
open Types
+module Duplicated_code = (* GAH: causes a stack overflow when encountering recursive type *)
+struct
+ let rec free_vars ty =
+ let ret = ref [] in
+ let rec loop ty =
+ let ty = Btype.repr ty in
+ if ty.level >= Btype.lowest_level then begin
+ ty.level <- Btype.pivot_level - ty.level;
+ match ty.desc with
+ | Tvar ->
+ ret := ty :: !ret
+ | _ ->
+ Btype.iter_type_expr loop ty
+ end
+ in
+ loop ty;
+ Btype.unmark_type ty;
+ !ret
+end
+
+
+let constructor_descrs_called = ref 0
+
let constructor_descrs ty_res cstrs priv =
let num_consts = ref 0 and num_nonconsts = ref 0 in
List.iter
(function (name, [],_) -> incr num_consts
| (name, _,_) -> incr num_nonconsts)
cstrs;
+ let all_ty_res =
+ List.map
+ (fun (_, _,x) -> x)
+ cstrs
+ in
let rec describe_constructors idx_const idx_nonconst = function
[] -> []
| (name, ty_args, ty_res_opt) :: rem ->
let ty_res =
match ty_res_opt with
- | Some ty_res -> ty_res
+ | Some ty_res' ->
+ (match ty_res.desc, ty_res'.desc with
+ | Tconstr (p,_,_), Tconstr(p',_,_) ->
+ if not (Path.same p p') then
+ failwith "the return type of a generalized constructor has incorrect type"
+ else
+ ty_res'
+ | _ -> fatal_error "return type must be a Tconstr")
| None -> ty_res
in
let (tag, descr_rem) =
@@ -39,25 +74,34 @@ let constructor_descrs ty_res cstrs priv =
describe_constructors (idx_const+1) idx_nonconst rem)
| _ -> (Cstr_block idx_nonconst,
describe_constructors idx_const (idx_nonconst+1) rem) in
-(* let existentials =
+ let existentials =
match ty_res_opt with
| None -> []
| Some type_ret ->
- let res_vars = List.fold_right Btype.TypeSet.add (free_vars type_ret) Btype.TypeSet.empty in
- let other_types
-*)
-
+ let res_vars = List.fold_right Btype.TypeSet.add (Duplicated_code.free_vars type_ret) Btype.TypeSet.empty in
+ let arg_vars =
+ List.fold_left
+ (fun s list -> List.fold_right Btype.TypeSet.add list s)
+ Btype.TypeSet.empty
+ (List.map Duplicated_code.free_vars ty_args)
+ in
+ Btype.TypeSet.elements (Btype.TypeSet.diff arg_vars res_vars)
+ in
+ incr constructor_descrs_called;
let cstr =
{ cstr_res = ty_res;
- cstr_existentials = [] ; (* GAH: HOW DO I GET THE EXISTENTIALS OF A TYPE?? *)
+ cstr_existentials = existentials ; (* GAH: HOW DO I GET THE EXISTENTIALS OF A TYPE?? *)
cstr_args = ty_args;
cstr_arity = List.length ty_args;
cstr_tag = tag;
cstr_consts = !num_consts;
cstr_nonconsts = !num_nonconsts;
+ cstr_all_ty_res = all_ty_res;
cstr_private = priv } in
(name, cstr) :: descr_rem in
- describe_constructors 0 0 cstrs
+ describe_constructors 0 0 cstrs
+
+
let exception_descr path_exc decl =
{ cstr_res = Predef.type_exn;
@@ -67,6 +111,7 @@ let exception_descr path_exc decl =
cstr_tag = Cstr_exception path_exc;
cstr_consts = -1;
cstr_nonconsts = -1;
+ cstr_all_ty_res = [];
cstr_private = Public }
let none = {desc = Ttuple []; level = -1; id = -1}
diff --git a/typing/env.ml b/typing/env.ml
index 391a363f4..ef898cbea 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -21,6 +21,7 @@ open Longident
open Path
open Types
+let store_type_called = ref 0
type error =
Not_an_interface of string
@@ -451,12 +452,13 @@ let rec scrape_modtype mty env =
| _ -> mty
(* Compute constructor descriptions *)
-
let constructors_of_type ty_path decl =
let handle_variants cstrs =
- Datarepr.constructor_descrs
+ let ret = Datarepr.constructor_descrs
(Btype.newgenty (Tconstr(ty_path, decl.type_params, ref Mnil)))
cstrs decl.type_private
+ in
+ ret
in
match decl.type_kind with
| Type_variant cstrs ->
diff --git a/typing/parmatch.ml b/typing/parmatch.ml
index 266d42795..9cafac4a4 100644
--- a/typing/parmatch.ml
+++ b/typing/parmatch.ml
@@ -259,6 +259,10 @@ and pretty_lvals lbls ppf = function
let top_pretty ppf v =
fprintf ppf "@[%a@]@?" pretty_val v
+let pretty_pat_now p =
+ top_pretty Format.str_formatter p ;
+ prerr_endline (Format.flush_str_formatter ())
+
let prerr_pat v =
top_pretty str_formatter v ;
@@ -618,11 +622,33 @@ let row_of_pat pat =
not.
*)
+let initial_env = ref Env.empty
+
+let unifiable t t' =
+ let snap = Btype.snapshot () in
+ try
+ Ctype.unify_gadt (ref !initial_env) t t'; (* GAH: ask garrigue: unify in which environment??? *)
+ Btype.backtrack snap;
+ true
+ with
+ _ ->
+ Btype.backtrack snap;
+ false
+
let full_match closing env = match env with
| ({pat_desc = Tpat_construct ({cstr_tag=Cstr_exception _},_)},_)::_ ->
false
-| ({pat_desc = Tpat_construct(c,_)},_) :: _ ->
- List.length env = c.cstr_consts + c.cstr_nonconsts
+| ({pat_desc = Tpat_construct(c,_);pat_type=typ},_) :: _ ->
+
+ let all_ty_res = c.cstr_all_ty_res in
+ let possibles = ref 0 in
+ List.iter
+ (function
+ | None -> incr possibles
+ | Some t ->
+ if unifiable typ t then incr possibles)
+ all_ty_res;
+ List.length env = !possibles (*c.cstr_consts + c.cstr_nonconsts*)
| ({pat_desc = Tpat_variant _} as p,_) :: _ ->
let fields =
List.map
@@ -711,12 +737,16 @@ let rec pat_of_constrs ex_pat = function
(pat_of_constr ex_pat cstr,
pat_of_constrs ex_pat rem, None)}
+
+
(* Sends back a pattern that complements constructor tags all_tag *)
-let complete_constrs p all_tags = match p.pat_desc with
+let complete_constrs p all_tags =
+ let ty = p.pat_type in
+ match p.pat_desc with
| Tpat_construct (c,_) ->
begin try
let not_tags = complete_tags c.cstr_consts c.cstr_nonconsts all_tags in
- List.map
+ map_filter
(fun tag ->
let _,targs,ret_type_opt = get_constr tag p.pat_type p.pat_env in (* GAH: is this correct? don't forget the existentials! *)
let ret_type =
@@ -724,18 +754,22 @@ let complete_constrs p all_tags = match p.pat_desc with
| None -> c.cstr_res
| Some ret_type -> ret_type
in
- {c with
- cstr_res = ret_type ;
- cstr_tag = tag ;
- cstr_args = targs ;
- cstr_arity = List.length targs})
+ if not (unifiable ty ret_type) then
+ None
+ else
+ Some
+ {c with
+ cstr_res = ret_type ;
+ cstr_tag = tag ;
+ cstr_args = targs ;
+ cstr_arity = List.length targs})
not_tags
with
-| Datarepr.Constr_not_found ->
- fatal_error "Parmatch.complete_constr: constr_not_found"
+ | Datarepr.Constr_not_found ->
+ fatal_error "Parmatch.complete_constr: constr_not_found"
end
| _ -> fatal_error "Parmatch.complete_constr"
-
+
(* Auxiliary for build_other *)
@@ -752,7 +786,8 @@ let build_other_constant proj make first next p 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 ({cstr_tag=Cstr_exception _} as c,_)},_)
::_ ->
make_pat
@@ -771,7 +806,9 @@ let build_other ext env = match env with
| {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
- pat_of_constrs p (complete_constrs p all_tags)
+ let cnstrs = complete_constrs p all_tags in
+ let ret = pat_of_constrs p cnstrs in
+ ret
end
| ({pat_desc = Tpat_variant (_,_,r)} as p,_) :: _ ->
let tags =
@@ -951,29 +988,53 @@ let rec try_many f = function
| r -> r
end
-let rec exhaust ext pss n = match pss with
+(*let pretty_pss pss =
+ let print_lst ppf lst =
+ fprintf ppf "{";
+ List.iter
+ (top_pretty ppf)
+ lst;
+ fprintf ppf "}";
+ in
+ let print_lstlst ppf lstlst =
+ fprintf ppf "[";
+ List.iter
+ (print_lst ppf)
+ lstlst;
+ fprintf ppf "]"
+ in
+ Format.fprintf Format.str_formatter "[%a]%!"
+ print_lstlst pss;
+ print_endline (Format.flush_str_formatter ())*)
+
+
+
+let rec exhaust ext pss n =
+ match pss with
| [] -> Rsome (omegas n)
| []::_ -> Rnone
-| pss ->
- let q0 = discr_pat omega pss in
+| pss ->
+ let q0 = discr_pat omega pss in
begin match filter_all q0 pss with
(* first column of pss is made of variables only *)
- | [] ->
+ | [] ->
begin match exhaust ext (filter_extra pss) (n-1) with
| Rsome r -> Rsome (q0::r)
| r -> r
end
- | constrs ->
+ | constrs ->
let try_non_omega (p,pss) =
if is_absent_pat p then
Rnone
else
- match
- exhaust
- ext pss (List.length (simple_match_args p omega) + n - 1)
- with
- | Rsome r -> Rsome (set_args p r)
- | r -> r in
+ begin
+ match
+ exhaust
+ ext pss (List.length (simple_match_args p omega) + n - 1)
+ with
+ | Rsome r -> Rsome (set_args p r)
+ | r -> r end in
+
if
full_match false constrs && not (should_extend ext constrs)
then
@@ -987,6 +1048,7 @@ let rec exhaust ext pss n = match pss with
* D exhaustive => pss exhaustive
* D non-exhaustive => we have a non-filtered value
*)
+
let r = exhaust ext (filter_extra pss) (n-1) in
match r with
| Rnone -> Rnone
@@ -1064,6 +1126,9 @@ let pretty_pat p =
top_pretty Format.str_formatter p ;
prerr_string (Format.flush_str_formatter ())
+
+
+
type matrix = pattern list list
let pretty_line ps =
@@ -1316,6 +1381,7 @@ and every_both pss qs q1 q2 =
(* le_pat p q means, forall V, V matches q implies V matches p *)
+(* GAH: ask garrigue: does le mean "less than or equal" ? *)
let rec le_pat p q =
match (p.pat_desc, q.pat_desc) with
| (Tpat_var _|Tpat_any),_ -> true
@@ -1450,7 +1516,7 @@ let rec initial_matrix = function
| (pat, act) :: rem ->
if has_guard act
then
- initial_matrix rem
+ initial_matrix rem
else
[pat] :: initial_matrix rem
@@ -1535,6 +1601,7 @@ let do_check_partial loc casel pss = match pss with
Then match MUST be considered non-exhaustive,
otherwise compilation of PM is broken.
*)
+ (* GAH: ask garrigue: what's PM? *)
begin match casel with
| [] -> ()
| _ -> Location.prerr_warning loc Warnings.All_clauses_guarded
@@ -1646,7 +1713,8 @@ let do_check_fragile loc casel pss =
on exhaustive matches only.
*)
-let check_partial loc casel =
+let check_partial loc casel env =
+ initial_env := env; (* GAH : make this more functional *)
if Warnings.is_active (Warnings.Partial_match "") then begin
let pss = initial_matrix casel in
let pss = get_mins le_pats pss in
diff --git a/typing/parmatch.mli b/typing/parmatch.mli
index 7ef6a8308..5bae2fa37 100644
--- a/typing/parmatch.mli
+++ b/typing/parmatch.mli
@@ -51,7 +51,7 @@ val complete_constrs :
pattern -> constructor_tag list -> constructor_description list
val pressure_variants: Env.t -> pattern list -> unit
-val check_partial: Location.t -> (pattern * expression) list -> partial
+val check_partial: Location.t -> (pattern * expression) list -> Env.t -> partial
val check_unused: Env.t -> (pattern * expression) list -> unit
(* Irrefutability tests *)
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index de093cfc5..d7c12fe93 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -809,12 +809,14 @@ and class_expr cl_num val_env met_env scl =
| _ -> true
in
let partial =
- Parmatch.check_partial pat.pat_loc
+ Parmatch.check_partial pat.pat_loc
[pat, (* Dummy expression *)
{exp_desc = Texp_constant (Asttypes.Const_int 1);
exp_loc = Location.none;
exp_type = Ctype.none;
- exp_env = Env.empty }] in
+ exp_env = Env.empty }]
+ val_env (* GAH : whoa, I don't know what val_env is, and quite frankly I'm scared. Ask garrigue *)
+ in
Ctype.raise_nongen_level ();
let cl = class_expr cl_num val_env' met_env scl' in
Ctype.end_def ();
diff --git a/typing/typecore.ml b/typing/typecore.ml
index a5452661e..942d50231 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -25,6 +25,8 @@ open Ctype
type error =
Polymorphic_label of Longident.t
| Constructor_arity_mismatch of Longident.t * int * int
+ | Constructor_inhabit_tunivar of type_expr * Longident.t
+ | Constant_inhabit_tunivar of type_expr
| Label_mismatch of Longident.t * (type_expr * type_expr) list
| Pattern_type_clash of (type_expr * type_expr) list
| Multiply_bound_variable of string
@@ -70,12 +72,7 @@ let type_module =
let type_open =
ref (fun _ -> assert false)
-(*let print_local_unifier ?(s="") () =
- Format.fprintf Format.std_formatter "%s local_unifier:\n[%a]\n%!" s
- (fun ppf lst -> List.iter (fun (t,t') -> Format.fprintf ppf "%a = %a;" Printtyp.raw_type_expr t Printtyp.raw_type_expr t') lst)
- (get_local_unifier ())
-;;
-*)
+
(* Forward declaration, to be filled in by Typeclass.class_structure *)
let type_object =
@@ -147,15 +144,41 @@ let rec extract_label_names sexp env ty =
(* Typing of patterns *)
+
+let unify_pat_types loc env ty ty' =
+ try
+ unify env ty ty'
+ with
+ Unify trace ->
+ raise(Error(loc, Pattern_type_clash(trace)))
+ | Tags(l1,l2) ->
+ raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
+
+
+let unify_pat_types_gadt loc env ty ty' =
+ try
+ unify_gadt env ty ty'
+ with
+ Unify trace ->
+ raise(Error(loc, Pattern_type_clash(trace)))
+ | Tags(l1,l2) ->
+ raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
+
+
(* Creating new conjunctive types is not allowed when typing patterns *)
let unify_pat env pat expected_ty =
- try
+ unify_pat_types pat.pat_loc env pat.pat_type expected_ty
+
+(* try
unify env pat.pat_type expected_ty
with
Unify trace ->
raise(Error(pat.pat_loc, Pattern_type_clash(trace)))
| Tags(l1,l2) ->
- raise(Typetexp.Error(pat.pat_loc, Typetexp.Variant_tags (l1, l2)))
+ raise(Typetexp.Error(pat.pat_loc, Typetexp.Variant_tags (l1, l2)))*)
+
+
+
(* make all Reither present in open variants *)
let finalize_variant pat =
@@ -397,7 +420,7 @@ let check_recordpat_labels loc lbl_pat_list closed =
(* Typing of patterns *)
-let rec type_pat env sp expected_ty =
+let rec type_pat (env:Env.t ref) sp expected_ty =
let loc = sp.ppat_loc in
match sp.ppat_desc with
|Ppat_any ->
@@ -405,20 +428,20 @@ let rec type_pat env sp expected_ty =
pat_desc = Tpat_any;
pat_loc = loc;
pat_type = expected_ty;
- pat_env = env }
- |Ppat_var name ->
+ pat_env = !env }
+ | Ppat_var name ->
let ty = newvar() in
let id = enter_variable loc name ty in (* GAH : what does this do? *)
- unify env ty expected_ty;
+ unify_pat_types loc !env expected_ty ty;
rp {
pat_desc = Tpat_var id;
pat_loc = loc;
pat_type = ty;
- pat_env = env }
+ pat_env = !env }
| Ppat_constraint({ppat_desc=Ppat_var name; ppat_loc=loc},
({ptyp_desc=Ptyp_poly _} as sty)) ->
(* explicitly polymorphic type *)
- let ty, force = Typetexp.transl_simple_type_delayed env sty in
+ let ty, force = Typetexp.transl_simple_type_delayed !env sty in
pattern_force := force :: !pattern_force;
begin match ty.desc with
|Tpoly (body, tyl) ->
@@ -430,13 +453,13 @@ let rec type_pat env sp expected_ty =
rp { pat_desc = Tpat_var id;
pat_loc = loc;
pat_type = ty;
- pat_env = env }
+ pat_env = !env }
| _ -> assert false
end
|Ppat_alias(sq, name) ->
let q = type_pat env sq expected_ty in (* GAH: no idea *)
begin_def ();
- let ty_var = build_as_type env q in
+ let ty_var = build_as_type !env q in
end_def ();
generalize ty_var;
let id = enter_variable loc name ty_var in
@@ -444,26 +467,34 @@ let rec type_pat env sp expected_ty =
pat_desc = Tpat_alias(q, id);
pat_loc = loc;
pat_type = q.pat_type;
- pat_env = env }
+ pat_env = !env }
|Ppat_constant cst ->
- (* GAH: dunno what to do here *)
- unify env expected_ty (type_constant cst);
+ if bare_tunivar expected_ty then
+ raise (Error(loc,Constant_inhabit_tunivar(expected_ty)));
+ unify_pat_types loc !env expected_ty (type_constant cst);
rp {
pat_desc = Tpat_constant cst;
pat_loc = loc;
pat_type = expected_ty; (*type_constant cst;*)
- pat_env = env }
+ pat_env = !env }
|Ppat_tuple spl ->
let spl_ann = List.map (fun p -> (p,newvar ())) spl in
let pl = List.map (fun (p,t) -> type_pat env p t) spl_ann in
- unify env expected_ty (newty (Ttuple(List.map snd spl_ann)));
+ unify_pat_types loc !env expected_ty (newty (Ttuple(List.map snd spl_ann)));
rp {
pat_desc = Tpat_tuple pl;
pat_loc = loc;
pat_type = expected_ty;
- pat_env = env }
+ pat_env = !env }
|Ppat_construct(lid, sarg, explicit_arity) ->
- let constr = Typetexp.find_constructor env loc lid in
+
+
+
+
+
+ if bare_tunivar expected_ty then
+ raise (Error(loc,Constructor_inhabit_tunivar(expected_ty,lid )));
+ let constr = Typetexp.find_constructor !env loc lid in
let sargs =
match sarg with
None -> []
@@ -479,13 +510,13 @@ let rec type_pat env sp expected_ty =
raise(Error(loc, Constructor_arity_mismatch(lid,
constr.cstr_arity, List.length sargs)));
let (ty_args, ty_res) = instance_constructor constr in
- unify env expected_ty ty_res;
+ unify_pat_types_gadt loc env expected_ty ty_res;
let args: Typedtree.pattern list = List.map2 (fun p t -> type_pat env p t) sargs ty_args in (* GAH : might be wrong *)
rp {
pat_desc = Tpat_construct(constr, args);
pat_loc = loc;
- pat_type = ty_res;
- pat_env = env }
+ pat_type = expected_ty;
+ pat_env = !env }
|Ppat_variant(l, sarg) ->
let arg = may_map (fun p -> type_pat env p (newvar())) sarg in (* GAH: this is certainly false *)
let arg_type = match arg with None -> [] | Some arg -> [arg.pat_type] in
@@ -499,17 +530,17 @@ let rec type_pat env sp expected_ty =
rp {
pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()});
pat_loc = loc;
- pat_type = newty (Tvariant row);
- pat_env = env }
+ pat_type = newty (Tvariant row); (* GAH : should probably expected_ty *)
+ pat_env = !env }
|Ppat_record(lid_sp_list, closed) ->
let ty = expected_ty in
let type_label_pat (lid, sarg) =
- let label = Typetexp.find_label env loc lid in
+ let label = Typetexp.find_label !env loc lid in
begin_def ();
let (vars, ty_arg, ty_res) = instance_label false label in
if vars = [] then end_def ();
begin try
- unify env ty_res ty
+ unify_pat_types loc !env ty ty_res
with Unify trace ->
raise(Error(loc, Label_mismatch(lid, trace)))
end;
@@ -519,7 +550,7 @@ let rec type_pat env sp expected_ty =
generalize ty_arg;
List.iter generalize vars;
let instantiated tv =
- let tv = expand_head env tv in
+ let tv = expand_head !env tv in
tv.desc <> Tvar || tv.level <> generic_level in
if List.exists instantiated vars then
raise (Error(loc, Polymorphic_label lid))
@@ -532,52 +563,49 @@ let rec type_pat env sp expected_ty =
pat_desc = Tpat_record lbl_pat_list;
pat_loc = loc;
pat_type = ty;
- pat_env = env }
+ pat_env = !env }
|Ppat_array spl ->
let ty_elt = newvar() in
- unify env expected_ty (instance (Predef.type_array ty_elt));
+ unify_pat_types loc !env expected_ty (instance (Predef.type_array ty_elt));
let spl_ann = List.map (fun p -> (p,newvar())) spl in
let pl = List.map (fun (p,t) -> type_pat env p ty_elt) spl_ann in
rp {
pat_desc = Tpat_array pl;
pat_loc = loc;
pat_type = expected_ty;
- pat_env = env }
- |Ppat_or(sp1, sp2) ->
+ pat_env = !env }
+ |Ppat_or(sp1, sp2) -> (* GAH: what do we do for or patterns? ask garrigue if this is ok *)
let initial_pattern_variables = !pattern_variables in
- let nv = newvar() in
- let p1 = type_pat env sp1 nv in (* GAH: so wrong *)
+ let p1 = type_pat env sp1 expected_ty in
let p1_variables = !pattern_variables in
pattern_variables := initial_pattern_variables ;
- let p2 = type_pat env sp2 nv in (* GAH: again, so wrong *)
+ let p2 = type_pat env sp2 expected_ty in
let p2_variables = !pattern_variables in
- unify_pat env p2 p1.pat_type;
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 ;
rp {
pat_desc = Tpat_or(p1, alpha_pat alpha_env p2, None);
pat_loc = loc;
- pat_type = p1.pat_type;
- pat_env = env }
+ pat_type = expected_ty;
+ pat_env = !env }
|Ppat_lazy sp1 ->
let nv = newvar () in
- unify env expected_ty (instance (Predef.type_lazy_t nv));
+ unify_pat_types loc !env expected_ty (instance (Predef.type_lazy_t nv));
let p1 = type_pat env sp1 nv in
rp {
pat_desc = Tpat_lazy p1;
pat_loc = loc;
pat_type = expected_ty;
- pat_env = env }
+ pat_env = !env }
|Ppat_constraint(sp, sty) ->
- let nv = newvar () in
- let p = type_pat env sp nv in (* GAH: so wrong *)
- let ty, force = Typetexp.transl_simple_type_delayed env sty in
- unify_pat env p ty;
+ let ty, force = Typetexp.transl_simple_type_delayed !env sty in
+ unify_pat_types loc !env expected_ty ty;
+ let p = type_pat env sp expected_ty in (* GAH: so wrong *)
pattern_force := force :: !pattern_force;
- p
+ p (* GAH: this pattern will have the wrong location! *)
|Ppat_type lid ->
- build_or_pat env loc lid
+ build_or_pat !env loc lid
let get_ref r =
let v = !r in r := []; v
@@ -594,34 +622,32 @@ let add_pattern_variables env =
let type_pattern env spat scope expected_ty =
reset_pattern scope;
-
- let pat = type_pat env spat expected_ty in
-
- let new_env = add_pattern_variables env in
-
+ set_gadt_pattern_level ();
+ let new_env = ref env in
+ let pat = type_pat new_env spat expected_ty in
+ let new_env = add_pattern_variables !new_env in
(pat, new_env, get_ref pattern_force)
let type_pattern_list env spatl scope expected_tys =
-
- reset_local_unifier ();
- set_unification_type `Pattern;
- try_finally
- (fun () ->
- reset_pattern scope;
-
- let patl = List.map2 (fun p t -> type_pat env p t) spatl expected_tys in
- let new_env = add_pattern_variables env in
-
- (patl, new_env, get_ref pattern_force))
- (fun () ->
- set_unification_type `Expression)
+ reset_pattern scope;
+ set_gadt_pattern_level ();
+ let new_env = ref env in
+ let patl =
+ List.map2
+ (fun p t ->
+ type_pat new_env p t)
+ spatl expected_tys
+ in
+ let new_env = add_pattern_variables !new_env in
+ (patl, new_env, get_ref pattern_force)
+
+
let type_class_arg_pattern cl_num val_env met_env l spat =
-
reset_pattern None;
let nv = newvar () in
- let pat = type_pat val_env spat nv in
+ let pat = type_pat (ref val_env) spat nv in
if has_variants pat then begin
Parmatch.pressure_variants val_env [pat];
@@ -652,13 +678,13 @@ let type_self_pattern cl_num privty val_env met_env par_env spat =
in
reset_pattern None;
let nv = newvar() in
- let pat = type_pat val_env spat nv in (* GAH: so wrong *)
+ let pat = type_pat (ref val_env) spat nv in (* GAH: so wrong *)
List.iter (fun f -> f()) (get_ref pattern_force);
let meths = ref Meths.empty in
let vars = ref Vars.empty in
let pv = !pattern_variables in
pattern_variables := [];
- let (val_env, met_env, par_env) =
+ let ((val_env:Env.t), met_env, par_env) =
List.fold_right
(fun (id, ty, _loc) (val_env, met_env, par_env) ->
(Env.add_value id {val_type = ty; val_kind = Val_unbound} val_env,
@@ -1154,9 +1180,8 @@ let rec type_exp env sexp =
let arg = type_exp env sarg in
let ty_res = newvar() in
let cases, partial =
- type_cases_gadt env arg.exp_type ty_res (Some loc) caselist
+ type_cases env arg.exp_type ty_res (Some loc) caselist
in
- Format.fprintf Format.std_formatter " match type : %a\n%! " Printtyp.raw_type_expr ty_res ;
re {
exp_desc = Texp_match(arg, cases, partial);
exp_loc = loc;
@@ -2098,7 +2123,7 @@ and type_expect ?in_function env sexp ty_expected =
else ty_arg
in
let cases, partial =
- type_cases_gadt ~in_function:(loc_fun,ty_fun) env ty_arg ty_res
+ type_cases ~in_function:(loc_fun,ty_fun) env ty_arg ty_res
(Some loc) caselist in
let not_function ty =
let ls, tvar = list_labels env ty in
@@ -2155,7 +2180,7 @@ and type_expect ?in_function env sexp ty_expected =
| Pexp_match(sarg, caselist) -> (* GAH : check with garrigue that this is ok *)
let arg = type_exp env sarg in
let cases, partial =
- type_cases_gadt env arg.exp_type ty_expected (Some loc) caselist
+ type_cases env arg.exp_type ty_expected (Some loc) caselist
in
re {
exp_desc = Texp_match(arg, cases, partial);
@@ -2197,14 +2222,9 @@ and type_statement env sexp =
(* Typing of match cases *)
-and type_pattern_gadt env spat scope ty_arg =
- reset_local_unifier ();
- set_unification_type `Pattern;
- try_finally
- (fun () -> type_pattern env spat scope ty_arg )
- (fun () -> set_unification_type `Expression)
-and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist =
+
+and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
(* let ty_arg' = newvar () in *) (* GAH : must ask garrigue about this *)
let pattern_force = ref [] in
let pat_env_list =
@@ -2215,13 +2235,10 @@ and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist
let scope = Some (Annot.Idef loc) in
let (pat, ext_env, force) =
- if gadt then
- type_pattern_gadt env spat scope ty_arg
- else
- type_pattern env spat scope ty_arg
+ type_pattern env spat scope ty_arg
in
- let local_unifier = get_local_unifier () in
- pattern_force := force @ !pattern_force;
+
+
let pat =
if !Clflags.principal then begin
end_def ();
@@ -2231,12 +2248,12 @@ and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist
in
(* unify_pat env pat ty_arg'; (* GAH: probably wrong. what in the blazes does ty_arg' do?? *)*)
- (pat, ext_env,local_unifier))
+ (pat, ext_env))
caselist in
(* Check for polymorphic variants to close *)
- let fst3 (a,b,c) = a in
- let patl = List.map fst3 pat_env_list in
+
+ let patl = List.map fst pat_env_list in
if List.exists has_variants patl then begin
Parmatch.pressure_variants env patl;
@@ -2244,37 +2261,35 @@ and type_cases ?in_function ?(gadt=false) env ty_arg ty_res partial_loc caselist
end;
(* `Contaminating' unifications start here *)
List.iter (fun f -> f()) !pattern_force;
-
+
(* begin match pat_env_list with [] -> ()
| (pat, _) :: _ -> unify_pat env pat ty_arg (* GAH: probably incorrect; check with garrigue. if we readd this code then it doesn't work *)
end;*)
let in_function = if List.length caselist = 1 then in_function else None in
let cases =
List.map2
- (fun (pat, ext_env,local_unifier) (spat, sexp) ->
- List.iter (fun (t,t') -> t.desc <- Tlink t') local_unifier;
- try_finally
- (fun () ->
- let exp = type_expect ?in_function ext_env sexp ty_res in
- (pat, exp))
- (fun () -> List.iter (fun (t,_) -> t.desc <- Tunivar) local_unifier))
+ (fun (pat, ext_env) (spat, sexp) ->
+ let ty_res = expand_head ext_env ty_res in
+ let exp = type_expect ?in_function ext_env sexp ty_res in
+ (pat, exp))
pat_env_list caselist
in
let partial =
match partial_loc with
| None -> Partial
- | Some partial_loc -> Parmatch.check_partial partial_loc cases
+ | Some partial_loc ->
+ let r = Parmatch.check_partial partial_loc cases env in
+ r
in
add_delayed_check (fun () -> Parmatch.check_unused env cases);
cases, partial
-and type_cases_gadt ?in_function env ty_arg ty_res partial_loc caselist =
- type_cases ?in_function ~gadt:true env ty_arg ty_res partial_loc caselist
+(*and type_cases_gadt ?in_function env ty_arg ty_res partial_loc caselist =
+ type_cases ?in_function env ty_arg ty_res partial_loc caselist*)
(* Typing of let bindings *)
and type_let env rec_flag spat_sexp_list scope =
-
begin_def();
if !Clflags.principal then begin_def ();
let spatl = List.map (fun (spat, sexp) -> spat) spat_sexp_list in
@@ -2328,7 +2343,7 @@ and type_let env rec_flag spat_sexp_list scope =
| _ -> type_expect exp_env sexp pat.pat_type)
spat_sexp_list pat_list in
List.iter2
- (fun pat exp -> ignore(Parmatch.check_partial pat.pat_loc [pat, exp]))
+ (fun pat exp -> ignore(Parmatch.check_partial pat.pat_loc [pat, exp] env))
pat_list exp_list;
end_def();
List.iter2
@@ -2371,7 +2386,15 @@ let report_error ppf = function
fprintf ppf
"@[The constructor %a@ expects %i argument(s),@ \
but is applied here to %i argument(s)@]"
- longident lid expected provided
+ longident lid expected provided
+ | Constructor_inhabit_tunivar(t,lid) ->
+ fprintf ppf
+ "The constructor %a does not inhabit the univarsal type %a"
+ longident lid type_scheme t
+ | Constant_inhabit_tunivar t ->
+ fprintf ppf
+ "This constant does not inhabit the type universal type %a"
+ type_scheme t
| Label_mismatch(lid, trace) ->
report_unification_error ppf trace
(function ppf ->
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 3fb90ff34..5114d3429 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -65,6 +65,8 @@ val self_coercion : (Path.t * Location.t list ref) list ref
type error =
Polymorphic_label of Longident.t
| Constructor_arity_mismatch of Longident.t * int * int
+ | Constructor_inhabit_tunivar of type_expr * Longident.t
+ | Constant_inhabit_tunivar of type_expr
| Label_mismatch of Longident.t * (type_expr * type_expr) list
| Pattern_type_clash of (type_expr * type_expr) list
| Multiply_bound_variable of string
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 5c8ed6f58..6aa8932f8 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -121,6 +121,9 @@ module StringSet =
let compare = compare
end)
+
+
+
let transl_declaration env (name, sdecl) id =
(* Bind type parameters *)
reset_type_variables();
@@ -150,21 +153,32 @@ let transl_declaration env (name, sdecl) id =
raise(Error(sdecl.ptype_loc, Duplicate_constructor name));
all_constrs := StringSet.add name !all_constrs)
cstrs;
+
if List.length (List.filter (fun (_, args, _, _) -> args <> []) cstrs) (* GAH: MIGHT BE WRONG *)
> (Config.max_tag + 1) then
raise(Error(sdecl.ptype_loc, Too_many_constructors));
- if List.for_all (fun (_,_,x,_) -> match x with Some _ -> false | None -> true) cstrs then
+(* if List.for_all (fun (_,_,x,_) -> match x with Some _ -> false | None -> true) cstrs then
Type_variant
(List.map
(fun (name, args,_, loc) ->
(name, List.map (transl_simple_type env true) args))
cstrs)
- else
+ else*)
+
+ let ret =
Type_generalized_variant
(List.map
(fun (name, args,ret_type_opt, loc) ->
- (name, List.map (transl_simple_type env false) args,may_map (transl_simple_type env false) ret_type_opt)) (* GAH: calling transl_simple_type with fixed=false, ask garrigue if this is ok *)
+ let gadt =
+ match ret_type_opt with
+ | None -> None
+ | Some _ -> Some (ref [])
+ in
+ (name, List.map (transl_simple_type ~gadt env false) args,may_map (transl_simple_type ~gadt env false) ret_type_opt)) (* GAH: calling transl_simple_type with fixed=false, ask garrigue if this is ok *)
cstrs)
+ in
+ ret
+
| Ptype_record lbls ->
let all_labels = ref StringSet.empty in
List.iter
@@ -196,6 +210,9 @@ let transl_declaration env (name, sdecl) id =
type_variance = List.map (fun _ -> true, true, true) params;
} in
+
+
+
(* Check constraints *)
List.iter
(fun (ty, ty', loc) ->
@@ -247,6 +264,7 @@ module TypeSet =
end)
let rec check_constraints_rec env loc visited ty =
+
let ty = Ctype.repr ty in
if TypeSet.mem ty !visited then () else begin
visited := TypeSet.add ty !visited;
@@ -279,17 +297,19 @@ let check_constraints env (_, sdecl) (_, decl) =
List.iter
(fun (name, tyl,ret_type_opt) -> (* GAH: again, no idea *)
let styl,sret_type_opt =
- try let (_,sty,ret_type_opt (* added by me *) ,_) = List.find (fun (n,_,_,_) -> n = name) pl in sty,ret_type_opt (* GAH: lord, I have no idea what this is about *)
+ try let (_,sty,sret_type_opt (* added by me *) ,_) = List.find (fun (n,_,_,_) -> n = name) pl in sty,sret_type_opt (* GAH: lord, I have no idea what this is about *)
with Not_found -> assert false in
List.iter2
(fun sty ty ->
check_constraints_rec env sty.ptyp_loc visited ty)
styl tyl;
+
+ (* GAH : ask garrigue how to do the following: *)
match sret_type_opt,ret_type_opt with
| Some sr,Some r ->
check_constraints_rec env sr.ptyp_loc visited r
| _ ->
- ())
+ () )
l
in
begin match decl.type_kind with
@@ -526,7 +546,23 @@ let compute_variance_decl env check decl (required, loc) =
let tvl1 = List.map make_variance fvl in
let tvl2 = List.map make_variance fvl in
let tvl = tvl0 @ tvl1 in
- begin match decl.type_kind with
+ let is_gadt =
+ match decl.type_kind with
+ | Type_generalized_variant tll -> (* GAH: what in the blazes *)
+ let ret = ref false in
+ List.iter
+ (function
+ | (_,_,Some _) ->
+ ret:=true;
+ | _ -> ())
+ tll;
+ !ret
+ | _ -> false
+ in
+ if is_gadt then
+ List.map (fun _ -> (true,true,true)) params
+ else
+ begin begin match decl.type_kind with
| Type_abstract ->
begin match decl.type_manifest with
None -> assert false
@@ -544,8 +580,8 @@ let compute_variance_decl env check decl (required, loc) =
| None ->
List.iter (compute_variance env tvl true false false) tl
| Some ret_type ->
- List.iter (compute_variance env tvl true true true) tl) (* GAH: variance calculation, is this right *)
- tll
+ fatal_error "gadt not properly handled")
+ tll;
| Type_record (ftl, _) ->
List.iter
(fun (_, mut, ty) ->
@@ -566,7 +602,7 @@ let compute_variance_decl env check decl (required, loc) =
tvl0 required;
List.iter2
(fun (ty, c1, n1, t1) (_, c2, n2, t2) ->
- if !c1 && not !c2 || !n1 && not !n2
+ if !c1 && not !c2 || !n1 && not !n2
(* || !t1 && not !t2 && decl.type_kind = Type_abstract *)
then raise (Error(loc,
if not (!c2 || !n2) then Unbound_type_var (ty, decl)
@@ -582,6 +618,7 @@ let compute_variance_decl env check decl (required, loc) =
let ct = if decl.type_kind = Type_abstract then ct else cn in
(!co, !cn, !ct))
tvl0 required
+ end
let is_sharp id =
let s = Ident.name id in
@@ -613,6 +650,7 @@ let rec compute_variance_fixpoint env decls required variances =
(fun (id, decl) req -> if not (is_sharp id) then
ignore (compute_variance_decl new_env true decl req))
new_decls required;
+
new_decls, new_env
end
@@ -680,6 +718,8 @@ let name_recursion sdecl id decl =
else decl
| _ -> decl
+
+
(* Translate a set of mutually recursive type declarations *)
let transl_type_decl env name_sdecl_list =
(* Add dummy types for fixed rows *)
@@ -753,6 +793,7 @@ let transl_type_decl env name_sdecl_list =
List.map (fun (_, sdecl) -> sdecl.ptype_variance, sdecl.ptype_loc)
name_sdecl_list
in
+
let final_decls, final_env =
compute_variance_fixpoint env decls required (List.map init_variance decls)
in
@@ -818,7 +859,7 @@ let transl_with_constraint env id row_path sdecl =
Ctype.unify env (transl_simple_type env false ty)
(transl_simple_type env false ty')
with Ctype.Unify tr ->
- raise(Error(loc, Unconsistent_constraint tr)))
+ raise(Error(loc, Unconsistent_constraint tr))) (* GAH : Unconsistent is not a word *)
sdecl.ptype_cstrs;
let no_row = not (is_fixed_type sdecl) in
let decl =
diff --git a/typing/types.ml b/typing/types.ml
index d1ef644a3..f9f011092 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -105,14 +105,15 @@ and value_kind =
(* Constructor descriptions *)
type constructor_description =
- { cstr_res: type_expr; (* Type of the result *)
- cstr_existentials: type_expr list; (* list of existentials *)
- cstr_args: type_expr list; (* Type of the arguments *)
- cstr_arity: int; (* Number of arguments *)
- cstr_tag: constructor_tag; (* Tag for heap blocks *)
- cstr_consts: int; (* Number of constant constructors *)
- cstr_nonconsts: int; (* Number of non-const constructors *)
- cstr_private: private_flag } (* Read-only constructor? *)
+ { cstr_res: type_expr; (* Type of the result *)
+ cstr_existentials: type_expr list; (* list of existentials *)
+ cstr_args: type_expr list; (* Type of the arguments *)
+ cstr_arity: int; (* Number of arguments *)
+ cstr_tag: constructor_tag; (* Tag for heap blocks *)
+ cstr_consts: int; (* Number of constant constructors *) (* GAH: ask garrigue: why is this field here?? is it the same for each constructor?*)
+ cstr_nonconsts: int; (* Number of non-const constructors *)
+ cstr_all_ty_res: type_expr option list; (* The return type of all the constructors of the type *)
+ cstr_private: private_flag } (* Read-only constructor? *)
and constructor_tag =
Cstr_constant of int (* Constant constructor (an int) *)
diff --git a/typing/types.mli b/typing/types.mli
index 962dfd02e..ef0b3460e 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -102,14 +102,15 @@ and value_kind =
(* Constructor descriptions *)
type constructor_description =
- { cstr_res: type_expr; (* Type of the result *)
- cstr_existentials: type_expr list; (* list of existentials *)
- cstr_args: type_expr list; (* Type of the arguments *)
- cstr_arity: int; (* Number of arguments *)
- cstr_tag: constructor_tag; (* Tag for heap blocks *)
- cstr_consts: int; (* Number of constant constructors *)
- cstr_nonconsts: int; (* Number of non-const constructors *)
- cstr_private: private_flag } (* Read-only constructor? *)
+ { cstr_res: type_expr; (* Type of the result *)
+ cstr_existentials: type_expr list; (* list of existentials *)
+ cstr_args: type_expr list; (* Type of the arguments *)
+ cstr_arity: int; (* Number of arguments *)
+ cstr_tag: constructor_tag; (* Tag for heap blocks *)
+ cstr_consts: int; (* Number of constant constructors *) (* GAH: ask garrigue: why is this field here?? is it the same for each constructor?*)
+ cstr_nonconsts: int; (* Number of non-const constructors *)
+ cstr_all_ty_res: type_expr option list; (* The return type of all the constructors of the type *)
+ cstr_private: private_flag } (* Read-only constructor? *)
and constructor_tag =
Cstr_constant of int (* Constant constructor (an int) *)
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 838719b7c..d395a793e 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -158,6 +158,7 @@ let type_variable loc name =
try
Tbl.find name !type_variables
with Not_found ->
+ print_endline "raising type_variable";
raise(Error(loc, Unbound_type_variable ("'" ^ name)))
let wrap_method ty =
@@ -174,9 +175,11 @@ let rec swap_list = function
type policy = Fixed | Extensible | Univars
+let gadt_map = ref None
+
let rec transl_type env policy styp =
match styp.ptyp_desc with
- Ptyp_any ->
+ | Ptyp_any ->
if policy = Univars then new_pre_univar () else
if policy = Fixed then
raise (Error (styp.ptyp_loc, Unbound_type_variable "_"))
@@ -184,15 +187,25 @@ let rec transl_type env policy styp =
| Ptyp_var name ->
if name <> "" && name.[0] = '_' then
raise (Error (styp.ptyp_loc, Invalid_variable_name ("'" ^ name)));
- begin try
- instance (List.assoc name !univars)
- with Not_found -> try
- instance (fst(Tbl.find name !used_variables))
- with Not_found ->
- let v =
- if policy = Univars then new_pre_univar () else newvar () in
- used_variables := Tbl.add name (v, styp.ptyp_loc) !used_variables;
- v
+ begin
+ match !gadt_map with
+ | Some lst ->
+ begin try
+ List.assoc name !lst
+ with Not_found ->
+ let ret = newvar () in
+ lst := (name,ret) :: !lst;
+ ret end
+ | None ->
+ try
+ instance (List.assoc name !univars)
+ with Not_found -> try
+ instance (fst(Tbl.find name !used_variables))
+ with Not_found ->
+ let v =
+ if policy = Univars then new_pre_univar () else newvar () in
+ used_variables := Tbl.add name (v, styp.ptyp_loc) !used_variables;
+ v
end
| Ptyp_arrow(l, st1, st2) ->
let ty1 = transl_type env policy st1 in
@@ -215,14 +228,15 @@ let rec transl_type env policy styp =
in
List.iter2
(fun (sty, ty) ty' ->
+ Format.fprintf Format.std_formatter " ty: %a \n ty': %a \n\n%! " Printtyp.raw_type_expr ty Printtyp.raw_type_expr ty' ;
try unify_param env ty' ty with Unify trace ->
- raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
+ (print_endline "mismatch from trans_type ";raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace)))))
(List.combine stl args) params;
let constr = newconstr path args in
begin try
Ctype.enforce_constraints env constr
with Unify trace ->
- raise (Error(styp.ptyp_loc, Type_mismatch trace))
+ (print_endline "another mismatch from trans_type"; raise (Error(styp.ptyp_loc, Type_mismatch trace)))
end;
constr
| Ptyp_object fields ->
@@ -264,7 +278,7 @@ let rec transl_type env policy styp =
List.iter2
(fun (sty, ty) ty' ->
try unify_var env ty' ty with Unify trace ->
- raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
+ (print_endline "yet another";raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace)))))
(List.combine stl args) params;
let ty =
try Ctype.expand_head env (newconstr path args)
@@ -310,9 +324,18 @@ let rec transl_type env policy styp =
begin
try
let t =
- try List.assoc alias !univars
- with Not_found ->
- instance (fst(Tbl.find alias !used_variables))
+ try List.assoc alias !univars
+ with Not_found ->
+ match !gadt_map with
+ | Some lst ->
+ begin try
+ List.assoc alias !lst
+ with Not_found ->
+ let ret = newvar () in
+ lst := (alias,ret) :: !lst;
+ ret end
+ | None ->
+ instance (fst(Tbl.find alias !used_variables))
in
let ty = transl_type env policy st in
begin try unify_var env t ty with Unify trace ->
@@ -475,6 +498,10 @@ and transl_fields env policy seen =
newty (Tfield (s, Fpresent, ty1, ty2))
+
+
+
+
(* Make the rows "fixed" in this type, to make universal check easier *)
let rec make_fixed_univars ty =
let ty = repr ty in
@@ -503,6 +530,7 @@ let make_fixed_univars ty =
let create_package_mty = create_package_mty false
let globalize_used_variables env fixed =
+ Printf.printf "globalize_used_variables, fixed: %B\n%!" fixed;
let r = ref [] in
Tbl.iter
(fun name (ty, loc) ->
@@ -513,7 +541,10 @@ let globalize_used_variables env fixed =
r := (loc, v, Tbl.find name !type_variables) :: !r
with Not_found ->
if fixed && (repr ty).desc = Tvar then
- raise(Error(loc, Unbound_type_variable ("'"^name)));
+ begin
+ print_endline "raising";
+ raise(Error(loc, Unbound_type_variable ("'"^name)))
+ end;
let v2 = new_global_var () in
r := (loc, v, v2) :: !r;
type_variables := Tbl.add name v2 !type_variables)
@@ -526,15 +557,21 @@ let globalize_used_variables env fixed =
raise (Error(loc, Type_mismatch trace)))
!r
-let transl_simple_type env fixed styp =
- univars := []; used_variables := Tbl.empty;
+let transl_simple_type env fixed ?(gadt=None) styp = (* GAH : ask garrigue about this *)
+ (match gadt with
+ | Some _ -> print_endline "doing gadt thing"
+ | None ->
+ print_endline "not doing gadt thing");
+ univars := []; used_variables := Tbl.empty;gadt_map:=gadt;
+ Format.fprintf Format.std_formatter " styp = %a\n%! " Printast.print_core_type styp ;
let typ = transl_type env (if fixed then Fixed else Extensible) styp in
+ Format.fprintf Format.std_formatter " typ: %a \n\n%! " Printtyp.raw_type_expr typ;
globalize_used_variables env fixed ();
make_fixed_univars typ;
typ
let transl_simple_type_univars env styp =
- univars := []; used_variables := Tbl.empty; pre_univars := [];
+ univars := []; used_variables := Tbl.empty; pre_univars := [];gadt_map:=None;
begin_def ();
let typ = transl_type env Univars styp in
(* Only keep already global variables in used_variables *)
@@ -560,13 +597,13 @@ let transl_simple_type_univars env styp =
instance (Btype.newgenty (Tpoly (typ, univs)))
let transl_simple_type_delayed env styp =
- univars := []; used_variables := Tbl.empty;
+ univars := []; used_variables := Tbl.empty;gadt_map:=None;
let typ = transl_type env Extensible styp in
make_fixed_univars typ;
(typ, globalize_used_variables env false)
let transl_type_scheme env styp =
- reset_type_variables();
+ reset_type_variables();gadt_map:=None;
begin_def();
let typ = transl_simple_type env false styp in
end_def();
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index ec9042ce8..e83f42453 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -17,7 +17,7 @@
open Format;;
val transl_simple_type:
- Env.t -> bool -> Parsetree.core_type -> Types.type_expr
+ Env.t -> bool -> ?gadt:(string*Types.type_expr) list ref option -> Parsetree.core_type -> Types.type_expr
val transl_simple_type_univars:
Env.t -> Parsetree.core_type -> Types.type_expr
val transl_simple_type_delayed:
diff --git a/utils/misc.ml b/utils/misc.ml
index 68ca8e3da..784c92985 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -195,3 +195,15 @@ let rev_split_words s =
| _ -> split2 res i (j+1)
end
in split1 [] 0
+
+let map_filter f =
+ let rec loop =
+ function
+ | [] -> []
+ | x :: xs ->
+ match f x with
+ | None -> loop xs
+ | Some y ->
+ y :: loop xs
+ in
+ loop
diff --git a/utils/misc.mli b/utils/misc.mli
index 87f74e257..da0a36c5e 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -23,6 +23,8 @@ val map_end: ('a -> 'b) -> 'a list -> 'b list -> 'b list
(* [map_end f l t] is [map f l @ t], just more efficient. *)
val map_left_right: ('a -> 'b) -> 'a list -> 'b list
(* Like [List.map], with guaranteed left-to-right evaluation order *)
+val map_filter: ('a -> 'b option) -> 'a list -> 'b list
+ (* Mapping and filtering at the same time *)
val for_all2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
(* Same as [List.for_all] but for a binary predicate.
In addition, this [for_all2] never fails: given two lists