X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=e48e772079b86ef6d0d0eb8fafc9fca6706b3852;hb=942ec766879070892420f6297b5c078c1582b78d;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..e48e77207 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,34 @@ 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
+    (HExtlib.list_findopt
+      (fun (p,arity,cpos) _ ->
+        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
+         let b = NCicReduction.alpha_eq metasenv subst context p t in
+         if not b then None else
+         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
+         let pis = 
+           let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
+           aux ty
+         in
+         Some (p,pis - arity - cpos - 1,cpos)
+        with
+         Failure _ -> None (* raised by split_nth *)
+      ) db)
+;;