aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-20 00:09:10 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-20 00:09:10 +0100
commit3d5936f280bc01bd6baa8b4396e641ac156bfd5b (patch)
treebaa9bc67abdff13d159f4e4b05921bd2a89e7e49 /printing
parentd846451c9a07b4e051173878a5446edea029bf5b (diff)
Moving mutual inductive printing from Printer to Printmod.
Diffstat (limited to 'printing')
-rw-r--r--printing/printer.ml106
-rw-r--r--printing/printer.mli4
-rw-r--r--printing/printmod.ml114
-rw-r--r--printing/printmodsig.mli6
4 files changed, 117 insertions, 113 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index e21c9a61b..8a906b3f1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -768,109 +768,3 @@ let pr_polymorphic b =
if b then str"Polymorphic " else str"Monomorphic "
else mt ()
-(** Inductive declarations *)
-
-open Termops
-open Reduction
-
-let print_params env sigma params =
- if List.is_empty params then mt ()
- else pr_rel_context env sigma params ++ brk(1,2)
-
-let print_constructors envpar names types =
- let pc =
- prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
- (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar Evd.empty c)
- (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
- in
- hv 0 (str " " ++ pc)
-
-let build_ind_type env mip =
- Inductive.type_of_inductive env mip
-
-let print_one_inductive env mib ((_,i) as ind) =
- 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
- let envpar = push_rel_context params env in
- hov 0 (
- pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
- str ": " ++ pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
- brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
-
-let print_mutual_inductive env mind mib =
- let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
- in
- let keyword =
- let open Decl_kinds in
- match mib.mind_finite with
- | Finite -> "Inductive "
- | BiFinite -> "Variant "
- | CoFinite -> "CoInductive "
- in
- hov 0 (pr_polymorphic mib.mind_polymorphic ++
- str keyword ++
- prlist_with_sep (fun () -> fnl () ++ str" with ")
- (print_one_inductive env mib) inds ++
- pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
-
-let get_fields =
- let rec prodec_rec l subst c =
- match kind_of_term c with
- | Prod (na,t,c) ->
- let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
- prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
- | LetIn (na,b,_,c) ->
- let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
- prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
- | _ -> List.rev l
- in
- 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 = 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 ((mind,0),u) (mib,mip) in
- 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 keyword =
- let open Decl_kinds in
- match mib.mind_finite with
- | BiFinite -> "Record "
- | Finite -> "Inductive "
- | CoFinite -> "CoInductive "
- in
- hov 0 (
- hov 0 (
- pr_polymorphic mib.mind_polymorphic ++
- str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++
- print_params env Evd.empty params ++
- str ": " ++ pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++
- str ":= " ++ pr_id 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 " := ") ++
- pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
- pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
-
-let pr_mutual_inductive_body env mind mib =
- if mib.mind_record <> None && not !Flags.raw_print then
- print_record env mind mib
- else
- print_mutual_inductive env mind mib
diff --git a/printing/printer.mli b/printing/printer.mli
index ac35a324a..ad6cedf7d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -175,7 +175,3 @@ val set_printer_pr : printer_pr -> unit
val default_printer_pr : printer_pr
-(** Inductive declarations *)
-
-val pr_mutual_inductive_body :
- env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
diff --git a/printing/printmod.ml b/printing/printmod.ml
index b6ee2eaa0..e19b3a92d 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -6,8 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
+open Term
open Pp
open Names
+open Environ
open Declarations
open Nameops
open Globnames
@@ -60,6 +63,115 @@ let get_new_id locals id =
in
get_id (List.map snd locals) id
+(** Inductive declarations *)
+
+open Termops
+open Reduction
+
+let print_params env sigma params =
+ if List.is_empty params then mt ()
+ else Printer.pr_rel_context env sigma params ++ brk(1,2)
+
+let print_constructors envpar names types =
+ let pc =
+ prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+ (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c)
+ (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
+ in
+ hv 0 (str " " ++ pc)
+
+let build_ind_type env mip =
+ Inductive.type_of_inductive env mip
+
+let print_one_inductive env mib ((_,i) as ind) =
+ 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
+ let envpar = push_rel_context params env in
+ hov 0 (
+ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
+ str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
+ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mind mib =
+ let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
+ in
+ let keyword =
+ let open Decl_kinds in
+ match mib.mind_finite with
+ | Finite -> "Inductive "
+ | BiFinite -> "Variant "
+ | CoFinite -> "CoInductive "
+ in
+ hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
+ str keyword ++
+ prlist_with_sep (fun () -> fnl () ++ str" with ")
+ (print_one_inductive env mib) inds ++
+ Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+
+let get_fields =
+ let rec prodec_rec l subst c =
+ match kind_of_term 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
+ | LetIn (na,b,_,c) ->
+ let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
+ prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c
+ | _ -> List.rev l
+ in
+ 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 = 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 ((mind,0),u) (mib,mip) in
+ 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 keyword =
+ let open Decl_kinds in
+ match mib.mind_finite with
+ | BiFinite -> "Record "
+ | Finite -> "Inductive "
+ | CoFinite -> "CoInductive "
+ in
+ hov 0 (
+ hov 0 (
+ Printer.pr_polymorphic mib.mind_polymorphic ++
+ str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++
+ print_params env Evd.empty params ++
+ str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++
+ str ":= " ++ pr_id 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 " := ") ++
+ Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
+ Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+
+let pr_mutual_inductive_body env mind mib =
+ if mib.mind_record <> None && not !Flags.raw_print then
+ print_record env mind mib
+ else
+ print_mutual_inductive env mind mib
+
+(** Modpaths *)
+
let rec print_local_modpath locals = function
| MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals)
| MPdot(mp,l) ->
@@ -167,7 +279,7 @@ let print_body is_impl env mp (l,body) =
| SFBmind mib ->
try
let env = Option.get env in
- Printer.pr_mutual_inductive_body env (MutInd.make2 mp l) mib
+ pr_mutual_inductive_body env (MutInd.make2 mp l) mib
with e when Errors.noncritical e ->
let keyword =
let open Decl_kinds in
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
index 2ccf4b7d5..2c1974bfc 100644
--- a/printing/printmodsig.mli
+++ b/printing/printmodsig.mli
@@ -6,10 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Pp
open Names
module type Pp =
sig
- val print_module : bool -> module_path -> Pp.std_ppcmds
- val print_modtype : module_path -> Pp.std_ppcmds
+ val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
+ val print_module : bool -> module_path -> std_ppcmds
+ val print_modtype : module_path -> std_ppcmds
end