From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 May 2008 09:17:02 +0000 (+0000)
Subject: thanks to the fact that we convert well typed term and that
X-Git-Tag: make_still_working~5101
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57ed1abc0fddb7644c396e15dd13600eef1f928f;p=helm.git

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
---

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)