+
+(* CSC: very inefficient implementation!
+ Enrico, can we use a discrimination tree here? *)
+let match_coercion status ~metasenv ~subst ~context t =
+ let db =
+ DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
+ in
+ (HExtlib.list_findopt
+ (fun (_,p,arity,cpos,_,_) _ ->
+ try
+ let t =
+ match p,t with
+ NCic.Appl lp, NCic.Appl lt ->
+ (match fst (HExtlib.split_nth (List.length lp) lt) with
+ [t] -> t
+ | l -> NCic.Appl l)
+ | _,NCic.Appl (he::_) -> he
+ | _,_ -> t
+ in
+ let b = NCicReduction.alpha_eq metasenv subst context p t in
+ if not b then None else
+ let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
+ let pis =
+ let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
+ aux ty
+ in
+ Some (p,pis - arity - cpos - 1,cpos)
+ with
+ Failure _ -> None (* raised by split_nth *)
+ ) db)
+;;
+
+let generate_dot_file status fmt =
+ let module Pp = GraphvizPp.Dot in
+ let src_db, _ = status#coerc_db in
+ let edges = ref [] in
+ DB.iter src_db (fun _ dataset ->
+ edges := !edges @
+ List.map
+ (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);
+ );
+ 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 ((name,_,_,_),src,tgt) ->
+ Pp.edge (mangle src) (mangle tgt)
+ ~attrs:["label", name] fmt)
+ !edges;
+;;