diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 64 |
1 files changed, 37 insertions, 27 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 755e905a70..fb9d45a793 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -7,12 +7,11 @@ (************************************************************************) open Util -open Term +open Constr open Pp open Names open Environ open Declarations -open Nameops open Globnames open Libnames open Goptions @@ -80,7 +79,7 @@ let print_params env sigma params = let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) + (fun (id,c) -> Id.print id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -107,7 +106,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else mt () in hov 0 ( - pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + Id.print mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes @@ -122,17 +121,24 @@ let instantiate_cumulativity_info cumi = in CumulativityInfo.make (expose univs, expose subtyp) -let print_mutual_inductive env mind mib = +let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> "Inductive" | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in + let univs = + let open Univ in + if Declareops.inductive_is_polymorphic mib then + Array.to_list (Instance.to_array + (AUContext.instance (Declareops.inductive_polymorphic_context mib))) + else [] + in + let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -149,7 +155,7 @@ let print_mutual_inductive env mind mib = let get_fields = let rec prodec_rec l subst c = - match kind_of_term c with + match kind c with | Prod (na,t,c) -> let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c @@ -160,7 +166,7 @@ let get_fields = in prodec_rec [] [] -let print_record env mind mib = +let print_record env mind mib udecl = let u = if Declareops.inductive_is_polymorphic mib then Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) @@ -174,10 +180,11 @@ let print_record env mind mib = let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in + let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) + (Array.to_list (Univ.Instance.to_array u)) udecl in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | BiFinite -> "Record" | Finite -> "Inductive" @@ -189,15 +196,15 @@ let print_record env mind mib = Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) (Declareops.inductive_is_cumulative mib) ++ - def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ + def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ - str ":= " ++ pr_id mip.mind_consnames.(0)) ++ + str ":= " ++ Id.print mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> - pr_id id ++ str (if b then " : " else " := ") ++ + Id.print id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" @@ -206,18 +213,18 @@ let print_record env mind mib = sigma (instantiate_cumulativity_info cumi) ) -let pr_mutual_inductive_body env mind mib = +let pr_mutual_inductive_body env mind mib udecl = if mib.mind_record <> None && not !Flags.raw_print then - print_record env mind mib + print_record env mind mib udecl else - print_mutual_inductive env mind mib + print_mutual_inductive env mind mib udecl (** Modpaths *) let rec print_local_modpath locals = function - | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals) + | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals) | MPdot(mp,l) -> - print_local_modpath locals mp ++ str "." ++ pr_lab l + print_local_modpath locals mp ++ str "." ++ Label.print l | MPfile _ -> raise Not_found let print_modpath locals mp = @@ -238,10 +245,10 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn -let nametab_register_dir mp = +let nametab_register_dir obj_mp = let id = mk_fake_top () in - let dir = DirPath.make [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))) + let obj_dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -301,7 +308,7 @@ let nametab_register_modparam mbid mtb = id let print_body is_impl env mp (l,body) = - let name = pr_label l in + let name = Label.print l in hov 2 (match body with | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name @@ -336,10 +343,10 @@ let print_body is_impl env mp (l,body) = | SFBmind mib -> try let env = Option.get env in - pr_mutual_inductive_body env (MutInd.make2 mp l) mib + pr_mutual_inductive_body env (MutInd.make2 mp l) mib None with e when CErrors.noncritical e -> let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> def "Inductive" | BiFinite -> def "Variant" @@ -375,9 +382,12 @@ let rec print_typ_expr env mp locals mty = | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in + (* XXX: What should env and sigma be here? *) + let env = Global.env () in + let sigma = Evd.empty in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() - ++ Printer.pr_lconstr c) + ++ Printer.pr_lconstr_env env sigma c) | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ @@ -403,7 +413,7 @@ let rec print_functor fty fatom is_type env mp locals = function let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ - str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++ + str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ spc() ++ print_functor fty fatom is_type env' mp locals' me2) let rec print_expression x = |