Moving mutual inductive printing from Printer to Printmod.

1 files changed, 113 insertions, 1 deletions

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