+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
module Ref = NReference
+let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
+
+(* porcatissima *)
+type reference = Ref of 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 (u,indinfo))))
+;;
+
type ctx =
| Ce of (NCic.hypothesis * NCic.obj list) Lazy.t
| Fix of (Ref.reference * string * NCic.term) Lazy.t
| NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2
| NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) ->
aux s1 s2; aux ty1 ty2; aux t1 t2
- | NCic.Const (NReference.Ref (_,uu1,xp1)),
- NCic.Const (NReference.Ref (_,uu2,xp2)) when
- let NReference.Ref (_,u1,_) = ref in
- let NReference.Ref (_,u2,_) = ref' in
+ | NCic.Const (NReference.Ref (uu1,xp1)),
+ NCic.Const (NReference.Ref (uu2,xp2)) when
+ let NReference.Ref (u1,_) = ref in
+ let NReference.Ref (u2,_) = ref' in
NUri.eq uu1 u1 && NUri.eq uu2 u2 && xp1 = xp2
-> ()
| NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> ()
(function (ref',obj') ->
let recno, fixno =
match ref with
- NReference.Ref (_,_,NReference.Fix (fixno,recno)) -> recno,fixno
- | NReference.Ref (_,_,NReference.CoFix (fixno)) -> ~-1,fixno
+ NReference.Ref (_,NReference.Fix (fixno,recno,_)) -> recno,fixno
+ | NReference.Ref (_,NReference.CoFix (fixno)) -> ~-1,fixno
| _ -> assert false in
let recno',fixno' =
match ref' with
- NReference.Ref (_,_,NReference.Fix (fixno',recno)) -> recno,fixno'
- | NReference.Ref (_,_,NReference.CoFix (fixno')) -> ~-1,fixno'
+ NReference.Ref (_,NReference.Fix (fixno',recno,_)) -> recno,fixno'
+ | NReference.Ref (_,NReference.CoFix (fixno')) -> ~-1,fixno'
| _ -> assert false in
if recno = recno' && fixno = fixno' && same_obj ref ref' (obj,obj') then (
(*
begin
match obj, ref with
| (_,_,_,_,NCic.Fixpoint (true,fl,_)) ,
- NReference.Ref (x,y,NReference.Fix _) ->
+ NReference.Ref (y,NReference.Fix _) ->
ignore(List.fold_left (fun i (_,name,rno,_,_) ->
let ref = NReference.mk_fix i rno ref in
Hashtbl.add cache name (ref,obj);
i+1
) 0 fl)
| (_,_,_,_,NCic.Fixpoint (false,fl,_)) ,
- NReference.Ref (x,y,NReference.CoFix _) ->
+ NReference.Ref (y,NReference.CoFix _) ->
ignore(List.fold_left (fun i (_,name,rno,_,_) ->
let ref = NReference.mk_cofix i ref in
Hashtbl.add cache name (ref,obj);
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,1))
in
bctx @ [Fix (lazy (r,name,ty))],
fixpoints_ty@fixpoints,ty::tys,idx-1)
let free_decls = Lazy.force free_decls in
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
- (Ref.Fix (idx,recno+free_decls)),name,ty))
+ | `Fix (Ref.Ref (_,Ref.Fix (idx, recno,height)),name, ty) ->
+ Fix (lazy (reference_of_ouri buri
+ (Ref.Fix (idx,recno+free_decls,height)),name,ty))
| _ -> assert false) bad_bctx @ ctx
in
let n_fl = List.length fl 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,1)) 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 1))
| 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]
;;
projects / helm.git / blobdiff