Added Method "exists".

[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 cd7bac62544b101ad2be9b0d61e30d21e559713b..04be41c45cd3515f78f4e83781e3d896d14f0211 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -220,15 +220,19 @@ and proof2pres term2pres p =
       match p.Con.proof_name with
         None -> body
       | Some name ->
-          let ac = 
-        (match concl with
-               None -> P.Mtext([],"NO PROOF!!!")
-             | Some c -> c) in 
           let action = 
-            P.Maction([None,"actiontype","toggle" ;
-                       None,"selection","1"],
-              [(make_concl "proof of" ac);
-                body]) in
+           match concl with
+              None -> body
+(*
+               P.Maction
+                 ([None,"actiontype","toggle" ; None,"selection","1"],
+                  [P.Mtext [] "proof" ; body])
+*)
+            | Some ac ->
+               P.Maction
+                 ([None,"actiontype","toggle" ; None,"selection","1"],
+                  [(make_concl "proof of" ac); body])
+          in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
@@ -293,7 +297,11 @@ and proof2pres term2pres p =
                    ty])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Proof p -> proof2pres p
+      | `Proof p -> 
+           (match  p.Con.proof_name with
+              Some "w" -> prerr_endline ("processing w");
+            | _ -> ());
+           proof2pres p 
       | `Definition d -> 
            (match d.Con.def_name with
               Some s ->
@@ -371,16 +379,19 @@ and proof2pres term2pres p =
     else if conclude.Con.conclude_method = "BU_Conversion" then
       assert false
     else if conclude.Con.conclude_method = "Exact" then
-      let conclusion = 
-        (match conclude.Con.conclude_conclusion with 
-           None -> P.Mtext([],"NO Conclusion!!!")
-         | Some c -> term2pres c) in
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
          | _ -> assert false) in
-      make_row 
-        [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
+      (match conclude.Con.conclude_conclusion with 
+         None ->
+          P.Mrow []
+           [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+       | Some c -> let conclusion = term2pres c in
+          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
@@ -402,6 +413,8 @@ and proof2pres term2pres p =
 *)
     else if (conclude.Con.conclude_method = "ByInduction") then
       byinduction conclude
+    else if (conclude.Con.conclude_method = "Exists") then
+      exists conclude
     else if (conclude.Con.conclude_method = "Rewrite") then
       let justif = 
         (match (List.nth conclude.Con.conclude_args 6) with
@@ -544,16 +557,7 @@ and proof2pres term2pres p =
           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 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)])]) *)
-    
+
     and make_cases args_for_cases =
     let module P = Mpresentation in
     List.map 
@@ -639,7 +643,55 @@ and proof2pres term2pres p =
              None,"columnalign","left"],
              pattern::asubconcl::induction_hypothesis@
               [P.Mtr([],[P.Mtd([],presacontext)])])
-      | _ -> assert false in
+       | _ -> assert false 
+
+     and exists 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 = 
+         (match conclude.Con.conclude_args with
+             [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
+           | _ -> assert false;
+             (* 
+             List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+             assert false *)) in
+       match proof.Con.proof_context with
+           `Declaration decl::`Hypothesis hyp::tl
+         | `Hypothesis decl::`Hypothesis hyp::tl ->
+           let get_name decl =
+             (match decl.Con.dec_name with
+                None -> "_"
+              | Some s -> s) in
+           let presdecl = 
+             P.Mrow ([],
+               [P.Mtext([None,"mathcolor","Red"],"let");
+                P.smallskip;
+                P.Mi([],get_name decl);
+                P.Mtext([],":"); term2pres decl.Con.dec_type]) in
+           let suchthat =
+             P.Mrow ([],
+               [P.Mtext([None,"mathcolor","Red"],"such that");
+                P.smallskip;
+                P.Mtext([],"(");
+                P.Mi([],get_name hyp);
+                P.Mtext([],")");
+                P.smallskip;
+                term2pres hyp.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 ([],presdecl)]);
+                P.Mtr ([],[P.Mtd ([],suchthat)]);
+                P.Mtr ([],[P.Mtd ([],presacontext)])]);
+         | _ -> assert false in
 
 proof2pres p
 ;;
@@ -693,7 +745,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                        (id,n,context,ty) ->
                          P.Mtr []
                           [P.Mtd []
-                           (P.Mrow []
+                           (P.Mrow [Some "helm", "xref", id]
                              (List.map
                                (function
                                    (_,None) ->