match_coercion gives back the saturations, not the arity:

[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 31768a62dd6ac11e474dca0c2ce997c24c422181..e48e772079b86ef6d0d0eb8fafc9fca6706b3852 100644 (file)
--- 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)
+;;