From ff3a27b1cbb969303ece080ef78cf53354545e5e Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 5 Apr 2011 20:30:48 +0000
Subject: [PATCH] we added an nmap from NCic.obj to NotationPt.obj (to be
 continued)

---
 .../ng_cic_content/interpretations.ml         | 52 ++++++++++++++++++-
 .../ng_cic_content/interpretations.mli        |  7 ++-
 matita/matita/applyTransformation.ml          |  2 +-
 3 files changed, 57 insertions(+), 4 deletions(-)

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index ee4bb9437..84638ad6d 100644
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -502,7 +502,7 @@ let build_decl_item seed id n s =
       }
 ;;
 
-let nmap_obj0 status ~idref (uri,_,metasenv,subst,kind) =
+let nmap_cobj0 status ~idref (uri,_,metasenv,subst,kind) =
   let module K = Content in
   let nast_of_cic =
    nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
@@ -587,7 +587,7 @@ let with_idrefs foo status obj =
   foo status ~idref:(idref register_ref) obj, ids_to_refs
 ;;
 
-let nmap_obj status = with_idrefs nmap_obj0 status
+let nmap_cobj status = with_idrefs nmap_cobj0 status
 
 let nmap_sequent status ~metasenv ~subst =
  with_idrefs (nmap_sequent0 ~metasenv ~subst) status
@@ -597,3 +597,51 @@ let nmap_term status ~metasenv ~subst ~context =
 
 let nmap_context status ~metasenv ~subst =
  with_idrefs (nmap_context0 ~metasenv ~subst) status
+
+(* FG ***********************************************************************)
+
+let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) =
+   let module N = NotationPt in
+   let nast_of_cic =
+      nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst
+   in
+   let rec mk_captures lno k c u = match lno, u with
+      | 0, _                                -> k, c
+      | _, NCic.Prod (n, w, u) when lno > 0 ->
+         let cap = nast_of_cic ~context:c w, None in
+	 let hyp = n, NCic.Decl w in
+	 mk_captures (pred lno) (cap :: k) (hyp :: c) u
+      | _                                 -> assert false
+   in
+   let build_captures lno = function
+      | []                -> [], []
+      | (_, _, u, _) :: _ -> mk_captures lno [] [] u
+   in
+   let rec eat_prods prods lno t = match prods, lno, t with
+      | _, 0, _                                      -> t
+      | true, _, NCic.Prod (_, _, t) when lno > 0    -> eat_prods prods (pred lno) t
+      | false, _, NCic.Lambda (_, _, t) when lno > 0 -> eat_prods prods (pred lno) t
+      | _                                            -> assert false
+   in
+   let build_constractor lno context (_, n, bo) =
+      let bo = nast_of_cic ~context (eat_prods false lno bo) in      
+      n, bo
+   in
+   let build_inductive is_ind lno context (_, n, ty, cl) =
+      let ty = nast_of_cic ~context (eat_prods true lno ty) in
+      n, is_ind, ty, List.map (build_constractor lno context) cl
+   in
+   match kind with
+      | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+	 let ty = nast_of_cic ~context:[] ty in
+         let xbo = match xbo with 
+	    | Some bo -> Some (nast_of_cic ~context:[] bo)
+	    | None    -> None
+	 in
+	 N.Theorem (flavour, n, ty, xbo, pragma)
+      | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->      
+         let captures, context = build_captures lno itl in
+	 N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
+      | _ -> assert false  (* NCic.Fixpoint (is_rec, ifl, _) -> *)
+
+let nmap_obj status = with_idrefs nmap_obj0 status
diff --git a/matita/components/ng_cic_content/interpretations.mli b/matita/components/ng_cic_content/interpretations.mli
index 71732cc7d..0eb294b76 100644
--- a/matita/components/ng_cic_content/interpretations.mli
+++ b/matita/components/ng_cic_content/interpretations.mli
@@ -95,7 +95,12 @@ val nmap_sequent:
    NotationPt.term Content.conjecture *
     (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
 
-val nmap_obj:
+val nmap_cobj:
  #status -> NCic.obj ->
   NotationPt.term Content.cobj *
    (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
+
+val nmap_obj:
+ #status -> NCic.obj ->
+  NotationPt.term NotationPt.obj *
+   (Content.id, NReference.reference) Hashtbl.t    (* id -> reference *)
diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml
index 51ac81268..705ef7936 100644
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -53,7 +53,7 @@ let ntxt_of_cic_sequent ~metasenv ~subst =
   (fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq])
 
 let ntxt_of_cic_object ~map_unicode_to_tex =
- to_text Interpretations.nmap_obj Content2pres.nobj2pres ~map_unicode_to_tex
+ to_text Interpretations.nmap_cobj Content2pres.nobj2pres ~map_unicode_to_tex
   (new NCicPp.status)#ppobj
 
 let ntxt_of_cic_term ~metasenv ~subst ~context =
-- 
2.39.2