let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;
-module COT : Set.OrderedType with type t = NCic.term * int * int * NCic.term *
+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 =
struct
- type t = NCic.term * int * int * NCic.term * NCic.term
- let compare = Pervasives.compare
+ type t = string * NCic.term * int * int * NCic.term * NCic.term
+ let compare = Pervasives.compare
end
module CoercionSet = Set.Make(COT)
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 c src tgt arity arg =
+let index_coercion status name c src tgt arity arg =
let db_src,db_tgt = status#coerc_db in
- let data = (c,arity,arg,src,tgt) in
-
- let debug s = prerr_endline (Lazy.force s) 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
NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
assert false
in
- index_coercion status c src tgt arity arg
+ index_coercion status "foo" c src tgt arity arg
with
| NCicEnvironment.BadDependency _
| NCicTypeChecker.TypeCheckerFailure _ -> status)
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: " ^
- String.concat "," (List.map (fun (t,_,_,_,_) ->
- NCicPp.ppterm ~metasenv ~subst ~context t)
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
(CoercionSet.elements candidates))));
List.map
- (fun (t,arity,arg,_,_) ->
+ (fun (name,t,arity,arg,_,_) ->
let ty =
try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
with NCicTypeChecker.TypeCheckerFailure s ->
(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)
+ name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
(CoercionSet.elements candidates)
;;
DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
in
(HExtlib.list_findopt
- (fun (p,arity,cpos,_,_) _ ->
+ (fun (_,p,arity,cpos,_,_) _ ->
try
let t =
match p,t with
) db)
;;
-let generate_dot_file status =
+let generate_dot_file status fmt =
let module Pp = GraphvizPp.Dot in
- let buf = Buffer.create 10240 in
- let fmt = Format.formatter_of_buffer buf in
- Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
- ~edge_attrs:["fontsize", "10"] fmt;
let src_db, _ = status#coerc_db in
let edges = ref [] in
DB.iter src_db (fun _ dataset ->
edges := !edges @
List.map
- (fun (t,a,g,sk,dk) ->
- prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
- ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk);
- let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in
- let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in
- (t,a,g),eq_s,eq_t
+ (fun (name,t,a,g,sk,dk) ->
+ debug(lazy (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
+ ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
+ let eq_s= sk::NCicUnifHint.eq_class_of status sk in
+ let eq_t= dk::NCicUnifHint.eq_class_of status dk in
+ (name,t,a,g),eq_s,eq_t
)
(CoercionSet.elements dataset);
);
fmt)
nodes;
List.iter
- (fun ((t,a,b),src,tgt) ->
+ (fun ((name,_,_,_),src,tgt) ->
Pp.edge (mangle src) (mangle tgt)
- ~attrs:["label",
- NCicPp.ppterm ~metasenv:[]
- ~subst:[] ~context:[] t] fmt)
+ ~attrs:["label", name] fmt)
!edges;
- Pp.trailer fmt;
- Buffer.contents buf
;;
projects / helm.git / blobdiff