X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=6dee8f04066b2a1023cb006fad016f480b0a7719;hb=cbd3ca06d7b0c8ea32cfc15b7206a940259e479e;hp=fc3a47b5e1c564fb168e1fcba94b09ccd40fa86e;hpb=c699a9669505947487dce49383fa50fe9b9968e8;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index fc3a47b5e..6dee8f040 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -929,7 +929,7 @@ let joint_def2pres term2pres def = | `Inductive ind -> inductive2pres term2pres ind | _ -> assert false (* ZACK or raise ToDo? *) -let content2pres +let content2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres (id,params,metasenv,obj) = @@ -963,7 +963,7 @@ let content2pres let name = get_name decl.Content.dec_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params); + ([B.b_h [] (B.b_kw ("axiom " ^ name) :: params2pres params); B.b_kw "Type:"; B.indent (term2pres decl.Content.dec_type)] @ metasenv2pres term2pres metasenv) @@ -976,11 +976,68 @@ let content2pres let content2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts = - content2pres ?skip_initial_lambdas ?skip_thm_and_qed + content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) annterm -> let ast, ids_to_uris = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres - (CicNotationPres.render ids_to_uris ~prec + (CicNotationPres.render + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec (TermContentPres.pp_ast ast))) + +let ncontent2pres0 + ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres + (id,params,metasenv,obj) += + match obj with + | `Def (Content.Const, thesis, `Proof p) -> + let name = get_name p.Content.proof_name in + let proof = proof2pres true term2pres ?skip_initial_lambdas p in + if skip_thm_and_qed then + proof + else + B.b_v + [Some "helm","xref","id"] + ([ B.b_h [] (B.b_kw ("ntheorem " ^ name) :: + params2pres params @ [B.b_kw ":"]); + B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @ + metasenv2pres term2pres metasenv @ + [proof ; B.b_kw "qed."]) + | `Def (_, ty, `Definition body) -> + let name = get_name body.Content.def_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] + (B.b_kw ("ndefinition " ^ name) :: params2pres params @ [B.b_kw ":"]); + B.indent (term2pres ty)] @ + metasenv2pres term2pres metasenv @ + [B.b_kw ":="; + B.indent (term2pres body.Content.def_term); + B.b_kw "."]) + | `Decl (_, `Declaration decl) + | `Decl (_, `Hypothesis decl) -> + let name = get_name decl.Content.dec_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: params2pres params); + B.b_kw "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 + +let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = + let lookup_uri id = + try + let nref = Hashtbl.find ids_to_nrefs id in + Some (NReference.string_of_reference nref) + with Not_found -> None + in + ncontent2pres0 ?skip_initial_lambdas ?skip_thm_and_qed + (fun ?(prec=90) ast -> + CicNotationPres.box_of_mpres + (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))