let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;
+let convert_term = ref (fun _ _ -> assert false);;
+let set_convert_term f = convert_term := f;;
+
module COT : Set.OrderedType
with type t = string * NCic.term * int * int * NCic.term *
NCic.term =
let empty_db = DB.empty,DB.empty
+class type g_status =
+ object
+ inherit NCicUnifHint.g_status
+ method coerc_db: db
+ end
+
class status =
object
inherit NCicUnifHint.status
method coerc_db = db
method set_coerc_db v = {< db = v >}
method set_coercion_status
- : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status ->
- 'self
- = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
end
let index_coercion status name c src tgt arity arg =
let db_src,db_tgt = status#coerc_db in
let data = (name,c,arity,arg,src,tgt) in
-
debug (lazy ("INDEX:" ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
string_of_int arg ^ " " ^ string_of_int arity));
-
let db_src = DB.index db_src src data in
let db_tgt = DB.index db_tgt tgt data in
status#set_coerc_db (db_src, db_tgt)
List.fold_left
(fun status (uri,_,arg) ->
try
- let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
+ let c=fst (!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
let look_for_coercion status metasenv subst context infty expty =
let db_src,db_tgt = status#coerc_db in
- match infty, expty with
+ match
+ NCicUntrusted.apply_subst subst context infty,
+ NCicUntrusted.apply_subst subst context expty
+ with
| (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
(NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
- | _ ->
+ | infty, expty ->
debug (lazy ("LOOK FOR COERCIONS: " ^
NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
CoercionSet.empty tgt_class
in
+
+ debug (lazy ("CANDIDATES SRC: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements set_src))));
+ debug (lazy ("CANDIDATES TGT: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements set_tgt))));
+
let candidates = CoercionSet.inter set_src set_tgt in
debug (lazy ("CANDIDATES: " ^