X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=46585f14cd80c1036782f580c649f10ac5939de7;hb=43f61eedd2a1f499166de33a98af00b767dcc117;hp=5d6923237e0b73ad25800f92edea881365d9f6bf;hpb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 5d6923237..46585f14c 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -42,7 +42,7 @@ let rec split n l =
 
 let is_big_general countterm p =
   let maxsize = Cexpr2pres.maxsize in
-  let module Con = Cic2content in
+  let module Con = Content in
   let rec countp current_size p =
     if current_size > maxsize then current_size
     else 
@@ -62,23 +62,23 @@ let is_big_general countterm p =
       if current_size > maxsize then maxsize
       else 
         (match e with
-          Con.Declaration d -> 
+          `Declaration d -> 
             (match d.Con.dec_name with
                Some s -> current_size + 4 + (String.length s)
              | None -> prerr_endline "NO NAME!!"; assert false)
-        | Con.Hypothesis h ->
+        | `Hypothesis h ->
             (match h.Con.dec_name with
                 Some s -> current_size + 4 + (String.length s)
               | None -> prerr_endline "NO NAME!!"; assert false) 
-        | Con.Proof p -> countp current_size p
-        | Con.Definition d -> 
+        | `Proof p -> countp current_size p
+        | `Definition d -> 
             (match d.Con.def_name with
                 Some s -> 
                   let c1 = (current_size + 4 + (String.length s)) in
                   (countterm c1 d.Con.def_term)
               | None -> 
                   prerr_endline "NO NAME!!"; assert false) 
-        | Con.Joint ho -> maxsize + 1) (* we assume is big *)
+        | `Joint ho -> maxsize + 1) (* we assume is big *)
   and 
     countapplycontext current_size ac =
       List.fold_left countp current_size ac
@@ -143,7 +143,7 @@ let make_concl verb concl =
 ;;
 
 let make_args_for_apply term2pres args =
- let module Con = Cic2content in
+ let module Con = Content in
  let module P = Mpresentation in
  let rec make_arg_for_apply is_first arg row = 
    (match arg with 
@@ -168,7 +168,7 @@ let make_args_for_apply term2pres args =
  | _ -> assert false;;
 
 let rec justification term2pres p = 
-  let module Con = Cic2content in
+  let module Con = Content in
   let module P = Mpresentation in
   if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
      ((p.Con.proof_context = []) &
@@ -183,13 +183,13 @@ let rec justification term2pres p =
      
 and proof2pres term2pres p =
   let rec proof2pres p =
-    let module Con = Cic2content in
+    let module Con = Content in
     let module P = Mpresentation in
       let indent = 
         let is_decl e = 
           (match e with 
-             Con.Declaration _
-           | Con.Hypothesis _ -> true
+             `Declaration _
+           | `Hypothesis _ -> true
            | _ -> false) in
         ((List.filter is_decl p.Con.proof_context) != []) in 
       let concl = 
@@ -239,9 +239,9 @@ and proof2pres term2pres p =
 
   and ce2pres =
     let module P = Mpresentation in
-    let module Con = Cic2content in
+    let module Con = Content in
       function
-        Con.Declaration d -> 
+        `Declaration d -> 
           (match d.Con.dec_name with
               Some s ->
                 let ty = term2pres d.Con.dec_type in
@@ -253,7 +253,7 @@ and proof2pres term2pres p =
                    ty])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false)
-      | Con.Hypothesis h ->
+      | `Hypothesis h ->
           (match h.Con.dec_name with
               Some s ->
                 let ty = term2pres h.Con.dec_type in
@@ -267,8 +267,8 @@ and proof2pres term2pres p =
                    ty])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | Con.Proof p -> proof2pres p
-      | Con.Definition d -> 
+      | `Proof p -> proof2pres p
+      | `Definition d -> 
            (match d.Con.def_name with
               Some s ->
                 let term = term2pres d.Con.def_term in
@@ -279,7 +279,7 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | Con.Joint ho -> 
+      | `Joint ho -> 
             P.Mtext ([],"jointdef")
 
   and acontext2pres ac continuation indent =
