diff options
| author | Amin Timany | 2017-04-01 17:35:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:45:19 +0200 |
| commit | fd1f420aef96822bed2ce14214c34e41ceda9b4e (patch) | |
| tree | 50a0e42a1a5a9ab9edc05f6c4a14a2f55df0cbf7 /printing | |
| parent | 4dd4f186895d16510f217778bb83933be8956082 (diff) | |
Using UInfoInd for universes in inductive types
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 7 | ||||
| -rw-r--r-- | printing/printer.mli | 1 | ||||
| -rw-r--r-- | printing/printmod.ml | 10 |
3 files changed, 13 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..c27a9b009d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,6 +261,13 @@ let pr_universe_ctx sigma c = else mt() +let pr_universe_info_ind sigma uii = + if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii + else + mt() + (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 3fce065613..6531036a1f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -97,6 +97,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds val pr_polymorphic : bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index c4affd4acd..7dc47a4a4c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -89,7 +89,7 @@ let build_ind_type env mip = let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -100,7 +100,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if mib.mind_polymorphic then - Printer.pr_universe_instance sigma mib.mind_universes + Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes) else mt () in hov 0 ( @@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib = def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -142,7 +142,7 @@ let get_fields = let print_record env mind mib = let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -175,7 +175,7 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then |