let splat_args ctx t n_fix =
let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in
- let rec aux = function
- | 0 -> []
- | n ->
- (match List.nth ctx (n-1) with
- | Ce _ when n <= bound -> NCic.Rel n
- | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
- splat_args_for_rel ctx (NCic.Const refe)
- | Fix _ | Ce _ -> NCic.Rel (n - n_fix)
- ) :: aux (n-1)
- in
- NCic.Appl (t:: aux (List.length ctx))
+ if ctx = [] then t
+ else
+ let rec aux = function
+ | 0 -> []
+ | n ->
+ (match List.nth ctx (n-1) with
+ | Ce _ when n <= bound -> NCic.Rel n
+ | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
+ splat_args_for_rel ctx (NCic.Const refe)
+ | Fix _ | Ce _ -> NCic.Rel (n - n_fix)
+ ) :: aux (n-1)
+ in
+ NCic.Appl (t:: aux (List.length ctx))
;;
(* we are lambda-lifting also variables that do not occur *)
(fun (name,ty,_) (ctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
let r = NReference.reference_of_ouri buri(NReference.CoFix idx) in
- ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1)
+ Fix (r,name,ty) :: ctx, fixpoints_ty @ fixpoints,ty::tys,idx+1)
fl ([], [], [], 0)
in
let bctx = bctx @ ctx in
let r =
NReference.reference_of_ouri buri (NReference.Fix (idx,recno))
in
- ctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx+1)
+ Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
fl ([], [], [], 0)
in
let bctx = bctx @ ctx in
let octx = Some (name, Cic.Decl old_s) :: octx in
let t, fixpoints_t = aux octx ctx n_fix uri t in
NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t
- | Cic.LetIn (name, (s as old_s), t) ->
- let s, fixpoints_s = aux octx ctx n_fix uri s in
- let old_ty,_ =
- CicTypeChecker.type_of_aux' [] octx old_s CicUniv.oblivion_ugraph
- in
- let ty, fixpoints_ty = aux octx ctx n_fix uri old_ty in
- let ctx = Ce (cn_to_s name, NCic.Def (s, ty)) :: ctx in
- let octx = Some (name, Cic.Def (old_s, Some old_ty)) :: octx in
+ | Cic.LetIn (name, (te as old_te), (ty as old_ty), t) ->
+ let te, fixpoints_s = aux octx ctx n_fix uri te in
+ let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
+ let ctx = Ce (cn_to_s name, NCic.Def (te, ty)) :: ctx in
+ let octx = Some (name, Cic.Def (old_te, old_ty)) :: octx in
let t, fixpoints_t = aux octx ctx n_fix uri t in
- NCic.LetIn (cn_to_s name, ty, s, t),
+ NCic.LetIn (cn_to_s name, ty, te, t),
fixpoints_s @ fixpoints_t @ fixpoints_ty
| Cic.Cast (t,ty) ->
let t, fixpoints_t = aux octx ctx n_fix uri t in
let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
| Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
- | Cic.Sort Cic.Set -> NCic.Sort NCic.Set,[]
| Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
| Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[]
+ | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[]
(* calculate depth in the univ_graph*)
| Cic.Appl l ->
let l, fixpoints =
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
;;