diff options
| author | Brian Campbell | 2018-12-11 11:54:36 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-12-11 12:05:34 +0000 |
| commit | 4f20163965e7c336f28740628fa9d64528006861 (patch) | |
| tree | 56601922410d37677f9f95cc2c93fec4ee56a7f7 /src/parser.mly | |
| parent | 25ab845211e3df24386a0573b517a01dab879b03 (diff) | |
Initial attempt at using termination measures in Coq
This only applies to recursive functions and uses the termination measure
merely as a limit to the recursive call depth, rather than proving the
measure correct.
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/parser.mly b/src/parser.mly index bb5aa5f1..9385c148 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -125,6 +125,8 @@ let doc_vs doc (VS_aux (v, l)) = VS_aux (v, Documented (doc, l)) let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l) +let mk_recr r n m = (Rec_aux(r, loc n m)) + let mk_recn = (Rec_aux((Rec_nonrec), Unknown)) let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown)) let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) @@ -1216,9 +1218,15 @@ type_unions: | type_union Comma type_unions { $1 :: $3 } +rec_measure: + | Lcurly pat EqGt exp Rcurly + { mk_recr (Rec_measure ($2, $4)) $startpos $endpos } + fun_def: | Function_ funcls { let funcls, tannot = $2 in mk_fun (FD_function (mk_recn, tannot, mk_eannotn, funcls)) $startpos $endpos } + | Function_ rec_measure funcls + { let funcls, tannot = $3 in mk_fun (FD_function ($2, tannot, mk_eannotn, funcls)) $startpos $endpos } fun_def_list: | fun_def |