open Printf;;
type coercion_search_result =
- | SomeCoercion of Cic.term
+ | SomeCoercion of Cic.term list
| NoCoercion
| NotMetaClosed
| NotHandled of string Lazy.t
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion src tgt =
+let look_for_coercion' src tgt =
let arity_of con =
try
let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
(CoercDb.name_of_carr src)
(CoercDb.name_of_carr tgt)));
None
- | [u] ->
+ | _::_ ->
debug_print (lazy (
- sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- Some u
- | u::_ ->
- debug_print (lazy (
- sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
+ sprintf ":-) TROVATE %d coercion(s) da %s a %s"
(List.length l)
(CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- Some u
+ (CoercDb.name_of_carr tgt)));
+ Some l
in
(match uri with
None -> NoCoercion
- | Some u ->
- let c = CicUtil.term_of_uri u in
- let arity = arity_of c in
- let args = mk_implicits (arity - 1) in
- let newt =
- match args with
- [] -> c
- | _ -> Cic.Appl (c::args)
+ | Some ul ->
+ let cl = List.map CicUtil.term_of_uri ul in
+ let funclass_arityl =
+ let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+ List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+ in
+ let arityl = List.map arity_of cl in
+ let argsl =
+ List.map2
+ (fun arity fn_arity ->
+ mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl
in
- SomeCoercion newt)
+ let newtl =
+ List.map2
+ (fun args c ->
+ match args with
+ | [] -> c
+ | _ -> Cic.Appl (c::args))
+ argsl cl
+ in
+ SomeCoercion newtl)
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
let look_for_coercion src tgt =
let src_uri = CoercDb.coerc_carr_of_term src in
let tgt_uri = CoercDb.coerc_carr_of_term tgt in
- look_for_coercion src_uri tgt_uri
+ look_for_coercion' src_uri tgt_uri
let is_a_coercion t =
try
let uri = CicUtil.uri_of_term t in
CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
with Invalid_argument _ -> assert false (* t must be a coercion *)
-
-let target_of t =
+
+let is_a_coercion_to_funclass t =
try
let uri = CicUtil.uri_of_term t in
- CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
- with Invalid_argument _ -> assert false (* t must be a coercion *)
-
+ match snd (CoercDb.get_carr uri) with
+ | CoercDb.Fun i -> Some i
+ | _ -> None
+ with Invalid_argument _ -> None
+
let generate_dot_file () =
+ 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 l = CoercDb.to_list () in
- let preamble = "
- digraph pippo {
- node [fontsize=9, width=.4, height=.4];
- edge [fontsize=10];
- \n"
- in
- let conclusion = " } \n" in
- let data = List.fold_left
- (fun acc (src,tgt,c) ->
- acc ^ CoercDb.name_of_carr src ^ " -> " ^
- CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^
- "\"];\n") "" l
- in
- preamble ^ data ^ conclusion
-
+ let pp_description carr =
+ match CoercDb.uri_of_carr carr with
+ | None -> ()
+ | Some uri ->
+ Pp.node (CoercDb.name_of_carr carr)
+ ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ List.iter
+ (fun (src, tgt, cl) ->
+ let src_name = CoercDb.name_of_carr src in
+ let tgt_name = CoercDb.name_of_carr tgt in
+ pp_description src;
+ pp_description tgt;
+ List.iter
+ (fun c ->
+ Pp.edge src_name tgt_name
+ ~attrs:[ "label", UriManager.name_of_uri c;
+ "href", UriManager.string_of_uri c ]
+ fmt)
+ cl)
+ l;
+ Pp.trailer fmt;
+ Buffer.contents buf
+;;
+
+let is_composite t =
+ try
+ let uri =
+ match t with
+ | Cic.Appl (he::_) -> CicUtil.uri_of_term he
+ | _ -> CicUtil.uri_of_term t
+ in
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | Cic.Constant (_,_, _, _, attrs),_ ->
+ List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
+ | _ -> false
+ with Invalid_argument _ -> false
+;;
+
(* EOF *)