diff options
| -rw-r--r-- | pretyping/inductiveops.ml | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 97 | ||||
| -rw-r--r-- | pretyping/termops.mli | 17 | ||||
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 4 | ||||
| -rw-r--r-- | toplevel/record.ml | 1 |
8 files changed, 43 insertions, 88 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 483b7cfd20..f14f219229 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -49,14 +49,14 @@ let mkAppliedInd (IndType ((ind,params), realargs)) = applist (mkInd ind,params@realargs) +(* Does not consider imbricated or mutually recursive types *) let mis_is_recursive_subset listind rarg = let rec one_is_rec rvec = List.exists (fun ra -> match dest_recarg ra with | Mrec i -> List.mem i listind - | Imbr _ -> array_exists one_is_rec (dest_subterms ra) - | Norec -> false) rvec + | _ -> false) rvec in array_exists one_is_rec (dest_subterms rarg) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 95acf3a6c1..26a627d178 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -756,7 +756,7 @@ let abstract_scheme env sigma (locc,a) t = if occur_meta a then mkLambda (na,ta,t) else - mkLambda (na, ta,subst_term_occ env locc a t) + mkLambda (na, ta,subst_term_occ locc a t) let pattern_occs loccs_trm env sigma c = diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 442eb7a5dc..05e60912b2 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -286,15 +286,6 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with then cstr else mkCoFix (ln,(lna,tl',bl')) - -(* Equality modulo let reduction *) -let rec zeta_eq_constr m n = - (m==n) or - match kind_of_term m, kind_of_term n with - | LetIn(_,v1,_,b1),_ -> zeta_eq_constr (subst1 v1 b1) n - | _,LetIn(_,v2,_,b2) -> zeta_eq_constr m (subst1 v2 b2) - | _ -> compare_constr zeta_eq_constr m n - (***************************) (* occurs check functions *) (***************************) @@ -366,7 +357,7 @@ let free_rels m = let dependent m t = let rec deprec m t = - if zeta_eq_constr m t then + if eq_constr m t then raise Occur else iter_constr_with_binders (lift 1) deprec m t @@ -384,53 +375,29 @@ let rec subst_meta bl c = | Meta i -> (try List.assoc i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c -(* Equality modulo let reduction *) -let rec whd_locals env c = - match kind_of_term c with - Rel i -> - (try - (match lookup_rel i env with - (_,Some v,_) -> whd_locals env (lift i v) - | _ -> c) - with Not_found -> c) - | Var id -> - (try - (match lookup_named id env with - (_,Some v,_) -> whd_locals env v - | _ -> c) - with Not_found -> c) - | _ -> c - -(* Expand de Bruijn indices bound to a value *) -let rec nf_locals env c = - map_constr_with_full_binders push_rel nf_locals env (whd_locals env c) - -(* compare terms modulo expansion of let and local variables *) -let compare_zeta env m n = zeta_eq_constr m (nf_locals env n) - (* First utilities for avoiding telescope computation for subst_term *) -let prefix_application eq_fun (e,k,c) (t : constr) = +let prefix_application eq_fun (k,c) (t : constr) = let c' = collapse_appl c and t' = collapse_appl t in match kind_of_term c', kind_of_term t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun e c' (mkApp (f2, Array.sub cl2 0 l1)) then + && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) else None | _ -> None -let my_prefix_application eq_fun (e,k,c) (by_c : constr) (t : constr) = +let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = let c' = collapse_appl c and t' = collapse_appl t in match kind_of_term c', kind_of_term t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun e c' (mkApp (f2, Array.sub cl2 0 l1)) then + && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1))) else None @@ -441,49 +408,43 @@ let my_prefix_application eq_fun (e,k,c) (by_c : constr) (t : constr) = term [c] in a term [t] *) (*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*) -let subst_term_gen eq_fun env c t = - let rec substrec (e,k,c as kc) t = +let subst_term_gen eq_fun c t = + let rec substrec (k,c as kc) t = match prefix_application eq_fun kc t with | Some x -> x | None -> - (if eq_fun e c t then mkRel k + if eq_fun c t then mkRel k else - let red_t = whd_locals env t in - let red_t' = - map_constr_with_full_binders - (fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c)) - substrec kc red_t in - if red_t == red_t' then t else red_t') + map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t in - substrec (env,1,nf_locals env c) t + substrec (1,c) t (* Recognizing occurrences of a given (closed) subterm in a term : [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed) term [c1] in a term [t] *) (*i Meme remarque : a priori [c] n'est pas forcement clos i*) -let replace_term_gen eq_fun env c by_c in_t = - let rec substrec (e,k,c as kc) t = +let replace_term_gen eq_fun c by_c in_t = + let rec substrec (k,c as kc) t = match my_prefix_application eq_fun kc by_c t with | Some x -> x | None -> - (if eq_fun e c t then (lift k by_c) else - map_constr_with_full_binders - (fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c)) + (if eq_fun c t then (lift k by_c) else + map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t) in - substrec (env,0,nf_locals env c) in_t + substrec (0,c) in_t -let subst_term = subst_term_gen (fun _ -> eq_constr) empty_env +let subst_term = subst_term_gen eq_constr -let replace_term = replace_term_gen (fun _ -> eq_constr) empty_env +let replace_term = replace_term_gen eq_constr (* Substitute only a list of locations locs, the empty list is interpreted as substitute all, if 0 is in the list then no substitution is done. The list may contain only negative occurrences that will not be substituted. *) -let subst_term_occ_gen env locs occ c t = +let subst_term_occ_gen locs occ c t = let maxocc = List.fold_right max locs 0 in let pos = ref occ in let check = ref true in @@ -491,10 +452,10 @@ let subst_term_occ_gen env locs occ c t = if except & (List.exists (fun n -> n>=0) locs) then error "mixing of positive and negative occurences" else - let rec substrec (e,k,c as kc) t = + let rec substrec (k,c as kc) t = if (not except) & (!pos > maxocc) then t else - if compare_zeta e c t then + if eq_constr c t then let r = if except then if List.mem (- !pos) locs then t else (mkRel k) @@ -503,34 +464,34 @@ let subst_term_occ_gen env locs occ c t = in incr pos; r else map_constr_with_binders_left_to_right - (fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c)) + (fun d (k,c) -> (k+1,lift 1 c)) substrec kc t in - let t' = substrec (env,1,nf_locals env c) t in + let t' = substrec (1,c) t in (!pos, t') -let subst_term_occ env locs c t = +let subst_term_occ locs c t = if locs = [] then - subst_term_gen compare_zeta env c t + subst_term_gen eq_constr c t else if List.mem 0 locs then t else - let (nbocc,t') = subst_term_occ_gen env locs 1 c t in + let (nbocc,t') = subst_term_occ_gen locs 1 c t in if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then errorlabstrm "subst_term_occ" (str "Too few occurences"); t' -let subst_term_occ_decl env locs c (id,bodyopt,typ as d) = +let subst_term_occ_decl locs c (id,bodyopt,typ as d) = match bodyopt with - | None -> (id,None,subst_term_occ env locs c typ) + | None -> (id,None,subst_term_occ locs c typ) | Some body -> if locs = [] then (id,Some (subst_term c body),type_app (subst_term c) typ) else if List.mem 0 locs then d else - let (nbocc,body') = subst_term_occ_gen env locs 1 c body in - let (nbocc',t') = subst_term_occ_gen env locs nbocc c typ in + let (nbocc,body') = subst_term_occ_gen locs 1 c body in + let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then errorlabstrm "subst_term_occ_decl" (str "Too few occurences"); (id,Some body',t') diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 431e69e7f0..95d769c43f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -73,10 +73,6 @@ val free_rels : constr -> Intset.t (* Substitution of metavariables *) val subst_meta : (int * constr) list -> constr -> constr -(* Expansion of local definitions *) -val whd_locals : env -> constr -> constr -val nf_locals : env -> constr -> constr - (* [pop c] lifts by -1 the positive indexes in [c] *) val pop : constr -> constr @@ -84,20 +80,19 @@ val pop : constr -> constr reduction of let *) val dependent : constr -> constr -> bool val subst_term_gen : - (env -> constr -> constr -> bool) -> env -> constr -> constr -> constr + (constr -> constr -> bool) -> constr -> constr -> constr val replace_term_gen : - (env -> constr -> constr -> bool) -> - env -> constr -> constr -> constr -> constr + (constr -> constr -> bool) -> + constr -> constr -> constr -> constr val subst_term : constr -> constr -> constr val replace_term : constr -> constr -> constr -> constr val subst_term_occ_gen : - env -> int list -> int -> constr -> types -> int * types -val subst_term_occ : env -> int list -> constr -> types -> types + int list -> int -> constr -> types -> int * types +val subst_term_occ : int list -> constr -> types -> types val subst_term_occ_decl : - env -> int list -> constr -> named_declaration -> named_declaration + int list -> constr -> named_declaration -> named_declaration (* Alternative term equalities *) -val zeta_eq_constr : constr -> constr -> bool val eta_reduce_head : constr -> constr val eta_eq_constr : constr -> constr -> bool diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1a527cbeaa..66e3181a3c 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -36,7 +36,7 @@ let abstract_scheme env c l lname_typ = (fun t (locc,a) (na,_,ta) -> if occur_meta ta then error "cannot find a type for the generalisation" else if occur_meta a then lambda_name env (na,ta,t) - else lambda_name env (na,ta,subst_term_occ env locc a t)) + else lambda_name env (na,ta,subst_term_occ locc a t)) c (List.rev l) lname_typ diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 62c95b53fe..572933eef8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -671,7 +671,7 @@ let letin_abstract id c occs gl = match occurrences_of_hyp hyp occs with | None -> raise Not_found | Some occ -> - let newdecl = subst_term_occ_decl env occ c d in + let newdecl = subst_term_occ_decl occ c d in if d = newdecl then if not (everywhere occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) @@ -690,7 +690,7 @@ let letin_abstract id c occs gl = let (depdecls,marks),_ = List.fold_left compute_marks (([],[]),None) ctxt' in let ccl = match occurrences_of_goal occs with | None -> pf_concl gl - | Some occ -> subst1 (mkVar id) (subst_term_occ env occ c (pf_concl gl)) + | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in (depdecls,marks,ccl) diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 4815028c0e..5cdfd96ce5 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -219,7 +219,7 @@ Apply pow_lt; Assumption. Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H8 := (sym_eq ? ? ? H7); Elim (fact_neq_0 ? H8). Clear Un Vn; Apply INR_le; Simpl. Induction M_nat. -Assert H6 := (archimed (Rabsolu x)); Elim H6; Intros; Fold M in H6. +Assert H6 := (archimed (Rabsolu x)); Fold M in H6; Elim H6; Intros. Rewrite H4 in H7; Rewrite <- INR_IZR_INZ in H7. Simpl in H7; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H2 H7)). Replace R1 with (INR (S O)); [Apply le_INR | Reflexivity]; Apply le_n_S; Apply le_O_n. @@ -515,4 +515,4 @@ Left; Assumption. Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0. Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity. Apply Rgt_RO_Ropp; Assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/toplevel/record.ml b/toplevel/record.ml index 9edb4e1d54..60855b2fc7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -205,7 +205,6 @@ let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) = let extract_name = function Vernacexpr.AssumExpr(id,_) -> id | Vernacexpr.DefExpr (id,_,_) -> id in let allnames = idstruc::idps@(List.map extract_name fs) in if not (list_distinct allnames) then error "Two objects have the same name"; - if occur_fields idstruc fs then error "A record cannot be recursive"; (* Now, younger decl in params and fields is on top *) let params,fields = typecheck_params_and_fields ps fs in (* let args = List.map mkVar idps in*) |