in
context2pres
(match skip_initial_lambdas_internal with
- Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context)
+ Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context)
| _ -> p.Con.proof_context)
presacontext
in
| `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)
=
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)
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)))