diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 20:02:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 23:39:01 +0200 |
| commit | 7002b3daca6da29eadf80019847630b8583c3daf (patch) | |
| tree | 9dcc3b618d33dd416805f70e878d71d007ddf4ff /printing | |
| parent | 5de89439d459edd402328a1e437be4d8cd2e4f46 (diff) | |
Move to a representation of universe polymorphic constants using indices for variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 5 | ||||
| -rw-r--r-- | printing/printer.ml | 16 |
2 files changed, 12 insertions, 9 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 42d779f04..6e45cb6b0 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -458,8 +458,9 @@ let ungeneralized_type_of_constant_type t = let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Declareops.body_of_constant cb in - let typ = ungeneralized_type_of_constant_type cb.const_type in - let univs = Declareops.universes_of_constant cb in + let typ = Declareops.type_of_constant cb in + let typ = ungeneralized_type_of_constant_type typ in + let univs = Univ.instantiate_univ_context (Declareops.universes_of_constant cb) in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> diff --git a/printing/printer.ml b/printing/printer.ml index 03f416a51..55a7d36a3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -756,12 +756,12 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env mib ((_,i) as ind) = - let mip = mib.mind_packets.(i) in - let params = mib.mind_params_ctxt in - let args = extended_rel_list 0 params in let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in + let mip = mib.mind_packets.(i) in + let params = Inductive.inductive_paramdecls (mib,u) in + let args = extended_rel_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -794,12 +794,14 @@ let get_fields = prodec_rec [] [] let print_record env mind mib = + let u = + if mib.mind_polymorphic then + Univ.UContext.instance mib.mind_universes + else Univ.Instance.empty + in let mip = mib.mind_packets.(0) in - let params = mib.mind_params_ctxt in + let params = Inductive.inductive_paramdecls (mib,u) in let args = extended_rel_list 0 params in - let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in |