The Coq mailing list

[tom.prince AT ualberta.net]

From: Tom Prince 
<tom.prince AT ualberta.net>

This is exactly the structure needed to handle controlling printing
of terms of record type with record or constructor syntax.

Signed-off-by: Tom Prince 
<tom.prince AT ualberta.net>
---

This functor could probably be move to somewhere more generic,
but I don't know where that would be.

 pretyping/detyping.ml  |   24 ++++++++++++------------
 pretyping/detyping.mli |   18 ++++++++++++++++++
 2 files changed, 30 insertions(+), 12 deletions(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e2533b2..fd85d15 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -45,34 +45,34 @@ let has_two_constructors lc =
 let isomorphic_to_tuple lc = (Array.length lc = 1)
 
 let encode_bool r =
-  let (_,lc as x) = encode_inductive r in
+  let (x,lc) = encode_inductive r in
   if not (has_two_constructors lc) then
     user_err_loc (loc_of_reference r,"encode_if",
       str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
-  let (_,lc as x) = encode_inductive r in
+  let (x,lc) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
     user_err_loc (loc_of_reference r,"encode_tuple",
       str "This type cannot be seen as a tuple type.");
   x
 
-module PrintingCasesMake =
+module PrintingInductiveMake =
   functor (Test : sig
-     val encode : reference -> inductive * int array
+     val encode : reference -> inductive
      val member_message : std_ppcmds -> bool -> std_ppcmds
      val field : string
      val title : string
   end) ->
   struct
-    type t = inductive * int array
+    type t = inductive
     let encode = Test.encode
-    let subst subst ((kn,i), ints as obj) =
+    let subst subst (kn, ints as obj) =
       let kn' = subst_ind subst kn in
        if kn' == kn then obj else
-         (kn',i), ints
-    let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
+         kn', ints
+    let printer ind = pr_global_env Idset.empty (IndRef ind)
     let key = ["Printing";Test.field]
     let title = Test.title
     let member_message x = Test.member_message (printer x)
@@ -80,7 +80,7 @@ module PrintingCasesMake =
   end
 
 module PrintingCasesIf =
-  PrintingCasesMake (struct
+  PrintingInductiveMake (struct
     let encode = encode_bool
     let field = "If"
     let title = "Types leading to pretty-printing of Cases using a `if' 
form: "
@@ -92,7 +92,7 @@ module PrintingCasesIf =
   end)
 
 module PrintingCasesLet =
-  PrintingCasesMake (struct
+  PrintingInductiveMake (struct
     let encode = encode_tuple
     let field = "Let"
     let title =
@@ -329,9 +329,9 @@ let detype_case computable detype detype_eqns testdep 
avoid data p c bl =
         RegularStyle
       else if st = LetPatternStyle then
        st
-      else if PrintingLet.active (indsp,consnargsl) then
+      else if PrintingLet.active indsp then
        LetStyle
-      else if PrintingIf.active (indsp,consnargsl) then
+      else if PrintingIf.active indsp then
        IfStyle
       else
        st
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index ff98f74..a423a47 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -54,3 +54,21 @@ val simple_cases_matrix_of_branches :
   inductive -> int list -> glob_constr list -> cases_clauses
 val return_type_of_predicate :
   inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr 
option
+
+module PrintingInductiveMake :
+  functor (Test : sig
+    val encode : Libnames.reference -> Names.inductive
+    val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds
+    val field : string
+    val title : string
+  end) ->
+    sig
+      type t = Names.inductive
+      val encode : Libnames.reference -> Names.inductive
+      val subst : substitution -> t -> t
+      val printer : t -> Pp.std_ppcmds
+      val key : Goptions.option_name
+      val title : string
+      val member_message : t -> bool -> Pp.std_ppcmds
+      val synchronous : bool
+    end
-- 
1.7.5.2