- 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 (lazy("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 (lazy("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', (m1 == m1' && m2 == m2') (* delta = 0 *)
+ 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