Skip to content

Commit

Permalink
Fix sailcov on foo @ match xxx
Browse files Browse the repository at this point in the history
  • Loading branch information
trdthg committed Aug 12, 2024
1 parent 48e0ca1 commit 814a274
Show file tree
Hide file tree
Showing 4 changed files with 81 additions and 3 deletions.
7 changes: 4 additions & 3 deletions src/lib/mappings.ml
Original file line number Diff line number Diff line change
Expand Up @@ -198,9 +198,10 @@ let name_gen prefix =

(* Take a arm like "<pat> => <exp>" and turn it into "<pat> => Some(<exp>)" *)
let some_arm = function
| Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, mk_exp (E_app (mk_id "Some", [exp]))), annot)
| Pat_aux (Pat_when (pat, guard, exp), annot) ->
Pat_aux (Pat_when (pat, guard, mk_exp (E_app (mk_id "Some", [exp]))), annot)
| Pat_aux (Pat_exp (pat, exp), ((l, _) as annot)) ->
Pat_aux (Pat_exp (pat, mk_exp ~loc:l (E_app (mk_id "Some", [exp]))), annot)
| Pat_aux (Pat_when (pat, guard, exp), ((l, _) as annot)) ->
Pat_aux (Pat_when (pat, guard, mk_exp ~loc:l (E_app (mk_id "Some", [exp]))), annot)

let wildcard_none = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit]))))

Expand Down
22 changes: 22 additions & 0 deletions test/sailcov/nested_mapping.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1
}

mapping encdec : bits(2) <-> ast = {
0b1 @ bool_not_bits(s) if true <-> B(s),
0b00 <-> Z()
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}
33 changes: 33 additions & 0 deletions test/sailcov/nested_mapping1.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>nested_mapping</title></head>
<body>
<h1>nested_mapping.sail (2/5) 40%</h1>
<code style="display: block">
default&nbsp;Order&nbsp;dec<br>
$include&nbsp;&lt;prelude.sail&gt;<br>
<br>
union&nbsp;ast&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;B&nbsp;:&nbsp;(bool),<br>
&nbsp;&nbsp;Z&nbsp;:&nbsp;unit<br>
}<br>
<br>
mapping&nbsp;bool_not_bits&nbsp;:&nbsp;bool&nbsp;&lt;-&gt;&nbsp;bits(1)&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">true</span>&nbsp;&nbsp;&nbsp;&lt;-&gt;&nbsp;0b0,<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">false</span>&nbsp;&nbsp;&lt;-&gt;&nbsp;0b1<br>
}<br>
<br>
mapping&nbsp;encdec&nbsp;&nbsp;:&nbsp;bits(2)&nbsp;&lt;-&gt;&nbsp;&nbsp;ast&nbsp;=&nbsp;{<br>
&nbsp;&nbsp;<span style="background-color: hsl(120, 85%, 80%)">0b00</span>&nbsp;&lt;-&gt;&nbsp;Z(),<br>
&nbsp;&nbsp;<span style="background-color: hsl(0, 85%, 80%)">0b1&nbsp;@&nbsp;bool_not_bits(s)</span>&nbsp;&lt;-&gt;&nbsp;B(s)<br>
}<br>
<br>
val&nbsp;main&nbsp;:&nbsp;unit&nbsp;-&gt;&nbsp;unit<br>
function&nbsp;main()&nbsp;=&nbsp;<span style="background-color: hsl(120, 85%, 80%)">{<br>
&nbsp;&nbsp;&nbsp;&nbsp;let&nbsp;_&nbsp;=&nbsp;encdec(0b00)<br>
}</span><br>
</code>
</body>
</html>
22 changes: 22 additions & 0 deletions test/sailcov/nested_mapping1.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
default Order dec
$include <prelude.sail>

union ast = {
B : (bool),
Z : unit
}

mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1
}

mapping encdec : bits(2) <-> ast = {
0b00 <-> Z(),
0b1 @ bool_not_bits(s) <-> B(s)
}

val main : unit -> unit
function main() = {
let _ = encdec(0b00)
}

0 comments on commit 814a274

Please sign in to comment.