From: Enrico Tassi Date: Wed, 14 May 2008 16:27:16 +0000 (+0000) Subject: partial implementation of reduction up to a given height X-Git-Tag: make_still_working~5209 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=81ea97cc0dba73a41e38c97d768c78b68126b0bc;p=helm.git partial implementation of reduction up to a given height --- diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 32c553367..9cae8d409 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -520,7 +520,7 @@ let are_convertible whd ?(subst=[]) = (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)) l1 l2 - with Invalid_argument _ -> false) + with Invalid_argument _ -> assert false) | C.Meta (n1,l1), _ -> (try @@ -553,26 +553,41 @@ let are_convertible whd ?(subst=[]) = if aux2 test_equality_only t1 t2 then true else - 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 (h,_,_)) -> h + | NCic.Appl (NCic.Const (NReference.Ref (h,_,_))::_) -> h + | _ -> 0 in - convert_machines - [R.reduce ~delta:0 ~subst context (0,[],t1,[]), - R.reduce ~delta:0 ~subst context (0,[],t2,[])] + let min_delta (k1,env1,t1,s1) (k2,env2,t2,s2) = + let h1 = height_of t1 and h2 = height_of t2 in + if h1 > h2 then + R.reduce ~delta:(h2+1) ~subst context (k1,env1,t1,s1), + (k2,env2,t2,s2), h2+1 + else if h1 < h2 then + (k1,env1,t1,s1), + R.reduce ~delta:(h1+1) ~subst context (k2,env2,t2,s2), + h1+1 + else + R.reduce ~delta:(max 0 (h1-1)) ~subst context (k1,env1,t1,s1), + R.reduce ~delta:(max 0 (h1-1)) ~subst context (k2,env2,t2,s2), + (max 0 (h1-1)) + in + let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) todo = + (aux2 test_equality_only + (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) && + try + match List.combine s1 s2 @ todo with + | [] -> true + | (t1,t2) :: todo -> + let t1 = RS.from_stack t1 and t2 = RS.from_stack t2 in + convert_machines (min_delta t1 t2) todo + 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) todo) + in + convert_machines (min_delta (0,[],t1,[]) (0,[],t2,[])) [] in aux false ;;