let rno = ref 0 in
let bctx, fixpoints_tys, tys, _ =
List.fold_right
- (fun (name,recno,ty,_) (ctx, fixpoints, tys, idx) ->
+ (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
if idx = k then rno := recno;
let r =
NReference.reference_of_ouri buri (NReference.Fix (idx,recno))
in
- Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
+ Fix (r,name,ty) :: bctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
fl ([], [], [], 0)
in
let bctx = bctx @ ctx in
assert(fixpoints_ty = []);
NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
fixpoints_bo @ fixpoints_ty
- | Cic.InductiveDefinition (_,_,_,_) -> assert false (*
+ | Cic.InductiveDefinition (itl,_,leftno,_) ->
let ind = let _,x,_,_ = List.hd itl in x in
- let itl =
- List.map
- (fun name, _, ty, cl ->
- [], name, convert_term ty,
- List.map (fun name, ty -> [], name, convert_term ty) cl)
- itl
+ let itl, fix_itl =
+ List.fold_right
+ (fun (name, _, ty, cl) (itl,acc) ->
+ let ty, fix_ty = convert_term uri ty in
+ let cl, fix_cl =
+ List.fold_right
+ (fun (name, ty) (cl,acc) ->
+ let ty, fix_ty = convert_term uri ty in
+ ([], name, ty)::cl, acc @ fix_ty)
+ cl ([],[])
+ in
+ ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
+ itl ([],[])
in
- NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) *)
+ NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)),
+ fix_itl
| Cic.Variable _
| Cic.CurrentProof _ -> assert false
;;