From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 Jul 2003 15:43:35 +0000 (+0000)
Subject: Added Method "exists".
X-Git-Tag: LucaOK~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=45bc31f244e06f1eead7c35bc5b812574edf1737

Added Method "exists".
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 1616c21c8..04be41c45 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -297,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 ->
@@ -409,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
@@ -551,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 
@@ -646,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
 ;;