From 2d548dd33a2a6b22a08d55daef7a65a574193ce7 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 30 Jun 2007 12:20:10 +0000
Subject: [PATCH] Bug fixed in bottom-up conversion. Since the bottom-up
 conversion body is put in the applicative context and since applicative
 contexts get flattened the test for being in a bottom-up conversion must be
 rather complex.

---
 components/content_pres/content2pres.ml | 54 +++++++++++++++++--------
 1 file changed, 38 insertions(+), 16 deletions(-)

diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml
index 5620b6847..97f225f62 100644
--- a/components/content_pres/content2pres.ml
+++ b/components/content_pres/content2pres.ml
@@ -257,17 +257,35 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
               term])
 
   and acontext2pres is_top_down ac continuation indent in_bu_conversion =
-    List.fold_right
-      (fun p continuation ->
+   let rec aux =
+    function
+       [] -> continuation
+     | p::tl ->
+        let continuation = aux tl in
+        (* Applicative context get flattened and the "body" of a BU_Conversion
+           is put in the applicative context. Thus two different situations
+           are possible:
+            {method = "BU_Conversion"; applicative_context=[p1; ...; pn]}
+            {method = xxx; applicative_context =
+              [ p1; ...; pn; {method="BU_Conversion"} ; p_{n+1}; ... ; pm ]}
+           In both situations only pn must be processed in in_bu_conversion
+           mode
+        *)
+        let in_bu_conversion =
+         match tl with
+            [] -> in_bu_conversion
+          | p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion"
+        in
         let hd = 
           if indent then
             B.indent (proof2pres is_top_down p in_bu_conversion)
           else 
             proof2pres is_top_down p in_bu_conversion
         in
-         B.V([Some "helm","xref",p.Con.proof_id],
-           [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
-            continuation])) ac continuation 
+        B.V([Some "helm","xref",p.Con.proof_id],
+          [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
+           continuation])
+   in aux ac
 
   and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot =
     let tconclude_body = 
@@ -320,10 +338,15 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                B.Text([],"")
               else if omit_conclusion then 
                 B.H([], [B.b_kw "done" ; B.Text([],".") ])
-              else B.b_hv []
-               ((if not is_top_down || omit_dot then [make_concl "we proved"
-               concl; B.Text([],if not is_top_down then "(previous)" else "")]
-               else [B.b_kw "done"]) @ if not omit_dot then [B.Text([],".")] else [])
+              else
+                B.b_hv []
+                 ((if not is_top_down || omit_dot then
+                    (make_concl "we proved" concl) ::
+                      if not is_top_down then
+                       [B.b_space; B.Text([],"(previous)")]
+                      else []
+                   else [B.b_kw "done"]
+                  ) @ if not omit_dot then [B.Text([],".")] else [])
             in
             B.V ([], prequel @ [conclude_body; ann_concl])
       | _ -> conclude_aux ?skip_initial_lambdas_internal conclude
@@ -596,8 +619,6 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                    | _ -> assert false in
                let hyps = List.map make_hyp indhyps in
                text::hyps) in          
-          (* let acontext = 
-               acontext2pres_old p.Con.proof_apply_context true in *)
           let body =
            conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in
           let presacontext = 
@@ -641,7 +662,6 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip;
                  B.b_kw "is contradictory, hence" ]
            | _ -> assert false) in
-            (* let body = proof2pres {proof with Con.proof_context = tl} false in *)
        make_row arg proof_conclusion
 
      and andind conclude =
@@ -679,8 +699,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                 B.Text([],")");
                 B.skip;
                 term2pres hyp2.Con.dec_type]) in
-            (* let body = proof2pres {proof with Con.proof_context = tl} false in *)
-            let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in
+            let body =
+             conclude2pres false proof.Con.proof_name proof.Con.proof_conclude
+              false true false in
             let presacontext = 
               acontext2pres false proof.Con.proof_apply_context body false false
             in
@@ -719,8 +740,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                 B.Text([],")");
                 B.skip;
                 term2pres hyp.Con.dec_type]) in
-            (* let body = proof2pres {proof with Con.proof_context = tl} false in *)
-            let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in
+            let body =
+             conclude2pres false proof.Con.proof_name proof.Con.proof_conclude
+              false true false in
             let presacontext = 
               acontext2pres false proof.Con.proof_apply_context body false false
             in
-- 
2.39.2