@@ -322,7 +322,7 @@ and proof2pres term2pres p =
         [P.Mtd ([], conclude_aux conclude)])
 
   and conclude_aux conclude =
-    let module Con = Cic2content in
+    let module Con = Content in
     let module P = Mpresentation in
     if conclude.Con.conclude_method = "TD_Conversion" then
       let expected = 
@@ -446,7 +446,7 @@ and proof2pres term2pres p =
 
   and arg2pres =
     let module P = Mpresentation in
-    let module Con = Cic2content in
+    let module Con = Content in
     function
         Con.Aux n -> 
           P.Mtext ([],"aux " ^ string_of_int n)
@@ -461,7 +461,7 @@ and proof2pres term2pres p =
  
    and byinduction conclude =
      let module P = Mpresentation in
-     let module Con = Cic2content in
+     let module Con = Content in
      let proof_conclusion = 
        (match conclude.Con.conclude_conclusion with
           None -> P.Mtext([],"No conclusion???")
@@ -507,7 +507,7 @@ and proof2pres term2pres p =
 
     and make_case =  
       let module P = Mpresentation in
-      let module Con = Cic2content in
+      let module Con = Content in
       function 
         Con.ArgProof p ->
           let name =
@@ -517,15 +517,15 @@ and proof2pres term2pres p =
           let indhyps,args =
              List.partition 
                (function
-                   Con.Hypothesis h -> h.Con.dec_inductive
+                   `Hypothesis h -> h.Con.dec_inductive
                  | _ -> false) p.Con.proof_context in
           let pattern_aux =
              List.fold_right
                (fun e p -> 
                   let dec  = 
                     (match e with 
-                       Con.Declaration h 
-                     | Con.Hypothesis h -> 
+                       `Declaration h 
+                     | `Hypothesis h -> 
                          let name = 
                            (match h.Con.dec_name with
                               None -> "NO NAME???"
@@ -557,7 +557,7 @@ and proof2pres term2pres p =
                  (P.Mtext([],"by induction hypothesis we know:")))]) in
                let make_hyp =
                  function 
-                   Con.Hypothesis h ->
+                   `Hypothesis h ->
                      let name = 
                        (match h.Con.dec_name with
                           None -> "no name"
@@ -588,11 +588,43 @@ and proof2pres term2pres p =
 proof2pres p
 ;;
 
-(*  
-let content2pres = 
-  proof2pres 
-    (function p -> Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr p))
-;; *)
-
+exception ToDo;;
 
+let content2pres term2pres (id,params,metasenv,obj) =
+ let module Con = Content in
+ let module P = Mpresentation in
+  match obj with
+     `Def (Con.Const,thesis,`Proof p) ->
+       P.Mtable
+        [None,"align","baseline 1";
+         None,"equalrows","false";
+         None,"columnalign","left";
+         None,"helm:xref","id"]
+        [(*P.Mtr []
+         [P.Mtd []
+           (P.Mrow []
+             [P.Mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ params ^ ")")])] ;
+*)
+         P.Mtr []
+          [P.Mtd []
+            (P.Mrow []
+              [P.Mtext [] "THESIS:"])] ;
+         P.Mtr []
+          [P.Mtd []
+            (P.Mrow []
+              [P.Mphantom []
+                (P.Mtext [] "__") ;
+              term2pres thesis])] ;
+         P.Mtr []
+          [P.Mtd []
+            (P.Mrow []
+              [proof2pres term2pres p])]]
+   | _ -> raise ToDo
+;;
 
+let content2pres ~ids_to_inner_sorts =
+ content2pres 
+  (function p -> 
+   (Cexpr2pres.cexpr2pres_charcount 
+    (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
+;;