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:" ^
*)
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 =
NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
assert false
in
- 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 empty_db = (DB.empty,DB.empty) ;;
-
-
-let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
+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 _::_)) -> []