- let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
- NCicReduction.reduce_machine ~delta ~subst context m1,
- NCicReduction.reduce_machine ~delta ~subst context m2,
- delta
+ let delta =
+ if flexible [t1] then max 0 (h2 - 1) else
+ if flexible [t2] then max 0 (h1 - 1) else
+ if h1 = h2 then max 0 (h1 -1) else min h1 h2
+ in
+ pp ("DELTA STEP TO: " ^ string_of_int delta);
+ let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+ let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+ if (m1' == m1 && m2' == m2 && delta > 0) then
+ (* if we have as heads a Fix of height n>m>0 and another term of height
+ * m, we set delta = m. The Fix may or may not reduce, depending on its
+ * rec argument. if no reduction was performed we decrease delta to m-1
+ * to reduce the other term *)
+ let delta = delta - 1 in
+ pp ("DELTA STEP TO: " ^ string_of_int delta);
+ let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+ let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+ m1', m2', (m1 == m1' && m2 == m2') || delta = 0
+ else m1', m2', delta = 0