From 4a4703054e9f022479ac7ab9cb96007984da7ef2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 20 Feb 2008 14:49:22 +0000 Subject: [PATCH] many fixed in translation functions --- .../components/ng_kernel/nCic2OCic.ml | 65 +++++++----- .../components/ng_kernel/oCic2NCic.ml | 98 ++++++++++++------- 2 files changed, 102 insertions(+), 61 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 13c703dae..e6a15d315 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -1,11 +1,14 @@ - -let rec convert_term k = function (* pass k along *) +let convert_term uri n_fl t = + let rec convert_term k = function (* pass k along *) | NCic.Rel i -> Cic.Rel i | NCic.Meta _ -> assert false | NCic.Appl l -> Cic.Appl (List.map (convert_term k) l) - | NCic.Prod (n,s,t) -> Cic.Prod (Cic.Name n,convert_term k s, convert_term k t) - | NCic.Lambda (n,s,t) -> Cic.Lambda(Cic.Name n,convert_term k s, convert_term k t) - | NCic.LetIn (n,_,s,t) -> Cic.LetIn (Cic.Name n,convert_term k s, convert_term k t) + | NCic.Prod (n,s,t) -> + Cic.Prod (Cic.Name n,convert_term k s, convert_term (k+1) t) + | NCic.Lambda (n,s,t) -> + Cic.Lambda(Cic.Name n,convert_term k s, convert_term (k+1) t) + | NCic.LetIn (n,_,s,t) -> + Cic.LetIn (Cic.Name n,convert_term k s, convert_term (k+1) t) | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp | NCic.Sort NCic.Set -> Cic.Sort Cic.Set @@ -21,31 +24,45 @@ let rec convert_term k = function (* pass k along *) | NCic.Match (NReference.Ref (_,u,NReference.Ind i),oty,t,pl) -> Cic.MutCase (NUri.ouri_of_nuri u,i, convert_term k oty, convert_term k t, List.map (convert_term k) pl) - | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_))) -> assert false - (* map to rel if is the self-fix, otherwise explode *) - | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) -> assert false - (* map to rel if is the self-fix, otherwise explode *) + | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_))) + | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) -> + if NUri.eq u uri then + Cic.Rel (n_fl - i + k) + else + Cic.Const (NUri.ouri_of_nuri u,[]) | _ -> assert false + in + convert_term 0 t ;; -let convert_fix k fl = +let convert_fix is_fix uri k fl = let n_fl = List.length fl in - let fl = - List.map - (fun (_, name,recno,ty,bo) -> - name, recno, convert_term 0 ty, convert_term 0 bo) - fl - in - Cic.Fix (k, fl) + if is_fix then + let fl = + List.map + (fun (_, name,recno,ty,bo) -> + name, recno, convert_term uri n_fl ty, convert_term uri n_fl bo) + fl + in + Cic.Fix (k, fl) + else + let fl = + List.map + (fun (_, name,_,ty,bo) -> + name, convert_term uri n_fl ty, convert_term uri n_fl bo) + fl + in + Cic.CoFix (k, fl) ;; let convert_nobj = function - | _,_,_,_,NCic.Constant (rel, name, Some bo, ty, _) -> - Cic.Constant (name, Some (convert_term 0 bo), convert_term 0 ty, [],[]) - | _,_,_,_,NCic.Constant (rel, name, None, ty, _) -> - Cic.Constant (name, None, convert_term 0 ty, [],[]) - | _,_,_,_,NCic.Fixpoint (is_fix, fl, _) -> - Cic.Constant ("pippo", Some (convert_fix 0 fl), - convert_term 0 (let _,_,_,ty,_ = List.hd fl in ty), [], []) + | u,_,_,_,NCic.Constant (_, name, Some bo, ty, _) -> + Cic.Constant (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[]) + | u,_,_,_,NCic.Constant (_, name, None, ty, _) -> + Cic.Constant (name, None, convert_term u 0 ty, [],[]) + | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) -> + Cic.Constant (UriManager.name_of_uri (NUri.ouri_of_nuri u), + Some (convert_fix is_fix u 0 fl), + convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], []) | _,_,_,_,NCic.Inductive _ -> assert false ;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index c3dfb418c..b81635581 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -5,7 +5,9 @@ let cn_to_s = function | Cic.Name s -> s ;; -type ctx = Ce of NCic.hypothesis | Fix of int * int +type ctx = + | Ce of NCic.hypothesis + | Fix of NReference.reference * string * NCic.term let splat mk_pi ctx t = List.fold_left @@ -14,30 +16,47 @@ let splat mk_pi ctx t = | Ce (name, NCic.Def (bo,ty)) -> NCic.LetIn (name, ty, bo, t) | Ce (name, NCic.Decl ty) when mk_pi -> NCic.Prod (name, ty, t) | Ce (name, NCic.Decl ty) -> NCic.Lambda (name, ty, t) - | Fix _ -> t) + | Fix (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t) + | Fix (_,name,ty) -> NCic.Lambda (name,ty,t)) t ctx ;; +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 + in + split true 0 1 ctx +;; + let splat_args ctx t = - let n_args = - List.length (List.filter (function Ce _ -> true | _ -> false) ctx) - in - if n_args = 0 then t + let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in + if free = 0 then t else let rec aux = function | 0 -> [] - | n -> aux (n-1) @ [NCic.Rel n] + | n -> + (match List.nth ctx (n+bound) with + | Fix (refe, _, _) when n < primo_ce_dopo_fix -> (NCic.Const refe) + | Fix _ | Ce _ -> NCic.Rel (n+bound)) :: aux (n-1) in - NCic.Appl (t:: aux n_args) + NCic.Appl (t:: aux free) ;; +(* 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 idx = ref ~-1 in - let bctx = - List.map (fun (_,_,_) -> - incr idx; Fix (~-1,!idx)) fl @ ctx + 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 + ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1) + fl (ctx, [], [], 0) in let buri = UriManager.uri_of_string @@ -51,26 +70,32 @@ let convert_term uri t = len+1)) (octx,0) fl in let fl, fixpoints = - List.fold_right - (fun (name,ty,bo) (l,fixpoints) -> - let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + List.fold_right2 + (fun (name,_,bo) ty (l,fixpoints) -> let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in (([],name,~-1,splat true ctx ty, splat false ctx bo)::l), - fixpoints_ty @ fixpoints_bo @ fixpoints) - fl ([],[]) + fixpoints_bo @ fixpoints) + fl tys ([],fixpoints_tys) in let obj = NUri.nuri_of_ouri uri,0,[],[], NCic.Fixpoint (false, fl, (`Generated, `Definition)) in - NCic.Const (NReference.reference_of_ouri uri (NReference.CoFix (k))), + splat_args ctx + (NCic.Const (NReference.reference_of_ouri uri (NReference.CoFix k))), obj::fixpoints | Cic.Fix (k, fl) -> - let idx = ref ~-1 in let rno = ref 0 in - let bctx = - List.map (fun (_,recno,_,_) -> - incr idx; if !idx = k then rno := recno;Fix (recno,!idx)) fl @ ctx + let bctx, fixpoints_tys, tys, _ = + List.fold_right + (fun (name,recno,ty,_) (ctx, 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 uri (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 @@ -84,31 +109,28 @@ let convert_term uri t = len+1)) (octx,0) fl in let fl, fixpoints = - List.fold_right - (fun (name,rno,ty,bo) (l,fixpoints) -> - let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + 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 (([],name,rno,splat true ctx ty, splat false ctx bo)::l), - fixpoints_ty @ fixpoints_bo @ fixpoints) - fl ([],[]) + fixpoints_bo @ fixpoints) + fl tys ([],fixpoints_tys) in let obj = NUri.nuri_of_ouri uri,0,[],[], NCic.Fixpoint (true, fl, (`Generated, `Definition)) in - NCic.Const (NReference.reference_of_ouri uri (NReference.Fix (k,!rno))), + splat_args ctx + (NCic.Const + (NReference.reference_of_ouri uri (NReference.Fix (k,!rno)))), obj::fixpoints | Cic.Rel n -> + let _, _, primo_ce_dopo_fix = context_tassonomy ctx in (match List.nth ctx n with - | Ce _ -> NCic.Rel (n-n_fix), [] - | Fix (recno, fixno) -> - (* uri should be in the context, since the inner - * fix may refer to the outer one *) - splat_args ctx (* this function must lift the args wrt len(octx) *) - (NCic.Const - (NReference.reference_of_ouri uri (NReference.Fix (fixno,recno)))), - []) + | Fix (r,_,_) when n < primo_ce_dopo_fix -> + splat_args ctx (NCic.Const r), [] + | Fix (_,_,_) | 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 @@ -149,7 +171,9 @@ let convert_term uri t = (t::l,fixpoints@acc)) l ([],[]) in - NCic.Appl l, fixpoints + (match l with + | (NCic.Appl l1)::l2 -> NCic.Appl (l1@l2), fixpoints + | _ -> NCic.Appl l, fixpoints) | Cic.Const (curi, _) -> NCic.Const (NReference.reference_of_ouri curi NReference.Def),[] | Cic.MutInd (curi, tyno, _) -> -- 2.39.2