- the mathql interpreter is not helm-dependent any more

[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..65d33f9171eedc75b8e657ef39eb419e73ffb128 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -157,29 +157,34 @@ let make_concl ?(attrs=[]) verb concl =
 let make_args_for_apply term2pres args =
  let module Con = Content in
  let module P = Mpresentation in
- let rec make_arg_for_apply is_first arg row = 
-   (match arg with 
+ let make_arg_for_apply is_first arg row = 
+  let res =
+   match arg with 
       Con.Aux n -> assert false
     | Con.Premise prem -> 
         let name = 
           (match prem.Con.premise_binder with
              None -> "previous"
            | Some s -> s) in
-        P.smallskip::P.Mi([],name)::row
+        P.Mi([],name)::row
     | Con.Lemma lemma -> 
-         P.smallskip::P.Mi([],lemma.Con.lemma_name)::row 
+         P.Mi([],lemma.Con.lemma_name)::row 
     | Con.Term t -> 
         if is_first then
           (term2pres t)::row
-        else P.smallskip::P.Mi([],"_")::row
+        else P.Mi([],"_")::row
     | Con.ArgProof _ 
     | Con.ArgMethod _ -> 
-       P.smallskip::P.Mi([],"_")::row) in
- match args with 
-   hd::tl -> 
-     make_arg_for_apply true hd 
-       (List.fold_right (make_arg_for_apply false) tl [])
- | _ -> assert false;;
+       P.Mi([],"_")::row
+  in
+   if is_first then res else P.smallskip::res
+ in
+  match args with 
+    hd::tl -> 
+      make_arg_for_apply true hd 
+        (List.fold_right (make_arg_for_apply false) tl [])
+  | _ -> assert false
+;;
 
 let rec justification term2pres p = 
   let module Con = Content in
@@ -290,9 +295,9 @@ and proof2pres term2pres p =
                 P.Mrow ([],
                   [P.Mtext([None,"mathcolor","Red"],"Suppose");
                    P.Mspace([None,"width","0.1cm"]);
-                   P.Mtext([],"(");
+                   P.Mo([],"(");
                    P.Mi ([],s);
-                   P.Mtext([],")");
+                   P.Mo([],")");
                    P.Mspace([None,"width","0.1cm"]);
                    ty])
             | None -> 
@@ -342,7 +347,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 +423,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
@@ -621,9 +631,9 @@ and proof2pres term2pres p =
                           None -> "no name"
                         | Some s -> s) in
                      P.indented (P.Mrow ([],
-                       [P.Mtext([],"(");
+                       [P.Mo([],"(");
                         P.Mi ([],name);
-                        P.Mtext([],")");
+                        P.Mo([],")");
                         P.Mspace([None,"width","0.1cm"]);
                         term2pres h.Con.dec_type]))
                    | _ -> assert false in
@@ -645,6 +655,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