X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Flibrary%2FcoercGraph.ml;h=99ba33c33502c5f56f549d1bff2d716a103f7f4c;hb=213cc7cf3c9da7c024b44b54e07035b831f7a31f;hp=62a89b0a71ea36ed8b5ad3b48912a1c7af8616a9;hpb=9393a9f9370014c904244358abe4ec6e11a9d158;p=helm.git diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml index 62a89b0a7..99ba33c33 100644 --- a/components/library/coercGraph.ml +++ b/components/library/coercGraph.ml @@ -28,7 +28,7 @@ open Printf;; type coercion_search_result = - | SomeCoercion of Cic.term + | SomeCoercion of Cic.term list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t @@ -37,35 +37,65 @@ let debug = false 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 + let rec count_pi = function + | Cic.Prod (_,_,t) -> 1 + count_pi t + | _ -> 0 + in + count_pi ty + with Invalid_argument _ -> assert false (* all coercions have an uri *) + in + let rec mk_implicits = function + | 0 -> [] + | n -> Cic.Implicit None :: mk_implicits (n-1) + in try let l = CoercDb.find_coercion - (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) + (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in + let uri = + match l with + | [] -> + debug_print + (lazy + (sprintf ":-( coercion non trovata da %s a %s" + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + None + | _::_ -> + debug_print (lazy ( + sprintf ":-) TROVATE %d coercion(s) da %s a %s" + (List.length l) + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + Some l in - match l with - | [] -> - debug_print - (lazy - (sprintf ":-( coercion non trovata da %s a %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); - NoCoercion - | [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))); - SomeCoercion (CicUtil.term_of_uri u) - | u::_ -> - debug_print (lazy ( - sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" - (List.length l) - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - SomeCoercion (CicUtil.term_of_uri u) + (match uri with + None -> NoCoercion + | 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 + 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 @@ -74,7 +104,7 @@ let look_for_coercion src tgt = 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 @@ -87,28 +117,58 @@ let source_of t = 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 *)