X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=29fe0fd540d48924dd06a8b52c319cc9497848bb;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=b8f31c805e18c414c1b1f85c5bdde2043ee86b70;hpb=002d456397be2f0046bb50356e80816f7296647d;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index b8f31c805..29fe0fd54 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -24,57 +24,101 @@ module DB =
 
 type db = DB.t * DB.t
 
-let index_coercion (db_src,db_tgt) c src tgt arity arg =
+let empty_db = DB.empty,DB.empty
+
+class status =
+ object
+  val db = empty_db
+  method coerc_db = db
+  method set_coerc_db v = {< db = v >}
+  method set_coercion_status
+   : 'status. < coerc_db : db; .. > as 'status -> 'self
+   = fun o -> {< db = o#coerc_db >}
+ end
+
+let index_coercion status c src tgt arity arg =
+  let db_src,db_tgt = status#coerc_db in
   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
+  status#set_coerc_db (db_src, db_tgt)
 ;;
 
-let db () =
+let index_old_db odb (status : #status) =
   List.fold_left 
-    (fun db (_,tgt,clist) -> 
+    (fun status (_,tgt,clist) -> 
        List.fold_left 
-         (fun db (uri,_,arg) ->
+         (fun status (uri,_,arg) ->
+           try
             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
             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 ())
+            index_coercion status c src tgt arity arg
+           with 
+           | NCicEnvironment.BadDependency _ 
+           | NCicTypeChecker.TypeCheckerFailure _ -> status)
+         status clist)
+    status (CoercDb.to_list odb)
 ;;
 
-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
-  prerr_endline "aaaaaaaaaaaaa";
-  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)
+let look_for_coercion status metasenv subst context infty expty =
+ let db_src,db_tgt = status#coerc_db in
+  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)
 ;;