X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=1d0e453b006457909f1bb6a5c55fe33c27c4667e;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=b81635581b924c18e1c74378cb1247493d32cee7;hpb=4a4703054e9f022479ac7ab9cb96007984da7ef2;p=helm.git diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index b81635581..1d0e453b0 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -30,7 +30,7 @@ let context_tassonomy ctx = split true 0 1 ctx ;; -let splat_args ctx t = +let splat_args_for_rel ctx t = let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in if free = 0 then t else @@ -38,30 +38,49 @@ let splat_args ctx t = | 0 -> [] | n -> (match List.nth ctx (n+bound) with - | Fix (refe, _, _) when n < primo_ce_dopo_fix -> (NCic.Const refe) + | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> NCic.Const refe | Fix _ | Ce _ -> NCic.Rel (n+bound)) :: 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 + 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 *) (* ctx does not distinguish successive blocks of cofix, since there may be no * lambda separating them *) let convert_term uri t = let rec aux octx (ctx : ctx list) n_fix uri = function | Cic.CoFix (k, fl) -> + let buri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri^"/"^ + UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con") + in let bctx, fixpoints_tys, tys, _ = List.fold_right (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 uri(NReference.CoFix idx) in + let r = NReference.reference_of_ouri buri(NReference.CoFix idx) in ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1) - fl (ctx, [], [], 0) - in - let buri = - UriManager.uri_of_string - (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con") + fl ([], [], [], 0) in + let bctx = bctx @ ctx in let n_fl = List.length fl in let boctx,_ = List.fold_left @@ -72,19 +91,25 @@ let convert_term uri t = let fl, fixpoints = List.fold_right2 (fun (name,_,bo) ty (l,fixpoints) -> - let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in + let bo, fixpoints_bo = aux boctx bctx n_fl buri bo in (([],name,~-1,splat true ctx ty, splat false ctx bo)::l), fixpoints_bo @ fixpoints) fl tys ([],fixpoints_tys) in let obj = - NUri.nuri_of_ouri uri,0,[],[], + NUri.nuri_of_ouri buri,0,[],[], NCic.Fixpoint (false, fl, (`Generated, `Definition)) in splat_args ctx - (NCic.Const (NReference.reference_of_ouri uri (NReference.CoFix k))), - obj::fixpoints + (NCic.Const (NReference.reference_of_ouri buri (NReference.CoFix k))) + n_fix, + fixpoints @ [obj] | Cic.Fix (k, fl) -> + let buri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri^"/"^ + UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con") + in let rno = ref 0 in let bctx, fixpoints_tys, tys, _ = List.fold_right @@ -92,15 +117,12 @@ let convert_term uri t = let ty, fixpoints_ty = aux octx ctx n_fix uri ty in if idx = k then rno := recno; let r = - NReference.reference_of_ouri uri (NReference.Fix (idx,recno)) + NReference.reference_of_ouri buri (NReference.Fix (idx,recno)) in ctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx+1) - fl (ctx, [], [], 0) - in - let buri = - UriManager.uri_of_string - (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con") + fl ([], [], [], 0) in + let bctx = bctx @ ctx in let n_fl = List.length fl in let boctx,_ = List.fold_left @@ -111,26 +133,30 @@ let convert_term uri t = let fl, fixpoints = List.fold_right2 (fun (name,rno,_,bo) ty (l,fixpoints) -> - let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in - let rno = rno + List.length ctx - n_fix in + let bo, fixpoints_bo = aux boctx bctx n_fl buri bo in + let _, free, _ = context_tassonomy bctx in + let rno = rno + free in (([],name,rno,splat true ctx ty, splat false ctx bo)::l), fixpoints_bo @ fixpoints) fl tys ([],fixpoints_tys) in let obj = - NUri.nuri_of_ouri uri,0,[],[], + NUri.nuri_of_ouri buri,0,[],[], NCic.Fixpoint (true, fl, (`Generated, `Definition)) in splat_args ctx (NCic.Const - (NReference.reference_of_ouri uri (NReference.Fix (k,!rno)))), - obj::fixpoints + (NReference.reference_of_ouri buri (NReference.Fix (k,!rno)))) + n_fix, + fixpoints @ [obj] | Cic.Rel n -> - let _, _, primo_ce_dopo_fix = context_tassonomy ctx in - (match List.nth ctx n with + 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 ctx (NCic.Const r), [] - | Fix (_,_,_) | Ce _ -> NCic.Rel (n-n_fix), []) + splat_args_for_rel ctx (NCic.Const r), [] + | Ce _ when n <= bound -> NCic.Rel n, [] + | Fix _ (* BUG 3 fix nested *) + | Ce _ -> NCic.Rel (n-n_fix), []) | Cic.Lambda (name, (s as old_s), t) -> let s, fixpoints_s = aux octx ctx n_fix uri s in let ctx = Ce (cn_to_s name, NCic.Decl s) :: ctx in @@ -227,5 +253,5 @@ let convert_obj_aux uri = function let convert_obj uri obj = let o, fixpoints = convert_obj_aux uri obj in let obj = NUri.nuri_of_ouri uri,0, [], [], o in - obj, fixpoints + fixpoints @ [obj] ;;