From 89d18c9a7d02ba3a26581a2d1c0f50bb56f231e2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 9 Apr 2008 12:19:06 +0000 Subject: [PATCH] Grave bug fixed: Ce that point to definitions were handled as those that point to declarations. So Fix-constants were too much abstracted, too much applied, etc. --- .../components/ng_kernel/oCic2NCic.ml | 37 ++++++++++++------- 1 file changed, 23 insertions(+), 14 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 5b4d9f9e1..c3a6558c2 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -25,38 +25,46 @@ let context_tassonomy ctx = let rec split inner acc acc1 = function | Ce _ :: tl when inner -> split inner (acc+1) (acc1+1) tl | Fix _ ::tl -> split false acc (acc1+1) tl - | _ as l -> acc, List.length l, acc1 + | _ as l -> + let only_decl = + List.filter (function Ce (_, NCic.Decl _) | Fix _ -> true | _ -> false) + l + in + acc, List.length l, List.length only_decl, acc1 in split true 0 1 ctx ;; let splat_args_for_rel ctx t = - let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in + let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in if free = 0 then t else let rec aux = function | 0 -> [] | n -> - (match List.nth ctx (n+bound) with - | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> NCic.Const refe - | Fix _ | Ce _ -> NCic.Rel (n+bound)) :: aux (n-1) + match List.nth ctx (n+bound) with + | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> + NCic.Const refe :: aux (n-1) + | Fix _ | Ce (_, NCic.Decl _) -> NCic.Rel (n+bound)::aux (n-1) + | Ce (_, NCic.Def _) -> aux (n-1) in NCic.Appl (t:: aux free) ;; let splat_args ctx t n_fix = - let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in + let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in 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 + | Ce (_, NCic.Decl _) when n <= bound -> NCic.Rel n:: aux (n-1) | 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) + splat_args_for_rel ctx (NCic.Const refe):: aux (n-1) + | Fix _ | Ce (_, NCic.Decl _) -> NCic.Rel (n - n_fix):: aux (n-1) + | Ce (_, NCic.Def _) -> aux (n - 1) + ) in NCic.Appl (t:: aux (List.length ctx)) ;; @@ -261,11 +269,12 @@ let convert_term uri t = Fix (r,name,ty) :: bctx, fixpoints_ty@fixpoints,ty::tys,idx+1) fl ([], [], [], 0) in - let _, free, _ = context_tassonomy (bad_bctx @ ctx) in + let _, _, free_decls, _ = context_tassonomy (bad_bctx @ ctx) in let bctx = List.map (function | Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) -> - Fix (Ref.reference_of_ouri buri(Ref.Fix (idx,recno+free)),name,ty) + Fix (Ref.reference_of_ouri buri + (Ref.Fix (idx,recno+free_decls)),name,ty) | _ -> assert false) bad_bctx @ ctx in let n_fl = List.length fl in @@ -280,7 +289,7 @@ let convert_term uri t = List.fold_right2 (fun (name,rno,_,bo) ty (l,fixpoints,idx) -> let bo, fixpoints_bo = aux boctx bctx n_fl buri bo in - let rno = rno + free in + let rno = rno + free_decls in if idx = k then rno_k := rno; (([],name,rno,splat true ctx ty, splat false ctx bo)::l), fixpoints_bo @ fixpoints,idx+1) @@ -296,7 +305,7 @@ let convert_term uri t = n_fix, fixpoints @ [obj] | Cic.Rel n -> - let bound, _, primo_ce_dopo_fix = context_tassonomy ctx in + let bound, _, _, primo_ce_dopo_fix = context_tassonomy ctx in (match List.nth ctx (n-1) with | Fix (r,_,_) when n < primo_ce_dopo_fix -> splat_args_for_rel ctx (NCic.Const r), [] -- 2.39.2