Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix type and coverage checking for patterns #538

Merged
merged 10 commits into from
Jul 5, 2019
Merged

Fix type and coverage checking for patterns #538

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
6e7f140
Clean up operator typing
rossberg Jun 27, 2019
1c01477
Fix pattern typing
rossberg Jul 1, 2019
2a0589d
Print Non as None
rossberg Jul 1, 2019
3ab5d6e
Eps
rossberg Jul 1, 2019
d49cb41
Claudio's comments
rossberg Jul 3, 2019
11d9386
Fix obj coverage; more tests
rossberg Jul 5, 2019
f1114d6
Coverage for uninhabited types
rossberg Jul 5, 2019
be15551
Update test/run/coverage.as
rossberg Jul 5, 2019
e57e884
Merge branch 'master' into pat-lub
rossberg Jul 5, 2019
8aaab4b
Test expectation
rossberg Jul 5, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 32 additions & 28 deletions src/as_frontend/coverage.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,8 @@ let value_of_lit = function
| PreLit _ -> assert false


let (&&&) = (&&) (* No short-cutting *)

let skip_pat pat sets =
sets.alts <- AtSet.add pat.at sets.alts;
true
Expand All @@ -79,7 +81,7 @@ let rec match_pat ctxt desc pat t sets =
| LitP lit ->
match_lit ctxt desc (value_of_lit !lit) t sets
| SignP (op, lit) ->
let f = Operator.unop pat.note op in
let f = Operator.unop op (Operator.type_unop op pat.note) in
match_lit ctxt desc (f (value_of_lit !lit)) t sets
| TupP pats ->
let ts = Type.as_tup (Type.promote t) in
Expand All @@ -90,19 +92,13 @@ let rec match_pat ctxt desc pat t sets =
| _ -> assert false
in match_tup ctxt [] descs pats ts sets
| ObjP pfs ->
let t' = Type.promote t in
let sensible (pf : pat_field) =
List.exists (fun {Type.lab; _} -> pf.it.id.it = lab) (snd (Type.as_obj_sub pf.it.id.it t')) in
let pfs' = List.filter sensible pfs in
let tf_of_pf (pf : pat_field) =
List.find (fun {Type.lab; _} -> pf.it.id.it = lab) (snd (Type.as_obj_sub pf.it.id.it t')) in
let tfs' = List.map tf_of_pf pfs' in
let _, tfs = Type.as_obj (Type.promote t) in
let descs =
match desc with
| Obj descs -> descs
| Any -> List.map (fun _ -> Any) pfs'
| Any -> List.map (fun _ -> Any) pfs
| _ -> assert false
in match_obj ctxt [] descs pfs' tfs' sets
in match_obj ctxt [] descs pfs tfs sets
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks okay. You look up the right type in match_obj below. Do you fix a bug with this change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It was just meant as a simplification. Especially the sensible filtering seemed dubious to me -- AFAICS, pfs' should never have been smaller than pfs, unless the type checker is unsound. Do you remember why you needed it?

But after adding a few more tests, I apparently introduced new bugs. Fixed now and more tests added to coverage.as.

Copy link
Contributor

@ggreif ggreif Jul 5, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I introduced sensible in #296 (commit 2bd2ed4) and the commit message says "now we only iterate over fields that are available as indicated by the
type." It fixed a crash in the type checker. The test it was relevant for was test/run/objpat-iter.as, e.g.

switch ([1,2]) {
   case { vals; len } { ...

This is the sequences-as-objects behaviour that you have eliminated recently. I can dig deeper, but I think this is moot now.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, thanks!

| OptP pat1 ->
let t' = Type.as_opt (Type.promote t) in
(match desc with
Expand All @@ -113,7 +109,7 @@ let rec match_pat ctxt desc pat t sets =
| Opt desc' ->
match_pat (InOpt ctxt) desc' pat1 t' sets
| Any ->
fail ctxt (Val Value.Null) sets &&
fail ctxt (Val Value.Null) sets &&&
match_pat (InOpt ctxt) Any pat1 t' sets
| _ -> assert false
)
Expand All @@ -127,15 +123,19 @@ let rec match_pat ctxt desc pat t sets =
else if Type.span t = Some (TagSet.cardinal ls + 1) then
match_pat (InTag (ctxt, id.it)) Any pat1 t' sets
else
fail ctxt (NotTag (TagSet.add id.it ls)) sets &&
fail ctxt (NotTag (TagSet.add id.it ls)) sets &&&
match_pat (InTag (ctxt, id.it)) Any pat1 t' sets
| Tag (desc', l) ->
if id.it <> l
then fail ctxt desc sets
else match_pat (InTag (ctxt, l)) desc' pat1 t' sets
if id.it = l then
match_pat (InTag (ctxt, l)) desc' pat1 t' sets
else
fail ctxt desc sets
| Any ->
fail ctxt (NotTag (TagSet.singleton id.it)) sets &&
match_pat (InTag (ctxt, id.it)) Any pat1 t' sets
if Type.span t = Some 1 then
match_pat (InTag (ctxt, id.it)) Any pat1 t' sets
ggreif marked this conversation as resolved.
Show resolved Hide resolved
else
fail ctxt (NotTag (TagSet.singleton id.it)) sets &&&
match_pat (InTag (ctxt, id.it)) Any pat1 t' sets
| _ -> assert false
)
| AltP (pat1, pat2) ->
Expand All @@ -153,19 +153,21 @@ and match_lit ctxt desc v t sets =
if Type.span t = Some 1 then
succeed ctxt desc_succ sets
else
succeed ctxt desc_succ sets &&
fail ctxt (desc_fail ValSet.empty) sets
fail ctxt (desc_fail ValSet.empty) sets &&&
succeed ctxt desc_succ sets
| Val v' ->
if Value.equal v v'
then succeed ctxt desc sets
else fail ctxt desc sets
if Value.equal v v' then
succeed ctxt desc sets
else
fail ctxt desc sets
| NotVal vs ->
if ValSet.mem v vs then
fail ctxt desc sets
else if Type.span t = Some (ValSet.cardinal vs + 1) then
succeed ctxt desc_succ sets
else
succeed ctxt desc_succ sets && fail ctxt (desc_fail vs) sets
fail ctxt (desc_fail vs) sets &&&
succeed ctxt desc_succ sets
| Opt _ ->
fail ctxt desc sets
| _ ->
Expand All @@ -181,11 +183,13 @@ and match_tup ctxt descs_r descs pats ts sets =
assert false

and match_obj ctxt descs_r descs (pfs : pat_field list) tfs sets =
match descs, pfs, tfs with
| [], [], [] ->
match descs, pfs with
| [], [] ->
succeed ctxt (Obj (List.rev descs_r)) sets
| desc::descs', pf::pfs', Type.{lab; typ}::tfs' ->
match_pat (InObj (ctxt, descs_r, descs', pfs', tfs')) desc pf.it.pat typ sets
| desc::descs', pf::pfs' ->
let tf = List.find (fun tf -> tf.Type.lab = pf.it.id.it) tfs in
match_pat (InObj (ctxt, descs_r, descs', pfs', tfs))
desc pf.it.pat tf.Type.typ sets
| _ ->
assert false

Expand Down Expand Up @@ -225,7 +229,7 @@ and fail ctxt desc sets : bool =
fail ctxt' (Tag (desc, l)) sets
| InTup (ctxt', descs', descs, pats, _ts) ->
fail ctxt' (Tup (List.rev descs' @ [desc] @ descs)) sets
| InObj (ctxt', descs', descs, pats, _ts) ->
| InObj (ctxt', descs', descs, pats, _tfs) ->
fail ctxt' (Obj (List.rev descs' @ [desc] @ descs)) sets
| InAlt1 (ctxt', at1, pat2, t) ->
match_pat (InAlt2 (ctxt', pat2.at)) desc pat2 t sets
Expand Down
Loading