fixed Whelp stuff

[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 29da14591e9fd6946f1e0062412ece9457985288..fdffe82760b840622a2f33829903e7d13abee456 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -186,6 +186,10 @@ let make_args_for_apply term2pres args =
   | _ -> assert false
 ;;
 
+let get_name = function
+  | Some s -> s
+  | None -> "_"
+
 let rec justification term2pres p = 
   let module Con = Content in
   let module P = Mpresentation in
@@ -257,7 +261,7 @@ and proof2pres term2pres p =
              [B.H([Some "helm", "xref", "ce_"^hd_xref],
                [ce2pres hd]);
              continuation'])
-         
+        
   and ce2pres =
     let module Con = Content in
       function
@@ -300,8 +304,10 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Joint ho -> 
-            B.Text ([],"jointdef")
+      | `Joint ho -> assert false (*
+        B.H ([],
+        (B.Text ([],"JOINT ")
+        :: List.map ce2pres ho.Content.joint_defs)) *)
 
   and acontext2pres ac continuation indent =
     let module Con = Content in
@@ -376,7 +382,11 @@ and proof2pres term2pres p =
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
-         | _ -> assert false) in
+         | [Con.Premise p] -> 
+             (match p.Con.premise_binder with
+             | None -> assert false; (* unnamed hypothesis ??? *)
+             | Some s -> B.Text([],s))
+         | err -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
           B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
@@ -820,24 +830,59 @@ let metasenv2pres term2pres = function
              (let _ = incr counter; in (string_of_int !counter)))) ::
          (List.map (conjecture2pres term2pres) metasenv'))]
 
-let get_name = function
-  | Some s -> s
-  | None -> "_"
+let params2pres params =
+  let param2pres uri =
+    B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
+      (UriManager.name_of_uri uri)
+  in
+  let rec spatiate = function
+    | [] -> []
+    | hd :: [] -> [hd]
+    | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
+  in
+  match params with
+  | [] -> []
+  | p ->
+      let params = spatiate (List.map param2pres p) in
+      [B.b_space;
+       B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
+
+let recursion_kind2pres params kind =
+  let kind =
+    match kind with
+    | `Recursive _ -> "Recursive definition"
+    | `CoRecursive -> "CoRecursive definition"
+    | `Inductive _ -> "Inductive definition"
+    | `CoInductive _ -> "CoInductive definition"
+  in
+  B.b_h [] (B.b_text [] kind :: params2pres params)
+
+let inductive2pres term2pres ind =
+  let constructor2pres decl =
+    B.b_h [] [
+      B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
+      B.b_space;
+      term2pres decl.Content.dec_type
+    ]
+  in
+  B.b_v []
+    (B.b_h [] [
+      B.b_text [] (ind.Content.inductive_name ^ " of arity ");
+      term2pres ind.Content.inductive_type ]
+    :: List.map constructor2pres ind.Content.inductive_constructors)
 
-let pp_params = function
-  | [] -> ""
-  | params ->
-      " (" ^
-      String.concat " ; " (List.map UriManager.string_of_uri params) ^
-      ")"
+let joint_def2pres term2pres def =
+  match def with
+  | `Inductive ind -> inductive2pres term2pres ind
+  | _ -> assert false (* ZACK or raise ToDo? *)
 
 let content2pres term2pres (id,params,metasenv,obj) =
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->
       let name = get_name p.Content.proof_name in
       B.b_v
-        [None,"helm:xref","id"]
-        ([ B.b_text [] ("Proof " ^ name ^ pp_params params);
+        [Some "helm","xref","id"]
+        ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params);
            B.b_text [] "Thesis:";
            B.indent (term2pres thesis) ] @
          metasenv2pres term2pres metasenv @
@@ -845,8 +890,8 @@ let content2pres term2pres (id,params,metasenv,obj) =
   | `Def (_, ty, `Definition body) ->
       let name = get_name body.Content.def_name in
       B.b_v
-        [None,"helm:xref","id"]
-        ([B.b_text [] ("Definition " ^ name ^ pp_params params);
+        [Some "helm","xref","id"]
+        ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params);
           B.b_text [] "Type:";
           B.indent (term2pres ty)] @
           metasenv2pres term2pres metasenv @
@@ -855,11 +900,15 @@ let content2pres term2pres (id,params,metasenv,obj) =
   | `Decl (_, `Hypothesis decl) ->
       let name = get_name decl.Content.dec_name in
       B.b_v
-        [None,"helm:xref","id"]
-        ([B.b_text [] ("Axiom " ^ name ^ pp_params params);
+        [Some "helm","xref","id"]
+        ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params);
           B.b_text [] "Type:";
           B.indent (term2pres decl.Content.dec_type)] @
           metasenv2pres term2pres metasenv)
+  | `Joint joint ->
+      B.b_v []
+        (recursion_kind2pres params joint.Content.joint_kind
+        :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
   | _ -> raise ToDo
 ;;