From 57ed1abc0fddb7644c396e15dd13600eef1f928f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 May 2008 09:17:02 +0000 Subject: [PATCH] thanks to the fact that we convert well typed term and that we convert only types, by inversion we know that types of lambdas source are convertible if in head position --- helm/software/components/extlib/hExtlib.ml | 5 +++++ helm/software/components/extlib/hExtlib.mli | 1 + helm/software/components/ng_kernel/nCicReduction.ml | 12 ++++++++++-- 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 0d19524dc..c16b11159 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -515,3 +515,8 @@ let chop_prefix prefix s = let touch s = try close_out(open_out s) with Sys_error _ -> () ;; + +let rec mk_list x = function + | 0 -> [] + | n -> x :: mk_list x (n-1) +;; diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index 1e2d8e047..594a80027 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -108,6 +108,7 @@ val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c - * @raise Failure when List.length l < n *) val split_nth: int -> 'a list -> 'a list * 'a list +val mk_list: 'a -> int -> 'a list (** {2 Debugging & Profiling} *) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index c6abbd0e0..4ff6af692 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -188,8 +188,9 @@ let are_convertible ?(subst=[]) = | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> aux true context s1 s2 && aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 - | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - aux true context s1 s2 && + | (C.Lambda (name1,s1,t1), C.Lambda(_,_,t2)) -> + (* thanks to inversion of well typedness, the source + * of these lambdas must be already convertible *) aux test_eq_only ((name1, C.Decl s1)::context) t1 t2 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> aux test_eq_only context ty1 ty2 && @@ -224,6 +225,13 @@ let are_convertible ?(subst=[]) = | (C.Appl (C.Const r1::tl1), C.Appl (C.Const r2::tl2)) -> r1 = r2 && let relevance = NCicEnvironment.get_relevance r1 in + let relevance = + match r1 with + | Ref.Ref (_,Ref.Con (_,_,lno)) -> + let _,relevance = HExtlib.split_nth lno relevance in + HExtlib.mk_list false lno @ relevance + | _ -> relevance + in (try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) -- 2.39.2