- let rec convert_machines = function
- | [] -> true
- | ((k1,env1,h1,s1),(k2,env2,h2,s2))::tl ->
- aux2 test_equality_only
- (R.unwind (k1,env1,h1,[])) (R.unwind (k2,env2,h2,[])) &&
- let problems =
- let red_stack =
- List.map
- (fun si-> R.reduce ~delta:0 ~subst context(RS.from_stack si))
- in
- try Some (List.combine (red_stack s1) (red_stack s2) @ tl)
- with Invalid_argument _ -> None
- in
- match problems with
- | None -> false
- | Some problems -> convert_machines problems
+ let height_of = function
+ | NCic.Const (NReference.Ref (_,NReference.Def h))
+ | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h)))
+ | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_)
+ | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
+ | _ -> 0
+ in
+ let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in
+ let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
+ R.reduce ~delta ~subst context m1,
+ R.reduce ~delta ~subst context m2,
+ delta
+ in
+ let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
+ (alpha_eq test_eq_only
+ (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
+ let relevance =
+ match t1 with
+ C.Const r -> NCicEnvironment.get_relevance r
+ | _ -> [] in
+ try
+ HExtlib.list_forall_default3
+ (fun t1 t2 b ->
+ not b ||
+ let t1 = RS.from_stack t1 in
+ let t2 = RS.from_stack t2 in
+ convert_machines (small_delta_step t1 t2)) s1 s2 true relevance
+ with Invalid_argument _ -> false) ||
+ (delta > 0 &&
+ let delta = delta - 1 in
+ let red = R.reduce ~delta ~subst context in
+ convert_machines (red m1,red m2,delta))