Different, not quite correct yet, but I think slightly closer to correct, approach to convincing the typechecker to get along with this new type grammar.

This commit is contained in:
Graydon Hoare 2010-06-29 18:25:16 -07:00
parent 2a00a61ef3
commit f05fc6b9d7

View file

@ -2,7 +2,7 @@ open Common;;
open Semant;; open Semant;;
type tyspec = type tyspec =
TYSPEC_equiv of tyvar TYSPEC_equiv of (simpl * tyvar)
| TYSPEC_all | TYSPEC_all
| TYSPEC_resolved of (Ast.ty_param array) * Ast.ty | TYSPEC_resolved of (Ast.ty_param array) * Ast.ty
| TYSPEC_callable of (tyvar * tyvar array) (* out, ins *) | TYSPEC_callable of (tyvar * tyvar array) (* out, ins *)
@ -19,6 +19,10 @@ type tyspec =
| TYSPEC_vector of tyvar | TYSPEC_vector of tyvar
| TYSPEC_app of (tyvar * Ast.ty array) | TYSPEC_app of (tyvar * Ast.ty array)
and simpl = SIMPL_none
| SIMPL_exterior
| SIMPL_mutable
and dict = (Ast.ident, tyvar) Hashtbl.t and dict = (Ast.ident, tyvar) Hashtbl.t
and tyvar = tyspec ref;; and tyvar = tyspec ref;;
@ -101,7 +105,15 @@ let rec tyspec_to_str (ts:tyspec) : string =
else else
Ast.fmt_ty ff ty Ast.fmt_ty ff ty
| TYSPEC_equiv tv -> | TYSPEC_equiv (SIMPL_none, tv) ->
fmt_tyspec ff (!tv)
| TYSPEC_equiv (SIMPL_exterior, tv) ->
fmt ff "@";
fmt_tyspec ff (!tv)
| TYSPEC_equiv (SIMPL_mutable, tv) ->
fmt ff "mutable ";
fmt_tyspec ff (!tv) fmt_tyspec ff (!tv)
| TYSPEC_callable (out, ins) -> | TYSPEC_callable (out, ins) ->
@ -156,7 +168,7 @@ let iflog cx thunk =
let rec resolve_tyvar (tv:tyvar) : tyvar = let rec resolve_tyvar (tv:tyvar) : tyvar =
match !tv with match !tv with
TYSPEC_equiv subtv -> resolve_tyvar subtv TYSPEC_equiv (_, subtv) -> resolve_tyvar subtv
| _ -> tv | _ -> tv
;; ;;
@ -243,20 +255,23 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
*) *)
and unify_tyvars' (simplify:bool) (av:tyvar) (bv:tyvar) : unit = and unify_tyvars' (simplify:bool) (av:tyvar) (bv:tyvar) : unit =
let (a, b) = ((resolve_tyvar av), (resolve_tyvar bv)) in let (a, b) = ((resolve_tyvar av), (resolve_tyvar bv)) in
let simplified tv = let wrap tv =
match !tv with match !tv with
TYSPEC_resolved (params_a, Ast.TY_mutable ty_a) -> TYSPEC_resolved (params, Ast.TY_mutable ty) ->
Some (ref (TYSPEC_resolved (params_a, ty_a))) tv := TYSPEC_equiv (SIMPL_mutable,
| TYSPEC_resolved (params_a, Ast.TY_exterior ty_a) -> (ref (TYSPEC_resolved (params, ty))));
Some (ref (TYSPEC_resolved (params_a, ty_a))) true
| _ -> None | TYSPEC_resolved (params, Ast.TY_exterior ty) ->
tv := TYSPEC_equiv (SIMPL_exterior,
(ref (TYSPEC_resolved (params, ty))));
true
| _ -> false
in in
if simplify if simplify
then then
match (simplified a, simplified b) with if (wrap a) || (wrap b)
(Some a', _) -> unify_tyvars' simplify a' bv then unify_tyvars' simplify a b
| (_, Some b') -> unify_tyvars' simplify av b' else unify_tyvars'' a b
| (None, None) -> unify_tyvars'' av bv
else else
unify_tyvars'' av bv unify_tyvars'' av bv
@ -777,8 +792,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
TYSPEC_vector av TYSPEC_vector av
in in
let c = ref result in let c = ref result in
a := TYSPEC_equiv c; a := TYSPEC_equiv (SIMPL_none, c);
b := TYSPEC_equiv c b := TYSPEC_equiv (SIMPL_none, c)
and unify_ty_parametric and unify_ty_parametric
(simplify:bool) (simplify:bool)
@ -1371,23 +1386,20 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| _ -> bug () "check_auto_tyvar: no slot defn" | _ -> bug () "check_auto_tyvar: no slot defn"
in in
let get_resolved_ty tv id = let rec get_resolved_ty tv id =
let ts = !(resolve_tyvar tv) in match !tv with
match ts with
TYSPEC_resolved ([||], ty) -> ty TYSPEC_resolved ([||], ty) -> ty
| TYSPEC_vector (tv) -> | TYSPEC_vector tv ->
begin Ast.TY_vec (get_resolved_ty tv id)
match !(resolve_tyvar tv) with | TYSPEC_equiv (SIMPL_none, tv) ->
TYSPEC_resolved ([||], ty) -> get_resolved_ty tv id
(Ast.TY_vec ty) | TYSPEC_equiv (SIMPL_mutable, tv) ->
| _ -> Ast.TY_mutable (get_resolved_ty tv id)
err (Some id) | TYSPEC_equiv (SIMPL_exterior, tv) ->
"unresolved vector-element type in %s (%d)" Ast.TY_exterior (get_resolved_ty tv id)
(tyspec_to_str ts) (int_of_node id)
end
| _ -> err (Some id) | _ -> err (Some id)
"unresolved type %s (%d)" "unresolved type %s (%d)"
(tyspec_to_str ts) (tyspec_to_str !tv)
(int_of_node id) (int_of_node id)
in in