From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 2 Feb 2005 14:12:24 +0000 (+0000)
Subject: - implemented inductive type rendering
X-Git-Tag: V_0_1_0~63
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=600584314336cb13922438d1e6bcf6044314db72;p=helm.git

- implemented inductive type rendering
- added hyperlinks on parameters
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 29da14591..ef79ab4ad 100644
--- 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
@@ -820,24 +824,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 +884,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 +894,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
 ;;
 
diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli
index 99a690f7f..369b06b3e 100644
--- a/helm/ocaml/cic_transformations/content2pres.mli
+++ b/helm/ocaml/cic_transformations/content2pres.mli
@@ -35,3 +35,4 @@
 val content2pres :
  ids_to_inner_sorts:(Cic.id, string) Hashtbl.t ->
   Cic.annterm Content.cobj -> Mpresentation.mpres Box.box
+