content2pres for the new cic fixed

[helm.git] / helm / software / components / content_pres / content2pres.ml

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 4d5ec86f5aff02446e9d0b6d44c6278b48991039..6dee8f04066b2a1023cb006fad016f480b0a7719 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -183,7 +183,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
         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
@@ -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)))