aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml121
1 files changed, 101 insertions, 20 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 9bf743152f..b25f38d630 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -360,17 +360,17 @@ let destConst c = match kind c with
(* Destructs an existential variable *)
let destEvar c = match kind c with
- | Evar (kn, a as r) -> r
+ | Evar (_kn, _a as r) -> r
| _ -> raise DestKO
(* Destructs a (co)inductive type named kn *)
let destInd c = match kind c with
- | Ind (kn, a as r) -> r
+ | Ind (_kn, _a as r) -> r
| _ -> raise DestKO
(* Destructs a constructor *)
let destConstruct c = match kind c with
- | Construct (kn, a as r) -> r
+ | Construct (_kn, _a as r) -> r
| _ -> raise DestKO
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
@@ -421,12 +421,12 @@ let fold f acc c = match kind c with
| 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
+ | 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)) ->
+ | Fix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
- | CoFix (_,(lna,tl,bl)) ->
+ | CoFix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
(* [iter f c] iters [f] on the immediate subterms of [c]; it is
@@ -441,7 +441,7 @@ let iter f c = match kind c with
| 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
+ | 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
@@ -463,7 +463,7 @@ let iter_with_binders g f n c = match kind c with
| App (c,l) -> f n c; Array.Fun1.iter f n l
| Evar (_,l) -> Array.Fun1.iter f n l
| Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
- | Proj (p,c) -> f n c
+ | Proj (_p,c) -> f n c
| Fix (_,(_,tl,bl)) ->
Array.Fun1.iter f n tl;
Array.Fun1.iter f (iterate g (Array.length tl) n) bl
@@ -483,19 +483,19 @@ let fold_constr_with_binders g f n acc c =
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> acc
| Cast (c,_, t) -> f n (f n acc c) t
- | Prod (na,t,c) -> f (g n) (f n acc t) c
- | Lambda (na,t,c) -> f (g n) (f n acc t) c
- | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c
+ | Prod (_na,t,c) -> f (g n) (f n acc t) c
+ | Lambda (_na,t,c) -> f (g n) (f n acc t) c
+ | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
- | Proj (p,c) -> f n acc c
+ | Proj (_p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+ let n' = CArray.fold_left2 (fun c _n _t -> g 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 (fun c n t -> g c) n lna tl in
+ let n' = CArray.fold_left2 (fun c _n _t -> g 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
@@ -503,7 +503,79 @@ let fold_constr_with_binders g f n acc c =
not recursive and the order with which subterms are processed is
not specified *)
-let map f c = match kind c with
+let rec map_under_context f n d =
+ if n = 0 then f d else
+ match kind d with
+ | LetIn (na,b,t,c) ->
+ let b' = f b in
+ let t' = f t in
+ let c' = map_under_context f (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 t in
+ let b' = map_under_context f (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 f ci bl =
+ let nl = Array.map List.length ci.ci_pp_info.cstr_tags in
+ let bl' = Array.map2 (map_under_context f) nl bl in
+ if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate f ci p =
+ map_under_context f (List.length ci.ci_pp_info.ind_tags) p
+
+let rec map_under_context_with_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_binders g f (g 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_binders g f (g 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_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_binders g f l) tags bl in
+ if Array.for_all2 (==) bl' bl then bl else 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_gen userview f c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c
| Cast (b,k,t) ->
@@ -540,6 +612,12 @@ let map f c = match kind c with
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
@@ -557,6 +635,9 @@ let map f c = match kind c with
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
+
(* Like {!map} but with an accumulator. *)
let fold_map f accu c = match kind c with
@@ -882,11 +963,11 @@ let constr_ord_int f t1 t2 =
| LetIn _, _ -> -1 | _, LetIn _ -> 1
| App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
| App _, _ -> -1 | _, App _ -> 1
- | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2
+ | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2
| Const _, _ -> -1 | _, Const _ -> 1
- | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2
+ | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2
| Ind _, _ -> -1 | _, Ind _ -> 1
- | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2
+ | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2
| Construct _, _ -> -1 | _, Construct _ -> 1
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
@@ -1145,9 +1226,9 @@ let rec hash t =
combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
| Case (_ , p, c, bl) ->
combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl))
- | Fix (ln ,(_, tl, bl)) ->
+ | Fix (_ln ,(_, tl, bl)) ->
combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
- | CoFix(ln, (_, tl, bl)) ->
+ | CoFix(_ln, (_, tl, bl)) ->
combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
| Meta n -> combinesmall 15 n
| Rel n -> combinesmall 16 n
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:30:25 +0000