diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 175 | ||||
| -rw-r--r-- | engine/termops.ml | 37 | ||||
| -rw-r--r-- | engine/termops.mli | 1 | ||||
| -rw-r--r-- | engine/univNames.ml | 8 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
5 files changed, 38 insertions, 185 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index cfc4bea85f..96f1ce5e60 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -296,6 +296,8 @@ let decompose_prod_n_assum sigma n c = let existential_type = Evd.existential_type +let lift n c = of_constr (Vars.lift n (unsafe_to_constr c)) + let map_under_context f n c = let f c = unsafe_to_constr (f (of_constr c)) in of_constr (Constr.map_under_context f n (unsafe_to_constr c)) @@ -306,137 +308,21 @@ let map_return_predicate f ci p = let f c = unsafe_to_constr (f (of_constr c)) in of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p)) -let map_gen userview sigma f c = match kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (b,k,t) -> - let b' = f b in - let t' = f t in - if b'==b && t' == t then c - else mkCast (b', k, t') - | Prod (na,t,b) -> - let b' = f b in - let t' = f t in - if b'==b && t' == t then c - else mkProd (na, t', b') - | Lambda (na,t,b) -> - let b' = f b in - let t' = f t in - if b'==b && t' == t then c - else mkLambda (na, t', b') - | LetIn (na,b,t,k) -> - let b' = f b in - let t' = f t in - let k' = f k in - if b'==b && t' == t && k'==k then c - else mkLetIn (na, b', t', k') - | App (b,l) -> - let b' = f b in - let l' = Array.Smart.map f l in - if b'==b && l'==l then c - else mkApp (b', l') - | Proj (p,t) -> - let t' = f t in - if t' == t then c - else mkProj (p, t') - | Evar (e,l) -> - let l' = Array.Smart.map f l in - if l'==l then c - else mkEvar (e, l') - | Case (ci,p,b,bl) when userview -> - let b' = f b in - let p' = map_return_predicate f ci p in - let bl' = map_branches f ci bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') - | Case (ci,p,b,bl) -> - let b' = f b in - let p' = f p in - let bl' = Array.Smart.map f bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') - | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map f tl in - let bl' = Array.Smart.map f bl in - if tl'==tl && bl'==bl then c - else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map f tl in - let bl' = Array.Smart.map f bl in - if tl'==tl && bl'==bl then c - else mkCoFix (ln,(lna,tl',bl')) - -let map_user_view = map_gen true -let map = map_gen false - -let map_with_binders sigma g f l c0 = match kind sigma c0 with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c0 - | Cast (c, k, t) -> - let c' = f l c in - let t' = f l t in - if c' == c && t' == t then c0 - else mkCast (c', k, t') - | Prod (na, t, c) -> - let t' = f l t in - let c' = f (g l) c in - if t' == t && c' == c then c0 - else mkProd (na, t', c') - | Lambda (na, t, c) -> - let t' = f l t in - let c' = f (g l) c in - if t' == t && c' == c then c0 - else mkLambda (na, t', c') - | LetIn (na, b, t, c) -> - let b' = f l b in - let t' = f l t in - let c' = f (g l) c in - if b' == b && t' == t && c' == c then c0 - else mkLetIn (na, b', t', c') - | App (c, al) -> - let c' = f l c in - let al' = Array.Fun1.Smart.map f l al in - if c' == c && al' == al then c0 - else mkApp (c', al') - | Proj (p, t) -> - let t' = f l t in - if t' == t then c0 - else mkProj (p, t') - | Evar (e, al) -> - let al' = Array.Fun1.Smart.map f l al in - if al' == al then c0 - else mkEvar (e, al') - | Case (ci, p, c, bl) -> - let p' = f l p in - let c' = f l c in - let bl' = Array.Fun1.Smart.map f l bl in - if p' == p && c' == c && bl' == bl then c0 - else mkCase (ci, p', c', bl') - | Fix (ln, (lna, tl, bl)) -> - let tl' = Array.Fun1.Smart.map f l tl in - let l' = iterate g (Array.length tl) l in - let bl' = Array.Fun1.Smart.map f l' bl in - if tl' == tl && bl' == bl then c0 - else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.Fun1.Smart.map f l tl in - let l' = iterate g (Array.length tl) l in - let bl' = Array.Fun1.Smart.map f l' bl in - mkCoFix (ln,(lna,tl',bl')) - -let iter sigma f c = match kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_,t) -> f c; f t - | Prod (_,t,c) -> f t; f c - | Lambda (_,t,c) -> f t; f c - | LetIn (_,b,t,c) -> f b; f t; f c - | App (c,l) -> f c; Array.iter f l - | Proj (p,c) -> f c - | Evar (_,l) -> Array.iter f l - | Case (_,p,c,bl) -> f p; f c; Array.iter f bl - | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl - | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl +let map_user_view sigma f c = + let f c = unsafe_to_constr (f (of_constr c)) in + of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c))) + +let map sigma f c = + let f c = unsafe_to_constr (f (of_constr c)) in + of_constr (Constr.map f (unsafe_to_constr (whd_evar sigma c))) + +let map_with_binders sigma g f l c = + let f l c = unsafe_to_constr (f l (of_constr c)) in + of_constr (Constr.map_with_binders g f l (unsafe_to_constr (whd_evar sigma c))) + +let iter sigma f c = + let f c = f (of_constr c) in + Constr.iter f (unsafe_to_constr (whd_evar sigma c)) let iter_with_full_binders sigma g f n c = let open Context.Rel.Declaration in @@ -453,31 +339,20 @@ let iter_with_full_binders sigma g f n c = | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in + let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i t)) n) n lna tl in Array.iter (f n') bl | CoFix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in + let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in Array.iter (f n') bl let iter_with_binders sigma g f n c = - iter_with_full_binders sigma (fun _ acc -> g acc) f n c + let f l c = f l (of_constr c) in + Constr.iter_with_binders g f n (unsafe_to_constr (whd_evar sigma c)) -let fold sigma f acc c = match kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_,t) -> f (f acc c) t - | Prod (_,t,c) -> f (f acc t) c - | Lambda (_,t,c) -> f (f acc t) c - | LetIn (_,b,t,c) -> f (f (f acc b) t) c - | App (c,l) -> Array.fold_left f (f acc c) l - | Proj (p,c) -> f acc c - | Evar (_,l) -> Array.fold_left f acc l - | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl - | CoFix (_,(lna,tl,bl)) -> - Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl +let fold sigma f acc c = + let f acc c = f acc (of_constr c) in + Constr.fold f acc (unsafe_to_constr (whd_evar sigma c)) let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 @@ -712,7 +587,7 @@ let to_rel_decl = unsafe_to_rel_decl type substl = t list (** Operations that commute with evar-normalization *) -let lift n c = of_constr (Vars.lift n (to_constr c)) +let lift = lift let liftn n m c = of_constr (Vars.liftn n m (to_constr c)) let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c)) diff --git a/engine/termops.ml b/engine/termops.ml index ada6311067..98300764df 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -721,18 +721,16 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let bl' = Array.map (f l) bl in if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else mkCase (ci, p', c', bl') - | Fix (ln,(lna,tl,bl)) -> + | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in + let l' = fold_rec_types g fx l in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> + | CoFix(ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in + let l' = fold_rec_types g fx l in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -759,34 +757,17 @@ let fold_constr_with_full_binders sigma g f n acc c = Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = - fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_constr_with_binders g f n acc c (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at each binder traversal; it is not recursive and the order with which subterms are processed is not specified *) -let iter_constr_with_full_binders sigma g f l c = - let open RelDecl in - match EConstr.kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_, t) -> f l c; f l t - | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c - | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c - | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c - | App (c,args) -> f l c; Array.iter (f l) args - | Proj (p,c) -> f l c - | Evar (_,args) -> Array.iter (f l) args - | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl - | Fix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl - | CoFix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl +let iter_constr_with_full_binders = EConstr.iter_with_full_binders (***************************) (* occurs check functions *) diff --git a/engine/termops.mli b/engine/termops.mli index 6c3d4fa612..eef8452e64 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -88,6 +88,7 @@ val iter_constr_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."] (**********************************************************************) diff --git a/engine/univNames.ml b/engine/univNames.ml index ad91d31f87..1019f8f0c2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -36,10 +36,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_of_global ref : Name.t array = - try AUContext.names (Environ.universes_of_global (Global.env ()) ref) - with Not_found -> [||] - let name_universe lvl = (** Best-effort naming from the string representation of the level. This is completely hackish and should be solved in upper layers instead. *) @@ -55,8 +51,8 @@ let compute_instance_binders inst ubinders = type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref names = - let orig = universe_binders_of_global ref in +let universe_binders_with_opt_names orig names = + let orig = AUContext.names orig in let orig = Array.to_list orig in let udecl = match names with | None -> orig diff --git a/engine/univNames.mli b/engine/univNames.mli index dc669f45d6..6e68153ac2 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -29,5 +29,5 @@ type univ_name_list = Names.lname list of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. Otherwise return the bound universe names registered for [ref]. *) -val universe_binders_with_opt_names : Names.GlobRef.t -> +val universe_binders_with_opt_names : AUContext.t -> univ_name_list option -> universe_binders |