From 5ae174c1243ae83ceeda6f2641d12565842d250f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 May 2008 16:09:43 +0000 Subject: [PATCH] First implementation of irrelevance in conversion. --- .../components/ng_kernel/nCicReduction.ml | 24 +++++++++++++++---- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index b6360a0c7..18e9f92cb 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -535,6 +535,15 @@ let are_convertible whd ?(subst=[]) = aux test_eq_only context t1 term with NCicUtils.Subst_not_found _ -> false) + | (C.Appl (C.Const r1::tl1), C.Appl (C.Const r2::tl2)) -> + r1 = r2 && + let relevance = NCicEnvironment.get_relevance r1 in + (try + HExtlib.list_forall_default3 + (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) + tl1 tl2 true relevance + with Invalid_argument _ -> false) + | (C.Appl l1, C.Appl l2) -> (try List.for_all2 (aux test_eq_only context) l1 l2 with Invalid_argument _ -> false) @@ -571,12 +580,17 @@ let are_convertible whd ?(subst=[]) = 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 - List.for_all - (fun (t1,t2) -> - let t1 = RS.from_stack t1 and t2 = RS.from_stack t2 in - convert_machines (small_delta_step t1 t2)) - (List.combine s1 s2) + 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 -- 2.39.2