diff options
| author | Hugo Herbelin | 2018-11-13 15:42:02 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-01 14:54:54 +0200 |
| commit | 45352e43db4c67eab23517f13e94ba1b5cc11808 (patch) | |
| tree | 7812917af30d62fa8edcb4e85a89c1ed4a3ec65e /printing | |
| parent | 7032085c809993d6a173e51aec447c02828ae070 (diff) | |
Towards unifying parsing/printing for universe instances and Type's argument.
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8d5213b988..5e64cfb04c 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -157,10 +157,8 @@ let tag_var = tag Tag.variable let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) - let pr_univ_expr = function - | Some (x,n) -> - pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) - | None -> str"_" + let pr_univ_expr (qid,n) = + pr_qualid qid ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) let pr_univ l = match l with @@ -173,8 +171,9 @@ let tag_var = tag Tag.variable | GSProp -> tag_type (str "SProp") | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") - | GType [] -> tag_type (str "Type") - | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) + | GType UUnknown -> tag_type (str "Type") + | GType UAnonymous -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") () + | GType (UNamed u) -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) let pr_glob_level = let open Glob_term in function | GSProp -> tag_type (str "SProp") |