Resolve and typecheck patterns in pattern alt redux. This time featuring way more correctness.

This commit is contained in:
Roy Frostig 2010-06-25 00:47:23 -07:00
parent 0d9565a4c1
commit 241305caab
8 changed files with 142 additions and 81 deletions

View File

@ -299,9 +299,14 @@ and domain =
DOMAIN_local
| DOMAIN_thread
(*
* PAT_tag uses lval for the tag constructor so that we can reuse our lval
* resolving machinery. The lval is restricted during parsing to have only
* named components.
*)
and pat =
PAT_lit of lit
| PAT_tag of ((name identified) * (pat array))
| PAT_tag of (lval * (pat array))
| PAT_slot of ((slot identified) * ident)
| PAT_wild
@ -331,6 +336,7 @@ and lval_component =
| COMP_atom of atom
(* identifying the name_base here is sufficient to identify the full lval *)
and lval =
LVAL_base of name_base identified
| LVAL_ext of (lval * lval_component)

View File

@ -127,6 +127,16 @@ and parse_auto_slot_and_init
and parse_stmts (ps:pstate) : Ast.stmt array =
let apos = lexpos ps in
let rec name_to_lval (apos:pos) (bpos:pos) (name:Ast.name)
: Ast.lval =
match name with
Ast.NAME_base nb ->
Ast.LVAL_base (span ps apos bpos nb)
| Ast.NAME_ext (n, nc) ->
Ast.LVAL_ext (name_to_lval apos bpos n, Ast.COMP_named nc)
in
match peek ps with
LOG ->
@ -139,15 +149,6 @@ and parse_stmts (ps:pstate) : Ast.stmt array =
bump ps;
begin
let rec name_to_lval (bpos:pos) (name:Ast.name)
: Ast.lval =
match name with
Ast.NAME_base nb ->
Ast.LVAL_base (span ps apos bpos nb)
| Ast.NAME_ext (n, nc) ->
Ast.LVAL_ext (name_to_lval bpos n, Ast.COMP_named nc)
in
let rec carg_path_to_lval (bpos:pos) (path:Ast.carg_path)
: Ast.lval =
match path with
@ -171,7 +172,7 @@ and parse_stmts (ps:pstate) : Ast.stmt array =
let synthesise_check_call (bpos:pos) (constr:Ast.constr)
: (Ast.lval * (Ast.atom array)) =
let lval = name_to_lval bpos constr.Ast.constr_name in
let lval = name_to_lval apos bpos constr.Ast.constr_name in
let args =
Array.map (carg_to_atom bpos) constr.Ast.constr_args
in
@ -243,13 +244,14 @@ and parse_stmts (ps:pstate) : Ast.stmt array =
|_ -> raise (unexpected ps)
end
else
let pats =
paren_comma_list parse_pat ps
in
Ast.PAT_tag ((span ps apos bpos name), pats)
let lv = name_to_lval apos bpos name in
Ast.PAT_tag (lv, paren_comma_list parse_pat ps)
| LIT_INT _ | LIT_CHAR _ | LIT_BOOL _ ->
Ast.PAT_lit (Pexp.parse_lit ps)
| UNDERSCORE -> bump ps; Ast.PAT_wild
| tok -> raise (Parse_err (ps,
"Expected pattern but found '" ^
(string_of_tok tok) ^ "'"))

View File

