1. Code simplification

2. Bug fixed: do not anticipate justification for rewritingLR or rewriting RL
   if justification is "exact"

diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml
index ae7c8d46d34ec143c92f85875700171e3015b00c..24c4faa348aa4e1c853b75ff5b5a79ae0b0cec5d 100644 (file)
--- a/components/content_pres/content2pres.ml
+++ b/components/content_pres/content2pres.ml
@@ -121,18 +121,25 @@ let add_xref id = function
   | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t)
   | _ -> assert false (* TODO, add_xref is meaningful for all boxes *)
 
-let rec justification term2pres p = 
-  if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
-     ((p.Con.proof_context = []) &
-      (p.Con.proof_apply_context = []) &
-      (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then
+let rec justification ~ignore_atoms term2pres p = 
+  if p.Con.proof_conclude.Con.conclude_method = "Exact" &&
+     ignore_atoms
+  then
+   [], None
+  else if
+   (p.Con.proof_conclude.Con.conclude_method = "Exact" && not ignore_atoms) ||
+   (p.Con.proof_context = [] &&
+    p.Con.proof_apply_context = [] &&
+    p.Con.proof_conclude.Con.conclude_method = "Apply")
+  then
     let pres_args = 
-      make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
-    B.H([],
-      (B.b_kw "by")::B.b_space::
-      B.Text([],"(")::pres_args@[B.Text([],")")]), None 
+      make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
+    in
+     [B.H([],
+       (B.b_kw "by")::B.b_space::
+       B.Text([],"(")::pres_args@[B.Text([],")")])], None 
   else
-   B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"]),
+   [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 =
@@ -432,21 +439,37 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
          || conclude.Con.conclude_method = "RewriteRL" then
       let justif1,justif2 = 
         (match (List.nth conclude.Con.conclude_args 6) with
-           Con.ArgProof p -> justification term2pres p
+           Con.ArgProof p -> justification ~ignore_atoms:true term2pres p
          | _ -> assert false) in
       let justif =
        match justif2 with
           None -> justif1
-        | Some j -> j
+        | Some j -> [j]
+      in
+      let index_term1, index_term2 =
+       if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
+        || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
+       then 2,5 else 5,2
       in
       let term1 = 
-        (match List.nth conclude.Con.conclude_args 2 with
+        (match List.nth conclude.Con.conclude_args index_term1 with
            Con.Term (_,t) -> term2pres t
          | _ -> assert false) in 
       let term2 = 
-        (match List.nth conclude.Con.conclude_args 5 with
+        (match List.nth conclude.Con.conclude_args index_term2 with
            Con.Term (_,t) -> term2pres t
          | _ -> assert false) in
+      let justif =
+       match justif with
+          [] -> []
+        | _ ->
+         justif @
+          [B.V([],
+            [B.b_kw "we proved (" ;
+             term1 ;
+             B.b_kw "=" ;
+             term2; B.b_kw ") (equality)."])]
+      in
 (*
       B.V ([], 
          B.H ([],[
@@ -457,17 +480,11 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
           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([], [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])]) *)
+      B.V([], justif @ [B.b_kw "by _"])
     else if conclude.Con.conclude_method = "Eq_chain" then
       let justification p =
-       let j1,j2 = justification term2pres p in
-        [j1], match j2 with Some j -> [j] | None -> []
+       let j1,j2 = justification ~ignore_atoms:false term2pres p in
+        j1, match j2 with Some j -> [j] | None -> []
       in
       let rec aux args =
        match args with