better coercions indexing and lookup

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 5c79aa95c30a975fc9b333ba2065591c4648cb0b..f2467605f085731d456816feb325ca2e30e4b56a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -26,6 +26,12 @@ type db = DB.t * DB.t
 
 let index_coercion (db_src,db_tgt) c src tgt arity arg =
   let data = (c,arity,arg) in
+(*
+  prerr_endline ("INDEX:" ^ 
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
+*)
   let db_src = DB.index db_src src data in
   let db_tgt = DB.index db_tgt tgt data in
   db_src, db_tgt
@@ -40,40 +46,61 @@ let db () =
             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
             let src, tgt = 
               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
-              match 
-               NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
-              with
-              | NCic.Prod (_, src, tgt),_,_ -> 
-                src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt 
-              | t,metasenv,_ -> 
+              let scty, metasenv,_ = 
+                NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
+              in
+              match scty with
+              | NCic.Prod (_, src, tgt) -> 
+                 let tgt =
+                   NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
+                 in
+(*
+            prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s" 
+              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
+              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
+              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
+*)
+                src, tgt
+              | t -> 
                   prerr_endline (
                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
                   assert false
             in
-(*
-            prerr_endline (Printf.sprintf "indicizzo %s %d %d" 
-              (UriManager.string_of_uri uri) arity arg);
-*)
             index_coercion db c src tgt arity arg)
          db clist)
     (DB.empty,DB.empty) (CoercDb.to_list ())
 ;;
 
 let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
-  let set_src = DB.retrieve_unifiables db_src infty in
-  let set_tgt = DB.retrieve_unifiables db_tgt expty in
-  let candidates = CoercionSet.inter set_src set_tgt in
-  List.map
-    (fun (t,arity,arg) ->
-        let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
-        let ty, metasenv, args = 
-          NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
-        in
-(*       prerr_endline (
-          NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
-          NCicPp.ppterm ~metasenv ~subst ~context
-          (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
-            string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
-        metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
-    (CoercionSet.elements candidates)
+  match infty, expty with
+  | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
+    (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
+  | _ ->
+(*
+    prerr_endline ("LOOK FOR COERCIONS: " ^ 
+      NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
+      NCicPp.ppterm ~metasenv ~subst ~context expty);
+*)
+    let set_src = DB.retrieve_unifiables db_src infty in
+    let set_tgt = DB.retrieve_unifiables db_tgt expty in
+    let candidates = CoercionSet.inter set_src set_tgt in
+(*
+    prerr_endline ("CANDIDATES: " ^ 
+      String.concat "," (List.map (fun (t,_,_) ->
+        NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements candidates)));
+*)
+    List.map
+      (fun (t,arity,arg) ->
+          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
+          let ty, metasenv, args = 
+           NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
+          in
+  (*       prerr_endline (
+            NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
+            NCicPp.ppterm ~metasenv ~subst ~context
+            (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
+              string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
+          metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
+      (CoercionSet.elements candidates)
 ;;