@ -868,56 +868,57 @@ let resolve_recursion
let pattern_resolving_visitor
(cx:ctxt)
(scopes:scope list ref)
(inner:Walk.visitor) : Walk.visitor =
let not_tag_ctor (nid:Ast.name identified) : unit =
err (Some nid.id) "'%s' is not a tag constructor"
(string_of_name nid.node)
let not_tag_ctor nm id : unit =
err (Some id) "'%s' is not a tag constructor" (string_of_name nm)
in
let resolve_pat_tag
(namei:Ast.name identified)
(name:Ast.name)
(id:node_id)
(pats:Ast.pat array)
(tag_ctor_id:node_id)
: unit =
(* NB this isn't really the proper tag type, since we aren't applying any
* type parameters from the tag constructor in the pattern, but since we
* are only looking at the fact that it's a tag-like type at all, and
* asking for its arity, it doesn't matter that the possibly parametric
* tag type has its parameters unbound here. *)
let tag_ty =
fn_output_ty
(Hashtbl.find cx.ctxt_all_item_types tag_ctor_id)
fn_output_ty (Hashtbl.find cx.ctxt_all_item_types tag_ctor_id)
in
begin
match tag_ty with
Ast.TY_tag _
| Ast.TY_iso _ ->
let tag_ty_tup = tag_or_iso_ty_tup_by_name tag_ty namei.node in
let tag_ty_tup = tag_or_iso_ty_tup_by_name tag_ty name in
let arity = Array.length tag_ty_tup in
if (Array.length pats) == arity
then Hashtbl.add cx.ctxt_pattag_to_item namei.id tag_ctor_id
else err (Some namei.id)
"tag pattern '%s' with wrong number of components"
(string_of_name namei.node)
| _ -> not_tag_ctor namei
if (Array.length pats) != arity
then
err (Some id)
"tag pattern '%s' with wrong number of components"
(string_of_name name)
else ()
| _ -> not_tag_ctor name id
end
in
let resolve_arm { node = arm } =
match fst arm with
Ast.PAT_tag (namei, pats) ->
begin
match lookup_by_name cx !scopes namei.node with
None ->
err (Some namei.id) "unresolved tag constructor '%s'"
(string_of_name namei.node)
| Some (_, tag_ctor_id) when referent_is_item cx tag_ctor_id ->
(*
* FIXME we should actually check here that the function
* is a tag value-ctor. For now this actually allows any
* function returning a tag type to pass as a tag pattern.
*)
resolve_pat_tag namei pats tag_ctor_id
|_ -> not_tag_ctor namei
end
Ast.PAT_tag (lval, pats) ->
let lval_nm = lval_to_name lval in
let lval_id = lval_base_id lval in
let tag_ctor_id = lval_to_referent cx lval_id in
if referent_is_item cx tag_ctor_id
(*
* FIXME we should actually check here that the function
* is a tag value-ctor. For now this actually allows any
* function returning a tag type to pass as a tag pattern.
*)
then resolve_pat_tag lval_nm lval_id pats tag_ctor_id
else not_tag_ctor lval_nm lval_id
| _ -> ()
in
@ -968,8 +969,8 @@ let process_crate
let passes_2 =
[|
(scope_stack_managing_visitor scopes
(pattern_resolving_visitor cx scopes
Walk.empty_visitor))
(pattern_resolving_visitor cx
Walk.empty_visitor))
|]
in
log cx "running primary resolve passes";

View File

@ -102,7 +102,6 @@ type ctxt =
(* reference id --> definition id *)
ctxt_lval_to_referent: (node_id,node_id) Hashtbl.t;
ctxt_pattag_to_item: (node_id,node_id) Hashtbl.t;
ctxt_required_items: (node_id, (required_lib * nabi_conv)) Hashtbl.t;
ctxt_required_syms: (node_id, string) Hashtbl.t;
@ -187,7 +186,6 @@ let new_ctxt sess abi crate =
ctxt_all_lvals = Hashtbl.create 0;
ctxt_all_defns = Hashtbl.create 0;
ctxt_lval_to_referent = Hashtbl.create 0;
ctxt_pattag_to_item = Hashtbl.create 0;
ctxt_required_items = crate.Ast.crate_required;
ctxt_required_syms = crate.Ast.crate_required_syms;
@ -409,14 +407,29 @@ let fn_output_ty (fn_ty:Ast.ty) : Ast.ty =
| _ -> bug () "fn_output_ty on non-TY_fn"
;;
(* name of tag constructor function -> name for indexing in the ty_tag *)
let rec tag_ctor_name_to_tag_name (name:Ast.name) : Ast.name =
match name with
Ast.NAME_base nb ->
begin
match nb with
Ast.BASE_ident _ -> name
| Ast.BASE_app (id, _) -> Ast.NAME_base (Ast.BASE_ident id)
| _ ->
bug () "tag_or_iso_ty_tup_by_name with non-tag-ctor name"
end
| Ast.NAME_ext (inner_name, _) -> tag_ctor_name_to_tag_name inner_name
;;
let tag_or_iso_ty_tup_by_name (ty:Ast.ty) (name:Ast.name) : Ast.ty_tup =
match ty with
Ast.TY_tag tags ->
Hashtbl.find tags name
| Ast.TY_iso { Ast.iso_index = i; Ast.iso_group = gp } ->
Hashtbl.find gp.(i) name
| _ ->
bug () "tag_or_iso_ty_tup_by_name called with non-tag or -iso type"
let tagname = tag_ctor_name_to_tag_name name in
match ty with
Ast.TY_tag tags ->
Hashtbl.find tags tagname
| Ast.TY_iso { Ast.iso_index = i; Ast.iso_group = gp } ->
Hashtbl.find gp.(i) tagname
| _ ->
bug () "tag_or_iso_ty_tup_by_name called with non-tag or -iso type"
;;
let defn_is_slot (d:defn) : bool =
@ -499,6 +512,22 @@ let atoms_to_names (atoms:Ast.atom array)
atoms
;;
let rec lval_to_name (lv:Ast.lval) : Ast.name =
match lv with
Ast.LVAL_base { node = nb } ->
Ast.NAME_base nb
| Ast.LVAL_ext (lv, lv_comp) ->
let comp =
begin
match lv_comp with
Ast.COMP_named comp -> comp
| _ -> bug ()
"lval_to_name with lval that contains non-name components"
end
in
Ast.NAME_ext (lval_to_name lv, comp)
;;
let rec lval_base_id (lv:Ast.lval) : node_id =
match lv with
Ast.LVAL_base nbi -> nbi.id

