Skip to content

Commit

Permalink
Add a when clause that applies to both sides of a mapping
Browse files Browse the repository at this point in the history
  • Loading branch information
Alasdair committed Mar 5, 2025
1 parent 54dd131 commit 571a4db
Show file tree
Hide file tree
Showing 7 changed files with 80 additions and 6 deletions.
33 changes: 29 additions & 4 deletions src/lib/initial_check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1846,14 +1846,39 @@ let pexp_of_mpexp (MPat_aux (aux, annot)) exp =
| MPat_pat mpat -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
| MPat_when (mpat, guard) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)

let rec to_ast_mapcl doc attrs ctx (P.MCL_aux (mapcl, l)) =
match mapcl with
let apply_when_guard guard (MCL_aux (mcl, annot)) =
match mcl with
| MCL_bidir (MPat_aux (MPat_pat mpat1, pexp_annot1), MPat_aux (MPat_pat mpat2, pexp_annot2)) ->
MCL_aux
( MCL_bidir (MPat_aux (MPat_when (mpat1, guard), pexp_annot1), MPat_aux (MPat_when (mpat2, guard), pexp_annot2)),
annot
)
| MCL_forwards (Pat_aux (Pat_exp (pat, exp), pexp_annot)) ->
MCL_aux (MCL_forwards (Pat_aux (Pat_when (pat, guard, exp), pexp_annot)), annot)
| MCL_backwards (Pat_aux (Pat_exp (pat, exp), pexp_annot)) ->
MCL_aux (MCL_backwards (Pat_aux (Pat_when (pat, guard, exp), pexp_annot)), annot)
| MCL_bidir (MPat_aux (MPat_when (_, if_guard), _), _)
| MCL_bidir (_, MPat_aux (MPat_when (_, if_guard), _))
| MCL_forwards (Pat_aux (Pat_when (_, if_guard, _), _))
| MCL_backwards (Pat_aux (Pat_when (_, if_guard, _), _)) ->
raise
(Reporting.err_general
(Hint ("'if' clause here", exp_loc if_guard, exp_loc guard))
"Mapping clause has both a 'when' guard and an 'if' clause"
)

let rec to_ast_mapcl doc attrs ctx (P.MCL_aux (mcl, l)) =
match mcl with
| P.MCL_attribute (attr, arg, mcl) -> to_ast_mapcl doc (attrs @ [(l, attr, arg)]) ctx mcl
| P.MCL_doc (doc_comment, mcl) -> begin
| P.MCL_doc (doc_comment, mcl) -> (
match doc with
| Some _ -> raise (Reporting.err_general l "Function clause has multiple documentation comments")
| None -> to_ast_mapcl (Some doc_comment) attrs ctx mcl
end
)
| P.MCL_when (mcl, guard) ->
let mcl = to_ast_mapcl doc attrs ctx mcl in
let guard = to_ast_exp ctx guard in
apply_when_guard guard mcl
| P.MCL_bidir (mpexp1, mpexp2) ->
MCL_aux
(MCL_bidir (to_ast_mpexp ctx mpexp1, to_ast_mpexp ctx mpexp2), (mk_def_annot ?doc ~attrs l (), empty_uannot))
Expand Down
1 change: 1 addition & 0 deletions src/lib/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ let kw_table =
("union", (fun _ -> Union));
("newtype", (fun _ -> Newtype));
("with", (fun _ -> With));
("when", (fun _ -> When));
("val", (fun _ -> Val));
("outcome", (fun _ -> Outcome));
("instantiation", (fun _ -> Instantiation));
Expand Down
1 change: 1 addition & 0 deletions src/lib/parse_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -364,6 +364,7 @@ and mapcl_aux =
| MCL_forwards_deprecated of mpexp * exp
| MCL_forwards of pexp
| MCL_backwards of pexp
| MCL_when of mapcl * exp

type mapdef_aux =
(* mapping definition (bidirectional pattern-match function) *)
Expand Down
8 changes: 7 additions & 1 deletion src/lib/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ let set_syntax_deprecated l =
/*Terminals with no content*/

%token And As Assert Bitzero Bitone By Match Config Clause Dec Default Effect End Op
%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ INT NAT ORDER BOOL Cast
%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ INT NAT ORDER BOOL Cast When
%token Pure Impure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
%token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
%token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl Private
Expand Down Expand Up @@ -1175,6 +1175,12 @@ mapcl:
{ MCL_aux (MCL_attribute (fst attr, snd attr, mcl), loc $startpos(attr) $endpos(attr)) }
| doc = Doc; mcl = mapcl
{ MCL_aux (MCL_doc (doc, mcl), loc $startpos(doc) $endpos(doc)) }
| mcl = mapcl0
{ mcl }
| mcl = mapcl0; When; guard=exp
{ MCL_aux (MCL_when (mcl, guard), loc $startpos(mcl) $endpos(guard)) }

mapcl0:
| mpexp Bidir mpexp
{ mk_bidir_mapcl $1 $3 $startpos $endpos }
| mpexp EqGt exp
Expand Down
2 changes: 1 addition & 1 deletion src/sail_doc_backend/html_source.ml
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ let highlights ~filename ~contents =
| Foreach | Function_ | Mapping | Overload | Throw | Try | Catch | If_ | In | Inc | Var | Ref | Pure | Impure
| Monadic | Register | Return | Scattered | Sizeof | Constraint | Constant | Struct | Then | Typedef | Union
| Newtype | With | Val | Outcome | Instantiation | Impl | Private | Repeat | Until | While | Do | Mutual | Config
| Configuration | TerminationMeasure | Forwards | Backwards | Let_ | Bitfield ->
| Configuration | TerminationMeasure | Forwards | Backwards | Let_ | Bitfield | When ->
mark Highlight.Keyword;
go ()
| StructuredPragma _ | Pragma _ | Attribute _ | Fixity _ ->
Expand Down
6 changes: 6 additions & 0 deletions test/c/mapping_when.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
0x0
100
200
0x12c
150
199
35 changes: 35 additions & 0 deletions test/c/mapping_when.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
default Order dec

$include <prelude.sail>

mapping decimal : int <-> string = {
forwards n => dec_str(n),
backwards "x" => 150,
backwards _ => 1000
}

mapping hexadecimal : int <-> string = {
forwards n => hex_str(n),
backwards _ => 199
}

val foo : int <-> string

mapping clause foo =
n <-> decimal(n)
when
100 <= n & n <= 200

mapping clause foo =
n <-> hexadecimal(n)

val main : unit -> unit

function main() = {
print_endline(foo(0));
print_endline(foo(100));
print_endline(foo(200));
print_endline(foo(300));
print_int("", foo("x"));
print_int("", foo("y"))
}

0 comments on commit 571a4db

Please sign in to comment.