diff options
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 29 |
1 files changed, 25 insertions, 4 deletions
diff --git a/src/parser.mly b/src/parser.mly index 39ca75ff..5e448a05 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -92,6 +92,7 @@ let mk_typ t n m = ATyp_aux (t, loc n m) let mk_pat p n m = P_aux (p, loc n m) let mk_pexp p n m = Pat_aux (p, loc n m) let mk_exp e n m = E_aux (e, loc n m) +let mk_measure meas n m = Measure_aux (meas, loc n m) let mk_lit l n m = L_aux (l, loc n m) let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m) @@ -748,6 +749,13 @@ exp_eof: | exp Eof { $1 } +/* Internal syntax for loop measures, rejected in normal code by initial_check */ +internal_loop_measure: + | + { mk_measure Measure_none $startpos $endpos } + | TerminationMeasure Lcurly exp Rcurly + { mk_measure (Measure_some $3) $startpos $endpos } + exp: | exp0 { $1 } @@ -802,10 +810,10 @@ exp: else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6)) in mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos } - | Repeat exp Until exp - { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos } - | While exp Do exp - { mk_exp (E_loop (While, $2, $4)) $startpos $endpos } + | Repeat internal_loop_measure exp Until exp + { mk_exp (E_loop (Until, $2, $5, $3)) $startpos $endpos } + | While internal_loop_measure exp Do exp + { mk_exp (E_loop (While, $2, $3, $5)) $startpos $endpos } /* Debugging only, will be rejected in initial_check if debugging isn't on */ | InternalPLet pat Eq exp In exp @@ -1401,6 +1409,17 @@ scattered_clause: | Function_ Clause funcl { mk_sd (SD_funcl $3) $startpos $endpos } +loop_measure: + | Until exp + { Loop (Until, $2) } + | While exp + { Loop (While, $2) } + +loop_measures: + | loop_measure + { [$1] } + | loop_measure Comma loop_measures + { $1::$3 } def: | fun_def @@ -1439,6 +1458,8 @@ def: { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) } | TerminationMeasure id pat Eq exp { DEF_measure ($2, $3, $5) } + | TerminationMeasure id loop_measures + { DEF_loop_measures ($2,$3) } defs_list: | def |