View File

@ -3761,8 +3761,8 @@ let trans_visitor
Ast.PAT_lit lit ->
trans_compare Il.JNE (trans_lit lit) (Il.Cell src_cell)
| Ast.PAT_tag (tag_namei, pats) ->
let tag_name = tag_namei.node in
| Ast.PAT_tag (lval, pats) ->
let tag_name = tag_ctor_name_to_tag_name (lval_to_name lval) in
let ty_tag =
match slot_ty src_slot with
Ast.TY_tag tag_ty -> tag_ty

View File

@ -881,7 +881,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
in
match lval with
Ast.LVAL_base nbi ->
let referent = Hashtbl.find cx.ctxt_lval_to_referent nbi.id in
let referent = lval_to_referent cx nbi.id in
begin
match Hashtbl.find cx.ctxt_all_defns referent with
DEFN_slot slot ->
@ -1196,33 +1196,54 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| _ -> ()
in
(*
* Tag patterns give us the type of every sub-pattern in the tag tuple, so
* we can "expect" those types by pushing them on a stack. Checking a
* pattern therefore involves seeing that it matches the "expected" type,
* and in turn setting any expectations for the inner descent.
*)
let visit_pat_pre (pat:Ast.pat) : unit =
let expected = pat_tv() in
match pat with
Ast.PAT_lit lit -> unify_lit lit expected
| Ast.PAT_tag (namei, _) ->
| Ast.PAT_tag (lval, _) ->
let expect ty =
let tv = ref TYSPEC_all in
unify_ty ty tv;
push_pat_tv tv;
in
let item_id = Hashtbl.find cx.ctxt_pattag_to_item namei.id in
let tag_ty =
fn_output_ty (Hashtbl.find cx.ctxt_all_item_types item_id)
in
let tag_ty_tup = tag_or_iso_ty_tup_by_name tag_ty namei.node in
let tag_tv = ref TYSPEC_all in
unify_ty tag_ty tag_tv;
unify_tyvars expected tag_tv;
List.iter
begin
fun slot ->
match slot.Ast.slot_ty with
let lval_nm = lval_to_name lval in
(* The lval here is our tag constructor, which we've already
* resolved (in Resolve) to have a the actual tag constructor
* function item as its referent. It should hence unify
* exactly to that function type, rebuilt under any latent type
* parameters applied in the lval. *)
let lval_tv = ref TYSPEC_all in
unify_lval lval lval_tv;
let tag_ctor_ty =
match !(resolve_tyvar lval_tv) with
TYSPEC_resolved (_, ty) -> ty
| _ ->
bug () "tag constructor is not a fully resolved type."
in
let tag_ty = fn_output_ty tag_ctor_ty in
let tag_ty_tup = tag_or_iso_ty_tup_by_name tag_ty lval_nm in
let tag_tv = ref TYSPEC_all in
unify_ty tag_ty tag_tv;
unify_tyvars expected tag_tv;
List.iter
begin
fun slot ->
match slot.Ast.slot_ty with
Some ty -> expect ty
| None -> bug () "no slot type in tag slot tuple"
end
(List.rev (Array.to_list tag_ty_tup));
| None -> bug () "no slot type in tag slot tuple"
end
(List.rev (Array.to_list tag_ty_tup));
| Ast.PAT_slot (sloti, _) ->
unify_slot sloti.node (Some sloti.id) expected

View File

@ -655,15 +655,17 @@ and walk_pat
let walk p =
match p with
Ast.PAT_lit lit -> walk_lit v lit
| Ast.PAT_tag (_, pats) -> Array.iter (walk_pat v) pats
| Ast.PAT_tag (lv, pats) ->
walk_lval v lv;
Array.iter (walk_pat v) pats
| Ast.PAT_slot (si, _) -> walk_slot_identified v si
| Ast.PAT_wild -> ()
in
walk_bracketed
v.visit_pat_pre
(fun _ -> walk p)
v.visit_pat_post
p
walk_bracketed
v.visit_pat_pre
(fun _ -> walk p)
v.visit_pat_post
p
and walk_block

View File

@ -3,7 +3,7 @@ type foo[T] = tag(arm(T));
fn altfoo[T](foo[T] f) {
auto hit = false;
alt (f) {
case (arm(x)) {
case (arm[T](x)) {
log "in arm";
hit = true;
}