diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:26:35 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:26:35 +0000 |
commit | d9dc86a6f7194c2e7ea704c95495955ca4f4b08d (patch) | |
tree | 6b113a93fa17e0383d72a9c88b5bce270bab3754 /kernel | |
parent | f08382bf7efb1195e8bbdf3602a910bd0bc6ea96 (diff) |
Ajout map_constr_with_full_binders et strong pour Simpl
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/reduction.ml | 12 | ||||
-rw-r--r-- | kernel/term.ml | 27 | ||||
-rw-r--r-- | kernel/term.mli | 10 |
3 files changed, 39 insertions, 10 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index d496a9e49..a5f9114a8 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -108,10 +108,10 @@ let stack_reduction_of_reduction red_fun env sigma s = let t = red_fun env sigma (app_stack s) in whd_stack t -(* BUGGE : NE PREND PAS EN COMPTE LES DEFS LOCALES *) -let strong whdfun env sigma = - let rec strongrec t = map_constr strongrec (whdfun env sigma t) in - strongrec +let strong whdfun env sigma t = + let rec strongrec env t = + map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in + strongrec env t let local_strong whdfun = let rec strongrec t = map_constr strongrec (whdfun t) in @@ -270,7 +270,6 @@ let reduce_fix whdfun fix stack = let whd_state_gen flags env sigma = let rec whrec (x, stack as s) = match kind_of_term x with -(* | IsRel n when red_delta flags -> (match lookup_rel_value n env with | Some body -> whrec (lift n body, stack) @@ -279,7 +278,6 @@ let whd_state_gen flags env sigma = (match lookup_named_value id env with | Some body -> whrec (body, stack) | None -> s) -*) | IsEvar ev when red_evar flags -> (match existential_opt_value sigma ev with | Some body -> whrec (body, stack) @@ -331,7 +329,7 @@ let whd_state_gen flags env sigma = let local_whd_state_gen flags = let rec whrec (x, stack as s) = match kind_of_term x with - | IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack + | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack | IsCast (c,_) -> whrec (c, stack) | IsApp (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> diff --git a/kernel/term.ml b/kernel/term.ml index e29a9edcd..ff96a8e15 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -666,9 +666,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with time being almost those of the ML representation (except for (co-)fixpoint) *) -(* Ocaml does not guarantee Array.map is LR (even if so), then we rewrite it *) -let array_map_left f a = - let l = Array.length a in +let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *) + let l = Array.length a in (* (even if so), then we rewrite it *) if l = 0 then [||] else begin let r = Array.create l (f a.(0)) in for i = 1 to l - 1 do @@ -714,6 +713,28 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with let tl', bl' = array_map_left_pair (f l) tl (f l') bl in mkCoFix (ln,(tl',lna,bl')) +(* strong *) +let map_constr_with_full_binders g f l c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsCast (c,t) -> mkCast (f l c, f l t) + | IsProd (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c) + | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c) + | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g (na,Some b,t) l) c) + | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al) + | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) + | IsConst (c,al) -> mkConst (c, Array.map (f l) al) + | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) + | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) + | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) + | IsFix (ln,(tl,lna,bl)) -> + let tll = Array.to_list tl in + let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in + mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsCoFix(ln,(tl,lna,bl)) -> + let tll = Array.to_list tl in + let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in + mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) diff --git a/kernel/term.mli b/kernel/term.mli index f909b90da..d4dbd8ce1 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -631,6 +631,16 @@ val map_constr_with_named_binders : val map_constr_with_binders_left_to_right : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr +(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate + subterms of [c]; it carries an extra data [l] (typically a name + list) which is processed by [g na] (which typically cons [na] to + [l]) at each binder traversal (with name [na]); it is not recursive + and the order with which subterms are processed is not specified *) + +val map_constr_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> + 'a -> constr -> constr + (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) |