Added all transformations for sequents.

[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 af3999a3963df8fd1aa714dce8ab6f86c2f394bc..c0cdc5c0f0f0c289cc07afd85c1127161b25d2d8 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -436,6 +436,8 @@ and proof2pres term2pres p =
                 (make_concl "we proved 1" conclusion))])]);
        | _ -> assert false)
 *)
+    else if (conclude.Con.conclude_method = "Case") then
+      case conclude
     else if (conclude.Con.conclude_method = "ByInduction") then
       byinduction conclude
     else if (conclude.Con.conclude_method = "Exists") then
@@ -507,6 +509,44 @@ and proof2pres term2pres p =
       | Con.ArgMethod s -> 
          P.Mtext ([],"method") 
  
+   and case 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 arg,args_for_cases = 
+       (match conclude.Con.conclude_args with
+           Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
+             arg,tl
+         | _ -> assert false) in
+     let case_on =
+       let case_arg = 
+         (match arg with
+            Con.Aux n -> 
+              P.Mtext ([],"an aux???")
+           | Con.Premise prem ->
+              (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 ->
+               P.Mtext ([],"a proof???")
+           | Con.ArgMethod s -> 
+               P.Mtext ([],"a method???")) in
+        (make_concl "we proceede by cases on" case_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 ([],case_on)])::
+          P.Mtr ([],[P.Mtd ([],to_prove)])::
+          (make_cases args_for_cases))
+
    and byinduction conclude =
      let module P = Mpresentation in
      let module Con = Content in
@@ -894,3 +934,4 @@ let content2pres ~ids_to_inner_sorts =
    (Cexpr2pres.cexpr2pres_charcount 
     (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
 ;;
+