Improved management of conclusions, to avoid repetitions.

Some problems of xrefs have been fixed.

diff --git a/helm/ocaml/META.helm-cic_omdoc.src b/helm/ocaml/META.helm-cic_omdoc.src
index 313d19cd2bfd657cd6a17a71e20737323f9635ab..e05ddfcecce92aedd7c09e7050c55f93fceeb2ec 100644 (file)
--- a/helm/ocaml/META.helm-cic_omdoc.src
+++ b/helm/ocaml/META.helm-cic_omdoc.src
@@ -1,4 +1,4 @@
-requires="helm-cic_proof_checking"
+requires="helm-cic_proof_checking helm-mathql_interpreter"
 version="0.0.1"
 archive(byte)="cic_omdoc.cma"
 archive(native)="cic_omdoc.cmxa"

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index da20856d2694a5152b8561d5b5a56751356d92fe..cd7bac62544b101ad2be9b0d61e30d21e559713b 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -206,12 +206,14 @@ and proof2pres term2pres p =
            | `Hypothesis _ -> true
            | _ -> false) in
         ((List.filter is_decl p.Con.proof_context) != []) in 
+      let omit_conclusion = (not indent) && (p.Con.proof_context != []) in
       let concl = 
         (match p.Con.proof_conclude.Con.conclude_conclusion with
            None -> None
          | Some t -> Some (term2pres t)) in
       let body =
-          let presconclude = conclude2pres p.Con.proof_conclude indent in
+          let presconclude = 
+            conclude2pres p.Con.proof_conclude indent omit_conclusion in
           let presacontext = 
             acontext2pres p.Con.proof_apply_context presconclude indent in
           context2pres p.Con.proof_context presacontext in
@@ -228,22 +230,39 @@ and proof2pres term2pres p =
               [(make_concl "proof of" ac);
                 body]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
-              None,"columnalign","left";Some "helm", "xref", p.Con.proof_id],
+              None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
              P.Mtr ([],[P.Mtd ([], P.indented action)])])
+(*
+          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+              None,"columnalign","left";Some "helm", "xref", p.Con.proof_id],
+            [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
+             P.Mtr ([],[P.Mtd ([], P.indented action)])]) *)
 
   and context2pres c continuation =
     (* we generate a subtable for each context element, for selection
-       purposes *)
+       purposes 
+       The table generated by the head-element does not have an xref;
+       the whole context-proof is already selectable *)
     let module P = Mpresentation in
-    List.fold_right
-      (fun ce continuation ->
-         let xref = get_xref ce in
+    match c with
+      [] -> continuation
+    | hd::tl -> 
+        let continuation' =
+          List.fold_right
+            (fun ce continuation ->
+              let xref = get_xref ce in
+              P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
+               None,"columnalign","left"; Some "helm", "xref", xref ],
+                [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]);
+                 P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in
+         let hd_xref= get_xref hd in
          P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
-          None,"columnalign","left"; Some "helm", "xref", xref ],
-           [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]);
-            P.Mtr([],[P.Mtd ([], continuation)])])) c continuation
-
+           None,"columnalign","left"],
+             [P.Mtr([Some "helm", "xref", "ce_"^hd_xref],
+               [P.Mtd ([],ce2pres hd)]);
+             P.Mtr([],[P.Mtd ([], continuation')])])
+         
   and ce2pres =
     let module P = Mpresentation in
     let module Con = Content in
@@ -304,12 +323,29 @@ and proof2pres term2pres p =
            [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]);
             P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation 
 
-  and conclude2pres conclude indent =
+  and conclude2pres conclude indent omit_conclusion =
+    let module Con = Content in
     let module P = Mpresentation in
-    if indent then
-      P.indented (conclude_aux conclude)
+    let tconclude_body = 
+      match conclude.Con.conclude_conclusion with
+        Some t when not omit_conclusion ->
+          let concl = (term2pres t) in 
+          if conclude.Con.conclude_method = "BU_Conversion" then
+            make_concl "that is equivalent to" concl
+          else  
+            let conclude_body = conclude_aux conclude in
+            let ann_concl = make_concl "we conclude" concl in
+            P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+              None,"columnalign","left"],
+                [P.Mtr ([],[P.Mtd ([],conclude_body)]);
+                 P.Mtr ([],[P.Mtd ([],ann_concl)])])
+      | _ -> conclude_aux conclude in
+    if indent then 
+      P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],
+                    [tconclude_body]))
     else 
-      conclude_aux conclude
+      P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
+
 
   and conclude_aux conclude =
     let module Con = Content in
@@ -328,18 +364,12 @@ and proof2pres term2pres p =
            None -> P.Mtext([],"NO SYNTH!!!")
          | Some c -> (term2pres c)) in
       P.Mtable 
-        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id],
+        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
         [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]);
          P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]);
          P.Mtr([],[P.Mtd([],proof2pres subproof)])])
     else if conclude.Con.conclude_method = "BU_Conversion" then
-      let conclusion = 
-      (match conclude.Con.conclude_conclusion with 
-         None -> P.Mtext([],"NO Conclusion!!!")
-       | Some c -> term2pres c) in
-      make_concl 
-        ~attrs:[Some "helm", "xref", conclude.Con.conclude_id]
-          "that is equivalent to" conclusion
+      assert false
     else if conclude.Con.conclude_method = "Exact" then
       let conclusion = 
         (match conclude.Con.conclude_conclusion with 
@@ -349,9 +379,13 @@ and proof2pres term2pres p =
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
          | _ -> assert false) in
-      make_row ~attrs:[Some "helm", "xref", conclude.Con.conclude_id]
+      make_row 
         [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
     else if conclude.Con.conclude_method = "Intros+LetTac" then
+      (match conclude.Con.conclude_args with
+         [Con.ArgProof p] -> proof2pres p
+       | _ -> assert false)
+(* OLD CODE 
       let conclusion = 
       (match conclude.Con.conclude_conclusion with 
          None -> P.Mtext([],"NO Conclusion!!!")
@@ -360,12 +394,12 @@ and proof2pres term2pres p =
          [Con.ArgProof p] -> 
            P.Mtable 
             ([None,"align","baseline 1"; None,"equalrows","false";
-              None,"columnalign","left"; 
-              Some "helm", "xref", conclude.Con.conclude_id],
+              None,"columnalign","left"],
               [P.Mtr([],[P.Mtd([],proof2pres p)]);
                P.Mtr([],[P.Mtd([],
-                (make_concl "we proved *" conclusion))])]);
+                (make_concl "we proved 1" conclusion))])]);
        | _ -> assert false)
+*)
     else if (conclude.Con.conclude_method = "ByInduction") then
       byinduction conclude
     else if (conclude.Con.conclude_method = "Rewrite") then
@@ -380,14 +414,23 @@ and proof2pres term2pres p =
       let term2 = 
         (match List.nth conclude.Con.conclude_args 5 with
            Con.Term t -> term2pres t
-         | _ -> assert false) in  
+         | _ -> assert false) in
+      P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
+        None,"columnalign","left"], 
+         [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
+          P.Mtext([None,"mathcolor","Red"],"rewrite");
+          P.Mspace([None,"width","0.1cm"]);term1;
+          P.Mspace([None,"width","0.1cm"]);
+          P.Mtext([None,"mathcolor","Red"],"with");
+          P.Mspace([None,"width","0.1cm"]);term2]))]);
+          P.Mtr ([],[P.Mtd ([],P.indented justif)])]);
+(* OLD CODE   
       let conclusion = 
         (match conclude.Con.conclude_conclusion with 
            None -> P.Mtext([],"NO Conclusion!!!")
          | Some c -> term2pres c) in
       P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
-            None,"columnalign","left"; 
-            Some "helm", "xref", conclude.Con.conclude_id],
+            None,"columnalign","left"],
              [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
                P.Mtext([None,"mathcolor","Red"],"rewrite");
                P.Mspace([None,"width","0.1cm"]);term1;
@@ -395,10 +438,15 @@ and proof2pres term2pres p =
                P.Mtext([None,"mathcolor","Red"],"with");
                P.Mspace([None,"width","0.1cm"]);term2]))]);
               P.Mtr ([],[P.Mtd ([],P.indented justif)]);
-              P.Mtr ([],[P.Mtd ([],make_concl "we proved" conclusion)])])
+              P.Mtr ([],[P.Mtd ([],make_concl "we proved 2" conclusion)])]) *)
     else if conclude.Con.conclude_method = "Apply" then
       let pres_args = 
-        make_args_for_apply term2pres conclude.Con.conclude_args in 
+        make_args_for_apply term2pres conclude.Con.conclude_args in
+      P.Mrow([],
+        P.Mtext([None,"mathcolor","Red"],"by")::
+        P.Mspace([None,"width","0.1cm"])::
+        P.Mo([],"(")::pres_args@[P.Mo([],")")])
+(* OLD CODE 
       let by = 
          P.Mrow([],
            P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
@@ -407,15 +455,15 @@ and proof2pres term2pres p =
         None -> P.Mrow([],[P.Mtext([],"QUA");by])
       | Some t ->
          let concl = (term2pres t) in
-         let ann_concl = make_concl "we proved" concl in
+         let ann_concl = make_concl "we proved 3" concl in
          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
             None,"columnalign","left"; 
             Some "helm", "xref", conclude.Con.conclude_id],
              [P.Mtr ([],[P.Mtd ([],by)]);
-              P.Mtr ([],[P.Mtd ([],ann_concl)])])
-    else let body =
+              P.Mtr ([],[P.Mtd ([],ann_concl)])]) *)
+    else 
       P.Mtable 
-        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id],
+        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
          [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]);
           P.Mtr ([],
            [P.Mtd ([], 
@@ -423,16 +471,17 @@ and proof2pres term2pres p =
                (P.Mtable 
                  ([None,"align","baseline 1"; None,"equalrows","false";
                    None,"columnalign","left"],
-                  args2pres conclude.Con.conclude_args))))])]) in
+                  args2pres conclude.Con.conclude_args))))])]) 
+(* OLD CODE 
      match conclude.Con.conclude_conclusion with
        None -> body
      | Some t ->
          let concl = (term2pres t) in
-         let ann_concl = make_concl "we proved" concl in
+         let ann_concl = make_concl "we proved 4" concl in
          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
             None,"columnalign","left"],
              [P.Mtr ([],[P.Mtd ([],body)]);
-              P.Mtr ([],[P.Mtd ([],ann_concl)])])
+              P.Mtr ([],[P.Mtd ([],ann_concl)])]) *)
 
   and args2pres l =
     let module P = Mpresentation in
@@ -489,14 +538,21 @@ and proof2pres term2pres p =
         (make_concl "we proceede by induction on" arg) in
      let to_prove =
         (make_concl "to prove" proof_conclusion) in
+     P.Mtable 
+       ([None,"align","baseline 1"; None,"equalrows","false"; 
+         None,"columnalign","left"],
+          P.Mtr ([],[P.Mtd ([],induction_on)])::
+          P.Mtr ([],[P.Mtd ([],to_prove)])::
+          (make_cases args_for_cases))
+(* OLD CODE   
      let we_proved = 
-        (make_concl "we proved" proof_conclusion) in
+        (make_concl "we proved 5" proof_conclusion) in 
      P.Mtable 
        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
           P.Mtr ([],[P.Mtd ([],induction_on)])::
           P.Mtr ([],[P.Mtd ([],to_prove)])::
           (make_cases args_for_cases) @
-          [P.Mtr ([],[P.Mtd ([],we_proved)])]) 
+          [P.Mtr ([],[P.Mtd ([],we_proved)])]) *)
     
     and make_cases args_for_cases =
     let module P = Mpresentation in
@@ -574,7 +630,7 @@ and proof2pres term2pres p =
                text::hyps) in          
           (* let acontext = 
                acontext2pres_old p.Con.proof_apply_context true in *)
-          let body = conclude2pres p.Con.proof_conclude true in
+          let body = conclude2pres p.Con.proof_conclude true false in
           let presacontext = 
             P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
               [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof"));