diff options
| author | Maxime Dénès | 2018-12-07 13:38:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:45:32 +0200 |
| commit | 414cfd64702be920c9d96514e3802bc950b5ea0b (patch) | |
| tree | bdc7e8eca2b50da60d1a893124a9c93aea9d1841 /parsing/g_constr.mlg | |
| parent | 4b9119d8090e366ecd2e803ad30a9dd839bc8ec9 (diff) | |
Clean the representation of recursive annotation in Constrexpr
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
Diffstat (limited to 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 0586dda555..7786155092 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = - let _ = Option.map (fun { CAst.loc = aloc } -> + Option.iter (fun { CAst.loc = aloc } -> CErrors.user_err ?loc:aloc ~hdr:"Constr:mk_cofixb" - (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in + (Pp.str"Annotation forbidden in cofix expression.")) ann; let ty = match tyc with Some ty -> ty | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in @@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) } - | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) } + [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id } + | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) } | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) } + rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) } ] ] ; impl_name_head: @@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> { (assum na :: fst bl), snd bl } - | f = fixannot -> { [], f } + | f = fixannot -> { [], Some (CAst.make ~loc f) } | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } - | -> { [], (None, CStructRec) } + | -> { [], None } ] ] ; open_binders: |