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 =
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
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 =
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;
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
;;
(*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
+;;