Added method AndInd.

[helm.git] / helm / ocaml / cic_transformations / content2pres.ml

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 04be41c45cd3515f78f4e83781e3d896d14f0211..575bb687af1eea1966a5aa59138b26afacc06e45 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -192,7 +192,7 @@ let rec justification term2pres p =
       make_args_for_apply term2pres p.Con.proof_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([],")")]) 
+      P.Mtext([],"(")::pres_args@[P.Mtext([],")")]) 
   else proof2pres term2pres p 
      
 and proof2pres term2pres p =
@@ -342,7 +342,10 @@ and proof2pres term2pres p =
             make_concl "that is equivalent to" concl
           else  
             let conclude_body = conclude_aux conclude in
-            let ann_concl = make_concl "we conclude" concl in
+            let ann_concl = 
+              if conclude.Con.conclude_method = "TD_Conversion" then
+                 make_concl "that is equivalent to" concl 
+              else make_concl "we conclude" concl in
             P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
                 [P.Mtr ([],[P.Mtd ([],conclude_body)]);
@@ -415,6 +418,8 @@ and proof2pres term2pres p =
       byinduction conclude
     else if (conclude.Con.conclude_method = "Exists") then
       exists conclude
+    else if (conclude.Con.conclude_method = "AndInd") then
+      andind conclude
     else if (conclude.Con.conclude_method = "Rewrite") then
       let justif = 
         (match (List.nth conclude.Con.conclude_args 6) with
@@ -645,6 +650,65 @@ and proof2pres term2pres p =
               [P.Mtr([],[P.Mtd([],presacontext)])])
        | _ -> assert false 
 
+     and andind conclude =
+       let module P = Mpresentation in
+       let module Con = Content in
+       let proof_conclusion = 
+         (match conclude.Con.conclude_conclusion with
+            None -> P.Mtext([],"No conclusion???")
+          | Some t -> term2pres t) in
+       let proof,case_arg = 
+         (match conclude.Con.conclude_args with
+             [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
+           | _ -> assert false;
+             (* 
+             List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+             assert false *)) in
+       let arg = 
+         (match case_arg with
+             Con.Aux n -> assert false
+           | Con.Premise prem ->
+              (match prem.Con.premise_binder with
+                 None -> []
+               | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)])
+           | Con.Lemma lemma -> 
+               [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)]
+           | _ -> assert false) in
+       match proof.Con.proof_context with
+         `Hypothesis hyp1::`Hypothesis hyp2::tl ->
+            let get_name hyp =
+              (match hyp.Con.dec_name with
+                None -> "_"
+              | Some s -> s) in
+            let preshyp1 = 
+              P.Mrow ([],
+               [P.Mtext([],"(");
+                P.Mi([],get_name hyp1);
+                P.Mtext([],")");
+                P.smallskip;
+                term2pres hyp1.Con.dec_type]) in
+            let preshyp2 = 
+              P.Mrow ([],
+               [P.Mtext([],"(");
+                P.Mi([],get_name hyp2);
+                P.Mtext([],")");
+                P.smallskip;
+                term2pres hyp2.Con.dec_type]) in
+            (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+            let body = conclude2pres proof.Con.proof_conclude false true in
+            let presacontext = 
+              acontext2pres proof.Con.proof_apply_context body false in
+            P.Mtable 
+              ([None,"align","baseline 1"; None,"equalrows","false"; 
+                None,"columnalign","left"],
+               [P.Mtr ([],[P.Mtd ([],
+                 P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]);
+                P.Mtr ([],[P.Mtd ([],preshyp1)]);
+                P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]);
+                P.Mtr ([],[P.Mtd ([],preshyp2)]);
+                P.Mtr ([],[P.Mtd ([],presacontext)])]);
+         | _ -> assert false
+
      and exists conclude =
        let module P = Mpresentation in
        let module Con = Content in