diff options
| -rw-r--r-- | engine/termops.ml | 28 | ||||
| -rw-r--r-- | engine/termops.mli | 10 | ||||
| -rw-r--r-- | kernel/term.ml | 19 | ||||
| -rw-r--r-- | kernel/term.mli | 7 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 13 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 |
10 files changed, 45 insertions, 38 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index ebd9d939a..5716a19dd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -846,6 +846,34 @@ let decompose_prod_letin : constr -> int * rel_context * constr = | _ -> i,l,c in prodec_rec 0 [] +(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction + * gives n (casts are ignored) *) +let nb_lam = + let rec nbrec n c = match kind_of_term c with + | Lambda (_,_,c) -> nbrec (n+1) c + | Cast (c,_,_) -> nbrec n c + | _ -> n + in + nbrec 0 + +(* similar to nb_lam, but gives the number of products instead *) +let nb_prod = + let rec nbrec n c = match kind_of_term c with + | Prod (_,_,c) -> nbrec (n+1) c + | Cast (c,_,_) -> nbrec n c + | _ -> n + in + nbrec 0 + +let nb_prod_modulo_zeta x = + let rec count n c = + match kind_of_term c with + Prod(_,_,t) -> count (n+1) t + | LetIn(_,a,_,t) -> count n (subst1 a t) + | Cast(c,_,_) -> count n c + | _ -> n + in count 0 x + let align_prod_letin c a : rel_context * constr = let (lc,_,_) = decompose_prod_letin c in let (la,l,a) = decompose_prod_letin a in diff --git a/engine/termops.mli b/engine/termops.mli index 6c680005d..5d812131e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -174,6 +174,16 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst val decompose_prod_letin : constr -> int * rel_context * constr val align_prod_letin : constr -> constr -> rel_context * constr +(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction + gives {% $ %}n{% $ %} (casts are ignored) *) +val nb_lam : constr -> int + +(** Similar to [nb_lam], but gives the number of products instead *) +val nb_prod : constr -> int + +(** Similar to [nb_prod], but zeta-contracts let-in on the way *) +val nb_prod_modulo_zeta : constr -> int + (** Get the last arg of a constr intended to be an application *) val last_arg : constr -> constr diff --git a/kernel/term.ml b/kernel/term.ml index 33ed25fe1..7d47c4609 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -616,25 +616,6 @@ let decompose_lam_n_decls n = in lamdec_rec empty_rel_context n -(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction - * gives n (casts are ignored) *) -let nb_lam = - let rec nbrec n c = match kind_of_term c with - | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - -(* similar to nb_lam, but gives the number of products instead *) -let nb_prod = - let rec nbrec n c = match kind_of_term c with - | Prod (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - let prod_assum t = fst (decompose_prod_assum t) let prod_n_assum n t = fst (decompose_prod_n_assum n t) let strip_prod_assum t = snd (decompose_prod_assum t) diff --git a/kernel/term.mli b/kernel/term.mli index 2bb811060..69adb517a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -308,13 +308,6 @@ val decompose_lam_n_assum : int -> constr -> rel_context * constr (** Idem, counting let-ins *) val decompose_lam_n_decls : int -> constr -> rel_context * constr -(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction - gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : constr -> int - -(** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int - (** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c9dd18a2f..5b9f82aa5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -9,6 +9,7 @@ open Names open Declarations open Pp open Tacmach +open Termops open Proof_type open Tacticals open Tactics diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d074bbabd..363dd1b3b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,6 +19,7 @@ open Tactics open Indfun_common open Tacmach open Misctypes +open Termops (* Some pretty printing function for debugging purpose *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index dd5381c76..6867939c2 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -29,6 +29,7 @@ open Proof_type open Pfedit open Glob_term open Pretyping +open Termops open Constrintern open Misctypes open Genredexpr diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index bf8f34855..ff1ed4030 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -19,6 +19,7 @@ open Tactics open Errors open Util open Evd +open Termops open Equality open Misctypes open Sigma.Notations diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4fb206ec9..a2275b08f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -45,15 +45,6 @@ open Misctypes open Proofview.Notations open Sigma.Notations -let nb_prod x = - let rec count n c = - match kind_of_term c with - Prod(_,_,t) -> count (n+1) t - | LetIn(_,a,_,t) -> count n (subst1 a t) - | Cast(c,_,_) -> count n c - | _ -> n - in count 0 x - let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost @@ -1511,7 +1502,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod concl in + let concl_nprod = nb_prod_modulo_zeta concl in let rec try_main_apply with_destruct c = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -1520,7 +1511,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try - let n = nb_prod thm_ty - nprod in + let n = nb_prod_modulo_zeta thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index bfa49fab8..cac81a939 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -528,7 +528,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - let m = nb_prod fixtype in + let m = Termops.nb_prod fixtype in let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx |