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

switched to abstract types, still needs work on exhaustion type. the code needs to be cleaned up. printfs need to be removed 

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadts@10682 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Jacques Le Normand 2010-09-19 04:55:40 +00:00
parent 8fc4a75a01
commit 56624533fb
21 changed files with 671 additions and 280 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
parsing/parser.mly
View File

@ -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) }
;

2
parsing/printast.ml
View File

@ -747,3 +747,5 @@ let print_expression = expression 0 ;;
let print_pattern = pattern 0 ;;
let print_core_type = core_type 0 ;;

1
parsing/printast.mli
View File

@ -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;;

10
typing/btype.ml
View File

@ -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)

2
typing/btype.mli
View File

@ -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

298
typing/ctype.ml
View File

@ -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 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 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 rec unify env t1 t2 =
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 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: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;
uni_equalities := TypeSetPair.empty;
unify env ty1 ty2
with Unify trace ->
uni_equalities := TypeSetPair.empty;
raise (Unify (expand_trace env trace))
raise (Unify (expand_trace !env trace))
let unify_gadt (env:Env.t ref) ty1 ty2 =
try
pattern_unification:=true;
unify env ty1 ty2;
pattern_unification:=false;
with Unify 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)

10
typing/ctype.mli
View File

@ -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

61
typing/datarepr.ml
View File

@ -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}

6
typing/env.ml
View File

@ -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 ->

122
typing/parmatch.ml
View File

@ -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

2
typing/parmatch.mli
View File

@ -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 *)

6
typing/typeclass.ml
View File

@ -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 ();

233
typing/typecore.ml
View File

@ -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;
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 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)
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 ->

2
typing/typecore.mli
View File

@ -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

61
typing/typedecl.ml
View File

@ -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 =

17
typing/types.ml
View File

@ -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) *)

17
typing/types.mli
View File

@ -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) *)

81
typing/typetexp.ml
View File

@ -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();

2
typing/typetexp.mli
View File

@ -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:

12
utils/misc.ml
View File

@ -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

2
utils/misc.mli
View File

@ -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