From: Stefano Zacchiroli 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 +