let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;
-module COT : Set.OrderedType with type t = NCic.term * int * int =
+module COT : Set.OrderedType with type t = NCic.term * int * int * NCic.term *
+NCic.term =
struct
- type t = NCic.term * int * int
+ type t = NCic.term * int * int * NCic.term * NCic.term
let compare = Pervasives.compare
end
class status =
object
+ inherit NCicUnifHint.status
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 >}
+ : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status ->
+ 'self
+ = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
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
+ let data = (c,arity,arg,src,tgt) in
+ let debug s = prerr_endline (Lazy.force s) in
debug (lazy ("INDEX:" ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
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 src_class = infty :: NCicUnifHint.eq_class_of status infty in
+ let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
+
+ let set_src =
+ List.fold_left
+ (fun set infty ->
+ CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
+ CoercionSet.empty src_class
+ in
+ let set_tgt =
+ List.fold_left
+ (fun set expty ->
+ CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
+ CoercionSet.empty tgt_class
+ in
let candidates = CoercionSet.inter set_src set_tgt in
debug (lazy ("CANDIDATES: " ^
- String.concat "," (List.map (fun (t,_,_) ->
+ String.concat "," (List.map (fun (t,_,_,_,_) ->
NCicPp.ppterm ~metasenv ~subst ~context t)
(CoercionSet.elements candidates))));
List.map
- (fun (t,arity,arg) ->
+ (fun (t,arity,arg,_,_) ->
let ty =
try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
with NCicTypeChecker.TypeCheckerFailure s ->
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
Failure _ -> None (* raised by split_nth *)
) db)
;;
+
+let generate_dot_file status =
+ 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
+ )
+ (CoercionSet.elements dataset);
+ );
+ let nodes =
+ HExtlib.list_uniq
+ (List.sort compare
+ (List.flatten
+ (List.map
+ (fun (_,a,b) ->
+ [a;b]
+ )
+ !edges)))
+ in
+ let names = ref [] in
+ let id = ref 0 in
+ let mangle l =
+ try List.assoc l !names
+ with Not_found ->
+ incr id;
+ names := (l,"node"^string_of_int!id) :: !names;
+ List.assoc l !names
+ in
+ List.iter
+ (fun cl ->
+ Pp.node (mangle cl)
+ ~attrs:["label",String.concat "\\n"
+ (List.map (fun t->
+ NCicPp.ppterm ~metasenv:[] ~subst:[]
+ ~context:[] t ~margin:max_int
+ ) cl)]
+ fmt)
+ nodes;
+ List.iter
+ (fun ((t,a,b),src,tgt) ->
+ Pp.edge (mangle src) (mangle tgt)
+ ~attrs:["label",
+ NCicPp.ppterm ~metasenv:[]
+ ~subst:[] ~context:[] t] fmt)
+ !edges;
+ Pp.trailer fmt;
+ Buffer.contents buf
+;;