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

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 46585f14c..2404fbea3 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -449,7 +449,7 @@ and proof2pres term2pres p =
     let module Con = Content in
     function
         Con.Aux n -> 
-          P.Mtext ([],"aux " ^ string_of_int n)
+          P.Mtext ([],"aux " ^ n)
       | Con.Premise prem -> 
           P.Mtext ([],"premise")
       | Con.Term t -> 
@@ -469,7 +469,7 @@ and proof2pres term2pres p =
      let inductive_arg,args_for_cases = 
        (match conclude.Con.conclude_args with
            Con.Aux(n)::_::tl ->
-             let l1,l2 = split n tl in
+             let l1,l2 = split (int_of_string n) tl in
              let last_pos = (List.length l2)-1 in
              List.nth l2 last_pos,l1
          | _ -> assert false) in
@@ -591,20 +591,22 @@ proof2pres p
 exception ToDo;;
 
 let content2pres term2pres (id,params,metasenv,obj) =
- let module Con = Content in
+ let module K = Content in
  let module P = Mpresentation in
   match obj with
-     `Def (Con.Const,thesis,`Proof p) ->
+     `Def (K.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 []
+               ("UNFINISHED PROOF" ^ id ^"(" ^
+                 String.concat " ; " (List.map UriManager.string_of_uri params)^
+                ")")])] ;
          P.Mtr []
           [P.Mtd []
             (P.Mrow []
@@ -614,11 +616,74 @@ let content2pres term2pres (id,params,metasenv,obj) =
             (P.Mrow []
               [P.Mphantom []
                 (P.Mtext [] "__") ;
-              term2pres thesis])] ;
-         P.Mtr []
+              term2pres thesis])]] @
+         (match metasenv with
+             None -> []
+           | Some metasenv' ->
+              (P.Mtr []
+                [P.Mtd []
+                  (P.Mrow []
+                    [P.Mtext [] "CONJECTURES:"])]) ::
+               List.map
+                (function
+                  (id,n,context,ty) ->
+                    P.Mtr []
+                     [P.Mtd []
+                      (P.Mrow []
+                        (List.map
+                          (function
+                              (_,None) ->
+                                P.Mrow []
+                                 [ P.Mi [] "_" ;
+                                   P.Mo [] ":?" ;
+                                   P.Mi [] "_"]
+                            | (_,Some (`Declaration d))
+                            | (_,Some (`Hypothesis d)) ->
+                               let
+                                { K.dec_name = dec_name ;
+                                  K.dec_type = ty } = d
+                                in
+                                 P.Mrow []
+                                  [ P.Mi []
+                                     (match dec_name with
+                                         None -> "_"
+                                       | Some n -> n) ;
+                                    P.Mo [] ":" ;
+                                    term2pres ty]
+                            | (_,Some (`Definition d)) ->
+                               let
+                                { K.def_name = def_name ;
+                                  K.def_term = bo } = d
+                                in
+                                 P.Mrow []
+                                  [ P.Mi []
+                                     (match def_name with
+                                         None -> "_"
+                                       | Some n -> n) ;
+                                    P.Mo [] ":=" ;
+                                    term2pres bo]
+                            | (_,Some (`Proof p)) ->
+                               let proof_name = p.K.proof_name in
+                                P.Mrow []
+                                 [ P.Mi []
+                                    (match proof_name with
+                                        None -> "_"
+                                      | Some n -> n) ;
+                                   P.Mo [] ":=" ;
+                                   proof2pres term2pres p]
+                          ) context @
+                        [ P.Mo [] "|-" ] @
+                        [ P.Mi [] (string_of_int n) ;
+                          P.Mo [] ":" ;
+                          term2pres ty ]
+                      ))
+                     ]
+                ) metasenv'
+         ) @
+        [P.Mtr []
           [P.Mtd []
             (P.Mrow []
-              [proof2pres term2pres p])]]
+              [proof2pres term2pres p])]])
    | _ -> raise ToDo
 ;;