| NCic.Const (Ref.Ref (_,Ref.Def h))
| NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
| NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
- | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
- | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> 0, true
- | _ -> 0, false
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+ | _ -> 0
in
let put_in_whd m1 m2 =
NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
false (* not in normal form *)
in
let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
- let h1, flex1 = height_of t1 in
- let h2, flex2 = height_of t2 in
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in
let delta =
- if flex1 then max 0 (h2 - 1) else
- if flex2 then max 0 (h1 - 1) else
+ 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
- m1', m2', (m1' == m1 && m2' == m2) || delta = 0
- (* if we have as heads two Fix of height n>0, they may or may not
- * reduce, depending on their rec argument... we thus check if
- * something changed or not. This relies on the reduction machine
- * preserving the original machine if it performs no action *)
+ 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
in
let rec unif_machines metasenv subst =
function