- better handling of proof expansion/contraction

- helm:xref added in most places

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 9356c288540066c7b207c4d02d75ba539866954e..da20856d2694a5152b8561d5b5a56751356d92fe 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -105,6 +105,8 @@ let is_big_general countterm p =
              (match prem.Con.premise_binder with
                 Some s -> current_size + (String.length s)
               | None -> current_size + 7) 
+         | Con.Lemma lemma -> 
+             current_size + (String.length lemma.Con.lemma_name)
          | Con.Term t -> countterm current_size t
          | Con.ArgProof p -> countp current_size p
          | Con.ArgMethod s -> (maxsize + 1)) in
@@ -115,28 +117,38 @@ let is_big_general countterm p =
 let is_big = is_big_general (Cexpr2pres.countterm)
 ;;
 
-let make_row items concl =
+let get_xref =
+    let module Con = Content in
+      function
+        `Declaration d  
+      | `Hypothesis d -> d.Con.dec_id
+      | `Proof p -> p.Con.proof_id
+      | `Definition d -> d.Con.def_id
+      | `Joint jo -> jo.Con.joint_id
+;;
+
+let make_row ?(attrs=[]) items concl =
   let module P = Mpresentation in
     (match concl with 
        P.Mtable _ -> (* big! *)
-         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+         P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false";
           None,"columnalign","left"],
            [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]);
             P.Mtr ([],[P.Mtd ([],P.indented concl)])])
      | _ ->  (* small *)
-       P.Mrow([],items@[P.Mspace([None,"width","0.1cm"]);concl]))
+       P.Mrow(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl]))
 ;;
 
-let make_concl verb concl =
+let make_concl ?(attrs=[]) verb concl =
   let module P = Mpresentation in
     (match concl with 
        P.Mtable _ -> (* big! *)
-         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
+         P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false";
           None,"columnalign","left"],
            [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]);
             P.Mtr ([],[P.Mtd ([],P.indented concl)])])
      | _ ->  (* small *)
-       P.Mrow([],
+       P.Mrow(attrs,
         [P.Mtext([None,"mathcolor","Red"],verb); 
          P.Mspace([None,"width","0.1cm"]);
          concl]))
@@ -153,14 +165,16 @@ let make_args_for_apply term2pres args =
           (match prem.Con.premise_binder with
              None -> "previous"
            | Some s -> s) in
-        P.Mi([],name)::row
+        P.smallskip::P.Mi([],name)::row
+    | Con.Lemma lemma -> 
+         P.smallskip::P.Mi([],lemma.Con.lemma_name)::row 
     | Con.Term t -> 
         if is_first then
           (term2pres t)::row
-        else P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row
+        else P.smallskip::P.Mi([],"_")::row
     | Con.ArgProof _ 
     | Con.ArgMethod _ -> 
-       P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row) in
+       P.smallskip::P.Mi([],"_")::row) in
  match args with 
    hd::tl -> 
      make_arg_for_apply true hd 
@@ -201,12 +215,6 @@ and proof2pres term2pres p =
           let presacontext = 
             acontext2pres p.Con.proof_apply_context presconclude indent in
           context2pres p.Con.proof_context presacontext in
-(*
-          P.Mtable ([("align","baseline 1");("equalrows","false");
-            ("columnalign","left")],
-            (context2pres_old p.Con.proof_context)@
-            (acontext2pres_old p.Con.proof_apply_context indent)@
-            [conclude2pres_old p.Con.proof_conclude indent]) in *)
       match p.Con.proof_name with
         None -> body
       | Some name ->
@@ -220,24 +228,22 @@ and proof2pres term2pres p =
               [(make_concl "proof of" ac);
                 body]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
-              None,"columnalign","left"],
+              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 *)
     let module P = Mpresentation in
     List.fold_right
       (fun ce continuation ->
+         let xref = get_xref ce in
          P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
-          None,"columnalign","left"],
-           [P.Mtr([],[P.Mtd ([],ce2pres ce)]);
+          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
 
-  and context2pres_old c =
-    let module P = Mpresentation in
-    List.map 
-      (function ce -> P.Mtr ([], [P.Mtd ([], ce2pres ce)])) c
-
   and ce2pres =
     let module P = Mpresentation in
     let module Con = Content in
@@ -284,6 +290,7 @@ and proof2pres term2pres p =
             P.Mtext ([],"jointdef")
 
   and acontext2pres ac continuation indent =
+    let module Con = Content in
     let module P = Mpresentation in
     List.fold_right
       (fun p continuation ->
@@ -293,20 +300,10 @@ and proof2pres term2pres p =
            else 
              proof2pres p in
          P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
-          None,"columnalign","left"],
-           [P.Mtr([],[P.Mtd ([],hd)]);
+          None,"columnalign","left"; Some "helm","xref",p.Con.proof_id],
+           [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]);
             P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation 
 
-  and acontext2pres_old ac indent =
-    let module P = Mpresentation in
-    List.map 
-      (function p -> 
-         if indent then
-           P.Mtr ([], [P.Mtd ([], P.indented (proof2pres p))])
-         else 
-           P.Mtr ([], 
-             [P.Mtd ([], proof2pres p)])) ac
-
   and conclude2pres conclude indent =
     let module P = Mpresentation in
     if indent then
@@ -314,14 +311,6 @@ and proof2pres term2pres p =
     else 
       conclude_aux conclude
 
-  and conclude2pres_old conclude indent =
-    let module P = Mpresentation in
-    if indent then
-      P.Mtr ([], [P.Mtd ([], P.indented (conclude_aux conclude))])
-    else 
-      P.Mtr ([], 
-        [P.Mtd ([], conclude_aux conclude)])
-
   and conclude_aux conclude =
     let module Con = Content in
     let module P = Mpresentation in
@@ -339,7 +328,7 @@ 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"],
+        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id],
         [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)])])
@@ -348,7 +337,9 @@ and proof2pres term2pres p =
       (match conclude.Con.conclude_conclusion with 
          None -> P.Mtext([],"NO Conclusion!!!")
        | Some c -> term2pres c) in
-      make_concl "that is equivalent to" conclusion
+      make_concl 
+        ~attrs:[Some "helm", "xref", conclude.Con.conclude_id]
+          "that is equivalent to" conclusion
     else if conclude.Con.conclude_method = "Exact" then
       let conclusion = 
         (match conclude.Con.conclude_conclusion with 
@@ -358,7 +349,7 @@ and proof2pres term2pres p =
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
          | _ -> assert false) in
-      make_row 
+      make_row ~attrs:[Some "helm", "xref", conclude.Con.conclude_id]
         [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       let conclusion = 
@@ -369,7 +360,8 @@ and proof2pres term2pres p =
          [Con.ArgProof p] -> 
            P.Mtable 
             ([None,"align","baseline 1"; None,"equalrows","false";
-              None,"columnalign","left"],
+              None,"columnalign","left"; 
+              Some "helm", "xref", conclude.Con.conclude_id],
               [P.Mtr([],[P.Mtd([],proof2pres p)]);
                P.Mtr([],[P.Mtd([],
                 (make_concl "we proved *" conclusion))])]);
@@ -394,7 +386,8 @@ and proof2pres term2pres p =
            None -> P.Mtext([],"NO Conclusion!!!")
          | Some c -> term2pres c) in
       P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
-            None,"columnalign","left"],
+            None,"columnalign","left"; 
+            Some "helm", "xref", conclude.Con.conclude_id],
              [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
                P.Mtext([None,"mathcolor","Red"],"rewrite");
                P.Mspace([None,"width","0.1cm"]);term1;
@@ -416,12 +409,13 @@ and proof2pres term2pres p =
          let concl = (term2pres t) in
          let ann_concl = make_concl "we proved" concl in
          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
-            None,"columnalign","left"],
+            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.Mtable 
-        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
+        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; Some "helm", "xref", conclude.Con.conclude_id],
          [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]);
           P.Mtr ([],
            [P.Mtd ([], 
@@ -453,6 +447,8 @@ and proof2pres term2pres p =
           P.Mtext ([],"aux " ^ n)
       | Con.Premise prem -> 
           P.Mtext ([],"premise")
+      | Con.Lemma lemma ->
+          P.Mtext ([],"lemma")
       | Con.Term t -> 
           term2pres t
       | Con.ArgProof p ->
@@ -483,6 +479,7 @@ and proof2pres term2pres p =
               (match prem.Con.premise_binder with
                  None -> P.Mtext ([],"the previous result")
                | Some n -> P.Mi([],n))
+           | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name)
            | Con.Term t -> 
                term2pres t
            | Con.ArgProof p ->
@@ -548,7 +545,7 @@ and proof2pres term2pres p =
              | Some t -> term2pres t) in
           let asubconcl =
              P.Mtr([],[P.Mtd([],
-              make_concl "the thesis becomes" subconcl)]) in
+              P.indented (make_concl "the thesis becomes" subconcl))]) in
           let induction_hypothesis = 
             (match indhyps with
               [] -> []
@@ -579,7 +576,9 @@ and proof2pres term2pres p =
                acontext2pres_old p.Con.proof_apply_context true in *)
           let body = conclude2pres p.Con.proof_conclude true in
           let presacontext = 
-            acontext2pres p.Con.proof_apply_context body true in
+            P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
+              [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof"));
+               acontext2pres p.Con.proof_apply_context body true]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
              None,"columnalign","left"],
              pattern::asubconcl::induction_hypothesis@

diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml
index 4dde38a366cc88967093b98ae73f7fb51cfeede0..09eb6331e085caa2dd1ae94a506ecdd16b4f8beb 100644 (file)
--- a/helm/ocaml/cic_transformations/mpresentation.ml
+++ b/helm/ocaml/cic_transformations/mpresentation.ml
@@ -92,20 +92,20 @@ let two_rows_table_with_brackets attr a b op =
   (* only the open bracket is added; the closed bracket must be in b *)
   Mtable(attr@standard_tbl_attr,
     [Mtr([],[Mtd([],Mrow([],[Mtext([],"(");a]))]);
-     Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);;
+     Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
 
 let two_rows_table_without_brackets attr a b op =
   Mtable(attr@standard_tbl_attr,
     [Mtr([],[Mtd([],a)]);
-     Mtr([],[Mtd([],Mrow([],[indentation;op;smallskip;b]))])]);;
+     Mtr([],[Mtd([],Mrow([],[indentation;op;b]))])]);;
 
 let row_with_brackets attr a b op =
   (* by analogy with two_rows_table_with_brackets we only add the
      open brackets *)
-  Mrow(attr,[Mtext([],"(");a;smallskip;op;smallskip;b])
+  Mrow(attr,[Mtext([],"(");a;op;b])
 
 let row_without_brackets attr a b op =
-  Mrow(attr,[a;smallskip;op;smallskip;b])
+  Mrow(attr,[a;op;b])
 
 (* MathML prefix *)
 let prefix = "m";;