From c22f39a5d5afc0ef55beb221e00e2e6703b13d90 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 02:10:13 +0000 Subject: [PATCH] Bug fixed: the debrujinate function (hence the one to compute objects height) did not take the substitution. --- .../grafite_engine/grafiteEngine.ml | 2 +- .../components/ng_kernel/nCicTypeChecker.ml | 35 ++++++++++++------- .../components/ng_kernel/nCicTypeChecker.mli | 6 ++-- .../components/ng_refiner/nCicRefiner.ml | 7 ++-- 4 files changed, 30 insertions(+), 20 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 9817474cd..eb994854f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -705,7 +705,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let obj_kind = NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst []) obj_kind in - let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in + let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in (* fix the height inside the object *) let rec fix () = function | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index ce16af7d2..c4c2af477 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -96,13 +96,22 @@ let fixed_args bos j n nn = (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos ;; -let debruijn uri number_of_types context = +let debruijn uri number_of_types ~subst context = +(* manca la subst! *) let rec aux k t = match t with - | C.Meta (i,(s,C.Ctx l)) -> - let l1 = HExtlib.sharing_map (aux (k-s)) l in - if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) - | C.Meta _ -> t + | C.Meta (i,(s,l)) -> + (try + let _,_,term,_ = U.lookup_subst i subst in + let ts = S.subst_meta (0,l) term in + let ts' = aux (k-s) ts in + if ts == ts' then t else ts' + with U.Subst_not_found _ -> + match l with + C.Ctx l -> + let l1 = HExtlib.sharing_map (aux (k-s)) l in + if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) + | _ -> t) | C.Const (Ref.Ref (uri1,(Ref.Fix (no,_,_) | Ref.CoFix no))) | C.Const (Ref.Ref (uri1,Ref.Ind (_,no,_))) when NUri.eq uri uri1 -> C.Rel (k + number_of_types - no) @@ -166,7 +175,7 @@ let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term = | _ -> assert false in context_dcl, - List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl, + List.map (fun (_,id,ty) -> id, debruijn r_uri r_len ~subst context ty) cl, len, len + r_len ;; @@ -695,7 +704,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty = and is_non_recursive_singleton ~subst (Ref.Ref (uri,_)) iname ity cty = let ctx = [iname, C.Decl ity] in - let cty = debruijn uri 1 [] cty in + let cty = debruijn uri 1 [] ~subst cty in let len = List.length ctx in let rec aux ctx n nn t = match R.whd ~subst ctx t with @@ -733,7 +742,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = let k_relev = try snd (HExtlib.split_nth leftno k_relev) with Failure _ -> k_relev in - let te = debruijn uri len [] te in + let te = debruijn uri len [] ~subst te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = HExtlib.split_nth (List.length tys) (List.rev context) in @@ -864,7 +873,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl) in let fl_len = List.length fl in - let bos = List.map (debruijn uri fl_len context) bos in + let bos = List.map (debruijn uri fl_len context ~subst) bos in let j = List.fold_left min max_int (List.map (fun (_,_,i,_,_)->i) fl) in let ctx_len = List.length context in (* we may look for fixed params not only up to j ... *) @@ -1204,7 +1213,7 @@ let height_of_term tl = 1 + !h ;; -let height_of_obj_kind uri = +let height_of_obj_kind uri ~subst = function NCic.Inductive _ | NCic.Constant (_,_,None,_,_) @@ -1214,7 +1223,7 @@ let height_of_obj_kind uri = height_of_term (List.fold_left (fun l (_,_,_,ty,bo) -> - let bo = debruijn uri iflno [] bo in + let bo = debruijn uri iflno [] ~subst bo in ty::bo::l ) [] ifl) | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty] @@ -1222,7 +1231,7 @@ let height_of_obj_kind uri = let typecheck_obj (uri,height,metasenv,subst,kind) = (*height must be checked since it is not only an optimization during reduction*) - let iheight = height_of_obj_kind uri kind in + let iheight = height_of_obj_kind uri ~subst kind in if height <> iheight then raise (TypeCheckerFailure (lazy (Printf.sprintf "the declared object height (%d) is not the inferred one (%d)" @@ -1259,7 +1268,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) = let dfl, kl = List.split (List.map2 (fun (_,_,_,_,bo) rno -> - let dbo = debruijn uri len [] bo in + let dbo = debruijn uri len [] ~subst bo in dbo, Evil rno) fl kl) in diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index af0f2cade..3cd11c0f8 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -30,7 +30,7 @@ val typeof: NCic.context -> NCic.term -> NCic.term -val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int +val height_of_obj_kind: NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int val get_relevance : metasenv:NCic.metasenv -> subst:NCic.substitution -> @@ -53,7 +53,9 @@ val check_allowed_sort_elimination : NCic.term -> NCic.term -> NCic.term -> unit (* Functions to be used by the refiner *) -val debruijn: NUri.uri -> int -> NCic.context -> NCic.term -> NCic.term +val debruijn: + NUri.uri -> int -> subst:NCic.substitution -> NCic.context -> NCic.term -> + NCic.term val are_all_occurrences_positive: subst:NCic.substitution -> NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 6bcda0df8..d279b840b 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -574,8 +574,7 @@ let typeof_obj match bo with | Some bo -> let metasenv, subst, bo, ty = - typeof rdb ~localise metasenv subst [] bo (Some ty) - in + typeof rdb ~localise metasenv subst [] bo (Some ty) in let height = (* XXX recalculate *) height in metasenv, subst, Some bo, ty, height | None -> metasenv, subst, None, ty, 0 @@ -588,7 +587,7 @@ let typeof_obj List.fold_left (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) -> let metasenv, subst, ty, _ = check_type metasenv subst [] ty in - let dbo = NCicTypeChecker.debruijn uri len [] bo in + let dbo = NCicTypeChecker.debruijn uri len [] ~subst bo in let localise = relocalise localise dbo bo in (name,C.Decl ty)::types, metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl @@ -637,7 +636,7 @@ let typeof_obj let k_relev = try snd (HExtlib.split_nth leftno k_relev) with Failure _ -> k_relev in - let te = NCicTypeChecker.debruijn uri len [] te in + let te = NCicTypeChecker.debruijn uri len [] ~subst te in let metasenv, subst, te, _ = check_type metasenv subst tys te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = -- 2.39.2