diff options
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 55 |
1 files changed, 40 insertions, 15 deletions
diff --git a/src/parser.mly b/src/parser.mly index 39ca75ff..f764995a 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 @@ -1056,6 +1064,8 @@ atomic_exp: { mk_exp (E_record $3) $startpos $endpos } | Lcurly exp With fexp_exp_list Rcurly { mk_exp (E_record_update ($2, $4)) $startpos $endpos } + | Lsquare Rsquare + { mk_exp (E_vector []) $startpos $endpos } | Lsquare exp_list Rsquare { mk_exp (E_vector $2) $startpos $endpos } | Lsquare exp With atomic_exp Eq exp Rsquare @@ -1341,31 +1351,31 @@ let_def: externs: | id Colon String - { ([(string_of_id $1, $3)], None) } + { [(string_of_id $1, $3)] } | Under Colon String - { ([], Some $3) } + { [("_", $3)] } | id Colon String Comma externs - { cons_fst (string_of_id $1, $3) $5 } + { (string_of_id $1, $3) :: $5 } val_spec_def: | Doc val_spec_def { doc_vs $1 $2 } | Val id Colon typschm - { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($4, $2, [], false)) $startpos $endpos } | Val Cast id Colon typschm - { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($5, $3, [], true)) $startpos $endpos } | Val id Eq String Colon typschm - { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($6, $2, [("_", $4)], false)) $startpos $endpos } | Val Cast id Eq String Colon typschm - { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($7, $3, [("_", $5)], true)) $startpos $endpos } | Val String Colon typschm - { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), [("_", $2)], false)) $startpos $endpos } | Val Cast String Colon typschm - { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), [("_", $3)], true)) $startpos $endpos } | Val id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos } + { mk_vs (VS_val_spec ($8, $2, $5, false)) $startpos $endpos } | Val Cast id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos } + { mk_vs (VS_val_spec ($9, $3, $6, true)) $startpos $endpos } register_def: | Register id Colon typ @@ -1401,6 +1411,19 @@ scattered_clause: | Function_ Clause funcl { mk_sd (SD_funcl $3) $startpos $endpos } +loop_measure: + | Until exp + { Loop (Until, $2) } + | Repeat 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 +1462,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 |