Skip to content

Commit 26fdfd0

Browse files
myreenmyreen
authored
Merge pull request #1188 from halogentlepersuasion/pan_prog_conv
2 parents 95250d9 + 5d137c6 commit 26fdfd0

File tree

3 files changed

+50
-65
lines changed

3 files changed

+50
-65
lines changed

‎pancake/parser/panConcreteExamplesScript.sml‎

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -420,6 +420,21 @@ val error_line_ex2 =
420420

421421
val error_line_ex2_parse = check_failure $ parse_pancake error_line_ex2
422422

423+
val error_line_ex3 =
424+
‘
425+
fun foo() {
426+
skip;
427+
while (1) {
428+
skip;
429+
skip;
430+
skeep;
431+
skip;
432+
}
433+
}
434+
’
435+
436+
val error_line_ex3_parse = check_failure $ parse_pancake error_line_ex3
437+
423438
(** Function pointers
424439
425440
& can only be used to get the address of functions.
@@ -478,7 +493,17 @@ val empty_blocks =
478493
fun j() { if(1) { x = 5; } else { } }
479494
’
480495

481-
val empty_body_parse = check_success $ parse_pancake empty_blocks;
496+
val empty_blocks_parse = check_success $ parse_pancake empty_blocks;
497+
498+
(* Dec blocks with no subsequent prog *)
499+
val empty_dec_prog =
500+
‘
501+
fun f() { var x = 0; }
502+
503+
fun g() { var 1 x = f(); }
504+
’
505+
506+
val empty_dec_prog_parse = check_success $ parse_pancake empty_dec_prog;
482507

483508
(* Using the annotation comment syntax. *)
484509
val annot_fun =

‎pancake/parser/panPEGScript.sml‎

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,15 @@ Definition try_default_def:
125125
try_default s t = choicel [s; empty $ mkleaf (t, unknown_loc)]
126126
End
127127

128+
(* add single Skip in place of empty Prog - will generate unnecessary Skips if used without caution *)
129+
Definition try_ProgNT_def:
130+
try_ProgNT =
131+
choicel [
132+
seql [consume_tok RCurT; empty $ mkleaf (KeywordT SkipK, unknown_loc)] (mksubtree ProgNT);
133+
mknt ProgNT
134+
]
135+
End
136+
128137
Definition pancake_peg_def[nocompute]:
129138
pancake_peg = <|
130139
start := mknt FunListNT;
@@ -146,7 +155,7 @@ Definition pancake_peg_def[nocompute]:
146155
];
147156
consume_tok RParT;
148157
consume_tok LCurT;
149-
mknt ProgNT]
158+
try_ProgNT]
150159
(mksubtree FunNT));
151160
(INL ParamListNT, seql [mknt ShapeNT; keep_ident;
152161
rpt (seql [consume_tok CommaT;
@@ -155,8 +164,8 @@ Definition pancake_peg_def[nocompute]:
155164
FLAT]
156165
(mksubtree ParamListNT));
157166
(INL ProgNT, choicel [seql [mknt BlockNT; mknt ProgNT] (mksubtree ProgNT);
158-
seql [mknt DecCallNT; mknt ProgNT] (mksubtree DecCallNT);
159-
seql [mknt DecNT; mknt ProgNT] (mksubtree DecNT);
167+
seql [mknt DecCallNT; try_ProgNT] (mksubtree DecCallNT);
168+
seql [mknt DecNT; try_ProgNT] (mksubtree DecNT);
160169
seql [keep_annot; mknt ProgNT] (mksubtree ProgNT);
161170
seql [mknt StmtNT; consume_tok SemiT; mknt ProgNT] (mksubtree ProgNT);
162171
consume_tok RCurT
@@ -178,7 +187,7 @@ Definition pancake_peg_def[nocompute]:
178187
mknt ExtCallNT;
179188
mknt RaiseNT; mknt RetCallNT; mknt ReturnNT;
180189
keep_kw TicK;
181-
seql [consume_tok LCurT; mknt ProgNT] I
190+
seql [consume_tok LCurT; try_ProgNT] I
182191
]);
183192
(INL DecCallNT, seql [consume_kw VarK; mknt ShapeNT; keep_ident; consume_tok AssignT;
184193
choicel [seql [consume_tok StarT; mknt ExpNT] I;
@@ -202,12 +211,12 @@ Definition pancake_peg_def[nocompute]:
202211
consume_tok CommaT; mknt ExpNT]
203212
(mksubtree Store32NT));
204213
(INL IfNT, seql [consume_kw IfK; mknt ExpNT; consume_tok LCurT;
205-
mknt ProgNT;
206-
try (seql [keep_kw ElseK; consume_tok LCurT;
207-
mknt ProgNT] I)]
214+
try_ProgNT;
215+
try_default (seql [consume_kw ElseK; consume_tok LCurT;
216+
try_ProgNT] I) (KeywordT SkipK)]
208217
(mksubtree IfNT));
209218
(INL WhileNT, seql [consume_kw WhileK; mknt ExpNT;
210-
consume_tok LCurT; mknt ProgNT] (mksubtree WhileNT));
219+
consume_tok LCurT; try_ProgNT] (mksubtree WhileNT));
211220
(INL CallNT, seql [try (choicel [keep_kw RetK; mknt RetNT]);
212221
choicel [seql [consume_tok StarT; mknt ExpNT] I;
213222
mknt FLabelNT];
@@ -219,7 +228,7 @@ Definition pancake_peg_def[nocompute]:
219228
(mksubtree RetNT));
220229
(INL HandleNT, seql [consume_kw WithK; keep_ident;
221230
consume_kw InK; keep_ident;
222-
consume_tok DArrowT; consume_tok LCurT; mknt ProgNT;
231+
consume_tok DArrowT; consume_tok LCurT; try_ProgNT;
223232
consume_kw HandleK]
224233
(mksubtree HandleNT));
225234
(INL ExtCallNT, seql [keep_ffi_ident;
@@ -715,7 +724,7 @@ Proof
715724
choicel_def, seql_def, pegf_def, keep_tok_def, consume_tok_def,
716725
keep_kw_def, consume_kw_def, keep_int_def, keep_nat_def,
717726
keep_ident_def, keep_annot_def, keep_ffi_ident_def, try_def,
718-
try_default_def] >>
727+
try_default_def, try_ProgNT_def] >>
719728
simp(pancake_wfpeg_thm :: wfpeg_rwts @ peg0_rwts @ npeg0_rwts)
720729
QED
721730

‎pancake/parser/panPtreeConversionScript.sml‎

Lines changed: 5 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -572,54 +572,18 @@ Definition conv_Prog_def:
572572
| _ => NONE
573573
else if isNT nodeNT IfNT then
574574
case args of
575-
[e] =>
576-
do e' <- conv_Exp e;
577-
SOME (add_locs_annot nd (If e' Skip Skip))
578-
od
579-
| [e; p] =>
580-
(if tokcheck p (kw ElseK) then
581-
do e' <- conv_Exp e;
582-
SOME (add_locs_annot nd (If e' Skip Skip))
583-
od
584-
else
585-
do e' <- conv_Exp e;
586-
p' <- conv_Prog p;
587-
SOME (add_locs_annot nd (If e' p' Skip))
588-
od
589-
)
590-
| [e; p1; p2] =>
591-
(if tokcheck p1 (kw ElseK) then
592-
do e' <- conv_Exp e;
593-
p2' <- conv_Prog p2;
594-
SOME (add_locs_annot nd (If e' Skip p2'))
595-
od
596-
else if tokcheck p2 (kw ElseK) then
597-
do e' <- conv_Exp e;
598-
p1' <- conv_Prog p1;
599-
SOME (add_locs_annot nd (If e' p1' Skip))
600-
od
601-
else
602-
do e' <- conv_Exp e;
603-
p1' <- conv_Prog p1;
604-
p2' <- conv_Prog p2;
605-
SOME (add_locs_annot nd (If e' p1' p2'))
606-
od)
607-
| [e; p1; _; p2] =>
608-
do e' <- conv_Exp e;
609-
p1' <- conv_Prog p1;
610-
p2' <- conv_Prog p2;
611-
SOME (add_locs_annot nd (If e' p1' p2'))
612-
od
575+
| [e; p1; p2] => do e' <- conv_Exp e;
576+
p1' <- conv_Prog p1;
577+
p2' <- conv_Prog p2;
578+
SOME (add_locs_annot nd (If e' p1' p2'))
579+
od
613580
| _ => NONE
614581
else if isNT nodeNT WhileNT then
615582
case args of
616583
[e; p] => do e' <- conv_Exp e;
617584
p' <- conv_Prog p;
618585
SOME (add_locs_annot nd (While e' p'))
619586
od
620-
| [e] => do e' <- conv_Exp e;
621-
SOME (add_locs_annot nd (While e' Skip))
622-
od
623587
| _ => NONE
624588
else if isNT nodeNT DecCallNT then
625589
case args of
@@ -628,10 +592,6 @@ Definition conv_Prog_def:
628592
p' <- conv_Prog p;
629593
SOME $ add_locs_annot nd $ DecCall i' s' e' args' p'
630594
od
631-
| [dec] =>
632-
do (s',i',e',args') <- conv_DecCall dec;
633-
SOME $ add_locs_annot nd $ DecCall i' s' e' args' Skip
634-
od
635595
| _ => NONE
636596
else if isNT nodeNT CallNT then
637597
case args of
@@ -714,15 +674,6 @@ End
714674
Definition conv_Fun_def:
715675
conv_Fun tree =
716676
case argsNT tree FunNT of
717-
SOME [e;n;ps] =>
718-
(case (argsNT ps ParamListNT) of
719-
SOME args =>
720-
(do ps' <- conv_params args;
721-
n' <- conv_ident n;
722-
e' <- conv_expos e;
723-
SOME (n', e', ps', Skip)
724-
od)
725-
| _ => NONE)
726677
| SOME [e;n;ps;c] =>
727678
(case (argsNT ps ParamListNT) of
728679
SOME args =>

0 commit comments

Comments
 (0)