X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=1487881c1cd0dd92bbca0c23439a1bc4f18d1b66;hb=7b112b0cd39c5ab0db5c28636c0a7f7e36b4d6e2;hp=0854b624f157aa486fd8aae0f67f2eadd7bb9389;hpb=5061952d0632ba8bc77be5cab11fab2f36e1e26f;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0854b624f..1487881c1 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -16,17 +16,14 @@ module Ref = NReference
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
 let mk_type n = 
-  if n = 0 then
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
-  else
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let is_proof_irrelevant context ty =
@@ -458,11 +455,11 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
  with Found ref -> Some ref
 ;;
 
+let cache1 = UriManager.UriHashtbl.create 313;;
 let rec get_height =
- let cache = UriManager.UriHashtbl.create 313 in
    function u ->
      try
-       UriManager.UriHashtbl.find cache u
+       UriManager.UriHashtbl.find cache1 u
      with
       Not_found ->
         let h = ref 0 in
@@ -476,7 +473,7 @@ let rec get_height =
                1 + !h
            | _ -> 0
          in
-           UriManager.UriHashtbl.add cache u res;
+           UriManager.UriHashtbl.add cache1 u res;
            res
 and height_of_term ?(h=ref 0) t =
  let rec aux =
@@ -549,7 +546,7 @@ and height_of_term ?(h=ref 0) t =
         in
         let obj = 
           nuri_of_ouri buri,0,[],[],
-            NCic.Fixpoint (false, fl, (`Generated, `Definition)) 
+            NCic.Fixpoint (false, fl, (`Generated, `Definition, `Regular))
         in
         let r = reference_of_ouri buri (Ref.CoFix cofixno) in
         let obj,r =
@@ -610,7 +607,7 @@ and height_of_term ?(h=ref 0) t =
         in
         let obj = 
           nuri_of_ouri buri,height,[],[],
-            NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
+            NCic.Fixpoint (true, fl, (`Generated, `Definition, `Regular)) in
 (*prerr_endline ("H(" ^ UriManager.string_of_uri buri ^ ") = " ^ string_of_int * height);*)
         let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,height)) in
         let obj,r =
@@ -845,6 +842,12 @@ let convert_obj uri obj =
   fixpoints @ [obj]
 ;;
 
+let clear () =
+  Hashtbl.clear cache;
+  UriManager.UriHashtbl.clear cache1
+;;
+
+(*
 let convert_context uri =
   let name_of = function Cic.Name s -> s | _ -> "_" in
   List.fold_right
@@ -858,9 +861,18 @@ let convert_context uri =
        let t, _ = aux true oc auxc 0 uri ty in
        (name_of s, NCic.Def (t,ty)) :: nc, 
        Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc,  e :: oc
-    | None -> ...
+    | None -> nc, , e :: oc
 ;;
 
 let convert_term uri ctx t = 
    aux false [] [] 0 uri t
 ;;
+*)
+
+let reference_of_oxuri u =
+ let t = CicUtil.term_of_uri u in
+ let t',l = convert_term (UriManager.uri_of_string "cic:/dummy/dummy.con") t in
+  match t',l with
+     NCic.Const nref, [] -> nref
+   | _,_ -> assert false
+;;