diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 33 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 5 | ||||
| -rw-r--r-- | pretyping/termops.ml | 13 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 |
4 files changed, 39 insertions, 14 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ef0867f7c4..10322c156c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,6 +23,15 @@ open Closure open Cbv open Rawterm +(* Errors *) + +type reduction_tactic_error = + InvalidAbstraction of env * constr * (env * Type_errors.type_error) + +exception ReductionTacticError of reduction_tactic_error + +(* Evaluable reference *) + exception Elimconst exception Redelimination @@ -619,7 +628,7 @@ let contextually byhead (locs,c) f env sigma t = in let t' = traverse (env,c) t in if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then - errorlabstrm "contextually" (str "Too few occurences"); + error_invalid_occurrence locs; t' (* linear bindings (following pretty-printer) of the value of name in c. @@ -683,7 +692,7 @@ let rec substlin env name n ol c = let (n2,ol2,c2') = substlin env name n1 ol1 c2 in (n2,ol2,mkProd (na,c1',c2'))) - | Case (ci,p,d,llf) -> + | Case (ci,p,d,llf) -> let rec substlist nn oll = function | [] -> (nn,oll,[]) | f::lfe -> @@ -694,11 +703,12 @@ let rec substlin env name n ol c = let (nn2,oll2,lfe') = substlist nn1 oll1 lfe in (nn2,oll2,f'::lfe')) in - let (n1,ol1,p') = substlin env name n ol p in (* ATTENTION ERREUR *) - (match ol1 with (* si P pas affiche *) - | [] -> (n1,[],mkCase (ci, p', d, llf)) + (* p is printed after d in v8 syntax *) + let (n1,ol1,d') = substlin env name n ol d in + (match ol1 with + | [] -> (n1,[],mkCase (ci, p, d', llf)) | _ -> - let (n2,ol2,d') = substlin env name n1 ol1 d in + let (n2,ol2,p') = substlin env name n1 ol1 p in (match ol2 with | [] -> (n2,[],mkCase (ci, p', d', llf)) | _ -> @@ -746,8 +756,8 @@ let unfoldoccs env sigma (occl,name) c = | (_,[],uc) -> nf_betaiota uc | (1,_,_) -> error ((string_of_evaluable_ref env name)^" does not occur") - | _ -> error ("bad occurrence numbers of " - ^(string_of_evaluable_ref env name)) + | (_,l,_) -> + error_invalid_occurrence l (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = @@ -790,8 +800,11 @@ let abstract_scheme env sigma (locc,a) c = let pattern_occs loccs_trm env sigma c = let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in - let _ = Typing.type_of env sigma abstr_trm in - applist(abstr_trm, List.map snd loccs_trm) + try + let _ = Typing.type_of env sigma abstr_trm in + applist(abstr_trm, List.map snd loccs_trm) + with Type_errors.TypeError (env',t) -> + raise (ReductionTacticError (InvalidAbstraction (env,abstr_trm,(env',t)))) (* Used in several tactics. *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 423a04723d..9ffa1dfb76 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -18,6 +18,11 @@ open Closure open Rawterm (*i*) +type reduction_tactic_error = + InvalidAbstraction of env * constr * (env * Type_errors.type_error) + +exception ReductionTacticError of reduction_tactic_error + (*s Reduction functions associated to tactics. \label{tacred} *) val is_evaluable : env -> evaluable_global_reference -> bool diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 95bdb74c51..597ddac57c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -615,6 +615,11 @@ let replace_term = replace_term_gen eq_constr bindings is done. The list may contain only negative occurrences that will not be substituted. *) +let error_invalid_occurrence l = + errorlabstrm "" + (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ + prlist_with_sep spc int l) + let subst_term_occ_gen locs occ c t = let maxocc = List.fold_right max locs 0 in let pos = ref occ in @@ -646,8 +651,8 @@ let subst_term_occ locs c t = t else 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"); + let rest = List.filter (fun o -> o >= nbocc or o <= -nbocc) locs in + if rest <> [] then error_invalid_occurrence rest; t' let subst_term_occ_decl locs c (id,bodyopt,typ as d) = @@ -661,8 +666,8 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) = else 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"); + let rest = List.filter (fun o -> o >= nbocc' or o <= -nbocc') locs in + if rest <> [] then error_invalid_occurrence rest; (id,Some body',t') diff --git a/pretyping/termops.mli b/pretyping/termops.mli index cd1cce1bae..5ecd0b685f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -124,6 +124,8 @@ val subst_term_occ : int list -> constr -> types -> types val subst_term_occ_decl : int list -> constr -> named_declaration -> named_declaration +val error_invalid_occurrence : int list -> 'a + (* Alternative term equalities *) val eta_reduce_head : constr -> constr val eta_eq_constr : constr -> constr -> bool |