From 241305caab232b04666704dc6853c41312cd283a Mon Sep 17 00:00:00 2001 From: Roy Frostig Date: Fri, 25 Jun 2010 00:47:23 -0700 Subject: [PATCH] Resolve and typecheck patterns in pattern alt redux. This time featuring way more correctness. --- src/boot/fe/ast.ml | 8 +++- src/boot/fe/item.ml | 30 ++++++------- src/boot/me/resolve.ml | 63 ++++++++++++++-------------- src/boot/me/semant.ml | 47 +++++++++++++++++---- src/boot/me/trans.ml | 4 +- src/boot/me/type.ml | 55 ++++++++++++++++-------- src/boot/me/walk.ml | 14 ++++--- src/test/run-pass/generic-tag-alt.rs | 2 +- 8 files changed, 142 insertions(+), 81 deletions(-) diff --git a/src/boot/fe/ast.ml b/src/boot/fe/ast.ml index 0903751066c..770b57bf82b 100644 --- a/src/boot/fe/ast.ml +++ b/src/boot/fe/ast.ml @@ -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) diff --git a/src/boot/fe/item.ml b/src/boot/fe/item.ml index 209526e52eb..031b9e49441 100644 --- a/src/boot/fe/item.ml +++ b/src/boot/fe/item.ml @@ -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) ^ "'")) diff --git a/src/boot/me/resolve.ml b/src/boot/me/resolve.ml index 2c718778197..6c4810404b2 100644 --- a/src/boot/me/resolve.ml +++ b/src/boot/me/resolve.ml @@ -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"; diff --git a/src/boot/me/semant.ml b/src/boot/me/semant.ml index ddf148380d0..b2ce7b793e0 100644 --- a/src/boot/me/semant.ml +++ b/src/boot/me/semant.ml @@ -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 diff --git a/src/boot/me/trans.ml b/src/boot/me/trans.ml index 3d23a94569a..02b8e3f709f 100644 --- a/src/boot/me/trans.ml +++ b/src/boot/me/trans.ml @@ -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 diff --git a/src/boot/me/type.ml b/src/boot/me/type.ml index a1bc886bf4d..01438142831 100644 --- a/src/boot/me/type.ml +++ b/src/boot/me/type.ml @@ -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 diff --git a/src/boot/me/walk.ml b/src/boot/me/walk.ml index 30b30e32e53..57864f99149 100644 --- a/src/boot/me/walk.ml +++ b/src/boot/me/walk.ml @@ -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 diff --git a/src/test/run-pass/generic-tag-alt.rs b/src/test/run-pass/generic-tag-alt.rs index 302096fb63c..1f4c5465157 100644 --- a/src/test/run-pass/generic-tag-alt.rs +++ b/src/test/run-pass/generic-tag-alt.rs @@ -3,7 +3,7 @@ fn altfoo[T](foo[T] f) { auto hit = false; alt (f) { - case (arm(x)) { + case (arm[T](x)) { log "in arm"; hit = true; }