Inverters/Inversion:

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 88bdf4f00e620fc7194d7cfd2083a90106abefd3..1487881c1cd0dd92bbca0c23439a1bc4f18d1b66 100644 (file)
--- 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,11 @@ 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
@@ -866,3 +868,11 @@ 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
+;;