module Ref = NReference
+let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
+
+(* porcatissima *)
+type reference = Ref of int * NUri.uri * NReference.spec
+let reference_of_ouri u indinfo =
+ let u = nuri_of_ouri u in
+ NReference.reference_of_string
+ (NReference.string_of_reference (Obj.magic (Ref (max_int,u,indinfo))))
+;;
+
type ctx =
| Ce of (NCic.hypothesis * NCic.obj list) Lazy.t
| Fix of (Ref.reference * string * NCic.term) Lazy.t
List.fold_right
(fun (name,ty,_) (bctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in
- let r = Ref.reference_of_ouri buri(Ref.CoFix idx) in
+ let r = reference_of_ouri buri(Ref.CoFix idx) in
bctx @ [Fix (lazy (r,name,ty))],
fixpoints_ty @ fixpoints,ty::tys,idx-1)
fl ([], [], [], List.length fl-1)
fl tys ([],fixpoints_tys)
in
let obj =
- NUri.nuri_of_ouri buri,0,[],[],
+ nuri_of_ouri buri,0,[],[],
NCic.Fixpoint (false, fl, (`Generated, `Definition))
in
- let r = Ref.reference_of_ouri buri (Ref.CoFix cofixno) in
+ let r = reference_of_ouri buri (Ref.CoFix cofixno) in
let obj,r =
let _,name,_,_,_ = List.nth fl cofixno in
match find_in_cache name obj r with
(fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in
let r = (* recno is dummy here, must be lifted by the ctx len *)
- Ref.reference_of_ouri buri (Ref.Fix (idx,recno))
+ reference_of_ouri buri (Ref.Fix (idx,recno))
in
bctx @ [Fix (lazy (r,name,ty))],
fixpoints_ty@fixpoints,ty::tys,idx-1)
let bctx =
List.map (function ce -> match strictify ce with
| `Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) ->
- Fix (lazy (Ref.reference_of_ouri buri
+ Fix (lazy (reference_of_ouri buri
(Ref.Fix (idx,recno+free_decls)),name,ty))
| _ -> assert false) bad_bctx @ ctx
in
fl tys ([],fixpoints_tys,0)
in
let obj =
- NUri.nuri_of_ouri buri,max_int,[],[],
+ nuri_of_ouri buri,max_int,[],[],
NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
- let r = Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in
+ let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in
let obj,r =
let _,name,_,_,_ = List.nth fl fixno in
match find_in_cache name obj r with
aux_ens k curi octx ctx n_fix uri ens
(match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
| Cic.Constant (_,Some _,_,_,_) ->
- NCic.Const (Ref.reference_of_ouri curi Ref.Def)
+ NCic.Const (reference_of_ouri curi Ref.Def)
| Cic.Constant (_,None,_,_,_) ->
- NCic.Const (Ref.reference_of_ouri curi Ref.Decl)
+ NCic.Const (reference_of_ouri curi Ref.Decl)
| _ -> assert false)
| Cic.MutInd (curi, tyno, ens) ->
let is_inductive =
| _ -> assert false
in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
| Cic.MutConstruct (curi, tyno, consno, ens) ->
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
| Cic.Var (curi, ens) ->
(match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
Cic.Variable (_,Some bo,_,_,_) ->
Cic.InductiveDefinition ([],_,_,_) -> true
| Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
| _ -> assert false in
- let r = Ref.reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+ let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
let t, fixpoints_t = aux k octx ctx n_fix uri t in
let branches, fixpoints =
let convert_obj uri obj =
reset_seed ();
let o, fixpoints = convert_obj_aux uri obj in
- let obj = NUri.nuri_of_ouri uri,max_int, [], [], o in
+ let obj = nuri_of_ouri uri,max_int, [], [], o in
fixpoints @ [obj]
;;