X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=5e121ccfcb12c89595a051fe04758f1743203f9a;hb=6f2f9693db45a2ef905123bc48cde9f04ddff54f;hp=31768a62dd6ac11e474dca0c2ce997c24c422181;hpb=72cd94b68037956a70b98cfa54f316fd54e52bae;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 31768a62d..5e121ccfc 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -114,7 +114,13 @@ let look_for_coercion status metasenv subst context infty expty =
 
     List.map
       (fun (t,arity,arg) ->
-          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
+          let ty =
+            try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
+            with NCicTypeChecker.TypeCheckerFailure s ->
+             prerr_endline ("illtyped coercion: "^Lazy.force s);
+             prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+             assert false
+          in
           let ty, metasenv, args = 
            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
           in
@@ -128,3 +134,31 @@ let look_for_coercion status metasenv subst context infty expty =
           metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
       (CoercionSet.elements candidates)
 ;;
+
+(* CSC: very inefficient implementation!
+   Enrico, can we use a discrimination tree here? *)
+let match_coercion status ~metasenv ~subst ~context t =
+ let db =
+  DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
+ in
+  try
+   Some
+    (List.find
+      (fun (p,_,_) ->
+        try
+         let t =
+          match p,t with
+             NCic.Appl lp, NCic.Appl lt ->
+              (match fst (HExtlib.split_nth (List.length lp) lt) with
+                  [t] -> t
+                | l -> NCic.Appl l)
+           | _,NCic.Appl (he::_) -> he
+           | _,_ -> t
+         in
+          NCicReduction.alpha_eq metasenv subst context p t
+        with
+         Failure _ -> false (* raised by split_nth *)
+      ) db)
+  with
+   Not_found -> None
+;;