Coercion hiding implemented. Notes:

[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 8a6e8a1c818f5f19a99ff816531a19eb9f3561fc..5e121ccfcb12c89595a051fe04758f1743203f9a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -134,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
+;;