+(*
+ ||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
| `Ce ((_, NCic.Def _),_) -> aux (n-1,tl))
| _,_ -> assert false
in
- NCic.Appl (t:: aux (List.length ctx,rels))
+ let args = aux (List.length ctx,rels) in
+ match args with
+ [] -> t
+ | _::_ -> NCic.Appl (t::args)
;;
let splat_args ctx t n_fix rels =
)
| _,_ -> assert false
in
- NCic.Appl (t:: aux ((List.length ctx,rels)))
+ let args = aux (List.length ctx,rels) in
+ match args with
+ [] -> t
+ | _::_ -> NCic.Appl (t::args)
;;
exception Nothing_to_do;;
let cache = Hashtbl.create 313;;
let same_obj ref ref' =
function
- | (_,_,_,_,NCic.Fixpoint (_,l1,_)), (_,_,_,_,NCic.Fixpoint (_,l2,_))
+ | (_,_,_,_,NCic.Fixpoint (b1,l1,_)), (_,_,_,_,NCic.Fixpoint (b2,l2,_))
when List.for_all2 (fun (_,_,_,ty1,bo1) (_,_,_,ty2,bo2) ->
- alpha ty1 ty2 ref ref' && alpha bo1 bo2 ref ref') l1 l2 ->
+ alpha ty1 ty2 ref ref' && alpha bo1 bo2 ref ref') l1 l2 && b1=b2->
true
| _ -> false
;;
let recno, fixno =
match ref with
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'
| _ -> assert false in
if recno = recno' && fixno = fixno' && same_obj ref ref' (obj,obj') then (
(*
(* prerr_endline "<<< CACHE MISS >>>"; *)
begin
match obj, ref with
- | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , NReference.Ref (x,y,NReference.Fix _) ->
+ | (_,_,_,_,NCic.Fixpoint (true,fl,_)) ,
+ NReference.Ref (x,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 _) ->
+ ignore(List.fold_left (fun i (_,name,rno,_,_) ->
+ let ref = NReference.mk_cofix i ref in
+ Hashtbl.add cache name (ref,obj);
+ i+1
+ ) 0 fl)
| _ -> assert false
end;
None
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
- splat_args ctx
- (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix cofixno)))
- n_fix rels,
- fixpoints @ [obj]
+ 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
+ Some r' -> [],r'
+ | None -> [obj],r
+ in
+ splat_args ctx (NCic.Const r) n_fix rels, fixpoints @ obj
| Cic.Fix _ as fix ->
let octx,ctx,fix,rels = restrict octx ctx fix in
let fixno,fl =
(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]
;;
projects / helm.git / blobdiff