]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/content2pres.ml
is_top_down was not propageted correctly under a bottom-up conversion.
[helm.git] / helm / software / components / content_pres / content2pres.ml
index 45e88ab0a26a9fc5626fc1a86bf6565d2477a9df..ae7c8d46d34ec143c92f85875700171e3015b00c 100644 (file)
@@ -132,12 +132,11 @@ let rec justification term2pres p =
       (B.b_kw "by")::B.b_space::
       B.Text([],"(")::pres_args@[B.Text([],")")]), None 
   else
-   (*(B.b_kw "by"),
-    Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])*)
-   proof2pres true term2pres p, None
+   B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"]),
+    Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)])
      
 and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
-  let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot =
+  let rec proof2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion =
     let indent = 
       let is_decl e = 
         (match e with 
@@ -153,18 +152,20 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
     let body =
         let presconclude = 
           conclude2pres
-           ?skip_initial_lambdas_internal:
-             (match skip_initial_lambdas_internal with
-                 Some (`Later s) -> Some (`Now s)
-               | _ -> None)
-             is_top_down
-             p.Con.proof_name p.Con.proof_conclude indent omit_conclusion
-           omit_dot in
+          ?skip_initial_lambdas_internal:
+            (match skip_initial_lambdas_internal with
+                Some (`Later s) -> Some (`Now s)
+              | _ -> None)
+          is_top_down p.Con.proof_name p.Con.proof_conclude indent
+          omit_conclusion in_bu_conversion in
         let presacontext = 
           acontext2pres
-           (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
-            p.Con.proof_apply_context
-            presconclude indent
+           (if p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" then
+             is_top_down
+            else
+             false)
+           p.Con.proof_apply_context
+           presconclude indent
            (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
         in
         context2pres 
@@ -173,6 +174,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
            | _ -> p.Con.proof_context)
           presacontext
     in
+let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in
     match p.Con.proof_name with
       None -> body
     | Some name ->
@@ -278,18 +280,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
             [] -> 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],
+        let hd = proof2pres is_top_down p in_bu_conversion in
+        let hd = if indent then B.indent hd else hd in
+         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 =
+  and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion in_bu_conversion =
     let tconclude_body = 
       match conclude.Con.conclude_conclusion with
         Some t (*when not omit_conclusion or
@@ -336,20 +334,21 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
               if  conclude.Con.conclude_method = "Intros+LetTac"
                || conclude.Con.conclude_method = "ByInduction"
                || conclude.Con.conclude_method = "TD_Conversion"
+               || conclude.Con.conclude_method = "Eq_chain"
               then
                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
+                 ((if not is_top_down || in_bu_conversion then
                     (make_concl "we proved" concl) ::
                       if not is_top_down then
                        let name = get_name ~default:"previous" name in
                         [B.b_space; B.Text([],"(" ^ name ^ ")")]
                       else []
                    else [B.b_kw "done"]
-                  ) @ if not omit_dot then [B.Text([],".")] else [])
+                  ) @ if not in_bu_conversion then [B.Text([],".")] else [])
             in
              B.V ([], prequel @ [conclude_body; ann_concl])
       | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude
@@ -435,6 +434,11 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
         (match (List.nth conclude.Con.conclude_args 6) with
            Con.ArgProof p -> justification term2pres p
          | _ -> assert false) in
+      let justif =
+       match justif2 with
+          None -> justif1
+        | Some j -> j
+      in
       let term1 = 
         (match List.nth conclude.Con.conclude_args 2 with
            Con.Term (_,t) -> term2pres t
@@ -453,30 +457,27 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
           B.b_space; justif1])::
            match justif2 with None -> [] | Some j -> [B.indent j])
 *)
-    if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
-     || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then
-     B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"])
-    else
-     B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"])
+     if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
+      || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then
+      B.V([], [justif ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"])
+     else
+      B.V([], [justif ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"])
 (*CSC: bad idea
  B.V([], [B.H([],[B.b_kw "obtain fooo " ; term2 ; B.b_kw "=" ; term1;  B.b_kw "by" ; B.b_kw "proof" ; B.Text([],"."); justif1])]) *)
     else if conclude.Con.conclude_method = "Eq_chain" then
       let justification p =
-(*
-        if skip_initial_lambdas <> None (* cheating *) then
-          [B.b_kw "by _"]
-        else
-*)
-          let j1,j2 = justification term2pres p in
-         j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
+       let j1,j2 = justification term2pres p in
+        [j1], match j2 with Some j -> [j] | None -> []
       in
       let rec aux args =
        match args with
          | [] -> []
          | (Con.ArgProof p)::(Con.Term (_,t))::tl -> 
-             B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw
-              "=";B.b_space;term2pres t;B.b_space]@justification p@
-              (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl)
+              let justif1,justif2 = justification p in
+              B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw
+               "=";B.b_space;term2pres t;B.b_space]@justif1@
+               (if tl <> [] then [B.Text ([],".")] else [B.b_space; B.b_kw "done" ; B.Text([],".")])@
+               justif2))::(aux tl)
          | _ -> assert false 
       in
       let hd =