- selection attribute of maction is now explicitly generated

[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 c2d10e5199818b524612a44064e41496269dc01e..9356c288540066c7b207c4d02d75ba539866954e 100644 (file)
--- 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 
@@ -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,7 +183,7 @@ 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 = 
@@ -215,7 +215,8 @@ and proof2pres term2pres p =
                None -> P.Mtext([],"NO PROOF!!!")
              | Some c -> c) in 
           let action = 
-            P.Maction([None,"actiontype","toggle"],
+            P.Maction([None,"actiontype","toggle" ;
+                       None,"selection","1"],
               [(make_concl "proof of" ac);
                 body]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
@@ -239,7 +240,7 @@ and proof2pres term2pres p =
 
   and ce2pres =
     let module P = Mpresentation in
-    let module Con = Cic2content in
+    let module Con = Content in
       function
         `Declaration d -> 
           (match d.Con.dec_name with
@@ -322,7 +323,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,10 +447,10 @@ 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)
+          P.Mtext ([],"aux " ^ n)
       | Con.Premise prem -> 
           P.Mtext ([],"premise")
       | Con.Term t -> 
@@ -461,7 +462,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???")
@@ -469,7 +470,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
@@ -507,7 +508,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 =
@@ -591,20 +592,22 @@ proof2pres p
 exception ToDo;;
 
 let content2pres term2pres (id,params,metasenv,obj) =
- let module Con = Cic2content 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 +617,83 @@ 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 []
+                  (* Conjectures are in their own table to make *)
+                  (* diffing the DOM trees easier.              *)
+                  (P.Mtable
+                    [None,"align","baseline 1";
+                     None,"equalrows","false";
+                     None,"columnalign","left"]
+                   ((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
 ;;