diff options
| -rw-r--r-- | engine/termops.ml | 47 | ||||
| -rw-r--r-- | kernel/constr.ml | 47 | ||||
| -rw-r--r-- | kernel/constr.mli | 23 | ||||
| -rw-r--r-- | vernac/assumptions.ml | 26 |
4 files changed, 60 insertions, 83 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index ccd49ca495..66131e1a8f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -677,12 +677,21 @@ let map_constr_with_binders_left_to_right sigma g f l c = if def' == def && t' == t && ty' == ty then c else mkArray(u,t',def',ty') -let map_under_context_with_full_binders sigma g f l n d = - let open EConstr in - let f l c = Unsafe.to_constr (f l (of_constr c)) in - let g d l = g (of_rel_decl d) l in - let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in - EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d) +let rec map_under_context_with_full_binders sigma g f l n d = + if n = 0 then f l d else + match EConstr.kind sigma d with + | LetIn (na,b,t,c) -> + let b' = f l b in + let t' = f l t in + let c' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in + if b' == b && t' == t && c' == c then d + else EConstr.mkLetIn (na,b',t',c') + | Lambda (na,t,b) -> + let t' = f l t in + let b' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in + if t' == t && b' == b then d + else EConstr.mkLambda (na,t',b') + | _ -> CErrors.anomaly (Pp.str "Ill-formed context") let map_branches_with_full_binders sigma g f l ci bl = let tags = Array.map List.length ci.ci_pp_info.cstr_tags in @@ -775,11 +784,27 @@ let map_constr_with_full_binders_user_view sigma g f = each binder traversal; it is not recursive *) let fold_constr_with_full_binders sigma g f n acc c = - let open EConstr in - let f l acc c = f l acc (of_constr c) in - let g d l = g (of_rel_decl d) l in - let c = Unsafe.to_constr (whd_evar sigma c) in - Constr.fold_with_full_binders g f n acc c + let open EConstr.Vars in + let open Context.Rel.Declaration in + match EConstr.kind sigma c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_,c) -> f n acc c + | Evar (_,l) -> List.fold_left (f n) acc l + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty let fold_constr_with_binders sigma g f n acc c = let open EConstr in diff --git a/kernel/constr.ml b/kernel/constr.ml index 3157ec9f57..bbaf95c9df 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -624,30 +624,6 @@ let map_branches_with_binders g f l ci bl = let map_return_predicate_with_binders g f l ci p = map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p -let rec map_under_context_with_full_binders g f l n d = - if n = 0 then f l d else - match kind d with - | LetIn (na,b,t,c) -> - let b' = f l b in - let t' = f l t in - let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in - if b' == b && t' == t && c' == c then d - else mkLetIn (na,b',t',c') - | Lambda (na,t,b) -> - let t' = f l t in - let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in - if t' == t && b' == b then d - else mkLambda (na,t',b') - | _ -> CErrors.anomaly (Pp.str "Ill-formed context") - -let map_branches_with_full_binders g f l ci bl = - let tags = Array.map List.length ci.ci_pp_info.cstr_tags in - let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in - if Array.for_all2 (==) bl' bl then bl else bl' - -let map_return_predicate_with_full_binders g f l ci p = - map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p - let map_invert f = function | NoInvert -> NoInvert | CaseInvert {univs;args;} as orig -> @@ -886,29 +862,6 @@ let liftn n k c = let lift n = liftn n 1 -let fold_with_full_binders g f n acc c = - let open Context.Rel.Declaration in - match kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (_,c) -> f n acc c - | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty - - type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool diff --git a/kernel/constr.mli b/kernel/constr.mli index 62f2555a7e..ed63ac507c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -478,25 +478,6 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr -(** [map_under_context_with_full_binders g f n l c] is similar to - [map_under_context_with_binders] except that [g] takes also a full - binder as argument and that only the number of binders (and not - their signature) is required *) - -val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr - -(** [map_branches_with_full_binders g f l br] is equivalent to - [map_branches_with_binders] but using - [map_under_context_with_full_binders] *) - -val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array - -(** [map_return_predicate_with_full_binders g f l p] is equivalent to - [map_return_predicate_with_binders] but using - [map_under_context_with_full_binders] *) - -val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr - (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] @@ -505,10 +486,6 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a -val fold_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b - val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a (** [map f c] maps [f] on the immediate subterms of [c]; it is diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 848cd501c6..792f07bb89 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -165,6 +165,28 @@ let label_of = let open GlobRef in function | ConstructRef ((kn,_),_) -> MutInd.label kn | VarRef id -> Label.of_id id +let fold_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_,c) -> f n acc c + | Evar (_,l) -> List.fold_left (f n) acc l + | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty + let rec traverse current ctx accu t = let open GlobRef in match Constr.kind t with @@ -189,10 +211,10 @@ let rec traverse current ctx accu t = traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> - Constr.fold_with_full_binders + fold_with_full_binders Context.Rel.add (traverse current) ctx accu t end -| _ -> Constr.fold_with_full_binders +| _ -> fold_with_full_binders Context.Rel.add (traverse current) ctx accu t and traverse_object ?inhabits (curr, data, ax2ty) body obj = |