X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=225269b70fe101eaccf2ed9373c4c1a1634a0e92;hb=0ef9250d71eacd6b1022194128e6acfb74d52aac;hp=56159ffa4e91846f28785b5af4c2b5667cec0d68;hpb=28f01bb2d0e5f1b3f180b0b478267d2beb06a5fe;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 56159ffa4..225269b70 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -16,10 +16,7 @@ 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")]
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let mk_cprop n = 
@@ -46,10 +43,12 @@ let get_relevance ty =
   match CicReduction.whd context ty with
       Cic.Prod (n,s,t) ->
         not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t
-    | ty -> if is_proof_irrelevant context ty then raise InProp else []
+    | _ -> []
+ in aux [] ty
+(*    | ty -> if is_proof_irrelevant context ty then raise InProp else []
  in
    try aux [] ty
-   with InProp -> []
+   with InProp -> []*)
 ;;
 
 (* porcatissima *)
@@ -456,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
@@ -474,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 =
@@ -502,10 +501,6 @@ and height_of_term ?(h=ref 0) t =
    1 + !h
 ;;
 
-(* we are lambda-lifting also variables that do not occur *)
-(* ctx does not distinguish successive blocks of cofix, since there may be no
- *   lambda separating them *)
-let convert_term uri t = 
   (* k=true if we are converting a term to be pushed in a ctx or if we are
             converting the type of a fix;
      k=false if we are converting a term to be put in the body of a fix;
@@ -763,7 +758,12 @@ let convert_term uri t =
        match ens with
           [] -> he,objs
         | _::_ -> NCic.Appl (he::ens),objs
-  in
+;;
+
+(* we are lambda-lifting also variables that do not occur *)
+(* ctx does not distinguish successive blocks of cofix, since there may be no
+ *   lambda separating them *)
+let convert_term uri t = 
    aux false [] [] 0 uri t
 ;;
 
@@ -841,3 +841,38 @@ let convert_obj uri obj =
 (*prerr_endline ("H(" ^ UriManager.string_of_uri uri ^ ") = " ^ string_of_int * (get_height uri));*)
   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
+    (function 
+    | (Some (s, Cic.Decl t) as e) -> fun (nc,auxc,oc) ->
+       let t, _ = aux true oc auxc 0 uri t in
+       (name_of s, NCic.Decl t) :: nc, 
+       Ce (lazy ((name_of s, NCic.Decl t),[])) :: auxc,  e :: oc
+    | (Some (Cic.Name s, Cic.Def (t,ty)) as e) -> fun (nc,auxc,oc) ->
+       let t, _ = aux true oc auxc 0 uri t in
+       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 -> 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
+;;