diff options
| -rw-r--r-- | library/redinfo.ml | 14 | ||||
| -rw-r--r-- | library/redinfo.mli | 3 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 45 |
3 files changed, 27 insertions, 35 deletions
diff --git a/library/redinfo.ml b/library/redinfo.ml index f289273ec..0ea9cdd92 100644 --- a/library/redinfo.ml +++ b/library/redinfo.ml @@ -9,7 +9,8 @@ open Constant open Reduction type constant_evaluation = - | Elimination of (int * constr) list * int * bool + | EliminationFix of (int * constr) list * int + | EliminationCases of int | NotAnElimination let eval_table = ref Spmap.empty @@ -45,20 +46,17 @@ let compute_consteval c = raise Elimconst) l in if list_distinct (List.map fst li) then - (li,n,true) + EliminationFix (li,n) else raise Elimconst | (DOPN(MutCase _,_) as mc,lapp) -> (match destCase mc with - | (_,_,Rel _,_) -> ([],n,false) + | (_,_,Rel _,_) -> EliminationCases n | _ -> raise Elimconst) | _ -> raise Elimconst in - try - let (lv,n,b) = srec 0 [] c in - Elimination (lv,n,b) - with Elimconst -> - NotAnElimination + try srec 0 [] c + with Elimconst -> NotAnElimination let constant_eval sp = try diff --git a/library/redinfo.mli b/library/redinfo.mli index 3f71baa98..1b600e57b 100644 --- a/library/redinfo.mli +++ b/library/redinfo.mli @@ -12,7 +12,8 @@ open Term (section~\refsec{tacred}). *) type constant_evaluation = - | Elimination of (int * constr) list * int * bool + | EliminationFix of (int * constr) list * int + | EliminationCases of int | NotAnElimination val constant_eval : section_path -> constant_evaluation diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 6054eaacf..7ec56e3ad 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -15,12 +15,6 @@ open Redinfo exception Elimconst exception Redelimination -let is_elim c = - let (sp, _) = destConst c in - match constant_eval sp with - | NotAnElimination -> raise Elimconst - | Elimination (lv,n,b) -> (lv,n,b) - let rev_firstn_liftn fn ln = let rec rfprec p res l = if p = 0 then @@ -33,26 +27,25 @@ let rev_firstn_liftn fn ln = rfprec fn [] let make_elim_fun f largs = - try - let (lv,n,b) = is_elim f - and ll = List.length largs in - if ll < n then raise Redelimination; - if b then - let labs,_ = list_chop n largs in - let p = List.length lv in - let la' = list_map_i - (fun q aq -> - try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) - with Failure _ -> aq) 1 - (List.map (lift p) labs) - in - list_fold_left_i - (fun i c (k,a) -> - DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a), - DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv - else - f - with Elimconst | Failure _ -> + try + let (sp, _) = destConst f in + match constant_eval sp with + | EliminationCases n when List.length largs >= n -> f + | EliminationFix (lv,n) when List.length largs >= n -> + let labs,_ = list_chop n largs in + let p = List.length lv in + let la' = list_map_i + (fun q aq -> + try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) + with Failure _ -> aq) 1 + (List.map (lift p) labs) + in + list_fold_left_i + (fun i c (k,a) -> + DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a), + DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv + | _ -> raise Redelimination + with Failure _ -> raise Redelimination (* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make |