+(*
+ ||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 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) ->
- aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)))
+ let is_inductive =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ Cic.InductiveDefinition ([],_,_,_) -> true
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ | _ -> assert false
+ in
+ aux_ens k curi octx ctx n_fix uri ens
+ (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,_,_,_) ->
aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
| _ -> assert false)
| Cic.MutCase (curi, tyno, outty, t, branches) ->
- let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in
+ let is_inductive =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ Cic.InductiveDefinition ([],_,_,_) -> true
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ | _ -> assert false 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]
;;