From 8097a4b158730b042f2d00bc91419ccae6bb71d5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 May 2008 12:39:00 +0000 Subject: [PATCH] Major code semplification and bugs removed (thanks to a better invariant): small_delta_step always put the terms in WHNF, even if it can do that with delta > 0. Terms in WHNF, delta=0 that are not head-alpha convertible and tail-machine convertible are not convertible. --- .../components/ng_kernel/nCicReduction.ml | 30 ++++++++----------- 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 99afc2aa8..6f94e4a77 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -554,23 +554,19 @@ let are_convertible whd ?(subst=[]) = true else let height_of = function - | NCic.Const (NReference.Ref (_,NReference.Def h)) -> h - | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h))) -> h - | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_) -> h + | 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 (k1,env1,t1,s1 as m1) (k2,env2,t2,s2 as m2) = - let h1 = height_of t1 and h2 = height_of t2 in - if h1 > h2 then - R.reduce ~delta:h2 ~subst context (k1,env1,t1,s1), m2, h2 - else if h1 < h2 then - m1, R.reduce ~delta:h1 ~subst context (k2,env2,t2,s2), h1 - else - let delta = max 0 (h1-1) in - R.reduce ~delta ~subst context (k1,env1,t1,s1), - R.reduce ~delta ~subst context (k2,env2,t2,s2), - delta + 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 @@ -582,11 +578,9 @@ let are_convertible whd ?(subst=[]) = convert_machines (small_delta_step t1 t2)) (List.combine s1 s2) with Invalid_argument _ -> false) || - (let red delta = R.reduce ~delta ~subst context in - if delta = 0 then - alpha_eq test_eq_only (R.unwind (red 0 m1)) (R.unwind (red 0 m2)) - else + (delta > 0 && let delta = delta - 1 in + let red = R.reduce ~delta ~subst context in convert_machines (red delta m1,red delta m2,delta)) in convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[])) -- 2.39.2