let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" c t) in
let csno, vsno = List.length classes, List.length vs in
if csno < vsno then
- let vvs, vs = HEL.split_nth "PO 1" csno vs in
+ let vvs, vs = HEL.split_nth csno vs in
let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
opt_proof g (info st "Optimizer: anticipate 2") true c x
else match conclusion, List.rev vs with
let eliminator = H.get_default_eliminator c uri tyno outty in
let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
let ps, sort_disp = H.get_ind_parameters c arg in
- let lps, rps = HEL.split_nth "PO 2" lpsno ps in
+ let lps, rps = HEL.split_nth lpsno ps in
let rpsno = List.length rps in
if rpsno = 0 && sort_disp = 0 then
(* FG: the transformation is not possible, we fall back into the plain case *)
opt_mutcase_plain g st es c uri tyno outty arg cases
else
let predicate = clear_absts rpsno (1 - sort_disp) outty in
+ if H.occurs c ~what:(C.Rel 0) ~where:predicate then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+ opt_mutcase_plain g st es c uri tyno outty arg cases
+ else
let is_recursive t =
I.S.mem tyno (I.get_mutinds_of_uri uri t)
in
in
let lifted_cases = List.map2 map2 cases constructors in
let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
- let x = H.refine c (C.Appl args) in
- opt_proof g (info st "Optimizer: remove 3") es c x
+ try
+ let x = H.refine c (C.Appl args) in
+ opt_proof g (info st "Optimizer: remove 3") es c x
+ with e ->
+(* FG: the transformation is not possible, we fall back into the plain case *)
+ let st = info st ("Optimizer: refine_error: " ^ Printexc.to_string e) in
+ opt_mutcase_plain g st es c uri tyno outty arg cases
and opt_mutcase_plain g st es c uri tyno outty arg cases =
let g st v =