The function exists_a_meta has been modified to capture also

[helm.git] / components / cic_unification / cicUnification.ml

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 437d541ea3617a66d77e3b311bd186fe8bfecc2f..8ba0ae917c828e807d85980acdb0a6a560a77718 100644 (file)
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -74,7 +74,11 @@ in profiler_toa.HExtlib.profile foo ()
 ;;
 
 let exists_a_meta l = 
-  List.exists (function Cic.Meta _ -> true | _ -> false) l
+  List.exists 
+    (function 
+       | Cic.Meta _  
+       | Cic.Appl (Cic.Meta _::_) -> true
+       | _ -> false) l
 
 let rec deref subst t =
   let snd (_,a,_) = a in
@@ -457,18 +461,19 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
           (sprintf
             "Can't unify %s with %s due to different constants"
             (CicMetaSubst.ppterm subst t1) 
-            (CicMetaSubst.ppterm subst t2)))) 
+            (CicMetaSubst.ppterm subst t2))))
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 then
          fo_unif_subst_exp_named_subst 
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure (lazy "4"))
-           (* (sprintf
-              "Can't unify %s with %s due to different inductive principles"
-              (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2))) *)
+         raise (UnificationFailure
+           (lazy
+            (sprintf
+             "Can't unify %s with %s due to different inductive principles"
+             (CicMetaSubst.ppterm subst t1) 
+             (CicMetaSubst.ppterm subst t2))))
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
@@ -476,11 +481,12 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure (lazy "5"))
-           (* (sprintf
+         raise (UnificationFailure
+          (lazy
+            (sprintf
               "Can't unify %s with %s due to different inductive constructors"
               (CicMetaSubst.ppterm subst t1) 
-              (CicMetaSubst.ppterm subst t2))) *)
+              (CicMetaSubst.ppterm subst t2))))
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                               subst context metasenv te t2 ugraph
@@ -578,13 +584,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                 fo_unif_l 
                   test_equality_only subst metasenv (lr1, lr2)  ugraph
               with 
-              | UnificationFailure _
-              | Uncertain _ as exn -> 
+              | UnificationFailure s
+              | Uncertain s as exn -> 
                   (match l1, l2 with
                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
                     CoercGraph.is_a_coercion c1 && 
-                    CoercGraph.is_a_coercion c2 ->
+                    CoercGraph.is_a_coercion c2 &&
+                    not (UriManager.eq uri1 uri2) ->
                       let body1, attrs1, ugraph = 
                         match CicEnvironment.get_obj ugraph uri1 with
                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
@@ -596,9 +603,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                         | _ -> assert false
                       in
                       let is_composite1 = 
-                        List.exists ((=) (`Class `Coercion)) attrs1 in
+                        List.exists 
+                         (function `Class (`Coercion _) -> true | _-> false) 
+                         attrs1 
+                      in
                       let is_composite2 = 
-                        List.exists ((=) (`Class `Coercion)) attrs2 in
+                        List.exists 
+                         (function `Class (`Coercion _) -> true | _-> false) 
+                         attrs2 
+                      in
                       (match is_composite1, is_composite2 with
                       | false, false -> raise exn
                       | true, false ->
@@ -625,6 +638,30 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                           fo_unif_subst 
                             test_equality_only subst context metasenv 
                              redappl1 redappl2 ugraph)
+                  (*CSC: This is necessary because of the "elim H" tactic
+                         where the type of H is only reducible to an
+                         inductive type. This could be extended from inductive
+                         types to any rigid term. However, the code is
+                         duplicated in two places: inside applications and
+                         outside them. Probably it would be better to
+                         work with lambda-bar terms instead. *)
+                  | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+                  | (_, Cic.MutInd _::_) ->
+                     let t1' = R.whd ~subst context t1 in
+                     (match t1' with
+                          C.Appl (C.MutInd _::_) -> 
+                            fo_unif_subst test_equality_only 
+                              subst context metasenv t1' t2 ugraph         
+                        | _ -> raise (UnificationFailure (lazy "88")))
+                  | (Cic.MutInd _::_,_) ->
+                     let t2' = R.whd ~subst context t2 in
+                     (match t2' with
+                          C.Appl (C.MutInd _::_) -> 
+                            fo_unif_subst test_equality_only 
+                              subst context metasenv t1 t2' ugraph         
+                        | _ -> raise 
+                           (UnificationFailure 
+                              (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 ))))
                   | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
@@ -669,6 +706,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        in
          fo_unif_subst test_equality_only subst context metasenv 
            beta_expanded (C.Meta (i,l)) ugraph1
+(* Works iff there are no arguments applied to it; similar to the
+   case below
+   | (_, C.MutInd _) ->
+       let t1' = R.whd ~subst context t1 in
+       (match t1' with
+            C.MutInd _ -> 
+              fo_unif_subst test_equality_only 
+                subst context metasenv t1' t2 ugraph         
+          | _ -> raise (UnificationFailure (lazy "8")))
+*)
 (* The following idea could be exploited again; right now we have no
    longer any example requiring it
    | (C.Prod _, t2) ->