- ng_refiner:

[helm.git] / matita / components / ng_cic_content / interpretations.ml

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index ee4bb9437ca5a5002f3f2587768b29a03ac2e239..e2c8c76d0c53a4286b8fca9643507f00dacbcc69 100644 (file)
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -305,6 +305,7 @@ let nast_of_cic0 status
                  [arg] -> idref (k ~context arg)
                | _ -> idref (Ast.Appl (List.map (k ~context) args))))
     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
+       (try
         let name = NUri.name_of_uri uri in
 (* CSC
         let uri_str = UriManager.string_of_uri uri in
@@ -351,6 +352,12 @@ let nast_of_cic0 status
           | `Term -> Some case_indty
         in
          idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
+     with
+      NCicEnvironment.ObjectNotFound msg ->
+       idref (Ast.Case(k ~context te,Some ("NOT_FOUND: " ^ Lazy.force msg,None),
+       Some (k ~context outty),
+       (List.map (fun t -> Ast.Pattern ("????", None, []), k ~context t)
+         patterns))))
 ;;
 
 let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
@@ -502,7 +509,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 +594,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 +604,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, attrs) ->
+        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 (n, ty, xbo, attrs)
+      | 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