Skip to content

Commit 65211ab

Browse files
f52985f52985
authored
[spec/spectec] Fix prose title of if instruction (#2154)
1 parent 0832c84 commit 65211ab

9 files changed

Lines changed: 37 additions & 45 deletions

File tree

‎spectec/src/al/al_util.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -268,7 +268,7 @@ let unwrap_cate e =
268268
| _ -> fail_expr "unwrap_cate" e
269269

270270
let name_of_algo algo = match algo.it with
271-
| RuleA (name, _, _, _) -> Print.string_of_atom name
271+
| RuleA (mixop, _, _, _) -> Print.string_of_mixop mixop
272272
| FuncA (name, _, _) -> name
273273

274274
let params_of_algo algo = match algo.it with

‎spectec/src/al/ast.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -146,9 +146,9 @@ and instr' =
146146
(* Algorithms *)
147147

148148
type algorithm = algorithm' phrase
149-
and algorithm' = (* `algorithm` f`(`expr*`)` `{`instr*`}` *)
150-
| RuleA of atom * anchor * arg list * instr list (* reduction rule *)
151-
| FuncA of id * arg list * instr list (* helper function *)
149+
and algorithm' = (* `algorithm` f`(`expr*`)` `{`instr*`}` *)
150+
| RuleA of mixop * anchor * arg list * instr list (* reduction rule *)
151+
| FuncA of id * arg list * instr list (* helper function *)
152152

153153

154154
(* Scripts *)

‎spectec/src/al/eq.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -142,8 +142,8 @@ and eq_instrs il1 il2 = eq_list eq_instr il1 il2
142142

143143
let eq_algos al1 al2 =
144144
match al1.it, al2.it with
145-
| RuleA (a1, an1, al1, il1), RuleA (a2, an2, al2, il2) ->
146-
Atom.eq a1 a2 && an1 = an2 && eq_args al1 al2 && eq_instrs il1 il2
145+
| RuleA (m1, an1, al1, il1), RuleA (m2, an2, al2, il2) ->
146+
Mixop.eq m1 m2 && an1 = an2 && eq_args al1 al2 && eq_instrs il1 il2
147147
| FuncA (i1, al1, il1), FuncA (i2, al2, il2) ->
148148
i1 = i2 && eq_args al1 al2 && eq_instrs il1 il2
149149
| _ -> false

‎spectec/src/backend-interpreter/ds.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,8 @@ let to_map algos =
2525
let f acc algo =
2626
let rmap, fmap = acc in
2727
match algo.it with
28-
| RuleA (atom, _, _, _) ->
29-
let name = Print.string_of_atom atom in
28+
| RuleA (mixop, _, _, _) ->
29+
let name = mixop |> Xl.Mixop.head |> Option.get |> Print.string_of_atom in
3030
Map.add name algo rmap, fmap
3131
| FuncA (name, _, _) -> rmap, Map.add name algo fmap
3232
in

‎spectec/src/backend-prose/render.ml‎

Lines changed: 16 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1483,20 +1483,22 @@ and render_instrs env algoname depth instrs =
14831483

14841484
(* Prose *)
14851485

1486-
let render_atom_title env name params =
1487-
(* TODO a workaround, for algorithms named label or name
1488-
that are defined as LABEL_ or FRAME_ in the dsl *)
1489-
let name' =
1490-
match name.it with
1491-
| Atom.Atom "label" -> Atom.Atom "LABEL_"
1492-
| Atom.Atom "frame" -> Atom.Atom "FRAME_"
1493-
| Atom.Atom s -> Atom.Atom (String.uppercase_ascii s)
1494-
| _ -> name.it
1486+
let render_mixop_title env mixop params =
1487+
let head = Mixop.head mixop in
1488+
(* HARDCODE: Tweak for these instructinos *)
1489+
let mixop =
1490+
match head with
1491+
| Some atom ->
1492+
(match atom.it with
1493+
| Atom ("LABEL_" | "FRAME_" | "HANDLER_") -> Mixop.Atom atom
1494+
| _ -> mixop
1495+
)
1496+
| _ -> mixop
14951497
in
1496-
let name = name' $$ no_region % name.note in
1497-
let op = Mixop.(Seq (Atom name :: List.init (List.length params) (fun _ -> Arg ()))) in
14981498
let params = List.filter_map (fun a -> match a.it with Al.Ast.ExpA e -> Some e | _ -> None) params in
1499-
let expr = Al.Al_util.caseE (op, params) ~at:no_region ~note:Al.Al_util.no_note in
1499+
if List.length params + 1 <> List.length (Mixop.flatten mixop) then
1500+
error (match head with | Some atom -> atom.at | None -> no_region) "Failed to render prose header";
1501+
let expr = Al.Al_util.caseE (mixop, params) ~at:no_region ~note:Al.Al_util.no_note in
15001502
match al_to_el_expr expr with
15011503
| Some ({ it = El.Ast.ParenE exp; _ }) -> render_el_exp env exp
15021504
| Some exp -> render_el_exp env exp
@@ -1505,12 +1507,6 @@ let render_atom_title env name params =
15051507
let render_funcname_title env fname params =
15061508
render_expr env (Al.Al_util.callE (fname, params) ~at:no_region ~note:Al.Al_util.no_note)
15071509

1508-
let _render_pred env name params instrs =
1509-
let title = render_atom_title env name params in
1510-
title ^ "\n" ^
1511-
String.make (String.length title) '.' ^ "\n" ^
1512-
render_stmts env 0 instrs
1513-
15141510
let render_rule env concl prems =
15151511
init_typs ();
15161512
match prems with
@@ -1523,8 +1519,8 @@ let render_rule env concl prems =
15231519
sprintf "%s if:\n%s" sconcl sprems
15241520

15251521
let render_rule_algo env name params instrs =
1526-
let title = render_atom_title env name params in
1527-
let rname = Al.Print.string_of_atom name in
1522+
let title = render_mixop_title env name params in
1523+
let rname = Al.Print.string_of_mixop name in
15281524
title ^ "\n" ^
15291525
String.make (String.length title) '.' ^ "\n" ^
15301526
render_instrs env rname 0 instrs

‎spectec/src/exe-spectec/main.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -223,8 +223,8 @@ let () =
223223
let match_algo_name algo_name al_elt =
224224
algo_name = "" ||
225225
(match al_elt.Util.Source.it with
226-
| Al.Ast.RuleA (a, _, _, _) ->
227-
Al.Print.string_of_atom a = String.uppercase_ascii algo_name
226+
| Al.Ast.RuleA (m, _, _, _) ->
227+
Al.Print.string_of_mixop m = String.uppercase_ascii algo_name
228228
| Al.Ast.FuncA (id , _, _) ->
229229
id = String.lowercase_ascii algo_name)
230230
in

‎spectec/src/il2al/manual.ml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ let listT ty = Il.Ast.IterT (ty, Il.Ast.List) $ no_region
1212
let expA e = ExpA e $ e.at
1313

1414
let eval_expr =
15-
let open Xl.Atom in
1615
let ty_instrs = listT instrT in
1716
let ty_vals = listT valT in
1817
let instrs = iter_var "instr" List instrT in
@@ -24,7 +23,10 @@ let eval_expr =
2423
Il.Env.bind_def !Al.Valid.il_env ("Eval_expr" $ no_region) ([param], ty_vals, []);
2524

2625
RuleA (
27-
Atom "Eval_expr" $$ no_region % {def=""; case=""},
26+
Xl.Mixop.(Seq [
27+
Atom Xl.Atom.(Atom "Eval_expr" $$ no_region % {def=""; case=""});
28+
Arg ()
29+
]),
2830
"Eval_expr",
2931
[expA instrs],
3032
[

‎spectec/src/il2al/translate.ml‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1216,13 +1216,7 @@ and translate_rgroup (rule: rule_def) =
12161216
let winstr = extract_winstr (List.hd rgroup) rule.at in
12171217
let instrs = translate_rgroup' rule in
12181218

1219-
let name =
1220-
try
1221-
match Mixop.head (case_of_case winstr) with
1222-
| Some atom -> atom
1223-
| _ -> failwith ""
1224-
with _ -> error rule.at "The reduction rules do not have valid or consistent target Wasm instructions."
1225-
in
1219+
let name = case_of_case winstr in
12261220
let anchor = rel_id.it ^ "/" ^ instr_name in
12271221
let al_params =
12281222
if List.mem instr_name ["frame"; "label"; "handler"] then [] else

‎spectec/test-prose/TEST.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1019,8 +1019,8 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as
10191019
a. Push the value :math:`{\mathit{val}}_2` to the stack.
10201020

10211021

1022-
:math:`\mathsf{if}~{t^?}~{{\mathit{instr}}_1^\ast}~{{\mathit{instr}}_2^\ast}`
1023-
.............................................................................
1022+
:math:`\mathsf{if}~{t^?}~{{\mathit{instr}}_1^\ast}~\mathsf{else}~{{\mathit{instr}}_2^\ast}`
1023+
...........................................................................................
10241024

10251025

10261026
1. Assert: Due to validation, a value of number type :math:`\mathsf{i{\scriptstyle 32}}` is on the top of the stack.
@@ -6240,8 +6240,8 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as
62406240
a. Push the value :math:`{\mathit{val}}_2` to the stack.
62416241

62426242

6243-
:math:`\mathsf{if}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}~{{\mathit{instr}}_2^\ast}`
6244-
.....................................................................................
6243+
:math:`\mathsf{if}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}~\mathsf{else}~{{\mathit{instr}}_2^\ast}`
6244+
...................................................................................................
62456245

62466246

62476247
1. Assert: Due to validation, a value of number type :math:`\mathsf{i{\scriptstyle 32}}` is on the top of the stack.
@@ -19005,8 +19005,8 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
1900519005
a. Push the value :math:`{\mathit{val}}_2` to the stack.
1900619006

1900719007

19008-
:math:`\mathsf{if}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}~{{\mathit{instr}}_2^\ast}`
19009-
.....................................................................................
19008+
:math:`\mathsf{if}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}~\mathsf{else}~{{\mathit{instr}}_2^\ast}`
19009+
...................................................................................................
1901019010

1901119011

1901219012
1. Assert: Due to validation, a value of number type :math:`\mathsf{i{\scriptstyle 32}}` is on the top of the stack.

0 commit comments

Comments
 (0)