From bf4f7d923f1bcf1f07d5d4f46fc6f8e7bce4b578 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 9 Apr 2008 14:57:34 +0000 Subject: [PATCH] Fixed serious bug that occurred only in the following situation: \lambda x. Fix f { \lambda y: P x. Fix g { The two fixes must be translated as Fix f { \lambda x. \lambda y: P x. ...} Fix g { \lambda x. \lambda f. \lambda y: P x. ... } In the first case, the x that occurs in the type of y must be a Rel 1. In the second case, the x that occurs in the type of y must be a Rel 2. The previous code translated both of them to Rel 1. --- .../components/ng_kernel/oCic2NCic.ml | 126 ++++++++++-------- 1 file changed, 71 insertions(+), 55 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index c3a6558c2..8b6fd7f45 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -6,19 +6,19 @@ let cn_to_s = function ;; type ctx = - | Ce of NCic.hypothesis + | Ce of NCic.hypothesis * NCic.obj list | Fix of Ref.reference * string * NCic.term let splat mk_pi ctx t = List.fold_left - (fun t c -> + (fun (t,l) c -> match c with - | 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 (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t) - | Fix (_,name,ty) -> NCic.Lambda (name,ty,t)) - t ctx + | Ce ((name, NCic.Def (bo,ty)),l') -> NCic.LetIn (name, ty, bo, t),l@l' + | Ce ((name, NCic.Decl ty),l') when mk_pi -> NCic.Prod (name, ty, t),l@l' + | Ce ((name, NCic.Decl ty),l') -> NCic.Lambda (name, ty, t),l@l' + | Fix (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t),l + | Fix (_,name,ty) -> NCic.Lambda (name,ty,t),l) + (t,[]) ctx ;; let context_tassonomy ctx = @@ -27,8 +27,8 @@ let context_tassonomy ctx = | Fix _ ::tl -> split false acc (acc1+1) tl | _ as l -> let only_decl = - List.filter (function Ce (_, NCic.Decl _) | Fix _ -> true | _ -> false) - l + List.filter + (function Ce ((_, NCic.Decl _),_) | Fix _ -> true | _ -> false) l in acc, List.length l, List.length only_decl, acc1 in @@ -45,8 +45,8 @@ let splat_args_for_rel ctx t = 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) + | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (n+bound)::aux (n-1) + | Ce ((_, NCic.Def _),_) -> aux (n-1) in NCic.Appl (t:: aux free) ;; @@ -59,11 +59,11 @@ let splat_args ctx t n_fix = | 0 -> [] | n -> (match List.nth ctx (n-1) with - | Ce (_, NCic.Decl _) when n <= bound -> NCic.Rel n:: aux (n-1) + | 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):: aux (n-1) - | Fix _ | Ce (_, NCic.Decl _) -> NCic.Rel (n - n_fix):: aux (n-1) - | Ce (_, NCic.Def _) -> 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)) @@ -214,8 +214,14 @@ let get_fresh,reset_seed = (* 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) -> + (* k=true if we are converting a term to be pushed in a ctx or if we are + converting the type of a fix; + k=false if we are converting a term to be put in the body of a fix; + in the latter case, we must permute Rels since the Fix abstraction will + preceed its lefts parameters; in the former case, there is nothing to + permute *) + let rec aux k octx (ctx : ctx list) n_fix uri = function + | Cic.CoFix (cofixno, fl) -> let buri = UriManager.uri_of_string (UriManager.buri_of_uri uri^"/"^ @@ -224,7 +230,7 @@ let convert_term uri t = let bctx, fixpoints_tys, tys, _ = List.fold_right (fun (name,ty,_) (bctx, fixpoints, tys, idx) -> - let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in let r = Ref.reference_of_ouri buri(Ref.CoFix idx) in Fix (r,name,ty) :: bctx, fixpoints_ty @ fixpoints,ty::tys,idx+1) fl ([], [], [], 0) @@ -240,9 +246,11 @@ 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_fl buri bo in - (([],name,~-1,splat true ctx ty, splat false ctx bo)::l), - fixpoints_bo @ fixpoints) + let bo, fixpoints_bo = aux false boctx bctx n_fl buri bo in + let splty,fixpoints_splty = splat true ctx ty in + let splbo,fixpoints_splbo = splat false ctx bo in + (([],name,~-1,splty,splbo)::l), + fixpoints_bo @ fixpoints_splty @ fixpoints_splbo @ fixpoints) fl tys ([],fixpoints_tys) in let obj = @@ -250,10 +258,10 @@ let convert_term uri t = NCic.Fixpoint (false, fl, (`Generated, `Definition)) in splat_args ctx - (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix k))) + (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix cofixno))) n_fix, fixpoints @ [obj] - | Cic.Fix (k, fl) -> + | Cic.Fix (fixno, fl) -> let buri = UriManager.uri_of_string (UriManager.buri_of_uri uri^"/"^ @@ -262,7 +270,7 @@ let convert_term uri t = let bad_bctx, fixpoints_tys, tys, _ = List.fold_right (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) -> - let ty, fixpoints_ty = aux octx ctx n_fix uri ty in + let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in let r = (* recno is dummy here, must be lifted by the ctx len *) Ref.reference_of_ouri buri (Ref.Fix (idx,recno)) in @@ -284,15 +292,17 @@ let convert_term uri t = (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types, len+1)) (octx,0) fl in - let rno_k = ref 0 in + let rno_fixno = ref 0 in let fl, fixpoints,_ = List.fold_right2 (fun (name,rno,_,bo) ty (l,fixpoints,idx) -> - let bo, fixpoints_bo = aux boctx bctx n_fl buri bo in + let bo, fixpoints_bo = aux false boctx bctx n_fl buri bo in + let splty,fixpoints_splty = splat true ctx ty in + let splbo,fixpoints_splbo = splat false ctx bo 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) + if idx = fixno then rno_fixno := rno; + (([],name,rno,splty,splbo)::l), + fixpoints_bo@fixpoints_splty@fixpoints_splbo@fixpoints,idx+1) fl tys ([],fixpoints_tys,0) in let obj = @@ -301,7 +311,7 @@ let convert_term uri t = in splat_args ctx (NCic.Const - (Ref.reference_of_ouri buri (Ref.Fix (k,!rno_k)))) + (Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)))) n_fix, fixpoints @ [obj] | Cic.Rel n -> @@ -310,31 +320,37 @@ let convert_term uri t = | Fix (r,_,_) when n < primo_ce_dopo_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), []) + | Fix _ when n <= bound -> assert false + | Fix _ | Ce _ when k = true -> NCic.Rel n, [] + | 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 + let s, fixpoints_s = aux k octx ctx n_fix uri s in + let s', fixpoints_s' = aux true octx ctx n_fix uri old_s in + let ctx = Ce ((cn_to_s name, NCic.Decl s'),fixpoints_s') :: ctx in let octx = Some (name, Cic.Decl old_s) :: octx in - let t, fixpoints_t = aux octx ctx n_fix uri t in + let t, fixpoints_t = aux k octx ctx n_fix uri t in NCic.Lambda (cn_to_s name, s, t), fixpoints_s @ fixpoints_t | Cic.Prod (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 + let s, fixpoints_s = aux k octx ctx n_fix uri s in + let s', fixpoints_s' = aux true octx ctx n_fix uri old_s in + let ctx = Ce ((cn_to_s name, NCic.Decl s'),fixpoints_s') :: ctx in let octx = Some (name, Cic.Decl old_s) :: octx in - let t, fixpoints_t = aux octx ctx n_fix uri t in + let t, fixpoints_t = aux k octx ctx n_fix uri t in NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t | 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 te, fixpoints_s = aux k octx ctx n_fix uri te in + let te', fixpoints_s' = aux true octx ctx n_fix uri old_te in + let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in + let ty', fixpoints_ty' = aux true octx ctx n_fix uri old_ty in + let fixpoints' = fixpoints_s' @ fixpoints_ty' in + let ctx = Ce ((cn_to_s name, NCic.Def (te', ty')),fixpoints') :: 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 + let t, fixpoints_t = aux k octx ctx n_fix uri t in 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 + let t, fixpoints_t = aux k octx ctx n_fix uri t in + let ty, fixpoints_ty = aux k 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.CProp -> NCic.Sort NCic.CProp,[] @@ -345,7 +361,7 @@ let convert_term uri t = let l, fixpoints = List.fold_right (fun t (l,acc) -> - let t, fixpoints = aux octx ctx n_fix uri t in + let t, fixpoints = aux k octx ctx n_fix uri t in (t::l,fixpoints@acc)) l ([],[]) in @@ -353,7 +369,7 @@ let convert_term uri t = | (NCic.Appl l1)::l2 -> NCic.Appl (l1@l2), fixpoints | _ -> NCic.Appl l, fixpoints) | Cic.Const (curi, ens) -> - aux_ens curi octx ctx n_fix uri ens + aux_ens k curi octx ctx n_fix uri ens (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with | Cic.Constant (_,Some _,_,_,_) -> NCic.Const (Ref.reference_of_ouri curi Ref.Def) @@ -361,30 +377,30 @@ let convert_term uri t = NCic.Const (Ref.reference_of_ouri curi Ref.Decl) | _ -> assert false) | Cic.MutInd (curi, tyno, ens) -> - aux_ens curi octx ctx n_fix uri ens + aux_ens k curi octx ctx n_fix uri ens (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno))) | Cic.MutConstruct (curi, tyno, consno, ens) -> - aux_ens curi octx ctx n_fix uri ens + aux_ens k curi octx ctx n_fix uri ens (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno)))) | Cic.Var (curi, ens) -> (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with Cic.Variable (_,Some bo,_,_,_) -> - aux octx ctx n_fix uri (CicSubstitution.subst_vars ens bo) + aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo) | _ -> assert false) | Cic.MutCase (curi, tyno, outty, t, branches) -> let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in - let outty, fixpoints_outty = aux octx ctx n_fix uri outty in - let t, fixpoints_t = aux octx ctx n_fix uri t in + let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in + let t, fixpoints_t = aux k octx ctx n_fix uri t in let branches, fixpoints = List.fold_right (fun t (l,acc) -> - let t, fixpoints = aux octx ctx n_fix uri t in + let t, fixpoints = aux k octx ctx n_fix uri t in (t::l,fixpoints@acc)) branches ([],[]) in NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints | Cic.Implicit _ | Cic.Meta _ -> assert false - and aux_ens curi octx ctx n_fix uri ens he = + and aux_ens k curi octx ctx n_fix uri ens he = match ens with [] -> he,[] | _::_ -> @@ -402,14 +418,14 @@ let convert_term uri t = Cic.Variable (_,Some _,_,_,_) -> l, objs | Cic.Variable (_,None,_,_,_) -> let t = List.assoc luri ens in - let t,o = aux octx ctx n_fix uri t in + let t,o = aux k octx ctx n_fix uri t in t::l, o@objs | _ -> assert false ) params ([],[]) in NCic.Appl (he::ens),objs in - aux [] [] 0 uri t + aux false [] [] 0 uri t ;; let cook mode vars t = -- 2.39.2