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 /printing/ppconstr.ml | |
| 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 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0ae3de7321..4dc3ba8789 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -399,12 +399,12 @@ let tag_var = tag Tag.variable pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c - let pr_guard_annot pr_aux bl (n,ro) = - match n with + let pr_guard_annot pr_aux bl ro = + match ro with | None -> mt () - | Some {loc; v = id} -> + | Some {loc; v = ro} -> match (ro : Constrexpr.recursion_order_expr) with - | CStructRec -> + | CStructRec { v = id } -> let names_of_binder = function | CLocalAssum (nal,_,_) -> nal | CLocalDef (_,_,_) -> [] @@ -413,10 +413,11 @@ let tag_var = tag Tag.variable if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" else mt() - | CWfRec c -> - spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" - | CMeasureRec (m,r) -> - spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ + | CWfRec (id,c) -> + spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}" + | CMeasureRec (id,m,r) -> + spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ + match id with None -> mt() | Some id -> spc () ++ pr_lident id ++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = |